Step
*
1
1
1
2
2
2
1
1
of Lemma
reliable-env-property
1. M : Type ⟶ Type
2. Continuous+(P.M[P])
3. S0 : 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(S0;env;n2m;l2m) ∈ pRunType(P.M[P])
8. reliable-env(env; pRun(S0;env;n2m;l2m))@i
9. n : ℕ@i
10. ∀n1:ℕn. ∀t:ℕ.
((run-command-node(pRun(S0;env;n2m;l2m);t;n1)
∧ (com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;n1)))) ∈ ``msg choose new``))
⇒ (∃e:runEvents(pRun(S0;env;n2m;l2m))
let t,n = <t, n1>
in (run-info(pRun(S0;env;n2m;l2m);e)
= intransit-to-info(n2m;l2m;pRun(S0;env;n2m;l2m);env;run-event-step(e);run-command(...;t;n))
∈ (ℤ × Id × pMsg(P.M[P])))
∧ (run-event-loc(e) = (fst(snd(run-command(pRun(S0;env;n2m;l2m);t;n)))) ∈ Id)))@i
11. t : ℕ@i
12. run-command-node(pRun(S0;env;n2m;l2m);t;n)@i
13. (com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;n)))) ∈ ``msg choose new``)@i
14. t' : ℕ
15. t < t'
16. ∀i:ℕ
¬(t < i
c∧ (((fst((env i pRun(S0;env;n2m;l2m)))) ≤ n)
∧ ↑lg-is-source(run-intransit(pRun(S0;env;n2m;l2m);i);fst((env i pRun(S0;env;n2m;l2m))))
supposing 0 < lg-size(run-intransit(pRun(S0;env;n2m;l2m);i))))
supposing i < t'
17. ∀t2:ℕ
((t ≤ t2)
⇒ t2 < t'
⇒ (n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) t2))))
∧ (∀x:ℕ
((x ≤ n)
⇒ (run-command(pRun(S0;env;n2m;l2m);t2;x)
= run-command(pRun(S0;env;n2m;l2m);t;x)
∈ pInTransit(P.M[P]))))))
18. n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) (t' - 1)))))
19. ∀x:ℕ
((x ≤ n)
⇒ (run-command(pRun(S0;env;n2m;l2m);t' - 1;x) = run-command(pRun(S0;env;n2m;l2m);t;x) ∈ pInTransit(P.M[P])))
20. run-command(pRun(S0;env;n2m;l2m);t' - 1;n) = run-command(pRun(S0;env;n2m;l2m);t;n) ∈ pInTransit(P.M[P])
⊢ ((fst((env t' pRun(S0;env;n2m;l2m)))) ≤ n)
⇒ ↑lg-is-source(run-intransit(pRun(S0;env;n2m;l2m);t');fst((env t' pRun(S0;env;n2m;l2m))))
supposing 0 < lg-size(run-intransit(pRun(S0;env;n2m;l2m);t'))
⇒ (¬fst((env t' pRun(S0;env;n2m;l2m))) < n)
⇒ (run-info(pRun(S0;env;n2m;l2m);<t', fst(snd(run-command(pRun(S0;env;n2m;l2m);t;n)))>)
= intransit-to-info(n2m;l2m;pRun(S0;env;n2m;l2m);env;run-event-step(<t'
, fst(snd(run-command(pRun(S0;env;n2m;l2m);t;n)))
>);run-command(pRun(S0;env;n2m;l2m);t;n))
∈ (ℤ × Id × pMsg(P.M[P])))
BY
{ (RepUR ``run-event-step run-info intransit-to-info`` 0
THEN (RW (AddrC [2;2;2;2] (RecUnfoldC `pRun`)) 0
THEN Reduce 0
THEN OldAutoSplit
THEN (GenConclAtAddr [1;1;1] THENA (Auto THEN DoSubsume THEN Auto))
THEN RepeatFor 2 (D (-2))
THEN Reduce 0
THEN skip{(MoveToConcl 13⋅
THEN MoveToConcl (-6)
THEN MoveToConcl 17 THEN RepUR ``run-intransit run-system run-command`` 0
THEN (GenConclAtAddr [1;2;1;1] THENA (Auto THEN DoSubsume THEN Auto)))})⋅
)⋅ }
1
1. M : Type ⟶ Type
2. Continuous+(P.M[P])
3. S0 : 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(S0;env;n2m;l2m) ∈ pRunType(P.M[P])
8. reliable-env(env; pRun(S0;env;n2m;l2m))@i
9. n : ℕ@i
10. ∀n1:ℕn. ∀t:ℕ.
((run-command-node(pRun(S0;env;n2m;l2m);t;n1)
∧ (com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;n1)))) ∈ ``msg choose new``))
⇒ (∃e:runEvents(pRun(S0;env;n2m;l2m))
let t,n = <t, n1>
in (run-info(pRun(S0;env;n2m;l2m);e)
= intransit-to-info(n2m;l2m;pRun(S0;env;n2m;l2m);env;run-event-step(e);run-command(...;t;n))
∈ (ℤ × Id × pMsg(P.M[P])))
∧ (run-event-loc(e) = (fst(snd(run-command(pRun(S0;env;n2m;l2m);t;n)))) ∈ Id)))@i
11. t : ℕ@i
12. run-command-node(pRun(S0;env;n2m;l2m);t;n)@i
13. (com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;n)))) ∈ ``msg choose new``)@i
14. t' : ℕ
15. t < t'
16. ∀i:ℕ
¬(t < i
c∧ (((fst((env i pRun(S0;env;n2m;l2m)))) ≤ n)
∧ ↑lg-is-source(run-intransit(pRun(S0;env;n2m;l2m);i);fst((env i pRun(S0;env;n2m;l2m))))
supposing 0 < lg-size(run-intransit(pRun(S0;env;n2m;l2m);i))))
supposing i < t'
17. ∀t2:ℕ
((t ≤ t2)
⇒ t2 < t'
⇒ (n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) t2))))
∧ (∀x:ℕ
((x ≤ n)
⇒ (run-command(pRun(S0;env;n2m;l2m);t2;x)
= run-command(pRun(S0;env;n2m;l2m);t;x)
∈ pInTransit(P.M[P]))))))
18. n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) (t' - 1)))))
19. ∀x:ℕ
((x ≤ n)
⇒ (run-command(pRun(S0;env;n2m;l2m);t' - 1;x) = run-command(pRun(S0;env;n2m;l2m);t;x) ∈ pInTransit(P.M[P])))
20. run-command(pRun(S0;env;n2m;l2m);t' - 1;n) = run-command(pRun(S0;env;n2m;l2m);t;n) ∈ pInTransit(P.M[P])
21. ¬(t' = 0 ∈ ℤ)
22. v1 : ℕ@i
23. v3 : ℕ@i
24. v4 : Id@i
25. (env t' pRun(S0;env;n2m;l2m)) = <v1, v3, v4> ∈ (ℕ × ℕ × Id)@i
⊢ (v1 ≤ n)
⇒ ↑lg-is-source(run-intransit(pRun(S0;env;n2m;l2m);t');v1)
supposing 0 < lg-size(run-intransit(pRun(S0;env;n2m;l2m);t'))
⇒ (¬v1 < n)
⇒ (let info,S = do-chosen-command(n2m;l2m;t';snd((pRun(S0;env;n2m;l2m) (t' - 1)));v1;v3;v4)
in let ev,z,m = outl(info) in
<ev, m>
= let ev,x,c = run-command(pRun(S0;env;n2m;l2m);t;n) in
<ev, command-to-msg(c;n2m v3;l2m v4)>
∈ (ℤ × Id × pMsg(P.M[P])))
Latex:
Latex:
1. M : Type {}\mrightarrow{} Type
2. Continuous+(P.M[P])
3. S0 : 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(S0;env;n2m;l2m) \mmember{} pRunType(P.M[P])
8. reliable-env(env; pRun(S0;env;n2m;l2m))@i
9. n : \mBbbN{}@i
10. \mforall{}n1:\mBbbN{}n. \mforall{}t:\mBbbN{}.
((run-command-node(pRun(S0;env;n2m;l2m);t;n1)
\mwedge{} (com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;n1)))) \mmember{} ``msg choose new``))
{}\mRightarrow{} (\mexists{}e:runEvents(pRun(S0;env;n2m;l2m))
let t,n = <t, n1>
in (run-info(pRun(S0;env;n2m;l2m);e)
= intransit-to-info(n2m;l2m;pRun(S0;env;n2m;l2m);env;run-event-step(e);...))
\mwedge{} (run-event-loc(e) = (fst(snd(run-command(pRun(S0;env;n2m;l2m);t;n)))))))@i
11. t : \mBbbN{}@i
12. run-command-node(pRun(S0;env;n2m;l2m);t;n)@i
13. (com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;n)))) \mmember{} ``msg choose new``)@i
14. t' : \mBbbN{}
15. t < t'
16. \mforall{}i:\mBbbN{}
\mneg{}(t < i
c\mwedge{} (((fst((env i pRun(S0;env;n2m;l2m)))) \mleq{} n)
\mwedge{} \muparrow{}lg-is-source(run-intransit(pRun(S0;env;n2m;l2m);i);fst((env i pRun(S0;env;n2m;l2m))))
supposing 0 < lg-size(run-intransit(pRun(S0;env;n2m;l2m);i))))
supposing i < t'
17. \mforall{}t2:\mBbbN{}
((t \mleq{} t2)
{}\mRightarrow{} t2 < t'
{}\mRightarrow{} (n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) t2))))
\mwedge{} (\mforall{}x:\mBbbN{}
((x \mleq{} n)
{}\mRightarrow{} (run-command(pRun(S0;env;n2m;l2m);t2;x)
= run-command(pRun(S0;env;n2m;l2m);t;x))))))
18. n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) (t' - 1)))))
19. \mforall{}x:\mBbbN{}
((x \mleq{} n)
{}\mRightarrow{} (run-command(pRun(S0;env;n2m;l2m);t' - 1;x) = run-command(pRun(S0;env;n2m;l2m);t;x)))
20. run-command(pRun(S0;env;n2m;l2m);t' - 1;n) = run-command(pRun(S0;env;n2m;l2m);t;n)
\mvdash{} ((fst((env t' pRun(S0;env;n2m;l2m)))) \mleq{} n)
{}\mRightarrow{} \muparrow{}lg-is-source(run-intransit(pRun(S0;env;n2m;l2m);t');fst((env t' pRun(S0;env;n2m;l2m))))
supposing 0 < lg-size(run-intransit(pRun(S0;env;n2m;l2m);t'))
{}\mRightarrow{} (\mneg{}fst((env t' pRun(S0;env;n2m;l2m))) < n)
{}\mRightarrow{} (run-info(pRun(S0;env;n2m;l2m);<t', fst(snd(run-command(pRun(S0;env;n2m;l2m);t;n)))>)
= intransit-to-info(n2m;l2m;pRun(S0;env;n2m;l2m);env;run-event-step(<t'
, fst(snd(...))
>);run-command(pRun(S0;env;n2\000Cm;l2m);t;n)))
By
Latex:
(RepUR ``run-event-step run-info intransit-to-info`` 0
THEN (RW (AddrC [2;2;2;2] (RecUnfoldC `pRun`)) 0
THEN Reduce 0
THEN OldAutoSplit
THEN (GenConclAtAddr [1;1;1] THENA (Auto THEN DoSubsume THEN Auto))
THEN RepeatFor 2 (D (-2))
THEN Reduce 0
THEN skip\{(MoveToConcl 13\mcdot{}
THEN MoveToConcl (-6)
THEN MoveToConcl 17 THEN RepUR ``run-intransit run-system run-command`` 0
THEN (GenConclAtAddr [1;2;1;1] THENA (Auto THEN DoSubsume THEN Auto)))\})\mcdot{}
)\mcdot{}
Home
Index