---

Step * of Lemma std-component-property

∀[M:Type ⟶ Type]
  ∀n2m:ℕ ⟶ pMsg(P.M[P]). ∀l2m:Id ⟶ pMsg(P.M[P]). ∀x:Id. ∀Q:Process(P.M[P]).
    assuming(env,r.reliable-env(env; r))
     <[<x, Q>], lg-nil()> |= es.∃cause:E ⟶ (E?)
                               ∀e:E
                                 let G = last(data-stream(Q;map(λe.info(e);≤loc(e)))) in
                                     ∀p∈G.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 
  supposing Continuous+(P.M[P])
BY
{ (InstLemma `std-components-property` []
   THEN RepeatFor 4 ((ParallelLast' THENA Auto))
   THEN Auto
   THEN ((InstHyp [⌜[<x, Q>]⌝] (-3)⋅ THENM (Thin (-4) THEN RepeatFor 3 ((ParallelLast' THENA Auto))))
         THENA (Unfold `component` 0 THEN Auto)
         )
   THEN Try ((RepeatFor 2 (ParallelLast) THEN All (RepUR ``let``) THEN ParallelLast))) }

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?)
     (∀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:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}n2m:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}l2m:Id  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}x:Id.  \mforall{}Q:Process(P.M[P]).
        assuming(env,r.reliable-env(env;  r))
          <[<x,  Q>],  lg-nil()>  |=  es.\mexists{}cause:E  {}\mrightarrow{}  (E?)
                                                              \mforall{}e:E
                                                                  let  G  =  last(data-stream(Q;map(\mlambda{}e.info(e);\mleq{}loc(e))))  in
                                                                          \mforall{}p\mmember{}G.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 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(InstLemma  `std-components-property`  []
  THEN  RepeatFor  4  ((ParallelLast'  THENA  Auto))
  THEN  Auto
  THEN  ((InstHyp  [\mkleeneopen{}[<x,  Q>]\mkleeneclose{}]  (-3)\mcdot{}  THENM  (Thin  (-4)  THEN  RepeatFor  3  ((ParallelLast'  THENA  Auto))))
              THENA  (Unfold  `component`  0  THEN  Auto)
              )
  THEN  Try  ((RepeatFor  2  (ParallelLast)  THEN  All  (RepUR  ``let``)  THEN  ParallelLast)))

---

Home Index