Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: prim1 x1 (aae7a.. (e76d4.. x0) (22ca9.. x0)).
Apply unknownprop_583e189228469f510dae093aa816b0d084f1acaf0341e7deab9d9a676d1b11ef with e76d4.. x0, 22ca9.. x0, x1, prim1 x1 x0 leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H1: ∃ x2 . and (prim1 x2 (e76d4.. x0)) (x1 = aae7a.. 4a7ef.. x2).
Apply exandE_i with λ x2 . prim1 x2 (e76d4.. x0), λ x2 . x1 = aae7a.. 4a7ef.. x2, prim1 x1 x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: prim1 x2 (e76d4.. x0).
Assume H3: x1 = aae7a.. 4a7ef.. x2.
Apply H3 with λ x3 x4 . prim1 x4 x0.
Apply unknownprop_1af9accd96c3abdabaa4f49f1ec8c648f52e722ea8b5a229f61aaf88b5e0cf83 with x0, x2.
The subproof is completed by applying H2.
Assume H1: ∃ x2 . and (prim1 x2 (22ca9.. x0)) (x1 = aae7a.. (4ae4a.. 4a7ef..) x2).
Apply exandE_i with λ x2 . prim1 x2 (22ca9.. x0), λ x2 . x1 = aae7a.. (4ae4a.. 4a7ef..) x2, prim1 x1 x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: prim1 x2 (22ca9.. x0).
Assume H3: x1 = aae7a.. (4ae4a.. 4a7ef..) x2.
Apply H3 with λ x3 x4 . prim1 x4 x0.
Apply unknownprop_faa0906fd70676f18d9a02c8ff6587696be109a33d66d00ec0a508d4784f9592 with x0, x2.
The subproof is completed by applying H2.
■