---

Step * 2 1 1 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. C : component(P.M[P]) List@i
12. G : LabeledDAG(pInTransit(P.M[P]))@i
13. ∀x∈G.((fst(fst(x))) ≤ t1) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))@i
14. e1 : pEnvType(P.M[P])@i
15. v1 : ℕ@i
16. v3 : ℕ@i
17. v4 : Id@i
18. (e1 (t1 + 1) pRun(<Cs0, G0>;e1;n2m;l2m)) = <v1, v3, v4> ∈ (ℕ × ℕ × Id)@i
19. ↑lg-is-source(G;v1)
⊢ let Cs,G = snd(let ev,x,c = lg-label(G;v1) in 
  let G' = lg-remove(G;v1) in
      if com-kind(c) =a "msg" then let ms = comm-msg(c) in <inl <ev, x, ms>, deliver-msg(t1 + 1;ms;x;C;G')>
      if com-kind(c) =a "create" then let P = comm-create(c) in <inr ⋅ , create-component(t1 + 1;P;x;C;G')>
      if com-kind(c) =a "choose" then let ms = n2m v3 in <inl <ev, x, ms>, deliver-msg(t1 + 1;ms;x;C;G')>
      if com-kind(c) =a "new" then let ms = l2m v4 in <inl <ev, x, ms>, deliver-msg(t1 + 1;ms;x;C;G')>
      else <inr ⋅ , C, G'>
      fi ) 
  in ∀x∈G.((fst(fst(x))) ≤ (t1 + 1)) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))
BY
{ (RepUR ``lg-is-source`` (-1)
   THEN (SplitOnHypITE -1  THENA Auto)
   THEN Reduce (-2)
   THEN Auto
   THEN (GenConclAtAddrType ⌈pInTransit(P.M[P])⌉ [1;1;1]⋅ THENA Auto)
   THEN RepeatFor 2 (D -2)
   THEN Reduce 0
   THEN (GenConclAtAddrType ⌈LabeledDAG(pInTransit(P.M[P]))⌉ [1;1;1]⋅ THENA Auto)
   THEN RenameVar `H' (-2)
   THEN RepUR ``let`` 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. C : component(P.M[P]) List@i
12. G : LabeledDAG(pInTransit(P.M[P]))@i
13. ∀x∈G.((fst(fst(x))) ≤ t1) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))@i
14. e1 : pEnvType(P.M[P])@i
15. v1 : ℕ@i
16. v3 : ℕ@i
17. v4 : Id@i
18. (e1 (t1 + 1) pRun(<Cs0, G0>;e1;n2m;l2m)) = <v1, v3, v4> ∈ (ℕ × ℕ × Id)@i
19. ↑null(lg-in-edges(G;v1))
20. v1 < lg-size(G)
21. v5 : ℤ × Id@i
22. v7 : Id@i
23. v8 : pCom(P.M[P])@i
24. lg-label(G;v1) = <v5, v7, v8> ∈ pInTransit(P.M[P])@i
25. H : LabeledDAG(pInTransit(P.M[P]))@i
26. lg-remove(G;v1) = H ∈ LabeledDAG(pInTransit(P.M[P]))@i
⊢ let Cs,G = snd(if com-kind(v8) =a "msg" then <inl <v5, v7, comm-msg(v8)>, deliver-msg(t1 + 1;comm-msg(v8);v7;C;H)>
  if com-kind(v8) =a "create" then <inr ⋅ , create-component(t1 + 1;comm-create(v8);v7;C;H)>
  if com-kind(v8) =a "choose" then <inl <v5, v7, n2m v3>, deliver-msg(t1 + 1;n2m v3;v7;C;H)>
  if com-kind(v8) =a "new" then <inl <v5, v7, l2m v4>, deliver-msg(t1 + 1;l2m v4;v7;C;H)>
  else <inr ⋅ , C, H>
  fi ) 
  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.  C  :  component(P.M[P])  List@i
12.  G  :  LabeledDAG(pInTransit(P.M[P]))@i
13.  \mforall{}x\mmember{}G.((fst(fst(x)))  \mleq{}  t1)  \mvee{}  (\mexists{}m:\mBbbN{}lg-size(G0).  ((fst(x))  =  (fst(lg-label(G0;m)))))@i
14.  e1  :  pEnvType(P.M[P])@i
15.  v1  :  \mBbbN{}@i
16.  v3  :  \mBbbN{}@i
17.  v4  :  Id@i
18.  (e1  (t1  +  1)  pRun(<Cs0,  G0>e1;n2m;l2m))  =  <v1,  v3,  v4>@i
19.  \muparrow{}lg-is-source(G;v1)
\mvdash{}  let  Cs,G  =  snd(let  ev,x,c  =  lg-label(G;v1)  in 
    let  G'  =  lg-remove(G;v1)  in
            if  com-kind(c)  =a  "msg"
                then  let  ms  =  comm-msg(c)  in
                                  <inl  <ev,  x,  ms>,  deliver-msg(t1  +  1;ms;x;C;G')>
            if  com-kind(c)  =a  "create"
                then  let  P  =  comm-create(c)  in
                                  <inr  \mcdot{}  ,  create-component(t1  +  1;P;x;C;G')>
            if  com-kind(c)  =a  "choose"
                then  let  ms  =  n2m  v3  in
                                  <inl  <ev,  x,  ms>,  deliver-msg(t1  +  1;ms;x;C;G')>
            if  com-kind(c)  =a  "new"  then  let  ms  =  l2m  v4  in  <inl  <ev,  x,  ms>,  deliver-msg(t1  +  1;ms;x;C;G'\000C)>
            else  <inr  \mcdot{}  ,  C,  G'>
            fi  ) 
    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:
(RepUR  ``lg-is-source``  (-1)
  THEN  (SplitOnHypITE  -1    THENA  Auto)
  THEN  Reduce  (-2)
  THEN  Auto
  THEN  (GenConclAtAddrType  \mkleeneopen{}pInTransit(P.M[P])\mkleeneclose{}  [1;1;1]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  -2)
  THEN  Reduce  0
  THEN  (GenConclAtAddrType  \mkleeneopen{}LabeledDAG(pInTransit(P.M[P]))\mkleeneclose{}  [1;1;1]\mcdot{}  THENA  Auto)
  THEN  RenameVar  `H'  (-2)
  THEN  RepUR  ``let``  0)\mcdot{}

---

Home Index