Nuprl Lemma : mapfilter-bor-eq
T,U:Type. f:T 
U. P,Q:T 
. L:T List.
((mapfilter(f;P;L) @ mapfilter(f;Q;L)) = (mapfilter(f;
x.(P[x] 
Q[x]);L) @ mapfilter(f;x.(P[x] 
Q[x]);L)))
Proof not projected
Definitions occuring in Statement :
append: as @ bs,
bor: p q,
band: p q,
bool: ,
so_apply: x[s],
all: x:A. B[x],
lambda: x.A[x],
function: x:A B[x],
list: type List,
universe: Type,
equal: s = t,
mapfilter: mapfilter(f;P;L),
bag: bag(T)
Definitions :
all: x:A. B[x],
bag: bag(T),
append: as @ bs,
mapfilter: mapfilter(f;P;L),
so_apply: x[s],
map: map(f;as),
filter: filter(P;l),
reduce: reduce(f;k;as),
ycomb: Y,
member: t 
T,
top: Top,
subtype: S 
T,
suptype: suptype(S; T),
prop: 
,
and: P Q,
cand: A c B,
true: True,
ifthenelse: if b then t else f fi ,
implies: P 
Q,
btrue: tt,
bfalse: ff,
guard: {T},
rev_implies: P 
Q,
iff: P Q,
squash: 
T,
bag-append: as + bs,
cons-bag: x.b,
uall: [x:A]. B[x],
or: P Q,
not: 
A,
false: False,
bool: ,
unit: Unit,
uimplies: b supposing a,
uiff: uiff(P;Q),
it: 
Lemmas :
bag_wf,
bool_wf,
top_wf,
l_member_wf,
bor_wf,
band_wf,
mapfilter-append,
mapfilter-singleton,
equal_wf,
assert_wf,
or_wf,
bnot_wf,
not_wf,
cons-bag_wf,
eqtt_to_assert,
uiff_transitivity,
eqff_to_assert,
assert_of_bnot,
assert_of_bor,
assert_functionality_wrt_uiff,
bnot_thru_bor,
assert_of_band,
and_functionality_wrt_uiff,
iff_transitivity,
iff_weakening_uiff,
bnot_thru_band,
or_functionality_wrt_uiff,
squash_wf,
true_wf,
bag-append-assoc,
mapfilter_wf,
bag_qinc,
bag-append-comm,
append_wf,
bag-append_wf
\mforall{}T,U:Type. \mforall{}f:T {}\mrightarrow{} U. \mforall{}P,Q:T {}\mrightarrow{} \mBbbB{}. \mforall{}L:T List.
((mapfilter(f;P;L) @ mapfilter(f;Q;L))
= (mapfilter(f;\mlambda{}x.(P[x] \mvee{}\msubb{}Q[x]);L) @ mapfilter(f;\mlambda{}x.(P[x] \mwedge{}\msubb{} Q[x]);L)))
Date html generated:
2012_01_23-PM-12_49_26
Last ObjectModification:
2011_12_01-PM-02_04_42
Home
Index