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.
Assume H0: prim1 x5 (85402.. x0 x1 x2 x3 x4).
Apply unknownprop_81f421271d5bfcfd6fe0047c052f7e57176b5e1c1f8a403c2c447b17d3ed45ac with x0, x1, x2, x3, x4, x5, ∃ x6 . and (prim1 x6 x0) (∃ x7 . and (prim1 x7 (x1 x6)) (∃ x8 . and (prim1 x8 (x2 x6 x7)) (and (x3 x6 x7 x8) (x5 = x4 x6 x7 x8)))) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x6 of type ι be given.
Assume H1: prim1 x6 x0.
Let x7 of type ι be given.
Assume H2: prim1 x7 (x1 x6).
Let x8 of type ι be given.
Assume H3: prim1 x8 (x2 x6 x7).
Assume H4: x3 x6 x7 x8.
Assume H5: x5 = x4 x6 x7 x8.
Let x9 of type ο be given.
Assume H6: ∀ x10 . and (prim1 x10 x0) (∃ x11 . and (prim1 x11 (x1 x10)) (∃ x12 . and (prim1 x12 (x2 x10 x11)) (and (x3 x10 x11 x12) (x5 = x4 x10 x11 x12))))x9.
Apply H6 with x6.
Apply andI with prim1 x6 x0, ∃ x10 . and (prim1 x10 (x1 x6)) (∃ x11 . and (prim1 x11 (x2 x6 x10)) (and (x3 x6 x10 x11) (x5 = x4 x6 x10 x11))) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x10 of type ο be given.
Assume H7: ∀ x11 . and (prim1 x11 (x1 x6)) (∃ x12 . and (prim1 x12 (x2 x6 x11)) (and (x3 x6 x11 x12) (x5 = x4 x6 x11 x12)))x10.
Apply H7 with x7.
Apply andI with prim1 x7 (x1 x6), ∃ x11 . and (prim1 x11 (x2 x6 x7)) (and (x3 x6 x7 x11) (x5 = x4 x6 x7 x11)) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x11 of type ο be given.
Assume H8: ∀ x12 . and (prim1 x12 (x2 x6 x7)) (and (x3 x6 x7 x12) (x5 = x4 x6 x7 x12))x11.
Apply H8 with x8.
Apply andI with prim1 x8 (x2 x6 x7), and (x3 x6 x7 x8) (x5 = x4 x6 x7 x8) leaving 2 subgoals.
The subproof is completed by applying H3.
Apply andI with x3 x6 x7 x8, x5 = x4 x6 x7 x8 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.