Nuprl Definition : omega

Nuprl Definition : omega_start

To create starting state of omega, we "gcd-reduce" the constraints.
This can sometimes detect that the equality constraints are unsatisfiable.⋅

omega_start(eqs;ineqs) ==
  case gcd-reduce-eq-constraints([];eqs)
   of inl(eqs') =>
   case gcd-reduce-ineq-constraints([];ineqs) of inl(ineqs') => inl <eqs', ineqs'> | inr(x) => inr x
   | inr(x) =>
   inr x

Definitions occuring in Statement : gcd-reduce-ineq-constraints: gcd-reduce-ineq-constraints(sat;LL), gcd-reduce-eq-constraints: gcd-reduce-eq-constraints(sat;LL), nil: [], pair: <a, b>, decide: case b of inl(x) => s[x] | inr(y) => t[y], inr: inr x , inl: inl x
Definitions occuring in definition : gcd-reduce-eq-constraints: gcd-reduce-eq-constraints(sat;LL), decide: case b of inl(x) => s[x] | inr(y) => t[y], gcd-reduce-ineq-constraints: gcd-reduce-ineq-constraints(sat;LL), nil: [], inl: inl x, pair: <a, b>, inr: inr x
FDL editor aliases : omega_start

Latex:
omega\_start(eqs;ineqs) == case gcd-reduce-eq-constraints([];eqs) of inl(eqs') => case gcd-reduce-ineq-constraints([];ineqs) of inl(ineqs') => inl <eqs', ineqs'> | inr(x) => inr x\000C | inr(x) => inr x Date html generated: 2016_07_08-PM-04_48_42 Last ObjectModification: 2015_12_14-PM-06_39_14 Theory : omega Home Index