(rs_integral_contnil 3494863474"" (lemma "connected_domain" ) (("" (propax) nil nil )) nil )nil rs_integral_cont nil )) nil ))nil 3494863474"" (lemma "not_one_element" ) (("" (propax) nil nil )) nil )nil rs_integral_cont nil )) nil ))nil 3494864317"" (skeep)"" (skeep) (("" (hide -) (("" (grind) nil nil )) nil )) nil )) nil )"real" reals nil )"bool" metric_spaces_def nil )"bool" metric_spaces_def nil )"bool" metric_spaces_def nil )"bool" metric_spaces_def nil )"nnreal" real_metric_space nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"odd_int" integers nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rs_integral_cont nil )nil rs_integral_cont nil )set type-eq-decl nil sets nil ) (fullset const-decl "set" sets nil )"(strict_total_order?[real])" real_props nil )"real" reals nil ))nil ))nil 3494864317"" (skeep)"" (skeep)"" (hide -)"" (lemma "real_metric_space" ) (("" (inst?) nil nil )) nil ))nil ))nil ))nil )nil real_metric_space 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 )"set" sets nil ))nil ))nil 3492526014"" (skolem 1 ("a" "b" "f" "gg" ))"" (flatten)"" (assert )"" (label "altb" -1)"" (flatten)"" (label "fcont" -2)"" (label "ginc" -3)"" (name "CI" "closed_intv[T](a,b)" )"" (replace -1)"" (label "CIname" -1)"" case "NOT uniformly_continuous?[T,real_dist,real,real_dist](f,CI)" )"1" "ff" "(LAMBDA (x:real): IF T_pred(x) THEN f(x) ELSE 0 ENDIF)" )"1" "Heine[real,real_dist,real,real_dist]" )"1" "LAMBDA (x:real): a<=x AND x<=b" "ff" )"1" assert )"1" "1" "1" expand "uniformly_continuous?" )"1" "1" "epsilon!1" )"1" "1" "delta!1" )"1" "1" "x!1" "p!1" )"1" assert )"1" expand "ff" )"1" nil nil ))nil ))nil )"2" assert )"2" "p!1" )"2" expand "CI" )"2" nil nil ))nil ))nil ))nil )"3" "x!1" )"3" expand "CI" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "fcont" 1))"2" expand "continuous?" )"2" "2" "x!1" )"1" expand "continuous_at?" )"1" "1" "epsilon!1" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" assert )"1" expand "ball" )"1" case "T_pred(x!1) AND T_pred(y!1)" )"1" "1" expand "ff" )"1" assert )nil nil ))nil ))nil )"2" "2" "connected_domain" )"2" expand "connected?" )"2" "a" "b" "x!1" )"2" "a" "b" "y!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "CI" )"2" "connected_domain" )"2" expand "connected?" )"2" "a" "b" "y!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "CI" )"2" "connected_domain" )"2" expand "connected?" )"2" "a" "b" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "closed_intervals_compact" )"3" (inst - "a" "b" ) nil nil ))nil )"4" assert )"4" "4" expand "empty?" )"4" "a" )"4" expand "member" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (label "funif" -1)"2" (lemma "integrable_lem2" )"2" (inst - "a" "b" "f" "gg" )"2" assert )"2" "1" "1" "eps" )"1" expand "uniformly_continuous?" )"1" "newep" "eps/(2*(abs(gg(b)-gg(a)) + 1))" )"1" "newepname" -1)"1" "funif" "newep" )"1" "funif" "deltaf" )"1" "deltaf/2" )"1" "1" "Pwidth" "1" "RSS1" "RSS2" ))"1" "RSS1" )"1" "RSS1name" "1" "RSS2" )"1" "RSS2name" "1" expand "Riemann_sum?" )"1" "RSS2name" "xis2" )"1" "RSS1name" "xis1" )"1" replace "RSS1name" "1" replace "RSS2name" "1" expand "Rie_sum" "1" rewrite "sigma_minus" )"1" "sigma_abs[below(P`length-1)]" )"1" "1" case "sigma(0, P`length - 2, LAMBDA (n: below(P`length - 1)):") "1" assert )nil nil )"2" "2" "2" "sigma_le[below(P`length-1)]" )"2" "LAMBDA (n: below(P`length - 1)): " "LAMBDA (n: below(P`length - 1)): " "P`length-2" "0" )"2" assert )"2" case "sigma(0, P`length - 2, LAMBDA (n: below(P`length - 1)):") "1" assert )"1" "1" "nn" )"1" case "abs(f(xis1`seq(nn))-f(xis2`seq(nn)))< newep" )"1" "abs(gg(P`seq(1+nn))-gg(P`seq(nn)))" )"1" case "abs(gg(P`seq(1 + nn)) - gg(P`seq(nn))) = gg(P`seq(1 + nn)) - gg(P`seq(nn))" )"1" rewrite "abs_mult" "1" assert )nil nil ))nil )"2" "2" "ginc" )"2" expand "increasing?" "2" expand "restrict" )"2" "P`seq(nn)" "P`seq(1+nn)" )"1" assert )"1" expand "abs" "1" "1" "1" "P" )"1" expand "increasing?" )"1" "nn" "1+nn" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "P" )"2" "1+nn" )nil nil ))nil ))nil )"3" "P" )"3" "nn" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "funif" "xis1`seq(nn)" "xis2`seq(nn)" )"1" assert )"1" expand "real_dist" )"1" "funif" "Pwidth" ))"1" "xis1" )"1" "nn" )"1" "xis2" )"1" "nn" )"1" assert )"1" "1" "width_lem" )"1" "a" "b" "P" "nn" )"1" "width" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "xis2" )"2" "nn" )"2" "2" "P" )"2" "nn" )"2" "nn+1" )"2" "2" expand "CI" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "xis1" )"3" "nn" )"3" "3" "P" )"3" "nn" )"3" "nn+1" )"3" "3" expand "CI" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "FORALL (nn:below(P`length-1)): sigma(0, nn, LAMBDA (n: below(P`length - 1)):") "1" "P`length-2" )"1" assert )"1" replace "1" "P" )"1" replace "1" replace "1" case "(gg(b)-gg(a))*newep < eps" )"1" assert )nil nil )"2" "CC1" "gg(b)-gg(a)" )"2" replace "2" expand "newep" "2" "2" replace "2" assert )"2" "ginc" )"2" expand "increasing?" "2" expand "restrict" )"2" "a" "b" )"2" assert )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "nn" )"1" "1" assert )"1" expand "sigma" )"1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "nn" )"2" "2" assert )"2" "2" expand "sigma" "2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "3" assert )nil nil ))nil ))nil ))nil )"4" "4" "4" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" assert )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" expand "monotonic?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "real_metric_space" )"3" (inst?) nil nil )) nil )"4" (hide-all-but 1) (("4" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil rs_integral_cont nil )"[real -> boolean]" rs_integral_cont nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(total_order?[real])" nil )"bool" metric_spaces_def nil )"bool" metric_spaces_def nil )"bool" metric_spaces_def nil )nil real_metric_space 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 )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )nil fseqs "structures/" )nil fseqs "structures/" )"bool" sort_fseq "structures/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil rs_partition nil )"bool" rs_integral_def nil )"int" integers nil )nil integers nil )"[bool, bool -> bool]" booleans nil )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil rs_integral_def nil )nil sigma "reals/" )"posint" nil )"posreal" nil )"(total_order?[real])" nil )"nnreal" nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil sigma "reals/" )nil bounded_nat_inductions nil )nil defined_types nil )"real" reals nil )nil real_props nil )nil reals nil )nil real_props nil )"posreal" rs_integral_cont nil )nil rs_partition nil )"xis?[T](a, b, P)" rs_integral_cont nil )"xis?[T](a, b, P)" rs_integral_cont nil )nil real_props nil )"subrange(0, P`length - 2)" rs_integral_contnil )"partition[T](a, b)" rs_integral_cont nil )"[T -> real]" rs_integral_cont nil )"int" integers nil )nil abs_lems "reals/" )"bool" real_fun_preds "reals/" )"real" reals nil )nil real_props nil )nil integers nil )"nnreal" sigma_below "reals/" )"real" sigma "reals/" )nil sigma "reals/" )"real" rs_integral_def nil )"real" reals nil )"odd_int" integers nil )"bool" real_fun_preds "reals/" )nil rs_integral_prep nil )"real" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil real_types nil )"bool" reals nil )nil real_types nil )"T" rs_integral_cont nil )"[T -> bool]" rs_integral_cont nil )"(CI)" rs_integral_cont nil )"T" rs_integral_cont nil )"(CI)" rs_integral_cont nil )"[real -> real]" rs_integral_cont nil )"bool" continuity_ms_def nil )"(LAMBDA (x: real): a <= x AND x <= b)" nil )"bool" sets nil )nil rs_integral_cont nil )"bool" deriv_domain_def nil )"set[T]" metric_spaces nil )"(LAMBDA (x: real): a <= x AND x <= b)" nil )"bool" continuity_ms_def nil )"bool" reals nil )nil real_metric_space nil )"bool" sets nil )nil uniform_continuity nil )"bool" metric_spaces_def nil )"set" sets nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil ) (>= const-decl "bool" reals nil )nil real_types nil )"R" restrict nil )"nnreal" real_metric_space nil )"bool" uniform_continuity nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3492526083"" (skolem 1 ("a" "b" "f" "gg" ))"" (assert )"" (flatten)"" (lemma "BV_decomposition" )"" (inst - "a" "b" "gg" )"" (assert )"" (skolem -1 ("vv" "ww" ))"" (flatten)"" (lemma "RS_integrable_cont_inc" )"" (inst-cp - "a" "b" "f" "vv" )"" (inst - "a" "b" "f" "ww" )"" (assert )"" (replace -3)"" (lemma "integral_diff_g" )"" "a" "b" "f" "vv" "ww" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )nil rs_integral_cont nil )"[real -> boolean]" rs_integral_cont nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil bounded_variation nil )"real" reals nil )nil rs_integral_prep nil )nil rs_integral_cont nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.43 Sekunden
(vorverarbeitet am 2026-04-28)
¤ *© Formatika GbR, Deutschland
