Nuprl Definition : es-class-causal-mrel

e

X(x)

c

Y(y)
            @locs such that
            R[e; x; y] ==
  (

e:E(Y). ((loc(e)

locs)

(

e':E(X). (e' c

e

R[e'; X(e'); Y(e)]))))

(

e':E(X). (

i

locs.

e:E(Y). ((loc(e) = i)

e' c

e

R[e'; X(e'); Y(e)])))

Definitions : l_member: (x

l), all:

x:A. B[x], l_all: (

x

L.P[x]), exists:

x:A. B[x], es-E-interface: E(X), equal: s = t, Id: Id, es-loc: loc(e), and: P

Q, es-causle: e c

e', eclass-val: X(e)
FDL editor aliases : es-class-causal-mrel

e\mmember{}X(x) \mLeftarrow{}c\mRightarrow{} Y(y) @locs such that R[e; x; y] == (\mforall{}e:E(Y). ((loc(e) \mmember{} locs) \mwedge{} (\mexists{}e':E(X). (e' c\mleq{} e \mwedge{} R[e'; X(e'); Y(e)])))) \mwedge{} (\mforall{}e':E(X). (\mforall{}i\mmember{}locs.\mexists{}e:E(Y). ((loc(e) = i) \mwedge{} e' c\mleq{} e \mwedge{} R[e'; X(e'); Y(e)]))) Date html generated: 2010_08_27-PM-03_31_23 Last ObjectModification: 2010_04_15-PM-11_21_48 Home Index