Nuprl Definition : strong-message-constraint-no-rep-large

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

e:E
(

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

(

e1,e2:E. (e1

bg

e2

bg

(

(e1 <loc e2))))

(

e':E. (e'

bg

(e' < e)))

sub-bag(Id

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

(

e':E. ((e' < e)

(

e'':E. (e''

bg

e'

loc e'' ))))))

Definitions occuring in Statement : delivered-with-headers: delivered-with-headers(hdrs;es;e), Message: Message, class-output: class-output(X;es;bg), es-le: e

loc e' , 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: bag(T)
FDL editor aliases : strong-message-constraint-no-rep-large

strong-message-constraint-no-rep-large\{i:l\}(es;X;hdrs) == \mforall{}e:E (\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{} (e' < e))) \mwedge{} sub-bag(Id \mtimes{} Message;delivered-with-headers(hdrs;es;e);class-output(X;es;bg)) \mwedge{} (\mforall{}e':E. ((e' < e) {}\mRightarrow{} (\mexists{}e'':E. (e'' \mdownarrow{}\mmember{} bg \mwedge{} e' \mleq{}loc e'' )))))) Date html generated: 2012_01_23-PM-12_48_33 Last ObjectModification: 2011_11_29-PM-01_22_28 Home Index