Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ιι be given.
Assume H0: ∀ x1 . 1eb0a.. x1and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x3 . and (SNo x3) (∃ x4 . and (SNo x4) (∃ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (∃ x8 . and (SNo x8) (x1 = bbc71.. (x0 x1) x2 x3 x4 x5 x6 x7 x8)))))))).
Assume H1: ∀ x1 . 1eb0a.. x1SNo (x0 x1).
Let x1 of type ιι be given.
Assume H2: ∀ x2 . 1eb0a.. x2and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x4 . and (SNo x4) (∃ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (∃ x8 . and (SNo x8) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x4 x5 x6 x7 x8))))))).
Assume H3: ∀ x2 . 1eb0a.. x2SNo (x1 x2).
Let x2 of type ιι be given.
Assume H4: ∀ x3 . 1eb0a.. x3and (SNo (x2 x3)) (∃ x4 . and (SNo x4) (∃ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (∃ x8 . and (SNo x8) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x4 x5 x6 x7 x8)))))).
Assume H5: ∀ x3 . 1eb0a.. x3SNo (x2 x3).
Let x3 of type ιι be given.
Assume H6: ∀ x4 . 1eb0a.. x4and (SNo (x3 x4)) (∃ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (∃ x8 . and (SNo x8) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x5 x6 x7 x8))))).
Assume H7: ∀ x4 . 1eb0a.. x4SNo (x3 x4).
Let x4 of type ιι be given.
Assume H8: ∀ x5 . 1eb0a.. x5and (SNo (x4 x5)) (∃ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (∃ x8 . and (SNo x8) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x6 x7 x8)))).
Let x5 of type ι be given.
Assume H9: 1eb0a.. x5.
Apply H8 with x5, and (SNo (28f5a.. x0 x1 x2 x3 x4 x5)) (∃ x6 . and (SNo x6) ...) leaving 2 subgoals.
...
...