---

Step * of Lemma norm-runinfo_wf

∀[M:Type ⟶ Type]
  ∀[info:pRunInfo(P.M[P])]. (norm-runinfo(info) ∈ {info':pRunInfo(P.M[P])| info' = info ∈ pRunInfo(P.M[P])} ) 
  supposing ∀P:Type. value-type(M[P])
BY
{ (Auto THEN D -1 THEN RepUR ``norm-runinfo`` 0) }

1
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])} 

2
1. M : Type ⟶ Type
2. ∀P:Type. value-type(M[P])
3. y : Unit
⊢ inr ⋅  ∈ {info':pRunInfo(P.M[P])| info' = (inr y ) ∈ pRunInfo(P.M[P])} 

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}[info:pRunInfo(P.M[P])].  (norm-runinfo(info)  \mmember{}  \{info':pRunInfo(P.M[P])|  info'  =  info\}  ) 
    supposing  \mforall{}P:Type.  value-type(M[P])


By

---

Latex:
(Auto  THEN  D  -1  THEN  RepUR  ``norm-runinfo``  0)

---

Home Index