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.
Assume H0: 45c1b.. (726e4.. x0 x1 x2 x3 x4).
Apply H0 with λ x5 . x5 = 726e4.. x0 x1 x2 x3 x4prim1 x3 x0 leaving 2 subgoals.
Let x5 of type ι be given.
Let x6 of type ιι be given.
Assume H1: ∀ x7 . prim1 x7 x5prim1 (x6 x7) x5.
Let x7 of type ιο be given.
Let x8 of type ι be given.
Assume H2: prim1 x8 x5.
Let x9 of type ι be given.
Assume H3: prim1 x9 x5.
Assume H4: 726e4.. x5 x6 x7 x8 x9 = 726e4.. x0 x1 x2 x3 x4.
Apply unknownprop_2fe36533018e189844c5de2b6d5f0e4e362a125ae417916f82888e946a69aef7 with x5, x0, x6, x1, x7, x2, x8, x3, x9, x4, prim1 x3 x0 leaving 2 subgoals.
The subproof is completed by applying H4.
Assume H5: and (and (and (x5 = x0) (∀ x10 . prim1 x10 x5x6 x10 = x1 x10)) (∀ x10 . prim1 x10 x5x7 x10 = x2 x10)) (x8 = x3).
Apply H5 with x9 = x4prim1 x3 x0.
Assume H6: and (and (x5 = x0) (∀ x10 . prim1 x10 x5x6 x10 = x1 x10)) (∀ x10 . prim1 x10 x5x7 x10 = x2 x10).
Apply H6 with x8 = x3x9 = x4prim1 x3 x0.
Assume H7: and (x5 = x0) (∀ x10 . prim1 x10 x5x6 x10 = x1 x10).
Apply H7 with (∀ x10 . prim1 x10 x5x7 x10 = x2 x10)x8 = x3x9 = x4prim1 x3 x0.
Assume H8: x5 = x0.
Assume H9: ∀ x10 . prim1 x10 x5x6 x10 = x1 x10.
Assume H10: ∀ x10 . prim1 x10 x5x7 x10 = x2 x10.
Assume H11: x8 = x3.
Assume H12: x9 = x4.
Apply H8 with λ x10 x11 . prim1 x3 x10.
Apply H11 with λ x10 x11 . prim1 x10 x5.
The subproof is completed by applying H2.
Let x5 of type ιιο be given.
Assume H1: x5 (726e4.. x0 x1 x2 x3 x4) (726e4.. x0 x1 x2 x3 x4).
The subproof is completed by applying H1.