---

Step * of Lemma pi-system_wf

∀[f:(Id List) ⟶ Id]. ∀[l_server,l_choose,l_comm,l_pi:Id].
  (pi-system(f;l_server;l_choose;l_comm;l_pi) ∈ pi_term() ⟶ System(P.piM(P)))
BY
{ ProveWfLemma }

1
1. f : (Id List) ⟶ Id
2. l_server : Id
3. l_choose : Id
4. l_comm : Id
5. l_pi : Id
6. P : pi_term()@i
⊢ <"msg", pDVfire()> ∈ pCom(P.piM(P))

---

Latex:

---

Latex:
\mforall{}[f:(Id  List)  {}\mrightarrow{}  Id].  \mforall{}[l$_{server}$,l$_{choose}$,l$\mbackslash{}ff5\000Cf{comm}$,l$_{pi}$:Id].
    (pi-system(f;l$_{server}$;l$_{choose}$;l$_{com\000Cm}$;l$_{pi}$)  \mmember{}  pi\_term()  {}\mrightarrow{}  System(P.piM(P)))


By

---

Latex:
ProveWfLemma

---

Home Index