Quellcode-Bibliothek piecewise_continuous.prf
Sprache: Lisp
(piecewise_continuousnil 3612529043"" (lemma "connected_domain" ) (("" (propax) nil nil )) nil )nil piecewise_continuous nil )) nil ))nil 3612529043"" (lemma "not_one_element" ) (("" (propax) nil nil )) nil )nil piecewise_continuous nil )) nil ))nil 3611578171"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil ))nil ))nil 3611578171"" (skosimp*) (("" (assert ) nil nil )) nil )"posint" nil )"(total_order?[real])" nil ))nil ))nil 3611578171"" (subtype-tcc) nil nil )"bool" real_fun_preds "reals/" )"bool" continuous_functions nil ) nil "real" reals nil ))nil ))nil 3611578171"" (skeep) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil ))nil ))nil 3611591182 ("" (grind) nil nil )"bool" real_fun_preds "reals/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"bool" continuous_functions nil ) nil "real" reals nil ))nil ))nil 3611591182 ("" (grind) nil nil )"bool" real_fun_preds "reals/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"bool" continuous_functions nil ) nil "real" reals nil ))nil ))nil 3611681282"" (skosimp*)"" (lemma "unif_cont_interval[closed_interval(a!1,b!1)]" )"1" (inst?)"1" (inst -1 "f!1" )"1" (assert )"1" (expand "restrict" )"1" case " continuous_on?(LAMBDA (s: closed_interval[T](a!1, b!1)): f!1(s), ") "1" (assert )"1" (hide -1)"1" (rewrite "step_to_integrable" )"1" (skosimp*)"1" (expand "uniformly_continuous?" )"1" (inst -1 "(eps!1/2)/(b!1-a!1)" )"1" (skosimp*)"1" "PP" "eq_partition(a!1,b!1,floor((b!1-a!1)/delta!1)+2)" )"1" case "step_function?(a!1, b!1, fmin(a!1, b!1, PP, f!1))" )"1" case "step_function?(a!1, b!1, fmax(a!1, b!1, PP, f!1))" )"1" "fmin(a!1,b!1,PP,f!1)" "fmax(a!1,b!1,PP,f!1)" )"1" assert )"1" case "integrable?(a!1, b!1, fmax(a!1, b!1, PP, f!1) - fmin(a!1, b!1, PP, f!1))" )"1" assert )"1" case " integral(a!1, b!1, fmax(a!1, b!1, PP, f!1) - fmin(a!1, b!1, PP, f!1)) < eps!1" )"1" assert )"1" "1" "1" "1" "fmin(a!1, b!1, PP, f!1)" )"1" "part_induction" )"1" "(LAMBDA x: fmin(a!1, b!1, PP, f!1)(x) <= f!1(x))" "a!1" "b!1" "PP" "xx!1" )"1" assert )"1" assert )"1" "1" assert )"1" "ii!1" )"1" "xx!1" )"1" "1" "1" assert )nil nil )"2" "2" assert )"2" replace "2" "2" assert )"2" "min_x(seq(PP)(ii!1), seq(PP)(1 + ii!1), f!1)" )"2" "2" "xx!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "fmax(a!1, b!1, PP, f!1)" )"2" "part_induction" )"2" "(LAMBDA x: fmax(a!1, b!1, PP, f!1)(x) >= f!1(x))" "a!1" "b!1" "PP" "xx!1" )"2" assert )"2" assert )"2" "2" "ii!1" )"2" "xx!1" )"2" "2" "1" assert )nil nil )"2" assert )"2" "2" assert )"2" replace "2" "2" "max_x(seq(PP)(ii!1), seq(PP)(1 + ii!1), f!1)" )"2" "2" "xx!1" )"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 )"2" "2" "width_eq_part" )"2" "2" assert )"2" replace -5)"2" case "width(a!1,b!1,PP) < delta!1" )"1" "1" "integral_bound_abs" )"1" "eps!1/(2*(b!1-a!1))" "a!1" "b!1" "fmax(a!1, b!1, PP, f!1) - fmin(a!1, b!1, PP, f!1)" )"1" "BMA" "b!1-a!1" )"1" assert )"1" "1" "III" "integral(a!1, b!1, fmax(a!1, b!1, PP, f!1) - fmin(a!1, b!1, PP, f!1))" )"1" case "III >= 0" )"1" replace "1" expand "abs" "1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "2" "2" expand "-" )"2" "part_induction" )"2" "(LAMBDA x: (fmax(a!1, b!1, PP, f!1) - fmin(a!1, b!1, PP, f!1))(x) <= eps!1 / (2 * BMA))" "a!1" "b!1" "PP" "x!1" )"2" assert )"2" expand "-" )"2" case "fmax(a!1, b!1, PP, f!1)(x!1) - fmin(a!1, b!1, PP, f!1)(x!1) >= 0" )"1" expand "abs" "1" assert )"1" assert )"1" "1" "fmax(a!1, b!1, PP, f!1)" )"1" "fmin(a!1, b!1, PP, f!1)" )"1" "ii!1" )"1" "ii!1" )"1" "x!1" )"1" "x!1" )"1" "1" case "(seq(PP)(ii!1) = x!1 OR x!1 = seq(PP)(1 + ii!1))" )"1" assert )"1" "1" assert )"1" "1" replace "1" replace "1" assert )"1" "1" "1" "(2*BMA)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" replace "2" replace "2" assert )"2" "2" "2" "(2*BMA)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" replace "2" "2" replace "2" "2" "MIN_x" "min_x(seq(PP)(ii!1), seq(PP)(1 + ii!1), f!1)" )"2" replace "2" "MAX_x" "max_x(seq(PP)(ii!1), seq(PP)(1 + ii!1), f!1)" )"2" replace "2" case "(FORALL (x,y: closed_interval(seq(PP)(ii!1),seq(PP)(ii!1+1))): abs(x-y) <= seq(PP)(1 + ii!1) - seq(PP)(ii!1))" )"1" case "abs(MAX_x - MIN_x) <= seq(PP)(1+ii!1) - seq(PP)(ii!1)" )"1" "MAX_x" "MIN_x" )"1" assert )"1" "width_lem" )"1" expand "finseq_appl" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil )"2" assert )"2" "2" "MAX_x" )"2" "MIN_x" )"2" "2" expand "abs" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "2" "x" )"2" "y" )"2" expand "abs" )"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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "fmax_ge" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" "2" "BMA" "b!1-a!1" )"2" "(1 + floor(BMA / delta!1))" )"1" "delta!1" )"1" assert )nil nil ))nil )"2" "2" "2" assert )"2" "BMA / delta!1 >= 0" )"1" assert )nil nil )"2" "2" "delta!1" )"2" assert )"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 )"2" "2" "integral_diff" )"2" "a!1" "b!1" "fmax(a!1, b!1, PP, f!1)" "fmin(a!1, b!1, PP, f!1)" )"2" assert )"2" "1" "1" assert )"1" expand "-" )"1" nil nil ))nil ))nil ))nil )"2" "2" rewrite "step_function_integrable?" )nil nil ))nil )"3" "3" rewrite "step_function_integrable?" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "fmax_step" )nil nil ))nil ))nil )"2" "2" rewrite "fmin_step" )nil nil ))nil )"3" "3" "3" "3" expand "continuous_on?" )"3" expand "continuous?" )"3" "x!1" )"3" "3" "epsilon" )"3" "3" "delta" )"3" "3" "x" )"3" expand "restrict" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "delta!1" )"2" assert )"2" case "floor((b!1 - a!1) / delta!1)>=0" )"1" "delta!1" )"1" (assert ) nil nil ))nil )"2" assert )"2" "1/delta!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "1" "b!1-a!1" )"1" (assert ) nil nil ))nil )"2" "b!1-a!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" (expand "continuous_on?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil )"2" (expand "not_one_element?" )"2" (skosimp*)"2" (typepred "x!1" )"2" (inst-cp 1 "a!1" )"2" (inst-cp 1 "b!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (lemma "connected_domain" )"3" (expand "connected?" )"3" (assert )"3" (skosimp*)"3" (lemma "connected_domain" )"3" (expand "connected?" )"3" (inst -1 "a!1" "b!1" "z!1" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil intervals_real "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil piecewise_continuous nil )"[real -> boolean]" piecewise_continuous nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil unif_cont_fun nil )"bool" deriv_domain_def nil )"bool" deriv_domain_def nil )"R" restrict nil )nil integral_step nil )"real" reals nil )"bool" unif_cont_fun nil )"real" reals nil )nil real_props nil )"posreal" nil )nil extra_real_propsnil )"bool" step_fun_def nil )"bool" continuous_functions nil )nil integral_cont_scaf nil )"[bool, bool -> bool]" booleans nil )nil interval_minmax nil )"{mx: T | AND AND AND x <= b IMPLIES f(mx) <= f(x))}" nil )OR const-decl "[bool, bool -> bool]" booleans nil )"{ff: [T -> real] | LET xx = seq(P) INAND x < xx(ii + 1) IMPLIESAND ((xx(ii) = x OR x = xx(ii + 1)) IMPLIES ff(x) = f(x))}" nil )nil integral_cont_scaf nil )"bool" integral_def nil )"[T -> real]" real_fun_ops "reals/" )"bool" integral_def nil )"{S: real | integral?(a, b, ff, S)}" nil )nil integral_def nil )"posint" nil )NOT const-decl "[bool -> bool]" booleans nil )nil integral_def nil )"posreal" integral_def nil )nil integral_prep nil )"odd_int" integers nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil real_props nil )"real" piecewise_continuous nil )nil real_props nil )nil reals nil )"[numfield -> numfield]" number_fields nil )"real" reals nil )"{fs: finite_sequence[{x | a!1 <= x AND x <= b!1}] | AND AND AND " piecewise_continuous nil )"below(length(PP) - 1)" nil )"[T -> real]" piecewise_continuous nil )"{mx: T | AND AND AND x <= seq(PP)(1 + ii!1) IMPLIES" piecewise_continuous nil) "{mx: T | AND AND AND x <= seq(PP)(1 + ii!1) IMPLIES" piecewise_continuous nil) nil integral_def nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil integral_cont_scaf nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"nnreal" nil )nil real_props nil )nil real_props nil )nil extra_real_props nil )"real" piecewise_continuous nil )"posreal" piecewise_continuous nil )nil extra_real_propsnil )"int" integers nil )nil integral_prep nil )nil integral_step nil )"{ff: [T -> real] | LET xx = seq(P) INAND x < xx(ii + 1) IMPLIESAND ((xx(ii) = x OR x = xx(ii + 1)) IMPLIES ff(x) = f(x))}" nil )"{mx: T | AND AND AND x <= b IMPLIES f(mx) >= f(x))}" nil )nil integral_cont_scaf nil )"{i | i <= x & x < i + 1}" floor_ceil nil )nil integers nil )"partition(a, b)" integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )nil naturalnumbers nil )"real" reals nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" piecewise_continuous nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )"nzreal" nil )"(total_order?[real])" nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"bool" booleans nil )"bool" continuous_functions nil )nil defined_types nil )"(strict_total_order?[real])" real_props nil )"T" piecewise_continuous nil )"T" piecewise_continuous nil )"(total_order?[real])" nil )nil piecewise_continuous nil ))nil ))nil 3612528404"" (skeep)"" (expand "Integrable?" )"" (assert )"" (lemma "integrable_split[T]" )"" (expand "piecewise_continuous?" )"" (skeep)"" (expand "piecewise_continuous?" )"" (flatten)"" case "FORALL (i:nat): i+1<=N IMPLIES integrable?(P(0),P(i+1),f)" )"1" (inst - "N-1" ) (("1" (assert ) nil nil )) nil )"2" case "FORALL (i:nat): i+1<=N IMPLIES integrable?(P(i),P(i+1),f)" )"1" (induct "i" )"1" (assert )"1" (inst - "0" ) (("1" (assert ) nil nil ))nil ))nil )"2" (skeep)"2" (assert )"2" (inst - "1+j" )"2" assert )"2" "P(0)" "P(1+j)" "P(2+j)" "f" )"2" assert )"2" expand "piecewise_continuous?" )"2" "2" expand "strict_increasing?" )"2" "0" "1+j" )"2" "1+j" "2+j" )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skeep)"3" (expand "piecewise_continuous?" )"3" (flatten)"3" expand "strict_increasing?" )"3" "0" "1+i" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "piecewise_continuous?" )"2" (flatten)"2" (hide 2)"2" (hide 2)"2" "continuous_on_integrable" )"2" "2" "i" )"1" assert )"1" "H(i)" )"1" assert )"1" "P(i)" "P(i+1)" )"1" assert )"1" expand "strict_increasing?" )"1" "1" assert )"1" assert )"1" "integral_chg_one_pt" )"1" "f1" "H(i) WITH [(P(i)):=f(P(i))]" )"1" "f2" "f1 WITH [(P(i+1)):=f(P(i+1))]" )"1" "P(i)" "P(i+1)" "H(i)" "f(P(i))" )"1" assert )"1" "P(i)" )"1" assert )"1" "1" "1" replace "1" "integral_chg_one_pt" )"1" "P(i)" "P(i+1)" "f1" "f(P(i+1))" )"1" assert )"1" "P(i+1)" )"1" assert )"1" "1" "1" replace "1" "integral_restrict_eq" )"1" "P(i)" "P(i+1)" "f2" "f" )"1" assert )"1" "1" expand "f2" "1" expand "f1" "1" "1" assert )"1" "1" "i" )"1" "x" )"1" 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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert )"3" (skeep)"3" (expand "piecewise_continuous?" )"3" (expand "strict_increasing?" )"3" "3" "i" "i+1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (skeep) (("4" (assert ) nil nil )) nil ))nil )"3" (assert )"3" (expand "piecewise_continuous?" )"3" (expand "strict_increasing?" )"3" (flatten)"3" (skeep)"3" "0" "i+1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" integral_def nil )nil piecewise_continuous nil )"[real -> boolean]" piecewise_continuous nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil integral_split nil )"nat" piecewise_continuous nil )"bool" piecewise_continuous nil )"bool" real_fun_preds "reals/" )"odd_int" integers nil )"odd_int" integers nil )"posint" nil )nil naturalnumbers nil )nil defined_types nil )"[upto(N) -> T]" piecewise_continuous nil )"posnat" piecewise_continuous nil )"[T, T -> boolean]" equalities nil )"[T -> real]" piecewise_continuous nil )"[T -> real]" piecewise_continuous nil )nil integral_def nil )nil integral_prep nil )nil naturalnumbers nil )"nat" piecewise_continuous nil )nil piecewise_continuousnil )"nat" piecewise_continuous nil )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"int" integers nil )"posint" nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )"bool" integral_def nil )nil naturalnumbers nil )"bool" piecewise_continuous nil )"bool" piecewise_continuous nil )"(strict_total_order?[real])" real_props nil ))nil )nil 3611589970"" (skeep)"" (lemma "integrable_split[T]" )"" (expand "piecewise_continuous?" )"" (skeep)"" (expand "piecewise_continuous?" )"" (flatten)"" case "FORALL (i:nat): i+1<=N IMPLIES integrable?(P(0),P(i+1),f)" )"1" (inst - "N-1" ) (("1" (assert ) nil nil )) nil )"2" case "FORALL (i:nat): i+1<=N IMPLIES integrable?(P(i),P(i+1),f)" )"1" (induct "i" )"1" (assert )"1" (inst - "0" ) (("1" (assert ) nil nil )) nil ))nil )"2" (skeep)"2" (assert )"2" (inst - "1+j" )"2" (assert )"2" (inst - "P(0)" "P(1+j)" "P(2+j)" "f" )"2" assert )"2" expand "piecewise_continuous?" )"2" "2" expand "strict_increasing?" )"2" "0" "1+j" )"2" "1+j" "2+j" )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skeep)"3" (expand "piecewise_continuous?" )"3" (flatten)"3" (expand "strict_increasing?" )"3" (inst - "0" "1+i" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "piecewise_continuous?" )"2" (flatten)"2" (hide 2)"2" (hide 2)"2" (lemma "continuous_on_integrable" )"2" (skeep)"2" "i" )"1" assert )"1" "H(i)" )"1" assert )"1" "P(i)" "P(i+1)" )"1" assert )"1" expand "strict_increasing?" )"1" "1" assert )"1" assert )"1" "integral_chg_one_pt" )"1" "f1" "H(i) WITH [(P(i)):=f(P(i))]" )"1" "f2" "f1 WITH [(P(i+1)):=f(P(i+1))]" )"1" "P(i)" "P(i+1)" "H(i)" "f(P(i))" )"1" assert )"1" "P(i)" )"1" assert )"1" "1" "1" replace "1" "integral_chg_one_pt" )"1" "P(i)" "P(i+1)" "f1" "f(P(i+1))" )"1" assert )"1" "P(i+1)" )"1" assert )"1" "1" "1" replace "1" "integral_restrict_eq" )"1" "P(i)" "P(i+1)" "f2" "f" )"1" assert )"1" "1" expand "f2" "1" expand "f1" "1" "1" assert )"1" "1" "i" )"1" "x" )"1" 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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert )"3" (skeep)"3" (expand "piecewise_continuous?" )"3" (expand "strict_increasing?" )"3" (flatten)"3" (inst - "i" "i+1" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"4" (skeep) (("4" (assert ) nil nil )) nil ))nil )"3" (assert )"3" (expand "piecewise_continuous?" )"3" (expand "strict_increasing?" )"3" (flatten)"3" (skeep)"3" (inst - "0" "i+1" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil piecewise_continuous nil )"[real -> boolean]" piecewise_continuous nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil integral_split nil )"bool" real_fun_preds "reals/" )"odd_int" integers nil )"odd_int" integers nil )"posint" nil )nil naturalnumbers nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )nil integral_def nil )nil integral_prep nil )nil naturalnumbers nil )nil piecewise_continuousnil )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"posint" nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )"bool" integral_def nil )nil naturalnumbers nil ))nil 3612186214"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3612186214"" (skosimp*) (("" (assert ) nil nil )) nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil ))nil 3612186214"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"posint" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3612186214"" (skosimp*) (("" (assert ) nil nil )) nil )"int" integers nil )"(total_order?[real])" nil )"posint" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3612186214"" (skosimp*) (("" (assert ) nil nil )) nil )"posint" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3612186214"" (skosimp*) (("" (assert ) nil nil )) nil )"posint" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3612186214"" (skosimp*)"" (lemma "continuous_on_integrable" )"" (expand "Integrable?" )"" (assert )"" (flatten)"" (hide (1 3))"" (assert )"" (hide -2)"" (expand "piecewise_continuous?" )"" (flatten)"" (expand "piecewise_continuous?" )"" (flatten)"" (expand "strict_increasing?" )"" (inst - "k!1" "k!1+1" )"" assert )"" "" assert )"" (inst - "k!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil piecewise_continuousnil )"posint" nil )"posint" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil naturalnumbers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"bool" reals nil )nil piecewise_continuous nil )"[real -> boolean]" piecewise_continuous nil )"bool" real_fun_preds "reals/" ) nil nil (Integrable? const-decl "bool" integral_def nil ))nil ))nil 3612186214"" (skeep) (("" (skeep) (("" (assert ) nil nil )) nil )) nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil )"(total_order?[real])" nil ))nil ))nil 3612187243"" (skosimp*)"" (lemma "continuous_on_integrable" )"" (expand "Integrable?" )"" (assert )"" (flatten)"" (assert )"" (inst - "P!1(i!1)" "x!1" "H!1(i!1)" )"" (assert )"" (expand "piecewise_continuous?" )"" (flatten)"" (expand "piecewise_continuous?" )"" (flatten)"" (assert )"" (inst - "i!1" )"" assert )"" expand "continuous_on?" )"" "" "x0" )"" "" "epsilon" )"" "" "delta" )"" "" "x_1" )"" 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 )nil piecewise_continuousnil )"posint" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"real" reals nil )"bool" continuous_functions nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )nil real_types nil )"(total_order?[real])" nil )nil nil (below type-eq-decl nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil piecewise_continuous nil )"[real -> boolean]" piecewise_continuous nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" integral_def nil ))nil )nil 3612186214"" (subtype-tcc) nil nil ) nil nil ))nil 3612273788"" (skeep)"" (label "px" (-4 -5))"" (copy -3)"" (label "pc1" -4)"" (expand "piecewise_continuous?" -1)"" (flatten)"" (label "p0a" -2)"" (label "PNb" -3)"" (label "Heq" -4)"" (copy -1)"" (expand "piecewise_continuous?" -1)"" (label "pc2" -2)"" (flatten)"" (label "si" -1)"" "" "cisaved" -1)"" "cisaved" )"" "ci" -2)"" "" expand "strict_increasing?" "" "0" "i" )"" "i" "i+1" )"" "i+1" "N" )"" "ci2" -1)"" "pii" -3)"" assert )"" case "NOT (a<=P(i) AND P(i+1)<=b)" )"1" nil nil )"2" "2" "pabz" "2" assert )"2" "ranges" "2" "ranges" )"2" "Integrable?_inside" )"2" "ii4" "2" "a" "b" "f" "a" "x" )"2" assert )"2" "piecewise_continuous_integrable" )"2" "a" "b" "f" )"2" assert )"2" case "NOT piecewise_continuous?(f, a, b)" )"1" assert )"1" expand "piecewise_continuous?" "1" "N" "P" "H" )nil nil ))nil ))nil )"2" assert )"2" "a" "x" "f" "2" assert )"2" "intss" "2" "Integral_split" )"2" "a" "P(i)" "x" "f" )"2" assert )"2" "a" "P(i)" )"2" "P(i)" "x" )"2" assert )"2" assert )"2" "integral_restrict_eq" )"2" "P(i)" "x" "f" "H(i)" )"2" assert )"2" case "NOT Integral(a, P(i), f) = sigma(0, i - 1, LAMBDA (k: nat):IF k < N THEN Integral(P(k), P(1 + k), H(k)) ELSE 0 ENDIF)") "1" "1" "1" case "FORALL (kv:nat): kv<N IMPLIES Integral(a, P(kv), f) = LAMBDA (k: nat):IF k < N THEN Integral(P(k), P(1 + k), H(k)) ELSE 0 ENDIF)") "1" "i" )"1" assert )nil nil ))nil )"2" "2" "kv" )"1" assert )"1" "Integral_a_to_a" )"1" "1" expand "sigma" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "Integral_split" )"2" "a" "P(j)" "P(j+1)" "f" )"2" assert )"2" "1" "1" "1" assert )"1" expand "sigma" "1" assert )"1" replace "1" "integral_restr_eq" )"1" "P(j)" "P(1+j)" "f" "H(j)" )"1" assert )"1" "1" "1" expand "Integral" "1" assert )"1" "ci2" )"1" "j" "1+j" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "ci2" )"2" "j" "1+j" )"2" assert )nil nil ))nil ))nil )"3" "Heq" )"3" "j" )nil nil ))nil )"4" "ii4" "a" "b" "f" "P(j)" "P(1+j)" )"4" assert )"4" "ci2" )"4" "0" "j" )"4" "j" "1+j" )"4" "1+j" "N" )"4" "1" expand "Integrable?" "1" nil nil ))nil )"2" expand "Integrable?" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Integrable?" "2" "2" "ci2" )"2" "0" "j" )"2" assert )"2" "ii4" "a" "b" "f" "a" "P(j)" )"2" assert )"2" "ii4" )"1" expand "Integrable?" "1" nil nil ))nil )"2" "j" "N" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "ii4" "a" "b" "f" "P(j)" "P(1+j)" )"3" assert )"3" expand "Integrable?" "3" "ci2" )"3" "j" "1+j" )"3" assert )"3" expand "Integrable?" "ii4" )"3" "ci2" )"3" "0" "j" )"3" "1+j" "N" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" "4" "4" "continuous_on_integrable" )"4" "P(k)" "P(1+k)" "H(k)" )"4" assert )"4" expand "Integrable?" "4" "4" assert )"4" "cisaved" )"4" "k" )"4" assert )"4" "ci2" )"4" "k" "1+k" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" "5" assert )nil nil ))nil )"6" "6" assert )nil nil ))nil )"7" "7" "10" )"7" assert )nil nil ))nil ))nil )"8" "8" assert )"8" "ii4" "a" "b" "f" "a" "P(kv)" )"8" assert )"8" "ci2" )"8" "0" "kv" )"8" "kv" "N" )"8" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"9" "9" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" "4" "ii4" "a" "b" "f" "P(k!1)" "P(1+k!1)" )"4" assert )"4" "ii4" )"1" "integral_restr_eq" )"1" "P(k!1)" "P(1+k!1)" "f" "H(k!1)" )"1" assert )"1" "1" "1" expand "Integrable?" "1" "1" assert )"1" "ci2" )"1" "k!1" "1+k!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ci2" )"2" "k!1" "1+k!1" )"2" assert )nil nil ))nil ))nil )"3" "Heq" )"3" "3" "k!1" )"3" "x!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil )"4" expand "Integrable?" "4" assert )"4" "ci2" )"4" "k!1" "1+k!1" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ci2" )"2" "0" "k!1" )"2" assert )nil nil ))nil ))nil )"3" "ci2" )"3" "k!1" "1+k!1" )"3" assert )nil nil ))nil ))nil )"4" "ci2" )"4" "1+k!1" "N" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" "5" assert )nil nil ))nil )"6" "6" assert )nil nil ))nil )"7" "7" assert )nil nil ))nil )"8" "8" "8" "ii4" "a" "b" "f" "a" "P(kv)" )"8" assert )"8" "ci2" )"8" "0" "kv" )"8" "kv" "N" )"8" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" "integral_restr_eq" )"2" "P(i)" "x" "f" "H(i)" )"2" "1" "1" assert )"1" expand "Integral" "1" assert )"1" "1" "1" "1" "1" "1" "1" assert )"1" "1" assert )"1" "1" replace "1" "integral_split" )"1" "a" "P(i)" "x" "f" )"1" assert )"1" expand "Integrable?" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOT x = P(i)" )"1" assert )nil nil )"2" replace "2" assert )"2" rewrite "Integral_a_to_a" nil nil ))nil ))nil ))nil )"3" "Heq" )"3" "3" "i" )"3" "x!1" )"3" nil nil ))nil ))nil ))nil ))nil )"4" "4" expand "Integrable?" "4" assert )"4" "4" assert )"4" rewrite "Integral_a_to_a" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" "ci2" )"4" "k" "1+k" )"4" assert )"4" expand "Integrable?" "4" assert )"4" "continuous_on_integrable" )"4" "4" assert )"4" "ci" "k" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" "5" assert )nil nil ))nil )"6" "6" 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 ))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 )"bool" real_fun_preds "reals/" )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" piecewise_continuous nil )"bool" reals nil )nil naturalnumbers nil )nil integral_def nil )nil integral_split nil )"posnat" piecewise_continuous nil )"T" piecewise_continuous nil )"[upto(N) -> T]" piecewise_continuous nil )"[T -> real]" piecewise_continuous nil )"[below(N) -> [T -> real]]" nil )nil defined_types nil )nil naturalnumbers nil )"nat" piecewise_continuous nil )"nat" piecewise_continuous nil )"nat" piecewise_continuous nil )"nat" piecewise_continuous nil )"nat" piecewise_continuous nil )"nat" piecewise_continuous nil )"nat" piecewise_continuous nil )nil integral nil )nil integral_prep nil )"(total_order?[real])" nil )nil piecewise_continuousnil )nil integers nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"real" integral_def nil )nil integral_def nil )"bool" integral_def nil )"[T, T -> boolean]" equalities nil )nil integral nil )nil nil )nil integral nil )"posint" nil )"real" reals nil )"int" integers nil )"[bool, bool -> bool]" booleans nil )nil piecewise_continuous nil )"[real -> boolean]" piecewise_continuous nil )AND const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" piecewise_continuous nil )"bool" piecewise_continuous nil ))nil )nil 3612260269"" (skeep)"" (label "px" (-4 -5))"" (copy -3)"" (label "pc1" -4)"" (expand "piecewise_continuous?" -1)"" (flatten)"" (label "p0a" -2)"" (label "PNb" -3)"" (label "Heq" -4)"" (copy -1)"" (expand "piecewise_continuous?" -1)"" (label "pc2" -2)"" (flatten)"" (label "si" -1)"" "ci" -2)"" "" expand "strict_increasing?" -1)"" "0" "i" )"" "i" "i+1" )"" "i+1" "N" )"" "ci2" -1)"" "pii" -3)"" assert )"" case "NOT (a<=P(i) AND P(i+1)<=b)" )"1" nil nil )"2" "2" "pabz" "2" assert )"2" "ranges" "2" "ranges" )"2" "Integrable?_inside" )"2" "ii4" "2" "a" "b" "f" "a" "x" )"2" assert )"2" "piecewise_continuous_integrable" )"2" "a" "b" "f" )"2" assert )"2" case "NOT piecewise_continuous?(f, a, b)" )"1" assert )"1" expand "piecewise_continuous?" "1" "N" "P" "H" )nil nil ))nil ))nil )"2" assert )"2" "a" "x" "f" "2" assert )"2" "intss" "2" expand "Integrable?" "2" assert )"2" assert )"2" "Integral_split" )"2" "a" "P(i)" "x" "f" )"2" assert )"2" "a" "P(i)" )"2" "P(i)" "x" )"2" assert )"2" assert )"2" "integral_restrict_eq" )"2" "P(i)" "x" "f" "H(i)" )"2" assert )"2" case "NOT Integral(a, P(i), f) = sigma(0, i - 1, LAMBDA (k: nat):IF k < N THEN Integral(P(k), P(1 + k), H(k)) ELSE 0 ENDIF)") "1" "1" "1" case "FORALL (kv:nat): kv<N IMPLIES Integral(a, P(kv), f) = LAMBDA (k: nat):IF k < N THEN Integral(P(k), P(1 + k), H(k)) ELSE 0 ENDIF)") "1" "i" )"1" assert )nil nil ))nil )"2" "2" "kv" )"1" assert )"1" "Integral_a_to_a" )"1" "1" expand "sigma" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "Integral_split" )"2" "a" "P(j)" "P(j+1)" "f" )"2" assert )"2" "1" "1" "1" assert )"1" expand "sigma" "1" assert )"1" replace "1" "integral_restr_eq" )"1" "P(j)" "P(1+j)" "f" "H(j)" )"1" assert )"1" "1" "1" expand "Integral" "1" assert )"1" "ci2" )"1" "j" "1+j" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "ci2" )"2" "j" "1+j" )"2" assert )nil nil ))nil ))nil )"3" "Heq" )"3" "j" )nil nil ))nil )"4" "ii4" "a" "b" "f" "P(j)" "P(1+j)" )"4" assert )"4" "ci2" )"4" "0" "j" )"4" "j" "1+j" )"4" "1+j" "N" )"4" "1" expand "Integrable?" "1" nil nil ))nil )"2" expand "Integrable?" "2" nil nil ))nil )"3" expand "Integrable?" "3" nil nil ))nil )"4" expand "Integrable?" "4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Integrable?" "2" "2" "ci2" )"2" "0" "j" )"2" assert )"2" "ii4" "a" "b" "f" "a" "P(j)" )"2" assert )"2" "ii4" )"1" expand "Integrable?" "1" nil nil ))nil )"2" "j" "N" )"2" assert )nil nil ))nil )"3" expand "Integrable?" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "ii4" "a" "b" "f" "P(j)" "P(1+j)" )"3" assert )"3" expand "Integrable?" "3" "ci2" )"3" "j" "1+j" )"3" assert )"3" expand "Integrable?" "ii4" )"3" "ci2" )"3" "0" "j" )"3" "1+j" "N" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" "4" "4" "continuous_on_integrable" )"4" "P(k)" "P(1+k)" "H(k)" )"4" assert )"4" expand "Integrable?" "4" "4" assert )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" nil nil )"6" nil nil )"7" nil nil )"8" nil nil )"9" nil nil ))nil ))nil )"3" nil nil )"4" nil nil )"5" nil nil )"6" nil nil )"7" nil nil )"8" nil nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil )"4" nil nil )"5" nil nil )"6" 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 ))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 shostak)))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.366 Sekunden
(vorverarbeitet am 2026-04-27)
¤ *© Formatika GbR, Deutschland
2026-05-26
