---

Step * 1 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?)
     (∀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)
⊢ ∃cause:E ─→ (E?)
   ∀e:E
     ∀p∈last(data-stream(Q;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) = x ∈ Id
BY
{ ExRepD }

1
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)
⊢ ∃cause:E ─→ (E?)
   ∀e:E
     ∀p∈last(data-stream(Q;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) = x ∈ Id

---

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.  \mexists{}cause:E  {}\mrightarrow{}  (E?)
          (\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)))
\mvdash{}  \mexists{}cause:E  {}\mrightarrow{}  (E?)
      \mforall{}e:E
          \mforall{}p\mmember{}last(data-stream(Q;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)  =  x


By

---

Latex:
ExRepD

---

Home Index