---

ste-val(ste) ==
  st_exp_ind(ste)
  var(v)=>sigma.(sigma v)
  const(b)=>sigma.(snd(b))
  f(a)=>rf,ra.sigma.(rf sigma (ra sigma))
  x:st.b=>rb.sigma,v.(rb (z.if z =a x then v else sigma z fi ))

---

Definitions occuring in Statement :  st_exp_ind: st_exp_ind,  eq_atom: x =a y,  ifthenelse: if b then t else f fi ,  pi2: snd(t),  apply: f a,  lambda: x.A[x]
Definitions :  st_exp_ind: st_exp_ind,  pi2: snd(t),  lambda: x.A[x],  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  apply: f a
FDL editor aliases :  ste-val

---

ste-val(ste)  ==
    st\_exp\_ind(ste)
    var(v)=>\mlambda{}sigma.(sigma  v)
    const(b)=>\mlambda{}sigma.(snd(b))
    f(a)=>rf,ra.\mlambda{}sigma.(rf  sigma  (ra  sigma))
    \mlambda{}x:st.b=>rb.\mlambda{}sigma,v.(rb  (\mlambda{}z.if  z  =a  x  then  v  else  sigma  z  fi  ))


Date html generated: 2011_08_17-PM-05_10_00
Last ObjectModification: 2011_02_04-PM-03_42_05

Home Index