Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: 3db62.. x0.
Apply H0 with λ x1 . x1 = 50ab0.. (f482f.. x1 4a7ef..) (f482f.. (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.
Assume H1: ∀ x3 . prim1 x3 x1 ⟶ prim1 (x2 x3) x1.
Let x3 of type ι → ι be given.
Assume H2: ∀ x4 . prim1 x4 x1 ⟶ prim1 (x3 x4) x1.
Let x4 of type ι → ι → ο be given.
Let x5 of type ι → ο be given.
Apply unknownprop_9b935f184e6ef19fd2887b24efdd6195f442b8ceca35e964096d01e16d81456d with x1, x2, x3, x4, x5, λ x6 x7 . 50ab0.. x1 x2 x3 x4 x5 = 50ab0.. x6 (f482f.. (f482f.. (50ab0.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (50ab0.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (50ab0.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. (50ab0.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))).
Apply unknownprop_61cd27499456a4b3be686ed5c9824e9b56fc4a7e385dcdbd01b9134351a43133 with x1, x2, f482f.. (f482f.. (50ab0.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, f482f.. (f482f.. (50ab0.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, 2b2e3.. (f482f.. (50ab0.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))), x5, decode_p (f482f.. (50ab0.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.
The subproof is completed by applying unknownprop_33b004c8f62843bcba581c3bb62c1b6860ed0922825af08a3ae7ea18e3233657 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_cc298fd33dfe686ee7b576905469258d62cae8b4852e26a02f0aa0c50d1f2c8b with x1, x2, x3, x4, x5.
Let x6 of type ι be given.
Assume H3: prim1 x6 x1.
Let x7 of type ι be given.
Assume H4: prim1 x7 x1.
Apply unknownprop_4d5576adce78b831f45c33ebbe5605fa8b4e2b873b249b058e32db9cb78c1ede with x1, x2, x3, x4, x5, x6, x7, λ x8 x9 : ο . iff (x4 x6 x7) x8 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying iff_refl with x4 x6 x7.
Let x6 of type ι be given.
Assume H3: prim1 x6 x1.
Apply unknownprop_83e4e93ebfb84f8cd49bab263850d2028f52dcb8263fa261f8e447c5e6ace519 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.
■