---

Step * 2 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) ∈ ℤ} )
⊢ eval r = pRun2(S0;env;nat2msg;loc2msg;t - 1) in
  eval nxt = let info,S = let n,m,nm = env t (λi.r[i]) in 
             do-chosen-command(nat2msg;loc2msg;t;snd(last(r));n;m;nm) 
             in eval info' = norm-runinfo(info) in
                eval S' = norm-system S in
                  <info', S'> in
    r @ [nxt] ∈ {L:(ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P])) List| ||L|| = (t + 1) ∈ ℤ} 
BY
{ ((InstHyp [⌈t - 1⌉] (-1)⋅ THENA Auto)
   THEN GenConclAtAddr [2;1]
   THEN (CallByValueReduceOn ⌈v⌉ 0⋅ THENA Auto)
   THEN (GenConclAtAddr [2;1;1;1] THENA (Auto THEN Auto THEN D -3 THEN Auto'))
   THEN RepeatFor 2 (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
⊢ eval nxt = let info,S = do-chosen-command(nat2msg;loc2msg;t;snd(last(v));v2;v4;v5) 
             in eval info' = norm-runinfo(info) in
                eval S' = norm-system S in
                  <info', S'> in
  v @ [nxt] ∈ {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)\}  )
\mvdash{}  eval  r  =  pRun2(S0;env;nat2msg;loc2msg;t  -  1)  in
    eval  nxt  =  let  info,S  =  let  n,m,nm  =  env  t  (\mlambda{}i.r[i])  in 
                          do-chosen-command(nat2msg;loc2msg;t;snd(last(r));n;m;nm) 
                          in  eval  info'  =  norm-runinfo(info)  in
                                eval  S'  =  norm-system  S  in
                                    <info',  S'>  in
        r  @  [nxt]  \mmember{}  \{L:(\mBbbZ{}  \mtimes{}  Id  \mtimes{}  Id  \mtimes{}  pMsg(P.M[P])?  \mtimes{}  System(P.M[P]))  List|  ||L||  =  (t  +  1)\} 


By

---

Latex:
((InstHyp  [\mkleeneopen{}t  -  1\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  GenConclAtAddr  [2;1]
  THEN  (CallByValueReduceOn  \mkleeneopen{}v\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (GenConclAtAddr  [2;1;1;1]  THENA  (Auto  THEN  Auto  THEN  D  -3  THEN  Auto'))
  THEN  RepeatFor  2  (D  (-2))
  THEN  Reduce  0)

---

Home Index