Step
*
of Lemma
stdEO-E-property
∀[M:Type ─→ Type]
∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀S2:InitialSystem(P.M[P]). ∀env:pEnvType(P.M[P]). ∀e:E.
(e ∈ ℕ+ × Id)
supposing Continuous+(P.M[P])
BY
{ 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. S2 : InitialSystem(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. e : E@i
⊢ e ∈ ℕ+ × 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{}S2:InitialSystem(P.M[P]). \mforall{}env:pEnvType(P.M[P]).
\mforall{}e:E.
(e \mmember{} \mBbbN{}\msupplus{} \mtimes{} Id)
supposing Continuous+(P.M[P])
By
Latex:
Auto
Home
Index