Step
*
1
1
2
1
1
1
1
1
of Lemma
std-components-property
1. [M] : Type ⟶ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ⟶ pMsg(P.M[P])@i
4. x : Id@i
5. Q : Process(P.M[P])@i
6. l2m : Id ⟶ pMsg(P.M[P])@i
7. S2 : InitialSystem(P.M[P])@i
8. sub-system(P.M[P];<[<x, Q>], lg-nil()>;S2)
9. env : pEnvType(P.M[P])@i
10. ∀e1,e2:runEvents(pRun(S2;env;n2m;l2m)).
(∀P:Process(P.M[P])
((P ∈ run-prior-state(S2;pRun(S2;env;n2m;l2m);e1))
⇒ (iterate-Process(P;map(λe.run-event-msg(pRun(S2;env;n2m;l2m);e);
run-event-interval(pRun(S2;env;n2m;l2m);e1;e2)))
∈ run-event-state(pRun(S2;env;n2m;l2m);e2)))) supposing
((run-event-step(e1) ≤ run-event-step(e2)) and
(run-event-loc(e1) = run-event-loc(e2) ∈ Id))
11. pRun(S2;env;n2m;l2m) ∈ pRunType(P.M[P])
12. reliable-env(env; pRun(S2;env;n2m;l2m))@i
13. ∀e:runEvents(pRun(S2;env;n2m;l2m)). ∀P:Process(P.M[P]).
((P ∈ run-event-state-when(pRun(S2;env;n2m;l2m);e))
⇒ ∀p∈snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e))))).let y,c = p
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':runEvents(pRun(S2;env;n2m;l2m))
((run-event-loc(e') = y ∈ Id)
∧ (e run-lt(pRun(S2;env;n2m;l2m)) e')
∧ (∃n:ℕ
∃nm:Id
((snd(run-info(pRun(S2;env;n2m;l2m);e')))
= command-to-msg(c;n2m n;l2m nm)
∈ pMsg(P.M[P])))
∧ ((run-cause(pRun(S2;env;n2m;l2m)) e')
= (inl e)
∈ (runEvents(pRun(S2;env;n2m;l2m))?)))))
14. E ⊆r runEvents(pRun(S2;env;n2m;l2m))
15. runEvents(pRun(S2;env;n2m;l2m)) ⊆r E
16. ∀e:runEvents(pRun(S2;env;n2m;l2m)). (loc(e) = run-event-loc(e) ∈ Id)
17. run-cause(pRun(S2;env;n2m;l2m)) ∈ E ⟶ (E?)
18. e : {e:runEvents(pRun(S2;env;n2m;l2m))| True} @i
19. P : Process(P.M[P])@i
20. e ∈ ℕ+ × Id
21. (P ∈ run-event-state-when(pRun(S2;env;n2m;l2m);e))@i
22. ∀n:ℕlg-size(snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e))))))
let y,c = lg-label(snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e)))));n)
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':runEvents(pRun(S2;env;n2m;l2m))
((run-event-loc(e') = y ∈ Id)
∧ (e run-lt(pRun(S2;env;n2m;l2m)) e')
∧ (∃n:ℕ
∃nm:Id. ((snd(run-info(pRun(S2;env;n2m;l2m);e'))) = command-to-msg(c;n2m n;l2m nm) ∈ pMsg(P.M[P])))
∧ ((run-cause(pRun(S2;env;n2m;l2m)) e') = (inl e) ∈ (runEvents(pRun(S2;env;n2m;l2m))?))))
23. n : ℕlg-size(snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e))))))@i
⊢ let y,c = lg-label(snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e)))));n)
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':{e:runEvents(pRun(S2;env;n2m;l2m))| True}
((run-event-loc(e') = y ∈ Id)
∧ (↓e run-lt(pRun(S2;env;n2m;l2m)) e')
∧ (∃n:ℕ. ∃nm:Id. ((snd(run-info(pRun(S2;env;n2m;l2m);e'))) = command-to-msg(c;n2m n;l2m nm) ∈ pMsg(P.M[P])))
∧ ((run-cause(pRun(S2;env;n2m;l2m)) e') = (inl e) ∈ ({e:runEvents(pRun(S2;env;n2m;l2m))| True} ?))))
BY
{ ((InstHyp [⌜n⌝] (-2)⋅ THENA Auto)
THEN MoveToConcl (-1)
THEN Fold `Process-apply` 0
THEN (GenConclAtAddr [1;1;1] THENA Auto)
THEN Unfold `pExt` -2
THEN GenConclAtAddrType ⌜Id × pCom(P.M[P])⌝ [1;1]⋅) }
1
.....wf.....
1. [M] : Type ⟶ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ⟶ pMsg(P.M[P])@i
4. x : Id@i
5. Q : Process(P.M[P])@i
6. l2m : Id ⟶ pMsg(P.M[P])@i
7. S2 : InitialSystem(P.M[P])@i
8. sub-system(P.M[P];<[<x, Q>], lg-nil()>;S2)
9. env : pEnvType(P.M[P])@i
10. ∀e1,e2:runEvents(pRun(S2;env;n2m;l2m)).
(∀P:Process(P.M[P])
((P ∈ run-prior-state(S2;pRun(S2;env;n2m;l2m);e1))
⇒ (iterate-Process(P;map(λe.run-event-msg(pRun(S2;env;n2m;l2m);e);
run-event-interval(pRun(S2;env;n2m;l2m);e1;e2)))
∈ run-event-state(pRun(S2;env;n2m;l2m);e2)))) supposing
((run-event-step(e1) ≤ run-event-step(e2)) and
(run-event-loc(e1) = run-event-loc(e2) ∈ Id))
11. pRun(S2;env;n2m;l2m) ∈ pRunType(P.M[P])
12. reliable-env(env; pRun(S2;env;n2m;l2m))@i
13. ∀e:runEvents(pRun(S2;env;n2m;l2m)). ∀P:Process(P.M[P]).
((P ∈ run-event-state-when(pRun(S2;env;n2m;l2m);e))
⇒ ∀p∈snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e))))).let y,c = p
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':runEvents(pRun(S2;env;n2m;l2m))
((run-event-loc(e') = y ∈ Id)
∧ (e run-lt(pRun(S2;env;n2m;l2m)) e')
∧ (∃n:ℕ
∃nm:Id
((snd(run-info(pRun(S2;env;n2m;l2m);e')))
= command-to-msg(c;n2m n;l2m nm)
∈ pMsg(P.M[P])))
∧ ((run-cause(pRun(S2;env;n2m;l2m)) e')
= (inl e)
∈ (runEvents(pRun(S2;env;n2m;l2m))?)))))
14. E ⊆r runEvents(pRun(S2;env;n2m;l2m))
15. runEvents(pRun(S2;env;n2m;l2m)) ⊆r E
16. ∀e:runEvents(pRun(S2;env;n2m;l2m)). (loc(e) = run-event-loc(e) ∈ Id)
17. run-cause(pRun(S2;env;n2m;l2m)) ∈ E ⟶ (E?)
18. e : {e:runEvents(pRun(S2;env;n2m;l2m))| True} @i
19. P : Process(P.M[P])@i
20. e ∈ ℕ+ × Id
21. (P ∈ run-event-state-when(pRun(S2;env;n2m;l2m);e))@i
22. ∀n:ℕlg-size(snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e))))))
let y,c = lg-label(snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e)))));n)
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':runEvents(pRun(S2;env;n2m;l2m))
((run-event-loc(e') = y ∈ Id)
∧ (e run-lt(pRun(S2;env;n2m;l2m)) e')
∧ (∃n:ℕ
∃nm:Id. ((snd(run-info(pRun(S2;env;n2m;l2m);e'))) = command-to-msg(c;n2m n;l2m nm) ∈ pMsg(P.M[P])))
∧ ((run-cause(pRun(S2;env;n2m;l2m)) e') = (inl e) ∈ (runEvents(pRun(S2;env;n2m;l2m))?))))
23. n : ℕlg-size(snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e))))))@i
24. v : LabeledDAG(Id × pCom(P.M[P]))@i
25. (snd(Process-apply(P;snd(run-info(pRun(S2;env;n2m;l2m);e))))) = v ∈ pExt(P.M[P])@i
⊢ lg-label(v;n) ∈ Id × pCom(P.M[P])
2
.....wf.....
1. [M] : Type ⟶ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ⟶ pMsg(P.M[P])@i
4. x : Id@i
5. Q : Process(P.M[P])@i
6. l2m : Id ⟶ pMsg(P.M[P])@i
7. S2 : InitialSystem(P.M[P])@i
8. sub-system(P.M[P];<[<x, Q>], lg-nil()>;S2)
9. env : pEnvType(P.M[P])@i
10. ∀e1,e2:runEvents(pRun(S2;env;n2m;l2m)).
(∀P:Process(P.M[P])
((P ∈ run-prior-state(S2;pRun(S2;env;n2m;l2m);e1))
⇒ (iterate-Process(P;map(λe.run-event-msg(pRun(S2;env;n2m;l2m);e);
run-event-interval(pRun(S2;env;n2m;l2m);e1;e2)))
∈ run-event-state(pRun(S2;env;n2m;l2m);e2)))) supposing
((run-event-step(e1) ≤ run-event-step(e2)) and
(run-event-loc(e1) = run-event-loc(e2) ∈ Id))
11. pRun(S2;env;n2m;l2m) ∈ pRunType(P.M[P])
12. reliable-env(env; pRun(S2;env;n2m;l2m))@i
13. ∀e:runEvents(pRun(S2;env;n2m;l2m)). ∀P:Process(P.M[P]).
((P ∈ run-event-state-when(pRun(S2;env;n2m;l2m);e))
⇒ ∀p∈snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e))))).let y,c = p
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':runEvents(pRun(S2;env;n2m;l2m))
((run-event-loc(e') = y ∈ Id)
∧ (e run-lt(pRun(S2;env;n2m;l2m)) e')
∧ (∃n:ℕ
∃nm:Id
((snd(run-info(pRun(S2;env;n2m;l2m);e')))
= command-to-msg(c;n2m n;l2m nm)
∈ pMsg(P.M[P])))
∧ ((run-cause(pRun(S2;env;n2m;l2m)) e')
= (inl e)
∈ (runEvents(pRun(S2;env;n2m;l2m))?)))))
14. E ⊆r runEvents(pRun(S2;env;n2m;l2m))
15. runEvents(pRun(S2;env;n2m;l2m)) ⊆r E
16. ∀e:runEvents(pRun(S2;env;n2m;l2m)). (loc(e) = run-event-loc(e) ∈ Id)
17. run-cause(pRun(S2;env;n2m;l2m)) ∈ E ⟶ (E?)
18. e : {e:runEvents(pRun(S2;env;n2m;l2m))| True} @i
19. P : Process(P.M[P])@i
20. e ∈ ℕ+ × Id
21. (P ∈ run-event-state-when(pRun(S2;env;n2m;l2m);e))@i
22. ∀n:ℕlg-size(snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e))))))
let y,c = lg-label(snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e)))));n)
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':runEvents(pRun(S2;env;n2m;l2m))
((run-event-loc(e') = y ∈ Id)
∧ (e run-lt(pRun(S2;env;n2m;l2m)) e')
∧ (∃n:ℕ
∃nm:Id. ((snd(run-info(pRun(S2;env;n2m;l2m);e'))) = command-to-msg(c;n2m n;l2m nm) ∈ pMsg(P.M[P])))
∧ ((run-cause(pRun(S2;env;n2m;l2m)) e') = (inl e) ∈ (runEvents(pRun(S2;env;n2m;l2m))?))))
23. n : ℕlg-size(snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e))))))@i
24. v : LabeledDAG(Id × pCom(P.M[P]))@i
25. (snd(Process-apply(P;snd(run-info(pRun(S2;env;n2m;l2m);e))))) = v ∈ pExt(P.M[P])@i
⊢ Id × pCom(P.M[P]) ∈ 𝕌{[1 | i 0]}
3
1. [M] : Type ⟶ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ⟶ pMsg(P.M[P])@i
4. x : Id@i
5. Q : Process(P.M[P])@i
6. l2m : Id ⟶ pMsg(P.M[P])@i
7. S2 : InitialSystem(P.M[P])@i
8. sub-system(P.M[P];<[<x, Q>], lg-nil()>;S2)
9. env : pEnvType(P.M[P])@i
10. ∀e1,e2:runEvents(pRun(S2;env;n2m;l2m)).
(∀P:Process(P.M[P])
((P ∈ run-prior-state(S2;pRun(S2;env;n2m;l2m);e1))
⇒ (iterate-Process(P;map(λe.run-event-msg(pRun(S2;env;n2m;l2m);e);
run-event-interval(pRun(S2;env;n2m;l2m);e1;e2)))
∈ run-event-state(pRun(S2;env;n2m;l2m);e2)))) supposing
((run-event-step(e1) ≤ run-event-step(e2)) and
(run-event-loc(e1) = run-event-loc(e2) ∈ Id))
11. pRun(S2;env;n2m;l2m) ∈ pRunType(P.M[P])
12. reliable-env(env; pRun(S2;env;n2m;l2m))@i
13. ∀e:runEvents(pRun(S2;env;n2m;l2m)). ∀P:Process(P.M[P]).
((P ∈ run-event-state-when(pRun(S2;env;n2m;l2m);e))
⇒ ∀p∈snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e))))).let y,c = p
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':runEvents(pRun(S2;env;n2m;l2m))
((run-event-loc(e') = y ∈ Id)
∧ (e run-lt(pRun(S2;env;n2m;l2m)) e')
∧ (∃n:ℕ
∃nm:Id
((snd(run-info(pRun(S2;env;n2m;l2m);e')))
= command-to-msg(c;n2m n;l2m nm)
∈ pMsg(P.M[P])))
∧ ((run-cause(pRun(S2;env;n2m;l2m)) e')
= (inl e)
∈ (runEvents(pRun(S2;env;n2m;l2m))?)))))
14. E ⊆r runEvents(pRun(S2;env;n2m;l2m))
15. runEvents(pRun(S2;env;n2m;l2m)) ⊆r E
16. ∀e:runEvents(pRun(S2;env;n2m;l2m)). (loc(e) = run-event-loc(e) ∈ Id)
17. run-cause(pRun(S2;env;n2m;l2m)) ∈ E ⟶ (E?)
18. e : {e:runEvents(pRun(S2;env;n2m;l2m))| True} @i
19. P : Process(P.M[P])@i
20. e ∈ ℕ+ × Id
21. (P ∈ run-event-state-when(pRun(S2;env;n2m;l2m);e))@i
22. ∀n:ℕlg-size(snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e))))))
let y,c = lg-label(snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e)))));n)
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':runEvents(pRun(S2;env;n2m;l2m))
((run-event-loc(e') = y ∈ Id)
∧ (e run-lt(pRun(S2;env;n2m;l2m)) e')
∧ (∃n:ℕ
∃nm:Id. ((snd(run-info(pRun(S2;env;n2m;l2m);e'))) = command-to-msg(c;n2m n;l2m nm) ∈ pMsg(P.M[P])))
∧ ((run-cause(pRun(S2;env;n2m;l2m)) e') = (inl e) ∈ (runEvents(pRun(S2;env;n2m;l2m))?))))
23. n : ℕlg-size(snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e))))))@i
24. v : LabeledDAG(Id × pCom(P.M[P]))@i
25. (snd(Process-apply(P;snd(run-info(pRun(S2;env;n2m;l2m);e))))) = v ∈ pExt(P.M[P])@i
26. v1 : Id × pCom(P.M[P])@i
27. lg-label(v;n) = v1 ∈ (Id × pCom(P.M[P]))@i
⊢ let y,c = v1
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':runEvents(pRun(S2;env;n2m;l2m))
((run-event-loc(e') = y ∈ Id)
∧ (e run-lt(pRun(S2;env;n2m;l2m)) e')
∧ (∃n:ℕ
∃nm:Id
((snd(run-info(pRun(S2;env;n2m;l2m);e')))
= command-to-msg(c;Process-apply(n2m;n);Process-apply(l2m;nm))
∈ pMsg(P.M[P])))
∧ (Process-apply(run-cause(pRun(S2;env;n2m;l2m));e') = (inl e) ∈ (runEvents(pRun(S2;env;n2m;l2m))?))))
⇒ let y,c = v1
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':{e:runEvents(pRun(S2;env;n2m;l2m))| True}
((run-event-loc(e') = y ∈ Id)
∧ (↓e run-lt(pRun(S2;env;n2m;l2m)) e')
∧ (∃n:ℕ
∃nm:Id
((snd(run-info(pRun(S2;env;n2m;l2m);e')))
= command-to-msg(c;Process-apply(n2m;n);Process-apply(l2m;nm))
∈ pMsg(P.M[P])))
∧ (Process-apply(run-cause(pRun(S2;env;n2m;l2m));e')
= (inl e)
∈ ({e:runEvents(pRun(S2;env;n2m;l2m))| True} ?))))
Latex:
Latex:
1. [M] : Type {}\mrightarrow{} Type
2. Continuous+(P.M[P])
3. n2m : \mBbbN{} {}\mrightarrow{} pMsg(P.M[P])@i
4. x : Id@i
5. Q : Process(P.M[P])@i
6. l2m : Id {}\mrightarrow{} pMsg(P.M[P])@i
7. S2 : InitialSystem(P.M[P])@i
8. sub-system(P.M[P];<[<x, Q>], lg-nil()>S2)
9. env : pEnvType(P.M[P])@i
10. \mforall{}e1,e2:runEvents(pRun(S2;env;n2m;l2m)).
(\mforall{}P:Process(P.M[P])
((P \mmember{} run-prior-state(S2;pRun(S2;env;n2m;l2m);e1))
{}\mRightarrow{} (iterate-Process(P;map(\mlambda{}e.run-event-msg(pRun(S2;env;n2m;l2m);e);
run-event-interval(pRun(S2;env;n2m;l2m);e1;e2)))
\mmember{} run-event-state(pRun(S2;env;n2m;l2m);e2)))) supposing
((run-event-step(e1) \mleq{} run-event-step(e2)) and
(run-event-loc(e1) = run-event-loc(e2)))
11. pRun(S2;env;n2m;l2m) \mmember{} pRunType(P.M[P])
12. reliable-env(env; pRun(S2;env;n2m;l2m))@i
13. \mforall{}e:runEvents(pRun(S2;env;n2m;l2m)). \mforall{}P:Process(P.M[P]).
((P \mmember{} run-event-state-when(pRun(S2;env;n2m;l2m);e))
{}\mRightarrow{} \mforall{}p\mmember{}snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e))))).
let y,c = p
in (com-kind(c) \mmember{} ``msg choose new``)
{}\mRightarrow{} (\mexists{}e':runEvents(pRun(S2;env;n2m;l2m))
((run-event-loc(e') = y)
\mwedge{} (e run-lt(pRun(S2;env;n2m;l2m)) e')
\mwedge{} (\mexists{}n:\mBbbN{}
\mexists{}nm:Id
((snd(run-info(pRun(S2;env;n2m;l2m);e'))) = command-to-msg(c;n2m n;l2m nm)))
\mwedge{} ((run-cause(pRun(S2;env;n2m;l2m)) e') = (inl e)))))
14. E \msubseteq{}r runEvents(pRun(S2;env;n2m;l2m))
15. runEvents(pRun(S2;env;n2m;l2m)) \msubseteq{}r E
16. \mforall{}e:runEvents(pRun(S2;env;n2m;l2m)). (loc(e) = run-event-loc(e))
17. run-cause(pRun(S2;env;n2m;l2m)) \mmember{} E {}\mrightarrow{} (E?)
18. e : \{e:runEvents(pRun(S2;env;n2m;l2m))| True\} @i
19. P : Process(P.M[P])@i
20. e \mmember{} \mBbbN{}\msupplus{} \mtimes{} Id
21. (P \mmember{} run-event-state-when(pRun(S2;env;n2m;l2m);e))@i
22. \mforall{}n:\mBbbN{}lg-size(snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e))))))
let y,c = lg-label(snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e)))));n)
in (com-kind(c) \mmember{} ``msg choose new``)
{}\mRightarrow{} (\mexists{}e':runEvents(pRun(S2;env;n2m;l2m))
((run-event-loc(e') = y)
\mwedge{} (e run-lt(pRun(S2;env;n2m;l2m)) e')
\mwedge{} (\mexists{}n:\mBbbN{}
\mexists{}nm:Id
((snd(run-info(pRun(S2;env;n2m;l2m);e'))) = command-to-msg(c;n2m n;l2m nm)))
\mwedge{} ((run-cause(pRun(S2;env;n2m;l2m)) e') = (inl e))))
23. n : \mBbbN{}lg-size(snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e))))))@i
\mvdash{} let y,c = lg-label(snd((P (snd(run-info(pRun(S2;env;n2m;l2m);e)))));n)
in (com-kind(c) \mmember{} ``msg choose new``)
{}\mRightarrow{} (\mexists{}e':\{e:runEvents(pRun(S2;env;n2m;l2m))| True\}
((run-event-loc(e') = y)
\mwedge{} (\mdownarrow{}e run-lt(pRun(S2;env;n2m;l2m)) e')
\mwedge{} (\mexists{}n:\mBbbN{}
\mexists{}nm:Id. ((snd(run-info(pRun(S2;env;n2m;l2m);e'))) = command-to-msg(c;n2m n;l2m nm)))
\mwedge{} ((run-cause(pRun(S2;env;n2m;l2m)) e') = (inl e))))
By
Latex:
((InstHyp [\mkleeneopen{}n\mkleeneclose{}] (-2)\mcdot{} THENA Auto)
THEN MoveToConcl (-1)
THEN Fold `Process-apply` 0
THEN (GenConclAtAddr [1;1;1] THENA Auto)
THEN Unfold `pExt` -2
THEN GenConclAtAddrType \mkleeneopen{}Id \mtimes{} pCom(P.M[P])\mkleeneclose{} [1;1]\mcdot{})
Home
Index