| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis_ax/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 8 kB |
|
Quelle continuous_functions_props.prf Sprache: Lisp |
|||||||||
|
(continuous_functions_props
(intermediate1 0 (intermediate1-1 nil 3473169490 ("" (skosimp) (("" (assert) (("" (auto-rewrite "sub_interval") (("" (lemma "intermediate_value2[a!1, b!1]") (("" (inst -1 "R(g!1, a!1, b!1)" "x!1") (("" (rewrite "continuous_in_subintervals") (("" (expand "R") (("" (skolem!) (("" (inst 1 "c!1") (("" (assert) nil)))))))))))))))))) nil) nil nil)) (intermediate2 0 (intermediate2-1 nil 3473169490 ("" (skosimp) (("" (assert) (("" (auto-rewrite "sub_interval") (("" (lemma "intermediate_value4[a!1, b!1]") (("" (inst -1 "R(g!1, a!1, b!1)" "x!1") (("" (rewrite "continuous_in_subintervals") (("" (expand "R") (("" (skolem!) (("" (inst 1 "c!1") (("" (assert) nil)))))))))))))))))) nil) nil nil)) (max_in_interval 0 (max_in_interval-1 nil 3473169490 ("" (skosimp) (("" (assert) (("" (auto-rewrite "sub_interval") (("" (lemma "maximum_exists[a!1, b!1]") (("" (inst -1 "R(g!1, a!1, b!1)") (("" (split) (("1" (grind :if-match nil) (("1" (inst 1 "c!1") (("1" (assert) (("1" (skosimp) (("1" (inst?) (("1" (assert) nil))))))))))) ("2" (rewrite "continuous_in_subintervals") nil)))))))))))) nil) ((is_maximum? const-decl "bool" real_fun_preds "reals/")) nil)) (min_in_interval 0 (min_in_interval-1 nil 3473169490 ("" (skosimp) (("" (assert) (("" (auto-rewrite "sub_interval") (("" (lemma "minimum_exists[a!1, b!1]") (("" (inst -1 "R(g!1, a!1, b!1)") (("" (split) (("1" (grind :if-match nil) (("1" (inst 1 "c!1") (("1" (assert) (("1" (skosimp) (("1" (inst?) (("1" (assert) nil))))))))))) ("2" (rewrite "continuous_in_subintervals") nil)))))))))))) nil) ((is_minimum? const-decl "bool" real_fun_preds "reals/")) nil)) (inj_continuous 0 (inj_continuous-1 nil 3473169490 ("" (skosimp) (("" (expand "injective?") (("" (assert) (("" (case "g!1(a!1) <= g!1(c!1)") (("1" (ground) (("1" (lemma "intermediate1" ("g" "g!1" "a" "b!1" "b" "c!1" "x" "g!1(a!1)")) (("1" (assert) (("1" (skosimp) (("1" (inst -5 "a!1" "c!2") (("1" (assert) nil))))))))) ("2" (lemma "intermediate1" ("g" "g!1" "a" "a!1" "b" "b!1" "x" "g!1(c!1)")) (("2" (assert) (("2" (skosimp) (("2" (inst -5 "c!1" "c!2") (("2" (assert) nil))))))))))) ("2" (ground) (("1" (lemma "intermediate2" ("g" "g!1" "a" "a!1" "b" "b!1" "x" "g!1(c!1)")) (("1" (assert) (("1" (skosimp) (("1" (inst -4 "c!1" "c!2") (("1" (assert) nil))))))))) ("2" (lemma "intermediate2" ("g" "g!1" "a" "b!1" "b" "c!1" "x" "g!1(a!1)")) (("2" (assert) (("2" (skosimp) (("2" (inst -4 "c!2" "a!1") (("2" (assert) nil)))))))))))))))))) nil) ((injective? const-decl "bool" functions nil) (continuous? const-decl "bool" continuous_functions nil) (T formal-subtype-decl nil continuous_functions_props nil) (T_pred const-decl "[real -> boolean]" continuous_functions_props 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) (intermediate1 formula-decl nil continuous_functions_props nil) (intermediate2 formula-decl nil continuous_functions_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (inj_monotone 0 (inj_monotone-1 nil 3473169490 ("" (skolem!) (("" (prop) (("1" (expand "strict_increasing?") (("1" (expand "strict_decreasing?") (("1" (skosimp*) (("1" (assert) (("1" (expand "injective?") (("1" (inst-cp -1 "x!1" "y!1") (("1" (inst -1 "x!2" "y!2") (("1" (assert) (("1" (case "x!1 <= x!2") (("1" (lemma "inj_continuous" ("g" "g!1" "a" "x!1" "b" "x!2" "c" "y!2")) (("1" (assert) (("1" (lemma "inj_continuous" ("g" "g!1" "a" "x!1" "b" "y!1" "c" "y!2")) (("1" (lemma "inj_continuous" ("g" "g!1" "a" "x!1" "b" "y!2" "c" "y!1")) (("1" (assert) nil))))))))) ("2" (lemma "inj_continuous" ("g" "g!1" "a" "x!2" "b" "x!1" "c" "y!1")) (("2" (assert) (("2" (lemma "inj_continuous" ("g" "g!1" "a" "x!2" "b" "y!2" "c" "y!1")) (("2" (lemma "inj_continuous" ("g" "g!1" "a" "x!2" "b" "y!1" "c" "y!2")) (("2" (assert) nil))))))))))))))))))))))))))) ("2" (grind :if-match nil) (("2" (inst-cp -3 "x1!1" "x2!1") (("2" (inst -3 "x2!1" "x1!1") (("2" (assert) nil))))))) ("3" (grind :if-match nil) (("3" (inst-cp -3 "x1!1" "x2!1") (("3" (inst -3 "x2!1" "x1!1") (("3" (assert) nil)))))))))) nil) ((strict_decreasing? const-decl "bool" real_fun_preds "reals/") (real_lt_is_strict_total_order name-judgement "(strict_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]" continuous_functions_props nil) (T formal-subtype-decl nil continuous_functions_props nil) (inj_continuous formula-decl nil continuous_functions_props nil) (continuous? const-decl "bool" continuous_functions nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (<= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (injective? const-decl "bool" functions nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (NOT const-decl "[bool -> bool]" booleans nil)) nil))) ¤ Dauer der Verarbeitung: 0.28 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28