---

{ [cSt:Comm-state()]. (Comm-st(cSt)  st:Id fp-> pi_prefix() List) }

{ Proof }

---

Definitions occuring in Statement :  Comm-st: Comm-st(cSt),  Comm-state: Comm-state(),  pi_prefix: pi_prefix(),  fpf: a:A fp-> B[a],  Id: Id,  uall: [x:A]. B[x],  member: t  T,  list: type List
Definitions :  uall: [x:A]. B[x],  member: t  T,  Comm-st: Comm-st(cSt),  top: Top,  so_lambda: x.t[x],  Comm-state: Comm-state(),  so_apply: x[s]
Lemmas :  pi1_wf_top,  fpf_wf,  Id_wf,  pi_prefix_wf,  Comm-state_wf

---

\mforall{}[cSt:Comm-state()].  (Comm-st(cSt)  \mmember{}  st:Id  fp->  pi\_prefix()  List)


Date html generated: 2011_08_17-PM-07_00_56
Last ObjectModification: 2011_06_18-PM-12_41_02

Home Index