Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: ∀ x0 x1 x2 . equip_mod (setsum (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2))) (setsum (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x1 (binrep (Power (Power 0)) 0))) (setsum (setprod (Power (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x1 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum ... ...)))))))))) ...) ... ...False.
...