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:
2015_07_21-PM-03_49_18
Last ObjectModification:
2012_02_25-PM-02_49_09
Home
Index