Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: c754f.. x0.
Apply H0 with λ x1 . x1 = de6e8.. (f482f.. x1 4a7ef..) (e3162.. (f482f.. x1 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (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 ⟶ prim1 (x4 x5) x1.
Let x5 of type ι → ο be given.
Apply unknownprop_b8b34a52999e886cc19aacd0dfc98c11cacae87a6c6875441ad2cdcc84e15f13 with x1, x2, x3, x4, x5, λ x6 x7 . de6e8.. x1 x2 x3 x4 x5 = de6e8.. x6 (e3162.. (f482f.. (de6e8.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (de6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. (de6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. (de6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))).
Apply unknownprop_1203a5201bc0fde7e22b200ba2bbd8a5a08ec3d9e6381007e1965996c8bce3e2 with x1, x2, e3162.. (f482f.. (de6e8.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, e3162.. (f482f.. (de6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, f482f.. (f482f.. (de6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))), x5, decode_p (f482f.. (de6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.
The subproof is completed by applying unknownprop_0584a84ffb1c701f11568ad09c12208aa203b83beb664047f3b41e307f006380 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_7406e4b4e96091f751b5e3e732abecdf4c8b326895755f8fbe97e4e3b9a7c699 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_6fe4748b552c1cdd2fd9e34a6e95c32a6e059b0f8c1228e79280b405dc1c3efd with x1, x2, x3, x4, x5.
Let x6 of type ι be given.
Assume H4: prim1 x6 x1.
Apply unknownprop_ae503b83ae9d7f088146b2bb572620ee5684172e580f4c67c9abf2d4251cf16f with x1, x2, x3, x4, x5, x6, λ x7 x8 : ο . iff (x5 x6) x7 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying iff_refl with x5 x6.
■