---

Step * of Lemma tagged-messages_wf

∀[S,V:Type]. ∀[M:IdLnk ─→ Id ─→ Type]. ∀[l:IdLnk]. ∀[s:S]. ∀[v:V]. ∀[L:(t:Id × (S ─→ V ─→ (M[l;t] List))) List].
  (tagged-messages(l;s;v;L) ∈ {m:Msg(M)| mlnk(m) = l ∈ IdLnk}  List)
BY
{ (Auto THEN Unfold `tagged-messages` 0 THEN Auto THEN Unfold `Msg` 0 THEN Auto) }

---

Latex:


\mforall{}[S,V:Type].  \mforall{}[M:IdLnk  {}\mrightarrow{}  Id  {}\mrightarrow{}  Type].  \mforall{}[l:IdLnk].  \mforall{}[s:S].  \mforall{}[v:V].
\mforall{}[L:(t:Id  \mtimes{}  (S  {}\mrightarrow{}  V  {}\mrightarrow{}  (M[l;t]  List)))  List].
    (tagged-messages(l;s;v;L)  \mmember{}  \{m:Msg(M)|  mlnk(m)  =  l\}    List)


By

(Auto  THEN  Unfold  `tagged-messages`  0  THEN  Auto  THEN  Unfold  `Msg`  0  THEN  Auto)

---

Home Index