---

Step * of Lemma accum-matching-tagged-indices_wf

∀[pre:pi_prefix()]. ∀[st:a:Id fp-> pi_prefix() List].
  (accum-matching-tagged-indices(pre;st) ∈ (Id × ((ℕ × Name) List)) List)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[pre:pi\_prefix()].  \mforall{}[st:a:Id  fp->  pi\_prefix()  List].
    (accum-matching-tagged-indices(pre;st)  \mmember{}  (Id  \mtimes{}  ((\mBbbN{}  \mtimes{}  Name)  List))  List)


By

---

Latex:
ProveWfLemma

---

Home Index