Proofgold Address

Param ordsucc^ordsucc : ι → ι
Param u19 : ι
Definition u20 := ordsucc u19
Param u1 : ι
Param u2 : ι
Param u3 : ι
Param u4 : ι
Param u5 : ι
Param u6 : ι
Param u7 : ι
Param u8 : ι
Param u9 : ι
Param u10 : ι
Param u11 : ι
Param u12 : ι
Param u13 : ι
Param u14 : ι
Param u15 : ι
Param u16 : ι
Param u17 : ι
Param u18 : ι
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 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
Theorem 6ab99.. : ∀ x0 . x0 ∈ u20 ⟶ ∀ 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 u19 ⟶ x1 x0
Definition u21 := ordsucc u20
Theorem a039e.. : ∀ x0 . x0 ∈ u21 ⟶ ∀ 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 u19 ⟶ x1 u20 ⟶ x1 x0
Definition u22 := ordsucc u21
Theorem df354.. : ∀ x0 . x0 ∈ u22 ⟶ ∀ 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 u19 ⟶ x1 u20 ⟶ x1 u21 ⟶ x1 x0
Definition u23 := ordsucc u22
Theorem eae4d.. : ∀ x0 . x0 ∈ u23 ⟶ ∀ 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 u19 ⟶ x1 u20 ⟶ x1 u21 ⟶ x1 u22 ⟶ x1 x0
Definition u24 := ordsucc u23
Theorem adedd.. : ∀ x0 . x0 ∈ u24 ⟶ ∀ 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 u19 ⟶ x1 u20 ⟶ x1 u21 ⟶ x1 u22 ⟶ x1 u23 ⟶ x1 x0