| 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 147 kB |
|
Quelle extended_nnreal.prfSprache: Lisp |
|||||||||||||||
|
(extended_nnreal (x_inf_TCC1 0 (x_inf_TCC1-1 nil 3396791560 ("" (skosimp*) (("" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "x!1`2") (("1" (inst + "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "0") (("2" (expand "lower_bound?") (("2" (skosimp) (("2" (typepred "s!1") (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil) (set type-eq-decl nil sets nil) (member const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (lower_bound? const-decl "bool" bounded_real_defs nil) (bounded_below? const-decl "bool" bounded_real_defs nil)) nil)) (x_inf_TCC2 0 (x_inf_TCC2-1 nil 3396791560 ("" (skosimp*) (("" (lemma "x_inf_TCC1" ("X" "X!1")) (("" (split -1) (("1" (flatten) (("1" (typepred "glb({z | EXISTS x: X!1(x) AND x`1 AND x`2 = z})") (("1" (name-replace "GLB" "glb({zz:real | EXISTS y: X!1(y) AND y`1 AND y`2 = zz})") (("1" (expand "greatest_lower_bound?") (("1" (flatten) (("1" (inst - "0") (("1" (assert) (("1" (hide 2) (("1" (expand "lower_bound?") (("1" (skosimp) (("1" (typepred "s!1") (("1" (skosimp) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (inst - "x!1") nil nil)) nil)) nil)) nil) ((set type-eq-decl nil sets nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (x_inf_TCC1 subtype-tcc nil extended_nnreal nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (lower_bound? const-decl "bool" bounded_real_defs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (nonempty? const-decl "bool" sets nil) (greatest_lower_bound? const-decl "bool" bounded_real_defs nil) (bounded_below? const-decl "bool" bounded_real_defs nil) (glb const-decl "{x | greatest_lower_bound?(x, SB)}" bounded_real_defs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil)) nil)) (x_sup_TCC1 0 (x_sup_TCC1-1 nil 3431062706 ("" (skosimp*) (("" (expand "empty?") (("" (skosimp) (("" (expand "member") (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (inst - "x!1`2") (("" (inst + "x!1") (("" (inst + "x!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (member const-decl "bool" sets 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil) (set type-eq-decl nil sets nil) (X!1 skolem-const-decl "set[extended_nnreal]" extended_nnreal nil) (x!1 skolem-const-decl "extended_nnreal" extended_nnreal nil) (nonempty? const-decl "bool" sets nil)) nil)) (x_sup_TCC2 0 (x_sup_TCC2-1 nil 3431062706 ("" (skosimp*) (("" (replace -1) (("" (lemma "x_sup_TCC1" ("X" "X!1")) (("" (replace 3) (("" (replace 2) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((x_sup_TCC1 subtype-tcc nil extended_nnreal nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil 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) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil) (set type-eq-decl nil sets nil)) nil)) (x_sup_TCC3 0 (x_sup_TCC3-1 nil 3431063075 ("" (skosimp*) (("" (lemma "x_sup_TCC2" ("X" "X!1")) (("" (replace -2) (("" (replace 1) (("" (replace 2) (("" (typepred "lub({z | EXISTS x: X!1(x) AND x`1 AND x`2 = z})") (("1" (expand "least_upper_bound?") (("1" (name-replace "LUB" "lub({z | EXISTS x: X!1(x) AND x`1 AND x`2 = z})") (("1" (flatten) (("1" (expand "empty?") (("1" (hide 1 2 -4) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (skosimp) (("1" (skosimp) (("1" (expand "upper_bound?") (("1" (hide -2) (("1" (inst - "x!1") (("1" (assert) nil nil) ("2" (inst + "x!2") (("2" (assert) 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) ((set type-eq-decl nil sets nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (x_sup_TCC2 subtype-tcc nil extended_nnreal nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (lub const-decl "{x | least_upper_bound?(x, SA)}" bounded_real_defs nil) (bounded_above? const-decl "bool" bounded_real_defs nil) (least_upper_bound? const-decl "bool" bounded_real_defs nil) (nonempty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (x!1 skolem-const-decl "real" extended_nnreal nil) (X!1 skolem-const-decl "set[extended_nnreal]" extended_nnreal nil) (upper_bound? const-decl "bool" bounded_real_defs nil)) nil)) (x_sigma_TCC1 0 (x_sigma_TCC1-1 nil 3396791560 ("" (subtype-tcc) nil nil) nil nil)) (x_sum_TCC1 0 (x_sum_TCC1-1 nil 3396590282 ("" (skosimp*) (("" (lemma "limit_nonneg" ("nna" "series(LAMBDA i: S!1(i)`2)")) (("1" (assert) (("1" (expand "series") (("1" (expand "limit") (("1" (expand "limit") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "series") (("2" (hide-all-but 1) (("2" (skosimp) (("2" (lemma "sigma_ge_0" ("low" "0" "high" "x1!1" "F" "LAMBDA i: S!1(i)`2")) (("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) ((extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil) (series const-decl "sequence[real]" series "series/") (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) (limit_nonneg formula-decl nil series_lems "series/") (limit const-decl "real" convergence_sequences "analysis/") (limit macro-decl "[(convergent?) -> real]" extended_nnreal nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (sigma_ge_0 formula-decl nil sigma "reals/")) nil)) (x_sum_TCC2 0 (x_sum_TCC2-1 nil 3454502638 ("" (skosimp) (("" (lemma "limit_nonneg" ("nna" "series(U!1)")) (("1" (assert) (("1" (expand "limit" 1) (("1" (propax) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skolem + "n!1") (("2" (expand "series") (("2" (lemma "sigma_ge_0" ("low" "0" "high" "n!1" "F" "U!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((series const-decl "sequence[real]" series "series/") (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) (limit_nonneg formula-decl nil series_lems "series/") (limit macro-decl "[(convergent?) -> real]" extended_nnreal nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (sigma_ge_0 formula-decl nil sigma "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)) nil)) (x_limit_TCC1 0 (x_limit_TCC1-1 nil 3450168447 ("" (skosimp) (("" (lemma "limit_nonneg" ("nna" "LAMBDA i: S!1(i)`2")) (("" (assert) (("" (expand "limit" 1) (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((extended_nnreal nonempty-type-eq-decl nil extended_nnreal 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) (limit_nonneg formula-decl nil series_lems "series/") (limit macro-decl "[(convergent?) -> real]" extended_nnreal nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (x_add_commutative 0 (x_add_commutative-1 nil 3396582760 ("" (expand "x_add") (("" (expand "commutative?") (("" (skosimp*) (("" (grind) nil nil)) nil)) nil)) nil) ((commutative? const-decl "bool" operator_defs nil) (x_add const-decl "extended_nnreal" extended_nnreal nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (x_add_associative 0 (x_add_associative-1 nil 3396582779 ("" (expand "x_add") (("" (expand "associative?") (("" (grind) nil nil)) nil)) nil) ((associative? const-decl "bool" operator_defs nil) (x_add const-decl "extended_nnreal" extended_nnreal nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (x_times_commutative 0 (x_times_commutative-1 nil 3457152809 ("" (expand "commutative?") (("" (expand "x_times") (("" (grind) nil nil)) nil)) nil) ((x_times const-decl "extended_nnreal" extended_nnreal nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (x_eq const-decl "bool" extended_nnreal nil) (commutative? const-decl "bool" operator_defs nil)) shostak)) (x_times_associative 0 (x_times_associative-1 nil 3457152828 ("" (expand "associative?") (("" (grind) (("1" (rewrite "zero_times3") nil nil) ("2" (rewrite "zero_times3") nil nil)) nil)) nil) ((x_eq const-decl "bool" extended_nnreal nil) (x_times const-decl "extended_nnreal" extended_nnreal nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal 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) (zero_times3 formula-decl nil real_props nil) (associative? const-decl "bool" operator_defs nil)) shostak)) (x_eq_equivalence 0 (x_eq_equivalence-1 nil 3396582792 ("" (expand "x_eq") (("" (expand "equivalence?") (("" (grind) nil nil)) nil)) nil) ((equivalence? const-decl "bool" relations nil) (reflexive? const-decl "bool" relations nil) (symmetric? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (x_eq const-decl "bool" extended_nnreal nil)) shostak)) (x_le_preorder 0 (x_le_preorder-1 nil 3396582803 ("" (expand "x_le") (("" (expand "preorder?") (("" (grind) nil nil)) nil)) nil) ((preorder? const-decl "bool" orders nil) (reflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (x_le const-decl "bool" extended_nnreal nil)) shostak)) (x_le_antisymmetric 0 (x_le_antisymmetric-1 nil 3396582814 ("" (expand "x_eq") (("" (expand "x_le") (("" (grind) nil nil)) nil)) nil) ((x_le const-decl "bool" extended_nnreal nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (x_eq const-decl "bool" extended_nnreal nil)) shostak)) (x_sigma_le 0 (x_sigma_le-1 nil 3397794298 ("" (skosimp*) (("" (expand "x_sigma") (("" (expand "x_le") (("" (case-replace "FORALL i: low!1 <= i AND i <= high!1 => T!1(i)`1") (("1" (case-replace "FORALL (i_1: nat): low!1 <= i_1 AND i_1 <= high!1 => S!1(i_1)`1") (("1" (lemma "sigma_le" ("low" "low!1" "high" "high!1" "F" "LAMBDA (i_2: nat): S!1(i_2)`2" "G" "LAMBDA (i_2: nat): T!1(i_2)`2")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "n!1") (("2" (inst - "n!1") (("2" (inst - "n!1") (("2" (inst - "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst - "i!1") (("2" (inst - "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((x_sigma const-decl "extended_nnreal" extended_nnreal 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (sigma_le formula-decl nil sigma "reals/") (NOT const-decl "[bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (x_le const-decl "bool" extended_nnreal nil)) shostak)) (x_sigma_lt 0 (x_sigma_lt-1 nil 3397794729 ("" (skosimp) (("" (expand "x_sigma") (("" (expand "x_lt") (("" (case-replace "FORALL i: low!1 <= i AND i <= high!1 => T!1(i)`1") (("1" (case-replace "FORALL (i_1: nat): low!1 <= i_1 AND i_1 <= high!1 => S!1(i_1)`1") (("1" (lemma "sigma_lt" ("low" "low!1" "high" "high!1" "F" "LAMBDA (i_1: nat): S!1(i_1)`2" "G" "LAMBDA (i_1: nat): T!1(i_1)`2")) (("1" (split -1) (("1" (propax) nil nil) ("2" (propax) nil nil) ("3" (hide 2) (("3" (skosimp) (("3" (typepred "n!1") (("3" (inst - "n!1") (("3" (inst - "n!1") (("3" (inst - "n!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst - "i!1") (("2" (inst - "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((x_sigma const-decl "extended_nnreal" extended_nnreal 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (sigma_lt formula-decl nil sigma "reals/") (NOT const-decl "[bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (x_lt const-decl "bool" extended_nnreal nil)) shostak)) (x_sum_le 0 (x_sum_le-1 nil 3397795096 ("" (skosimp) (("" (expand "x_le") (("" (expand "x_sum") (("" (case-replace "(FORALL i: T!1(i)`1) AND convergent?(series(LAMBDA i: T!1(i)`2))") (("1" (case-replace "(FORALL (i_1: nat): S!1(i_1)`1) AND convergent?(series(LAMBDA (i_1: nat): S!1(i_1)`2))") (("1" (flatten) (("1" (name "F" "LAMBDA (i_2: nat): T!1(i_2)`2-S!1(i_2)`2") (("1" (case "forall i: 0<=F(i)") (("1" (case "series(F)= series(LAMBDA i: T!1(i)`2)-series(LAMBDA (i_1: nat): S!1(i_1)`2)") (("1" (lemma "convergent_diff" ("s1" "series(LAMBDA i: T!1(i)`2)" "s2" "series(LAMBDA (i_1: nat): S!1(i_1)`2)")) (("1" (replace -2 -1 rl) (("1" (assert) (("1" (lemma "limit_diff" ("v1" "series(LAMBDA i: T!1(i)`2)" "v2" "series(LAMBDA (i_1: nat): S!1(i_1)`2)")) (("1" (replace -3 -1 rl) (("1" (name-replace "L1" "convergence_sequences.limit(series(LAMBDA (i_2: nat): S!1(i_2)`2))") (("1" (name-replace "L2" "convergence_sequences.limit(series(LAMBDA (i_1: nat): T!1(i_1)`2))") (("1" (lemma "limit_nonneg" ("nna" "series(F)")) (("1" (assert) nil nil) ("2" (skolem + ("n!1")) (("2" (hide-all-but (-4 1)) (("2" (expand "series") (("2" (lemma "sigma_ge_0" ("low" "0" "high" "n!1" "F" "F")) (("2" (assert) (("2" (skosimp) (("2" (inst - "n!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "F") (("2" (rewrite "series_diff") (("2" (expand "-") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "F" 1) (("2" (inst - "i!1") (("2" (inst - "i!1") (("2" (inst - "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (skosimp) (("1" (inst - "i!1") (("1" (inst - "i!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "comparison_test" ("b" "LAMBDA i: T!1(i)`2" "a" "LAMBDA (i_1: nat): S!1(i_1)`2")) (("2" (replace -3) (("2" (split) (("1" (propax) nil nil) ("2" (hide -2 2) (("2" (skosimp) (("2" (expand "abs") (("2" (assert) (("2" (typepred "S!1(n!1)`2") (("2" (assert) (("2" (inst - "n!1") (("2" (inst - "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((x_le const-decl "bool" extended_nnreal nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil) (sequence type-eq-decl nil sequences nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (series const-decl "sequence[real]" series "series/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (NOT const-decl "[bool -> bool]" booleans nil) (comparison_test formula-decl nil series "series/") (<= const-decl "bool" reals nil) (series_diff formula-decl nil series "series/") (F skolem-const-decl "[nat -> real]" extended_nnreal nil) (convergent_diff formula-decl nil convergence_ops "analysis/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (subrange type-eq-decl nil integers nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (sigma_ge_0 formula-decl nil sigma "reals/") (limit_nonneg formula-decl nil series_lems "series/") (limit const-decl "real" convergence_sequences "analysis/") (limit_diff formula-decl nil convergence_ops "analysis/") (- const-decl "[T -> real]" real_fun_ops "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (x_sum const-decl "extended_nnreal" extended_nnreal nil)) shostak)) (x_sum_eq 0 (x_sum_eq-1 nil 3450459000 ("" (skosimp) (("" (lemma "x_sum_le" ("S" "S!1" "T" "T!1")) (("" (lemma "x_sum_le" ("S" "T!1" "T" "S!1")) (("" (split) (("1" (split) (("1" (lemma "x_le_antisymmetric" ("x" "x_sum(S!1)" "y" "x_sum(T!1)")) (("1" (assert) nil nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (skosimp) (("2" (inst - "i!1") (("2" (expand "x_le") (("2" (expand "x_eq") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (skosimp) (("2" (inst - "i!1") (("2" (expand "x_eq") (("2" (expand "x_le") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((extended_nnreal nonempty-type-eq-decl nil extended_nnreal 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) (x_sum_le formula-decl nil extended_nnreal nil) (x_eq const-decl "bool" extended_nnreal nil) (x_le const-decl "bool" extended_nnreal nil) (x_sum const-decl "extended_nnreal" extended_nnreal nil) (x_le_antisymmetric formula-decl nil extended_nnreal nil)) shostak)) (x_sum_lt 0 (x_sum_lt-1 nil 3397796467 ("" (skosimp) (("" (expand "x_sum") (("" (expand "x_lt") (("" (case-replace "(FORALL i: T!1(i)`1) AND convergent?(series(LAMBDA i: T!1(i)`2))") (("1" (flatten) (("1" (case-replace "(FORALL (i_1: nat): S!1(i_1)`1) AND convergent?(series(LAMBDA (i_1: nat): S!1(i_1)`2))") (("1" (flatten) (("1" (name "F" "series(LAMBDA (i_2: nat): T!1(i_2)`2-S!1(i_2)`2)") (("1" (case "forall i: F(i)>0") (("1" (case "series(LAMBDA (i_2: nat): T!1(i_2)`2)-series(LAMBDA (i_2: nat): S!1(i_2)`2)=F") (("1" (lemma "convergent_diff" ("s1" "series(LAMBDA (i_2: nat): T!1(i_2)`2)" "s2" "series(LAMBDA (i_2: nat): S!1(i_2)`2)")) (("1" (replace -2) (("1" (assert) (("1" (lemma "limit_diff" ("v1" "series(LAMBDA (i_2: nat): T!1(i_2)`2)" "v2" "series(LAMBDA (i_2: nat): S!1(i_2)`2)")) (("1" (replace -3 -1) (("1" (name-replace "L1" "convergence_sequences.limit(series(LAMBDA (i_1: nat): S!1(i_1)`2))") (("1" (name-replace "L2" "convergence_sequences.limit(series(LAMBDA (i_2: nat): T!1(i_2)`2))") (("1" (hide -3 -5 -7 -9) (("1" (expand "F") (("1" (lemma "limit_series_shift" ("a" "LAMBDA (i_2: nat): T!1(i_2)`2 - S!1(i_2)`2" "pn" "1")) (("1" (assert) (("1" (replace -2) (("1" (lemma "conv_series_shift" ("a" "LAMBDA (i_2: nat): T!1(i_2)`2 - S!1(i_2)`2" "N" "1")) (("1" (assert) (("1" (lemma "limit_pos" ("a" "series(LAMBDA i: T!1(1 + i)`2 - S!1(1 + i)`2)")) (("1" (replace -2) (("1" (name-replace "L3" "convergence_sequences.limit(series(LAMBDA i: T!1(1 + i)`2 - S!1(1 + i)`2))") (("1" (split -1) (("1" (expand "sigma") (("1" (inst -6 "0") (("1" (expand "series" -6) (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "series" (1 -5)) (("2" (lemma "sigma_gt_0" ("low" "0" "high" "n!1" "F" "LAMBDA (i_1: nat): T!1(1 + i_1)`2 - S!1(1 + i_1)`2")) (("2" (assert) (("2" (hide -5 2) (("2" (skosimp) (("2" (typepred "n!2") (("2" (inst - "1+n!2") (("2" (inst - "1+n!2") (("2" (inst - "1+n!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "series_diff") (("2" (expand "F") (("2" (expand "-") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide -1 -3 -5 2) (("2" (expand "F") (("2" (expand "series") (("2" (lemma "sigma_gt_0" ("low" "0" "high" "i!1" "F" "LAMBDA (i_2: nat): T!1(i_2)`2 - S!1(i_2)`2")) (("2" (assert) (("2" (hide 2) (("2" (skosimp) (("2" (typepred "n!1") (("2" (inst - "n!1") (("2" (inst - "n!1") (("2" (inst - "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (skosimp) (("1" (inst - "i!1") (("1" (inst - "i!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "comparison_test" ("a" "LAMBDA (i_1: nat): S!1(i_1)`2" "b" "LAMBDA i: T!1(i)`2")) (("2" (assert) (("2" (hide -2 2) (("2" (skosimp) (("2" (typepred "S!1(n!1)`2") (("2" (expand "abs") (("2" (assert) (("2" (inst - "n!1") (("2" (inst - "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((x_sum const-decl "extended_nnreal" extended_nnreal nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil) (sequence type-eq-decl nil sequences nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (series const-decl "sequence[real]" series "series/") (real_minus_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (limit_diff formula-decl nil convergence_ops "analysis/") (limit const-decl "real" convergence_sequences "analysis/") (limit_series_shift formula-decl nil series "series/") (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers 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) (sigma_0_neg formula-decl nil sigma_nat "reals/") (sigma def-decl "real" sigma "reals/") (sigma_gt_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/") (NOT const-decl "[bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (limit_pos formula-decl nil series "series/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (conv_series_shift formula-decl nil series "series/") (F skolem-const-decl "sequence[real]" extended_nnreal nil) (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) (convergent_diff formula-decl nil convergence_ops "analysis/") (series_diff formula-decl nil series "series/") (> const-decl "bool" reals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (comparison_test formula-decl nil series "series/") (x_lt const-decl "bool" extended_nnreal nil)) shostak)) (x_inf_le 0 (x_inf_le-1 nil 3450519245 ("" (skosimp) (("" (expand "x_inf") (("" (expand "x_le" 1) (("" (flatten) (("" (assert) (("" (expand "fullset") (("" (expand "image") (("" (expand "x_inf") (("" (prop) (("1" (skosimp) (("1" (typepred "x!1") (("1" (skosimp) (("1" (inst -4 "x!2") (("1" (expand "x_le") (("1" (assert) (("1" (flatten) (("1" (inst - "S!1(x!2)") (("1" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (skolem! 1) (("2" (lift-if) (("2" (assert) (("2" (case-replace "FORALL (x: ({y: extended_nnreal | EXISTS (x_1: ({x: nat | TRUE})): y = S!1(x_1)})): NOT x`1") (("1" (inst - "x!1") (("1" (typepred "glb({z:real | EXISTS x: (EXISTS (x_1: ({x: nat | TRUE})): x = T!1(x_1)) AND x`1 AND x`2 = z})") (("1" (name-replace "RHS" "glb({z:real | EXISTS x: (EXISTS (x_1: ({x: nat | TRUE})): x = T!1(x_1)) AND x`1 AND x`2 = z})") (("1" (expand "greatest_lower_bound?" -1) (("1" (flatten) (("1" (inst -2 "0") (("1" (assert) (("1" (expand "lower_bound?") (("1" (skosimp) (("1" (typepred "s!1") (("1" (skosimp) (("1" (skosimp) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (assert) (("2" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (typepred "x!1") (("1" (skosimp) (("1" (inst -2 "x!1`2") (("1" (inst + "x!1") (("1" (assert) (("1" (inst 1 "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "bounded_below?") (("2" (inst + "0") (("2" (expand "lower_bound?") (("2" (skosimp) (("2" (typepred "s!1") (("2" (skosimp) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (skosimp) (("2" (typepred "glb({z:real | EXISTS x: (EXISTS (x_1: ({x: nat | TRUE})): x = S!1(x_1)) AND x`1 AND x`2 = z})") (("1" (name-replace "LHS" "glb({z:real | EXISTS x: (EXISTS (x_1: ({x: nat | TRUE})): x = S!1(x_1)) AND x`1 AND x`2 = z})") (("1" (typepred "glb({z:real | EXISTS x: (EXISTS (x_1: ({x: nat | TRUE})): x = T!1(x_1)) AND x`1 AND x`2 = z})") (("1" (name-replace "RHS" "glb({z:real | EXISTS x: (EXISTS (x_1: ({x: nat | TRUE})): x = T!1(x_1)) AND x`1 AND x`2 = z})") (("1" (expand "greatest_lower_bound?") (("1" (flatten) (("1" (inst -2 "LHS") (("1" (assert) (("1" (expand "lower_bound?" 1) (("1" (skosimp) (("1" (typepred "s!1") (("1" (skosimp) (("1" (skosimp) (("1" (inst -9 "x!4") (("1" (expand "x_le" -9) (("1" (assert) (("1" (flatten) (("1" (hide -4 -6) (("1" (expand "lower_bound?") (("1" (inst - "S!1(x!4)`2") (("1" (assert) nil nil) ("2" (inst + "S!1(x!4)") (("2" (assert) (("2" (inst + "x!4") 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" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "x!1`2") (("1" (inst + "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "0") (("2" (expand "lower_bound?") (("2" (skosimp) (("2" (typepred "s!1") (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "x!2`2") (("1" (inst + "x!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "0") (("2" (expand "lower_bound?") (("2" (skosimp) (("2" (typepred "s!1") (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((x_inf const-decl "extended_nnreal" extended_nnreal nil) (fullset const-decl "set" sets nil) (x_inf const-decl "extended_nnreal" extended_nnreal nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (greatest_lower_bound? const-decl "bool" bounded_real_defs nil) (bounded_below? const-decl "bool" bounded_real_defs nil) (glb const-decl "{x | greatest_lower_bound?(x, SB)}" bounded_real_defs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (lower_bound? const-decl "bool" bounded_real_defs nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (x!1 skolem-const-decl "({y: extended_nnreal | EXISTS (x_1: ({x | TRUE})): y = T!1(x_1)})" extended_nnreal nil) (T!1 skolem-const-decl "[nat -> extended_nnreal]" extended_nnreal nil) (x!4 skolem-const-decl "({x: nat | TRUE})" extended_nnreal nil) (x!2 skolem-const-decl "({x | TRUE})" extended_nnreal nil) (S!1 skolem-const-decl "[nat -> extended_nnreal]" extended_nnreal nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (TRUE const-decl "bool" booleans nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil) (= const-decl "[T, T -> boolean]" equalities nil) (image const-decl "set[R]" function_image nil) (x_le const-decl "bool" extended_nnreal nil)) shostak)) (x_le_add 0 (x_le_add-1 nil 3453696018 ("" (skosimp) (("" (grind) nil nil)) nil) ((nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (x_add const-decl "extended_nnreal" extended_nnreal nil) (x_le const-decl "bool" extended_nnreal nil)) shostak)) (x_add_sum 0 (x_add_sum-1 nil 3453696210 ("" (skosimp) (("" (expand "x_eq") (("" (expand "x_add") (("" (expand "x_sum") (("" (lift-if) (("" (assert) (("" (case-replace "FORALL i: S!1(i)`1") (("1" (case-replace "FORALL i: T!1(i)`1") (("1" (case-replace "FORALL (i: nat): S!1(i)`1 AND T!1(i)`1") (("1" (case-replace "convergent?(series(LAMBDA i: S!1(i)`2))") (("1" (case-replace "convergent?(series(LAMBDA i: T!1(i)`2))") (("1" (lemma "convergent_sum" ("s1" "series(LAMBDA i: S!1(i)`2)" "s2" "series(LAMBDA i: T!1(i)`2)")) (("1" (assert) (("1" (lemma "limit_sum" ("v1" "series(LAMBDA i: S!1(i)`2)" "v2" "series(LAMBDA i: T!1(i)`2)")) (("1" (rewrite "series_sum") (("1" (expand "+") (("1" (case-replace "(LAMBDA (i_1: nat): IF S!1(i_1)`1 AND T!1(i_1)`1 THEN S!1(i_1)`2 + T!1(i_1)`2 ELSE 0 ENDIF)=(LAMBDA (i: nat): S!1(i)`2 + T!1(i)`2)") (("1" (replace -3) (("1" (replace -2) (("1" (propax) nil nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("2" (inst - "x!1") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (assert) (("2" (lemma "comparison_test" ("b" "(LAMBDA (i_1: nat): IF S!1(i_1)`1 AND T!1(i_1)`1 THEN S!1(i_1)`2 + T!1(i_1)`2 ELSE 0 ENDIF)" "a" "LAMBDA i: T!1(i)`2")) (("2" (assert) (("2" (skosimp) (("2" (inst - "n!1") (("2" (flatten) (("2" (assert) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (lemma "comparison_test" ("b" "(LAMBDA (i_1: nat): IF S!1(i_1)`1 AND T!1(i_1)`1 THEN S!1(i_1)`2 + T!1(i_1)`2 ELSE 0 ENDIF)" "a" "LAMBDA i: S!1(i)`2")) (("2" (assert) (("2" (hide -4 2) (("2" (skosimp) (("2" (inst - "n!1") (("2" (flatten) (("2" (assert) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "i!1") (("2" (inst - "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (assert) (("2" (flatten) (("2" (skosimp) (("2" (inst -2 "i!1") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (flatten) (("2" (skosimp) (("2" (inst - "i!1") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((x_eq const-decl "bool" extended_nnreal nil) (x_sum const-decl "extended_nnreal" extended_nnreal nil) (series const-decl "sequence[real]" series "series/") (convergent? const-decl "bool" convergence_sequences "analysis/") (sequence type-eq-decl nil sequences nil) (comparison_test formula-decl nil series "series/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (convergent_sum formula-decl nil convergence_ops "analysis/") (limit_sum formula-decl nil convergence_ops "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (series_sum formula-decl nil series "series/") (AND const-decl "[bool, bool -> bool]" booleans nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal 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) (x_add const-decl "extended_nnreal" extended_nnreal nil)) shostak)) (x_limit_to_sum 0 (x_limit_to_sum-1 nil 3456471599 ("" (skosimp) (("" (expand "x_limit") (("" (expand "x_sum") (("" (expand "x_eq") (("" (case-replace "FORALL i: S!1(i)`1") (("1" (case-replace "FORALL i: T!1(i)`1") (("1" (case-replace "series(LAMBDA i: T!1(i)`2)=LAMBDA i: S!1(i)`2") (("1" (hide 2) (("1" (apply-extensionality :hide? t) (("1" (expand "series") (("1" (inst -3 "x!1") (("1" (flatten) (("1" (inst -2 "x!1") (("1" (assert) (("1" (expand "x_sigma") (("1" (prop) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst -2 "i!1") (("2" (inst-cp - "i!1") (("2" (replace -2) (("2" (flatten) (("2" (expand "x_sigma") (("2" (prop) (("2" (inst - "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (prop) (("2" (skosimp) (("2" (inst -3 "i!1") (("2" (flatten) (("2" (assert) (("2" (hide -2 -3 1) (("2" (expand "x_sigma") (("2" (prop) (("2" (skosimp) (("2" (inst - "i!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((x_limit const-decl "extended_nnreal" extended_nnreal nil) (x_eq const-decl "bool" extended_nnreal 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/") (x_sigma const-decl "extended_nnreal" extended_nnreal nil) (series const-decl "sequence[real]" series "series/") (= const-decl "[T, T -> boolean]" equalities nil) (sequence type-eq-decl nil sequences nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal 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) (x_sum const-decl "extended_nnreal" extended_nnreal nil)) shostak)) (x_times_sum 0 (x_times_sum-1 nil 3457160189 ("" (case "FORALL (S, T: [nat -> extended_nnreal], x:nnreal): (FORALL i: x_eq(x_times(x, S(i)), T(i))) => x_eq(x_times(x, x_sum(S)), x_sum(T))") (("1" (skosimp) (("1" (expand "x_eq") (("1" (expand "x_times") (("1" (expand "x_times") (("1" (case-replace "x!1`1") (("1" (inst - "S!1" "T!1" "x!1`2") (("1" (case-replace "x!1`2 = 0") (("1" (expand "x_eq" -4 1) (("1" (assert) (("1" (expand "x_eq" -4 1) (("1" (assert) (("1" (expand "x_eq" -4 1) (("1" (replace -4 -3) (("1" (flatten) (("1" (expand "x_eq" 1 1) (("1" (expand "x_eq" 1 1) (("1" (expand "x_eq" 1 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (expand "x_eq" -3 1) (("2" (assert) (("2" (expand "x_eq" 2 1) (("2" (expand "x_eq" 2 2) (("2" (expand "x_eq" 2 3) (("2" (expand "x_eq" -3 4) (("2" (expand "x_eq" -3 2) (("2" (split) (("1" (flatten) (("1" (case-replace "x_sum(S!1)`1") (("1" (assert) nil nil) ("2" (assert) (("2" (expand "x_eq") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "i!1") (("2" (case-replace "S!1(i!1)`1") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (expand "x_eq") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "x_eq" 2 1) (("2" (expand "x_eq" 2 2) (("2" (expand "x_eq" 2 3) (("2" (assert) (("2" (expand "x_eq" -2 1) (("2" (expand "x_eq" -2 2) (("2" (expand "x_eq" -2 3) (("2" (expand "x_eq" -2) (("2" (hide -1) (("2" (case "forall i: S!1(i)`1") (("1" (case "FORALL i: S!1(i)`2 = 0") (("1" (case-replace "x_eq(x_sum(S!1), 0)") (("1" (lemma "x_sum_eq" ("S" "S!1" "T" "T!1")) (("1" (split) (("1" (expand "x_eq") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "i!1") (("2" (inst - "i!1") (("2" (inst - "i!1") (("2" (expand "x_eq") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (expand "x_eq") (("2" (expand "x_sum") (("2" (replace -2) (("2" (case-replace "(LAMBDA i: S!1(i)`2)=(lambda i: 0)") (("1" (rewrite "zero_series_conv") (("1" (rewrite "zero_series_limit") nil nil)) nil) ("2" (apply-extensionality :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (case-replace "x_eq(x_sum(S!1), 0)") (("1" (expand "x_eq" -1) (("1" (flatten) (("1" (expand "x_sum") (("1" (replace -3) (("1" (hide 3) (("1" (prop) (("1" (replace -1) (("1" (lemma "convergence_nonneg" ("nna" "LAMBDA i: S!1(i)`2" "nnx" "0")) (("1" (split) (("1" (inst - "i!1") (("1" (expand "series") (("1" (lemma "sigma_nonneg_eq_0" ("low" "0" "high" "i!1" "Fnnr" "LAMBDA i: S!1(i)`2" "i" "i!1")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (rewrite "limit_def") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (assert) (("2" (expand "x_eq" 1) (("2" (expand "x_sum" -3) (("2" (hide 1) (("2" (prop) (("2" (inst -4 "i!1") (("2" (assert) (("2" (inst - "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "x_eq(x_sum(S!1), 0)") (("1" (hide-all-but (-1 1)) (("1" (expand "x_eq") (("1" (expand "x_sum") (("1" (flatten) (("1" (replace 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (assert) (("2" (expand "x_sum") (("2" (hide 1) (("2" (prop) (("2" (skosimp) (("2" (inst - "i!1") (("2" (inst - "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "x_times") (("2" (expand "x_times") (("2" (expand "x_eq") (("2" (case-replace "x!1=0") (("1" (lemma "x_sum_eq" ("S" "lambda i: (TRUE,0)" "T" "T!1")) (("1" (split) (("1" (expand "x_eq") (("1" (flatten) (("1" (expand "x_sum" -1 1) (("1" (expand "x_sum" -2 1) (("1" (expand "x_sum" -2 1) (("1" (rewrite "zero_series_conv") (("1" (assert) (("1" (rewrite "zero_series_limit") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst - "i!1") (("2" (flatten) (("2" (expand "x_eq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "forall i: S!1(i)`1") (("1" (expand "x_sum") (("1" (replace -1) (("1" (case-replace "FORALL i: T!1(i)`1") (("1" (case "forall i: S!1(i)`2 * x!1=T!1(i)`2") (("1" (hide -4) (("1" (case-replace "convergent?(series(LAMBDA i: S!1(i)`2))") (("1" (case-replace "convergent?(series(LAMBDA i: T!1(i)`2))") (("1" (lemma "limit_scal" ("a" "x!1" "v1" "series(LAMBDA i: S!1(i)`2)")) (("1" (rewrite "series_scal") (("1" (case-replace "(LAMBDA i: x!1 * S!1(i)`2)=(LAMBDA i: T!1(i)`2)") (("1" (assert) nil nil) ("2" (apply-extensionality :hide? t) (("2" (inst -4 "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (lemma "convergent_scal" ("s1" "series(LAMBDA i: S!1(i)`2)" "a" "x!1")) (("2" (assert) (("2" (rewrite "series_scal") (("2" (case-replace "(LAMBDA i: x!1 * S!1(i)`2)=(LAMBDA i: T!1(i)`2)") (("2" (apply-extensionality :hide? t) (("2" (inst -3 "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (assert) (("2" (prop) (("2" (lemma "convergent_scal" ("s1" "series(LAMBDA i: T!1(i)`2)" "a" "1/x!1")) (("2" (assert) (("2" (rewrite "series_scal" -1) (("2" (case-replace "(LAMBDA i: 1 / x!1 * T!1(i)`2)=(LAMBDA i: S!1(i)`2)") (("2" (apply-extensionality :hide? t) (("2" (inst -3 "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (skosimp) (("2" (inst - "i!1") (("2" (inst - "i!1") (("2" (inst - "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (skosimp) (("2" (inst - "i!1") (("2" (inst - "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "x_sum") (("2" (replace 1) (("2" (assert) (("2" (prop) (("2" (skosimp) (("2" (inst - "i!1") (("2" (inst - "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (series_scal formula-decl nil series "series/") (real_times_real_is_real application-judgement "real" reals nil) (limit_scal formula-decl nil convergence_ops "analysis/") (convergent_scal formula-decl nil convergence_ops "analysis/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (TRUE const-decl "bool" booleans nil) (x_times const-decl "extended_nnreal" extended_nnreal nil) (= const-decl "[T, T -> boolean]" equalities nil) (x_eq const-decl "bool" extended_nnreal nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (series const-decl "sequence[real]" series "series/") (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) (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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sigma_nonneg_eq_0 formula-decl nil sigma "reals/") (limit_def formula-decl nil convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (sequence type-eq-decl nil sequences nil) (convergence_nonneg formula-decl nil series_lems "series/") (x_sum_eq formula-decl nil extended_nnreal nil) (zero_series_conv formula-decl nil series "series/") (zero_series_limit formula-decl nil series "series/") (x_times const-decl "extended_nnreal" extended_nnreal 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) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (x_eq const-decl "bool" extended_nnreal nil) (x_times const-decl "extended_nnreal" extended_nnreal nil) (x_sum const-decl "extended_nnreal" extended_nnreal nil)) shostak)) (epsilon_x_le 0 (epsilon_x_le-1 nil 3453694470 ("" (skosimp) (("" (split) (("1" (grind) nil nil) ("2" (flatten) (("2" (expand "x_add") (("2" (expand "x_le") (("2" (flatten) (("2" (replace -2) (("2" (inst-cp - "1") (("2" (flatten) (("2" (assert) (("2" (hide -3) (("2" (lemma "varying_epsilon" ("x" "x!1`2" "y" "y!1`2")) (("2" (replace -1) (("2" (skosimp) (("2" (inst -3 "epsilon!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (x_add const-decl "extended_nnreal" extended_nnreal nil) (x_le const-decl "bool" extended_nnreal 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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types 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) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (varying_epsilon formula-decl nil epsilon_lemmas "analysis/") (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil)) shostak)) (double_x_sum 0 (double_x_sum-1 nil 3408435224 ("" (skosimp) (("" (expand "x_eq") (("" (expand "x_sum") (("" (case-replace "FORALL i: single_index(U!1)(i)`1") (("1" (case-replace "convergent?(series(LAMBDA i: single_index(U!1)(i)`2))") (("1" (case-replace "(FORALL (i_1: nat): IF (FORALL (i_2: nat): U!1(i_1, i_2)`1) AND convergent?(series(LAMBDA (i_2: nat): U!1(i_1, i_2)`2)) THEN TRUE ELSE FALSE ENDIF) AND convergent?(series(LAMBDA (i_1: nat): IF (FORALL (i_2: nat): U!1(i_1, i_2)`1) AND convergent?(series (LAMBDA (i_2: nat): U!1(i_1, i_2)`2)) THEN convergence_sequences.limit (series (LAMBDA (i_2: nat): U!1(i_1, i_2)`2)) ELSE 0 ENDIF))") (("1" (flatten) (("1" (lemma "double_left_limit" ("u" "lambda (i,j): U!1(i,j)`2")) (("1" (expand "single_index") (("1" (replace -4) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "(LAMBDA (i_1: nat): IF (FORALL (i_2: nat): U!1(i_1, i_2)`1) AND convergent?(series (LAMBDA (i_2: nat): U!1(i_1, i_2)`2)) THEN convergence_sequences.limit (series(LAMBDA (i_2: nat): U!1(i_1, i_2)`2)) ELSE 0 ENDIF)=(LAMBDA (i_1: nat): limit(series(LAMBDA (j_1: nat): U!1(i_1, j_1)`2)))") (("1" (hide 2) (("1" (apply-extensionality :hide? t) (("1" (inst - "x!1") (("1" (prop) (("1" (replace -1) (("1" (replace -2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "i!1") (("2" (prop) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (skosimp) (("2" (inst - "i!1") (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case-replace "(FORALL (i_1: nat): IF (FORALL (i_2: nat): U!1(i_1, i_2)`1) AND convergent?(series(LAMBDA (i_2: nat): U!1(i_1, i_2)`2)) THEN TRUE ELSE FALSE ENDIF)") (("1" (lemma "double_left_convergent" ("u" "lambda (i,j): U!1(i,j)`2")) (("1" (flatten) (("1" (hide -2) (("1" (split -1) (("1" (flatten) (("1" (case-replace "(LAMBDA (i_1: nat): IF (FORALL (i_2: nat): U!1(i_1, i_2)`1) AND convergent?(series (LAMBDA (i_2: nat): U!1(i_1, i_2)`2)) THEN convergence_sequences.limit (series (LAMBDA (i_2: nat): U!1(i_1, i_2)`2)) ELSE 0 ENDIF)=(LAMBDA (i_1: nat): limit(series(LAMBDA (j_1: nat): (LAMBDA (i, j): U!1(i, j)`2) (i_1, j_1))))") (("1" (assert) nil nil) ("2" (apply-extensionality 1 :hide? t) (("2" (hide 2) (("2" (inst -3 "x!1") (("2" (prop) (("2" (replace -1) (("2" (replace -2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (inst -3 "i!1") (("3" (prop) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -1) (("2" (expand "single_index") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (prop) (("1" (skosimp) (("1" (hide -1) (("1" (expand "single_index") (("1" (lemma "double_index_ij_n" ("i" "i!1" "j" "i!2")) (("1" (flatten) (("1" (inst - "double_index_n(i!1, i!2)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "double_subseq_convergent" ("u" "lambda (i,j): U!1(i,j)`2" "i" "i!1")) (("2" (split -1) (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "single_index") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (prop) (("2" (lemma "double_left_convergent") (("2" (inst - "lambda (i,j): U!1(i,j)`2") (("2" (expand "single_index" 1) (("2" (expand "single_index" -1 1) (("2" (replace -1 1) (("2" (hide -1) (("2" (split 1) (("1" (skosimp) (("1" (inst - "i!1") (("1" (prop) nil nil)) nil)) nil) ("2" (case-replace "(LAMBDA (i_1: nat): IF (FORALL (i_2: nat): U!1(i_1, i_2)`1) AND convergent?(series (LAMBDA (i_2: nat): U!1(i_1, i_2)`2)) THEN convergence_sequences.limit (series (LAMBDA (i_2: nat): U!1(i_1, i_2)`2)) ELSE 0 ENDIF)=(LAMBDA (i_1: nat): convergence_sequences.limit(series(LAMBDA (j_1: nat): U!1(i_1, j_1)`2)))") (("1" (apply-extensionality 1 :hide? t) (("1" (hide 2) (("1" (inst - "x!1") (("1" (prop) (("1" (replace -1) (("1" (replace -2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "i!1") (("2" (prop) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "i!1") (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (prop) (("2" (skosimp) (("2" (expand "single_index") (("2" (inst - "double_index_i(i!1)") (("2" (prop) (("2" (inst - "double_index_j(i!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((x_eq const-decl "bool" extended_nnreal 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) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil) (single_index const-decl "[nat -> T]" double_index nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (TRUE const-decl "bool" booleans nil) (FALSE const-decl "bool" booleans nil) (limit const-decl "real" convergence_sequences "analysis/") (double_left_limit formula-decl nil double_nn_sequence nil) (U!1 skolem-const-decl "[[nat, nat] -> extended_nnreal]" extended_nnreal nil) (= const-decl "[T, T -> boolean]" equalities nil) (double_left_convergent formula-decl nil double_nn_sequence nil) (double_subseq_convergent formula-decl nil double_nn_sequence nil) (double_index_n const-decl "nat" code_product nil) (double_index_ij_n formula-decl nil code_product nil) (series const-decl "sequence[real]" series "series/") (convergent? const-decl "bool" convergence_sequences "analysis/") (sequence type-eq-decl nil sequences nil) (double_index_i const-decl "nat" code_product nil) (double_index_j const-decl "nat" code_product nil) (x_sum const-decl "extended_nnreal" extended_nnreal nil)) shostak)) (double_x_sum_eq 0 (double_x_sum_eq-1 nil 3450440513 ("" (skosimp) (("" (lemma "double_x_sum" ("U" "U!1")) (("" (name-replace "LHS" "x_sum(LAMBDA i: x_sum(LAMBDA j: U!1(i, j)))") (("" (lemma "double_x_sum" ("U" "lambda i,j: U!1(j,i)")) (("" (assert) (("" (name-replace "RHS" "x_sum(LAMBDA j: x_sum(LAMBDA i: U!1(i, j)))") (("" (case "x_eq(x_sum(single_index(U!1)),x_sum(single_index(LAMBDA i, j: U!1(j, i))))") (("1" (expand "x_eq") (("1" (flatten) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (case "forall i,j: U!1(i, j)`1") (("1" (expand "x_sum") (("1" (case-replace "FORALL i: single_index(U!1)(i)`1") (("1" (case-replace "FORALL (i_1: nat): single_index(LAMBDA i, j: U!1(j, i))(i_1)`1") (("1" (lemma "double_right_convergent" ("u" "lambda i,j: U!1(i,j)`2")) (("1" (expand "single_index" (-1 1)) (("1" (replace -1 1 rl) (("1" (case-replace "convergent?(series(LAMBDA i: U!1(double_index_i(i), double_index_j(i))`2))") (("1" (assert) (("1" (expand "x_eq" 1) (("1" (lemma "double_right_limit" ("u" "lambda i,j: U!1(i,j)`2")) (("1" (expand "single_index") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide-all-but 3) (("2" (expand "x_eq") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (skosimp) (("2" (expand "single_index") (("2" (inst - "double_index_j(i!1)" "double_index_i(i!1)") nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "single_index") (("2" (inst - "double_index_i(i!1)" "double_index_j(i!1)") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "x_sum") (("2" (expand "x_eq") (("2" (case-replace "FORALL i: single_index(U!1)(i)`1") (("1" (assert) (("1" (hide 2) (("1" (lemma "double_single" ("u" "U!1")) (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (expand "double_index") (("1" (expand "o ") (("1" (inst - "double_index_n(i!1, j!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 3) (("2" (assert) (("2" (prop) (("2" (hide -2 2) (("2" (skosimp) (("2" (expand "single_index") (("2" (inst - "double_index_n(double_index_j(i!2),double_index_i(i!2))") (("2" (lemma "double_index_ij_n" ("i" "double_index_j(i!2)" "j" "double_index_i(i!2)")) (("2" (flatten) (("2" (replace -1) (("2" (replace -2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((extended_nnreal nonempty-type-eq-decl nil extended_nnreal 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_x_sum formula-decl nil extended_nnreal nil) (double_index_ij_n formula-decl nil code_product nil) (double_single formula-decl nil double_index nil) (O const-decl "T3" function_props nil) (double_index_n const-decl "nat" code_product nil) (double_index const-decl "[[nat, nat] -> T]" double_index nil) (double_index_j const-decl "nat" code_product nil) (double_index_i const-decl "nat" code_product nil) (series const-decl "sequence[real]" series "series/") (convergent? const-decl "bool" convergence_sequences "analysis/") (sequence type-eq-decl nil sequences nil) (double_right_limit formula-decl nil double_nn_sequence nil) (double_right_convergent formula-decl nil double_nn_sequence nil) (x_eq const-decl "bool" extended_nnreal nil) (single_index const-decl "[nat -> T]" double_index nil) (x_sum const-decl "extended_nnreal" extended_nnreal nil) (= const-decl "[T, T -> boolean]" equalities nil)) shostak)))
¤ Dauer der Verarbeitung: 0.86 Sekunden (vorverarbeitet am 2026-04-29) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26