---

Step * of Lemma Comm-process-q_wf

∀[q:(Id × (pi_prefix() List)) List]. ∀[id:Id]. ∀[st:st:Id fp-> pi_prefix() List].
  (Comm-process-q(q;id;st) ∈ (Id × (pi_prefix() List)) List
   × st:Id fp-> pi_prefix() List
   × Id
   × ((ℕ × Id × ℕ × Name) List))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[q:(Id  \mtimes{}  (pi\_prefix()  List))  List].  \mforall{}[id:Id].  \mforall{}[st:st:Id  fp->  pi\_prefix()  List].
    (Comm-process-q(q;id;st)  \mmember{}  (Id  \mtimes{}  (pi\_prefix()  List))  List
      \mtimes{}  st:Id  fp->  pi\_prefix()  List
      \mtimes{}  Id
      \mtimes{}  ((\mBbbN{}  \mtimes{}  Id  \mtimes{}  \mBbbN{}  \mtimes{}  Name)  List))


By

---

Latex:
ProveWfLemma

---

Home Index