---

Step * 1 1 1 of Lemma run-event-state-next2


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. S0 : System(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. n : {1...}
8. x : Id@i
9. v1 : ℕ@i
10. v3 : ℕ@i
11. v4 : Id@i
12. (env n pRun(S0;env;n2m;l2m)) = <v1, v3, v4> ∈ (ℕ × ℕ × Id)@i
13. x2 : ℤ × Id@i
14. x5 : pMsg(P.M[P])@i
15. v7 : component(P.M[P]) List@i
16. v8 : LabeledDAG(pInTransit(P.M[P]))@i
17. v9 : ℤ × Id × Id × pMsg(P.M[P])?@i
18. v11 : component(P.M[P]) List@i
19. v12 : LabeledDAG(pInTransit(P.M[P]))@i
20. (pRun(S0;env;n2m;l2m) (n - 1)) = <v9, v11, v12> ∈ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))@i
21. ↑lg-is-source(v12;v1)
⊢ (let ev,x,c = lg-label(v12;v1) in 
let G' = lg-remove(v12;v1) in
    if com-kind(c) =a "msg" then let ms = comm-msg(c) in <inl <ev, x, ms>, deliver-msg(n;ms;x;v11;G')>
    if com-kind(c) =a "create" then let P = comm-create(c) in <inr ⋅ , create-component(n;P;x;v11;G')>
    if com-kind(c) =a "choose" then let ms = n2m v3 in <inl <ev, x, ms>, deliver-msg(n;ms;x;v11;G')>
    if com-kind(c) =a "new" then let ms = l2m v4 in <inl <ev, x, ms>, deliver-msg(n;ms;x;v11;G')>
    else <inr ⋅ , v11, G'>
    fi 
= <inl <x2, x, x5>, v7, v8>
∈ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P])))
⇒ (∃G:LabeledDAG(pInTransit(P.M[P])). (v7 = (fst(deliver-msg(n;x5;x;v11;G))) ∈ (component(P.M[P]) List)))
BY
{ ((GenConclAtAddrType ⌜pInTransit(P.M[P])⌝ [1;2;1]⋅
    THENA (Auto THEN RepUR ``lg-is-source`` (-1) THEN SplitOnHypITE -1  THEN Auto)
    )
   THEN RepeatFor 2 (D (-2))
   THEN RepUR ``let`` 0
   THEN Repeat (AutoSplit)
   THEN (RepUR ``bfalse`` 0 THEN Auto THEN InstConcl [⌜lg-remove(v12;v1)⌝] ⋅ THEN Auto)⋅) }

---

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.  S0  :  System(P.M[P])@i
6.  env  :  pEnvType(P.M[P])@i
7.  n  :  \{1...\}
8.  x  :  Id@i
9.  v1  :  \mBbbN{}@i
10.  v3  :  \mBbbN{}@i
11.  v4  :  Id@i
12.  (env  n  pRun(S0;env;n2m;l2m))  =  <v1,  v3,  v4>@i
13.  x2  :  \mBbbZ{}  \mtimes{}  Id@i
14.  x5  :  pMsg(P.M[P])@i
15.  v7  :  component(P.M[P])  List@i
16.  v8  :  LabeledDAG(pInTransit(P.M[P]))@i
17.  v9  :  \mBbbZ{}  \mtimes{}  Id  \mtimes{}  Id  \mtimes{}  pMsg(P.M[P])?@i
18.  v11  :  component(P.M[P])  List@i
19.  v12  :  LabeledDAG(pInTransit(P.M[P]))@i
20.  (pRun(S0;env;n2m;l2m)  (n  -  1))  =  <v9,  v11,  v12>@i
21.  \muparrow{}lg-is-source(v12;v1)
\mvdash{}  (let  ev,x,c  =  lg-label(v12;v1)  in 
let  G'  =  lg-remove(v12;v1)  in
        if  com-kind(c)  =a  "msg"  then  let  ms  =  comm-msg(c)  in  <inl  <ev,  x,  ms>,  deliver-msg(n;ms;x;v11;G'\000C)>
        if  com-kind(c)  =a  "create"
            then  let  P  =  comm-create(c)  in
                              <inr  \mcdot{}  ,  create-component(n;P;x;v11;G')>
        if  com-kind(c)  =a  "choose"  then  let  ms  =  n2m  v3  in  <inl  <ev,  x,  ms>,  deliver-msg(n;ms;x;v11;G')>
        if  com-kind(c)  =a  "new"  then  let  ms  =  l2m  v4  in  <inl  <ev,  x,  ms>,  deliver-msg(n;ms;x;v11;G')>
        else  <inr  \mcdot{}  ,  v11,  G'>
        fi 
=  <inl  <x2,  x,  x5>,  v7,  v8>)
{}\mRightarrow{}  (\mexists{}G:LabeledDAG(pInTransit(P.M[P])).  (v7  =  (fst(deliver-msg(n;x5;x;v11;G)))))


By

---

Latex:
((GenConclAtAddrType  \mkleeneopen{}pInTransit(P.M[P])\mkleeneclose{}  [1;2;1]\mcdot{}
    THENA  (Auto  THEN  RepUR  ``lg-is-source``  (-1)  THEN  SplitOnHypITE  -1    THEN  Auto)
    )
  THEN  RepeatFor  2  (D  (-2))
  THEN  RepUR  ``let``  0
  THEN  Repeat  (AutoSplit)
  THEN  (RepUR  ``bfalse``  0  THEN  Auto  THEN  InstConcl  [\mkleeneopen{}lg-remove(v12;v1)\mkleeneclose{}]  \mcdot{}  THEN  Auto)\mcdot{})

---

Home Index