Nuprl Lemma : bag-diff-property

  ∀eq:EqDecider(T). ∀as,bs:bag(T).
    case bag-diff(eq;bs;as) of inl(cs) => bs (as cs) ∈ bag(T) inr(z) => ∀cs:bag(T). (bs (as cs) ∈ bag(T)))


Definitions occuring in Statement :  bag-diff: bag-diff(eq;bs;as) bag-append: as bs bag: bag(T) deq: EqDecider(T) uall: [x:A]. B[x] all: x:A. B[x] not: ¬A decide: case of inl(x) => s[x] inr(y) => t[y] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] member: t ∈ T squash: T exists: x:A. B[x] prop: implies:  Q so_lambda: λ2x.t[x] so_apply: x[s] bag-diff: bag-diff(eq;bs;as) bag-accum: bag-accum(v,x.f[v; x];init;bs) guard: {T} int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q uimplies: supposing a not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) false: False top: Top decidable: Dec(P) or: P ∨ Q subtype_rel: A ⊆B sq_type: SQType(T) nat: ge: i ≥  le: A ≤ B less_than: a < b list_accum: list_accum nil: [] it: cons: [a b] assert: b ifthenelse: if then else fi  bfalse: ff iff: ⇐⇒ Q uiff: uiff(P;Q) rev_implies:  Q int_iseg: {i...j} cand: c∧ B so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] bag-append: as bs append: as bs so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] single-bag: {x} true: True sq_or: a ↓∨ b sq_stable: SqStable(P)
Lemmas referenced :  bag_wf deq_wf bag_to_squash_list squash_wf bag-diff_wf unit_wf2 equal_wf bag-append_wf all_wf not_wf int_seg_properties full-omega-unsat intformand_wf intformless_wf itermVar_wf itermConstant_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf int_seg_wf decidable__equal_int subtract_wf subtype_base_sq set_subtype_base 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 lelt_wf subtype_rel_self le_wf length_wf non_neg_length nat_properties less_than_wf decidable__assert null_wf3 subtype_rel_list top_wf list-cases product_subtype_list null_cons_lemma last-lemma-sq pos_length iff_transitivity equal-wf-T-base list_wf assert_wf bnot_wf assert_of_null iff_weakening_uiff assert_of_bnot firstn_wf length_firstn list_accum_wf bag-remove1_wf list-subtype-bag set_wf primrec-wf2 nat_wf itermAdd_wf int_term_value_add_lemma length_wf_nat list_ind_nil_lemma list_accum_append list_accum_cons_lemma list_accum_nil_lemma bag-remove1-property last_wf append_wf cons_wf nil_wf true_wf bag-append-assoc iff_weakening_equal single-bag_wf bag-append-cancel bag-member_wf bag-member-append bag-member-single bag-append-comm-assoc sq_stable__equal sq_stable__all sq_stable__not
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis universeEquality imageElimination productElimination promote_hyp rename hyp_replacement equalitySymmetry applyLambdaEquality unionEquality equalityTransitivity unionElimination sqequalRule lambdaEquality dependent_functionElimination independent_functionElimination imageMemberEquality baseClosed natural_numberEquality because_Cache setElimination independent_isectElimination approximateComputation dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation addLevel applyEquality instantiate dependent_set_memberEquality levelHypothesis hypothesis_subsumption impliesFunctionality productEquality functionEquality inlEquality inrEquality addEquality cumulativity equalityUniverse inlFormation

    \mforall{}eq:EqDecider(T).  \mforall{}as,bs:bag(T).
        case  bag-diff(eq;bs;as)  of  inl(cs)  =>  bs  =  (as  +  cs)  |  inr(z)  =>  \mforall{}cs:bag(T).  (\mneg{}(bs  =  (as  +  cs)))

Date html generated: 2019_10_16-AM-11_31_55
Last ObjectModification: 2018_08_21-PM-01_59_55

Theory : bags_2

Home Index