| products/sources/formale sprachen/PVS/series/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: series.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(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) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.65 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
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.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
