---

{ [compList:(pi_prefix()  Pi_term) List].
  [g:{Q:Pi_term| (CcompList. pi-rank(Q)  pi-rank(snd(C)))} 
       Id
       Name
       Name List
       pi-process()].
    (pi-guarded-trans(compList;g)  Id  Name  Name List  pi-process()) }

{ Proof }

---

Definitions occuring in Statement :  pi-guarded-trans: pi-guarded-trans(compList;g),  pi-process: pi-process(),  pi-rank: pi-rank(p),  pi_term: Pi_term,  pi_prefix: pi_prefix(),  Id: Id,  name: Name,  uall: [x:A]. B[x],  pi2: snd(t),  le: A  B,  member: t  T,  set: {x:A| B[x]} ,  function: x:A  B[x],  product: x:A  B[x],  list: type List,  l_exists: (xL. P[x])
Definitions :  top: Top,  member: t  T,  pi-process: pi-process(),  pMsg: pMsg(P.M[P]),  piM: piM(T),  uall: [x:A]. B[x]
Lemmas :  top_wf,  pi-guarded-aux_wf,  pDVfire_wf

---

\mforall{}[compList:(pi\_prefix()  \mtimes{}  Pi\_term)  List].  \mforall{}[g:\{Q:Pi\_term| 
                                                                                              (\mexists{}C\mmember{}compList.  pi-rank(Q)  \mleq{}  pi-rank(snd(C)))\} 
                                                                                            {}\mrightarrow{}  Id
                                                                                            {}\mrightarrow{}  Name
                                                                                            {}\mrightarrow{}  Name  List
                                                                                            {}\mrightarrow{}  pi-process()].
    (pi-guarded-trans(compList;g)  \mmember{}  Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  Name  List  {}\mrightarrow{}  pi-process())


Date html generated: 2011_08_17-PM-07_04_08
Last ObjectModification: 2011_06_18-PM-12_46_17

Home Index