Proofgold Address

Param ordsucc^ordsucc : ι → ι
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known EmptyE^EmptyE : ∀ x0 . nIn x0 0
Theorem cases_1^cases_1 : ∀ x0 . x0 ∈ 1 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 x0 (proof)
Theorem cases_2^cases_2 : ∀ x0 . x0 ∈ 2 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 x0 (proof)
Theorem cases_3^cases_3 : ∀ x0 . x0 ∈ 3 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 x0 (proof)
Theorem cases_4^cases_4 : ∀ x0 . x0 ∈ 4 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 x0 (proof)
Theorem cases_5^cases_5 : ∀ x0 . x0 ∈ 5 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 4 ⟶ x1 x0 (proof)
Theorem cases_6^cases_6 : ∀ x0 . x0 ∈ 6 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 4 ⟶ x1 5 ⟶ x1 x0 (proof)
Theorem cases_7^cases_7 : ∀ x0 . x0 ∈ 7 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 4 ⟶ x1 5 ⟶ x1 6 ⟶ x1 x0 (proof)
Theorem cases_8^cases_8 : ∀ x0 . x0 ∈ 8 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 4 ⟶ x1 5 ⟶ x1 6 ⟶ x1 7 ⟶ x1 x0 (proof)
Theorem cases_9^cases_9 : ∀ x0 . x0 ∈ 9 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 4 ⟶ x1 5 ⟶ x1 6 ⟶ x1 7 ⟶ x1 8 ⟶ x1 x0 (proof)
Known neq_ordsucc_0^{neq_ordsucc_0} : ∀ x0 . ordsucc x0 = 0 ⟶ ∀ x1 : ο . x1
Theorem neq_1_0^neq_1_0 : 1 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_2_0^neq_2_0 : 2 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Known ordsucc_inj^ordsucc_inj : ∀ x0 x1 . ordsucc x0 = ordsucc x1 ⟶ x0 = x1
Theorem ordsucc_inj_contra^{ordsucc_inj_contra} : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ ordsucc x0 = ordsucc x1 ⟶ ∀ x2 : ο . x2 (proof)
Theorem neq_2_1^neq_2_1 : 2 = 1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem nIn_2_1^nIn_2_1 : nIn 2 1 (proof)
Theorem neq_3_0^neq_3_0 : 3 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_3_1^neq_3_1 : 3 = 1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_3_2^neq_3_2 : 3 = 2 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_4_0^neq_4_0 : 4 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_4_1^neq_4_1 : 4 = 1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_4_2^neq_4_2 : 4 = 2 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_4_3^neq_4_3 : 4 = 3 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_5_0^neq_5_0 : 5 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_5_1^neq_5_1 : 5 = 1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_5_2^neq_5_2 : 5 = 2 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_5_3^neq_5_3 : 5 = 3 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_5_4^neq_5_4 : 5 = 4 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_6_0^neq_6_0 : 6 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_6_1^neq_6_1 : 6 = 1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_6_2^neq_6_2 : 6 = 2 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_6_3^neq_6_3 : 6 = 3 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_6_4^neq_6_4 : 6 = 4 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_6_5^neq_6_5 : 6 = 5 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_7_0^neq_7_0 : 7 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_7_1^neq_7_1 : 7 = 1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_7_2^neq_7_2 : 7 = 2 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_7_3^neq_7_3 : 7 = 3 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_7_4^neq_7_4 : 7 = 4 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_7_5^neq_7_5 : 7 = 5 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_7_6^neq_7_6 : 7 = 6 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_8_0^neq_8_0 : 8 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_8_1^neq_8_1 : 8 = 1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_8_2^neq_8_2 : 8 = 2 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_8_3^neq_8_3 : 8 = 3 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_8_4^neq_8_4 : 8 = 4 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_8_5^neq_8_5 : 8 = 5 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_8_6^neq_8_6 : 8 = 6 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_8_7^neq_8_7 : 8 = 7 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_9_0^neq_9_0 : 9 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_9_1^neq_9_1 : 9 = 1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_9_2^neq_9_2 : 9 = 2 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_9_3^neq_9_3 : 9 = 3 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_9_4^neq_9_4 : 9 = 4 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_9_5^neq_9_5 : 9 = 5 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_9_6^neq_9_6 : 9 = 6 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_9_7^neq_9_7 : 9 = 7 ⟶ ∀ x0 : ο . x0 (proof)
Theorem neq_9_8^neq_9_8 : 9 = 8 ⟶ ∀ x0 : ο . x0 (proof)