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: a3459.. x0 x2 x4 x6 x8 = a3459.. x1 x3 x5 x7 x9.
Claim L1: x1 = f482f.. (a3459.. x0 x2 x4 x6 x8) 4a7ef..
Apply unknownprop_5dace1e87a84357530b97ff9ad3bd9b43b92295b7638cf3c2712453650299ce8 with a3459.. x0 ... ... ... ..., ..., ..., ..., ..., ....
...
Claim L2: x0 = x1
Apply L1 with λ x10 x11 . x0 = x11.
The subproof is completed by applying unknownprop_97c6febb4d48ff36e4cb1a67ae96e731bb4d0d88ae631b336ee8d751a8ea3644 with x0, x2, x4, x6, x8.
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 x0x6 x10 = x7 x10, x8 = x9 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_f126e736effd1cf0374523a6b7386d5add53fdd920a5f78d4f4f605963832861 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_f126e736effd1cf0374523a6b7386d5add53fdd920a5f78d4f4f605963832861 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_3b64a3196710182a4d35cba1546eee2e2f7980f2ed75b429503d9f04f3d32e71 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 . 2b2e3.. (f482f.. x13 (4ae4a.. (4ae4a.. 4a7ef..))) x10 x11 = x5 x10 x11.
Let x12 of type οοο be given.
Apply unknownprop_3b64a3196710182a4d35cba1546eee2e2f7980f2ed75b429503d9f04f3d32e71 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_a2cc32195c89ba000a0e2e102a49e880cf6082a249cefcf846a21241ed3c6cf3 with x0, x2, x4, x6, x8, x10, λ x11 x12 : ο . x12 = x7 x10 leaving 2 subgoals.
The subproof is completed by applying H3.
Claim L4: prim1 x10 x1
Apply L2 with λ x11 x12 . prim1 x10 x11.
The subproof is completed by applying H3.
Apply H0 with λ x11 x12 . decode_p (f482f.. x12 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x10 = x7 x10.
Let x11 of type οοο be given.
Apply unknownprop_a2cc32195c89ba000a0e2e102a49e880cf6082a249cefcf846a21241ed3c6cf3 with x1, x3, x5, x7, x9, x10, λ x12 x13 : ο . x11 x13 x12.
The subproof is completed by applying L4.
Apply unknownprop_68fa418e80e05b5f5d85946aaba333bbaea1a45e6bff44a3e7bbfdbb8602422f with x0, x2, x4, x6, x8, λ x10 x11 . x11 = x9.
Apply H0 with λ x10 x11 . f482f.. x11 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = x9.
Let x10 of type ιιο be given.
The subproof is completed by applying unknownprop_68fa418e80e05b5f5d85946aaba333bbaea1a45e6bff44a3e7bbfdbb8602422f with x1, x3, x5, x7, x9, λ x11 x12 . x10 x12 x11.