Search for blocks/addresses/...
Proofgold Proof
pf
Apply df_bigo__df_blen__df_dig__df_setrecs__df_pg__df_gte__df_gt__df_sinh__df_cosh__df_tanh__df_sec__df_csc__df_cot__df_logbALT__df_reflexive__df_irreflexive__df_alsi__df_alsc with
wceq
cbigo
(
cmpt
(
λ x0 .
co
cr
cr
cpm
)
(
λ x0 .
crab
(
λ x1 .
wrex
(
λ x2 .
wrex
(
λ x3 .
wral
(
λ x4 .
wbr
(
cfv
(
cv
x4
)
(
cv
x1
)
)
(
co
(
cv
x3
)
(
cfv
(
cv
x4
)
(
cv
x0
)
)
cmul
)
cle
)
(
λ x4 .
cin
(
cdm
(
cv
x1
)
)
(
co
(
cv
x2
)
cpnf
cico
)
)
)
(
λ x3 .
cr
)
)
(
λ x2 .
cr
)
)
(
λ x1 .
co
cr
cr
cpm
)
)
)
.
Assume H0:
wceq
cbigo
(
cmpt
(
λ x0 .
co
cr
cr
cpm
)
(
λ x0 .
crab
(
λ x1 .
wrex
(
λ x2 .
wrex
(
λ x3 .
wral
(
λ x4 .
wbr
(
cfv
(
cv
x4
)
(
cv
x1
)
)
(
co
(
cv
x3
)
(
cfv
(
cv
x4
)
(
cv
x0
)
)
cmul
)
cle
)
(
λ x4 .
cin
(
cdm
(
cv
x1
)
)
(
co
(
cv
x2
)
cpnf
cico
)
)
)
(
λ x3 .
cr
)
)
(
λ x2 .
cr
)
)
(
λ x1 .
co
cr
cr
cpm
)
)
)
.
Assume H1:
wceq
cblen
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
cif
(
wceq
(
cv
x0
)
cc0
)
c1
(
co
(
cfv
(
co
c2
(
cfv
(
cv
x0
)
cabs
)
clogb
)
cfl
)
c1
caddc
)
)
)
.
Assume H2:
wceq
cdig
(
cmpt
(
λ x0 .
cn
)
(
λ x0 .
cmpt2
(
λ x1 x2 .
cz
)
(
λ x1 x2 .
co
cc0
cpnf
cico
)
(
λ x1 x2 .
co
(
cfv
(
co
(
co
(
cv
x0
)
(
cneg
(
cv
x1
)
)
cexp
)
(
cv
x2
)
cmul
)
cfl
)
(
cv
x0
)
cmo
)
)
)
.
Assume H3:
∀ x0 :
ι → ο
.
wceq
(
csetrecs
x0
)
(
cuni
(
cab
(
λ x1 .
∀ x2 .
(
∀ x3 .
wss
(
cv
x3
)
(
cv
x1
)
⟶
wss
(
cv
x3
)
(
cv
x2
)
⟶
wss
(
cfv
(
cv
x3
)
x0
)
(
cv
x2
)
)
⟶
wss
(
cv
x1
)
(
cv
x2
)
)
)
)
.
Assume H4:
wceq
cpg
(
csetrecs
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
cxp
(
cpw
(
cv
x0
)
)
(
cpw
(
cv
x0
)
)
)
)
)
.
Assume H5:
wceq
cge_real
(
ccnv
cle
)
.
Assume H6:
wceq
cgt
(
ccnv
clt
)
.
Assume H7:
wceq
csinh
(
cmpt
(
λ x0 .
cc
)
(
λ x0 .
co
(
cfv
(
co
ci
(
cv
x0
)
cmul
)
csin
)
ci
cdiv
)
)
.
Assume H8:
wceq
ccosh
(
cmpt
(
λ x0 .
cc
)
(
λ x0 .
cfv
(
co
ci
(
cv
x0
)
cmul
)
ccos
)
)
.
Assume H9:
wceq
ctanh
(
cmpt
...
...
)
.
...
■