---

st_exp_ind(x)
var(name)=>var[name]
const(val)=>const[val]
fun(arg)=>rec1,rec2.ap[fun; arg; rec1; rec2]
bound:type.body=>rec1.lambda[bound; type; body; rec1] ==
  Y 
  (st_exp_ind,x.
    case x
    of inl(x) =>
     var[x]
     | inr(x) =>
     case x
     of inl(x) =>
      const[x]
      | inr(x) =>
      case x
      of inl(x) =>
       ap[fst(x); snd(x); st_exp_ind (fst(x)); st_exp_ind (snd(x))]
       | inr(x) =>
       lambda[fst(x); fst(snd(x)); snd(snd(x)); st_exp_ind (snd(snd(x)))]) 
  x

---

Definitions occuring in Statement :  pi1: fst(t),  pi2: snd(t),  ycomb: Y,  apply: f a,  lambda: x.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y]
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 :  st_exp_ind st_exp_ind

---

st\_exp\_ind(x)
var(name)=>var[name]
const(val)=>const[val]
fun(arg)=>rec1,rec2.ap[fun;  arg;  rec1;  rec2]
\mlambda{}bound:type.body=>rec1.lambda[bound;  type;  body;  rec1]  ==
    Y 
    (\mlambda{}st\_exp$_{ind}$,x.
        case  x
        of  inl(x)  =>
          var[x]
          |  inr(x)  =>
          case  x
          of  inl(x)  =>
            const[x]
            |  inr(x)  =>
            case  x
            of  inl(x)  =>
              ap[fst(x);  snd(x);  st\_exp$_{ind}$  (fst(x));  st\_exp$_{ind}\000C$  (snd(x))]
              |  inr(x)  =>
              lambda[fst(x);  fst(snd(x));  snd(snd(x));  st\_exp$_{ind}$  (snd(snd(x)))]) 
    x


Date html generated: 2011_08_17-PM-05_03_07
Last ObjectModification: 2011_02_04-AM-11_56_23

Home Index