| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/vect_analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 53 kB |
|
Quelle deriv_sigma.prf Sprache: Lisp |
|||||||||
|
(deriv_sigma
(IMP_derivatives_TCC1 0 (IMP_derivatives_TCC1-1 nil 3514223777 ("" (lemma "deriv_domain") (("" (propax) nil nil)) nil) ((deriv_domain formula-decl nil deriv_sigma nil)) nil)) (IMP_derivatives_TCC2 0 (IMP_derivatives_TCC2-1 nil 3514223777 ("" (lemma "not_one_element") (("" (propax) nil nil)) nil) ((not_one_element formula-decl nil deriv_sigma nil)) nil)) (sigma_derivable_TCC1 0 (sigma_derivable_TCC1-1 nil 3460460862 ("" (subtype-tcc) nil nil) ((fullset const-decl "set" sets nil) (adh const-decl "setof[real]" convergence_functions "analysis/") (NQ const-decl "real" derivatives_def "analysis/") (convergence const-decl "bool" convergence_functions "analysis/") (convergence const-decl "bool" lim_of_functions "analysis/") (convergent? const-decl "bool" lim_of_functions "analysis/") (derivable? const-decl "bool" derivatives_def "analysis/") (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (sigma_derivable_TCC2 0 (sigma_derivable_TCC2-1 nil 3460460862 ("" (subtype-tcc) nil nil) ((fullset const-decl "set" sets nil) (adh const-decl "setof[real]" convergence_functions "analysis/") (NQ const-decl "real" derivatives_def "analysis/") (convergence const-decl "bool" convergence_functions "analysis/") (convergence const-decl "bool" lim_of_functions "analysis/") (convergent? const-decl "bool" lim_of_functions "analysis/") (derivable? const-decl "bool" derivatives_def "analysis/") (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (sigma_derivable_TCC3 0 (sigma_derivable_TCC3-1 nil 3460460862 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[real -> boolean]" deriv_sigma nil) (T formal-subtype-decl nil deriv_sigma nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Index type-eq-decl nil vectors "vectors/") (integer nonempty-type-from-decl nil integers nil) (fullset const-decl "set" sets nil) (adh const-decl "setof[real]" convergence_functions "analysis/") (NQ const-decl "real" derivatives_def "analysis/") (convergence const-decl "bool" convergence_functions "analysis/") (convergence const-decl "bool" lim_of_functions "analysis/") (convergent? const-decl "bool" lim_of_functions "analysis/") (derivable? const-decl "bool" derivatives_def "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) nil)) (sigma_derivable 0 (sigma_derivable-1 nil 3460463493 ("" (induct "m") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp*) (("3" (case "j!1 > 0") (("1" (assert) (("1" (case-replace "(LAMBDA (x: T): sigma(0, j!1, LAMBDA (i: Index[1 + j!1]): h!1(x)(i))) = (LAMBDA (x: T): sigma(0, j!1-1, LAMBDA (i: Index[1 + j!1]): h!1(x)(i)) + h!1(x)(j!1))") (("1" (hide -1) (("1" (inst - "y!1" "LAMBDA (x:T): LAMBDA (i: Index[j!1]): h!1(x)(i)") (("1" (assert) (("1" (split -2) (("1" (lemma "sum_derivable[T]") (("1" (inst - "(LAMBDA (x: T): h!1(x)(j!1))" "(LAMBDA (x: T): sigma(0, j!1 - 1, LAMBDA (i: Index[1 + j!1]): h!1(x)(i)))" "y!1") (("1" (assert) (("1" (split -1) (("1" (expand "+ ") (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (inst?) nil nil)) nil) ("3" (hide 2) (("3" (case-replace "(LAMBDA (x_1: T): sigma(0, j!1 - 1, LAMBDA (i_1: Index[j!1]): h!1(x_1)(i_1))) = (LAMBDA (x: T): sigma(0, j!1 - 1, LAMBDA (i: Index[1 + j!1]): h!1(x)(i))) ") (("1" (hide 2) (("1" (apply-extensionality 1 :hide? t) (("1" (hide -1) (("1" (lemma "sigma_diff_eq[j!1,j!1+1]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (apply-extensionality 1 :hide? t) (("1" (lemma "sigma_last[Index[j!1+1]]") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (assert) (("2" (expand "sigma") (("2" (expand "sigma") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (sigma_last formula-decl nil sigma "reals/") (sum_derivable formula-decl nil derivatives_def "analysis/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (below type-eq-decl nil naturalnumbers nil) (sigma_diff_eq formula-decl nil sigma_below_sub "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (j!1 skolem-const-decl "nat" deriv_sigma nil) (real_plus_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (nat_induction formula-decl nil naturalnumbers nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (pred type-eq-decl nil defined_types nil) (integer nonempty-type-from-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (T_pred const-decl "[real -> boolean]" deriv_sigma nil) (T formal-subtype-decl nil deriv_sigma nil) (< const-decl "bool" reals nil) (Index type-eq-decl nil vectors "vectors/") (below type-eq-decl nil nat_types nil) (derivable? const-decl "bool" derivatives_def "analysis/") (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (deriv_sigma_TCC1 0 (deriv_sigma_TCC1-1 nil 3460386482 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T_pred const-decl "[real -> boolean]" deriv_sigma nil) (T formal-subtype-decl nil deriv_sigma nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (fullset const-decl "set" sets nil) (adh const-decl "setof[real]" convergence_functions "analysis/") (NQ const-decl "real" derivatives_def "analysis/") (convergence const-decl "bool" convergence_functions "analysis/") (convergence const-decl "bool" lim_of_functions "analysis/") (convergent? const-decl "bool" lim_of_functions "analysis/") (derivable? const-decl "bool" derivatives_def "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) nil)) (deriv_sigma_TCC2 0 (deriv_sigma_TCC2-1 nil 3460461487 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T_pred const-decl "[real -> boolean]" deriv_sigma nil) (T formal-subtype-decl nil deriv_sigma nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (fullset const-decl "set" sets nil) (adh const-decl "setof[real]" convergence_functions "analysis/") (NQ const-decl "real" derivatives_def "analysis/") (convergence const-decl "bool" convergence_functions "analysis/") (convergence const-decl "bool" lim_of_functions "analysis/") (convergent? const-decl "bool" lim_of_functions "analysis/") (derivable? const-decl "bool" derivatives_def "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) nil)) (deriv_sigma_TCC3 0 (deriv_sigma_TCC3-1 nil 3460461487 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T_pred const-decl "[real -> boolean]" deriv_sigma nil) (T formal-subtype-decl nil deriv_sigma nil) (integer nonempty-type-from-decl nil integers nil) (Index type-eq-decl nil vectors "vectors/") (< const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (fullset const-decl "set" sets nil) (adh const-decl "setof[real]" convergence_functions "analysis/") (NQ const-decl "real" derivatives_def "analysis/") (convergence const-decl "bool" convergence_functions "analysis/") (convergence const-decl "bool" lim_of_functions "analysis/") (convergent? const-decl "bool" lim_of_functions "analysis/") (derivable? const-decl "bool" derivatives_def "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) nil)) (deriv_sigma_TCC4 0 (deriv_sigma_TCC4-1 nil 3460461487 ("" (skosimp*) (("" (lemma "sigma_derivable") (("" (inst - "n!1" "y!1" "h!1") (("" (assert) nil nil)) nil)) nil)) nil) ((sigma_derivable formula-decl nil deriv_sigma nil) (int_minus_int_is_int application-judgement "int" integers nil) (Index type-eq-decl nil vectors "vectors/") (< const-decl "bool" reals nil) (T formal-subtype-decl nil deriv_sigma nil) (T_pred const-decl "[real -> boolean]" deriv_sigma nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (> const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (n!1 skolem-const-decl "nat" deriv_sigma nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (deriv_sigma_TCC5 0 (deriv_sigma_TCC5-1 nil 3460462472 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T_pred const-decl "[real -> boolean]" deriv_sigma nil) (T formal-subtype-decl nil deriv_sigma nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (fullset const-decl "set" sets nil) (adh const-decl "setof[real]" convergence_functions "analysis/") (NQ const-decl "real" derivatives_def "analysis/") (convergence const-decl "bool" convergence_functions "analysis/") (convergence const-decl "bool" lim_of_functions "analysis/") (convergent? const-decl "bool" lim_of_functions "analysis/") (derivable? const-decl "bool" derivatives_def "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) nil)) (deriv_sigma_TCC6 0 (deriv_sigma_TCC6-1 nil 3460463371 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T_pred const-decl "[real -> boolean]" deriv_sigma nil) (T formal-subtype-decl nil deriv_sigma nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (fullset const-decl "set" sets nil) (adh const-decl "setof[real]" convergence_functions "analysis/") (NQ const-decl "real" derivatives_def "analysis/") (convergence const-decl "bool" convergence_functions "analysis/") (convergence const-decl "bool" lim_of_functions "analysis/") (convergent? const-decl "bool" lim_of_functions "analysis/") (derivable? const-decl "bool" derivatives_def "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) nil)) (deriv_sigma_TCC7 0 (deriv_sigma_TCC7-1 nil 3460463371 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T_pred const-decl "[real -> boolean]" deriv_sigma nil) (T formal-subtype-decl nil deriv_sigma nil) (fullset const-decl "set" sets nil) (adh const-decl "setof[real]" convergence_functions "analysis/") (NQ const-decl "real" derivatives_def "analysis/") (convergence const-decl "bool" convergence_functions "analysis/") (convergence const-decl "bool" lim_of_functions "analysis/") (convergent? const-decl "bool" lim_of_functions "analysis/") (derivable? const-decl "bool" derivatives_def "analysis/") (derivable? const-decl "bool" deriv_real_vect_def nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) nil)) (deriv_sigma_TCC8 0 (deriv_sigma_TCC8-1 nil 3460463371 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (deriv_sigma 0 (deriv_sigma-1 nil 3460387081 ("" (induct "n") (("1" (skosimp*) (("1" (expand "sigma") (("1" (lemma "deriv_const[T]") (("1" (inst?) (("1" (expand "const_fun") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case "j!1 = 0") (("1" (replace -1) (("1" (hide -2) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "deriv" 1 2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "y!1") (("2" (assert) (("1" (inst - "LAMBDA (x: T): LAMBDA (i: Index[j!1]): h!1(x)(i)") (("1" (split -1) (("1" (lemma "sigma_last[below(j!1+1)]") (("1" (inst?) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "(LAMBDA (x: T): sigma(0, j!1, LAMBDA (i: Index[1 + j!1]): h!1(x)(i))) = (LAMBDA (x: T): sigma(0, j!1-1, LAMBDA (i: Index[1 + j!1]): h!1(x)(i)) + h!1(x)(j!1))") (("1" (hide -1) (("1" (lemma "deriv_sum[T]") (("1" (inst - "(LAMBDA (x: T): sigma(0, j!1 - 1, LAMBDA (i: Index[1 + j!1]): h!1(x)(i)))" "(LAMBDA (x: T): h!1(x)(j!1))" "y!1") (("1" (assert) (("1" (split -1) (("1" (expand "+ " -1) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "(LAMBDA (x: T): sigma(0, j!1 - 1, LAMBDA (i: Index[1 + j!1]): h!1(x)(i))) = (LAMBDA (x: T): sigma(0, j!1 - 1, LAMBDA (i: Index[j!1]): h!1(x)(i)))") (("1" (hide -1) (("1" (replace -1) (("1" (hide -1) (("1" (case "sigma(0, j!1 - 1, LAMBDA (i: Index[1 + j!1]): deriv(h!1, y!1)(i)) = sigma(0, j!1 - 1, LAMBDA (i: Index[j!1]): deriv(h!1, y!1)(i))") (("1" (case-replace "sigma(0, j!1 - 1, LAMBDA (i: Index[1 + j!1]): deriv(h!1, y!1)(i)) = sigma(0, j!1 - 1, LAMBDA (i: Index[j!1]): deriv(h!1, y!1)(i))") (("1" (hide -1) (("1" (expand "deriv" 2 3) (("1" (expand "deriv" 2 2) (("1" (assert) (("1" (expand "deriv" 2 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (lemma "sigma_diff_eq[1+j!1,j!1]") (("2" (inst?) (("1" (assert) nil nil) ("2" (skosimp*) (("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (lemma "deriv_domain") (("3" (propax) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (expand "derivable?" 1) (("4" (propax) nil nil)) nil)) nil) ("5" (skosimp*) (("5" (lemma "not_one_element") (("5" (propax) nil nil)) nil)) nil) ("6" (skosimp*) (("6" (lemma "deriv_domain") (("6" (propax) nil nil)) nil)) nil) ("7" (skosimp*) (("7" (expand "derivable?" 1) (("7" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (lemma "not_one_element") (("4" (propax) nil nil)) nil)) nil) ("5" (skosimp*) (("5" (assert) (("5" (lemma "deriv_domain") (("5" (propax) nil nil)) nil)) nil)) nil) ("6" (skosimp*) (("6" (lemma "not_one_element") (("6" (propax) nil nil)) nil)) nil) ("7" (skosimp*) (("7" (lemma "deriv_domain") (("7" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (apply-extensionality 1 :hide? t) (("1" (lemma "sigma_diff_eq[1+j!1,j!1]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (hide -1) (("2" (case-replace "(LAMBDA (x: T): sigma(0, j!1 - 1, LAMBDA (i: Index[1 + j!1]): h!1(x)(i))) = (LAMBDA (x: T): sigma(0, j!1 - 1, LAMBDA (i: Index[ j!1]): h!1(x)(i)))") (("1" (hide -1) (("1" (lemma "sigma_derivable") (("1" (hide -1) (("1" (lemma "sigma_derivable") (("1" (inst - "j!1" "y!1" "(LAMBDA (x: T): LAMBDA (i: Index[j!1]): h!1(x)(i))") (("1" (assert) (("1" (skosimp*) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("1" (lemma "sigma_diff_eq[1+j!1,j!1]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 3) (("3" (hide -1) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (apply-extensionality 1 :hide? t) (("1" (hide -1) (("1" (lemma "sigma_last[below(j!1+1)]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide 3) (("2" (hide -1) (("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (lemma "deriv_domain") (("3" (propax) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (expand "derivable?" 1) (("4" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("2" (hide 3) (("2" (expand "derivable?") (("2" (skosimp*) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (lemma "not_one_element") (("4" (propax) nil nil)) nil)) nil) ("5" (skosimp*) (("5" (assert) (("5" (lemma "deriv_domain") (("5" (propax) nil nil)) nil)) nil)) nil) ("6" (skosimp*) (("6" (assert) (("6" (hide 2) (("6" (expand "derivable?" 1) (("6" (propax) nil nil)) nil)) nil)) nil)) nil) ("7" (skosimp*) (("7" (assert) nil nil)) nil) ("8" (skosimp*) (("8" (assert) nil nil)) nil) ("9" (skosimp*) (("9" (assert) (("9" (hide 2) (("9" (lemma "sigma_derivable") (("9" (inst - "n!2" "y!1" "h!1") (("9" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("10" (hide 2) (("10" (skosimp*) (("10" (assert) nil nil)) nil)) nil) ("11" (skosimp*) (("11" (assert) nil nil)) nil) ("12" (skosimp*) (("12" (assert) nil nil)) nil)) nil) ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma_last formula-decl nil sigma "reals/") (below type-eq-decl nil naturalnumbers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_diff_eq formula-decl nil sigma_below_sub "reals/") (deriv_domain formula-decl nil deriv_sigma nil) (not_one_element formula-decl nil deriv_sigma nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (sigma_derivable formula-decl nil deriv_sigma nil) (deriv_sum formula-decl nil derivatives_def "analysis/") (real_plus_real_is_real application-judgement "real" reals nil) (y!1 skolem-const-decl "T" deriv_sigma nil) (h!1 skolem-const-decl "[T -> [Index[1 + j!1] -> real]]" deriv_sigma nil) (j!1 skolem-const-decl "nat" deriv_sigma nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (deriv_const formula-decl nil derivatives_def "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (nat_induction formula-decl nil naturalnumbers nil) (deriv const-decl "Vector[n]" deriv_real_vect_def nil) (deriv const-decl "real" derivatives_def "analysis/") (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (Vector type-eq-decl nil vectors "vectors/") (derivable? const-decl "bool" deriv_real_vect_def nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (integer nonempty-type-from-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T_pred const-decl "[real -> boolean]" deriv_sigma nil) (T formal-subtype-decl nil deriv_sigma nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (< const-decl "bool" reals nil) (Index type-eq-decl nil vectors "vectors/") (below type-eq-decl nil nat_types nil) (derivable? const-decl "bool" derivatives_def "analysis/") (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak))) ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.36Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤*Eine klare Vorstellung vom Zielzustand |
|
2026-03-28