---

{ [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)) }

{ Proof }

---

Definitions occuring in Statement :  Comm-process-q: Comm-process-q(q;id;st),  pi_prefix: pi_prefix(),  fpf: a:A fp-> B[a],  Id: Id,  name: Name,  nat: ,  uall: [x:A]. B[x],  member: t  T,  product: x:A  B[x],  list: type List
Definitions :  uall: [x:A]. B[x],  member: t  T,  Comm-process-q: Comm-process-q(q;id;st),  so_lambda: x.t[x],  so_apply: x[s]
Lemmas :  Comm-process-q_aux_wf,  fpf_wf,  Id_wf,  pi_prefix_wf

---

\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))


Date html generated: 2011_08_17-PM-07_02_28
Last ObjectModification: 2011_06_18-PM-12_43_15

Home Index