---

Step * 1 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 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])?)} 
BY
{ Assert ⌈(x4)↓⌉⋅ }

1
.....assertion..... 
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])
⊢ (x4)↓

2
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])
7. (x4)↓
⊢ 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  ms'  =  x4  in
    inl  <<x5,  x6>,  x3,  ms'>  \mmember{}  \{info':\mBbbZ{}  \mtimes{}  Id  \mtimes{}  Id  \mtimes{}  pMsg(P.M[P])?|  info'  =  (inl  <<x5,  x6>,  x3,  x4>)\} 


By

---

Latex:
Assert  \mkleeneopen{}(x4)\mdownarrow{}\mkleeneclose{}\mcdot{}

---

Home Index