Quelle integral_pulse.prf
Sprache: Lisp
(integral_pulsenil 3260699953"" (skosimp*)"" (lemma "connected_domain" )"" (inst -1 "x!1" "y!1" "z!1" ) (("" (assert ) nil nil )) nil ))nil ))nil )nil integral_pulse nil )) nil ))nil 3260699953"" (lemma "not_one_element" ) (("" (propax) nil nil )) nil )nil integral_pulse nil )) nil ))nil 3262360238"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3262360239 ("" (subtype-tcc) nil 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]" integral_pulse nil )nil integral_pulse nil )nil integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )nil intervals_real "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil ))nil 3262360239 ("" (subtype-tcc) nil nil ) nil shostak))nil 3262360239 ("" (assuming-tcc) nil 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]" integral_pulse nil )nil integral_pulse nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )nil integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )nil intervals_real "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil ))nil 3262360240 ("" (subtype-tcc) nil 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]" integral_pulse nil )nil integral_pulse nil )nil naturalnumbers nil )nil integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )nil integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )nil intervals_real "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil ))nil 3262360240 ("" (subtype-tcc) nil 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]" integral_pulse nil )nil integral_pulse nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )nil intervals_real "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil ))nil 3352532343 ("" (subtype-tcc) nil 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]" integral_pulse nil )nil integral_pulse nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )nil intervals_real "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil ))nil ))nil 3262360246"" (skosimp*)"" case "FORALL (P: partition(a!1,b!1),p,q:nat): AND p+q <= length(P) - 1 IMPLIESLAMBDA (n: upto(length(P) - 1)):IF n = 0 THEN 0 ELSE seq(P)(n) - seq(P)(n - 1) ENDIF)) =") "1" (inst -1 "P!1" "p!1" "q!1-p!1" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil )"2" (hide 2)"2" (induct "q" )"1" (skosimp*)"1" (expand "sigma" )"1" (ground)"1" (expand "sigma" ) (("1" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst - "P!2" "p!2" )"2" (assert )"2" (expand "sigma" 1)"2" (replace -1) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp*) (("3" (assert ) nil nil )) nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil )"5" (skosimp*) (("5" (assert ) nil nil )) nil )"6" (skosimp*) (("6" (assert ) nil nil )) nil )"7" (skosimp*) nil nil )"8" (skosimp*) (("8" (assert ) nil nil )) nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil )"5" (skosimp*) (("5" (assert ) nil nil )) nil )"6" (skosimp*) (("6" (assert ) nil nil )) nil )"7" (skosimp*) nil nil )"8" (hide 2)"8" (skosimp*)"8" (inst + "0" ) (("8" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )nil naturalnumbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )nil finite_sequences nil )nil intervals_real "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integral_pulse nil )"[real -> boolean]" integral_pulse nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nat_types nil )nil naturalnumbers nil )"real" reals nil )"int" integers nil )"nonneg_int" nil )NOT const-decl "[bool -> bool]" booleans nil )nil integers nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nat" integral_pulse nil )"nat" integral_pulse nil )"(total_order?[real])" nil )"T" integral_pulse nil )"T" integral_pulse nil )nil defined_types nil )nil naturalnumbers nil )"real" reals nil )"real" reals nil )"odd_int" integers nil )"posint" nil )"posint" nil ))nil 3262447218"" (skosimp*) (("" (assert ) nil nil )) nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3280253181"" (skosimp*)"" (expand "Rie_sec" )"" (typepred "P!1" )"" (assert )"" (inst - "ii!1-1" )"" (name "FF" "f!1(xis!1(ii!1 - 1))" )"" (replace -1)"" (lemma "width_lem" )"" (expand "finseq_appl" )"" (inst -1 "a!1" "b!1" "P!1" "ii!1-1" )"" (assert )"" (case " FF >= 0 AND FF <= 1" )"1" (flatten)"1" (assert )"1" "1" assert )"1" expand "abs" )"1" "1" assert )"1" "FF = 0" )"1" (assert ) nil nil )"2" "FF" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst - "xis!1(ii!1-1)" )"2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )"real" integral_def nil )"(total_order?[real])" nil )"{j: nonneg_int | j >= i}" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"bool" integral_def nil )nil integral_def nil )"(total_order?[real])" nil )"[bool, bool -> bool]" booleans nil )"real" integral_pulse nil )nil real_props nil )nil extra_real_props nil )nil abs_lems "reals/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"posreal" nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )"posreal" integral_def nil )"int" integers nil )"[below[length(fs)] -> T]" finite_sequencesnil )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 )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )"[real -> boolean]" integral_pulse nil )nil integral_pulse nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil intervals_real "reals/" )nil finite_sequences nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil integral_def nil ))nil )nil 3262529290"" (skosimp*)"" (expand "Rie_sec" )"" (typepred "P!1" )"" (assert )"" (inst - "ii!1-1" )"" (name "FF" "f!1(xis!1`seq(ii!1 - 1))" )"1" (replace -1)"1" (lemma "width_lem" )"1" (expand "finseq_appl" )"1" (inst -1 "a!1" "b!1" "P!1" "ii!1-1" )"1" (assert )"1" (case " FF >= 0 AND FF <= 1" )"1" (flatten)"1" (assert )"1" "1" assert )"1" expand "abs" )"1" "1" assert )"1" "FF = 0" )"1" (assert ) nil nil )"2" "FF" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst - "xis!1`seq(ii!1-1)" )"1" (ground) nil nil )"2" (assert )"2" "xis!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "xis!1" )"2" (assert )"2" (flatten) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" integral_def nil )"bool" integral_def nil )nil integral_def nil )"posreal" integral_def nil )nil integral_def nil ))nil )nil 3262440806"" (skosimp*)"" (expand "section" )"" (typepred "P!1" )"" (inst - "ii!1-1" )"1" "FF" "f!1(x_in(seq(P!1)(ii!1 - 1), seq(P!1)(ii!1)))" )"1" (replace -1)"1" (lemma "width_lem" )"1" (expand "finseq_appl" )"1" (inst -1 "a!1" "b!1" "P!1" "ii!1-1" )"1" (assert )"1" (case " FF >= 0 AND FF <= 1" )"1" (flatten)"1" (assert )"1" (mult-ineq -2 -3)"1" assert )"1" expand "abs" )"1" "1" assert )"1" "FF = 0" )"1" (assert ) nil nil )"2" "FF" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x_in(seq(P!1)(ii!1-1), seq(P!1)(ii!1))" )"2" (ground) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (propax) nil nil )"4" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"posreal" integral_def nil )nil integral_def nil )"{t: T | aa <= t AND t <= bb}" integral_def nil )nil integral_def nil ))nil 3262529445"" (skosimp*) (("" (assert ) nil nil )) nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil 3282559921"" (auto-rewrite "xis?" )"" (auto-rewrite "xis_lem" )"" (skosimp*)"" (rewrite "integral_def" )"" (expand "integral?" )"" (skosimp*)"" (inst + "epsi!1/1000" )"" (skosimp*)"" (typepred "R!1" )"" (expand "Riemann_sum?" )"" (skosimp*)"" (replace -1)"" (hide -1)"" (lemma "Rie_sum_alt_lem" )"" "a!1" "b!1" "f!1" )"" assert )"" "" replace -1)"" "" "N" "length(P!1)" )"" case "(EXISTS (k: below(N-1)): xl!1 < seq(P!1)(k) AND seq(P!1)(k+1) < xh!1)" )"1" "1" case "EXISTS (p,q: nat): p >= 1 AND p <= length(P!1) -1 AND seq(P!1)(p-1) <= xl!1 AND xl!1 < seq(P!1)(p)AND q >= 1 AND q <= length(P!1) - 1AND seq(P!1)(q-1) < xh!1 AND xh!1 <= seq(P!1)(q) AND p+1 <= q-1") "1" "1" expand "Rie_sum_alt" )"1" expand "Rie_sec" )"1" assert )"1" "SEC" " LAMBDA (n: upto(length(P!1) - 1)): IF n = 0 THEN 0") "1" replace "1" "SS" "sigma[upto(length(P!1) - 1)](1, length(P!1) - 1, SEC)" )"1" replace "1" case "sigma(p!1+1,q!1-1,SEC) <= SS AND SS <= sigma(p!1,q!1,SEC)" )"1" "1" case "sigma(p!1+1, q!1 - 1, SEC) = seq(P!1)(q!1-1) - seq(P!1)(p!1)" )"1" case "sigma(p!1, q!1, SEC) <= seq(P!1)(q!1) - seq(P!1)(p!1-1)" )"1" "abs(-1 * SS - xl!1 + xh!1) = abs(SS - xh!1 + xl!1)" )"1" "1" expand "abs" )"1" "1" "1" "width_lem" )"1" expand "finseq_appl" )"1" "a!1" "b!1" "P!1" "p!1-1" )"1" "a!1" "b!1" "P!1" "p!1" )"1" "a!1" "b!1" "P!1" "q!1-1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "abs_neg" )"2" "SS - xh!1 + xl!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "EX3p" )"2" "a!1" "b!1" )"2" "2" assert )"2" "P!1" "p!1" "q!1" )"2" assert )"2" assert )"2" replace "2" rewrite "sigma_le" )"1" "1" "1" replace "1" assert )"1" "1" case "f!1(xis!1(n!1 - 1)) <= 1" )"1" assert )"1" "seq(P!1)(n!1) - seq(P!1)(n!1 - 1)" )"1" assert )nil nil )"2" "2" "xis!1" )"2" assert )"2" "n!1-1" )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "xis!1(n!1 - 1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "EX3p" )"2" "a!1" "b!1" )"2" assert )"2" "P!1" "p!1+1" "q!1-1" )"2" assert )"2" case "1 + p!1 <= q!1 - 1" )"1" assert )"1" "1" replace "1" "1" rewrite "sigma_restrict_eq" )"1" "1" expand "restrict" )"1" "1" "1" "1" replace "1" assert )"1" "xis!1(x!1 - 1)" )"1" "1" "parts_order" )"1" "a!1" "b!1" "P!1" "p!1" "x!1-1" )"1" "a!1" "b!1" "P!1" "x!1" "q!1-1" )"1" "1" "xis!1" )"1" expand "xis?" )"1" assert )"1" "xis_lem" )"1" assert )"1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )"3" expand "SEC" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" assert )"2" "2" replace "2" "1" "sigma_upto[length(P!1) - 1].sigma_split_ge" )"1" "_" "N-1" "1" "p!1" )"1" "1" assert )"1" replace "1" "1" "sigma_upto[length(P!1) - 1].sigma_split_ge" )"1" "_" "N-1" "1+p!1" "q!1-1" )"1" "1" assert )"1" replace "1" "sigma(q!1, N - 1, SEC) >= 0 AND sigma(1, p!1, SEC) >= 0" )"1" "1" assert )nil nil ))nil )"2" "2" "sigma_nonneg[upto(length(P!1)-1)]" )"2" case "(FORALL (i: upto(length(P!1) - 1)): SEC(i) >= 0)" )"1" "SEC" "N-1" "q!1" )"1" "SEC" "p!1" "1" )"1" assert )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace "2" assert )"2" "2" "2" "2" "xis!1(i!1 - 1)" )"2" "xis_lem" )"2" assert )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "SEC" )"3" 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 ))nil ))nil )"2" assert )"2" "sigma_upto[length(P!1) - 1].sigma_split_ge" )"2" "_" "N-1" "1" "p!1-1" )"2" "2" assert )"2" replace "2" "2" "sigma(1, p!1 - 1, SEC) = 0" )"1" assert )"1" "1" "sigma_upto[length(P!1) - 1].sigma_split_ge" )"1" "_" "N-1" "p!1" "q!1" )"1" "1" assert )"1" replace "1" "1" "sigma(1 + q!1, N - 1, SEC) = 0" )"1" assert )nil nil )"2" "2" "2" "sigma(1+q!1,N-1, SEC) = sigma(1+q!1,N-1,(LAMBDA (n: upto(length(P!1) - 1)): 0))" )"1" rewrite "sigma_const[upto(length(P!1) - 1)]" )nil nil )"2" "2" rewrite "sigma_restrict_eq" )"2" "2" expand "restrict" )"2" "1" "1" "1" replace "1" assert )"1" "xis!1(x!1 - 1)" )"1" case "xis!1(x!1 - 1) >= xh!1" )"1" assert )nil nil )"2" assert )"2" "xis!1" )"2" assert )"2" "parts_order" )"2" "a!1" "b!1" "P!1" "q!1-1" "x!1" )"2" "a!1" "b!1" "P!1" "q!1" "x!1" )"2" "a!1" "b!1" "P!1" "q!1+1" "x!1" )"2" assert )"2" "a!1" "b!1" "P!1" "q!1" "x!1-1" )"2" "xis_lem" )"2" "a!1" "b!1" "P!1" "xis!1" "x!1-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "SEC" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "sigma(1, p!1 - 1, SEC) = sigma(1,p!1-1,(LAMBDA (n: upto(length(P!1) - 1)): 0))" )"1" "1" rewrite "sigma_const[upto(length(P!1) - 1)]" )nil nil ))nil )"2" rewrite "sigma_restrict_eq" )"2" expand "restrict" )"2" "1" "1" "1" "1" replace "1" assert )"1" "xis!1(x!1-1)" )"1" case "xl!1 >= xis!1(x!1-1)" )"1" nil nil )"2" "xis!1" )"2" assert )"2" "2" "parts_order" )"2" "a!1" "b!1" "P!1" "x!1" "p!1-1" )"2" assert )"2" "xis_lem" )"2" "a!1" "b!1" "P!1" "xis!1" "x!1-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 )"2" "2" expand "SEC" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "M_xl" "min_nat.min({j: below(N) | seq(P!1)(j) > xl!1})" )"1" "M_xh" "min_nat.min({j: below(N) | seq(P!1)(j) >= xh!1})" )"1" "M_xl" "M_xh" )"1" assert )"1" "M_xh" )"1" "M_xh-1" )"1" assert )"1" "M_xl" )"1" "M_xl" )"1" "M_xl-1" )"1" assert )"1" "k!1" )"1" assert )"1" "M_xh" )"1" "k!1+1" )"1" "parts_order" )"1" "a!1" "b!1" "P!1" "M_xl" "k!1+1" )"1" assert )"1" "a!1" "b!1" "P!1" "M_xh" "k!1" )"1" "a!1" "b!1" "P!1" "M_xh" "k!1+1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "N-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "k!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )nil nil ))nil )"5" "5" assert )nil nil ))nil )"6" "6" assert )nil nil ))nil ))nil ))nil )"2" "triangle" )"2" "-1 * Rie_sum(a!1, b!1, P!1, xis!1, f!1)" "xh!1-xl!1" )"2" case "abs(xh!1 - xl!1) < epsi!1/2" )"1" case "abs(-1 * Rie_sum(a!1, b!1, P!1, xis!1, f!1)) < epsi!1/2" )"1" assert )nil nil )"2" "2" rewrite "abs_mult" )"2" "abs(-1) = 1" )"1" "1" "Rie_sum_alt_lem" )"1" "a!1" "b!1" "f!1" )"1" assert )"1" "1" replace "1" "1" expand "Rie_sum_alt" )"1" "M_xh" "min_nat.min({j: below(N) | seq(P!1)(j) >= xh!1})" )"1" case "M_xh > 1" )"1" "M_xh-2" )"1" assert )"1" "M_xh" )"1" "M_xh-1" )"1" assert )"1" "sigma_upto[length(P!1) - 1].sigma_split_ge" )"1" "_" "N-1" "1" "M_xh-2" )"1" "(LAMBDA (n: upto(length(P!1) - 1)): ") "1" assert )"1" replace "1" replace "1" "1" assert )"1" "sigma(1, M_xh - 2, LAMBDA (n: upto(length(P!1) - 1)):") "1" assert )"1" case "abs(Rie_sec(a!1, b!1, P!1, xis!1, f!1, M_xh)) < epsi!1 / 4" )"1" case "abs(Rie_sec(a!1, b!1, P!1, xis!1, f!1, M_xh-1)) < epsi!1 / 4" )"1" "sigma_upto[length(P!1) - 1].sigma_first_ge" )"1" "(LAMBDA (n: upto(length(P!1) - 1)): " "N-1" "M_xh-1" )"1" assert )"1" replace "1" "1" case "1 + M_xh <= length(P!1) - 1" )"1" "sigma_upto[length(P!1) - 1].sigma_first_ge" )"1" "(LAMBDA (n: upto(length(P!1) - 1)): " "N-1" "M_xh" )"1" assert )"1" replace "1" "1" "sigma(1 + M_xh, N - 1, LAMBDA (n: upto(length(P!1) - 1)):") "1" assert )"1" assert )"1" "triangle" )"1" "Rie_sec(a!1, b!1, P!1, xis!1, f!1, M_xh)" "Rie_sec(a!1, b!1, P!1, xis!1, f!1, M_xh - 1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "sigma(1 + M_xh, N - 1, LAMBDA (n: upto(length(P!1) - 1)):LAMBDA (n: upto(length(P!1) - 1)): 0))") "1" assert )"1" rewrite "sigma_const[upto(length(P!1) - 1)]" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq" )"1" "1" expand "restrict" )"1" "1" "1" "1" expand "Rie_sec" )"1" assert )"1" "xis!1(x!1-1)" )"1" assert )"1" case "xis!1(x!1-1) >= xh!1" )"1" assert )nil nil )"2" "2" "xis!1(x!1-1)" )"2" "parts_order" )"2" "a!1" "b!1" "P!1" "M_xh" "x!1-1" )"2" assert )"2" "xis_lem" )"2" assert )"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 )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "M_xh" )"2" rewrite "sigma_rew" "1" assert )"1" assert )"1" "triangle" )"1" "Rie_sec(a!1, b!1, P!1, xis!1, f!1, M_xh)" "Rie_sec(a!1, b!1, P!1, xis!1, f!1, M_xh - 1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "EXse" )"2" "epsi!1/1000" "a!1" "b!1" "f!1" "M_xh-1" "xh!1" "xl!1" )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "Rie_sec" )"2" "2" assert )"2" case "f!1(xis!1(M_xh - 1)) <= 1" )"1" case "P!1`seq(1 + (M_xh - 1)) - P!1`seq(M_xh - 1) < epsi!1 / 4" )"1" "1" "f!1(xis!1(M_xh - 1)) >= 0" )"1" "1" expand "abs" )"1" "1" case "seq(P!1)(M_xh) - seq(P!1)(M_xh - 1) > 0" )"1" assert )"1" case "(seq(P!1)(M_xh) - seq(P!1)(M_xh - 1))* f!1(xis!1(M_xh - 1)) >= 0" )"1" assert )nil nil )"2" "2" "ge_times_ge_pos" )"2" "0" "0" "f!1(xis!1(M_xh - 1))" "seq(P!1)(M_xh) - seq(P!1)(M_xh - 1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "xis!1(M_xh - 1)" )"2" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "width_lem" )"2" assert )"2" "a!1" "b!1" "P!1" "M_xh-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "xis!1(M_xh - 1)" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "sigma(1, M_xh - 2, LAMBDA (n: upto(length(P!1) - 1)):LAMBDA (n: upto(length(P!1) - 1)):") "1" assert )"1" rewrite "sigma_const[upto(length(P!1) - 1)]" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq" )"1" "1" expand "restrict" )"1" "1" "1" "1" expand "Rie_sec" )"1" case "f!1(xis!1(x!1-1)) = 0" )"1" assert )nil nil )"2" assert )"2" "2" "xis!1(x!1-1)" )"2" assert )"2" "2" "parts_order" )"2" "a!1" "b!1" "P!1" "x!1" "M_xh-2" )"2" "xis_lem" )"2" assert )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "P!1" )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "M_xh = 1" )"1" replace "1" case "3 <= length(P!1)" )"1" assert )"1" "sigma_upto[length(P!1) - 1].sigma_first_ge" )"1" "(LAMBDA (n: upto(length(P!1) - 1)): Rie_sec(a!1, b!1, " "N-1" "1" )"1" assert )"1" replace "1" "sigma(2, N - 1, LAMBDA (n: upto(length(P!1) - 1)):") "1" "1" "EXse" )"1" "epsi!1/1000" "a!1" "b!1" "f!1" "1" "xh!1" "xl!1" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "sigma(2, N - 1, (LAMBDA (n: upto(length(P!1) - 1)): LAMBDA (n:") "1" rewrite "sigma_const[upto(length(P!1) - 1)]" )"1" "1" assert )nil nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq" )"1" "1" expand "restrict" )"1" "1" "1" "1" "x!1 - 1 >= M_xh" )"1" expand "Rie_sec" )"1" assert )"1" "xis!1(x!1-1)" )"1" assert )"1" "xis!1(x!1-1) >= xh!1" )"1" nil nil )"2" "2" "parts_order" )"2" "a!1" "b!1" "P!1" "M_xh" "x!1-1" )"2" assert )"2" "xis_lem" )"2" assert )"2" "2" "2" assert )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 )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "sigma_rew" )"1" "EXse" )"1" "epsi!1/1000" "a!1" "b!1" "f!1" "1" "xh!1" "xl!1" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "N-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "M_xh" "min_nat.min({j: below(N) | seq(P!1)(j) >= xh!1})" )"1" case "M_xh = 1" )"1" case "xh!1 - xl!1 <=seq(P!1)(M_xh) - seq(P!1)(0)" )"1" expand "abs" "1" assert )"1" "width_lem" )"1" assert )"1" "a!1" "b!1" "P!1" "M_xh-1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil )"2" "M_xh-2" )"1" assert )"1" "M_xh" )"1" assert )"1" "M_xh-1" )"1" assert )"1" expand "abs" "1" case "xh!1 - xl!1 <=seq(P!1)(M_xh) - seq(P!1)(M_xh-2)" )"1" "width_lem" )"1" assert )"1" "a!1" "b!1" "P!1" "M_xh-2" )"1" "a!1" "b!1" "P!1" "M_xh-1" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "N-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil )"4" "4" (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 )"real" reals nil )nil integral_def nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields 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]" integral_pulse nil )nil integral_pulse nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )nil integral_def nil )"(total_order?[real])" nil )nil real_props nil )"odd_int" integers nil )nil integral_pulse nil )nil sigma_upto "reals/" )nil sigma "reals/" )nil real_props nil )nil extra_real_props nil )nil abs_lems "reals/" )"posreal" nil )"{a | AND " nil )"T" integral_pulse nil )"nat" integral_pulse nil )"nnreal" nil )"{j: posint | j >= i}" nil )nil real_props nil )"nnreal" nil )"{a | AND " nil )"real" integral_def nil )set type-eq-decl nil sets nil )"bool" sets nil )min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" nil )"bool" sets nil )"bool" sets nil )"real" integral_def nil )nil naturalnumbers nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )nil integers nil )nil integral_pulse nil )nil sigma "reals/" )nil integers nil )nil extra_real_propsnil )"subrange(p!1, q!1)" integral_pulse nil )"nat" integral_pulse nil )"nat" integral_pulse nil )"partition[T](a!1, b!1)" integral_pulse nil )"T" integral_pulse nil )"T" integral_pulse nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )"odd_int" integers nil )"[below[length(fs)] -> T]" finite_sequencesnil )"real" reals nil )"int" integers nil )"posint" nil )nil integral_def nil )nil abs_lems "reals/" )"[upto(length(P!1) - 1) -> numfield]" nil )"(strict_total_order?[real])" real_props nil )nil integral_def nil )nil integral_def nil )"[T -> real]" sigma "reals/" )nil sigma "reals/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )nil sigma "reals/" )"nat" sigma_upto "reals/" )nil sigma_upto "reals/" )nil sigma "reals/" )"even_int" integersnil )nil nat_types nil )"real" integral_def nil )"[bool, bool -> bool]" booleans nil )"posint" nil )"bool" integral_def nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" integral_def nil )nil intervals_real "reals/" )nil finite_sequences nil )nil integral_def nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"posreal" nil )"bool" integral_def nil )"real" reals nil )"real" reals nil ))nil )nil 3280253494"" (skosimp*)"" (rewrite "integral_def" )"" (expand "integral?" )"" (skosimp*)"" (inst + "epsi!1/1000" )"" (skosimp*)"" (typepred "R!1" )"" (expand "Riemann_sum?" )"" (skosimp*)"" (replace -1)"" (hide -1)"" (lemma "Rie_sum_alt_lem" )"" (inst - "a!1" "b!1" "f!1" )"" (assert )"" "" replace -1)"" "" "N" "length(P!1)" )"" case "(EXISTS (k: below(N-1)): xl!1 < seq(P!1)(k) AND seq(P!1)(k+1) < xh!1)" )"1" "1" case "EXISTS (p,q: nat): p >= 1 AND p <= length(P!1) -1 AND seq(P!1)(p-1) <= xl!1 AND xl!1 < seq(P!1)(p)AND q >= 1 AND q <= length(P!1) - 1AND seq(P!1)(q-1) < xh!1 AND xh!1 <= seq(P!1)(q) AND p+1 <= q-1") "1" "1" expand "Rie_sum_alt" )"1" expand "Rie_sec" )"1" assert )"1" "SEC" " LAMBDA (n: upto(length(P!1) - 1)): IF n = 0 THEN 0") "1" replace -1)"1" "SS" "sigma[upto(length(P!1) - 1)](1, length(P!1) - 1, SEC)" )"1" replace "1" case "sigma(p!1+1,q!1-1,SEC) <= SS AND SS <= sigma(p!1,q!1,SEC)" )"1" "1" case "sigma(p!1+1, q!1 - 1, SEC) = seq(P!1)(q!1-1) - seq(P!1)(p!1)" )"1" case "sigma(p!1, q!1, SEC) <= seq(P!1)(q!1) - seq(P!1)(p!1-1)" )"1" "abs(-1 * SS - xl!1 + xh!1) = abs(SS - xh!1 + xl!1)" )"1" "1" expand "abs" )"1" "1" "1" "width_lem" )"1" expand "finseq_appl" )"1" "a!1" "b!1" "P!1" "p!1-1" )"1" "a!1" "b!1" "P!1" "p!1" )"1" "a!1" "b!1" "P!1" "q!1-1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" expand "abs" )"2" "2" "2" "1" "1" nil nil ))nil )"2" "2" "1" "1" assert )nil nil ))nil )"2" "2" "AAAA" "SS - xh!1 + xl!1" )"2" replace "2" "-1" )"2" replace "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "EX3p" )"2" "a!1" "b!1" )"2" "2" assert )"2" "P!1" "p!1" "q!1" )"2" assert )"2" assert )"2" replace "2" rewrite "sigma_le" )"1" "1" "1" replace "1" assert )"1" "1" case "f!1(xis!1(n!1 - 1)) <= 1" )"1" assert )"1" "seq(P!1)(n!1) - seq(P!1)(n!1 - 1)" )"1" assert )nil nil )"2" "2" "xis!1" )"2" assert )"2" "n!1-1" )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "xis!1(n!1 - 1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "EX3p" )"2" "a!1" "b!1" )"2" assert )"2" "P!1" "p!1+1" "q!1-1" )"2" assert )"2" case "1 + p!1 <= q!1 - 1" )"1" assert )"1" "1" replace "1" "1" rewrite "sigma_restrict_eq" )"1" "1" expand "restrict" )"1" "1" "1" "1" replace "1" assert )"1" "xis!1(x!1 - 1)" )"1" "1" "parts_order" )"1" "a!1" "b!1" "P!1" "p!1" "x!1-1" )"1" "a!1" "b!1" "P!1" "x!1" "q!1-1" )"1" "1" "xis!1" )"1" expand "xis?" )"1" assert )"1" "xis_lem" )"1" assert )"1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" assert )"2" "2" replace "2" "1" "sigma_split_ge[length(P!1) - 1]" )"1" "_" "N-1" "1" "p!1" )"1" "1" assert )"1" replace "1" "1" "sigma_split_ge[length(P!1) - 1]" )"1" "_" "N-1" "1+p!1" "q!1-1" )"1" "1" assert )"1" replace "1" "sigma(q!1, N - 1, SEC) >= 0 AND sigma(1, p!1, SEC) >= 0" )"1" "1" assert )nil nil ))nil )"2" "2" "sigma_nonneg[upto(length(P!1)-1)]" )"2" case "(FORALL (i: upto(length(P!1) - 1)): SEC(i) >= 0)" )"1" "SEC" "N-1" "q!1" )"1" "SEC" "p!1" "1" )"1" assert )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace "2" assert )"2" "2" "2" "2" "xis!1(i!1 - 1)" )"2" "xis_lem" )"2" assert )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 ))nil ))nil )"2" assert )"2" "sigma_split_ge[length(P!1) - 1]" )"2" "_" "N-1" "1" "p!1-1" )"2" "2" assert )"2" replace "2" "2" "sigma(1, p!1 - 1, SEC) = 0" )"1" assert )"1" "1" "sigma_split_ge[length(P!1) - 1]" )"1" "_" "N-1" "p!1" "q!1" )"1" "1" assert )"1" replace "1" "1" "sigma(1 + q!1, N - 1, SEC) = 0" )"1" assert )nil nil )"2" "2" "2" "sigma(1+q!1,N-1, SEC) = sigma(1+q!1,N-1,(LAMBDA (n: upto(length(P!1) - 1)): 0))" )"1" rewrite "sigma_const" )nil nil )"2" "2" rewrite "sigma_restrict_eq" )"2" "2" expand "restrict" )"2" "2" "2" "2" replace "2" assert )"2" "xis!1(x!1 - 1)" )"2" case "xis!1(x!1 - 1) >= xh!1" )"1" assert )nil nil )"2" assert )"2" "xis!1" )"2" assert )"2" "parts_order" )"2" "a!1" "b!1" "P!1" "q!1-1" "x!1" )"2" "a!1" "b!1" "P!1" "q!1" "x!1" )"2" "a!1" "b!1" "P!1" "q!1+1" "x!1" )"2" assert )"2" "a!1" "b!1" "P!1" "q!1" "x!1-1" )"2" "xis_lem" )"2" "a!1" "b!1" "P!1" "xis!1" "x!1-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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "sigma(1, p!1 - 1, SEC) = sigma(1,p!1-1,(LAMBDA (n: upto(length(P!1) - 1)): 0))" )"1" "1" rewrite "sigma_const" )nil nil ))nil )"2" rewrite "sigma_restrict_eq" )"2" expand "restrict" )"2" "2" "2" "2" "2" replace "2" assert )"2" "xis!1(x!1-1)" )"2" case "xl!1 >= xis!1(x!1-1)" )"1" nil nil )"2" "xis!1" )"2" assert )"2" "2" "parts_order" )"2" "a!1" "b!1" "P!1" "x!1" "p!1-1" )"2" assert )"2" "xis_lem" )"2" "a!1" "b!1" "P!1" "xis!1" "x!1-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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "M_xl" "min_nat.min({j: below(N) | seq(P!1)(j) > xl!1})" )"1" "M_xh" "min_nat.min({j: below(N) | seq(P!1)(j) >= xh!1})" )"1" "M_xl" "M_xh" )"1" assert )"1" "M_xh" )"1" "M_xh-1" )"1" assert )"1" "M_xl" )"1" "M_xl" )"1" "M_xl-1" )"1" assert )"1" "k!1" )"1" assert )"1" "M_xh" )"1" "k!1+1" )"1" "parts_order" )"1" "a!1" "b!1" "P!1" "M_xl" "k!1+1" )"1" assert )"1" "a!1" "b!1" "P!1" "M_xh" "k!1" )"1" "a!1" "b!1" "P!1" "M_xh" "k!1+1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "N-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "k!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil )"3" "3" (assert ) nil nil ))nil )"4" "4" (assert ) nil nil ))nil )"5" "5" (assert ) nil nil ))nil )"6" "6" (assert ) nil nil ))nil ))nil ))nil )"2" "triangle" )"2" "-1 * Rie_sum(a!1, b!1, P!1, xis!1, f!1)" "xh!1-xl!1" )"2" case "abs(xh!1 - xl!1) < epsi!1/2" )"1" case "abs(-1 * Rie_sum(a!1, b!1, P!1, xis!1, f!1)) < epsi!1/2" )"1" (assert ) nil nil )"2" "2" rewrite "abs_mult" )"2" "abs(-1) = 1" )"1" "1" "Rie_sum_alt_lem" )"1" "a!1" "b!1" "f!1" )"1" assert )"1" "1" replace "1" "1" expand "Rie_sum_alt" )"1" "M_xh" "min_nat.min({j: below(N) | seq(P!1)(j) >= xh!1})" )"1" case "M_xh > 1" )"1" "M_xh-2" )"1" assert )"1" "M_xh" )"1" "M_xh-1" )"1" assert )"1" "sigma_split_ge[length(P!1) - 1]" )"1" "_" "N-1" "1" "M_xh-2" )"1" "(LAMBDA (n: upto(length(P!1) - 1)): ") "1" assert )"1" replace "1" replace "1" "1" assert )"1" "sigma(1, M_xh - 2, LAMBDA (n: upto(length(P!1) - 1)):") "1" assert )"1" case "abs(Rie_sec(a!1, b!1, P!1, xis!1, f!1, M_xh)) < epsi!1 / 4" )"1" case "abs(Rie_sec(a!1, b!1, P!1, xis!1, f!1, M_xh-1)) < epsi!1 / 4" )"1" "sigma_first_ge[length(P!1) - 1]" )"1" "(LAMBDA (n: upto(length(P!1) - 1)): " "N-1" "M_xh-1" )"1" assert )"1" replace "1" "1" case "1 + M_xh <= length(P!1) - 1" )"1" "sigma_first_ge[length(P!1) - 1]" )"1" "(LAMBDA (n: upto(length(P!1) - 1)): " "N-1" "M_xh" )"1" assert )"1" replace "1" "1" "sigma(1 + M_xh, N - 1, LAMBDA (n: upto(length(P!1) - 1)):") "1" assert )"1" assert )"1" "triangle" )"1" "Rie_sec(a!1, b!1, P!1, xis!1, f!1, M_xh)" "Rie_sec(a!1, b!1, P!1, xis!1, f!1, M_xh - 1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "sigma(1 + M_xh, N - 1, LAMBDA (n: upto(length(P!1) - 1)):LAMBDA (n: upto(length(P!1) - 1)): 0))") "1" rewrite "sigma_const" )"1" "1" assert )nil nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq" )"1" "1" expand "restrict" )"1" "1" "1" "1" expand "Rie_sec" )"1" assert )"1" "xis!1(x!1-1)" )"1" assert )"1" case "xis!1(x!1-1) >= xh!1" )"1" assert )nil nil )"2" "2" "xis!1(x!1-1)" )"2" "parts_order" )"2" "a!1" "b!1" "P!1" "M_xh" "x!1-1" )"2" assert )"2" "xis_lem" )"2" assert )"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 )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "M_xh" )"2" expand "sigma" "2" assert )"2" assert )"2" "triangle" )"2" "Rie_sec(a!1, b!1, P!1, xis!1, f!1, M_xh)" "Rie_sec(a!1, b!1, P!1, xis!1, f!1, M_xh - 1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "EXse" )"2" "epsi!1/1000" "a!1" "b!1" "f!1" "M_xh-1" "xh!1" "xl!1" )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "Rie_sec" )"2" "2" assert )"2" case "f!1(xis!1(M_xh - 1)) <= 1" )"1" case "P!1`seq(1 + (M_xh - 1)) - P!1`seq(M_xh - 1) < epsi!1 / 4" )"1" "1" "f!1(xis!1(M_xh - 1)) >= 0" )"1" "1" expand "abs" )"1" "1" case "seq(P!1)(M_xh) - seq(P!1)(M_xh - 1) > 0" )"1" assert )"1" case "(seq(P!1)(M_xh) - seq(P!1)(M_xh - 1))* f!1(xis!1(M_xh - 1)) >= 0" )"1" assert )nil nil )"2" "2" "ge_times_ge_pos" )"2" "0" "0" "f!1(xis!1(M_xh - 1))" "seq(P!1)(M_xh) - seq(P!1)(M_xh - 1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "xis!1(M_xh - 1)" )"2" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "width_lem" )"2" assert )"2" "a!1" "b!1" "P!1" "M_xh-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "xis!1(M_xh - 1)" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "sigma(1, M_xh - 2, LAMBDA (n: upto(length(P!1) - 1)):LAMBDA (n: upto(length(P!1) - 1)):") "1" rewrite "sigma_const" )"1" "1" assert )nil nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq" )"1" "1" expand "restrict" )"1" "1" "1" "1" expand "Rie_sec" )"1" case "f!1(xis!1(x!1-1)) = 0" )"1" assert )nil nil )"2" assert )"2" "2" "xis!1(x!1-1)" )"2" assert )"2" "2" "parts_order" )"2" "a!1" "b!1" "P!1" "x!1" "M_xh-2" )"2" "xis_lem" )"2" assert )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "P!1" )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "M_xh = 1" )"1" replace "1" case "3 <= length(P!1)" )"1" "sigma_first_ge[length(P!1) - 1]" )"1" "(LAMBDA (n: upto(length(P!1) - 1)): Rie_sec(a!1, b!1, " "N-1" "1" )"1" assert )"1" replace "1" "sigma(2, N - 1, LAMBDA (n: upto(length(P!1) - 1)):") "1" "1" "EXse" )"1" "epsi!1/1000" "a!1" "b!1" "f!1" "1" "xh!1" "xl!1" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "sigma(2, N - 1, (LAMBDA (n: upto(length(P!1) - 1)): LAMBDA (n:") "1"
Messung V0.5 in Prozent C=100 H=99 G=99
¤ Dauer der Verarbeitung: 0.601 Sekunden
(vorverarbeitet am 2026-05-05)
¤ *© Formatika GbR, Deutschland
2026-05-26
