---

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

{ Proof }

---

Definitions occuring in Statement :  comm-create: comm-create(c),  com-kind: com-kind(c),  pCom: pCom(P.M[P]),  Process: Process(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 :  prop: ,  pi2: snd(t),  pi1: fst(t),  tagged-val: x.val,  tagged-tag: x.tag,  comm-create: comm-create(c),  member: t  T,  com-kind: com-kind(c),  uimplies: b supposing a,  and: P  Q,  iff: P  Q,  guard: {T},  sq_type: SQType(T),  bfalse: ff,  btrue: tt,  or: P  Q,  all: x:A. B[x],  ifthenelse: if b then t else f fi ,  false: False,  implies: P  Q,  not: A,  uall: [x:A]. B[x],  tag-case: z:T
Lemmas :  not_functionality_wrt_uiff,  assert_of_bnot,  eqff_to_assert,  assert_of_eq_atom,  eqtt_to_assert,  uiff_transitivity,  iff_weakening_uiff,  bool_subtype_base,  subtype_base_sq,  bool_cases,  bnot_wf,  not_wf,  assert_wf,  bool_wf,  eq_atom_wf

---

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


Date html generated: 2011_08_16-PM-06_48_54
Last ObjectModification: 2011_06_18-AM-11_03_10

Home Index