| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 54 kB |
|
Quelle interval_minmax.prf Sprache: Lisp |
|||||||||
|
(interval_minmax
(min_x_TCC1 0 (min_x_TCC1-1 nil 3253546854 ("" (case "FORALL (a: T, b: {x: T | a < x}, f: fun_cont_on(a, b)): continuous?[J[a, b]](restrict[T, J[a, b], real](f))") (("1" (inst + "(LAMBDA (a: T, b: {x: T | a < x}, f: fun_cont_on(a, b)): min_pt[a,b](restrict[T,J[a,b],real](f)))") (("1" (skosimp*) (("1" (prop) (("1" (name "mp" "min_pt[a!1, b!1](restrict[T, J[a!1, b!1], real](f!1))") (("1" (replace -1) (("1" (typepred "mp") (("1" (lemma "connected_domain") (("1" (expand "connected?") (("1" (inst?) (("1" (inst -1 "b!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (assert) (("2" (typepred "x!1") (("2" (lemma "connected_domain") (("2" (expand "connected?") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil) ("4" (skosimp*) (("4" (assert) (("4" (typepred "min_pt[a!1, b!1](restrict[T, J[a!1, b!1], real](f!1))") (("1" (expand "is_minimum?") (("1" (inst - "x!1") (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -3) (("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (expand "connected?") (("2" (inst - "a!1" "b!1" "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "x!1") (("2" (lemma "connected_domain") (("2" (expand "connected?") (("2" (inst?) (("2" (inst -1 "b!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (typepred "f!1") (("2" (expand "continuous?" 1) (("2" (skosimp*) (("2" (inst?) (("1" (assert) (("1" (expand "restrict") (("1" (expand "continuous?") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "connected_domain") (("2" (expand "connected?") (("2" (inst?) (("2" (assert) (("2" (typepred "x0!1") (("2" (inst - a!1 b!1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (typepred "x!1") (("3" (lemma "connected_domain") (("3" (expand "connected?") (("3" (inst?) (("3" (inst -1 "b!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals 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) (real_lt_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) (x0!1 skolem-const-decl "J[a!1, b!1]" interval_minmax nil) (b!1 skolem-const-decl "{x: T | a!1 < x}" interval_minmax nil) (a!1 skolem-const-decl "T" interval_minmax nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (is_minimum? const-decl "bool" real_fun_preds "reals/") (min_pt const-decl "{xj: J | is_minimum?(xj, f)}" continuity_interval nil) (connected_domain formula-decl nil interval_minmax nil) (connected? const-decl "bool" deriv_domain_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities 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) (T_pred const-decl "[real -> boolean]" interval_minmax nil) (T formal-subtype-decl nil interval_minmax nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (continuous? const-decl "bool" continuous_functions nil) (restrict const-decl "R" restrict nil) (fun_cont_on type-eq-decl nil interval_minmax nil) (J nonempty-type-eq-decl nil continuity_interval nil) (continuous? const-decl "bool" continuous_functions nil)) nil)) (max_x_TCC1 0 (max_x_TCC1-2 nil 3477750694 ("" (case "FORALL (a: T, b: {x: T | a < x}, f: fun_cont_on(a, b)): continuous?[J[a, b]](restrict[T, J[a, b], real](f))") (("1" (inst + "(LAMBDA (a: T, b: {x: T | a < x}, f: fun_cont_on(a, b)): max_pt[a,b](restrict[T,J[a,b],real](f)))") (("1" (skosimp*) (("1" (prop) (("1" (name "mp" "max_pt[a!1, b!1](restrict[T, J[a!1, b!1], real](f!1))") (("1" (replace -1) (("1" (typepred "mp") (("1" (lemma "connected_domain") (("1" (expand "connected?") (("1" (inst?) (("1" (inst -1 "b!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (lemma "connected_domain") (("2" (expand "connected?") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil) ("4" (skosimp*) (("4" (assert) (("4" (typepred "max_pt[a!1, b!1](restrict[T, J[a!1, b!1], real](f!1))") (("1" (expand "is_maximum?") (("1" (inst - "x!1") (("1" (expand "restrict") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -3) (("2" (lemma "connected_domain") (("2" (expand "connected?") (("2" (assert) (("2" (skosimp*) (("2" (inst - "a!1" "b!1" "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "x!1") (("2" (lemma "connected_domain") (("2" (expand "connected?") (("2" (inst?) (("2" (inst -1 "b!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (typepred "f!1") (("2" (expand "continuous?" 1) (("2" (skosimp*) (("2" (inst?) (("1" (assert) (("1" (expand "restrict") (("1" (expand "continuous?") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "connected_domain") (("2" (expand "connected?") (("2" (inst?) (("2" (inst - a!1 b!1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (typepred "x!1") (("3" (lemma "connected_domain") (("3" (expand "connected?") (("3" (inst?) (("3" (inst -1 "b!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (x0!1 skolem-const-decl "J[a!1, b!1]" interval_minmax nil) (b!1 skolem-const-decl "{x: T | a!1 < x}" interval_minmax nil) (a!1 skolem-const-decl "T" interval_minmax nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (is_maximum? const-decl "bool" real_fun_preds "reals/") (max_pt const-decl "{xj: J | is_maximum?(xj, f)}" continuity_interval nil) (connected_domain formula-decl nil interval_minmax nil) (connected? const-decl "bool" deriv_domain_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (T_pred const-decl "[real -> boolean]" interval_minmax nil) (T formal-subtype-decl nil interval_minmax nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (continuous? const-decl "bool" continuous_functions nil) (restrict const-decl "R" restrict nil) (fun_cont_on type-eq-decl nil interval_minmax nil) (J nonempty-type-eq-decl nil continuity_interval nil) (continuous? const-decl "bool" continuous_functions nil)) nil) (max_x_TCC1-1 nil 3253546854 ("" (case "FORALL (a: T, b: {x: T | a < x}, f: fun_cont_on(a, b)): continuous?[J[a, b]](restrict[T, J[a, b], real](f))") (("1" (inst + "(LAMBDA (a: T, b: {x: T | a < x}, f: fun_cont_on(a, b)): max_pt[a,b](restrict[T,J[a,b],real](f)))") (("1" (skosimp*) (("1" (prop) (("1" (name "mp" "max_pt[a!1, b!1](restrict[T, J[a!1, b!1], real](f!1))") (("1" (replace -1) (("1" (typepred "mp") (("1" (lemma "connected_domain") (("1" (inst?) (("1" (inst -1 "b!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "x1!1") (("2" (lemma "connected_domain") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil) ("4" (skosimp*) (("4" (assert) (("4" (typepred "max_pt[a!1, b!1](restrict[T, J[a!1, b!1], real](f!1))") (("1" (expand "is_maximum?") (("1" (inst - "x!1") (("1" (expand "restrict") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (inst?) (("2" (hide -3) (("2" (lemma "connected_domain") (("2" (assert) (("2" (skosimp*) (("2" (inst - "a!1" "b!1" "x1!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "x1!1") (("2" (lemma "connected_domain") (("2" (inst?) (("2" (inst -1 "b!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (typepred "f!1") (("2" (expand "continuous?" 1) (("2" (skosimp*) (("2" (inst?) (("1" (assert) (("1" (expand "restrict") (("1" (expand "continuous?") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "connected_domain") (("2" (inst?) (("2" (inst - a!1 b!1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (typepred "x1!1") (("3" (lemma "connected_domain") (("3" (inst?) (("3" (inst -1 "b!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((is_maximum? const-decl "bool" real_fun_preds "reals/") (max_pt const-decl "{xj: J | is_maximum?(xj, f)}" continuity_interval nil) (closed_interval type-eq-decl nil intervals_real "reals/") (J nonempty-type-eq-decl nil continuity_interval nil)) nil))) ¤ 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.0.16Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28