Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: b089b.. x0.
Apply H0 with λ x1 . x1 = a599b.. (f482f.. x1 4a7ef..) (e3162.. (f482f.. x1 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).
Let x1 of type ι be given.
Let x2 of type ι → ι → ι be given.
Assume H1: ∀ x3 . prim1 x3 x1 ⟶ ∀ x4 . prim1 x4 x1 ⟶ prim1 (x2 x3 x4) x1.
Let x3 of type ι → ι → ι be given.
Assume H2: ∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ prim1 (x3 x4 x5) x1.
Let x4 of type ι → ι → ο be given.
Let x5 of type ι be given.
Assume H3: prim1 x5 x1.
Apply unknownprop_eabedd3d76039b491d5e84d806a1531556f3f3c91026c65ab26cd33b32e8a0f8 with x1, x2, x3, x4, x5, λ x6 x7 . a599b.. x1 x2 x3 x4 x5 = a599b.. x6 (e3162.. (f482f.. (a599b.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (a599b.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (a599b.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. (a599b.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).
Apply unknownprop_f61d3deee040b5ae75f3822d9e31727f50b0b0f309182f0b5d03c7a5e18acd59 with x1, x2, x3, x4, x5, λ x6 x7 . a599b.. x1 x2 x3 x4 x5 = a599b.. x1 (e3162.. (f482f.. (a599b.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (a599b.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (a599b.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x6.
Apply unknownprop_e8ceeaffdd3a89ce898466d1fe3ffbf4a683f4a3f057af46c4541f0b2e7df630 with x1, x2, e3162.. (f482f.. (a599b.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, e3162.. (f482f.. (a599b.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, 2b2e3.. (f482f.. (a599b.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))), x5 leaving 3 subgoals.
The subproof is completed by applying unknownprop_b5795914eb193bbfa4f632de98b54a6a76bdf54be34a0176ad47fbe277bed7e0 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_02057732628d0db44b1bb613fdfbb3b7e15d7c624fa9ca0b22b5faab75926897 with x1, x2, x3, x4, x5.
Let x6 of type ι be given.
Assume H4: prim1 x6 x1.
Let x7 of type ι be given.
Assume H5: prim1 x7 x1.
Apply unknownprop_717c381bdb867b0ee25ff7f9445699e0386c192122d455239cc3e38f81c565e2 with x1, x2, x3, x4, x5, x6, x7, λ x8 x9 : ο . iff (x4 x6 x7) x8 leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying iff_refl with x4 x6 x7.
■