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 Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known fdaf0.. : 9 ∈ 16
Theorem fd1a6.. : u9 ∈ u17 (proof)
Known 662c8.. : 10 ∈ 16
Theorem e886d.. : u10 ∈ u17 (proof)
Known 2039c.. : 11 ∈ 16
Theorem e57ea.. : u11 ∈ u17 (proof)
Known be924.. : 12 ∈ 16
Theorem a1a10.. : u12 ∈ u17 (proof)
Param ap^ap : ι → ι → ι
Param lam^Sigma : ι → (ι → ι) → ι
Param If_i^If_i : ο → ι → ι → ι
Known neq_9_0^neq_9_0 : u9 = 0 ⟶ ∀ x0 : ο . x0
Known neq_9_1^neq_9_1 : u9 = u1 ⟶ ∀ x0 : ο . x0
Known neq_9_2^neq_9_2 : u9 = u2 ⟶ ∀ x0 : ο . x0
Known neq_9_3^neq_9_3 : u9 = u3 ⟶ ∀ x0 : ο . x0
Known neq_9_4^neq_9_4 : u9 = u4 ⟶ ∀ x0 : ο . x0
Known neq_9_5^neq_9_5 : u9 = u5 ⟶ ∀ x0 : ο . x0
Known neq_9_6^neq_9_6 : u9 = u6 ⟶ ∀ x0 : ο . x0
Known neq_9_7^neq_9_7 : u9 = u7 ⟶ ∀ x0 : ο . x0
Known neq_9_8^neq_9_8 : u9 = u8 ⟶ ∀ x0 : ο . x0
Theorem 511d7.. : (∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 . x3 ∈ x1 ⟶ ap (lam x1 (λ x5 . If_i (x5 = x3) x0 (x2 (ordsucc x3) x5))) x3 = x0) ⟶ (∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 x4 . (x4 = x3 ⟶ ∀ x5 : ο . x5) ⟶ ap (lam x1 (λ x6 . If_i (x6 = x3) x0 (x2 (ordsucc x3) x6))) x4 = ap (lam x1 (x2 (ordsucc x3))) x4) ⟶ ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . ap (lam 17 (λ x18 . If_i (x18 = 0) x0 (If_i (x18 = 1) x1 (If_i (x18 = 2) x2 (If_i (x18 = 3) x3 (If_i (x18 = 4) x4 (If_i (x18 = 5) x5 (If_i (x18 = 6) x6 (If_i (x18 = 7) x7 (If_i (x18 = 8) x8 (If_i (x18 = 9) x9 (If_i (x18 = 10) x10 (If_i (x18 = 11) x11 (If_i (x18 = 12) x12 (If_i (x18 = 13) x13 (If_i (x18 = 14) x14 (If_i (x18 = 15) x15 x16))))))))))))))))) u9 = x9 (proof)
Known 0e10e.. : u10 = 0 ⟶ ∀ x0 : ο . x0
Known d183f.. : u10 = u1 ⟶ ∀ x0 : ο . x0
Known e02d9.. : u10 = u2 ⟶ ∀ x0 : ο . x0
Known 68152.. : u10 = u3 ⟶ ∀ x0 : ο . x0
Known 33d16.. : u10 = u4 ⟶ ∀ x0 : ο . x0
Known a7d50.. : u10 = u5 ⟶ ∀ x0 : ο . x0
Known d0401.. : u10 = u6 ⟶ ∀ x0 : ο . x0
Known 7d7a8.. : u10 = u7 ⟶ ∀ x0 : ο . x0
Known 96175.. : u10 = u8 ⟶ ∀ x0 : ο . x0
Known 4fc31.. : u10 = u9 ⟶ ∀ x0 : ο . x0
Theorem 929f6.. : (∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 . x3 ∈ x1 ⟶ ap (lam x1 (λ x5 . If_i (x5 = x3) x0 (x2 (ordsucc x3) x5))) x3 = x0) ⟶ (∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 x4 . (x4 = x3 ⟶ ∀ x5 : ο . x5) ⟶ ap (lam x1 (λ x6 . If_i (x6 = x3) x0 (x2 (ordsucc x3) x6))) x4 = ap (lam x1 (x2 (ordsucc x3))) x4) ⟶ ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . ap (lam 17 (λ x18 . If_i (x18 = 0) x0 (If_i (x18 = 1) x1 (If_i (x18 = 2) x2 (If_i (x18 = 3) x3 (If_i (x18 = 4) x4 (If_i (x18 = 5) x5 (If_i (x18 = 6) x6 (If_i (x18 = 7) x7 (If_i (x18 = 8) x8 (If_i (x18 = 9) x9 (If_i (x18 = 10) x10 (If_i (x18 = 11) x11 (If_i (x18 = 12) x12 (If_i (x18 = 13) x13 (If_i (x18 = 14) x14 (If_i (x18 = 15) x15 x16))))))))))))))))) u10 = x10 (proof)
Known 19f75.. : u11 = 0 ⟶ ∀ x0 : ο . x0
Known 618f7.. : u11 = u1 ⟶ ∀ x0 : ο . x0
Known 2c42c.. : u11 = u2 ⟶ ∀ x0 : ο . x0
Known b06e1.. : u11 = u3 ⟶ ∀ x0 : ο . x0
Known 6a6f1.. : u11 = u4 ⟶ ∀ x0 : ο . x0
Known 1b659.. : u11 = u5 ⟶ ∀ x0 : ο . x0
Known 949f2.. : u11 = u6 ⟶ ∀ x0 : ο . x0
Known 4abfa.. : u11 = u7 ⟶ ∀ x0 : ο . x0
Known b3a20.. : u11 = u8 ⟶ ∀ x0 : ο . x0
Known 4f03f.. : u11 = u9 ⟶ ∀ x0 : ο . x0
Known ebfb7.. : u11 = u10 ⟶ ∀ x0 : ο . x0
Theorem 02699.. : (∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 . x3 ∈ x1 ⟶ ap (lam x1 (λ x5 . If_i (x5 = x3) x0 (x2 (ordsucc x3) x5))) x3 = x0) ⟶ (∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 x4 . (x4 = x3 ⟶ ∀ x5 : ο . x5) ⟶ ap (lam x1 (λ x6 . If_i (x6 = x3) x0 (x2 (ordsucc x3) x6))) x4 = ap (lam x1 (x2 (ordsucc x3))) x4) ⟶ ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . ap (lam 17 (λ x18 . If_i (x18 = 0) x0 (If_i (x18 = 1) x1 (If_i (x18 = 2) x2 (If_i (x18 = 3) x3 (If_i (x18 = 4) x4 (If_i (x18 = 5) x5 (If_i (x18 = 6) x6 (If_i (x18 = 7) x7 (If_i (x18 = 8) x8 (If_i (x18 = 9) x9 (If_i (x18 = 10) x10 (If_i (x18 = 11) x11 (If_i (x18 = 12) x12 (If_i (x18 = 13) x13 (If_i (x18 = 14) x14 (If_i (x18 = 15) x15 x16))))))))))))))))) u11 = x11 (proof)
Known efdfc.. : u12 = 0 ⟶ ∀ x0 : ο . x0
Known ce0cd.. : u12 = u1 ⟶ ∀ x0 : ο . x0
Known 8158b.. : u12 = u2 ⟶ ∀ x0 : ο . x0
Known e015c.. : u12 = u3 ⟶ ∀ x0 : ο . x0
Known 7aa79.. : u12 = u4 ⟶ ∀ x0 : ο . x0
Known 07eba.. : u12 = u5 ⟶ ∀ x0 : ο . x0
Known 0bd83.. : u12 = u6 ⟶ ∀ x0 : ο . x0
Known 6a15f.. : u12 = u7 ⟶ ∀ x0 : ο . x0
Known a6a6c.. : u12 = u8 ⟶ ∀ x0 : ο . x0
Known 22885.. : u12 = u9 ⟶ ∀ x0 : ο . x0
Known 6c583.. : u12 = u10 ⟶ ∀ x0 : ο . x0
Known ab306.. : u12 = u11 ⟶ ∀ x0 : ο . x0
Theorem 6f2dd.. : (∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 . x3 ∈ x1 ⟶ ap (lam x1 (λ x5 . If_i (x5 = x3) x0 (x2 (ordsucc x3) x5))) x3 = x0) ⟶ (∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 x4 . (x4 = x3 ⟶ ∀ x5 : ο . x5) ⟶ ap (lam x1 (λ x6 . If_i (x6 = x3) x0 (x2 (ordsucc x3) x6))) x4 = ap (lam x1 (x2 (ordsucc x3))) x4) ⟶ ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . ap (lam 17 (λ x18 . If_i (x18 = 0) x0 (If_i (x18 = 1) x1 (If_i (x18 = 2) x2 (If_i (x18 = 3) x3 (If_i (x18 = 4) x4 (If_i (x18 = 5) x5 (If_i (x18 = 6) x6 (If_i (x18 = 7) x7 (If_i (x18 = 8) x8 (If_i (x18 = 9) x9 (If_i (x18 = 10) x10 (If_i (x18 = 11) x11 (If_i (x18 = 12) x12 (If_i (x18 = 13) x13 (If_i (x18 = 14) x14 (If_i (x18 = 15) x15 x16))))))))))))))))) u12 = x12 (proof)