Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type (ιο) → ο be given.
Let x3 of type (ιο) → ο be given.
Let x4 of type ιιι be given.
Let x5 of type ιιι be given.
Let x6 of type ιιο be given.
Let x7 of type ιιο be given.
Let x8 of type ιο be given.
Let x9 of type ιο be given.
Assume H0: d4d11.. x0 x2 x4 x6 x8 = d4d11.. x1 x3 x5 x7 x9.
Claim L1: ...
...
Claim L2: ...
...
Apply and5I with x0 = x1, ∀ x10 : ι → ο . (∀ x11 . x10 x11prim1 x11 x0)x2 x10 = x3 x10, ∀ x10 . prim1 x10 x0∀ x11 . prim1 x11 x0x4 x10 x11 = x5 x10 x11, ∀ x10 . prim1 x10 x0∀ x11 . prim1 x11 x0x6 x10 x11 = x7 x10 x11, ∀ x10 . prim1 x10 x0x8 x10 = x9 x10 leaving 5 subgoals.
The subproof is completed by applying L2.
Let x10 of type ιο be given.
Assume H3: ∀ x11 . x10 x11prim1 x11 x0.
Apply unknownprop_a13f39ce3530571ab5d7d409efb9808d2175605b15fc1b6ce954f75d09f6b2e8 with x0, x2, x4, x6, x8, x10, λ x11 x12 : ο . x12 = x3 x10 leaving 2 subgoals.
The subproof is completed by applying H3.
Claim L4: ∀ x11 . x10 x11prim1 x11 x1
Apply L2 with λ x11 x12 . ∀ x13 . x10 x13prim1 x13 x11.
The subproof is completed by applying H3.
Apply H0 with λ x11 x12 . decode_c (f482f.. x12 (4ae4a.. 4a7ef..)) x10 = x3 x10.
Let x11 of type οοο be given.
Apply unknownprop_a13f39ce3530571ab5d7d409efb9808d2175605b15fc1b6ce954f75d09f6b2e8 with x1, x3, x5, x7, x9, x10, λ x12 x13 : ο . x11 x13 x12.
The subproof is completed by applying L4.
Let x10 of type ι be given.
Assume H3: prim1 x10 x0.
Let x11 of type ι be given.
Assume H4: prim1 x11 x0.
Apply unknownprop_176a3e345e9291817f18fc19bfb2975b27525c4a82c8e0443a0f749010f60e60 with x0, x2, x4, x6, x8, x10, x11, λ x12 x13 . x13 = x5 x10 x11 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Claim L5: prim1 x10 x1
Apply L2 with λ x12 x13 . prim1 x10 x12.
The subproof is completed by applying H3.
Claim L6: prim1 x11 x1
Apply L2 with λ x12 x13 . prim1 x11 x12.
The subproof is completed by applying H4.
Apply H0 with λ x12 x13 . e3162.. (f482f.. x13 (4ae4a.. (4ae4a.. 4a7ef..))) x10 x11 = x5 x10 x11.
Let x12 of type ιιο be given.
Apply unknownprop_176a3e345e9291817f18fc19bfb2975b27525c4a82c8e0443a0f749010f60e60 with x1, x3, x5, x7, x9, x10, x11, λ x13 x14 . x12 x14 x13 leaving 2 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying L6.
Let x10 of type ι be given.
Assume H3: prim1 x10 x0.
Let x11 of type ι be given.
Assume H4: prim1 x11 x0.
Apply unknownprop_89af4783e9576b1d0a6b988eb1fbb58f946402e826b60b72738feba68dd40cce with x0, x2, x4, x6, x8, x10, x11, λ x12 x13 : ο . x13 = x7 x10 x11 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Claim L5: prim1 x10 x1
Apply L2 with λ x12 x13 . prim1 x10 x12.
The subproof is completed by applying H3.
Claim L6: prim1 x11 x1
Apply L2 with λ x12 x13 . prim1 x11 x12.
The subproof is completed by applying H4.
Apply H0 with λ x12 x13 . 2b2e3.. (f482f.. x13 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x10 x11 = x7 x10 x11.
Let x12 of type οοο be given.
Apply unknownprop_89af4783e9576b1d0a6b988eb1fbb58f946402e826b60b72738feba68dd40cce with x1, x3, x5, x7, x9, x10, x11, λ x13 x14 : ο . x12 x14 x13 leaving 2 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying L6.
Let x10 of type ι be given.
Assume H3: prim1 x10 x0.
Apply unknownprop_818c354870766ca0d98d8f35da722912c8cfdc27ac6bcafebe688cfcdef505b7 with x0, x2, x4, x6, x8, x10, λ x11 x12 : ο . x12 = x9 x10 leaving 2 subgoals.
The subproof is completed by applying H3.
Claim L4: ...
...
Apply H0 with λ x11 x12 . decode_p ... ... = ....
...