| products/sources/formale Sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: integral_bounded.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(integral_bounded
(IMP_integral_prep_TCC1 0 (IMP_integral_prep_TCC1-1 nil 3282561874 ("" (lemma "connected_domain") (("" (propax) nil nil)) nil) ((connected_domain formula-decl nil integral_bounded nil)) shostak)) (IMP_integral_prep_TCC2 0 (IMP_integral_prep_TCC2-1 nil 3282561874 ("" (lemma "not_one_element") (("" (propax) nil nil)) nil) ((not_one_element formula-decl nil integral_bounded nil)) shostak)) (int_to_bnd_TCC1 0 (int_to_bnd_TCC1-1 nil 3282561874 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (int_to_bnd_TCC2 0 (int_to_bnd_TCC2-1 nil 3282561874 ("" (skosimp*) (("" (assert) nil nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (int_to_bnd 0 (int_to_bnd-2 nil 3477651374 ("" (skosimp*) (("" (case "(FORALL (eps: posreal): (EXISTS (EP: partition[T](a!1,b!1)): (FORALL (j: below(length(EP)-1)): FORALL (xx: real): (EP(j) <= xx AND xx <= EP(j+1)) IMPLIES abs(f!1(xx) - f!1(EP(j))) < eps/abs(EP(j+1) - EP(j)))))") (("1" (assert) (("1" (inst - "1000") (("1" (skosimp*) (("1" (inst + "EP!1") (("1" (skosimp*) (("1" (inst - "j!1") (("1" (expand "bounded_on?") (("1" (inst + "1000 / abs(EP!1`seq(1 + j!1) - EP!1`seq(j!1)) + abs(f!1(EP!1`seq(j!1)))") (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (lemma "abs_diff") (("1" (inst - "f!1(x!1)" "f!1(EP!1`seq(j!1))") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "EP!1") (("2" (inst - "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (lemma "Lemma_1[T]") (("2" (inst?) (("2" (assert) (("2" (inst -1 "eps!1") (("2" (skosimp*) (("2" (name "EP" "eq_partition(a!1,b!1,floor((b!1-a!1)/delta!1) + 2)") (("1" (inst + "EP") (("1" (skosimp*) (("1" (case "T_pred(xx!1)") (("1" (case "abs(EP`seq(1 + j!1) - EP`seq(j!1)) > 0") (("1" (cross-mult 1) (("1" (hide -1) (("1" (name "SecJ" "(EP`seq(1 + j!1) - EP`seq(j!1))") (("1" (name "F_DIF" "(f!1((EP)(j!1)) - f!1(xx!1))") (("1" (assert) (("1" (rewrite "abs_mult" :dir rl) (("1" (case-replace "EP`seq(1 + j!1) * f!1(xx!1) - EP`seq(j!1) * f!1(xx!1) + (EP`seq(j!1) * f!1(EP`seq(j!1))- EP`seq(1 + j!1) * f!1(EP`seq(j!1))) = -SecJ*F_DIF") (("1" (hide -1) (("1" (lemma "abs_neg") (("1" (inst - "SecJ * F_DIF") (("1" (replace -1) (("1" (hide -1) (("1" (inst - "EP" "EP" "gxis(a!1,b!1,EP,j!1,true,xx!1)" "gxis(a!1,b!1,EP,j!1,false,xx!1)") (("1" (split -5) (("1" (expand "Rie_sum") (("1" (assert) (("1" (assert) (("1" (rewrite "sigma_minus[below[length(EP)-1]]") (("1" (case-replace "(LAMBDA (i: below(length(EP) - 1)): EP`seq(i) * f!1(gxis(a!1, b!1, EP, j!1, FALSE, xx!1)(i)) + EP`seq(1 + i) * f!1(gxis(a!1, b!1, EP, j!1, TRUE, xx!1)(i)) - EP`seq(i) * f!1(gxis(a!1, b!1, EP, j!1, TRUE, xx!1)(i)) - EP`seq(1 + i) * f!1(gxis(a!1, b!1, EP, j!1, FALSE, xx!1)(i))) = (LAMBDA (i: below(length(EP) - 1)): IF i = j!1 THEN (EP`seq(1 + j!1) - EP`seq(j!1)) * (f!1(EP(j!1)) - f!1(xx!1)) ELSE 0 ENDIF)") (("1" (assert) (("1" (hide -1) (("1" (case-replace "EP`seq(1 + j!1) * f!1(EP`seq(j!1)) - EP`seq(1 + j!1) * f!1(xx!1) + (EP`seq(j!1) * f!1(xx!1) - EP`seq(j!1) * f!1(EP`seq(j!1))) = SecJ*F_DIF") (("1" (hide -1) (("1" (case "j!1 < length(EP) - 2") (("1" (lemma "sigma_below[length(EP)-1].sigma_split_ge") (("1" (inst - "_" "length(EP) - 2" "0" "j!1") (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "sigma(1 + j!1, length(EP) - 2, (LAMBDA (i: below(length(EP) - 1)): IF i = j!1 THEN SecJ * F_DIF ELSE 0 ENDIF)) = 0") (("1" (hide -1) (("1" (rewrite "sigma_last_ge") (("1" (assert) (("1" (case "sigma(0, j!1 - 1, (LAMBDA (i: below(length(EP) - 1)): IF i = j!1 THEN SecJ * F_DIF ELSE 0 ENDIF)) = 0") (("1" (assert) nil nil) ("2" (lemma "sigma_restrict_eq[below(length(EP)-1)]") (("2" (inst?) (("2" (inst - "(LAMBDA (i: below(length(EP) - 1)): 0)") (("2" (expand "restrict") (("2" (replace -1) (("2" (hide -1) (("2" (lemma "sigma_const[below(length(EP)-1)]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_restrict_eq[below(length(EP)-1)]") (("1" (inst?) (("1" (inst - "(LAMBDA (i: below(length(EP) - 1)): 0)") (("1" (expand "restrict") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_const[below(length(EP)-1)]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1 = length(EP) - 2") (("1" (rewrite "sigma_last_ge") (("1" (case-replace "sigma(0, length(EP) - 3, (LAMBDA (i: below(length(EP) - 1)): IF i = j!1 THEN SecJ * F_DIF ELSE 0 ENDIF)) = 0") (("1" (assert) nil nil) ("2" (lemma "sigma_restrict_eq[below(length(EP)-1)]") (("1" (inst?) (("1" (inst - "(LAMBDA (i: below(length(EP) - 1)): 0)") (("1" (expand "restrict") (("1" (assert) (("1" (lemma "sigma_const[below(length(EP)-1)]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "gxis") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "gxis") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "N_from_delta") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("3" (lemma "N_from_delta") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "EP") (("2" (inst - "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "connected_domain") (("2" (expand "connected?") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "(b!1 - a!1) / delta!1 > 0") (("1" (assert) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (typepred "EP!1") (("3" (inst - "j!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (lemma "connected_domain") (("4" (expand "connected?") (("4" (inst - "_" "_" "xx!1") (("4" (inst?) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T formal-subtype-decl nil integral_bounded nil) (T_pred const-decl "[real -> boolean]" integral_bounded nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (a!1 skolem-const-decl "T" integral_bounded nil) (b!1 skolem-const-decl "T" integral_bounded nil) (EP!1 skolem-const-decl "partition[T](a!1, b!1)" integral_bounded nil) (j!1 skolem-const-decl "below(length(EP!1) - 1)" integral_bounded nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (abs_diff formula-decl nil abs_lems "reals/") (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) (int_minus_int_is_int application-judgement "int" integers nil) (bounded_on? const-decl "bool" integral_bounded nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Lemma_1 formula-decl nil integral_prep nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (j!1 skolem-const-decl "below(length(EP) - 1)" integral_bounded nil) (EP skolem-const-decl "{fs: finite_sequence[{x | a!1 <= x AND x <= b!1}] | length(fs) > 1 AND seq(fs)(0) = a!1 AND seq(fs)(length(fs) - 1) = b!1 AND (FORALL (ii: below(length(fs) - 1)): seq(fs)(ii) < seq(fs)(1 + ii))}" integral_bounded nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (minus_real_is_real application-judgement "real" reals nil) (abs_neg formula-decl nil abs_lems "reals/") (FALSE const-decl "bool" booleans nil) (TRUE const-decl "bool" booleans nil) (gxis const-decl "(xis?(a, b, P))" integral_prep nil) (xis? const-decl "bool" integral_def nil) (N_from_delta formula-decl nil integral_def nil) (Rie_sum const-decl "real" integral_def nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sigma_split_ge formula-decl nil sigma_below "reals/") (sigma_restrict_eq formula-decl nil sigma "reals/") (sigma_nat application-judgement "nat" sigma_below "reals/") (sigma_const formula-decl nil sigma "reals/") (int_times_even_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (restrict const-decl "[T -> real]" sigma "reals/") (sigma_last_ge formula-decl nil sigma_below "reals/") (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma def-decl "real" sigma "reals/") (int_below type-eq-decl nil sigma_below "reals/") (sigma_minus formula-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (real_times_real_is_real application-judgement "real" reals nil) (abs_mult formula-decl nil real_props nil) (connected_domain formula-decl nil integral_bounded nil) (connected? const-decl "bool" deriv_domain_def nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (integer nonempty-type-from-decl nil integers nil) (eq_partition const-decl "partition(a, b)" integral_def nil) (above nonempty-type-eq-decl nil integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil) (int_to_bnd-1 nil 3282561219 ("" (skosimp*) (("" (case "(FORALL (eps: posreal): (EXISTS (EP: partition[T](a!1,b!1)): (FORALL (j: below(length(EP)-1)): FORALL (xx: real): (EP(j) <= xx AND xx <= EP(j+1)) IMPLIES abs(f!1(xx) - f!1(EP(j))) < eps/abs(EP(j+1) - EP(j)))))") (("1" (assert) (("1" (inst - "1000") (("1" (skosimp*) (("1" (inst + "EP!1") (("1" (skosimp*) (("1" (inst - "j!1") (("1" (expand "bounded_on?") (("1" (inst + "1000 / abs(EP!1`seq(1 + j!1) - EP!1`seq(j!1)) + abs(f!1(EP!1`seq(j!1)))") (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (lemma "abs_diff") (("1" (inst - "f!1(x!1)" "f!1(EP!1`seq(j!1))") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "EP!1") (("2" (inst - "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (lemma "Lemma_1[T]") (("2" (inst?) (("2" (assert) (("2" (inst -1 "eps!1") (("2" (skosimp*) (("2" (name "EP" "eq_partition(a!1,b!1,floor((b!1-a!1)/delta!1) + 2)") (("1" (inst + "EP") (("1" (skosimp*) (("1" (case "T_pred(xx!1)") (("1" (case "abs(EP`seq(1 + j!1) - EP`seq(j!1)) > 0") (("1" (cross-mult 1) (("1" (hide -1) (("1" (name "SecJ" "(EP`seq(1 + j!1) - EP`seq(j!1))") (("1" (name "F_DIF" "(f!1((EP)(j!1)) - f!1(xx!1))") (("1" (assert) (("1" (rewrite "abs_mult" :dir rl) (("1" (case-replace "EP`seq(1 + j!1) * f!1(xx!1) - EP`seq(j!1) * f!1(xx!1) + (EP`seq(j!1) * f!1(EP`seq(j!1))- EP`seq(1 + j!1) * f!1(EP`seq(j!1))) = -SecJ*F_DIF") (("1" (hide -1) (("1" (lemma "abs_neg") (("1" (inst - "SecJ * F_DIF") (("1" (replace -1) (("1" (hide -1) (("1" (inst - "EP" "EP" "gxis(a!1,b!1,EP,j!1,true,xx!1)" "gxis(a!1,b!1,EP,j!1,false,xx!1)") (("1" (split -5) (("1" (expand "Rie_sum") (("1" (assert) (("1" (assert) (("1" (rewrite "sigma_minus[below[length(EP)-1]]") (("1" (case-replace "(LAMBDA (i: below(length(EP) - 1)): EP`seq(i) * f!1(gxis(a!1, b!1, EP, j!1, FALSE, xx!1)(i)) + EP`seq(1 + i) * f!1(gxis(a!1, b!1, EP, j!1, TRUE, xx!1)(i)) - EP`seq(i) * f!1(gxis(a!1, b!1, EP, j!1, TRUE, xx!1)(i)) - --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.37 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
