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: supposing a uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] implies:  Q and: P ∧ Q function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: 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 ⊆B implies:  Q iff: ⇐⇒ 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: λ2y.t[x; y] so_apply: x[s1;s2] cons: [a b] less_than: a < b less_than': less_than'(a;b) cand: c∧ B rev_implies:  Q bag-size: #(bs) ge: i ≥  deq: EqDecider(T) colength: colength(L) nil: [] it: bool: 𝔹 unit: Unit btrue: tt ifthenelse: if then else 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