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:
es-LnkTag-deq \mmember{} EqDecider(IdLnk \mtimes{} 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)
Home
Index