### Nuprl Lemma : bag-val_wf

`∀[T:Type]. ∀[+:T ⟶ T ⟶ T]. ∀[zero:T].  (Comm(T;+) `` Assoc(T;+) `` Ident(T;+;zero) `` (bag-val(zero;+) ∈ bag(T) ⟶ T))`

Proof

Definitions occuring in Statement :  bag-val: `bag-val(zero;+)` bag: `bag(T)` comm: `Comm(T;op)` assoc: `Assoc(T;op)` uall: `∀[x:A]. B[x]` implies: `P `` Q` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type` ident: `Ident(T;op;id)`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` bag-val: `bag-val(zero;+)` prop: `ℙ` bag: `bag(T)` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` all: `∀x:A. B[x]` uimplies: `b supposing a` decidable: `Dec(P)` or: `P ∨ Q` so_lambda: `λ2x y.t[x; y]` infix_ap: `x f y` so_apply: `x[s1;s2]` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` length: `||as||` list_ind: list_ind nil: `[]` it: `⋅` false: `False` cons: `[a / b]` combine-list: `combine-list(x,y.f[x; y];L)` top: `Top` guard: `{T}` true: `True` ident: `Ident(T;op;id)` ge: `i ≥ j ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` not: `¬A` assoc: `Assoc(T;op)` comm: `Comm(T;op)` le: `A ≤ B`
Lemmas referenced :  bag_wf ident_wf assoc_wf comm_wf list_wf permutation-length decidable__lt permutation_wf equal_wf equal-wf-base list_accum_wf list-cases product_subtype_list list_accum_cons_lemma reduce_hd_cons_lemma reduce_tl_cons_lemma infix_ap_wf squash_wf true_wf combine-list_wf length_of_nil_lemma non_neg_length satisfiable-full-omega-tt intformand_wf intformless_wf itermConstant_wf itermVar_wf intformeq_wf int_formula_prop_and_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_wf combine-list-permutation nil_wf length_of_cons_lemma intformle_wf itermAdd_wf int_formula_prop_le_lemma int_term_value_add_lemma intformnot_wf int_formula_prop_not_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation lambdaEquality extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality hypothesis functionExtensionality applyEquality sqequalRule dependent_functionElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache functionEquality universeEquality pointwiseFunctionalityForEquality pertypeElimination productElimination rename independent_isectElimination natural_numberEquality unionElimination independent_functionElimination productEquality hyp_replacement applyLambdaEquality imageElimination voidElimination promote_hyp hypothesis_subsumption voidEquality imageMemberEquality baseClosed dependent_pairFormation int_eqEquality intEquality independent_pairFormation computeAll

Latex:
\mforall{}[T:Type].  \mforall{}[+:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].  \mforall{}[zero:T].
(Comm(T;+)  {}\mRightarrow{}  Assoc(T;+)  {}\mRightarrow{}  Ident(T;+;zero)  {}\mRightarrow{}  (bag-val(zero;+)  \mmember{}  bag(T)  {}\mrightarrow{}  T))

Date html generated: 2017_10_01-AM-08_46_16
Last ObjectModification: 2017_07_26-PM-04_31_12

Theory : bags

Home Index