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