Search for blocks/addresses/...
Proofgold Proof
pf
Apply df_sub__df_neg__df_div__df_nn__df_2__df_3__df_4__df_5__df_6__df_7__df_8__df_9__df_10OLD__df_n0__df_xnn0__df_z__df_dec__df_uz with
wceq
c2
(
co
c1
c1
caddc
)
.
Assume H0:
wceq
cmin
(
cmpt2
(
λ x0 x1 .
cc
)
(
λ x0 x1 .
cc
)
(
λ x0 x1 .
crio
(
λ x2 .
wceq
(
co
(
cv
x1
)
(
cv
x2
)
caddc
)
(
cv
x0
)
)
(
λ x2 .
cc
)
)
)
.
Assume H1:
∀ x0 :
ι → ο
.
wceq
(
cneg
x0
)
(
co
cc0
x0
cmin
)
.
Assume H2:
wceq
cdiv
(
cmpt2
(
λ x0 x1 .
cc
)
(
λ x0 x1 .
cdif
cc
(
csn
cc0
)
)
(
λ x0 x1 .
crio
(
λ x2 .
wceq
(
co
(
cv
x1
)
(
cv
x2
)
cmul
)
(
cv
x0
)
)
(
λ x2 .
cc
)
)
)
.
Assume H3:
wceq
cn
(
cima
(
crdg
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
co
(
cv
x0
)
c1
caddc
)
)
c1
)
com
)
.
Assume H4:
wceq
c2
(
co
c1
c1
caddc
)
.
Assume H5:
wceq
c3
(
co
c2
c1
caddc
)
.
Assume H6:
wceq
c4
(
co
c3
c1
caddc
)
.
Assume H7:
wceq
c5
(
co
c4
c1
caddc
)
.
Assume H8:
wceq
c6
(
co
c5
c1
caddc
)
.
Assume H9:
wceq
c7
(
co
c6
c1
caddc
)
.
Assume H10:
wceq
c8
(
co
c7
c1
caddc
)
.
Assume H11:
wceq
c9
(
co
c8
c1
caddc
)
.
Assume H12:
wceq
c10
(
co
c9
c1
caddc
)
.
Assume H13:
wceq
cn0
(
cun
cn
(
csn
cc0
)
)
.
Assume H14:
wceq
cxnn0
(
cun
cn0
(
csn
cpnf
)
)
.
Assume H15:
wceq
cz
(
crab
(
λ x0 .
w3o
(
wceq
(
cv
x0
)
cc0
)
(
wcel
(
cv
x0
)
cn
)
(
wcel
(
cneg
(
cv
x0
)
)
cn
)
)
(
λ x0 .
cr
)
)
.
Assume H16:
∀ x0 x1 :
ι → ο
.
wceq
(
cdc
x0
x1
)
(
co
(
co
(
co
c9
c1
caddc
)
x0
cmul
)
x1
caddc
)
.
Assume H17:
wceq
cuz
(
cmpt
(
λ x0 .
cz
)
(
λ x0 .
crab
(
λ x1 .
wbr
(
cv
x0
)
(
cv
x1
)
cle
)
(
λ x1 .
cz
)
)
)
.
The subproof is completed by applying H4.
■