---

{ [M:Type  Type]. [c:pCom(P.M[P])].
    comm-msg(c)  pMsg(P.M[P]) supposing com-kind(c) = "msg" }

{ Proof }

---

Definitions occuring in Statement :  comm-msg: comm-msg(c),  com-kind: com-kind(c),  pCom: pCom(P.M[P]),  pMsg: pMsg(P.M[P]),  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s],  member: t  T,  function: x:A  B[x],  token: "$token",  atom: Atom,  universe: Type,  equal: s = t
Definitions :  uall: [x:A]. B[x],  so_apply: x[s],  uimplies: b supposing a,  member: t  T,  so_lambda: x.t[x],  all: x:A. B[x],  implies: P  Q,  prop: ,  pMsg: pMsg(P.M[P]),  and: P  Q,  com-kind: com-kind(c),  comm-msg: comm-msg(c),  tagged-tag: x.tag,  tagged-val: x.val,  pi1: fst(t),  pi2: snd(t),  pCom: pCom(P.M[P]),  Com: Com(P.M[P]),  tagged+: T |+ z:B,  tag-case: z:T,  not: A,  false: False,  ifthenelse: if b then t else f fi ,  or: P  Q,  btrue: tt,  bfalse: ff,  sq_type: SQType(T),  guard: {T},  iff: P  Q
Lemmas :  tag-case_wf,  pMsg_wf,  pCom_wf,  com-kind_wf,  isect2_decomp,  isect2_wf,  Process_wf,  Id_wf,  unit_wf,  eq_atom_wf,  bool_wf,  assert_wf,  not_wf,  bnot_wf,  bool_cases,  subtype_base_sq,  bool_subtype_base,  iff_weakening_uiff,  uiff_transitivity,  eqtt_to_assert,  assert_of_eq_atom,  eqff_to_assert,  assert_of_bnot,  not_functionality_wrt_uiff

---

\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[c:pCom(P.M[P])].    comm-msg(c)  \mmember{}  pMsg(P.M[P])  supposing  com-kind(c)  =  "msg"


Date html generated: 2011_08_16-PM-06_48_44
Last ObjectModification: 2011_06_18-AM-11_03_00

Home Index