Nuprl Lemma : mapfilter-mapfilter
∀[f1,as,P2,f2,P1:Top]. (mapfilter(f1;P1;mapfilter(f2;P2;as)) ~ mapfilter(f1 o f2;λa.((P2 a) ∧b (P1 (f2 a)));as))
Proof
Definitions occuring in Statement :
mapfilter: mapfilter(f;P;L),
compose: f o g,
band: p ∧b q,
uall: ∀[x:A]. B[x],
top: Top,
apply: f a,
lambda: λx.A[x],
sqequal: s ~ t
Definitions unfolded in proof :
mapfilter: mapfilter(f;P;L),
member: t ∈ T,
top: Top,
compose: f o g,
uall: ∀[x:A]. B[x]
Lemmas referenced :
top_wf,
filter-map,
filter-filter,
map-map
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
hypothesisEquality,
isect_memberEquality,
voidElimination,
voidEquality,
sqequalRule,
cut,
lemma_by_obid,
hypothesis,
because_Cache,
isect_memberFormation,
introduction,
sqequalAxiom,
sqequalHypSubstitution,
isectElimination,
thin
Latex:
\mforall{}[f1,as,P2,f2,P1:Top].
(mapfilter(f1;P1;mapfilter(f2;P2;as)) \msim{} mapfilter(f1 o f2;\mlambda{}a.((P2 a) \mwedge{}\msubb{} (P1 (f2 a)));as))
Date html generated:
2016_05_14-PM-01_29_07
Last ObjectModification:
2015_12_26-PM-05_22_02
Theory : list_1
Home
Index