Nuprl Lemma : deliver-msg_functionality
∀[M:Type ⟶ Type]
∀t:ℕ. ∀x:Id. ∀m:pMsg(P.M[P]). ∀G1,G2:LabeledDAG(pInTransit(P.M[P])). ∀Cs1,Cs2:component(P.M[P]) List.
((∀k:ℕ||Cs1||. let x,P = Cs1[k] in let z,Q = Cs2[k] in (x = z ∈ Id) ∧ P≡Q)
⇒ (system-equiv(P.M[P];deliver-msg(t;m;x;Cs1;G1);deliver-msg(t;m;x;Cs2;G2))
∧ (deliver-msg(t;m;x;Cs1;G1)
= deliver-msg(t;m;x;Cs2;G2)
∈ (Top × LabeledDAG(pInTransit(P.M[P])))))) supposing
((||Cs1|| = ||Cs2|| ∈ ℤ) and
(G1 = G2 ∈ LabeledDAG(pInTransit(P.M[P]))))
supposing Continuous+(P.M[P])
Proof
Definitions occuring in Statement :
deliver-msg: deliver-msg(t;m;x;Cs;L),
system-equiv: system-equiv(T.M[T];S1;S2),
pInTransit: pInTransit(P.M[P]),
component: component(P.M[P]),
process-equiv: process-equiv,
pMsg: pMsg(P.M[P]),
ldag: LabeledDAG(T),
Id: Id,
select: L[n],
length: ||as||,
list: T List,
strong-type-continuous: Continuous+(T.F[T]),
int_seg: {i..j-},
nat: ℕ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
top: Top,
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
function: x:A ⟶ B[x],
spread: spread def,
product: x:A × B[x],
natural_number: $n,
int: ℤ,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
member: t ∈ T,
strong-type-continuous: Continuous+(T.F[T]),
ext-eq: A ≡ B,
and: P ∧ Q,
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
deliver-msg: deliver-msg(t;m;x;Cs;L),
system-equiv: system-equiv(T.M[T];S1;S2),
select: L[n],
nil: [],
it: ⋅,
so_lambda: λ2x y.t[x; y],
top: Top,
so_apply: x[s1;s2],
cand: A c∧ B,
int_seg: {i..j-},
nat: ℕ,
ge: i ≥ j ,
lelt: i ≤ j < k,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
false: False,
not: ¬A,
prop: ℙ,
System: System(P.M[P]),
so_lambda: λ2x.t[x],
so_apply: x[s],
guard: {T},
decidable: Dec(P),
or: P ∨ Q,
component: component(P.M[P]),
cons: [a / b],
le: A ≤ B,
uiff: uiff(P;Q),
subtract: n - m,
less_than: a < b,
squash: ↓T,
iff: P ⇐⇒ Q,
list_accum: list_accum,
less_than': less_than'(a;b),
nat_plus: ℕ+,
true: True,
deliver-msg-to-comp: deliver-msg-to-comp(t;m;x;S;C),
Id: Id,
sq_type: SQType(T),
bool: 𝔹,
unit: Unit,
btrue: tt,
ifthenelse: if b then t else f fi ,
bfalse: ff,
bnot: ¬bb,
assert: ↑b,
process-equiv: process-equiv,
Process-stream: Process-stream(P;msgs),
dataflow-ap: df(a),
Process-apply: Process-apply(P;m),
pi2: snd(t),
rev_implies: P ⇐ Q,
listp: A List+,
pi1: fst(t)
Latex:
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}t:\mBbbN{}. \mforall{}x:Id. \mforall{}m:pMsg(P.M[P]). \mforall{}G1,G2:LabeledDAG(pInTransit(P.M[P])).
\mforall{}Cs1,Cs2:component(P.M[P]) List.
((\mforall{}k:\mBbbN{}||Cs1||. let x,P = Cs1[k] in let z,Q = Cs2[k] in (x = z) \mwedge{} P\mequiv{}Q)
{}\mRightarrow{} (system-equiv(P.M[P];deliver-msg(t;m;x;Cs1;G1);deliver-msg(t;m;x;Cs2;G2))
\mwedge{} (deliver-msg(t;m;x;Cs1;G1) = deliver-msg(t;m;x;Cs2;G2)))) supposing
((||Cs1|| = ||Cs2||) and
(G1 = G2))
supposing Continuous+(P.M[P])
Date html generated:
2016_05_17-AM-10_38_37
Last ObjectModification:
2016_01_18-AM-00_24_05
Theory : process-model
Home
Index