---

Step * 1 1 of Lemma pRun-invariant1


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. S1 : component(P.M[P]) List@i
6. S2 : LabeledDAG(pInTransit(P.M[P]))@i
7. env : pEnvType(P.M[P])@i
8. ∀t:ℕ
     let info,Cs,G = pRun(<S1, S2>;env;n2m;l2m) t in 
     ∀x∈G.((fst(fst(x))) ≤ t) ∨ (∃m:ℕlg-size(S2). ((fst(x)) = (fst(lg-label(S2;m))) ∈ (ℤ × Id)))
9. <S1, S2> ∈ System(P.M[P])
10. t : ℕ@i
11. x : Id@i
12. ↑is-run-event(pRun(<S1, S2>;env;n2m;l2m);t;x)
⊢ fst(fst(run-info(pRun(<S1, S2>;env;n2m;l2m);<t, x>))) < t ∨ (∃m:ℕlg-size(S2). ((fst(run-info(pRun(<S1, S2>;env;n2m;l2m\000C);<t, x>))) = (fst(lg-label(S2;m))) ∈ (ℤ × Id)))
BY
{ (MoveToConcl (-1)⋅
   THEN RepUR ``run-info`` 0
   THEN RecUnfold `pRun` 0
   THEN RepUR ``let is-run-event do-chosen-command`` 0
   THEN AutoSplit
   THEN RepUR ``bfalse`` 0
   THEN Try (Complete (Auto))
   THEN (GenConclAtAddr [1;1;1;1] THENM (RepeatFor 2 (D -2) THEN Reduce 0))
   THEN (GenConclAtAddr [1;1;1;1]⋅
   THENM (D -2
          THEN Reduce 0
          THEN AutoSplit
          THEN Try ((RepUR ``bfalse`` 0 THEN Complete (Auto)))
          THEN RepUR ``lg-is-source`` -1
          THEN (SplitOnHypITE -1  THENA Auto)
          THEN Try ((All Reduce THEN Trivial))
          THEN (GenConclAtAddrType ⌈pInTransit(P.M[P])⌉ [1;1;1;1]⋅ THENA Auto)
          THEN 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. S1 : component(P.M[P]) List@i
6. S2 : LabeledDAG(pInTransit(P.M[P]))@i
7. env : pEnvType(P.M[P])@i
8. ∀t:ℕ
     let info,Cs,G = pRun(<S1, S2>;env;n2m;l2m) t in 
     ∀x∈G.((fst(fst(x))) ≤ t) ∨ (∃m:ℕlg-size(S2). ((fst(x)) = (fst(lg-label(S2;m))) ∈ (ℤ × Id)))
9. <S1, S2> ∈ System(P.M[P])
10. t : {1...}
11. x : Id@i
12. v1 : ℕ@i
13. v3 : ℕ@i
14. v4 : Id@i
15. (env t pRun(<S1, S2>;env;n2m;l2m)) = <v1, v3, v4> ∈ (ℕ × ℕ × Id)@i
16. v5 : component(P.M[P]) List@i
17. v6 : LabeledDAG(pInTransit(P.M[P]))@i
18. (snd((pRun(<S1, S2>;env;n2m;l2m) (t - 1)))) = <v5, v6> ∈ System(P.M[P])@i
19. ↑null(lg-in-edges(v6;v1))
20. v1 < lg-size(v6)
21. v7 : ℤ × Id@i
22. v9 : Id@i
23. v10 : pCom(P.M[P])@i
24. lg-label(v6;v1) = <v7, v9, v10> ∈ pInTransit(P.M[P])@i
⊢ (↑let info,S = if com-kind(v10) =a "msg"
                   then <inl <v7, v9, comm-msg(v10)>, deliver-msg(t;comm-msg(v10);v9;v5;lg-remove(v6;v1))>
    if com-kind(v10) =a "create" then <inr ⋅ , create-component(t;comm-create(v10);v9;v5;lg-remove(v6;v1))>
    if com-kind(v10) =a "choose" then <inl <v7, v9, n2m v3>, deliver-msg(t;n2m v3;v9;v5;lg-remove(v6;v1))>
    if com-kind(v10) =a "new" then <inl <v7, v9, l2m v4>, deliver-msg(t;l2m v4;v9;v5;lg-remove(v6;v1))>
    else <inr ⋅ , v5, lg-remove(v6;v1)>
    fi  
    in isl(info) ∧b let ev,z,m = outl(info) in x = z)
⇒ (fst(fst(let info,S = if com-kind(v10) =a "msg"
                           then <inl <v7, v9, comm-msg(v10)>, deliver-msg(t;comm-msg(v10);v9;v5;lg-remove(v6;v1))>
            if com-kind(v10) =a "create" then <inr ⋅ , create-component(t;comm-create(v10);v9;v5;lg-remove(v6;v1))>
            if com-kind(v10) =a "choose" then <inl <v7, v9, n2m v3>, deliver-msg(t;n2m v3;v9;v5;lg-remove(v6;v1))>
            if com-kind(v10) =a "new" then <inl <v7, v9, l2m v4>, deliver-msg(t;l2m v4;v9;v5;lg-remove(v6;v1))>
            else <inr ⋅ , v5, lg-remove(v6;v1)>
            fi  
            in let ev,z,m = outl(info) in 
               <ev, m>)) < t
   ∨ (∃m:ℕlg-size(S2)
       ((fst(let info,S = if com-kind(v10) =a "msg"
                            then <inl <v7, v9, comm-msg(v10)>, deliver-msg(t;comm-msg(v10);v9;v5;lg-remove(v6;v1))>
             if com-kind(v10) =a "create" then <inr ⋅ , create-component(t;comm-create(v10);v9;v5;lg-remove(v6;v1))>
             if com-kind(v10) =a "choose" then <inl <v7, v9, n2m v3>, deliver-msg(t;n2m v3;v9;v5;lg-remove(v6;v1))>
             if com-kind(v10) =a "new" then <inl <v7, v9, l2m v4>, deliver-msg(t;l2m v4;v9;v5;lg-remove(v6;v1))>
             else <inr ⋅ , v5, lg-remove(v6;v1)>
             fi  
             in let ev,z,m = outl(info) in 
                <ev, m>))
       = (fst(lg-label(S2;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.  S1  :  component(P.M[P])  List@i
6.  S2  :  LabeledDAG(pInTransit(P.M[P]))@i
7.  env  :  pEnvType(P.M[P])@i
8.  \mforall{}t:\mBbbN{}
          let  info,Cs,G  =  pRun(<S1,  S2>env;n2m;l2m)  t  in 
          \mforall{}x\mmember{}G.((fst(fst(x)))  \mleq{}  t)  \mvee{}  (\mexists{}m:\mBbbN{}lg-size(S2).  ((fst(x))  =  (fst(lg-label(S2;m)))))
9.  <S1,  S2>  \mmember{}  System(P.M[P])
10.  t  :  \mBbbN{}@i
11.  x  :  Id@i
12.  \muparrow{}is-run-event(pRun(<S1,  S2>env;n2m;l2m);t;x)
\mvdash{}  fst(fst(run-info(pRun(<S1,  S2>env;n2m;l2m);<t,  x>)))  <  t  \mvee{}  (\mexists{}m:\mBbbN{}lg-size(S2).  ((fst(run-info(pRun(\000C<S1,  S2>env;n2m;l2m);<t,  x>)))  =  (fst(lg-label(S2;m)))))


By

---

Latex:
(MoveToConcl  (-1)\mcdot{}
  THEN  RepUR  ``run-info``  0
  THEN  RecUnfold  `pRun`  0
  THEN  RepUR  ``let  is-run-event  do-chosen-command``  0
  THEN  AutoSplit
  THEN  RepUR  ``bfalse``  0
  THEN  Try  (Complete  (Auto))
  THEN  (GenConclAtAddr  [1;1;1;1]  THENM  (RepeatFor  2  (D  -2)  THEN  Reduce  0))
  THEN  (GenConclAtAddr  [1;1;1;1]\mcdot{}
  THENM  (D  -2
                THEN  Reduce  0
                THEN  AutoSplit
                THEN  Try  ((RepUR  ``bfalse``  0  THEN  Complete  (Auto)))
                THEN  RepUR  ``lg-is-source``  -1
                THEN  (SplitOnHypITE  -1    THENA  Auto)
                THEN  Try  ((All  Reduce  THEN  Trivial))
                THEN  (GenConclAtAddrType  \mkleeneopen{}pInTransit(P.M[P])\mkleeneclose{}  [1;1;1;1]\mcdot{}  THENA  Auto)
                THEN  RepeatFor  2  (D  -2)
                THEN  Reduce  0\mcdot{})
  ))\mcdot{}

---

Home Index