---

Step * 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]))
⊢ eval S = norm-system S0 in
  [<inr ⋅ , S>] ∈ {L:(ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P])) List| ||L|| = (t + 1) ∈ ℤ} 
BY
{ (GenConclAtAddr [2;1]⋅ THENA Auto)⋅ }

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. v : {y:System(P.M[P])| S0 = y ∈ System(P.M[P])} @i
14. (norm-system S0) = v ∈ {y:System(P.M[P])| S0 = y ∈ System(P.M[P])} @i
⊢ eval S = v in
  [<inr ⋅ , S>] ∈ {L:(ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P])) List| ||L|| = (t + 1) ∈ ℤ} 

---

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]))
\mvdash{}  eval  S  =  norm-system  S0  in
    [<inr  \mcdot{}  ,  S>]  \mmember{}  \{L:(\mBbbZ{}  \mtimes{}  Id  \mtimes{}  Id  \mtimes{}  pMsg(P.M[P])?  \mtimes{}  System(P.M[P]))  List|  ||L||  =  (t  +  1)\} 


By

---

Latex:
(GenConclAtAddr  [2;1]\mcdot{}  THENA  Auto)\mcdot{}

---

Home Index