Nuprl Definition : prior-as-rec-bind-class-in

prior-as-rec-bind-class-in(X;i) ==
  case i
   of inl(b) =>
   Null
   | inr(x) =>

   case x of inl(b) => (Skip(send-class({b})) until Skip(X)) (+) Null | inr(u) => Null (+) Lift(X) (+) Null

Definitions occuring in Statement : send-class: send-class(b), lift-class: Lift(X), null-class: Null, disjoint-union-comb: X (+) Y, skip-first-class: Skip(X), until-class: (X until Y), decide: case b of inl(x) => s[x] | inr(y) => t[y], single-bag: {x}
FDL editor aliases : prior-as-rec-bind-class-in

Latex:
prior-as-rec-bind-class-in(X;i) == case i of inl(b) => Null | inr(x) => case x of inl(b) => (Skip(send-class(\{b\})) until Skip(X)) (+) Null | inr(u) => Null (+) Lift(X) (+) Null Date html generated: 2015_07_21-PM-03_13_42 Last ObjectModification: 2012_04_15-PM-04_40_32 Home Index