Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Assume H0: ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) (e5b72.. (4ae4a.. 4a7ef..)).
Apply unknownprop_85c22e88a806aabda7246f27ac458442bcb94ac25cc9a3616a68cf646d95941d with 4ae4a.. 4a7ef.., 3097a.. x0 (λ x2 . x1 x2).
Let x2 of type ι be given.
Assume H1: prim1 x2 (3097a.. x0 (λ x3 . x1 x3)).
Claim L2: x2 = 4a7ef..
Apply unknownprop_fa66e3d1737b2c05fa4008399b4c740ee88bf9334c6b435957b41684dfedfe51 with x2.
Let x3 of type ι be given.
Assume H2: prim1 x3 x2.
Apply unknownprop_e91802ac95034c32a27830a437206af24864b973eefcd7f0fba6473c100b9bd7 with x0, x1, x2, False leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H3: ∀ x4 . prim1 x4 x2 ⟶ and (cad8f.. x4) (prim1 (f482f.. x4 4a7ef..) x0).
Assume H4: ∀ x4 . prim1 x4 x0 ⟶ prim1 (f482f.. x2 x4) (x1 x4).
Apply H3 with x3, False leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H5: aae7a.. (f482f.. x3 4a7ef..) (f482f.. x3 (4ae4a.. 4a7ef..)) = x3.
Assume H6: prim1 (f482f.. x3 4a7ef..) x0.
Claim L7: prim1 (f482f.. x2 (f482f.. x3 4a7ef..)) (x1 (f482f.. x3 4a7ef..))
Apply H4 with f482f.. x3 4a7ef...
The subproof is completed by applying H6.
Claim L8: prim1 (x1 (f482f.. x3 4a7ef..)) (e5b72.. (4ae4a.. 4a7ef..))
Apply H0 with f482f.. x3 4a7ef...
The subproof is completed by applying H6.
Claim L9: prim1 (f482f.. x2 (f482f.. x3 4a7ef..)) (4ae4a.. 4a7ef..)
Apply unknownprop_4134b8a5d866cd7ad711ea569ada0ca0ba949f5cad571bf5782dc7c2d15cdb1c with 4ae4a.. 4a7ef.., x1 (f482f.. x3 4a7ef..), f482f.. x2 (f482f.. x3 4a7ef..) leaving 2 subgoals.
The subproof is completed by applying L8.
The subproof is completed by applying L7.
Claim L10: prim1 (f482f.. x2 (f482f.. x3 4a7ef..)) (91630.. 4a7ef..)
Apply unknownprop_745f0ddae55929306ce167ef9bae0ede767961c0319e8b14305a55d5b24d73e4 with f482f.. x2 (f482f.. x3 4a7ef..).
The subproof is completed by applying L9.
Claim L11: f482f.. x2 (f482f.. x3 4a7ef..) = 4a7ef..
Apply unknownprop_30833a9978e304b25ffd59c347245315985872140acc9e441a97543a28184d79 with 4a7ef.., f482f.. x2 (f482f.. x3 4a7ef..).
The subproof is completed by applying L10.
Claim L12: prim1 (f482f.. x3 (4ae4a.. 4a7ef..)) (f482f.. x2 (f482f.. x3 4a7ef..))
Apply unknownprop_5843a53f522dbf92d80ac36289685067f008fd2f46b9067d54fc3bf68053a1a3 with x2, f482f.. x3 4a7ef.., f482f.. x3 (4ae4a.. 4a7ef..).
Apply H5 with λ x4 x5 . prim1 x5 x2.
The subproof is completed by applying H2.
Claim L13: prim1 (f482f.. x3 (4ae4a.. 4a7ef..)) 4a7ef..
Apply L11 with λ x4 x5 . prim1 (f482f.. x3 (4ae4a.. 4a7ef..)) x4.
The subproof is completed by applying L12.
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with f482f.. x3 (4ae4a.. 4a7ef..).
The subproof is completed by applying L13.
Apply L2 with λ x3 x4 . prim1 x4 (4ae4a.. 4a7ef..).
The subproof is completed by applying unknownprop_375af585d676cd889234cd20860ce45033e1ffceb375ac6277c1b1a2e16f15bd.
■