Search for blocks/addresses/...

Proofgold Proposition

(∀ 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 (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod x1 (setexp x2 (Power (Power 0)))))) (setsum (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod x1 x2)) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) x1)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0)))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) x2)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setexp x0 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0))))) (setsum (setprod (Power (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2))) (setsum (setprod (Power (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setexp x1 (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 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x0 (Power (Power 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))) 0) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setexp x1 (Power (Power 0))))) (setsum (setprod (Power (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setprod x1 (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 (Power (Power 0))) (setprod x1 (setexp x2 (Power (Power 0)))))) (setsum (setprod (setexp x0 (Power (Power 0))) (setprod x1 x2)) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod (setexp x0 (Power (Power 0))) x1)) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod (setexp x0 (Power (Power 0))) (setexp x2 (Power (Power 0))))) (setsum (setprod (Power (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) x2)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setexp x0 (Power (Power 0)))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod x0 (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setprod x0 (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod x0 (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2))) (setsum (setprod (Power (Power 0)) (setprod x0 (setexp x1 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod x0 (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (Power (Power (Power 0))) (setprod x0 (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0)))))) (setsum (setprod (Power (Power 0)) (setprod x0 (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod x0 (setexp x1 (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod x0 (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod x0 (setprod x1 (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod x0 (setprod x1 x2))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod x0 x1)) (setsum (setprod (Power (Power 0)) (setprod x0 (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) (setprod x0 (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod x0 x2)) (setsum x0 (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2)) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setexp x1 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod (setexp x1 (Power (Power 0))) x2)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) (setexp x1 (Power (Power 0)))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod x1 (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod x1 x2)) (setsum (setprod (Power (Power (Power 0))) x1) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setexp x2 (Power (Power 0)))) (Power 0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Power (Power (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (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 (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0)))))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x1 (binrep (Power (Power 0)) 0)))) (setsum (setprod (Power (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 (binrep (Power (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 (Power (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x1 (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (Power (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod x1 x2))) (setsum (setprod (setexp x0 (binrep (Power (Power 0)) 0)) x1) (setsum (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 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)) x2)) (setsum (setprod (Power (Power (Power 0))) (setexp x0 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (Power (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0)))))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2))) (setsum (setprod (Power (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setexp x1 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (Power (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (Power (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setexp x1 (Power (Power 0))))) (setsum (setprod (setexp x0 (Power (Power 0))) (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setprod x1 (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setprod x1 x2))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) x1)) (setsum (setprod (Power (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (Power (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod (setexp x0 (Power (Power 0))) x2)) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setexp x0 (Power (Power 0)))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod x0 (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod x0 (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod x0 (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2))) (setsum (setprod (Power (Power (Power 0))) (setprod x0 (setexp x1 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod x0 (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod x0 (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) (setprod x0 (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) (setprod x0 (setexp x1 (Power (Power 0))))) (setsum (setprod (Power (Power 0)) (setprod x0 (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod x0 (setprod x1 (setexp x2 (Power (Power 0)))))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod x0 (setprod x1 x2))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod x0 x1)) (setsum (setprod (Power (Power 0)) (setprod x0 (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod x0 (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod x0 x2)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) x0) (setsum (setprod (Power (Power 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setexp x1 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod (setexp x1 (Power (Power 0))) x2)) (setsum (setprod (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) (setexp x1 (Power (Power 0)))) (setsum (setprod (Power (Power (Power 0))) (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod x1 (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod x1 x2)) (setsum x1 (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setexp x2 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (Power (Power 0)) 0) (setexp x2 (Power (Power 0)))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) x2) (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (binrep (binrep (binrep (binrep (binrep (binrep (binrep (binrep (binrep (binrep (binrep (binrep (binrep (Power (binrep (binrep (binrep (Power (Power (Power (Power 0)))) (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0)) (binrep (binrep (Power (Power (Power (Power 0)))) (binrep (Power (Power 0)) 0)) (Power (Power 0)))) (binrep (binrep (binrep (Power (Power (Power (Power 0)))) (binrep (Power (Power 0)) 0)) (Power 0)) 0)) (binrep (binrep (Power (Power (Power (Power 0)))) (binrep (Power (Power 0)) 0)) (Power 0))) (binrep (binrep (Power (Power (Power (Power 0)))) (Power (Power 0))) 0)) (binrep (Power (Power (Power (Power 0)))) (Power (Power 0)))) (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0)) (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0))) (binrep (Power (Power (Power 0))) (Power 0))) (binrep (Power (Power (Power 0))) 0)) (Power (Power (Power 0)))) (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0))False)∀ x0 : ο . x0
type
prop
theory
HF
name
-
proof
PUh4o..
Megalodon
-
proofgold address
TMJfj..
creator
35071 PrAFa../c513d..
owner
35071 PrAFa../c513d..
term root
98f2a..