Nuprl Lemma : order-messages_wf
∀[allhdrs:Name List]. ∀[f:hdr:Name ⟶ Type]. ∀[locs:Id List]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ⟶ comparison(f hdr)].
order-messages(mcmp;locs;allhdrs) ∈ {b:bag(Interface(to locs, with allhdrs))|
single-valued-bag([mi∈b|¬bmsg-header(mi.msg) ∈b hdrs];Interface)} ⟶ (Interface(\000Cto locs, with allhdrs) List)
supposing (∀h∈allhdrs.valueall-type(f h)) ∧ (∀h∈hdrs.∀x,y:f h. (((mcmp h x y) = 0 ∈ ℤ) ⇒ (x = y ∈ (f h))))
Proof
Definitions occuring in Statement :
order-messages: order-messages(mcmp;locs;hdrs),
constrained-msg-interface: Interface(to locs, with hdrs),
msg-interface-message: mi.msg,
msg-interface: Interface,
msg-header: msg-header(m),
Id: Id,
name-deq: NameDeq,
name: Name,
comparison: comparison(T),
l_all: (∀x∈L.P[x]),
deq-member: x ∈b L,
list: T List,
valueall-type: valueall-type(T),
bnot: ¬bb,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
int: ℤ,
universe: Type,
equal: s = t ∈ T,
single-valued-bag: single-valued-bag(b;T),
bag-filter: [x∈b|p[x]],
bag: bag(T)
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
and: P ∧ Q,
order-messages: order-messages(mcmp;locs;hdrs),
subtype_rel: A ⊆r B,
prop: ℙ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
guard: {T},
comparison: comparison(T),
so_lambda: λ2x.t[x],
so_apply: x[s],
constrained-msg-interface: Interface(to locs, with hdrs),
decidable: Dec(P),
or: P ∨ Q,
cand: A c∧ B,
iff: P ⇐⇒ Q,
msg-type: msg-type(msg;f),
rev_implies: P ⇐ Q,
uiff: uiff(P;Q),
single-valued-bag: single-valued-bag(b;T),
rev_uimplies: rev_uimplies(P;Q),
not: ¬A,
false: False,
squash: ↓T,
true: True
Latex:
\mforall{}[allhdrs:Name List]. \mforall{}[f:hdr:Name {}\mrightarrow{} Type]. \mforall{}[locs:Id List]. \mforall{}[hdrs:Name List].
\mforall{}[mcmp:hdr:Name {}\mrightarrow{} comparison(f hdr)].
order-messages(mcmp;locs;allhdrs) \mmember{} \{b:bag(Interface(to locs, with allhdrs))|
single-valued-bag([mi\mmember{}b|\mneg{}\msubb{}msg-header(mi.msg) \mmember{}\msubb{} hdrs];
Interface)\} {}\mrightarrow{} (Interface(to locs, with allhdrs) List)
supposing (\mforall{}h\mmember{}allhdrs.valueall-type(f h)) \mwedge{} (\mforall{}h\mmember{}hdrs.\mforall{}x,y:f h. (((mcmp h x y) = 0) {}\mRightarrow{} (x = y)))
Date html generated:
2016_05_17-AM-09_04_03
Last ObjectModification:
2016_01_17-PM-08_34_46
Theory : messages
Home
Index