Prior(X)?b ==
  es,e.
   case last(e'.0 <z bag-size(X es e')) e
   of inl(e') =>
    X es e'
    | inr(x) =>
    b loc(e)



Definitions occuring in Statement :  es-local-pred: last(P),  es-loc: loc(e),  lt_int: i <z j,  apply: f a,  lambda: x.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  natural_number: $n,  bag-size: bag-size(bs)
FDL editor aliases :  primed-class-opt

Prior(X)?b  ==
    \mlambda{}es,e.case  last(\mlambda{}e'.0  <z  bag-size(X  es  e'))  e  of  inl(e')  =>  X  es  e'  |  inr(x)  =>  b  loc(e)


Date html generated: 2011_08_16-PM-04_44_05
Last ObjectModification: 2011_07_22-PM-11_30_08

Home Index