| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 MB |
|
Quelle integral_prep.prfSprache: Lisp |
|||||||||||||||
|
(integral_prep (IMP_integral_def_TCC1 0 (IMP_integral_def_TCC1-1 nil 3253532115 ("" (skosimp*) (("" (lemma "connected_domain") (("" (inst?) (("" (assert) (("" (inst -1 "y!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((connected_domain formula-decl nil integral_prep nil)) nil)) (IMP_integral_def_TCC2 0 (IMP_integral_def_TCC2-1 nil 3253532115 ("" (skosimp*) (("" (lemma "not_one_element") (("" (inst?) nil nil)) nil)) nil) ((not_one_element formula-decl nil integral_prep nil)) nil)) (integral_const_fun 0 (integral_const_fun-1 nil 3253532115 ("" (skosimp*) (("" (rewrite "integral_def") (("" (expand "integral?") (("" (skosimp*) (("" (auto-rewrite "Rie_sum") (("" (inst + "1") (("" (skosimp*) (("" (case-replace "R!1 = D!1*(b!1-a!1)") (("1" (assert) (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "R!1") (("2" (expand "Riemann_sum?") (("2" (skosimp*) (("2" (replace -1) (("2" (hide -1) (("2" (assert) (("1" (expand "const_fun") (("1" (case "FORALL (n: below(length(P!1))): n > 0 IMPLIES sigma[below(length(P!1) - 1)] (0, n-1, LAMBDA ( (("1" (inst -1 "length(P!1)-1") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "n" 1 "below_induction[length(P!1)]") (("1" (assert) nil nil) ("2" (skosimp*) (("2" (assert) (("1" (case-replace "jb!1 = 0") (("1" (hide -3) (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("1" (expand "sigma" 2) (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (integral_def formula-decl nil integral_def nil) (const_fun 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) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (T_pred const-decl "[real -> boolean]" integral_prep nil) (T formal-subtype-decl nil integral_prep nil) (real_minus_real_is_real application-judgement "real" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Riemann_sum? const-decl "bool" integral_def nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (partition type-eq-decl nil integral_def nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (sigma_0_neg formula-decl nil sigma_below "reals/") (below_induction formula-decl nil bounded_nat_inductions nil) (pred type-eq-decl nil defined_types nil) (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_prep nil) (b!1 skolem-const-decl "T" integral_prep nil) (a!1 skolem-const-decl "T" integral_prep nil) (integer nonempty-type-from-decl nil integers 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (Rie_sum const-decl "real" integral_def nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (integral? const-decl "bool" integral_def nil)) nil)) (integral_const_restrict 0 (integral_const_restrict-3 nil 3278176127 ("" (skosimp*) (("" (lemma "integral_const_fun") (("" (inst?) (("" (assert) (("" (flatten) (("" (typepred "integral(a!1, b!1, const_fun[T](D!1))") (("1" (expand "integral?") (("1" (skosimp*) (("1" (inst -1 "epsi!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (replace -3) (("1" (typepred "R!1") (("1" (inst -2 "R!1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "Riemann_sum?") (("2" (auto-rewrite "Rie_sum") (("2" (skosimp*) (("2" (assert) (("2" (inst + "xis!1") (("2" (replace -1) (("2" (hide -1) (("2" (assert) (("2" (expand "const_fun") (("2" (rewrite "sigma_restrict_eq[below(length(P!1) - 1)]") (("1" (hide 2) (("1" (expand "restrict") (("1" (apply-extensionality 1 :hide? t) (("1" (inst?) (("1" (assert) nil nil) ("2" (hide 2) (("2" (typepred "P!1") (("2" (typepred "xis!1") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "xis!1") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide 2) (("2" (typepred "xis!1") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (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" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((integral_const_fun formula-decl nil integral_prep nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (integral const-decl "{S: real | integral?(a, b, ff, S)}" integral_def nil) (integrable? const-decl "bool" integral_def nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (integral? const-decl "bool" integral_def nil) (< const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (Riemann_sum? const-decl "bool" integral_def nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (Rie_sum const-decl "real" integral_def nil) (integer nonempty-type-from-decl nil integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma_restrict_eq formula-decl nil sigma "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (restrict const-decl "[T -> real]" sigma "reals/") (xis? const-decl "bool" integral_def nil) (int_minus_int_is_int application-judgement "int" integers nil) (R!1 skolem-const-decl "(Riemann_sum?(a!1, b!1, P!1, f!1))" integral_prep nil) (f!1 skolem-const-decl "[T -> real]" integral_prep nil) (D!1 skolem-const-decl "real" integral_prep nil) (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_prep nil) (b!1 skolem-const-decl "T" integral_prep nil) (a!1 skolem-const-decl "T" integral_prep nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (T formal-subtype-decl nil integral_prep nil) (T_pred const-decl "[real -> boolean]" integral_prep nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil) (integral_const_restrict-2 nil 3277741047 ("" (skosimp*) (("" (lemma "integral_const_fun") (("" (inst?) (("" (assert) (("" (flatten) (("" (typepred "integral(a!1, b!1, const_fun[T](D!1))") (("1" (expand "integral?") (("1" (skosimp*) (("1" (inst -1 "epsi!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (replace -3) (("1" (typepred "R!1") (("1" (inst -2 "R!1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "Riemann_sum?") (("2" (skosimp*) (("2" (assert) (("2" (inst + "xis!1") (("2" (replace -1) (("2" (hide -1) (("2" (assert) (("2" (expand "const_fun") (("2" (rewrite "sigma_restrict_eq[below(length(P!1) - 1)]") (("1" (hide 2) (("1" (expand "restrict") (("1" (apply-extensionality 1 :hide? t) (("1" (inst?) (("1" (assert) nil nil) ("2" (hide 2) (("2" (typepred "P!1") (("2" (typepred "xis!1") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "xis!1") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide 2) (("2" (typepred "xis!1") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (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) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((x_in const-decl "{t: T | aa <= t AND t <= bb}" integral_def nil) (integral const-decl "{S: real | integral?(a, b, ff, S)}" integral_def nil) (integrable? const-decl "bool" integral_def nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (integral? const-decl "bool" integral_def nil) (Riemann_sum? const-decl "bool" integral_def nil) (xis? const-decl "bool" integral_def nil) (restrict const-decl "[T -> real]" sigma "reals/") (sigma_restrict_eq formula-decl nil sigma "reals/") (partition type-eq-decl nil integral_def nil)) nil) (integral_const_restrict-1 nil 3253532115 ("" (skosimp*) (("" (lemma "integral_const_fun") (("" (inst?) (("" (assert) (("" (flatten) (("" (typepred "integral(a!1, b!1, const_fun[T](D!1))") (("1" (expand "is_integral") (("1" (skosimp*) (("1" (inst -1 "epsi!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (replace -3) (("1" (hide -3) (("1" (case-replace "Riemann_sum(a!1, b!1, P!1, f!1) = Riemann_sum(a!1, b!1, P!1, const_fun[T](D!1))") (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (expand "Riemann_sum") (("2" (rewrite "sigma_restrict_eq") (("1" (hide 2) (("1" (expand "restrict") (("1" (apply-extensionality 1 :hide? t) (("1" (lift-if) (("1" (ground) (("1" (expand "const_fun") (("1" (inst?) (("1" (replace -3) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "P!1") (("2" (inst - "i!1-1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (typepred "P!1") (("2" (inst - "n!1-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (skosimp*) (("4" (ground) nil 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)) nil)) nil) ((integral const-decl "{S: real | integral?(a, b, ff, S)}" integral_def nil) (integrable? const-decl "bool" integral_def nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (x_in const-decl "{t: T | aa <= t AND t <= bb}" integral_def nil) (sigma_restrict_eq formula-decl nil sigma "reals/") (restrict const-decl "[T -> real]" sigma "reals/") (partition type-eq-decl nil integral_def nil)) nil)) (integral_scal 0 (integral_scal-3 nil 3280253820 ("" (skosimp*) (("" (case-replace "D!1 = 0") (("1" (assert) (("1" (expand "*") (("1" (lemma "integral_const_fun") (("1" (inst - "0" "a!1" "b!1") (("1" (expand "const_fun") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "integral_def") (("2" (typepred "integral(a!1, b!1, f!1)") (("1" (expand "integral?") (("1" (skosimp*) (("1" (inst -1 "epsi!1/abs(D!1)") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (typepred "R!1") (("1" (expand "Riemann_sum?") (("1" (auto-rewrite "Rie_sum") (("1" (assert) (("1" (skosimp*) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "Rie_sum(a!1, b!1, P!1, xis!1, D!1 * f!1) = D!1*Rie_sum(a!1, b!1, P!1, xis!1, f!1)") (("1" (expand "Rie_sum") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (inst - "sigma[below(length(P!1) - 1)] (0, length(P!1) - 2, LAMBDA (n: below(length(P!1) - 1)): P!1`seq(1 + n) * f!1(xis!1(n)) - P!1`seq(n) * f!1(xis!1(n)))") (("1" (cross-mult -1) (("1" (assert) (("1" (split -1) (("1" (flatten) (("1" (rewrite "abs_mult " :dir rl) (("1" (assert) nil nil) ("2" (hide 3) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (hide-all-but (1 2)) (("2" (expand "abs") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (hide-all-but (1 2)) (("3" (grind) nil nil)) nil)) nil) ("2" (hide 3) (("2" (expand "Riemann_sum?") (("2" (assert) (("2" (inst + "xis!1") nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide 2) (("2" (expand "Rie_sum") (("2" (assert) (("2" (lemma "sigma_scal[below(length(P!1) - 1)]") (("1" (inst?) (("1" (assert) (("1" (expand "*") (("1" (assert) nil nil)) nil)) nil)) nil) ("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) ("2" (hide 3) (("2" (assert) (("2" (case "epsi!1 / abs(D!1) > 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -2) (("2" (cross-mult 1) (("1" (grind) nil nil) ("2" (assert) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (hide -2 3) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (T formal-subtype-decl nil integral_prep nil) (T_pred const-decl "[real -> boolean]" integral_prep nil) (real_times_real_is_real application-judgement "real" reals nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (integral_const_fun formula-decl nil integral_prep nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (Rie_sum const-decl "real" integral_def nil) (xis? const-decl "bool" integral_def nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (div_mult_pos_neg_lt2 formula-decl nil extra_real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (abs_mult formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (xis!1 skolem-const-decl "(xis?(a!1, b!1, P!1))" integral_prep 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) (f!1 skolem-const-decl "[T -> real]" integral_prep nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_prep nil) (b!1 skolem-const-decl "T" integral_prep nil) (a!1 skolem-const-decl "T" integral_prep nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (sigma_scal formula-decl nil sigma "reals/") (Riemann_sum? const-decl "bool" integral_def nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (epsi!1 skolem-const-decl "posreal" integral_prep nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (D!1 skolem-const-decl "real" integral_prep nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" 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) (real_minus_real_is_real application-judgement "real" reals nil) (integral const-decl "{S: real | integral?(a, b, ff, S)}" integral_def nil) (integral? const-decl "bool" integral_def nil) (integrable? const-decl "bool" integral_def nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (integral_def formula-decl nil integral_def nil)) nil) (integral_scal-2 nil 3278176311 ("" (skosimp*) (("" (case-replace "D!1 = 0") (("1" (assert) (("1" (expand "*") (("1" (lemma "integral_const_fun") (("1" (inst - "0" "a!1" "b!1") (("1" (expand "const_fun") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "integral_def") (("2" (typepred "integral(a!1, b!1, f!1)") (("1" (expand "integral?") (("1" (skosimp*) (("1" (inst -1 "epsi!1/abs(D!1)") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (typepred "R!1") (("1" (expand "Riemann_sum?") (("1" (auto-rewrite "Rie_sum") (("1" (assert) (("1" (skosimp*) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "Rie_sum(a!1, b!1, P!1, xis!1, D!1 * f!1) = D!1*Rie_sum(a!1, b!1, P!1, xis!1, f!1)") (("1" (expand "Rie_sum") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (inst - "sigma[below(length(P!1) - 1)] (0, length(P!1) - 2, LAMBDA (n: below(length(P!1) - 1)): P!1`seq(1 + n) * f!1(xis!1`seq(n)) - P!1`seq(n) * f!1(xis!1`seq(n)))") (("1" (cross-mult -1) (("1" (assert) (("1" (split -1) (("1" (flatten) (("1" (rewrite "abs_mult " :dir rl) (("1" (assert) nil nil) ("2" (hide 3) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) (("3" (typepred "xis!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (hide-all-but (1 2)) (("2" (expand "abs") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) (("3" (typepred "xis!1") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (hide-all-but (1 2)) (("4" (expand "abs") (("4" (lift-if) (("4" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (expand "Riemann_sum?") (("2" (assert) (("2" (inst + "xis!1") nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) (("4" (typepred "xis!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide 2) (("2" (expand "Rie_sum") (("2" (assert) (("2" (lemma "sigma_scal[below(length(P!1) - 1)]") (("1" (inst?) (("1" (assert) (("1" (expand "*") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (typepred "xis!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("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) ("2" (hide 3) (("2" (assert) (("2" (case "epsi!1 / abs(D!1) > 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -2) (("2" (cross-mult 1) (("1" (grind) nil nil) ("2" (assert) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (hide -2 3) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil) ((const_fun const-decl "[T -> real]" real_fun_ops "reals/") (width const-decl "posreal" integral_def nil) (Rie_sum const-decl "real" integral_def nil) (xis? const-decl "bool" integral_def nil) (sigma def-decl "real" sigma "reals/") (sigma_scal formula-decl nil sigma "reals/") (Riemann_sum? const-decl "bool" integral_def nil) (partition type-eq-decl nil integral_def nil) (integral const-decl "{S: real | integral?(a, b, ff, S)}" integral_def nil) (integral? const-decl "bool" integral_def nil) (integrable? const-decl "bool" integral_def nil) (integral_def formula-decl nil integral_def nil)) nil) (integral_scal-1 nil 3253532115 ("" (skosimp*) (("" (case-replace "D!1 = 0") (("1" (assert) (("1" (expand "*") (("1" (lemma "integral_const_fun") (("1" (inst - "0" "a!1" "b!1") (("1" (expand "const_fun") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "integral_def") (("2" (typepred "integral(a!1, b!1, f!1)") (("1" (expand "integral?") (("1" (skosimp*) (("1" (inst -1 "epsi!1/abs(D!1)") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (typepred "R!1") (("1" (expand "Riemann_sum?") (("1" (assert) (("1" (skosimp*) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "Rie_sum(a!1, b!1, P!1, xis!1, D!1 * f!1) = D!1*Rie_sum(a!1, b!1, P!1, xis!1, f!1)") (("1" (expand "Rie_sum") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (inst - "sigma[below(length(P!1) - 1)] (0, length(P!1) - 2, LAMBDA (n: below(length(P!1) - 1)): P!1`seq(1 + n) * f!1(xis!1`seq(n)) - P!1`seq(n) * f!1(xis!1`seq(n)))") (("1" (cross-mult -1) (("1" (assert) (("1" (split -1) (("1" (flatten) (("1" (rewrite "abs_mult " :dir rl) (("1" (assert) nil nil) ("2" (hide 3) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) (("3" (typepred "xis!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) (("3" (typepred "xis!1") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (hide-all-but (1 2)) (("4" (expand "abs") (("4" (lift-if) (("4" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (expand "Riemann_sum?") (("2" (assert) (("2" (inst + "xis!1") nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) (("4" (typepred "xis!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide 2) (("2" (expand "Rie_sum") (("2" (assert) (("2" (lemma "sigma_scal[below(length(P!1) - 1)]") (("1" (inst?) (("1" (assert) (("1" (expand "*") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (typepred "xis!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (assert) (("2" (case "epsi!1 / abs(D!1) > 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -2) (("2" (cross-mult 1) (("1" (grind) nil nil) ("2" (assert) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (hide -2 3) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil) ((x_in const-decl "{t: T | aa <= t AND t <= bb}" integral_def nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (width const-decl "posreal" integral_def nil) (sigma_scal formula-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (Rie_sum const-decl "real" integral_def nil) (xis? const-decl "bool" integral_def nil) (Riemann_sum? const-decl "bool" integral_def nil) (partition type-eq-decl nil integral_def nil) (integral const-decl "{S: real | integral?(a, b, ff, S)}" integral_def nil) (integral? const-decl "bool" integral_def nil) (integrable? const-decl "bool" integral_def nil) (integral_def formula-decl nil integral_def nil)) nil)) (integral_sum 0 (integral_sum-1 nil 3253532115 ("" (skosimp*) (("" (rewrite "integral_def") (("" (typepred "integral(a!1, b!1, f!1)") (("1" (typepred "integral(a!1, b!1, g!1)") (("1" (name-replace "I1" "integral(a!1, b!1, f!1)") (("1" (name-replace "I2" "integral(a!1, b!1, g!1)") (("1" (expand "integral?") (("1" (skosimp*) (("1" (inst -1 "epsi!1/2") (("1" (inst - "epsi!1/2") (("1" (skosimp*) (("1" (inst + "min(delta!1,delta!2)") (("1" (skosimp*) (("1" (inst - "P!1") (("1" (inst - "P!1") (("1" (split -1) (("1" (split -2) (("1" (hide -4 -5 -6) (("1" (typepred "R!1") (("1" (expand "Riemann_sum?") (("1" (skosimp*) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "Rie_sum(a!1, b!1, P!1, xis!1, LAMBDA x: f!1(x) + g!1(x)) = Rie_sum(a!1, b!1, P!1, xis!1, f!1) (("1" (hide -1) (("1" (inst - "Rie_sum(a!1, b!1, P!1, xis!1, f!1)") (("1" (inst - "Rie_sum(a!1, b!1, P!1, xis!1, g!1)") (("1" (lemma "triangle") (("1" (inst -1 "I1 - Rie_sum(a!1, b!1, P!1, xis!1, f!1)" "I2 - Rie_sum(a!1, b!1, P!1, xis!1, g!1)") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "Riemann_sum?") (("2" (inst?) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "Riemann_sum?") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1 -2) (("2" (expand "Rie_sum") (("2" (assert) (("2" (lemma "sigma_sum[below(length(P!1) - 1)]") (("1" (inst?) (("1" (assert) nil nil) ("2" (hide 2) (("2" (skosimp*) (("2" (typepred "xis!1") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) 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) ("2" (hide -1 -2 -3 -4 2) (("2" (expand "min") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 2) (("2" (expand "min") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (assert) (("2" (expand "min") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (integral_def formula-decl nil integral_def nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (integrable? const-decl "bool" integral_def nil) (integral? const-decl "bool" integral_def nil) (integral const-decl "{S: real | integral?(a, b, ff, S)}" integral_def 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) (T_pred const-decl "[real -> boolean]" integral_prep nil) (T formal-subtype-decl nil integral_prep nil) (posreal_min application-judgement "{z: posreal | z <= x AND z <= y}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (partition type-eq-decl nil integral_def nil) (below 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (Rie_sum const-decl "real" integral_def nil) (xis? const-decl "bool" integral_def nil) (a!1 skolem-const-decl "T" integral_prep nil) (b!1 skolem-const-decl "T" integral_prep nil) (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_prep nil) (f!1 skolem-const-decl "[T -> real]" integral_prep nil) (xis!1 skolem-const-decl "(xis?(a!1, b!1, P!1))" integral_prep nil) (triangle formula-decl nil real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (g!1 skolem-const-decl "[T -> real]" integral_prep nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (integer nonempty-type-from-decl nil integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sigma_sum formula-decl nil sigma "reals/") (real_times_real_is_real application-judgement "real" reals nil) (Riemann_sum? const-decl "bool" integral_def 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) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (NOT const-decl "[bool -> bool]" booleans nil)) nil)) (integral?_sum 0 (integral?_sum-1 nil 3278177576 ("" (skosimp*) (("" (lemma "integral_sum") (("" (inst?) (("" (inst?) (("" (assert) (("" (lemma "integral_def") (("" (inst - "a!1" "b!1" "f!1" "v1!1") (("" (assert) (("" (lemma "integral_def") (("" (inst - "a!1" "b!1" "g!1" "v2!1") (("" (assert) (("" (flatten) (("" (assert) (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((integral_sum formula-decl nil integral_prep nil) (integral_def formula-decl nil integral_def nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (T formal-subtype-decl nil integral_prep nil) (T_pred const-decl "[real -> boolean]" integral_prep nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (integral_diff 0 (integral_diff-1 nil 3253532115 ("" (skosimp*) (("" (lemma "integral_sum") (("" (inst -1 "a!1" "b!1" "f!1" "-g!1") (("" (assert) (("" (split -1) (("1" (flatten) (("1" (assert) (("1" (expand "-") (("1" (assert) (("1" (assert) (("1" (replace -2) (("1" (assert) (("1" (lemma "integral_scal") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (case-replace "(LAMBDA (x: T): -g!1(x)) = -1 * g!1") (("1" (assert) nil nil) ("2" (apply-extensionality 1 :hide? t) (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "integral_scal") (("2" (inst -1 "-1" "a!1" "b!1" "g!1") (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (case-replace "-g!1 = -1*g!1") (("2" (apply-extensionality 1 :hide? t) (("2" (expand "*") (("2" (assert) (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((integral_sum formula-decl nil integral_prep nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (real_times_real_is_real application-judgement "real" reals nil) (integral_scal formula-decl nil integral_prep nil) (real_plus_real_is_real application-judgement "real" reals nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (T formal-subtype-decl nil integral_prep nil) (T_pred const-decl "[real -> boolean]" integral_prep nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (integral_ge_0 0 (integral_ge_0-1 nil 3253532115 ("" (skosimp*) (("" (typepred "integral(a!1, b!1, f!1)") (("" (expand "integral?") (("" (case "FORALL (eps: posreal): integral(a!1, b!1, f!1) >= -eps") (("1" (hide -2 -3 -5) (("1" (inst -1 "-integral(a!1, b!1, f!1)/2") (("1" (assert) nil nil) ("2" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (inst -1 "eps!1") (("2" (skosimp*) (("2" (lemma "axiom_of_archimedes") (("2" (inst -1 "(b!1-a!1)/delta!1+2") (("2" (skosimp*) (("2" (name "NM" "real_defs.max(i!1,2)") (("2" (inst - "eq_partition(a!1,b!1,NM)") (("1" (split -3) (("1" (inst - "Rie_sum(a!1, b!1, eq_partition(a!1, b!1, NM), gen_xis(a!1, b!1, eq_partition(a!1, b!1, N (("1" (name-replace "II" "integral(a!1, b!1, f!1)") (("1" (case "Rie_sum(a!1, b!1, eq_partition(a!1, b!1, NM), gen_xis(a!1,b!1,eq_partition(a!1, b!1, N (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (hide -1 -4 2 3) (("2" (name "NN" "eq_partition(a!1, b!1, NM)") (("2" (replace -1) (("2" (expand "Rie_sum") (("2" (lemma "sigma_nonneg[below(length(NN) - 1)]") (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (skosimp*) (("1" (factor 1 l) (("1" (inst?) (("1" (case "(NN`seq(1 + i!2) - NN`seq(i!2)) > 0") (("1" (mult-ineq -1 -6) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (typepred "NN") (("2" (inst - "i!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "Riemann?_Rie") (("2" (inst -1 "a!1" "b!1" "f!1") (("2" (assert) (("2" (inst?) (("2" (assert) (("2" (hide -3 -4 -5 2 3) (("2" (name-replace ba "b!1-a!1") (("2" (lemma "Riemann?_Rie") (("2" (inst -1 "a!1" "b!1" "f!1") (("2" (split -1) (("1" (inst?) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil) ("2" (rewrite "width_eq_part") (("2" (hide -3 -4 -5 2 3) (("2" (name-replace ba "b!1-a!1") (("2" (move-terms -2 l 2) (("2" (case "ba / delta!1 < i!1 - 1") (("1" (hide -3) (("1" (mult-by -1 "delta!1") (("1" (mult-by 1 "NM-1") (("1" (expand "max") (("1" (lift-if) (("1" (ground) (("1" (replace -2 * rl) (("1" (hide -2) (("1" (assert) (("1" (typepred "i!1") (("1" (factor -3 r) (("1" (case "i!1-1 < 1") (("1" (hide -3) (("1" (mult-by -1 "delta!1") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) 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) ((integral const-decl "{S: real | integral?(a, b, ff, S)}" integral_def nil) (integrable? const-decl "bool" integral_def nil) (integral? const-decl "bool" integral_def nil) (< const-decl "bool" reals nil) (T formal-subtype-decl nil integral_prep nil) (T_pred const-decl "[real -> boolean]" integral_prep nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (a!1 skolem-const-decl "T" integral_prep nil) (b!1 skolem-const-decl "T" integral_prep nil) (f!1 skolem-const-decl "[T -> real]" integral_prep nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_max application-judgement "{k: int | i <= k AND j <= k}" real_defs nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (= const-decl "[T, T -> boolean]" equalities nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs 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) (Riemann?_Rie formula-decl nil integral_def nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_nonneg formula-decl nil sigma "reals/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (posint_plus_nnint_is_posint application-judgement "posint" 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs_0 formula-decl nil abs_lems "reals/") (gt_times_gt_any1 formula-decl nil extra_real_props 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) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (gen_xis const-decl "(xis?(a, b, P))" integral_def nil) (Rie_sum const-decl "real" integral_def nil) (xis? const-decl "bool" integral_def nil) (Riemann_sum? const-decl "bool" integral_def nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel2 formula-decl nil real_props nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (width_eq_part formula-decl nil integral_def nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil naturalnumbers nil) (partition type-eq-decl nil integral_def nil) (above nonempty-type-eq-decl nil integers nil) (eq_partition const-decl "partition(a, b)" integral_def nil) (NM skolem-const-decl "{k: int | i!1 <= k AND 2 <= k}" integral_prep nil) (i!1 skolem-const-decl "int" integral_prep nil) (axiom_of_archimedes formula-decl nil real_props nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (integral_jmp 0 (integral_jmp-12 "" 3403520684 ("" (skosimp*) (("" (lemma "integral_def") (("" (inst?) (("" (assert) (("" (flatten) (("" (hide -1) (("" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (expand "integral?") (("2" (skosimp*) (("2" (case "cc!1 = 0") (("1" (inst + "1") (("1" (skosimp*) (("1" (typepred "R!1") (("1" (expand "Riemann_sum?") (("1" (skosimp*) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "Rie_sum(a!1, b!1, P!1, xis!1, f!1) = 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "Rie_sum") (("2" (assert) (("2" (case-replace "(LAMBDA (n: below(length(P!1) - 1)): P!1`seq(1 + n) * f!1(xis!1(n)) - P!1`seq(n) * f!1(xis!1(n))) = (LAMBDA (n: below(length(P!1) - 1)): 0)") (("1" (lemma "sigma_const[below(length(P!1) - 1)]") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "epsi!1/(2*abs(cc!1))") (("1" (skosimp*) (("1" (lemma "part_in") (("1" (inst -1 "a!1" "b!1" "z!1" "P!1") (("1" (assert) (("1" (skosimp*) (("1" (typepred "R!1") (("1" (expand "Riemann_sum?") (("1" (skosimp*) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "Rie_sum_alt_lem") (("1" (inst - "a!1" "b!1" "f!1") (("1" (assert) (("1" (inst?) (("1" (replace -1) (("1" (hide -1) (("1" (expand "Rie_sum_alt") (("1" (expand "Rie_sec") (("1" (assert) (("1" (name "SS1" "sigma(1, length(P!1) - 1, LAMBDA (n: upto(length(P!1) - 1)): IF n = 0 THEN 0 ELSE seq(P!1)(n) * f!1(xis!1(n - 1)) - seq(P!1)(n - 1) * f!1(xis!1(n - 1)) ENDIF)") (("1" (replace -1) (("1" (name "W" "width(a!1, b!1, P!1)") (("1" (replace -1) (("1" (case "abs(SS1) <= 2* W * abs(cc!1) ") (("1" (hide -2) (("1" (assert) (("1" (case-replace "abs(-1 * SS1) = abs(SS1)") (("1" (cross-mult -6) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (expand "abs") (("2" (lift-if) (("2" (lift-if) (("2" (ground) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "Intv" "(LAMBDA (nn: upto[length(P!1)-2]): seq(P!1)(nn+1) - seq(P!1)(nn))") (("2" (case-replace "(LAMBDA (n: upto(length(P!1) - 1)): IF n = 0 THEN 0 ELSE seq(P!1)(n) * f!1(xis!1(n - 1)) - seq(P!1)(n - 1) * f!1(xis!1(n - 1)) ENDIF) = (LAMBDA (n: upto(length(P!1) - 1)): IF n = 0 THEN 0 ELSE Intv(n-1) * f!1(xis!1(n - 1)) ENDIF)") (("1" (hide -1) (("1" (name "FF" "(LAMBDA (n: upto(length(P!1) - 1)): IF n = 0 THEN 0 ELSE Intv(n - 1) * f!1(xis!1(n - 1)) ENDIF)") (("1" (case-replace "length(P!1) = 1") (("1" (rewrite "sigma_rew" -5) (("1" (replace -5 * rl) (("1" (expand "abs" 1 1) (("1" (expand "abs" +) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case-replace "length(P!1) = 2") (("1" (rewrite "sigma_rew") (("1" (assert) (("1" (hide 4) (("1" (replace -5 * rl) (("1" (rewrite "abs_mult") (("1" (case "abs(Intv(0)) <= W") (("1" (case "abs(f!1(xis!1(0))) <= abs(cc!1)") (("1" (mult-ineq -1 -2 (+ +)) (("1" (assert) nil nil) ("2" (rewrite "abs_abs") (("2" (rewrite "abs_abs") (("2" (rewrite "abs_abs") (("2" (assert) (("2" (expand "abs" 1 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (inst -14 "xis!1(0)") (("2" (assert) (("2" (hide-all-but (-13 -14 1 2)) (("2" (replace -2) (("2" (expand "abs") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -3 -4 1)) (("2" (replace -2 * rl) (("2" (assert) (("2" (expand "abs") (("2" (lemma "width_lem") (("2" (expand "finseq_appl") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("2" (replace -1) (("2" (hide 5) (("2" (case-replace "(FORALL (nn: upto(length(P!1) - 1)): abs(FF(nn)) <= W*abs(cc!1))") (("1" (hide -8 -9 -10 -11 -12 -13) (("1" (case "(FORALL (ii: upto(length(P!1)-2)): abs(Intv(ii)) <= W)") (("1" (case-replace "ii!1 = 0") (("1" (rewrite "sigma_first_ge") (("1" (case-replace "SS1 = FF(1) + FF(2)") (("1" (hide -1) (("1" (hide -6) (("1" (inst-cp -3 "1") (("1" (inst-cp -3 "2") (("1" (lemma "triangle") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (rewrite "sigma_first_ge") (("2" (case-replace "sigma(3, length(P!1) - 1, FF) = 0") (("1" (assert) nil nil) ("2" (lemma "sigma_restrict[upto(length(P!1) - 1)]") (("2" (inst?) (("2" (inst -1 "length(P!1) - 1" "3") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "restrict(FF, 3, length(P!1) - 1) = (LAMBDA (n: upto(length(P!1) - 1)): 0)") (("1" (hide -1) (("1" (lemma "sigma_const[upto(length(P!1) - 1)]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "restrict") (("2" (apply-extensionality 1 :hide? t) (("2" (lift-if) (("2" (ground) (("2" (hide -5 -6 -7) (("2" (hide 3 4) (("2" (replace -4 * rl) (("2" (assert) (("2" (reveal -13) (("2" (inst?) (("2" (assert) (("2" (lemma "parts_order") (("2" (inst -1 "a!1" "b!1" "P!1" "1" "x!1-1") (("2" (assert) (("2" (lemma "xis_lem") (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "sigma") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (hide -5) (("2" (lemma "sigma_upto[(length(P!1) - 1)].sigma_split_ge") (("2" (inst?) (("2" (inst -1 "ii!1") (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (rewrite "sigma_last_ge") (("2" (case-replace "sigma(1, ii!1 - 1, FF) = 0") (("1" (assert) (("1" (hide -1) (("1" (case "z!1 = seq(P!1)(1+ii!1)") (("1" (case "FF(1 + ii!1) + FF(ii!1) = SS1") (("1" (hide -7) (("1" (replace -1 * rl) (("1" (hide -1) (("1" (lemma "triangle") (("1" (inst?) (("1" (inst-cp -4 "1+ii!1") (("1" (inst -4 "ii!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "ii!1 = length(P!1) -2") (("1" (rewrite "sigma_rew") (("1" (assert) nil nil)) nil) ("2" (rewrite "sigma_first_ge") (("2" (assert) (("2" (rewrite "sigma_first_ge") (("2" (assert) (("2" (case-replace "sigma(3 + ii!1, length(P!1) - 1, FF) = 0") (("1" (hide -1) (("1" (hide 2) (("1" (case "FF(ii!1) = 0") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (replace -6 * rl) (("1" (hide -6) (("1" (lemma "triangle") (("1" (inst?) (("1" (inst-cp -4 "1+ii!1") (("1" (inst-cp -4 "2+ii!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 -3 -5 -6 6) (("2" (replace -2 * rl) (("2" (assert) (("2" (hide -2) (("2" (reveal -17) (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (typepred "P!1") (("2" (inst -4 "ii!1") (("2" (assert) (("2" (lemma "xis_lem") (("2" (assert) (("2" (inst - "a!1" "b!1" "P!1" "xis!1" "ii!1-1") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "sigma_restrict_to") (("2" (case-replace "restrict(FF, 3 + ii!1, length(P!1) - 1) = (LAMBDA (n: upto(length(P!1) - 1)): 0)") (("1" (hide -1) (("1" (rewrite "sigma_const[upto(length(P!1) - 1)]") nil nil)) nil) ("2" (hide 2) (("2" (expand "restrict") (("2" (apply-extensionality 1 :hide? t) (("2" (hide -2 -3 -5 -6 3 7) (("2" (replace -2 * rl) (("2" (assert) (("2" (hide -2) (("2" (lift-if) (("2" (ground) (("2" (reveal -17) (("2" (inst?) (("2" (assert) (("2" (lemma "parts_order") (("2" (inst -1 "a!1" "b!1" "P!1" "ii!1+1" "x!1-1") (("2" (assert) (("2" (lemma "xis_lem") (("2" (assert) (("2" (inst - "a!1" "b!1" "P!1" "xis!1" "x!1-1") (("2" (flatten) (("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) ("2" (case "FF(1 + ii!1) + FF(ii!1) = SS1") (("1" (hide -6) (("1" (replace -1 * rl) (("1" (hide -1) (("1" (inst-cp -2 "ii!1") (("1" (inst-cp -2 "ii!1+1") (("1" (lemma "triangle") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "sigma_first_ge") (("2" (case-replace "sigma(2 + ii!1, length(P!1) - 1, FF) = 0") (("1" (hide -1) (("1" (assert) nil nil)) nil) ("2" (hide -1 -2 -4 -5 2 7) (("2" (rewrite "sigma_restrict_to") (("2" (case "restrict(FF, 2 + ii!1, length(P!1) - 1) = (LAMBDA (n: upto(length(P!1) - 1)): 0)") (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "sigma_const[upto(length(P!1) - 1)]") nil nil)) nil)) nil) ("2" (expand "restrict") (("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (assert) (("2" (ground) (("2" (lift-if) (("2" (ground) (("2" (reveal -17) (("2" (inst?) (("2" (assert) (("2" (lemma "parts_order") (("2" (inst -1 "a!1" "b!1" "P!1" "ii!1+1" "x!1-1") (("2" (assert) (("2" (typepred "P!1") (("2" (inst?) (("2" (lemma "xis_lem") (("2" (assert) (("2" (inst - "a!1" "b!1" "P!1" "xis!1" "x!1-1") (("2" (flatten) (("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)) nil) ("2" (rewrite "sigma_restrict_to") (("2" (case-replace "restrict(FF, 1, ii!1 - 1) = (LAMBDA (n: upto(length(P!1) - 1)): 0)") (("1" (hide -1) (("1" (rewrite "sigma_const[upto(length(P!1) - 1)]") nil nil)) nil) ("2" (hide 2) (("2" (expand "restrict") (("2" (apply-extensionality 1 :hide? t) (("2" (lift-if) (("2" (ground) (("2" (hide -4 -5) (("2" (replace -3 * rl) (("2" (hide -3) (("2" (hide -1 -2) (("2" (assert) (("2" (reveal -16) (("2" (inst?) (("2" (assert) (("2" (expand "abs") (("2" (assert) (("2" (lemma "parts_order") (("2" (inst -1 "a!1" "b!1" "P!1" "x!1" "ii!1") (("2" (assert) (("2" (typepred "P!1") (("2" (inst?) (("2" (assert) (("2" (lemma "xis_lem") (("2" (assert) (("2" (inst - "a!1" "b!1" "P!1" "xis!1" "x!1-1") (("2" (flatten) (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (replace -3 * rl) (("2" (assert) (("2" (hide 4) (("2" (replace -4 * rl) (("2" (hide-all-but 1) (("2" (lemma "width_lem") (("2" (expand "finseq_appl") (("2" (inst?) (("2" (typepred "P!1") (("2" (inst -4 "ii!2") (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (replace -1 * rl) (("2" (assert) (("2" (ground) (("2" (lift-if) (("2" (ground) (("2" (hide -1) (("2" (inst - "xis!1(nn!1 - 1)") (("2" (rewrite "abs_mult") (("2" (case "abs(Intv(nn!1 - 1)) <= W") (("1" (case "abs(f!1(xis!1(nn!1 - 1))) <= abs(cc!1)") (("1" (mult-ineq -1 -2) (("1" (assert) nil nil) ("2" (rewrite "abs_abs") (("2" (rewrite "abs_abs") (("2" (rewrite "abs_abs") (("2" (assert) (("2" (hide 2 4 7 -1 -5) (("2" (expand "abs" 1 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 -4 3) (("2" (assert) (("2" (ground) nil nil)) nil)) nil)) nil) ("2" (expand "abs" 1 1) (("2" (assert) (("2" (hide 3 6 -3 -6 -7 -8 -9 -10 -11) (("2" (replace -1 * rl) (("2" (assert) (("2" (hide -1) (("2" (lemma "width_lem") (("2" (assert) (("2" (inst?) (("2" (assert) (("2" (typepred "P!1") (("2" (inst?) (("2" (assert) (("2" (lift-if) (("2" (ground) (("2" (typepred "P!1") (("2" (inst -4 "nn!1-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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2 4) (("2" (apply-extensionality 1 :hide? t) (("1" (replace -1 * rl) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (typepred "P!1") (("4" (inst?) (("4" (skosimp*) (("4" (assert) nil nil)) 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)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (prop) (("1" (cross-mult 1) (("1" (ground) nil nil)) nil) ("2" (cross-mult 1) (("2" (ground) nil nil)) nil)) nil)) nil) ("3" (expand "abs") (("3" (lift-if) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-subtype-decl nil integral_prep nil) (T_pred const-decl "[real -> boolean]" integral_prep 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) (integral_def formula-decl nil integral_def nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (/= const-decl "boolean" notequal nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (cc!1 skolem-const-decl "real" integral_prep nil) (epsi!1 skolem-const-decl "posreal" integral_prep nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (part_in formula-decl nil integral_def nil) (Rie_sec const-decl "real" integral_def nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (sigma def-decl "real" sigma "reals/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (width const-decl "posreal" integral_def nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (le_times_le_any1 formula-decl nil extra_real_props nil) (abs_abs formula-decl nil real_props nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (width_lem formula-decl nil integral_def nil) (abs_mult formula-decl nil real_props nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (abs_nat formula-decl nil abs_lems "reals/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (triangle formula-decl nil real_props nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_restrict formula-decl nil sigma "reals/") (a!1 skolem-const-decl "T" integral_prep nil) (b!1 skolem-const-decl "T" integral_prep nil) (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_prep nil) (restrict const-decl "[T -> real]" sigma "reals/") (sigma_nnreal application-judgement "nnreal" sigma_upto "reals/") (sigma_nat application-judgement "nat" sigma_upto "reals/") (parts_order formula-decl nil integral_def nil) (xis_lem formula-decl nil integral_def nil) (real_plus_real_is_real application-judgement "real" reals nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (sigma_first_ge formula-decl nil sigma_upto "reals/") (sigma_restrict_to formula-decl nil sigma "reals/") (sigma_last_ge formula-decl nil sigma_upto "reals/") (sigma_split_ge formula-decl nil sigma_upto "reals/") (sigma_rew formula-decl nil sigma "reals/") (odd_minus_odd_is_even application-judgement "even_int" integers nil) (upto nonempty-type-eq-decl nil nat_types nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (Rie_sum_alt const-decl "real" integral_def nil) (Rie_sum_alt_lem formula-decl nil integral_def nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (partition type-eq-decl nil integral_def nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (Riemann_sum? const-decl "bool" integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans 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) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (sigma_const formula-decl nil sigma "reals/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (sigma_nnreal application-judgement "nnreal" sigma_below "reals/") (sigma_nat application-judgement "nat" sigma_below "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs_0 formula-decl nil abs_lems "reals/") (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_times_even_is_even application-judgement "even_int" integers nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (xis? const-decl "bool" integral_def nil) (Rie_sum const-decl "real" integral_def nil) (int_minus_int_is_int application-judgement "int" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (integral? const-decl "bool" integral_def nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil) (integral_jmp-11 "" 3352608695 ("" (skosimp*) (("" (lemma "integral_def") (("" (inst?) (("" (assert) (("" (flatten) (("" (hide -1) (("" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (expand "integral?") (("2" (skosimp*) (("2" (case "cc!1 = 0") (("1" (inst + "1") (("1" (skosimp*) (("1" (typepred "R!1") (("1" (expand "Riemann_sum?") (("1" (skosimp*) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "Rie_sum(a!1, b!1, P!1, xis!1, f!1) = 0") (("1" (assert) (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "Rie_sum") (("2" (assert) (("2" (case-replace "(LAMBDA (n: below(length(P!1) - 1)): P!1`seq(1 + n) * f!1(xis!1(n)) - P!1`seq(n) * f!1(xis!1(n))) = (LAMBDA (n: below(length(P!1) - 1)): 0)") (("1" (lemma "sigma_const[below(length(P!1) - 1)]") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "epsi!1/(2*abs(cc!1))") (("1" (skosimp*) (("1" (lemma "part_in") (("1" (inst -1 "a!1" "b!1" "z!1" "P!1") (("1" (assert) (("1" (skosimp*) (("1" (typepred "R!1") (("1" (expand "Riemann_sum?") (("1" (skosimp*) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "Rie_sum_alt_lem") (("1" (inst - "a!1" "b!1" "f!1") (("1" (assert) (("1" (inst?) (("1" (replace -1) (("1" (hide -1) (("1" (expand "Rie_sum_alt") (("1" (expand "Rie_sec") (("1" (assert) (("1" (name "SS1" "sigma(1, length(P!1) - 1, LAMBDA (n: upto(length(P!1) - 1)): IF n = 0 THEN 0 ELSE seq(P!1)(n) * f!1(xis!1(n - 1)) - seq(P!1)(n - 1) * f!1(xis!1(n - 1)) ENDIF)") (("1" (replace -1) (("1" (name "W" "width(a!1, b!1, P!1)") (("1" (replace -1) (("1" (case "abs(SS1) <= 2* W * abs(cc!1) ") (("1" (hide -2) (("1" (assert) (("1" (case-replace "abs(-1 * SS1) = abs(SS1)") (("1" (cross-mult -6) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (expand "abs") (("2" (lift-if) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "Intv" "(LAMBDA (nn: upto[length(P!1)-2]): seq(P!1)(nn+1) - seq(P!1)(nn))") (("2" (case-replace "(LAMBDA (n: upto(length(P!1) - 1)): IF n = 0 THEN 0 ELSE seq(P!1)(n) * f!1(xis!1(n - 1)) - seq(P!1)(n - 1) * f!1(xis!1(n - 1)) ENDIF) = (LAMBDA (n: upto(length(P!1) - 1)): IF n = 0 THEN 0 ELSE Intv(n-1) * f!1(xis!1(n - 1)) ENDIF)") (("1" (hide -1) (("1" (name "FF" "(LAMBDA (n: upto(length(P!1) - 1)): IF n = 0 THEN 0 ELSE Intv(n - 1) * f!1(xis!1(n - 1)) ENDIF)") (("1" (case-replace "length(P!1) = 1") (("1" (expand "sigma" -5) (("1" (replace -5 * rl) (("1" (expand "abs" 1 1) (("1" (expand "abs" +) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case-replace "length(P!1) = 2") (("1" (expand "sigma") (("1" (assert) (("1" (hide 4) (("1" (replace -5 * rl) (("1" (rewrite "abs_mult") (("1" (case "abs(Intv(0)) <= W") (("1" (case "abs(f!1(xis!1(0))) <= abs(cc!1)") (("1" (mult-ineq -1 -2 (+ +)) (("1" (assert) nil nil) ("2" (rewrite "abs_abs") (("2" (rewrite "abs_abs") (("2" (rewrite "abs_abs") (("2" (assert) (("2" (expand "abs" 1 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (inst -14 "xis!1(0)") (("2" (assert) (("2" (hide-all-but (-13 -14 1 2)) (("2" (replace -2) (("2" (expand "abs") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -3 -4 1)) (("2" (replace -2 * rl) (("2" (assert) (("2" (expand "abs") (("2" (lemma "width_lem") (("2" (expand "finseq_appl") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide 5) (("2" (case-replace "(FORALL (nn: upto(length(P!1) - 1)): abs(FF(nn)) <= W*abs(cc!1))") (("1" (hide -8 -9 -10 -11 -12 -13) (("1" (case "(FORALL (ii: upto(length(P!1)-2)): abs(Intv(ii)) <= W)") (("1" (case-replace "ii!1 = 0") (("1" (rewrite "sigma_first_ge") (("1" (case-replace "SS1 = FF(1) + FF(2)") (("1" (hide -1) (("1" (hide -6) (("1" (inst-cp -3 "1") (("1" (inst-cp -3 "2") (("1" (lemma "triangle") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (rewrite "sigma_first_ge") (("2" (case-replace "sigma(3, length(P!1) - 1, FF) = 0") (("1" (assert) nil nil) ("2" (lemma "sigma_restrict[upto(length(P!1) - 1)]") (("2" (inst?) (("2" (inst -1 "length(P!1) - 1" "3") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "restrict(FF, 3, length(P!1) - 1) = (LAMBDA (n: upto(length(P!1) - 1)): 0)") (("1" (hide -1) (("1" (lemma "sigma_const[upto(length(P!1) - 1)]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "restrict") (("2" (apply-extensionality 1 :hide? t) (("2" (lift-if) (("2" (ground) (("2" (hide -5 -6 -7) (("2" (hide 3 4) (("2" (replace -4 * rl) (("2" (assert) (("2" (reveal -13) (("2" (inst?) (("2" (assert) (("2" (lemma "parts_order") (("2" (inst -1 "a!1" "b!1" "P!1" "1" "x!1-1") (("2" (assert) (("2" (lemma "xis_lem") (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "sigma") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (hide -5) (("2" (lemma "sigma_upto[(length(P!1) - 1)].sigma_split_ge") (("2" (inst?) (("2" (inst -1 "ii!1") (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (rewrite "sigma_last_ge") (("2" (case-replace "sigma(1, ii!1 - 1, FF) = 0") (("1" (assert) (("1" (hide -1) (("1" (case "z!1 = seq(P!1)(1+ii!1)") (("1" (case "FF(1 + ii!1) + FF(ii!1) = SS1") (("1" (hide -7) (("1" (replace -1 * rl) (("1" (hide -1) (("1" (lemma "triangle") (("1" (inst?) (("1" (inst-cp -4 "1+ii!1") (("1" (inst -4 "ii!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "ii!1 = length(P!1) -2") (("1" (expand "sigma") (("1" (assert) nil nil)) nil) ("2" (rewrite "sigma_first_ge") (("2" (assert) (("2" (rewrite "sigma_first_ge") (("2" (assert) (("2" (case-replace "sigma(3 + ii!1, length(P!1) - 1, FF) = 0") (("1" (hide -1) (("1" (hide 2) (("1" (case "FF(ii!1) = 0") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (replace -6 * rl) (("1" (hide -6) (("1" (lemma "triangle") (("1" (inst?) (("1" (inst-cp -4 "1+ii!1") (("1" (inst-cp -4 "2+ii!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 -3 -5 -6 6) (("2" (replace -2 * rl) (("2" (assert) (("2" (hide -2) (("2" (reveal -17) (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (typepred "P!1") (("2" (inst -4 "ii!1") (("2" (assert) (("2" (lemma "xis_lem") (("2" (assert) (("2" (inst - "a!1" "b!1" "P!1" "xis!1" "ii!1-1") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "sigma_restrict_to") (("2" (case-replace "restrict(FF, 3 + ii!1, length(P!1) - 1) = (LAMBDA (n: upto(length(P!1) - 1)): 0)") (("1" (hide -1) (("1" (rewrite "sigma_const[upto(length(P!1) - 1)]") nil nil)) nil) ("2" (hide 2) (("2" (expand "restrict") (("2" (apply-extensionality 1 :hide? t) (("2" (hide -2 -3 -5 -6 3 7) (("2" (replace -2 * rl) (("2" (assert) (("2" (hide -2) (("2" (lift-if) (("2" (ground) (("2" (reveal -17) (("2" (inst?) (("2" (assert) (("2" (lemma "parts_order") (("2" (inst -1 "a!1" "b!1" "P!1" "ii!1+1" "x!1-1") (("2" (assert) (("2" (lemma "xis_lem") (("2" (assert) (("2" (inst - "a!1" "b!1" "P!1" "xis!1" "x!1-1") (("2" (flatten) (("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) ("2" (case "FF(1 + ii!1) + FF(ii!1) = SS1") (("1" (hide -6) (("1" (replace -1 * rl) (("1" (hide -1) (("1" (inst-cp -2 "ii!1") (("1" (inst-cp -2 "ii!1+1") (("1" (lemma "triangle") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "sigma_first_ge") (("2" (case-replace "sigma(2 + ii!1, length(P!1) - 1, FF) = 0") (("1" (hide -1) (("1" (assert) nil nil)) nil) ("2" (hide -1 -2 -4 -5 2 7) (("2" (rewrite "sigma_restrict_to") (("2" (case "restrict(FF, 2 + ii!1, length(P!1) - 1) = (LAMBDA (n: upto(length(P!1) - 1)): 0)") (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "sigma_const[upto(length(P!1) - 1)]") nil nil)) nil)) nil) ("2" (expand "restrict") (("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (assert) (("2" (ground) (("2" (lift-if) (("2" (ground) (("2" (reveal -17) (("2" (inst?) (("2" (assert) (("2" (lemma "parts_order") (("2" (inst -1 "a!1" "b!1" "P!1" "ii!1+1" "x!1-1") (("2" (assert) (("2" (typepred "P!1") (("2" (inst?) (("2" (lemma "xis_lem") (("2" (assert) (("2" (inst - "a!1" "b!1" "P!1" "xis!1" "x!1-1") (("2" (flatten) (("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)) nil) ("2" (rewrite "sigma_restrict_to") (("2" (case-replace "restrict(FF, 1, ii!1 - 1) = (LAMBDA (n: upto(length(P!1) - 1)): 0)") (("1" (hide -1) (("1" (rewrite "sigma_const[upto(length(P!1) - 1)]") nil nil)) nil) ("2" (hide 2) (("2" (expand "restrict") (("2" (apply-extensionality 1 :hide? t) (("2" (lift-if) (("2" (ground) (("2" (hide -4 -5) (("2" (replace -3 * rl) (("2" (hide -3) (("2" (hide -1 -2) (("2" (assert) (("2" (reveal -16) (("2" (inst?) (("2" (assert) (("2" (expand "abs") (("2" (assert) (("2" (lemma "parts_order") (("2" (inst -1 "a!1" "b!1" "P!1" "x!1" "ii!1") (("2" (assert) (("2" (typepred "P!1") (("2" (inst?) (("2" (assert) (("2" (lemma "xis_lem") (("2" (assert) (("2" (inst - "a!1" "b!1" "P!1" "xis!1" "x!1-1") (("2" (flatten) (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (replace -3 * rl) (("2" (assert) (("2" (hide 4) (("2" (replace -4 * rl) (("2" (hide-all-but 1) (("2" (lemma "width_lem") (("2" (expand "finseq_appl") (("2" (inst?) (("2" (typepred "P!1") (("2" (inst -4 "ii!2") (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (replace -1 * rl) (("2" (assert) (("2" (ground) --> -------------------- --> maximum size reached --> --------------------
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.464Bemerkung: (vorverarbeitet am 2026-04-28) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26