Nuprl Definition : strong-message-constraint-bag

strong-message-constraint-bag{i:l}(es;X;hdrs) ==

be:bag(E)
(bag-no-repeats(E;be)

(

e1,e2:E. (e1

be

e2

be

(

(e1 <loc e2))))

(

bg:bag(E)
(bag-no-repeats(E;bg)

(

e1,e2:E. (e1

bg

e2

bg

(

(e1 <loc e2))))

(

e':E. (e'

bg

(

e:E. (e

be

(e' < e)))))

sub-bag(Id

Message;

e

be.delivered-with-headers(hdrs;es;e);class-output(X;es;bg)))))

Definitions occuring in Statement : delivered-with-headers: delivered-with-headers(hdrs;es;e), Message: Message, class-output: class-output(X;es;bg), es-locl: (e <loc e'), es-causl: (e < e'), es-E: E, Id: Id, all:

x:A. B[x], exists:

x:A. B[x], not:

A, squash:

T, implies: P

Q, and: P

Q, product: x:A

B[x], bag-member: x

bs, sub-bag: sub-bag(T;as;bs), bag-no-repeats: bag-no-repeats(T;bs), bag-combine:

x

bs.f[x], bag: bag(T)
FDL editor aliases : strong-message-constraint-bag

strong-message-constraint-bag\{i:l\}(es;X;hdrs) == \mforall{}be:bag(E) (bag-no-repeats(E;be) {}\mRightarrow{} (\mforall{}e1,e2:E. (e1 \mdownarrow{}\mmember{} be {}\mRightarrow{} e2 \mdownarrow{}\mmember{} be {}\mRightarrow{} (\mneg{}(e1 <loc e2)))) {}\mRightarrow{} (\mdownarrow{}\mexists{}bg:bag(E) (bag-no-repeats(E;bg) \mwedge{} (\mforall{}e1,e2:E. (e1 \mdownarrow{}\mmember{} bg {}\mRightarrow{} e2 \mdownarrow{}\mmember{} bg {}\mRightarrow{} (\mneg{}(e1 <loc e2)))) \mwedge{} (\mforall{}e':E. (e' \mdownarrow{}\mmember{} bg {}\mRightarrow{} (\mexists{}e:E. (e \mdownarrow{}\mmember{} be \mwedge{} (e' < e))))) \mwedge{} sub-bag(Id \mtimes{} Message;\mcup{}e\mmember{}be.delivered-with-headers(hdrs;es;e);class-output(X;es;bg))))) Date html generated: 2012_01_23-PM-12_50_06 Last ObjectModification: 2011_11_15-PM-05_46_26 Home Index