Nuprl Definition : es-propagation-rule-iff

A

f

B@g ==

p:E(A)

(E(B) List)
((

e1,e2:E(A). ((

(e1 = e2))

l_disjoint(E(B);p e1;p e2)))

(

e:E(A)
(

e'

p e.(e < e')

(B(e') = (f loc(e) A(e)))

(loc(e')

g A(e))))

(

e:E(A). (

x

g A(e).(

e'

p e. loc(e') = x)))

(

e':E(B).

e:E(A). (e'

p e)))

Definitions : es-E-interface: E(X), apply: f a, l_member: (x

l), exists:

x:A. B[x], all:

x:A. B[x], es-loc: loc(e), Id: Id, equal: s = t, l_exists: (

x

L. P[x]), eclass-val: X(e), l_all: (

x

L.P[x]), and: P

Q, es-causl: (e < e'), l_disjoint: l_disjoint(T;l1;l2), es-E: E, not:

A, implies: P

Q, list: type List, function: x:A

B[x]
FDL editor aliases : es-propagation-rule-iff es-propagation-rule-iff

A \mLeftarrow{}{}f{}\mRightarrow{} B@g == \mexists{}p:E(A) {}\mrightarrow{} (E(B) List) ((\mforall{}e1,e2:E(A). ((\mneg{}(e1 = e2)) {}\mRightarrow{} l\_disjoint(E(B);p e1;p e2))) \mwedge{} (\mforall{}e:E(A). (\mforall{}e'\mmember{}p e.(e < e') \mwedge{} (B(e') = (f loc(e) A(e))) \mwedge{} (loc(e') \mmember{} g A(e)))) \mwedge{} (\mforall{}e:E(A). (\mforall{}x\mmember{}g A(e).(\mexists{}e'\mmember{}p e. loc(e') = x))) \mwedge{} (\mforall{}e':E(B). \mexists{}e:E(A). (e' \mmember{} p e))) Date html generated: 2010_08_30-AM-12_51_46 Last ObjectModification: 2010_08_23-PM-12_31_10 Home Index