Quelle integral_step.prf
Sprache: Lisp
(integral_stepnil 3282481239"" (lemma "connected_domain" ) (("" (propax) nil nil )) nil )nil integral_step nil )) shostak))nil 3282481239"" (lemma "not_one_element" ) (("" (propax) nil nil )) nil )nil integral_step nil )) shostak))nil 3403457729 ("" (subtype-tcc) nil nil )"(total_order?[real])" nil ))nil ))nil 3403457729 ("" (subtype-tcc) nil nil )"odd_int" integers nil )"(total_order?[real])" nil ))nil ))nil 3403457729 ("" (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 )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil ))nil 3403457735"" (skosimp*) (("" (expand "sigma" ) (("" (propax) nil nil )) nil ))nil )"real" sigma "reals/" )) shostak))nil 3281791727 ("" (subtype-tcc) nil nil ) nil shostak))nil 3281791727 ("" (subtype-tcc) nil nil ) nil shostak))nil 3281791727 ("" (subtype-tcc) nil nil ) nil shostak))nil 3281793131"" (skosimp*)"" (expand "nonempty?" )"" (expand "empty?" )"" (expand "member" )"" (inst - "(seq(P!1)(j!1) + seq(P!1)(1 + j!1))/2" )"1" (typepred "P!1" )"1" (inst - "j!1" )"1" (split)"1" (cross-mult 1) (("1" (assert ) nil nil )) nil )"2" (cross-mult 1) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (lemma "connected_domain" )"2" (expand "connected?" )"2" "seq(P!1)(j!1)" "seq(P!1)(1 + j!1)" "(seq(P!1)(j!1) + seq(P!1)(1 + j!1))/2" )"2" (assert )"2" (hide 2)"2" (typepred "P!1" )"2" (inst - "j!1" )"2" (split)"1" (cross-mult 1)"1" (assert ) nil nil )) nil )"2" (cross-mult 1)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )nil integral_step nil )nil real_props nil )nil real_props nil )"(total_order?[real])" nil )"bool" deriv_domain_def nil )NOT const-decl "[bool -> bool]" booleans nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil real_types nil )nil real_types nil )nil real_props nil )nil 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]" integral_step nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )nil nat_types nil )nil integral_step nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"T" integral_step nil )"bool" reals nil )"{x: T | a!1 < x}" integral_step nil )nil intervals_real "reals/" )nil finite_sequences nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil integral_def nil )"partition[T](a!1, b!1)" integral_step nil )"below(length(P!1) - 1)" integral_step nil )"posint" nil )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil ))nil )nil 3281791727"" (subtype-tcc)"1" (postpone) nil nil ) ("2" (postpone) nil nil )) nil )nil shostak))nil 3262529911"" (skosimp*) (("" (assert ) nil nil )) nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil ))nil 3262529911"" (skosimp*) (("" (assert ) nil nil )) nil )"posint" nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3262529911"" (skosimp*) (("" (assert ) nil nil )) nil )"int" integers nil )"(total_order?[real])" nil )"posint" nil )"(strict_total_order?[real])" real_props nil ))nil 3262529911"" (skosimp*) (("" (assert ) nil nil )) nil )"(strict_total_order?[real])" real_props nil ))nil 3262529850"" (skosimp*)"" (expand "stp_sect" )"" (case "x!1 = seq(P!1)(ii!1)" )"1" (assert )"1" (lemma "parts_order" )"1" (inst - "a!1" "b!1" "P!1" "ii!1" "jj!1" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (assert )"2" (lift-if)"2" (lemma "parts_order" )"2" (inst - "a!1" "b!1" "P!1" "ii!1" "jj!1" )"2" (assert )"2" (lemma "parts_order" )"2" (inst - "a!1" "b!1" "P!1" "ii!1+1" "jj!1" )"2" (assert ) (("2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" integral_step nil )"posint" nil )"posint" nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil integral_def nil )"(strict_total_order?[real])" real_props nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" integral_step nil )nil integral_step nil )nil naturalnumbers nil )nil nat_types nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil intervals_real "reals/" )nil finite_sequences nil )"bool" reals 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 naturalnumbers nil ))nil ))nil 3262529911"" (skosimp*) (("" (assert ) nil nil )) nil )"posint" nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3262529911"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3262529900"" (skolem!)"" (assert )"" (flatten)"" (skolem!)"" (induct "j" )"1" (assert )"1" (flatten)"1" (expand "sigma" )"1" (lemma "stp_sect_lem" )"1" (inst?)"1" (inst -1 "f!1" "x!1" )"1" (assert )"1" (inst?)"1" (inst -1 "1" )"1" assert )"1" expand "sigma" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "sigma" 1)"2" (assert )"2" " sigma(0, j!1, LAMBDA (ii: nat):IF ii >= 2 + j!1 THEN 0LAMBDA (ii: nat):IF ii >= 1 + j!1 THEN 0") "1" (hide -1)"1" (case "x!1 > seq(P!1)(1 + j!1)" )"1" (assert )"1" (replace -2)"1" (lemma "stp_sect_lem" )"1" "1" "f!1" "x!1" )"1" assert )"1" "1" "j!1+2" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "parts_order" )"2" "a!1" "b!1" "P!1" "j!1+1" "j!1+2" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" (rewrite "sigma_restrict_eq[nat]" )"2" (hide 2)"2" (expand "restrict" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*) nil nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"[T -> real]" sigma "reals/" )nil sigma "reals/" )nil integral_def nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )nil naturalnumbers nil )nil integral_step nil )nil naturalnumbers nil )"real" integral_step nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil defined_types nil )"T" integral_step nil )NOT const-decl "[bool -> bool]" booleans 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, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil nat_types nil )"[real -> boolean]" integral_step nil )nil integral_step nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T" integral_step nil )"T" integral_step nil )nil intervals_real "reals/" )nil finite_sequences nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil integral_def nil )"partition[T](a!1, b!1)" integral_step nil )"int" integers nil )"posint" nil ))nil ))nil 3281868373 ("" (subtype-tcc) nil nil )nil shostak))nil 3281868373 ("" (subtype-tcc) nil nil )nil shostak))nil 3281796581"" (skosimp*)"" (rewrite "integral_def" :dir rl)"1" (lemma "zero_except_intv?_integrable" )"1" (inst?)"1" (assert )"1" (assert )"1" "val_in(a!1, b!1, P!1, j!1, f!1)" "seq(P!1)(1 + j!1)" "seq(P!1)(j!1)" )"1" (assert )"1" (split -1)"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (typepred "P!1" )"2" (inst - "j!1" ) nil nil )) nil )"3" (assert )"3" (hide 2)"3" (expand "zero_except_intv?" )"3" (skosimp*)"3" (assert )"3" expand "stp_sect" )"3" assert )"3" "3" expand "val_in" )"3" "3" "P!1" )"3" "j!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (lemma "parts_order[T]" )"2" (inst - "a!1" "b!1" "P!1" "0" "1+j!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"posint" nil )"real" reals nil )nil integral_def nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil intervals_real "reals/" )nil finite_sequences nil )"bool" reals 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 )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil integral_def nil )"real" integral_step nil )"[numfield, numfield -> numfield]" number_fields nil )"real" integral_step 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_step nil )nil integral_step nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"posint" nil )NOT const-decl "[bool -> bool]" booleans nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"bool" integral_pulse nil )"(total_order?[real])" nil )nil integral_pulse nil ))nil 3281876432 ("" (subtype-tcc) nil nil ) nil shostak))nil 3281876432 ("" (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 )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"[real -> boolean]" integral_step nil )nil integral_step nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil 3261756014"" (skosimp*) (("" (assert ) nil nil )) nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil ))nil 3306073359"" (auto-rewrite "sigma_0_m1" )"" (skolem!)"" (flatten)"" (expand "step_function_on?" )"" (induct "n" )"1" (assert )"1" (skosimp*)"1" (expand "sumof" )"1" (expand "sigma" )"1" (inst - "0" )"1" (skosimp*)"1" (expand "stp_sect" )"1" (assert )"1" (lift-if)"1" "1" "P!1" )"1" "0" )"1" "1" expand "val_in" )"1" "pick(a!1, b!1, P!1, 0)" )"1" "x!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "P!1" )"2" (assert )"2" (skosimp*)"2" (split -5)"1" (inst?)"1" (assert )"1" (case "x!1 <= seq(P!1)(1 + j!1)" )"1" (assert )"1" (expand "sumof" )"1" expand "sigma" 1)"1" " sigma(0, j!1, LAMBDA (ii: nat):IF ii > 1 + j!1 THEN 0LAMBDA (ii: nat):IF ii > j!1 THEN 0") "1" "1" "1" replace -2)"1" "1" expand "stp_sect" )"1" "1" "P!1" )"1" "j!1+1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq[nat]" )"2" "2" expand "restrict" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (hide -1)"2" expand "sumof" )"2" assert )"2" "j!1+1" )"2" assert )"2" "2" "x!1 = seq(P!1)(2 + j!1)" )"1" assert )"1" "(LAMBDA (ii: nat): IF ii > 1 + j!1 THEN 0LAMBDA (ii: nat): 0)") "1" rewrite "sigma_const[nat]" )nil nil )"2" "2" "2" "2" "2" expand "stp_sect" )"2" "2" "1" "parts_order[T]" )"1" "a!1" "b!1" "P!1" "x!2" "2+j!1" )"1" assert )nil nil ))nil ))nil )"2" expand "val_in" )"2" "parts_order[T]" )"2" "a!1" "b!1" "P!1" "x!2+1" "2+j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "sigma_stp_sect" )"2" "a!1" "b!1" "f!1" "x!1" )"2" assert )"2" "P!1" )"2" expand "sigma" "2" "j!1" )"2" assert )"2" assert )"2" " sigma(0, j!1, LAMBDA (ii: nat):IF ii > 1 + j!1 THEN 0LAMBDA (ii: nat):IF ii >= 1 + j!1 THEN 0") "1" "1" replace "1" expand "stp_sect" )"1" "j!1+1" )"1" "1" "x!1" )"1" expand "val_in" )"1" "pick(a!1, b!1, P!1, 1 + j!1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" rewrite "sigma_restrict_eq[nat]" )"2" "2" expand "restrict" )"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 )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (assert ) nil nil )"5" (skosimp*) (("5" (assert ) nil nil )) nil )"6" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"bool" step_fun_def nil )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"real" reals nil )nil sigma "reals/" )"[T -> real]" sigma "reals/" )nil sigma "reals/" )"int" integers nil )"(total_order?[real])" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil integral_def nil )nil integral_step nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"odd_int" integers nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"{t: T | seq(P)(j) < t AND t < seq(P)(j + 1)}" nil )nil intervals_real "reals/" )"real" integral_step nil )nil integral_step nil )"real" reals nil )"real" sigma "reals/" )"nat" integral_step nil )"(strict_total_order?[real])" real_props nil )"nat" integral_step nil )nil naturalnumbers nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" integral_step nil )"real" integral_step nil )nil integral_step nil )nil naturalnumbers nil )nil defined_types 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, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil nat_types nil )"[real -> boolean]" integral_step nil )nil integral_step nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T" integral_step nil )"bool" reals nil )"{x: T | a!1 < x}" integral_step nil )nil intervals_real "reals/" )nil finite_sequences nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil integral_def nil )"partition[T](a!1, b!1)" integral_step nil )"int" integers nil )"posint" nil ))nil )nil 3281792634"" (skolem!)"" (flatten)"" (expand "step_function_on?" )"" (induct "n" )"1" (assert )"1" (skosimp*)"1" (expand "sumof" )"1" (expand "sigma" )"1" (inst - "0" )"1" (skosimp*)"1" (expand "stp_sect" )"1" (assert )"1" (lift-if)"1" (lift-if)"1" "P!1" )"1" "0" )"1" "1" expand "val_in" )"1" "pick(a!1, b!1, P!1, 0)" )"1" "x!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "P!1" )"2" (assert )"2" (skosimp*)"2" (split -5)"1" (inst?)"1" (assert )"1" (case "x!1 <= seq(P!1)(1 + j!1)" )"1" (assert )"1" (expand "sumof" )"1" (expand "sigma" 1)"1" " sigma(0, j!1, LAMBDA (ii: nat):IF ii > 1 + j!1 THEN 0LAMBDA (ii: nat):IF ii > j!1 THEN 0") "1" "1" "1" replace -2)"1" "1" expand "stp_sect" )"1" "1" "P!1" )"1" "j!1+1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq[nat]" )"1" "1" expand "restrict" )"1" (propax) nil nil ))nil ))nil )"2" "connected_domain" )"2" assert )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" "connected_domain" )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (hide -1)"2" (expand "sumof" )"2" assert )"2" "j!1+1" )"2" assert )"2" "2" "x!1 = seq(P!1)(2 + j!1)" )"1" assert )"1" "(LAMBDA (ii: nat): IF ii > 1 + j!1 THEN 0LAMBDA (ii: nat): 0)") "1" rewrite "sigma_const[nat]" )"1" "1" assert )nil nil ))nil ))nil )"2" "2" "2" "2" "2" expand "stp_sect" )"2" "2" "1" "parts_order[T]" )"1" "a!1" "b!1" "P!1" "x!2" "2+j!1" )"1" assert )nil nil ))nil ))nil )"2" expand "val_in" )"2" "parts_order[T]" )"2" "a!1" "b!1" "P!1" "x!2+1" "2+j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "sigma_stp_sect[T]" )"2" "a!1" "b!1" "f!1" "x!1" )"2" assert )"2" "P!1" )"2" expand "sigma" 3)"2" "j!1" )"2" assert )"2" assert )"2" " sigma(0, j!1, LAMBDA (ii: nat):IF ii > 1 + j!1 THEN 0LAMBDA (ii: nat):IF ii >= 1 + j!1 THEN 0") "1" "1" replace "1" expand "stp_sect" )"1" "j!1+1" )"1" "1" "x!1" )"1" expand "val_in" )"1" "pick(a!1, b!1, P!1, 1 + j!1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" rewrite "sigma_restrict_eq[nat]" )"1" "1" expand "restrict" )"1" nil nil ))nil ))nil )"2" "connected_domain" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" 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" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (assert ) nil nil )"5" (skosimp*) (("5" (assert ) nil nil )) nil )"6" (assert ) nil nil ))nil ))nil ))nil ))nil )nil integral_def nil )"real" sigma "reals/" )nil integral_def nil )nil sigma "reals/" )"[T -> real]" sigma "reals/" )nil sigma "reals/" )"bool" step_fun_def nil ))nil )nil 3261754034"" (skosimp*)"" (expand "step_function?" )"" (skosimp*)"" (inst + "P!1" )"" (induct "n" )"1" (assert )"1" (skosimp*)"1" (expand "sumof" )"1" (expand "sigma" )"1" (inst - "0" )"1" (skosimp*)"1" (expand "stp_sect" )"1" (assert )"1" (lift-if)"1" "1" "P!1" )"1" "0" )"1" "1" "(seq(P!1)(0) + seq(P!1)(1)) / 2" )"1" "x!1" )"1" (assert ) nil nil ))nil )"2" assert )"2" "2" "connected_domain" )"2" "2" "seq(P!1)(0)" "seq(P!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 )"2" (typepred "P!1" )"2" (assert )"2" (skosimp*)"2" (split -5)"1" (inst?)"1" (assert )"1" (case "x!1 <= seq(P!1)(1 + j!1)" )"1" (assert )"1" (expand "sumof" )"1" expand "sigma" 1)"1" " sigma(0, j!1, LAMBDA (ii: nat):IF ii > 1 + j!1 THEN 0LAMBDA (ii: nat):IF ii > j!1 THEN 0") "1" "1" "1" replace -2)"1" "1" expand "stp_sect" )"1" "1" "P!1" )"1" "j!1+1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq[nat]" )"1" "1" expand "restrict" )"1" (propax) nil nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (hide -1)"2" expand "sumof" )"2" assert )"2" "j!1+1" )"2" assert )"2" "2" "x!1 = seq(P!1)(2 + j!1)" )"1" assert )"1" "(LAMBDA (ii: nat): IF ii > 1 + j!1 THEN 0LAMBDA (ii: nat): 0)") "1" rewrite "sigma_const[nat]" )"1" "1" assert )nil nil ))nil ))nil )"2" "2" "2" "2" "2" expand "stp_sect" )"2" "2" "1" "parts_order" )"1" "a!1" "b!1" "P!1" "x!2" "2+j!1" )"1" assert )nil nil ))nil ))nil )"2" "parts_order" )"2" "a!1" "b!1" "P!1" "x!2+1" "2+j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "sigma_stp_sect" )"2" "a!1" "b!1" "f!1" "x!1" )"2" assert )"2" "P!1" )"2" expand "sigma" "2" "j!1" )"2" assert )"2" assert )"2" " sigma(0, j!1, LAMBDA (ii: nat):IF ii > 1 + j!1 THEN 0LAMBDA (ii: nat):IF ii >= 1 + j!1 THEN 0") "1" "1" replace "1" expand "stp_sect" )"1" "j!1+1" )"1" "1" "x!1" )"1" "(seq(P!1)(1 + j!1) + seq(P!1)(2 + j!1)) / 2" )"1" assert )nil nil )"2" "2" "connected_domain" )"2" "2" "seq(P!1)(1+j!1)" "seq(P!1)(2+j!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq[nat]" )"1" "1" expand "restrict" )"1" nil nil ))nil ))nil )"2" "2" 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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil )"5" (skosimp*) nil nil ) ("6" (assert ) nil nil )"7" (skosimp*) (("7" (assert ) nil nil )) nil )"8" (skosimp*) (("8" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"real" sigma "reals/" )nil integral_def nil )nil sigma "reals/" )"[T -> real]" sigma "reals/" )nil sigma "reals/" )nil integral_def nil ))nil 3281796457"" (induct "n" )"1" (skosimp*)"1" (expand "sumof" )"1" (expand "sigma" )"1" (lemma "integral_stp_sect" )"1" (inst?)"1" (rewrite "integral_def" - :dir rl)"1" (flatten)"1" (expand "stp_sect" )"1" (expand "sigma" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (skosimp*)"2" (expand "sumof" )"2" (expand "sigma" 1)"2" (lemma "integral_sum" )"2" "a!1" "b!1" "stp_sect(a!1, b!1, P!1, 1 + j!1, f!1)" "(LAMBDA (x: T): LAMBDA (ii: nat):IF ii > 1 + j!1 THEN 0") "2" (assert )"2" (hide 2)"2" (lemma "integral_stp_sect" )"2" (inst?)"2" (rewrite "integral_def" - :dir rl)"2" (flatten)"2" "(LAMBDA x: stp_sect(a!1, b!1, P!1, 1 + j!1, f!1)(x)) = stp_sect(a!1, b!1, P!1, 1 + j!1, f!1)" )"1" assert )"1" "1" "1" "1" "(LAMBDA x: sigma(0, j!1, LAMBDA (ii: nat):IF ii > 1 + j!1 THEN 0LAMBDA x: sigma(0, j!1,LAMBDA (ii: nat):IF ii > j!1 THEN 0") "1" (assert ) nil nil )"2" "2" "2" rewrite "sigma_restrict_eq[nat]" )"2" "2" expand "restrict" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "stp_sect" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integral_prep nil )"(total_order?[real])" nil )nil sigma "reals/" )"[T -> real]" sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )nil sigma "reals/" )IF const-decl "[boolean, T, T -> T]" if_def nil )"posint" nil )"real" sigma "reals/" )"(strict_total_order?[real])" real_props nil )"real" reals nil )"posint" nil )"odd_int" integers nil )"real" reals nil )nil integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )"real" integral_step nil )nil integral_step nil )nil naturalnumbers nil )"real" integral_step nil )"real" integral_step nil )nil integral_step nil )nil naturalnumbers nil )"bool" integral_def nil )"[bool, bool -> bool]" booleans nil )nil integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers 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 nat_types nil )"bool" reals nil )nil integral_step nil )"[real -> boolean]" integral_step nil )nil defined_types 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 )"int" integers nil ))nil 3281794545"" (skosimp*)"" (lemma "integrable_sumof" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )nil integral_step nil )"int" integers nil )"(total_order?[real])" nil )nil integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers 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 nat_types 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 integral_step nil )"[real -> boolean]" integral_step nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3281794546"" (skosimp*)"" (typepred "P!1" )"" (lemma "parts_order" )"" (inst - "a!1" "b!1" "P!1" "0" "n!1+1" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil ))nil )nil integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"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 ) (<= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integral_step nil )"[real -> boolean]" integral_step nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"partition[T](a!1, b!1)" integral_step nil )"{x: T | a!1 < x}" integral_step nil )"T" integral_step nil )"nat" integral_step nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"posint" nil )nil integral_def nil ))nil 3281794546"" (subtype-tcc) (("" (postpone) nil 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 )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"[real -> boolean]" integral_step nil )nil integral_step nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil nat_types 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 )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil integral_def nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil 3281794560 ("" (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 )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"[real -> boolean]" integral_step nil )nil integral_step nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil nat_types 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 )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil integral_def 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 integers nil ))nil 3281870156"" (induct "n" )"1" (skosimp*)"1" (assert )"1" (expand "sumof" )"1" (expand "sigma" )"1" (lemma "integral_stp_sect" )"1" (inst?)"1" (assert )"1" (rewrite "integral_def" - :dir rl)"1" (flatten)"1" (expand "stp_sect" )"1" (expand "sigma" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "sumof" )"2" (expand "sigma" 1)"2" (assert )"2" (lemma "integral_sum" )"2" "a!1" "b!1" "stp_sect(a!1, b!1, P!1, 1 + j!1, f!1)" "(LAMBDA (x: T): LAMBDA (ii: nat):IF ii > 1 + j!1 THEN 0") "2" (assert )"2" (split -1)"1" (flatten)"1" (hide -1)"1" (replace -1)"1" "(LAMBDA x: sigma(0, j!1, LAMBDA (ii: nat):IF ii > 1 + j!1 THEN 0LAMBDA x: sigma(0, j!1,LAMBDA (ii: nat):IF ii > j!1 THEN 0") "1" (hide -1 -2)"1" "1" assert )"1" replace -1)"1" "1" "integral_stp_sect" )"1" "1" rewrite "integral_def" "1" "1" replace -2)"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "2" rewrite "sigma_restrict_eq[nat]" )"2" "2" expand "restrict" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" (lemma "integral_stp_sect" )"2" (inst?)"2" (rewrite "integral_def" - :dir rl)"2" (flatten) nil nil )) nil ))nil ))nil ))nil )"3" (hide -1 2)"3" (lemma "integrable_sumof" )"3" (expand "sumof" )"3" (inst - "f!1" "j!1" "a!1" "b!1" "P!1" )"3" (assert )"3" "(LAMBDA x: sigma(0, j!1, LAMBDA (ii: nat):IF ii > 1 + j!1 THEN 0LAMBDA x: sigma(0, j!1,LAMBDA (ii: nat):IF ii > j!1 THEN 0") "3" "3" "3" rewrite "sigma_restrict_eq[nat]" )"3" "3" expand "restrict" )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil )"5" (skosimp*)"5" (assert )"5" (hide 2)"5" (lemma "integrable_sumof" )"5" (inst?) (("5" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil integral_prep nil )nil integral_step nil )nil sigma "reals/" )"[T -> real]" sigma "reals/" )IF const-decl "[boolean, T, T -> T]" if_def nil )"posint" nil )nil integral_step nil )"real" reals nil )"odd_int" integers nil )nil sigma_below "reals/" )nil integral_def nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil naturalnumbers nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil finite_sequences nil )"real" integral_step nil )"[numfield, numfield -> numfield]" number_fields nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"{S: real | integral?(a, b, ff, S)}" nil )"bool" integral_def nil )nil defined_types nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans 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 )"[real -> boolean]" integral_step nil )nil integral_step nil )"bool" reals nil )nil nat_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil intervals_real "reals/" )nil finite_sequences nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil integral_def nil )"[bool, bool -> bool]" booleans nil )"bool" integral_def nil )nil naturalnumbers nil )nil integral_step nil )"real" integral_step nil )"real" integral_step nil )"int" integers nil )"posint" nil )"real" reals nil ))nil )nil 3281795059"" (induct "n" )"1" (skosimp*)"1" (assert )"1" (expand "sumof" )"1" (expand "sigma" )"1" (lemma "integral_stp_sect" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "sumof" )"2" (expand "sigma" 1)"2" (assert )"2" (lemma "integral_sum" )"2" "a!1" "seq(P!1)(2 + j!1)" "stp_sect(a!1, b!1, P!1, 1 + j!1, f!1)" "(LAMBDA (x: T): LAMBDA (ii: nat):IF ii > 1 + j!1 THEN 0") "1" (lemma "parts_order[T]" )"1" (inst - "a!1" "b!1" "P!1" "0" "2+j!1" )"1" (assert )"1" (rewrite "integral_def" :dir rl)"1" "(LAMBDA x: sigma(0, j!1, LAMBDA (ii: nat):IF ii > 1 + j!1 THEN 0LAMBDA x: sigma(0, j!1,LAMBDA (ii: nat):IF ii > j!1 THEN 0") "1" (prop)"1" (replace -2)"1" "1" " integral(a!1, seq(P!1)(2 + j!1), LAMBDA (x: T):LAMBDA (ii: nat):IF ii > j!1 THEN 0LAMBDA (x: T):LAMBDA (ii: nat):IF ii > j!1 THEN 0") "1" "1" "1" assert )"1" rewrite "integral_def" "1" "1" "1" replace -2)"1" "1" "integral_stp_sect" )"1" "1" "seq(P!1)(2 + j!1)" )"1" assert )"1" rewrite "integral_def" "1" "1" assert )"1" expand "stp_sect" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "parts_order[T]" )"2" "a!1" "b!1" "P!1" "0" "1+j!1" )"2" assert )nil nil ))nil ))nil ))nil )"3" "3" (assert ) nil nil ))nil )"4" "4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "integral_restrict_eq" )"2" (postpone) nil nil ))nil ))nil ))nil )"3" (postpone) nil nil )"4" (postpone) nil nil )"5" (postpone) nil nil )"6" (postpone) nil nil ))nil ))nil ))nil )"2" (postpone) nil nil )"3" (postpone) nil nil )"4" (postpone) nil nil )"5" (postpone) nil nil ))nil )"2" (hide 2)"2" (apply-extensionality 1 :hide? t)"1" rewrite "sigma_restrict_eq[nat]" )"1" "1" expand "restrict" )"1" (propax) nil nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil )"5" (skosimp*) (("5" (assert ) (("5" (postpone) nil nil )) nil ))nil )"6" (skosimp*) (("6" (assert ) nil nil )) nil ))nil )nil shostak))nil 3281876432 ("" (subtype-tcc) nil nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil nat_types 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 )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil integral_def nil )"posint" nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil integral_step nil )"[real -> boolean]" integral_step nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" step_fun_def nil ))nil 3281872825"" (auto-rewrite "sigma_0_m1" )"" (induct "n" )"1" (skosimp*) (("1" (inst?) (("1" (assert ) nil nil )) nil ))nil )"2" (skosimp*)"2" (expand "sumof" )"2" (assert )"2" (lift-if)"2" (expand "sigma" )"2" (ground)"2" (expand "stp_sect" )"2" (lift-if)"2" (ground)"2" (expand "val_in" )"2" (assert )"2" (expand "step_function_on?" )"2" "0" )"2" "2" "x!1" )"2" "pick(a!1, b!1, P!1, 0)" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (expand "sumof" )"3" (lift-if)"3" (ground)"3" (expand "sigma" 2)"3" (inst?)"3" (assert )"3" (typepred "x!1" )"3" (case "x!1 <= seq(P!1)(1 + j!1)" )"1" (inst?)"1" (lift-if)"1" (assert )"1" "1" " sigma(0, j!1, LAMBDA (ii: nat):IF ii > 1 + j!1 THEN 0") "1" assert )"1" expand "stp_sect" )"1" (propax) nil nil ))nil ))nil )"2" "2" "sigma(0, j!1, LAMBDA (ii: nat):IF ii > 1 + j!1 THEN 0LAMBDA (ii: nat): 0)") "1" "sigma_const[nat]" )"1" "1" (assert ) nil nil ))nil ))nil )"2" assert )"2" "2" rewrite "sigma_restrict_eq[nat]" )"2" "2" expand "restrict" )"2" "2" "2" "2" expand "stp_sect" )"2" "2" "1" "parts_order" )"1" "a!1" "b!1" "P!1" "x!2" "j!1+1" )"1" assert )nil nil ))nil ))nil )"2" expand "val_in" )"2" case "x!2 = 1 + j!1" )"1" assert )nil nil )"2" assert )"2" "parts_order" )"2" "a!1" "b!1" "P!1" "x!2+1" "j!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 )"2" " sigma(0, j!1, LAMBDA (ii: nat):IF ii > 1 + j!1 THEN 0LAMBDA (ii: nat):IF ii > j!1 THEN 0") "1" "1" replace -1)"1" "1" expand "stp_sect" )"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq[nat]" )"2" "2" expand "restrict" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (hide -4)"2" (lemma "sigma_stp_sect" )"2" "a!1" "b!1" "f!1" "x!1" )"2" assert )"2" "P!1" "j!1" )"2" assert )"2" assert )"2" "sigma(0, j!1, LAMBDA (ii: nat):IF ii >= 1 + j!1 THEN 0LAMBDA (ii: nat):IF ii > 1 + j!1 THEN 0") "1" assert )"1" replace -2)"1" "1" expand "step_function_on?" )"1" "j!1+1" )"1" "1" "x!1" )"1" "pick(a!1, b!1, P!1, 1+j!1)" )"1" expand "stp_sect" )"1" expand "val_in" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq[nat]" )"2" "2" expand "restrict" )"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 )"4" (hide 2) (("4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil )"posint" nil )"int" integers nil )"bool" step_fun_def nil )"[bool, bool -> bool]" booleans nil )nil integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers 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 nat_types nil )"bool" reals nil )nil integral_step nil )"[real -> boolean]" integral_step 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 )nil defined_types nil )nil naturalnumbers nil )nil integral_step nil )"real" integral_step nil )"real" integral_step nil )nil naturalnumbers nil )"(total_order?[real])" nil )nil integral_step nil )"real" reals nil )"real" integral_step nil )"{t: T | seq(P)(j) < t AND t < seq(P)(j + 1)}" nil )nil intervals_real "reals/" )"(strict_total_order?[real])" real_props nil )"real" sigma "reals/" )"posint" nil )NOT const-decl "[bool -> bool]" booleans nil )nil integral_step nil )"T" integral_step nil )"{x: T | a!1 < x}" integral_step nil )"partition[T](a!1, b!1)" integral_step nil )"nat" integral_step nil )"closed_interval[T](a!1, seq(P!1)(2 + j!1))" nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"(total_order?[real])" nil )"int" integers nil )nil sigma "reals/" )"(strict_total_order?[real])" real_props nil )nil integral_def nil )"[T -> real]" sigma "reals/" )nil sigma "reals/" ))nil 3281872417"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"int" integers nil ))nil 3281872574"" (skosimp*)"" (lemma "step_fun_is_sumof_n" )"" (inst?)"" (assert )"" (inst - "length(P!1)-2" )"" (assert )"" (inst - "x!1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil integral_step nil )"int" integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"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 nat_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integral_step nil )"[real -> boolean]" integral_step nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3261749327"" (skosimp*)"" (expand "step_function?" )"" (skosimp*)"" (lemma "step_fun_is_sumof" )"" (inst?)"" (inst - "a!1" "b!1" "P!1" )"" (assert )"" (split -1)"1" (lemma "integrable_sumof" )"1" (inst?)"1" (assert )"1" (lemma "integral_restr_eq" )"1" "a!1" "b!1" " sumof(length(P!1) - 2, LAMBDA (jj: upto(length(P!1) - 2)):" " f!1") "1" (assert )"1" "1" "1" "1" (assert ) nil nil ))nil ))nil )"2" "2" "2" "integral_chg_one_pt" )"2" "a!1" "b!1" "sumof(length(P!1) - 2, LAMBDA (jj: upto(length(P!1) - 2)):" "f!1(b!1)" )"2" assert )"2" "b!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "step_function_on?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" step_fun_def nil )nil integral_step nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil integral_prep nil )nil integral_prep nil )"T" integral_step nil )"T" integral_step nil )"T" integral_step nil )nil naturalnumbers nil )nil integral_step nil )"real" integral_step nil )"real" integral_step nil )"(total_order?[real])" nil )nil integral_step nil )nil integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"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 nat_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integral_step nil )"[real -> boolean]" integral_step nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil )nil 3261494969"" (skosimp*)"" (lemma "step_fun_is_sumof" )"" (inst?)"" (assert )"" (skosimp*)"" (replace -2 * rl)"" (hide -2)"" (lemma "sum_zero_excepts_integrable" )"" (inst?)"" (inst -1 "n!1" )"" (assert )"" (inst?) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak))nil 3281794562"" (skosimp*)"" (lemma "step_function_integrable?" )"" (inst?)"" (assert )"" (expand "step_function?" ) (("" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )nil integral_step nil )"(strict_total_order?[real])" real_props 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 nat_types nil )nil naturalnumbers nil )"bool" step_fun_def nil )nil integral_step nil )"[real -> boolean]" integral_step nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3281794594"" (subtype-tcc) nil nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"posint" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props 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 integral_step nil )"[real -> boolean]" integral_step nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" step_fun_def nil ))nil 3281794594"" (subtype-tcc) nil nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"posint" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props 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 integral_step nil )"[real -> boolean]" integral_step nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" step_fun_def nil ))nil 3281794594"" (subtype-tcc) nil nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"posint" nil )"int" integers 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 integral_step nil )"[real -> boolean]" integral_step nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" step_fun_def nil ))nil 3281794594"" (subtype-tcc) nil nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"posint" nil )"real" reals nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props 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 integral_step nil )"[real -> boolean]" integral_step nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" step_fun_def nil ))nil 3281794594"" (subtype-tcc) nil nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props 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 integral_step nil )"[real -> boolean]" integral_step nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" step_fun_def nil ))nil 3281794594"" (assuming-tcc) nil nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"posint" nil )nil integers 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 integral_step nil )"[real -> boolean]" integral_step nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" step_fun_def nil ))nil 3281871787"" (skosimp*)"" (assert )"" (lemma "step_fun_is_sumof" )"" (inst - "f!1" "a!1" "b!1" "P!1" )"" (assert )"" (lemma "integral_sumof" )"" (inst?)"" (assert )"" (replace -1 * rl)"" (hide -1)"" (lemma "integral_chg_one_pt" )"" "a!1" "b!1" "sumof(length(P!1) - 2, LAMBDA (jj: upto(length(P!1) - 2)):" "f!1(b!1)" )"" (assert )"" (inst - "b!1" )"" assert )"" "integrable_sumof" )"" "" assert )"" "" replace -3)"" "" "integral_restr_eq" )"" "a!1" "b!1" " sumof(length(P!1) - 2, LAMBDA (jj: upto(length(P!1) - 2)):" "f!1" )"" assert )"" "" "" assert )"" "" 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 booleans nil )nil booleans nil )AND const-decl "[bool, 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )nil nat_types nil )"[real -> boolean]" integral_step nil )nil integral_step nil )"bool" reals nil )nil intervals_real "reals/" )nil finite_sequences nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil integral_def nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil integral_step nil )"real" integral_step nil )"real" integral_step nil )nil integral_step nil )nil naturalnumbers nil )nil integral_step nil )nil integral_prep nil )nil integral_prep nil )nil integral_step nil ))nil 3278425755"" (skosimp*)"" (lemma "integrable_lem" )"" (inst?)"" (assert )"" (skosimp*)"" (inst - "epsi!1/3" )"" (skosimp*)"" (lemma "step_function_integrable?" )"" (inst-cp -1 "a!1" "b!1" "f2!1" )"" (inst -1 "a!1" "b!1" "f1!1" )"" (assert )"" (expand "integrable?" -)"" (skosimp*)"" case "integral(a!1, b!1, f1!1) = S!1" )"1" case "integral(a!1, b!1, f2!1) = S!2" )"1" expand "integral?" )"1" "epsi!1/3" )"1" "epsi!1/3" )"1" "1" "DEL" "IF delta!1 <= delta!2 THEN delta!1 ELSE delta!2 ENDIF" )"1" case "FORALL (P: partition[T](a!1, b!1), xis: (xis?(a!1,b!1,P))): width(a!1, b!1, P) < DEL IMPLIES S!1-epsi!1/3 < Rie_sum(a!1, b!1, P, xis, f!1) AND Rie_sum(a!1, b!1, P, xis, f!1) < S!2+epsi!1/3" )"1" "DEL" )"1" "1" "RS1!1" )"1" expand "Riemann_sum?" )"1" "1" replace -1)"1" "1" "RS2!1" )"1" expand "Riemann_sum?" )"1" "1" replace "1" "1" "P1!1" "xis!1" )"1" "P2!1" "xis!2" )"1" assert )"1" "integral_diff" )"1" "a!1" "b!1" "f2!1" "f1!1" )"1" assert )"1" "1" "(LAMBDA x: f2!1(x) - f1!1(x)) = f2!1 - f1!1" )"1" "1" replace "1" "1" "1" "Rie_sum(a!1, b!1, P1!1, xis!1, f!1)" )"1" "Rie_sum(a!1, b!1, P2!1, xis!2, f!1)" )"1" replace "1" "1" replace "1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "-" )"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" "2" "2" "P!1" )"2" "P!1" )"2" assert )"2" "1" "1" "Rie_sum(a!1, b!1, P!1, xis!1, f2!1)" )"1" "Rie_sum(a!1, b!1, P!1, xis!1, f1!1)" )"1" "1" "1" case "Rie_sum(a!1, b!1, P!1, xis!1, f1!1) <= Rie_sum(a!1, b!1, P!1, xis!1, f!1)" )"1" case "Rie_sum(a!1, b!1, P!1, xis!1, f!1) <= Rie_sum(a!1, b!1, P!1, xis!1, f2!1)" )"1" "1" "1" "Rie_sum" )nil nil ))nil ))nil )"2" "2" expand "Rie_sum" )"2" assert )"2" "sigma[below(length(P!1)-1)].sigma_le" )"1" "1" assert )"1" "1" "1" "1" "1" "DD" "(seq(P!1)(n!1+1) - seq(P!1)(n!1))" )"1" replace "1" "1" "1" "DD" )"1" "xis!1" )"1" assert )"1" "1" "parts_order" )"1" "a!1" "b!1" "P!1" "n!1" "n!1+1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "xis!1" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Rie_sum" )"2" assert )"2" "2" "sigma[below(length(P!1)-1)].sigma_le" )"1" "1" assert )"1" "1" "1" "1" "1" "DD" "(seq(P!1)(n!1+1) - seq(P!1)(n!1))" )"1" replace "1" "1" "1" "DD" )"1" "xis!1" )"1" assert )"1" "1" "parts_order" )"1" "a!1" "b!1" "P!1" "n!1" "n!1+1" )"1" assert )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 ))nil ))nil ))nil ))nil )"2" "2" "Riemann?_Rie" )"2" "a!1" "b!1" "f1!1" )"2" "1" assert )"1" "P!1" "xis!1" )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "Riemann?_Rie" )"2" "a!1" "b!1" "f2!1" )"2" "1" "P!1" "xis!1" )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "width" )nil nil ))nil ))nil )"2" "2" "width" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "integral_def" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "integral_def" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integral_step nil )"[real -> boolean]" integral_step 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_prep nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )nil booleans 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 )nil integral_step nil )"bool" integral_def nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )"bool" integral_def nil )"{S: real | integral?(a, b, ff, S)}" nil )nil integral_def nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil )"[T -> real]" integral_step nil )"real" integral_step nil )"real" reals nil )"real" reals nil )nil sigma "reals/" )nil integers nil )nil integral_def nil )"real" integral_step nil )nil extra_real_propsnil )"int" integers nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )nil sigma "reals/" )"posint" nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(strict_total_order?[real])" real_props nil )nil integral_def nil )"(xis?(a!1, b!1, P!1))" integral_step nil )"[T -> real]" integral_step nil )"partition[T](a!1, b!1)" integral_step nil )"T" integral_step nil )"T" integral_step nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" integral_def nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[T -> real]" real_fun_ops "reals/" )nil integral_prep nil )"odd_int" integers nil )"int" integers nil )"real" reals nil )nil naturalnumbers nil )nil nat_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil intervals_real "reals/" )nil finite_sequences nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil integral_def nil )"bool" integral_def nil )"[bool, bool -> bool]" booleans nil )"posreal" integral_def nil )"real" integral_def nil ))nil )nil 3262523207"" (skosimp*)"" (lemma "integrable_lem" )"" (inst?)"" (assert )"" (skosimp*)"" (inst - "epsi!1/3" )"" (skosimp*)"" (lemma "step_function_integrable?" )"" (inst-cp -1 "a!1" "b!1" "f2!1" )"" (inst -1 "a!1" "b!1" "f1!1" )"" (assert )"" (expand "integrable?" -)"" (skosimp*)"" case "integral(a!1, b!1, f1!1) = S!1" )"1" case "integral(a!1, b!1, f2!1) = S!2" )"1" expand "is_integral" )"1" "epsi!1/3" )"1" "epsi!1/3" )"1" "1" "DEL" "IF delta!1 <= delta!2 THEN delta!1 ELSE delta!2 ENDIF" )"1" case "FORALL (P: partition[T](a!1, b!1)): width(a!1, b!1, P) < DEL IMPLIES S!1-epsi!1/3 < Riemann_sum(a!1, b!1, P, f!1) AND Riemann_sum(a!1, b!1, P, f!1) < S!2+epsi!1/3" )"1" "DEL" )"1" "1" "P1!1" )"1" "P2!1" )"1" assert )"1" "integral_diff" )"1" "a!1" "b!1" "f2!1" "f1!1" )"1" assert )"1" "1" "(LAMBDA x: f2!1(x) - f1!1(x)) = f2!1 - f1!1" )"1" "1" replace "1" "1" "1" "Riemann_sum(a!1, b!1, P1!1, f!1)" )"1" "Riemann_sum(a!1, b!1, P2!1, f!1)" )"1" replace "1" "1" replace "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "-" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "P!1" )"2" "P!1" )"2" assert )"2" "1" "1" "1" "1" case "Riemann_sum(a!1, b!1, P!1, f1!1) <= Riemann_sum(a!1, b!1, P!1, f!1)" )"1" case "Riemann_sum(a!1, b!1, P!1, f!1) <= Riemann_sum(a!1, b!1, P!1, f2!1)" )"1" "1" "1" "Riemann_sum" )nil nil ))nil ))nil )"2" "2" expand "Riemann_sum" )"2" "sigma[upto(length(P!1)-1)].sigma_le" )"1" "1" assert )"1" "1" "1" "1" "1" "DD" "(seq(P!1)(n!1) - seq(P!1)(n!1-1))" )"1" replace "1" "1" "1" "DD" )nil nil ))nil )"2" "2" assert )"2" "parts_order" )"2" "a!1" "b!1" "P!1" "0" "n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" "parts_order" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "parts_order" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "parts_order" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "parts_order" )"2" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "Riemann_sum" )"2" "sigma[upto(length(P!1)-1)].sigma_le" )"1" "1" assert )"1" "1" "1" "1" "1" "DD" "(seq(P!1)(n!1) - seq(P!1)(n!1-1))" )"1" replace "1" "1" "1" "DD" )nil nil ))nil )"2" "2" "n!1 = 0" )"1" assert )nil nil )"2" "parts_order" )"2" "a!1" "b!1" "P!1" "0" "1" )"2" assert )"2" "parts_order" )"2" "a!1" "b!1" "P!1" "0" "n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" "P!1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "width" )nil nil ))nil ))nil )"2" "2" "width" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "integral_def" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "integral_def" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integral_prep nil )"bool" integral_def nil )"{S: real | integral?(a, b, ff, S)}" nil )nil integral_def nil )"{t: T | aa <= t AND t <= bb}" integral_def nil )nil integral_def nil )nil sigma "reals/" )"real" sigma "reals/" )nil integral_prep nil )nil integral_def nil )"posreal" integral_def nil ))nil )))
Messung V0.5 in Prozent C=100 H=98 G=98
¤ Dauer der Verarbeitung: 0.344 Sekunden
(vorverarbeitet am 2026-04-27)
¤ *© Formatika GbR, Deutschland
2026-05-26
