---

{ [X:{j}]. [x:Expression]. [base:val:Atom  X]. [pair:fst:Expression
                                                             snd:Expression
                                                             rec1:X
                                                             rec2:X
                                                             X].
  [apply:fun:Atom  arg:Expression  rec1:X  X].
    (case(x)
     leaf(val) => base[val]
     pair(fst,snd) => rec1,rec2.pair[fst;snd;rec1;rec2]
     fun(arg) => rec1.apply[fun;arg;rec1]  X) }

{ Proof }

---

Definitions occuring in Statement :  expression_ind: expression_ind,  expression: Expression,  uall: [x:A]. B[x],  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],  atom: Atom,  universe: Type
Definitions :  uall: [x:A]. B[x],  expression: Expression,  member: t  T,  expression_ind: expression_ind,  so_apply: x[s],  so_apply: x[s1;s2;s3;s4],  so_apply: x[s1;s2;s3],  type-monotone: Monotone(T.F[T]),  uimplies: b supposing a,  ycomb: Y,  pi1: fst(t),  pi2: snd(t)
Lemmas :  subtype_rel_sum,  subtype_rel_simple_product,  expression_wf

---

\mforall{}[X:\mBbbU{}\{j\}].  \mforall{}[x:Expression].  \mforall{}[base:val:Atom  {}\mrightarrow{}  X].  \mforall{}[pair:fst:Expression
                                                                                                                    {}\mrightarrow{}  snd:Expression
                                                                                                                    {}\mrightarrow{}  rec1:X
                                                                                                                    {}\mrightarrow{}  rec2:X
                                                                                                                    {}\mrightarrow{}  X].  \mforall{}[apply:fun:Atom
                                                                                                                                                  {}\mrightarrow{}  arg:Expression
                                                                                                                                                  {}\mrightarrow{}  rec1:X
                                                                                                                                                  {}\mrightarrow{}  X].
    (case(x)
      leaf(val)  =>  base[val]
      pair(fst,snd)  =>  rec1,rec2.pair[fst;snd;rec1;rec2]
      fun(arg)  =>  rec1.apply[fun;arg;rec1]  \mmember{}  X)


Date html generated: 2011_08_17-PM-04_33_45
Last ObjectModification: 2011_06_18-AM-11_44_44

Home Index