Quellverzeichnis series.prf
Interaktion und
(seriesnil 3374405059 ("" (subtype-tcc) nil nil ) nil nil ))nil 3249311615 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil sequences nil )"bool" series nil )"sequence[real]" series nil )"bool" convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )"real" reals nil ))nil ))nil 3298729340"" (skosimp*)"" (assert )"" (typepred "a!1" )"" (expand "conv_series?" ) (("" (propax) nil nil )) nil ))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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil sequences nil )"bool" series nil ))nil 3299339188"" (skosimp*)"" (expand "series" )"" (apply-extensionality 1 :hide? t)"" (expand "-" ) (("" (rewrite "sigma_minus" ) nil nil )) nil ))nil ))nil ))nil )"sequence[real]" series nil )nil sigma "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[T -> real]" real_fun_ops "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )nil sequences 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 ))nil 3299339288"" (skosimp*)"" (expand "series" )"" (apply-extensionality 1 :hide? t)"" (expand "+" ) (("" (rewrite "sigma_sum" ) nil nil )) nil ))nil ))nil ))nil )"sequence[real]" series nil )nil sigma "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[T -> real]" real_fun_ops "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )nil sequences 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 )nil 3299339277 ("" (postpone) nil nil ) nil shostak))nil 3299339692"" (skosimp*)"" (expand "series" )"" (apply-extensionality 1 :hide? t)"" (expand "-" ) (("" (rewrite "sigma_minus" ) nil nil )) nil ))nil ))nil ))nil )"sequence[real]" series nil )nil sigma "reals/" )"[T -> real]" real_fun_ops "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )nil sequences 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 ))nil 3299339707"" (skosimp*)"" (expand "series" )"" (apply-extensionality 1 :hide? t)"" (expand "+" ) (("" (rewrite "sigma_sum" ) nil nil )) nil ))nil ))nil ))nil )"sequence[real]" series nil )nil sigma "reals/" )"[T -> real]" real_fun_ops "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )nil sequences 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 ))nil 3299339880"" (skosimp*)"" (expand "series" )"" (expand "*" )"" (apply-extensionality 1 :hide? t)"" (lemma "sigma_scal" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"sequence[real]" series 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 )nil number_fields nil )nil sequences nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )nil sigma "reals/" )"[T -> real]" real_fun_ops "reals/" ))nil 3299339979"" (skosimp*)"" (expand "series" )"" (apply-extensionality 1 :hide? t)"" (rewrite "sigma_eq" )"" (skosimp*) (("" (inst?) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"sequence[real]" series nil )nil sigma "reals/" )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )nil sequences 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 3299339856"" (skosimp*)"" (expand "series" )"" (expand "*" )"" (apply-extensionality 1 :hide? t)"" (lemma "sigma_scal" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"sequence[real]" series 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 )nil number_fields nil )nil sequences nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil sigma "reals/" )"[T -> real]" real_fun_ops "reals/" ))nil 3299836761"" (skosimp*)"" (lemma "convergence_cauchy1" )"" (inst?)"" (assert )"" (hide -2)"" (expand "convergence" )"" (skosimp*)"" (expand "cauchy" )"" (inst - "epsilon!1" )"" (skosimp*)"" (inst 1 "n!1+1" )"" (skosimp*)"" (expand "series" )"" (inst - "i!1" "i!1-1" )"1" assert )"1" expand "sigma" -1 1)"1" (propax) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil convergence_sequences"analysis/" )"bool" convergence_sequences "analysis/" )"real" reals nil )"bool" convergence_sequences "analysis/" )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" series nil )"real" sigma "reals/" )"(strict_total_order?[real])" real_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"sequence[real]" series nil )nil sequences 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 )nil 3249311615"" (skosimp*)"" (lemma "sc_lem" ) (("" (inst?) (("" (assert ) nil nil )) nil ))nil ))nil )nil nil ))nil 3297507108"" (skosimp*)"" (lemma "conv_series_terms_to_0" )"" (inst?)"" (assert )"" (hide -2)"" (expand "convergent?" ) (("" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil series nil )"bool" convergence_sequences "analysis/" )nil sequences 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 3297504127"" (skosimp*)"" (lemma "conv_series_terms_to_0" )"" (inst?)"" (assert )"" (hide -2)"" (rewrite "limit_def" )"" (expand "convergent?" ) (("" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil series nil )nil convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )nil sequences 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 3249311615"" (skosimp*)"" (lemma "convergence_cauchy1" )"" (inst?)"" (assert )"" (hide -2)"" (lemma "convergence_cauchy2" )"" (inst?)"" (assert )"" (hide 2)"" (expand "cauchy" )"" (skosimp*)"" (inst? -)"" (skosimp*)"" (inst?)"" "" "i!1" "j!1" )"" assert )"" expand "series" )"" "i!1 = j!1" )"1" (assert ) nil nil )"2" "i!1 < j!1" )"1" rewrite "sigma_diff_neg" )"1" rewrite "sigma_diff_neg" )"1" "sigma_abs" )"1" "1" "(LAMBDA (n:nat): abs(a!1(n))) = abs(a!1)" )"1" "1" assert )"1" "sigma" )nil nil ))nil ))nil )"2" "2" "1" nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "sigma_diff" )"2" "2" assert )"2" replace -1)"2" "2" rewrite "sigma_diff" )"2" "sigma_abs" )"2" "2" assert )"2" case "(LAMBDA (n:nat): abs(a!1(n))) = abs(a!1)" )"1" replace "1" "1" assert )nil nil ))nil ))nil )"2" "2" "1" "1" nil nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil convergence_sequences"analysis/" )nil convergence_sequences"analysis/" )"real" reals nil )"bool" convergence_sequences "analysis/" )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"sequence[real]" series nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil sigma "reals/" )"(total_order?[real])" nil )"odd_int" integersnil )"real" reals nil )"posint" nil )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"nnreal" sigma_nat "reals/" )nil sigma "reals/" )"[T, T -> boolean]" equalities nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"sequence[real]" series nil )"sequence[real]" series nil )nil sequences 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 ))nil 3249311615"" (skosimp*)"" (prop)"1" (lemma "convergence_cauchy1" )"1" (inst?)"1" (assert )"1" (hide -2)"1" (expand "cauchy" )"1" (skosimp*)"1" (inst -1 "epsilon!1" )"1" (skosimp*)"1" (inst 1 "n!1+1" )"1" (skosimp*)"1" (expand "series" )"1" (inst -1 "n!2" "m!1" )"1" assert )"1" case "sigma(0, n!2, a!1) - sigma(0, m!1, a!1) = sigma(m!1+1, n!2, a!1)" )"1" replace -1)"1" "1" expand "abs" )"1" (propax) nil nil ))nil ))nil ))nil )"2" "2" "sigma_diff" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "convergence_cauchy2" )"2" (inst?)"2" (assert )"2" (hide 2)"2" (expand "cauchy" )"2" (skosimp*)"2" (inst - "epsilon!1" )"2" (skosimp*)"2" (inst 1 "N!1" )"2" (skosimp*)"2" (expand "series" )"2" (case "i!1 = j!1" )"1" replace -1)"1" assert )"1" expand "abs" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" case "i!1 < j!1" )"1" rewrite "sigma_diff_neg" )"1" "1" assert )"1" expand "abs" )"1" "1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "sigma_diff" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 )nil sequences nil )"sequence[real]" series nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil sigma "reals/" )"odd_int" integersnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )nil integers nil )nil integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" convergence_sequences "analysis/" )"real" reals nil )nil convergence_sequences"analysis/" )nil abs_lems "reals/" )nil sigma "reals/" )"real" reals nil )"bool" reals nil )nil convergence_sequences"analysis/" ))nil ))nil 3249311615"" (expand "convergent?" )"" (inst + "0" )"" (expand "convergence" )"" (skosimp*)"" (inst 1 "1" )"" (skosimp*)"" (expand "series" )"" (rewrite "sigma_const" ) (("" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"int" integers nil )"int" integers nil )"(total_order?[real])" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(strict_total_order?[real])" real_props nil )"{j: nonneg_int | j >= i}" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"sequence[real]" series nil )"nat" sigma_nat "reals/" )"nnreal" sigma_nat "reals/" )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" ))nil ))nil 3249311615"" (rewrite "zero_series_conv" ) nil nil )nil series nil )) nil ))nil 3249311615"" (rewrite "limit_def" )"1" (expand "convergence" )"1" (skosimp*)"1" (inst 1 "1" )"1" (skosimp*)"1" (expand "series" )"1" (rewrite "sigma_const" ) (("1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (rewrite "zero_series_conv" ) nil nil )) nil ))nil )"bool" convergence_sequences "analysis/" )"nnreal" sigma_nat "reals/" )"nat" sigma_nat "reals/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"{j: nonneg_int | j >= i}" nil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"(total_order?[real])" nil )"int" integers nil )"int" integers nil )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"sequence[real]" series nil )"bool" convergence_sequences "analysis/" )nil sequences 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 convergence_sequences "analysis/" ))nil ))nil 3249311615"" (skosimp*)"" (case-replace "N!1 = 0" )"1" (case-replace "a!1 = (LAMBDA n: a!1(n + 0))" )"1" (assert ) nil nil )"2" (hide 2) (("2" (apply-extensionality :hide? t) nil nil ))nil ))nil )"2" (expand "series" )"2" (expand "convergent?" )"2" (skosimp*)"2" (name "AA" "sigma(0, N!1-1, a!1)" )"1" (inst + "l!1-AA" )"1" (expand "convergence" )"1" (skosimp*)"1" (inst -2 "epsilon!1" )"1" (skosimp*)"1" (inst + "n!1" )"1" (skosimp*)"1" (lemma "sigma_shift" )"1" "1" assert )"1" replace -1 * rl)"1" "1" replace -1 * rl)"1" "N!1+i!1" )"1" assert )"1" "sigma_split" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil 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]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil sequences nil )"nonneg_int" nil )"bool" convergence_sequences "analysis/" )"[numfield, numfield -> numfield]" number_fields nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"int" integers nil )"(total_order?[real])" nil )"real" reals nil )"bool" convergence_sequences "analysis/" )nil real_types nil )"bool" reals nil )nil real_types nil )nil sigma_nat "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sigma "reals/" )"odd_int" integersnil )"odd_int" integers nil )"real" reals nil )"sequence[real]" series nil ))nil ))nil 3249311615"" (skosimp*)"" (case-replace "N!1 = 0" )"1" (case-replace "a!1 = (LAMBDA n: a!1(n + 0))" )"1" (assert ) nil nil )"2" (hide 2) (("2" (apply-extensionality :hide? t) nil nil ))nil ))nil )"2" (expand "series" )"2" (expand "convergent?" )"2" (skosimp*)"2" (name "AA" "sigma(0, N!1-1, a!1)" )"1" (inst + "l!1+AA" )"1" (expand "convergence" )"1" (skosimp*)"1" (inst -2 "epsilon!1" )"1" (skosimp*)"1" (inst + "n!1+N!1" )"1" (skosimp*)"1" (inst -2 "i!1-N!1" )"1" assert )"1" assert )"1" "sigma_shift" )"1" "1" assert )"1" replace -1 * rl)"1" "1" "sigma_split" )"1" "a!1" "i!1" "0" "N!1-1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) 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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil sequences nil )"nonneg_int" nil )"bool" convergence_sequences "analysis/" )"[numfield, numfield -> numfield]" number_fields nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"int" integers nil )"(total_order?[real])" nil )"real" reals nil )"bool" convergence_sequences "analysis/" )nil real_types nil )"bool" reals nil )nil real_types nil )"nat" series nil )"nat" series nil )"odd_int" integers nil )nil sigma "reals/" )"odd_int" integersnil )"int" integers nil )nil sigma_nat "reals/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"sequence[real]" series nil ))nil ))nil 3298646790"" (skosimp*)"" (prop)"1" (lemma "tail_series_conv" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil )"2" (lemma "tail_series_conv2" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))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 )nil sequences nil )nil series nil )nil series nil ))nil 3249311615"" (skosimp*)"" (lemma "tail_series_conv" )"" (inst?)"" (inst -1 "N!1" )"" (assert )"" (hide -2)"" (lemma "tail_series_conv2" )"" (inst -1 "N!1" "b!1" )"" (assert )"" (hide 2)"" "series(LAMBDA n: a!1(n + N!1)) = series(LAMBDA n: b!1(n + N!1))" )"" (hide -1 2)"" (expand "series" )"" (apply-extensionality 1 :hide? t)"" rewrite "sigma_eq" )"" "" "" "" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil series nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"sequence[real]" series nil )"[T, T -> boolean]" equalities nil )"nonneg_int" nil )nil series nil )nil sequences 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 ))nil 3297672929"" (skosimp*)"" (expand "series" )"" (case "m!1 = 0" )"1" (ground) nil nil )"2" (prop)"1" (expand "convergent?" )"1" (skosimp*)"1" (inst + "l!1 - sigma(0, m!1-1, a!1)" )"1" (expand "convergence" )"1" (skosimp*)"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "n!1" )"1" (skosimp*)"1" (case "m!1 - 1 >= i!1" )"1" expand "sigma" 1 2)"1" assert )"1" "m!1-1" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" rewrite "sigma_split" :dir rl)"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (expand "convergent?" )"2" (skosimp*)"2" (inst + "l!1 + sigma(0, m!1-1, a!1)" )"1" (expand "convergence" )"1" (skosimp*)"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "max(n!1,m!1)" )"1" (skosimp*)"1" (expand "max" )"1" "1" "1" "sigma_split" )"1" "a!1" "i!1" "0" "m!1-1" )"1" assert )"1" replace -1)"1" assert )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "sigma_split" )"2" "a!1" "i!1" "0" "m!1-1" )"2" assert )"2" replace -1)"2" assert )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"sequence[real]" series nil )"sequence[real]" series nil )"real" reals nil )"bool" convergence_sequences "analysis/" )nil real_types nil )"bool" reals nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"odd_int" integersnil )"odd_int" integers nil )nil sigma "reals/" )nil sequences nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )"nat" series nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"int" integers nil )"real" reals nil )"(total_order?[real])" nil )"bool" convergence_sequences "analysis/" )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"{k: nat | i <= k AND j <= k}" nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields 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]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil ))nil 3299840486"" (skosimp*)"" (case-replace "c!1 = 0" )"1" (hide -1 -2)"1" (expand "*" )"1" (assert )"1" (lemma "zero_series_conv" )"1" case "(LAMBDA (x: nat): 0 * series(a!1)(x)) = series(LAMBDA n: 0)" )"1" (replace -1 +) (("1" (propax) nil nil )) nil )"2" (hide -1 2)"2" (apply-extensionality 1 :hide? t)"2" (expand "series" )"2" (assert )"2" (lemma "sigma_const" )"2" (inst?)"2" (lift-if) (("2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "convergent?" )"2" (skosimp*)"2" (inst + "c!1*l!1" )"2" (expand "convergence" )"2" (skosimp*)"2" (inst -1 "epsilon!1/abs(c!1)" )"1" (skosimp*)"1" (inst + "n!1" )"1" (skosimp*)"1" (inst?)"1" (assert )"1" (assert )"1" expand "*" )"1" "c!1 * series(a!1)(i!1) - c!1 * l!1 = c!1 * (series(a!1)(i!1) - l!1)" )"1" "1" rewrite "abs_mult" )"1" "both_sides_div_pos_lt1" )"1" "abs(c!1)" "abs(c!1) * abs((series(a!1)(i!1) - l!1)) " "epsilon!1" )"1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (typepred "epsilon!1" )"2" (rewrite "pos_div_ge" )"1" (rewrite "pos_div_gt" )"1" (grind) nil nil )"2" (hide 2) (("2" (grind) nil nil )) nil ))nil )"2" (hide 2) (("2" (grind) nil nil )) nil ))nil ))nil ))nil )"3" (hide 3) (("3" (grind) 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 )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )nil series nil )nil sigma "reals/" )"int" integers nil )"int" integers nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"(total_order?[real])" nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nnreal" sigma_nat "reals/" )"nat" sigma_nat "reals/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil sequences nil )"sequence[real]" series nil )"real" reals nil )"bool" convergence_sequences "analysis/" )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"boolean" notequal nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" series nil )"posreal" series nil )nil real_types nil )"bool" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"odd_int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"nnreal" nil )"real" reals nil )nil real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil real_props nil )nil real_props nil )nil reals nil )"bool" convergence_sequences "analysis/" ))nil ))nil 3299840513"" (skosimp*)"" (prop)"1" (lemma "scal_series_conv" )"1" (inst - "(LAMBDA (x: nat): cnz!1 * a!1(x))" "1/cnz!1" )"1" (expand "*" )"1" (lemma "series_scal" )"1" "(LAMBDA (x: nat): cnz!1 * a!1(x))" "1/cnz!1" )"1" (assert )"1" (expand "*" )"1" (replace -1)"1" (assert )"1" (hide -1)"1" "(LAMBDA n: 1 / cnz!1 * (cnz!1 * a!1(n))) = a!1" )"1" (assert )"1" "1" "series_scal" )"1" "1" expand "*" )"1" replace -1)"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (apply-extensionality 1 :hide? t) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "scal_series_conv" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil )"nzreal" nil )"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]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil sequences nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil reals nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil series nil )"[T, T -> boolean]" equalities nil )"[T -> real]" real_fun_ops "reals/" )nil series nil ))nil )nil 3297419186"" (skosimp*)"" (prop)"1" (lemma "convergent_scal" )"1" (inst - "(LAMBDA (x: nat): cnz!1 * a!1(x))" "1/cnz!1" )"1" (expand "*" )"1" (lemma "series_scal" )"1" "(LAMBDA (x: nat): cnz!1 * a!1(x))" "1/cnz!1" )"1" (assert )"1" (expand "*" )"1" (replace -1)"1" (assert )"1" (hide -1)"1" "(LAMBDA n: 1 / cnz!1 * (cnz!1 * a!1(n))) = a!1" )"1" (assert )"1" "1" "series_scal" )"1" "1" expand "*" )"1" replace -1)"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (apply-extensionality 1 :hide? t) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "convergent_scal" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil )nil nil )nil 3297418252"" (skosimp*)"" (prop)"1" (lemma "convergent_scal" )"1" (inst - "(LAMBDA (x: nat): c!1 * a!1(x))" "1/c!1" )"1" (expand "*" )"1" (lemma "series_scal" )"1" (inst - "(LAMBDA (x: nat): c!1 * a!1(x))" "1/c!1" )"1" (assert )"1" (expand "*" )"1" (replace -1)"1" (assert )"1" (hide -1)"1" "(LAMBDA n: 1 / c!1 * (c!1 * a!1(n))) = a!1" )"1" (assert )"1" "1" "series_scal" )"1" "1" expand "*" )"1" replace -1)"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (apply-extensionality 1 :hide? t)"2" (postpone) nil nil )) nil )"3" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil )"2" (lemma "convergent_scal" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil )nil shostak))nil 3249311615"" (assert )"" (skosimp*)"" (assert )"" (lemma "conv_series_shift" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil nil ))nil 3374405059"" (skosimp*)"" (lemma "conv_series_shift" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )nil series nil )nil sequences nil )nil integers nil )"bool" reals nil )nil integers 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 ))nil 3249311615"" (skosimp*)"" (rewrite "limit_def" )"1" (name "LSH" "limit(series(LAMBDA n: a!1(pn!1 + n)))" )"1" (replace -1)"1" (rewrite "limit_def" )"1" (hide -2)"1" (expand "convergence" )"1" (skosimp*)"1" (inst -1 "epsilon!1" )"1" (skosimp*)"1" (inst + "n!1+pn!1" )"1" (skosimp*)"1" (inst -1 "i!1-pn!1" )"1" (assert )"1" expand "series" )"1" "sigma_split" )"1" "a!1" "i!1" "0" "pn!1-1" )"1" assert )"1" replace -1)"1" "1" assert )"1" "sigma_shift" )"1" "a!1" "i!1-pn!1" "0" "pn!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "tail_series_conv" ) nil nil ))nil ))nil )"2" (rewrite "tail_series_conv" ) nil nil ))nil )"2" (rewrite "tail_series_conv" ) nil nil ))nil ))nil )"int" integers nil )"posint" nil )"real" reals nil )nil convergence_sequences "analysis/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil 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 )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"bool" reals nil )nil integers nil )nil sequences nil )"bool" convergence_sequences "analysis/" )"real" convergence_sequences "analysis/" )"sequence[real]" series nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil series nil )nil sigma "reals/" )"odd_int" integersnil )nil sigma_nat "reals/" )"int" integers nil )"real" reals nil )"odd_int" integers nil )"posnat" series nil )"nat" series nil )"(total_order?[real])" nil )nil real_types nil )nil real_types nil )"bool" convergence_sequences "analysis/" )"real" reals nil )"[T, T -> boolean]" equalities nil )"posint" nil ))nil ))nil 3249311615"" (skosimp*)"" (lemma "limit_def" )"" (inst -1 "limit(a!1)" "a!1" )"" (assert )"" (expand "convergence" )"" (inst -1 "-limit(a!1)/2" )"" (skosimp*)"" (inst -1 "n!1" )"" (assert ) (("" (grind :exclude "limit" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil convergence_sequences "analysis/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" 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 )"[numfield -> numfield]" number_fields nil )NOT const-decl "[bool -> bool]" booleans nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(strict_total_order?[real])" real_props nil )"bool" convergence_sequences "analysis/" )"real" reals nil )"real" convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )nil sequences 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 ))nil 3299340007"" (skosimp*)"" (lemma "end_series_conv" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )nil series nil )nil sequences 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 3299339903"" (skosimp*)"" (copy -1)"" (hide -1)"" (expand "series" )"" (lemma "sigma_first" )"" (inst?)"" "(LAMBDA (n: nat): sigma(0, n, a!1)) = LAMBDA (n: nat): a!1(0) + sigma(1, n, a!1))") "1" (hide -1 -2)"1" (lemma "limit_sum" )"1" "(LAMBDA (n: nat): sigma(1, n, a!1))" "(LAMBDA (n: nat): a!1(0))" )"1" (expand "+" )"1" (replace -1)"1" (hide -1)"1" (lemma "limit_const" )"1" "a!1(0)" )"1" expand "const_fun" )"1" replace -1)"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "convergent_const" )"2" (expand "const_fun" )"2" (inst?) nil nil )) nil ))nil ))nil )"3" (case "convergent?(series(a!1))" )"1" (hide 2)"1" (lemma "end_series_conv" )"1" (inst?)"1" "1" )"1" assert )"1" expand "series" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 3)"2" (reveal -5) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (apply-extensionality 1 :hide? t)"2" (inst?)"2" (assert )"2" (expand "sigma" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"sequence[real]" series nil )"sequence[real]" series nil )"int" integers nil )"even_int" integersnil )"odd_int" integersnil )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sequences nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"bool" convergence_sequences "analysis/" )"sequence[real]" series nil )nil convergence_ops "analysis/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )nil convergence_ops "analysis/" )nil series nil )nil convergence_ops "analysis/" )"real" reals nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil sigma "reals/" )"real" sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )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 ))nil 3299340007"" (skosimp*)"" (expand "conv_series?" ) (("" (propax) nil nil )) nil )) nil )"bool" series nil )) shostak))nil 3299340007"" (skosimp*)"" (expand "conv_series?" )"" (lemma "conv_series_scal" )"" (inst?)"" (inst - "c!1" )"1" (assert )"1" (lemma "end_series_conv" )"1" (inst?)"1" (assert )"1" (rewrite "series_scal" )"1" (assert )"1" (hide -1)"1" (lemma "end_series_conv" )"1" (assert )"1" "(LAMBDA n: c!1 * a!1(n))" "k!1" )"1" assert )"1" expand "series" )"1" expand "*" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (flatten)"2" (replace -1)"2" (expand "*" )"2" (hide -)"2" (lemma "end_series_conv" )"2" (inst?)"2" (assert )"2" (hide 2)"2" "zero_series_conv" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" series 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 )nil sequences nil )nil series nil )nil series nil )"[T -> real]" real_fun_ops "reals/" )"sequence[real]" series nil )"sequence[real]" series nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )nil series nil )nil reals nil )"real" series nil )"boolean" notequal nil )nil series nil ))nil 3299339613"" (skosimp*)"" (expand "inf_sum" )"" (lemma "limit_scal" )"" (inst - "c!1" "series(a!1,k!1)" )"" (assert )"" (lemma "series_m_scal" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"real" series 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 )nil sequences nil )"bool" convergence_sequences "analysis/" )"sequence[real]" series nil )nil series nil )"real" reals nil )nil convergence_ops "analysis/" ))nil ))nil 3249311615"" (skosimp*)"" (lemma "convergence_cauchy1" )"" (inst -1 "series(b!1)" )"" (assert )"" (lemma "convergence_cauchy2" )"" (inst -1 "series(a!1)" )"" (assert )"" (hide -2 2)"" (expand "cauchy" )"" (skosimp*)"" (inst? -)"" (skosimp*)"" (inst?)"" (skosimp*)"" "i!1" "j!1" )"" assert )"" "i!1 = j!1" )"1" (assert ) nil nil )"2" expand "series" )"2" case "i!1 < j!1" )"1" rewrite "sigma_diff_neg" +)"1" rewrite "sigma_diff_neg" )"1" "sigma_abs" )"1" "1" "sigma_abs_bnd" )"1" "a!1" "b!1" "j!1" "1+i!1" )"1" "1" "abs(-sigma(1 + i!1, j!1, a!1)) = abs(sigma(1 + i!1, j!1, a!1))" )"1" "1" case "sigma(1 + i!1, j!1, b!1) <= abs(-sigma(1 + i!1, j!1, b!1))" )"1" assert )nil nil )"2" "2" "sigma" )nil nil ))nil ))nil ))nil )"2" "2" "sigma" )nil nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "sigma_diff" )"2" rewrite "sigma_diff" )"2" "sigma_abs" )"2" "2" "sigma_abs_bnd" )"2" "a!1" "b!1" "i!1" "1+j!1" )"2" "1" case "sigma(1 + i!1, j!1, b!1) <= abs(sigma(1 + i!1, j!1, b!1))" )"1" assert )nil nil )"2" "2" "sigma" )nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil convergence_sequences"analysis/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )"posint" nil )"real" reals nil )"odd_int" integersnil )"(total_order?[real])" nil )nil sigma "reals/" )nil sigma "reals/" )"nnreal" sigma_nat "reals/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" sigma "reals/" )nil integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" convergence_sequences "analysis/" )"real" reals nil )nil convergence_sequences"analysis/" )"sequence[real]" series nil )nil sequences 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 ))nil 3249311615"" (skosimp*)"" (lemma "tail_series_conv2" )"" (inst -1 "N!1" "a!1" )"" (assert )"" (hide 2)"" (lemma "tail_series_conv" )"" (inst -1 "N!1" "b!1" )"" (split -1)"1" (hide -2)"1" (lemma "comparison_test" )"1" "(LAMBDA n: a!1(n + N!1))" "(LAMBDA n: b!1(n + N!1))" )"1" (assert )"1" (hide -1 2)"1" (skosimp*)"1" "n!1+N!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil series nil )nil series nil )nil series nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_int" nil )nil sequences 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 ))nil 3299582002"" (skosimp*)"" (expand "inf_sum" )"" (case-replace "series(b!1, m!1) = series(a!1, m!1)" )"" (assert )"" (hide 2)"" (expand "series" )"" (apply-extensionality 1 :hide? t)"" (rewrite "sigma_eq" )"" (skosimp*)"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" series nil )nil sigma "reals/" )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )"sequence[real]" series nil )"[T, T -> boolean]" equalities nil )nil sequences 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 ))nil 3299340008"" (skosimp*)"" (lemma "comparison_test_gen" )"" (expand "conv_series?" )"" (inst - "a!1" "b!1" )"" (assert )"" (lemma "end_series_conv" )"" (inst?)"" (assert )"" (split -2)"1" (lemma "end_series_conv" )"1" (inst - "a!1" "m!1" )"1" (assert ) nil nil )) nil ))nil )"2" (inst + "m!1" )"2" (skosimp*) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil series 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 )nil sequences nil )nil series nil )"nat" series nil )"nat" series nil )nil integers nil )"(total_order?[real])" nil )"bool" series nil ))nil 3299340008"" (skosimp*)"" (expand "conv_series?" ) (("" (propax) nil nil )) nil )) nil )"bool" series nil )) shostak))nil 3299332283"" (skosimp*)"" (expand "inf_sum" )"" (lemma "comparison_test_gen" )"" (inst - "a!1" "b!1" )"" (lemma "end_series_conv" )"" (inst?)"" (assert )"" (split -2)"1" (lemma "end_series_conv" )"1" (inst - "a!1" "m!1" )"1" (assert )"1" (name "LA" "limit(series(a!1, m!1))" )"1" (replace -1)"1" (name "LB" "limit(series(b!1, m!1))" )"1" replace -1)"1" "cnv_seq_order" )"1" "LA" "LB" "series(a!1,m!1)" "series(b!1,m!1)" )"1" assert )"1" "1" "limit_equiv" )"1" "1" (assert ) nil nil ))nil ))nil )"2" "limit_equiv" )"2" "2" (assert ) nil nil ))nil ))nil )"3" "3" "3" expand "series" )"3" "sigma_le" )"3" "3" assert )"3" "3" "3" expand "abs" )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst + "m!1" )"2" (skosimp*) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" series 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 )nil sequences nil )"sequence[real]" series nil )"real" convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )"[T, T -> boolean]" equalities nil )nil convergence_ops "analysis/" )"sequence[real]" series nil )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"(total_order?[real])" nil )nil sigma "reals/" )nil convergence_ops "analysis/" )"nat" series nil )"nat" series nil )"(total_order?[real])" nil )nil series nil )nil series nil ))nil 3299840577"" (skosimp*)"" (expand "inf_sum" )"" (lemma "comparison_test_gen" )"" (inst - "a!1" "b!1" )"" (lemma "end_series_conv" )"" (inst?)"" (assert )"" (split -2)"1" (lemma "end_series_conv" )"1" (inst - "a!1" "m!1" )"1" (assert )"1" (hide -2 -3)"1" (name "LA" "limit(series(a!1, m!1))" )"1" (replace -1)"1" "LB" "limit(series(b!1, m!1))" )"1" replace -1)"1" case "LA <= LB AND -LB <= LA" )"1" expand "abs" )"1" "1" (ground) nil nil ))nil ))nil )"2" "2" "1" "cnv_seq_order" )"1" "LA" "LB" "series(a!1,m!1)" "series(b!1,m!1)" )"1" assert )"1" "1" "limit_equiv" )"1" "1" assert )nil nil ))nil ))nil )"2" "limit_equiv" )"2" "2" assert )nil nil ))nil ))nil )"3" "3" "3" expand "series" )"3" "sigma_le" )"3" "3" assert )"3" "3" "3" expand "abs" )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "cnv_seq_order" )"2" "-LB" "LA" "-series(b!1,m!1)" "series(a!1,m!1)" )"2" assert )"2" "1" "conv_series_scal" )"1" "1" "-1" )"1" assert )"1" "inf_sum_scal" )"1" "b!1" "-1" "m!1" )"1" assert )"1" expand "inf_sum" )"1" "series_m_scal" )"1" "1" assert )"1" replace "1" replace "1" "limit_equiv" )"1" "1" assert )"1" "-series(b!1, m!1) = -1*series(b!1, m!1)" )"1" assert )"1" "1" "end_series_conv" )"1" "-b!1" "m!1" )"1" "-1 * series(b!1) = series(-b!1)" )"1" assert )"1" "series(-b!1, m!1) = (-1 * series(b!1, m!1))" )"1" expand "*" )"1" "1" expand "-" )"1" assert )"1" "1" expand "series" )"1" "sigma_scal" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "series" )"2" assert )"2" expand "*" )"2" "2" "sigma_scal" )"2" "2" assert )"2" expand "-" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "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 ))nil ))nil ))nil ))nil )"2" "limit_equiv" )"2" "2" assert )nil nil ))nil ))nil )"3" "limit_equiv" )"3" "3" assert )"3" "3" "3" expand "series" )"3" expand "-" )"3" "-sigma(m!1, n!1, b!1) = sigma(m!1, n!1, -b!1)" )"1" "1" "sigma_le" )"1" "1" assert )"1" "1" "1" expand "-" )"1" expand "abs" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "sigma_scal" )"2" "2" "-1" )"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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst + "m!1" )"2" (skosimp*) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" series 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 )nil sequences nil )nil series nil )"odd_int" integers nil )nil reals nil )"boolean" notequal nil )nil series nil )nil series nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"real" sigma "reals/" )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"sequence[real]" series nil )"[T -> real]" real_fun_ops "reals/" )nil convergence_ops "analysis/" )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil integers nil )nil sigma "reals/" )nil convergence_ops "analysis/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(strict_total_order?[real])" real_props nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" reals nil )"sequence[real]" series nil )"real" convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )"[T, T -> boolean]" equalities nil )"nat" series nil )"nat" series nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil series nil )nil series nil ))nil )nil 3299500011"" (skosimp*)"" (expand "inf_sum" )"" (lemma "comparison_test_gen" )"" (inst - "a!1" "b!1" )"" (lemma "end_series_conv" )"" (inst?)"" (assert )"" (split -2)"1" (lemma "end_series_conv" )"1" (inst - "a!1" "m!1" )"1" (assert )"1" (hide -2 -3)"1" (name "LA" "limit(series(a!1, m!1))" )"1" (replace -1)"1" "LB" "limit(series(b!1, m!1))" )"1" replace -1)"1" case "LA <= LB AND -LB <= LA" )"1" expand "abs" )"1" "1" (ground) nil nil ))nil ))nil )"2" "2" "1" "cnv_seq_order" )"1" "LA" "LB" "series(a!1,m!1)" "series(b!1,m!1)" )"1" assert )"1" "1" "limit_equiv" )"1" "1" assert )nil nil ))nil ))nil )"2" "limit_equiv" )"2" "2" assert )nil nil ))nil ))nil )"3" "3" "3" expand "series" )"3" "sigma_le" )"3" "3" assert )"3" "3" "3" expand "abs" )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "cnv_seq_order" )"2" "-LB" "LA" "-series(b!1,m!1)" "series(a!1,m!1)" )"2" assert )"2" "1" "convergent_scal" )"1" "1" "-1" )"1" assert )"1" "inf_sum_scal" )"1" "b!1" "-1" "m!1" )"1" assert )"1" expand "inf_sum" )"1" "series_m_scal" )"1" "1" assert )"1" replace "1" replace "1" "limit_equiv" )"1" "1" assert )"1" "-series(b!1, m!1) = -1*series(b!1, m!1)" )"1" assert )"1" "1" "end_series_conv" )"1" "-b!1" "m!1" )"1" "-1 * series(b!1) = series(-b!1)" )"1" assert )"1" "series(-b!1, m!1) = (-1 * series(b!1, m!1))" )"1" expand "*" )"1" "1" expand "-" )"1" assert )"1" "1" expand "series" )"1" "sigma_scal" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "series" )"2" assert )"2" expand "*" )"2" "2" "sigma_scal" )"2" "2" assert )"2" expand "-" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "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 ))nil ))nil ))nil ))nil )"2" "limit_equiv" )"2" "2" assert )nil nil ))nil ))nil )"3" "limit_equiv" )"3" "3" assert )"3" "3" "3" expand "series" )"3" expand "-" )"3" "-sigma(m!1, n!1, b!1) = sigma(m!1, n!1, -b!1)" )"1" "1" "sigma_le" )"1" "1" assert )"1" "1" "1" expand "-" )"1" expand "abs" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "sigma_scal" )"2" "2" "-1" )"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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst + "m!1" )"2" (skosimp*) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" sigma "reals/" )nil sigma "reals/" )nil convergence_ops "analysis/" )nil sigma "reals/" )nil convergence_ops "analysis/" )"real" convergence_sequences "analysis/" ))nil ))nil 3299583110"" (skosimp*)"" (expand "conv_series?" )"" (lemma "convergent_abs" )"" (inst - "a!1" )"" (assert )"" (lemma "end_series_conv" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" series 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 )nil sequences nil )nil series nil )nil series nil ))nil 3299583110"" (skosimp*)"" (expand "conv_series?" )"" (lemma "end_series_conv" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"bool" series 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 )nil sequences nil )"sequence[real]" series nil )nil series nil ))nil 3299581718"" (skosimp*)"" (lemma "inf_sum_le_abs" )"" (inst?)"" (assert )"" (hide 2)"" (prop)"1" (skosimp*) (("1" (grind) nil nil )) nil )"2" (lemma "end_series_conv" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil series nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"int" integers nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" sigma "reals/" )"sequence[real]" series nil )"bool" convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )NOT const-decl "[bool -> bool]" booleans nil )nil series nil )"sequence[real]" series nil )nil sequences 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 )nil 3299581703 ("" (postpone) nil nil ) nil nil 3249311615"" (skosimp*)"" (expand "convergent?" )"" (skosimp*)"" (inst 1 "l!1+l!2" )"" (expand "convergence" )"" (skosimp*)"" (inst - "epsilon!1/2" )"" (inst - "epsilon!1/2" )"" (skosimp*)"" (inst + "max(n!1,n!2)" )"" (skosimp*)"" (inst - "i!1" )"" (inst - "i!1" )"" (split -1)"1" "1" "1" expand "series" )"1" "sigma_sum" )"1" "1" "a!1" )"1" expand "+ " )"1" replace -1 * rl)"1" "1" "sigma" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" convergence_sequences "analysis/" )"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 )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"{k: nat | i <= k AND j <= k}" nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"(total_order?[real])" nil )nil sigma "reals/" )"real" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[T -> real]" real_fun_ops "reals/" )nil sequences nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"sequence[real]" series nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"posreal" nil )"bool" convergence_sequences "analysis/" )"real" reals nil ))nil ))nil 3249311615"" (skosimp*)"" (lemma "cnv_seq_sum" )"" (inst -1 "l1!1" "l2!1" "series(a!1)" "series(b!1)" )"" (assert )"" (hide -2 -3)"" (expand "series" )"" case "(LAMBDA (n: nat): sigma(0, n, a!1)) + LAMBDA (n: nat): sigma(0, n, b!1)) = (LAMBDA (n: nat): sigma(0, n, a!1 + b!1))") "1" (replace -1) (("1" (propax) nil nil )) nil )"2" (hide -1 2)"2" (expand "+ " )"2" (apply-extensionality 1 :hide? t)"2" (lemma "sigma_sum" ) (("2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil convergence_ops "analysis/" )"real" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil sigma "reals/" )"[T, T -> boolean]" equalities nil )"[T -> real]" real_fun_ops "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )"sequence[real]" series nil )nil sequences 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 ))nil 3249311615"" (skosimp*)"" (expand "conv_series?" )"" (lemma "series_sum_convergence" )"" (inst?)"" (expand "convergent?" )"" (skosimp*)"" (inst 1 "l!1+l!2" )"" (inst -1 "l!2" "l!1" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" series 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 )nil sequences nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"bool" convergence_sequences "analysis/" )nil series nil ))nil ))nil 3298728979 ("" (subtype-tcc) nil nil )"sequence[real]" series nil )"bool" convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )"bool" series nil )"real" reals nil ))nil 3298728979 ("" (subtype-tcc) nil nil )"sequence[real]" series nil )"bool" convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )"bool" series nil )"real" reals nil ))nil 3249311615"" (skosimp*)"" (expand "inf_sum" )"" (rewrite "limit_def" )"1" (lemma "series_sum_convergence" )"1" (inst?)"1" (assert )"1" (hide 2)"1" (expand "convergent?" )"1" (skosimp*)"1" (split)"1" (hide -2)"1" (lemma "limit_def" )"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (hide -1)"2" (lemma "limit_def" )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "convergent?" )"2" (skosimp*)"2" (inst 1 "l!1+l!2" )"2" (rewrite "series_sum_convergence" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" series nil )nil series nil )"[T -> real]" real_fun_ops "reals/" )"sequence[real]" series nil )"real" convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )nil sequences nil )nil naturalnumbers nil )"bool" reals nil )nil booleans 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 )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil convergence_sequences "analysis/" )"real" reals nil ))nil ))nil 3249311615 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3249311615"" (skosimp*)"" (lemma "decreasing_bounded_convergence" )"" (expand "convergent?" )"" case "bounded_below?[nat]((LAMBDA (n: nat): abs(x!1) ^ n))" )"1" (inst - "(LAMBDA (n: nat): abs(x!1) ^ n)" )"1" (inst + "inf((LAMBDA (n: nat): abs(x!1) ^ n))" )"1" (assert )"1" (hide -1 2)"1" (expand "decreasing?" )"1" (skosimp*)"1" (case-replace "x!1 = 0" )"1" (expand "abs" 1)"1" (assert )"1" (expand "^" )"1" expand "expt" )"1" assert )"1" "1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "both_sides_expt_lt1_le" )"2" (inst?)"1" (assert ) nil nil )"2" (hide -2 3) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" (expand "bounded_below?" )"2" (inst + "0" )"2" (skosimp*)"2" (lemma "expt_pos" )"2" (inst?)"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil "analysis/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" real_fun_preds "reals/" )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 )"real" real_fun_supinf "analysis/" )nil exponentiation nil )nil real_types nil )"bool" reals nil ) (> const-decl "bool" reals nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"nat" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"real" exponentiation nil )nil abs_lems "reals/" )"(total_order?[real])" nil )"nat" exponentiation nil )"{j: nonneg_int | j >= i}" nil )"[T, T -> boolean]" equalities nil )"bool" real_fun_preds "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sequences nil )"real" series nil )"nnreal" exponentiation nil )nil abs_lems "reals/" )nil exponentiation nil )"bool" convergence_sequences "analysis/" ))nil ))nil 3249311615"" (skosimp*) (("" (rewrite "abs_x_to_n_conv" ) nil nil )) nil )nil series nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))nil ))nil 3249311615"" (skosimp*)"" (name "LL" "limit(LAMBDA (n: nat): abs(x!1) ^ n)" )"1" case "convergent?(abs(x!1) * (LAMBDA (n: nat): abs(x!1) ^ n))" )"1" case "abs(x!1)*LL = limit(abs(x!1) * (LAMBDA (n: nat): abs(x!1) ^ n))" )"1" case "abs(x!1) * (LAMBDA (n: nat): abs(x!1) ^ n) = (LAMBDA (n: nat): abs(x!1) ^ (n+1))" )"1" "limit(abs(x!1) * (LAMBDA (n: nat): abs(x!1) ^ n)) = limit(LAMBDA (n: nat): abs(x!1) ^ (n+1))" )"1" (hide -2)"1" "limit(LAMBDA (n: nat): abs(x!1) ^ (n+1)) = limit(LAMBDA (n: nat): abs(x!1) ^ n)" )"1" (hide -1 -2 -4)"1" (replace -2)"1" (hide -2)"1" (lemma "both_sides_times1" )"1" (inst?)"1" (inst -1 "1" )"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 -2 2)"2" (rewrite "limit_def" )"1" (replace -2)"1" (expand "convergence" )"1" (skosimp*)"1" (rewrite "limit_def" -)"1" expand "convergence" )"1" "epsilon!1" )"1" "1" "n!1+1" )"1" "1" "i!1+1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "*" )"2" (hide 2)"2" case "(LAMBDA (x: nat): abs(x!1) * abs(x!1) ^ x) = (LAMBDA (n: nat): abs(x!1) ^ (1 + n))" )"1" (assert ) nil nil )"2" (hide -1 -2 -3 2 3)"2" "2" expand "^" )"2" expand "expt" 1 2)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide -1 -2 -4 2)"3" case "(LAMBDA (n: nat): abs(x!1) ^ (1 + n)) = abs(x!1) * (LAMBDA (n: nat): abs(x!1) ^ n)" )"1" (replace -1 * rl) (("1" (propax) nil nil ))nil )"2" (hide -1 -2 2)"2" (expand "*" )"2" (apply-extensionality 1 :hide? t)"2" (expand "^" )"2" expand "expt" 1 1)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (hide -1 -2 -3 2)"3" (lemma "convergent_scal" )"3" (lemma "abs_x_to_n_conv" )"3" (inst?)"3" (inst?)"3" (inst - "abs(x!1)" )"3" (assert )"3" (hide -1 -3)"3" expand "*" )"3" expand "^" )"3" expand "expt" 1)"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 -2 -3 2)"2" (expand "*" )"2" (apply-extensionality 1 :hide? t)"2" (expand "^" )"2" (expand "expt" 1 2) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" (lemma "limit_scal" )"2" (replace -2 * rl)"2" (hide -2)"2" (inst?)"1" (assert ) nil nil )"2" (hide 2)"2" (rewrite "abs_x_to_n_conv" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"3" (propax) nil nil ))nil )"2" (hide -1 2)"2" (lemma "convergent_scal" )"2" (lemma "abs_x_to_n_conv" )"2" (inst?)"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (rewrite "abs_x_to_n_conv" ) nil nil )) nil ))nil ))nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )nil sequences 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 )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"nnreal" exponentiation nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"int" integers nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )nil reals nil )"real" series nil )nil convergence_sequences "analysis/" )"real" reals nil )"bool" convergence_sequences "analysis/" )nil real_types nil )"bool" reals nil )"posint" nil )"real" exponentiation nil )"nnreal" nil )nil convergence_ops "analysis/" )"nnreal" exponentiation nil )nil series nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )nil convergence_ops "analysis/" )"real" series nil )"[T -> real]" real_fun_ops "reals/" ))nil ))nil 3249311615 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3249311615"" (skosimp*)"" (lemma "abs_x_to_n_conv" )"" (inst?)"" (assert )"" (expand "convergent?" )"" (skosimp*)"" (inst + "l!1" )"" (case-replace "l!1 = 0" )"1" (expand "convergence" )"1" (skosimp*)"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "n!1" )"1" (skosimp*)"1" "1" assert )"1" "1" "abs(x!1 ^ i!1) = abs(x!1)^i!1" )"1" "1" expand "abs" )"1" "1" (ground) nil nil ))nil ))nil ))nil )"2" "2" rewrite "abs_hat_nat" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "cnv_seq_abs_x_to_n" )"2" (inst?)"2" (assert )"2" (rewrite "limit_def" )"2" (lemma "unique_limit" )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil series nil )"nnreal" exponentiation nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"[T, T -> boolean]" equalities nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" reals nil )nil exponentiation nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" convergence_sequences "analysis/" )nil series nil )nil convergence_sequences "analysis/" )nil sequences nil )nil convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3249311615"" (skosimp*)"" (lemma "abs_x_to_n_conv" )"" (inst?)"" (assert )"" (case "convergence(LAMBDA (n: nat): x!1 ^ n, 0)" )"1" (hide -2)"1" (lemma "cnv_seq_scal" )"1" (inst?)"1" (inst - "c!1" )"1" (assert )"1" (hide -2)"1" "(c!1 * (LAMBDA (n: nat): x!1 ^ n), 0) = (LAMBDA (n: nat): c!1 * x!1 ^ n, 0)" )"1" (hide -1 2)"1" (expand "*" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "convergent?" )"2" (skosimp*)"2" (case-replace "l!1 = 0" )"1" (expand "convergence" )"1" (skosimp*)"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "n!1" )"1" "1" "1" assert )"1" "1" "abs(x!1 ^ i!1) = abs(x!1)^i!1" )"1" "1" expand "abs" )"1" "1" (ground) nil nil ))nil ))nil ))nil )"2" "2" rewrite "abs_hat_nat" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "cnv_seq_abs_x_to_n" )"2" (inst?)"2" (assert )"2" (rewrite "limit_def" )"2" "unique_limit" )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil series nil )"nnreal" exponentiation nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil convergence_sequences "analysis/" )nil convergence_sequences "analysis/" )nil series nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil exponentiation nil )"real" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"bool" convergence_sequences "analysis/" )"[numfield, numfield -> numfield]" number_fields nil )"[T -> real]" real_fun_ops "reals/" )"[T, T -> boolean]" equalities nil )nil number_fields nil )nil convergence_ops "analysis/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil sequences nil )"bool" convergence_sequences "analysis/" )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation 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 3249311615 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3519664155 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3519664155"" (skeep)"" (assert )"" (rewrite "sigma_scal_right" :dir rl)"" (lemma "sigma_split" )"" "LAMBDA (i: nat): geometric(x)(i) * x" "n" "0" "n-1" )"" (assert )"" (replace -1)"" (hide -1)"" (expand "sigma" + 3)"" (expand "sigma" + 3)"" (expand "geometric" + 3)"" (case "x ^ n * x = x^(1+n)" )"1" (replace -1)"1" (hide -1)"1" assert )"1" "sigma_split" )"1" "geometric(x)" "n" "0" "0" )"1" assert )"1" replace -1)"1" "1" expand "sigma" + 1)"1" expand "sigma" + 1)"1" expand "geometric" "1" expand "^" + 1)"1" expand "expt" + 1)"1" "sigma_shift" )"1" "geometric(x)" "n-1" "0" "1" )"1" assert )"1" replace "1" "1" case "(LAMBDA (n_1: nat): geometric(x)(1 + n_1)) = (LAMBDA (i: nat): geometric(x)(i) * x)" )"1" assert )nil nil )"2" "2" "2" expand "geometric" )"2" expand "^" )"2" expand "expt" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "^" )"2" expand "expt" + 2)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )nil sigma "reals/" )"odd_int" integersnil )"posint" nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma_nat "reals/" )"int" integers nil )"odd_int" integers nil )"real" exponentiation nil )"odd_int" integers nil )"real" sigma "reals/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers 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 sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"sequence[real]" series nil )nil sequences nil )nil sigma "reals/" ))nil ))nil 3249311615 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" reals nil )"boolean" notequal nil ))nil ))nil 3249311615"" (skeep)"" (lemma "sigma_geometric_aux" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )nil series nil )"real" reals nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil ))nil 3519664192 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil ))nil ))nil 3249311615"" (skosimp*)"" (expand "series" )"" "(LAMBDA (n: nat): sigma(0, n, geometric(x!1))) = (LAMBDA (n: nat): (1-x!1^(n+1))/(1-x!1))" )"1" (hide -1)"1" "(LAMBDA (n: nat): (1 - x!1 ^(n+1)) / (1 - x!1)) = (LAMBDA (n: nat): 1 / (1 - x!1)) - (LAMBDA (n: nat): x!1 ^(n+1) / (1 - x!1))" )"1" (hide -1)"1" (lemma "cnv_seq_diff" )"1" "1/(1-x!1)" "0" "(LAMBDA (n: nat): 1/(1-x!1))" "(LAMBDA (n: nat): x!1^(n+1)/(1-x!1))" )"1" (assert )"1" (hide 2)"1" (lemma "cnv_seq_const" )"1" (inst -1 "1/(1-x!1)" )"1" (expand "const_fun" )"1" (replace -1)"1" assert )"1" "1" "cnv_seq_div" )"1" "0" "(1-x!1)" "(LAMBDA (n: nat): x!1^(n+1))" "(LAMBDA (n: nat): (1-x!1))" )"1" expand "/" -1)"1" "1" "cnv_seq_const" )"1" "(1-x!1)" )"1" expand "const_fun" )"1" assert )"1" "1" "convergence_x_to_n" )"1" "1" "x!1" )"1" assert )"1" expand "^" )"1" expand "expt" "1" nil 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" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "-" )"2" (apply-extensionality 1 :hide? t) nil nil )) nil ))nil )"3" (hide 2) (("3" (grind) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (apply-extensionality 1 :hide? t)"2" (lemma "sigma_geometric" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil )"3" (hide 2) (("3" (grind) nil nil )) nil ))nil ))nil ))nil )"sequence[real]" series nil )nil series nil )"int" integers nil )"(total_order?[real])" nil )nil abs_lems "reals/" )"posint" nil )"real" series nil )nil reals nil )nil series nil )"real" exponentiation nil )"[T -> real]" real_fun_ops "reals/" )nil convergence_ops "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil convergence_ops "analysis/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil convergence_ops "analysis/" )"nzreal" nil )"[T -> real]" real_fun_ops "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"sequence[real]" series nil )nil sequences nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields 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 )"real" reals nil )"posint" nil )"real" reals nil ))nil ))nil 3321109163"" (skosimp*)"" (lemma "geometric_series" )"" (inst?)"" (assert )"" (expand "convergent?" ) (("" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )nil series nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nzreal" nil )"bool" convergence_sequences "analysis/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3249311615"" (skosimp*)"" (lemma "geometric_series" )"" (inst?)"" (assert )"" (lemma "cnv_seq_scal" )"" "c!1" "1 / (1 - x!1)" "series(geometric(x!1))" )"" (assert )"" (hide -2)"" (expand "*" )"" (expand "series" )"" "(LAMBDA (n: nat): sigma(0, n, LAMBDA (x: nat): c!1 * geometric(x!1)(x))) =(LAMBDA (x: nat): c!1 * sigma(0, x, geometric(x!1)))" )"1" (assert ) nil nil )"2" (hide -1 2)"2" (apply-extensionality :hide? t)"2" (rewrite "sigma_scal" )"2" assert )"2" "(LAMBDA (x: nat): geometric(x!1)(x)) = geometric(x!1)" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil series nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil sequences nil )"sequence[real]" series nil )"sequence[real]" series nil )nil sigma "reals/" )"(total_order?[real])" nil )"real" reals nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"[T -> real]" real_fun_ops "reals/" )nil convergence_ops "analysis/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3249311615"" (skosimp*)"" (expand "conv_series?" )"" (lemma "geometric_series" )"" (inst?)"" (expand "convergent?" )"" (assert ) (("" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"bool" series nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" convergence_sequences "analysis/" )nil series nil ))nil ))nil 3249311615"" (skosimp*)"" (expand "inf_sum" )"" (rewrite "limit_def" )"1" (rewrite "geometric_series" ) nil nil )"2" (hide 2)"2" (expand "convergent?" )"2" (lemma "geometric_series" )"2" (inst?)"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" series nil )nil series nil )"sequence[real]" series nil )"sequence[real]" series nil )"bool" convergence_sequences "analysis/" )nil sequences nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals 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 reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil convergence_sequences "analysis/" )"nzreal" nil )"real" reals nil ))nil ))nil 3249311615 ("" (subtype-tcc) nil nil ) nil nil ))nil 3249311615"" (induct "n1" )"1" (skosimp*)"1" (assert )"1" (expand "^" )"1" (expand "expt" ) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (skosimp*)"2" (inst?)"2" (assert )"2" (replace -2)"2" (assert )"2" (inst?)"2" (lemma "both_sides_times_pos_le1" )"2" "rho!1" "abs(a!1(j!1))" "abs(a!1(0)) * rho!1 ^ j!1" )"2" (assert )"2" "rho!1 ^ (1 + j!1) = rho!1 ^ j!1 * rho!1" )"1" (assert ) nil nil )"2" (hide -1 -3)"2" "T3" "abs(a!1(0)) * (rho!1 ^ j!1 * rho!1)" )"2" "T2" "rho!1 * abs(a!1(j!1))" )"2" assert )"2" "2" expand "^" )"2" expand "expt" 1 1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )nil real_props nil )"nzreal" exponentiation nil )nil real_types nil )"posreal" nil )"[T, T -> boolean]" equalities nil )"int" integers nil )"odd_int" integersnil )"posreal" exponentiation nil )"real" exponentiation nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"nzreal" exponentiation nil )nil naturalnumbers nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil sequences 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 )"posint" nil )"nnreal" nil ))nil ))nil 3249311615 ("" (subtype-tcc) nil nil )nil real_types nil )"bool" reals nil )nil real_types 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 )"boolean" notequal nil ))nil ))nil 3249311615"" (skosimp*)"" (lemma "const_geometric_series" )"" (inst -1 "abs(a!1(0))" "rho!1" )"" (expand "abs" -1 1)"" (assert )"" (lemma "comparison_test" )"" (inst -1 "a!1" "abs(a!1(0)) * geometric(rho!1)" )"" (assert )"" (hide 2)"" (split +)"1" (expand "convergent?" )"1" (inst?) nil nil )) nil )"2" (hide -1)"2" (expand "geometric" )"2" (lemma "scaf_abs" )"2" (skosimp*)"2" expand "*" )"2" "2" assert )"2" "2" "2" "n!2" )"2" rewrite "abs_div" )"1" "both_sides_times_pos_le1" )"1" "abs(a!1(n!2))" "abs(a!1(1 + n!2)) / abs(a!1(n!2))" "rho!1" )"1" (assert ) nil nil )"2" "2" "2" nil nil ))nil ))nil )"3" "3" "3" nil nil ))nil ))nil ))nil ))nil )"2" "2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil series nil )"real" reals nil )nil series nil )"(total_order?[real])" nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" convergence_sequences "analysis/" )nil real_props nil )"real" reals nil )"nat" series nil )"sequence[real]" series nil )"(strict_total_order?[real])" real_props nil )"posint" nil )nil real_props nil )nil reals nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"nnreal" nil )"nzreal" exponentiation nil )nil series nil )"[T -> real]" real_fun_ops "reals/" )"sequence[real]" series nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"bool" reals nil )nil sequences nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans 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 )"real" reals nil ))nil ))nil 3249314763"" (skosimp*)"" (lemma "tail_conv" )"" (inst?)"" "(LAMBDA n: IF n < N!1 then a!1(N!1)/rho!1^(N!1-n) ") "" (inst - "BB" )"" (assert )"" (hide 2)"" (split +)"1" (lemma "ratio_test" )"1" (inst?)"1" (assert )"1" (hide 2)"1" (split)"1" (skosimp*)"1" replace -2 * rl)"1" assert )"1" "1" "1" "1" "1" "1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst?)"2" assert )"2" "2" case "n!1 < N!1" )"1" replace -2 * rl)"1" "1" assert )"1" "1" "1" "1" "1" expand "^" )"1" expand "expt" "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "n!1 = N!1-1" )"1" assert )"1" "1" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "n!1" )"2" assert )"2" replace -1 * rl)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst?)"2" (skosimp*)"2" (replace -2 * rl) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil series nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"posreal" exponentiation nil )"nzreal" exponentiation nil )"int" integers nil )"[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil )"(total_order?[real])" nil )"real" exponentiation nil )"nzreal" exponentiation nil )"posreal" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"posreal" exponentiation nil )"posreal" nil )"int" integers nil )nil series nil )nil sequences 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 )"real" reals nil ))nil )nil 3249311615"" (skosimp*)"" (lemma "tail_conv" )"" (inst?)"" "(LAMBDA n: IF n < N!1 then a!1(N!1)/rho!1^(N!1-n) ") "" (inst - "B" )"" (assert )"" (hide 2)"" (split +)"1" (lemma "ratio_test" )"1" (inst?)"1" (assert )"1" (hide 2)"1" (split)"1" (skosimp*)"1" replace -2 * rl)"1" assert )"1" "1" "1" "1" "1" "1" "1" assert )"1" "div_eq_zero" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst?)"2" assert )"2" "2" case "n!1 < N!1" )"1" replace -2 * rl)"1" "1" assert )"1" "1" "1" "1" "1" expand "^" )"1" expand "expt" "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "n!1 = N!1-1" )"1" assert )"1" "1" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "n!1" )"2" assert )"2" replace -1 * rl)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst?)"2" (skosimp*)"2" (replace -2 * rl) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil ))nil 3298110791"" (skosimp*)"" (lemma "tail_series_conv2" )"" (inst?)"" (inst - "N!1" )"" (assert )"" (hide 2)"" (lemma "ratio_test" )"" (inst?)"" (assert )"" (prop)"1" (skosimp*)"1" (inst?) (("1" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (inst + "rho!1" )"2" (assert )"2" (skosimp*)"2" "n!1 + N!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil series nil )"posint" nil )"nonneg_int" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"(total_order?[real])" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"(total_order?[real])" nil )nil series nil )"(strict_total_order?[real])" real_props nil )nil sequences 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 )"real" reals nil ))nil ))nil 3249311615 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3249311615"" (skosimp*)"" (name "LL" "limit(LAMBDA n: abs(a!1(n + 1) / a!1(n)))" )"1" (case "LL >= 0" )"1" (replace -2)"1" (rewrite "limit_def" )"1" (hide -4)"1" (lemma "ratio_test_gen" )"1" (inst?)"1" (assert )"1" (replace -3)"1" (assert )"1" (hide 2)"1" (expand "convergence" )"1" case "(EXISTS (nr: real): LL < nr AND nr < 1)" )"1" "1" "abs(nr!1)-LL" )"1" "1" "abs(nr!1)" )"1" expand "abs" 1 1)"1" assert )"1" "n!1" )"1" "1" "n!2" )"1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" "2" "(1+LL)/2" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -3 2)"2" (lemma "limit_pos" )"2" (inst?)"2" (split -1)"1" (assert ) nil nil )"2" (hide -1 -3 2)"2" (skosimp*)"2" (inst-cp -1 "n!1" )"2" (inst -1 "n!1+1" )"2" (grind)"2" (lemma "div_eq_zero" )"2" (inst?) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (reveal -2) (("3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (propax) nil nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"real" convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )nil sequences 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 )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"posint" nil )"sequence[real]" series nil )nil series nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"real" series nil )"real" series nil )"bool" reals nil )nil real_types nil )"posint" nil )"(total_order?[real])" nil )"real" reals nil )"bool" convergence_sequences "analysis/" )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil series nil )"(total_order?[real])" nil )nil convergence_sequences "analysis/" )"real" reals nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.605 Sekunden
(vorverarbeitet am 2026-04-30)
¤ *© Formatika GbR, Deutschland
2026-05-26
