Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: f1fbf.. x0.
Apply H0 with λ x1 . x1 = 9b6e8.. (f482f.. x1 4a7ef..) (e3162.. (f482f.. x1 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (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 x1prim1 (x2 x3 x4) x1.
Let x3 of type ιι be given.
Assume H2: ∀ x4 . prim1 x4 x1prim1 (x3 x4) x1.
Let x4 of type ι be given.
Assume H3: prim1 x4 x1.
Let x5 of type ι be given.
Assume H4: prim1 x5 x1.
Apply unknownprop_0663073412d695176e3e23ffbbbb5da2857252d5c0f47051c9f0c33ecb11f4b6 with x1, x2, x3, x4, x5, λ x6 x7 . 9b6e8.. x1 x2 x3 x4 x5 = 9b6e8.. x6 (e3162.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).
Apply unknownprop_a5be19faa2e80b8da858086292146d3f609318d0df557aec5c9ce5a6ab6b4ab0 with x1, x2, x3, x4, x5, λ x6 x7 . 9b6e8.. x1 x2 x3 x4 x5 = 9b6e8.. x1 (e3162.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).
Apply unknownprop_c1003d86b72ccf1c88f05bbb3160c1287244e653b755f6f0f8f6e6dea303f1e4 with x1, x2, x3, x4, x5, λ x6 x7 . 9b6e8.. x1 x2 x3 x4 x5 = 9b6e8.. x1 (e3162.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x6.
Apply unknownprop_7d246bf0e68f4796fefa8cfbc9dab886d0e6d737797c87a6ed01831e1a2add66 with x1, x2, e3162.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, f482f.. (f482f.. (9b6e8.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, x5 leaving 2 subgoals.
The subproof is completed by applying unknownprop_a0d932da53985136bc4d111609d0ae5a2ed2e4f1789b9bd8811552fd687d1136 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_c64bca701150bd7d152f116af6a1108b34c2b6e6d2765f2dada41711a2cb9dfa with x1, x2, x3, x4, x5.