Nuprl Definition : negate-poly-constraint
negate-poly-constraint(X) ==
  let eqs,ineqs = X 
  in accumulate (with value pcs and list item e):
      [<[], [minus-poly(add-ipoly(e;const-poly(1)))]> [<[], [add-ipoly(e;const-poly(-1))]> / pcs]]
     over list:
       eqs
     with starting value:
      map(λineq.<[], [minus-poly(add-ipoly(ineq;const-poly(1)))]>ineqs))
Definitions occuring in Statement : 
const-poly: const-poly(n)
, 
minus-poly: minus-poly(p)
, 
add-ipoly: add-ipoly(p;q)
, 
map: map(f;as)
, 
list_accum: list_accum, 
cons: [a / b]
, 
nil: []
, 
lambda: λx.A[x]
, 
spread: spread def, 
pair: <a, b>
, 
minus: -n
, 
natural_number: $n
Definitions occuring in definition : 
spread: spread def, 
list_accum: list_accum, 
minus: -n
, 
map: map(f;as)
, 
lambda: λx.A[x]
, 
pair: <a, b>
, 
cons: [a / b]
, 
minus-poly: minus-poly(p)
, 
add-ipoly: add-ipoly(p;q)
, 
const-poly: const-poly(n)
, 
natural_number: $n
, 
nil: []
FDL editor aliases : 
negate-poly-constraint
Latex:
negate-poly-constraint(X)  ==
    let  eqs,ineqs  =  X 
    in  accumulate  (with  value  pcs  and  list  item  e):
            [<[],  [minus-poly(add-ipoly(e;const-poly(1)))]>  [<[],  [add-ipoly(e;const-poly(-1))]>  /  pcs]]
          over  list:
              eqs
          with  starting  value:
            map(\mlambda{}ineq.<[],  [minus-poly(add-ipoly(ineq;const-poly(1)))]>ineqs))
Date html generated:
2016_05_14-AM-07_08_46
Last ObjectModification:
2015_09_22-PM-05_52_58
Theory : omega
Home
Index