---

es-pred?(es;e) ==
  list_accum(x,e'.case x
                  of inl(z) => if es-bcausl(es;z;e') then inl e'  else x fi 
                   | inr(z) => inl e' ;
             inr  ;
             filter(z.loc(z) = loc(e);es-pred-list(es;e)))

---

Definitions :  list_accum: list_accum(x,a.f[x; a];y;l),  decide: case b of inl(x) => s[x] | inr(y) => t[y],  ifthenelse: if b then t else f fi ,  es-bcausl: es-bcausl(es;e;e'),  inl: inl x ,  inr: inr x ,  it: ,  filter: filter(P;l),  lambda: x.A[x],  eq_id: a = b,  es-loc: loc(e),  es-pred-list: es-pred-list(es;e)
FDL editor aliases :  es-pred?

---

es-pred?(es;e)  ==
    list\_accum(x,e'.case  x
                                    of  inl(z)  =>  if  es-bcausl(es;z;e')  then  inl  e'    else  x  fi 
                                      |  inr(z)  =>  inl  e'  ;
                          inr  \mcdot{}  ;
                          filter(\mlambda{}z.loc(z)  =  loc(e);es-pred-list(es;e)))


Date html generated: 2010_08_27-AM-01_06_42
Last ObjectModification: 2009_12_28-PM-01_13_10

Home Index