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

`∀[n:ℕ]. ∀[f:ℕn ⟶ partial(ℕ)].  ∀i:ℕn. (f[i])↓ supposing (Σ(f[x] | x < n))↓`

Proof

Definitions occuring in Statement :  sum: `Σ(f[x] | x < k)` partial: `partial(T)` int_seg: `{i..j-}` 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]` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` member: `t ∈ T` so_apply: `x[s]` implies: `P `` Q` nat: `ℕ` prop: `ℙ` uimplies: `b supposing a` all: `∀x:A. B[x]` has-value: `(a)↓` top: `Top` guard: `{T}` int_seg: `{i..j-}` ge: `i ≥ j ` lelt: `i ≤ j < k` and: `P ∧ Q` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` less_than: `a < b` less_than': `less_than'(a;b)` true: `True` squash: `↓T` subtype_rel: `A ⊆r B` le: `A ≤ B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` uiff: `uiff(P;Q)` subtract: `n - m` sq_type: `SQType(T)`
Lemmas referenced :  uniform-comp-nat-induction nat_wf int_seg_wf partial_wf sum-partial-nat has-value_wf-partial set-value-type le_wf istype-int int-value-type sum-unroll istype-void int_seg_properties nat_properties decidable__lt full-omega-unsat intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_wf istype-top subtract_wf decidable__le itermSubtract_wf int_term_value_subtract_lemma istype-le istype-lt subtype_partial_sqtype_base set_subtype_base int_subtype_base subtype_rel_function int_seg_subtype istype-false not-le-2 condition-implies-le add-associates minus-add minus-one-mul add-swap minus-one-mul-top add-mul-special zero-mul add-zero add-commutes le-add-cancel2 subtype_rel_self less_than_wf value-type-has-value decidable__equal_int intformeq_wf int_formula_prop_eq_lemma subtype_base_sq int_seg_subtype_nat isect_wf all_wf uall_wf
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin sqequalRule independent_functionElimination hypothesis lemma_by_obid lambdaEquality hypothesisEquality rename setElimination natural_numberEquality functionEquality applyEquality because_Cache intEquality independent_isectElimination Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  Error :universeIsType,  Error :functionIsType,  Error :lambdaEquality_alt,  dependent_functionElimination axiomSqleEquality Error :functionIsTypeImplies,  Error :inhabitedIsType,  equalityTransitivity equalitySymmetry Error :isect_memberEquality_alt,  voidElimination productElimination unionElimination approximateComputation Error :dependent_pairFormation_alt,  int_eqEquality independent_pairFormation lessCases axiomSqEquality imageMemberEquality baseClosed imageElimination Error :dependent_set_memberEquality_alt,  Error :productIsType,  addEquality minusEquality multiplyEquality callbyvalueAdd instantiate cumulativity Error :isectIsType

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  partial(\mBbbN{})].    \mforall{}i:\mBbbN{}n.  (f[i])\mdownarrow{}  supposing  (\mSigma{}(f[x]  |  x  <  n))\mdownarrow{}

Date html generated: 2019_06_20-PM-01_18_19
Last ObjectModification: 2018_10_05-AM-11_01_46

Theory : int_2

Home Index