---

Step * 1 1 3 1 3 of Lemma std-component-property


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. x : Id@i
6. Q : Process(P.M[P])@i
7. S2 : InitialSystem(P.M[P])@i
8. sub-system(P.M[P];<[<x, Q>], lg-nil()>;S2)@i
9. env : pEnvType(P.M[P])@i
10. reliable-env(env; pRun(S2;env;n2m;l2m))@i
11. cause : E ─→ (E?)
12. (∀C∈[<x, Q>].∀e:E
                 ∀p∈last(data-stream(snd(C);map(λe.info(e);≤loc(e)))).let y,c = p 
                                                                      in (com-kind(c) ∈ ``msg choose new``)
                                                                         ⇒ (∃e':E
                                                                              ((loc(e') = y ∈ Id)
                                                                              ∧ (e < e')
                                                                              ∧ (∃n:ℕ
                                                                                  ∃nm:Id
                                                                                   (info(e')
                                                                                   = command-to-msg(c;n2m n;l2m nm)
                                                                                   ∈ pMsg(P.M[P])))
                                                                              ∧ ((cause e') = (inl e) ∈ (E?)))) 
                 supposing loc(e) = (fst(C)) ∈ Id)
13. c1 : E ─→ (E?)
14. e : E@i
15. loc(e) = x ∈ Id@i
16. v : pExt(P.M[P])@i
17. last(data-stream(Q;map(λe.info(e);≤loc(e)))) = v ∈ pExt(P.M[P])@i
⊢ ∀p∈v.let y,c = p 
       in (com-kind(c) ∈ ``msg choose new``)
          ⇒ (∃e':E
               ((loc(e') = y ∈ Id)
               ∧ (e < e')
               ∧ (∃n:ℕ. ∃nm:Id. (info(e') = command-to-msg(c;n2m n;l2m nm) ∈ pMsg(P.M[P])))
               ∧ ((c1 e') = (inl e) ∈ (E?)))) ∈ ℙ
BY
{ (D (-2) THEN Auto) }

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  Continuous+(P.M[P])
3.  n2m  :  \mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])@i
4.  l2m  :  Id  {}\mrightarrow{}  pMsg(P.M[P])@i
5.  x  :  Id@i
6.  Q  :  Process(P.M[P])@i
7.  S2  :  InitialSystem(P.M[P])@i
8.  sub-system(P.M[P];<[<x,  Q>],  lg-nil()>S2)@i
9.  env  :  pEnvType(P.M[P])@i
10.  reliable-env(env;  pRun(S2;env;n2m;l2m))@i
11.  cause  :  E  {}\mrightarrow{}  (E?)
12.  (\mforall{}C\mmember{}[<x,  Q>].\mforall{}e:E
                                  \mforall{}p\mmember{}last(data-stream(snd(C);map(\mlambda{}e.info(e);\mleq{}loc(e)))).
                                    let  y,c  =  p 
                                    in  (com-kind(c)  \mmember{}  ``msg  choose  new``)
                                          {}\mRightarrow{}  (\mexists{}e':E
                                                    ((loc(e')  =  y)
                                                    \mwedge{}  (e  <  e')
                                                    \mwedge{}  (\mexists{}n:\mBbbN{}.  \mexists{}nm:Id.  (info(e')  =  command-to-msg(c;n2m  n;l2m  nm)))
                                                    \mwedge{}  ((cause  e')  =  (inl  e)))) 
                                  supposing  loc(e)  =  (fst(C)))
13.  c1  :  E  {}\mrightarrow{}  (E?)
14.  e  :  E@i
15.  loc(e)  =  x@i
16.  v  :  pExt(P.M[P])@i
17.  last(data-stream(Q;map(\mlambda{}e.info(e);\mleq{}loc(e))))  =  v@i
\mvdash{}  \mforall{}p\mmember{}v.let  y,c  =  p 
              in  (com-kind(c)  \mmember{}  ``msg  choose  new``)
                    {}\mRightarrow{}  (\mexists{}e':E
                              ((loc(e')  =  y)
                              \mwedge{}  (e  <  e')
                              \mwedge{}  (\mexists{}n:\mBbbN{}.  \mexists{}nm:Id.  (info(e')  =  command-to-msg(c;n2m  n;l2m  nm)))
                              \mwedge{}  ((c1  e')  =  (inl  e))))  \mmember{}  \mBbbP{}


By

---

Latex:
(D  (-2)  THEN  Auto)

---

Home Index