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 Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known 179f3.. : 0 ∈ u21
Theorem c34a2.. : 0 ∈ u22 (proof)
Known 07fdb.. : u1 ∈ u21
Theorem 617e2.. : u1 ∈ u22 (proof)
Known c25ea.. : u2 ∈ u21
Theorem a7839.. : u2 ∈ u22 (proof)
Known 0750b.. : u3 ∈ u21
Theorem 9018e.. : u3 ∈ u22 (proof)
Known 701a9.. : u4 ∈ u21
Theorem 540e6.. : u4 ∈ u22 (proof)
Known 0dc69.. : u5 ∈ u21
Theorem 8a085.. : u5 ∈ u22 (proof)
Known 1d1d3.. : u6 ∈ u21
Theorem 8f513.. : u6 ∈ u22 (proof)
Known 0b77c.. : u7 ∈ u21
Theorem 3224f.. : u7 ∈ u22 (proof)
Known 5fc29.. : u8 ∈ u21
Theorem e5453.. : u8 ∈ u22 (proof)
Known 4b046.. : u9 ∈ u21
Theorem 8413f.. : u9 ∈ u22 (proof)
Known 46da3.. : u10 ∈ u21
Theorem abaf6.. : u10 ∈ u22 (proof)
Known 3ad1f.. : u11 ∈ u21
Theorem 0158f.. : u11 ∈ u22 (proof)
Known 07061.. : u12 ∈ u21
Theorem 126ca.. : u12 ∈ u22 (proof)
Known d16a4.. : u13 ∈ u21
Theorem 49a59.. : u13 ∈ u22 (proof)
Known a6788.. : u14 ∈ u21
Theorem caae0.. : u14 ∈ u22 (proof)
Known ce294.. : u15 ∈ u21
Theorem 9c9ec.. : u15 ∈ u22 (proof)
Known 20f4b.. : u16 ∈ u21
Theorem d63b1.. : u16 ∈ u22 (proof)
Known d5f90.. : u17 ∈ u21
Theorem 96b76.. : u17 ∈ u22 (proof)
Known 08993.. : u18 ∈ u21
Theorem 7ba92.. : u18 ∈ u22 (proof)
Param nat_p^nat_p : ι → ο
Known nat_trans^nat_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Known daa33.. : nat_p u22
Theorem e46ec.. : u17 ⊆ u22 (proof)
Param ap^ap : ι → ι → ι
Param lam^Sigma : ι → (ι → ι) → ι
Param If_i^If_i : ο → ι → ι → ι
Known d21a1.. : ∀ 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
Known 160ad.. : u15 = 0 ⟶ ∀ x0 : ο . x0
Known 174d1.. : u15 = u1 ⟶ ∀ x0 : ο . x0
Known 4d715.. : u15 = u2 ⟶ ∀ x0 : ο . x0
Known 70124.. : u15 = u3 ⟶ ∀ x0 : ο . x0
Known 4b742.. : u15 = u4 ⟶ ∀ x0 : ο . x0
Known 24fad.. : u15 = u5 ⟶ ∀ x0 : ο . x0
Known f5ac7.. : u15 = u6 ⟶ ∀ x0 : ο . x0
Known 008b1.. : u15 = u7 ⟶ ∀ x0 : ο . x0
Known c0d75.. : u15 = u8 ⟶ ∀ x0 : ο . x0
Known 3a7bc.. : u15 = u9 ⟶ ∀ x0 : ο . x0
Known b7f53.. : u15 = u10 ⟶ ∀ x0 : ο . x0
Known 9c5db.. : u15 = u11 ⟶ ∀ x0 : ο . x0
Known 72647.. : u15 = u12 ⟶ ∀ x0 : ο . x0
Known 4d8d4.. : u15 = u13 ⟶ ∀ x0 : ο . x0
Known b8e82.. : u15 = u14 ⟶ ∀ x0 : ο . x0
Known 48efb.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 . x3 ∈ x1 ⟶ ap (lam x1 (λ x5 . If_i (x5 = x3) x0 (x2 (ordsucc x3) x5))) x3 = x0
Theorem edaef.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 . ap (lam 22 (λ x23 . If_i (x23 = 0) x0 (If_i (x23 = 1) x1 (If_i (x23 = 2) x2 (If_i (x23 = 3) x3 (If_i (x23 = 4) x4 (If_i (x23 = 5) x5 (If_i (x23 = 6) x6 (If_i (x23 = 7) x7 (If_i (x23 = 8) x8 (If_i (x23 = 9) x9 (If_i (x23 = 10) x10 (If_i (x23 = 11) x11 (If_i (x23 = 12) x12 (If_i (x23 = 13) x13 (If_i (x23 = 14) x14 (If_i (x23 = 15) x15 (If_i (x23 = 16) x16 (If_i (x23 = 17) x17 (If_i (x23 = 18) x18 (If_i (x23 = 19) x19 (If_i (x23 = 20) x20 x21)))))))))))))))))))))) u15 = x15 (proof)
Known 86ae3.. : u16 = 0 ⟶ ∀ x0 : ο . x0
Known ab690.. : u16 = u1 ⟶ ∀ x0 : ο . x0
Known 296ac.. : u16 = u2 ⟶ ∀ x0 : ο . x0
Known ca5c3.. : u16 = u3 ⟶ ∀ x0 : ο . x0
Known 7b2eb.. : u16 = u4 ⟶ ∀ x0 : ο . x0
Known 35bff.. : u16 = u5 ⟶ ∀ x0 : ο . x0
Known 3bd28.. : u16 = u6 ⟶ ∀ x0 : ο . x0
Known d3a2f.. : u16 = u7 ⟶ ∀ x0 : ο . x0
Known 6c306.. : u16 = u8 ⟶ ∀ x0 : ο . x0
Known 78b49.. : u16 = u9 ⟶ ∀ x0 : ο . x0
Known 6879f.. : u16 = u10 ⟶ ∀ x0 : ο . x0
Known 22184.. : u16 = u11 ⟶ ∀ x0 : ο . x0
Known fa664.. : u16 = u12 ⟶ ∀ x0 : ο . x0
Known 4326e.. : u16 = u13 ⟶ ∀ x0 : ο . x0
Known 71c5e.. : u16 = u14 ⟶ ∀ x0 : ο . x0
Known 41073.. : u16 = u15 ⟶ ∀ x0 : ο . x0
Theorem db976.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 . ap (lam 22 (λ x23 . If_i (x23 = 0) x0 (If_i (x23 = 1) x1 (If_i (x23 = 2) x2 (If_i (x23 = 3) x3 (If_i (x23 = 4) x4 (If_i (x23 = 5) x5 (If_i (x23 = 6) x6 (If_i (x23 = 7) x7 (If_i (x23 = 8) x8 (If_i (x23 = 9) x9 (If_i (x23 = 10) x10 (If_i (x23 = 11) x11 (If_i (x23 = 12) x12 (If_i (x23 = 13) x13 (If_i (x23 = 14) x14 (If_i (x23 = 15) x15 (If_i (x23 = 16) x16 (If_i (x23 = 17) x17 (If_i (x23 = 18) x18 (If_i (x23 = 19) x19 (If_i (x23 = 20) x20 x21)))))))))))))))))))))) u16 = x16 (proof)
Known fcaf7.. : u17 = 0 ⟶ ∀ x0 : ο . x0
Known d4359.. : u17 = u1 ⟶ ∀ x0 : ο . x0
Known 2c536.. : u17 = u2 ⟶ ∀ x0 : ο . x0
Known 6c299.. : u17 = u3 ⟶ ∀ x0 : ο . x0
Known 506a9.. : u17 = u4 ⟶ ∀ x0 : ο . x0
Known 4ab36.. : u17 = u5 ⟶ ∀ x0 : ο . x0
Known b74f3.. : u17 = u6 ⟶ ∀ x0 : ο . x0
Known 66c81.. : u17 = u7 ⟶ ∀ x0 : ο . x0
Known dc9e6.. : u17 = u8 ⟶ ∀ x0 : ο . x0
Known 66dfd.. : u17 = u9 ⟶ ∀ x0 : ο . x0
Known 2e5d5.. : u17 = u10 ⟶ ∀ x0 : ο . x0
Known 454a8.. : u17 = u11 ⟶ ∀ x0 : ο . x0
Known 9a69f.. : u17 = u12 ⟶ ∀ x0 : ο . x0
Known 30174.. : u17 = u13 ⟶ ∀ x0 : ο . x0
Known 82608.. : u17 = u14 ⟶ ∀ x0 : ο . x0
Known ac12b.. : u17 = u15 ⟶ ∀ x0 : ο . x0
Known 7fbc8.. : u17 = u16 ⟶ ∀ x0 : ο . x0
Theorem 39d71.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 . ap (lam 22 (λ x23 . If_i (x23 = 0) x0 (If_i (x23 = 1) x1 (If_i (x23 = 2) x2 (If_i (x23 = 3) x3 (If_i (x23 = 4) x4 (If_i (x23 = 5) x5 (If_i (x23 = 6) x6 (If_i (x23 = 7) x7 (If_i (x23 = 8) x8 (If_i (x23 = 9) x9 (If_i (x23 = 10) x10 (If_i (x23 = 11) x11 (If_i (x23 = 12) x12 (If_i (x23 = 13) x13 (If_i (x23 = 14) x14 (If_i (x23 = 15) x15 (If_i (x23 = 16) x16 (If_i (x23 = 17) x17 (If_i (x23 = 18) x18 (If_i (x23 = 19) x19 (If_i (x23 = 20) x20 x21)))))))))))))))))))))) u17 = x17 (proof)
Known 99743.. : u18 = 0 ⟶ ∀ x0 : ο . x0
Known 9ccac.. : u18 = u1 ⟶ ∀ x0 : ο . x0
Known ad866.. : u18 = u2 ⟶ ∀ x0 : ο . x0
Known 1f012.. : u18 = u3 ⟶ ∀ x0 : ο . x0
Known 60e5c.. : u18 = u4 ⟶ ∀ x0 : ο . x0
Known ac512.. : u18 = u5 ⟶ ∀ x0 : ο . x0
Known 8347f.. : u18 = u6 ⟶ ∀ x0 : ο . x0
Known c9d3b.. : u18 = u7 ⟶ ∀ x0 : ο . x0
Known d47e8.. : u18 = u8 ⟶ ∀ x0 : ο . x0
Known d3922.. : u18 = u9 ⟶ ∀ x0 : ο . x0
Known a335e.. : u18 = u10 ⟶ ∀ x0 : ο . x0
Known 8da43.. : u18 = u11 ⟶ ∀ x0 : ο . x0
Known c1bd9.. : u18 = u12 ⟶ ∀ x0 : ο . x0
Known 5cb8a.. : u18 = u13 ⟶ ∀ x0 : ο . x0
Known d92fd.. : u18 = u14 ⟶ ∀ x0 : ο . x0
Known dfba1.. : u18 = u15 ⟶ ∀ x0 : ο . x0
Known 0eaf4.. : u18 = u16 ⟶ ∀ x0 : ο . x0
Known 82c6a.. : u18 = u17 ⟶ ∀ x0 : ο . x0
Theorem a7d2d.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 . ap (lam 22 (λ x23 . If_i (x23 = 0) x0 (If_i (x23 = 1) x1 (If_i (x23 = 2) x2 (If_i (x23 = 3) x3 (If_i (x23 = 4) x4 (If_i (x23 = 5) x5 (If_i (x23 = 6) x6 (If_i (x23 = 7) x7 (If_i (x23 = 8) x8 (If_i (x23 = 9) x9 (If_i (x23 = 10) x10 (If_i (x23 = 11) x11 (If_i (x23 = 12) x12 (If_i (x23 = 13) x13 (If_i (x23 = 14) x14 (If_i (x23 = 15) x15 (If_i (x23 = 16) x16 (If_i (x23 = 17) x17 (If_i (x23 = 18) x18 (If_i (x23 = 19) x19 (If_i (x23 = 20) x20 x21)))))))))))))))))))))) u18 = x18 (proof)
Definition 55574.. := λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . ap (lam 22 (λ x23 . If_i (x23 = 0) x1 (If_i (x23 = 1) x2 (If_i (x23 = 2) x3 (If_i (x23 = 3) x4 (If_i (x23 = 4) x5 (If_i (x23 = 5) x6 (If_i (x23 = 6) x7 (If_i (x23 = 7) x8 (If_i (x23 = 8) x9 (If_i (x23 = 9) x10 (If_i (x23 = 10) x11 (If_i (x23 = 11) x12 (If_i (x23 = 12) x13 (If_i (x23 = 13) x14 (If_i (x23 = 14) x15 (If_i (x23 = 15) x16 (If_i (x23 = 16) x17 (If_i (x23 = 17) x18 (If_i (x23 = 18) x19 (If_i (x23 = 19) x20 (If_i (x23 = 20) x21 x22)))))))))))))))))))))) x0
Theorem 134b9.. : 55574.. u15 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x16 (proof)
Theorem b8157.. : 55574.. u16 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x17 (proof)
Theorem e86b0.. : 55574.. u17 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x18 (proof)
Theorem bb555.. : 55574.. u18 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x19 (proof)