Nuprl Lemma : sum-map-cons

[T:Type]. ∀[f:T ⟶ ℤ]. ∀[L:T List]. ∀[x:T].  f[x] for x ∈ [x L] f[x] + Σf[x] for x ∈ L)


Proof




Definitions occuring in Statement :  sum-map: Σf[x] for x ∈ L cons: [a b] list: List uall: [x:A]. B[x] so_apply: x[s] function: x:A ⟶ B[x] add: m int: universe: Type sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a so_lambda: λ2x.t[x] so_apply: x[s] implies:  Q all: x:A. B[x] top: Top prop: guard: {T} sq_type: SQType(T) sum-map: Σf[x] for x ∈ L squash: T nat_plus: + less_than: a < b less_than': less_than'(a;b) true: True and: P ∧ Q int_seg: {i..j-} lelt: i ≤ j < k decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A subtype_rel: A ⊆B iff: ⇐⇒ Q rev_implies:  Q le: A ≤ B nat: subtract: m append: as bs so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3]
Lemmas referenced :  subtype_base_sq int_subtype_base last_induction all_wf equal_wf sum-map_wf cons_wf list_wf sum_map_nil_lemma length_of_cons_lemma length_of_nil_lemma squash_wf true_wf sum_split_first less_than_wf select_wf nil_wf int_seg_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf length-singleton decidable__lt intformless_wf int_formula_prop_less_lemma int_seg_wf iff_weakening_equal add_functionality_wrt_eq false_wf sum_wf subtract_wf le_wf itermSubtract_wf int_term_value_subtract_lemma empty_support select-cons-hd list_ind_cons_lemma subtype_rel_list top_wf decidable__equal_int intformeq_wf itermAdd_wf int_formula_prop_eq_lemma int_term_value_add_lemma sum-map-append1
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin instantiate extract_by_obid sqequalHypSubstitution isectElimination cumulativity intEquality independent_isectElimination hypothesis hypothesisEquality sqequalRule lambdaEquality applyEquality functionExtensionality addEquality independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality lambdaFormation because_Cache equalityTransitivity equalitySymmetry sqequalAxiom functionEquality universeEquality imageElimination dependent_set_memberEquality natural_numberEquality independent_pairFormation imageMemberEquality baseClosed setElimination rename productElimination unionElimination dependent_pairFormation int_eqEquality computeAll

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[L:T  List].  \mforall{}[x:T].    (\mSigma{}f[x]  for  x  \mmember{}  [x  /  L]  \msim{}  f[x]  +  \mSigma{}f[x]  for  x  \mmember{}  L)



Date html generated: 2018_05_21-PM-08_29_19
Last ObjectModification: 2017_07_26-PM-05_56_25

Theory : general


Home Index