Nuprl Lemma : filter-list-diff
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L1,L2:T List]. ∀[eq:EqDecider(T)]. (filter(P;L1-L2) ~ filter(P;L1)-filter(P;L2))
Proof
Definitions occuring in Statement :
list-diff: as-bs,
filter: filter(P;l),
list: T List,
deq: EqDecider(T),
bool: 𝔹,
uall: ∀[x:A]. B[x],
function: x:A ⟶ B[x],
universe: Type,
sqequal: s ~ t
Definitions unfolded in proof :
list-diff: as-bs,
top: Top,
member: t ∈ T,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
prop: ℙ,
implies: P ⇒ Q,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
band: p ∧b q,
ifthenelse: if b then t else f fi ,
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
exists: ∃x:A. B[x],
or: P ∨ Q,
sq_type: SQType(T),
guard: {T},
bnot: ¬bb,
assert: ↑b,
bfalse: ff,
false: False,
not: ¬A,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
so_apply: x[s],
cand: A c∧ B
Lemmas referenced :
filter-sq,
l_member_wf,
bnot_wf,
deq-member_wf,
bool_wf,
eqtt_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
eqff_to_assert,
assert-bnot,
assert-deq-member,
filter_wf5,
subtype_rel_dep_function,
subtype_rel_self,
set_wf,
assert_witness,
assert_wf,
not_wf,
member_filter_2,
iff_wf,
band_wf,
bfalse_wf,
assert_elim,
and_wf,
btrue_neq_bfalse,
deq_wf,
list_wf,
filter-filter,
iff_transitivity,
iff_weakening_uiff,
assert_of_band,
assert_of_bnot
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberEquality,
voidElimination,
voidEquality,
sqequalRule,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
lambdaEquality,
lambdaFormation,
cumulativity,
hypothesis,
setElimination,
rename,
unionElimination,
equalityElimination,
productElimination,
independent_isectElimination,
because_Cache,
dependent_pairFormation,
equalityTransitivity,
equalitySymmetry,
promote_hyp,
dependent_functionElimination,
instantiate,
independent_functionElimination,
applyEquality,
functionExtensionality,
setEquality,
independent_pairFormation,
productEquality,
addLevel,
impliesFunctionality,
andLevelFunctionality,
impliesLevelFunctionality,
levelHypothesis,
dependent_set_memberEquality,
applyLambdaEquality,
functionEquality,
universeEquality,
isect_memberFormation,
sqequalAxiom
Latex:
\mforall{}[T:Type]. \mforall{}[P:T {}\mrightarrow{} \mBbbB{}]. \mforall{}[L1,L2:T List]. \mforall{}[eq:EqDecider(T)].
(filter(P;L1-L2) \msim{} filter(P;L1)-filter(P;L2))
Date html generated:
2017_04_17-AM-09_14_58
Last ObjectModification:
2017_02_27-PM-05_20_51
Theory : decidable!equality
Home
Index