Search for blocks/addresses/...
Proofgold Proof
pf
Apply df_fallfac__df_bpoly__df_ef__df_e__df_sin__df_cos__df_tan__df_pi__df_dvds__df_bits__df_sad__df_smu__df_gcd__df_lcm__df_lcmf__df_prm__df_numer__df_denom with
wceq
ctan
(
cmpt
(
λ x0 .
cima
(
ccnv
ccos
)
(
cdif
cc
(
csn
cc0
)
)
)
(
λ x0 .
co
(
cfv
(
cv
x0
)
csin
)
(
cfv
(
cv
x0
)
ccos
)
cdiv
)
)
.
Assume H0:
wceq
cfallfac
(
cmpt2
(
λ x0 x1 .
cc
)
(
λ x0 x1 .
cn0
)
(
λ x0 x1 .
cprod
(
λ x2 .
co
cc0
(
co
(
cv
x1
)
c1
cmin
)
cfz
)
(
λ x2 .
co
(
cv
x0
)
(
cv
x2
)
cmin
)
)
)
.
Assume H1:
wceq
cbp
(
cmpt2
(
λ x0 x1 .
cn0
)
(
λ x0 x1 .
cc
)
(
λ x0 x1 .
cfv
(
cv
x0
)
(
cwrecs
cn0
clt
(
cmpt
(
λ x2 .
cvv
)
(
λ x2 .
csb
(
cfv
(
cdm
(
cv
x2
)
)
chash
)
(
λ x3 .
co
(
co
(
cv
x1
)
(
cv
x3
)
cexp
)
(
csu
(
cdm
(
cv
x2
)
)
(
λ x4 .
co
(
co
(
cv
x3
)
(
cv
x4
)
cbc
)
(
co
(
cfv
(
cv
x4
)
(
cv
x2
)
)
(
co
(
co
(
cv
x3
)
(
cv
x4
)
cmin
)
c1
caddc
)
cdiv
)
cmul
)
)
cmin
)
)
)
)
)
)
.
Assume H2:
wceq
ce
(
cmpt
(
λ x0 .
cc
)
(
λ x0 .
csu
cn0
(
λ x1 .
co
(
co
(
cv
x0
)
(
cv
x1
)
cexp
)
(
cfv
(
cv
x1
)
cfa
)
cdiv
)
)
)
.
Assume H3:
wceq
ceu
(
cfv
c1
ce
)
.
Assume H4:
wceq
csin
(
cmpt
(
λ x0 .
cc
)
(
λ x0 .
co
(
co
(
cfv
(
co
ci
(
cv
x0
)
cmul
)
ce
)
(
cfv
(
co
(
cneg
ci
)
(
cv
x0
)
cmul
)
ce
)
cmin
)
(
co
c2
ci
cmul
)
cdiv
)
)
.
Assume H5:
wceq
ccos
(
cmpt
(
λ x0 .
cc
)
(
λ x0 .
co
(
co
(
cfv
(
co
ci
(
cv
x0
)
cmul
)
ce
)
(
cfv
(
co
(
cneg
ci
)
(
cv
x0
)
cmul
)
ce
)
caddc
)
c2
cdiv
)
)
.
Assume H6:
wceq
ctan
(
cmpt
(
λ x0 .
cima
(
ccnv
ccos
)
(
cdif
cc
(
csn
cc0
)
)
)
(
λ x0 .
co
(
cfv
(
cv
x0
)
csin
)
(
cfv
(
cv
x0
)
ccos
)
cdiv
)
)
.
Assume H7:
wceq
cpi
(
cinf
(
cin
crp
(
cima
(
ccnv
csin
)
(
csn
cc0
)
)
)
cr
clt
)
.
Assume H8:
wceq
cdvds
(
copab
(
λ x0 x1 .
wa
(
wa
(
wcel
(
cv
x0
)
cz
)
(
wcel
(
cv
x1
)
cz
)
)
(
wrex
(
λ x2 .
wceq
(
co
(
cv
x2
)
(
cv
x0
)
cmul
)
...
)
...
)
)
)
.
...
■