### 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