Nuprl Definition : int-problem-dimension

If the integer problem is known to be unsatisfiable (the inr case) then
it has dimension 0. Otherwise, all the constraints are lists of the
same length, [c,a1,a2,...] representing the linear form
c+ a1*v1 + a2*v2 + ...., so the dimension is the length of (any of) these
lists decremented by 1.⋅

dim(p) ==
  case p
   of inl(q) =>
   let eqs,ineqs = q
   in if eqs = Ax then if ineqs = Ax then 0 otherwise ||hd(ineqs)|| - 1 otherwise ||hd(eqs)|| - 1
   | inr(_) =>
   0

Definitions occuring in Statement : hd: hd(l), length: ||as||, isaxiom: if z = Ax then a otherwise b, spread: spread def, decide: case b of inl(x) => s[x] | inr(y) => t[y], subtract: n - m, natural_number: $n
Definitions occuring in definition : decide: case b of inl(x) => s[x] | inr(y) => t[y], spread: spread def, isaxiom: if z = Ax then a otherwise b, subtract: n - m, length: ||as||, hd: hd(l), natural_number: $n
FDL editor aliases : int-problem-dimension

Latex:
dim(p) == case p of inl(q) => let eqs,ineqs = q in if eqs = Ax then if ineqs = Ax then 0 otherwise ||hd(ineqs)|| - 1 otherwise ||hd(eqs)|| - 1 | inr($_{}$) => 0 Date html generated: 2016_07_08-PM-04_48_28 Last ObjectModification: 2015_12_14-PM-06_57_23 Theory : omega Home Index