Nuprl Definition : sub-es-pred

sub-es-pred(es;dom;e) ==
  fix((λ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 occuring in Statement :  es-first: first(e),  es-pred: pred(e),  ifthenelse: if b then t else f fi ,  it: ⋅,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  inr: inr x ,  inl: inl x
FDL editor aliases :  sub-es-pred sub-es-pred
Latex:
sub-es-pred(es;dom;e)  ==
    fix((\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: 2016_05_16-AM-10_25_20
Last ObjectModification: 2013_03_25-PM-01_43_44

Theory : new!event-ordering


Home Index