Search for blocks/addresses/...
Proofgold Proof
pf
Apply df_lvec__df_sra__df_rgmod__df_lidl__df_rsp__df_2idl__df_lpidl__df_lpir__df_nzr__df_rlreg__df_domn__df_idom__df_pid__df_assa__df_asp__df_ascl__df_psr__df_mvr with
wceq
csra
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
cmpt
(
λ x1 .
cpw
(
cfv
(
cv
x0
)
cbs
)
)
(
λ x1 .
co
(
co
(
co
(
cv
x0
)
(
cop
(
cfv
cnx
csca
)
(
co
(
cv
x0
)
(
cv
x1
)
cress
)
)
csts
)
(
cop
(
cfv
cnx
cvsca
)
(
cfv
(
cv
x0
)
cmulr
)
)
csts
)
(
cop
(
cfv
cnx
cip
)
(
cfv
(
cv
x0
)
cmulr
)
)
csts
)
)
)
.
Assume H0:
wceq
clvec
(
crab
(
λ x0 .
wcel
(
cfv
(
cv
x0
)
csca
)
cdr
)
(
λ x0 .
clmod
)
)
.
Assume H1:
wceq
csra
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
cmpt
(
λ x1 .
cpw
(
cfv
(
cv
x0
)
cbs
)
)
(
λ x1 .
co
(
co
(
co
(
cv
x0
)
(
cop
(
cfv
cnx
csca
)
(
co
(
cv
x0
)
(
cv
x1
)
cress
)
)
csts
)
(
cop
(
cfv
cnx
cvsca
)
(
cfv
(
cv
x0
)
cmulr
)
)
csts
)
(
cop
(
cfv
cnx
cip
)
(
cfv
(
cv
x0
)
cmulr
)
)
csts
)
)
)
.
Assume H2:
wceq
crglmod
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
cfv
(
cfv
(
cv
x0
)
cbs
)
(
cfv
(
cv
x0
)
csra
)
)
)
.
Assume H3:
wceq
clidl
(
ccom
clss
crglmod
)
.
Assume H4:
wceq
crsp
(
ccom
clspn
crglmod
)
.
Assume H5:
wceq
c2idl
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
cin
(
cfv
(
cv
x0
)
clidl
)
(
cfv
(
cfv
(
cv
x0
)
coppr
)
clidl
)
)
)
.
Assume H6:
wceq
clpidl
(
cmpt
(
λ x0 .
crg
)
(
λ x0 .
ciun
(
λ x1 .
cfv
(
cv
x0
)
cbs
)
(
λ x1 .
csn
(
cfv
(
csn
(
cv
x1
)
)
(
cfv
(
cv
x0
)
crsp
)
)
)
)
)
.
Assume H7:
wceq
clpir
(
crab
(
λ x0 .
wceq
(
cfv
(
cv
x0
)
clidl
)
(
cfv
(
cv
x0
)
clpidl
)
)
(
λ x0 .
crg
)
)
.
Assume H8:
wceq
cnzr
(
crab
(
λ x0 .
wne
(
cfv
(
cv
x0
)
cur
)
(
cfv
(
cv
x0
)
c0g
)
)
(
λ x0 .
crg
)
)
.
Assume H9:
wceq
crlreg
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
crab
(
λ x1 .
wral
(
λ x2 .
wceq
(
co
(
cv
x1
)
(
cv
x2
)
(
cfv
(
cv
x0
)
cmulr
)
)
(
cfv
(
cv
x0
)
c0g
)
⟶
wceq
(
cv
x2
)
(
cfv
(
cv
x0
)
c0g
)
)
(
λ x2 .
cfv
(
cv
x0
)
cbs
)
)
(
λ x1 .
cfv
(
cv
x0
)
cbs
)
)
)
.
Assume H10:
wceq
cdomn
...
.
...
■