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:  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:  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: supposing a decidable: Dec(P) or: P ∨ Q so_lambda: λ2y.t[x; y] infix_ap: 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 ≥  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