### Nuprl Lemma : bag-parts-no-repeats

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

Proof

Definitions occuring in Statement :  bag-parts: `bag-parts(eq;bs)` bag-no-repeats: `bag-no-repeats(T;bs)` bag: `bag(T)` listp: `A List+` 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` bag-no-repeats: `bag-no-repeats(T;bs)` squash: `↓T` all: `∀x:A. B[x]` nat: `ℕ` implies: `P `` Q` false: `False` ge: `i ≥ j ` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` and: `P ∧ Q` prop: `ℙ` guard: `{T}` int_seg: `{i..j-}` lelt: `i ≤ j < k` le: `A ≤ B` decidable: `Dec(P)` or: `P ∨ Q` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` sq_type: `SQType(T)` empty-bag: `{}` cons: `[a / b]` less_than': `less_than'(a;b)` colength: `colength(L)` nil: `[]` it: `⋅` less_than: `a < b` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` cons-bag: `x.b` istype: `istype(T)` bag-size: `#(bs)` bag-parts: `bag-parts(eq;bs)` bag-partitions: `bag-partitions(eq;bs)` bag-splits: `bag-splits(b)` list_ind: list_ind bag-append: `as + bs` append: `as @ bs` bag-map: `bag-map(f;bs)` map: `map(f;as)` single-bag: `{x}` pi1: `fst(t)` pi2: `snd(t)` bottom: `⊥` bag-to-set: `bag-to-set(eq;bs)` bag-remove-repeats: `bag-remove-repeats(eq;bs)` list-to-set: `list-to-set(eq;L)` l-union: `as ⋃ bs` reduce: `reduce(f;k;as)` insert: `insert(a;L)` eval_list: `eval_list(t)` ifthenelse: `if b then t else f fi ` deq-member: `x ∈b L` bor: `p ∨bq` proddeq: `proddeq(a;b)` band: `p ∧b q` bag-deq: `bag-deq(eq)` bag-eq: `bag-eq(eq;as;bs)` bag-all: `bag-all(x.p[x];bs)` bag-reduce: `bag-reduce(x,y.f[x; y];zero;bs)` btrue: `tt` eq_int: `(i =z j)` bag-count: `(#x in bs)` count: `count(P;L)` bfalse: `ff` lt_int: `i <z j` bag-combine: `⋃x∈bs.f[x]` bag-union: `bag-union(bbs)` concat: `concat(ll)` bag-null: `bag-null(bs)` null: `null(as)` so_lambda: so_lambda4 so_apply: `x[s1;s2;s3;s4]` strict4: `strict4(F)` callbyvalueall: callbyvalueall evalall: `evalall(t)` has-value: `(a)↓` uiff: `uiff(P;Q)` has-valueall: `has-valueall(a)` bool: `𝔹` unit: `Unit` bnot: `¬bb` assert: `↑b` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` listp: `A List+` cand: `A c∧ B` length: `||as||` true: `True` inject: `Inj(A;B;f)` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  bag_wf deq_wf valueall-type_wf istype-universe nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf istype-less_than int_seg_properties int_seg_wf subtract-1-ge-0 decidable__equal_int subtract_wf subtype_base_sq set_subtype_base lelt_wf int_subtype_base intformnot_wf intformeq_wf itermSubtract_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_subtract_lemma decidable__le decidable__lt istype-le subtype_rel_self bag_to_squash_list le_wf bag-size_wf bag-no-repeats_wf listp_wf bag-parts_wf list-cases product_subtype_list colength-cons-not-zero colength_wf_list istype-void list_wf spread_cons_lemma itermAdd_wf int_term_value_add_lemma squash_wf equal_wf list-subtype-bag no_repeats_wf istype-nat empty-bag-no-repeats length_of_nil_lemma lifting-strict-callbyvalueall has-valueall-if-has-value-callbyvalueall has-valueall-has-value has-value_wf_base istype-base is-exception_wf is-exception-evalall cbv_sqequal lifting-strict-ifthenelse strict4-decide lifting-strict-ispair has-value-ifthenelse-type lifting-strict-spread strict4-ispair value-type-has-value int-value-type lifting-strict-isaxiom cons-bag_wf length_of_cons_lemma length_wf add-is-int-iff false_wf valueall-type-has-valueall bag-valueall-type product-valueall-type bag-partitions_wf evalall-reduce bag-combine-no-repeats bag-member_wf bag-null_wf empty-bag_wf eqff_to_assert bool_cases_sqequal bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf equal-wf-T-base pi1_wf_top assert-bag-null subtype_rel_product top_wf single-bag_wf cons_wf_listp nil_wf pi2_wf set-valueall-type less_than_wf list-valueall-type bag-map_wf cons-listp product-deq_wf bag-deq_wf strong-subtype-deq-subtype strong-subtype-set2 list-deq_wf strong-subtype-set3 strong-subtype-self bag-subtype subtype_rel_set bag_size_cons_lemma bool_cases eqtt_to_assert bag-member-empty-iff iff_transitivity bnot_wf not_wf assert_of_bnot istype-assert bag-member-single reduce_hd_cons_lemma hd_wf istype-false bag-member-map bag-member-parts listp_properties true_wf iff_weakening_equal tl_wf reduce_tl_cons_lemma bag-union_wf reduce_nil_lemma length_cons_ge_one subtype_rel_list bag_qinc bag-single-no-repeats bag-map-no-repeats easy-member-int_seg bag-member-partitions bag-size-append bag-size-zero no-repeats-bag-partitions bag-no-repeats-settype decidable__equal_product decidable__equal_bag decidable-equal-deq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule sqequalHypSubstitution imageElimination hypothesis imageMemberEquality hypothesisEquality thin baseClosed universeIsType extract_by_obid isectElimination isect_memberEquality_alt isectIsTypeImplies inhabitedIsType instantiate universeEquality lambdaFormation_alt setElimination rename intWeakElimination natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality dependent_functionElimination Error :memTop,  independent_pairFormation voidElimination functionIsTypeImplies productElimination unionElimination applyEquality cumulativity intEquality equalityTransitivity equalitySymmetry applyLambdaEquality dependent_set_memberEquality_alt because_Cache productIsType promote_hyp hypothesis_subsumption hyp_replacement functionEquality equalityIstype baseApply closedConclusion sqequalBase productEquality addEquality callbyvalueExceptionCases inrFormation_alt callbyvalueCallbyvalue callbyvalueReduce sqleReflexivity decideExceptionCases exceptionSqequal inlFormation_alt callbyvalueAdd addExceptionCases sqequalSqle divergentSqle callbyvalueSpread spreadExceptionCases axiomSqleEquality callbyvalueDecide pointwiseFunctionality setEquality equalityElimination independent_pairEquality setIsType functionIsType

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

Date html generated: 2020_05_20-AM-09_04_42
Last ObjectModification: 2020_01_01-PM-00_11_16

Theory : bags_2

Home Index