---

{ [l_comm:Id]. [piD:PiDataVal()]. [cSt:Comm-state()].
    Comm-next-guards(l_comm;piD;cSt)  Comm-output() 
    supposing pDVguards?(piD) }

{ Proof }

---

Definitions occuring in Statement :  Comm-next-guards: Comm-next-guards(l_comm;piD;cSt),  Comm-output: Comm-output(),  Comm-state: Comm-state(),  PiDataVal: PiDataVal(),  Id: Id,  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  member: t  T
Definitions :  uall: [x:A]. B[x],  Comm-state: Comm-state(),  uimplies: b supposing a,  member: t  T,  Comm-output: Comm-output(),  Comm-next-guards: Comm-next-guards(l_comm;piD;cSt),  prop:
Lemmas :  Comm-st_wf,  append_wf,  Id_wf,  pi_prefix_wf,  Comm-q_wf,  pDVguards-from_wf,  pDVguards-preList_wf,  Comm-req_from_wf,  Comm-waiting_wf,  Comm-count_wf,  make-lg_wf_dag,  tag-by_wf,  mk-tagged_wf2,  pDVcontinue_wf,  assert_wf,  pDVguards?_wf,  Comm-state_wf,  PiDataVal_wf

---

\mforall{}[l$_{comm}$:Id].  \mforall{}[piD:PiDataVal()].  \mforall{}[cSt:Comm-state()].
    Comm-next-guards(l$_{comm}$;piD;cSt)  \mmember{}  Comm-output()  supposing  \muparrow{}pDVguards?(piD\000C)


Date html generated: 2011_08_17-PM-07_01_48
Last ObjectModification: 2011_06_18-PM-12_42_25

Home Index