Proofgold Address

Param SNo^SNo : ι → ο
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param bbc71.. : ι → ι → ι → ι → ι → ι → ι → ι → ι
Definition 1eb0a.. := λ x0 . ∀ x1 : ο . (∀ x2 . and (SNo x2) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (∀ x15 : ο . (∀ x16 . and (SNo x16) (x0 = bbc71.. x2 x4 x6 x8 x10 x12 x14 x16) ⟶ x15) ⟶ x15) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1
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) (proof)
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 (proof)
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.. (proof)
Theorem 630e7.. : 1eb0a.. 0f074.. (proof)
Theorem 77598.. : 1eb0a.. e6ddb.. (proof)
Theorem 429ac.. : 1eb0a.. 2e3ac.. (proof)
Theorem 2dc23.. : 1eb0a.. 71a7b.. (proof)
Theorem 20480.. : 1eb0a.. fd2a6.. (proof)
Theorem 4056c.. : 1eb0a.. ea520.. (proof)