---

Step * of Lemma es-LnkTag-deq_wf

es-LnkTag-deq ∈ EqDecider(IdLnk × Id)
BY
{ (Unfold `es-LnkTag-deq` 0
   THEN Auto
   THEN D 1
   THEN Unfold `event_system_typename` 1
   THEN Unfolds ``es-types es-Lnk es-Tag`` 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
es-LnkTag-deq  \mmember{}  EqDecider(IdLnk  \mtimes{}  Id)


By

---

Latex:
(Unfold  `es-LnkTag-deq`  0
  THEN  Auto
  THEN  D  1
  THEN  Unfold  `event\_system\_typename`  1
  THEN  Unfolds  ``es-types  es-Lnk  es-Tag``  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index