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.
Assume H0: 6b90c.. x0 x1 = 6b90c.. x2 x3.
Apply unknownprop_f4ff16b9b21fb43bec0dd0d2e94569d632f3d21b75932b9bcc0c1ffd4c0d62b6 with x0, x1, x2, x3.
Apply unknownprop_3b55668ebff4b5090f31d28781617fd36508e9eaa3458c4a604deaa4db096497 with prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x4 x5)) (prim0 (prim0 x5 x5) (prim0 x4 x4))))) (prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x4 x5)) (prim0 (prim0 x4 x4) (prim0 x4 x4))))) (prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x4 x4)) (prim0 (prim0 x5 x5) (prim0 x4 x5))))) (prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x4 x5)) (prim0 (prim0 x5 x4) (prim0 x5 x4))))) (prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x5 x4)) (prim0 (prim0 x4 x4) (prim0 x4 x4))))) (prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x4 x4)) (prim0 (prim0 x5 x5) (prim0 x4 x4))))) (prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x4 x5)) (prim0 (prim0 x4 x5) (prim0 x5 x4))))) (prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x4 x5)) (prim0 (prim0 x4 x4) (prim0 x5 x4))))) (prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x4 x4)) (prim0 (prim0 x5 x5) (prim0 x5 x5))))) (prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x4 x5)) (prim0 (prim0 x4 x4) (prim0 x5 x5))))) (prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x4 x5)) (prim0 (prim0 x4 x5) (prim0 x5 x4))))) (prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x4 x5)) (prim0 (prim0 x5 x5) (prim0 x4 ...))))) ...))))))))))), ..., ..., ....
...