Step
*
1
1
1
of Lemma
pRun_wf
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. nat2msg : ℕ ─→ pMsg(P.M[P])
4. loc2msg : Id ─→ pMsg(P.M[P])
5. S0 : System(P.M[P])
6. env : pEnvType(P.M[P])
7. t : {1...}
8. ∀t:ℕt. (pRun(S0;env;nat2msg;loc2msg) t ∈ ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))
⊢ pRun(S0;env;nat2msg;loc2msg) ∈ ℕt ─→ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P])))
BY
{ (ExtWith [`t'][⌈Top ─→ Top⌉]⋅ THEN Auto)⋅ }
Latex:
Latex:
1. M : Type {}\mrightarrow{} Type
2. Continuous+(P.M[P])
3. nat2msg : \mBbbN{} {}\mrightarrow{} pMsg(P.M[P])
4. loc2msg : Id {}\mrightarrow{} pMsg(P.M[P])
5. S0 : System(P.M[P])
6. env : pEnvType(P.M[P])
7. t : \{1...\}
8. \mforall{}t:\mBbbN{}t. (pRun(S0;env;nat2msg;loc2msg) t \mmember{} \mBbbZ{} \mtimes{} Id \mtimes{} Id \mtimes{} pMsg(P.M[P])? \mtimes{} System(P.M[P]))
\mvdash{} pRun(S0;env;nat2msg;loc2msg) \mmember{} \mBbbN{}t {}\mrightarrow{} (\mBbbZ{} \mtimes{} Id \mtimes{} Id \mtimes{} pMsg(P.M[P])?
\mtimes{} Top
\mtimes{} LabeledDAG(pInTransit(P.M[P])))
By
Latex:
(ExtWith [`t'][\mkleeneopen{}Top {}\mrightarrow{} Top\mkleeneclose{}]\mcdot{} THEN Auto)\mcdot{}
Home
Index