Search for blocks/addresses/...
Proofgold Proof
pf
Apply df_polarityN__df_psubclN__df_lhyp__df_laut__df_watsN__df_pautN__df_ldil__df_ltrn__df_dilN__df_trnN__df_trl__df_tgrp__df_tendo__df_edring_rN__df_edring__df_dveca__df_disoa__df_dvech with
wceq
ctrnN
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
cmpt
(
λ x1 .
cfv
(
cv
x0
)
catm
)
(
λ x1 .
crab
(
λ x2 .
wral
(
λ x3 .
wral
(
λ x4 .
wceq
(
cin
(
co
(
cv
x3
)
(
cfv
(
cv
x3
)
(
cv
x2
)
)
(
cfv
(
cv
x0
)
cpadd
)
)
(
cfv
(
csn
(
cv
x1
)
)
(
cfv
(
cv
x0
)
cpolN
)
)
)
(
cin
(
co
(
cv
x4
)
(
cfv
(
cv
x4
)
(
cv
x2
)
)
(
cfv
(
cv
x0
)
cpadd
)
)
(
cfv
(
csn
(
cv
x1
)
)
(
cfv
(
cv
x0
)
cpolN
)
)
)
)
(
λ x4 .
cfv
(
cv
x1
)
(
cfv
(
cv
x0
)
cwpointsN
)
)
)
(
λ x3 .
cfv
(
cv
x1
)
(
cfv
(
cv
x0
)
cwpointsN
)
)
)
(
λ x2 .
cfv
(
cv
x1
)
(
cfv
(
cv
x0
)
cdilN
)
)
)
)
)
.
Assume H0:
wceq
cpolN
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
cmpt
(
λ x1 .
cpw
(
cfv
(
cv
x0
)
catm
)
)
(
λ x1 .
cin
(
cfv
(
cv
x0
)
catm
)
(
ciin
(
λ x2 .
cv
x1
)
(
λ x2 .
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x0
)
coc
)
)
(
cfv
(
cv
x0
)
cpmap
)
)
)
)
)
)
.
Assume H1:
wceq
cpscN
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
cab
(
λ x1 .
wa
(
wss
(
cv
x1
)
(
cfv
(
cv
x0
)
catm
)
)
(
wceq
(
cfv
(
cfv
(
cv
x1
)
(
cfv
(
cv
x0
)
cpolN
)
)
(
cfv
(
cv
x0
)
cpolN
)
)
(
cv
x1
)
)
)
)
)
.
Assume H2:
wceq
clh
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
crab
(
λ x1 .
wbr
(
cv
x1
)
(
cfv
(
cv
x0
)
cp1
)
(
cfv
(
cv
x0
)
ccvr
)
)
(
λ x1 .
cfv
(
cv
x0
)
cbs
)
)
)
.
Assume H3:
wceq
claut
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
cab
(
λ x1 .
wa
(
wf1o
(
cfv
(
cv
x0
)
cbs
)
(
cfv
(
cv
x0
)
cbs
)
(
cv
x1
)
)
(
wral
(
λ x2 .
wral
(
λ x3 .
wb
(
wbr
(
cv
x2
)
(
cv
x3
)
(
cfv
(
cv
x0
)
cple
)
)
(
wbr
(
cfv
(
cv
x2
)
(
cv
x1
)
)
(
cfv
(
cv
x3
)
(
cv
x1
)
)
(
cfv
(
cv
x0
)
cple
)
)
)
(
λ x3 .
cfv
(
cv
x0
)
cbs
)
)
(
λ x2 .
cfv
(
cv
x0
)
cbs
)
)
)
)
)
.
Assume H4:
wceq
cwpointsN
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
cmpt
(
λ x1 .
cfv
(
cv
x0
)
catm
)
...
)
)
.
...
■