Nuprl Lemma : filter-normal-form

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


Definitions occuring in Statement :  filter: filter(P;l) list_ind: list_ind cons: [a b] nil: [] ifthenelse: if then else fi  uall: [x:A]. B[x] top: Top so_apply: x[s] lambda: λx.A[x] sqequal: t
Definitions :  nil: [] it: ifthenelse: if then else fi  so_apply: x[s] cons: [a b] filter: filter(P;l) reduce: reduce(f;k;as)
Lemmas :  top_wf
    (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: 2015_07_17-AM-09_15_13
Last ObjectModification: 2015_02_02-PM-06_30_43

Home Index