---

Step * 1 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?)
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
BY
{ At ⌈Type⌉ (With ⌈cause⌉ (D 0))⋅ }

1
.....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)
⊢ cause ∈ E ─→ (E?)

2
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)
⊢ ∀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

3
.....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

---

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)))
\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:
At  \mkleeneopen{}Type\mkleeneclose{}  (With  \mkleeneopen{}cause\mkleeneclose{}  (D  0))\mcdot{}

---

Home Index