Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: 687c3.. x0.
Apply H0 with λ x1 . x1 = 7ac32.. (f482f.. x1 4a7ef..) (decode_c (f482f.. x1 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (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.
Let x3 of type ι → ι be given.
Assume H1: ∀ x4 . prim1 x4 x1 ⟶ prim1 (x3 x4) x1.
Let x4 of type ι → ι → ο be given.
Let x5 of type ι → ο be given.
Apply unknownprop_a1b93da6bd5ab5ca91f8dab96152d61f9ea5f3b97a23278da48b759601e8b693 with x1, x2, x3, x4, x5, λ x6 x7 . 7ac32.. x1 x2 x3 x4 x5 = 7ac32.. x6 (decode_c (f482f.. (7ac32.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (7ac32.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (7ac32.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. (7ac32.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))).
Apply unknownprop_6e7ef0d9cfb93cc02bc993937d42a2ed755238077bae7fa81033567b7d46cc82 with x1, x2, decode_c (f482f.. (7ac32.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, f482f.. (f482f.. (7ac32.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, 2b2e3.. (f482f.. (7ac32.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))), x5, decode_p (f482f.. (7ac32.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.
Let x6 of type ι → ο be given.
Assume H2: ∀ x7 . x6 x7 ⟶ prim1 x7 x1.
Apply unknownprop_76e354ddaaf5ea9ad81b81b42ecb99d89d4b1fa6ed8985ecdc96882fad13e5e2 with x1, x2, x3, x4, x5, x6, λ x7 x8 : ο . iff (x2 x6) x7 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying iff_refl with x2 x6.
The subproof is completed by applying unknownprop_4fc332daa2b99c12352c1d15dd590601e19fa9821e6ba1b89579fa710ea0d2a1 with x1, x2, x3, x4, x5.
Let x6 of type ι be given.
Assume H2: prim1 x6 x1.
Let x7 of type ι be given.
Assume H3: prim1 x7 x1.
Apply unknownprop_d1c17917281d83596bb85722df08e758bcfafa86d8f4cbeab8958beeb91edd03 with x1, x2, x3, x4, x5, x6, x7, λ x8 x9 : ο . iff (x4 x6 x7) x8 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying iff_refl with x4 x6 x7.
Let x6 of type ι be given.
Assume H2: prim1 x6 x1.
Apply unknownprop_3ae4f9831850519ac9905885268b7578d3c76b0ebb4555db0b7a62ea1e85c525 with x1, x2, x3, x4, x5, x6, λ x7 x8 : ο . iff (x5 x6) x7 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying iff_refl with x5 x6.
■