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.
Assume H0: ∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x1 x7 x8 = x2 x7 x8.
Assume H1: ∀ x7 . prim1 x7 x0iff (x3 x7) (x4 x7).
Claim L2: ...
...
Apply L2 with λ x7 x8 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x9 . If_i (x9 = 4a7ef..) x0 (If_i (x9 = 4ae4a.. 4a7ef..) (eb53d.. x0 x1) (If_i (x9 = 4ae4a.. (4ae4a.. 4a7ef..)) (1216a.. x0 x3) (If_i (x9 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6)))) = 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x9 . If_i (x9 = 4a7ef..) x0 (If_i (x9 = 4ae4a.. 4a7ef..) x7 (If_i (x9 = 4ae4a.. (4ae4a.. 4a7ef..)) (1216a.. x0 x4) (If_i (x9 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6)))).
Claim L3: ...
...
Apply L3 with λ x7 x8 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x9 . If_i (x9 = 4a7ef..) x0 (If_i (x9 = 4ae4a.. 4a7ef..) (eb53d.. x0 x1) (If_i (x9 = 4ae4a.. (4ae4a.. 4a7ef..)) (1216a.. x0 x3) (If_i (x9 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6)))) = 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x9 . If_i (x9 = 4a7ef..) x0 (If_i (x9 = 4ae4a.. 4a7ef..) (eb53d.. x0 x1) (If_i (x9 = 4ae4a.. (4ae4a.. 4a7ef..)) x7 (If_i (x9 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6)))).
Let x7 of type ιιο be given.
Assume H4: x7 (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x8 . If_i (x8 = 4a7ef..) x0 (If_i (x8 = 4ae4a.. 4a7ef..) (eb53d.. x0 x1) (If_i (x8 = 4ae4a.. (4ae4a.. 4a7ef..)) (1216a.. x0 x3) (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6))))) (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x8 . If_i (x8 = 4a7ef..) x0 (If_i (x8 = 4ae4a.. 4a7ef..) (eb53d.. x0 x1) (If_i (x8 = 4ae4a.. (4ae4a.. 4a7ef..)) (1216a.. x0 x3) (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6))))).
...