---

{ [M:Type  Type]
    [Q:Type]
      [m:pMsg(T.M[T])]. (mk-tagged("msg";m)  Com(P.M[P]) Q) 
      supposing Process(P.M[P]) r Q 
    supposing Monotone(T.M[T]) }

{ Proof }

---

Definitions occuring in Statement :  pMsg: pMsg(P.M[P]),  Process: Process(P.M[P]),  Com: Com(P.M[P]),  type-monotone: Monotone(T.F[T]),  subtype_rel: A r B,  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s],  member: t  T,  apply: f a,  function: x:A  B[x],  token: "$token",  universe: Type,  mk-tagged: mk-tagged(tg;x)
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  so_apply: x[s],  pMsg: pMsg(P.M[P]),  member: t  T,  Com: Com(P.M[P]),  tagged+: T |+ z:B,  isect2: T1  T2,  ifthenelse: if b then t else f fi ,  btrue: tt,  bfalse: ff,  not: A,  top: Top,  assert: b,  eq_atom: x =a y,  implies: P  Q,  so_lambda: x.t[x],  unit: Unit,  bool: ,  rev_implies: P  Q,  iff: P  Q,  and: P  Q,  false: False,  type-monotone: Monotone(T.F[T]),  it: ,  prop: ,  guard: {T}
Lemmas :  mk-tagged_wf,  mk-tagged_wf_unequal,  iff_weakening_uiff,  not_wf,  assert_wf,  eq_atom_wf,  not_functionality_wrt_uiff,  uiff_inversion,  assert_of_eq_atom,  false_wf,  Id_wf,  unit_wf,  bool_wf,  Process_wf,  type-monotone_wf

---

\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}[Q:Type].  \mforall{}[m:pMsg(T.M[T])].  (mk-tagged("msg";m)  \mmember{}  Com(P.M[P])  Q)  supposing  Process(P.M[P])  \msubseteq{}r  Q 
    supposing  Monotone(T.M[T])


Date html generated: 2011_08_16-PM-06_47_57
Last ObjectModification: 2011_06_18-AM-11_00_21

Home Index