| products/sources/formale Sprachen/PVS/series/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: library.mllib Sprache: LispOriginal von: PVS© |
|
||||||
|
(series_aux
(zero_tail_series_conv 0 (zero_tail_series_conv-1 nil 3314015810 ("" (skosimp*) (("" (lemma "partial_sums" ("a" "a!1")) (("" (replace -1 1) (("" (hide -1) (("" (skosimp) (("" (inst + "n!1+1") (("" (skosimp) (("" (lemma "sigma_eq" ("low" "m!1+1" "high" "n!2" "F" "a!1" "G" "lambda (n:nat): 0")) (("" (rewrite "sigma_zero") (("" (split -1) (("1" (replace -1) (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (typepred "n!3") (("2" (inst - "n!3") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((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) (partial_sums formula-decl nil series nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals 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) (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_eq formula-decl nil sigma "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (subrange type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (sigma_zero formula-decl nil sigma "reals/")) shostak)) (zero_tail_series_limit_TCC1 0 (zero_tail_series_limit_TCC1-1 nil 3314015766 ("" (lemma "zero_tail_series_conv") (("" (propax) nil nil)) nil) ((zero_tail_series_conv formula-decl nil series_aux nil)) shostak)) (zero_tail_series_limit 0 (zero_tail_series_limit-1 nil 3314016598 ("" (skosimp) (("" (lemma "zero_tail_series_conv" ("a" "a!1" "n" "n!1")) (("" (replace -2 -1) (("" (expand "series" 1 2) (("" (lemma "limit_series_shift" ("a" "a!1" "pn" "n!1+1")) (("" (replace -2 -1) (("" (replace -1 1) (("" (assert) (("" (hide -1) (("" (case-replace "(LAMBDA (n:nat): a!1(1 + n + n!1)) = (LAMBDA (n:nat): 0)") (("1" (rewrite "zero_series_limit") nil nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (inst - "1+n!1+x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((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) (zero_tail_series_conv formula-decl nil series_aux nil) (series const-decl "sequence[real]" series nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (zero_series_limit formula-decl nil series nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (limit_series_shift formula-decl nil series nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (zero_tail_series 0 (zero_tail_series-1 nil 3321845471 ("" (skosimp) (("" (lemma "zero_tail_series_conv" ("a" "a!1" "n" "n!1")) (("" (lemma "zero_tail_series_limit" ("a" "a!1" "n" "n!1")) (("" (replace -3 (-1 -2)) (("" (rewrite "limit_equiv") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((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) (zero_tail_series_conv formula-decl nil series_aux nil) (series const-decl "sequence[real]" series nil) (limit_equiv formula-decl nil convergence_ops "analysis/") (zero_tail_series_limit formula-decl nil series_aux nil)) shostak)) (single_nz_series_conv 0 (single_nz_series_conv-1 nil 3314567201 ("" (skosimp) (("" (lemma "zero_tail_series_conv" ("a" "a!1" "n" "n!1")) (("" (split) (("1" (propax) nil nil) ("2" (skosimp) (("2" (inst - "m!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((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) (zero_tail_series_conv formula-decl nil series_aux nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (single_nz_series_limit_TCC1 0 (single_nz_series_limit_TCC1-1 nil 3314567614 ("" (lemma "single_nz_series_conv") (("" (propax) nil nil)) nil) ((single_nz_series_conv formula-decl nil series_aux nil)) shostak)) (single_nz_series_limit 0 (single_nz_series_limit-1 nil 3314567245 ("" (skosimp) (("" (lemma "zero_tail_series_limit" ("a" "a!1" "n" "n!1")) (("" (split -1) (("1" (expand "series" -1 2) (("1" (expand "sigma" -1) (("1" (case-replace "n!1=0") (("1" (assert) nil nil) ("2" (lemma "sigma_restrict_eq" ("low" "0" "high" "n!1-1" "F" "a!1" "G" "lambda (i:nat): 0")) (("2" (rewrite "sigma_zero") (("2" (split) (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (expand "restrict") (("2" (apply-extensionality :hide? t) (("2" (inst - "x!1") (("2" (lift-if) (("2" (prop) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "m!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((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) (zero_tail_series_limit formula-decl nil series_aux nil) (series const-decl "sequence[real]" series nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_plus_real_is_real application-judgement "real" reals nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_0_neg formula-decl nil sigma_nat "reals/") (sigma_zero formula-decl nil sigma "reals/") (restrict const-decl "[T -> real]" sigma "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (> const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def 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) (int_minus_int_is_int application-judgement "int" integers nil) (sigma_restrict_eq 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/") (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (T_low type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/")) shostak)) (single_nz_series 0 (single_nz_series-1 nil 3321845412 ("" (skosimp) (("" (lemma "single_nz_series_conv" ("a" "a!1" "n" "n!1")) (("" (lemma "single_nz_series_limit" ("a" "a!1" "n" "n!1")) (("" (assert) (("" (replace -3 (-1 -2)) (("" (rewrite "limit_equiv") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((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) (single_nz_series_conv formula-decl nil series_aux nil) (limit_equiv formula-decl nil convergence_ops "analysis/") (series const-decl "sequence[real]" series nil) (single_nz_series_limit formula-decl nil series_aux nil)) shostak)) (limit_nonneg 0 (limit_nonneg-1 nil 3322859396 ("" (skosimp) (("" (lemma "cnv_seq_order" ("s1" "LAMBDA n: 0" "s2" "nna!1" "l1" "0" "l2" "limit(nna!1)")) (("" (lemma "limit_equiv" ("s" "nna!1" "l" "limit(nna!1)")) (("" (simplify -1) (("" (replace -3 -1) (("" (simplify -1) (("" (replace -1 -2) (("" (split -2) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (expand "convergence") (("2" (expand "abs") (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnreal 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (cnv_seq_order formula-decl nil convergence_ops "analysis/") (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) (convergence const-decl "bool" convergence_sequences "analysis/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (limit_equiv formula-decl nil convergence_ops "analysis/")) shostak)) (convergence_nonneg 0 (convergence_nonneg-1 nil 3322862860 ("" (skosimp*) (("" (case "FORALL m: n!1 < m => nna!1(m) = 0") (("1" (lemma "zero_tail_series" ("a" "nna!1" "n" "n!1")) (("1" (replace -2 -1) (("1" (lemma "unique_limit" ("u" "series(nna!1)" "l1" "nnx!1" "l2" "series(nna!1)(n!1)")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "convergence") (("2" (inst - "nna!1(m!1)") (("1" (skosimp) (("1" (inst - "max(n!2,m!1)") (("1" (split -2) (("1" (case "increasing?(series(nna!1))") (("1" (expand "abs") (("1" (case-replace "series(nna!1)(max(n!2, m!1)) - nnx!1 < 0") (("1" (expand "increasing?") (("1" (inst - "n!1" "max(n!2,m!1)") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (hide 1) (("2" (expand "series") (("2" (expand "max") (("2" (case-replace "n!2 (("1" (expand "sigma" -3) (("1" (assert) (("1" (expand "increasing?") (("1" (inst - "n!1" "m!1-1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "n!2 >= m!1") (("1" (hide 1) (("1" (expand ">=") (("1" (expand "<=" -1) (("1" (split -1) (("1" (lemma "sigma_middle[nat]" ("high" "n!2" "i" "m!1" "low" "0" "F" "nna!1")) (("1" (assert) (("1" (replace -1 -4) (("1" (hide -1) (("1" (case "forall m: 0 <= sigma(1 + m!1, 1+m!1+m, nna!1)") (("1" (inst - "n!2-m!1-1") (("1" (expand "increasing?") (("1" (inst - "n!1" "m!1-1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (induct "m") (("1" (expand "sigma") (("1" (assert) (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "sigma" -2) (("2" (expand "increasing?") (("2" (inst - "n!1" "m!1-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "increasing?") (("2" (expand "series") (("2" (case "forall n,m: sigma(0, n, nna!1) <= sigma(0, n+m, nna!1)") (("1" (skosimp) (("1" (inst - "x!1" "y!1-x!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (induct "m") (("1" (skosimp) (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst - "n!3") (("2" (expand "sigma" 1 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "max") (("2" (case-replace "n!2 < m!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((sequence type-eq-decl nil sequences nil) (nnreal type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (< const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (series const-decl "sequence[real]" series nil) (unique_limit formula-decl nil convergence_sequences "analysis/") (zero_tail_series formula-decl nil series_aux nil) (real_minus_real_is_real application-judgement "real" reals nil) (convergence const-decl "bool" convergence_sequences "analysis/") (x!1 skolem-const-decl "nat" series_aux nil) (y!1 skolem-const-decl "nat" series_aux nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma def-decl "real" sigma "reals/") (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (int_plus_int_is_int application-judgement "int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (sigma_middle formula-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (increasing? const-decl "bool" real_fun_preds "reals/") (AND const-decl "[bool, bool -> bool]" booleans nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (m!1 skolem-const-decl "nat" series_aux nil) (nna!1 skolem-const-decl "sequence[nnreal]" series_aux nil) (> const-decl "bool" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (nonneg_series_bij 0 (nonneg_series_bij-1 nil 3322860486 ("" (skosimp*) (("" (typepred "phi!1") (("" (name "MM" "LAMBDA (f:(bijective?[nat,nat]),n:nat): image(LAMBDA (i:below[n+1]): f(i))(full (("" (lemma "surjective_inverse_exists[nat,nat]" ("f" "phi!1")) (("" (lemma "bij_inv_is_bij_alt[nat,nat]" ("f" "phi!1")) (("" (skolem - ("phi1")) (("" (inst - "phi1") (("" (case "forall (f: (bijective?[nat, nat]), n: nat): is_finite[nat](MM(f,n))") (("1" (case "FORALL (f: (bijective?[nat, nat]), n: nat): has_greatest?(MM(f,n),reals.<=)") (("1" (expand "restrict") (("1" (expand "has_greatest?") (("1" (expand "greatest?") (("1" (expand "upper_bound?") (("1" (case "increasing?(series(nna!1))") (("1" (case "increasing?(series(nna!1 o phi!1))") (("1" (case "FORALL n: EXISTS m: series(nna!1 o phi!1)(n) <= series(nna!1)(m)") (("1" (case "FORALL (a: sequence[nnreal], l: real): increasing?(a) & convergence(a, l) => (FORALL (j: nat): a(j) <= l)") (("1" (inst - "series(nna!1)" "nnx!1") (("1" (assert) (("1" (case "FORALL (j: nat): series(nna!1 o phi!1)(j) <= nnx!1") (("1" (expand "convergence") (("1" (skosimp) (("1" (inst -12 "epsilon!1") (("1" (skosimp) (("1" (case "FORALL i: i >= n!1 IMPLIES nnx!1-series(nna!1)(i) < epsilon!1") (("1" (case "EXISTS n: FORALL i: i >= n IMPLIES nnx!1 - series(nna!1 o phi!1)(i) < epsilon!1") (("1" (skosimp) (("1" (inst + "n!2") (("1" (skosimp) (("1" (inst - "i!1") (("1" (assert) (("1" (expand "abs" 1) (("1" (assert) (("1" (inst -3 "i!1") (("1" (assert) (("1" (expand "<=" -3) (("1" (split -3) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "FORALL n: EXISTS m: series(nna!1)(n) <= series(nna!1 o phi!1)(m)") (("1" (inst - "n!1") (("1" (skosimp) (("1" (inst - "n!1") (("1" (assert) (("1" (inst + "m!1") (("1" (skosimp) (("1" (expand "increasing?" -7) (("1" (inst -7 "m!1" "i!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -12 -11 -10 -9 -8 -7 -5 -6)) (("2" (skosimp) (("2" (inst -3 "phi!1" "n!2") (("2" (case " EXISTS (t: nat): MM(phi1, n!2)(t) AND (FORALL (r: (MM(phi1, n!2))): (reals.<=(r, t)))") (("1" (hide -4) (("1" (skosimp) (("1" (inst + "t!1") (("1" (case "FORALL (j: nat): j <= n!2 => sigma(0, j, nna!1) = sigma(0, t!1, LAMBDA (i: nat): IF MM(phi1, j)(i) THEN nna!1(phi!1(i)) ELSE 0 ENDIF)") (("1" (expand "series") (("1" (inst - "n!2") (("1" (assert) (("1" (replace -1) (("1" (lemma "sigma_le" ("low" "0" "high" "t!1" "F" "LAMBDA (i: nat): IF MM(phi1, n!2)(i) THEN nna!1(phi!1(i)) ELSE 0 ENDIF" "G" "nna!1 o phi!1")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "o" 1) (("2" (case-replace "MM(phi1, n!2)(n!3)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "j") (("1" (assert) (("1" (expand "sigma" 1 1) (("1" (lemma "sigma_with" ("low" "0" "high" "t!1" "i" "phi1(0)" "a" "nna!1(0)" "F" "LAMBDA (i: nat): IF MM(phi1, 0)(i) THEN nna!1(phi!1(i)) ELSE 0 ENDIF" "G" "LAMBDA (i:nat): 0")) (("1" (split -1) (("1" (replace -1) (("1" (lemma "sigma_zero" ("low" "0" "high" "t!1")) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (inst - "phi1(0)") (("3" (expand "MM") (("3" (expand "image") (("3" (expand "image") (("3" (inst + "0") (("3" (expand "fullset") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (apply-extensionality 1 :hide? t) (("4" (case-replace "x!1=phi1(0)") (("1" (assert) (("1" (case-replace "MM(phi1, 0)(phi1(0))") (("1" (lemma "comp_inverse_right_alt[nat,nat]" ("f" "phi!1" "g" "phi1" "r" "0")) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (expand "MM") (("2" (expand "image") (("2" (expand "image") (("2" (inst + "0") (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.105 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 |
