Proofgold Address

Param ordsucc^ordsucc : ι → ι
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Definition u5 := ordsucc u4
Definition u6 := ordsucc u5
Definition u7 := ordsucc u6
Definition u8 := ordsucc u7
Definition u9 := ordsucc u8
Definition u10 := ordsucc u9
Definition u11 := ordsucc u10
Definition u12 := ordsucc u11
Definition u13 := ordsucc u12
Known neq_1_0^neq_1_0 : u1 = 0 ⟶ ∀ x0 : ο . x0
Theorem neq_1_0^neq_1_0 : u1 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_2_0^neq_2_0 : u2 = 0 ⟶ ∀ x0 : ο . x0
Theorem neq_2_0^neq_2_0 : u2 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_2_1^neq_2_1 : u2 = u1 ⟶ ∀ x0 : ο . x0
Theorem neq_2_1^neq_2_1 : u2 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_3_0^neq_3_0 : u3 = 0 ⟶ ∀ x0 : ο . x0
Theorem neq_3_0^neq_3_0 : u3 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_3_1^neq_3_1 : u3 = u1 ⟶ ∀ x0 : ο . x0
Theorem neq_3_1^neq_3_1 : u3 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_3_2^neq_3_2 : u3 = u2 ⟶ ∀ x0 : ο . x0
Theorem neq_3_2^neq_3_2 : u3 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_4_0^neq_4_0 : u4 = 0 ⟶ ∀ x0 : ο . x0
Theorem neq_4_0^neq_4_0 : u4 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_4_1^neq_4_1 : u4 = u1 ⟶ ∀ x0 : ο . x0
Theorem neq_4_1^neq_4_1 : u4 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_4_2^neq_4_2 : u4 = u2 ⟶ ∀ x0 : ο . x0
Theorem neq_4_2^neq_4_2 : u4 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_4_3^neq_4_3 : u4 = u3 ⟶ ∀ x0 : ο . x0
Theorem neq_4_3^neq_4_3 : u4 = u3 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_5_0^neq_5_0 : u5 = 0 ⟶ ∀ x0 : ο . x0
Theorem neq_5_0^neq_5_0 : u5 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_5_1^neq_5_1 : u5 = u1 ⟶ ∀ x0 : ο . x0
Theorem neq_5_1^neq_5_1 : u5 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_5_2^neq_5_2 : u5 = u2 ⟶ ∀ x0 : ο . x0
Theorem neq_5_2^neq_5_2 : u5 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_5_3^neq_5_3 : u5 = u3 ⟶ ∀ x0 : ο . x0
Theorem neq_5_3^neq_5_3 : u5 = u3 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_5_4^neq_5_4 : u5 = u4 ⟶ ∀ x0 : ο . x0
Theorem neq_5_4^neq_5_4 : u5 = u4 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_6_0^neq_6_0 : u6 = 0 ⟶ ∀ x0 : ο . x0
Theorem neq_6_0^neq_6_0 : u6 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_6_1^neq_6_1 : u6 = u1 ⟶ ∀ x0 : ο . x0
Theorem neq_6_1^neq_6_1 : u6 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_6_2^neq_6_2 : u6 = u2 ⟶ ∀ x0 : ο . x0
Theorem neq_6_2^neq_6_2 : u6 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_6_3^neq_6_3 : u6 = u3 ⟶ ∀ x0 : ο . x0
Theorem neq_6_3^neq_6_3 : u6 = u3 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_6_4^neq_6_4 : u6 = u4 ⟶ ∀ x0 : ο . x0
Theorem neq_6_4^neq_6_4 : u6 = u4 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_6_5^neq_6_5 : u6 = u5 ⟶ ∀ x0 : ο . x0
Theorem neq_6_5^neq_6_5 : u6 = u5 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_7_0^neq_7_0 : u7 = 0 ⟶ ∀ x0 : ο . x0
Theorem neq_7_0^neq_7_0 : u7 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_7_1^neq_7_1 : u7 = u1 ⟶ ∀ x0 : ο . x0
Theorem neq_7_1^neq_7_1 : u7 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_7_2^neq_7_2 : u7 = u2 ⟶ ∀ x0 : ο . x0
Theorem neq_7_2^neq_7_2 : u7 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_7_3^neq_7_3 : u7 = u3 ⟶ ∀ x0 : ο . x0
Theorem neq_7_3^neq_7_3 : u7 = u3 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_7_4^neq_7_4 : u7 = u4 ⟶ ∀ x0 : ο . x0
Theorem neq_7_4^neq_7_4 : u7 = u4 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_7_5^neq_7_5 : u7 = u5 ⟶ ∀ x0 : ο . x0
Theorem neq_7_5^neq_7_5 : u7 = u5 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_7_6^neq_7_6 : u7 = u6 ⟶ ∀ x0 : ο . x0
Theorem neq_7_6^neq_7_6 : u7 = u6 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_8_0^neq_8_0 : u8 = 0 ⟶ ∀ x0 : ο . x0
Theorem neq_8_0^neq_8_0 : u8 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_8_1^neq_8_1 : u8 = u1 ⟶ ∀ x0 : ο . x0
Theorem neq_8_1^neq_8_1 : u8 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_8_2^neq_8_2 : u8 = u2 ⟶ ∀ x0 : ο . x0
Theorem neq_8_2^neq_8_2 : u8 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_8_3^neq_8_3 : u8 = u3 ⟶ ∀ x0 : ο . x0
Theorem neq_8_3^neq_8_3 : u8 = u3 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_8_4^neq_8_4 : u8 = u4 ⟶ ∀ x0 : ο . x0
Theorem neq_8_4^neq_8_4 : u8 = u4 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_8_5^neq_8_5 : u8 = u5 ⟶ ∀ x0 : ο . x0
Theorem neq_8_5^neq_8_5 : u8 = u5 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_8_6^neq_8_6 : u8 = u6 ⟶ ∀ x0 : ο . x0
Theorem neq_8_6^neq_8_6 : u8 = u6 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_8_7^neq_8_7 : u8 = u7 ⟶ ∀ x0 : ο . x0
Theorem neq_8_7^neq_8_7 : u8 = u7 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_9_0^neq_9_0 : u9 = 0 ⟶ ∀ x0 : ο . x0
Theorem neq_9_0^neq_9_0 : u9 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_9_1^neq_9_1 : u9 = u1 ⟶ ∀ x0 : ο . x0
Theorem neq_9_1^neq_9_1 : u9 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_9_2^neq_9_2 : u9 = u2 ⟶ ∀ x0 : ο . x0
Theorem neq_9_2^neq_9_2 : u9 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_9_3^neq_9_3 : u9 = u3 ⟶ ∀ x0 : ο . x0
Theorem neq_9_3^neq_9_3 : u9 = u3 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_9_4^neq_9_4 : u9 = u4 ⟶ ∀ x0 : ο . x0
Theorem neq_9_4^neq_9_4 : u9 = u4 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_9_5^neq_9_5 : u9 = u5 ⟶ ∀ x0 : ο . x0
Theorem neq_9_5^neq_9_5 : u9 = u5 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_9_6^neq_9_6 : u9 = u6 ⟶ ∀ x0 : ο . x0
Theorem neq_9_6^neq_9_6 : u9 = u6 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_9_7^neq_9_7 : u9 = u7 ⟶ ∀ x0 : ο . x0
Theorem neq_9_7^neq_9_7 : u9 = u7 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_9_8^neq_9_8 : u9 = u8 ⟶ ∀ x0 : ο . x0
Theorem neq_9_8^neq_9_8 : u9 = u8 ⟶ ∀ x0 : ο . x0 (proof)
Known neq_ordsucc_0^{neq_ordsucc_0} : ∀ x0 . ordsucc x0 = 0 ⟶ ∀ x1 : ο . x1
Theorem 0e10e.. : u10 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Known ordsucc_inj_contra^{ordsucc_inj_contra} : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ ordsucc x0 = ordsucc x1 ⟶ ∀ x2 : ο . x2
Theorem d183f.. : u10 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem e02d9.. : u10 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 68152.. : u10 = u3 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 33d16.. : u10 = u4 ⟶ ∀ x0 : ο . x0 (proof)
Theorem a7d50.. : u10 = u5 ⟶ ∀ x0 : ο . x0 (proof)
Theorem d0401.. : u10 = u6 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 7d7a8.. : u10 = u7 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 96175.. : u10 = u8 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 4fc31.. : u10 = u9 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 19f75.. : u11 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 618f7.. : u11 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 2c42c.. : u11 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Theorem b06e1.. : u11 = u3 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 6a6f1.. : u11 = u4 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 1b659.. : u11 = u5 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 949f2.. : u11 = u6 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 4abfa.. : u11 = u7 ⟶ ∀ x0 : ο . x0 (proof)
Theorem b3a20.. : u11 = u8 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 4f03f.. : u11 = u9 ⟶ ∀ x0 : ο . x0 (proof)
Theorem ebfb7.. : u11 = u10 ⟶ ∀ x0 : ο . x0 (proof)
Theorem efdfc.. : u12 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Theorem ce0cd.. : u12 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 8158b.. : u12 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Theorem e015c.. : u12 = u3 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 7aa79.. : u12 = u4 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 07eba.. : u12 = u5 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 0bd83.. : u12 = u6 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 6a15f.. : u12 = u7 ⟶ ∀ x0 : ο . x0 (proof)
Theorem a6a6c.. : u12 = u8 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 22885.. : u12 = u9 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 6c583.. : u12 = u10 ⟶ ∀ x0 : ο . x0 (proof)
Theorem ab306.. : u12 = u11 ⟶ ∀ x0 : ο . x0 (proof)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Known 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
Theorem 44418.. : ∀ x0 . x0 ∈ u10 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 x0 (proof)
Theorem 83484.. : ∀ x0 . x0 ∈ u11 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 x0 (proof)
Theorem 866c8.. : ∀ x0 . x0 ∈ u12 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 x0 (proof)
Theorem 6de8d.. : ∀ x0 . x0 ∈ u13 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 x0 (proof)