---

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


∀[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
{ (InductionOnList THEN Reduce 0 THEN Auto) }

1
1. [M] : Type ⟶ Type
2. G0 : LabeledDAG(pInTransit(P.M[P]))@i
3. t1 : ℕ@i
4. u : component(P.M[P])@i
5. v : component(P.M[P]) List@i
6. ∀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@0: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@0;v7;S;C)
                            over list:
                              v
                            with starting value:
                             <cs, H>) 
                 in ∀x∈G.((fst(fst(x))) ≤ t1) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))))))@i'
7. v7 : Id@i
8. Continuous+(P.M[P])@i'
9. H : LabeledDAG(pInTransit(P.M[P]))@i
10. ∀x∈H.((fst(fst(x))) ≤ t1) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))@i
11. v@0 : pMsg(P.M[P])@i
12. cs : component(P.M[P]) List@i
⊢ let Cs,G = accumulate (with value S and list item C):
              deliver-msg-to-comp(t1;v@0;v7;S;C)
             over list:
               v
             with starting value:
              deliver-msg-to-comp(t1;v@0;v7;<cs, H>;u)) 
  in ∀x∈G.((fst(fst(x))) ≤ t1) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))

---

Latex:

---

Latex:

\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:
(InductionOnList  THEN  Reduce  0  THEN  Auto)

---

Home Index