---

case(x)
leaf(val) => base[val]
pair(fst,snd) => rec1,rec2.pair[fst; snd; rec1; rec2]
fun(arg) => rec1.apply[fun; arg; rec1] ==
  Y 
  (expression_ind,x.
    case x
    of inl(x) => base[x]
     | inr(x) => case x
                 of inl(x) => pair[fst(x); snd(x); expression_ind 
                                                   (fst(x)); expression_ind 
                                                             (snd(x))]
                  | inr(x) => apply[fst(x); snd(x); expression_ind (snd(x))]) 
  x

---

Definitions :  ycomb: Y,  lambda: x.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  pi1: fst(t),  apply: f a,  pi2: snd(t)
FDL editor aliases :  expression_ind expression_ind

---

case(x)
leaf(val)  =>  base[val]
pair(fst,snd)  =>  rec1,rec2.pair[fst;  snd;  rec1;  rec2]
fun(arg)  =>  rec1.apply[fun;  arg;  rec1]  ==
    Y 
    (\mlambda{}expression$_{ind}$,x.
        case  x
        of  inl(x)  =>  base[x]
          |  inr(x)  =>  case  x
                                  of  inl(x)  =>  pair[fst(x);  snd(x);  expression$_{ind}$  (fst(x));  \000C
expression$_{ind}$  (snd(x))]
                                    |  inr(x)  =>  apply[fst(x);  snd(x);  expression$_{ind}$  (snd(x))]\000C
) 
    x


Date html generated: 2010_08_27-PM-08_21_27
Last ObjectModification: 2010_06_22-PM-12_58_09

Home Index