---

Step * 1 1 1 1 1 of Lemma pRun2_wf

.....aux..... 
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. v : System(P.M[P])@i
14. S0 = v ∈ System(P.M[P])@i
15. (norm-system S0) = v ∈ {y:System(P.M[P])| S0 = y ∈ System(P.M[P])} @i
⊢ (v)↓
BY
{ (DVar `v' THEN RepUR ``has-value`` 0) }

1
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

---

Latex:

---

Latex:
.....aux..... 
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.  v  :  System(P.M[P])@i
14.  S0  =  v@i
15.  (norm-system  S0)  =  v@i
\mvdash{}  (v)\mdownarrow{}


By

---

Latex:
(DVar  `v'  THEN  RepUR  ``has-value``  0)

---

Home Index