---

Step * of Lemma pRun-intransit-invariant

∀[M:Type ─→ Type]
  ∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀Cs0:component(P.M[P]) List. ∀G0:LabeledDAG(pInTransit(P.M[P])).
  ∀env:pEnvType(P.M[P]). ∀t:ℕ.
    let r = pRun(<Cs0, G0>;env;n2m;l2m) in
        let info,Cs,G = r t in 
        ∀x∈G.let ev = fst(x) in
                 ((fst(ev)) ≤ t) ∨ (∃m:ℕlg-size(G0). (ev = (fst(lg-label(G0;m))) ∈ (ℤ × Id))) 
  supposing Continuous+(P.M[P])
BY
{ (RepUR ``let`` 0
   THEN Auto
   THEN (Assert ∀x:pInTransit(P.M[P]). ∀t:ℤ.
                  (((fst(fst(x))) ≤ t) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id))) ∈ ℙ) BY
               (Auto THEN DoSubsume THEN Auto))
   THEN ((InstLemma `pRun-System-invariant` [⌈M⌉;⌈λ2t S.let Cs,G = S 
                                                        in ∀x∈G.((fst(fst(x))) ≤ t)
                                                            ∨ (∃m:ℕlg-size(G0)
                                                                ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))⌉;⌈n2m⌉;
          ⌈l2m⌉;⌈<Cs0, G0>⌉]⋅
          THENA Auto
          )
         THEN Try ((DVar `S2' THEN Auto)⋅)
         )⋅) }

1
.....antecedent..... 
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))) ∈ ℙ)
⊢ let Cs,G = <Cs0, G0> 
  in ∀x∈G.((fst(fst(x))) ≤ 0) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))

2
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. S : System(P.M[P])@i
12. let Cs,G = S 
    in ∀x∈G.((fst(fst(x))) ≤ t1) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))@i
13. e1 : pEnvType(P.M[P])@i
⊢ let n,m,nm = e1 (t1 + 1) pRun(<Cs0, G0>;e1;n2m;l2m) in 
let Cs,G = snd(do-chosen-command(n2m;l2m;t1 + 1;S;n;m;nm)) 
in ∀x∈G.((fst(fst(x))) ≤ (t1 + 1)) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))

3
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. ∀env:pEnvType(P.M[P]). ∀t:ℕ.
      let Cs,G = snd((pRun(<Cs0, G0>;env;n2m;l2m) t)) 
      in ∀x∈G.((fst(fst(x))) ≤ t) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))
⊢ let info,Cs,G = pRun(<Cs0, G0>;env;n2m;l2m) t in 
∀x∈G.((fst(fst(x))) ≤ t) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}n2m:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}l2m:Id  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}Cs0:component(P.M[P])  List.
    \mforall{}G0:LabeledDAG(pInTransit(P.M[P])).  \mforall{}env:pEnvType(P.M[P]).  \mforall{}t:\mBbbN{}.
        let  r  =  pRun(<Cs0,  G0>env;n2m;l2m)  in
                let  info,Cs,G  =  r  t  in 
                \mforall{}x\mmember{}G.let  ev  =  fst(x)  in
                                  ((fst(ev))  \mleq{}  t)  \mvee{}  (\mexists{}m:\mBbbN{}lg-size(G0).  (ev  =  (fst(lg-label(G0;m))))) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(RepUR  ``let``  0
  THEN  Auto
  THEN  (Assert  \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{})  BY
                          (Auto  THEN  DoSubsume  THEN  Auto))
  THEN  ((InstLemma  `pRun-System-invariant`  [\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}t  S.let  Cs,G  =  S 
                                                                                                            in  \mforall{}x\mmember{}G.((fst(fst(x)))  \mleq{}  t)
                                                                                                                    \mvee{}  (\mexists{}m:\mBbbN{}lg-size(G0)
                                                                                                                            ((fst(x))  =  (fst(lg-label(G0;m)))))\mkleeneclose{};
                \mkleeneopen{}n2m\mkleeneclose{};\mkleeneopen{}l2m\mkleeneclose{};\mkleeneopen{}<Cs0,  G0>\mkleeneclose{}]\mcdot{}
                THENA  Auto
                )
              THEN  Try  ((DVar  `S2'  THEN  Auto)\mcdot{})
              )\mcdot{})

---

Home Index