---

sub-es-pred(es;dom;e) ==
  Y 
  (sub-es-pred,e.
    if first(e) then inr  
    if dom pred(e) then inl pred(e) 
    else sub-es-pred pred(e)
    fi ) 
  e

---

Definitions :  ycomb: Y,  lambda: x.A[x],  es-first: first(e),  inr: inr x ,  it: ,  ifthenelse: if b then t else f fi ,  inl: inl x ,  apply: f a,  es-pred: pred(e)
FDL editor aliases :  sub-es-pred

---

sub-es-pred(es;dom;e)  ==
    Y 
    (\mlambda{}sub-es-pred,e.
        if  first(e)  then  inr  \mcdot{} 
        if  dom  pred(e)  then  inl  pred(e) 
        else  sub-es-pred  pred(e)
        fi  ) 
    e


Date html generated: 2010_08_27-AM-09_41_21
Last ObjectModification: 2009_12_17-PM-10_44_06

Home Index