Prior(X) ==
es,e.
case last(e'.0 <z bag-size(X es e')) e of inl(e') => X es e' | inr(x) => {}
Definitions occuring in Statement :
es-local-pred: last(P),
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),
empty-bag: {}
Definitions :
decide: case b of inl(x) => s[x] | inr(y) => t[y],
es-local-pred: last(P),
lambda: x.A[x],
lt_int: i <z j,
natural_number: $n,
bag-size: bag-size(bs),
apply: f a,
empty-bag: {}
FDL editor aliases :
primed-class
Prior(X) == \mlambda{}es,e.case last(\mlambda{}e'.0 <z bag-size(X es e')) e of inl(e') => X es e' | inr(x) => \{\}
Date html generated:
2011_08_16-PM-04_43_49
Last ObjectModification:
2011_01_19-PM-12_48_29
Home
Index