| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/series/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 94 kB |
|
Quelle absconv_series.prfSprache: Lisp |
|||||||||||||||
|
(absconv_series (Convergent_Series_TCC1 0 (Convergent_Series_TCC1-2 "" 3351489592 ("" (lemma "single_nz_series_conv" ("a" "LAMBDA n: 0" "n" "0")) (("" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp) nil nil)) nil)) nil)) nil) ((single_nz_series_conv formula-decl nil series_lems nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (sequence type-eq-decl nil sequences nil)) shostak) (Convergent_Series_TCC1-1 nil 3351489385 ("" (subtype-tcc) nil nil) nil nil)) (absconvergent_series_TCC1 0 (absconvergent_series_TCC1-1 nil 3323144142 ("" (inst + "lambda n: 0") (("" (expand "absconvergent?") (("" (expand "abs") (("" (expand "abs") (("" (rewrite "zero_series_conv") nil nil)) nil)) nil)) nil)) nil) ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (zero_series_conv formula-decl nil series nil) (abs const-decl "sequence[real]" series nil) (absconvergent? const-decl "bool" absconv_series nil) (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (absconvergent_series_is_convergent 0 (absconvergent_series_is_convergent-1 nil 3323402098 ("" (skosimp) (("" (typepred "x!1") (("" (expand "absconvergent?") (("" (lemma "convergent_abs" ("a" "x!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((absconvergent_series nonempty-type-eq-decl nil absconv_series nil) (absconvergent? const-decl "bool" absconv_series nil) (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (convergent_abs formula-decl nil series nil)) shostak)) (abs_series_bij_abs 0 (abs_series_bij_abs-1 nil 3351600269 ("" (skosimp) (("" (typepred "phi!1") (("" (split) (("1" (flatten) (("1" (lemma "bijective_inverse_exists[nat,nat]" ("f" "phi!1")) (("1" (expand "exists1") (("1" (flatten) (("1" (skosimp) (("1" (lemma "bij_inv_is_bij_alt" ("f" "phi!1" "g" "x!2")) (("1" (lemma "abs_series_bij" ("a" "aa!1 o phi!1" "phi" "x!2" "x" "x!1")) (("1" (split -1) (("1" (lemma "extensionality" ("f" "aa!1 o phi!1 o x!2" "g" "aa!1")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but (-2 -3 -4 -6 1)) (("2" (rewrite "assoc") (("2" (case-replace "phi!1 o x!2 = lambda (n:nat): n") (("1" (expand "o" 1) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "o") (("2" (lemma "comp_inverse_right_alt" ("f" "phi!1" "g" "x!2" "r" "x!3")) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "aa!1") (("2" (expand "absconvergent?") (("2" (hide-all-but (-1 -6 1)) (("2" (lemma "abs_series_bij_conv" ("a" "abs(aa!1)" "phi" "phi!1")) (("2" (split -1) (("1" (hide -2 -3) (("1" (expand "o ") (("1" (expand "abs") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (case-replace "abs(abs(aa!1)) = abs(aa!1)") (("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "abs_series_bij" ("a" "aa!1" "phi" "phi!1" "x" "x!1")) (("2" (assert) (("2" (typepred "aa!1") (("2" (expand "absconvergent?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bijective? const-decl "bool" functions nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (exists1 const-decl "bool" exists1 nil) (absconvergent_series nonempty-type-eq-decl nil absconv_series nil) (absconvergent? const-decl "bool" absconv_series nil) (O const-decl "T3" function_props nil) (sequence type-eq-decl nil sequences nil) (abs_series_bij formula-decl nil series_lems nil) (minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (abs const-decl "sequence[real]" series nil) (abs_series_bij_conv formula-decl nil series_lems nil) (extensionality formula-decl nil functions nil) (= const-decl "[T, T -> boolean]" equalities nil) (comp_inverse_right_alt formula-decl nil function_inverse_def nil) (assoc formula-decl nil function_props2 nil) (inverse? const-decl "bool" function_inverse_def nil) (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil) (bijective_inverse_exists formula-decl nil function_inverse_def nil)) shostak)) (abs_series_bij_conv_abs 0 (abs_series_bij_conv_abs-1 nil 3351601719 ("" (skosimp) (("" (lemma "abs_series_bij_abs" ("aa" "aa!1" "phi" "phi!1")) (("" (expand "convergent?") (("" (split) (("1" (skosimp*) (("1" (inst - "l!1") (("1" (inst + "l!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "l!1") (("2" (inst + "l!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bijective? const-decl "bool" functions nil) (absconvergent_series nonempty-type-eq-decl nil absconv_series nil) (absconvergent? const-decl "bool" absconv_series nil) (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (abs_series_bij_abs formula-decl nil absconv_series nil) (convergent? const-decl "bool" convergence_sequences "analysis/")) shostak)) (abs_series_bij_limit_abs_TCC1 0 (abs_series_bij_limit_abs_TCC1-1 nil 3351601341 ("" (skosimp) (("" (typepred "aa!1") (("" (expand "absconvergent?") (("" (lemma "abs_series_bij_conv" ("a" "aa!1" "phi" "phi!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((absconvergent_series nonempty-type-eq-decl nil absconv_series nil) (absconvergent? const-decl "bool" absconv_series nil) (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (bijective? const-decl "bool" functions nil) (abs_series_bij_conv formula-decl nil series_lems nil)) nil)) (abs_series_bij_limit_abs 0 (abs_series_bij_limit_abs-1 nil 3351601471 ("" (skosimp) (("" (lemma "abs_series_bij_abs" ("aa" "aa!1" "phi" "phi!1")) (("" (typepred "aa!1") (("" (expand "absconvergent?") (("" (inst - "limit(series(aa!1))") (("" (lemma "limit_equiv" ("s" "series(aa!1)" "l" "limit(series(aa!1))")) (("" (assert) (("" (lemma "absconvergent_series_is_convergent" ("x" "aa!1")) (("" (assert) (("" (rewrite "limit_equiv" -4) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bijective? const-decl "bool" functions nil) (absconvergent_series nonempty-type-eq-decl nil absconv_series nil) (absconvergent? const-decl "bool" absconv_series nil) (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (abs_series_bij_abs formula-decl nil absconv_series nil) (limit_equiv formula-decl nil convergence_ops "analysis/") (absconvergent_series_is_convergent judgement-tcc nil absconv_series nil) (O const-decl "T3" function_props nil) (series const-decl "sequence[real]" series nil) (limit const-decl "real" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (extract_convergent 0 (extract_convergent-1 nil 3323310225 ("" (expand "convergent?") (("" (skosimp*) (("" (inst + "l!1") (("" (lemma "convergence_subsequence" ("u1" "series(a!1)" "u2" "series(a!1) o f!1" "l" "l!1")) (("" (assert) (("" (hide-all-but 1) (("" (expand "subseq") (("" (inst + "f!1") (("" (expand "o") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((extraction type-eq-decl nil sequence_props "analysis/") (strict_increasing? const-decl "bool" real_fun_preds "reals/") (O const-decl "T3" function_props nil) (series const-decl "sequence[real]" series nil) (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (convergence_subsequence formula-decl nil convergence_sequences "analysis/") (subseq const-decl "bool" sequence_props "analysis/") (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (convergent? const-decl "bool" convergence_sequences "analysis/")) shostak)) (extract_comp 0 (extract_comp-1 nil 3323305712 ("" (skosimp) (("" (typepred "f!1") (("" (expand "o") (("" (expand "series") (("" (rewrite "extensionality_postulate" 1 :dir rl) (("1" (case "forall (n:nat): sigma(if n = 0 then 0 else f!1(n-1)+1 endif,f!1(n),LAMBDA n: IF EXISTS m (("1" (induct "x_1") (("1" (inst - "0") (("1" (replace -1) (("1" (hide -1) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "j!1+1") (("2" (assert) (("2" (assert) (("2" (expand "strict_increasing?") (("2" (inst - "j!1" "1+j!1") (("2" (assert) (("2" (expand "sigma" 1 1) (("2" (name-replace "F" "LAMBDA (n_1: nat): IF EXISTS (m_1: nat): n_1 = f!1(m_1) THEN a!1(n_1) ELSE 0 ENDIF") (("2" (replace -1 1) (("2" (hide -1) (("2" (replace -1 1 rl) (("2" (lemma "sigma_split" ("low" "0" "high" "f!1(1 + j!1)" "F" "F" "z" "f!1(j!1)")) (("2" (assert) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "f!1") (("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "strict_increasing?") (("2" (skosimp) (("2" (case-replace "n!1=0") (("1" (hide -1) (("1" (typepred "f!1(0)") (("1" (expand ">=") (("1" (expand "<=") (("1" (split -1) (("1" (expand "sigma" 1) (("1" (assert) (("1" (case-replace "EXISTS m: f!1(0) = f!1(m)") (("1" (assert) (("1" (hide -1) (("1" (lemma "sigma_restrict_eq[nat]" ("low" "0" "high" "f!1(0)-1" "F" "LAMBDA n: IF EXISTS m: n = f!1(m) THEN a!1(n) ELSE 0 ENDIF" "G" "LAMBDA n: 0")) (("1" (split -1) (("1" (rewrite "sigma_zero") nil nil) ("2" (hide 2) (("2" (expand "restrict") (("2" (apply-extensionality 1 :hide? t) (("2" (typepred "x!1") (("2" (case "x!1<f!1(0)") (("1" (assert) (("1" (case-replace "EXISTS m: x!1 = f!1(m)") (("1" (hide 1) (("1" (skosimp) (("1" (typepred "m!1") (("1" (expand ">=") (("1" (expand "<=" -1) (("1" (split -1) (("1" (inst - "0" "m!1") (("1" (assert) nil nil)) nil) ("2" (replace -1 * rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "0") nil nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (expand "sigma" 1) (("2" (case-replace "EXISTS m: 0 = f!1(m)") (("1" (expand "sigma") (("1" (propax) nil nil)) nil) ("2" (inst + "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "f!1(n!1 - 1)") (("2" (inst-cp - "n!1-1" "n!1") (("2" (assert) (("2" (expand "sigma" 2) (("2" (assert) (("2" (case-replace "EXISTS m: f!1(n!1) = f!1(m)") (("1" (case-replace "1 + f!1(n!1 - 1) = f!1(n!1)") (("1" (expand "sigma") (("1" (propax) nil nil)) nil) ("2" (assert) (("2" (hide -1) (("2" (lemma "sigma_restrict_eq[nat]" ("low" "1 + f!1(n!1 - 1)" "high" "f!1(n!1) - 1" "F" "LAMBDA n: IF EXISTS m: n = f!1(m) THEN a!1(n) ELSE 0 ENDIF" "G" "lambda n:0")) (("2" (split -1) (("1" (rewrite "sigma_zero[nat]") nil nil) ("2" (hide 4) (("2" (expand "restrict") (("2" (apply-extensionality 1 :hide? t) (("2" (typepred "x!1") (("2" (lift-if 1) (("2" (case-replace "x!1 < 1 + f!1(n!1 - 1) OR x!1 > f!1(n!1) - 1") (("2" (replace 1 2) (("2" (flatten) (("2" (case-replace "EXISTS m: x!1 = f!1(m)") (("1" (skosimp) (("1" (replace -1) (("1" (hide -1 3) (("1" (lemma "trich_lt" ("x" "m!1" "y" "n!1")) (("1" (split -1) (("1" (case "m!1=n!1-1") (("1" (assert) nil nil) ("2" (inst - "m!1" "n!1-1") (("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (inst - "n!1" "m!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 4) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((extraction type-eq-decl nil sequence_props "analysis/") (strict_increasing? const-decl "bool" real_fun_preds "reals/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (series const-decl "sequence[real]" series nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_split formula-decl nil sigma "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (f!1 skolem-const-decl "extraction" absconv_series nil) (sigma_zero formula-decl nil sigma "reals/") (restrict const-decl "[T -> real]" sigma "reals/") (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (sigma_restrict_eq formula-decl nil sigma "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (trich_lt formula-decl nil real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sequence type-eq-decl nil sequences nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (extensionality_postulate formula-decl nil functions nil) (O const-decl "T3" function_props nil)) shostak)) (subseq_absconvergent 0 (subseq_absconvergent-1 nil 3323310449 ("" (expand "subseq") (("" (skosimp*) (("" (typepred "bb!1") (("" (expand "absconvergent?") (("" (case-replace "series(abs(a!1)) = series(abs(bb!1) o f!1)") (("1" (hide -1 -3) (("1" (rewrite "extract_comp") (("1" (name-replace "DRL" "LAMBDA n: IF EXISTS m: n = f!1(m) THEN abs(bb!1)(n) ELSE 0 ENDIF") (("1" (lemma "comparison_test" ("b" "abs(bb!1)" "a" "DRL")) (("1" (split -1) (("1" (lemma "extract_convergent" ("a" "DRL" "f" "f!1")) (("1" (assert) nil nil)) nil) ("2" (propax) nil nil) ("3" (hide-all-but 1) (("3" (expand "abs" 1 2) (("3" (expand "DRL") (("3" (skosimp) (("3" (expand "abs" 1 2) (("3" (expand "abs" 1 3) (("3" (lift-if 1) (("3" (case-replace "EXISTS m: n!1 = f!1(m)") (("1" (expand "abs" 1 1) (("1" (case-replace "abs(bb!1(n!1)) < 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (expand "series") (("2" (rewrite "extensionality_postulate" 1 :dir rl) (("2" (expand "o") (("2" (case "FORALL (i:nat): abs(a!1(i)) = abs(bb!1(f!1(i)))") (("1" (hide -2) (("1" (expand "abs" 1) (("1" (induct "x") (("1" (expand "sigma") (("1" (inst - "0") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (inst - "1+j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst - "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((extensionality_postulate formula-decl nil functions nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (extract_convergent formula-decl nil absconv_series nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (DRL skolem-const-decl "[nat -> real]" absconv_series nil) (comparison_test formula-decl nil series nil) (extract_comp formula-decl nil absconv_series nil) (extraction type-eq-decl nil sequence_props "analysis/") (strict_increasing? const-decl "bool" real_fun_preds "reals/") (O const-decl "T3" function_props nil) (abs const-decl "sequence[real]" series nil) (series const-decl "sequence[real]" series nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (sequence type-eq-decl nil sequences nil) (absconvergent? const-decl "bool" absconv_series nil) (absconvergent_series nonempty-type-eq-decl nil absconv_series nil) (subseq const-decl "bool" sequence_props "analysis/")) shostak)) (nonneg_subseq 0 (nonneg_subseq-2 nil 3406890926 ("" (skosimp) (("" (lemma "subseq_absconvergent" ("a" "nna!1" "bb" "nnb!1")) (("1" (assert) (("1" (lemma "absconvergent_series_is_convergent" ("x" "nna!1")) (("1" (lemma "limit_nonneg" ("nna" "series(nna!1)")) (("1" (assert) (("1" (expand "convergent?") (("1" (skosimp) (("1" (lemma "limit_equiv" ("s" "series(nna!1)" "l" "l!1")) (("1" (inst + "l!1") (("1" (assert) (("1" (lemma "subseq_def" ("u" "nna!1" "v" "nnb!1")) (("1" (assert) (("1" (skosimp) (("1" (case "nna!1 = nnb!1 o f!1") (("1" (lemma "extract_comp" ("a" "nnb!1" "f" "f!1")) (("1" (expand "o" -1 1) (("1" (expand "o" -2) (("1" (replace -2 -1 rl) (("1" (lemma "limit_order" ("s1" "series(nna!1)" "l1" "l!1" "s2" "series(nnb!1) o f!1" "l2" "nny!1")) (("1" (replace -7) (("1" (lemma "convergence_subsequence" ("u1" "series(nnb!1)" "l" "nny!1" "u2" "series(nnb!1) o f!1")) (("1" (replace -11) (("1" (split -1) (("1" (replace -1 -2) (("1" (split -2) (("1" (propax) nil nil) ("2" (replace -2 1) (("2" (expand "o") (("2" (expand "series") (("2" (skosimp) (("2" (lemma "sigma_le" ("low" "0" "high" "f!1(n!1)" "F" "LAMBDA n: IF EXISTS m: n = f!1(m) THEN nnb!1(n) ELSE 0 ENDIF" "G" "nnb!1")) (("2" (split -1) (("1" (propax) nil nil) ("2" (skosimp) (("2" (lift-if 1) (("2" (prop) (("1" (skosimp) (("1" (assert) nil nil)) nil) ("2" (typepred "n!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "subseq") (("2" (inst + "f!1") (("2" (skosimp) (("2" (expand "o ") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "o ") (("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "series") (("2" (skosimp) (("2" (lemma "sigma_nonneg" ("low" "0" "high" "x1!1" "F" "nna!1")) (("2" (split -1) (("1" (propax) nil nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "absconvergent?") (("2" (expand "convergent?") (("2" (inst + "nny!1") (("2" (hide-all-but (-2 1)) (("2" (expand "convergence") (("2" (skosimp) (("2" (inst - "epsilon!1") (("2" (skosimp) (("2" (inst + "n!1") (("2" (skosimp) (("2" (inst - "i!1") (("2" (assert) (("2" (expand "abs" 1 2) (("2" (expand "abs" 1 2) (("2" (case-replace "(LAMBDA (n: nat): IF nnb!1(n) < 0 THEN -nnb!1(n) ELSE nnb!1(n) ENDIF) = nnb!1") (("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((absconvergent_series nonempty-type-eq-decl nil absconv_series nil) (absconvergent? const-decl "bool" absconv_series nil) (nnreal type-eq-decl nil real_types nil) (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (subseq_absconvergent formula-decl nil absconv_series nil) (absconvergent_series_is_convergent judgement-tcc nil absconv_series nil) (sigma_nonneg formula-decl nil sigma "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (l!1 skolem-const-decl "real" absconv_series nil) (subseq_def formula-decl nil sequence_props "analysis/") (extract_comp formula-decl nil absconv_series nil) (limit_order formula-decl nil convergence_ops "analysis/") (convergence_subsequence formula-decl nil convergence_sequences "analysis/") (NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sigma_le formula-decl nil sigma "reals/") (subseq const-decl "bool" sequence_props "analysis/") (extraction type-eq-decl nil sequence_props "analysis/") (strict_increasing? const-decl "bool" real_fun_preds "reals/") (O const-decl "T3" function_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (limit_equiv formula-decl nil convergence_ops "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (series const-decl "sequence[real]" series nil) (limit_nonneg formula-decl nil series_lems nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (minus_real_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "sequence[real]" series nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (convergence const-decl "bool" convergence_sequences "analysis/") (real_minus_real_is_real application-judgement "real" reals nil)) nil) (nonneg_subseq-1 nil 3324005273 ("" (skosimp) (("" (lemma "subseq_absconvergent" ("a" "nna!1" "bb" "nnb!1")) (("1" (assert) (("1" (lemma "absconvergent_series_is_convergent" ("x" "nna!1")) (("1" (lemma "limit_nonneg" ("nna" "series(nna!1)")) (("1" (assert) (("1" (expand "convergent?") (("1" (skosimp) (("1" (lemma "limit_equiv" ("s" "series(nna!1)" "l" "l!1")) (("1" (inst + "l!1") (("1" (assert) (("1" (lemma "subseq_def" ("a" "nna!1" "b" "nnb!1")) (("1" (assert) (("1" (skosimp) (("1" (case "nna!1 = nnb!1 o f!1") (("1" (lemma "extract_comp" ("a" "nnb!1" "f" "f!1")) (("1" (expand "o" -1 1) (("1" (expand "o" -2) (("1" (replace -2 -1 rl) (("1" (lemma "limit_order" ("s1" "series(nna!1)" "l1" "l!1" "s2" "series(nnb!1) o f!1" "l2" "nny!1")) (("1" (replace -7) (("1" (lemma "convergence_subsequence" ("u1" "series(nnb!1)" "l" "nny!1" "u2" "series(nnb!1) o f!1")) (("1" (replace -11) (("1" (split -1) (("1" (replace -1 -2) (("1" (split -2) (("1" (propax) nil nil) ("2" (replace -2 1) (("2" (expand "o") (("2" (expand "series") (("2" (skosimp) (("2" (lemma "sigma_le" ("low" "0" "high" "f!1(n!1)" "F" "LAMBDA n: IF EXISTS m: n = f!1(m) THEN nnb!1(n) ELSE 0 ENDIF" "G" "nnb!1")) (("2" (split -1) (("1" (propax) nil nil) ("2" (skosimp) (("2" (lift-if 1) (("2" (prop) (("1" (skosimp) (("1" (assert) nil nil)) nil) ("2" (typepred "n!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "subseq") (("2" (inst + "f!1") (("2" (skosimp) (("2" (expand "o ") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "o ") (("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "series") (("2" (skosimp) (("2" (lemma "sigma_nonneg" ("low" "0" "high" "x1!1" "F" "nna!1")) (("2" (split -1) (("1" (propax) nil nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "absconvergent?") (("2" (expand "convergent?") (("2" (inst + "nny!1") (("2" (hide-all-but (-2 1)) (("2" (expand "convergence") (("2" (skosimp) (("2" (inst - "epsilon!1") (("2" (skosimp) (("2" (inst + "n!1") (("2" (skosimp) (("2" (inst - "i!1") (("2" (assert) (("2" (expand "abs" 1 2) (("2" (expand "abs" 1 2) (("2" (case-replace "(LAMBDA (n: nat): IF nnb!1(n) < 0 THEN -nnb!1(n) ELSE nnb!1(n) ENDIF) = nnb!1") (("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_nonneg formula-decl nil sigma "reals/") (convergence_subsequence formula-decl nil convergence_sequences "analysis/") (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma_le formula-decl nil sigma "reals/") (subseq const-decl "bool" sequence_props "analysis/") (extraction type-eq-decl nil sequence_props "analysis/") (strict_increasing? const-decl "bool" real_fun_preds "reals/") (limit_equiv formula-decl nil convergence_ops "analysis/") (abs const-decl "sequence[real]" series nil) (convergence const-decl "bool" convergence_sequences "analysis/")) shostak)) (sum_absconvergent 0 (sum_absconvergent-1 nil 3323310709 ("" (skosimp) (("" (typepred "aa!1") (("" (typepred "bb!1") (("" (expand "absconvergent?") (("" (lemma "series_sum_conv" ("a" "abs(aa!1)" "b" "abs(bb!1)")) (("" (assert) (("" (lemma "comparison_test" ("b" "abs(aa!1) + abs(bb!1)" "a" "abs(aa!1 + bb!1)")) (("" (assert) (("" (hide-all-but 1) (("" (skosimp) (("" (expand "abs") (("" (expand "+") (("" (case-replace "abs(aa!1(n!1) + bb!1(n!1)) < 0") (("1" (lemma "triangle" ("x" "aa!1(n!1)" "y" "bb!1(n!1)")) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (lemma "triangle" ("x" "aa!1(n!1)" "y" "bb!1(n!1)")) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((absconvergent_series nonempty-type-eq-decl nil absconv_series nil) (absconvergent? const-decl "bool" absconv_series nil) (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_plus_real_is_real application-judgement "real" reals nil) (triangle formula-decl nil real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (comparison_test formula-decl nil series nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (series_sum_conv formula-decl nil series nil) (abs const-decl "sequence[real]" series nil)) shostak)) (opp_absconvergent 0 (opp_absconvergent-1 nil 3323311392 ("" (skosimp) (("" (typepred "aa!1") (("" (expand "absconvergent?") (("" (case-replace "abs(-aa!1) = abs(aa!1)") (("1" (hide-all-but 1) (("1" (expand "-") (("1" (expand "abs") (("1" (apply-extensionality :hide? t) (("1" (expand "abs") (("1" (lemma "trichotomy" ("x" "aa!1(x!1)")) (("1" (split -1) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "abs") (("2" (case-replace "aa!1(n!1) < 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "abs") (("2" (expand "abs") (("2" (skosimp) (("2" (lemma "trichotomy" ("x" "aa!1(x1!1)")) (("2" (split -1) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((absconvergent_series nonempty-type-eq-decl nil absconv_series nil) (absconvergent? const-decl "bool" absconv_series nil) (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (abs const-decl "sequence[real]" series nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (aa!1 skolem-const-decl "absconvergent_series" absconv_series nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (trichotomy formula-decl nil real_axioms nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (minus_real_is_real application-judgement "real" reals nil)) shostak)) (diff_absconvergent 0 (diff_absconvergent-1 nil 3323311541 ("" (skosimp) (("" (typepred "bb!1") (("" (lemma "opp_absconvergent" ("aa" "bb!1")) (("" (lemma "sum_absconvergent" ("aa" "aa!1" "bb" "-bb!1")) (("1" (expand "-") (("1" (expand "+") (("1" (case-replace "(LAMBDA (x_1: nat): aa!1(x_1) + -bb!1(x_1)) = (LAMBDA (x: nat): aa!1(x) - bb!1(x))") (("1" (hide-all-but 1) (("1" (apply-extensionality :hide? t) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ((absconvergent_series nonempty-type-eq-decl nil absconv_series nil) (absconvergent? const-decl "bool" absconv_series nil) (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (sum_absconvergent formula-decl nil absconv_series nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (opp_absconvergent formula-decl nil absconv_series nil)) shostak)) (scal_absconvergent 0 (scal_absconvergent-1 nil 3323311650 ("" (skosimp) (("" (case "forall (px:posreal): absconvergent?(px * aa!1)") (("1" (lemma "trichotomy" ("x" "x!1")) (("1" (split -1) (("1" (inst - "x!1") (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (hide-all-but 1) (("2" (expand "absconvergent?") (("2" (expand "*") (("2" (case-replace "abs(LAMBDA (x: nat): 0 * aa!1(x)) = LAMBDA (x: nat): 0") (("1" (rewrite "zero_series_conv") nil nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (expand "abs") (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (inst - "-x!1") (("1" (lemma "opp_absconvergent" ("aa" "-x!1 * aa!1")) (("1" (case-replace "-(-x!1 * aa!1) = x!1 * aa!1") (("1" (hide-all-but 1) (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "aa!1") (("2" (skosimp) (("2" (expand "absconvergent?") (("2" (lemma "convergent_scal" ("s1" "series(abs(aa!1))" "a" "px!1")) (("2" (assert) (("2" (hide -2) (("2" (case-replace "series(abs(px!1 * aa!1)) = px!1 * series(abs(aa!1))") (("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (expand "series") (("2" (expand "abs") (("2" (expand "*") (("2" (rewrite "sigma_scal[nat]" 1 :dir rl) (("2" (lemma "sigma_eq[nat]" ("low" "0" "high" "x!2" "F" "LAMBDA (n: nat): abs(px!1 * aa!1(n))" "G" "LAMBDA (i: nat): px!1 * abs(aa!1(i))")) (("2" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp*) (("2" (rewrite "abs_mult" 1) (("2" (expand "abs" 1 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((absconvergent_series nonempty-type-eq-decl nil absconv_series nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (absconvergent? const-decl "bool" absconv_series nil) (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (x!1 skolem-const-decl "real" absconv_series nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (zero_series_conv formula-decl nil series nil) (real_times_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (abs const-decl "sequence[real]" series nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (opp_absconvergent formula-decl nil absconv_series nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (minus_real_is_real application-judgement "real" reals nil) (trichotomy formula-decl nil real_axioms nil) (NOT const-decl "[bool -> bool]" booleans nil) (sigma_scal formula-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (abs_mult formula-decl nil real_props nil) (subrange type-eq-decl nil integers nil) (sigma_eq formula-decl nil sigma "reals/") (convergent_scal formula-decl nil convergence_ops "analysis/") (series const-decl "sequence[real]" series nil)) shostak)))
¤ Dauer der Verarbeitung: 0.55 Sekunden (vorverarbeitet am 2026-04-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26