| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/series/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 310 kB |
|
Impressum series.prfInteraktion undPortierbarkeitLisp |
|||||||||||||||
|
(series (series_TCC1 0 (series_TCC1-1 nil 3374405059 ("" (subtype-tcc) nil nil) nil nil)) (inf_sum_TCC1 0 (inf_sum_TCC1-1 nil 3249311615 ("" (subtype-tcc) nil 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) (conv_series? const-decl "bool" series nil) (series const-decl "sequence[real]" series nil) (convergence const-decl "bool" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (inf_sum_TCC2 0 (inf_sum_TCC2-1 nil 3298729340 ("" (skosimp*) (("" (assert) (("" (typepred "a!1") (("" (expand "conv_series?") (("" (propax) nil nil)) nil)) nil)) nil)) 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) (conv_series? const-decl "bool" series nil)) shostak)) (series_diff 0 (series_diff-1 nil 3299339188 ("" (skosimp*) (("" (expand "series") (("" (apply-extensionality 1 :hide? t) (("" (expand "-") (("" (rewrite "sigma_minus") nil nil)) nil)) nil)) nil)) nil) ((series const-decl "sequence[real]" series nil) (sigma_minus formula-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) (- const-decl "[T -> real]" real_fun_ops "reals/") (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/") (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)) nil)) (series_sum 0 (series_sum-2 nil 3299339288 ("" (skosimp*) (("" (expand "series") (("" (apply-extensionality 1 :hide? t) (("" (expand "+") (("" (rewrite "sigma_sum") nil nil)) nil)) nil)) nil)) nil) ((series const-decl "sequence[real]" series nil) (sigma_sum formula-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) (+ const-decl "[T -> real]" real_fun_ops "reals/") (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/") (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)) nil) (series_sum-1 nil 3299339277 ("" (postpone) nil nil) nil shostak)) (series_m_diff 0 (series_m_diff-1 nil 3299339692 ("" (skosimp*) (("" (expand "series") (("" (apply-extensionality 1 :hide? t) (("" (expand "-") (("" (rewrite "sigma_minus") nil nil)) nil)) nil)) nil)) nil) ((series const-decl "sequence[real]" series nil) (sigma_minus formula-decl nil sigma "reals/") (- const-decl "[T -> real]" real_fun_ops "reals/") (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/") (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)) nil)) (series_m_sum 0 (series_m_sum-1 nil 3299339707 ("" (skosimp*) (("" (expand "series") (("" (apply-extensionality 1 :hide? t) (("" (expand "+") (("" (rewrite "sigma_sum") nil nil)) nil)) nil)) nil)) nil) ((series const-decl "sequence[real]" series nil) (sigma_sum formula-decl nil sigma "reals/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (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/") (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)) nil)) (series_m_scal 0 (series_m_scal-1 nil 3299339880 ("" (skosimp*) (("" (expand "series") (("" (expand "*") (("" (apply-extensionality 1 :hide? t) (("" (lemma "sigma_scal") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((series const-decl "sequence[real]" series 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) (numfield nonempty-type-eq-decl nil number_fields 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (sigma_scal formula-decl nil sigma "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/")) shostak)) (series_m_eq 0 (series_m_eq-1 nil 3299339979 ("" (skosimp*) (("" (expand "series") (("" (apply-extensionality 1 :hide? t) (("" (rewrite "sigma_eq") (("" (skosimp*) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((series const-decl "sequence[real]" series nil) (sigma_eq formula-decl nil sigma "reals/") (subrange type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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/") (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)) (series_scal 0 (series_scal-1 nil 3299339856 ("" (skosimp*) (("" (expand "series") (("" (expand "*") (("" (apply-extensionality 1 :hide? t) (("" (lemma "sigma_scal") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((series const-decl "sequence[real]" series 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) (numfield nonempty-type-eq-decl nil number_fields 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_scal formula-decl nil sigma "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/")) shostak)) (conv_series_terms_to_0 0 (conv_series_terms_to_0-2 nil 3299836761 ("" (skosimp*) (("" (lemma "convergence_cauchy1") (("" (inst?) (("" (assert) (("" (hide -2) (("" (expand "convergence") (("" (skosimp*) (("" (expand "cauchy") (("" (inst - "epsilon!1") (("" (skosimp*) (("" (inst 1 "n!1+1") (("" (skosimp*) (("" (expand "series") (("" (inst - "i!1" "i!1-1") (("1" (assert) (("1" (expand "sigma" -1 1) (("1" (propax) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((convergence_cauchy1 formula-decl nil convergence_sequences "analysis/") (convergence const-decl "bool" convergence_sequences "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (cauchy const-decl "bool" convergence_sequences "analysis/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (i!1 skolem-const-decl "nat" series nil) (sigma def-decl "real" sigma "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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) (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) (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)) nil) (conv_series_terms_to_0-1 nil 3249311615 ("" (skosimp*) (("" (lemma "sc_lem") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) nil nil)) (series_limit_0_TCC1 0 (series_limit_0_TCC1-1 nil 3297507108 ("" (skosimp*) (("" (lemma "conv_series_terms_to_0") (("" (inst?) (("" (assert) (("" (hide -2) (("" (expand "convergent?") (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((conv_series_terms_to_0 formula-decl nil series nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (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)) (series_limit_0 0 (series_limit_0-1 nil 3297504127 ("" (skosimp*) (("" (lemma "conv_series_terms_to_0") (("" (inst?) (("" (assert) (("" (hide -2) (("" (rewrite "limit_def") (("" (expand "convergent?") (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((conv_series_terms_to_0 formula-decl nil series nil) (limit_def formula-decl nil convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (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)) (convergent_abs 0 (convergent_abs-1 nil 3249311615 ("" (skosimp*) (("" (lemma "convergence_cauchy1") (("" (inst?) (("" (assert) (("" (hide -2) (("" (lemma "convergence_cauchy2") (("" (inst?) (("" (assert) (("" (hide 2) (("" (expand "cauchy") (("" (skosimp*) (("" (inst? -) (("" (skosimp*) (("" (inst?) (("" (skosimp*) (("" (inst - "i!1" "j!1") (("" (assert) (("" (expand "series") (("" (case-replace "i!1 = j!1") (("1" (assert) nil nil) ("2" (case-replace "i!1 < j!1") (("1" (rewrite "sigma_diff_neg") (("1" (rewrite "sigma_diff_neg") (("1" (lemma "sigma_abs") (("1" (inst?) (("1" (case-replace "(LAMBDA (n:nat): abs(a!1(n))) = abs(a!1)") (("1" (hide -1) (("1" (assert) (("1" (grind :exclude "sigma") nil nil)) nil)) nil) ("2" (hide -1 -5 3) (("2" (apply-extensionality :hide? t) (("1" (grind) nil nil) ("2" (skosimp*) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sigma_diff") (("2" (inst?) (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (rewrite "sigma_diff") (("2" (lemma "sigma_abs") (("2" (inst?) (("2" (assert) (("2" (case "(LAMBDA (n:nat): abs(a!1(n))) = abs(a!1)") (("1" (replace -1) (("1" (hide -1) (("1" (assert) nil nil)) nil)) nil) ("2" (hide -1 4) (("2" (apply-extensionality 1 :hide? t) (("1" (hide -3) (("1" (grind) nil nil)) nil) ("2" (skosimp*) (("2" (hide -3) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((convergence_cauchy1 formula-decl nil convergence_sequences "analysis/") (convergence_cauchy2 formula-decl nil convergence_sequences "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (cauchy const-decl "bool" convergence_sequences "analysis/") (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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (a!1 skolem-const-decl "sequence[real]" series nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sigma_abs formula-decl nil sigma "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (sigma_diff_neg 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/") (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (sigma_diff formula-decl nil sigma "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs const-decl "sequence[real]" series 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) (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)) nil)) (partial_sums 0 (partial_sums-1 nil 3249311615 ("" (skosimp*) (("" (prop) (("1" (lemma "convergence_cauchy1") (("1" (inst?) (("1" (assert) (("1" (hide -2) (("1" (expand "cauchy") (("1" (skosimp*) (("1" (inst -1 "epsilon!1") (("1" (skosimp*) (("1" (inst 1 "n!1+1") (("1" (skosimp*) (("1" (expand "series") (("1" (inst -1 "n!2" "m!1") (("1" (assert) (("1" (case "sigma(0, n!2, a!1) - sigma(0, m!1, a!1) = sigma(m!1+1, n!2, a!1)") (("1" (replace -1) (("1" (hide -1) (("1" (expand "abs") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (lemma "sigma_diff") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "convergence_cauchy2") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (expand "cauchy") (("2" (skosimp*) (("2" (inst - "epsilon!1") (("2" (skosimp*) (("2" (inst 1 "N!1") (("2" (skosimp*) (("2" (expand "series") (("2" (case "i!1 = j!1") (("1" (replace -1) (("1" (assert) (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (case "i!1 < j!1") (("1" (rewrite "sigma_diff_neg") (("1" (inst?) (("1" (assert) (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "sigma_diff") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (series const-decl "sequence[real]" series nil) (= const-decl "[T, T -> boolean]" equalities nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sigma_diff formula-decl nil sigma "reals/") (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posint nonempty-type-eq-decl nil integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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) (cauchy const-decl "bool" convergence_sequences "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (convergence_cauchy1 formula-decl nil convergence_sequences "analysis/") (abs_0 formula-decl nil abs_lems "reals/") (sigma_diff_neg formula-decl nil sigma "reals/") (minus_real_is_real application-judgement "real" reals nil) (< const-decl "bool" reals nil) (convergence_cauchy2 formula-decl nil convergence_sequences "analysis/")) nil)) (zero_series_conv 0 (zero_series_conv-1 nil 3249311615 ("" (expand "convergent?") (("" (inst + "0") (("" (expand "convergence") (("" (skosimp*) (("" (inst 1 "1") (("" (skosimp*) (("" (expand "series") (("" (rewrite "sigma_const") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((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) (sigma_const 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/") (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_times_even_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (series const-decl "sequence[real]" series nil) (sigma_nat application-judgement "nat" sigma_nat "reals/") (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (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 const-decl "bool" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/")) nil)) (zero_series_limit_TCC1 0 (zero_series_limit_TCC1-1 nil 3249311615 ("" (rewrite "zero_series_conv") nil nil) ((zero_series_conv formula-decl nil series nil)) nil)) (zero_series_limit 0 (zero_series_limit-1 nil 3249311615 ("" (rewrite "limit_def") (("1" (expand "convergence") (("1" (skosimp*) (("1" (inst 1 "1") (("1" (skosimp*) (("1" (expand "series") (("1" (rewrite "sigma_const") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "zero_series_conv") nil nil)) nil)) nil) ((convergence const-decl "bool" convergence_sequences "analysis/") (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (sigma_nat application-judgement "nat" sigma_nat "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_times_even_is_even application-judgement "even_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (sigma_const 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/") (series const-decl "sequence[real]" series nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (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) (limit_def formula-decl nil convergence_sequences "analysis/")) nil)) (tail_series_conv 0 (tail_series_conv-1 nil 3249311615 ("" (skosimp*) (("" (case-replace "N!1 = 0") (("1" (case-replace "a!1 = (LAMBDA n: a!1(n + 0))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) nil nil)) nil)) nil) ("2" (expand "series") (("2" (expand "convergent?") (("2" (skosimp*) (("2" (name "AA" "sigma(0, N!1-1, a!1)") (("1" (inst + "l!1-AA") (("1" (expand "convergence") (("1" (skosimp*) (("1" (inst -2 "epsilon!1") (("1" (skosimp*) (("1" (inst + "n!1") (("1" (skosimp*) (("1" (lemma "sigma_shift") (("1" (inst?) (("1" (assert) (("1" (replace -1 * rl) (("1" (hide -1) (("1" (replace -1 * rl) (("1" (inst -2 "N!1+i!1") (("1" (assert) (("1" (lemma "sigma_split") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sequence type-eq-decl nil sequences nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (convergence const-decl "bool" convergence_sequences "analysis/") (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sigma_shift formula-decl nil sigma_nat "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) (sigma_split formula-decl nil sigma "reals/") (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (series const-decl "sequence[real]" series nil)) nil)) (tail_series_conv2 0 (tail_series_conv2-1 nil 3249311615 ("" (skosimp*) (("" (case-replace "N!1 = 0") (("1" (case-replace "a!1 = (LAMBDA n: a!1(n + 0))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) nil nil)) nil)) nil) ("2" (expand "series") (("2" (expand "convergent?") (("2" (skosimp*) (("2" (name "AA" "sigma(0, N!1-1, a!1)") (("1" (inst + "l!1+AA") (("1" (expand "convergence") (("1" (skosimp*) (("1" (inst -2 "epsilon!1") (("1" (skosimp*) (("1" (inst + "n!1+N!1") (("1" (skosimp*) (("1" (inst -2 "i!1-N!1") (("1" (assert) (("1" (assert) (("1" (lemma "sigma_shift") (("1" (inst?) (("1" (assert) (("1" (replace -1 * rl) (("1" (hide -1) (("1" (lemma "sigma_split") (("1" (inst -1 "a!1" "i!1" "0" "N!1-1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sequence type-eq-decl nil sequences nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (convergence const-decl "bool" convergence_sequences "analysis/") (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (i!1 skolem-const-decl "nat" series nil) (N!1 skolem-const-decl "nat" series nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_split formula-decl nil sigma "reals/") (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (sigma_shift formula-decl nil sigma_nat "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (series const-decl "sequence[real]" series nil)) nil)) (conv_series_shift 0 (conv_series_shift-1 nil 3298646790 ("" (skosimp*) (("" (prop) (("1" (lemma "tail_series_conv") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "tail_series_conv2") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((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) (tail_series_conv formula-decl nil series nil) (tail_series_conv2 formula-decl nil series nil)) shostak)) (tail_conv 0 (tail_conv-1 nil 3249311615 ("" (skosimp*) (("" (lemma "tail_series_conv") (("" (inst?) (("" (inst -1 "N!1") (("" (assert) (("" (hide -2) (("" (lemma "tail_series_conv2") (("" (inst -1 "N!1" "b!1") (("" (assert) (("" (hide 2) (("" (case-replace "series(LAMBDA n: a!1(n + N!1)) = series(LAMBDA n: b!1(n + N!1))") (("" (hide -1 2) (("" (expand "series") (("" (apply-extensionality 1 :hide? t) (("" (rewrite "sigma_eq") (("" (hide 2) (("" (skosimp*) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tail_series_conv formula-decl nil series 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (subrange type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_eq formula-decl nil sigma "reals/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (series const-decl "sequence[real]" series nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (tail_series_conv2 formula-decl nil 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)) nil)) (end_series_conv 0 (end_series_conv-1 nil 3297672929 ("" (skosimp*) (("" (expand "series") (("" (case "m!1 = 0") (("1" (ground) nil nil) ("2" (prop) (("1" (expand "convergent?") (("1" (skosimp*) (("1" (inst + "l!1 - sigma(0, m!1-1, a!1)") (("1" (expand "convergence") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "n!1") (("1" (skosimp*) (("1" (case "m!1 - 1 >= i!1") (("1" (expand "sigma" 1 2) (("1" (assert) (("1" (inst - "m!1-1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (rewrite "sigma_split" :dir rl) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "convergent?") (("2" (skosimp*) (("2" (inst + "l!1 + sigma(0, m!1-1, a!1)") (("1" (expand "convergence") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "max(n!1,m!1)") (("1" (skosimp*) (("1" (expand "max") (("1" (lift-if) (("1" (ground) (("1" (lemma "sigma_split") (("1" (inst - "a!1" "i!1" "0" "m!1-1") (("1" (assert) (("1" (replace -1) (("1" (assert) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sigma_split") (("2" (inst - "a!1" "i!1" "0" "m!1-1") (("2" (assert) (("2" (replace -1) (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((series const-decl "sequence[real]" series nil) (series const-decl "sequence[real]" series nil) (real_plus_real_is_real application-judgement "real" reals nil) (convergence const-decl "bool" convergence_sequences "analysis/") (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (real_gt_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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_split formula-decl nil sigma "reals/") (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) (m!1 skolem-const-decl "nat" series nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_times_real_is_real application-judgement "real" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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)) shostak)) (scal_series_conv 0 (scal_series_conv-1 nil 3299840486 ("" (skosimp*) (("" (case-replace "c!1 = 0") (("1" (hide -1 -2) (("1" (expand "*") (("1" (assert) (("1" (lemma "zero_series_conv") (("1" (case "(LAMBDA (x: nat): 0 * series(a!1)(x)) = series(LAMBDA n: 0)") (("1" (replace -1 +) (("1" (propax) nil nil)) nil) ("2" (hide -1 2) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "series") (("2" (assert) (("2" (lemma "sigma_const") (("2" (inst?) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "convergent?") (("2" (skosimp*) (("2" (inst + "c!1*l!1") (("2" (expand "convergence") (("2" (skosimp*) (("2" (inst -1 "epsilon!1/abs(c!1)") (("1" (skosimp*) (("1" (inst + "n!1") (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (assert) (("1" (expand "*") (("1" (case-replace "c!1 * series(a!1)(i!1) - c!1 * l!1 = c!1 * (series(a!1)(i!1) - l!1)") (("1" (hide -1) (("1" (rewrite "abs_mult") (("1" (lemma "both_sides_div_pos_lt1") (("1" (inst -1 "abs(c!1)" "abs(c!1) * abs((series(a!1)(i!1) - l!1)) " "epsilon!1") (("1" (assert) nil nil) ("2" (hide -1 3) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (typepred "epsilon!1") (("2" (rewrite "pos_div_ge") (("1" (rewrite "pos_div_gt") (("1" (grind) nil nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 3) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (zero_series_conv formula-decl nil series nil) (sigma_const formula-decl nil sigma "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_times_even_is_even application-judgement "even_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (sigma_nat application-judgement "nat" sigma_nat "reals/") (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) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sequence type-eq-decl nil sequences nil) (series const-decl "sequence[real]" series nil) (real_minus_real_is_real application-judgement "real" reals nil) (convergence const-decl "bool" convergence_sequences "analysis/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (/= const-decl "boolean" notequal nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (c!1 skolem-const-decl "real" series nil) (epsilon!1 skolem-const-decl "posreal" series nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs_mult formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (both_sides_div_pos_lt1 formula-decl nil real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (pos_div_gt formula-decl nil real_props nil) (pos_div_ge formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (convergent? const-decl "bool" convergence_sequences "analysis/")) nil)) (conv_series_scal 0 (conv_series_scal-3 nil 3299840513 ("" (skosimp*) (("" (prop) (("1" (lemma "scal_series_conv") (("1" (inst - "(LAMBDA (x: nat): cnz!1 * a!1(x))" "1/cnz!1") (("1" (expand "*") (("1" (lemma "series_scal") (("1" (inst - "(LAMBDA (x: nat): cnz!1 * a!1(x))" "1/cnz!1") (("1" (assert) (("1" (expand "*") (("1" (replace -1) (("1" (assert) (("1" (hide -1) (("1" (case-replace "(LAMBDA n: 1 / cnz!1 * (cnz!1 * a!1(n))) = a!1") (("1" (assert) (("1" (hide 2) (("1" (lemma "series_scal") (("1" (inst?) (("1" (expand "*") (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "scal_series_conv") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_times_real_is_real application-judgement "real" reals 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) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (series_scal formula-decl nil series nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (scal_series_conv formula-decl nil series nil)) nil) (conv_series_scal-2 nil 3297419186 ("" (skosimp*) (("" (prop) (("1" (lemma "convergent_scal") (("1" (inst - "(LAMBDA (x: nat): cnz!1 * a!1(x))" "1/cnz!1") (("1" (expand "*") (("1" (lemma "series_scal") (("1" (inst - "(LAMBDA (x: nat): cnz!1 * a!1(x))" "1/cnz!1") (("1" (assert) (("1" (expand "*") (("1" (replace -1) (("1" (assert) (("1" (hide -1) (("1" (case-replace "(LAMBDA n: 1 / cnz!1 * (cnz!1 * a!1(n))) = a!1") (("1" (assert) (("1" (hide 2) (("1" (lemma "series_scal") (("1" (inst?) (("1" (expand "*") (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "convergent_scal") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) nil nil) (conv_series_scal-1 nil 3297418252 ("" (skosimp*) (("" (prop) (("1" (lemma "convergent_scal") (("1" (inst - "(LAMBDA (x: nat): c!1 * a!1(x))" "1/c!1") (("1" (expand "*") (("1" (lemma "series_scal") (("1" (inst - "(LAMBDA (x: nat): c!1 * a!1(x))" "1/c!1") (("1" (assert) (("1" (expand "*") (("1" (replace -1) (("1" (assert) (("1" (hide -1) (("1" (case-replace "(LAMBDA n: 1 / c!1 * (c!1 * a!1(n))) = a!1") (("1" (assert) (("1" (hide 2) (("1" (lemma "series_scal") (("1" (inst?) (("1" (expand "*") (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("2" (postpone) nil nil)) nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (lemma "convergent_scal") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) nil shostak)) (limit_series_shift_TCC1 0 (limit_series_shift_TCC1-1 nil 3249311615 ("" (assert) (("" (skosimp*) (("" (assert) (("" (lemma "conv_series_shift") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (limit_series_shift_TCC2 0 (limit_series_shift_TCC2-1 nil 3374405059 ("" (skosimp*) (("" (lemma "conv_series_shift") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((conv_series_shift formula-decl nil series nil) (sequence type-eq-decl nil sequences nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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)) nil)) (limit_series_shift 0 (limit_series_shift-1 nil 3249311615 ("" (skosimp*) (("" (rewrite "limit_def") (("1" (name "LSH" "limit(series(LAMBDA n: a!1(pn!1 + n)))") (("1" (replace -1) (("1" (rewrite "limit_def") (("1" (hide -2) (("1" (expand "convergence") (("1" (skosimp*) (("1" (inst -1 "epsilon!1") (("1" (skosimp*) (("1" (inst + "n!1+pn!1") (("1" (skosimp*) (("1" (inst -1 "i!1-pn!1") (("1" (assert) (("1" (expand "series") (("1" (lemma "sigma_split") (("1" (inst -1 "a!1" "i!1" "0" "pn!1-1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (lemma "sigma_shift") (("1" (inst -1 "a!1" "i!1-pn!1" "0" "pn!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "tail_series_conv") nil nil)) nil)) nil) ("2" (rewrite "tail_series_conv") nil nil)) nil) ("2" (rewrite "tail_series_conv") nil nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (limit_def formula-decl nil convergence_sequences "analysis/") (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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (sequence type-eq-decl nil sequences nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (limit const-decl "real" convergence_sequences "analysis/") (series const-decl "sequence[real]" series 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) (tail_series_conv formula-decl nil series nil) (sigma_split formula-decl nil sigma "reals/") (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_shift formula-decl nil sigma_nat "reals/") (int_plus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (pn!1 skolem-const-decl "posnat" series nil) (i!1 skolem-const-decl "nat" series nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types 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) (= const-decl "[T, T -> boolean]" equalities nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (limit_pos 0 (limit_pos-1 nil 3249311615 ("" (skosimp*) (("" (lemma "limit_def") (("" (inst -1 "limit(a!1)" "a!1") (("" (assert) (("" (expand "convergence") (("" (inst -1 "-limit(a!1)/2") (("" (skosimp*) (("" (inst -1 "n!1") (("" (assert) (("" (grind :exclude "limit") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((limit_def formula-decl nil convergence_sequences "analysis/") (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) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals 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) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (convergence const-decl "bool" convergence_sequences "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (limit const-decl "real" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (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)) nil)) (series_first_TCC1 0 (series_first_TCC1-1 nil 3299340007 ("" (skosimp*) (("" (lemma "end_series_conv") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((end_series_conv formula-decl nil 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)) (series_first 0 (series_first-1 nil 3299339903 ("" (skosimp*) (("" (copy -1) (("" (hide -1) (("" (expand "series") (("" (lemma "sigma_first") (("" (inst?) (("" (case-replace "(LAMBDA (n: nat): sigma(0, n, a!1)) = (LAMBDA (n: nat): a!1(0) + sigma(1, n, a!1))") (("1" (hide -1 -2) (("1" (lemma "limit_sum") (("1" (inst - "(LAMBDA (n: nat): sigma(1, n, a!1))" "(LAMBDA (n: nat): a!1(0))") (("1" (expand "+") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "limit_const") (("1" (inst - "a!1(0)") (("1" (expand "const_fun") (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "convergent_const") (("2" (expand "const_fun") (("2" (inst?) nil nil)) nil)) nil)) nil) ("3" (case "convergent?(series(a!1))") (("1" (hide 2) (("1" (lemma "end_series_conv") (("1" (inst?) (("1" (inst - "1") (("1" (assert) (("1" (expand "series") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (reveal -5) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (inst?) (("2" (assert) (("2" (expand "sigma") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((series const-decl "sequence[real]" series nil) (series const-decl "sequence[real]" series nil) (int_minus_int_is_int application-judgement "int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (T_low type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (sequence type-eq-decl nil sequences nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (convergent? const-decl "bool" convergence_sequences "analysis/") (a!1 skolem-const-decl "sequence[real]" series nil) (limit_const formula-decl nil convergence_ops "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (convergent_const formula-decl nil convergence_ops "analysis/") (end_series_conv formula-decl nil series nil) (limit_sum formula-decl nil convergence_ops "analysis/") (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) (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma_first formula-decl nil sigma "reals/") (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)) shostak)) (inf_sum_scal_TCC1 0 (inf_sum_scal_TCC1-1 nil 3299340007 ("" (skosimp*) (("" (expand "conv_series?") (("" (propax) nil nil)) nil)) nil) ((conv_series? const-decl "bool" series nil)) shostak)) (inf_sum_scal_TCC2 0 (inf_sum_scal_TCC2-1 nil 3299340007 ("" (skosimp*) (("" (expand "conv_series?") (("" (lemma "conv_series_scal") (("" (inst?) (("" (inst - "c!1") (("1" (assert) (("1" (lemma "end_series_conv") (("1" (inst?) (("1" (assert) (("1" (rewrite "series_scal") (("1" (assert) (("1" (hide -1) (("1" (lemma "end_series_conv") (("1" (assert) (("1" (inst - "(LAMBDA n: c!1 * a!1(n))" "k!1") (("1" (assert) (("1" (expand "series") (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (replace -1) (("2" (expand "*") (("2" (hide -) (("2" (lemma "end_series_conv") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (lemma "zero_series_conv") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((conv_series? const-decl "bool" series 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) (zero_series_conv formula-decl nil series nil) (series_scal formula-decl nil series nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (series const-decl "sequence[real]" series nil) (series const-decl "sequence[real]" series nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (end_series_conv formula-decl nil series nil) (nzreal nonempty-type-eq-decl nil reals nil) (c!1 skolem-const-decl "real" series nil) (/= const-decl "boolean" notequal nil) (conv_series_scal formula-decl nil series nil)) shostak)) (inf_sum_scal 0 (inf_sum_scal-1 nil 3299339613 ("" (skosimp*) (("" (expand "inf_sum") (("" (lemma "limit_scal") (("" (inst - "c!1" "series(a!1,k!1)") (("" (assert) (("" (lemma "series_m_scal") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((inf_sum const-decl "real" series 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) (convergent? const-decl "bool" convergence_sequences "analysis/") (series const-decl "sequence[real]" series nil) (series_m_scal formula-decl nil series nil) (real_times_real_is_real application-judgement "real" reals nil) (limit_scal formula-decl nil convergence_ops "analysis/")) nil)) (comparison_test 0 (comparison_test-1 nil 3249311615 ("" (skosimp*) (("" (lemma "convergence_cauchy1") (("" (inst -1 "series(b!1)") (("" (assert) (("" (lemma "convergence_cauchy2") (("" (inst -1 "series(a!1)") (("" (assert) (("" (hide -2 2) (("" (expand "cauchy") (("" (skosimp*) (("" (inst? -) (("" (skosimp*) (("" (inst?) (("" (skosimp*) (("" (inst -3 "i!1" "j!1") (("" (assert) (("" (case-replace "i!1 = j!1") (("1" (assert) nil nil) ("2" (expand "series") (("2" (case "i!1 < j!1") (("1" (rewrite "sigma_diff_neg" +) (("1" (rewrite "sigma_diff_neg") (("1" (lemma "sigma_abs") (("1" (inst?) (("1" (lemma "sigma_abs_bnd") (("1" (inst - "a!1" "b!1" "j!1" "1+i!1") (("1" (split -1) (("1" (case-replace "abs(-sigma(1 + i!1, j!1, a!1)) = abs(sigma(1 + i!1, j!1, a!1))") (("1" (hide -1) (("1" (case "sigma(1 + i!1, j!1, b!1) <= abs(-sigma(1 + i!1, j!1, b!1))") (("1" (assert) nil nil) ("2" (hide -1 -2 -6 -7 3) (("2" (grind :exclude "sigma") nil nil)) nil)) nil)) nil) ("2" (hide -1 -2 -6 -7 3) (("2" (grind :exclude "sigma") nil nil)) nil)) nil) ("2" (hide -1 -4 3) (("2" (skosimp*) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "sigma_diff") (("2" (rewrite "sigma_diff") (("2" (lemma "sigma_abs") (("2" (inst?) (("2" (lemma "sigma_abs_bnd") (("2" (inst - "a!1" "b!1" "i!1" "1+j!1") (("2" (split -1) (("1" (case "sigma(1 + i!1, j!1, b!1) <= abs(sigma(1 + i!1, j!1, b!1))") (("1" (assert) nil nil) ("2" (hide -1 -2 -5 -6 4) (("2" (grind :exclude "sigma") nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((convergence_cauchy1 formula-decl nil convergence_sequences "analysis/") (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) (sigma_diff formula-decl nil sigma "reals/") (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) (sigma_diff_neg formula-decl nil sigma "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (minus_real_is_real application-judgement "real" reals nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_abs formula-decl nil sigma "reals/") (sigma_abs_bnd formula-decl nil sigma "reals/") (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sigma def-decl "real" sigma "reals/") (subrange type-eq-decl nil integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (< const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities 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) (cauchy const-decl "bool" convergence_sequences "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (convergence_cauchy2 formula-decl nil convergence_sequences "analysis/") (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) (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)) nil)) (comparison_test_gen 0 (comparison_test_gen-1 nil 3249311615 ("" (skosimp*) (("" (lemma "tail_series_conv2") (("" (inst -1 "N!1" "a!1") (("" (assert) (("" (hide 2) (("" (lemma "tail_series_conv") (("" (inst -1 "N!1" "b!1") (("" (split -1) (("1" (hide -2) (("1" (lemma "comparison_test") (("1" (inst -1 "(LAMBDA n: a!1(n + N!1))" "(LAMBDA n: b!1(n + N!1))") (("1" (assert) (("1" (hide -1 2) (("1" (skosimp*) (("1" (inst -1 "n!1+N!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tail_series_conv2 formula-decl nil series nil) (tail_series_conv formula-decl nil series nil) (comparison_test formula-decl nil series 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers 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)) nil)) (inf_sum_eq 0 (inf_sum_eq-1 nil 3299582002 ("" (skosimp*) (("" (expand "inf_sum") (("" (case-replace "series(b!1, m!1) = series(a!1, m!1)") (("" (assert) (("" (hide 2) (("" (expand "series") (("" (apply-extensionality 1 :hide? t) (("" (rewrite "sigma_eq") (("" (skosimp*) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((inf_sum const-decl "real" series nil) (sigma_eq formula-decl nil sigma "reals/") (subrange type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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/") (series const-decl "sequence[real]" series nil) (= const-decl "[T, T -> boolean]" equalities 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)) nil)) (inf_sum_le_TCC1 0 (inf_sum_le_TCC1-1 nil 3299340008 ("" (skosimp*) (("" (lemma "comparison_test_gen") (("" (expand "conv_series?") (("" (inst - "a!1" "b!1") (("" (assert) (("" (lemma "end_series_conv") (("" (inst?) (("" (assert) (("" (split -2) (("1" (lemma "end_series_conv") (("1" (inst - "a!1" "m!1") (("1" (assert) nil nil)) nil)) nil) ("2" (inst + "m!1") (("2" (skosimp*) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((comparison_test_gen formula-decl nil series 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) (end_series_conv formula-decl nil series nil) (m!1 skolem-const-decl "nat" series nil) (n!1 skolem-const-decl "nat" series nil) (upfrom nonempty-type-eq-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (conv_series? const-decl "bool" series nil)) shostak)) (inf_sum_le_TCC2 0 (inf_sum_le_TCC2-1 nil 3299340008 ("" (skosimp*) (("" (expand "conv_series?") (("" (propax) nil nil)) nil)) nil) ((conv_series? const-decl "bool" series nil)) shostak)) (inf_sum_le 0 (inf_sum_le-1 nil 3299332283 ("" (skosimp*) (("" (expand "inf_sum") (("" (lemma "comparison_test_gen") (("" (inst - "a!1" "b!1") (("" (lemma "end_series_conv") (("" (inst?) (("" (assert) (("" (split -2) (("1" (lemma "end_series_conv") (("1" (inst - "a!1" "m!1") (("1" (assert) (("1" (name "LA" "limit(series(a!1, m!1))") (("1" (replace -1) (("1" (name "LB" "limit(series(b!1, m!1))") (("1" (replace -1) (("1" (lemma "cnv_seq_order") (("1" (inst - "LA" "LB" "series(a!1,m!1)" "series(b!1,m!1)") (("1" (assert) (("1" (prop) (("1" (lemma "limit_equiv") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "limit_equiv") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (hide 2) (("3" (expand "series") (("3" (lemma "sigma_le") (("3" (inst?) (("3" (assert) (("3" (skosimp*) (("3" (inst?) (("3" (expand "abs") (("3" (lift-if) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "m!1") (("2" (skosimp*) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((inf_sum const-decl "real" series 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) (series const-decl "sequence[real]" series nil) (limit const-decl "real" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (= const-decl "[T, T -> boolean]" equalities nil) (cnv_seq_order formula-decl nil convergence_ops "analysis/") (series const-decl "sequence[real]" series 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) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (upfrom nonempty-type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_le formula-decl nil sigma "reals/") (limit_equiv formula-decl nil convergence_ops "analysis/") (n!1 skolem-const-decl "nat" series nil) (m!1 skolem-const-decl "nat" series nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (end_series_conv formula-decl nil series nil) (comparison_test_gen formula-decl nil series nil)) shostak)) (inf_sum_le_abs 0 (inf_sum_le_abs-2 nil 3299840577 ("" (skosimp*) (("" (expand "inf_sum") (("" (lemma "comparison_test_gen") (("" (inst - "a!1" "b!1") (("" (lemma "end_series_conv") (("" (inst?) (("" (assert) (("" (split -2) (("1" (lemma "end_series_conv") (("1" (inst - "a!1" "m!1") (("1" (assert) (("1" (hide -2 -3) (("1" (name "LA" "limit(series(a!1, m!1))") (("1" (replace -1) (("1" (name "LB" "limit(series(b!1, m!1))") (("1" (replace -1) (("1" (case "LA <= LB AND -LB <= LA") (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (hide 2) (("2" (split +) (("1" (lemma "cnv_seq_order") (("1" (inst - "LA" "LB" "series(a!1,m!1)" "series(b!1,m!1)") (("1" (assert) (("1" (prop) (("1" (lemma "limit_equiv") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "limit_equiv") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (hide 2) (("3" (expand "series") (("3" (lemma "sigma_le") (("3" (inst?) (("3" (assert) (("3" (skosimp*) (("3" (inst?) (("3" (expand "abs") (("3" (lift-if) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "cnv_seq_order") (("2" (inst - "-LB" "LA" "-series(b!1,m!1)" "series(a!1,m!1)") (("2" (assert) (("2" (prop) (("1" (lemma "conv_series_scal") (("1" (inst?) (("1" (inst -1 "-1") (("1" (assert) (("1" (lemma "inf_sum_scal") (("1" (inst -1 "b!1" "-1" "m!1") (("1" (assert) (("1" (expand "inf_sum") (("1" (lemma "series_m_scal") (("1" (inst?) (("1" (assert) (("1" (replace -1 * rl) (("1" (replace -4) (("1" (lemma "limit_equiv") (("1" (inst?) (("1" (assert) (("1" (case-replace "-series(b!1, m!1) = -1*series(b!1, m!1)") (("1" (assert) (("1" (hide -1 -2 -3) (("1" (lemma "end_series_conv") (("1" (inst -1 "-b!1" "m!1") (("1" (case-replace "-1 * series(b!1) = series(-b!1)") (("1" (assert) (("1" (case-replace "series(-b!1, m!1) = (-1 * series(b!1, m!1))") (("1" (expand "*") (("1" (apply-extensionality 1 :hide? t) (("1" (expand "-") (("1" (assert) (("1" (hide 2 3 4) (("1" (expand "series") (("1" (lemma "sigma_scal") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "series") (("2" (assert) (("2" (expand "*") (("2" (apply-extensionality 1 :hide? t) (("2" (lemma "sigma_scal") (("2" (inst?) (("2" (assert) (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("2" (expand "-") (("2" (assert) (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "limit_equiv") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("3" (lemma "limit_equiv") (("3" (inst?) (("3" (assert) (("3" (skosimp*) (("3" (hide 2) (("3" (expand "series") (("3" (expand "-") (("3" (case-replace "-sigma(m!1, n!1, b!1) = sigma(m!1, n!1, -b!1)") (("1" (hide -1) (("1" (lemma "sigma_le") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst?) (("1" (expand "-") (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_scal") (("2" (inst?) (("2" (inst - "-1") (("2" (assert) (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "m!1") (("2" (skosimp*) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((inf_sum const-decl "real" series 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) (conv_series_scal formula-decl nil series nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (inf_sum_scal formula-decl nil series nil) (series_m_scal formula-decl nil series nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (sigma def-decl "real" sigma "reals/") (sigma_scal formula-decl nil sigma "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (series const-decl "sequence[real]" series nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (cnv_seq_order formula-decl nil convergence_ops "analysis/") (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (upfrom nonempty-type-eq-decl nil integers nil) (subrange type-eq-decl nil integers nil) (sigma_le formula-decl nil sigma "reals/") (limit_equiv formula-decl nil convergence_ops "analysis/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (minus_real_is_real application-judgement "real" reals nil) (series const-decl "sequence[real]" series nil) (limit const-decl "real" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (= const-decl "[T, T -> boolean]" equalities nil) (n!1 skolem-const-decl "nat" series nil) (m!1 skolem-const-decl "nat" series 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) (end_series_conv formula-decl nil series nil) (comparison_test_gen formula-decl nil series nil)) nil) (inf_sum_le_abs-1 nil 3299500011 ("" (skosimp*) (("" (expand "inf_sum") (("" (lemma "comparison_test_gen") (("" (inst - "a!1" "b!1") (("" (lemma "end_series_conv") (("" (inst?) (("" (assert) (("" (split -2) (("1" (lemma "end_series_conv") (("1" (inst - "a!1" "m!1") (("1" (assert) (("1" (hide -2 -3) (("1" (name "LA" "limit(series(a!1, m!1))") (("1" (replace -1) (("1" (name "LB" "limit(series(b!1, m!1))") (("1" (replace -1) (("1" (case "LA <= LB AND -LB <= LA") (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (hide 2) (("2" (split +) (("1" (lemma "cnv_seq_order") (("1" (inst - "LA" "LB" "series(a!1,m!1)" "series(b!1,m!1)") (("1" (assert) (("1" (prop) (("1" (lemma "limit_equiv") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "limit_equiv") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (hide 2) (("3" (expand "series") (("3" (lemma "sigma_le") (("3" (inst?) (("3" (assert) (("3" (skosimp*) (("3" (inst?) (("3" (expand "abs") (("3" (lift-if) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "cnv_seq_order") (("2" (inst - "-LB" "LA" "-series(b!1,m!1)" "series(a!1,m!1)") (("2" (assert) (("2" (prop) (("1" (lemma "convergent_scal") (("1" (inst?) (("1" (inst -1 "-1") (("1" (assert) (("1" (lemma "inf_sum_scal") (("1" (inst -1 "b!1" "-1" "m!1") (("1" (assert) (("1" (expand "inf_sum") (("1" (lemma "series_m_scal") (("1" (inst?) (("1" (assert) (("1" (replace -1 * rl) (("1" (replace -4) (("1" (lemma "limit_equiv") (("1" (inst?) (("1" (assert) (("1" (case-replace "-series(b!1, m!1) = -1*series(b!1, m!1)") (("1" (assert) (("1" (hide -1 -2 -3) (("1" (lemma "end_series_conv") (("1" (inst -1 "-b!1" "m!1") (("1" (case-replace "-1 * series(b!1) = series(-b!1)") (("1" (assert) (("1" (case-replace "series(-b!1, m!1) = (-1 * series(b!1, m!1))") (("1" (expand "*") (("1" (apply-extensionality 1 :hide? t) (("1" (expand "-") (("1" (assert) (("1" (hide 2 3 4) (("1" (expand "series") (("1" (lemma "sigma_scal") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "series") (("2" (assert) (("2" (expand "*") (("2" (apply-extensionality 1 :hide? t) (("2" (lemma "sigma_scal") (("2" (inst?) (("2" (assert) (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("2" (expand "-") (("2" (assert) (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "limit_equiv") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("3" (lemma "limit_equiv") (("3" (inst?) (("3" (assert) (("3" (skosimp*) (("3" (hide 2) (("3" (expand "series") (("3" (expand "-") (("3" (case-replace "-sigma(m!1, n!1, b!1) = sigma(m!1, n!1, -b!1)") (("1" (hide -1) (("1" (lemma "sigma_le") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst?) (("1" (expand "-") (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_scal") (("2" (inst?) (("2" (inst - "-1") (("2" (assert) (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "m!1") (("2" (skosimp*) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma def-decl "real" sigma "reals/") (sigma_scal formula-decl nil sigma "reals/") (cnv_seq_order formula-decl nil convergence_ops "analysis/") (sigma_le formula-decl nil sigma "reals/") (limit_equiv formula-decl nil convergence_ops "analysis/") (limit const-decl "real" convergence_sequences "analysis/")) nil)) (inf_sum_triangle_TCC1 0 (inf_sum_triangle_TCC1-1 nil 3299583110 ("" (skosimp*) (("" (expand "conv_series?") (("" (lemma "convergent_abs") (("" (inst - "a!1") (("" (assert) (("" (lemma "end_series_conv") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((conv_series? const-decl "bool" series 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) (end_series_conv formula-decl nil series nil) (convergent_abs formula-decl nil series nil)) shostak)) (inf_sum_triangle_TCC2 0 (inf_sum_triangle_TCC2-1 nil 3299583110 ("" (skosimp*) (("" (expand "conv_series?") (("" (lemma "end_series_conv") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((conv_series? const-decl "bool" series 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) (abs const-decl "sequence[real]" series nil) (end_series_conv formula-decl nil series nil)) shostak)) (inf_sum_triangle 0 (inf_sum_triangle-2 nil 3299581718 ("" (skosimp*) (("" (lemma "inf_sum_le_abs") (("" (inst?) (("" (assert) (("" (hide 2) (("" (prop) (("1" (skosimp*) (("1" (grind) nil nil)) nil) ("2" (lemma "end_series_conv") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((inf_sum_le_abs formula-decl nil series 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) (int_minus_int_is_int application-judgement "int" integers nil) (real_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) (sigma def-decl "real" sigma "reals/") (series const-decl "sequence[real]" series nil) (convergence const-decl "bool" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (NOT const-decl "[bool -> bool]" booleans nil) (end_series_conv formula-decl nil series nil) (abs 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) (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)) nil) (inf_sum_triangle-1 nil 3299581703 ("" (postpone) nil nil) nil shostak)) (series_sum_conv 0 (series_sum_conv-1 nil 3249311615 ("" (skosimp*) (("" (expand "convergent?") (("" (skosimp*) (("" (inst 1 "l!1+l!2") (("" (expand "convergence") (("" (skosimp*) (("" (inst - "epsilon!1/2") (("" (inst - "epsilon!1/2") (("" (skosimp*) (("" (inst + "max(n!1,n!2)") (("" (skosimp*) (("" (inst - "i!1") (("" (inst - "i!1") (("" (split -1) (("1" (split -2) (("1" (hide -3) (("1" (expand "series") (("1" (lemma "sigma_sum") (("1" (inst?) (("1" (inst - "a!1") (("1" (expand "+ ") (("1" (replace -1 * rl) (("1" (hide -1) (("1" (grind :exclude "sigma") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (grind) nil nil)) nil)) nil) ("2" (hide -1 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((convergent? const-decl "bool" convergence_sequences "analysis/") (real_plus_real_is_real application-judgement "real" reals 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_sum formula-decl nil sigma "reals/") (minus_real_is_real application-judgement "real" reals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs 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) (+ const-decl "[T -> real]" real_fun_ops "reals/") (sequence type-eq-decl nil sequences nil) (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/") (series const-decl "sequence[real]" series nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal 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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (convergence const-decl "bool" convergence_sequences "analysis/") (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (series_sum_convergence 0 (series_sum_convergence-1 nil 3249311615 ("" (skosimp*) (("" (lemma "cnv_seq_sum") (("" (inst -1 "l1!1" "l2!1" "series(a!1)" "series(b!1)") (("" (assert) (("" (hide -2 -3) (("" (expand "series") (("" (case "(LAMBDA (n: nat): sigma(0, n, a!1)) + (LAMBDA (n: nat): sigma(0, n, b!1)) = (LAMBDA (n: nat): sigma(0, n, a!1 + b!1))") (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide -1 2) (("2" (expand "+ ") (("2" (apply-extensionality 1 :hide? t) (("2" (lemma "sigma_sum") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cnv_seq_sum formula-decl nil convergence_ops "analysis/") (real_plus_real_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_sum formula-decl nil sigma "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (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/") (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) (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)) nil)) (inf_sum_of_sum_TCC1 0 (inf_sum_of_sum_TCC1-1 nil 3249311615 ("" (skosimp*) (("" (expand "conv_series?") (("" (lemma "series_sum_convergence") (("" (inst?) (("" (expand "convergent?") (("" (skosimp*) (("" (inst 1 "l!1+l!2") (("" (inst -1 "l!2" "l!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((conv_series? const-decl "bool" series 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (series_sum_convergence formula-decl nil series nil)) nil)) (inf_sum_of_sum_TCC2 0 (inf_sum_of_sum_TCC2-1 nil 3298728979 ("" (subtype-tcc) nil nil) ((series const-decl "sequence[real]" series nil) (convergence const-decl "bool" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (conv_series? const-decl "bool" series nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (inf_sum_of_sum_TCC3 0 (inf_sum_of_sum_TCC3-1 nil 3298728979 ("" (subtype-tcc) nil nil) ((series const-decl "sequence[real]" series nil) (convergence const-decl "bool" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (conv_series? const-decl "bool" series nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (inf_sum_of_sum 0 (inf_sum_of_sum-1 nil 3249311615 ("" (skosimp*) (("" (expand "inf_sum") (("" (rewrite "limit_def") (("1" (lemma "series_sum_convergence") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (expand "convergent?") (("1" (skosimp*) (("1" (split) (("1" (hide -2) (("1" (lemma "limit_def") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (lemma "limit_def") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "convergent?") (("2" (skosimp*) (("2" (inst 1 "l!1+l!2") (("2" (rewrite "series_sum_convergence") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((inf_sum const-decl "real" series nil) (series_sum_convergence formula-decl nil series nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (series const-decl "sequence[real]" series nil) (limit const-decl "real" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (limit_def formula-decl nil convergence_sequences "analysis/") (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (abs_x_to_n_conv_TCC1 0 (abs_x_to_n_conv_TCC1-1 nil 3249311615 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (abs_x_to_n_conv 0 (abs_x_to_n_conv-1 nil 3249311615 ("" (skosimp*) (("" (lemma "decreasing_bounded_convergence") (("" (expand "convergent?") (("" (case "bounded_below?[nat]((LAMBDA (n: nat): abs(x!1) ^ n))") (("1" (inst - "(LAMBDA (n: nat): abs(x!1) ^ n)") (("1" (inst + "inf((LAMBDA (n: nat): abs(x!1) ^ n))") (("1" (assert) (("1" (hide -1 2) (("1" (expand "decreasing?") (("1" (skosimp*) (("1" (case-replace "x!1 = 0") (("1" (expand "abs" 1) (("1" (assert) (("1" (expand "^") (("1" (expand "expt") (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "both_sides_expt_lt1_le") (("2" (inst?) (("1" (assert) nil nil) ("2" (hide -2 3) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (expand "bounded_below?") (("2" (inst + "0") (("2" (skosimp*) (("2" (lemma "expt_pos") (("2" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((decreasing_bounded_convergence formula-decl nil convergence_sequences "analysis/") (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 "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bounded_below? const-decl "bool" real_fun_preds "reals/") (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) (inf const-decl "real" real_fun_supinf "analysis/") (both_sides_expt_lt1_le formula-decl nil exponentiation nil) (posreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (nat_expt application-judgement "nat" exponentiation nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (expt def-decl "real" exponentiation nil) (abs_0 formula-decl nil abs_lems "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nat_exp application-judgement "nat" exponentiation nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (= const-decl "[T, T -> boolean]" equalities nil) (decreasing? const-decl "bool" real_fun_preds "reals/") (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) (sequence type-eq-decl nil sequences nil) (x!1 skolem-const-decl "real" series nil) (nnreal_exp application-judgement "nnreal" exponentiation nil) (abs_nat formula-decl nil abs_lems "reals/") (expt_pos formula-decl nil exponentiation nil) (convergent? const-decl "bool" convergence_sequences "analysis/")) nil)) (cnv_seq_abs_x_to_n_TCC1 0 (cnv_seq_abs_x_to_n_TCC1-1 nil 3249311615 ("" (skosimp*) (("" (rewrite "abs_x_to_n_conv") nil nil)) nil) ((abs_x_to_n_conv formula-decl nil series 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)) nil)) (cnv_seq_abs_x_to_n 0 (cnv_seq_abs_x_to_n-1 nil 3249311615 ("" (skosimp*) (("" (name "LL" "limit(LAMBDA (n: nat): abs(x!1) ^ n)") (("1" (case "convergent?(abs(x!1) * (LAMBDA (n: nat): abs(x!1) ^ n))") (("1" (case "abs(x!1)*LL = limit(abs(x!1) * (LAMBDA (n: nat): abs(x!1) ^ n))") (("1" (case "abs(x!1) * (LAMBDA (n: nat): abs(x!1) ^ n) = (LAMBDA (n: nat): abs(x!1) ^ (n+1))") (("1" (case-replace "limit(abs(x!1) * (LAMBDA (n: nat): abs(x!1) ^ n)) = limit(LAMBDA (n: nat): abs(x!1) ^ (n+1))" (("1" (hide -2) (("1" (case-replace "limit(LAMBDA (n: nat): abs(x!1) ^ (n+1)) = limit(LAMBDA (n: nat): abs(x!1) ^ n)") (("1" (hide -1 -2 -4) (("1" (replace -2) (("1" (hide -2) (("1" (lemma "both_sides_times1") (("1" (inst?) (("1" (inst -1 "1") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 2) (("2" (rewrite "limit_def") (("1" (replace -2) (("1" (expand "convergence") (("1" (skosimp*) (("1" (rewrite "limit_def" -) (("1" (expand "convergence") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst 1 "n!1+1") (("1" (skosimp*) (("1" (inst -3 "i!1+1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "*") (("2" (hide 2) (("2" (case "(LAMBDA (x: nat): abs(x!1) * abs(x!1) ^ x) = (LAMBDA (n: nat): abs(x!1) ^ (1 + n))") (("1" (assert) nil nil) ("2" (hide -1 -2 -3 2 3) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "^") (("2" (expand "expt" 1 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 -2 -4 2) (("3" (case "(LAMBDA (n: nat): abs(x!1) ^ (1 + n)) = abs(x!1) * (LAMBDA (n: nat): abs(x!1) ^ n)") (("1" (replace -1 * rl) (("1" (propax) nil nil)) nil) ("2" (hide -1 -2 2) (("2" (expand "*") (("2" (apply-extensionality 1 :hide? t) (("2" (expand "^") (("2" (expand "expt" 1 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (hide -1 -2 -3 2) (("3" (lemma "convergent_scal") (("3" (lemma "abs_x_to_n_conv") (("3" (inst?) (("3" (inst?) (("3" (inst - "abs(x!1)") (("3" (assert) (("3" (hide -1 -3) (("3" (expand "*") (("3" (expand "^") (("3" (expand "expt" 1) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 2) (("2" (expand "*") (("2" (apply-extensionality 1 :hide? t) (("2" (expand "^") (("2" (expand "expt" 1 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (lemma "limit_scal") (("2" (replace -2 * rl) (("2" (hide -2) (("2" (inst?) (("1" (assert) nil nil) ("2" (hide 2) (("2" (rewrite "abs_x_to_n_conv") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil) ("2" (hide -1 2) (("2" (lemma "convergent_scal") (("2" (lemma "abs_x_to_n_conv") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "abs_x_to_n_conv") nil nil)) nil)) nil)) nil) ((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 "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (limit const-decl "real" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nnreal_exp application-judgement "nnreal" exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (both_sides_times1 formula-decl nil real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (LL skolem-const-decl "real" series nil) (limit_def formula-decl nil convergence_sequences "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (convergence const-decl "bool" convergence_sequences "analysis/") (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (expt def-decl "real" exponentiation nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (convergent_scal formula-decl nil convergence_ops "analysis/") (nnreal_expt application-judgement "nnreal" exponentiation nil) (abs_x_to_n_conv formula-decl nil series nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (limit_scal formula-decl nil convergence_ops "analysis/") (x!1 skolem-const-decl "real" series nil) (* const-decl "[T -> real]" real_fun_ops "reals/")) nil)) (x_to_n_conv_TCC1 0 (x_to_n_conv_TCC1-1 nil 3249311615 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (x_to_n_conv 0 (x_to_n_conv-1 nil 3249311615 ("" (skosimp*) (("" (lemma "abs_x_to_n_conv") (("" (inst?) (("" (assert) (("" (expand "convergent?") (("" (skosimp*) (("" (inst + "l!1") (("" (case-replace "l!1 = 0") (("1" (expand "convergence") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "n!1") (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (hide -1 -3) (("1" (case-replace "abs(x!1 ^ i!1) = abs(x!1)^i!1") (("1" (hide -1) (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (rewrite "abs_hat_nat") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "cnv_seq_abs_x_to_n") (("2" (inst?) (("2" (assert) (("2" (rewrite "limit_def") (("2" (lemma "unique_limit") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((abs_x_to_n_conv formula-decl nil series nil) (nnreal_exp application-judgement "nnreal" exponentiation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans 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) (minus_real_is_real application-judgement "real" reals nil) (abs_hat_nat formula-decl nil exponentiation 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals 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/") (cnv_seq_abs_x_to_n formula-decl nil series nil) (unique_limit formula-decl nil convergence_sequences "analysis/") (sequence type-eq-decl nil sequences nil) (limit_def formula-decl nil convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "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)) nil)) (convergence_x_to_n 0 (convergence_x_to_n-1 nil 3249311615 ("" (skosimp*) (("" (lemma "abs_x_to_n_conv") (("" (inst?) (("" (assert) (("" (case "convergence(LAMBDA (n: nat): x!1 ^ n, 0)") (("1" (hide -2) (("1" (lemma "cnv_seq_scal") (("1" (inst?) (("1" (inst - "c!1") (("1" (assert) (("1" (hide -2) (("1" (case-replace "(c!1 * (LAMBDA (n: nat): x!1 ^ n), 0) = (LAMBDA (n: nat): c!1 * x!1 ^ n, 0)") (("1" (hide -1 2) (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "convergent?") (("2" (skosimp*) (("2" (case-replace "l!1 = 0") (("1" (expand "convergence") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "n!1") (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (hide -1 -2 -4) (("1" (case-replace "abs(x!1 ^ i!1) = abs(x!1)^i!1") (("1" (hide -1) (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (rewrite "abs_hat_nat") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "cnv_seq_abs_x_to_n") (("2" (inst?) (("2" (assert) (("2" (rewrite "limit_def") (("2" (lemma "unique_limit") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((abs_x_to_n_conv formula-decl nil series nil) (nnreal_exp application-judgement "nnreal" exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (limit_def formula-decl nil convergence_sequences "analysis/") (unique_limit formula-decl nil convergence_sequences "analysis/") (cnv_seq_abs_x_to_n formula-decl nil series 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) (abs_hat_nat formula-decl nil exponentiation nil) (minus_real_is_real application-judgement "real" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (cnv_seq_scal formula-decl nil convergence_ops "analysis/") (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) (convergence const-decl "bool" convergence_sequences "analysis/") (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation 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)) nil)) (geometric_TCC1 0 (geometric_TCC1-1 nil 3249311615 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (sigma_geometric_aux_TCC1 0 (sigma_geometric_aux_TCC1-1 nil 3519664155 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (sigma_geometric_aux 0 (sigma_geometric_aux-1 nil 3519664155 ("" (skeep) (("" (assert) (("" (rewrite "sigma_scal_right" :dir rl) (("" (lemma "sigma_split") (("" (inst - "LAMBDA (i: nat): geometric(x)(i) * x" "n" "0" "n-1") (("" (assert) (("" (replace -1) (("" (hide -1) (("" (expand "sigma" + 3) (("" (expand "sigma" + 3) (("" (expand "geometric" + 3) (("" (case "x ^ n * x = x^(1+n)") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (lemma "sigma_split") (("1" (inst - "geometric(x)" "n" "0" "0") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (expand "sigma" + 1) (("1" (expand "sigma" + 1) (("1" (expand "geometric" + 1) (("1" (expand "^" + 1) (("1" (expand "expt" + 1) (("1" (lemma "sigma_shift") (("1" (inst - "geometric(x)" "n-1" "0" "1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (case "(LAMBDA (n_1: nat): geometric(x)(1 + n_1)) = (LAMBDA (i: nat): geometric(x)(i) * x)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (decompose-equality) (("2" (expand "geometric") (("2" (expand "^") (("2" (expand "expt" + 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "^") (("2" (expand "expt" + 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_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) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (sigma_split formula-decl nil sigma "reals/") (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma_shift formula-decl nil sigma_nat "reals/") (int_plus_int_is_int application-judgement "int" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (expt def-decl "real" exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma def-decl "real" sigma "reals/") (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) (int_minus_int_is_int application-judgement "int" integers 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) (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) (geometric const-decl "sequence[real]" series nil) (sequence type-eq-decl nil sequences nil) (sigma_scal_right formula-decl nil sigma "reals/")) nil)) (sigma_geometric_TCC1 0 (sigma_geometric_TCC1-1 nil 3249311615 ("" (subtype-tcc) nil 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) (real_minus_real_is_real application-judgement "real" reals nil) (/= const-decl "boolean" notequal nil)) nil)) (sigma_geometric 0 (sigma_geometric-1 nil 3249311615 ("" (skeep) (("" (lemma "sigma_geometric_aux") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((sigma_geometric_aux formula-decl nil series nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nnint_plus_posint_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) (real_times_real_is_real application-judgement "real" reals 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) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (geometric_series_TCC1 0 (geometric_series_TCC1-1 nil 3519664192 ("" (subtype-tcc) nil 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) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil)) nil)) (geometric_series 0 (geometric_series-1 nil 3249311615 ("" (skosimp*) (("" (expand "series") (("" (case-replace "(LAMBDA (n: nat): sigma(0, n, geometric(x!1))) = (LAMBDA (n: nat): (1-x!1^(n+1))/(1-x!1)) (("1" (hide -1) (("1" (case-replace "(LAMBDA (n: nat): (1 - x!1 ^(n+1)) / (1 - x!1)) = (LAMBDA (n: nat): 1 / (1 - x!1)) - (LAMBDA (n: nat): (("1" (hide -1) (("1" (lemma "cnv_seq_diff") (("1" (inst -1 "1/(1-x!1)" "0" "(LAMBDA (n: nat): 1/(1-x!1))" "(LAMBDA (n: nat): x!1^(n+1)/(1-x!1))") (("1" (assert) (("1" (hide 2) (("1" (lemma "cnv_seq_const") (("1" (inst -1 "1/(1-x!1)") (("1" (expand "const_fun") (("1" (replace -1) (("1" (assert) (("1" (hide -1) (("1" (lemma "cnv_seq_div") (("1" (inst -1 "0" "(1-x!1)" "(LAMBDA (n: nat): x!1^(n+1))" "(LAMBDA (n: nat): (1-x!1))") (("1" (expand "/" -1) (("1" (hide 2) (("1" (lemma "cnv_seq_const") (("1" (inst -1 "(1-x!1)") (("1" (expand "const_fun") (("1" (assert) (("1" (hide -1) (("1" (lemma "convergence_x_to_n") (("1" (inst?) (("1" (inst -1 "x!1") (("1" (assert) (("1" (expand "^") (("1" (expand "expt" 1) (("1" (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)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "-") (("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (lemma "sigma_geometric") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ((series const-decl "sequence[real]" series nil) (sigma_geometric formula-decl nil series nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (abs_nat formula-decl nil abs_lems "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (x!1 skolem-const-decl "real" series nil) (nzreal nonempty-type-eq-decl nil reals nil) (convergence_x_to_n formula-decl nil series nil) (expt def-decl "real" exponentiation nil) (/ const-decl "[T -> real]" real_fun_ops "reals/") (cnv_seq_div formula-decl nil convergence_ops "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (cnv_seq_const formula-decl nil convergence_ops "analysis/") (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) (cnv_seq_diff formula-decl nil convergence_ops "analysis/") (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (^ const-decl "real" exponentiation nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (geometric const-decl "sequence[real]" series 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) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields 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) (real_minus_real_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) nil)) (geometric_conv 0 (geometric_conv-1 nil 3321109163 ("" (skosimp*) (("" (lemma "geometric_series") (("" (inst?) (("" (assert) (("" (expand "convergent?") (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ((geometric_series formula-decl nil series nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (convergent? const-decl "bool" convergence_sequences "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)) shostak)) (const_geometric_series 0 (const_geometric_series-1 nil 3249311615 ("" (skosimp*) (("" (lemma "geometric_series") (("" (inst?) (("" (assert) (("" (lemma "cnv_seq_scal") (("" (inst -1 "c!1" "1 / (1 - x!1)" "series(geometric(x!1))") (("" (assert) (("" (hide -2) (("" (expand "*") (("" (expand "series") (("" (case-replace "(LAMBDA (n: nat): sigma(0, n, LAMBDA (x: nat): c!1 * geometric(x!1)(x))) =(LAMBDA (x: nat): c (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (apply-extensionality :hide? t) (("2" (rewrite "sigma_scal") (("2" (assert) (("2" (case-replace "(LAMBDA (x: nat): geometric(x!1)(x)) = geometric(x!1)") (("2" (hide 2) (("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) ((geometric_series formula-decl nil series nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (series const-decl "sequence[real]" series nil) (geometric const-decl "sequence[real]" series nil) (sigma_scal formula-decl nil sigma "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities 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/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (cnv_seq_scal formula-decl nil convergence_ops "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)) nil)) (geometric_sum_TCC1 0 (geometric_sum_TCC1-1 nil 3249311615 ("" (skosimp*) (("" (expand "conv_series?") (("" (lemma "geometric_series") (("" (inst?) (("" (expand "convergent?") (("" (assert) (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((conv_series? const-decl "bool" series 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) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (geometric_series formula-decl nil series nil)) nil)) (geometric_sum 0 (geometric_sum-1 nil 3249311615 ("" (skosimp*) (("" (expand "inf_sum") (("" (rewrite "limit_def") (("1" (rewrite "geometric_series") nil nil) ("2" (hide 2) (("2" (expand "convergent?") (("2" (lemma "geometric_series") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((inf_sum const-decl "real" series nil) (geometric_series formula-decl nil series nil) (geometric const-decl "sequence[real]" series nil) (series const-decl "sequence[real]" series nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields 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) (limit_def formula-decl nil convergence_sequences "analysis/") (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (scaf_abs_TCC1 0 (scaf_abs_TCC1-1 nil 3249311615 ("" (subtype-tcc) nil nil) nil nil)) (scaf_abs 0 (scaf_abs-1 nil 3249311615 ("" (induct "n1") (("1" (skosimp*) (("1" (assert) (("1" (expand "^") (("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (replace -2) (("2" (assert) (("2" (inst?) (("2" (lemma "both_sides_times_pos_le1") (("2" (inst -1 "rho!1" "abs(a!1(j!1))" "abs(a!1(0)) * rho!1 ^ j!1") (("2" (assert) (("2" (case-replace "rho!1 ^ (1 + j!1) = rho!1 ^ j!1 * rho!1") (("1" (assert) nil nil) ("2" (hide -1 -3) (("2" (name-replace "T3" "abs(a!1(0)) * (rho!1 ^ j!1 * rho!1)") (("2" (name-replace "T2" "rho!1 * abs(a!1(j!1))") (("2" (assert) (("2" (hide -1 -2 -3 2) (("2" (expand "^") (("2" (expand "expt" 1 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (nnreal type-eq-decl nil real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (int_minus_int_is_int application-judgement "int" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (posreal_exp application-judgement "posreal" exponentiation nil) (expt def-decl "real" exponentiation 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) (nzreal_exp application-judgement "nzreal" exponentiation nil) (nat_induction formula-decl nil naturalnumbers nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (sequence type-eq-decl nil sequences nil) (pred type-eq-decl nil defined_types 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) nil)) (ratio_test_TCC1 0 (ratio_test_TCC1-1 nil 3249311615 ("" (subtype-tcc) nil 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) (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 "boolean" notequal nil)) nil)) (ratio_test 0 (ratio_test-1 nil 3249311615 ("" (skosimp*) (("" (lemma "const_geometric_series") (("" (inst -1 "abs(a!1(0))" "rho!1") (("" (expand "abs" -1 1) (("" (assert) (("" (lemma "comparison_test") (("" (inst -1 "a!1" "abs(a!1(0)) * geometric(rho!1)") (("" (assert) (("" (hide 2) (("" (split +) (("1" (expand "convergent?") (("1" (inst?) nil nil)) nil) ("2" (hide -1) (("2" (expand "geometric") (("2" (lemma "scaf_abs") (("2" (skosimp*) (("2" (expand "*") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (skosimp*) (("2" (inst -3 "n!2") (("2" (rewrite "abs_div") (("1" (lemma "both_sides_times_pos_le1") (("1" (inst -1 "abs(a!1(n!2))" "abs(a!1(1 + n!2)) / abs(a!1(n!2))" "rho!1") (("1" (assert) nil nil) ("2" (hide -2 -3 2) (("2" (inst?) (("2" (grind) nil nil)) nil)) nil) ("3" (hide -2 -3 2) (("3" (inst?) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -2 -3 2) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((const_geometric_series formula-decl nil series nil) (real_minus_real_is_real application-judgement "real" reals nil) (comparison_test formula-decl nil series nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (both_sides_times_pos_le1 formula-decl nil real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (n!2 skolem-const-decl "nat" series nil) (a!1 skolem-const-decl "sequence[real]" series nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (abs_div formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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) (nzreal_exp application-judgement "nzreal" exponentiation nil) (scaf_abs formula-decl nil series nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (geometric const-decl "sequence[real]" series nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals 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) (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) (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) (real_div_nzreal_is_real application-judgement "real" reals nil)) nil)) (ratio_test_gen 0 (ratio_test_gen-2 nil 3249314763 ("" (skosimp*) (("" (lemma "tail_conv") (("" (inst?) (("" (name BB "(LAMBDA n: IF n < N!1 then a!1(N!1)/rho!1^(N!1-n) ELSE a!1(n) ENDIF)") (("" (inst - "BB") (("" (assert) (("" (hide 2) (("" (split +) (("1" (lemma "ratio_test") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (split) (("1" (skosimp*) (("1" (replace -2 * rl) (("1" (assert) (("1" (hide -2) (("1" (lift-if) (("1" (split -1) (("1" (flatten) (("1" (hide -4 -5) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (assert) (("2" (skosimp*) (("2" (case "n!1 < N!1") (("1" (replace -2 * rl) (("1" (hide -2) (("1" (assert) (("1" (lift-if) (("1" (split 1) (("1" (flatten) (("1" (hide -3 -5) (("1" (expand "^") (("1" (expand "expt" 1 2) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case-replace "n!1 = N!1-1") (("1" (assert) (("1" (hide -3 -5) (("1" (grind) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst -4 "n!1") (("2" (assert) (("2" (replace -1 * rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (skosimp*) (("2" (replace -2 * rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tail_conv formula-decl nil series nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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 "real" exponentiation nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (< const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal_exp application-judgement "posreal" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (int_minus_int_is_int application-judgement "int" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (expt def-decl "real" exponentiation nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (posreal_expt application-judgement "posreal" exponentiation nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (int_plus_int_is_int application-judgement "int" integers nil) (ratio_test formula-decl nil 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) (real_div_nzreal_is_real application-judgement "real" reals nil)) nil) (ratio_test_gen-1 nil 3249311615 ("" (skosimp*) (("" (lemma "tail_conv") (("" (inst?) (("" (name b "(LAMBDA n: IF n < N!1 then a!1(N!1)/rho!1^(N!1-n) ELSE a!1(n) ENDIF)") (("" (inst - "B") (("" (assert) (("" (hide 2) (("" (split +) (("1" (lemma "ratio_test") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (split) (("1" (skosimp*) (("1" (replace -2 * rl) (("1" (assert) (("1" (hide -2) (("1" (lift-if) (("1" (split -1) (("1" (flatten) (("1" (hide -4 -5) (("1" (inst?) (("1" (assert) (("1" (lemma "div_eq_zero") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (assert) (("2" (skosimp*) (("2" (case "n!1 < N!1") (("1" (replace -2 * rl) (("1" (hide -2) (("1" (assert) (("1" (lift-if) (("1" (split 1) (("1" (flatten) (("1" (hide -3 -5) (("1" (expand "^") (("1" (expand "expt" 1 2) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case-replace "n!1 = N!1-1") (("1" (assert) (("1" (hide -3 -5) (("1" (grind) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst -4 "n!1") (("2" (assert) (("2" (replace -1 * rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (skosimp*) (("2" (replace -2 * rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (ratio_test_gt_N 0 (ratio_test_gt_N-1 nil 3298110791 ("" (skosimp*) (("" (lemma "tail_series_conv2") (("" (inst?) (("" (inst - "N!1") (("" (assert) (("" (hide 2) (("" (lemma "ratio_test") (("" (inst?) (("" (assert) (("" (prop) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (inst + "rho!1") (("2" (assert) (("2" (skosimp*) (("2" (inst - "n!1 + N!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tail_series_conv2 formula-decl nil series nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (ratio_test formula-decl nil series nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (real_div_nzreal_is_real application-judgement "real" reals nil)) nil)) (ratio_test_lim_TCC1 0 (ratio_test_lim_TCC1-1 nil 3249311615 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (ratio_test_lim 0 (ratio_test_lim-1 nil 3249311615 ("" (skosimp*) (("" (name "LL" "limit(LAMBDA n: abs(a!1(n + 1) / a!1(n)))") (("1" (case "LL >= 0") (("1" (replace -2) (("1" (rewrite "limit_def") (("1" (hide -4) (("1" (lemma "ratio_test_gen") (("1" (inst?) (("1" (assert) (("1" (replace -3) (("1" (assert) (("1" (hide 2) (("1" (expand "convergence") (("1" (case "(EXISTS (nr: real): LL < nr AND nr < 1)") (("1" (skosimp*) (("1" (inst - "abs(nr!1)-LL") (("1" (skosimp*) (("1" (inst + "abs(nr!1)") (("1" (expand "abs" 1 1) (("1" (assert) (("1" (inst 1 "n!1") (("1" (skosimp*) (("1" (inst - "n!2") (("1" (assert) (("1" (hide -3 -6 2) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -4 -5) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide -3 -4 2) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (inst 1 "(1+LL)/2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3 2) (("2" (lemma "limit_pos") (("2" (inst?) (("2" (split -1) (("1" (assert) nil nil) ("2" (hide -1 -3 2) (("2" (skosimp*) (("2" (inst-cp -1 "n!1") (("2" (inst -1 "n!1+1") (("2" (grind) (("2" (lemma "div_eq_zero") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (reveal -2) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (propax) nil nil)) nil)) nil) ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal 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) (limit const-decl "real" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (a!1 skolem-const-decl "sequence[real]" series nil) (limit_pos formula-decl nil series nil) (< const-decl "bool" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nr!1 skolem-const-decl "real" series nil) (LL skolem-const-decl "real" series nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (convergence const-decl "bool" convergence_sequences "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ratio_test_gen formula-decl nil series nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (limit_def formula-decl nil convergence_sequences "analysis/") (real_div_nzreal_is_real application-judgement "real" reals nil)) nil)))
¤ 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.394Bemerkung: (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-30) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26