---

Step * 1 1 1 1 1 1 of Lemma pRun2_wf


1. M : Type ─→ Type
2. M[Top]
3. ∀P:Type. value-type(M[P])
4. Continuous+(P.M[P])
5. nat2msg : ℕ ─→ pMsg(P.M[P])
6. loc2msg : Id ─→ pMsg(P.M[P])
7. S0 : System(P.M[P])
8. env : pEnvType(P.M[P])
9. t : ℕ
10. ∀t:ℕt
      (pRun2(S0;env;nat2msg;loc2msg;t) ∈ {L:(ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P])) List| ||L|| = (t + 1) ∈ ℤ} )
11. t = 0 ∈ ℤ
12. norm-system ∈ id-fun(System(P.M[P]))
13. v1 : component(P.M[P]) List@i
14. v2 : LabeledDAG(pInTransit(P.M[P]))@i
15. S0 = <v1, v2> ∈ System(P.M[P])@i
16. (norm-system S0) = <v1, v2> ∈ {y:System(P.M[P])| S0 = y ∈ System(P.M[P])} @i
⊢ 0 ≤ 0
BY
{ Auto }

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  M[Top]
3.  \mforall{}P:Type.  value-type(M[P])
4.  Continuous+(P.M[P])
5.  nat2msg  :  \mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])
6.  loc2msg  :  Id  {}\mrightarrow{}  pMsg(P.M[P])
7.  S0  :  System(P.M[P])
8.  env  :  pEnvType(P.M[P])
9.  t  :  \mBbbN{}
10.  \mforall{}t:\mBbbN{}t
            (pRun2(S0;env;nat2msg;loc2msg;t)  \mmember{}  \{L:(\mBbbZ{}  \mtimes{}  Id  \mtimes{}  Id  \mtimes{}  pMsg(P.M[P])?  \mtimes{}  System(P.M[P]))  List| 
                                                                                    ||L||  =  (t  +  1)\}  )
11.  t  =  0
12.  norm-system  \mmember{}  id-fun(System(P.M[P]))
13.  v1  :  component(P.M[P])  List@i
14.  v2  :  LabeledDAG(pInTransit(P.M[P]))@i
15.  S0  =  <v1,  v2>@i
16.  (norm-system  S0)  =  <v1,  v2>@i
\mvdash{}  0  \mleq{}  0


By

---

Latex:
Auto

---

Home Index