Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: 80242.. x0.
Assume H1: 80242.. x1.
Assume H2: 099f3.. x0 x1.
Let x2 of type ο be given.
Assume H3: ∀ x3 . prim1 x3 (23e07.. x1)prim1 x3 (5246e.. x0)x2.
Assume H4: prim1 x0 (23e07.. x1)x2.
Assume H5: prim1 x1 (5246e.. x0)x2.
Apply unknownprop_334a5a4dfd5441f12538cd3c70458238b05308c372afbd4cf94b09dd8e7afe85 with x0, x1, x2 leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Let x3 of type ι be given.
Assume H6: 80242.. x3.
Assume H7: prim1 (e4431.. x3) (d3786.. (e4431.. x0) (e4431.. x1)).
Assume H8: SNoEq_ (e4431.. x3) x3 x0.
Assume H9: SNoEq_ (e4431.. x3) x3 x1.
Assume H10: 099f3.. x0 x3.
Assume H11: 099f3.. x3 x1.
Assume H12: nIn (e4431.. x3) x0.
Assume H13: prim1 (e4431.. x3) x1.
Apply unknownprop_1ac99d32a7ae5dc08fd640ea6c8b661df6b3535fe85e88b30b17c3701cb4c7ce with e4431.. x0, e4431.. x1, e4431.. x3, x2 leaving 2 subgoals.
The subproof is completed by applying H7.
Assume H14: prim1 (e4431.. x3) (e4431.. x0).
Assume H15: prim1 (e4431.. x3) (e4431.. x1).
Apply H3 with x3 leaving 2 subgoals.
Apply unknownprop_ecae2d2d3708015d34ac3eacd84df17c3571bd5e56ae2362f9cb0de5042f4b16 with x1, x3 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H6.
The subproof is completed by applying H15.
The subproof is completed by applying H11.
Apply unknownprop_ee5bcd8a678317db72ef3d355308c7e294e59766f08f82a0b083647c04eafd99 with x0, x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H6.
The subproof is completed by applying H14.
The subproof is completed by applying H10.
Assume H6: prim1 (e4431.. x0) (e4431.. x1).
Assume H7: SNoEq_ (e4431.. x0) x0 x1.
Assume H8: prim1 (e4431.. x0) x1.
Apply H4.
Apply unknownprop_ecae2d2d3708015d34ac3eacd84df17c3571bd5e56ae2362f9cb0de5042f4b16 with x1, x0 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H6.
The subproof is completed by applying H2.
Assume H6: prim1 (e4431.. x1) (e4431.. x0).
Assume H7: SNoEq_ (e4431.. x1) x0 x1.
Assume H8: nIn (e4431.. x1) x0.
Apply H5.
Apply unknownprop_ee5bcd8a678317db72ef3d355308c7e294e59766f08f82a0b083647c04eafd99 with x0, x1 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H6.
The subproof is completed by applying H2.