---

Step * 1 of Lemma msg-rename_wf


1. M : IdLnk ─→ Id ─→ Type
2. rt : Id ─→ Id
3. rtinv : Id ─→ (Id?)
4. inv-rel(Id;Id;rt;rtinv)
5. m : Msg(M)
6. ↑isl(rtinv mtag(m))
⊢ msg-rename(rtinv;m) ∈ Msg(λl,tg. (M l (rt tg)))
BY
{ (DVar `m' THEN DVar `m1' THEN Unfolds ``msg-rename Msg`` 0 THEN Reduce 0) }

1
1. M : IdLnk ─→ Id ─→ Type
2. rt : Id ─→ Id
3. rtinv : Id ─→ (Id?)
4. inv-rel(Id;Id;rt;rtinv)
5. l : IdLnk
6. t : Id
7. m2 : M l t
8. ↑isl(rtinv mtag(<l, t, m2>))
⊢ <l, outl(rtinv t), m2> ∈ l:IdLnk × t:Id × (M l (rt t))

---

Latex:



1.  M  :  IdLnk  {}\mrightarrow{}  Id  {}\mrightarrow{}  Type
2.  rt  :  Id  {}\mrightarrow{}  Id
3.  rtinv  :  Id  {}\mrightarrow{}  (Id?)
4.  inv-rel(Id;Id;rt;rtinv)
5.  m  :  Msg(M)
6.  \muparrow{}isl(rtinv  mtag(m))
\mvdash{}  msg-rename(rtinv;m)  \mmember{}  Msg(\mlambda{}l,tg.  (M  l  (rt  tg)))


By

(DVar  `m'  THEN  DVar  `m1'  THEN  Unfolds  ``msg-rename  Msg``  0  THEN  Reduce  0)

---

Home Index