### Nuprl Lemma : finite-deriv-seq_wf

`∀[I:Interval]. ∀[k:ℕ]. ∀[F:ℕk + 1 ⟶ I ⟶ℝ].  (finite-deriv-seq(I;k;i,x.F[i;x]) ∈ ℙ)`

Proof

Definitions occuring in Statement :  finite-deriv-seq: `finite-deriv-seq(I;k;i,x.F[i; x])` rfun: `I ⟶ℝ` interval: `Interval` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` member: `t ∈ T` function: `x:A ⟶ B[x]` add: `n + m` natural_number: `\$n`
Definitions unfolded in proof :  subtract: `n - m` uiff: `uiff(P;Q)` so_apply: `x[s]` subtype_rel: `A ⊆r B` prop: `ℙ` top: `Top` not: `¬A` implies: `P `` Q` false: `False` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` uimplies: `b supposing a` or: `P ∨ Q` decidable: `Dec(P)` all: `∀x:A. B[x]` ge: `i ≥ j ` and: `P ∧ Q` lelt: `i ≤ j < k` int_seg: `{i..j-}` so_apply: `x[s1;s2]` rfun: `I ⟶ℝ` label: `...\$L... t` so_lambda: `λ2x.t[x]` nat: `ℕ` finite-deriv-seq: `finite-deriv-seq(I;k;i,x.F[i; x])` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  all_wf int_seg_wf derivative_wf nat_properties decidable__lt satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermVar_wf itermAdd_wf itermConstant_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_add_lemma int_term_value_constant_lemma int_formula_prop_wf lelt_wf real_wf i-member_wf add-member-int_seg2 decidable__le subtract_wf intformle_wf itermSubtract_wf int_formula_prop_le_lemma int_term_value_subtract_lemma add-subtract-cancel rfun_wf nat_wf interval_wf
Rules used in proof :  functionEquality equalitySymmetry equalityTransitivity axiomEquality setEquality because_Cache computeAll voidEquality voidElimination isect_memberEquality intEquality int_eqEquality dependent_pairFormation independent_isectElimination unionElimination addEquality dependent_functionElimination independent_pairFormation productElimination dependent_set_memberEquality applyEquality lambdaEquality hypothesis hypothesisEquality rename setElimination natural_numberEquality thin isectElimination sqequalHypSubstitution lemma_by_obid sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[I:Interval].  \mforall{}[k:\mBbbN{}].  \mforall{}[F:\mBbbN{}k  +  1  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}].    (finite-deriv-seq(I;k;i,x.F[i;x])  \mmember{}  \mBbbP{})

Date html generated: 2016_05_18-AM-10_20_33
Last ObjectModification: 2016_01_17-AM-00_31_21

Theory : reals

Home Index