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 unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
list_ind: list_ind,
ifthenelse: if b then t else f fi ,
so_apply: x[s],
cons: [a / b],
nil: [],
it: ⋅,
filter: filter(P;l),
reduce: reduce(f;k;as)
Latex:
\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:
2016_05_16-AM-11_02_13
Last ObjectModification:
2016_01_07-PM-11_53_48
Theory : event-ordering
Home
Index