---

Step * 2 1 1 1 1 2 1 of Lemma pRun-intransit-invariant

.....assertion..... 
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
27. ∀x∈H.((fst(fst(x))) ≤ (t1 + 1)) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))
⊢ ∀[M:Type ⟶ Type]
    ∀G0:LabeledDAG(pInTransit(P.M[P])). ∀t1:ℕ. ∀C:component(P.M[P]) List. ∀v7:Id.
      (Continuous+(P.M[P])
      ⇒ (∀H:LabeledDAG(pInTransit(P.M[P]))
            (∀x∈H.((fst(fst(x))) ≤ t1) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))
            ⇒ (∀v:pMsg(P.M[P]). ∀cs:component(P.M[P]) List.
                  let Cs,G = accumulate (with value S and list item C):
                              deliver-msg-to-comp(t1;v;v7;S;C)
                             over list:
                               C
                             with starting value:
                              <cs, H>) 
                  in ∀x∈G.((fst(fst(x))) ≤ t1) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))))))
BY
{ All Thin }

1
∀[M:Type ⟶ Type]
  ∀G0:LabeledDAG(pInTransit(P.M[P])). ∀t1:ℕ. ∀C:component(P.M[P]) List. ∀v7:Id.
    (Continuous+(P.M[P])
    ⇒ (∀H:LabeledDAG(pInTransit(P.M[P]))
          (∀x∈H.((fst(fst(x))) ≤ t1) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))
          ⇒ (∀v:pMsg(P.M[P]). ∀cs:component(P.M[P]) List.
                let Cs,G = accumulate (with value S and list item C):
                            deliver-msg-to-comp(t1;v;v7;S;C)
                           over list:
                             C
                           with starting value:
                            <cs, H>) 
                in ∀x∈G.((fst(fst(x))) ≤ t1) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))))))

---

Latex:

---

Latex:
.....assertion..... 
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{}null(lg-in-edges(G;v1))
20.  v1  <  lg-size(G)
21.  v5  :  \mBbbZ{}  \mtimes{}  Id@i
22.  v7  :  Id@i
23.  v8  :  pCom(P.M[P])@i
24.  lg-label(G;v1)  =  <v5,  v7,  v8>@i
25.  H  :  LabeledDAG(pInTransit(P.M[P]))@i
26.  lg-remove(G;v1)  =  H@i
27.  \mforall{}x\mmember{}H.((fst(fst(x)))  \mleq{}  (t1  +  1))  \mvee{}  (\mexists{}m:\mBbbN{}lg-size(G0).  ((fst(x))  =  (fst(lg-label(G0;m)))))
\mvdash{}  \mforall{}[M:Type  {}\mrightarrow{}  Type]
        \mforall{}G0:LabeledDAG(pInTransit(P.M[P])).  \mforall{}t1:\mBbbN{}.  \mforall{}C:component(P.M[P])  List.  \mforall{}v7:Id.
            (Continuous+(P.M[P])
            {}\mRightarrow{}  (\mforall{}H:LabeledDAG(pInTransit(P.M[P]))
                        (\mforall{}x\mmember{}H.((fst(fst(x)))  \mleq{}  t1)  \mvee{}  (\mexists{}m:\mBbbN{}lg-size(G0).  ((fst(x))  =  (fst(lg-label(G0;m)))))
                        {}\mRightarrow{}  (\mforall{}v:pMsg(P.M[P]).  \mforall{}cs:component(P.M[P])  List.
                                    let  Cs,G  =  accumulate  (with  value  S  and  list  item  C):
                                                            deliver-msg-to-comp(t1;v;v7;S;C)
                                                          over  list:
                                                              C
                                                          with  starting  value:
                                                            <cs,  H>) 
                                    in  \mforall{}x\mmember{}G.((fst(fst(x)))  \mleq{}  t1)
                                            \mvee{}  (\mexists{}m:\mBbbN{}lg-size(G0).  ((fst(x))  =  (fst(lg-label(G0;m)))))))))


By

---

Latex:
All  Thin

---

Home Index