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
Definition u14 := ordsucc u13
Definition u15 := ordsucc u14
Definition u16 := ordsucc u15
Definition u17 := ordsucc u16
Definition u18 := ordsucc u17
Definition u19 := ordsucc u18
Definition u20 := ordsucc u19
Definition u21 := ordsucc u20
Definition u22 := ordsucc u21
Definition u23 := ordsucc u22
Definition u24 := ordsucc u23
Definition u25 := ordsucc u24
Known neq_ordsucc_0^{neq_ordsucc_0} : ∀ x0 . ordsucc x0 = 0 ⟶ ∀ x1 : ο . x1
Theorem 733b2.. : u13 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Known ordsucc_inj_contra^{ordsucc_inj_contra} : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ ordsucc x0 = ordsucc x1 ⟶ ∀ x2 : ο . x2
Known efdfc.. : u12 = 0 ⟶ ∀ x0 : ο . x0
Theorem 16246.. : u13 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Known ce0cd.. : u12 = u1 ⟶ ∀ x0 : ο . x0
Theorem 40d25.. : u13 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Known 8158b.. : u12 = u2 ⟶ ∀ x0 : ο . x0
Theorem 19222.. : u13 = u3 ⟶ ∀ x0 : ο . x0 (proof)
Known e015c.. : u12 = u3 ⟶ ∀ x0 : ο . x0
Theorem 4d850.. : u13 = u4 ⟶ ∀ x0 : ο . x0 (proof)
Known 7aa79.. : u12 = u4 ⟶ ∀ x0 : ο . x0
Theorem 29333.. : u13 = u5 ⟶ ∀ x0 : ο . x0 (proof)
Known 07eba.. : u12 = u5 ⟶ ∀ x0 : ο . x0
Theorem 02f5c.. : u13 = u6 ⟶ ∀ x0 : ο . x0 (proof)
Known 0bd83.. : u12 = u6 ⟶ ∀ x0 : ο . x0
Theorem d9b35.. : u13 = u7 ⟶ ∀ x0 : ο . x0 (proof)
Known 6a15f.. : u12 = u7 ⟶ ∀ x0 : ο . x0
Theorem 0b225.. : u13 = u8 ⟶ ∀ x0 : ο . x0 (proof)
Known a6a6c.. : u12 = u8 ⟶ ∀ x0 : ο . x0
Theorem 3f24c.. : u13 = u9 ⟶ ∀ x0 : ο . x0 (proof)
Known 22885.. : u12 = u9 ⟶ ∀ x0 : ο . x0
Theorem 78358.. : u13 = u10 ⟶ ∀ x0 : ο . x0 (proof)
Known 6c583.. : u12 = u10 ⟶ ∀ x0 : ο . x0
Theorem bf497.. : u13 = u11 ⟶ ∀ x0 : ο . x0 (proof)
Known ab306.. : u12 = u11 ⟶ ∀ x0 : ο . x0
Theorem ad02f.. : u13 = u12 ⟶ ∀ x0 : ο . x0 (proof)
Theorem fc551.. : u14 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Theorem ac679.. : u14 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 0bb18.. : u14 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Theorem d0fe4.. : u14 = u3 ⟶ ∀ x0 : ο . x0 (proof)
Theorem ffd62.. : u14 = u4 ⟶ ∀ x0 : ο . x0 (proof)
Theorem d6c57.. : u14 = u5 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 62d80.. : u14 = u6 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 01bf6.. : u14 = u7 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 4f6ad.. : u14 = u8 ⟶ ∀ x0 : ο . x0 (proof)
Theorem d7730.. : u14 = u9 ⟶ ∀ x0 : ο . x0 (proof)
Theorem f5ab5.. : u14 = u10 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 4e1aa.. : u14 = u11 ⟶ ∀ x0 : ο . x0 (proof)
Theorem ef4da.. : u14 = u12 ⟶ ∀ x0 : ο . x0 (proof)
Theorem e1947.. : u14 = u13 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 160ad.. : u15 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 174d1.. : u15 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 4d715.. : u15 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 70124.. : u15 = u3 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 4b742.. : u15 = u4 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 24fad.. : u15 = u5 ⟶ ∀ x0 : ο . x0 (proof)
Theorem f5ac7.. : u15 = u6 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 008b1.. : u15 = u7 ⟶ ∀ x0 : ο . x0 (proof)
Theorem c0d75.. : u15 = u8 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 3a7bc.. : u15 = u9 ⟶ ∀ x0 : ο . x0 (proof)
Theorem b7f53.. : u15 = u10 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 9c5db.. : u15 = u11 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 72647.. : u15 = u12 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 4d8d4.. : u15 = u13 ⟶ ∀ x0 : ο . x0 (proof)
Theorem b8e82.. : u15 = u14 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 86ae3.. : u16 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Theorem ab690.. : u16 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 296ac.. : u16 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Theorem ca5c3.. : u16 = u3 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 7b2eb.. : u16 = u4 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 35bff.. : u16 = u5 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 3bd28.. : u16 = u6 ⟶ ∀ x0 : ο . x0 (proof)
Theorem d3a2f.. : u16 = u7 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 6c306.. : u16 = u8 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 78b49.. : u16 = u9 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 6879f.. : u16 = u10 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 22184.. : u16 = u11 ⟶ ∀ x0 : ο . x0 (proof)
Theorem fa664.. : u16 = u12 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 4326e.. : u16 = u13 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 71c5e.. : u16 = u14 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 41073.. : u16 = u15 ⟶ ∀ x0 : ο . x0 (proof)
Theorem fcaf7.. : u17 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Theorem d4359.. : u17 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 2c536.. : u17 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 6c299.. : u17 = u3 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 506a9.. : u17 = u4 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 4ab36.. : u17 = u5 ⟶ ∀ x0 : ο . x0 (proof)
Theorem b74f3.. : u17 = u6 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 66c81.. : u17 = u7 ⟶ ∀ x0 : ο . x0 (proof)
Theorem dc9e6.. : u17 = u8 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 66dfd.. : u17 = u9 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 2e5d5.. : u17 = u10 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 454a8.. : u17 = u11 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 9a69f.. : u17 = u12 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 30174.. : u17 = u13 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 82608.. : u17 = u14 ⟶ ∀ x0 : ο . x0 (proof)
Theorem ac12b.. : u17 = u15 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 7fbc8.. : u17 = u16 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 99743.. : u18 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 9ccac.. : u18 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem ad866.. : u18 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 1f012.. : u18 = u3 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 60e5c.. : u18 = u4 ⟶ ∀ x0 : ο . x0 (proof)
Theorem ac512.. : u18 = u5 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 8347f.. : u18 = u6 ⟶ ∀ x0 : ο . x0 (proof)
Theorem c9d3b.. : u18 = u7 ⟶ ∀ x0 : ο . x0 (proof)
Theorem d47e8.. : u18 = u8 ⟶ ∀ x0 : ο . x0 (proof)
Theorem d3922.. : u18 = u9 ⟶ ∀ x0 : ο . x0 (proof)
Theorem a335e.. : u18 = u10 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 8da43.. : u18 = u11 ⟶ ∀ x0 : ο . x0 (proof)
Theorem c1bd9.. : u18 = u12 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 5cb8a.. : u18 = u13 ⟶ ∀ x0 : ο . x0 (proof)
Theorem d92fd.. : u18 = u14 ⟶ ∀ x0 : ο . x0 (proof)
Theorem dfba1.. : u18 = u15 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 0eaf4.. : u18 = u16 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 82c6a.. : u18 = u17 ⟶ ∀ 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 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
Theorem dca77.. : ∀ x0 . x0 ∈ u14 ⟶ ∀ 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 u13 ⟶ x1 x0 (proof)
Theorem f3498.. : ∀ x0 . x0 ∈ u15 ⟶ ∀ 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 u13 ⟶ x1 u14 ⟶ x1 x0 (proof)
Theorem 660da.. : ∀ x0 . x0 ∈ u16 ⟶ ∀ 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 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 x0 (proof)
Theorem 66f20.. : ∀ x0 . x0 ∈ u17 ⟶ ∀ 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 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 u16 ⟶ x1 x0 (proof)
Theorem f9732.. : ∀ x0 . x0 ∈ u18 ⟶ ∀ 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 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 u16 ⟶ x1 u17 ⟶ x1 x0 (proof)
Theorem 27a71.. : ∀ x0 . x0 ∈ u19 ⟶ ∀ 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 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 u16 ⟶ x1 u17 ⟶ x1 u18 ⟶ x1 x0 (proof)