Step
*
of Lemma
std-components-property
∀[M:Type ⟶ Type]
∀n2m:ℕ ⟶ pMsg(P.M[P]). ∀l2m:Id ⟶ pMsg(P.M[P]). ∀Cs:component(P.M[P]) List.
assuming(env,r.reliable-env(env; r))
<Cs, lg-nil()> |= es.∃cause:E ⟶ (E?)
(∀C∈Cs.∀e:E
let G = last(data-stream(snd(C);map(λe.info(e);≤loc(e)))) in
∀p∈G.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])))
∧ ((cause e') = (inl e) ∈ (E?))))
supposing loc(e) = (fst(C)) ∈ Id)
supposing Continuous+(P.M[P])
BY
{ (InstLemma `pRun-invariant2` []
THEN RepeatFor 4 ((ParallelLast' THENA Auto))
THEN Auto
THEN (Assert <Cs, lg-nil()> ∈ System(P.M[P]) BY
(Unfold `System` 0 THEN Auto))
THEN RepeatFor 3 ((D 0 THENA Auto))
THEN (InstHyp [⌜S2⌝;⌜env⌝] 5⋅ THENA Auto)
THEN Thin 5
THEN All (RepUR ``let``)
THEN (Assert pRun(S2;env;n2m;l2m) ∈ pRunType(P.M[P]) BY
Auto)
THEN (D 0 THENA Auto)
THEN ((InstLemma `reliable-env-property2` [⌜M⌝;⌜S2⌝;⌜n2m⌝;⌜l2m⌝;⌜env⌝]⋅ THENM (RepUR ``let`` -1 THEN D -1))
THENA Auto
)
THEN ((Assert (E ⊆r runEvents(pRun(S2;env;n2m;l2m))) ∧ (runEvents(pRun(S2;env;n2m;l2m)) ⊆r E) BY
(RepUR ``es-E run-eo mk-extended-eo mk-eo mk-eo-record`` 0 THEN Auto THEN D 0 THEN Auto))
THEN ((Assert ∀e:runEvents(pRun(S2;env;n2m;l2m)). (loc(e) = run-event-loc(e) ∈ Id) BY
(RepUR ``es-loc run-eo mk-extended-eo mk-eo mk-eo-record`` 0 THEN Auto))
THEN (All (Fold `runEO`)⋅
THEN All (Fold `stdEO`)
THEN Unfold `es-le-before` 0⋅
THEN Auto
THEN (Assert run-cause(pRun(S2;env;n2m;l2m)) ∈ E ⟶ (E?) BY
(RepUR ``es-E stdEO runEO run-eo mk-extended-eo mk-eo mk-eo-record`` 0 THEN Auto))
THEN (At ⌜Type⌝ (With ⌜run-cause(pRun(S2;env;n2m;l2m))⌝ (D 0))⋅ THENA Try (Trivial)))⋅
)⋅
)⋅) }
1
1. [M] : Type ⟶ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ⟶ pMsg(P.M[P])@i
4. l2m : Id ⟶ pMsg(P.M[P])@i
5. Cs : component(P.M[P]) List@i
6. <Cs, lg-nil()> ∈ System(P.M[P])
7. S2 : InitialSystem(P.M[P])@i
8. sub-system(P.M[P];<Cs, lg-nil()>;S2)@i
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?)
⊢ (∀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)
2
.....wf.....
1. M : Type ⟶ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ⟶ pMsg(P.M[P])@i
4. l2m : Id ⟶ pMsg(P.M[P])@i
5. Cs : component(P.M[P]) List@i
6. <Cs, lg-nil()> ∈ System(P.M[P])
7. S2 : InitialSystem(P.M[P])@i
8. sub-system(P.M[P];<Cs, lg-nil()>;S2)@i
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. cause : E ⟶ (E?)
⊢ (∀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])))
∧ ((cause e') = (inl e) ∈ (E?))))
supposing loc(e) = (fst(C)) ∈ Id) ∈ Type
Latex:
Latex:
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}n2m:\mBbbN{} {}\mrightarrow{} pMsg(P.M[P]). \mforall{}l2m:Id {}\mrightarrow{} pMsg(P.M[P]). \mforall{}Cs:component(P.M[P]) List.
assuming(env,r.reliable-env(env; r))
<Cs, lg-nil()> |= es.\mexists{}cause:E {}\mrightarrow{} (E?)
(\mforall{}C\mmember{}Cs.\mforall{}e:E
let G = last(data-stream(snd(C);map(\mlambda{}e.info(e);\mleq{}loc(e)))) in
\mforall{}p\mmember{}G.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{} ((cause e') = (inl e))))
supposing loc(e) = (fst(C)))
supposing Continuous+(P.M[P])
By
Latex:
(InstLemma `pRun-invariant2` []
THEN RepeatFor 4 ((ParallelLast' THENA Auto))
THEN Auto
THEN (Assert <Cs, lg-nil()> \mmember{} System(P.M[P]) BY
(Unfold `System` 0 THEN Auto))
THEN RepeatFor 3 ((D 0 THENA Auto))
THEN (InstHyp [\mkleeneopen{}S2\mkleeneclose{};\mkleeneopen{}env\mkleeneclose{}] 5\mcdot{} THENA Auto)
THEN Thin 5
THEN All (RepUR ``let``)
THEN (Assert pRun(S2;env;n2m;l2m) \mmember{} pRunType(P.M[P]) BY
Auto)
THEN (D 0 THENA Auto)
THEN ((InstLemma `reliable-env-property2` [\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}S2\mkleeneclose{};\mkleeneopen{}n2m\mkleeneclose{};\mkleeneopen{}l2m\mkleeneclose{};\mkleeneopen{}env\mkleeneclose{}]\mcdot{}
THENM (RepUR ``let`` -1 THEN D -1)
)
THENA Auto
)
THEN
((Assert (E \msubseteq{}r runEvents(pRun(S2;env;n2m;l2m))) \mwedge{} (runEvents(pRun(S2;env;n2m;l2m)) \msubseteq{}r E) BY
(RepUR ``es-E run-eo mk-extended-eo mk-eo mk-eo-record`` 0 THEN Auto THEN D 0 THEN Auto))
THEN ((Assert \mforall{}e:runEvents(pRun(S2;env;n2m;l2m)). (loc(e) = run-event-loc(e)) BY
(RepUR ``es-loc run-eo mk-extended-eo mk-eo mk-eo-record`` 0 THEN Auto))
THEN (All (Fold `runEO`)\mcdot{}
THEN All (Fold `stdEO`)
THEN Unfold `es-le-before` 0\mcdot{}
THEN Auto
THEN (Assert run-cause(pRun(S2;env;n2m;l2m)) \mmember{} E {}\mrightarrow{} (E?) BY
(RepUR ``es-E stdEO runEO run-eo mk-extended-eo mk-eo mk-eo-record`` 0
THEN Auto
))
THEN (At \mkleeneopen{}Type\mkleeneclose{} (With \mkleeneopen{}run-cause(pRun(S2;env;n2m;l2m))\mkleeneclose{} (D 0))\mcdot{} THENA Try (Trivial)))\mcdot{}
)\mcdot{}
)\mcdot{})
Home
Index