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.
Assume H0: e2219.. (b6bd3.. x0 x1 x2).
Apply H0 with λ x3 . x3 = b6bd3.. x0 x1 x2∀ x4 . prim1 x4 x0∀ x5 . prim1 x5 x0prim1 (x2 x4 x5) x0 leaving 2 subgoals.
Let x3 of type ι be given.
Let x4 of type ιιι be given.
Assume H1: ∀ x5 . prim1 x5 x3∀ x6 . prim1 x6 x3prim1 (x4 x5 x6) x3.
Let x5 of type ιιι be given.
Assume H2: ∀ x6 . prim1 x6 x3∀ x7 . prim1 x7 x3prim1 (x5 x6 x7) x3.
Assume H3: b6bd3.. x3 x4 x5 = b6bd3.. x0 x1 x2.
Apply unknownprop_7f80ec3822be3c72deb8d67082e2ad00c541f16edb0690153a8f263ec09d639c with x3, x0, x4, x1, x5, x2, ∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0prim1 (x2 x6 x7) x0 leaving 2 subgoals.
The subproof is completed by applying H3.
Assume H4: and (x3 = x0) (∀ x6 . prim1 x6 x3∀ x7 . prim1 x7 x3x4 x6 x7 = x1 x6 x7).
Apply H4 with (∀ x6 . prim1 x6 x3∀ x7 . prim1 x7 x3x5 x6 x7 = x2 x6 x7)∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0prim1 (x2 x6 x7) x0.
Assume H5: x3 = x0.
Assume H6: ∀ x6 . prim1 x6 x3∀ x7 . prim1 x7 x3x4 x6 x7 = x1 x6 x7.
Assume H7: ∀ x6 . prim1 x6 x3∀ x7 . prim1 x7 x3x5 x6 x7 = x2 x6 x7.
Apply H5 with λ x6 x7 . ∀ x8 . prim1 x8 x6∀ x9 . prim1 x9 x6prim1 (x2 x8 x9) x6.
Let x6 of type ι be given.
Assume H8: prim1 x6 x3.
Let x7 of type ι be given.
Assume H9: prim1 x7 x3.
Apply H7 with x6, x7, λ x8 x9 . prim1 x8 x3 leaving 3 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
Apply H2 with x6, x7 leaving 2 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
Let x3 of type ιιο be given.
Assume H1: x3 (b6bd3.. x0 x1 x2) (b6bd3.. x0 x1 x2).
The subproof is completed by applying H1.