---

Step * of Lemma reliable-env-property1

∀[M:Type ─→ Type]
  ∀S0:InitialSystem(P.M[P]). ∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀env:pEnvType(P.M[P]).
    let r = pRun(S0;env;n2m;l2m) in
        reliable-env(env; r)
        ⇒ (∀tn:run-msg-commands(r)
              let t,n = tn 
              in ∃t':ℕ
                  ((t < t'
                  c∧ (((fst((env t' r))) ≤ n)
                     ∧ ↑lg-is-source(run-intransit(r;t');fst((env t' r))) supposing 0 < lg-size(run-intransit(r;t'))))
                  ∧ (∀i:ℕ
                       ¬(t < i
                       c∧ (((fst((env i r))) ≤ n)
                          ∧ ↑lg-is-source(run-intransit(r;i);fst((env i r))) 
                            supposing 0 < lg-size(run-intransit(r;i)))) 
                       supposing i < t'))) 
  supposing Continuous+(P.M[P])
BY
{ ((Auto THEN (GenConclAtAddrType ⌈pRunType(P.M[P])⌉ [1]⋅ THENA Auto) THEN RenameVar `r' (-2) THEN RepUR ``let`` 0)
   THEN (Auto
         THEN Unfold `reliable-env` -2
         THEN D -1
         THEN Reduce 0
         THEN RenameVar `n' (-1)
         THEN D -1
         THEN (Assert run-command-node(r;t;n) ∧ (com-kind(snd(snd(run-command(r;t;n)))) ∈ ``msg choose new``) BY
                     (Auto
                      THEN Try ((Unhide
                                 THEN Auto
                                 THEN GenConclAtAddr [2;1;1;1]
                                 THEN RepeatFor 2 (D -2)
                                 THEN Reduce 0
                                 THEN Auto))
                      THEN All (Unfold `run-command-node`)
                      THEN Auto))
         THEN Thin (-2))⋅
   ) }

1
1. [M] : Type ─→ Type
2. Continuous+(P.M[P])
3. S0 : InitialSystem(P.M[P])@i
4. n2m : ℕ ─→ pMsg(P.M[P])@i
5. l2m : Id ─→ pMsg(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. r : pRunType(P.M[P])@i
8. pRun(S0;env;n2m;l2m) = r ∈ pRunType(P.M[P])@i
9. ∀t:ℕ. ∃t':ℕ. (t < t' ∧ ((fst((env t' r))) = 0 ∈ ℤ))@i
10. t : ℕ@i
11. n : ℕ@i
12. run-command-node(r;t;n) ∧ (com-kind(snd(snd(run-command(r;t;n)))) ∈ ``msg choose new``)
⊢ ∃t':ℕ
   ((t < t'
   c∧ (((fst((env t' r))) ≤ n)
      ∧ ↑lg-is-source(run-intransit(r;t');fst((env t' r))) supposing 0 < lg-size(run-intransit(r;t'))))
   ∧ (∀i:ℕ
        ¬(t < i
        c∧ (((fst((env i r))) ≤ n)
           ∧ ↑lg-is-source(run-intransit(r;i);fst((env i r))) supposing 0 < lg-size(run-intransit(r;i)))) 
        supposing i < t'))

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}S0:InitialSystem(P.M[P]).  \mforall{}n2m:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}l2m:Id  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}env:pEnvType(P.M[P]).
        let  r  =  pRun(S0;env;n2m;l2m)  in
                reliable-env(env;  r)
                {}\mRightarrow{}  (\mforall{}tn:run-msg-commands(r)
                            let  t,n  =  tn 
                            in  \mexists{}t':\mBbbN{}
                                    ((t  <  t'
                                    c\mwedge{}  (((fst((env  t'  r)))  \mleq{}  n)
                                          \mwedge{}  \muparrow{}lg-is-source(run-intransit(r;t');fst((env  t'  r))) 
                                              supposing  0  <  lg-size(run-intransit(r;t'))))
                                    \mwedge{}  (\mforall{}i:\mBbbN{}
                                              \mneg{}(t  <  i
                                              c\mwedge{}  (((fst((env  i  r)))  \mleq{}  n)
                                                    \mwedge{}  \muparrow{}lg-is-source(run-intransit(r;i);fst((env  i  r))) 
                                                        supposing  0  <  lg-size(run-intransit(r;i)))) 
                                              supposing  i  <  t'))) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
((Auto
    THEN  (GenConclAtAddrType  \mkleeneopen{}pRunType(P.M[P])\mkleeneclose{}  [1]\mcdot{}  THENA  Auto)
    THEN  RenameVar  `r'  (-2)
    THEN  RepUR  ``let``  0)
  THEN  (Auto
              THEN  Unfold  `reliable-env`  -2
              THEN  D  -1
              THEN  Reduce  0
              THEN  RenameVar  `n'  (-1)
              THEN  D  -1
              THEN  (Assert  run-command-node(r;t;n)
                                      \mwedge{}  (com-kind(snd(snd(run-command(r;t;n))))  \mmember{}  ``msg  choose  new``)  BY
                                      (Auto
                                        THEN  Try  ((Unhide
                                                              THEN  Auto
                                                              THEN  GenConclAtAddr  [2;1;1;1]
                                                              THEN  RepeatFor  2  (D  -2)
                                                              THEN  Reduce  0
                                                              THEN  Auto))
                                        THEN  All  (Unfold  `run-command-node`)
                                        THEN  Auto))
              THEN  Thin  (-2))\mcdot{}
  )

---

Home Index