Quelle series_aux.prf
Sprache: Lisp
(series_auxnil 3314015810"" (skosimp*)"" (lemma "partial_sums" ("a" "a!1" ))"" (replace -1 1)"" (hide -1)"" (skosimp)"" (inst + "n!1+1" )"" (skosimp)"" "sigma_eq" "low" "m!1+1" "high" "n!2" "F" "a!1" "G" "lambda (n:nat): 0" ))"" (rewrite "sigma_zero" )"" (split -1)"1" (replace -1)"1" (expand "abs" ) (("1" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (typepred "n!3" )"2" (inst - "n!3" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 series nil )"posint" nil )nil integers nil )"bool" reals nil )nil integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"(total_order?[real])" nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil sigma "reals/" ))nil 3314015766"" (lemma "zero_tail_series_conv" ) (("" (propax) nil nil )) nil )nil series_aux nil )) shostak))nil 3314016598"" (skosimp)"" (lemma "zero_tail_series_conv" ("a" "a!1" "n" "n!1" ))"" (replace -2 -1)"" (expand "series" 1 2)"" (lemma "limit_series_shift" ("a" "a!1" "pn" "n!1+1" ))"" (replace -2 -1)"" (replace -1 1)"" (assert )"" (hide -1)"" "(LAMBDA (n:nat): a!1(1 + n + n!1)) = (LAMBDA (n:nat): 0)" )"1" (rewrite "zero_series_limit" ) nil nil )"2" (hide 2)"2" (apply-extensionality :hide? t)"2" (inst - "1+n!1+x!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 series_aux nil )"sequence[real]" series nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"real" reals nil )"[T, T -> boolean]" equalities nil )nil series nil )"posint" nil )nil series nil )nil integers nil )"bool" reals nil )nil integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3321845471"" (skosimp)"" (lemma "zero_tail_series_conv" ("a" "a!1" "n" "n!1" ))"" (lemma "zero_tail_series_limit" ("a" "a!1" "n" "n!1" ))"" (replace -3 (-1 -2))"" (rewrite "limit_equiv" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))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 series_aux nil )"sequence[real]" series nil )nil convergence_ops "analysis/" )nil series_aux nil ))nil 3314567201"" (skosimp)"" (lemma "zero_tail_series_conv" ("a" "a!1" "n" "n!1" ))"" (split)"1" (propax) nil nil )"2" (skosimp)"2" (inst - "m!1" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))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 series_aux nil )"(strict_total_order?[real])" real_props nil ))nil 3314567614"" (lemma "single_nz_series_conv" ) (("" (propax) nil nil )) nil )nil series_aux nil )) shostak))nil 3314567245"" (skosimp)"" (lemma "zero_tail_series_limit" ("a" "a!1" "n" "n!1" ))"" (split -1)"1" (expand "series" -1 2)"1" (expand "sigma" -1)"1" (case-replace "n!1=0" )"1" (assert ) nil nil )"2" "sigma_restrict_eq" "low" "0" "high" "n!1-1" "F" "a!1" "G" "lambda (i:nat): 0" ))"2" (rewrite "sigma_zero" )"2" (split)"1" (replace -1) (("1" (assert ) nil nil )) nil )"2" (expand "restrict" )"2" (apply-extensionality :hide? t)"2" (inst - "x!1" )"2" (lift-if)"2" (prop) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (inst - "m!1" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))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 series_aux nil )"sequence[real]" series nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"odd_int" integersnil )nil sigma_nat "reals/" )nil sigma "reals/" )"[T -> real]" sigma "reals/" )"(strict_total_order?[real])" real_props nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"real" sigma "reals/" ))nil 3321845412"" (skosimp)"" (lemma "single_nz_series_conv" ("a" "a!1" "n" "n!1" ))"" (lemma "single_nz_series_limit" ("a" "a!1" "n" "n!1" ))"" (assert )"" (replace -3 (-1 -2))"" (rewrite "limit_equiv" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))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 series_aux nil )nil convergence_ops "analysis/" )"sequence[real]" series nil )nil series_aux nil ))nil 3322859396"" (skosimp)"" "cnv_seq_order" "s1" "LAMBDA n: 0" "s2" "nna!1" "l1" "0" "l2" "limit(nna!1)" ))"" (lemma "limit_equiv" ("s" "nna!1" "l" "limit(nna!1)" ))"" (simplify -1)"" (replace -3 -1)"" (simplify -1)"" (replace -1 -2)"" (split -2)"1" (assert ) nil nil )"2" (hide-all-but 1)"2" (expand "convergence" )"2" (expand "abs" ) (("2" (propax) nil nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 )nil booleans nil )nil numbers nil )nil convergence_ops "analysis/" )"(total_order?[real])" nil )"(total_order?[real])" nil )"bool" convergence_sequences "analysis/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil convergence_ops "analysis/" ))nil 3322862860"" (skosimp*)"" (case "FORALL m: n!1 < m => nna!1(m) = 0" )"1" (lemma "zero_tail_series" ("a" "nna!1" "n" "n!1" ))"1" (replace -2 -1)"1" "unique_limit" "u" "series(nna!1)" "l1" "nnx!1" "l2" "series(nna!1)(n!1)" ))"1" (assert ) nil nil )) nil ))nil ))nil )"2" (skosimp)"2" (expand "convergence" )"2" (inst - "nna!1(m!1)" )"1" (skosimp)"1" (inst - "max(n!2,m!1)" )"1" (split -2)"1" (case "increasing?(series(nna!1))" )"1" (expand "abs" )"1" "series(nna!1)(max(n!2, m!1)) - nnx!1 < 0" )"1" (expand "increasing?" )"1" (inst - "n!1" "max(n!2,m!1)" )"1" (assert ) nil nil )) nil ))nil )"2" (assert )"2" (hide 1)"2" (expand "series" )"2" expand "max" )"2" "n!2<m!1" )"1" expand "sigma" -3)"1" assert )"1" expand "increasing?" )"1" "n!1" "m!1-1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "n!2 >= m!1" )"1" "1" expand ">=" )"1" expand "<=" -1)"1" "1" "sigma_middle[nat]" "high" "n!2" "i" "m!1" "low" "0" "F" "nna!1" ))"1" assert )"1" replace -1 -4)"1" "1" case "forall m: 0 <= sigma(1 + m!1, 1+m!1+m, nna!1)" )"1" "n!2-m!1-1" )"1" expand "increasing?" )"1" "n!1" "m!1-1" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "m" )"1" expand "sigma" )"1" assert )"1" expand "sigma" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" expand "sigma" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1 * rl)"2" "2" expand "sigma" -2)"2" expand "increasing?" )"2" "n!1" "m!1-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "increasing?" )"2" (expand "series" )"2" case "forall n,m: sigma(0, n, nna!1) <= sigma(0, n+m, nna!1)" )"1" (skosimp)"1" "x!1" "y!1-x!1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" "m" )"1" "1" (assert ) nil nil ))nil )"2" "2" "n!3" )"2" expand "sigma" 1 2)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "max" )"2" (case-replace "n!2 < m!1" )"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil sequences nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )"[bool, bool -> bool]" booleans 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 )"(total_order?[real])" nil )"sequence[real]" series nil )nil convergence_sequences "analysis/" )nil series_aux nil )"real" reals nil )"bool" convergence_sequences "analysis/" )"nat" series_aux nil )"nat" series_aux nil )"nonneg_int" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"int" integers nil )"nnreal" nil )"nnreal" sigma_nat "reals/" )"(total_order?[real])" nil )"real" sigma "reals/" )nil naturalnumbers nil )nil defined_types nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"odd_int" integers nil )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )"bool" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" real_fun_preds "reals/" )AND const-decl "[bool, bool -> bool]" booleans nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"{k: nat | i <= k AND j <= k}" nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )nil real_types nil )nil real_types nil )"nat" series_aux nil )"sequence[nnreal]" series_aux nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil ))nil 3322860486"" (skosimp*)"" (typepred "phi!1" )"" "MM" "LAMBDA (f:(bijective?[nat,nat]),n:nat): image(LAMBDA (i:below[n+1]): f(i))(fullset[below[n+1]])" )"" (lemma "surjective_inverse_exists[nat,nat]" ("f" "phi!1" ))"" (lemma "bij_inv_is_bij_alt[nat,nat]" ("f" "phi!1" ))"" (skolem - ("phi1" ))"" (inst - "phi1" )"" case "forall (f: (bijective?[nat, nat]), n: nat): is_finite[nat](MM(f,n))" )"1" case "FORALL (f: (bijective?[nat, nat]), n: nat): has_greatest?(MM(f,n),reals.<=)" )"1" (expand "restrict" )"1" (expand "has_greatest?" )"1" (expand "greatest?" )"1" (expand "upper_bound?" )"1" (case "increasing?(series(nna!1))" )"1" case "increasing?(series(nna!1 o phi!1))" )"1" case "FORALL n: EXISTS m: series(nna!1 o phi!1)(n) <= series(nna!1)(m)" )"1" case "FORALL (a: sequence[nnreal], l: real): ") "1" "series(nna!1)" "nnx!1" )"1" assert )"1" case "FORALL (j: nat): series(nna!1 o phi!1)(j) <= nnx!1" )"1" expand "convergence" )"1" "1" "epsilon!1" )"1" "1" case "FORALL i: i >= n!1 IMPLIES nnx!1-series(nna!1)(i) < epsilon!1" )"1" case "EXISTS n: ") "1" "1" "n!2" )"1" "1" "i!1" )"1" assert )"1" expand "abs" "1" assert )"1" "i!1" )"1" assert )"1" expand "<=" "1" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "FORALL n: EXISTS m: series(nna!1)(n) <= series(nna!1 o phi!1)(m)" )"1" "n!1" )"1" "1" "n!1" )"1" assert )"1" "m!1" )"1" "1" expand "increasing?" "1" "m!1" "i!1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "phi!1" "n!2" )"2" case " EXISTS (t: nat): AND ") "1" "1" "1" "t!1" )"1" case "FORALL (j: nat): LAMBDA (i: nat):IF MM(phi1, j)(i) THEN nna!1(phi!1(i)) ELSE 0 ENDIF)") "1" expand "series" )"1" "n!2" )"1" assert )"1" replace "1" "sigma_le" "low" "0" "high" "t!1" "F" "LAMBDA (i: nat): IF MM(phi1, n!2)(i) THEN nna!1(phi!1(i)) ELSE 0 ENDIF" "G" "nna!1 o phi!1" ))"1" "1" nil nil )"2" "2" "2" expand "o" "2" "MM(phi1, n!2)(n!3)" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "j" )"1" assert )"1" expand "sigma" "1" "sigma_with" "low" "0" "high" "t!1" "i" "phi1(0)" "a" "nna!1(0)" "F" "LAMBDA (i: nat): IF MM(phi1, 0)(i) THEN nna!1(phi!1(i)) ELSE 0 ENDIF" "G" "LAMBDA (i:nat): 0" ))"1" "1" replace "1" "sigma_zero" "low" "0" "high" "t!1" ))"1" assert )nil nil ))nil ))nil )"2" assert )nil nil )"3" "phi1(0)" )"3" expand "MM" )"3" expand "image" )"3" expand "image" )"3" "0" )"3" expand "fullset" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "4" "x!1=phi1(0)" )"1" assert )"1" "MM(phi1, 0)(phi1(0))" )"1" "comp_inverse_right_alt[nat,nat]" "f" "phi!1" "g" "phi1" "r" "0" ))"1" assert )nil nil ))nil )"2" "2" expand "MM" )"2" expand "image" )"2" expand "image" )"2" "0" )"2" expand "fullset" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "MM(phi1, 0)(x!1)" )"1" expand "MM" )"1" expand "image" )"1" expand "image" )"1" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "sigma" "2" replace "2" "2" "sigma_with" "low" "0" "high" "t!1" "F" "LAMBDA (i: nat): IF MM(phi1, 1 + j!1)(i) THEN nna!1(phi!1(i)) ELSE 0 ENDIF" "G" "LAMBDA (i: nat): IF MM(phi1, j!1)(i) THEN nna!1(phi!1(i)) ELSE 0 ENDIF" "i" "phi1(1+j!1)" "a" "nna!1(1+j!1)" ))"2" "1" replace "1" assert )"1" case "MM(phi1, j!1)(phi1(1 + j!1))" )"1" "1" expand "MM" )"1" expand "image" )"1" expand "image" )"1" "1" "x!1" )"1" expand "bijective?" "1" "1" expand "injective?" )"1" "1+j!1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )"3" "phi1(1+j!1)" )"3" expand "MM" )"3" expand "image" )"3" expand "image" )"3" "1+j!1" )"3" expand "fullset" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "4" "x!1=phi1(1 + j!1)" )"1" assert )"1" "MM(phi1, 1 + j!1)(phi1(1 + j!1))" )"1" "comp_inverse_right_alt[nat,nat]" "f" "phi!1" "g" "phi1" "r" "1+j!1" ))"1" assert )nil nil ))nil )"2" "2" expand "MM" )"2" expand "image" )"2" expand "image" )"2" "1+j!1" )"2" expand "fullset" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "MM(phi1, 1 + j!1)(x!1)" )"1" "MM(phi1,j!1)(x!1)" )"1" "1" expand "MM" )"1" expand "image" )"1" expand "image" )"1" "1" "x!2" )"1" "x!2" )"1" expand "fullset" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" replace "2" "2" expand "image" )"2" expand "image" )"2" "2" "2" "2" "2" "x" )"2" expand "fullset" )"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 )"2" "2" "2" "phi1" "n!2" )"2" "non_empty_finite_has_greatest[nat]" "NF" "MM(phi1,n!2)" ))"1" "LAMBDA (i,j:nat): reals.<=(i,j)" )"1" expand "has_greatest?" )"1" expand "greatest?" )"1" expand "upper_bound?" )"1" nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil )"2" assert )"2" expand "empty?" )"2" expand "member" )"2" "2" expand "MM" )"2" expand "fullset" )"2" expand "image" )"2" expand "image" )"2" "phi1(0)" )"2" "0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil )"2" "2" "2" "i!1" )"1" assert )"1" "i!1" )"1" expand "abs" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "j!1" )"2" "2" "m!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "increasing?" )"2" "2" "0" "x1!1" )"2" assert )"2" expand "series" "2" expand "sigma" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "convergence_cauchy" "u" "a!1" ))"2" "cauchy_bounded" "u" "a!1" ))"2" replace -2 -1 rl)"2" "increasing_bounded_convergence" "v1" "a!1" ))"1" assert )"1" "unique_limit" "u" "a!1" "l1" "l!1" "l2" "sup(a!1)" ))"1" assert )"1" replace -1)"1" expand "sup" )"1" "lub(Im(a!1))" )"1" expand "least_upper_bound?" )"1" "1" expand "upper_bound?" )"1" "1" "a!1(j!1)" )"1" expand "Im" )"1" "j!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" nil nil )"2" expand "convergent?" )"2" "l!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "phi!1" "n!1" )"2" "2" "t!1" )"2" case "series(nna!1 o phi!1)(n!1) = LAMBDA (i: nat):IF MM(phi!1, n!1)(i) THEN nna!1(i) ELSE 0 ENDIF)") "1" replace -1 1)"1" "1" expand "series" )"1" "sigma_le" "low" "0" "high" "t!1" "F" "LAMBDA (i: nat): IF MM(phi!1, n!1)(i) THEN nna!1(i) ELSE 0 ENDIF" "G" "nna!1" ))"1" "1" nil nil )"2" "2" "2" "n!2" )"2" "MM(phi!1, n!1)(n!2)" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "series" )"2" case "forall (j:nat): j <= n!1 => sigma(0, j, nna!1 o phi!1) = LAMBDA (i: nat):IF MM(phi!1, j)(i) THEN nna!1(i) ELSE 0 ENDIF)") "1" "n!1" )"1" assert )nil nil ))nil )"2" "2" "j" )"1" assert )"1" expand "sigma" "1" expand "o" "1" "phi!1(0)" )"1" "phi!1(0)" )"1" "sigma_with" "low" "0" "high" "t!1" "F" "LAMBDA (i: nat): IF MM(phi!1, 0)(i) THEN nna!1(i) ELSE 0 ENDIF" "G" "LAMBDA (i:nat): 0" "a" "nna!1(phi!1(0))" "i" "phi!1(0)" ))"1" assert )"1" "1" replace "1" "sigma_zero" "low" "0" "high" "t!1" ))"1" assert )nil nil ))nil ))nil )"2" "2" "2" "2" "MM(phi!1, 0)(x!1)" )"1" assert )"1" "x!1=phi!1(0)" )"1" assert )nil nil )"2" assert )"2" expand "MM" )"2" expand "image" )"2" expand "image" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "x!1=phi!1(0)" )"1" assert )"1" expand "MM" )"1" expand "image" )"1" expand "image" )"1" "0" )"1" expand "fullset" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "MM" )"2" expand "image" )"2" expand "image" )"2" "0" )"2" expand "fullset" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "sigma" "2" replace "2" "2" "sigma_with" "low" "0" "high" "t!1" "G" "LAMBDA (i:nat): IF MM(phi!1, j!1)(i) THEN nna!1(i) ELSE 0 ENDIF" "F" "LAMBDA (i:nat): IF MM(phi!1, 1 + j!1)(i) THEN nna!1(i) ELSE 0 ENDIF" "i" "phi!1(1+j!1)" "a" "nna!1(phi!1(1+j!1))" ))"2" "phi!1(1+j!1)" )"2" "phi!1(1+j!1)" )"1" assert )"1" "1" replace "1" assert )"1" expand "o" "1" "1" assert )"1" "MM(phi!1, j!1)(phi!1(1 + j!1))" )"1" expand "MM" )"1" expand "image" )"1" expand "image" )"1" "1" "x!1" )"1" "1" expand "bijective?" )"1" "1" expand "injective?" )"1" "1+j!1" "x!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 )"2" "2" "2" "x!1=phi!1(1 + j!1)" )"1" assert )"1" "1" "MM(phi!1, 1 + j!1)(phi!1(1 + j!1))" )"1" assert )"1" expand "MM" )"1" expand "image" )"1" expand "image" )"1" "1+j!1" )"1" expand "fullset" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "MM(phi!1, j!1)(x!1)" )"1" "MM(phi!1, 1+j!1)(x!1)" )"1" expand "MM" )"1" expand "image" )"1" expand "image" )"1" "1" "x!2" )"1" "x!2" )"1" expand "fullset" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "MM(phi!1, 1 + j!1)(x!1)" )"1" expand "MM" )"1" expand "image" )"1" expand "image" )"1" "1" "x!2" )"1" "x!2" )"1" expand "fullset" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "MM" )"2" expand "image" )"2" expand "image" )"2" "1+j!1" )"2" expand "fullset" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "increasing?" )"2" expand "o " )"2" expand "series" )"2" "2" expand "<=" -1)"2" "1" assert )"1" "sigma_zero" "low" "1+x!1" "high" "y!1" ))"1" "sigma_le" "low" "1+x!1" "high" "y!1" "F" "LAMBDA (i: nat): 0" "G" "LAMBDA (x: nat): nna!1(phi!1(x))" ))"1" "1" assert )"1" replace -2)"1" "1" "sigma_split" "low" "0" "high" "y!1" "z" "x!1" "F" "LAMBDA (x: nat): nna!1(phi!1(x))" ))"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "increasing?" )"2" expand "series" )"2" "2" expand "<=" -1)"2" "1" assert )"1" "1" "sigma_le" "low" "1+x!1" "high" "y!1" "F" "lambda (i:nat): 0" "G" "nna!1" ))"1" "1" "sigma_zero" "low" "1+x!1" "high" "y!1" ))"1" assert )"1" "1" replace "1" "1" "sigma_split" "low" "0" "high" "y!1" "z" "x!1" "F" "nna!1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 -1))"2" (skosimp)"2" (inst - "f!1" "n!1" )"2" (expand "restrict" )"2" "non_empty_finite_has_greatest[nat]" "NF" "MM(f!1,n!1)" "le" "LAMBDA (s: [nat, nat]): reals.<=(s)" ))"1" (propax) nil nil )"2" "2" (grind) nil nil ))nil )"3" assert )"3" expand "empty?" )"3" expand "member" )"3" expand "MM" )"3" expand "fullset" )"3" expand "image" )"3" expand "image" )"3" "f!1(0)" )"3" "0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 -3)"2" (skosimp)"2" (expand "MM" )"2" "finite_image[below[1+n!1],nat]" "f" "f!1" "S" "fullset[below[1 + n!1]]" ))"1" (expand "restrict" )"1" (expand "image" )"1" expand "image" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "fullset" )"2" expand "is_finite" )"2" "1+n!1" "LAMBDA (n:below[1+n!1]): n" )"2" expand "injective?" )"2" (skosimp) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" functions nil )nil naturalnumbers nil )"bool" reals 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 numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil function_inverse_defnil )"bool" functions nil )"bool" finite_sets nil )"bool" minmax_orders "orders/" )"bool" real_fun_preds "reals/" )nil sequences nil )"sequence[real]" series nil )nil real_types nil )"odd_int" integersnil )nil sigma "reals/" )nil convergence_sequences"analysis/" )"bool" convergence_sequences "analysis/" )"bool" bounded_real_defs nil )"sequence[nnreal]" series_aux nil )"nat" series_aux nil )"setof[real]" real_fun_props "reals/" )nil defined_types nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )"(nonempty?[real])" "analysis/" )"real" real_fun_supinf "analysis/" )nil convergence_sequences "analysis/" )"bool" real_fun_preds "reals/" )nil "analysis/" )nil convergence_sequences "analysis/" )"sequence[nnreal]" series_aux nil )"int" series_aux nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" series_aux nil )"nnreal" sigma_nat "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )IF const-decl "[boolean, T, T -> T]" if_def nil )nil integers nil )nil sigma "reals/" )nil naturalnumbers nil )nil sigma "reals/" )"nat" sigma_nat "reals/" )"real" reals nil )"int" integers nil )"nnreal" nil )nil sigma_nat "reals/" )"set[R]" function_image nil )"nat" series_aux nil )"[[(bijective?[nat, nat]), nat] -> set[nat]]" nil )nil function_inverse_def nil )nil sigma "reals/" )"posint" nil )"(fullset[below[2 + j!1]])" series_aux nil )"(fullset[below[1 + j!1]])" series_aux nil )"nat" series_aux nil )"bool" functions nil )"real" reals nil )nil minmax_orders"orders/" )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"bool" orders nil )"bool" orders nil )"bool" relations nil )"bool" orders nil )"bool" relations nil )"bool" relations nil )"bool" orders nil )"bool" booleans nil )"bool" sets nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" reals nil )"bool" convergence_sequences "analysis/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"(fullset[below[1 + j!1]])" series_aux nil )"(fullset[below[2 + j!1]])" series_aux nil )"nat" series_aux nil )"nat" series_aux nil )"T3" function_props nil )"bool" bounded_orders "orders/" )"bool" reals nil )"R" restrict nil )"bool" minmax_orders "orders/" )nil defined_types nil )"(reflexive?[S])" nil )"(antisymmetric?[S])" nil )"(transitive?[S])" nil )"(preorder?[S])" nil )"(partial_order?[S])" nil )"(dichotomous?[S])" nil )"(total_order?[S])" nil )"(total_order?[real])" nil )nil function_image_aux nil )"(bijective?[nat, nat])" series_aux nil )"[nat -> nat]" series_aux nil )"bool" function_inverse_def nil )nil function_inverse_def nil )"posint" nil )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil nat_types nil )"set[R]" function_image nil )"set" sets nil ))nil 3322860950"" (skosimp)"" (expand "convergent?" )"" (skosimp)"" (inst + "l!1" )"" "nonneg_series_bij" "nna" "nna!1" "phi" "phi!1" "nnx" "l!1" ))"1" (assert ) nil nil )"2" (lemma "limit_nonneg" ("nna" "series(nna!1)" ))"1" (rewrite "limit_equiv" -2)"1" (flatten) (("1" (assert ) nil nil )) nil )) nil )"2" (hide-all-but 1)"2" (expand "series" )"2" (induct "x1" )"1" (expand "sigma" ) (("1" (assert ) nil nil ))nil )"2" (skosimp*)"2" (expand "sigma" 1) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" 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 series_aux nil )"sequence[real]" series nil )nil convergence_ops "analysis/" )"posint" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"nnreal" nil )"nnreal" sigma_nat "reals/" )nil sigma_nat "reals/" )nil naturalnumbers nil )nil defined_types nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )"(total_order?[real])" nil )nil series_aux 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 real_types nil )nil sequences nil )"bool" functions nil ))nil 3322861248"" (skosimp)"" (lemma "nonneg_series_bij_conv" ("nna" "nna!1" "phi" "phi!1" ))"" (assert ) nil nil )) nil ))nil )"bool" functions nil )nil sequences nil )nil real_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 )nil series_aux nil ))nil 3322861180"" (skosimp)"" (lemma "nonneg_series_bij_conv" ("nna" "nna!1" "phi" "phi!1" ))"" (assert )"" (expand "convergent?" )"" (skosimp*)"" "nonneg_series_bij" "nna" "nna!1" "phi" "phi!1" "nnx" "l!2" ))"1" (assert )"1" "unique_limit" "u" "series(nna!1 o phi!1)" "l1" "l!1" "l2" "l!2" ))"1" (assert )"1" (rewrite "limit_equiv" -2)"1" (rewrite "limit_equiv" -4)"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" (lemma "limit_nonneg" ("nna" "series(nna!1)" ))"1" (assert )"1" "limit_def" "v" "series(nna!1)" "l" "l!2" ))"1" (assert ) nil nil )) nil ))nil )"2" (hide-all-but 1)"2" (expand "series" )"2" (induct "x1" )"1" (expand "sigma" ) (("1" (assert ) nil nil ))nil )"2" (skosimp)"2" (expand "sigma" 1)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" functions nil )nil sequences nil )nil real_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 )nil series_aux nil )"bool" convergence_sequences "analysis/" )nil series_aux nil )"(total_order?[real])" nil )nil convergence_sequences "analysis/" )"sequence[real]" series nil )"T3" function_props nil )nil convergence_ops "analysis/" )nil series_aux nil )nil convergence_sequences "analysis/" )"posint" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"nnreal" nil )"nnreal" sigma_nat "reals/" )nil sigma_nat "reals/" )nil naturalnumbers nil )nil defined_types nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" ))nil 3322870394"" (skosimp)"" "AA" "lambda (n:nat): IF a!1(n) < 0 THEN 0 ELSE a!1(n) ENDIF" )"" "BB" "lambda (n:nat): IF a!1(n) < 0 THEN -a!1(n) ELSE 0 ENDIF" )"" (case "a!1 = AA-BB" )"1" (hide -2 -3)"1" (case "convergent?(series(AA))" )"1" (case "convergent?(series(BB))" )"1" (replace -3)"1" (hide -3 -4)"1" (expand "convergent?" )"1" (skosimp*)"1" (assert )"1" "nonneg_series_bij" "nna" "AA" "nnx" "l!2" "phi" "phi!1" ))"1" "nonneg_series_bij" "nna" "BB" "nnx" "l!1" "phi" "phi!1" ))"1" assert )"1" "series(AA) - series(BB) = series(AA - BB)" )"1" "series(AA o phi!1) - series(BB o phi!1) = series((AA -BB)o phi!1)" )"1" "unique_limit" "u" "series(AA - BB)" "l1" "l!2-l!1" "l2" "x!1" ))"1" assert )"1" replace -3 -1 rl)"1" "cnv_seq_diff" "s1" "series(AA)" "s2" "series(BB)" "l1" "l!2" "l2" "l!1" ))"1" assert )"1" replace -2)"1" replace -3 1 rl)"1" "cnv_seq_diff" "s1" "series(AA o phi!1)" "s2" "series(BB o phi!1)" "l1" "l!2" "l2" "l!1" ))"1" assert )"1" "1" expand "o" )"1" expand "series" )"1" expand "convergence" )"1" assert )"1" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "o" )"2" expand "series" )"2" "2" expand "-" )"2" "sigma_minus[nat]" "low" "0" "high" "x!2" "F" "LAMBDA (x: nat): AA(phi!1(x))" "G" "LAMBDA (x: nat): BB(phi!1(x))" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "series" )"2" "2" expand "-" )"2" "sigma_minus[nat]" "low" "0" "high" "x!2" "F" "AA" "G" "BB" ))"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "limit_nonneg" "nna" "series(BB)" ))"1" "1" rewrite "limit_equiv" -2)"1" "1" assert )"1" "1" "1" rewrite "limit_equiv" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "convergent?" )"2" "l!1" )"2" "2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "series" )"2" "x1" )"1" expand "sigma" )"1" expand "BB" )"1" (grind) nil nil ))nil ))nil )"2" expand "BB" )"2" "2" expand "sigma" 1)"2" "a!1(1 + j!1) < 0" )"1" (assert ) nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "BB" )"3" (grind) nil nil ))nil ))nil ))nil )"2" (hide-all-but (1 -3))"2" "limit_nonneg" "nna" "series(AA)" ))"1" "1" "1" rewrite "limit_equiv" -2)"1" "1" (assert ) nil nil ))nil ))nil )"2" expand "convergent?" )"2" (inst + "l!2" ) nil nil ))nil ))nil ))nil )"2" "2" expand "series" )"2" expand "AA" )"2" "x1" )"1" (grind) nil nil )"2" "2" expand "sigma" 1)"2" "a!1(1 + j!1) < 0" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" expand "AA" )"3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-3 1))"2" "comparison_test" ("a" "BB" "b" "abs(a!1)" ))"2" (assert )"2" (hide-all-but 1)"2" (skosimp)"2" (expand "BB" )"2" (expand "abs" )"2" "2" expand "abs" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-2 1))"2" "comparison_test" ("b" "abs(a!1)" "a" "AA" ))"2" (assert )"2" (hide-all-but 1)"2" (expand "AA" ) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (expand "-" )"2" (expand "AA" )"2" (expand "BB" )"2" (case-replace "a!1(x!2) < 0" )"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sequences nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities 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 )"[T -> real]" real_fun_ops "reals/" )"bool" convergence_sequences "analysis/" )"sequence[real]" series nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"sequence[real]" series nil )nil series nil )"[nat -> real]" series_aux nil )nil sigma "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" reals nil )nil convergence_sequences "analysis/" )"[numfield, numfield -> numfield]" number_fields nil )"bool" convergence_sequences "analysis/" )"odd_int" integers nil )nil convergence_ops "analysis/" )"T3" function_props nil )nil series_aux nil )nil convergence_ops "analysis/" )"int" integers nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"[nat -> real]" series_aux nil )nil naturalnumbers nil )nil defined_types nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"bool" functions nil )nil real_types nil )nil series_aux nil )"real" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil ))nil 3322870238"" (skosimp)"" (lemma "convergent_abs" ("a" "a!1" ))"" (assert )"" (expand "convergent?" (-1 1))"" (skosimp)"" "abs_series_bij" "a" "a!1" "phi" "phi!1" "x" "l!1" ))"" (assert ) (("" (inst + "l!1" ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))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 series nil )"bool" convergence_sequences "analysis/" )"bool" functions nil )nil series_aux nil ))nil 3322870064"" (skosimp)"" (lemma "convergent_abs" ("a" "a!1" )) (("" (assert ) nil nil ))nil ))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 series nil ))nil 3322870064"" (skosimp)"" (lemma "abs_series_bij_conv" ("a" "a!1" "phi" "phi!1" ))"" (assert ) nil nil )) nil ))nil )"bool" functions 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 series_aux nil ))nil 3462013823"" (skosimp)"" (lemma "abs_series_bij_conv" ("a" "a!1" "phi" "phi!1" ))"" (lemma "convergent_abs" ("a" "a!1" ))"" (assert )"" (expand "convergent?" (-1 -2))"" (skosimp*)"" "abs_series_bij" "a" "a!1" "phi" "phi!1" "x" "l!1" ))"" (assert )"" "unique_limit" "u" "series(a!1 o phi!1)" "l1" "l!1" "l2" "l!2" ))"" (assert )"" (rewrite "limit_equiv" -2)"" (rewrite "limit_equiv" -3)"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" functions 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 series_aux nil )nil convergence_ops "analysis/" )"T3" function_props nil )"sequence[real]" series nil )nil convergence_sequences "analysis/" )nil series_aux nil )"bool" convergence_sequences "analysis/" )nil series nil ))nil )nil 3322869658"" (skosimp)"" (lemma "abs_series_bij_conv" ("a" "a!1" "phi" "phi!1" ))"" (lemma "convergent?_abs" ("a" "a!1" ))"" (assert )"" (expand "convergent?" (-1 -2))"" (skosimp*)"" "abs_series_bij" "a" "a!1" "phi" "phi!1" "x" "l!1" ))"" (assert )"" "unique_limit" "u" "series(a!1 o phi!1)" "l1" "l!1" "l2" "l!2" ))"" (assert )"" (rewrite "limit_equiv" -2)"" (rewrite "limit_equiv" -3)"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil convergence_ops "analysis/" )nil convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" ))
Messung V0.5 in Prozent C=97 H=97 G=96
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.472Bemerkung:
(vorverarbeitet am 2026-04-25)
¤ *Bot Zugriff
2026-05-26
