Nuprl Definition : satisfies-poly-constraints
satisfies-poly-constraints(f;X) ==
let eqs,ineqs = X
in (∀p∈eqs.int_term_value(f;ipolynomial-term(p)) = 0 ∈ ℤ) ∧ (∀p∈ineqs.0 ≤ int_term_value(f;ipolynomial-term(p)))
Definitions occuring in Statement :
ipolynomial-term: ipolynomial-term(p)
,
int_term_value: int_term_value(f;t)
,
l_all: (∀x∈L.P[x])
,
le: A ≤ B
,
and: P ∧ Q
,
spread: spread def,
natural_number: $n
,
int: ℤ
,
equal: s = t ∈ T
Definitions occuring in definition :
spread: spread def,
and: P ∧ Q
,
equal: s = t ∈ T
,
int: ℤ
,
l_all: (∀x∈L.P[x])
,
le: A ≤ B
,
natural_number: $n
,
int_term_value: int_term_value(f;t)
,
ipolynomial-term: ipolynomial-term(p)
FDL editor aliases :
satisfies-poly-constraints
Latex:
satisfies-poly-constraints(f;X) ==
let eqs,ineqs = X
in (\mforall{}p\mmember{}eqs.int\_term\_value(f;ipolynomial-term(p)) = 0)
\mwedge{} (\mforall{}p\mmember{}ineqs.0 \mleq{} int\_term\_value(f;ipolynomial-term(p)))
Date html generated:
2016_05_14-AM-07_07_53
Last ObjectModification:
2015_09_22-PM-05_52_51
Theory : omega
Home
Index