### Nuprl Lemma : bag-diff-property

`∀[T:Type]`
`  ∀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)))`

Proof

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 b of inl(x) => s[x] | inr(y) => t[y]` universe: `Type` equal: `s = 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: `P `` 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: `b supposing a` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` top: `Top` decidable: `Dec(P)` or: `P ∨ Q` subtype_rel: `A ⊆r B` sq_type: `SQType(T)` nat: `ℕ` ge: `i ≥ j ` le: `A ≤ B` less_than: `a < b` list_accum: list_accum nil: `[]` it: `⋅` cons: `[a / b]` assert: `↑b` ifthenelse: `if b then t else f fi ` bfalse: `ff` iff: `P `⇐⇒` Q` uiff: `uiff(P;Q)` rev_implies: `P `` Q` int_iseg: `{i...j}` cand: `A c∧ B` so_lambda: `λ2x y.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

Latex:
\mforall{}[T:Type]
\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