Nuprl Lemma : no_repeats-bag

[T:Type]. ∀[as,bs:T List].  (no_repeats(T;as)) supposing (no_repeats(T;bs) and (as bs ∈ bag(T)))


Definitions occuring in Statement :  bag: bag(T) no_repeats: no_repeats(T;l) list: List uimplies: supposing a uall: [x:A]. B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a bag: bag(T) quotient: x,y:A//B[x; y] sq_stable: SqStable(P) implies:  Q all: x:A. B[x] and: P ∧ Q iff: ⇐⇒ Q rev_implies:  Q squash: T prop: subtype_rel: A ⊆B
Lemmas referenced :  list-subtype-bag bag_wf equal_wf no_repeats_wf no_repeats_witness permutation_wf list_wf member_wf and_wf no_repeats_functionality_wrt_permutation sq_stable__no_repeats
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution sqequalRule pertypeElimination lemma_by_obid isectElimination thin hypothesisEquality hypothesis independent_functionElimination because_Cache dependent_functionElimination productElimination imageMemberEquality baseClosed imageElimination isect_memberEquality equalityTransitivity equalitySymmetry cumulativity applyEquality independent_isectElimination lambdaEquality

\mforall{}[T:Type].  \mforall{}[as,bs:T  List].    (no\_repeats(T;as))  supposing  (no\_repeats(T;bs)  and  (as  =  bs))

Date html generated: 2016_05_15-PM-02_55_10
Last ObjectModification: 2016_01_16-AM-08_40_05

Theory : bags

Home Index