---

{ [X:{j}]. [x:esharp_exp()]. [var:name:Atom  X]. [basic:val:Base  X].
  [op:name:Atom  X]. [apply:fun:esharp_exp()
                                 arg:esharp_exp()
                                 rec1:X
                                 rec2:X
                                 X]. [lambda:var:Atom
                                                 body:esharp_exp()
                                                 rec1:X
                                                 X].
  [let:lhs:E#Lhs
         rsh:esharp_exp()
         body:esharp_exp()
         rec1:X
         rec2:X
         X].
    (case(x)
       var(name)=>var[name]
       basic(val)=>basic[val]
       operator(name)=>op[name]
       fun(arg)=>rec1,rec2.apply[fun;arg;rec1;rec2]
       lambda v1. body=>rec1.lambda[v1;body;rec1]
       let lhs = rsh in body=> rec1,rec2.let[lhs;rsh;body;rec1;rec2])  X) }

{ Proof }

---

Definitions occuring in Statement :  esharp_exp_ind: esharp_exp_ind,  esharp_exp: esharp_exp(),  esharp-lhs: E#Lhs,  uall: [x:A]. B[x],  so_apply: x[s1;s2;s3;s4;s5],  so_apply: x[s1;s2;s3;s4],  so_apply: x[s1;s2;s3],  so_apply: x[s],  member: t  T,  function: x:A  B[x],  base: Base,  atom: Atom,  universe: Type
Definitions :  type-expr: Error :type-expr,  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;s3;s4;s5],  so_apply: x[s1;s2;s3],  so_apply: x[s1;s2;s3;s4],  apply: f a,  so_apply: x[s],  esharp_exp_ind: esharp_exp_ind,  equal: s = t,  so_lambda: x.t[x],  member: t  T,  prop: ,  esharp-lhs: E#Lhs,  base: Base,  function: x:A  B[x],  atom: Atom,  esharp_exp: esharp_exp(),  universe: Type,  uall: [x:A]. B[x],  isect: x:A. B[x]
Lemmas :  esharp_exp_wf,  base_wf,  uall_wf,  esharp-lhs_wf,  member_wf,  type-monotone_wf,  subtype_rel_wf,  subtype_rel_sum,  subtype_rel_simple_product

---

\mforall{}[X:\mBbbU{}\{j\}].  \mforall{}[x:esharp\_exp()].  \mforall{}[var:name:Atom  {}\mrightarrow{}  X].  \mforall{}[basic:val:Base  {}\mrightarrow{}  X].  \mforall{}[op:name:Atom  {}\mrightarrow{}  X].
\mforall{}[apply:fun:esharp\_exp()  {}\mrightarrow{}  arg:esharp\_exp()  {}\mrightarrow{}  rec1:X  {}\mrightarrow{}  rec2:X  {}\mrightarrow{}  X].
\mforall{}[lambda:var:Atom  {}\mrightarrow{}  body:esharp\_exp()  {}\mrightarrow{}  rec1:X  {}\mrightarrow{}  X].  \mforall{}[let:lhs:E\#Lhs
                                                                                                                            {}\mrightarrow{}  rsh:esharp\_exp()
                                                                                                                            {}\mrightarrow{}  body:esharp\_exp()
                                                                                                                            {}\mrightarrow{}  rec1:X
                                                                                                                            {}\mrightarrow{}  rec2:X
                                                                                                                            {}\mrightarrow{}  X].
    (case(x)
          var(name)=>var[name]
          basic(val)=>basic[val]
          operator(name)=>op[name]
          fun(arg)=>rec1,rec2.apply[fun;arg;rec1;rec2]
          lambda  v1.  body=>rec1.lambda[v1;body;rec1]
          let  lhs  =  rsh  in  body=>  rec1,rec2.let[lhs;rsh;body;rec1;rec2])  \mmember{}  X)


Date html generated: 2011_08_17-PM-05_14_23
Last ObjectModification: 2011_02_03-PM-04_33_13

Home Index