Proofgold Asset

Param SNo^SNo : ι → ο
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param bbc71.. : ι → ι → ι → ι → ι → ι → ι → ι → ι
Definition 1eb0a.. := λ x0 . ∃ x1 . and (SNo x1) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (∃ x15 . and (SNo x15) (x0 = bbc71.. x1 x3 x5 x7 x9 x11 x13 x15))))))))
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem d5242.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ 1eb0a.. (bbc71.. x0 x1 x2 x3 x4 x5 x6 x7)
Definition d4639.. := λ x0 : ι → ι . λ x1 . prim0 (λ x2 . and (SNo x2) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x1 = bbc71.. (x0 x1) x2 x3 x5 x7 x9 x11 x13))))))))
Known Eps_i_ex^Eps_i_ex : ∀ x0 : ι → ο . (∃ x1 . x0 x1) ⟶ x0 (prim0 x0)
Theorem 26f49.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ ∀ x1 . 1eb0a.. x1 ⟶ and (SNo (d4639.. x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (x1 = bbc71.. (x0 x1) (d4639.. x0 x1) x2 x4 x6 x8 x10 x12)))))))
Theorem fd099.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ ∀ x1 . 1eb0a.. x1 ⟶ SNo (d4639.. x0 x1)
Known babe8.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x1 = x9
Theorem 33b4a.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 x2 x3 x4 x5 x6 x7 x8 . SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ d4639.. x0 (bbc71.. x1 x2 x3 x4 x5 x6 x7 x8) = x2
Definition 50208.. := λ x0 x1 : ι → ι . λ x2 . prim0 (λ x3 . and (SNo x3) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x4 x6 x8 x10 x12)))))))
Theorem 9b0e1.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x5 x7 x9 x11 x13)))))))) ⟶ ∀ x2 . 1eb0a.. x2 ⟶ and (SNo (50208.. x0 x1 x2)) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (x2 = bbc71.. (x0 x2) (x1 x2) (50208.. x0 x1 x2) x3 x5 x7 x9 x11))))))
Theorem 1131a.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x5 x7 x9 x11 x13)))))))) ⟶ ∀ x2 . 1eb0a.. x2 ⟶ SNo (50208.. x0 x1 x2)
Known 6488e.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x2 = x10
Theorem 90339.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x5 x7 x9 x11 x13)))))))) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ 50208.. x0 x1 (bbc71.. x2 x3 x4 x5 x6 x7 x8 x9) = x4
Definition 8d7df.. := λ x0 x1 x2 : ι → ι . λ x3 . prim0 (λ x4 . and (SNo x4) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x4 x5 x7 x9 x11))))))
Theorem 0a376.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x5 x7 x9 x11 x13)))))))) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x4 x6 x8 x10 x12))))))) ⟶ ∀ x3 . 1eb0a.. x3 ⟶ and (SNo (8d7df.. x0 x1 x2 x3)) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) (8d7df.. x0 x1 x2 x3) x4 x6 x8 x10)))))
Theorem 5e734.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x5 x7 x9 x11 x13)))))))) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x4 x6 x8 x10 x12))))))) ⟶ ∀ x3 . 1eb0a.. x3 ⟶ SNo (8d7df.. x0 x1 x2 x3)
Known ad01a.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x3 = x11
Theorem 71a99.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x5 x7 x9 x11 x13)))))))) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x4 x6 x8 x10 x12))))))) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 . SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ 8d7df.. x0 x1 x2 (bbc71.. x3 x4 x5 x6 x7 x8 x9 x10) = x6
Definition 41ec1.. := λ x0 x1 x2 x3 : ι → ι . λ x4 . prim0 (λ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x5 x6 x8 x10)))))
Theorem 15adc.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x5 x7 x9 x11 x13)))))))) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x4 x6 x8 x10 x12))))))) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x5 x7 x9 x11)))))) ⟶ ∀ x4 . 1eb0a.. x4 ⟶ and (SNo (41ec1.. x0 x1 x2 x3 x4)) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) (41ec1.. x0 x1 x2 x3 x4) x5 x7 x9))))
Theorem af528.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x5 x7 x9 x11 x13)))))))) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x4 x6 x8 x10 x12))))))) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x5 x7 x9 x11)))))) ⟶ ∀ x4 . 1eb0a.. x4 ⟶ SNo (41ec1.. x0 x1 x2 x3 x4)
Known f4559.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x4 = x12
Theorem 26f65.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x5 x7 x9 x11 x13)))))))) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x4 x6 x8 x10 x12))))))) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x5 x7 x9 x11)))))) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 x5 x6 x7 x8 x9 x10 x11 . SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ 41ec1.. x0 x1 x2 x3 (bbc71.. x4 x5 x6 x7 x8 x9 x10 x11) = x8
Definition 28f5a.. := λ x0 x1 x2 x3 x4 : ι → ι . λ x5 . prim0 (λ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x6 x7 x9))))
Theorem baa4b.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x5 x7 x9 x11 x13)))))))) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x4 x6 x8 x10 x12))))))) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x5 x7 x9 x11)))))) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 : ι → ι . (∀ x5 . 1eb0a.. x5 ⟶ and (SNo (x4 x5)) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x6 x8 x10))))) ⟶ ∀ x5 . 1eb0a.. x5 ⟶ and (SNo (28f5a.. x0 x1 x2 x3 x4 x5)) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) (28f5a.. x0 x1 x2 x3 x4 x5) x6 x8)))
Theorem 69bbd.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x5 x7 x9 x11 x13)))))))) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x4 x6 x8 x10 x12))))))) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x5 x7 x9 x11)))))) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 : ι → ι . (∀ x5 . 1eb0a.. x5 ⟶ and (SNo (x4 x5)) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x6 x8 x10))))) ⟶ ∀ x5 . 1eb0a.. x5 ⟶ SNo (28f5a.. x0 x1 x2 x3 x4 x5)
Known f56fc.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x5 = x13
Theorem 62fb0.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x5 x7 x9 x11 x13)))))))) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x4 x6 x8 x10 x12))))))) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x5 x7 x9 x11)))))) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 : ι → ι . (∀ x5 . 1eb0a.. x5 ⟶ and (SNo (x4 x5)) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x6 x8 x10))))) ⟶ (∀ x5 . 1eb0a.. x5 ⟶ SNo (x4 x5)) ⟶ ∀ x5 x6 x7 x8 x9 x10 x11 x12 . SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ 28f5a.. x0 x1 x2 x3 x4 (bbc71.. x5 x6 x7 x8 x9 x10 x11 x12) = x10
Definition 717b4.. := λ x0 x1 x2 x3 x4 x5 : ι → ι . λ x6 . prim0 (λ x7 . and (SNo x7) (∃ x8 . and (SNo x8) (x6 = bbc71.. (x0 x6) (x1 x6) (x2 x6) (x3 x6) (x4 x6) (x5 x6) x7 x8)))
Theorem 42518.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x5 x7 x9 x11 x13)))))))) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x4 x6 x8 x10 x12))))))) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x5 x7 x9 x11)))))) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 : ι → ι . (∀ x5 . 1eb0a.. x5 ⟶ and (SNo (x4 x5)) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x6 x8 x10))))) ⟶ (∀ x5 . 1eb0a.. x5 ⟶ SNo (x4 x5)) ⟶ ∀ x5 : ι → ι . (∀ x6 . 1eb0a.. x6 ⟶ and (SNo (x5 x6)) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (x6 = bbc71.. (x0 x6) (x1 x6) (x2 x6) (x3 x6) (x4 x6) (x5 x6) x7 x9)))) ⟶ ∀ x6 . 1eb0a.. x6 ⟶ and (SNo (717b4.. x0 x1 x2 x3 x4 x5 x6)) (∃ x7 . and (SNo x7) (x6 = bbc71.. (x0 x6) (x1 x6) (x2 x6) (x3 x6) (x4 x6) (x5 x6) (717b4.. x0 x1 x2 x3 x4 x5 x6) x7))
Theorem 9599d.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x5 x7 x9 x11 x13)))))))) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x4 x6 x8 x10 x12))))))) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x5 x7 x9 x11)))))) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 : ι → ι . (∀ x5 . 1eb0a.. x5 ⟶ and (SNo (x4 x5)) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x6 x8 x10))))) ⟶ (∀ x5 . 1eb0a.. x5 ⟶ SNo (x4 x5)) ⟶ ∀ x5 : ι → ι . (∀ x6 . 1eb0a.. x6 ⟶ and (SNo (x5 x6)) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (x6 = bbc71.. (x0 x6) (x1 x6) (x2 x6) (x3 x6) (x4 x6) (x5 x6) x7 x9)))) ⟶ ∀ x6 . 1eb0a.. x6 ⟶ SNo (717b4.. x0 x1 x2 x3 x4 x5 x6)
Known 4a66b.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x6 = x14
Theorem c7d23.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x5 x7 x9 x11 x13)))))))) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x4 x6 x8 x10 x12))))))) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x5 x7 x9 x11)))))) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 : ι → ι . (∀ x5 . 1eb0a.. x5 ⟶ and (SNo (x4 x5)) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x6 x8 x10))))) ⟶ (∀ x5 . 1eb0a.. x5 ⟶ SNo (x4 x5)) ⟶ ∀ x5 : ι → ι . (∀ x6 . 1eb0a.. x6 ⟶ and (SNo (x5 x6)) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (x6 = bbc71.. (x0 x6) (x1 x6) (x2 x6) (x3 x6) (x4 x6) (x5 x6) x7 x9)))) ⟶ (∀ x6 . 1eb0a.. x6 ⟶ SNo (x5 x6)) ⟶ ∀ x6 x7 x8 x9 x10 x11 x12 x13 . SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ 717b4.. x0 x1 x2 x3 x4 x5 (bbc71.. x6 x7 x8 x9 x10 x11 x12 x13) = x12
Definition 053de.. := λ x0 x1 x2 x3 x4 x5 x6 : ι → ι . λ x7 . prim0 (λ x8 . and (SNo x8) (x7 = bbc71.. (x0 x7) (x1 x7) (x2 x7) (x3 x7) (x4 x7) (x5 x7) (x6 x7) x8))
Theorem 0b166.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x5 x7 x9 x11 x13)))))))) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x4 x6 x8 x10 x12))))))) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x5 x7 x9 x11)))))) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 : ι → ι . (∀ x5 . 1eb0a.. x5 ⟶ and (SNo (x4 x5)) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x6 x8 x10))))) ⟶ (∀ x5 . 1eb0a.. x5 ⟶ SNo (x4 x5)) ⟶ ∀ x5 : ι → ι . (∀ x6 . 1eb0a.. x6 ⟶ and (SNo (x5 x6)) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (x6 = bbc71.. (x0 x6) (x1 x6) (x2 x6) (x3 x6) (x4 x6) (x5 x6) x7 x9)))) ⟶ (∀ x6 . 1eb0a.. x6 ⟶ SNo (x5 x6)) ⟶ ∀ x6 : ι → ι . (∀ x7 . 1eb0a.. x7 ⟶ and (SNo (x6 x7)) (∃ x8 . and (SNo x8) (x7 = bbc71.. (x0 x7) (x1 x7) (x2 x7) (x3 x7) (x4 x7) (x5 x7) (x6 x7) x8))) ⟶ ∀ x7 . 1eb0a.. x7 ⟶ and (SNo (053de.. x0 x1 x2 x3 x4 x5 x6 x7)) (x7 = bbc71.. (x0 x7) (x1 x7) (x2 x7) (x3 x7) (x4 x7) (x5 x7) (x6 x7) (053de.. x0 x1 x2 x3 x4 x5 x6 x7))
Theorem 0c70a.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x5 x7 x9 x11 x13)))))))) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x4 x6 x8 x10 x12))))))) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x5 x7 x9 x11)))))) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 : ι → ι . (∀ x5 . 1eb0a.. x5 ⟶ and (SNo (x4 x5)) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x6 x8 x10))))) ⟶ (∀ x5 . 1eb0a.. x5 ⟶ SNo (x4 x5)) ⟶ ∀ x5 : ι → ι . (∀ x6 . 1eb0a.. x6 ⟶ and (SNo (x5 x6)) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (x6 = bbc71.. (x0 x6) (x1 x6) (x2 x6) (x3 x6) (x4 x6) (x5 x6) x7 x9)))) ⟶ (∀ x6 . 1eb0a.. x6 ⟶ SNo (x5 x6)) ⟶ ∀ x6 : ι → ι . (∀ x7 . 1eb0a.. x7 ⟶ and (SNo (x6 x7)) (∃ x8 . and (SNo x8) (x7 = bbc71.. (x0 x7) (x1 x7) (x2 x7) (x3 x7) (x4 x7) (x5 x7) (x6 x7) x8))) ⟶ ∀ x7 . 1eb0a.. x7 ⟶ SNo (053de.. x0 x1 x2 x3 x4 x5 x6 x7)
Known 7c302.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x7 = x15
Theorem 48feb.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x5 x7 x9 x11 x13)))))))) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x4 x6 x8 x10 x12))))))) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x5 x7 x9 x11)))))) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 : ι → ι . (∀ x5 . 1eb0a.. x5 ⟶ and (SNo (x4 x5)) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x6 x8 x10))))) ⟶ (∀ x5 . 1eb0a.. x5 ⟶ SNo (x4 x5)) ⟶ ∀ x5 : ι → ι . (∀ x6 . 1eb0a.. x6 ⟶ and (SNo (x5 x6)) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (x6 = bbc71.. (x0 x6) (x1 x6) (x2 x6) (x3 x6) (x4 x6) (x5 x6) x7 x9)))) ⟶ (∀ x6 . 1eb0a.. x6 ⟶ SNo (x5 x6)) ⟶ ∀ x6 : ι → ι . (∀ x7 . 1eb0a.. x7 ⟶ and (SNo (x6 x7)) (∃ x8 . and (SNo x8) (x7 = bbc71.. (x0 x7) (x1 x7) (x2 x7) (x3 x7) (x4 x7) (x5 x7) (x6 x7) x8))) ⟶ (∀ x7 . 1eb0a.. x7 ⟶ SNo (x6 x7)) ⟶ ∀ x7 x8 x9 x10 x11 x12 x13 x14 . SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ 053de.. x0 x1 x2 x3 x4 x5 x6 (bbc71.. x7 x8 x9 x10 x11 x12 x13 x14) = x14
Definition 8dd2c.. := λ x0 . prim0 (λ x1 . and (SNo x1) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x0 = bbc71.. x1 x2 x4 x6 x8 x10 x12 x14)))))))))
Theorem 340c0.. : ∀ x0 . 1eb0a.. x0 ⟶ and (SNo (8dd2c.. x0)) (∃ x1 . and (SNo x1) (∃ x3 . and (SNo x3) (∃ x5 . and (SNo x5) (∃ x7 . and (SNo x7) (∃ x9 . and (SNo x9) (∃ x11 . and (SNo x11) (∃ x13 . and (SNo x13) (x0 = bbc71.. (8dd2c.. x0) x1 x3 x5 x7 x9 x11 x13))))))))
Theorem 95571.. : ∀ x0 . 1eb0a.. x0 ⟶ SNo (8dd2c.. x0)
Known cca09.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x0 = x8
Theorem 212d5.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ 8dd2c.. (bbc71.. x0 x1 x2 x3 x4 x5 x6 x7) = x0