Nuprl Lemma : mapfilter-cons

[u,v,P,f:Top].  (mapfilter(f;P;[u v]) mapfilter(f;P;[u]) mapfilter(f;P;v))


Proof




Definitions occuring in Statement :  mapfilter: mapfilter(f;P;L) append: as bs cons: [a b] nil: [] uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  append: as bs all: x:A. B[x] so_lambda: so_lambda(x,y,z.t[x; y; z]) member: t ∈ T top: Top so_apply: x[s1;s2;s3] uall: [x:A]. B[x]
Lemmas referenced :  list_ind_cons_lemma list_ind_nil_lemma mapfilter-append top_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis isectElimination hypothesisEquality because_Cache isect_memberFormation introduction sqequalAxiom

Latex:
\mforall{}[u,v,P,f:Top].    (mapfilter(f;P;[u  /  v])  \msim{}  mapfilter(f;P;[u])  @  mapfilter(f;P;v))



Date html generated: 2016_05_14-PM-01_28_47
Last ObjectModification: 2015_12_26-PM-05_21_44

Theory : list_1


Home Index