---

Step * of Lemma accum-matching-indices_wf

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

---

Latex:

---

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


By

---

Latex:
ProveWfLemma

---

Home Index