Search for blocks/addresses/...
Proofgold Proof
pf
Apply df_md__df_dmd__df_at__df_dp2__df_dp__df_xdiv__ax_xrssca__ax_xrsvsca__df_omnd__df_ogrp__df_sgns__df_inftm__df_archi__df_slmd__df_orng__df_ofld__df_resv__df_smat with
wceq
cmd
(
copab
(
λ x0 x1 .
wa
(
wa
(
wcel
(
cv
x0
)
cch
)
(
wcel
(
cv
x1
)
cch
)
)
(
wral
(
λ x2 .
wss
(
cv
x2
)
(
cv
x1
)
⟶
wceq
(
cin
(
co
(
cv
x2
)
(
cv
x0
)
chj
)
(
cv
x1
)
)
(
co
(
cv
x2
)
(
cin
(
cv
x0
)
(
cv
x1
)
)
chj
)
)
(
λ x2 .
cch
)
)
)
)
.
Assume H0:
wceq
cmd
(
copab
(
λ x0 x1 .
wa
(
wa
(
wcel
(
cv
x0
)
cch
)
(
wcel
(
cv
x1
)
cch
)
)
(
wral
(
λ x2 .
wss
(
cv
x2
)
(
cv
x1
)
⟶
wceq
(
cin
(
co
(
cv
x2
)
(
cv
x0
)
chj
)
(
cv
x1
)
)
(
co
(
cv
x2
)
(
cin
(
cv
x0
)
(
cv
x1
)
)
chj
)
)
(
λ x2 .
cch
)
)
)
)
.
Assume H1:
wceq
cdmd
(
copab
(
λ x0 x1 .
wa
(
wa
(
wcel
(
cv
x0
)
cch
)
(
wcel
(
cv
x1
)
cch
)
)
(
wral
(
λ x2 .
wss
(
cv
x1
)
(
cv
x2
)
⟶
wceq
(
co
(
cin
(
cv
x2
)
(
cv
x0
)
)
(
cv
x1
)
chj
)
(
cin
(
cv
x2
)
(
co
(
cv
x0
)
(
cv
x1
)
chj
)
)
)
(
λ x2 .
cch
)
)
)
)
.
Assume H2:
wceq
cat
(
crab
(
λ x0 .
wbr
c0h
(
cv
x0
)
ccv
)
(
λ x0 .
cch
)
)
.
Assume H3:
∀ x0 x1 :
ι → ο
.
wceq
(
cdp2
x0
x1
)
(
co
x0
(
co
x1
(
cdc
c1
cc0
)
cdiv
)
caddc
)
.
Assume H4:
wceq
cdp
(
cmpt2
(
λ x0 x1 .
cn0
)
(
λ x0 x1 .
cr
)
(
λ x0 x1 .
cdp2
(
cv
x0
)
(
cv
x1
)
)
)
.
Assume H5:
wceq
cxdiv
(
cmpt2
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cdif
cr
(
csn
cc0
)
)
(
λ x0 x1 .
crio
(
λ x2 .
wceq
(
co
(
cv
x1
)
(
cv
x2
)
cxmu
)
(
cv
x0
)
)
(
λ x2 .
cxr
)
)
)
.
Assume H6:
wceq
crefld
(
cfv
cxrs
csca
)
.
Assume H7:
wceq
cxmu
(
cfv
cxrs
cvsca
)
.
Assume H8:
wceq
comnd
(
crab
(
λ x0 .
wsbc
(
λ x1 .
wsbc
(
λ x2 .
wsbc
(
λ x3 .
wa
(
wcel
(
cv
x0
)
ctos
)
(
wral
(
λ x4 .
wral
(
λ x5 .
wral
(
λ x6 .
wbr
(
cv
x4
)
(
cv
x5
)
(
cv
x3
)
⟶
wbr
(
co
(
cv
x4
)
(
cv
x6
)
(
cv
x2
)
)
(
co
(
cv
x5
)
(
cv
x6
)
(
cv
x2
)
)
(
cv
x3
)
)
(
λ x6 .
cv
x1
)
)
(
λ x5 .
cv
x1
)
)
...
)
)
...
)
...
)
...
)
...
)
.
...
■