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