Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: 7c481.. x0.
Apply H0 with λ x1 . x1 = 94613.. (f482f.. x1 4a7ef..) (e3162.. (f482f.. x1 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (e3162.. (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 ⟶ ∀ x6 . prim1 x6 x1 ⟶ prim1 (x4 x5 x6) x1.
Let x5 of type ι → ο be given.
Apply unknownprop_996291121317bd28c520c8830689109eaa5eb658691dbcb92ca5dc25aa0668cb with x1, x2, x3, x4, x5, λ x6 x7 . 94613.. x1 x2 x3 x4 x5 = 94613.. x6 (e3162.. (f482f.. (94613.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (94613.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (e3162.. (f482f.. (94613.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. (94613.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))).
Apply unknownprop_8f3a91ac69573a69747ca90a3388651f93cf611176f50719cab8751454e754aa with x1, x2, e3162.. (f482f.. (94613.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, e3162.. (f482f.. (94613.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, e3162.. (f482f.. (94613.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))), x5, decode_p (f482f.. (94613.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.
The subproof is completed by applying unknownprop_fc264994e9fe69947f39a2155e3b678222607a73685180f878ae6bee13d7c92e with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_f06030f48dfa8b9a3ae3b2086298a361c60007f8d582114218ce4d0e9b3c2f15 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_37557e7f0ffd09d385c71300094cf77a808eb546d116f78961140ab099ada3d4 with x1, x2, x3, x4, x5.
Let x6 of type ι be given.
Assume H4: prim1 x6 x1.
Apply unknownprop_afe428c5c12956c8dfb4d90a681589485dc1dc57c1822e0cb3a9b977019fa9eb 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.
■