---

Step * 1 of Lemma norm-runinfo_wf


1. M : Type ⟶ Type
2. ∀P:Type. value-type(M[P])
3. x : ℤ × Id × Id × pMsg(P.M[P])
⊢ let ev,x,ms = x in 
  let t,z = ev 
  in eval t' = t in
     eval z' = z in
     eval x' = x in
     eval ms' = ms in
       inl <<t', z'>, x', ms'> ∈ {info':pRunInfo(P.M[P])| info' = (inl x) ∈ pRunInfo(P.M[P])} 
BY
{ ((RepeatFor 2 (D (-1)) THEN D -3) THEN RepUR ``pRunInfo`` 0) }

1
1. M : Type ⟶ Type
2. ∀P:Type. value-type(M[P])
3. x5 : ℤ
4. x6 : Id
5. x3 : Id
6. x4 : pMsg(P.M[P])
⊢ eval t' = x5 in
  eval z' = x6 in
  eval x' = x3 in
  eval ms' = x4 in
    inl <<t', z'>, x', ms'> ∈ {info':ℤ × Id × Id × pMsg(P.M[P])?| 
                          info' = (inl <<x5, x6>, x3, x4>) ∈ (ℤ × Id × Id × pMsg(P.M[P])?)} 

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  \mforall{}P:Type.  value-type(M[P])
3.  x  :  \mBbbZ{}  \mtimes{}  Id  \mtimes{}  Id  \mtimes{}  pMsg(P.M[P])
\mvdash{}  let  ev,x,ms  =  x  in 
    let  t,z  =  ev 
    in  eval  t'  =  t  in
          eval  z'  =  z  in
          eval  x'  =  x  in
          eval  ms'  =  ms  in
              inl  <<t',  z'>,  x',  ms'>  \mmember{}  \{info':pRunInfo(P.M[P])|  info'  =  (inl  x)\} 


By

---

Latex:
((RepeatFor  2  (D  (-1))  THEN  D  -3)  THEN  RepUR  ``pRunInfo``  0)

---

Home Index