---

Step * of Lemma pRun2_wf

∀[M:Type ─→ Type]
  (∀[nat2msg:ℕ ─→ pMsg(P.M[P])]. ∀[loc2msg:Id ─→ pMsg(P.M[P])]. ∀[S0:System(P.M[P])]. ∀[env:pEnvType(P.M[P])]. ∀[t:ℕ].
     (pRun2(S0;env;nat2msg;loc2msg;t) ∈ {L:(ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P])) List| ||L|| = (t + 1) ∈ ℤ} )) \000Csupposing 
     (Continuous+(P.M[P]) and 
     (∀P:Type. value-type(M[P])) and 
     M[Top])
BY
{ (Auto THEN CompNatInd (-1) THEN RecUnfold `pRun2` 0 THEN Reduce 0 THEN AutoSplit)⋅ }

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

2
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) ∈ ℤ} 

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    (\mforall{}[nat2msg:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])].  \mforall{}[loc2msg:Id  {}\mrightarrow{}  pMsg(P.M[P])].  \mforall{}[S0:System(P.M[P])].
      \mforall{}[env:pEnvType(P.M[P])].  \mforall{}[t:\mBbbN{}].
          (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)\}  ))  supposing 
          (Continuous+(P.M[P])  and 
          (\mforall{}P:Type.  value-type(M[P]))  and 
          M[Top])


By

---

Latex:
(Auto  THEN  CompNatInd  (-1)  THEN  RecUnfold  `pRun2`  0  THEN  Reduce  0  THEN  AutoSplit)\mcdot{}

---

Home Index