Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param omega^omega : ι
Param mul_nat^mul_nat : ι → ι → ι
Param ordsucc^ordsucc : ι → ι
Definition even_nat^even_nat := λ x0 . and (x0 ∈ omega) (∀ x1 : ο . (∀ x2 . and (x2 ∈ omega) (x0 = mul_nat 2 x2) ⟶ x1) ⟶ x1)
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition odd_nat^odd_nat := λ x0 . and (x0 ∈ omega) (∀ x1 . x1 ∈ omega ⟶ x0 = mul_nat 2 x1 ⟶ ∀ x2 : ο . x2)
Known even_nat_not_odd_nat^{even_nat_not_odd_nat} : ∀ x0 . even_nat x0 ⟶ not (odd_nat x0)
Param nat_p^nat_p : ι → ο
Known even_nat_double^{even_nat_double} : ∀ x0 . nat_p x0 ⟶ even_nat (mul_nat 2 x0)
Param exactly1of2^exactly1of2 : ο → ο → ο
Known even_nat_xor_S^{even_nat_xor_S} : ∀ x0 . nat_p x0 ⟶ exactly1of2 (even_nat x0) (even_nat (ordsucc x0))
Param mul_SNo^mul_SNo : ι → ι → ι
Known mul_nat_mul_SNo^{mul_nat_mul_SNo} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ mul_nat x0 x1 = mul_SNo x0 x1
Known nat_p_omega^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Known nat_2^nat_2 : nat_p 2
Param SNo^SNo : ι → ο
Known mul_SNo_oneL^mul_SNo_oneL : ∀ x0 . SNo x0 ⟶ mul_SNo 1 x0 = x0
Known nat_p_SNo^nat_p_SNo : ∀ x0 . nat_p x0 ⟶ SNo x0
Param eps_^eps_ : ι → ι
Known eps_1_half_eq3^{eps_1_half_eq3} : mul_SNo (eps_ 1) 2 = 1
Known mul_SNo_assoc^{mul_SNo_assoc} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ mul_SNo x0 (mul_SNo x1 x2) = mul_SNo (mul_SNo x0 x1) x2
Known SNo_eps_^SNo_eps_ : ∀ x0 . x0 ∈ omega ⟶ SNo (eps_ x0)
Known nat_1^nat_1 : nat_p 1
Theorem double_nat_cancel^{double_nat_cancel} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ mul_nat 2 x0 = mul_nat 2 x1 ⟶ x0 = x1 (proof)
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known nat_0^nat_0 : nat_p 0
Known mul_nat_0R^mul_nat_0R : ∀ x0 . mul_nat x0 0 = 0
Theorem even_nat_0^even_nat_0 : even_nat 0 (proof)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known nat_ind^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known exactly1of2_E^{exactly1of2_E} : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ not x1 ⟶ x2) ⟶ (not x0 ⟶ x1 ⟶ x2) ⟶ x2
Known omega_ordsucc^{omega_ordsucc} : ∀ x0 . x0 ∈ omega ⟶ ordsucc x0 ∈ omega
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Theorem even_nat_or_odd_nat^{even_nat_or_odd_nat} : ∀ x0 . nat_p x0 ⟶ or (even_nat x0) (odd_nat x0) (proof)
Theorem not_odd_nat_0^{not_odd_nat_0} : not (odd_nat 0) (proof)
Known omega_nat_p^omega_nat_p : ∀ x0 . x0 ∈ omega ⟶ nat_p x0
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Theorem even_nat_odd_nat_S^{even_nat_odd_nat_S} : ∀ x0 . even_nat x0 ⟶ odd_nat (ordsucc x0) (proof)
Theorem odd_nat_even_nat_S^{odd_nat_even_nat_S} : ∀ x0 . odd_nat x0 ⟶ even_nat (ordsucc x0) (proof)
Param add_nat^add_nat : ι → ι → ι
Known add_nat_0R^add_nat_0R : ∀ x0 . add_nat x0 0 = x0
Known exactly1of2_I2^{exactly1of2_I2} : ∀ x0 x1 : ο . not x0 ⟶ x1 ⟶ exactly1of2 x0 x1
Known add_nat_SR^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known add_nat_p^add_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (add_nat x0 x1)
Known exactly1of2_I1^{exactly1of2_I1} : ∀ x0 x1 : ο . x0 ⟶ not x1 ⟶ exactly1of2 x0 x1
Theorem odd_nat_xor_odd_sum^{odd_nat_xor_odd_sum} : ∀ x0 . odd_nat x0 ⟶ ∀ x1 . nat_p x1 ⟶ exactly1of2 (odd_nat x1) (odd_nat (add_nat x0 x1)) (proof)
Param iff^iff : ο → ο → ο
Known iff_refl^iff_refl : ∀ x0 : ο . iff x0 x0
Known mul_nat_SR^mul_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ mul_nat x0 (ordsucc x1) = add_nat x0 (mul_nat x0 x1)
Known iffI^iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Known mul_nat_p^mul_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (mul_nat x0 x1)
Known iffER^iffER : ∀ x0 x1 : ο . iff x0 x1 ⟶ x1 ⟶ x0
Known iffEL^iffEL : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 ⟶ x1
Theorem odd_nat_iff_odd_mul_nat^{odd_nat_iff_odd_mul_nat} : ∀ x0 . odd_nat x0 ⟶ ∀ x1 . nat_p x1 ⟶ iff (odd_nat x1) (odd_nat (mul_nat x0 x1)) (proof)
Theorem odd_nat_mul_nat^{odd_nat_mul_nat} : ∀ x0 x1 . odd_nat x0 ⟶ odd_nat x1 ⟶ odd_nat (mul_nat x0 x1) (proof)
Known nat_inv^nat_inv : ∀ x0 . nat_p x0 ⟶ or (x0 = 0) (∀ x1 : ο . (∀ x2 . and (nat_p x2) (x0 = ordsucc x2) ⟶ x1) ⟶ x1)
Known neq_ordsucc_0^{neq_ordsucc_0} : ∀ x0 . ordsucc x0 = 0 ⟶ ∀ x1 : ο . x1
Known add_nat_SL^add_nat_SL : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ add_nat (ordsucc x0) x1 = ordsucc (add_nat x0 x1)
Theorem add_nat_0_inv^{add_nat_0_inv} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ add_nat x0 x1 = 0 ⟶ and (x0 = 0) (x1 = 0) (proof)
Theorem mul_nat_0_inv^{mul_nat_0_inv} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ mul_nat x0 x1 = 0 ⟶ or (x0 = 0) (x1 = 0) (proof)
Known mul_nat_1R^mul_nat_1R : ∀ x0 . mul_nat x0 1 = x0
Known In_1_2^In_1_2 : 1 ∈ 2
Known add_nat_0L^add_nat_0L : ∀ x0 . nat_p x0 ⟶ add_nat 0 x0 = x0
Param ordinal^ordinal : ι → ο
Known ordinal_ordsucc_In^{ordinal_ordsucc_In} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ ordsucc x0
Known nat_p_ordinal^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Theorem ordsucc_in_double_nat_ordsucc^{ordsucc_in_double_nat_ordsucc} : ∀ x0 . nat_p x0 ⟶ ordsucc x0 ∈ mul_nat 2 (ordsucc x0) (proof)
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Theorem double_nat_Subq_0^{double_nat_Subq_0} : ∀ x0 . nat_p x0 ⟶ mul_nat 2 x0 ⊆ x0 ⟶ x0 = 0 (proof)
Known Subq_ref^Subq_ref : ∀ x0 . x0 ⊆ x0
Known Subq_tra^Subq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Theorem add_nat_Subq_L^{add_nat_Subq_L} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ x0 ⊆ add_nat x0 x1 (proof)
Known Empty_Subq_eq^{Empty_Subq_eq} : ∀ x0 . x0 ⊆ 0 ⟶ x0 = 0
Known ordinal_In_Or_Subq^{ordinal_In_Or_Subq} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (x0 ∈ x1) (x1 ⊆ x0)
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Known ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Known nat_trans^nat_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Known mul_nat_SL^mul_nat_SL : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ mul_nat (ordsucc x0) x1 = add_nat (mul_nat x0 x1) x1
Known add_nat_com^add_nat_com : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ add_nat x0 x1 = add_nat x1 x0
Theorem square_nat_Subq^{square_nat_Subq} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ x0 ⊆ x1 ⟶ mul_nat x0 x0 ⊆ mul_nat x1 x1 (proof)
Known nat_complete_ind^{nat_complete_ind} : ∀ x0 : ι → ο . (∀ x1 . nat_p x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Known mul_nat_asso^mul_nat_asso : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . nat_p x2 ⟶ mul_nat (mul_nat x0 x1) x2 = mul_nat x0 (mul_nat x1 x2)
Known mul_nat_com^mul_nat_com : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ mul_nat x0 x1 = mul_nat x1 x0
Theorem form100_1_v1_lem^{form100_1_v1_lem} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ mul_nat x0 x0 = mul_nat 2 (mul_nat x1 x1) ⟶ x1 = 0 (proof)
Param setminus^setminus : ι → ι → ι
Known setminusE^setminusE : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ and (x2 ∈ x0) (nIn x2 x1)
Known In_0_1^In_0_1 : 0 ∈ 1
Theorem form100_1_v1^form100_1_v1 : ∀ x0 . x0 ∈ setminus omega 1 ⟶ ∀ x1 . x1 ∈ setminus omega 1 ⟶ mul_nat x0 x0 = mul_nat 2 (mul_nat x1 x1) ⟶ ∀ x2 : ο . x2 (proof)

Proofgold Address