Proofgold Address

Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Definition nSubq^nSubq := λ x0 x1 . not (x0 ⊆ x1)
Param ordsucc^ordsucc : ι → ι
Known neq_0_ordsucc^{neq_0_ordsucc} : ∀ x0 . 0 = ordsucc x0 ⟶ ∀ x1 : ο . x1
Theorem neq_0_1^neq_0_1 : 0 = 1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_0_2^neq_0_2 : 0 = 2 ⟶ ∀ x0 : ο . x0 (proof)
Known ordsucc_inj_contra^{ordsucc_inj_contra} : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ ordsucc x0 = ordsucc x1 ⟶ ∀ x2 : ο . x2
Theorem neq_1_2^neq_1_2 : 1 = 2 ⟶ ∀ x0 : ο . x0 (proof)
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known EmptyE^EmptyE : ∀ x0 . nIn x0 0
Theorem nIn_0_0^nIn_0_0 : nIn 0 0 (proof)
Theorem nIn_1_0^nIn_1_0 : nIn 1 0 (proof)
Theorem nIn_2_0^nIn_2_0 : nIn 2 0 (proof)
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Theorem nIn_1_1^nIn_1_1 : nIn 1 1 (proof)
Theorem nIn_2_2^nIn_2_2 : nIn 2 2 (proof)
Known Subq_Empty^Subq_Empty : ∀ x0 . 0 ⊆ x0
Theorem Subq_0_0^Subq_0_0 : 0 ⊆ 0 (proof)
Theorem Subq_0_1^Subq_0_1 : 0 ⊆ 1 (proof)
Theorem Subq_0_2^Subq_0_2 : 0 ⊆ 2 (proof)
Known In_0_1^In_0_1 : 0 ∈ 1
Theorem nSubq_1_0^nSubq_1_0 : nSubq 1 0 (proof)
Known Subq_ref^Subq_ref : ∀ x0 . x0 ⊆ x0
Theorem Subq_1_1^Subq_1_1 : 1 ⊆ 1 (proof)
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Theorem Subq_1_2^Subq_1_2 : 1 ⊆ 2 (proof)
Known In_0_2^In_0_2 : 0 ∈ 2
Theorem nSubq_2_0^nSubq_2_0 : nSubq 2 0 (proof)
Known In_1_2^In_1_2 : 1 ∈ 2
Theorem nSubq_2_1^nSubq_2_1 : nSubq 2 1 (proof)
Theorem Subq_2_2^Subq_2_2 : 2 ⊆ 2 (proof)
Param nat_p^nat_p : ι → ο
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 set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Known UnionE_impred^{UnionE_impred} : ∀ x0 x1 . x1 ∈ prim3 x0 ⟶ ∀ x2 : ο . (∀ x3 . x1 ∈ x3 ⟶ x3 ∈ x0 ⟶ x2) ⟶ x2
Known nat_ordsucc_trans^{nat_ordsucc_trans} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ ordsucc x0 ⟶ x1 ⊆ x0
Known UnionI^UnionI : ∀ x0 x1 x2 . x1 ∈ x2 ⟶ x2 ∈ x0 ⟶ x1 ∈ prim3 x0
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Known Union_ordsucc_eq^{Union_ordsucc_eq} : ∀ x0 . nat_p x0 ⟶ prim3 (ordsucc x0) = x0
Theorem In_0_3^In_0_3 : 0 ∈ 3 (proof)
Theorem In_1_3^In_1_3 : 1 ∈ 3 (proof)
Theorem In_2_3^In_2_3 : 2 ∈ 3 (proof)
Theorem In_0_4^In_0_4 : 0 ∈ 4 (proof)
Theorem In_1_4^In_1_4 : 1 ∈ 4 (proof)
Theorem In_2_4^In_2_4 : 2 ∈ 4 (proof)
Theorem In_3_4^In_3_4 : 3 ∈ 4 (proof)
Theorem In_0_5^In_0_5 : 0 ∈ 5 (proof)
Theorem In_1_5^In_1_5 : 1 ∈ 5 (proof)
Theorem In_2_5^In_2_5 : 2 ∈ 5 (proof)
Theorem In_3_5^In_3_5 : 3 ∈ 5 (proof)
Theorem In_4_5^In_4_5 : 4 ∈ 5 (proof)
Theorem In_0_6^In_0_6 : 0 ∈ 6 (proof)
Theorem In_1_6^In_1_6 : 1 ∈ 6 (proof)
Theorem In_2_6^In_2_6 : 2 ∈ 6 (proof)
Theorem In_3_6^In_3_6 : 3 ∈ 6 (proof)
Theorem In_4_6^In_4_6 : 4 ∈ 6 (proof)
Theorem In_5_6^In_5_6 : 5 ∈ 6 (proof)
Theorem In_0_7^In_0_7 : 0 ∈ 7 (proof)
Theorem In_1_7^In_1_7 : 1 ∈ 7 (proof)
Theorem In_2_7^In_2_7 : 2 ∈ 7 (proof)
Theorem In_3_7^In_3_7 : 3 ∈ 7 (proof)
Theorem In_4_7^In_4_7 : 4 ∈ 7 (proof)
Theorem In_5_7^In_5_7 : 5 ∈ 7 (proof)
Theorem In_6_7^In_6_7 : 6 ∈ 7 (proof)
Theorem In_0_8^In_0_8 : 0 ∈ 8 (proof)
Theorem In_1_8^In_1_8 : 1 ∈ 8 (proof)
Theorem In_2_8^In_2_8 : 2 ∈ 8 (proof)
Theorem In_3_8^In_3_8 : 3 ∈ 8 (proof)
Theorem In_4_8^In_4_8 : 4 ∈ 8 (proof)
Theorem In_5_8^In_5_8 : 5 ∈ 8 (proof)
Theorem In_6_8^In_6_8 : 6 ∈ 8 (proof)
Theorem In_7_8^In_7_8 : 7 ∈ 8 (proof)
Theorem In_0_9^In_0_9 : 0 ∈ 9 (proof)
Theorem In_1_9^In_1_9 : 1 ∈ 9 (proof)
Theorem In_2_9^In_2_9 : 2 ∈ 9 (proof)
Theorem In_3_9^In_3_9 : 3 ∈ 9 (proof)
Theorem In_4_9^In_4_9 : 4 ∈ 9 (proof)
Theorem In_5_9^In_5_9 : 5 ∈ 9 (proof)
Theorem In_6_9^In_6_9 : 6 ∈ 9 (proof)
Theorem In_7_9^In_7_9 : 7 ∈ 9 (proof)
Theorem In_8_9^In_8_9 : 8 ∈ 9 (proof)
Param In_rec_i^In_rec_i : (ι → (ι → ι) → ι) → ι → ι
Param If_i^If_i : ο → ι → ι → ι
Definition nat_primrec^nat_primrec := λ x0 . λ x1 : ι → ι → ι . In_rec_i (λ x2 . λ x3 : ι → ι . If_i (prim3 x2 ∈ x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known If_i_0^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Theorem nat_primrec_r^{nat_primrec_r} : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . ∀ x3 x4 : ι → ι . (∀ x5 . x5 ∈ x2 ⟶ x3 x5 = x4 x5) ⟶ If_i (prim3 x2 ∈ x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0 = If_i (prim3 x2 ∈ x2) (x1 (prim3 x2) (x4 (prim3 x2))) x0 (proof)
Known In_rec_i_eq^In_rec_i_eq : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_i x0 x1 = x0 x1 (In_rec_i x0)
Theorem nat_primrec_0^{nat_primrec_0} : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0 (proof)
Known If_i_1^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Theorem nat_primrec_S^{nat_primrec_S} : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . nat_p x2 ⟶ nat_primrec x0 x1 (ordsucc x2) = x1 x2 (nat_primrec x0 x1 x2) (proof)
Definition add_nat^add_nat := λ x0 . nat_primrec x0 (λ x1 . ordsucc)
Theorem add_nat_0R^add_nat_0R : ∀ x0 . add_nat x0 0 = x0 (proof)
Theorem add_nat_SR^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1) (proof)
Known nat_ind^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Theorem add_nat_p^add_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (add_nat x0 x1) (proof)
Theorem add_nat_asso^add_nat_asso : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . nat_p x2 ⟶ add_nat (add_nat x0 x1) x2 = add_nat x0 (add_nat x1 x2) (proof)
Theorem add_nat_0L^add_nat_0L : ∀ x0 . nat_p x0 ⟶ add_nat 0 x0 = x0 (proof)
Theorem add_nat_SL^add_nat_SL : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ add_nat (ordsucc x0) x1 = ordsucc (add_nat x0 x1) (proof)
Theorem add_nat_com^add_nat_com : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ add_nat x0 x1 = add_nat x1 x0 (proof)
Definition mul_nat^mul_nat := λ x0 . nat_primrec 0 (λ x1 . add_nat x0)
Theorem mul_nat_0R^mul_nat_0R : ∀ x0 . mul_nat x0 0 = 0 (proof)
Theorem mul_nat_SR^mul_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ mul_nat x0 (ordsucc x1) = add_nat x0 (mul_nat x0 x1) (proof)
Known nat_0^nat_0 : nat_p 0
Theorem mul_nat_p^mul_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (mul_nat x0 x1) (proof)
Theorem mul_nat_0L^mul_nat_0L : ∀ x0 . nat_p x0 ⟶ mul_nat 0 x0 = 0 (proof)
Theorem 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 (proof)
Theorem mul_nat_com^mul_nat_com : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ mul_nat x0 x1 = mul_nat x1 x0 (proof)
Theorem mul_add_nat_distrL^{mul_add_nat_distrL} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . nat_p x2 ⟶ mul_nat x0 (add_nat x1 x2) = add_nat (mul_nat x0 x1) (mul_nat x0 x2) (proof)
Theorem mul_add_nat_distrR^{mul_add_nat_distrR} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . nat_p x2 ⟶ mul_nat (add_nat x0 x1) x2 = add_nat (mul_nat x0 x2) (mul_nat x1 x2) (proof)
Theorem 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) (proof)
Theorem add_nat_1_1_2^{add_nat_1_1_2} : add_nat 1 1 = 2 (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known nat_ordsucc_in_ordsucc^{nat_ordsucc_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ ordsucc x0
Known ordsucc_inj^ordsucc_inj : ∀ x0 x1 . ordsucc x0 = ordsucc x1 ⟶ x0 = x1
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem PigeonHole_nat^{PigeonHole_nat} : ∀ x0 . nat_p x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ ordsucc x0 ⟶ x1 x2 ∈ x0) ⟶ not (∀ x2 . x2 ∈ ordsucc x0 ⟶ ∀ x3 . x3 ∈ ordsucc x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) (proof)
Definition bij^bij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Theorem PigeonHole_nat_bij^{PigeonHole_nat_bij} : ∀ x0 . nat_p x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ x0) ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ bij x0 x0 x1 (proof)