---

Step * 2 1 of Lemma pRun-intransit-invariant


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. Cs0 : component(P.M[P]) List@i
6. G0 : LabeledDAG(pInTransit(P.M[P]))@i
7. env : pEnvType(P.M[P])@i
8. t : ℕ@i
9. ∀x:pInTransit(P.M[P]). ∀t:ℤ.
     (((fst(fst(x))) ≤ t) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id))) ∈ ℙ)
10. t1 : ℕ@i
11. S : System(P.M[P])@i
12. let Cs,G = S 
    in ∀x∈G.((fst(fst(x))) ≤ t1) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))@i
13. e1 : pEnvType(P.M[P])@i
14. v : ℕ × ℕ × Id@i
15. (e1 (t1 + 1) pRun(<Cs0, G0>;e1;n2m;l2m)) = v ∈ (ℕ × ℕ × Id)@i
⊢ let n,m,nm = v in 
let Cs,G = snd(do-chosen-command(n2m;l2m;t1 + 1;S;n;m;nm)) 
in ∀x∈G.((fst(fst(x))) ≤ (t1 + 1)) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))
BY
{ (RepeatFor 2 (D (-2)) THEN Reduce 0) }

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. Cs0 : component(P.M[P]) List@i
6. G0 : LabeledDAG(pInTransit(P.M[P]))@i
7. env : pEnvType(P.M[P])@i
8. t : ℕ@i
9. ∀x:pInTransit(P.M[P]). ∀t:ℤ.
     (((fst(fst(x))) ≤ t) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id))) ∈ ℙ)
10. t1 : ℕ@i
11. S : System(P.M[P])@i
12. let Cs,G = S 
    in ∀x∈G.((fst(fst(x))) ≤ t1) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))@i
13. e1 : pEnvType(P.M[P])@i
14. v1 : ℕ@i
15. v3 : ℕ@i
16. v4 : Id@i
17. (e1 (t1 + 1) pRun(<Cs0, G0>;e1;n2m;l2m)) = <v1, v3, v4> ∈ (ℕ × ℕ × Id)@i
⊢ let Cs,G = snd(do-chosen-command(n2m;l2m;t1 + 1;S;v1;v3;v4)) 
  in ∀x∈G.((fst(fst(x))) ≤ (t1 + 1)) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))

---

Latex:

---

Latex:

1.  [M]  :  Type  {}\mrightarrow{}  Type
2.  Continuous+(P.M[P])
3.  n2m  :  \mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])@i
4.  l2m  :  Id  {}\mrightarrow{}  pMsg(P.M[P])@i
5.  Cs0  :  component(P.M[P])  List@i
6.  G0  :  LabeledDAG(pInTransit(P.M[P]))@i
7.  env  :  pEnvType(P.M[P])@i
8.  t  :  \mBbbN{}@i
9.  \mforall{}x:pInTransit(P.M[P]).  \mforall{}t:\mBbbZ{}.
          (((fst(fst(x)))  \mleq{}  t)  \mvee{}  (\mexists{}m:\mBbbN{}lg-size(G0).  ((fst(x))  =  (fst(lg-label(G0;m)))))  \mmember{}  \mBbbP{})
10.  t1  :  \mBbbN{}@i
11.  S  :  System(P.M[P])@i
12.  let  Cs,G  =  S 
        in  \mforall{}x\mmember{}G.((fst(fst(x)))  \mleq{}  t1)  \mvee{}  (\mexists{}m:\mBbbN{}lg-size(G0).  ((fst(x))  =  (fst(lg-label(G0;m)))))@i
13.  e1  :  pEnvType(P.M[P])@i
14.  v  :  \mBbbN{}  \mtimes{}  \mBbbN{}  \mtimes{}  Id@i
15.  (e1  (t1  +  1)  pRun(<Cs0,  G0>e1;n2m;l2m))  =  v@i
\mvdash{}  let  n,m,nm  =  v  in 
let  Cs,G  =  snd(do-chosen-command(n2m;l2m;t1  +  1;S;n;m;nm)) 
in  \mforall{}x\mmember{}G.((fst(fst(x)))  \mleq{}  (t1  +  1))  \mvee{}  (\mexists{}m:\mBbbN{}lg-size(G0).  ((fst(x))  =  (fst(lg-label(G0;m)))))


By

---

Latex:
(RepeatFor  2  (D  (-2))  THEN  Reduce  0)

---

Home Index