Search for blocks/addresses/...

Proofgold Asset

asset id
60dbc8c9730c498f250505e3f1a9cee64b914f3e389f32c9a83b4eab4bd3dfff
asset hash
897fd1750433cd6cc969b7ed1ef1f0d0657a4fa104421e9c64c353530f58c668
bday / block
35066
tx
d030a..
preasset
doc published by PrAFa..
Known 86c40.. : ∀ x0 x1 x2 . equip x1 x0equip x2 x0equip x1 x2
Known 12ef8.. : ∀ x0 x1 . equip x0 0equip (setprod x0 x1) 0
Known 9f38c.. : ∀ x0 x1 . equip x1 0equip (setprod x0 x1) 0
Known FalseEFalseE : False∀ x0 : ο . x0
Param 69aae..exp_nat : ιιι
Known a84bb.. : ∀ x0 x1 x2 x3 . equip x0 x3equip x1 (ordsucc x3)equip_mod x0 x1 x2
Known 3fe1c..add_nat_com : ∀ x0 . nat_p x0∀ x1 . nat_p x1add_nat x0 x1 = add_nat x1 x0
Known 02169..add_nat_0R : ∀ x0 . add_nat x0 0 = x0
Known 2b177.. : ∀ x0 x1 . nat_p x1add_nat x0 (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc x1)))))))) = ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (add_nat x0 x1))))))))
Known 5af12.. : ∀ x0 . add_nat x0 2 = ordsucc (ordsucc x0)
Known 7bb3f.. : ∀ x0 x1 . nat_p x1add_nat x0 (ordsucc (ordsucc (ordsucc (ordsucc x1)))) = ordsucc (ordsucc (ordsucc (ordsucc (add_nat x0 x1))))
Known 54d4b..equip_ref : ∀ x0 . equip x0 x0
Known 9b388..mul_nat_1R : ∀ x0 . mul_nat x0 1 = x0
Known d6dd4.. : ∀ x0 . nat_p x0∀ x1 . nat_p x1∀ x2 x3 . equip x2 x0equip x3 x1equip (binrep x2 x3) (add_nat x0 (69aae.. 2 x1))
Known 63495.. : ∀ x0 . add_nat x0 1 = ordsucc x0
Known fddcf.. : 69aae.. 2 2 = 4
Known b2788.. : ∀ x0 . nat_p x0nat_p (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc x0))))))))
Known c83a0.. : ∀ x0 . nat_p x0nat_p (ordsucc (ordsucc (ordsucc (ordsucc x0))))
Known a2e43.. : ∀ x0 . nat_p x0nat_p (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc x0))))))))))))))))
Known 74cfe.. : ∀ x0 . nat_p x0nat_p (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc x0))))))))))))))))))))))))))))))))
Known 9e914.. : ∀ x0 x1 . nat_p x1add_nat x0 (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc x1)))))))))))))))) = ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (add_nat x0 x1))))))))))))))))
Known a62e2.. : ∀ x0 . equip x0 4equip (Power x0) 16
Known 02b3e.. : ∀ x0 . equip x0 3equip (Power x0) 8
Known 37c59..exp_nat_1 : ∀ x0 . 69aae.. x0 1 = x0
Known a1573.. : ∀ x0 . equip x0 2equip (Power x0) 4
Known 2b6ba.. : nat_p 4
Known f4890..exp_nat_S : ∀ x0 x1 . nat_p x169aae.. x0 (ordsucc x1) = mul_nat x0 (69aae.. x0 x1)
Known c7c31..nat_1 : nat_p 1
Known fad70..mul_nat_0R : ∀ x0 . mul_nat x0 0 = 0
Known 94de7..exp_nat_0 : ∀ x0 . 69aae.. x0 0 = 1
Known e6b7d.. : ∀ x0 . equip x0 1equip (Power x0) 2
Known 224e2.. : ∀ x0 . equip x0 0equip (Power x0) 1
Known 9814f.. : nat_p 3
Known 08405..nat_0 : nat_p 0
Known 36841..nat_2 : nat_p 2
Known 4c6ff.. : ∀ x0 . nat_p x0∀ x1 . nat_p x1∀ x2 x3 . equip x2 x0equip x3 x1equip (setexp x2 x3) (69aae.. x0 x1)
Known 912b9..equip_setprod_mul_nat_2 : ∀ x0 . nat_p x0∀ x1 . nat_p x1∀ x2 x3 . equip x2 x0equip x3 x1equip (setprod x2 x3) (mul_nat x0 x1)
Known 56707..equip_setsum_add_nat_2 : ∀ x0 . nat_p x0∀ x1 . nat_p x1∀ x2 x3 . equip x2 x0equip x3 x1equip (setsum x2 x3) (add_nat x0 x1)
Theorem 3c3f3.. : (∀ x0 x1 x2 . equip_mod (setsum (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 (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod (setexp x0 (binrep (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 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 (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))) (Power 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 (binrep (Power (Power (Power 0))) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod x1 (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod x1 x2))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) x1)) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 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 (Power 0))) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) x2)) (setsum (setprod (binrep (Power (Power 0)) 0) (setexp x0 (binrep (Power (Power 0)) 0))) (setsum (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 (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0)))))) (setsum (setprod (Power (Power 0)) (setprod (setexp x0 (Power (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) (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 (Power 0))) 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)) 0) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) (setexp x1 (Power (Power 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setprod x1 (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 (Power (Power 0))) (setprod x1 (setexp x2 (Power (Power 0)))))) (setsum (setprod (Power (Power 0)) (setprod (setexp x0 (Power (Power 0))) x1)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (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 (Power (binrep (Power (Power 0)) 0)) (setprod (setexp x0 (Power (Power 0))) x2)) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setexp x0 (Power (Power 0)))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 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 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 (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 (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod x0 (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod x0 (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (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 (Power (Power 0)))))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod x0 (setprod x1 x2))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod x0 x1)) (setsum (setprod (Power (Power (Power 0))) (setprod x0 (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 x0 (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod x0 x2)) (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)) (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 (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setexp x1 (binrep (Power (Power 0)) 0))) (setsum (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 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 (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setexp x1 (Power (Power 0)))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod x1 (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod x1 x2)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) x1) (setsum (setprod (Power (Power 0)) (setexp x2 (binrep (Power (Power 0)) 0))) (setsum (setexp x2 (Power (Power 0))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) x2) (binrep (Power (binrep (Power (Power 0)) 0)) 0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Power (Power (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)) (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)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x1 (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 (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 (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 (Power (Power 0))) x2))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x1 (Power (Power 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod x1 (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 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 (Power (Power (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 (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setexp x0 (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 (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 (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 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setexp x1 (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 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (Power (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 (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setprod x1 (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) (setprod x1 x2))) (setsum (setprod (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) x1)) (setsum (setprod (binrep (Power (Power 0)) 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 (setexp x0 (Power (Power 0))) x2) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 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 (Power (Power 0)) (setprod x0 (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod x0 (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) (setprod x0 (setexp x1 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod x0 (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (Power (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 (Power (binrep (Power (Power 0)) 0)) (setprod x0 (setexp x1 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod x0 (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (Power (Power 0)) (setprod x0 (setprod x1 (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 x1 x2))) (setsum (setprod (Power (Power 0)) (setprod x0 x1)) (setsum (setprod x0 (setexp x2 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod x0 (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) (setprod x0 x2)) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) x0) (setsum (setprod (binrep (Power (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 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 (Power 0))) (Power 0)) (setexp x1 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (Power (Power (Power 0))) (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 (Power 0))) (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))) (Power 0)) (setprod (setexp x1 (Power (Power 0))) x2)) (setsum (setprod (Power (Power (Power 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 (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) (setprod x1 (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod x1 x2)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) x1) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 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 (Power 0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (binrep (binrep (binrep (binrep (binrep (binrep (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 (Power (Power (Power (Power 0)))) (binrep (Power (Power 0)) 0)) (Power 0))) (binrep (Power (Power (Power (Power 0)))) (binrep (Power (Power 0)) 0))) (binrep (binrep (binrep (Power (Power (Power (Power 0)))) (Power (Power 0))) (Power 0)) 0)) (binrep (binrep (Power (Power (Power (Power 0)))) (Power (Power 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 (Power (Power (Power 0)))) (Power 0)) 0)) (binrep (Power (Power (Power (Power 0)))) (Power 0))) (binrep (Power (Power (Power (Power 0)))) 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 (Power 0))) 0)) (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0)) (binrep (Power (binrep (Power (Power 0)) 0)) 0)) (Power (binrep (Power (Power 0)) 0))) (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0)) (binrep (Power (Power (Power 0))) (Power 0))) (Power (Power 0))) (Power 0)) 0)False)∀ x0 : ο . x0 (proof)