### Nuprl Lemma : sum-partial-list-has-value

`∀[T:Type]. ∀[L:T List]. ∀[f:T ⟶ partial(ℕ)].  ∀x:T. (f[x])↓ supposing (x ∈ L) supposing (Σ(f[L[i]] | i < ||L||))↓`

Proof

Definitions occuring in Statement :  sum: `Σ(f[x] | x < k)` l_member: `(x ∈ l)` select: `L[n]` length: `||as||` list: `T List` partial: `partial(T)` nat: `ℕ` has-value: `(a)↓` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` member: `t ∈ T` all: `∀x:A. B[x]` has-value: `(a)↓` prop: `ℙ` squash: `↓T` less_than: `a < b` top: `Top` not: `¬A` implies: `P `` Q` false: `False` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` or: `P ∨ Q` decidable: `Dec(P)` and: `P ∧ Q` lelt: `i ≤ j < k` guard: `{T}` int_seg: `{i..j-}` so_apply: `x[s]` so_lambda: `λ2x.t[x]` le: `A ≤ B` nat: `ℕ` cand: `A c∧ B` l_member: `(x ∈ l)`
Lemmas referenced :  partial_wf nat_wf list_wf l_member_wf int_seg_wf int_formula_prop_less_lemma intformless_wf decidable__lt int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le length_wf int_seg_properties select_wf length_wf_nat sum-partial-has-value lelt_wf int-value-type le_wf set-value-type has-value_wf-partial sum-partial-nat full-omega-unsat equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule sqequalHypSubstitution Error :lambdaEquality_alt,  dependent_functionElimination thin hypothesisEquality Error :isect_memberEquality_alt,  isectElimination axiomSqleEquality hypothesis Error :isectIsTypeImplies,  Error :inhabitedIsType,  Error :functionIsTypeImplies,  Error :functionIsType,  Error :universeIsType,  extract_by_obid universeEquality cumulativity isect_memberFormation lambdaFormation imageElimination computeAll independent_pairFormation voidEquality voidElimination isect_memberEquality intEquality int_eqEquality dependent_pairFormation unionElimination productElimination natural_numberEquality independent_isectElimination rename setElimination because_Cache functionExtensionality applyEquality lambdaEquality dependent_set_memberEquality applyLambdaEquality hyp_replacement equalitySymmetry approximateComputation independent_functionElimination equalityTransitivity

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[f:T  {}\mrightarrow{}  partial(\mBbbN{})].
\mforall{}x:T.  (f[x])\mdownarrow{}  supposing  (x  \mmember{}  L)  supposing  (\mSigma{}(f[L[i]]  |  i  <  ||L||))\mdownarrow{}

Date html generated: 2019_06_20-PM-01_48_49
Last ObjectModification: 2018_10_15-PM-01_44_59

Theory : list_1

Home Index