| products/Sources/formale Sprachen/Isabelle/Sequents/ (Beweissystem der NASA Version 6.0.9©) Datei vom 16.11.2025 mit Größe 1 kB |
|
integral_bounded.prf
Interaktion und |
||||||
|
(integral_bounded (IMP_integral_prep_TCC1 0 (IMP_integral_prep_TCC1-1 nil 3282561874 ("" (lemma "connected_domain") (("" (propax) nil nil)) nil) ((connected_domain formula-decl nil integral_bounded nil)) shostak)) (IMP_integral_prep_TCC2 0 (IMP_integral_prep_TCC2-1 nil 3282561874 ("" (lemma "not_one_element") (("" (propax) nil nil)) nil) ((not_one_element formula-decl nil integral_bounded nil)) shostak)) (int_to_bnd_TCC1 0 (int_to_bnd_TCC1-1 nil 3282561874 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (int_to_bnd_TCC2 0 (int_to_bnd_TCC2-1 nil 3282561874 ("" (skosimp*) (("" (assert) nil nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (int_to_bnd 0 (int_to_bnd-2 nil 3477651374 ("" (skosimp*) (("" (case "(FORALL (eps: posreal): (EXISTS (EP: partition[T](a!1,b!1)): (FORALL (j: below(length(EP)-1)): FORALL (xx: real): (EP(j) <= xx AND xx <= EP(j+1)) IMPLIES abs(f!1(xx) - f!1(EP(j))) < eps/abs(EP(j+1) - EP(j)))))") (("1" (assert) (("1" (inst - "1000") (("1" (skosimp*) (("1" (inst + "EP!1") (("1" (skosimp*) (("1" (inst - "j!1") (("1" (expand "bounded_on?") (("1" (inst + "1000 / abs(EP!1`seq(1 + j!1) - EP!1`seq(j!1)) + abs(f!1(EP!1`seq(j!1)))") (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (lemma "abs_diff") (("1" (inst - "f!1(x!1)" "f!1(EP!1`seq(j!1))") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "EP!1") (("2" (inst - "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (lemma "Lemma_1[T]") (("2" (inst?) (("2" (assert) (("2" (inst -1 "eps!1") (("2" (skosimp*) (("2" (name "EP" "eq_partition(a!1,b!1,floor((b!1-a!1)/delta!1) + 2)") (("1" (inst + "EP") (("1" (skosimp*) (("1" (case "T_pred(xx!1)") (("1" (case "abs(EP`seq(1 + j!1) - EP`seq(j!1)) > 0") (("1" (cross-mult 1) (("1" (hide -1) (("1" (name "SecJ" "(EP`seq(1 + j!1) - EP`seq(j!1))") (("1" (name "F_DIF" "(f!1((EP)(j!1)) - f!1(xx!1))") (("1" (assert) (("1" (rewrite "abs_mult" :dir rl) (("1" (case-replace "EP`seq(1 + j!1) * f!1(xx!1) - EP`seq(j!1) * f!1(xx!1) + (EP`seq(j!1) * f!1(EP`seq(j!1))- EP`seq(1 + j!1) * f!1(EP`seq(j!1))) = -SecJ*F_DIF") (("1" (hide -1) (("1" (lemma "abs_neg") (("1" (inst - "SecJ * F_DIF") (("1" (replace -1) (("1" (hide -1) (("1" (inst - "EP" "EP" "gxis(a!1,b!1,EP,j!1,true,xx!1)" "gxis(a!1,b!1,EP,j!1,false,xx!1)") (("1" (split -5) (("1" (expand "Rie_sum") (("1" (assert) (("1" (assert) (("1" (rewrite "sigma_minus[below[length(EP)-1]]") (("1" (case-replace "(LAMBDA (i: below(length(EP) - 1)): EP`seq(i) * f!1(gxis(a!1, b!1, EP, j!1, FALSE, xx!1)(i)) + EP`seq(1 + i) * f!1(gxis(a!1, b!1, EP, j!1, TRUE, xx!1)(i)) - EP`seq(i) * f!1(gxis(a!1, b!1, EP, j!1, TRUE, xx!1)(i)) - EP`seq(1 + i) * f!1(gxis(a!1, b!1, EP, j!1, FALSE, xx!1)(i))) = (LAMBDA (i: below(length(EP) - 1)): IF i = j!1 THEN (EP`seq(1 + j!1) - EP`seq(j!1)) * (f!1(EP(j!1)) - f!1(xx!1)) ELSE 0 ENDIF)") (("1" (assert) (("1" (hide -1) (("1" (case-replace "EP`seq(1 + j!1) * f!1(EP`seq(j!1)) - EP`seq(1 + j!1) * f!1(xx!1) + (EP`seq(j!1) * f!1(xx!1) - EP`seq(j!1) * f!1(EP`seq(j!1))) = SecJ*F_DIF") (("1" (hide -1) (("1" (case "j!1 < length(EP) - 2") (("1" (lemma "sigma_below[length(EP)-1].sigma_split_ge") (("1" (inst - "_" "length(EP) - 2" "0" "j!1") (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "sigma(1 + j!1, length(EP) - 2, (LAMBDA (i: below(length(EP) - 1)): IF i = j!1 THEN SecJ * F_DIF ELSE 0 ENDIF)) = 0") (("1" (hide -1) (("1" (rewrite "sigma_last_ge") (("1" (assert) (("1" (case "sigma(0, j!1 - 1, (LAMBDA (i: below(length(EP) - 1)): IF i = j!1 THEN SecJ * F_DIF ELSE 0 ENDIF)) = 0") (("1" (assert) nil nil) ("2" (lemma "sigma_restrict_eq[below(length(EP)-1)]") (("2" (inst?) (("2" (inst - "(LAMBDA (i: below(length(EP) - 1)): 0)") (("2" (expand "restrict") (("2" (replace -1) (("2" (hide -1) (("2" (lemma "sigma_const[below(length(EP)-1)]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_restrict_eq[below(length(EP)-1)]") (("1" (inst?) (("1" (inst - "(LAMBDA (i: below(length(EP) - 1)): 0)") (("1" (expand "restrict") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_const[below(length(EP)-1)]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1 = length(EP) - 2") (("1" (rewrite "sigma_last_ge") (("1" (case-replace "sigma(0, length(EP) - 3, (LAMBDA (i: below(length(EP) - 1)): IF i = j!1 THEN SecJ * F_DIF ELSE 0 ENDIF)) = 0") (("1" (assert) nil nil) ("2" (lemma "sigma_restrict_eq[below(length(EP)-1)]") (("1" (inst?) (("1" (inst - "(LAMBDA (i: below(length(EP) - 1)): 0)") (("1" (expand "restrict") (("1" (assert) (("1" (lemma "sigma_const[below(length(EP)-1)]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "gxis") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "gxis") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "N_from_delta") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("3" (lemma "N_from_delta") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "EP") (("2" (inst - "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "connected_domain") (("2" (expand "connected?") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "(b!1 - a!1) / delta!1 > 0") (("1" (assert) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (typepred "EP!1") (("3" (inst - "j!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (lemma "connected_domain") (("4" (expand "connected?") (("4" (inst - "_" "_" "xx!1") (("4" (inst?) (("4" (inst?) (("4" (assert) 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) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- 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) (T formal-subtype-decl nil integral_bounded nil) (T_pred const-decl "[real -> boolean]" integral_bounded nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (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) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (a!1 skolem-const-decl "T" integral_bounded nil) (b!1 skolem-const-decl "T" integral_bounded nil) (EP!1 skolem-const-decl "partition[T](a!1, b!1)" integral_bounded nil) (j!1 skolem-const-decl "below(length(EP!1) - 1)" integral_bounded nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (abs_diff formula-decl nil abs_lems "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (bounded_on? const-decl "bool" integral_bounded nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Lemma_1 formula-decl nil integral_prep nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (j!1 skolem-const-decl "below(length(EP) - 1)" integral_bounded nil) (EP skolem-const-decl "{fs: finite_sequence[{x | a!1 <= x AND x <= b!1}] | length(fs) > 1 AND seq(fs)(0) = a!1 AND seq(fs)(length(fs) - 1) = b!1 AND (FORALL (ii: below(length(fs) - 1)): seq(fs)(ii) < seq(fs)(1 + ii))}" integral_bounded nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (minus_real_is_real application-judgement "real" reals nil) (abs_neg formula-decl nil abs_lems "reals/") (FALSE const-decl "bool" booleans nil) (TRUE const-decl "bool" booleans nil) (gxis const-decl "(xis?(a, b, P))" integral_prep nil) (xis? const-decl "bool" integral_def nil) (N_from_delta formula-decl nil integral_def nil) (Rie_sum const-decl "real" integral_def nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sigma_split_ge formula-decl nil sigma_below "reals/") (sigma_restrict_eq formula-decl nil sigma "reals/") (sigma_nat application-judgement "nat" sigma_below "reals/") (sigma_const formula-decl nil sigma "reals/") (int_times_even_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (restrict const-decl "[T -> real]" sigma "reals/") (sigma_last_ge formula-decl nil sigma_below "reals/") (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma def-decl "real" sigma "reals/") (int_below type-eq-decl nil sigma_below "reals/") (sigma_minus formula-decl nil sigma "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/") (real_times_real_is_real application-judgement "real" reals nil) (abs_mult formula-decl nil real_props nil) (connected_domain formula-decl nil integral_bounded nil) (connected? const-decl "bool" deriv_domain_def nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (integer nonempty-type-from-decl nil integers nil) (eq_partition const-decl "partition(a, b)" integral_def nil) (above nonempty-type-eq-decl nil integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil) (int_to_bnd-1 nil 3282561219 ("" (skosimp*) (("" (case "(FORALL (eps: posreal): (EXISTS (EP: partition[T](a!1,b!1)): (FORALL (j: below(length(EP)-1)): FORALL (xx: real): (EP(j) <= xx AND xx <= EP(j+1)) IMPLIES abs(f!1(xx) - f!1(EP(j))) < eps/abs(EP(j+1) - EP(j)))))") (("1" (assert) (("1" (inst - "1000") (("1" (skosimp*) (("1" (inst + "EP!1") (("1" (skosimp*) (("1" (inst - "j!1") (("1" (expand "bounded_on?") (("1" (inst + "1000 / abs(EP!1`seq(1 + j!1) - EP!1`seq(j!1)) + abs(f!1(EP!1`seq(j!1)))") (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (lemma "abs_diff") (("1" (inst - "f!1(x!1)" "f!1(EP!1`seq(j!1))") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "EP!1") (("2" (inst - "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (lemma "Lemma_1[T]") (("2" (inst?) (("2" (assert) (("2" (inst -1 "eps!1") (("2" (skosimp*) (("2" (name "EP" "eq_partition(a!1,b!1,floor((b!1-a!1)/delta!1) + 2)") (("1" (inst + "EP") (("1" (skosimp*) (("1" (case "T_pred(xx!1)") (("1" (case "abs(EP`seq(1 + j!1) - EP`seq(j!1)) > 0") (("1" (cross-mult 1) (("1" (hide -1) (("1" (name "SecJ" "(EP`seq(1 + j!1) - EP`seq(j!1))") (("1" (name "F_DIF" "(f!1((EP)(j!1)) - f!1(xx!1))") (("1" (assert) (("1" (rewrite "abs_mult" :dir rl) (("1" (case-replace "EP`seq(1 + j!1) * f!1(xx!1) - EP`seq(j!1) * f!1(xx!1) + (EP`seq(j!1) * f!1(EP`seq(j!1))- EP`seq(1 + j!1) * f!1(EP`seq(j!1))) = -SecJ*F_DIF") (("1" (hide -1) (("1" (lemma "abs_neg") (("1" (inst - "SecJ * F_DIF") (("1" (replace -1) (("1" (hide -1) (("1" (inst - "EP" "EP" "gxis(a!1,b!1,EP,j!1,true,xx!1)" "gxis(a!1,b!1,EP,j!1,false,xx!1)") (("1" (split -5) (("1" (expand "Rie_sum") (("1" (assert) (("1" (assert) (("1" (rewrite "sigma_minus[below[length(EP)-1]]") (("1" (case-replace "(LAMBDA (i: below(length(EP) - 1)): EP`seq(i) * f!1(gxis(a!1, b!1, EP, j!1, FALSE, xx!1)(i)) + EP`seq(1 + i) * f!1(gxis(a!1, b!1, EP, j!1, TRUE, xx!1)(i)) - EP`seq(i) * f!1(gxis(a!1, b!1, EP, j!1, TRUE, xx!1)(i)) - EP`seq(1 + i) * f!1(gxis(a!1, b!1, EP, j!1, FALSE, xx!1)(i))) = (LAMBDA (i: below(length(EP) - 1)): IF i = j!1 THEN (EP`seq(1 + j!1) - EP`seq(j!1)) * (f!1(EP(j!1)) - f!1(xx!1)) ELSE 0 ENDIF)") (("1" (assert) (("1" (hide -1) (("1" (case-replace "EP`seq(1 + j!1) * f!1(EP`seq(j!1)) - EP`seq(1 + j!1) * f!1(xx!1) + (EP`seq(j!1) * f!1(xx!1) - EP`seq(j!1) * f!1(EP`seq(j!1))) = SecJ*F_DIF") (("1" (hide -1) (("1" (case "j!1 < length(EP) - 2") (("1" (lemma "sigma_below[length(EP)-1].sigma_split_ge") (("1" (inst - "_" "length(EP) - 2" "0" "j!1") (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "sigma(1 + j!1, length(EP) - 2, (LAMBDA (i: below(length(EP) - 1)): IF i = j!1 THEN SecJ * F_DIF ELSE 0 ENDIF)) = 0") (("1" (hide -1) (("1" (rewrite "sigma_last_ge") (("1" (assert) (("1" (case "sigma(0, j!1 - 1, (LAMBDA (i: below(length(EP) - 1)): IF i = j!1 THEN SecJ * F_DIF ELSE 0 ENDIF)) = 0") (("1" (assert) nil nil) ("2" (lemma "sigma_restrict_eq[below(length(EP)-1)]") (("2" (inst?) (("1" (inst - "(LAMBDA (i: below(length(EP) - 1)): 0)") (("1" (expand "restrict") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_const[below(length(EP)-1)]") (("1" (inst?) (("1" (assert) nil nil) ("2" (expand "sigma") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "sigma") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (expand "sigma") (("4" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "sigma") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_restrict_eq[below(length(EP)-1)]") (("1" (inst?) (("1" (inst - "(LAMBDA (i: below(length(EP) - 1)): 0)") (("1" (expand "restrict") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_const[below(length(EP)-1)]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1 = length(EP) - 2") (("1" (rewrite "sigma_last_ge") (("1" (case-replace "sigma(0, length(EP) - 3, (LAMBDA (i: below(length(EP) - 1)): IF i = j!1 THEN SecJ * F_DIF ELSE 0 ENDIF)) = 0") (("1" (assert) nil nil) ("2" (lemma "sigma_restrict_eq[below(length(EP)-1)]") (("1" (inst?) (("1" (inst - "(LAMBDA (i: below(length(EP) - 1)): 0)") (("1" (expand "restrict") (("1" (assert) (("1" (lemma "sigma_const[below(length(EP)-1)]") (("1" (inst?) (("1" (assert) nil nil) ("2" (expand "sigma") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (expand "sigma") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (assert) (("4" (expand "sigma") (("4" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "sigma") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "gxis") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "gxis") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "N_from_delta") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("3" (lemma "N_from_delta") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "EP") (("2" (inst - "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "connected_domain") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "(b!1 - a!1) / delta!1 > 0") (("1" (assert) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (typepred "EP!1") (("3" (inst - "j!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (lemma "connected_domain") (("4" (inst - "_" "_" "xx!1") (("4" (inst?) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((partition type-eq-decl nil integral_def nil) (Lemma_1 formula-decl nil integral_prep nil) (gxis const-decl "(xis?(a, b, P))" integral_prep nil) (xis? const-decl "bool" integral_def nil) (N_from_delta formula-decl nil integral_def nil) (Rie_sum const-decl "real" integral_def nil) (sigma_split_ge formula-decl nil sigma_below "reals/") (sigma_restrict_eq formula-decl nil sigma "reals/") (sigma_const formula-decl nil sigma "reals/") (restrict const-decl "[T -> real]" sigma "reals/") (sigma_last_ge formula-decl nil sigma_below "reals/") (sigma def-decl "real" sigma "reals/") (sigma_minus formula-decl nil sigma "reals/") (eq_partition const-decl "partition(a, b)" integral_def nil)) nil)) (bounded_on_all?_TCC1 0 (bounded_on_all?_TCC1-1 nil 3280230043 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (bounded_on_all?_TCC2 0 (bounded_on_all?_TCC2-1 nil 3280230043 ("" (skosimp*) (("" (assert) nil nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (bounded_on_all_lem 0 (bounded_on_all_lem-3 nil 3306073138 ("" (skosimp*) (("" (lemma "int_to_bnd") (("" (inst?) (("" (assert) (("" (skosimp*) (("" (inst + "EP!1") (("" (expand "bounded_on_all?") (("" (skosimp*) (("" (inst - "j!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_to_bnd formula-decl nil integral_bounded nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans 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 "bool" 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) (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) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (T formal-subtype-decl nil integral_bounded nil) (T_pred const-decl "[real -> boolean]" integral_bounded 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) (bounded_on_all_lem-2 nil 3280237813 ("" (skosimp*) (("" (lemma "int_to_bnd[T]") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst + "EP!1") (("1" (expand "bounded_on_all?") (("1" (skosimp*) (("1" (inst - "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil) ((partition type-eq-decl nil integral_def nil)) nil) (bounded_on_all_lem-1 nil 3280237114 ("" (skosimp*) (("" (lemma "int_to_bnd_EE[T]") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst + "EP!1") (("1" (expand "bounded_on_all?") (("1" (skosimp*) (("1" (inst - "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil) ((partition type-eq-decl nil integral_def nil)) shostak)) (MINj_prep_TCC1 0 (MINj_prep_TCC1-1 nil 3280166020 ("" (skosimp*) (("" (assert) nil nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (MINj_prep 0 (MINj_prep-2 nil 3477651413 ("" (skosimp*) (("" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (typepred "P!1") (("1" (inst - "j!1") (("1" (case "T_pred((P!1`seq(1 + j!1) + P!1`seq(j!1)) / 2)") (("1" (inst - "f!1((P!1`seq(j!1) + P!1`seq(j!1+1))/2)") (("1" (inst + "(P!1`seq(j!1) + P!1`seq(j!1+1))/2") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (expand "connected?") (("2" (hide -2) (("2" (inst?) (("2" (inst - "P!1`seq(j!1)" "P!1`seq(j!1+1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "f!1") (("2" (expand "bounded?") (("2" (prop) (("1" (expand "bounded_above?") (("1" (expand "bounded_on_all?") (("1" (assert) (("1" (inst? -) (("1" (expand "bounded_on?") (("1" (skosimp*) (("1" (inst + "B!1") (("1" (expand "upper_bound?") (("1" (skosimp*) (("1" (typepred "s!1") (("1" (skosimp*) (("1" (replace -3) (("1" (hide -3) (("1" (inst?) (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_on_all?") (("2" (expand "bounded_below?") (("2" (assert) (("2" (inst? -) (("2" (expand "bounded_on?") (("2" (skosimp*) (("2" (inst + "-B!1") (("2" (expand "lower_bound?") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (skosimp*) (("2" (replace -3) (("2" (hide -3) (("2" (inst?) (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- 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) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T formal-subtype-decl nil integral_bounded nil) (T_pred const-decl "[real -> boolean]" integral_bounded nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (j!1 skolem-const-decl "below(P!1`length - 1)" integral_bounded nil) (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_bounded nil) (b!1 skolem-const-decl "{x: T | a!1 < x}" integral_bounded nil) (a!1 skolem-const-decl "T" integral_bounded nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (connected? const-decl "bool" deriv_domain_def nil) (connected_domain formula-decl nil integral_bounded nil) (member const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (bounded? const-decl "bool" bounded_real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (xx!1 skolem-const-decl "T" integral_bounded nil) (lower_bound? const-decl "bool" bounded_real_defs nil) (bounded_below? const-decl "bool" bounded_real_defs nil) (bounded_above? const-decl "bool" bounded_real_defs nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (bounded_on? const-decl "bool" integral_bounded nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (minus_real_is_real application-judgement "real" reals nil) (xx!1 skolem-const-decl "T" integral_bounded nil) (upper_bound? const-decl "bool" bounded_real_defs nil)) nil) (MINj_prep-1 nil 3280170323 ("" (skosimp*) (("" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (typepred "P!1") (("1" (inst - "j!1") (("1" (case "T_pred((P!1`seq(1 + j!1) + P!1`seq(j!1)) / 2)") (("1" (inst - "f!1((P!1`seq(j!1) + P!1`seq(j!1+1))/2)") (("1" (inst + "(P!1`seq(j!1) + P!1`seq(j!1+1))/2") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (hide -2) (("2" (inst?) (("2" (inst - "P!1`seq(j!1)" "P!1`seq(j!1+1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "f!1") (("2" (expand "bounded?") (("2" (prop) (("1" (expand "bounded_above?") (("1" (expand "bounded_on_all?") (("1" (assert) (("1" (inst? -) (("1" (expand "bounded_on?") (("1" (skosimp*) (("1" (inst + "B!1") (("1" (expand "upper_bound?") (("1" (skosimp*) (("1" (typepred "s!1") (("1" (skosimp*) (("1" (replace -3) (("1" (hide -3) (("1" (inst?) (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_on_all?") (("2" (expand "bounded_below?") (("2" (assert) (("2" (inst? -) (("2" (expand "bounded_on?") (("2" (skosimp*) (("2" (inst + "-B!1") (("2" (expand "lower_bound?") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (skosimp*) (("2" (replace -3) (("2" (hide -3) (("2" (inst?) (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((partition type-eq-decl nil integral_def nil)) shostak)) (MINj_TCC1 0 (MINj_TCC1-1 nil 3280165711 ("" (skosimp*) (("" (assert) nil nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (MINj_TCC2 0 (MINj_TCC2-1 nil 3280165712 ("" (skosimp*) (("" (lemma "MINj_prep") (("" (assert) (("" (inst?) (("" (flatten) (("" (assert) (("" (expand "bounded?") (("" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((MINj_prep formula-decl nil integral_bounded 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_bounded nil) (T formal-subtype-decl nil integral_bounded nil) (bool nonempty-type-eq-decl nil booleans 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) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (> const-decl "bool" 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) (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) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (bounded? const-decl "bool" bounded_real_defs nil)) shostak)) (MINj_lem 0 (MINj_lem-3 nil 3280236096 ("" (skosimp*) (("" (expand "MINj") (("" (name-replace "GLB" "glb({fx: real | EXISTS (xx: T): P!1`seq(j!1) <= xx AND xx <= P!1`seq(1 + j!1) AND fx = f!1(xx)})") (("1" (typepred "GLB") (("1" (expand "greatest_lower_bound?") (("1" (flatten) (("1" (hide -2) (("1" (expand "lower_bound?") (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "MINj_prep") (("2" (inst?) (("2" (flatten) (("2" (assert) (("2" (expand "bounded?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((MINj const-decl "real" integral_bounded nil) (bounded? const-decl "bool" bounded_real_defs nil) (MINj_prep formula-decl nil integral_bounded nil) (NOT const-decl "[bool -> bool]" booleans nil) (lower_bound? const-decl "bool" bounded_real_defs 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!1 skolem-const-decl "closed_interval[T](seq(P!1)(j!1), seq(P!1)(1 + j!1))" integral_bounded nil) (f!1 skolem-const-decl "(bounded_on_all?(a!1, b!1, P!1))" integral_bounded nil) (j!1 skolem-const-decl "below(length(P!1) - 1)" integral_bounded nil) (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_bounded nil) (b!1 skolem-const-decl "T" integral_bounded nil) (a!1 skolem-const-decl "T" integral_bounded nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (> const-decl "bool" reals 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) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T formal-subtype-decl nil integral_bounded nil) (T_pred const-decl "[real -> boolean]" integral_bounded nil) (glb const-decl "{x | greatest_lower_bound?(x, SB)}" bounded_real_defs nil) (greatest_lower_bound? const-decl "bool" bounded_real_defs nil) (bounded_below? const-decl "bool" bounded_real_defs nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets 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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)) nil) (MINj_lem-2 nil 3280234547 ("" (skosimp*) (("" (expand "MINj") (("" (name-replace "GLB" "glb({fx: real | EXISTS (xx: T): P!1`seq(j!1) < xx AND xx < P!1`seq(1 + j!1) AND fx = f!1(xx)})") (("1" (typepred "GLB") (("1" (expand "greatest_lower_bound?") (("1" (flatten) (("1" (hide -2) (("1" (expand "lower_bound?") (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "MINj_prep") (("2" (inst?) (("2" (flatten) (("2" (assert) (("2" (expand "bounded?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((partition type-eq-decl nil integral_def nil)) nil) (MINj_lem-1 nil 3280166943 ("" (skosimp*) (("" (expand "MINj") (("" (name-replace "GLB" "glb({fx: real | EXISTS (xx: T): P!1`seq(j!1) <= xx AND xx <= P!1`seq(1 + j!1) AND fx = f!1(xx)})") (("1" (typepred "GLB") (("1" (expand "greatest_lower_bound?") (("1" (flatten) (("1" (hide -2) (("1" (expand "lower_bound?") (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "MINj_prep") (("2" (inst?) (("1" (flatten) (("1" (assert) (("1" (expand "bounded?") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "is_bounded") (("2" (hide 2) (("2" (lemma "integrable_bounded") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((partition type-eq-decl nil integral_def nil)) shostak)) (MAXj_TCC1 0 (MAXj_TCC1-1 nil 3280165714 ("" (skosimp*) (("" (lemma "MINj_prep") (("" (inst?) (("" (flatten) (("" (expand "bounded?") (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((MINj_prep formula-decl nil integral_bounded nil) (bounded? const-decl "bool" bounded_real_defs nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals 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) (bool nonempty-type-eq-decl nil booleans nil) (T formal-subtype-decl nil integral_bounded nil) (T_pred const-decl "[real -> boolean]" integral_bounded 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)) (MAXj_lem 0 (MAXj_lem-4 nil 3280236216 ("" (skosimp*) (("" (expand "MAXj") (("" (name-replace "LUB" "lub({fx: real | EXISTS (xx: T): P!1`seq(j!1) <= xx AND xx <= P!1`seq(1 + j!1) AND fx = f!1(xx)})") (("1" (typepred "LUB") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (hide -2) (("1" (expand "upper_bound?") (("1" (inst - "f!1(x!1)") (("1" (assert) nil nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "MINj_prep") (("2" (inst?) (("2" (flatten) (("2" (expand "bounded?") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((MAXj const-decl "real" integral_bounded nil) (bounded? const-decl "bool" bounded_real_defs nil) (MINj_prep formula-decl nil integral_bounded nil) (NOT const-decl "[bool -> bool]" booleans nil) (upper_bound? const-decl "bool" bounded_real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (x!1 skolem-const-decl "closed_interval[T](seq(P!1)(j!1), seq(P!1)(1 + j!1))" integral_bounded nil) (f!1 skolem-const-decl "(bounded_on_all?(a!1, b!1, P!1))" integral_bounded nil) (j!1 skolem-const-decl "below(length(P!1) - 1)" integral_bounded nil) (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_bounded nil) (b!1 skolem-const-decl "T" integral_bounded nil) (a!1 skolem-const-decl "T" integral_bounded nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (> const-decl "bool" reals 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) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T formal-subtype-decl nil integral_bounded nil) (T_pred const-decl "[real -> boolean]" integral_bounded nil) (lub const-decl "{x | least_upper_bound?(x, SA)}" bounded_real_defs nil) (least_upper_bound? const-decl "bool" bounded_real_defs nil) (bounded_above? const-decl "bool" bounded_real_defs nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)) nil) (MAXj_lem-3 nil 3280234562 ("" (skosimp*) (("" (expand "MAXj") (("" (name-replace "LUB" "lub({fx: real | EXISTS (xx: T): P!1`seq(j!1) < xx AND xx < P!1`seq(1 + j!1) AND fx = f!1(xx)})") (("1" (typepred "LUB") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (hide -2) (("1" (expand "upper_bound?") (("1" (inst - "f!1(x!1)") (("1" (assert) nil nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "MINj_prep") (("2" (inst?) (("2" (flatten) (("2" (expand "bounded?") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((partition type-eq-decl nil integral_def nil)) nil) (MAXj_lem-2 nil 3280227504 ("" (skosimp*) (("" (expand "MAXj") (("" (name-replace "LUB" "lub({fx: real | EXISTS (xx: T): P!1`seq(j!1) <= xx AND xx <= P!1`seq(1 + j!1) AND fx = f!1(xx)})") (("1" (typepred "LUB") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (hide -2) (("1" (expand "upper_bound?") (("1" (inst - "f!1(x!1)") (("1" (assert) nil nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "MINj_prep") (("2" (inst?) (("1" (flatten) (("1" (expand "bounded?") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "is_bounded") (("2" (hide 2) (("2" (lemma "integrable_bounded") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((partition type-eq-decl nil integral_def nil)) nil) (MAXj_lem-1 nil 3280227458 ("" (skosimp*) (("" (expand "MAXj") (("" (name-replace "LUB" "glb({fx: real | EXISTS (xx: T): P!1`seq(j!1) <= xx AND xx <= P!1`seq(1 + j!1) AND fx = f!1(xx)})") (("1" (typepred "LUB") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (hide -2) (("1" (expand "upper_bound?") (("1" (inst?) (("1" (inst?) (("1" (assert) nil))))))))))))))) ("2" (hide 2) (("2" (lemma "MINj_prep") (("2" (inst?) (("1" (flatten) (("1" (assert) (("1" (expand "bounded?") (("1" (propax) nil))))))) ("2" (expand "is_bounded") (("2" (hide 2) (("2" (lemma "integrable_bounded") (("2" (inst?) (("2" (assert) nil)))))))))))))))))))) nil) nil nil)) (MIN_ALL_TCC1 0 (MIN_ALL_TCC1-1 nil 3280167808 ("" (skosimp*) (("" (prop) (("1" (lemma "is_finite_surj[real]") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (inst + "length(P!1) -1" "(LAMBDA (jj: below[length(P!1)-1]): MINj(a!1, b!1, P!1, jj, f!1))") (("1" (expand "surjective?") (("1" (skosimp*) (("1" (typepred "y!1") (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "MINj(a!1, b!1, P!1, 0, f!1)") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ((bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets 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) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil nat_types nil) (T_pred const-decl "[real -> boolean]" integral_bounded nil) (T formal-subtype-decl nil integral_bounded nil) (AND const-decl "[bool, bool -> bool]" booleans 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 "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (MINj const-decl "real" integral_bounded nil) (surjective? const-decl "bool" functions nil) (NOT const-decl "[bool -> bool]" booleans nil) (a!1 skolem-const-decl "T" integral_bounded nil) (b!1 skolem-const-decl "{x: T | a!1 < x}" integral_bounded nil) (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_bounded nil) (f!1 skolem-const-decl "(bounded_on_all?(a!1, b!1, P!1))" integral_bounded nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (is_finite_surj formula-decl nil finite_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) (member const-decl "bool" sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (empty? const-decl "bool" sets nil)) shostak)) (MAX_ALL_TCC1 0 (MAX_ALL_TCC1-2 nil 3280168363 ("" (skosimp*) (("" (prop) (("1" (lemma "is_finite_surj[real]") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (inst + "length(P!1) -1" "(LAMBDA (jj: below[length(P!1)-1]): MAXj(a!1, b!1, P!1, jj, f!1))") (("1" (expand "surjective?") (("1" (skosimp*) (("1" (typepred "y!1") (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "MAXj(a!1, b!1, P!1, 0, f!1)") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ((bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets 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) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil nat_types nil) (T_pred const-decl "[real -> boolean]" integral_bounded nil) (T formal-subtype-decl nil integral_bounded nil) (AND const-decl "[bool, bool -> bool]" booleans 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 "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (MAXj const-decl "real" integral_bounded nil) (surjective? const-decl "bool" functions nil) (NOT const-decl "[bool -> bool]" booleans nil) (a!1 skolem-const-decl "T" integral_bounded nil) (b!1 skolem-const-decl "{x: T | a!1 < x}" integral_bounded nil) (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_bounded nil) (f!1 skolem-const-decl "(bounded_on_all?(a!1, b!1, P!1))" integral_bounded nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (is_finite_surj formula-decl nil finite_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) (member const-decl "bool" sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (empty? const-decl "bool" sets nil)) nil) (MAX_ALL_TCC1-1 nil 3280167867 ("" (subtype-tcc) (("1" (postpone) nil nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil) ("5" (postpone) nil nil) ("6" (postpone) nil nil) ("7" (postpone) nil nil) ("8" (postpone) nil nil) ("9" (postpone) nil nil) ("10" (postpone) nil nil) ("11" (postpone) nil nil) ("12" (postpone) nil nil) ("13" (postpone) nil nil) ("14" (postpone) nil nil)) nil) nil shostak)) (MIN_ALL_lem 0 (MIN_ALL_lem-1 nil 3280232267 ("" (skosimp*) (("" (lemma "part_in[T]") (("" (inst - "a!1" "b!1" "x!1" "P!1") (("" (assert) (("" (skosimp*) (("" (expand "MIN_ALL") (("" (lemma "MINj_lem") (("" (inst - "a!1" "b!1") (("" (assert) (("" (inst - "P!1" "f!1" "ii!1" "x!1") (("1" (assert) (("1" (typepred "min({mm: real | EXISTS (jj: below(length(P!1) - 1)): mm = MINj(a!1, b!1, P!1, jj, f!1)})") (("1" (skosimp*) (("1" (inst -2 "MINj(a!1, b!1, P!1, ii!1, f!1)") (("1" (assert) (("1" (hide 2) (("1" (inst + "ii!1") nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "MIN_ALL_TCC1") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-subtype-decl nil integral_bounded nil) (T_pred const-decl "[real -> boolean]" integral_bounded 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) (part_in 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) (MIN_ALL const-decl "real" integral_bounded nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (MINj const-decl "real" integral_bounded nil) (min const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}" finite_sets_minmax "finite_sets/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (MIN_ALL_TCC1 subtype-tcc nil integral_bounded nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (MINj_lem formula-decl nil integral_bounded nil) (partition type-eq-decl nil integral_def nil) (finite_sequence type-eq-decl nil finite_sequences nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil)) shostak)) (MAX_ALL_lem 0 (MAX_ALL_lem-2 nil 3280236321 ("" (skosimp*) (("" (lemma "part_in[T]") (("" (inst - "a!1" "b!1" "x!1" "P!1") (("" (assert) (("" (skosimp*) (("" (expand "MAX_ALL") (("" (lemma "MAXj_lem") (("" (inst - "a!1" "b!1") (("" (assert) (("" (inst - "P!1" "f!1" "ii!1" "x!1") (("" (assert) (("" (typepred "max({mm: real | EXISTS (jj: below(length(P!1) - 1)): mm = MAXj(a!1, b!1, P!1, jj, f!1)})") (("1" (skosimp*) (("1" (inst -2 "MAXj(a!1, b!1, P!1, ii!1, f!1)") (("1" (assert) (("1" (hide 2) (("1" (inst + "ii!1") nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "MAX_ALL_TCC1") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-subtype-decl nil integral_bounded nil) (T_pred const-decl "[real -> boolean]" integral_bounded 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) (part_in formula-decl nil integral_def 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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (MAX_ALL const-decl "real" integral_bounded nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (MAXj const-decl "real" integral_bounded nil) (max const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" finite_sets_minmax "finite_sets/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (MAX_ALL_TCC1 subtype-tcc nil integral_bounded nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (MAXj_lem formula-decl nil integral_bounded nil) (partition type-eq-decl nil integral_def nil) (finite_sequence type-eq-decl nil finite_sequences nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil)) nil) (MAX_ALL_lem-1 nil 3280236256 ("" (skosimp*) (("" (lemma "part_in[T]") (("" (inst - "a!1" "b!1" "x!1" "P!1") (("" (assert) (("" (skosimp*) (("" (expand "MAX_ALL") (("" (lemma "MAXj_lem") (("" (inst - "a!1" "b!1") (("" (assert) (("" (inst - "P!1" "f!1" "ii!1" "x!1") (("1" (assert) (("1" (typepred "min({mm: real | EXISTS (jj: below(length(P!1) - 1)): mm = MAXj(a!1, b!1, P!1, jj, f!1)})") (("1" (skosimp*) (("1" (inst -2 "MAXj(a!1, b!1, P!1, ii!1, f!1)") (("1" (assert) (("1" (hide 2) (("1" (inst + "ii!1") nil))))))))) ("2" (hide 2) (("2" (lemma "MAX_ALL_TCC1") (("2" (inst?) nil))))))))) ("2" (postpone) nil)))))))))))))))))))) nil) nil nil)) (bounded_on_all_is 0 (bounded_on_all_is-1 nil 3280238950 ("" (skosimp*) (("" (lemma "bounded_on_all_lem") (("" (inst?) (("" (assert) (("" (expand "bounded_on?") (("" (inst + "max(abs(MIN_ALL(a!1,b!1,P!1,f!1)), abs(MAX_ALL(a!1,b!1,P!1,f!1)))") (("" (skosimp*) (("" (lemma "MAX_ALL_lem") (("" (inst?) (("" (assert) (("" (inst?) (("" (inst?) (("" (lemma "MIN_ALL_lem") (("" (inst?) (("" (assert) (("" (inst?) (("" (inst?) (("" (hide -3 -5) (("" (grind :exclude ("MAX_ALL" "MIN_ALL")) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_on_all_lem formula-decl nil integral_bounded nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (< const-decl "bool" reals nil) (partition type-eq-decl nil 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 "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities 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) (bounded_on_all? const-decl "bool" integral_bounded nil) (MIN_ALL const-decl "real" integral_bounded nil) (MAX_ALL const-decl "real" integral_bounded nil) (MAX_ALL_lem formula-decl nil integral_bounded nil) (nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs 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) (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (MIN_ALL_lem formula-decl nil integral_bounded nil) (bounded_on? const-decl "bool" integral_bounded nil) (T formal-subtype-decl nil integral_bounded nil) (T_pred const-decl "[real -> boolean]" integral_bounded 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)) (integrable_bounded 0 (integrable_bounded-1 nil 3280227717 ("" (skosimp*) (("" (lemma "bounded_on_all_lem") (("" (inst?) (("" (assert) (("" (skosimp*) (("" (lemma "bounded_on_all_is") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_on_all_lem formula-decl nil integral_bounded nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (bounded_on_all_is formula-decl nil integral_bounded nil) (T formal-subtype-decl nil integral_bounded nil) (T_pred const-decl "[real -> boolean]" integral_bounded 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)) (bnd_on_lem 0 (bnd_on_lem-1 nil 3282500824 ("" (skosimp*) (("" (expand "bounded_on_all?") (("" (skosimp*) (("" (assert) (("" (expand "bounded_on?") (("" (skosimp*) (("" (inst + "B!1") (("" (skosimp*) (("" (inst?) (("" (assert) (("" (typepred "x!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_on_all? const-decl "bool" integral_bounded nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (a!1 skolem-const-decl "T" integral_bounded nil) (b!1 skolem-const-decl "T" integral_bounded nil) (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_bounded nil) (j!1 skolem-const-decl "below(P!1`length - 1)" integral_bounded nil) (x!1 skolem-const-decl "closed_interval[T](P!1`seq(j!1), P!1`seq(1 + j!1))" integral_bounded nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-subtype-decl nil integral_bounded nil) (T_pred const-decl "[real -> boolean]" integral_bounded nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props 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) (bounded_on? const-decl "bool" integral_bounded nil)) nil)) (integrable_bounded_on_all 0 (integrable_bounded_on_all-3 nil 3306073181 ("" (skosimp*) (("" (lemma "integrable_bounded") (("" (inst?) (("" (assert) (("" (lemma "bnd_on_lem") (("" (inst?) (("" (assert) (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((integrable_bounded formula-decl nil integral_bounded nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals 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) (bool nonempty-type-eq-decl nil booleans nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (bnd_on_lem formula-decl nil integral_bounded nil) (T formal-subtype-decl nil integral_bounded nil) (T_pred const-decl "[real -> boolean]" integral_bounded 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) (integrable_bounded_on_all-2 nil 3282500899 ("" (skosimp*) (("" (lemma "integrable_bounded[T]") (("" (inst?) (("" (assert) (("" (lemma "bnd_on_lem") (("" (inst?) (("" (assert) (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((partition type-eq-decl nil integral_def nil)) nil) (integrable_bounded_on_all-1 nil 3282500856 ("" (skosimp*) (("" (expand "bounded_on_all?") (("" (skosimp*) (("" (assert) (("" (expand "bounded_on?") (("" (skosimp*) (("" (inst + "B!1") (("" (skosimp*) (("" (inst?) (("" (assert) (("" (typepred "x!1") (("" (assert) nil)))))))))))))))))))))) nil) nil nil)))
[Konzepte0.128Was zu einem Entwurf gehörtWie die Entwicklung von Software durchgeführt wird2026-04-30] |
||||||
2026-05-26