Nuprl Lemma : sub-bags-no-repeats

`∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].  bag-no-repeats(bag(T);sub-bags(eq;bs)) supposing valueall-type(T)`

Proof

Definitions occuring in Statement :  sub-bags: `sub-bags(eq;bs)` bag-no-repeats: `bag-no-repeats(T;bs)` bag: `bag(T)` deq: `EqDecider(T)` valueall-type: `valueall-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` sub-bags: `sub-bags(eq;bs)` bag-no-repeats: `bag-no-repeats(T;bs)` squash: `↓T` all: `∀x:A. B[x]` prop: `ℙ` implies: `P `` Q` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` top: `Top` uiff: `uiff(P;Q)` and: `P ∧ Q` inject: `Inj(A;B;f)` pi1: `fst(t)` rev_uimplies: `rev_uimplies(P;Q)` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  valueall-type_wf bag_wf deq_wf bag-subtype bag-partitions_wf bag-member_wf equal_wf bag-map-no-repeats pi1_wf_top subtype_rel_product top_wf set_wf bag-member-partitions and_wf bag-append_wf bag-append-cancel bag-no-repeats_wf subtype_rel_bag no-repeats-bag-partitions bag-no-repeats-settype decidable__equal_product decidable__equal_bag decidable-equal-deq squash_wf true_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution imageElimination hypothesis imageMemberEquality hypothesisEquality thin baseClosed extract_by_obid isectElimination cumulativity isect_memberEquality because_Cache equalityTransitivity equalitySymmetry universeEquality productEquality dependent_functionElimination independent_isectElimination setEquality productElimination independent_pairEquality lambdaFormation independent_functionElimination lambdaEquality setElimination rename applyEquality voidElimination voidEquality dependent_set_memberEquality independent_pairFormation applyLambdaEquality hyp_replacement instantiate natural_numberEquality

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].
bag-no-repeats(bag(T);sub-bags(eq;bs))  supposing  valueall-type(T)

Date html generated: 2018_05_21-PM-09_52_37
Last ObjectModification: 2017_07_26-PM-06_31_54

Theory : bags_2

Home Index