Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι be given.
Let x6 of type ι be given.
Let x7 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNo x1.
Assume H2: SNo x2.
Assume H3: SNo x3.
Assume H4: SNo x4.
Assume H5: SNo x5.
Assume H6: SNo x6.
Assume H7: SNo x7.
Let x8 of type ο be given.
Assume H8: ∀ x9 . and (SNo x9) (∃ x10 . and (SNo x10) (∃ x11 . and (SNo x11) (∃ x12 . and (SNo x12) (∃ x13 . and (SNo x13) (∃ x14 . and (SNo x14) (∃ x15 . and (SNo x15) (∃ x16 . and (SNo x16) (bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x9 x10 x11 x12 x13 x14 x15 x16)))))))) ⟶ x8.
Apply H8 with x0.
Apply andI with SNo x0, ∃ x9 . and (SNo x9) (∃ x10 . and (SNo x10) (∃ x11 . and (SNo x11) (∃ x12 . and (SNo x12) (∃ x13 . and (SNo x13) (∃ x14 . and (SNo x14) (∃ x15 . and (SNo x15) (bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x0 x9 x10 x11 x12 x13 x14 x15))))))) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x9 of type ο be given.
Assume H9: ∀ x10 . and (SNo x10) (∃ x11 . and (SNo x11) (∃ x12 . and (SNo x12) (∃ x13 . and (SNo x13) (∃ x14 . and (SNo x14) (∃ x15 . and (SNo x15) (∃ x16 . and (SNo x16) (bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x0 x10 x11 x12 x13 x14 x15 x16))))))) ⟶ x9.
Apply H9 with x1.
Apply andI with SNo x1, ∃ x10 . and (SNo x10) (∃ x11 . and (SNo x11) (∃ x12 . and (SNo x12) (∃ x13 . and (SNo x13) (∃ x14 . and (SNo x14) (∃ x15 . and (SNo x15) (bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x0 x1 x10 x11 x12 x13 x14 x15)))))) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x10 of type ο be given.
Assume H10: ∀ x11 . and (SNo x11) (∃ x12 . and (SNo x12) (∃ x13 . and (SNo x13) (∃ x14 . and (SNo x14) (∃ x15 . and (SNo x15) (∃ x16 . and (SNo x16) (bbc71.. x0 x1 x2 x3 x4 x5 ... ... = ...)))))) ⟶ x10.
...
■