Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: 4e60e.. x0.
Apply H0 with λ x1 . x1 = 1eafe.. (f482f.. x1 4a7ef..) (e3162.. (f482f.. x1 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (e3162.. (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (2b2e3.. (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.
Assume H3: ∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ prim1 (x4 x5 x6) x1.
Let x5 of type ι → ι → ο be given.
Apply unknownprop_8ea69fc9abac0355b105f07aa76ed34b3962fcf544d9757d1d9d05aa9d0cad83 with x1, x2, x3, x4, x5, λ x6 x7 . 1eafe.. x1 x2 x3 x4 x5 = 1eafe.. x6 (e3162.. (f482f.. (1eafe.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (1eafe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (e3162.. (f482f.. (1eafe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (2b2e3.. (f482f.. (1eafe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))).
Apply unknownprop_4fcf1c41dd74381dd43abf3e020e4abe97220e99f9d7d9747bd8e75c322f5299 with x1, x2, e3162.. (f482f.. (1eafe.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, e3162.. (f482f.. (1eafe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, e3162.. (f482f.. (1eafe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))), x5, 2b2e3.. (f482f.. (1eafe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.
The subproof is completed by applying unknownprop_9b67ca9ab1646382899bbdc59f47517de76380f07be13a5ce2de56c82d4796e9 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_1800ba7fa99d61c31829fa17fb98b2c724b98156c3096d47aa78e26b0544c68e with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_4296533c60aa73eebe625d72d0577a7e8b212c89496259f10b26dbb5c0255a76 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_c26ef7bf18140bad8d6953993defcebda527e5707dd4d63400179c3d1438050f with x1, x2, x3, x4, x5, x6, x7, λ x8 x9 : ο . iff (x5 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 x5 x6 x7.
■