---

Step * of Lemma reliable-env-property2

∀[M:Type ─→ Type]
  ∀S:InitialSystem(P.M[P]). ∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀env:pEnvType(P.M[P]).
    let r = pRun(S;env;n2m;l2m) in
        reliable-env(env; r)
        ⇒ (∀e:runEvents(r). ∀P:Process(P.M[P]).
              ((P ∈ run-event-state-when(r;e))
              ⇒ ∀p∈snd((P (snd(run-info(r;e))))).let y,c = p 
                                                  in (com-kind(c) ∈ ``msg choose new``)
                                                     ⇒ (∃e':runEvents(r)
                                                          ((run-event-loc(e') = y ∈ Id)
                                                          ∧ (e run-lt(r) e')
                                                          ∧ (∃n:ℕ
                                                              ∃nm:Id
                                                               ((snd(run-info(r;e')))
                                                               = command-to-msg(c;n2m n;l2m nm)
                                                               ∈ pMsg(P.M[P])))
                                                          ∧ ((run-cause(r) e') = (inl e) ∈ (runEvents(r)?)))))) 
  supposing Continuous+(P.M[P])
BY
{ (InstLemma `reliable-env-property` []
   THEN RepeatFor 6 ((ParallelLast' THENA Auto))
   THEN All (RepUR ``let``)
   THEN (Assert pRun(S;env;n2m;l2m) ∈ pRunType(P.M[P]) BY
               Auto)
   THEN ParallelOp -2
   THEN Auto
   THEN (Assert 0 < run-event-step(e) BY
               (BLemma `run-event-step-positive` THEN Auto))
   THEN Unfold `run-event-step` -1
   THEN Try ((RepeatFor 2 (DVar `e') THEN All Reduce THEN Complete (Auto)))) }

1
1. [M] : Type ─→ Type
2. Continuous+(P.M[P])
3. S : 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. pRun(S;env;n2m;l2m) ∈ pRunType(P.M[P])
8. reliable-env(env; pRun(S;env;n2m;l2m))@i
9. ∀tn:run-msg-commands(pRun(S;env;n2m;l2m))
     ∃e:runEvents(pRun(S;env;n2m;l2m))
      let t,n = tn 
      in (run-info(pRun(S;env;n2m;l2m);e)
         = intransit-to-info(n2m;l2m;pRun(S;env;n2m;l2m);env;run-event-step(e);run-command(pRun(S;env;n2m;l2m);t;n))
         ∈ (ℤ × Id × pMsg(P.M[P])))
         ∧ (run-event-loc(e) = (fst(snd(run-command(pRun(S;env;n2m;l2m);t;n)))) ∈ Id)
10. e : runEvents(pRun(S;env;n2m;l2m))@i
11. P : Process(P.M[P])@i
12. (P ∈ run-event-state-when(pRun(S;env;n2m;l2m);e))@i
13. 0 < fst(e)
⊢ ∀p∈snd((P (snd(run-info(pRun(S;env;n2m;l2m);e))))).let y,c = p 
                                                     in (com-kind(c) ∈ ``msg choose new``)
                                                        ⇒ (∃e':runEvents(pRun(S;env;n2m;l2m))
                                                             ((run-event-loc(e') = y ∈ Id)
                                                             ∧ (e run-lt(pRun(S;env;n2m;l2m)) e')
                                                             ∧ (∃n:ℕ
                                                                 ∃nm:Id
                                                                  ((snd(run-info(pRun(S;env;n2m;l2m);e')))
                                                                  = command-to-msg(c;n2m n;l2m nm)
                                                                  ∈ pMsg(P.M[P])))
                                                             ∧ ((run-cause(pRun(S;env;n2m;l2m)) e')
                                                               = (inl e)
                                                               ∈ (runEvents(pRun(S;env;n2m;l2m))?))))

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}S: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(S;env;n2m;l2m)  in
                reliable-env(env;  r)
                {}\mRightarrow{}  (\mforall{}e:runEvents(r).  \mforall{}P:Process(P.M[P]).
                            ((P  \mmember{}  run-event-state-when(r;e))
                            {}\mRightarrow{}  \mforall{}p\mmember{}snd((P  (snd(run-info(r;e))))).let  y,c  =  p 
                                                                                                    in  (com-kind(c)  \mmember{}  ``msg  choose  new``)
                                                                                                          {}\mRightarrow{}  (\mexists{}e':runEvents(r)
                                                                                                                    ((run-event-loc(e')  =  y)
                                                                                                                    \mwedge{}  (e  run-lt(r)  e')
                                                                                                                    \mwedge{}  (\mexists{}n:\mBbbN{}
                                                                                                                            \mexists{}nm:Id
                                                                                                                              ((snd(run-info(r;e')))
                                                                                                                              =  command-to-msg(c;n2m  n;l2m  nm)))
                                                                                                                    \mwedge{}  ((run-cause(r)  e')  =  (inl  e)))))) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(InstLemma  `reliable-env-property`  []
  THEN  RepeatFor  6  ((ParallelLast'  THENA  Auto))
  THEN  All  (RepUR  ``let``)
  THEN  (Assert  pRun(S;env;n2m;l2m)  \mmember{}  pRunType(P.M[P])  BY
                          Auto)
  THEN  ParallelOp  -2
  THEN  Auto
  THEN  (Assert  0  <  run-event-step(e)  BY
                          (BLemma  `run-event-step-positive`  THEN  Auto))
  THEN  Unfold  `run-event-step`  -1
  THEN  Try  ((RepeatFor  2  (DVar  `e')  THEN  All  Reduce  THEN  Complete  (Auto))))

---

Home Index