---

Step * 2 1 1 2 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 : {1...}
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. pRun2(S0;env;nat2msg;loc2msg;t - 1) ∈ {L:(ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P])) List| 
                                           ||L|| = ((t - 1) + 1) ∈ ℤ} 
12. v : {L:(ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P])) List| ||L|| = ((t - 1) + 1) ∈ ℤ} @i
13. pRun2(S0;env;nat2msg;loc2msg;t - 1)
= v
∈ {L:(ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P])) List| ||L|| = ((t - 1) + 1) ∈ ℤ} @i
14. v2 : ℕ@i
15. v4 : ℕ@i
16. v5 : Id@i
17. (env t (λi.v[i])) = <v2, v4, v5> ∈ (ℕ × ℕ × Id)@i
18. v7 : ℤ × Id × Id × pMsg(P.M[P])?@i
19. v8 : System(P.M[P])@i
20. do-chosen-command(nat2msg;loc2msg;t;snd(last(v));v2;v4;v5)
= <v7, v8>
∈ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))@i
21. v10 : component(P.M[P]) List@i
22. v11 : LabeledDAG(pInTransit(P.M[P]))@i
23. (norm-system v8) = <v10, v11> ∈ System(P.M[P])@i
⊢ norm-runinfo(v7) ∈ ℤ × Id × Id × pMsg(P.M[P])?
BY
{ All (Fold `pRunInfo`) }

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 : {1...}
10. ∀t:ℕt. (pRun2(S0;env;nat2msg;loc2msg;t) ∈ {L:(pRunInfo(P.M[P]) × System(P.M[P])) List| ||L|| = (t + 1) ∈ ℤ} )
11. pRun2(S0;env;nat2msg;loc2msg;t - 1) ∈ {L:(pRunInfo(P.M[P]) × System(P.M[P])) List| ||L|| = ((t - 1) + 1) ∈ ℤ} 
12. v : {L:(pRunInfo(P.M[P]) × System(P.M[P])) List| ||L|| = ((t - 1) + 1) ∈ ℤ} @i
13. pRun2(S0;env;nat2msg;loc2msg;t - 1) = v ∈ {L:(pRunInfo(P.M[P]) × System(P.M[P])) List| ||L|| = ((t - 1) + 1) ∈ ℤ} @i
14. v2 : ℕ@i
15. v4 : ℕ@i
16. v5 : Id@i
17. (env t (λi.v[i])) = <v2, v4, v5> ∈ (ℕ × ℕ × Id)@i
18. v7 : pRunInfo(P.M[P])@i
19. v8 : System(P.M[P])@i
20. do-chosen-command(nat2msg;loc2msg;t;snd(last(v));v2;v4;v5) = <v7, v8> ∈ (pRunInfo(P.M[P]) × System(P.M[P]))@i
21. v10 : component(P.M[P]) List@i
22. v11 : LabeledDAG(pInTransit(P.M[P]))@i
23. (norm-system v8) = <v10, v11> ∈ System(P.M[P])@i
⊢ norm-runinfo(v7) ∈ pRunInfo(P.M[P])

---

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  :  \{1...\}
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.  pRun2(S0;env;nat2msg;loc2msg;t  -  1)  \mmember{}  \{L:(\mBbbZ{}  \mtimes{}  Id  \mtimes{}  Id  \mtimes{}  pMsg(P.M[P])?  \mtimes{}  System(P.M[P]))  List| 
                                                                                      ||L||  =  ((t  -  1)  +  1)\} 
12.  v  :  \{L:(\mBbbZ{}  \mtimes{}  Id  \mtimes{}  Id  \mtimes{}  pMsg(P.M[P])?  \mtimes{}  System(P.M[P]))  List|  ||L||  =  ((t  -  1)  +  1)\}  @i
13.  pRun2(S0;env;nat2msg;loc2msg;t  -  1)  =  v@i
14.  v2  :  \mBbbN{}@i
15.  v4  :  \mBbbN{}@i
16.  v5  :  Id@i
17.  (env  t  (\mlambda{}i.v[i]))  =  <v2,  v4,  v5>@i
18.  v7  :  \mBbbZ{}  \mtimes{}  Id  \mtimes{}  Id  \mtimes{}  pMsg(P.M[P])?@i
19.  v8  :  System(P.M[P])@i
20.  do-chosen-command(nat2msg;loc2msg;t;snd(last(v));v2;v4;v5)  =  <v7,  v8>@i
21.  v10  :  component(P.M[P])  List@i
22.  v11  :  LabeledDAG(pInTransit(P.M[P]))@i
23.  (norm-system  v8)  =  <v10,  v11>@i
\mvdash{}  norm-runinfo(v7)  \mmember{}  \mBbbZ{}  \mtimes{}  Id  \mtimes{}  Id  \mtimes{}  pMsg(P.M[P])?


By

---

Latex:
All  (Fold  `pRunInfo`)

---

Home Index