---

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


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)))
BY
{ (Assert ∀p:Top × Top. (p ~ <fst(p), snd(p)>) BY
         ((D 0 THENA Auto) THEN D -1 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
13. ∀p:Top × Top. (p ~ <fst(p), snd(p)>)
⊢ 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:

1.  [M]  :  Type  {}\mrightarrow{}  Type
2.  G0  :  LabeledDAG(pInTransit(P.M[P]))@i
3.  t1  :  \mBbbN{}@i
4.  u  :  component(P.M[P])@i
5.  v  :  component(P.M[P])  List@i
6.  \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@0: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@0;v7;S;C)
                                                        over  list:
                                                            v
                                                        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)))))))))@i'
7.  v7  :  Id@i
8.  Continuous+(P.M[P])@i'
9.  H  :  LabeledDAG(pInTransit(P.M[P]))@i
10.  \mforall{}x\mmember{}H.((fst(fst(x)))  \mleq{}  t1)  \mvee{}  (\mexists{}m:\mBbbN{}lg-size(G0).  ((fst(x))  =  (fst(lg-label(G0;m)))))@i
11.  v@0  :  pMsg(P.M[P])@i
12.  cs  :  component(P.M[P])  List@i
\mvdash{}  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  \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:
(Assert  \mforall{}p:Top  \mtimes{}  Top.  (p  \msim{}  <fst(p),  snd(p)>)  BY
              ((D  0  THENA  Auto)  THEN  D  -1  THEN  Reduce  0  THEN  Auto))\mcdot{}

---

Home Index