Step
*
1
of Lemma
reliable-env-property2
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. e : runEvents(pRun(S;env;n2m;l2m))@i
11. P : Process(P.M[P])@i
12. (P ∈ run-event-state-when(pRun(S;env;n2m;l2m);e))@i
13. 0 < fst(e)
⊢ ∀p∈snd((P (snd(run-info(pRun(S;env;n2m;l2m);e))))).let y,c = p
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':runEvents(pRun(S;env;n2m;l2m))
((run-event-loc(e') = y ∈ Id)
∧ (e run-lt(pRun(S;env;n2m;l2m)) e')
∧ (∃n:ℕ
∃nm:Id
((snd(run-info(pRun(S;env;n2m;l2m);e')))
= command-to-msg(c;n2m n;l2m nm)
∈ pMsg(P.M[P])))
∧ ((run-cause(pRun(S;env;n2m;l2m)) e')
= (inl e)
∈ (runEvents(pRun(S;env;n2m;l2m))?))))
BY
{ (GenConclAtAddr [1;1;2;1] ⋅
THEN D -2
THEN Reduce 0
THEN RenameVar `ms' (-2)
THEN Subst' P ms ~ Process-apply(P;ms) 0
THEN Try ((Unfold `Process-apply` 0 THEN Complete (Auto)))
THEN (RepeatFor 2 (DVar `e')
THEN RenameVar `t' (-9)
THEN RenameVar `x' (-8)
THEN All Reduce
THEN RepUR ``run-info`` -1
THEN GenConclAtAddr [1;1] ⋅
THEN D -2
THEN RenameVar `G' (-2)
THEN Reduce 0
THEN RepUR ``pExt`` -2
THEN D 0
THEN Auto
THEN (GenConclAtAddrType ⌈Id × pCom(P.M[P])⌉ [1]⋅ THENA Auto)
THEN D -2
THEN Reduce 0
THEN Auto)⋅)⋅ }
1
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. \\%12 : ↑is-run-event(pRun(S;env;n2m;l2m);t;x)@i
13. P : Process(P.M[P])@i
14. (P ∈ run-event-state-when(pRun(S;env;n2m;l2m);<t, x>))@i
15. 0 < t
16. v1 : ℤ × Id@i
17. ms : pMsg(P.M[P])@i
18. 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
19. v2 : Process(P.M[P])@i
20. G : LabeledDAG(Id × pCom(P.M[P]))@i
21. Process-apply(P;ms) = <v2, G> ∈ (Process(P.M[P]) × pExt(P.M[P]))@i
22. n : ℕlg-size(G)@i
23. v3 : Id@i
24. v4 : pCom(P.M[P])@i
25. lg-label(G;n) = <v3, v4> ∈ (Id × pCom(P.M[P]))@i
26. (com-kind(v4) ∈ ``msg choose new``)@i
⊢ ∃e':runEvents(pRun(S;env;n2m;l2m))
((run-event-loc(e') = v3 ∈ Id)
∧ (<t, x> run-lt(pRun(S;env;n2m;l2m)) e')
∧ (∃n:ℕ. ∃nm:Id. ((snd(run-info(pRun(S;env;n2m;l2m);e'))) = command-to-msg(v4;n2m n;l2m nm) ∈ pMsg(P.M[P])))
∧ ((run-cause(pRun(S;env;n2m;l2m)) e') = (inl <t, x>) ∈ (runEvents(pRun(S;env;n2m;l2m))?)))
Latex:
Latex:
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. e : runEvents(pRun(S;env;n2m;l2m))@i
11. P : Process(P.M[P])@i
12. (P \mmember{} run-event-state-when(pRun(S;env;n2m;l2m);e))@i
13. 0 < fst(e)
\mvdash{} \mforall{}p\mmember{}snd((P (snd(run-info(pRun(S;env;n2m;l2m);e))))).
let y,c = p
in (com-kind(c) \mmember{} ``msg choose new``)
{}\mRightarrow{} (\mexists{}e':runEvents(pRun(S;env;n2m;l2m))
((run-event-loc(e') = y)
\mwedge{} (e run-lt(pRun(S;env;n2m;l2m)) e')
\mwedge{} (\mexists{}n:\mBbbN{}
\mexists{}nm:Id. ((snd(run-info(pRun(S;env;n2m;l2m);e'))) = command-to-msg(c;n2m n;l2m nm)))
\mwedge{} ((run-cause(pRun(S;env;n2m;l2m)) e') = (inl e))))
By
Latex:
(GenConclAtAddr [1;1;2;1] \mcdot{}
THEN D -2
THEN Reduce 0
THEN RenameVar `ms' (-2)
THEN Subst' P ms \msim{} Process-apply(P;ms) 0
THEN Try ((Unfold `Process-apply` 0 THEN Complete (Auto)))
THEN (RepeatFor 2 (DVar `e')
THEN RenameVar `t' (-9)
THEN RenameVar `x' (-8)
THEN All Reduce
THEN RepUR ``run-info`` -1
THEN GenConclAtAddr [1;1] \mcdot{}
THEN D -2
THEN RenameVar `G' (-2)
THEN Reduce 0
THEN RepUR ``pExt`` -2
THEN D 0
THEN Auto
THEN (GenConclAtAddrType \mkleeneopen{}Id \mtimes{} pCom(P.M[P])\mkleeneclose{} [1]\mcdot{} THENA Auto)
THEN D -2
THEN Reduce 0
THEN Auto)\mcdot{})\mcdot{}
Home
Index