Proofgold Address

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)
Theorem b501e.. : ∀ x0 . 1eb0a.. x0 ⟶ ∀ x1 : ι → ο . (∀ x2 x3 x4 x5 x6 x7 x8 x9 . SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ x0 = bbc71.. x2 x3 x4 x5 x6 x7 x8 x9 ⟶ x1 (bbc71.. x2 x3 x4 x5 x6 x7 x8 x9)) ⟶ x1 x0
Param ordsucc^ordsucc : ι → ι
Definition 3e294.. := bbc71.. 0 1 0 0 0 0 0 0
Definition 0f074.. := bbc71.. 0 0 1 0 0 0 0 0
Definition e6ddb.. := bbc71.. 0 0 0 1 0 0 0 0
Definition 2e3ac.. := bbc71.. 0 0 0 0 1 0 0 0
Definition 71a7b.. := bbc71.. 0 0 0 0 0 1 0 0
Definition fd2a6.. := bbc71.. 0 0 0 0 0 0 1 0
Definition ea520.. := bbc71.. 0 0 0 0 0 0 0 1
Known SNo_0^SNo_0 : SNo 0
Known SNo_1^SNo_1 : SNo 1
Theorem 9899a.. : 1eb0a.. 3e294..
Theorem 630e7.. : 1eb0a.. 0f074..
Theorem 77598.. : 1eb0a.. e6ddb..
Theorem 429ac.. : 1eb0a.. 2e3ac..
Theorem 2dc23.. : 1eb0a.. 71a7b..
Theorem 20480.. : 1eb0a.. fd2a6..
Theorem 4056c.. : 1eb0a.. ea520..