Search for blocks/addresses/...
Proofgold Proposition
(
∀ x0 x1 x2 .
equip
(
setsum
(
setsum
(
setprod
(
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
(
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
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x2
)
)
)
(
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
(
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
)
)
)
(
Power
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
(
Power
0
)
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x1
(
Power
(
Power
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
x1
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
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
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x1
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
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
(
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
)
)
(
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
(
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
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
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
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
0
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setexp
x1
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
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
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
x1
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
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
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setprod
(
setexp
x0
(
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
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
(
setprod
(
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
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
x0
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
(
Power
0
)
)
)
(
setprod
x0
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
x0
(
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
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
)
)
)
(
Power
0
)
)
(
setprod
x0
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
x2
)
)
)
(
setsum
(
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
(
Power
0
)
)
)
(
setprod
x0
(
setprod
x1
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
(
setprod
x0
(
setprod
x1
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setprod
x0
x1
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
0
)
)
0
)
(
setprod
x0
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
0
)
)
(
setprod
x0
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
0
)
)
(
setprod
x0
x2
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
x0
)
(
setsum
(
setprod
(
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
(
Power
(
Power
0
)
)
)
(
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
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
0
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
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
x1
(
Power
(
Power
0
)
)
)
x2
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
setexp
x1
(
Power
(
Power
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
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
x1
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
x1
x2
)
(
setsum
(
setprod
(
Power
(
Power
(
Power
0
)
)
)
x1
)
(
setsum
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
(
setsum
x2
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(
Power
(
Power
(
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
(
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
(
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
)
)
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
Power
(
Power
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
(
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
)
)
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
0
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x1
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
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
(
Power
(
Power
0
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
x1
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x1
)
)
(
setsum
(
setprod
(
binrep
(
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
0
)
)
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
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
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
(
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
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
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
)
)
)
(
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
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
binrep
(
Power
(
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
(
Power
(
Power
0
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
x1
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
x1
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
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
(
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
(
binrep
(
Power
(
Power
0
)
)
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
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
x0
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x2
)
)
)
(
setsum
(
setprod
x0
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
(
setsum
(
setprod
(
Power
(
Power
0
)
)
(
setprod
x0
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
x0
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
(
Power
0
)
)
)
(
setprod
x0
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
(
setprod
x0
(
setexp
x1
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
x0
(
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
x0
(
setprod
x1
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
(
setprod
x0
(
setprod
x1
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
(
setprod
x0
x1
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
x0
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
0
)
)
0
)
(
setprod
x0
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
x0
x2
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
0
)
x0
)
(
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
(
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
(
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
)
)
)
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
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
x1
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
0
)
(
setprod
x1
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setprod
x1
x2
)
)
(
setsum
(
setprod
(
Power
(
Power
(
Power
0
)
)
)
x1
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
x2
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
⟶
False
)
⟶
∀ x0 : ο .
x0
type
prop
theory
HF
name
-
proof
PUdqy..
Megalodon
-
proofgold address
TMdp2..
creator
22398
PrBTh..
/
ce1e9..
owner
22398
PrBTh..
/
ce1e9..
term root
4ff6f..