Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: 04214.. x0.
Apply H0 with λ x1 . x1 = dd5e6.. (f482f.. x1 4a7ef..) (f482f.. (f482f.. x1 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (2b2e3.. (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_746c504ce6d83f9198628211620c6dd932e9ad2ee5565467ff3c37a1a593fb8e with x1, x2, x3, x4, x5, λ x6 x7 . dd5e6.. x1 x2 x3 x4 x5 = dd5e6.. x6 (f482f.. (f482f.. (dd5e6.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (dd5e6.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (dd5e6.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (2b2e3.. (f482f.. (dd5e6.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))).
Apply unknownprop_94fd551ed96a42a4de9a4a3f96fe90d87c2151538e6c23e040dd8ac138e36f9c with x1, x2, f482f.. (f482f.. (dd5e6.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, f482f.. (f482f.. (dd5e6.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, 2b2e3.. (f482f.. (dd5e6.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))), x5, 2b2e3.. (f482f.. (dd5e6.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.
The subproof is completed by applying unknownprop_5c0dfa81d135413630d40198f380b99880d733daeee8e129b4a5d28d7d207083 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_9a2968cd6fb30108e6f9e7f55ebbd94ee83065a46958e63af2137d297ff71f1e 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_5cb8388f483d51e46bdfc58663301ae218a26e1890aaa5ae374d943cb2c0b71e 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.
Let x7 of type ι be given.
Assume H4: prim1 x7 x1.
Apply unknownprop_01493f66cd210cbabae1129d96b075b27bb1d5f8be40aad66910afee0cc11964 with x1, x2, x3, x4, x5, x6, x7, λ x8 x9 : ο . iff (x5 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 x5 x6 x7.
■