| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 27 kB |
|
Quellcode-Bibliothek inverse_continuous_functions.prf Sprache: Lisp |
|||||||||
|
(inverse_continuous_functions
(inverse_incr 0 (inverse_incr-1 nil 3324805607 ("" (skosimp) (("" (assert) (("" (expand "bijective?") (("" (expand "continuous?") (("" (skosimp) (("" (delete -1) (("" (expand "continuous?") (("" (expand "surjective?") (("" (inst-cp -1 "x0!1") (("" (skolem!) (("" (case-replace "inverse(g!1)(x0!1) = x!1") (("1" (delete -1) (("1" (skolem!) (("1" (case "EXISTS (d : posreal) : FORALL (u : T1) : x0!1 - g!1(u) < d IMPLIES x!1 - u < epsilon!1") (("1" (case "EXISTS (d : posreal) : FORALL (u : T1) : g!1(u) - x0!1 < d IMPLIES u - x!1 < epsilon!1") (("1" (skosimp*) (("1" (inst 1 "min(d!1, d!2)") (("1" (skosimp) (("1" (inst -3 "x!2") (("1" (skolem!) (("1" (case-replace "inverse(g!1)(x!2) = x!3") (("1" (delete -1) (("1" (inst -1 "x!3") (("1" (inst -2 "x!3") (("1" (delete -5) (("1" (grind :exclude "min") nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "bijective_inverse") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete -1 -2 2) (("2" (case "EXISTS (v : T1) : x!1 + epsilon!1 = v") (("1" (skolem!) (("1" (expand "strict_increasing?") (("1" (inst-cp -3 "x!1" "v!1") (("1" (assert) (("1" (assert) (("1" (inst 1 "g!1(v!1) - x0!1") (("1" (skosimp) (("1" (inst -4 "v!1" "u!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst 2 "1") (("2" (skosimp) (("2" (lemma "connected_domain") (("2" (inst -1 "x!1" "u!1" "x!1 + epsilon!1") (("2" (assert) (("2" (inst + "epsilon!1 + x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete -1 2) (("2" (case "EXISTS (v : T1) : x!1 - epsilon!1 = v") (("1" (skolem!) (("1" (expand "strict_increasing?") (("1" (inst-cp -3 "v!1" "x!1") (("1" (assert) (("1" (assert) (("1" (inst 1 "x0!1 - g!1(v!1)") (("1" (skosimp) (("1" (inst -4 "u!1" "v!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst 2 "1") (("2" (skosimp) (("2" (lemma "connected_domain") (("2" (inst -1 "u!1" "x!1" "x!1 - epsilon!1") (("2" (assert) (("2" (inst + "-epsilon!1 + x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "bijective_inverse") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous? const-decl "bool" continuous_functions nil) (surjective? const-decl "bool" functions nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (connected_domain formula-decl nil inverse_continuous_functions 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (bijective_inverse formula-decl nil function_inverse nil) (minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (posreal_min application-judgement "{z: posreal | z <= x AND z <= y}" real_defs nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (inverse const-decl "D" function_inverse nil) (T1 formal-nonempty-subtype-decl nil inverse_continuous_functions nil) (T1_pred const-decl "[real -> boolean]" inverse_continuous_functions nil) (= const-decl "[T, T -> boolean]" equalities nil) (T2 formal-nonempty-subtype-decl nil inverse_continuous_functions nil) (T2_pred const-decl "[real -> boolean]" inverse_continuous_functions 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) (continuous? const-decl "bool" continuous_functions nil) (real_minus_real_is_real application-judgement "real" reals nil) (bijective? const-decl "bool" functions nil)) nil)) (inverse_decr 0 (inverse_decr-1 nil 3324805607 ("" (skosimp) (("" (assert) (("" (expand "bijective?") (("" (expand "continuous?") (("" (skosimp) (("" (delete -1) (("" (expand "continuous?") (("" (expand "surjective?") (("" (inst-cp -1 "x0!1") (("" (skolem!) (("" (skolem!) (("" (case-replace "inverse(g!1)(x0!1) = x!1") (("1" (delete -1) (("1" (case "EXISTS (d : posreal) : FORALL (u : T1) : x0!1 - g!1(u) < d IMPLIES u - x!1 < epsilon!1") (("1" (case "EXISTS (d : posreal) : FORALL (u : T1) : g!1(u) - x0!1 < d IMPLIES x!1 - u < epsilon!1") (("1" (skosimp*) (("1" (inst 1 "min(d!1, d!2)") (("1" (skosimp) (("1" (inst -3 "x!2") (("1" (skolem!) (("1" (case-replace "inverse(g!1)(x!2) = x!3") (("1" (delete -1) (("1" (inst -1 "x!3") (("1" (inst -2 "x!3") (("1" (grind :exclude ("min" "strict_decreasing?")) nil nil)) nil)) nil)) nil) ("2" (rewrite "bijective_inverse") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete -1 -2 2) (("2" (case "EXISTS (v : T1) : x!1 - epsilon!1 = v") (("1" (skolem!) (("1" (expand "strict_decreasing?") (("1" (inst-cp -3 "v!1" "x!1") (("1" (assert) (("1" (assert) (("1" (inst 1 "g!1(v!1) - x0!1") (("1" (skosimp) (("1" (inst -4 "u!1" "v!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst 2 "1") (("2" (skosimp) (("2" (lemma "connected_domain") (("2" (inst -1 "u!1" "x!1" "x!1 - epsilon!1") (("2" (assert) (("2" (inst + "-epsilon!1 + x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete -1 2) (("2" (case "EXISTS (v : T1) : x!1 + epsilon!1 = v") (("1" (skolem!) (("1" (expand "strict_decreasing?") (("1" (inst-cp -3 "x!1" "v!1") (("1" (assert) (("1" (assert) (("1" (inst 1 "x0!1 - g!1(v!1)") (("1" (skosimp) (("1" (inst -4 "v!1" "u!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst 2 "1") (("2" (skosimp) (("2" (lemma "connected_domain") (("2" (inst -1 "x!1" "u!1" "x!1 + epsilon!1") (("2" (assert) (("2" (inst + "epsilon!1 + x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "bijective_inverse") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous? const-decl "bool" continuous_functions nil) (surjective? const-decl "bool" functions nil) (= const-decl "[T, T -> boolean]" equalities nil) (T1_pred const-decl "[real -> boolean]" inverse_continuous_functions nil) (T1 formal-nonempty-subtype-decl nil inverse_continuous_functions nil) (inverse const-decl "D" function_inverse nil) (bool nonempty-type-eq-decl nil booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (connected_domain formula-decl nil inverse_continuous_functions nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types 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) (strict_decreasing? const-decl "bool" real_fun_preds "reals/") (bijective_inverse formula-decl nil function_inverse nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (posreal_min application-judgement "{z: posreal | z <= x AND z <= y}" real_defs nil) (T2 formal-nonempty-subtype-decl nil inverse_continuous_functions nil) (T2_pred const-decl "[real -> boolean]" inverse_continuous_functions 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) (continuous? const-decl "bool" continuous_functions nil) (real_minus_real_is_real application-judgement "real" reals nil) (bijective? const-decl "bool" functions nil)) nil)) (inverse_continuous 0 (inverse_continuous-1 nil 3324805607 ("" (skosimp) (("" (assert) (("" (expand "bijective?") (("" (flatten) (("" (use "inj_monotone[T1]") (("1" (ground) (("1" (rewrite "inverse_incr") nil) ("2" (rewrite "inverse_decr") nil) ("3" (expand "injective?") (("3" (propax) nil))))) ("2" (lemma "connected_domain") (("2" (skosimp) (("2" (inst -1 "x!1" "y!1" "z!1") (("2" (assert) nil)))))))))))))))) nil) ((connected_domain formula-decl nil inverse_continuous_functions nil) (inverse_incr formula-decl nil inverse_continuous_functions nil) (inverse_decr formula-decl nil inverse_continuous_functions nil) (injective? const-decl "bool" functions nil) (continuous? const-decl "bool" continuous_functions nil) (T2_pred const-decl "[real -> boolean]" inverse_continuous_functions nil) (T2 formal-nonempty-subtype-decl nil inverse_continuous_functions nil) (T1 formal-nonempty-subtype-decl nil inverse_continuous_functions nil) (T1_pred const-decl "[real -> boolean]" inverse_continuous_functions 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) (inj_monotone formula-decl nil continuous_functions_props nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (bijective? const-decl "bool" functions 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.18Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28