---

{ ClassDerivation  ' }

{ Proof }

---

Definitions occuring in Statement :  classderiv: ClassDerivation,  member: t  T,  universe: Type
Definitions :  universe: Type,  member: t  T,  equal: s = t,  function: x:A  B[x],  subtype_rel: A r B,  top: Top,  union: left + right,  lambda: x.A[x],  product: x:A  B[x],  all: x:A. B[x],  unit: Unit,  implies: P  Q,  or: P  Q,  rev_implies: P  Q,  and: P  Q,  iff: P  Q,  true: True,  ldag: LabeledDAG(T),  tag-by: zT,  labeled-graph: LabeledGraph(T),  record: record(x.T[x]),  isect2: T1  T2,  record+: record+,  eclass: EClass(A[eo; e]),  fset: fset(T),  isect: x:A. B[x],  b-union: A  B,  list: type List,  set: {x:A| B[x]} ,  so_lambda: x.t[x],  base-deriv: BaseDef,  type-monotone: Monotone(T.F[T]),  rec: rec(x.A[x]),  classderiv: ClassDerivation
Lemmas :  type-monotone_wf,  base-deriv_wf,  subtype_rel_sum,  subtype_rel_product,  subtype_rel_simple_product,  subtype_rel_wf,  unit_wf,  top_wf

---

ClassDerivation  \mmember{}  \mBbbU{}'


Date html generated: 2010_08_27-PM-08_07_45
Last ObjectModification: 2010_06_18-PM-04_20_33

Home Index