---

{ [X:{j}]. [x:SimpleType]. [var:name:Atom  X]. [const:ty:Type  X].
  [arrow,prod,union:left:SimpleType
                      right:SimpleType
                      rec1:X
                      rec2:X
                      X]. [list,class:kind:SimpleType  rec1:X  X].
    (case(x)
     var(name)=>var[name]
     const(ty)=>const[ty]
     domainrange =>rec1,rec2.arrow[domain;range;rec1;rec2]
     fst  snd =>rec1,rec2.prod[fst;snd;rec1;rec2]
     left + right =>rec1,rec2.union[left;right;rec1;rec2]
     kind list =>rec1.list[kind;rec1]
     Class(kind) =>rec1.class[kind;rec1]  X) }

{ Proof }

---

Definitions occuring in Statement :  simple_type_ind: simple_type_ind,  simple_type: SimpleType,  uall: [x:A]. B[x],  so_apply: x[s1;s2;s3;s4],  so_apply: x[s1;s2],  so_apply: x[s],  member: t  T,  function: x:A  B[x],  atom: Atom,  universe: Type
Definitions :  fpf: a:A fp-> B[a],  strong-subtype: strong-subtype(A;B),  le: A  B,  ge: i  j ,  not: A,  less_than: a < b,  tag-by: zT,  ldag: LabeledDAG(T),  labeled-graph: LabeledGraph(T),  record+: record+,  record: record(x.T[x]),  eclass: EClass(A[eo; e]),  fset: FSet{T},  dataflow: dataflow(A;B),  isect2: T1  T2,  b-union: A  B,  rev_implies: P  Q,  or: P  Q,  implies: P  Q,  iff: P  Q,  uiff: uiff(P;Q),  and: P  Q,  bag: bag(T),  list: type List,  set: {x:A| B[x]} ,  top: Top,  true: True,  subtype_rel: A r B,  uimplies: b supposing a,  type-monotone: Monotone(T.F[T]),  product: x:A  B[x],  union: left + right,  rec: rec(x.A[x]),  all: x:A. B[x],  axiom: Ax,  so_apply: x[s1;s2],  so_apply: x[s1;s2;s3;s4],  apply: f a,  so_apply: x[s],  simple_type_ind: simple_type_ind,  equal: s = t,  isect: x:A. B[x],  uall: [x:A]. B[x],  so_lambda: x.t[x],  member: t  T,  prop: ,  simple_type: SimpleType,  universe: Type,  function: x:A  B[x],  atom: Atom
Lemmas :  uall_wf,  simple_type_wf,  member_wf,  type-monotone_wf,  subtype_rel_wf,  subtype_rel_sum,  subtype_rel_simple_product

---

\mforall{}[X:\mBbbU{}\{j\}].  \mforall{}[x:SimpleType].  \mforall{}[var:name:Atom  {}\mrightarrow{}  X].  \mforall{}[const:ty:Type  {}\mrightarrow{}  X].
\mforall{}[arrow,prod,union:left:SimpleType  {}\mrightarrow{}  right:SimpleType  {}\mrightarrow{}  rec1:X  {}\mrightarrow{}  rec2:X  {}\mrightarrow{}  X].
\mforall{}[list,class:kind:SimpleType  {}\mrightarrow{}  rec1:X  {}\mrightarrow{}  X].
    (case(x)
      var(name)=>var[name]
      const(ty)=>const[ty]
      domain{}\mrightarrow{}range  =>rec1,rec2.arrow[domain;range;rec1;rec2]
      fst  \mtimes{}  snd  =>rec1,rec2.prod[fst;snd;rec1;rec2]
      left  +  right  =>rec1,rec2.union[left;right;rec1;rec2]
      kind  list  =>rec1.list[kind;rec1]
      Class(kind)  =>rec1.class[kind;rec1]  \mmember{}  X)


Date html generated: 2011_08_17-PM-04_42_20
Last ObjectModification: 2011_02_06-PM-04_03_35

Home Index