Search for blocks/addresses/...

Proofgold Proposition

(∀ x0 x1 x2 . equip_mod (setsum (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 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 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 (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod (setexp x0 (binrep (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) (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))) x2))) (setsum (setprod (Power (Power (Power 0))) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x1 (Power (Power 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod x1 x2))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) x1)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0))))) (setsum (setprod (setexp x0 (binrep (Power (Power 0)) 0)) x2) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (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 (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 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 (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (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 (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (binrep (Power (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 (setexp x0 (Power (Power 0))) (setprod x1 (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setprod x1 x2))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod (setexp x0 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod (setexp x0 (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 (setexp x0 (Power (Power 0))) x2)) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setexp x0 (Power (Power 0)))) (setsum (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 (Power 0))) (setprod x0 (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (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 (Power (Power 0)) 0) (setprod x0 (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 x0 (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod x0 (setexp x1 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod x0 (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setprod x0 (setprod x1 (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod x0 (setprod x1 x2))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) (setprod x0 x1)) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod x0 (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod x0 (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod x0 x2)) (setsum (setprod (binrep (Power (Power (Power 0))) 0) x0) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 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))) 0) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2)) (setsum (setprod (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) (setexp x1 (binrep (Power (Power 0)) 0))) (setsum (setprod (Power (Power (Power 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 0)) 0) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0))))) (setsum (setprod (Power (Power (Power 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 (binrep (Power (Power 0)) 0) (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod x1 (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod x1 x2)) (setsum (setprod (binrep (Power (Power (Power 0))) 0) x1) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0))) (setsum (setprod (Power (Power (Power 0))) (setexp x2 (Power (Power 0)))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) x2) (binrep (Power (Power (Power 0))) (Power 0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Power (Power (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)) (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 (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 (binrep (Power (Power (Power 0))) (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 (binrep (Power (binrep (Power (Power 0)) 0)) (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 (binrep (Power (Power 0)) 0)) (Power (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 (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 (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 x1 x2))) (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)) x1)) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod (setexp x0 (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)) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (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 (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (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 (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod (setexp x0 (Power (Power 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 x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod (setexp x0 (Power (Power 0))) (setexp x1 (binrep (Power (Power 0)) 0)))) (setsum (setprod (Power (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setexp x1 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (Power (Power 0)) 0) (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)) 0) (setprod (setexp x0 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod (setexp x0 (Power (Power 0))) x2)) (setsum (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 x0 (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))) (Power 0)) (setprod x0 (setexp x1 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod x0 (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setprod x0 (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 x0 (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod x0 (setexp x1 (Power (Power 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod x0 (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod x0 (setprod x1 (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod x0 (setprod x1 x2))) (setsum (setprod (Power (Power (Power 0))) (setprod x0 x1)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod x0 (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod x0 x2) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) x0) (setsum (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 x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 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 (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod (setexp x1 (Power (Power 0))) x2)) (setsum (setprod (Power (Power (Power 0))) (setexp x1 (Power (Power 0)))) (setsum (setprod (Power (binrep (Power (Power 0)) 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 (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod x1 x2)) (setsum (setprod (binrep (Power (Power 0)) 0) x1) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setexp x2 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setexp x2 (Power (Power 0)))) (setsum (setprod (Power (Power (Power 0))) x2) (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (binrep (binrep (binrep (binrep (binrep (binrep (binrep (binrep (binrep (binrep (binrep (binrep (binrep (Power (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)))) (binrep (Power (Power 0)) 0)) 0)) (binrep (Power (Power (Power (Power 0)))) (binrep (Power (Power 0)) 0))) (binrep (Power (Power (Power (Power 0)))) (Power (Power 0)))) (binrep (Power (Power (Power (Power 0)))) (Power 0))) (binrep (Power (Power (Power (Power 0)))) 0)) (Power (Power (Power (Power 0))))) (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0)) (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0)) (Power (binrep (Power (Power 0)) 0))) (binrep (Power (Power (Power 0))) (Power 0))) (binrep (Power (Power (Power 0))) 0))False)∀ x0 : ο . x0
type
prop
theory
HF
name
-
proof
PUcCM..
Megalodon
-
proofgold address
TMQC5..
creator
22392 PrBTh../01271..
owner
22392 PrBTh../01271..
term root
13e69..