---

{ [l_comm,l_choose:Id]. [piD:PiDataVal()]. [cSt:Comm-state()].
    Comm-next-continue(l_comm;l_choose;piD;cSt)  Comm-output() 
    supposing pDVcontinue?(piD) }

{ Proof }

---

Definitions occuring in Statement :  Comm-next-continue: Comm-next-continue(l_comm;l_choose;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],  uimplies: b supposing a,  member: t  T,  Comm-output: Comm-output(),  Comm-next-continue: Comm-next-continue(l_comm;l_choose;piD;cSt),  let: let,  append: as @ bs,  Comm-state: Comm-state(),  ifthenelse: if b then t else f fi ,  bfalse: ff,  btrue: tt,  all: x:A. B[x],  implies: P  Q,  prop: ,  top: Top,  subtype: S  T,  so_lambda: x.t[x],  nat: ,  bool: ,  unit: Unit,  iff: P  Q,  and: P  Q,  so_apply: x[s],  it:
Lemmas :  assert_wf,  pDVcontinue?_wf,  Comm-state_wf,  PiDataVal_wf,  Id_wf,  Comm-waiting_wf,  bool_wf,  iff_weakening_uiff,  eqtt_to_assert,  make-lg_wf_dag,  tag-by_wf,  not_wf,  uiff_transitivity,  bnot_wf,  eqff_to_assert,  assert_of_bnot,  null_wf3,  pi1_wf_top,  top_wf,  Comm-process-q_wf,  Comm-q_wf,  Comm-st_wf,  pi_prefix_wf,  fpf_wf,  nat_wf,  name_wf,  assert_of_null,  pi2_wf,  bfalse_wf,  Comm-count_wf,  not_functionality_wrt_uiff,  mk-tagged_wf2,  pDVcontinue_wf,  map_wf,  pDVrequest_wf,  btrue_wf,  le_wf

---

\mforall{}[l$_{comm}$,l$_{choose}$:Id].  \mforall{}[piD:PiDataVal()].  \mforall{}[cSt:Com\000Cm-state()].
    Comm-next-continue(l$_{comm}$;l$_{choose}$;piD;cSt)  \mmember{}  Comm\000C-output()  supposing  \muparrow{}pDVcontinue?(piD)


Date html generated: 2011_08_17-PM-07_02_41
Last ObjectModification: 2011_06_18-PM-12_44_37

Home Index