Step * 1 1 of Lemma msg-rename_wf


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

1
1. IdLnk ─→ Id ─→ Type
2. rt Id ─→ Id
3. rtinv Id ─→ (Id?)
4. inv-rel(Id;Id;rt;rtinv)
5. IdLnk
6. Id
7. m2 t
8. ↑isl(rtinv t)
⊢ m2 ∈ (rt outl(rtinv 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.  l  :  IdLnk
6.  t  :  Id
7.  m2  :  M  l  t
8.  \muparrow{}isl(rtinv  mtag(<l,  t,  m2>))
\mvdash{}  <l,  outl(rtinv  t),  m2>  \mmember{}  l:IdLnk  \mtimes{}  t:Id  \mtimes{}  (M  l  (rt  t))


By

((Unfold  `mtag`  (-1))  THEN  (Reduce  (-1))  THEN  Auto)




Home Index