| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/extended_nnreal/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 235 kB |
|
Quelle double_nn_sequence.prfSprache: Lisp |
|||||||||||||||
|
(double_nn_sequence (nn_series_increasing 0 (nn_series_increasing-1 nil 3408339793 ("" (expand "increasing?") (("" (expand "series") (("" (skosimp*) (("" (lemma "sigma_split" ("low" "0" "high" "y!1" "z" "x!1" "F" "v!1")) (("" (assert) (("" (lemma "sigma_ge_0" ("low" "x!1+1" "high" "y!1" "F" "v!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((series const-decl "sequence[real]" series "series/") (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) (nnreal type-eq-decl nil real_types nil) (sigma_split formula-decl nil sigma "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (sigma_ge_0 formula-decl nil sigma "reals/") (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" 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) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (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) (increasing? const-decl "bool" real_fun_preds "reals/")) shostak)) (nn_index_scaf1_TCC1 0 (nn_index_scaf1_TCC1-1 nil 3408961994 ("" (subtype-tcc) nil nil) nil nil)) (nn_index_scaf1_TCC2 0 (nn_index_scaf1_TCC2-1 nil 3408961994 ("" (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) (>= const-decl "bool" 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (nn_index_scaf1 0 (nn_index_scaf1-1 nil 3408961995 ("" (induct "n") (("1" (skosimp) (("1" (case-replace "double_index_n(0, 0)=0") (("1" (expand "series") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "single_index") (("1" (lemma "double_index_ij_n" ("i" "0" "j" "0")) (("1" (replace -2) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "double_index_n") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "series") (("2" (inst - "u!1") (("2" (expand "sigma" 1 2) (("2" (expand "sigma" 1 2) (("2" (expand "sigma" 1 2) (("2" (expand "sigma" 1 3) (("2" (assert) (("2" (case "double_index_n(0, j!1)<double_index_n(0, 1 + j!1)") (("1" (lemma "sigma_split" ("low" "0" "high" "double_index_n(0, 1 + j!1)" "z" "double_index_n(0, j!1)" "F" "single_index(u!1)")) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_sum" ("low" "0" "high" "j!1" "F" "LAMBDA i:IF 0 > 1 - i + j!1 THEN 0 ELSE u!1(i, 1 - i + j!1)ENDIF" "G" "LAMBDA i: IF 0 > 1 - i + j!1 THEN 0 ELSE sigma(0, j!1 - i, LAMBDA j: u!1(i, j))ENDIF")) (("1" (assert) (("1" (case-replace "(LAMBDA (i_1: nat): IF 0 > 1 - i_1 + j!1 THEN 0 ELSE u!1(i_1, 1 - i_1 + j!1) ENDIF + IF 0 > 1 - i_1 + j!1 THEN 0 ELSE sigma(0, j!1 - i_1, LAMBDA j: u!1(i_1, j)) ENDIF)=LAMBDA i: IF 0 > 1 - i + j!1 THEN 0 ELSE u!1(i, 1 - i + j!1) + sigma(0, j!1 - i, LAMBDA j: u!1(i, j)) ENDIF") (("1" (name-replace "FF" "LAMBDA i: IF 0 > 1 - i + j!1 THEN 0 ELSE u!1(i, 1 - i + j!1) + sigma(0, j!1 - i, LAMBDA j: u!1(i, j)) ENDIF") (("1" (replace -2 1 rl) (("1" (hide -1 -2) (("1" (case-replace "sigma(0, j!1, LAMBDA i: IF 0 > 1 - i + j!1 THEN 0 ELSE sigma(0, j!1 - i, LAMBDA j: u!1(i, j)) ENDIF)=sigma(0, double_index_n(0, j!1), single_index(u!1))") (("1" (assert) (("1" (hide -1 -3) (("1" (case "forall n: sigma(1 + double_index_n(0, n), double_index_n(0, 1 + n), single_index(u!1)) = u!1(1 + n, 0) + sigma(0, n, LAMBDA i: IF 0 > 1 - i + n THEN 0 ELSE u!1(i, 1 - i + n) ENDIF)") (("1" (inst - "j!1") nil nil) ("2" (hide -1 2) (("2" (case " FORALL n: u!1(1 + n, 0) + sigma(0, n, LAMBDA i: IF 0 > 1 - i + n THEN 0 ELSE u!1(i, 1 - i + n) ENDIF) = sigma(0,n+1, LAMBDA i: IF 0 > 1 - i + n THEN 0 ELSE u!1(i,1-i+n)endif)") (("1" (case "FORALL n: sigma(1 + double_index_n(0, n), double_index_n(0, 1 + n), single_index(u!1)) =sigma(0, n + 1, LAMBDA i: IF 0 > 1 - i + n THEN 0 ELSE u!1(i, 1 - i + n) ENDIF)") (("1" (skosimp) (("1" (inst - "n!1") (("1" (inst - "n!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (case "FORALL n: sigma(1 + double_index_n(0, n), double_index_n(0, 1 + n), single_index(u!1)) =sigma(0, n + 1, LAMBDA i: IF 0 > 1 - i + n THEN 0 ELSE u!1(n+1-i,i) endif)") (("1" (case "FORALL n:sigma(0, n + 1, LAMBDA i: IF 0 > 1 - i + n THEN 0 ELSE u!1(n + 1 - i, i) ENDIF) = sigma(0, n + 1, LAMBDA i: IF 0 > 1 - i + n THEN 0 ELSE u!1(i, 1 - i + n) ENDIF)") (("1" (skosimp) (("1" (inst - "n!1") (("1" (inst - "n!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (skosimp) (("2" (case "forall j: j <= n!1+1 => sigma(0, j, LAMBDA i: IF 0 > 1 - i + n!1 THEN 0 ELSE u!1(n!1 + 1 - i, i) ENDIF) = sigma(n!1+1-j, n!1 + 1, LAMBDA i: IF 0 > 1 - i + n!1 THEN 0 ELSE u!1(i, 1 - i + n!1) ENDIF)") (("1" (inst - "n!1+1") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "j") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1 1) (("2" (assert) (("2" (replace -1 1) (("2" (hide -1) (("2" (lemma "sigma_first" ("low" "n!1 - j!2" "high" "1 + n!1" "F" "LAMBDA i: IF 0 > 1 - i + n!1 THEN 0 ELSE u!1(i, 1 - i + n!1) ENDIF")) (("1" (assert) nil nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp) (("4" (assert) nil nil)) nil) ("5" (skosimp) (("5" (skosimp) (("5" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp) (("4" (assert) nil nil)) nil) ("5" (skosimp) (("5" (skosimp) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil) ("4" (skosimp) (("4" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (case "forall j: j <=n!1+1=>sigma(1 + double_index_n(0, n!1), 1+double_index_n(0, n!1)+j, single_index(u!1)) = sigma(0, j, LAMBDA i: IF 0 > 1 - i + n!1 THEN 0 ELSE u!1(n!1 + 1 - i, i) ENDIF)") (("1" (inst - "n!1+1") (("1" (assert) (("1" (case-replace "double_index_n(0, 1 + n!1)=2 + double_index_n(0, n!1) + n!1") (("1" (assert) (("1" (hide -1 2) (("1" (expand "double_index_n") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "j") (("1" (assert) (("1" (expand "sigma") (("1" (assert) (("1" (expand "sigma") (("1" (case-replace "1 + double_index_n(0, n!1)=double_index_n(n!1+1,0)") (("1" (expand "single_index") (("1" (lemma "double_index_ij_n" ("i" "1+n!1" "j" "0")) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "double_index_n") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (assert) (("2" (case-replace "2 + double_index_n(0, n!1) + j!2=double_index_n(n!1-j!2,1+j!2)") (("1" (expand "single_index") (("1" (lemma "double_index_ij_n" ("i" "n!1-j!2" "j" "1+j!2")) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "double_index_n") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp) (("4" (assert) nil nil)) nil) ("5" (skosimp) (("5" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (lemma "sigma_last" ("low" "0" "high" "n!1+1" "F" "LAMBDA i: IF 0 > 1 - i + n!1 THEN 0 ELSE u!1(i, 1 - i + n!1) ENDIF")) (("1" (assert) nil nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil) ("4" (skosimp) (("4" (assert) nil nil)) nil) ("5" (skosimp) (("5" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (replace -2) (("2" (hide -2) (("2" (lemma "sigma_restrict_eq" ("low" "0" "high" "j!1" "F" "LAMBDA i: IF 0 > 1 - i + j!1 THEN 0 ELSE sigma(0, j!1 - i, LAMBDA j: u!1(i, j)) ENDIF" "G" "LAMBDA i: sigma(0, j!1 - i, LAMBDA j: u!1(i, j))")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (expand "restrict") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (apply-extensionality :hide? t) (("1" (case-replace "0 > 1 - x!1 + j!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (skosimp) (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "double_index_n") (("2" (rewrite "sq_rew") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst + "n!2") (("3" (assert) nil nil)) nil)) nil)) nil) ((< const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (even_plus_even_is_even application-judgement "even_int" integers nil) (j!1 skolem-const-decl "nat" double_nn_sequence nil) (restrict const-decl "[T -> real]" sigma "reals/") (sigma_restrict_eq formula-decl nil sigma "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posrat_plus_nnrat_is_posrat application-judgement "posrat" rationals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (n!1 skolem-const-decl "nat" double_nn_sequence nil) (real_minus_real_is_real application-judgement "real" reals nil) (sigma_0_neg formula-decl nil sigma_nat "reals/") (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (even_minus_even_is_even application-judgement "even_int" integers 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) (sigma_first formula-decl nil sigma "reals/") (n!1 skolem-const-decl "nat" double_nn_sequence nil) (sigma_last formula-decl nil sigma "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sigma_sum formula-decl nil sigma "reals/") (int_plus_int_is_int application-judgement "int" integers nil) (sigma_split formula-decl nil sigma "reals/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (sq_rew formula-decl nil sq "reals/") (sigma_nnreal application-judgement "nnreal" 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (double_index_ij_n formula-decl nil code_product nil) (nat_induction formula-decl nil naturalnumbers nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (double_index_n const-decl "nat" code_product nil) (single_index const-decl "[nat -> T]" double_index nil) (series const-decl "sequence[real]" series "series/") (sequence type-eq-decl nil sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) (pred type-eq-decl nil defined_types 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (nn_double_index_incr 0 (nn_double_index_incr-1 nil 3408979981 ("" (skosimp) (("" (expand "double_index_n") (("" (propax) nil nil)) nil)) nil) ((nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (double_index_n const-decl "nat" code_product nil)) shostak)) (nn_index_scaf2 0 (nn_index_scaf2-1 nil 3408975051 ("" (skosimp) (("" (rewrite "nn_index_scaf1") (("" (lemma "sigma_split" ("low" "0" "high" "2*n!1" "z" "n!1" "F" "LAMBDA i: sigma(0, 2 * n!1 - i, LAMBDA j: u!1(i, j))")) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_le" ("low" "0" "high" "n!1" "F" "LAMBDA i: sigma(0, n!1, LAMBDA j: u!1(i, j))" "G" "LAMBDA i: sigma(0, 2 * n!1 - i, LAMBDA j: u!1(i, j))")) (("1" (split -1) (("1" (lemma "sigma_ge_0" ("low" "1+n!1" "high" "2*n!1" "F" "LAMBDA i: sigma(0, 2 * n!1 - i, LAMBDA j: u!1(i, j))")) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "n!2") (("2" (lemma "sigma_split" ("low" "0" "high" "2*n!1-n!2" "z" "n!1" "F" "LAMBDA j: u!1(n!2, j)")) (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nn_index_scaf1 formula-decl nil double_nn_sequence 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal type-eq-decl nil real_types 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_nnreal application-judgement "nnreal" sigma_nat "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma_ge_0 formula-decl nil sigma "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (subrange type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (sigma_le formula-decl nil sigma "reals/") (- 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) (sigma_split formula-decl nil sigma "reals/")) shostak)) (nn_index_scaf3 0 (nn_index_scaf3-1 nil 3408981469 ("" (skolem + ("i!1" "j!1" "u!1")) (("" (lemma "nn_index_scaf2" ("u" "u!1" "n" "i!1+j!1")) (("" (inst + "double_index_n(0, 2 * (i!1 + j!1))") (("" (name-replace "RHS" "series(single_index(u!1))(double_index_n(0, 2 * (i!1 + j!1)))") (("" (lemma "sigma_split" ("low" "0" "high" "i!1+j!1" "z" "i!1" "F" "LAMBDA i: sigma(0, i!1 + j!1, LAMBDA j: u!1(i, j))")) (("" (assert) (("" (replace -1) (("" (hide -1) (("" (lemma "sigma_ge_0" ("low" "1+i!1" "high" "i!1+j!1" "F" "LAMBDA i: sigma(0, i!1 + j!1, LAMBDA j: u!1(i, j))")) (("" (split -1) (("1" (name-replace "DRL1" "sigma(1 + i!1, i!1 + j!1, LAMBDA i: sigma(0, i!1 + j!1, LAMBDA j: u!1(i, j)))") (("1" (lemma "sigma_sum" ("low" "0" "high" "i!1" "F" "LAMBDA i: sigma(0, j!1, LAMBDA j: u!1(i, j))" "G" "LAMBDA i: sigma(j!1+1, i!1+j!1,LAMBDA j: u!1(i, j))")) (("1" (assert) (("1" (case-replace "(LAMBDA (i_1: nat): sigma(0, j!1, LAMBDA j: u!1(i_1, j)) + sigma(1 + j!1, i!1 + j!1, LAMBDA j: u!1(i_1, j)))=LAMBDA i: sigma(0, i!1 + j!1, LAMBDA j: u!1(i, j (("1" (replace -2 -4 rl) (("1" (assert) nil nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("2" (hide-all-but 1) (("2" (lemma "sigma_split" ("low" "0" "high" "i!1+j!1" "z" "j!1" "F" "LAMBDA j: u!1(x!1, j)")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide-all-but 1) (("2" (rewrite "sigma_ge_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnreal type-eq-decl nil real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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) (nn_index_scaf2 formula-decl nil double_nn_sequence nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (single_index const-decl "[nat -> T]" double_index nil) (series const-decl "sequence[real]" series "series/") (sequence type-eq-decl nil sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (sigma_sum formula-decl nil sigma "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (sigma_ge_0 formula-decl nil sigma "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers 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) (sigma_split formula-decl nil sigma "reals/") (double_index_n const-decl "nat" code_product nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil)) shostak)) (nn_index_scaf4 0 (nn_index_scaf4-1 nil 3408985014 ("" (skosimp) (("" (inst + "n!1" "n!1") (("" (lemma "nn_index_scaf1" ("u" "u!1" "n" "n!1")) (("" (case "n!1<=double_index_n(0, n!1)") (("1" (lemma "nn_series_increasing" ("v" "single_index(u!1)")) (("1" (expand "increasing?") (("1" (inst - "n!1" "double_index_n(0, n!1)") (("1" (assert) (("1" (name-replace "LHS" "series(single_index(u!1))(n!1)") (("1" (name-replace "DRL1" "series(single_index(u!1))(double_index_n(0, n!1))") (("1" (lemma "sigma_le" ("low" "0" "high" "n!1" "F" "LAMBDA i: sigma(0, n!1 - i, LAMBDA j: u!1(i, j))" "G" "LAMBDA i: sigma(0, n!1, LAMBDA j: u!1(i, j))")) (("1" (assert) (("1" (skosimp) (("1" (hide-all-but 1) (("1" (typepred "n!2") (("1" (lemma "sigma_split" ("low" "0" "high" "n!1" "z" "n!1-n!2" "F" "LAMBDA j: u!1(n!2, j)")) (("1" (assert) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "double_index_n") (("2" (assert) 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) (double_index_n const-decl "nat" code_product nil) (<= const-decl "bool" reals nil) (increasing? const-decl "bool" real_fun_preds "reals/") (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_nnreal application-judgement "nnreal" sigma_nat "reals/") (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) (sigma_split formula-decl nil sigma "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (int_plus_int_is_int application-judgement "int" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (subrange type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil 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/") (OR const-decl "[bool, bool -> bool]" booleans nil) (sigma_le formula-decl nil sigma "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (sequence type-eq-decl nil sequences nil) (series const-decl "sequence[real]" series "series/") (single_index const-decl "[nat -> T]" double_index nil) (nn_series_increasing formula-decl nil double_nn_sequence nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnrat_plus_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (nn_index_scaf1 formula-decl nil double_nn_sequence nil) (nnreal type-eq-decl nil real_types nil)) shostak)) (nn_convegent_bounded 0 (nn_convegent_bounded-1 nil 3408339871 ("" (skosimp) (("" (split) (("1" (flatten) (("1" (expand "bounded_above?") (("1" (expand "convergent?") (("1" (skosimp) (("1" (inst + "l!1") (("1" (expand "upper_bound?") (("1" (skosimp) (("1" (typepred "s!1") (("1" (expand "Im") (("1" (skolem - ("n!1")) (("1" (expand "convergence") (("1" (case "l!1<series(v!1)(n!1)") (("1" (hide -2 1) (("1" (inst - "series(v!1)(n!1)-l!1") (("1" (skosimp) (("1" (inst - "n!1+n!2") (("1" (assert) (("1" (lemma "nn_series_increasing" ("v" "v!1")) (("1" (expand "increasing?") (("1" (inst - "n!1" "n!1+n!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (typepred "lub(Im(series(v!1)))") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (expand "convergent?") (("1" (inst + "lub(Im(series(v!1)))") (("1" (expand "convergence") (("1" (skosimp) (("1" (name-replace "LUB" "lub(Im(series(v!1)))") (("1" (case "EXISTS n: FORALL i: i >= n IMPLIES LUB-series(v!1)(i) < epsilon!1") (("1" (skosimp) (("1" (inst + "n!1") (("1" (skosimp) (("1" (inst - "i!1") (("1" (assert) (("1" (expand "upper_bound?") (("1" (inst - "series(v!1)(i!1)") (("1" (expand "abs") (("1" (expand "<=" -2) (("1" (split -2) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "Im") (("2" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (inst - "LUB-epsilon!1") (("2" (assert) (("2" (expand "upper_bound?") (("2" (skosimp) (("2" (typepred "s!1") (("2" (case "LUB<s!1+epsilon!1") (("1" (hide 2) (("1" (copy -2) (("1" (expand "Im" -1) (("1" (skolem - "n!1") (("1" (replace -1) (("1" (hide -1) (("1" (inst + "n!1") (("1" (skosimp) (("1" (lemma "nn_series_increasing" ("v" "v!1")) (("1" (expand "increasing?") (("1" (inst - "n!1" "i!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ((bounded_above? const-decl "bool" bounded_real_defs nil) (upper_bound? const-decl "bool" bounded_real_defs nil) (nnreal type-eq-decl nil real_types nil) (series const-decl "sequence[real]" series "series/") (sequence type-eq-decl nil sequences nil) (Im const-decl "setof[real]" real_fun_props "reals/") (setof type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (v!1 skolem-const-decl "[nat -> nnreal]" double_nn_sequence nil) (n!1 skolem-const-decl "nat" double_nn_sequence nil) (l!1 skolem-const-decl "real" double_nn_sequence nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nn_series_increasing formula-decl nil double_nn_sequence nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (increasing? const-decl "bool" real_fun_preds "reals/") (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) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (lub const-decl "{x | least_upper_bound?(x, SA)}" bounded_real_defs nil) (least_upper_bound? const-decl "bool" bounded_real_defs nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (nonempty_image application-judgement "(nonempty?[real])" double_nn_sequence nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (minus_real_is_real application-judgement "real" reals nil) (<= const-decl "bool" reals nil) (i!1 skolem-const-decl "nat" double_nn_sequence nil) (real_plus_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil)) shostak)) (nn_limit_lub_TCC1 0 (nn_limit_lub_TCC1-1 nil 3408300976 ("" (skosimp) (("" (rewrite "nn_convegent_bounded") nil nil)) nil) ((nonempty_image application-judgement "(nonempty?[real])" double_nn_sequence nil) (nn_convegent_bounded formula-decl nil double_nn_sequence 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) (nnreal type-eq-decl nil real_types nil)) nil)) (nn_limit_lub 0 (nn_limit_lub-1 nil 3408340830 ("" (skosimp) (("" (lemma "nn_series_increasing" ("v" "v!1")) (("" (lemma "nn_convegent_bounded" ("v" "v!1")) (("" (assert) (("" (lemma "increasing_bounded_convergence" ("v1" "series(v!1)")) (("1" (assert) (("1" (expand "sup") (("1" (rewrite "limit_def" 1) nil nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "Im") (("2" (expand "bounded_above?") (("2" (skosimp) (("2" (expand "upper_bound?") (("2" (inst + "x!1") (("2" (skosimp) (("2" (inst - "series(v!1)(x!2)") (("2" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnreal type-eq-decl nil real_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) (nn_series_increasing formula-decl nil double_nn_sequence nil) (nonempty_image application-judgement "(nonempty?[real])" double_nn_sequence nil) (upper_bound? const-decl "bool" bounded_real_defs nil) (x!2 skolem-const-decl "nat" double_nn_sequence nil) (v!1 skolem-const-decl "[nat -> nnreal]" double_nn_sequence nil) (= const-decl "[T, T -> boolean]" equalities nil) (limit_def formula-decl nil convergence_sequences "analysis/") (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (bounded_above? const-decl "bool" bounded_real_defs nil) (least_upper_bound? const-decl "bool" bounded_real_defs nil) (lub const-decl "{x | least_upper_bound?(x, SA)}" bounded_real_defs nil) (setof type-eq-decl nil defined_types nil) (Im const-decl "setof[real]" real_fun_props "reals/") (convergent? const-decl "bool" convergence_sequences "analysis/") (sup const-decl "real" real_fun_supinf "analysis/") (increasing_bounded_convergence formula-decl nil convergence_sequences "analysis/") (sequence type-eq-decl nil sequences nil) (bounded_above? const-decl "bool" real_fun_preds "reals/") (series const-decl "sequence[real]" series "series/") (nn_convegent_bounded formula-decl nil double_nn_sequence nil)) shostak)) (nn_convergence_least_upper_bound 0 (nn_convergence_least_upper_bound-1 nil 3408517555 ("" (skosimp) (("" (split) (("1" (flatten) (("1" (lemma "increasing_bounded_convergence" ("v1" "v!1")) (("1" (assert) (("1" (expand "sup") (("1" (expand "Im") (("1" (lemma "unique_limit" ("u" "v!1" "l1" "lub({z:real | EXISTS (x: nat): z = v!1(x)})" "l2" "l!1")) (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "v!1(0)") (("1" (inst + "0") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_above?") (("2" (inst + "l!1") (("2" (expand "upper_bound?") (("2" (skosimp) (("2" (typepred "s!1") (("2" (skosimp) (("2" (expand "convergence") (("2" (replace -1) (("2" (case "l!1<v!1(x!1)") (("1" (hide -2 1) (("1" (inst - "v!1(x!1)-l!1") (("1" (skosimp) (("1" (inst - "x!1+n!1") (("1" (assert) (("1" (expand "increasing?") (("1" (inst - "x!1" "n!1+x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "bounded_above?") (("2" (inst + "l!1") (("2" (skosimp) (("2" (case "l!1<v!1(x!1)") (("1" (hide 1) (("1" (expand "convergence") (("1" (inst - "v!1(x!1)-l!1") (("1" (skosimp) (("1" (inst - "x!1+n!1") (("1" (assert) (("1" (expand "increasing?") (("1" (inst - "x!1" "n!1+x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "convergence") (("2" (skosimp) (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (inst - "l!1-epsilon!1") (("2" (assert) (("2" (expand "upper_bound?") (("2" (skosimp) (("2" (typepred "s!1") (("2" (expand "Im") (("2" (skosimp) (("2" (inst + "x!1") (("2" (skosimp) (("2" (expand "increasing?") (("2" (inst -4 "x!1" "i!1") (("2" (assert) (("2" (inst - "v!1(i!1)") (("1" (expand "abs") (("1" (assert) (("1" (case-replace "v!1(i!1) - l!1 < 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "Im") (("2" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnreal type-eq-decl nil real_types nil) (bounded_above? const-decl "bool" real_fun_preds "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) (increasing_bounded_convergence formula-decl nil convergence_sequences "analysis/") (sup const-decl "real" real_fun_supinf "analysis/") (= const-decl "[T, T -> boolean]" equalities nil) (lub const-decl "{x | least_upper_bound?(x, SA)}" bounded_real_defs nil) (least_upper_bound? const-decl "bool" bounded_real_defs nil) (bounded_above? const-decl "bool" bounded_real_defs nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (unique_limit formula-decl nil convergence_sequences "analysis/") (AND const-decl "[bool, bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets 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) (increasing? const-decl "bool" real_fun_preds "reals/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (l!1 skolem-const-decl "nnreal" double_nn_sequence nil) (x!1 skolem-const-decl "nat" double_nn_sequence nil) (v!1 skolem-const-decl "[nat -> nnreal]" double_nn_sequence 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (convergence const-decl "bool" convergence_sequences "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (upper_bound? const-decl "bool" bounded_real_defs nil) (Im const-decl "setof[real]" real_fun_props "reals/") (nonempty_image application-judgement "(nonempty?[real])" double_nn_sequence nil) (x!1 skolem-const-decl "nat" double_nn_sequence nil) (setof type-eq-decl nil defined_types nil) (i!1 skolem-const-decl "nat" double_nn_sequence nil) (minus_real_is_real application-judgement "real" reals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil)) shostak)) (double_series 0 (double_series-1 nil 3408520787 ("" (skolem + ("_" "j!1" "u!1")) (("" (induct "i1") (("1" (expand "series") (("1" (expand "sigma" 1 4) (("1" (expand "sigma" 1 4) (("1" (expand "sigma" 1 1) (("1" (expand "sigma" 1 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "series") (("2" (expand "sigma" 1 4) (("2" (expand "sigma" 1 1) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "sigma_sum" ("low" "0" "high" "j!1" "F" "LAMBDA j: u!1(1 + j!2, j)" "G" "LAMBDA j: sigma(0, j!2, LAMBDA i: u!1(i, j))")) (("2" (assert) 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) (pred type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (sequence type-eq-decl nil sequences nil) (series const-decl "sequence[real]" series "series/") (nnreal type-eq-decl nil real_types nil) (nat_induction formula-decl nil naturalnumbers nil) (sigma def-decl "real" sigma "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (sigma_sum formula-decl nil sigma "reals/") (numfield nonempty-type-eq-decl nil number_fields 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_nnreal application-judgement "nnreal" sigma_nat "reals/")) shostak)) (double_subseq_convergent 0 (double_subseq_convergent-1 nil 3408341599 ("" (skosimp) (("" (lemma "nonneg_series_inj_conv" ("nna" "single_index(u!1)")) (("" (assert) (("" (hide -2) (("" (expand "o ") (("" (expand "single_index") (("" (lemma "double_index_n_bijective") (("" (expand "bijective?") (("" (flatten) (("" (inst - "lambda j: double_index_n(i!1,j)") (("1" (case-replace "(LAMBDA (x: nat): u!1(double_index_i(double_index_n(i!1, x)), double_index_j(double_index_n(i!1, x))))=(LAMBDA j: u!1(i!1, j))") (("1" (hide -2 2) (("1" (apply-extensionality :hide? t) (("1" (lemma "double_index_ij_n" ("i" "i!1" "j" "x!1")) (("1" (flatten) (("1" (replace -1) (("1" (replace -2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -2) (("2" (expand "injective?") (("2" (skosimp) (("2" (inst - "(i!1, x1!1)" "(i!1, x2!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((single_index const-decl "[nat -> T]" double_index nil) (sequence type-eq-decl nil sequences nil) (nnreal type-eq-decl nil real_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) (nonneg_series_inj_conv formula-decl nil absconv_series_aux "sigma_set/") (bijective? const-decl "bool" functions nil) (injective? const-decl "bool" functions nil) (double_index_n const-decl "nat" code_product nil) (i!1 skolem-const-decl "nat" double_nn_sequence nil) (double_index_ij_n formula-decl nil code_product nil) (= const-decl "[T, T -> boolean]" equalities nil) (double_index_i const-decl "nat" code_product nil) (double_index_j const-decl "nat" code_product nil) (double_index_n_bijective formula-decl nil code_product nil) (O const-decl "T3" function_props nil)) shostak)) (double_subseq_bounded 0 (double_subseq_bounded-1 nil 3408342728 ("" (skosimp) (("" (lemma "double_subseq_convergent" ("u" "u!1" "i" "i!1")) (("" (lemma "nn_convegent_bounded" ("v" "single_index(u!1)")) (("" (assert) (("" (lemma "nn_convegent_bounded" ("v" "LAMBDA j: u!1(i!1, j)")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((nnreal type-eq-decl nil real_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) (double_subseq_convergent formula-decl nil double_nn_sequence nil) (nonempty_image application-judgement "(nonempty?[real])" double_nn_sequence nil) (nn_convegent_bounded formula-decl nil double_nn_sequence nil) (single_index const-decl "[nat -> T]" double_index nil)) shostak)) (series_limit_def_TCC1 0 (series_limit_def_TCC1-1 nil 3408513053 ("" (subtype-tcc) nil 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)) (series_limit_def_TCC2 0 (series_limit_def_TCC2-1 nil 3408513053 ("" (skolem + ("_" "u!1")) (("" (case-replace "FORALL i: convergent?(LAMBDA j: u!1(i, j))") (("1" (induct "i1") (("1" (expand "series") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (inst - "0") nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "series") (("2" (expand "sigma" 1) (("2" (inst - "1+j!1") (("2" (lemma "convergent_sum" ("s1" "LAMBDA j: u!1(1 + j!1, j)" "s2" "LAMBDA j: sigma(0, j!1, LAMBDA i: u!1(i, j))")) (("2" (expand "+") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "i!1") 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) (convergent? const-decl "bool" convergence_sequences "analysis/") (nnreal type-eq-decl nil real_types nil) (convergent_sum formula-decl nil convergence_ops "analysis/") (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/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (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) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (sigma def-decl "real" sigma "reals/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nat_induction formula-decl nil naturalnumbers nil) (series const-decl "sequence[real]" series "series/") (pred type-eq-decl nil defined_types nil)) nil)) (series_limit_def 0 (series_limit_def-1 nil 3408513054 ("" (skolem + ("_" "u!1")) (("" (case-replace "FORALL i: convergent?(LAMBDA j: u!1(i, j))") (("1" (case "forall i: convergent?(LAMBDA j: series(LAMBDA i: u!1(i, j))(i))") (("1" (induct "i1") (("1" (expand "series") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "series") (("2" (expand "sigma" 1) (("2" (replace -1) (("2" (rewrite "limit_sum" 1 :dir rl) (("1" (expand "+" 1) (("1" (propax) nil nil)) nil) ("2" (inst - "j!1") nil nil) ("3" (inst -3 "1+j!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "i") (("1" (expand "series") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (inst - "0") nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "series") (("2" (expand "sigma" 1) (("2" (lemma "convergent_sum" ("s1" "LAMBDA j: u!1(1 + j!1, j)" "s2" "LAMBDA j: sigma(0, j!1, LAMBDA i: u!1(i, j))")) (("2" (inst - "1+j!1") (("2" (replace -2) (("2" (replace -3) (("2" (expand "+") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (inst - "i!1") 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) (convergent? const-decl "bool" convergence_sequences "analysis/") (nnreal type-eq-decl nil real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (convergent_sum formula-decl nil convergence_ops "analysis/") (u!1 skolem-const-decl "[[nat, nat] -> nnreal]" double_nn_sequence nil) (pred type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (limit const-decl "real" convergence_sequences "analysis/") (nat_induction formula-decl nil naturalnumbers nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sigma def-decl "real" sigma "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (+ const-decl "[T -> real]" real_fun_ops "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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (limit_sum formula-decl nil convergence_ops "analysis/") (numfield nonempty-type-eq-decl nil number_fields 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/") (series const-decl "sequence[real]" series "series/")) shostak)) (double_approx_TCC1 0 (double_approx_TCC1-1 nil 3408512402 ("" (subtype-tcc) nil nil) ((series const-decl "sequence[real]" series "series/") (convergence const-decl "bool" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")) nil)) (double_approx_TCC2 0 (double_approx_TCC2-1 nil 3408512810 ("" (skolem + ("_" "u!1")) (("" (induct "i1") (("1" (flatten) (("1" (expand "series") (("1" (expand "sigma" 1 2) (("1" (expand "sigma" 1 2) (("1" (inst - "0") nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (replace -2) (("2" (expand "series") (("2" (expand "sigma" 1 2) (("2" (inst - "1+j!1") (("2" (lemma "convergent_sum" ("s1" "LAMBDA (n: nat): sigma(0, n, LAMBDA j: u!1(1 + j!1, j))" "s2" "LAMBDA (n: nat): sigma(0, n, LAMBDA j: sigma(0, j!1, LAMBDA i: u!1(i, j)))")) (("2" (assert) (("2" (expand "+" -1) (("2" (hide -2 -3) (("2" (lemma "extensionality_postulate" ("f" "(LAMBDA (x: nat): sigma(0, x, LAMBDA j: u!1(1 + j!1, j)) + sigma(0, x, LAMBDA j: sigma(0, j!1, LAMBDA i: u!1(i, j))))" "g" "(LAMBDA (n: nat): sigma(0, n, LAMBDA j: u!1(1 + j!1, j) + sigma(0, j!1, LAMBDA i: u!1(i, j))))")) (("2" (flatten) (("2" (hide -2) (("2" (split -1) (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide -1 2) (("2" (skosimp*) (("2" (lemma "sigma_sum" ("low" "0" "high" "x!1" "F" "LAMBDA j: u!1(1 + j!1, j)" "G" "LAMBDA j: sigma(0, j!1, LAMBDA i: u!1(i, j))")) (("2" (assert) nil 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) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sequence type-eq-decl nil sequences nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (series const-decl "sequence[real]" series "series/") (nnreal type-eq-decl nil real_types nil) (nat_induction formula-decl nil naturalnumbers nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (sigma def-decl "real" sigma "reals/") (convergent_sum formula-decl nil convergence_ops "analysis/") (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/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (extensionality_postulate formula-decl nil functions nil) (sigma_sum formula-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) (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)) nil)) (double_approx 0 (double_approx-1 nil 3408512411 ("" (skosimp*) (("" (lemma "series_limit_def") (("" (inst - "i1!1" "lambda (i,j): series(LAMBDA j: u!1(i, j))(j)") (("1" (split) (("1" (expand "series") (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "extensionality_postulate" ("f" "(LAMBDA (j_1: nat): sigma(0, i1!1, LAMBDA (i_1: nat): sigma(0, j_1, LAMBDA j: u!1(i_1, j))))" "g" "(LAMBDA (n: nat): sigma(0, n, LAMBDA j: sigma(0, i1!1, LAMBDA i: u!1(i, j))))")) (("1" (flatten) (("1" (hide -2 -3) (("1" (split -1) (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (induct "x") (("1" (expand "sigma" 1 3) (("1" (expand "sigma" 1 3) (("1" (expand "sigma" 1 2) (("1" (expand "sigma" 1 2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1 3) (("2" (expand "sigma" 1 2) (("2" (lemma "sigma_sum" ("low" "0" "high" "i1!1" "F" "LAMBDA (i_1: nat): u!1(i_1, 1 + j!1)" "G" "LAMBDA (i_1: nat):sigma(0, j!1, LAMBDA j: u!1(i_1, j))")) (("2" (replace -1 1 rl) (("2" (hide -1) (("2" (replace -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "i_1") (("1" (inst - "0") (("1" (expand "series") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "series") (("2" (inst - "1+j!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (expand "series") (("2" (lemma "sigma_ge_0" ("low" "0" "high" "j!1" "F" "LAMBDA (j_1: nat): u!1(i!1, j_1)")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((series_limit_def formula-decl nil double_nn_sequence nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_ge_0 formula-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (extensionality_postulate formula-decl nil functions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sigma_sum formula-decl nil sigma "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (convergent? const-decl "bool" 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) (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 "series/") (nnreal type-eq-decl nil real_types nil) (u!1 skolem-const-decl "[[nat, nat] -> nnreal]" double_nn_sequence nil)) shostak)) (double_approx1_TCC1 0 (double_approx1_TCC1-1 nil 3408955470 ("" (skosimp) (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (inst - "series(LAMBDA j: series(LAMBDA i: u!1(i, j))(0))(0)") (("" (inst + "0" "0") nil nil)) nil)) nil)) nil)) nil)) nil) ((nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (nnreal type-eq-decl nil real_types nil) (series const-decl "sequence[real]" series "series/") (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) (empty? const-decl "bool" sets nil)) nil)) (double_approx1 0 (double_approx1-1 nil 3408955569 ("" (skosimp) (("" (split) (("1" (flatten) (("1" (lemma "nn_convegent_bounded" ("v" "single_index(u!1)")) (("1" (flatten -1) (("1" (hide -2) (("1" (split) (("1" (lemma "nn_convergence_least_upper_bound" ("v" "series(single_index(u!1))" "l" "l!1")) (("1" (rewrite "nn_series_increasing") (("1" (assert) (("1" (hide -2 -3) (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (split 1) (("1" (hide -2) (("1" (expand "upper_bound?") (("1" (skosimp) (("1" (typepred "s!1") (("1" (skosimp) (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (expand "series") (("1" (lemma "nn_index_scaf3" ("u" "u!1")) (("1" (inst - "i!1" "j!1") (("1" (skosimp) (("1" (inst - "series(single_index(u!1))(n!1)") (("1" (lemma "double_series" ("u" "u!1")) (("1" (expand "series" -1) (("1" (inst - "i!1" "j!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "Im") (("2" (inst + "n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "upper_bound?" -1) (("2" (inst -3 "y!1") (("2" (assert) (("2" (case "y!1<l!1") (("1" (hide 1) (("1" (expand "upper_bound?") (("1" (skosimp) (("1" (typepred "s!1") (("1" (expand "Im" -1) (("1" (skolem - ("n!1")) (("1" (replace -1) (("1" (lemma "nn_index_scaf4" ("n" "n!1" "u" "u!1")) (("1" (skosimp) (("1" (inst - "series(LAMBDA j: series(LAMBDA i: u!1(i, j))(i!1))(j!1)") (("1" (rewrite "double_series" -4 :dir rl) (("1" (expand "series" -4) (("1" (assert) nil nil)) nil)) nil) ("2" (inst + "i!1" "j!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "series") (("2" (rewrite "sigma_ge_0") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "convergent?") (("2" (inst + "l!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "bounded_above?(Im(series(single_index(u!1))))") (("1" (lemma "nn_convegent_bounded" ("v" "single_index(u!1)")) (("1" (assert) (("1" (lemma "nn_convergence_least_upper_bound" ("v" "series(single_index(u!1))" "l" "l!1")) (("1" (rewrite "nn_series_increasing") (("1" (replace -1) (("1" (hide -1 -2) (("1" (hide -1) (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (split) (("1" (expand "upper_bound?") (("1" (skosimp) (("1" (typepred "s!1") (("1" (expand "Im" -1) (("1" (skolem - ("n!1")) (("1" (lemma "nn_index_scaf4" ("u" "u!1" "n" "n!1")) (("1" (skosimp) (("1" (inst - "series(LAMBDA j: series(LAMBDA i: u!1(i, j))(i!1))(j!1)") (("1" (rewrite "double_series" -3 :dir rl) (("1" (expand "series" -3) (("1" (assert) nil nil)) nil)) nil) ("2" (inst + "i!1" "j!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -3 "y!1") (("2" (assert) (("2" (case "y!1<l!1") (("1" (hide 1) (("1" (expand "upper_bound?" 1) (("1" (skosimp) (("1" (typepred "s!1") (("1" (skosimp) (("1" (rewrite "double_series" -1 :dir rl) (("1" (expand "series" -1) (("1" (lemma "nn_index_scaf3" ("u" "u!1")) (("1" (inst - "i!1" "j!1") (("1" (skosimp) (("1" (replace -2) (("1" (expand "upper_bound?" -4) (("1" (inst - "series(single_index(u!1))(n!1)") (("1" (assert) nil nil) ("2" (expand "Im") (("2" (inst + "n!1") 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)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "series") (("2" (rewrite "sigma_ge_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (hide -2 2) (("2" (expand "bounded_above?") (("2" (inst + "l!1") (("2" (expand "upper_bound?") (("2" (skosimp) (("2" (typepred "s!1") (("2" (expand "Im") (("2" (skolem - "n!1") (("2" (replace -1) (("2" (hide -1) (("2" (lemma "nn_index_scaf4" ("u" "u!1" "n" "n!1")) (("2" (skosimp) (("2" (inst - "series(LAMBDA j: series(LAMBDA i: u!1(i, j))(i!1))(j!1)") (("1" (rewrite "double_series" -2 :dir rl) (("1" (expand "series") (("1" (assert) nil nil)) nil)) nil) ("2" (inst + "i!1" "j!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((single_index const-decl "[nat -> T]" double_index nil) (nnreal type-eq-decl nil real_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) (nn_convegent_bounded formula-decl nil double_nn_sequence nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (series const-decl "sequence[real]" series "series/") (sequence type-eq-decl nil sequences nil) (nn_convergence_least_upper_bound formula-decl nil double_nn_sequence nil) (nonempty_image application-judgement "(nonempty?[real])" double_nn_sequence nil) (least_upper_bound? const-decl "bool" bounded_real_defs nil) (upper_bound? const-decl "bool" bounded_real_defs nil) (NOT const-decl "[bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (setof type-eq-decl nil defined_types nil) (Im const-decl "setof[real]" real_fun_props "reals/") (u!1 skolem-const-decl "[[nat, nat] -> nnreal]" double_nn_sequence nil) (n!1 skolem-const-decl "nat" double_nn_sequence nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (double_series formula-decl nil double_nn_sequence nil) (nn_index_scaf3 formula-decl nil double_nn_sequence nil) (j!1 skolem-const-decl "nat" double_nn_sequence nil) (i!1 skolem-const-decl "nat" double_nn_sequence nil) (nn_index_scaf4 formula-decl nil double_nn_sequence nil) (< const-decl "bool" reals nil) (nn_series_increasing formula-decl nil double_nn_sequence nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_ge_0 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/") (bounded_above? const-decl "bool" bounded_real_defs nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (i!1 skolem-const-decl "nat" double_nn_sequence nil) (j!1 skolem-const-decl "nat" double_nn_sequence nil) (n!1 skolem-const-decl "nat" double_nn_sequence nil) (j!1 skolem-const-decl "nat" double_nn_sequence nil) (i!1 skolem-const-decl "nat" double_nn_sequence nil)) shostak)) (double_approx2 0 (double_approx2-1 nil 3409031657 ("" (skosimp) (("" (lemma "nn_convergence_least_upper_bound" ("v" "series(LAMBDA i: limit(series(LAMBDA j: u!1(i, j))))" "l" "l!1")) (("1" (rewrite "nn_series_increasing") (("1" (replace -1) (("1" (hide -1) (("1" (split) (("1" (flatten) (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (case-replace "upper_bound?(l!1, {z | EXISTS i, j: series(LAMBDA j: series(LAMBDA i: u!1(i, j))(i))(j) = z})") (("1" (skosimp) (("1" (inst -3 "y!1") (("1" (assert) (("1" (case "y!1<l!1") (("1" (hide 2) (("1" (expand "upper_bound?") (("1" (skosimp) (("1" (typepred "s!1") (("1" (expand "Im" -1) (("1" (skolem - ("n!1")) (("1" (lemma "double_approx" ("u" "u!1")) (("1" (inst -1 "n!1") (("1" (replace -7) (("1" (replace -2 * rl) (("1" (lemma "nn_limit_lub" ("v" "(LAMBDA j: series(LAMBDA i: u!1(i, j))(n!1))")) (("1" (replace -2 * rl) (("1" (lemma "nn_convegent_bounded" ("v" "LAMBDA j: series(LAMBDA i: u!1(i, j))(n!1)")) (("1" (flatten -1) (("1" (hide -1) (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (hide -2 -3) (("1" (typepred "lub(Im(series((LAMBDA j: series(LAMBDA i: u!1(i, j))(n!1)))))") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (replace -3 * rl) (("1" (inst -2 "y!1") (("1" (assert) (("1" (expand "upper_bound?" 1) (("1" (skosimp) (("1" (typepred "s!2") (("1" (expand "Im" -1) (("1" (skosimp) (("1" (inst -7 "s!2") (("1" (inst + "n!1" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-5 1)) (("2" (expand "bounded_above?") (("2" (inst + "l!1") (("2" (expand "upper_bound?") (("2" (skosimp) (("2" (typepred "s!2") (("2" (expand "Im") (("2" (skosimp) (("2" (inst - "s!2") (("2" (inst + "n!1" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "series") (("2" (rewrite "sigma_ge_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -2) (("2" (expand "upper_bound?") (("2" (skosimp) (("2" (typepred "s!1") (("2" (skosimp) (("2" (rewrite "double_series" -1 :dir rl) (("2" (inst - "series(LAMBDA i: limit(series(LAMBDA j: u!1(i, j))))(i!1)") (("1" (case "series(LAMBDA i: series(LAMBDA j: u!1(i, j))(j!1))(i!1)<=series(LAMBDA i: limit(series( (("1" (assert) nil nil) ("2" (hide-all-but (-3 1)) (("2" (expand "series" 1 3) (("2" (expand "series" 1 1) (("2" (rewrite "sigma_le") (("2" (hide 2) (("2" (skosimp) (("2" (inst - "n!1") (("2" (lemma "nn_limit_lub" ("v" "LAMBDA j: u!1(n!1, j)")) (("2" (assert) (("2" (replace -1) (("2" (hide -1 -2) (("2" (typepred "lub(Im(series(LAMBDA j: u!1(n!1, j))))") (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (hide -2) (("2" (expand "upper_bound?") (("2" (inst - "series(LAMBDA j: u!1(n!1, j))(j!1)") (("2" (expand "Im") (("2" (inst + "j!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "Im") (("2" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (expand "nonempty?") (("3" (expand "empty?") (("3" (expand "member") (("3" (inst - "series(LAMBDA j: series(LAMBDA i: u!1(i, j))(0))(0)") (("3" (inst + "0" "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (case-replace "upper_bound?(l!1, Im(series(LAMBDA i: limit(series(LAMBDA j: u!1(i, j))))))") (("1" (skosimp) (("1" (inst -3 "y!1") (("1" (assert) (("1" (case "y!1<l!1") (("1" (hide 2) (("1" (expand "upper_bound?") (("1" (skosimp) (("1" (typepred "s!1") (("1" (skosimp) (("1" (inst -5 "series(LAMBDA i: limit(series(LAMBDA j: u!1(i, j))))(i!1)") (("1" (rewrite "double_series" -1 :dir rl) (("1" (case "series(LAMBDA i: series(LAMBDA j: u!1(i, j))(j!1))(i!1)<=series(LAMBDA i: limit(series( (("1" (assert) nil nil) ("2" (hide-all-but (-6 1)) (("2" (expand "series" 1 3) (("2" (expand "series" 1 1) (("2" (rewrite "sigma_le") (("2" (hide 2) (("2" (skosimp) (("2" (inst - "n!1") (("2" (lemma "nn_limit_lub" ("v" "LAMBDA j: u!1(n!1, j)")) (("2" (replace -2) (("2" (replace -1) (("2" (hide -1 -2) (("2" (typepred "lub(Im(series(LAMBDA j: u!1(n!1, j))))") (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (hide -2) (("2" (expand "upper_bound?") (("2" (inst - "series(LAMBDA j: u!1(n!1, j))(j!1)") (("2" (expand "Im") (("2" (inst + "j!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "Im") (("2" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "upper_bound?") (("2" (skosimp) (("2" (typepred "s!1") (("2" (expand "Im" -1) (("2" (skolem - ("n!1")) (("2" (lemma "double_approx" ("u" "u!1")) (("2" (inst - "n!1") (("2" (replace -5) (("2" (replace -2 * rl) (("2" (lemma "nn_limit_lub" ("v" "LAMBDA j: series(LAMBDA i: u!1(i, j))(n!1)")) (("1" (replace -2 * rl) (("1" (lemma "nn_convegent_bounded" ("v" "LAMBDA j: series(LAMBDA i: u!1(i, j))(n!1)")) (("1" (replace -1 -2) (("1" (hide -1) (("1" (split -1) (("1" (hide -2 -3) (("1" (typepred "lub(Im(series(LAMBDA j: series(LAMBDA i: u!1(i, j))(n!1))))") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (replace -3 * rl) (("1" (inst -2 "l!1") (("1" (assert) (("1" (expand "upper_bound?" 1) (("1" (skosimp) (("1" (typepred "s!2") (("1" (expand "Im" -1) (("1" (skosimp) (("1" (inst -4 "s!2") (("1" (inst + "n!1" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (expand "bounded_above?") (("2" (inst + "l!1") (("2" (expand "upper_bound?") (("2" (skosimp) (("2" (typepred "s!2") (("2" (expand "Im") (("2" (skosimp) (("2" (inst - "s!2") (("2" (inst + "n!1" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "series") (("2" (rewrite "sigma_ge_0") 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 -1) (("2" (skosimp) (("2" (inst - "i!1") (("2" (lemma "limit_nonneg" ("nna" "series(LAMBDA j: u!1(i!1, j))")) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "series") (("2" (rewrite "sigma_ge_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "series") (("2" (rewrite "sigma_ge_0") (("2" (hide 2) (("2" (skosimp) (("2" (inst - "n!1") (("2" (lemma "limit_nonneg" ("nna" "LAMBDA (n: nat): sigma(0, n, LAMBDA j: u!1(n!1, j))")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil)) nil) ((limit const-decl "real" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (series const-decl "sequence[real]" series "series/") (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) (nnreal 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) (nn_convergence_least_upper_bound formula-decl nil double_nn_sequence nil) (limit_nonneg formula-decl nil series_lems "series/") (least_upper_bound? const-decl "bool" bounded_real_defs nil) (= const-decl "[T, T -> boolean]" equalities nil) (upper_bound? const-decl "bool" bounded_real_defs nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (< const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (setof type-eq-decl nil defined_types nil) (Im const-decl "setof[real]" real_fun_props "reals/") (sigma_ge_0 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/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (bounded_above? const-decl "bool" bounded_real_defs nil) (lub const-decl "{x | least_upper_bound?(x, SA)}" bounded_real_defs nil) (s!2 skolem-const-decl "(Im(series((LAMBDA j: series(LAMBDA i: u!1(i, j))(n!1)))))" double_nn_sequence nil) (n!1 skolem-const-decl "nat" double_nn_sequence nil) (u!1 skolem-const-decl "[[nat, nat] -> nnreal]" double_nn_sequence nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (s!2 skolem-const-decl "(Im(series(LAMBDA j: series(LAMBDA i: u!1(i, j))(n!1))))" double_nn_sequence nil) (nn_convegent_bounded formula-decl nil double_nn_sequence nil) (nn_limit_lub formula-decl nil double_nn_sequence nil) (double_approx formula-decl nil double_nn_sequence nil) (nonempty_image application-judgement "(nonempty?[real])" double_nn_sequence nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (i!1 skolem-const-decl "nat" double_nn_sequence nil) (subrange type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (n!1 skolem-const-decl "subrange(0, i!1)" double_nn_sequence nil) (j!1 skolem-const-decl "nat" double_nn_sequence nil) (sigma_le formula-decl nil sigma "reals/") (double_series formula-decl nil double_nn_sequence nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (i!1 skolem-const-decl "nat" double_nn_sequence nil) (j!1 skolem-const-decl "nat" double_nn_sequence nil) (n!1 skolem-const-decl "subrange(0, i!1)" double_nn_sequence nil) (s!2 skolem-const-decl "(Im(series(LAMBDA j: series(LAMBDA i: u!1(i, j))(n!1))))" double_nn_sequence nil) (n!1 skolem-const-decl "nat" double_nn_sequence nil) (s!2 skolem-const-decl "(Im(series(LAMBDA j: series(LAMBDA i: u!1(i, j))(n!1))))" double_nn_sequence nil) (nn_series_increasing formula-decl nil double_nn_sequence nil) (sigma def-decl "real" sigma "reals/")) shostak)) (double_left_convergence 0 (double_left_convergence-1 nil 3409030535 ("" (skosimp) (("" (case-replace "(FORALL i: convergent?(series(LAMBDA j: u!1(i, j))))") (("1" (lemma "double_approx2" ("u" "u!1" "l" "l!1")) (("1" (lemma "double_approx1" ("u" "u!1" "l" "l!1")) (("1" (replace -3) (("1" (name-replace "LUB" "least_upper_bound?(l!1, {z | EXISTS i, j: series(LAMBDA j: series(LAMBDA i: u!1(i, j))(i)) (j) = z})") (("1" (replace -1) (("1" (replace -2) (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "series(LAMBDA j: series(LAMBDA i: u!1(i, j))(0))(0)") (("2" (inst + "0" "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split) (("1" (flatten) (("1" (hide 1) (("1" (skosimp) (("1" (lemma "double_subseq_convergent" ("u" "u!1" "i" "i!1")) (("1" (assert) (("1" (expand "convergent?") (("1" (hide 2) (("1" (inst + "l!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) 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) (convergent? const-decl "bool" convergence_sequences "analysis/") (series const-decl "sequence[real]" series "series/") (nnreal type-eq-decl nil real_types nil) (double_approx1 formula-decl nil double_nn_sequence nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (least_upper_bound? const-decl "bool" bounded_real_defs nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (double_approx2 formula-decl nil double_nn_sequence nil) (double_subseq_convergent formula-decl nil double_nn_sequence nil)) shostak)) (double_left_convergent 0 (double_left_convergent-1 nil 3408341025 ("" (skosimp) (("" (split) (("1" (flatten) (("1" (split) (("1" (skosimp) (("1" (lemma "double_subseq_convergent" ("u" "u!1" "i" "i!1")) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "convergent?") (("2" (skosimp) (("2" (inst + "l!1") (("2" (lemma "double_left_convergence" ("u" "u!1" "l" "l!1")) (("1" (assert) nil nil) ("2" (lemma "limit_nonneg" ("nna" "series(single_index(u!1))")) (("1" (assert) (("1" (split -1) (("1" (rewrite "limit_def" -2 :dir rl) (("1" (assert) nil nil)) nil) ("2" (expand "convergent?") (("2" (inst + "l!1") nil nil)) nil)) nil)) nil) ("2" (skolem + ("n!1")) (("2" (lemma "nn_series_increasing" ("v" "single_index[nnreal](u!1)")) (("2" (expand "increasing?") (("2" (inst - "0" "n!1") (("2" (assert) (("2" (expand "series" -1 1) (("2" (expand "sigma") (("2" (expand "single_index") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "convergent?" (-2 1)) (("2" (skosimp) (("2" (inst + "l!1") (("2" (lemma "double_left_convergence" ("u" "u!1" "l" "l!1")) (("1" (replace -1 1) (("1" (replace -2) (("1" (propax) nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "limit_nonneg" ("nna" "series(LAMBDA i: limit(series(LAMBDA j: u!1(i, j))))")) (("1" (split -1) (("1" (rewrite "limit_def" -3 :dir rl) (("1" (assert) nil nil)) nil) ("2" (expand "convergent?") (("2" (inst + "l!1") nil nil)) nil)) nil) ("2" (skolem + ("n!1")) (("2" (hide -2 2) (("2" (lemma "nn_series_increasing" ("v" "LAMBDA i: limit(series(LAMBDA j: u!1(i, j)))")) (("1" (expand "increasing?") (("1" (inst - "0" "n!1") (("1" (assert) (("1" (expand "series" -1 1) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (inst - "0") (("1" (lemma "limit_nonneg" ("nna" "series(LAMBDA j: u!1(0, j))")) (("1" (split -1) (("1" (assert) nil nil) ("2" (propax) nil nil)) nil) ("2" (skolem + ("m!1")) (("2" (hide 2) (("2" (expand "series") (("2" (lemma "sigma_ge_0" ("low" "0" "high" "m!1" "F" "LAMBDA j: u!1(0, j)")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "i!1") (("2" (hide 2) (("2" (lemma "limit_nonneg" ("nna" "series(LAMBDA j: u!1(i!1, j))")) (("1" (assert) nil nil) ("2" (skolem + ("m!1")) (("2" (hide -1 2) (("2" (expand "series") (("2" (lemma "sigma_ge_0" ("low" "0" "high" "m!1" "F" "LAMBDA j: u!1(i!1, j)")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnreal type-eq-decl nil real_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) (double_subseq_convergent formula-decl nil double_nn_sequence nil) (double_left_convergence formula-decl nil double_nn_sequence nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (increasing? const-decl "bool" real_fun_preds "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma def-decl "real" sigma "reals/") (sigma_0_neg formula-decl nil sigma_nat "reals/") (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nn_series_increasing formula-decl nil double_nn_sequence nil) (limit_def formula-decl nil convergence_sequences "analysis/") (limit_nonneg formula-decl nil series_lems "series/") (sequence type-eq-decl nil sequences nil) (series const-decl "sequence[real]" series "series/") (single_index const-decl "[nat -> T]" double_index nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (sigma_ge_0 formula-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (limit const-decl "real" convergence_sequences "analysis/")) shostak)) (double_left_limit_TCC1 0 (double_left_limit_TCC1-1 nil 3408339534 ("" (skosimp) (("" (lemma "double_left_convergent" ("u" "u!1")) (("" (assert) (("" (flatten) nil nil)) nil)) nil)) nil) ((nnreal type-eq-decl nil real_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) (double_left_convergent formula-decl nil double_nn_sequence nil)) nil)) (double_left_limit_TCC2 0 (double_left_limit_TCC2-1 nil 3408516161 ("" (skosimp) (("" (lemma "double_left_convergent" ("u" "u!1")) (("" (assert) nil nil)) nil)) nil) ((nnreal type-eq-decl nil real_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) (double_left_convergent formula-decl nil double_nn_sequence nil)) nil)) (double_left_limit 0 (double_left_limit-1 nil 3408341291 ("" (skosimp) (("" (lemma "double_left_convergence" ("u" "u!1" "l" "limit(series(single_index(u!1)))")) (("1" (rewrite "limit_lemma") (("1" (rewrite "limit_def" -1 :dir rl) (("1" (assert) nil nil) ("2" (skosimp) (("2" (lemma "double_subseq_convergent" ("u" "u!1" "i" "i!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "limit_nonneg" ("nna" "series(single_index(u!1))")) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (lemma "nn_series_increasing" ("v" "single_index[nnreal](u!1)")) (("2" (expand "increasing?") (("2" (inst - "0" "x1!1") (("2" (assert) (("2" (expand "series" -1 1) (("2" (expand "sigma") (("2" (expand "sigma") (("2" (expand "single_index" -1 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((single_index const-decl "[nat -> T]" double_index nil) (series const-decl "sequence[real]" series "series/") (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) (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) (nnreal 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) (double_left_convergence formula-decl nil double_nn_sequence nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (limit_def formula-decl nil convergence_sequences "analysis/") (double_subseq_convergent formula-decl nil double_nn_sequence nil) (limit_lemma formula-decl nil convergence_sequences "analysis/") (limit_nonneg formula-decl nil series_lems "series/") (increasing? const-decl "bool" real_fun_preds "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma def-decl "real" sigma "reals/") (nn_series_increasing formula-decl nil double_nn_sequence nil)) shostak)) (double_right_convergence 0 (double_right_convergence-1 nil 3450445461 ("" (skosimp) (("" (name "PHI" "lambda n: double_index_n(double_index_j(n), double_index_i(n))") (("" (case "bijective?[nat,nat](PHI)") (("1" (split 1) (("1" (flatten) (("1" (lemma "nonneg_series_bij" ("nna" "single_index(u!1)" "nnx" "l!1" "phi" "PHI")) (("1" (assert) (("1" (expand "o") (("1" (case-replace "(LAMBDA (x: nat): single_index(u!1)(PHI(x)))=single_index(LAMBDA j, i: u!1(i, j))") (("1" (hide-all-but 1) (("1" (apply-extensionality :hide? t) (("1" (expand "single_index") (("1" (expand "PHI") (("1" (lemma "double_index_ij_n" ("i" "double_index_j(x!1)" "j" "double_index_i(x!1)")) (("1" (flatten) (("1" (replace -1) (("1" (replace -2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (flatten) (("2" (lemma "nonneg_series_bij" ("nna" "single_index(LAMBDA j, i: u!1(i, j))" "nnx" "l!1" "phi" "PHI")) (("1" (assert) (("1" (expand "o") (("1" (case-replace "(LAMBDA (x: nat): single_index(LAMBDA j, i: u!1(i, j))(PHI(x)))=single_index(u!1)") (("1" (apply-extensionality :hide? t) (("1" (hide-all-but 1) (("1" (expand "PHI") (("1" (expand "single_index") (("1" (lemma "double_index_ij_n" ("i" "double_index_j(x!1)" "j" "double_index_i(x!1)")) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "PHI") (("2" (lemma "double_index_n_bijective") (("2" (expand "bijective?") (("2" (flatten) (("2" (split) (("1" (expand "injective?") (("1" (skosimp) (("1" (inst -2 "(double_index_j(x1!1), double_index_i(x1!1))" "(double_index_j(x2!1), double_index_i(x2!1))") (("1" (assert) (("1" (flatten) (("1" (expand "double_index_i") (("1" (assert) (("1" (replace -2) (("1" (assert) (("1" (expand "double_index_j") (("1" (hide -1) (("1" (replace -2) (("1" (name-replace "TRI" "double_index_triangle(x2!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "surjective?") (("2" (skosimp) (("2" (inst - "y!1") (("2" (hide -1) (("2" (inst + "double_index_n(double_index_j(y!1), double_index_i(y!1))") (("2" (lemma "double_index_ij_n" ("i" "double_index_j(y!1)" "j" "double_index_i(y!1)")) (("2" (flatten) (("2" (replace -1) (("2" (replace -2) (("2" (rewrite "double_index_n_ij") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((double_index_i const-decl "nat" code_product nil) (double_index_j const-decl "nat" code_product nil) (double_index_n const-decl "nat" code_product nil) (= const-decl "[T, T -> boolean]" equalities 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) (double_index_n_bijective formula-decl nil code_product nil) (double_index_n_ij formula-decl nil code_product nil) (surjective? const-decl "bool" functions nil) (injective? const-decl "bool" functions nil) (int_minus_int_is_int application-judgement "int" integers nil) (double_index_triangle const-decl "nat" code_product nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (single_index const-decl "[nat -> T]" double_index nil) (sequence type-eq-decl nil sequences nil) (nnreal type-eq-decl nil real_types nil) (nonneg_series_bij formula-decl nil series_lems "series/") (O const-decl "T3" function_props nil) (double_index_ij_n formula-decl nil code_product nil) (PHI skolem-const-decl "[nat -> nat]" double_nn_sequence nil) (bijective? const-decl "bool" functions nil)) shostak)) (double_right_convergent 0 (double_right_convergent-1 nil 3450448710 ("" (skosimp) (("" (expand "convergent?") (("" (split) (("1" (skosimp) (("1" (skosimp) (("1" (inst + "l!1") (("1" (rewrite "double_right_convergence") (("1" (lemma "limit_nonneg" ("nna" "series(single_index(u!1))")) (("1" (split -1) (("1" (rewrite "limit_def" -2 :dir rl) (("1" (assert) nil nil)) nil) ("2" (expand "convergent?") (("2" (inst + "l!1") nil nil)) nil)) nil) ("2" (skolem + "i!1") (("2" (hide-all-but 1) (("2" (expand "series") (("2" (lemma "sigma_ge_0[nat]" ("low" "0" "high" "i!1" "F" "single_index[nnreal](u!1)")) (("2" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "single_index") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "l!1") (("2" (rewrite "double_right_convergence" 1) (("2" (hide 2) (("2" (lemma "limit_nonneg" ("nna" "series(single_index(LAMBDA j, i: u!1(i, j)))")) (("1" (split) (("1" (rewrite "limit_def" -2 :dir rl) (("1" (assert) nil nil)) nil) ("2" (expand "convergent?") (("2" (inst + "l!1") nil nil)) nil)) nil) ("2" (hide -1 2) (("2" (skolem + "n!1") (("2" (expand "series") (("2" (expand "single_index") (("2" (lemma "sigma_ge_0[nat]" ("low" "0" "high" "n!1" "F" "LAMBDA n: u!1(double_index_j(n), double_index_i(n))")) (("2" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((convergent? const-decl "bool" convergence_sequences "analysis/") (double_index_j const-decl "nat" code_product nil) (double_index_i const-decl "nat" code_product 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) (single_index const-decl "[nat -> T]" double_index nil) (series const-decl "sequence[real]" series "series/") (sequence type-eq-decl nil sequences nil) (limit_nonneg formula-decl nil series_lems "series/") (limit_def formula-decl nil convergence_sequences "analysis/") (sigma_ge_0 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/") (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) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (double_right_convergence formula-decl nil double_nn_sequence nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (double_right_limit_TCC1 0 (double_right_limit_TCC1-1 nil 3450448709 ("" (skosimp) (("" (lemma "double_right_convergent" ("u" "u!1")) (("" (assert) nil nil)) nil)) nil) ((nnreal type-eq-decl nil real_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) (double_right_convergent formula-decl nil double_nn_sequence nil)) nil)) (double_right_limit 0 (double_right_limit-1 nil 3450455470 ("" (skosimp) (("" (expand "convergent?") (("" (skosimp) (("" (lemma "double_right_convergence" ("u" "u!1" "l" "l!1")) (("1" (assert) (("1" (rewrite "limit_def" -1 :dir rl) (("1" (rewrite "limit_def" -2 :dir rl) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "limit_nonneg" ("nna" "series(single_index(u!1))")) (("1" (split) (("1" (rewrite "limit_def" -2 :dir rl) (("1" (assert) nil nil)) nil) ("2" (expand "convergent?") (("2" (inst + "l!1") nil nil)) nil)) nil) ("2" (skolem + ("n!1")) (("2" (hide-all-but 1) (("2" (expand "series") (("2" (expand "single_index") (("2" (rewrite "sigma_ge_0[nat]" +) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((convergent? const-decl "bool" convergence_sequences "analysis/") (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) (nnreal 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) (double_right_convergence formula-decl nil double_nn_sequence nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (limit_def formula-decl nil convergence_sequences "analysis/") (sequence type-eq-decl nil sequences nil) (series const-decl "sequence[real]" series "series/") (single_index const-decl "[nat -> T]" double_index nil) (limit_nonneg formula-decl nil series_lems "series/") (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) (double_index_j const-decl "nat" code_product nil) (double_index_i const-decl "nat" code_product nil) (sigma_ge_0 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) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")) shostak)))
¤ Dauer der Verarbeitung: 0.270 Sekunden (vorverarbeitet am 2026-04-30) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26