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 then else fi  it: apply: a fix: fix(F) lambda: λx.A[x] inr: inr  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