Nuprl Lemma : bag-combine-no-repeats

`∀[T1,T2:Type]. ∀[f:T1 ⟶ bag(T2)]. ∀[eq1:EqDecider(T1)]. ∀[eq2:EqDecider(T2)]. ∀[bs:bag(T1)].`
`  (bag-no-repeats(T2;⋃x∈bs.f[x])) supposing `
`     (bag-no-repeats(T1;bs) and `
`     ((∀x,y:T1. ∀z:T2.  (z ↓∈ f[x] `` z ↓∈ f[y] `` (x = y ∈ T1))) ∧ (∀x:T1. bag-no-repeats(T2;f[x]))))`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` bag-no-repeats: `bag-no-repeats(T;bs)` bag-combine: `⋃x∈bs.f[x]` bag: `bag(T)` deq: `EqDecider(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` uiff: `uiff(P;Q)` all: `∀x:A. B[x]` so_apply: `x[s]` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` implies: `P `` Q` iff: `P `⇐⇒` Q` rev_uimplies: `rev_uimplies(P;Q)` decidable: `Dec(P)` or: `P ∨ Q` le: `A ≤ B` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` prop: `ℙ` nat: `ℕ` bag-no-repeats: `bag-no-repeats(T;bs)` squash: `↓T` bag: `bag(T)` quotient: `x,y:A//B[x; y]` sq_type: `SQType(T)` guard: `{T}` true: `True` istype: `istype(T)` bag-filter: `[x∈b|p[x]]` bag-sum: `bag-sum(ba;x.f[x])` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` cons: `[a / b]` less_than: `a < b` less_than': `less_than'(a;b)` cand: `A c∧ B` rev_implies: `P `` Q` bag-size: `#(bs)` ge: `i ≥ j ` deq: `EqDecider(T)` colength: `colength(L)` nil: `[]` it: `⋅` bool: `𝔹` unit: `Unit` btrue: `tt` ifthenelse: `if b then t else f fi ` eqof: `eqof(d)` bfalse: `ff` bnot: `¬bb` assert: `↑b` nat_plus: `ℕ+`
Lemmas referenced :  bag-no-repeats-count iff_weakening_uiff bag-no-repeats_wf uall_wf uiff_wf le_wf bag-count_wf equal-wf-T-base istype-universe bag-combine_wf decidable__equal_int decidable__lt full-omega-unsat intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf intformeq_wf intformle_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_le_lemma int_formula_prop_wf bag-count-combine bag-sum-count decidable__le le_witness_for_triv set_subtype_base int_subtype_base bag-member_wf bag_wf deq_wf list_wf permutation_wf permutation_weakening equal_wf subtype_base_sq list-subtype-bag filter_wf5 l_member_wf le_int_wf list-cases list_accum_nil_lemma product_subtype_list list_accum_cons_lemma less_than_wf add-is-int-iff itermAdd_wf int_term_value_add_lemma false_wf list_accum_wf length_wf_nat nat_wf cons_member cons_wf member_filter assert_of_le_int bag-member-count list-member-bag-member subtype_rel_dep_function bool_wf bag-count-sqequal nat_properties ge_wf member-less_than filter_nil_lemma length_of_nil_lemma colength-cons-not-zero colength_wf_list istype-false length_wf subtract-1-ge-0 spread_cons_lemma subtract_wf itermSubtract_wf int_term_value_subtract_lemma filter_cons_lemma null_nil_lemma btrue_wf null_wf3 subtype_rel_list top_wf null_cons_lemma bfalse_wf btrue_neq_bfalse eqtt_to_assert safe-assert-deq length_of_cons_lemma eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot assert_wf reduce_hd_cons_lemma hd_wf squash_wf length_cons_ge_one eqof_wf reduce_tl_cons_lemma tl_wf nil_wf add_nat_plus nat_plus_properties true_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalHypSubstitution productElimination thin extract_by_obid isectElimination hypothesisEquality hypothesis independent_isectElimination lambdaFormation_alt dependent_functionElimination applyEquality sqequalRule lambdaEquality_alt natural_numberEquality because_Cache independent_functionElimination independent_pairFormation unionElimination approximateComputation dependent_pairFormation_alt int_eqEquality isect_memberEquality_alt voidElimination universeIsType equalityTransitivity equalitySymmetry equalityIsType4 intEquality baseClosed independent_pairEquality axiomEquality imageElimination imageMemberEquality productIsType functionIsType inhabitedIsType equalityIsType1 universeEquality promote_hyp pointwiseFunctionality pertypeElimination instantiate cumulativity isectIsType setElimination rename closedConclusion setIsType hypothesis_subsumption addEquality baseApply dependent_set_memberEquality_alt inlFormation_alt inrFormation_alt hyp_replacement applyLambdaEquality productEquality functionEquality setEquality intWeakElimination functionIsTypeImplies equalityIsType3 equalityIsType2 equalityElimination

Latex:
\mforall{}[T1,T2:Type].  \mforall{}[f:T1  {}\mrightarrow{}  bag(T2)].  \mforall{}[eq1:EqDecider(T1)].  \mforall{}[eq2:EqDecider(T2)].  \mforall{}[bs:bag(T1)].
(bag-no-repeats(T2;\mcup{}x\mmember{}bs.f[x]))  supposing
(bag-no-repeats(T1;bs)  and
((\mforall{}x,y:T1.  \mforall{}z:T2.    (z  \mdownarrow{}\mmember{}  f[x]  {}\mRightarrow{}  z  \mdownarrow{}\mmember{}  f[y]  {}\mRightarrow{}  (x  =  y)))  \mwedge{}  (\mforall{}x:T1.  bag-no-repeats(T2;f[x]))))

Date html generated: 2019_10_16-AM-11_30_31
Last ObjectModification: 2018_10_11-PM-03_22_09

Theory : bags_2

Home Index