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 
   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 of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x
Definitions occuring in definition :  gcd-reduce-eq-constraints: gcd-reduce-eq-constraints(sat;LL) decide: case 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 
FDL editor aliases :  omega_start

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