---

Step * 1 1 of Lemma norm-runinfo_wf


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])?)} 
BY
{ RepeatFor 3 ((CallByValueReduce 0 THENA Auto)) }

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 ms' = x4 in
  inl <<x5, x6>, x3, ms'> ∈ {info':ℤ × Id × Id × pMsg(P.M[P])?| info' = (inl <<x5, x6>, x3, x4>) ∈ (ℤ × Id × Id × pMsg(P\000C.M[P])?)} 

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  \mforall{}P:Type.  value-type(M[P])
3.  x5  :  \mBbbZ{}
4.  x6  :  Id
5.  x3  :  Id
6.  x4  :  pMsg(P.M[P])
\mvdash{}  eval  t'  =  x5  in
    eval  z'  =  x6  in
    eval  x'  =  x3  in
    eval  ms'  =  x4  in
        inl  <<t',  z'>,  x',  ms'>  \mmember{}  \{info':\mBbbZ{}  \mtimes{}  Id  \mtimes{}  Id  \mtimes{}  pMsg(P.M[P])?|  info'  =  (inl  <<x5,  x6>,  x3,  x4>)\} 


By

---

Latex:
RepeatFor  3  ((CallByValueReduce  0  THENA  Auto))

---

Home Index