---

Step * of Lemma std-env-reliable

∀nm:Id
  ∀[M:Type ⟶ Type]
    ∀S0:InitialSystem(P.M[P]). ∀n2m:ℕ ⟶ pMsg(P.M[P]). ∀l2m:Id ⟶ pMsg(P.M[P]).
      reliable-env(std-env(nm); pRun(S0;std-env(nm);n2m;l2m)) 
    supposing Continuous+(P.M[P])
BY
{ (Auto THEN D 0 THEN RepUR ``std-env`` 0 THEN Auto THEN With ⌜t + 1⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}nm:Id
    \mforall{}[M:Type  {}\mrightarrow{}  Type]
        \mforall{}S0:InitialSystem(P.M[P]).  \mforall{}n2m:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}l2m:Id  {}\mrightarrow{}  pMsg(P.M[P]).
            reliable-env(std-env(nm);  pRun(S0;std-env(nm);n2m;l2m)) 
        supposing  Continuous+(P.M[P])


By

---

Latex:
(Auto  THEN  D  0  THEN  RepUR  ``std-env``  0  THEN  Auto  THEN  With  \mkleeneopen{}t  +  1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index