Step
*
1
1
1
1
1
2
1
1
2
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(lg-label(snd(snd((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);lg-label(snd(snd((...
t)));n))
∈ (ℤ × Id × pMsg(P.M[P])))
∧ (run-event-loc(e) = (fst(snd(lg-label(snd(snd((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(lg-label(snd(snd((pRun(S0;env;n2m;l2m) t)));n)))) ∈ ``msg choose new``)@i
14. t' : ℕ
15. t < t'
16. (fst((env t' pRun(S0;env;n2m;l2m)))) ≤ n
17. ↑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'))
18. ∀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'
19. k : ℤ@i
20. [%20] : 0 < k@i
21. t + k < t'@i
22. n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) (t + (k - 1))))))
∧ (∀x:ℕ
((x ≤ n)
⇒ (lg-label(snd(snd((pRun(S0;env;n2m;l2m) (t + (k - 1)))));x)
= lg-label(snd(snd((pRun(S0;env;n2m;l2m) t)));x)
∈ pInTransit(P.M[P]))))@i
⊢ (¬(t < t + k
c∧ (((fst((env (t + k) pRun(S0;env;n2m;l2m)))) ≤ n)
∧ ↑lg-is-source(run-intransit(pRun(S0;env;n2m;l2m);t + k);fst((env (t + k) pRun(S0;env;n2m;l2m))))
supposing 0 < lg-size(run-intransit(pRun(S0;env;n2m;l2m);t + k)))))
⇒ (n < lg-size(snd(snd(let n,m,nm = env (t + k) pRun(S0;env;n2m;l2m) in
do-chosen-command(n2m;l2m;t + k;snd((pRun(S0;env;n2m;l2m) (t + (k - 1))));n;m;nm))))
∧ (∀x:ℕ
((x ≤ n)
⇒ (lg-label(snd(snd(let n,m,nm = env (t + k) pRun(S0;env;n2m;l2m) in
do-chosen-command(n2m;l2m;t + k;snd((pRun(S0;env;n2m;l2m) (t + (k - 1))));n;m;nm)));x)
= lg-label(snd(snd((pRun(S0;env;n2m;l2m) t)));x)
∈ pInTransit(P.M[P])))))
BY
{ (Thin 7
THEN (RepUR ``run-intransit run-system`` 0 THEN Subst' (t + k) - 1 ~ t + (k - 1) 0 THEN Try (Complete (Auto')))
THEN ((MoveToConcl (-1) THEN GenConclAtAddr [1;1;2;1;1]) THENA Auto')
THEN D -2) }
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. reliable-env(env; pRun(S0;env;n2m;l2m))@i
8. n : ℕ@i
9. ∀n1:ℕn. ∀t:ℕ.
((run-command-node(pRun(S0;env;n2m;l2m);t;n1)
∧ (com-kind(snd(snd(lg-label(snd(snd((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);lg-label(snd(snd((...
t)));n))
∈ (ℤ × Id × pMsg(P.M[P])))
∧ (run-event-loc(e) = (fst(snd(lg-label(snd(snd((pRun(S0;env;n2m;l2m) t)));n)))) ∈ Id)))@i
10. t : ℕ@i
11. run-command-node(pRun(S0;env;n2m;l2m);t;n)@i
12. (com-kind(snd(snd(lg-label(snd(snd((pRun(S0;env;n2m;l2m) t)));n)))) ∈ ``msg choose new``)@i
13. t' : ℕ
14. t < t'
15. (fst((env t' pRun(S0;env;n2m;l2m)))) ≤ n
16. ↑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'))
17. ∀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'
18. k : ℤ@i
19. [%20] : 0 < k@i
20. t + k < t'@i
21. v1 : component(P.M[P]) List@i
22. v2 : LabeledDAG(pInTransit(P.M[P]))@i
23. (snd((pRun(S0;env;n2m;l2m) (t + (k - 1))))) = <v1, v2> ∈ System(P.M[P])@i
⊢ (n < lg-size(snd(<v1, v2>)) ∧ (∀x:ℕ. ((x ≤ n) ⇒ (lg-label(snd(<v1, v2>);x) = lg-label(snd(snd((pRun(S0;env;n2m;l2m) t\000C)));x) ∈ pInTransit(P.M[P])))))
⇒ (¬(t < t + k
c∧ (((fst((env (t + k) pRun(S0;env;n2m;l2m)))) ≤ n)
∧ ↑lg-is-source(snd(<v1, v2>);fst((env (t + k) pRun(S0;env;n2m;l2m)))) supposing 0 < lg-size(snd(<v1, v2>)))))
⇒ (n < lg-size(snd(snd(let n,m,nm = env (t + k) pRun(S0;env;n2m;l2m) in
do-chosen-command(n2m;l2m;t + k;<v1, v2>;n;m;nm))))
∧ (∀x:ℕ
((x ≤ n)
⇒ (lg-label(snd(snd(let n,m,nm = env (t + k) pRun(S0;env;n2m;l2m) in
do-chosen-command(n2m;l2m;t + k;<v1, v2>;n;m;nm)));x)
= lg-label(snd(snd((pRun(S0;env;n2m;l2m) t)));x)
∈ pInTransit(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(lg-label(snd(snd((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(lg-label(snd(snd((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(lg-label(snd(snd((pRun(S0;env;n2m;l2m) t)));n)))) \mmember{} ``msg choose new``)@i
14. t' : \mBbbN{}
15. t < t'
16. (fst((env t' pRun(S0;env;n2m;l2m)))) \mleq{} n
17. \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'))
18. \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'
19. k : \mBbbZ{}@i
20. [\%20] : 0 < k@i
21. t + k < t'@i
22. n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) (t + (k - 1))))))
\mwedge{} (\mforall{}x:\mBbbN{}
((x \mleq{} n)
{}\mRightarrow{} (lg-label(snd(snd((pRun(S0;env;n2m;l2m) (t + (k - 1)))));x)
= lg-label(snd(snd((pRun(S0;env;n2m;l2m) t)));x))))@i
\mvdash{} (\mneg{}(t < t + k
c\mwedge{} (((fst((env (t + k) pRun(S0;env;n2m;l2m)))) \mleq{} n)
\mwedge{} \muparrow{}lg-is-source(run-intransit(pRun(S0;env;n2m;l2m);t + k);fst((env (t + k)
pRun(S0;env;n2m;l2m))))
supposing 0 < lg-size(run-intransit(pRun(S0;env;n2m;l2m);t + k)))))
{}\mRightarrow{} (n < lg-size(snd(snd(let n,m,nm = env (t + k) pRun(S0;env;n2m;l2m) in
do-chosen-command(n2m;l2m;t + k;snd((pRun(S0;env;n2m;l2m) (t + (k - 1))));n;m;nm))))
\mwedge{} (\mforall{}x:\mBbbN{}
((x \mleq{} n)
{}\mRightarrow{} (lg-label(snd(snd(let n,m,nm = env (t + k) pRun(S0;env;n2m;l2m) in
do-chosen-command(n2m;l2m;t + k;snd((pRun(S0;env;n2m;l2m) (t + (k - 1))));n;m;nm)));x)
= lg-label(snd(snd((pRun(S0;env;n2m;l2m) t)));x)))))
By
Latex:
(Thin 7
THEN (RepUR ``run-intransit run-system`` 0
THEN Subst' (t + k) - 1 \msim{} t + (k - 1) 0
THEN Try (Complete (Auto')))
THEN ((MoveToConcl (-1) THEN GenConclAtAddr [1;1;2;1;1]) THENA Auto')
THEN D -2)
Home
Index