---

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

.....wf..... 
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?)
⊢ ∀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])))
                                                            ∧ ((c1 e') = (inl e) ∈ (E?)))) 
    supposing loc(e) = x ∈ Id ∈ Type
BY
{ ((All (Fold `runEO`) THEN All (Fold `stdEO`)) THEN Auto) }

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)
13. c1 : E ─→ (E?)
14. e : E@i
15. loc(e) = x ∈ Id@i
⊢ ∀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])))
                                                          ∧ ((c1 e') = (inl e) ∈ (E?)))) ∈ ℙ

---

Latex:

---

Latex:
.....wf..... 
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?)
\mvdash{}  \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{}  ((c1  e')  =  (inl  e)))) 
        supposing  loc(e)  =  x  \mmember{}  Type


By

---

Latex:
((All  (Fold  `runEO`)  THEN  All  (Fold  `stdEO`))  THEN  Auto)

---

Home Index