(metric_space_real_funnil 3462120666"" (lemma "fullset_metric_space" ) (("" (propax) nil nil )) nil )nil metric_space_real_fun nil ))nil ))nil 3462120666"" (lemma "real_metric_space" )"" (inst - "fullset[real]" ) nil nil )) nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )set type-eq-decl nil sets nil ) (fullset const-decl "set" sets nil )nil real_metric_space nil ))nil ))nil 3462120679"" (skosimp*)"" (expand "continuous?" )"" (skosimp*)"" (inst - "x!1" )"" (expand "continuous_at?" )"" (skosimp*)"" (case "c!1 = 0" )"1" (grind) nil nil )"2" (inst - "epsilon!1/abs(c!1)" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (inst - "y!1" )"1" (expand "member" )"1" (expand "ball" )"1" expand "*" )"1" expand "real_dist" )"1" "1" "1" "abs_mult" )"1" "f!1(x!1) - f!1(y!1)" "c!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (prop)"1" (cross-mult 1) (("1" (assert ) nil nil )) nil )"2" (cross-mult 1) (("2" (assert ) nil nil )) nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" continuity_ms_def nil )nil metric_space_real_fun nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"nzreal" nil )"real" metric_space_real_fun nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )"boolean" notequal nil )"posreal" metric_space_real_fun nil )nil real_types nil )"bool" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )nil abs_lems "reals/" )"nnreal" nil )nil real_props nil )nil extra_real_props nil )nil real_props nil )"set[T]" metric_spaces nil )"bool" sets nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"nnreal" real_metric_space nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"real" reals nil )nil numbers nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" continuity_ms_def nil ))nil 3462121435"" (skosimp*)"" (lemma "scal_continuous" )"" (inst - "S!1" "-1" "f!1" ) (("" (grind) nil nil )) nil )) nil ))nil )nil metric_space_real_fun nil )"set[T]" metric_spaces nil )"bool" sets nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"nnreal" real_metric_space nil )"[T, T -> nnreal]" metric_space_real_fun nil )nil real_types nil )"bool" reals nil )"bool" continuity_ms_def nil )"bool" continuity_ms_def nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"real" reals nil )"real" reals nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil metric_space_real_fun nil )"odd_int" integers nil ))nil 3462121520"" (skosimp*)"" (expand "continuous?" )"" (skosimp*)"" (inst - "x!1" )"" (inst - "x!1" )"" (expand "continuous_at?" )"" (skosimp*)"" (inst - "epsilon!1/2" )"" (inst - "epsilon!1/2" )"" (skosimp*)"" (inst + "min(delta!1,delta!2)" )"" (skosimp*)"" (inst - "y!1" )"" (inst - "y!1" )"" expand "member" )"" expand "ball" )"" expand "real_dist" )"" expand "+" )"" "triangle" )"" "f!1(x!1) - f!1(y!1)" "g!1(x!1) - g!1(y!1)" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" continuity_ms_def nil )nil metric_space_real_fun nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" continuity_ms_def nil )"posreal" nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"set[T]" metric_spaces nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"nnreal" nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"nnreal" real_metric_space nil )"real" reals nil )"bool" sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"{z: posreal | z <= x AND z <= y}" real_defs nil ))nil 3462121763"" (skosimp*)"" (expand "continuous?" )"" (skosimp*)"" (inst - "x!1" )"" (inst - "x!1" )"" (expand "continuous_at?" )"" (skosimp*)"" (inst - "epsilon!1/2" )"" (inst - "epsilon!1/2" )"" (skosimp*)"" (inst + "min(delta!1,delta!2)" )"" (skosimp*)"" (inst - "y!1" )"" (inst - "y!1" )"" expand "member" )"" expand "ball" )"" expand "-" )"" expand "real_dist" )"" "triangle" )"" "f!1(x!1) - f!1(y!1)" "-g!1(x!1) + g!1(y!1)" )"" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" continuity_ms_def nil )nil metric_space_real_fun nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" continuity_ms_def nil )"posreal" nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"set[T]" metric_spaces nil )"real" reals nil )"real" reals nil )"nnreal" real_metric_space nil )"real" reals nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"odd_int" integers nil )nil real_props nil )"[T -> real]" real_fun_ops "reals/" )"bool" sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"{z: posreal | z <= x AND z <= y}" real_defs nil ))nil )nil 3462121727";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" ";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" expand "continuous?" )";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" ";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" "x!1" )";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" "x!1" )";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" expand "continuous_at?" )";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" ";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" "epsilon!1/2" )";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" "epsilon!1/2" )";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" ";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" "min(delta!1,delta!2)" )";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" ";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" "y!1" )";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" "y!1" )";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" expand "member" )";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" expand "ball" )";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" expand "real_dist" )";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" expand "+" )";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" "triangle" )";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" "f!1(x!1) - f!1(y!1)" "g!1(x!1) - g!1(y!1)" )";;; Proof sum_continuous-1 for formula metric_space_real_fun.sum_continuous" assert )nil ))))))))))))))))))))))))))))))))))))))))";;; developed with shostak decision procedures") nil nil ))nil 3462270340"" (skosimp*)"" (expand "continuous?" )"" (skosimp*)"" (inst - "x!1" )"" (inst - "x!1" )"" (expand "continuous_at?" )"" (skosimp*)"" (case "g!1(x!1) = 0" )"1" (inst - "1" )"1" (inst - "epsilon!1/(abs(f!1(x!1)) + 1)" )"1" (skosimp*)"1" (inst + "min(delta!1,delta!2)" )"1" (skosimp*)"1" (inst - "y!1" )"1" "y!1" )"1" expand "member" )"1" expand "ball" )"1" expand "*" )"1" replace -1)"1" expand "real_dist" )"1" "abs_mult" )"1" "-1" "f!1(y!1)*g!1(y!1)" )"1" replace -1)"1" expand "abs" 1 1)"1" "1" "1" "triangle" )"1" "f!1(x!1) - f!1(y!1)" "- f!1(x!1)" )"1" case "abs(f!1(x!1) - f!1(y!1) + -f!1(x!1)) = abs(f!1(y!1))" )"1" replace "1" "1" assert )"1" "1" case "abs(-1 * g!1(y!1)) = abs(g!1(y!1))" )"1" replace "1" "1" case "abs(-1 * f!1(x!1)) = abs(f!1(x!1))" )"1" replace "1" "1" "1" "-" "abs(f!1(x!1) - f!1(y!1))" "1" assert )"1" "abs(g!1(y!1))" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (label "fcont" -1)"2" (label "gcont" -2)"2" (name "ep1" "epsilon!1/(2*abs(g!1(x!1)))" )"1" "ep2" "epsilon!1/(2*(abs(f!1(x!1)) + ep1))" )"1" (label "ep1name" -2)"1" (label "ep2name" -1)"1" "ep1" )"1" "ep2" )"1" "1" "min(delta!1,delta!2)" )"1" "1" "y!1" )"1" "y!1" )"1" expand "member" )"1" expand "ball" )"1" "fcont" )"1" "fct2" -1)"1" "fct2" )"1" replace "ep1name" "1" replace "ep2name" "1" "mindelta" "1" expand "real_dist" )"1" "1" "1" "1" expand "*" )"1" "triangle" )"1" "f!1(x!1) * g!1(x!1) - f!1(y!1) * g!1(x!1)" " f!1(y!1) * g!1(x!1) - ") "1" assert )"1" "abs_mult" )"1" "f!1(x!1)-f!1(y!1)" "g!1(x!1)" )"1" assert )"1" replace "1" "abs_mult" )"1" "f!1(y!1)" "g!1(x!1) - g!1(y!1)" )"1" assert )"1" replace "1" "1" "1" "ep1name" )"1" "ep2name" )"1" "finaltop" "1" "mindelta" )"1" "ep1name" )"1" case "abs(f!1(y!1)) <= abs(f!1(x!1)) + ep1" )"1" replace "ep1name" "1" "ep1name" )"1" "A" "f!1(x!1)" )"1" "B" "f!1(y!1)" )"1" "X" "g!1(x!1)" )"1" "Y" "g!1(y!1)" )"1" "yname" "1" "xname" "1" "bname" "1" "aname" "1" replace "aname" )"1" replace "bname" )"1" replace "xname" )"1" replace "yname" )"1" "aname" )"1" "bname" )"1" "xname" )"1" "yname" )"1" "gcont" )"1" "myvar" "abs(A) + epsilon!1 / (2 * abs(X))" )"1" "namemyvar" "1" replace "namemyvar" )"1" "namemyvar" )"1" "nmv2" "1" case "2=2" )"1" "1" assert )"1" replace "1" "1" "nmv2" )"1" "1" nil nil )"2" "1" case "myvar > 0" )"1" nil nil )"2" nil nil ))nil )"2" nil nil )"3" nil nil )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "fct2" )"2" "mindelta" )"2" assert )"2" expand "real_dist" )"2" "triangle" )"2" "-f!1(x!1)" "f!1(x!1)-f!1(y!1)" )"2" assert )"2" "mindelta" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ep2name" "ep1name" 1 2))"2" "pos_div_lt" )"2" "(2 * (abs(f!1(x!1)) + ep1))" "epsilon!1" )"2" assert )"2" "pos_div_lt" )"2" "(2 * abs(g!1(x!1)))" "epsilon!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ep2name" "ep1name" 1 2))"2" "pos_div_lt" )"2" "2" "(2 * (abs(f!1(x!1)) + ep1))" "epsilon!1" )"2" "(2 * abs(g!1(x!1)))" "epsilon!1" )"2" replace "ep2name" )"2" replace "ep1name" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "pos_div_lt" )"2" "(2 * abs(g!1(x!1)))" "epsilon!1" )"2" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" continuity_ms_def nil )nil metric_space_real_fun nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" continuity_ms_def nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil numbers nil )"posreal" nil )"posreal" nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"{z: posreal | z <= x AND z <= y}" real_defs nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )"posreal" nil )"bool" sets nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"real" reals nil )"nnreal" real_metric_space nil )"odd_int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"nnreal" nil )"(total_order?[real])" nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil real_props nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )"(total_order?[real])" nil )nil real_props nil )"set[T]" metric_spaces nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"nzreal" nil )"nzreal" metric_space_real_fun nil )"(S!1)" metric_space_real_fun nil )"set[T]" metric_space_real_fun nil )"[T -> real]" metric_space_real_fun nil )nil abs_lems "reals/" )nil extra_real_props nil )"{y: posreal | y >= x}" nil )"nzreal" real_typesnil )nil real_props nil )nil reals nil )"nzreal" metric_space_real_fun nil )"nzreal" nil )nil reals nil ))nil )nil 3462270324 ("" (postpone) nil nil ) nil nil 3462122007"" (skosimp*)"" (expand "continuous?" )"" (skosimp*)"" (inst - "x!1" )"" (expand "continuous_at?" )"" (skosimp*)"" (inst - "epsilon!1" )"" (skosimp*)"" (inst + "delta!1" )"" (skosimp*)"" (inst - "y!1" )"" (expand "member" )"" (expand "ball" )"" (expand "real_dist" )"" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" continuity_ms_def nil )nil metric_space_real_fun nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil ) (member const-decl "bool" sets nil )"real" reals nil )"nnreal" real_metric_space nil )"(strict_total_order?[real])" real_props nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[T -> nonneg_real]" real_fun_ops "reals/" )"real" reals nil )"odd_int" integers nil )"set[T]" metric_spaces nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"bool" continuity_ms_def nil ))
Messung V0.5 in Prozent C=99 H=100 G=99
¤ Dauer der Verarbeitung: 0.33 Sekunden
(vorverarbeitet am 2026-04-30)
¤ *© Formatika GbR, Deutschland
