Nuprl Lemma : single-valued-bag-append

`∀[A:Type]. ∀[as,bs:bag(A)].`
`  (single-valued-bag(as + bs;A)) supposing `
`     (similar-bags(A;as;bs) and `
`     single-valued-bag(as;A) and `
`     single-valued-bag(bs;A))`

Proof

Definitions occuring in Statement :  single-valued-bag: `single-valued-bag(b;T)` similar-bags: `similar-bags(A;as;bs)` bag-append: `as + bs` bag: `bag(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` single-valued-bag: `single-valued-bag(b;T)` all: `∀x:A. B[x]` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` sq_or: `a ↓∨ b` squash: `↓T` or: `P ∨ Q` similar-bags: `similar-bags(A;as;bs)` rev_implies: `P `` Q` subtype_rel: `A ⊆r B` nat: `ℕ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` decidable: `Dec(P)` false: `False` guard: `{T}` ge: `i ≥ j ` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` prop: `ℙ` cand: `A c∧ B` uiff: `uiff(P;Q)`
Lemmas referenced :  bag-member-append decidable__or equal-wf-base bag-size_wf set_subtype_base le_wf istype-int int_subtype_base less_than_wf decidable__equal_int decidable__lt nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformnot_wf intformor_wf intformeq_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_not_lemma int_formula_prop_or_lemma int_formula_prop_eq_lemma int_formula_prop_less_lemma int_formula_prop_wf bag-member_wf bag-append_wf similar-bags_wf single-valued-bag_wf bag_wf istype-universe bag-size-zero decidable__le bag-member-empty-iff
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalHypSubstitution lambdaFormation_alt extract_by_obid isectElimination thin hypothesisEquality dependent_functionElimination hypothesis productElimination independent_functionElimination imageElimination unionElimination sqequalRule intEquality applyEquality lambdaEquality_alt natural_numberEquality independent_isectElimination baseClosed setElimination rename inhabitedIsType equalityTransitivity equalitySymmetry because_Cache applyLambdaEquality approximateComputation dependent_pairFormation_alt int_eqEquality Error :memTop,  independent_pairFormation universeIsType voidElimination axiomEquality functionIsTypeImplies isect_memberEquality_alt isectIsTypeImplies instantiate universeEquality

Latex:
\mforall{}[A:Type].  \mforall{}[as,bs:bag(A)].
(single-valued-bag(as  +  bs;A))  supposing
(similar-bags(A;as;bs)  and
single-valued-bag(as;A)  and
single-valued-bag(bs;A))

Date html generated: 2020_05_20-AM-08_01_57
Last ObjectModification: 2020_01_10-PM-03_01_29

Theory : bags

Home Index