---

{ [P,L:Top].
    (rec-case(L) of
     [] => []
     a::_ =>
      r.if P[a] then [a / r] else r fi  ~ filter(a.P[a];L)) }

{ Proof }

---

Definitions occuring in Statement :  ifthenelse: if b then t else f fi ,  uall: [x:A]. B[x],  top: Top,  so_apply: x[s],  lambda: x.A[x],  list_ind: list_ind def,  cons: [car / cdr],  nil: [],  sqequal: s ~ t,  filter: filter(P;l)
Definitions :  uall: [x:A]. B[x],  ifthenelse: if b then t else f fi ,  so_apply: x[s],  filter: filter(P;l),  member: t  T,  reduce: reduce(f;k;as)
Lemmas :  top_wf

---

\mforall{}[P,L:Top].
    (rec-case(L)  of
      []  =>  []
      a::$_{}$  =>
        r.if  P[a]  then  [a  /  r]  else  r  fi    \msim{}  filter(\mlambda{}a.P[a];L))


Date html generated: 2011_08_10-AM-07_52_51
Last ObjectModification: 2011_06_18-AM-08_14_48

Home Index