Step
*
2
1
1
2
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. v9 : System(P.M[P])@i
22. (norm-system v8) = v9 ∈ System(P.M[P])@i
⊢ eval nxt = eval S' = v9 in
<norm-runinfo(v7), S'> in
v @ [nxt] ∈ {L:(ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P])) List| ||L|| = (t + 1) ∈ ℤ}
BY
{ (D -2 THEN Reduce 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 : {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
⊢ v @ [<norm-runinfo(v7), v10, v11>] ∈ {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 : \{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. v9 : System(P.M[P])@i
22. (norm-system v8) = v9@i
\mvdash{} eval nxt = eval S' = v9 in
<norm-runinfo(v7), S'> in
v @ [nxt] \mmember{} \{L:(\mBbbZ{} \mtimes{} Id \mtimes{} Id \mtimes{} pMsg(P.M[P])? \mtimes{} System(P.M[P])) List| ||L|| = (t + 1)\}
By
Latex:
(D -2 THEN Reduce 0)
Home
Index