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.
Assume H0: ∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0iff (x1 x6 x7) (x2 x6 x7).
Assume H1: ∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0iff (x3 x6 x7) (x4 x6 x7).
Claim L2: d2155.. x0 x1 = d2155.. x0 x2
Apply unknownprop_75d5b46497f20dc30e2e5351a60197c4fa9d445bc23c6c8245597bb858180907 with x0, x1, x2.
The subproof is completed by applying H0.
Apply L2 with λ x6 x7 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x8 . If_i (x8 = 4a7ef..) x0 (If_i (x8 = 4ae4a.. 4a7ef..) (d2155.. x0 x1) (If_i (x8 = 4ae4a.. (4ae4a.. 4a7ef..)) (d2155.. x0 x3) x5))) = 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x8 . If_i (x8 = 4a7ef..) x0 (If_i (x8 = 4ae4a.. 4a7ef..) x6 (If_i (x8 = 4ae4a.. (4ae4a.. 4a7ef..)) (d2155.. x0 x4) x5))).
Claim L3: d2155.. x0 x3 = d2155.. x0 x4
Apply unknownprop_75d5b46497f20dc30e2e5351a60197c4fa9d445bc23c6c8245597bb858180907 with x0, x3, x4.
The subproof is completed by applying H1.
Apply L3 with λ x6 x7 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x8 . If_i (x8 = 4a7ef..) x0 (If_i (x8 = 4ae4a.. 4a7ef..) (d2155.. x0 x1) (If_i (x8 = 4ae4a.. (4ae4a.. 4a7ef..)) (d2155.. x0 x3) x5))) = 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x8 . If_i (x8 = 4a7ef..) x0 (If_i (x8 = 4ae4a.. 4a7ef..) (d2155.. x0 x1) (If_i (x8 = 4ae4a.. (4ae4a.. 4a7ef..)) x6 x5))).
Let x6 of type ιιο be given.
Assume H4: x6 (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x7 . If_i (x7 = 4a7ef..) x0 (If_i (x7 = 4ae4a.. 4a7ef..) (d2155.. x0 x1) (If_i (x7 = 4ae4a.. (4ae4a.. 4a7ef..)) (d2155.. x0 x3) x5)))) (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x7 . If_i (x7 = 4a7ef..) x0 (If_i (x7 = 4ae4a.. 4a7ef..) (d2155.. x0 x1) (If_i (x7 = 4ae4a.. (4ae4a.. 4a7ef..)) (d2155.. x0 x3) x5)))).
The subproof is completed by applying H4.