Nuprl Definition : es-prior-match

es-prior-match(R; X; Y) ==  λes,e. if (e ∈b (X)' ∧b e ∈b Y) ∧b (R (X)'(e) Y(e)) then {<(X)'(e), Y(e)>} else {} fi 


Definitions occuring in Statement :  es-prior-val: (X)',  eclass-val: X(e),  in-eclass: e ∈b X,  band: p ∧b q,  ifthenelse: if b then t else f fi ,  apply: f a,  lambda: λx.A[x],  pair: <a, b>,  single-bag: {x},  empty-bag: {}
Latex:
es-prior-match(R;  X;  Y)  ==
    \mlambda{}es,e.  if  (e  \mmember{}\msubb{}  (X)'  \mwedge{}\msubb{}  e  \mmember{}\msubb{}  Y)  \mwedge{}\msubb{}  (R  (X)'(e)  Y(e))  then  \{<(X)'(e),  Y(e)>\}  else  \{\}  fi 


Date html generated: 2016_05_17-AM-07_19_42
Last ObjectModification: 2012_02_25-PM-02_49_09

Theory : event-ordering


Home Index