Nuprl Definition : es-prior-class-when

(X'?d) when Y ==  λes,e. if e ∈b Y then {<Y(e), if e ∈b (X)' then (X)'(e) else d fi >} else {} fi 


Definitions occuring in Statement :  es-prior-val: (X)',  eclass-val: X(e),  in-eclass: e ∈b X,  ifthenelse: if b then t else f fi ,  lambda: λx.A[x],  pair: <a, b>,  single-bag: {x},  empty-bag: {}
FDL editor aliases :  es-prior-class-when
Latex:
(X'?d)  when  Y  ==    \mlambda{}es,e.  if  e  \mmember{}\msubb{}  Y  then  \{<Y(e),  if  e  \mmember{}\msubb{}  (X)'  then  (X)'(e)  else  d  fi  >\}  else  \{\}  fi 


Date html generated: 2016_05_17-AM-07_18_12
Last ObjectModification: 2012_02_25-PM-02_48_21

Theory : event-ordering


Home Index