---

{ ds1,ds2:x:Id fp-> Type.  (Normal(ds1)  Normal(ds2)  Normal(ds1  ds2)) }

{ Proof }

---

Definitions occuring in Statement :  normal-ds: Normal(ds),  fpf-join: f  g,  fpf: a:A fp-> B[a],  id-deq: IdDeq,  Id: Id,  all: x:A. B[x],  implies: P  Q,  universe: Type
Definitions :  member: t  T,  prop: ,  ifthenelse: if b then t else f fi ,  top: Top,  normal-ds: Normal(ds),  fpf-all: xdom(f). v=f(x)   P[x; v],  implies: P  Q,  btrue: tt,  so_lambda: x.t[x],  bfalse: ff,  all: x:A. B[x],  false: False,  not: A,  or: P  Q,  bool: ,  iff: P  Q,  unit: Unit,  so_apply: x[s],  and: P  Q,  it:
Lemmas :  fpf-dom_wf,  assert_wf,  not_wf,  bnot_wf,  bool_wf,  iff_transitivity,  normal-ds_wf,  fpf-join-dom,  fpf-join_wf,  eqff_to_assert,  Id_wf,  eqtt_to_assert,  top_wf,  id-deq_wf,  fpf-trivial-subtype-top,  fpf-join-ap-sq,  assert_of_bnot,  fpf_wf

---

\mforall{}ds1,ds2:x:Id  fp->  Type.    (Normal(ds1)  {}\mRightarrow{}  Normal(ds2)  {}\mRightarrow{}  Normal(ds1  \moplus{}  ds2))


Date html generated: 2010_08_27-AM-12_03_49
Last ObjectModification: 2008_02_27-PM-09_50_01

Home Index