Nuprl Lemma : mapfilter-mapfilter1

[f1,P2,f2,P1,as:Top].  (mapfilter(f1;P1;mapfilter(f2;P2;as)) mapfilter(f1 f2;λa.((P2 a) ∧b (P1 (f2 a)));as))


Proof




Definitions occuring in Statement :  mapfilter: mapfilter(f;P;L) compose: g band: p ∧b q uall: [x:A]. B[x] top: Top apply: a lambda: λx.A[x] sqequal: t
Definitions unfolded in proof :  mapfilter: mapfilter(f;P;L) member: t ∈ T top: Top compose: 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,P2,f2,P1,as: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_02
Last ObjectModification: 2015_12_26-PM-05_22_06

Theory : list_1


Home Index