Step
*
1
1
of Lemma
std-components-property
1. [M] : Type ─→ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ─→ pMsg(P.M[P])@i
4. C : component(P.M[P])@i
5. l2m : Id ─→ pMsg(P.M[P])@i
6. Cs : component(P.M[P]) List@i
7. <Cs, lg-nil()> ∈ System(P.M[P])
8. S2 : InitialSystem(P.M[P])@i
9. sub-system(P.M[P];<Cs, lg-nil()>;S2)@i
10. env : pEnvType(P.M[P])@i
11. ∀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))
12. pRun(S2;env;n2m;l2m) ∈ pRunType(P.M[P])
13. reliable-env(env; pRun(S2;env;n2m;l2m))@i
14. ∀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))?)))))
15. E ⊆r runEvents(pRun(S2;env;n2m;l2m))
16. runEvents(pRun(S2;env;n2m;l2m)) ⊆r E
17. ∀e:runEvents(pRun(S2;env;n2m;l2m)). (loc(e) = run-event-loc(e) ∈ Id)
18. run-cause(pRun(S2;env;n2m;l2m)) ∈ E ─→ (E?)
19. (C ∈ Cs)
⊢ ∀e:E
∀p∈last(data-stream(snd(C);map(λe.info(e);before(e) @ [e]))).let y,c = p
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':E
((loc(e') = y ∈ Id)
∧ (e < e')
∧ (∃n:ℕ
∃nm:Id
(info(e')
= command-to-msg(c;n2m n;l2m nm)
∈ pMsg(P.M[P])))
∧ ((run-cause(pRun(S2;env;n2m;l2m)) e')
= (inl e)
∈ (E?))))
supposing loc(e) = (fst(C)) ∈ Id
BY
{ Assert ⌈sub-system(P.M[P];<[C], lg-nil()>;S2)⌉⋅ }
1
.....assertion.....
1. [M] : Type ─→ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ─→ pMsg(P.M[P])@i
4. C : component(P.M[P])@i
5. l2m : Id ─→ pMsg(P.M[P])@i
6. Cs : component(P.M[P]) List@i
7. <Cs, lg-nil()> ∈ System(P.M[P])
8. S2 : InitialSystem(P.M[P])@i
9. sub-system(P.M[P];<Cs, lg-nil()>;S2)@i
10. env : pEnvType(P.M[P])@i
11. ∀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))
12. pRun(S2;env;n2m;l2m) ∈ pRunType(P.M[P])
13. reliable-env(env; pRun(S2;env;n2m;l2m))@i
14. ∀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))?)))))
15. E ⊆r runEvents(pRun(S2;env;n2m;l2m))
16. runEvents(pRun(S2;env;n2m;l2m)) ⊆r E
17. ∀e:runEvents(pRun(S2;env;n2m;l2m)). (loc(e) = run-event-loc(e) ∈ Id)
18. run-cause(pRun(S2;env;n2m;l2m)) ∈ E ─→ (E?)
19. (C ∈ Cs)
⊢ sub-system(P.M[P];<[C], lg-nil()>;S2)
2
1. [M] : Type ─→ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ─→ pMsg(P.M[P])@i
4. C : component(P.M[P])@i
5. l2m : Id ─→ pMsg(P.M[P])@i
6. Cs : component(P.M[P]) List@i
7. <Cs, lg-nil()> ∈ System(P.M[P])
8. S2 : InitialSystem(P.M[P])@i
9. sub-system(P.M[P];<Cs, lg-nil()>;S2)@i
10. env : pEnvType(P.M[P])@i
11. ∀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))
12. pRun(S2;env;n2m;l2m) ∈ pRunType(P.M[P])
13. reliable-env(env; pRun(S2;env;n2m;l2m))@i
14. ∀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))?)))))
15. E ⊆r runEvents(pRun(S2;env;n2m;l2m))
16. runEvents(pRun(S2;env;n2m;l2m)) ⊆r E
17. ∀e:runEvents(pRun(S2;env;n2m;l2m)). (loc(e) = run-event-loc(e) ∈ Id)
18. run-cause(pRun(S2;env;n2m;l2m)) ∈ E ─→ (E?)
19. (C ∈ Cs)
20. sub-system(P.M[P];<[C], lg-nil()>;S2)
⊢ ∀e:E
∀p∈last(data-stream(snd(C);map(λe.info(e);before(e) @ [e]))).let y,c = p
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':E
((loc(e') = y ∈ Id)
∧ (e < e')
∧ (∃n:ℕ
∃nm:Id
(info(e')
= command-to-msg(c;n2m n;l2m nm)
∈ pMsg(P.M[P])))
∧ ((run-cause(pRun(S2;env;n2m;l2m)) e')
= (inl e)
∈ (E?))))
supposing loc(e) = (fst(C)) ∈ Id
Latex:
Latex:
1. [M] : Type {}\mrightarrow{} Type
2. Continuous+(P.M[P])
3. n2m : \mBbbN{} {}\mrightarrow{} pMsg(P.M[P])@i
4. C : component(P.M[P])@i
5. l2m : Id {}\mrightarrow{} pMsg(P.M[P])@i
6. Cs : component(P.M[P]) List@i
7. <Cs, lg-nil()> \mmember{} System(P.M[P])
8. S2 : InitialSystem(P.M[P])@i
9. sub-system(P.M[P];<Cs, lg-nil()>S2)@i
10. env : pEnvType(P.M[P])@i
11. \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)))
12. pRun(S2;env;n2m;l2m) \mmember{} pRunType(P.M[P])
13. reliable-env(env; pRun(S2;env;n2m;l2m))@i
14. \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)))))
15. E \msubseteq{}r runEvents(pRun(S2;env;n2m;l2m))
16. runEvents(pRun(S2;env;n2m;l2m)) \msubseteq{}r E
17. \mforall{}e:runEvents(pRun(S2;env;n2m;l2m)). (loc(e) = run-event-loc(e))
18. run-cause(pRun(S2;env;n2m;l2m)) \mmember{} E {}\mrightarrow{} (E?)
19. (C \mmember{} Cs)
\mvdash{} \mforall{}e:E
\mforall{}p\mmember{}last(data-stream(snd(C);map(\mlambda{}e.info(e);before(e) @ [e]))).
let y,c = p
in (com-kind(c) \mmember{} ``msg choose new``)
{}\mRightarrow{} (\mexists{}e':E
((loc(e') = y)
\mwedge{} (e < e')
\mwedge{} (\mexists{}n:\mBbbN{}. \mexists{}nm:Id. (info(e') = command-to-msg(c;n2m n;l2m nm)))
\mwedge{} ((run-cause(pRun(S2;env;n2m;l2m)) e') = (inl e))))
supposing loc(e) = (fst(C))
By
Latex:
Assert \mkleeneopen{}sub-system(P.M[P];<[C], lg-nil()>S2)\mkleeneclose{}\mcdot{}
Home
Index