Search for blocks/addresses/...
Proofgold Proof
pf
Apply df_q__df_rp__df_xneg__df_xadd__df_xmul__df_ioo__df_ioc__df_ico__df_icc__df_fz__df_fzo__df_fl__df_ceil__df_mod__df_seq__df_exp__df_fac__df_bc with
wceq
cxad
(
cmpt2
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cif
(
wceq
(
cv
x0
)
cpnf
)
(
cif
(
wceq
(
cv
x1
)
cmnf
)
cc0
cpnf
)
(
cif
(
wceq
(
cv
x0
)
cmnf
)
(
cif
(
wceq
(
cv
x1
)
cpnf
)
cc0
cmnf
)
(
cif
(
wceq
(
cv
x1
)
cpnf
)
cpnf
(
cif
(
wceq
(
cv
x1
)
cmnf
)
cmnf
(
co
(
cv
x0
)
(
cv
x1
)
caddc
)
)
)
)
)
)
.
Assume H0:
wceq
cq
(
cima
cdiv
(
cxp
cz
cn
)
)
.
Assume H1:
wceq
crp
(
crab
(
λ x0 .
wbr
cc0
(
cv
x0
)
clt
)
(
λ x0 .
cr
)
)
.
Assume H2:
∀ x0 :
ι → ο
.
wceq
(
cxne
x0
)
(
cif
(
wceq
x0
cpnf
)
cmnf
(
cif
(
wceq
x0
cmnf
)
cpnf
(
cneg
x0
)
)
)
.
Assume H3:
wceq
cxad
(
cmpt2
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cif
(
wceq
(
cv
x0
)
cpnf
)
(
cif
(
wceq
(
cv
x1
)
cmnf
)
cc0
cpnf
)
(
cif
(
wceq
(
cv
x0
)
cmnf
)
(
cif
(
wceq
(
cv
x1
)
cpnf
)
cc0
cmnf
)
(
cif
(
wceq
(
cv
x1
)
cpnf
)
cpnf
(
cif
(
wceq
(
cv
x1
)
cmnf
)
cmnf
(
co
(
cv
x0
)
(
cv
x1
)
caddc
)
)
)
)
)
)
.
Assume H4:
wceq
cxmu
(
cmpt2
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cif
(
wo
(
wceq
(
cv
x0
)
cc0
)
(
wceq
(
cv
x1
)
cc0
)
)
cc0
(
cif
(
wo
(
wo
(
wa
(
wbr
cc0
(
cv
x1
)
clt
)
(
wceq
(
cv
x0
)
cpnf
)
)
(
wa
(
wbr
(
cv
x1
)
cc0
clt
)
(
wceq
(
cv
x0
)
cmnf
)
)
)
(
wo
(
wa
(
wbr
cc0
(
cv
x0
)
clt
)
(
wceq
(
cv
x1
)
cpnf
)
)
(
wa
(
wbr
(
cv
x0
)
cc0
clt
)
(
wceq
(
cv
x1
)
cmnf
)
)
)
)
cpnf
(
cif
(
wo
(
wo
(
wa
(
wbr
cc0
(
cv
x1
)
clt
)
(
wceq
(
cv
x0
)
cmnf
)
)
(
wa
(
wbr
(
cv
x1
)
cc0
clt
)
(
wceq
(
cv
x0
)
cpnf
)
)
)
(
wo
(
wa
(
wbr
cc0
(
cv
x0
)
clt
)
(
wceq
(
cv
x1
)
cmnf
)
)
(
wa
(
wbr
(
cv
x0
)
cc0
clt
)
(
wceq
(
cv
x1
)
cpnf
)
)
)
)
cmnf
(
co
(
cv
x0
)
(
cv
x1
)
...
)
)
)
)
)
.
...
■