SSL series_lems.prf
Interaktion und
(series_lemsnil 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_lems 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_lems 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_lems nil )"sequence[real]" series nil )nil convergence_ops "analysis/" )nil series_lems 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_lems nil )"(strict_total_order?[real])" real_props nil ))nil 3314567614"" (lemma "single_nz_series_conv" ) (("" (propax) nil nil )) nil )nil series_lems 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_lems 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_lems nil )nil convergence_ops "analysis/" )"sequence[real]" series nil )nil series_lems 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" expand "sigma" )"1" assert )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_lems nil )"real" reals nil )"bool" convergence_sequences "analysis/" )"nat" series_lems nil )"nat" series_lems 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_lems nil )"sequence[nnreal]" series_lems nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil ))nil 3445686407"" (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_lems nil )"nat" series_lems 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_lems nil )"int" series_lems 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_lems 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_lems nil )"[[(bijective?[nat, nat]), nat] -> set[nat]]" nil )nil function_inverse_def nil )nil sigma "reals/" )"posint" nil )"(fullset[below[2 + j!1]])" series_lems nil )"(fullset[below[1 + j!1]])" series_lems nil )"nat" series_lems 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_lems nil )"(fullset[below[2 + j!1]])" series_lems nil )"nat" series_lems nil )"nat" series_lems 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_lems nil )"[nat -> nat]" series_lems 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 )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 )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" finite_sets nil )"bool" real_fun_preds "reals/" )nil sigma "reals/" )nil convergence_sequences"analysis/" )"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/" )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )nil sigma_nat "reals/" )nil sigma "reals/" )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" sets nil )"bool" convergence_sequences "analysis/" )set type-eq-decl nil sets 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_lems 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_lems 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_lems 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_lems nil )"bool" convergence_sequences "analysis/" )nil series_lems nil )"(total_order?[real])" nil )nil convergence_sequences "analysis/" )"sequence[real]" series nil )"T3" function_props nil )nil convergence_ops "analysis/" )nil series_lems 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_lems 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_lems 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_lems 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_lems nil )"real" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil ))nil 3445686459"" (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_lems nil ))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 series nil )) shostak))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_lems nil ))nil 3445686483"" (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_lems nil )nil convergence_ops "analysis/" )"T3" function_props nil )"sequence[real]" series nil )nil convergence_sequences "analysis/" )nil series_lems 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/" )nil series nil ))
Messung V0.5 in Prozent C=99 H=98 G=98
¤ 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.703Bemerkung:
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-05-01)
¤ *Bot Zugriff
2026-05-26
