Search for blocks/addresses/...
Proofgold Proof
pf
Apply df_lnop__df_bdop__df_unop__df_hmop__df_nmfn__df_nlfn__df_cnfn__df_lnfn__df_adjh__df_bra__df_kb__df_leop__df_eigvec__df_eigval__df_spec__df_st__df_hst__df_cv with
wceq
chst
(
crab
(
λ x0 .
wa
(
wceq
(
cfv
(
cfv
chil
(
cv
x0
)
)
cno
)
c1
)
(
wral
(
λ x1 .
wral
(
λ x2 .
wss
(
cv
x1
)
(
cfv
(
cv
x2
)
cort
)
⟶
wa
(
wceq
(
co
(
cfv
(
cv
x1
)
(
cv
x0
)
)
(
cfv
(
cv
x2
)
(
cv
x0
)
)
csp
)
cc0
)
(
wceq
(
cfv
(
co
(
cv
x1
)
(
cv
x2
)
chj
)
(
cv
x0
)
)
(
co
(
cfv
(
cv
x1
)
(
cv
x0
)
)
(
cfv
(
cv
x2
)
(
cv
x0
)
)
cva
)
)
)
(
λ x2 .
cch
)
)
(
λ x1 .
cch
)
)
)
(
λ x0 .
co
chil
cch
cmap
)
)
.
Assume H0:
wceq
clo
(
crab
(
λ x0 .
wral
(
λ x1 .
wral
(
λ x2 .
wral
(
λ x3 .
wceq
(
cfv
(
co
(
co
(
cv
x1
)
(
cv
x2
)
csm
)
(
cv
x3
)
cva
)
(
cv
x0
)
)
(
co
(
co
(
cv
x1
)
(
cfv
(
cv
x2
)
(
cv
x0
)
)
csm
)
(
cfv
(
cv
x3
)
(
cv
x0
)
)
cva
)
)
(
λ x3 .
chil
)
)
(
λ x2 .
chil
)
)
(
λ x1 .
cc
)
)
(
λ x0 .
co
chil
chil
cmap
)
)
.
Assume H1:
wceq
cbo
(
crab
(
λ x0 .
wbr
(
cfv
(
cv
x0
)
cnop
)
cpnf
clt
)
(
λ x0 .
clo
)
)
.
Assume H2:
wceq
cuo
(
cab
(
λ x0 .
wa
(
wfo
chil
chil
(
cv
x0
)
)
(
wral
(
λ x1 .
wral
(
λ x2 .
wceq
(
co
(
cfv
(
cv
x1
)
(
cv
x0
)
)
(
cfv
(
cv
x2
)
(
cv
x0
)
)
csp
)
(
co
(
cv
x1
)
(
cv
x2
)
csp
)
)
(
λ x2 .
chil
)
)
(
λ x1 .
chil
)
)
)
)
.
Assume H3:
wceq
cho
(
crab
(
λ x0 .
wral
(
λ x1 .
wral
(
λ x2 .
wceq
(
co
(
cv
x1
)
(
cfv
(
cv
x2
)
(
cv
x0
)
)
csp
)
(
co
(
cfv
(
cv
x1
)
(
cv
x0
)
)
(
cv
x2
)
csp
)
)
(
λ x2 .
chil
)
)
(
λ x1 .
chil
)
)
(
λ x0 .
co
chil
chil
cmap
)
)
.
Assume H4:
wceq
cnmf
(
cmpt
(
λ x0 .
co
cc
chil
cmap
)
(
λ x0 .
csup
(
cab
(
λ x1 .
wrex
(
λ x2 .
wa
(
wbr
(
cfv
(
cv
x2
)
cno
)
c1
cle
)
(
wceq
(
cv
x1
)
(
cfv
(
cfv
(
cv
x2
)
(
cv
x0
)
)
cabs
)
)
)
(
λ x2 .
chil
)
)
)
cxr
clt
)
)
.
Assume H5:
wceq
cnl
(
cmpt
(
λ x0 .
co
...
...
...
)
...
)
.
...
■