Nuprl - list 3 jlc Citations of filter

list 3 jlc Sections Support(jlc) Doc

Def filter(f;L) == (letrec filter f L = (Case of L; nil

nil ; h.t

if f(h)

h.filter(f,t) else filter(f,t) fi) ) (f,L)

is mentioned by

Thm* eq:{T=}, P:(T), L:T List, x:T. x(eq) L P(x) x(eq) filter((x.P(x));L) [filter_is_member_lemma]

Thm* eq:{T=}, P:(T), L:T List, x:T. x(eq) filter((x.P(x));L) P(x) [is_member_filter_lemma]

list 3 jlc Sections Support(jlc) Doc

`Thm* eq:{T=}, P:(T), L:T List, x:T. x(eq) L P(x) x(eq) filter((x.P(x));L)`	[filter_is_member_lemma]
`Thm* eq:{T=}, P:(T), L:T List, x:T. x(eq) filter((x.P(x));L) P(x)`	[is_member_filter_lemma]