Search for blocks/addresses/...
Proofgold Proof
pf
Apply df_strset__df_bj_diag__df_bj_inftyexpi__df_bj_ccinfty__df_bj_ccbar__df_bj_pinfty__df_bj_minfty__df_bj_rrbar__df_bj_infty__df_bj_cchat__df_bj_rrhat__df_bj_addc__df_bj_oppc__df_bj_prcpal__df_bj_arg__df_bj_mulc__df_bj_invc__df_bj_finsum with
wceq
cprcpal
(
cmpt
(
λ x0 .
cr
)
(
λ x0 .
co
(
co
(
cv
x0
)
(
co
c2
cpi
cmul
)
cmo
)
(
cif
(
wbr
(
co
(
cv
x0
)
(
co
c2
cpi
cmul
)
cmo
)
cpi
cle
)
cc0
(
co
c2
cpi
cmul
)
)
cmin
)
)
.
Assume H0:
∀ x0 x1 x2 :
ι → ο
.
wceq
(
cstrset
x0
x1
x2
)
(
cun
(
cres
x2
(
cdif
cvv
(
csn
(
cfv
cnx
x0
)
)
)
)
(
csn
(
cop
(
cfv
cnx
x0
)
x1
)
)
)
.
Assume H1:
wceq
cdiag2
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
cin
cid
(
cxp
(
cv
x0
)
(
cv
x0
)
)
)
)
.
Assume H2:
wceq
cinftyexpi
(
cmpt
(
λ x0 .
co
(
cneg
cpi
)
cpi
cioc
)
(
λ x0 .
cop
(
cv
x0
)
cc
)
)
.
Assume H3:
wceq
cccinfty
(
crn
cinftyexpi
)
.
Assume H4:
wceq
cccbar
(
cun
cc
cccinfty
)
.
Assume H5:
wceq
cpinfty
(
cfv
cc0
cinftyexpi
)
.
Assume H6:
wceq
cminfty
(
cfv
cpi
cinftyexpi
)
.
Assume H7:
wceq
crrbar
(
cun
cr
(
cpr
cminfty
cpinfty
)
)
.
Assume H8:
wceq
cinfty
(
cpw
(
cuni
cc
)
)
.
Assume H9:
wceq
ccchat
(
cun
cc
(
csn
cinfty
)
)
.
Assume H10:
wceq
crrhat
(
cun
cr
(
csn
cinfty
)
)
.
Assume H11:
wceq
caddcc
(
cmpt
(
λ x0 .
cun
(
cun
(
cxp
cc
cccbar
)
(
cxp
cccbar
cc
)
)
(
cun
(
cxp
ccchat
ccchat
)
(
cfv
cccinfty
cdiag2
)
)
)
(
λ x0 .
cif
(
wo
(
wceq
(
cfv
(
cv
x0
)
c1st
)
cinfty
)
(
wceq
(
cfv
(
cv
x0
)
c2nd
)
cinfty
)
)
cinfty
(
cif
(
wcel
(
cfv
(
cv
x0
)
c1st
)
cc
)
(
cif
(
wcel
(
cfv
(
cv
x0
)
c2nd
)
cc
)
(
co
(
cfv
(
cv
x0
)
c1st
)
(
cfv
(
cv
x0
)
c2nd
)
caddc
)
(
cfv
(
cv
x0
)
c2nd
)
)
(
cfv
(
cv
x0
)
c1st
)
)
)
)
.
Assume H12:
wceq
coppcc
(
cmpt
(
λ x0 .
cun
cccbar
ccchat
)
(
λ x0 .
cif
(
wceq
(
cv
x0
)
cinfty
)
cinfty
(
cif
(
wcel
(
cv
x0
)
cc
)
(
cneg
(
cv
x0
)
)
(
cfv
(
cif
(
wbr
cc0
(
cfv
(
cv
x0
)
c1st
)
clt
)
(
co
(
cfv
(
cv
x0
)
c1st
)
cpi
cmin
)
(
co
(
cfv
(
cv
x0
)
c1st
)
cpi
caddc
)
)
cinftyexpi
)
)
)
)
.
Assume H13:
wceq
cprcpal
(
cmpt
(
λ x0 .
cr
)
(
λ x0 .
co
...
...
...
)
)
.
...
■