Step
*
1
1
2
2
2
3
3
2
of Lemma
reliable-env-property2
.....subterm..... T:t
2:n
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. S : InitialSystem(P.M[P])@i
4. n2m : ℕ ─→ pMsg(P.M[P])@i
5. l2m : Id ─→ pMsg(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. pRun(S;env;n2m;l2m) ∈ pRunType(P.M[P])
8. reliable-env(env; pRun(S;env;n2m;l2m))@i
9. ∀tn:run-msg-commands(pRun(S;env;n2m;l2m))
∃e:runEvents(pRun(S;env;n2m;l2m))
let t,n = tn
in (run-info(pRun(S;env;n2m;l2m);e)
= intransit-to-info(n2m;l2m;pRun(S;env;n2m;l2m);env;run-event-step(e);run-command(pRun(S;env;n2m;l2m);t;n))
∈ (ℤ × Id × pMsg(P.M[P])))
∧ (run-event-loc(e) = (fst(snd(run-command(pRun(S;env;n2m;l2m);t;n)))) ∈ Id)
10. t : ℕ@i
11. x : Id@i
12. λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹
13. ↑is-run-event(pRun(S;env;n2m;l2m);t;x)@i
14. P : Process(P.M[P])@i
15. (P ∈ run-event-state-when(pRun(S;env;n2m;l2m);<t, x>))@i
16. 0 < t
17. v1 : ℤ × Id@i
18. ms : pMsg(P.M[P])@i
19. let info,S = pRun(S;env;n2m;l2m) t in let ev,z,m = outl(info) in <ev, m> = <v1, ms> ∈ (ℤ × Id × pMsg(P.M[P]))@i
20. v2 : Process(P.M[P])@i
21. G : LabeledDAG(Id × pCom(P.M[P]))@i
22. Process-apply(P;ms) = <v2, G> ∈ (Process(P.M[P]) × pExt(P.M[P]))@i
23. n : ℕlg-size(G)@i
24. v3 : Id@i
25. v4 : pCom(P.M[P])@i
26. lg-label(G;n) = <v3, v4> ∈ (Id × pCom(P.M[P]))@i
27. (com-kind(v4) ∈ ``msg choose new``)@i
28. add-cause(<t, x>;G) ⊆ snd(snd((pRun(S;env;n2m;l2m) t)))
29. m : ℕlg-size(snd(snd((pRun(S;env;n2m;l2m) t))))
30. lg-label(snd(snd((pRun(S;env;n2m;l2m) t)));m) = <<t, x>, v3, v4> ∈ pInTransit(P.M[P])
31. e : runEvents(pRun(S;env;n2m;l2m))
32. (run-info(pRun(S;env;n2m;l2m);e)
= intransit-to-info(n2m;l2m;pRun(S;env;n2m;l2m);env;run-event-step(e);run-command(pRun(S;env;n2m;l2m);t;m))
∈ (ℤ × Id × pMsg(P.M[P])))
∧ (run-event-loc(e) = (fst(snd(run-command(pRun(S;env;n2m;l2m);t;m)))) ∈ Id)
33. e' : runEvents(pRun(S;env;n2m;l2m))
34. v : pRunType(P.M[P])@i
35. pRun(S;env;n2m;l2m) = v ∈ pRunType(P.M[P])@i
⊢ (<t, x> run-lt(v) e')
∧ (∃n:ℕ. ∃nm:Id. ((snd(run-info(v;e'))) = command-to-msg(v4;n2m n;l2m nm) ∈ pMsg(P.M[P])))
∧ ((run-cause(v) e') = (inl <t, x>) ∈ (runEvents(v)?)) ∈ ℙ
BY
{ MemCD }
1
.....subterm..... T:t
1:n
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. S : InitialSystem(P.M[P])@i
4. n2m : ℕ ─→ pMsg(P.M[P])@i
5. l2m : Id ─→ pMsg(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. pRun(S;env;n2m;l2m) ∈ pRunType(P.M[P])
8. reliable-env(env; pRun(S;env;n2m;l2m))@i
9. ∀tn:run-msg-commands(pRun(S;env;n2m;l2m))
∃e:runEvents(pRun(S;env;n2m;l2m))
let t,n = tn
in (run-info(pRun(S;env;n2m;l2m);e)
= intransit-to-info(n2m;l2m;pRun(S;env;n2m;l2m);env;run-event-step(e);run-command(pRun(S;env;n2m;l2m);t;n))
∈ (ℤ × Id × pMsg(P.M[P])))
∧ (run-event-loc(e) = (fst(snd(run-command(pRun(S;env;n2m;l2m);t;n)))) ∈ Id)
10. t : ℕ@i
11. x : Id@i
12. λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹
13. ↑is-run-event(pRun(S;env;n2m;l2m);t;x)@i
14. P : Process(P.M[P])@i
15. (P ∈ run-event-state-when(pRun(S;env;n2m;l2m);<t, x>))@i
16. 0 < t
17. v1 : ℤ × Id@i
18. ms : pMsg(P.M[P])@i
19. let info,S = pRun(S;env;n2m;l2m) t in let ev,z,m = outl(info) in <ev, m> = <v1, ms> ∈ (ℤ × Id × pMsg(P.M[P]))@i
20. v2 : Process(P.M[P])@i
21. G : LabeledDAG(Id × pCom(P.M[P]))@i
22. Process-apply(P;ms) = <v2, G> ∈ (Process(P.M[P]) × pExt(P.M[P]))@i
23. n : ℕlg-size(G)@i
24. v3 : Id@i
25. v4 : pCom(P.M[P])@i
26. lg-label(G;n) = <v3, v4> ∈ (Id × pCom(P.M[P]))@i
27. (com-kind(v4) ∈ ``msg choose new``)@i
28. add-cause(<t, x>;G) ⊆ snd(snd((pRun(S;env;n2m;l2m) t)))
29. m : ℕlg-size(snd(snd((pRun(S;env;n2m;l2m) t))))
30. lg-label(snd(snd((pRun(S;env;n2m;l2m) t)));m) = <<t, x>, v3, v4> ∈ pInTransit(P.M[P])
31. e : runEvents(pRun(S;env;n2m;l2m))
32. (run-info(pRun(S;env;n2m;l2m);e)
= intransit-to-info(n2m;l2m;pRun(S;env;n2m;l2m);env;run-event-step(e);run-command(pRun(S;env;n2m;l2m);t;m))
∈ (ℤ × Id × pMsg(P.M[P])))
∧ (run-event-loc(e) = (fst(snd(run-command(pRun(S;env;n2m;l2m);t;m)))) ∈ Id)
33. e' : runEvents(pRun(S;env;n2m;l2m))
34. v : pRunType(P.M[P])@i
35. pRun(S;env;n2m;l2m) = v ∈ pRunType(P.M[P])@i
⊢ <t, x> run-lt(v) e' ∈ ℙ
2
.....subterm..... T:t
2:n
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. S : InitialSystem(P.M[P])@i
4. n2m : ℕ ─→ pMsg(P.M[P])@i
5. l2m : Id ─→ pMsg(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. pRun(S;env;n2m;l2m) ∈ pRunType(P.M[P])
8. reliable-env(env; pRun(S;env;n2m;l2m))@i
9. ∀tn:run-msg-commands(pRun(S;env;n2m;l2m))
∃e:runEvents(pRun(S;env;n2m;l2m))
let t,n = tn
in (run-info(pRun(S;env;n2m;l2m);e)
= intransit-to-info(n2m;l2m;pRun(S;env;n2m;l2m);env;run-event-step(e);run-command(pRun(S;env;n2m;l2m);t;n))
∈ (ℤ × Id × pMsg(P.M[P])))
∧ (run-event-loc(e) = (fst(snd(run-command(pRun(S;env;n2m;l2m);t;n)))) ∈ Id)
10. t : ℕ@i
11. x : Id@i
12. λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹
13. ↑is-run-event(pRun(S;env;n2m;l2m);t;x)@i
14. P : Process(P.M[P])@i
15. (P ∈ run-event-state-when(pRun(S;env;n2m;l2m);<t, x>))@i
16. 0 < t
17. v1 : ℤ × Id@i
18. ms : pMsg(P.M[P])@i
19. let info,S = pRun(S;env;n2m;l2m) t in let ev,z,m = outl(info) in <ev, m> = <v1, ms> ∈ (ℤ × Id × pMsg(P.M[P]))@i
20. v2 : Process(P.M[P])@i
21. G : LabeledDAG(Id × pCom(P.M[P]))@i
22. Process-apply(P;ms) = <v2, G> ∈ (Process(P.M[P]) × pExt(P.M[P]))@i
23. n : ℕlg-size(G)@i
24. v3 : Id@i
25. v4 : pCom(P.M[P])@i
26. lg-label(G;n) = <v3, v4> ∈ (Id × pCom(P.M[P]))@i
27. (com-kind(v4) ∈ ``msg choose new``)@i
28. add-cause(<t, x>;G) ⊆ snd(snd((pRun(S;env;n2m;l2m) t)))
29. m : ℕlg-size(snd(snd((pRun(S;env;n2m;l2m) t))))
30. lg-label(snd(snd((pRun(S;env;n2m;l2m) t)));m) = <<t, x>, v3, v4> ∈ pInTransit(P.M[P])
31. e : runEvents(pRun(S;env;n2m;l2m))
32. (run-info(pRun(S;env;n2m;l2m);e)
= intransit-to-info(n2m;l2m;pRun(S;env;n2m;l2m);env;run-event-step(e);run-command(pRun(S;env;n2m;l2m);t;m))
∈ (ℤ × Id × pMsg(P.M[P])))
∧ (run-event-loc(e) = (fst(snd(run-command(pRun(S;env;n2m;l2m);t;m)))) ∈ Id)
33. e' : runEvents(pRun(S;env;n2m;l2m))
34. v : pRunType(P.M[P])@i
35. pRun(S;env;n2m;l2m) = v ∈ pRunType(P.M[P])@i
⊢ (∃n:ℕ. ∃nm:Id. ((snd(run-info(v;e'))) = command-to-msg(v4;n2m n;l2m nm) ∈ pMsg(P.M[P])))
∧ ((run-cause(v) e') = (inl <t, x>) ∈ (runEvents(v)?)) ∈ ℙ
Latex:
Latex:
.....subterm..... T:t
2:n
1. M : Type {}\mrightarrow{} Type
2. Continuous+(P.M[P])
3. S : InitialSystem(P.M[P])@i
4. n2m : \mBbbN{} {}\mrightarrow{} pMsg(P.M[P])@i
5. l2m : Id {}\mrightarrow{} pMsg(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. pRun(S;env;n2m;l2m) \mmember{} pRunType(P.M[P])
8. reliable-env(env; pRun(S;env;n2m;l2m))@i
9. \mforall{}tn:run-msg-commands(pRun(S;env;n2m;l2m))
\mexists{}e:runEvents(pRun(S;env;n2m;l2m))
let t,n = tn
in ...
\mwedge{} (run-event-loc(e) = (fst(snd(run-command(pRun(S;env;n2m;l2m);t;n)))))
10. t : \mBbbN{}@i
11. x : Id@i
12. \mlambda{}c.fst(c) = x \mmember{} component(P.M[P]) {}\mrightarrow{} \mBbbB{}
13. \muparrow{}is-run-event(pRun(S;env;n2m;l2m);t;x)@i
14. P : Process(P.M[P])@i
15. (P \mmember{} run-event-state-when(pRun(S;env;n2m;l2m);<t, x>))@i
16. 0 < t
17. v1 : \mBbbZ{} \mtimes{} Id@i
18. ms : pMsg(P.M[P])@i
19. let info,S = pRun(S;env;n2m;l2m) t in let ev,z,m = outl(info) in <ev, m> = <v1, ms>@i
20. v2 : Process(P.M[P])@i
21. G : LabeledDAG(Id \mtimes{} pCom(P.M[P]))@i
22. Process-apply(P;ms) = <v2, G>@i
23. n : \mBbbN{}lg-size(G)@i
24. v3 : Id@i
25. v4 : pCom(P.M[P])@i
26. lg-label(G;n) = <v3, v4>@i
27. (com-kind(v4) \mmember{} ``msg choose new``)@i
28. add-cause(<t, x>G) \msubseteq{} snd(snd((pRun(S;env;n2m;l2m) t)))
29. m : \mBbbN{}lg-size(snd(snd((pRun(S;env;n2m;l2m) t))))
30. lg-label(snd(snd((pRun(S;env;n2m;l2m) t)));m) = <<t, x>, v3, v4>
31. e : runEvents(pRun(S;env;n2m;l2m))
32. (run-info(pRun(S;env;n2m;l2m);e)
= intransit-to-info(n2m;l2m;pRun(S;env;n2m;l2m);env;run-event-step(e);run-command(...;t;m)))
\mwedge{} (run-event-loc(e) = (fst(snd(run-command(pRun(S;env;n2m;l2m);t;m)))))
33. e' : runEvents(pRun(S;env;n2m;l2m))
34. v : pRunType(P.M[P])@i
35. pRun(S;env;n2m;l2m) = v@i
\mvdash{} (<t, x> run-lt(v) e')
\mwedge{} (\mexists{}n:\mBbbN{}. \mexists{}nm:Id. ((snd(run-info(v;e'))) = command-to-msg(v4;n2m n;l2m nm)))
\mwedge{} ((run-cause(v) e') = (inl <t, x>)) \mmember{} \mBbbP{}
By
Latex:
MemCD
Home
Index