Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: 33bf8.. x0.
Apply H0 with λ x1 . x1 = f7962.. (f482f.. x1 4a7ef..) (e3162.. (f482f.. x1 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (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.
Let x5 of type ι → ο be given.
Apply unknownprop_c341b7440910602e792f26987e546b511b5749bf467d1f72d813bfce5b1ed693 with x1, x2, x3, x4, x5, λ x6 x7 . f7962.. x1 x2 x3 x4 x5 = f7962.. x6 (e3162.. (f482f.. (f7962.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (f7962.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. (f7962.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. (f7962.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))).
Apply unknownprop_ba3ab9bf4468a2bf1812f025499c00c467891a240e018bab13b510e399a6dff6 with x1, x2, e3162.. (f482f.. (f7962.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, e3162.. (f482f.. (f7962.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, decode_p (f482f.. (f7962.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))), x5, decode_p (f482f.. (f7962.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.
The subproof is completed by applying unknownprop_c2ca3388e7571dad4d42b42366014268adefe96d1d41c7e170cf20dbb544ae00 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_e2a8881b4dcc5e7ef375032556706c0b864f9b70856efad475466b1f73418cd1 with x1, x2, x3, x4, x5.
Let x6 of type ι be given.
Assume H3: prim1 x6 x1.
Apply unknownprop_e23415cb38f298df79e7981d0d8d62f7101ea2b1b23df49e598ae101fc8e2a6a with x1, x2, x3, x4, x5, x6, λ x7 x8 : ο . iff (x4 x6) x7 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying iff_refl with x4 x6.
Let x6 of type ι be given.
Assume H3: prim1 x6 x1.
Apply unknownprop_369831d43bf550327cc360b73e895f425516f2277cdee517d594df0fa34b7b6c with x1, x2, x3, x4, x5, x6, λ x7 x8 : ο . iff (x5 x6) x7 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying iff_refl with x5 x6.
■