Nuprl Lemma : filter-normal-form
∀[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 :
filter: filter(P;l),
list_ind: list_ind,
cons: [a / b],
nil: [],
ifthenelse: if b then t else f fi ,
uall: ∀[x:A]. B[x],
top: Top,
so_apply: x[s],
lambda: λx.A[x],
sqequal: s ~ t
Definitions :
nil: [],
it: ⋅,
ifthenelse: if b then t else f fi ,
so_apply: x[s],
cons: [a / b],
filter: filter(P;l),
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:
2015_07_17-AM-09_15_13
Last ObjectModification:
2015_02_02-PM-06_30_43
Home
Index