Nuprl Lemma : count_wf
∀s:DSet. ∀a:|s|. ∀bs:|s| List. (a #∈ bs ∈ ℤ)
Proof
Definitions occuring in Statement :
count: a #∈ as,
list: T List,
all: ∀x:A. B[x],
member: t ∈ T,
int: ℤ,
dset: DSet,
set_car: |p|
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
count: a #∈ as,
subtype_rel: A ⊆r B,
abgrp: AbGrp,
grp: Group{i},
mon: Mon,
imon: IMonoid,
uall: ∀[x:A]. B[x],
prop: ℙ,
dset: DSet,
so_lambda: λ2x.t[x],
infix_ap: x f y,
grp_car: |g|,
pi1: fst(t),
int_add_grp: <ℤ+>,
guard: {T},
uimplies: b supposing a,
so_apply: x[s]
Lemmas referenced :
mon_for_wf,
int_add_grp_wf,
grp_sig_wf,
monoid_p_wf,
grp_car_wf,
grp_op_wf,
grp_id_wf,
inverse_wf,
grp_inv_wf,
comm_wf,
set_car_wf,
b2i_wf,
set_eq_wf,
subtype_rel_self,
mon_subtype_grp_sig,
grp_subtype_mon,
abgrp_subtype_grp,
subtype_rel_transitivity,
abgrp_wf,
grp_wf,
mon_wf,
list_wf,
dset_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalRule,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesis,
applyEquality,
lambdaEquality,
setElimination,
rename,
hypothesisEquality,
setEquality,
cumulativity,
isectElimination,
because_Cache,
instantiate,
independent_isectElimination,
intEquality
Latex:
\mforall{}s:DSet. \mforall{}a:|s|. \mforall{}bs:|s| List. (a \#\mmember{} bs \mmember{} \mBbbZ{})
Date html generated:
2018_05_22-AM-07_45_17
Last ObjectModification:
2018_05_19-AM-08_32_15
Theory : list_2
Home
Index