---

Step * 1 1 1 1 2 2 of Lemma pRun2_wf

.....set predicate..... 
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
⊢ ||[<inr ⋅ , v>]|| = (t + 1) ∈ ℤ
BY
{ (Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
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{}  ||[<inr  \mcdot{}  ,  v>]||  =  (t  +  1)


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index