Quelle rs_integral_prep.prf
Sprache: Lisp
(rs_integral_prepnil 3494857844"" (lemma "connected_domain" ) (("" (propax) nil nil )) nil )nil rs_integral_prep nil )) nil ))nil 3494857844"" (lemma "not_one_element" ) (("" (propax) nil nil )) nil )nil rs_integral_prep nil )) nil ))nil 3253532115"" (skosimp*)"" (rewrite "integral_def" )"" (expand "integral?" )"" (skosimp*)"" (auto-rewrite "Rie_sum" )"" (inst + "1" )"" (skosimp*)"" (case-replace "R!1 = D!1*(g!1(b!1)-g!1(a!1))" )"1" (assert )"1" (expand "abs" ) (("1" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (typepred "R!1" )"2" (expand "Riemann_sum?" )"2" (skosimp*)"2" (replace -1)"2" (hide -1)"2" assert )"2" expand "const_fun" )"2" case "FORALL (n: below(length(P!1))): n > 0 IMPLIES sigma[below(length(P!1) - 1)] (0, n-1, LAMBDA (n: below(length(P!1) - 1)): g!1(seq(P!1)(1 + n)) * D!1 - g!1(seq(P!1)(n)) * D!1) = D!1*g!1(seq(P!1)(n)) - D!1*g!1(seq(P!1)(0))" )"1" "length(P!1)-1" )"1" (assert ) nil nil ))nil )"2" "2" "n" "below_induction[length(P!1)]" )"1" (assert ) nil nil )"2" "2" assert )"2" "jb!1 = 0" )"1" "1" expand "sigma" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" expand "sigma" 2)"2" replace -2)"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" (assert ) nil nil ))nil )"4" "4" (assert ) nil nil ))nil ))nil ))nil )"3" "3" "3" (assert ) nil nil ))nil ))nil )"4" "4" "4" (assert ) 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 rs_integral_def nil )"[T -> real]" real_fun_ops "reals/" )nil number_fields nil )"[numfield, numfield -> numfield]" 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]" rs_integral_prep nil )nil rs_integral_prep nil )"real" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )nil naturalnumbers nil )nil fseqs "structures/" )nil fseqs "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )"R" restrict nil )"bool" reals nil )"bool" sort_fseq "structures/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil rs_partition nil )"bool" rs_integral_def nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"odd_int" integers nil )"real" reals nil )"odd_int" integers nil )"posint" nil )nil sigma_below "reals/" )nil bounded_nat_inductions nil )nil defined_types nil )"partition[T](a!1, b!1)" rs_integral_prepnil )"T" rs_integral_prep nil )"T" rs_integral_prep nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"posint" nil )"real" rs_integral_def nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"bool" rs_integral_def nil ))nil ))nil 3278176127"" (skosimp*)"" (lemma "integral_const_fun" )"" (inst?)"" (assert )"" (flatten)"" (typepred "integral(a!1, b!1,g!1, const_fun(D!1))" )"" (expand "integral?" )"" (skosimp*)"" (inst -1 "epsi!1" )"" (skosimp*)"" (inst + "delta!1" )"" (skosimp*)"" (inst?)"" (assert )"" replace -3)"" "R!1" )"" "R!1" )"1" (assert ) nil nil )"2" "2" expand "Riemann_sum?" )"2" "Rie_sum" )"2" "2" assert )"2" "xis!1" )"2" replace -1)"2" "2" assert )"2" expand "const_fun" )"2" rewrite "sigma_restrict_eq[below(length(P!1) - 1)]" )"1" "1" expand "restrict" )"1" "1" "1" assert )nil nil )"2" "xis!1" )"2" "x!1" )"2" "P!1" )"2" "x!1" )"2" "x!1+1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil rs_integral_prep nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"{S: real | integral?(a, b, gg, ff, S)}" nil )"bool" rs_integral_def nil )"[T -> real]" real_fun_ops "reals/" )"bool" rs_integral_def nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )"bool" rs_integral_def nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" rs_integral_def nil )nil integers nil )"[bool, bool -> bool]" booleans nil )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"posint" nil )"[T -> real]" sigma "reals/" )"xis?[T](a!1, b!1, P!1)" rs_integral_prepnil )"below(length(P!1) - 1)" rs_integral_prepnil )nil intervals_real "reals/" )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil rs_integral_def nil )"int" integers nil )"(Riemann_sum?(a!1, b!1, P!1, g!1, f!1))" nil )"[T -> real]" rs_integral_prep nil )"real" rs_integral_prep nil )"[T -> real]" rs_integral_prep nil )"partition[T](a!1, b!1)" rs_integral_prepnil )"T" rs_integral_prep nil )"T" rs_integral_prep nil )"odd_int" integers nil )nil rs_partition nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil rs_integral_prep nil )"[real -> boolean]" rs_integral_prep nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil )nil 3277741047"" (skosimp*)"" (lemma "integral_const_fun" )"" (inst?)"" (assert )"" (flatten)"" (typepred "integral(a!1, b!1, const_fun[T](D!1))" )"1" (expand "integral?" )"1" (skosimp*)"1" (inst -1 "epsi!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (inst?)"1" (assert )"1" replace -3)"1" "R!1" )"1" "R!1" )"1" (assert ) nil nil )"2" "2" expand "Riemann_sum?" )"2" "2" assert )"2" "xis!1" )"2" replace -1)"2" "2" assert )"2" expand "const_fun" )"2" rewrite "sigma_restrict_eq[below(length(P!1) - 1)]" )"1" "1" expand "restrict" )"1" "1" "1" assert )nil nil )"2" "2" "P!1" )"2" "xis!1" )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "xis!1" )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "xis!1" )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" sigma "reals/" )nil sigma "reals/" ))nil )nil 3253532115"" (skosimp*)"" (lemma "integral_const_fun" )"" (inst?)"" (assert )"" (flatten)"" (typepred "integral(a!1, b!1, const_fun[T](D!1))" )"1" (expand "is_integral" )"1" (skosimp*)"1" (inst -1 "epsi!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (inst?)"1" (assert )"1" replace -3)"1" "1" "Riemann_sum(a!1, b!1, P!1, f!1) = Riemann_sum(a!1, b!1, P!1, const_fun[T](D!1))" )"1" (assert ) nil nil )"2" "2" expand "Riemann_sum" )"2" rewrite "sigma_restrict_eq" )"1" "1" expand "restrict" )"1" "1" "1" "1" expand "const_fun" )"1" "1" replace -3)"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "P!1" )"2" "i!1-1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" "P!1" )"2" "n!1-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" (assert ) nil nil ))nil ))nil )"4" "4" "4" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T -> real]" real_fun_ops "reals/" )nil sigma "reals/" )"[T -> real]" sigma "reals/" ))nil ))nil 3280253820"" (skosimp*)"" (case-replace "D!1 = 0" )"1" (assert )"1" (expand "*" )"1" (lemma "integral_const_fun" )"1" (inst - "0" "a!1" "b!1" "g!1" )"1" (expand "const_fun" )"1" (flatten) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"2" (rewrite "integral_def" )"2" (typepred "integral(a!1, b!1, g!1,f!1)" )"2" (expand "integral?" )"2" (skosimp*)"2" (inst -1 "epsi!1/abs(D!1)" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (inst?)"1" (assert )"1" (typepred "R!1" )"1" (expand "Riemann_sum?" )"1" "Rie_sum" )"1" assert )"1" "1" replace -1)"1" "1" "Rie_sum(a!1, b!1,g!1, P!1, xis!1, D!1 * f!1) = D!1*Rie_sum(a!1, b!1, g!1,P!1, xis!1, f!1)" )"1" expand "Rie_sum" )"1" assert )"1" replace -1)"1" "1" "sigma[below(length(P!1) - 1)] LAMBDA (n: below(length(P!1) - 1)):") "1" "1" assert )"1" "1" "1" rewrite "abs_mult " "1" assert )nil nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "abs" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "Rie_sum" )"2" assert )"2" "sigma_scal[below(length(P!1) - 1)]" )"1" "1" assert )"1" expand "*" )"1" nil nil ))nil ))nil ))nil )"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 )"2" (case "epsi!1 / abs(D!1) > 0" )"1" (assert ) nil nil )"2" (hide-all-but (1 3))"2" (cross-mult 1) (("2" (assert ) nil nil )) nil ))nil )"3" (lemma "abs_eq_0" )"3" (inst?) (("3" (assert ) nil nil )) nil )) nil ))nil )"3" (lemma "abs_eq_0" )"3" (inst?) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 )"[T -> real]" real_fun_ops "reals/" )nil rs_integral_prep nil )"[real -> boolean]" rs_integral_prep nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )nil rs_integral_prep nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil extra_real_props nil )nil abs_lems "reals/" )nil abs_lems "reals/" )"int" integers nil )"real" rs_integral_def nil )nil rs_integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"real" reals nil )"int" integers nil )nil extra_real_props nil )nil reals nil )nil real_props nil )"nnreal" nil )"xis?[T](a!1, b!1, P!1)" rs_integral_prepnil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"[T -> real]" rs_integral_prep nil )"[T -> real]" rs_integral_prep nil )"[bool, bool -> bool]" booleans nil )nil integers nil )"partition[T](a!1, b!1)" rs_integral_prepnil )"T" rs_integral_prep nil )"T" rs_integral_prep nil )"posint" nil )nil sigma "reals/" )"bool" rs_integral_def nil )nil naturalnumbers nil )nil fseqs "structures/" )nil fseqs "structures/" )"[numfield, numfield -> numfield]" number_fields nil )"R" restrict nil )"bool" reals nil )"bool" sort_fseq "structures/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil rs_partition nil )"posreal" rs_integral_prep nil )nil real_types nil )"bool" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"real" rs_integral_prep nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )"boolean" notequal nil )"nzreal" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"{S: real | integral?(a, b, gg, ff, S)}" nil )"bool" rs_integral_def nil )"bool" rs_integral_def nil )"bool" reals nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil rs_integral_def nil ))nil )nil 3278176311"" (skosimp*)"" (case-replace "D!1 = 0" )"1" (assert )"1" (expand "*" )"1" (lemma "integral_const_fun" )"1" (inst - "0" "a!1" "b!1" )"1" (expand "const_fun" )"1" (flatten) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"2" (rewrite "integral_def" )"2" (typepred "integral(a!1, b!1, f!1)" )"1" (expand "integral?" )"1" (skosimp*)"1" (inst -1 "epsi!1/abs(D!1)" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (inst?)"1" (assert )"1" (typepred "R!1" )"1" (expand "Riemann_sum?" )"1" "Rie_sum" )"1" assert )"1" "1" replace -1)"1" "1" "Rie_sum(a!1, b!1, P!1, xis!1, D!1 * f!1) = D!1*Rie_sum(a!1, b!1, P!1, xis!1, f!1)" )"1" expand "Rie_sum" )"1" assert )"1" replace -1)"1" "1" "sigma[below(length(P!1) - 1)] LAMBDA (n: below(length(P!1) - 1)):") "1" "1" assert )"1" "1" "1" rewrite "abs_mult " "1" assert )nil nil )"2" "2" "2" assert )nil nil ))nil ))nil )"3" "3" assert )"3" "xis!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "abs" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )"3" "xis!1" )"3" assert )nil nil ))nil ))nil ))nil )"4" "4" expand "abs" )"4" "4" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "Riemann_sum?" )"2" assert )"2" "xis!1" )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )"4" "xis!1" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "Rie_sum" )"2" assert )"2" "sigma_scal[below(length(P!1) - 1)]" )"1" "1" assert )"1" expand "*" )"1" assert )nil nil ))nil ))nil )"2" "2" "2" assert )"2" "xis!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"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" (hide 3)"2" (assert )"2" (case "epsi!1 / abs(D!1) > 0" )"1" (assert ) nil nil )"2" (hide 2)"2" (hide -2)"2" (cross-mult 1)"1" (grind) nil nil )"2" (assert )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2) (("3" (grind) nil nil )) nil ))nil ))nil ))nil )"3" (hide -2 3) (("3" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (propax) nil nil ) ("3" (propax) nil nil ))nil ))nil ))nil ))nil )"[T -> real]" real_fun_ops "reals/" )"real" sigma "reals/" )nil sigma "reals/" ))nil )nil 3253532115"" (skosimp*)"" (case-replace "D!1 = 0" )"1" (assert )"1" (expand "*" )"1" (lemma "integral_const_fun" )"1" (inst - "0" "a!1" "b!1" )"1" (expand "const_fun" )"1" (flatten) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"2" (rewrite "integral_def" )"2" (typepred "integral(a!1, b!1, f!1)" )"1" (expand "integral?" )"1" (skosimp*)"1" (inst -1 "epsi!1/abs(D!1)" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (inst?)"1" (assert )"1" (typepred "R!1" )"1" (expand "Riemann_sum?" )"1" assert )"1" "1" replace -1)"1" "1" "Rie_sum(a!1, b!1, P!1, xis!1, D!1 * f!1) = D!1*Rie_sum(a!1, b!1, P!1, xis!1, f!1)" )"1" expand "Rie_sum" )"1" assert )"1" replace -1)"1" "1" "sigma[below(length(P!1) - 1)] LAMBDA (n: below(length(P!1) - 1)):") "1" "1" assert )"1" "1" "1" rewrite "abs_mult " "1" assert )nil nil )"2" "2" "2" assert )nil nil ))nil ))nil )"3" "3" assert )"3" "xis!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )"3" "xis!1" )"3" assert )nil nil ))nil ))nil ))nil )"4" "4" expand "abs" )"4" "4" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "Riemann_sum?" )"2" assert )"2" "xis!1" )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )"4" "xis!1" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "Rie_sum" )"2" assert )"2" "sigma_scal[below(length(P!1) - 1)]" )"1" "1" assert )"1" expand "*" )"1" assert )nil nil ))nil ))nil )"2" "2" "2" assert )"2" "xis!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (assert )"2" (case "epsi!1 / abs(D!1) > 0" )"1" (assert ) nil nil )"2" (hide 2)"2" (hide -2)"2" (cross-mult 1)"1" (grind) nil nil )"2" (assert )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2) (("3" (grind) nil nil )) nil ))nil ))nil ))nil )"3" (hide -2 3) (("3" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (propax) nil nil ) ("3" (propax) nil nil ))nil ))nil ))nil ))nil )"[T -> real]" real_fun_ops "reals/" )nil sigma "reals/" )"real" sigma "reals/" ))nil ))nil 3488722885"" (skosimp*)"" (case-replace "D!1 = 0" )"1" (assert )"1" case "integral?(a!1, b!1, LAMBDA (x: T): 0 * g!1(x), f!1, 0)" )"1" (expand "integrable?" )"1" (split +)"1" (inst + "0" )"1" (assert )"1" (expand "*" ) (("1" (propax) nil nil )) nil ))nil ))nil )"2" (typepred "integral(a!1, b!1, 0 * g!1, f!1)" )"2" (lemma "integral_unique" )"2" "0" "integral(a!1, b!1, 0 * g!1, f!1)" "a!1" "b!1" "f!1" "0*g!1" )"2" (assert )"2" (expand "*" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "integral?" )"2" (skosimp*)"2" (inst + "1" )"2" (skosimp*)"2" (typepred "R!1" )"2" (expand "Riemann_sum?" )"2" (skosimp*)"2" case "Rie_sum(a!1, b!1, LAMBDA (x: T): 0 * g!1(x), P!1, xis!1, f!1) = 0" )"1" (lemma "abs_0" )"1" (assert ) nil nil )) nil )"2" (hide 2)"2" "2" expand "Rie_sum" )"2" "sigma_zero[below(P!1`length-1)]" )"1" "1" (assert ) nil nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "integral_def" )"2" (typepred "integral(a!1, b!1, g!1,f!1)" )"2" (expand "integral?" )"2" (skosimp*)"2" (inst -1 "epsi!1/abs(D!1)" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (inst?)"1" (assert )"1" (typepred "R!1" )"1" (expand "Riemann_sum?" )"1" "Rie_sum" )"1" assert )"1" "1" replace -1)"1" "1" "Rie_sum(a!1, b!1,g!1, P!1, xis!1, D!1 * f!1) = D!1*Rie_sum(a!1, b!1, g!1,P!1, xis!1, f!1)" )"1" expand "Rie_sum" )"1" assert )"1" "1" "sigma[below(P!1`length - 1)] LAMBDA (n: below(P!1`length - 1)):") "1" "1" assert )"1" "1" "1" "sigma_scal[below(P!1`length - 1)]" )"1" "1" "D!1" )"1" expand "*" )"1" assert )"1" replace "1" "abs_mult" )"1" "integral(a!1, b!1, g!1, f!1) - LAMBDA (n: below(P!1`length - 1)):" "D!1" )"1" assert )nil nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "2" expand "Riemann_sum?" )"2" "xis!1" )"2" expand "Rie_sum" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "Rie_sum" )"2" expand "*" )"2" "sigma_scal[below(P!1`length - 1)]" )"1" "LAMBDA (n: below(P!1`length - 1)): " "D!1" "P!1`length-2" "0" )"1" assert )nil nil ))nil )"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" (case "epsi!1/abs(D!1)>0" )"1" (assert ) nil nil )"2" (cross-mult 1) (("2" (assert ) nil nil )) nil )"3" (assert ) nil nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" rs_integral_def nil )"bool" reals nil )nil booleans nil )nil rs_integral_prep nil )"[real -> boolean]" rs_integral_prep nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )nil rs_integral_def nil )"{S: real | integral?(a, b, gg, ff, S)}" nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" rs_integral_def nil )"real" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"bool" rs_integral_def nil )nil rs_partition nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"nat" sigma_below "reals/" )"(total_order?[real])" nil )nil integers nil )"[bool, bool -> bool]" booleans nil )nil sigma "reals/" )nil abs_lems "reals/" )"{j: nonneg_int | j >= i}" nil )"(total_order?[real])" nil )nil abs_lems "reals/" )"real" rs_integral_def nil )nil rs_integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil extra_real_props nil )"posint" nil )"T" rs_integral_prep nil )"T" rs_integral_prep nil )"partition[T](a!1, b!1)" rs_integral_prepnil )"[T -> real]" rs_integral_prep nil )"[T -> real]" rs_integral_prep nil )"real" sigma "reals/" )"xis?[T](a!1, b!1, P!1)" rs_integral_prepnil )"nnreal" nil )nil real_props nil )nil sigma "reals/" )nil reals nil )nil extra_real_props nil )"posreal" rs_integral_prep nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"real" rs_integral_prep nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )"boolean" notequal nil )"nzreal" nil )"(strict_total_order?[real])" real_props nil )nil rs_integral_def nil ))nil ))nil 3253532115"" (skosimp*)"" (rewrite "integral_def" )"" (typepred "integral(a!1, b!1, g!1, f!1)" )"" (typepred "integral(a!1, b!1, g!1, h!1)" )"" (name-replace "I1" "integral(a!1, b!1, g!1, f!1)" )"" (name-replace "I2" "integral(a!1, b!1, g!1, h!1)" )"" (expand "integral?" )"" (skosimp*)"" (inst -1 "epsi!1/2" )"" (inst - "epsi!1/2" )"" (skosimp*)"" (inst + "min(delta!1,delta!2)" )"" (skosimp*)"" (inst - "P!1" )"" "P!1" )"" "1" "1" "1" "R!1" )"1" expand "Riemann_sum?" )"1" "1" replace -1)"1" "1" "Rie_sum(a!1, b!1, g!1, P!1, xis!1, LAMBDA x: f!1(x) + h!1(x)) = Rie_sum(a!1, b!1, g!1,P!1, xis!1, f!1) + Rie_sum(a!1, b!1, g!1,P!1, xis!1, h!1)" )"1" "1" "Rie_sum(a!1, b!1, g!1, P!1, xis!1, f!1)" )"1" "Rie_sum(a!1, b!1, g!1, P!1, xis!1, h!1)" )"1" "triangle" )"1" "I1 - Rie_sum(a!1, b!1,g!1, P!1, xis!1, f!1)" "I2 - Rie_sum(a!1, b!1, g!1,P!1, xis!1, h!1)" )"1" assert )nil nil ))nil ))nil )"2" "2" expand "Riemann_sum?" )"2" nil nil ))nil ))nil ))nil )"2" "2" expand "Riemann_sum?" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "Rie_sum" )"2" assert )"2" "sigma_sum[below(length(P!1) - 1)]" )"1" "1" assert )nil nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )nil rs_integral_def nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )"bool" rs_integral_def nil )"bool" rs_integral_def nil )"{S: real | integral?(a, b, gg, ff, S)}" 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]" rs_integral_prep nil )nil rs_integral_prep nil )"{z: posreal | z <= x AND z <= y}" real_defs nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil rs_partition nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )"int" integers nil )"real" rs_integral_def nil )nil rs_integral_def nil )"T" rs_integral_prep nil )"T" rs_integral_prep nil )"partition[T](a!1, b!1)" rs_integral_prepnil )"[T -> real]" rs_integral_prep nil )"[T -> real]" rs_integral_prep nil )"xis?[T](a!1, b!1, P!1)" rs_integral_prepnil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"[T -> real]" rs_integral_prep nil )"(strict_total_order?[real])" real_props nil )"posint" nil )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"[bool, bool -> bool]" booleans nil )nil sigma "reals/" )"real" reals nil )"bool" rs_integral_def 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 )"real" reals nil )"[T, T -> boolean]" equalities nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3488732672"" (skosimp*)"" (rewrite "integral_def" )"" (typepred "integral(a!1, b!1, g!1, f!1)" )"" (typepred "integral(a!1, b!1, h!1, f!1)" )"" (name-replace "I1" "integral(a!1, b!1, g!1, f!1)" )"" (name-replace "I2" "integral(a!1, b!1, h!1, f!1)" )"" (expand "integral?" )"" (skosimp*)"" (inst -1 "epsi!1/2" )"" (inst - "epsi!1/2" )"" (skosimp*)"" (inst + "min(delta!1,delta!2)" )"" (skosimp*)"" (inst - "P!1" )"" "P!1" )"" "1" "1" "1" "R!1" )"1" expand "Riemann_sum?" )"1" "1" replace -1)"1" "1" "Rie_sum(a!1, b!1, LAMBDA x: g!1(x) + h!1(x), P!1, xis!1, f!1) = Rie_sum(a!1, b!1, g!1,P!1, xis!1, f!1) + Rie_sum(a!1, b!1, h!1,P!1, xis!1, f!1)" )"1" "1" "Rie_sum(a!1, b!1, g!1, P!1, xis!1, f!1)" )"1" "Rie_sum(a!1, b!1, h!1, P!1, xis!1, f!1)" )"1" "triangle" )"1" "I1 - Rie_sum(a!1, b!1,g!1, P!1, xis!1, f!1)" "I2 - Rie_sum(a!1, b!1, h!1,P!1, xis!1, f!1)" )"1" assert )nil nil ))nil ))nil )"2" "2" expand "Riemann_sum?" )"2" nil nil ))nil ))nil ))nil )"2" "2" expand "Riemann_sum?" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "Rie_sum" )"2" assert )"2" "sigma_sum[below(length(P!1) - 1)]" )"1" "1" assert )nil nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )nil rs_integral_def nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )"bool" rs_integral_def nil )"bool" rs_integral_def nil )"{S: real | integral?(a, b, gg, ff, S)}" 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]" rs_integral_prep nil )nil rs_integral_prep nil )"{z: posreal | z <= x AND z <= y}" real_defs nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil rs_partition nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )"int" integers nil )"real" rs_integral_def nil )nil rs_integral_def nil )"T" rs_integral_prep nil )"T" rs_integral_prep nil )"partition[T](a!1, b!1)" rs_integral_prepnil )"[T -> real]" rs_integral_prep nil )"[T -> real]" rs_integral_prep nil )"xis?[T](a!1, b!1, P!1)" rs_integral_prepnil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"[T -> real]" rs_integral_prep nil )"(strict_total_order?[real])" real_props nil )"posint" nil )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"[bool, bool -> bool]" booleans nil )nil sigma "reals/" )"real" reals nil )"bool" rs_integral_def 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 )"real" reals nil )"[T, T -> boolean]" equalities nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3278177576"" (skosimp*)"" (lemma "integral_sum" )"" (inst?)"" (inst?)"" (assert )"" (lemma "integral_def" )"" (inst - "a!1" "b!1" "f!1" "g!1" "v1!1" )"" (assert )"" (lemma "integral_def" )"" (inst - "a!1" "b!1" "h!1" "g!1" "v2!1" )"" (assert )"" (flatten)"" (assert )"" (inst - "g!1" )"" assert )"" "" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil rs_integral_prep nil )nil rs_integral_def nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil rs_integral_prep nil )"[real -> boolean]" rs_integral_prep nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3489152310"" (skosimp*)"" (lemma "integral_sum_g" )"" (inst?)"" (inst?)"" (inst - "f!1" )"" (assert )"" (lemma "integral_def" )"" (inst - "a!1" "b!1" "f!1" "g!1" "v1!1" )"" (assert )"" (lemma "integral_def" )"" (inst - "a!1" "b!1" "f!1" "h!1" "v2!1" )"" (assert )"" (flatten)"" (assert )"" replace -2)"" replace -4)"" "" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil rs_integral_prep nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil rs_integral_def nil )nil rs_integral_prep nil )"[real -> boolean]" rs_integral_prep 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 3253532115"" (skosimp*)"" (lemma "integral_sum" )"" (inst -1 "a!1" "b!1" "f!1" "g!1" "-h!1" )"" (assert )"" (split -1)"1" (flatten)"1" (assert )"1" (expand "-" )"1" (assert )"1" (assert )"1" (replace -2)"1" (assert )"1" (lemma "integral_scal" )"1" (inst?)"1" assert )"1" "1" "(LAMBDA (x: T): -h!1(x)) = -1 * h!1" )"1" (assert ) nil nil )"2" "2" expand "*" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "integral_scal" )"2" (inst -1 "-1" "a!1" "b!1" "h!1" "g!1" )"2" (assert )"2" (flatten)"2" (assert )"2" (case-replace "-h!1 = -1*h!1" )"2" (apply-extensionality 1 :hide? t)"2" (expand "*" )"2" assert )"2" expand "-" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil rs_integral_prep nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"odd_int" integers nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"[numfield -> numfield]" number_fields nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )nil rs_integral_prep nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )nil rs_integral_prep nil )"[real -> boolean]" rs_integral_prep 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 3489152523"" (skosimp*)"" (lemma "integral_sum_g" )"" (inst -1 "a!1" "b!1" "f!1" "g!1" "-h!1" )"" (assert )"" (split -1)"1" (flatten)"1" (assert )"1" case "(LAMBDA x: (-h!1)(x) + g!1(x)) = (LAMBDA x: g!1(x) - h!1(x))" )"1" (assert )"1" (replace -1)"1" (lemma "integral_scal_g" )"1" (inst - "-1" "a!1" "b!1" "f!1" "h!1" )"1" (assert )"1" (flatten)"1" case "-1*h!1 = -h!1" )"1" (assert ) nil nil )"2" "2" expand "*" )"2" "2" expand "-" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (lemma "integral_scal_g" )"2" (inst - "-1" "a!1" "b!1" "f!1" "h!1" )"2" (assert )"2" (flatten)"2" (case "-1*h!1 = -h!1" )"1" (assert ) nil nil )"2" (hide-all-but 1)"2" (decompose-equality)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil rs_integral_prep nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"odd_int" integers nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )nil rs_integral_prep nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )nil rs_integral_prep nil )"[real -> boolean]" rs_integral_prep 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 3253532115"" (skosimp*)"" (typepred "integral(a!1, b!1,g!1, f!1)" )"" (expand "integral?" )"" case "FORALL (eps: posreal): integral(a!1, b!1, g!1, f!1) >= -eps" )"1" (hide -2 -3 -5)"1" (inst -1 "-integral(a!1, b!1, g!1, f!1)/2" )"1" (assert ) nil nil )"2" (prop)"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil )"2" (skosimp*)"2" (assert )"2" (inst -1 "eps!1" )"2" (skosimp*)"2" (lemma "axiom_of_archimedes" )"2" (inst -1 "(b!1-a!1)/delta!1+2" )"2" (skosimp*)"2" (name "NM" "real_defs.max(i!1,2)" )"2" (inst - "eq_partition(a!1,b!1,NM)" )"1" (split -3)"1" "Rie_sum(a!1, b!1, g!1, eq_partition(a!1, b!1, NM), gen_xis(a!1, b!1, eq_partition(a!1, b!1, NM)), f!1)" )"1" "II" "integral(a!1, b!1, g!1, f!1)" )"1" case "Rie_sum(a!1, b!1, g!1, eq_partition(a!1, b!1, NM), gen_xis(a!1,b!1,eq_partition(a!1, b!1, NM)), f!1) >= 0" )"1" expand "abs" )"1" "1" (ground) nil nil ))nil ))nil )"2" "2" "NN" "eq_partition(a!1, b!1, NM)" )"2" replace -1)"2" expand "Rie_sum" )"2" "sigma_nonneg[below(length(NN) - 1)]" )"1" assert )"1" "1" assert )"1" "1" "1" "1" "1" case "g!1(NN`seq(1 + i!2)) - g!1(NN`seq(i!2)) >= 0" )"1" "f!1(gen_xis(a!1, b!1, NN)`seq(i!2))" )"1" assert )nil nil ))nil )"2" "2" "NN" )"2" "i!2" )"2" assert )"2" expand "increasing?" )"2" assert )"2" "seq(NN)(i!2)" "seq(NN)(1+i!2)" )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "gen_xis(a!1, b!1, NN)" )"2" "i!2" )"2" "2" "NN" )"2" "i!2" )"2" "i!2+1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "Riemann?_Rie" )"2" "a!1" "b!1" "f!1" "g!1" )"2" "1" (inst?) nil nil )"2" (propax) nil nil ))nil ))nil ))nil )"3" expand "max" -1)"3" "3" (ground) nil nil ))nil ))nil ))nil )"2" rewrite "width_eq_part" )"2" "2" "b!1-a!1" )"2" "2" case "ba / delta!1 < i!1 - 1" )"1" "1" "delta!1" )"1" "NM-1" )"1" expand "max" )"1" "1" "1" replace -2 * rl)"1" "1" assert )"1" "i!1" )"1" "1" case "i!1-1 < 1" )"1" "delta!1" )"1" assert )nil nil ))nil )"2" assert )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" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{S: real | integral?(a, b, gg, ff, S)}" nil )"bool" rs_integral_def nil )"bool" rs_integral_def nil )"bool" reals nil )nil rs_integral_prep nil )"[real -> boolean]" rs_integral_prep 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 )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"nzreal" real_typesnil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(total_order?[real])" nil )"real" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"T" rs_integral_prep nil )"T" rs_integral_prep nil )"[T -> real]" rs_integral_prep nil )"[T -> real]" rs_integral_prep nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"{k: int | i <= k AND j <= k}" nil )"{s: rat | s >= q AND s >= r}" nil )"[T, T -> boolean]" equalities nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil rs_integral_def nil )"odd_int" integers nil )nil sigma "reals/" )"[bool, bool -> bool]" booleans nil )nil integers nil )"posint" nil )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )nil extra_real_propsnil )"bool" real_fun_preds "reals/" )nil intervals_real "reals/" )"below(length(NN) - 1)" rs_integral_prepnil )"partition[T](a!1, b!1)" rs_integral_prepnil )"int" integers nil )"(total_order?[real])" nil )"real" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"xis?(a, b, P)" rs_integral_def nil )"real" rs_integral_def nil )nil rs_integral_def nil )"bool" rs_integral_def nil )"[bool, bool -> bool]" booleans nil )"posreal" nil )nil reals nil )nil real_props nil )nil real_props nil )nil rs_partition nil )nil naturalnumbers nil )nil fseqs "structures/" )nil fseqs "structures/" )"R" restrict nil )"bool" sort_fseq "structures/" )nil naturalnumbers nil )nil rs_partition nil )nil integers nil )"partition(a, b)" rs_partition nil )"{k: int | i!1 <= k AND 2 <= k}" nil )"int" rs_integral_prep nil )nil real_props nil )"real" reals nil ))nil ))nil 3281700217"" (skosimp*)"" (lemma "integral_restrict_eq" )"" (inst?) (("" (assert ) (("" (ground) nil nil )) nil )) nil ))nil ))nil )nil rs_integral_prep nil )"[real -> boolean]" rs_integral_prep nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil rs_integral_def nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3494858073"" (skosimp*)"" (lemma "integral_const_fun" )"" (inst -1 "_" "a!1" "b!1" "g!1" )"" (lemma "integral_diff" )"" (inst -1 "a!1" "b!1" "_" "g!1" "_" )"" (lemma "integral_ge_0" )"" "a!1" "b!1" "(LAMBDA (t:T): M!1 - f!1(t))" "g!1" )"" (assert )"" case "integrable?(a!1, b!1, g!1,(LAMBDA (t: T): M!1 - f!1(t)))" )"1" (assert )"1" (inst -4 "M!1" )"1" (flatten)"1" (expand "const_fun" )"1" "(LAMBDA (x: T): M!1)" "f!1" )"1" assert )"1" "1" replace -5)"1" "1" replace -3)"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst -2 "(LAMBDA (x: T): M!1)" "f!1" )"2" (assert )"2" (inst -2 "M!1" )"2" (flatten)"2" (assert )"2" expand "const_fun" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil rs_integral_prep nil )nil rs_integral_prep nil )nil rs_integral_prep nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"continuous_fun" nil )"(total_order?[real])" nil )"odd_int" integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil intervals_real "reals/" )"[T -> real]" real_fun_ops "reals/" )"bool" rs_integral_def nil )"bool" reals nil )nil booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )nil rs_integral_prep nil )"[real -> boolean]" rs_integral_prep 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 3489155712"" (skosimp*)"" (lemma "integral_const_fun" )"" (inst -1 "_" "a!1" "b!1" "g!1" )"" (lemma "integral_diff" )"" (inst -1 "a!1" "b!1" "_" "g!1" "_" )"" (lemma "integral_ge_0" )"" "a!1" "b!1" "(LAMBDA (t:real): M!1 - f!1(t))" "g!1" )"" (assert )"" case "integrable?(a!1, b!1, g!1,(LAMBDA (t: real): M!1 - f!1(t)))" )"1" (assert )"1" (inst -4 "M!1" )"1" (flatten)"1" (expand "const_fun" )"1" "(LAMBDA (x: real): M!1)" "f!1" )"1" assert )"1" "1" replace -5)"1" "1" replace -3)"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst -2 "(LAMBDA (x: real): M!1)" "f!1" )"2" (assert )"2" (inst -2 "M!1" )"2" (flatten)"2" (assert )"2" expand "const_fun" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"continuous_fun" nil )nil intervals_real "reals/" )"[T -> real]" real_fun_ops "reals/" ))nil ))nil 3494858091"" (skosimp*)"" (lemma "integral_const_fun" )"" (inst -1 "_" "a!1" "b!1" "g!1" )"" (lemma "integral_diff" )"" (inst -1 "a!1" "b!1" "_" "g!1" "_" )"" (lemma "integral_ge_0" )"" "a!1" "b!1" "(LAMBDA (t:T): f!1(t) - m!1)" "g!1" )"" (assert )"" case "integrable?(a!1, b!1, g!1,(LAMBDA (t: T): f!1(t) - m!1))" )"1" (assert )"1" (inst -4 "m!1" )"1" (flatten)"1" (inst -3 "f!1" "const_fun(m!1)" )"1" (assert )"1" expand "const_fun" )"1" replace -5)"1" "1" "1" (assert ) nil nil )"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst -2 "f!1" "const_fun(m!1)" )"2" (assert )"2" (inst -3 "m!1" )"2" (expand "const_fun" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil rs_integral_prep nil )nil rs_integral_prep nil )nil rs_integral_prep nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"continuous_fun" nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil intervals_real "reals/" )"[T -> real]" real_fun_ops "reals/" )"bool" rs_integral_def nil )"bool" reals nil )nil booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )nil rs_integral_prep nil )"[real -> boolean]" rs_integral_prep 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 3489155718"" (skosimp*)"" (lemma "integral_const_fun" )"" (inst -1 "_" "a!1" "b!1" "g!1" )"" (lemma "integral_diff" )"" (inst -1 "a!1" "b!1" "_" "g!1" "_" )"" (lemma "integral_ge_0" )"" "a!1" "b!1" "(LAMBDA (t:real): f!1(t) - m!1)" "g!1" )"" (assert )"" case "integrable?(a!1, b!1, g!1,(LAMBDA (t: real): f!1(t) - m!1))" )"1" (assert )"1" (inst -4 "m!1" )"1" (flatten)"1" (inst -3 "f!1" "const_fun(m!1)" )"1" (assert )"1" expand "const_fun" )"1" replace -5)"1" "1" "1" (assert ) nil nil )"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst -2 "f!1" "const_fun(m!1)" )"2" (assert )"2" (inst -3 "m!1" )"2" (expand "const_fun" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"continuous_fun" nil )nil intervals_real "reals/" )"[T -> real]" real_fun_ops "reals/" ))nil ))nil 3297781017"" (skosimp*)"" (lemma "integral_diff" )"" (inst - "a!1" "b!1" "h!1" "g!1" "f!1" )"" (assert )"" (flatten)"" case "integral(a!1, b!1, g!1, LAMBDA x: h!1(x) - f!1(x)) >= 0" )"1" (assert ) nil nil )"2" (hide 2)"2" (lemma "integral_bound_below" )"2" "a!1" "b!1" "LAMBDA x: h!1(x) - f!1(x)" "g!1" "0" )"2" (assert ) nil nil )) nil ))nil ))nil )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil rs_integral_prep nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"{S: real | integral?(a, b, gg, ff, S)}" nil )"bool" rs_integral_def nil )"bool" rs_integral_def nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil booleans nil )"real" reals nil )"(total_order?[real])" nil )nil rs_integral_prep nil )nil rs_integral_prep nil )"[real -> boolean]" rs_integral_prep nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3282496507"" (skosimp*)"" (expand "integrable?" )"" (skosimp*)"" (expand "integral?" )"" (inst - "eps!1/2" )"" (skosimp*)"" (inst + "delta!1" )"" (skosimp*)"" (copy -2)"" (inst - "P1!1" )"" (inst - "P2!1" )"" (assert )"" (flatten)"" (assert )"" "R1" "Rie_sum(a!1, b!1,g!1, P1!1, xis1!1, f!1)" )"" replace -1)"" "R2" "Rie_sum(a!1, b!1, g!1,P2!1, xis2!1, f!1)" )"" replace -1)"" "R1 - R2 = (R1 - S!1) - (R2 - S!1)" )"1" "triangle" )"1" "R1-S!1" "-(R2 - S!1)" )"1" assert )"1" assert )"1" "abs(S!1 - R2) = abs(R2 - S!1)" )"1" "abs(S!1 - R1) = abs(R1 - S!1)" )"1" assert )"1" "R1" )"1" "R2" )"1" assert )nil nil )"2" "Riemann?_Rie" )"2" "a!1" "b!1" "f!1" "g!1" )"2" "1" "P2!1" "xis2!1" )"1" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" "Riemann?_Rie" )"2" "a!1" "b!1" "f!1" "g!1" )"2" "1" "P1!1" "xis1!1" )"1" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" rs_integral_def nil )"real" reals nil )"bool" rs_integral_def nil )nil naturalnumbers nil )"[real -> boolean]" rs_integral_prep nil )nil rs_integral_prep nil )nil fseqs "structures/" )nil fseqs "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"R" restrict nil )"bool" reals nil )"bool" sort_fseq "structures/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil rs_partition nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )nil real_props nil )"nnreal" nil )"(total_order?[real])" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"partition[T](a!1, b!1)" rs_integral_prepnil )"real" rs_integral_prep nil )nil rs_integral_def nil )"real" rs_integral_prep nil )"[T -> real]" rs_integral_prep nil )"[T -> real]" rs_integral_prep nil )"partition[T](a!1, b!1)" rs_integral_prepnil )"T" rs_integral_prep nil )"T" rs_integral_prep nil )"bool" rs_integral_def nil )"[numfield -> numfield]" number_fields nil )"real" reals nil )"real" reals nil )"real" rs_integral_def nil )nil rs_integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" nil ))nil )nil 3282496495 ("" (postpone) nil nil ) nil shostak))"DEbugging PVS 3.2" 3495206489"" (auto-rewrite + "member" )"" (skosimp*)"" (prop)"1" (skosimp*)"1" (expand "integrable?" )"1" (skosimp*)"1" (expand "integral?" )"1" (inst -1 "epsi!1/2" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (inst-cp -1 "P1!1" )"1" (inst -1 "P2!1" )"1" (assert )"1" "RS2!1" )"1" "RS1!1" )"1" "RS1!1 - RS2!1 = (RS1!1 - S!1) - (RS2!1 - S!1)" )"1" "triangle" )"1" "RS1!1-S!1" "-(RS2!1-S!1)" )"1" "abs(-(RS2!1 - S!1)) = abs(S!1 - RS2!1)" )"1" "abs(RS1!1 - S!1) = abs(S!1 - RS1!1)" )"1" (assert ) nil nil )"2" "2" expand "abs" )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "abs" )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case " FORALL (n: nat): nonempty?({S: real | EXISTS (P: partition(a!1, b!1),xis:xis?(a!1,b!1,P)): width(a!1, b!1, P) < 1 / (1 + n) AND S = Rie_sum(a!1, b!1, g!1,P, xis, f!1)})" )"1" "SS" "(LAMBDA (n: nat): choose({S:real| EXISTS (P: partition(a!1,b!1), AND ") "1" (case "cauchy(SS)" )"1" (lemma "convergence_cauchy2" )"1" (inst?)"1" (assert )"1" (expand "convergent?" )"1" (skosimp*)"1" (expand "integrable?" )"1" (inst + "l!1" )"1" (expand "integral?" )"1" "1" "epsi!1/2" )"1" "1" "delta!1" )"1" "1" "R!1" )"1" expand "Riemann_sum?" )"1" "1" replace -1)"1" "1" expand "convergence" )"1" "epsi!1/2" )"1" "1" "NN" "choose({nn: nat | nn > n!1 AND nn > 1/delta!1})" )"1" "NN" )"1" assert )"1" "choose({S: real | EXISTS (P: partition(a!1, b!1), AND S = Rie_sum(a!1, b!1, g!1,P, xis, f!1)})") "1" "1" "P!1" "P!2" )"1" assert )"1" case "width(a!1, b!1, P!2) < delta!1" )"1" assert )"1" "ST" "Rie_sum(a!1, b!1,g!1, P!1, xis!1, f!1)" )"1" replace "1" "abs(l!1 - ST) = abs(ST - l!1)" )"1" "ST- l!1 = (ST - SS(NN)) + (SS(NN) - l!1)" )"1" "triangle" )"1" "ST- SS(NN)" "SS(NN) - l!1" )"1" "ST" "SS(NN)" )"1" assert )nil nil )"2" "2" case "SS(NN) = Rie_sum(a!1, b!1, g!1,P!2, xis!2, f!1)" )"1" replace "1" "1" "Riemann?_Rie" )"1" "a!1" "b!1" "f!1" "g!1" )"1" "1" nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" replace "3" "3" "Riemann?_Rie" )"3" "a!1" "b!1" "f!1" "g!1" )"3" "1" nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" case "1 / (1 + NN) < delta!1" )"1" assert )nil nil )"2" "2" "2" "NN" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "NN" )nil nil ))nil ))nil ))nil )"2" "2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "axiom_of_archimedes" )"2" case "n!1 > 1/delta!1" )"1" "n!1" )"1" "1" "i!1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "1/delta!1" )"2" "2" "i!1" )"1" assert )nil nil )"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 )"2" (hide 2)"2" (expand "cauchy" )"2" (skosimp*)"2" (inst -3 "epsilon!1" )"2" (skosimp*)"2" "NN" "choose({n: posnat | 1/n < delta!1})" )"1" (inst + "NN" )"1" (skosimp*)"1" "choose({S: real | EXISTS (P: partition(a!1, b!1), AND ") "1" "1" "choose({S: real | EXISTS (P: partition(a!1, b!1), AND ") "1" "1" assert )"1" "P!1" "P!2" )"1" "1" assert )"1" "1" "1" "1" replace "1" "1" replace -1)"1" expand "Riemann_sum?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" "2" replace -2)"2" expand "Riemann_sum?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "1 / NN < delta!1" )"1" case "1 / (1 + i!1) <= 1/NN" )"1" assert )nil nil )"2" "2" "2" "ip1" "i!1+1" )"2" replace -1)"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"3" "1 / (1 + j!1) <= 1/NN" )"1" (assert ) nil nil )"2" "2" "2" "jp1" "j!1+1" )"2" replace -1)"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst -7 "j!1" ) nil nil ))nil ))nil )"2" (inst -5 "i!1" ) nil nil )"3" (skosimp*) nil nil )"4" (skosimp*) nil nil ))nil ))nil ))nil )"2" (assert )"2" (hide 2)"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "axiom_of_archimedes" )"2" "1/delta!1" )"2" "2" "i!1" )"1" case "i!1 >= 0" )"1" "div_mult_pos_lt1" )"1" "1" "div_mult_pos_lt1" )"1" "i!1" "delta!1" "1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil )"2" (skosimp*)"2" (hide -1 2)"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (assert )"2" (name "BMA" "b!1-a!1" )"2" "NP" "choose({n: above(1) | BMA/(n-1) < 1/(1+n!1)})" )"1" "Rie_sum(a!1, b!1,g!1, eq_partition(a!1,b!1,NP), gen_xis(a!1,b!1,eq_partition(a!1,b!1,NP)), f!1)" )"1" (inst?)"1" rewrite "width_eq_part" )"1" assert )"1" replace -2 :dir rl)"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" expand "member" )"2" "axiom_of_archimedes" )"2" "2 + BMA*(n!1+1)" )"2" "2" "pos_times_lt" )"2" "2" assert )"2" "i!1" )"2" case "BMA / (i!1 - 1) < BMA / (1 + BMA * (n!1 + 1) )" )"1" "np1" "n!1+1" )"1" "BMA / (1 + BMA * np1) < 1/np1" )"1" assert )nil nil )"2" "2" "2" nil nil ))nil ))nil )"3" nil nil ))nil ))nil )"2" assert )"2" "2" "2" assert )"2" "1 + BMA + BMA * n!1 < i!1 -1" )"1" "1" "TT" "1 + BMA + BMA * n!1" )"1" "im1" "i!1-1" )"1" nil nil ))nil ))nil ))nil )"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 )"real" reals nil )"real" rs_integral_def nil )"posreal" rs_partition nil )nil rs_integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" sets nil )set type-eq-decl nil sets nil )"posrat" nil )"posint" nil )nil sequences nil )"bool" convergence_sequences nil )"bool" convergence_sequences nil )NOT const-decl "[bool -> bool]" booleans nil )nil real_props nil )"posreal" nil )"nnreal" nil )nil extra_real_props nil )"(strict_total_order?[real])" real_props nil )nil rs_integral_def nil )"({nn: nat | nn > n!1 AND nn > 1 / delta!1})" nil )"posreal" rs_integral_prep nil )"nat" rs_integral_prep nil )"[n: nat -> AND " rs_integral_prep nil )"partition[T](a!1, b!1)" rs_integral_prepnil )"real" rs_integral_prep nil )"[T -> real]" rs_integral_prep nil )"[T -> real]" rs_integral_prep nil )"partition[T](a!1, b!1)" rs_integral_prepnil )"T" rs_integral_prep nil )"T" rs_integral_prep nil )"bool" sets nil )nil real_props nil )"int" rs_integral_prep nil )"int" rs_integral_prep nil )"bool" sets nil )"bool" convergence_sequences nil )"int" integers nil )nil convergence_sequences nil )nil integers nil )nil integers nil )"rat" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )nil reals nil )nil real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"posint" nil )nil real_props nil )nil integers nil )"partition[T](a!1, b!1)" rs_integral_prepnil )"nat" rs_integral_prep nil )"partition[T](a!1, b!1)" rs_integral_prepnil )"nat" rs_integral_prep nil )"[bool, bool -> bool]" booleans nil )"int" rs_integral_prep nil )"real" reals nil )"nzrat" rationalsnil )"(p)" sets nil )"posint" nil )"real" reals nil )nil integers nil )nil rs_partition nil )"partition(a, b)" rs_partition nil )"xis?(a, b, P)" rs_integral_def nil )"odd_int" integersnil )nil real_props nil )nil real_props nil )"posint" rs_integral_prep nil )"real" rs_integral_prep nil )nil real_props nil )"posreal" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"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 naturalnumbers nil )"[real -> boolean]" rs_integral_prep nil )nil rs_integral_prep nil )nil fseqs "structures/" )nil fseqs "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"R" restrict nil )"bool" reals nil )"bool" sort_fseq "structures/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil rs_partition nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"nnreal" nil )"(total_order?[real])" nil )"[numfield -> numfield]" number_fields nil )"real" reals nil )"real" reals nil )"odd_int" integers nil )"bool" rs_integral_def nil )"bool" rs_integral_def nil )"bool" rs_integral_def nil ))nil ))nil 3492182124"" case "FORALL (a, b:T, f, g: [T -> real]): AND LAMBDA (x:T): a <= x AND x <= b)]LAMBDA (x:T): a <= x AND x <= b), real]") "1" (skolem 1 ("a" "b" "f" "gg" ))"1" (flatten)"1" (assert )"1" (expand "monotonic?" )"1" (flatten)"1" (split -)"1" (inst?) (("1" (assert ) nil nil )) nil )"2" (case "NOT increasing?[(closed_intv(a,b))](-gg)" )"1" (hide-all-but (-1 1))"1" (expand "increasing?" )"1" (expand "decreasing?" )"1" (skeep)"1" (inst - "x" "y" )"1" (assert )"1" expand "restrict" )"1" expand "-" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2)"2" (inst - "a" "b" "f" "-gg" )"2" (assert )"2" (split +)"1" (flatten)"1" (case "integrable?(a,b,-gg,f)" )"1" assert )"1" "1" "1" "epsi" )"1" "1" "delta" )"1" "1" "P" )"1" assert )"1" "RSS1" "RSS2" ))"1" "RSS1" )"1" "RSS2" )"1" expand "Riemann_sum?" )"1" "xis2" )"1" "xis1" )"1" "RSP1" "Rie_sum(a,b,-gg,P,xis1,f)" )"1" "RSP2" "Rie_sum(a,b,-gg,P,xis2,f)" )"1" case "RSP1 = -RSS1 AND RSP2 = -RSS2" )"1" "1" "RSP1" "RSP2" )"1" "1" nil nil ))nil )"2" replace "2" "Riemann?_Rie" )"2" "a" "b" "f" "-gg" )"2" "1" "P" "xis2" )nil nil )"2" nil nil ))nil ))nil ))nil ))nil )"3" replace "3" "Riemann?_Rie" )"3" "a" "b" "f" "-gg" )"3" "1" "P" "xis1" )nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" replace "2" replace "2" replace "2" "2" expand "Rie_sum" )"2" "1" "sigma_scal[below(P`length-1)]" )"1" "LAMBDA (n: below(P`length - 1)): " "-1" "P`length-2" "0" )"1" replace "1" "1" "sigma_restrict_eq[below(P`length-1)]" )"1" "1" assert )"1" "1" expand "restrict" )"1" expand "-" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "sigma_scal[below(P`length-1)]" )"1" "LAMBDA (n: below(P`length - 1)): " "-1" "P`length-2" "0" )"1" replace "1" "1" "sigma_restrict_eq[below(P`length-1)]" )"1" "1" assert )"1" "1" expand "restrict" )"1" expand "-" )"1" 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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "integral_scal_g" )"2" "-1" "a" "b" "f" "gg" )"2" assert )"2" "2" assert )"2" expand "-" )"2" expand "*" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (case "integrable?(a,b,-gg,f)" )"1" "1" "integral_scal_g" )"1" "-1" "a" "b" "f" "-gg" )"1" assert )"1" "1" expand "-" )"1" expand "*" )"1" case "gg = (LAMBDA (x_1:T): -1 * -gg(x_1))" )"1" (assert ) nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "2" "2" "epsi" )"2" "2" "delta" )"2" "2" "P" )"2" assert )"2" "RSS1" "RSS2" ))"2" "RSS1" )"2" "RSS2" )"2" expand "Riemann_sum?" )"2" "xis2" )"2" "xis1" )"2" "RSP1" "Rie_sum(a,b,gg,P,xis1,f)" )"2" "RSP2" "Rie_sum(a,b,gg,P,xis2,f)" )"2" case "RSP1 = -RSS1 AND RSP2 = -RSS2" )"1" "1" "RSP1" "RSP2" )"1" "1" nil nil ))nil )"2" "Riemann?_Rie" )"2" "a" "b" "f" "gg" )"2" "1" "P" "xis2" )"1" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil )"3" "Riemann?_Rie" )"3" "a" "b" "f" "gg" )"3" "1" "P" "xis1" )"1" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" replace "2" replace "2" replace "2" "2" expand "Rie_sum" )"2" "1" "sigma_scal[below(P`length-1)]" )"1" "LAMBDA (n: below(P`length - 1)): " "-1" "P`length-2" "0" )"1" replace "1" "1" "sigma_restrict_eq[below(P`length-1)]" )"1" "1" assert )"1" "1" expand "restrict" )"1" expand "-" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "sigma_scal[below(P`length-1)]" )"1" "LAMBDA (n: below(P`length - 1)): " "-1" "P`length-2" "0" )"1" replace "1" "1" "sigma_restrict_eq[below(P`length-1)]" )"1" "1" assert )"1" "1" expand "restrict" )"1" expand "-" )"1" 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 ))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" (hide 2)"2" (skolem 1 ("a" "b" "f" "gg" ))"2" (flatten)"2" (label "gincreasing?" -2)"2" (hide "gincreasing?" )"2" (ground)"1" (rewrite "integrable_lem" )"1" (skeep)"1" (inst - "epsi" )"1" (skeep -1)"1" (inst + "delta" )"1" (skeep)"1" (inst - "P" "P" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (epsi:posreal): EXISTS (delta: posreal): ") "1" (hide -2)"1" (rewrite "integrable_lem" )"1" (skeep)"1" (inst - "epsi/2" )"1" (skeep -1)"1" (inst + "delta" )"1" "1" "P1" "P2" )"1" "P2" "P1" )"1" assert )"1" case "EXISTS (RS12: (Riemann_sum?(a, b, partition_union(a, b)(P1, P2), gg,f))): TRUE" )"1" "1" "1" "RS2!1" "RS12" )"1" "RS1!1" "RS12" )"1" "1" "1" nil nil ))nil ))nil ))nil )"2" "RS12" )"2" "partition_union_sym" )"2" "a" "b" )"2" assert )"2" "P1" "P2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "Riemann?_Rie" )"2" "a" "b" "f" "gg" )"2" "1" "partition_union(a,b)(P1,P2)" "gen_xis(a,b,partition_union(a,b)(P1,P2))" )"1" "Rie_sum(a, b, gg, partition_union(a, b)(P1, P2), ") nil nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "Rie_sum_diff_extend_union" )"2" (skeep)"2" (inst -2 "epsi" )"2" (skeep -2)"2" (inst + "delta" )"2" "P" "Q" ))"2" "a" "b" "f" "gg" )"2" assert )"2" "gincreasing?" )"2" replace "gincreasing?" )"2" "gincreasing?" )"2" "P" "Q" )"2" "2" "RSS1" "RSS2" ))"2" "RSS1" )"2" "RSS2" )"2" expand "Riemann_sum?" )"2" "xispq" )"2" "xis" )"2" "xispq" "xis" )"2" "2" "P" )"2" assert )"2" "RSS1" "Rie_sum(a, b, gg, P, xis2, f)" )"1" assert )nil nil )"2" "Riemann?_Rie" )"2" "a" "b" "f" "gg" )"2" "1" "P" "xis2" )nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{PQ: partition(a, b) | OR member(x, Q)))AND strictly_increasing?(PQ)}" rs_partition nil) "bool" sort_fseq "structures/" )"bool" fseqs "structures/" )"posreal" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"xis?(a, b, P)" rs_integral_def nil )"T" rs_integral_prep nil )"T" rs_integral_prep nil )"partition[T](a, b)" rs_integral_prep nil )"partition[T](a, b)" rs_integral_prep nil )"[T -> real]" rs_integral_prep nil )"[T -> real]" rs_integral_prep nil )"(Riemann_sum?(a, b, partition_union(a, b)(P1, P2), gg, f))" nil )nil rs_partition nil )"bool" booleans nil )nil rs_integral_def nil )"xis?[T](a, b, P)" rs_integral_prep nil )"partition[T](a, b)" rs_integral_prep nil )nil rs_integral_prep nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"[T -> real]" real_fun_ops "reals/" )"(total_order?[real])" nil )"real" reals nil )"bool" real_fun_preds "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil rs_integral_def nil )"real" rs_integral_def nil )"T" rs_integral_prep nil )"T" rs_integral_prep nil )"partition[T](a, b)" rs_integral_prep nil )"[T -> real]" rs_integral_prep nil )"[T -> real]" rs_integral_prep nil )"real" rs_integral_prep nil )"real" rs_integral_prep nil )"odd_int" integers nil )nil rs_integral_def nil )"real" reals nil )nil sigma "reals/" )nil integers nil )nil sigma "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[T -> real]" sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )nil sigma "reals/" )"posint" nil )"int" integers nil )nil rs_integral_prep nil )"[T -> real]" real_fun_ops "reals/" )"partition[T](a, b)" rs_integral_prep nil )"real" rs_integral_prep nil )"real" rs_integral_prep nil )"bool" real_fun_preds "reals/" )"real" reals 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]" rs_integral_prep nil )nil rs_integral_prep nil )nil booleans nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (<= const-decl "bool" reals nil )"bool" real_fun_preds "reals/" )"R" restrict nil )"[bool, bool -> bool]" booleans nil )"bool" rs_integral_def nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil naturalnumbers nil )nil fseqs "structures/" )nil fseqs "structures/" )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" sort_fseq "structures/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil rs_partition nil )"posreal" rs_partition nil )"bool" rs_integral_def nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil ))nil ))nil 3494858376"" case "FORALL (a, b:T, f, g: [T -> real]): AND LAMBDA (x:T): a <= x AND x <= b)]LAMBDA (x:T): a <= x AND x <= b), real]") "1" (skolem 1 ("a" "b" "f" "gg" ))"1" (flatten)"1" (assert )"1" (expand "monotonic?" )"1" (flatten)"1" (split -)"1" (inst?) (("1" (assert ) nil nil )) nil )"2" (case "NOT increasing?[(closed_intv(a,b))](-gg)" )"1" (hide-all-but (-1 1))"1" (expand "increasing?" )"1" (expand "decreasing?" )"1" (skeep)"1" (inst - "x" "y" )"1" (assert )"1" expand "restrict" )"1" expand "-" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2)"2" (inst - "a" "b" "f" "-gg" )"2" (assert )"2" (split +)"1" (flatten)"1" (case "integrable?(a,b,-gg,f)" )"1" assert )"1" "1" "1" "epsi" )"1" "1" "delta" )"1" "1" "P" )"1" assert )"1" "RSS1" "RSS2" ))"1" "RSS1" )"1" "RSS2" )"1" expand "Riemann_sum?" )"1" "xis2" )"1" "xis1" )"1" "RSP1" "Rie_sum(a,b,-gg,P,xis1,f)" )"1" "RSP2" "Rie_sum(a,b,-gg,P,xis2,f)" )"1" case "RSP1 = -RSS1 AND RSP2 = -RSS2" )"1" "1" "RSP1" "RSP2" )"1" "1" nil nil ))nil )"2" replace "2" "Riemann?_Rie" )"2" "a" "b" "f" "-gg" )"2" "1" "P" "xis2" )nil nil )"2" nil nil ))nil ))nil ))nil ))nil )"3" replace "3" "Riemann?_Rie" )"3" "a" "b" "f" "-gg" )"3" "1" "P" "xis1" )nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" replace "2" replace "2" replace "2" "2" expand "Rie_sum" )"2" "1" "sigma_scal[below(P`length-1)]" )"1" "LAMBDA (n: below(P`length - 1)): " "-1" "P`length-2" "0" )"1" replace "1" "1" "sigma_restrict_eq[below(P`length-1)]" )"1" "1" assert )"1" "1" expand "restrict" )"1" expand "-" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "sigma_scal[below(P`length-1)]" )"1" "LAMBDA (n: below(P`length - 1)): " "-1" "P`length-2" "0" )"1" replace "1" "1" "sigma_restrict_eq[below(P`length-1)]" )"1" "1" assert )"1" "1" expand "restrict" )"1" expand "-" )"1" 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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "integral_scal_g" )"2" "-1" "a" "b" "f" "gg" )"2" assert )"2" "2" assert )"2" expand "-" )"2" expand "*" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (case "integrable?(a,b,-gg,f)" )"1" "1" "integral_scal_g" )"1" "-1" "a" "b" "f" "-gg" )"1" assert )"1" "1" expand "-" )"1" expand "*" )"1" case "gg = (LAMBDA (x_1:T): -1 * -gg(x_1))" )"1" (assert ) nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "2" "2" "epsi" )"2" "2" "delta" )"2" "2" "P" )"2" assert )"2" "RSS1" "RSS2" ))"2" "RSS1" )"2" "RSS2" )"2" expand "Riemann_sum?" )"2" "xis2" )"2" "xis1" )"2" "RSP1" "Rie_sum(a,b,gg,P,xis1,f)" )"2" "RSP2" "Rie_sum(a,b,gg,P,xis2,f)" )"2" case "RSP1 = -RSS1 AND RSP2 = -RSS2" )"1" "1" "RSP1" "RSP2" )"1" "1" nil nil ))nil )"2" "Riemann?_Rie" )"2" "a" "b" "f" "gg" )"2" "1" "P" "xis2" )"1" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil )"3" "Riemann?_Rie" )"3" "a" "b" "f" "gg" )"3" "1" "P" "xis1" )"1" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" replace "2" replace "2" replace "2" "2" expand "Rie_sum" )"2" "1" "sigma_scal[below(P`length-1)]" )"1" "LAMBDA (n: below(P`length - 1)): " "-1" "P`length-2" "0" )"1" replace "1" "1" "sigma_restrict_eq[below(P`length-1)]" )"1" "1" assert )"1" "1" expand "restrict" )"1" expand "-" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "sigma_scal[below(P`length-1)]" )"1" "LAMBDA (n: below(P`length - 1)): " "-1" "P`length-2" "0" )"1" replace "1" "1" "sigma_restrict_eq[below(P`length-1)]" )"1" "1" assert )"1" "1" expand "restrict" )"1" expand "-" )"1" 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 ))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" (hide 2)"2" (skolem 1 ("a" "b" "f" "gg" ))"2" (flatten)"2" (label "gincreasing?" -2)"2" (hide "gincreasing?" )"2" (ground)"1" (rewrite "integrable_lem" )"1" (skeep)"1" (inst - "epsi" )"1" (skeep -1)"1" (inst + "delta" )"1" (skeep)"1" (inst - "P" "P" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (epsi:posreal): EXISTS (delta: posreal): ") "1" (hide -2)"1" (rewrite "integrable_lem" )"1" (skeep)"1" (inst - "epsi/2" )"1" (skeep -1)"1" (inst + "delta" )"1" "1" "P1" "P2" )"1" "P2" "P1" )"1" assert )"1" case "EXISTS (RS12: (Riemann_sum?(a, b, partition_union(a, b)(P1, P2), gg,f))): TRUE" )"1" "1" "1" "RS2!1" "RS12" )"1" "RS1!1" "RS12" )"1" "1" "1" nil nil ))nil ))nil ))nil )"2" "RS12" )"2" "partition_union_sym" )"2" "a" "b" )"2" assert )"2" "P1" "P2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "Riemann?_Rie" )"2" "a" "b" "f" "gg" )"2" "1" "partition_union(a,b)(P1,P2)" "gen_xis(a,b,partition_union(a,b)(P1,P2))" )"1" "Rie_sum(a, b, gg, partition_union(a, b)(P1, P2), ") nil nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "Rie_sum_diff_extend_union" )"2" (skeep)"2" (inst -2 "epsi" )"2" (skeep -2)"2" (inst + "delta" )"2" "P" "Q" ))"2" "a" "b" "f" "gg" )"2" assert )"2" "gincreasing?" )"2" replace "gincreasing?" )"2" "gincreasing?" )"2" "P" "Q" )"2" "2" "RSS1" "RSS2" ))"2" "RSS1" )"2" "RSS2" )"2" expand "Riemann_sum?" )"2" "xispq" )"2" "xis" )"2" "xispq" "xis" )"2" "2" "P" )"2" assert )"2" "RSS1" "Rie_sum(a, b, gg, P, xis2, f)" )"1" assert )nil nil )"2" "Riemann?_Rie" )"2" "a" "b" "f" "gg" )"2" "1" "P" "xis2" )nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{PQ: partition(a, b) | OR member(x, Q)))AND strictly_increasing?(PQ)}" rs_partition nil) "bool" sort_fseq "structures/" )"bool" fseqs "structures/" )"posreal" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"xis?(a, b, P)" rs_integral_def nil )"T" rs_integral_prep nil )"T" rs_integral_prep nil )"partition[T](a, b)" rs_integral_prep nil )"partition[T](a, b)" rs_integral_prep nil )"[T -> real]" rs_integral_prep nil )"[T -> real]" rs_integral_prep nil )"(Riemann_sum?(a, b, partition_union(a, b)(P1, P2), gg, f))" nil )nil rs_partition nil )"bool" booleans nil )nil rs_integral_def nil )"xis?[T](a, b, P)" rs_integral_prep nil )"partition[T](a, b)" rs_integral_prep nil )nil rs_integral_prep nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"[T -> real]" real_fun_ops "reals/" )"(total_order?[real])" nil )"real" reals nil )"bool" real_fun_preds "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil rs_integral_def nil )"real" rs_integral_def nil )"T" rs_integral_prep nil )"T" rs_integral_prep nil )"partition[T](a, b)" rs_integral_prep nil )"[T -> real]" rs_integral_prep nil )"[T -> real]" rs_integral_prep nil )"real" rs_integral_prep nil )"real" rs_integral_prep nil )"odd_int" integers nil )nil rs_integral_def nil )"real" reals nil )nil sigma "reals/" )nil integers nil )nil sigma "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[T -> real]" sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )nil sigma "reals/" )"posint" nil )"int" integers nil )nil rs_integral_prep nil )"[T -> real]" real_fun_ops "reals/" )"partition[T](a, b)" rs_integral_prep nil )"real" rs_integral_prep nil )"real" rs_integral_prep nil )"bool" real_fun_preds "reals/" )"real" reals 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]" rs_integral_prep nil )nil rs_integral_prep nil )nil booleans nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (<= const-decl "bool" reals nil )"bool" real_fun_preds "reals/" )"R" restrict nil )"[bool, bool -> bool]" booleans nil )"bool" rs_integral_def nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil naturalnumbers nil )nil fseqs "structures/" )nil fseqs "structures/" )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" sort_fseq "structures/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil rs_partition nil )"posreal" rs_partition nil )"bool" rs_integral_def nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil ))nil )nil 3492513670"" case "FORALL (a, b: real, f, g: [real -> real]): AND LAMBDA (x: real): a <= x AND x <= b)]LAMBDA (x: real): a <= x AND x <= b), real]") "1" (skolem 1 ("a" "b" "f" "gg" ))"1" (flatten)"1" (assert )"1" (expand "monotonic?" )"1" (flatten)"1" (split -)"1" (inst?) (("1" (assert ) nil nil )) nil )"2" (case "NOT increasing?[(closed_intv(a,b))](-gg)" )"1" (hide-all-but (-1 1))"1" (expand "increasing?" )"1" (expand "decreasing?" )"1" (skeep)"1" (inst - "x" "y" )"1" (assert )"1" expand "restrict" )"1" expand "-" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2)"2" (inst - "a" "b" "f" "-gg" )"2" (assert )"2" (split +)"1" (flatten)"1" (case "integrable?(a,b,-gg,f)" )"1" assert )"1" "1" "1" "epsi" )"1" "1" "delta" )"1" "1" "P" )"1" assert )"1" "RSS1" "RSS2" ))"1" "RSS1" )"1" "RSS2" )"1" expand "Riemann_sum?" )"1" "xis2" )"1" "xis1" )"1" "RSP1" "Rie_sum(a,b,-gg,P,xis1,f)" )"1" "RSP2" "Rie_sum(a,b,-gg,P,xis2,f)" )"1" case "RSP1 = -RSS1 AND RSP2 = -RSS2" )"1" "1" "RSP1" "RSP2" )"1" "1" nil nil ))nil )"2" replace "2" "Riemann?_Rie" )"2" "a" "b" "f" "-gg" )"2" "1" "P" "xis2" )nil nil )"2" nil nil ))nil ))nil ))nil ))nil )"3" replace "3" "Riemann?_Rie" )"3" "a" "b" "f" "-gg" )"3" "1" "P" "xis1" )nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" replace "2" replace "2" replace "2" "2" expand "Rie_sum" )"2" "1" "sigma_scal[below(P`length-1)]" )"1" "LAMBDA (n: below(P`length - 1)): " "-1" "P`length-2" "0" )"1" replace "1" "1" "sigma_restrict_eq[below(P`length-1)]" )"1" "1" assert )"1" "1" expand "restrict" )"1" expand "-" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "sigma_scal[below(P`length-1)]" )"1" "LAMBDA (n: below(P`length - 1)): " "-1" "P`length-2" "0" )"1" replace "1" "1" "sigma_restrict_eq[below(P`length-1)]" )"1" "1" assert )"1" "1" expand "restrict" )"1" expand "-" )"1" 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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "integral_scal_g" )"2" "-1" "a" "b" "f" "gg" )"2" assert )"2" "2" assert )"2" expand "-" )"2" expand "*" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (case "integrable?(a,b,-gg,f)" )"1" "1" "integral_scal_g" )"1" "-1" "a" "b" "f" "-gg" )"1" assert )"1" "1" expand "-" )"1" expand "*" )"1" case "gg = (LAMBDA (x_1: real): -1 * -gg(x_1))" )"1" (assert ) nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "2" "2" "epsi" )"2" "2" "delta" )"2" "2" "P" )"2" assert )"2" "RSS1" "RSS2" ))"2" "RSS1" )"2" "RSS2" )"2" expand "Riemann_sum?" )"2" "xis2" )"2" "xis1" )"2" "RSP1" "Rie_sum(a,b,gg,P,xis1,f)" )"2" "RSP2" "Rie_sum(a,b,gg,P,xis2,f)" )"2" case "RSP1 = -RSS1 AND RSP2 = -RSS2" )"1" "1" "RSP1" "RSP2" )"1" "1" nil nil ))nil )"2" "Riemann?_Rie" )"2" "a" "b" "f" "gg" )"2" "1" "P" "xis2" )"1" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil )"3" "Riemann?_Rie" )"3" "a" "b" "f" "gg" )"3" "1" "P" "xis1" )"1" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" replace "2" replace "2" replace "2" "2" expand "Rie_sum" )"2" "1" "sigma_scal[below(P`length-1)]" )"1" "LAMBDA (n: below(P`length - 1)): " "-1" "P`length-2" "0" )"1" replace "1" "1" "sigma_restrict_eq[below(P`length-1)]" )"1" "1" assert )"1" "1" expand "restrict" )"1" expand "-" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "sigma_scal[below(P`length-1)]" )"1" "LAMBDA (n: below(P`length - 1)): " "-1" "P`length-2" "0" )"1" replace "1" "1" "sigma_restrict_eq[below(P`length-1)]" )"1" "1" assert )"1" "1" expand "restrict" )"1" expand "-" )"1" 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 ))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" (hide 2)"2" (skolem 1 ("a" "b" "f" "gg" ))"2" (flatten)"2" (label "gincreasing?" -2)"2" (hide "gincreasing?" )"2" (ground)"1" (rewrite "integrable_lem" )"1" (skeep)"1" (inst - "epsi" )"1" (skeep -1)"1" (inst + "delta" )"1" (skeep)"1" (inst - "P" "P" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (epsi:posreal): EXISTS (delta: posreal): ") "1" (hide -2)"1" (rewrite "integrable_lem" )"1" (skeep)"1" (inst - "epsi/2" )"1" (skeep -1)"1" (inst + "delta" )"1" "1" "P1" "P2" )"1" "P2" "P1" )"1" assert )"1" case "EXISTS (RS12: (Riemann_sum?(a, b, partition_union(a, b)(P1, P2), gg,f))): TRUE" )"1" "1" "1" "RS2!1" "RS12" )"1" "RS1!1" "RS12" )"1" "1" "1" nil nil ))nil ))nil ))nil )"2" "RS12" )"2" "partition_union_sym" )"2" "a" "b" )"2" assert )"2" "P1" "P2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "Riemann?_Rie" )"2" "a" "b" "f" "gg" )"2" "1" "partition_union(a,b)(P1,P2)" "gen_xis(a,b,partition_union(a,b)(P1,P2))" )"1" "Rie_sum(a, b, gg, partition_union(a, b)(P1, P2), ") nil nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "Rie_sum_diff_extend_union" )"2" (skeep)"2" (inst -2 "epsi" )"2" (skeep -2)"2" (inst + "delta" )"2" "P" "Q" ))"2" "a" "b" "f" "gg" )"2" assert )"2" "gincreasing?" )"2" replace "gincreasing?" )"2" "gincreasing?" )"2" "P" "Q" )"2" "2" "RSS1" "RSS2" ))"2" "RSS1" )"2" "RSS2" )"2" expand "Riemann_sum?" )"2" "xispq" )"2" "xis" )"2" "xispq" "xis" )"2" "2" "P" )"2" assert )"2" "RSS1" "Rie_sum(a, b, gg, P, xis2, f)" )"1" assert )nil nil )"2" "Riemann?_Rie" )"2" "a" "b" "f" "gg" )"2" "1" "P" "xis2" )nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sort_fseq "structures/" )nil fseqs "structures/" )nil fseqs "structures/" )"bool" real_fun_preds "reals/" )"bool" real_fun_preds "reals/" )nil sigma "reals/" )nil sigma "reals/" )"[T -> real]" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" real_fun_preds "reals/" )"bool" sort_fseq "structures/" )"bool" fseqs "structures/" ))nil )nil 3491565290"" case "FORALL (a, b: real, f, g: [real -> real]): AND LAMBDA (x: real): a <= x AND x <= b)]LAMBDA (x: real): a <= x AND x <= b), real]") "1" (skolem 1 ("a" "b" "f" "gg" ))"1" (flatten)"1" (expand "monotonic?" )"1" (split -)"1" (inst?) (("1" (assert ) nil nil )) nil )"2" (case "NOT increasing?[(closed_intv(a,b))](-gg)" )"1" (hide-all-but (-1 1))"1" (expand "increasing?" )"1" (expand "decreasing?" )"1" (skeep)"1" (inst - "x" "y" )"1" (assert )"1" (expand "restrict" )"1" (expand "-" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2)"2" (inst - "a" "b" "f" "-gg" )"2" (assert )"2" (split +)"1" (flatten)"1" (case "integrable?(a,b,-gg,f)" )"1" (assert )"1" (hide -5)"1" "1" "epsi" )"1" "1" "delta" )"1" "1" "P" )"1" assert )"1" "RSS1" "RSS2" ))"1" "RSS1" )"1" "RSS2" )"1" expand "Riemann_sum?" )"1" "xis2" )"1" "xis1" )"1" "RSP1" "Rie_sum(a,b,-gg,P,xis1,f)" )"1" "RSP2" "Rie_sum(a,b,-gg,P,xis2,f)" )"1" case "RSP1 = -RSS1 AND RSP2 = -RSS2" )"1" "1" "RSP1" "RSP2" )"1" "1" nil nil ))nil )"2" replace "2" "Riemann?_Rie" )"2" "a" "b" "f" "-gg" )"2" "1" "P" "xis2" )nil nil )"2" nil nil ))nil ))nil ))nil ))nil )"3" replace "3" "Riemann?_Rie" )"3" "a" "b" "f" "-gg" )"3" "1" "P" "xis1" )nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" replace "2" replace "2" replace "2" "2" expand "Rie_sum" )"2" "1" "sigma_scal[below(P`length-1)]" )"1" "LAMBDA (n: below(P`length - 1)): " "-1" "P`length-2" "0" )"1" replace "1" "1" "sigma_restrict_eq[below(P`length-1)]" )"1" "1" assert )"1" "1" expand "restrict" )"1" expand "-" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "sigma_scal[below(P`length-1)]" )"1" "LAMBDA (n: below(P`length - 1)): " "-1" "P`length-2" "0" )"1" replace "1" "1" "sigma_restrict_eq[below(P`length-1)]" )"1" "1" assert )"1" "1" expand "restrict" )"1" expand "-" )"1" 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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (lemma "integral_scal_g" )"2" "-1" "a" "b" "f" "gg" )"2" assert )"2" "2" assert )"2" expand "-" )"2" expand "*" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (case "integrable?(a,b,-gg,f)" )"1" (hide-all-but (-1 1))"1" (lemma "integral_scal_g" )"1" "-1" "a" "b" "f" "-gg" )"1" assert )"1" "1" expand "-" )"1" expand "*" )"1" case "gg = (LAMBDA (x_1: real): -1 * -gg(x_1))" )"1" (assert ) nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (assert )"2" "2" "2" "2" "epsi" )"2" "2" "delta" )"2" "2" "P" )"2" assert )"2" "RSS1" "RSS2" ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.925 Sekunden
(vorverarbeitet am 2026-04-28)
¤ *© Formatika GbR, Deutschland
2026-05-26
