Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Apply set_ext with ac767.. x0 x0, b5c9f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)) leaving 2 subgoals.
Let x1 of type ι be given.
Assume H0: prim1 x1 (ac767.. x0 x0).
Apply and3E with aae7a.. (e76d4.. x1) (22ca9.. x1) = x1, prim1 (e76d4.. x1) x0, prim1 (22ca9.. x1) x0, prim1 x1 (b5c9f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) leaving 2 subgoals.
Apply unknownprop_4861fab3b9bde4ccc5c91f323e4d2535c7d435027e9067e34ce3781cfa602d01 with x0, λ x2 . x0, x1.
The subproof is completed by applying H0.
Assume H1: aae7a.. (e76d4.. x1) (22ca9.. x1) = x1.
Assume H2: prim1 (e76d4.. x1) x0.
Assume H3: prim1 (22ca9.. x1) x0.
Apply H1 with λ x2 x3 . prim1 x2 (b5c9f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))).
Apply unknownprop_dc63f07f5e92258921347b0c89ef1b6f68ff3d0c7d527390f78d57fc4bdb18d0 with e76d4.. x1, 22ca9.. x1, λ x2 x3 . prim1 x3 (3097a.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x4 . x0)).
Apply unknownprop_78f4273a7b4d13f02d77d194b65be481121674fd021f4ffb88d69be4bcd0ab71 with 4ae4a.. (4ae4a.. 4a7ef..), λ x2 . x0, λ x2 . If_i (x2 = 4a7ef..) (e76d4.. x1) (22ca9.. x1).
Let x2 of type ι be given.
Assume H4: prim1 x2 (4ae4a.. (4ae4a.. 4a7ef..)).
Apply If_i_or with x2 = 4a7ef.., e76d4.. x1, 22ca9.. x1, prim1 (If_i (x2 = 4a7ef..) (e76d4.. x1) (22ca9.. x1)) x0 leaving 2 subgoals.
Assume H5: If_i (x2 = 4a7ef..) (e76d4.. x1) (22ca9.. x1) = e76d4.. x1.
Apply H5 with λ x3 x4 . prim1 x4 x0.
The subproof is completed by applying H2.
Assume H5: If_i (x2 = 4a7ef..) (e76d4.. x1) (22ca9.. x1) = 22ca9.. x1.
Apply H5 with λ x3 x4 . prim1 x4 x0.
The subproof is completed by applying H3.
Let x1 of type ι be given.
Assume H0: prim1 x1 (b5c9f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))).
Apply unknownprop_e91802ac95034c32a27830a437206af24864b973eefcd7f0fba6473c100b9bd7 with 4ae4a.. (4ae4a.. 4a7ef..), λ x2 . x0, x1, prim1 x1 (ac767.. x0 x0) leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: ∀ x2 . prim1 x2 x1 ⟶ and (cad8f.. x2) (prim1 (f482f.. x2 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..))).
Assume H2: ∀ x2 . prim1 x2 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ prim1 (f482f.. x1 x2) x0.
Claim L3: aae7a.. (f482f.. x1 4a7ef..) (f482f.. x1 (4ae4a.. 4a7ef..)) = x1
Apply unknownprop_5896ce98646deef8ec3dfd6486cb5e8ac723fe9e353ebdbde1d65018fd75b748 with x1.
The subproof is completed by applying H1.
Apply L3 with λ x2 x3 . prim1 x2 (ac767.. x0 x0).
Apply unknownprop_1f27075d0cd8d16888a609d68ca6246fb2307839dccadd646f85ab18bdcaae8e with x0, λ x2 . x0, f482f.. x1 4a7ef.., f482f.. x1 (4ae4a.. 4a7ef..) leaving 2 subgoals.
Apply H2 with 4a7ef...
The subproof is completed by applying unknownprop_94c438c3f41134cd86e0be06a85b5e5b3aa8448f9221f51d2dfe9b1364042f49.
Apply H2 with 4ae4a.. 4a7ef...
The subproof is completed by applying unknownprop_e256c3837ff221325e66d4c83283618d462d76cb96bca463e1abd4876bf63511.
■