| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 949 kB |
|
Quelle integral_split.prfSprache: Lisp |
|||||||||||||||
|
(integral_split (partition_join_TCC1 0 (partition_join_TCC1-1 nil 3281885132 ("" (lemma "connected_domain") (("" (skosimp*) nil nil)) nil) ((connected_domain formula-decl nil integral_split nil)) shostak)) (partition_join_TCC2 0 (partition_join_TCC2-1 nil 3282313772 ("" (lemma "not_one_element") (("" (assert) nil nil)) nil) ((not_one_element formula-decl nil integral_split nil)) shostak)) (partition_join_TCC3 0 (partition_join_TCC3-1 nil 3282313772 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (partition_join 0 (partition_join-3 nil 3399973962 ("" (auto-rewrite "xis?") (("" (auto-rewrite "xis_lem") (("" (skosimp*) (("" (typepred "xisa!1") (("" (typepred "xisb!1") (("" (expand "xis?") (("" (assert) (("" (inst + "UUPart(a!1,b!1,c!1,Pa!1,Pb!1)" "xisa!1 o xisb!1") (("1" (split +) (("1" (hide -1 -2) (("1" (expand "width") (("1" (lemma "connected_domain") (("1" (name "LUU" "{l: real | EXISTS (ii: below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)): l = seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(1 + ii) - seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(ii)}") (("1" (replace -1) (("1" (case "is_finite[real](LUU) AND NOT empty?[real](LUU)") (("1" (name "LA" "{l: real | EXISTS (ii: below(length(Pa!1) - 1)): l = seq(Pa!1)(1 + ii) - seq(Pa!1)(ii)}") (("1" (replace -1) (("1" (name "LB" "{l: real | EXISTS (ii: below(length(Pb!1) - 1)): l = seq(Pb!1)(1 + ii) - seq(Pb!1)(ii)}") (("1" (replace -1) (("1" (case "is_finite[real](LA) AND NOT empty?[real](LA)") (("1" (case "is_finite[real](LB) AND NOT empty?[real](LB)") (("1" (typepred "max(LUU)") (("1" (replace -8 -1 rl) (("1" (assert) (("1" (skosimp*) (("1" (replace -8) (("1" (replace -1) (("1" (hide -1) (("1" (expand "UUPart") (("1" (ground) (("1" (lift-if) (("1" (case "1 + ii!1 < length(Pa!1)") (("1" (assert) (("1" (typepred "max(LA)") (("1" (inst -2 "Pa!1`seq(1 + ii!1) - Pa!1`seq(ii!1)") (("1" (assert) (("1" (replace -7 + rl) (("1" (assert) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lift-if) (("2" (case-replace "ii!1 = length(Pa!1) - 1") (("1" (case-replace "Pa!1`seq(length(Pa!1) - 1) = Pb!1`seq(0)") (("1" (assert) (("1" (typepred "max(LB)") (("1" (replace -8 -1 rl) (("1" (assert) (("1" (skosimp*) (("1" (replace -8) (("1" (inst -2 "Pb!1`seq(1) - Pb!1`seq(0)") (("1" (assert) (("1" (replace -7 + rl) (("1" (assert) (("1" (inst 1 "0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) (("2" (typepred "max(LB)") (("2" (replace -6 -1 rl) (("2" (assert) (("2" (skosimp*) (("2" (replace -6) (("2" (inst -2 "Pb!1`seq(2 - length(Pa!1) + ii!1) - Pb!1`seq(1 - length(Pa!1) + ii!1)") (("2" (assert) (("2" (replace -5 1 rl) (("2" (assert) (("2" (inst 1 "1-length(Pa!1)+ii!1") (("1" (assert) nil nil) ("2" (assert) (("2" (hide -5 -6 -8) (("2" (hide -2 -3 -4 -5 -6) (("2" (typepred "ii!1") (("2" (assert) (("2" (expand "UUPart") (("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) ("2" (replace -2 * rl) (("2" (hide-all-but 1) (("2" (split +) (("1" (lemma "is_finite_surj") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (inst + "length(Pb!1)-1" "(LAMBDA (ii: below(length(Pb!1) - 1)): seq(Pb!1)(1 + ii) - seq(Pb!1)(ii))") (("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 - "seq(Pb!1)(1) - seq(Pb!1)(0)") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -2 * rl) (("2" (hide-all-but 1) (("2" (split +) (("1" (lemma "is_finite_surj") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (inst + "length(Pa!1)-1" "(LAMBDA (ii: below(length(Pa!1) - 1)): seq(Pa!1)(1 + ii) - seq(Pa!1)(ii))") (("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" (inst - "seq(Pa!1)(1) - seq(Pa!1)(0)") (("2" (expand "member") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (hide-all-but 1) (("2" (split +) (("1" (lemma "is_finite_surj") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (inst + "length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))-1" "(LAMBDA (ii: below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)): seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(1 + ii) - seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(ii))") (("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) ("3" (lemma "connected_domain") (("3" (skosimp*) nil nil)) nil) ("4" (expand "UUPart") (("4" (assert) nil nil)) nil) ("5" (lemma "connected_domain") (("5" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(1) - seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(0)") (("1" (assert) (("1" (inst + "0") (("1" (assert) nil nil) ("2" (expand "UUPart") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "UUPart") (("2" (assert) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil) ("4" (expand "UUPart") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2) (("2" (expand "Rie_sum") (("2" (assert) (("1" (case " length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) = length(Pa!1) + length(Pb!1) - 1") (("1" (same-name "sigma[below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)]" "sigma[below(length(Pa!1) + length(Pb!1) - 2)]") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (lemma "sigma_split[below(length(Pa!1) + length(Pb!1) - 2)]") (("1" (inst?) (("1" (assert) (("1" (inst - "length(Pa!1) - 2") (("1" (assert) (("1" (replace -2) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "sigma[below(length(Pa!1) + length(Pb!1) - 2)].sigma(0, length(Pa!1) - 2, LAMBDA (n: below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)): UUPart(a!1, b!1, c!1, Pa!1, Pb!1)`seq(1 + n) * f!1((concat_arrays.o(xisa!1, xisb!1))(n)) - UUPart(a!1, b!1, c!1, Pa!1, Pb!1)`seq(n) * f!1((concat_arrays.o(xisa!1, xisb!1))(n))) = sigma[below(length(Pa!1) - 1)] (0, length(Pa!1) - 2, LAMBDA (n: below(length(Pa!1) - 1)): Pa!1`seq(1 + n) * f!1(xisa!1(n)) - Pa!1`seq(n) * f!1(xisa!1(n)))") (("1" (assert) (("1" (hide -1) (("1" (lemma "sigma_diff_shift[length(Pb!1) - 1,length(Pa!1) + length(Pb!1) - 2 ]") (("1" (inst - "(LAMBDA (n: below(length(Pb!1) - 1)): Pb!1`seq(1 + n) * f!1(xisb!1(n)) - Pb!1`seq(n) * f!1(xisb!1(n)))" "(LAMBDA (n: below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)): UUPart(a!1, b!1, c!1, Pa!1, Pb!1)`seq(1 + n) * f!1((concat_arrays.o(xisa!1, xisb!1))(n)) - UUPart(a!1, b!1, c!1, Pa!1, Pb!1)`seq(n) * f!1((concat_arrays.o(xisa!1, xisb!1))(n)))" "length(Pa!1) - 1" "length(Pb!1) - 2" "0") (("1" (assert) (("1" (hide 2) (("1" (skosimp*) (("1" (expand "UUPart") (("1" (assert) (("1" (expand "o ") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (ground) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "connected_domain") (("3" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_diff_eq[length(Pa!1) + length(Pb!1) - 2 ,length(Pa!1) - 1]") (("2" (lemma "connected_domain") (("2" (lemma "sigma_diff_eq[length(Pa!1) + length(Pb!1) - 2 ,length(Pa!1) - 1]") (("2" (inst?) (("1" (assert) (("1" (hide 2) (("1" (skosimp*) (("1" (expand "UUPart") (("1" (assert) (("1" (expand "o ") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (ground) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (lemma "connected_domain") (("4" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil) ("3" (assert) (("3" (hide 2) (("3" (skosimp*) (("3" (ground) nil nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (lemma "connected_domain") (("4" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "UUPart") (("2" (propax) 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) ("2" (expand "UUPart") (("2" (propax) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (assert) nil nil)) nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (skosimp*) (("1" (expand "UUPart") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "o") (("2" (assert) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (typepred "ii!1") (("3" (expand "UUPart") (("3" (expand "o") (("3" (case-replace "ii!1 < length(Pa!1) - 1") (("1" (inst -4 "ii!1") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (inst -2 "1 - length(Pa!1) + ii!1") (("2" (assert) (("2" (flatten) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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/") (xis? const-decl "bool" 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) (<= 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) (T formal-nonempty-subtype-decl nil integral_split nil) (T_pred const-decl "[real -> boolean]" integral_split 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (connected? const-decl "bool" deriv_domain_def nil) (xisb!1 skolem-const-decl "(xis?(b!1, c!1, Pb!1))" integral_split nil) (xisa!1 skolem-const-decl "(xis?(a!1, b!1, Pa!1))" integral_split nil) (O const-decl "below_array[n + m, T]" concat_arrays "structures/") (below_array type-eq-decl nil below_arrays "structures/") (UUPart const-decl "partition[T](a, c)" step_fun_props nil) (Pb!1 skolem-const-decl "partition[T](b!1, c!1)" integral_split nil) (c!1 skolem-const-decl "T" integral_split nil) (Pa!1 skolem-const-decl "partition[T](a!1, b!1)" integral_split nil) (b!1 skolem-const-decl "T" integral_split nil) (a!1 skolem-const-decl "T" integral_split nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (not_one_element formula-decl nil integral_split nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (integer nonempty-type-from-decl nil integers nil) (sigma_split formula-decl nil sigma "reals/") (sigma_diff_eq formula-decl nil sigma_below_sub "reals/") (sigma_diff_shift formula-decl nil sigma_below_sub "reals/") (sigma def-decl "real" sigma "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (Rie_sum const-decl "real" integral_def nil) (real_times_real_is_real application-judgement "real" reals nil) (connected_domain formula-decl nil integral_split nil) (surjective? const-decl "bool" functions nil) (is_finite_surj formula-decl nil finite_sets nil) (member const-decl "bool" sets nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (finite_set type-eq-decl nil finite_sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (max const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" finite_sets_minmax "finite_sets/") (ii!1 skolem-const-decl "below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)" integral_split nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (empty? const-decl "bool" sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (not_one_element? const-decl "bool" deriv_domain_def nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (width const-decl "posreal" integral_def nil) (ii!1 skolem-const-decl "below(length(UUPart[T](a!1, b!1, c!1, Pa!1, Pb!1)) - 1)" integral_split nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil) (partition_join-2 nil 3306066580 ("" (skosimp*) (("" (typepred "xisa!1") (("" (typepred "xisb!1") (("" (expand "xis?") (("" (assert) (("" (inst + "UUPart(a!1,b!1,c!1,Pa!1,Pb!1)" "xisa!1 o xisb!1") (("1" (split +) (("1" (hide -1 -2) (("1" (expand "width") (("1" (lemma "connected_domain") (("1" (name "LUU" "{l: real | EXISTS (ii: below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)): l = seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(1 + ii) - seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(ii)}") (("1" (replace -1) (("1" (case "is_finite[real](LUU) AND NOT empty?[real](LUU)") (("1" (name "LA" "{l: real | EXISTS (ii: below(length(Pa!1) - 1)): l = seq(Pa!1)(1 + ii) - seq(Pa!1)(ii)}") (("1" (replace -1) (("1" (name "LB" "{l: real | EXISTS (ii: below(length(Pb!1) - 1)): l = seq(Pb!1)(1 + ii) - seq(Pb!1)(ii)}") (("1" (replace -1) (("1" (case "is_finite[real](LA) AND NOT empty?[real](LA)") (("1" (case "is_finite[real](LB) AND NOT empty?[real](LB)") (("1" (typepred "max(LUU)") (("1" (replace -8 -1 rl) (("1" (assert) (("1" (skosimp*) (("1" (replace -8) (("1" (replace -1) (("1" (hide -1) (("1" (expand "UUPart") (("1" (ground) (("1" (lift-if) (("1" (case "1 + ii!1 < length(Pa!1)") (("1" (assert) (("1" (typepred "max(LA)") (("1" (inst -2 "Pa!1`seq(1 + ii!1) - Pa!1`seq(ii!1)") (("1" (assert) (("1" (replace -7 + rl) (("1" (assert) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lift-if) (("2" (case-replace "ii!1 = length(Pa!1) - 1") (("1" (case-replace "Pa!1`seq(length(Pa!1) - 1) = Pb!1`seq(0)") (("1" (assert) (("1" (typepred "max(LB)") (("1" (replace -8 -1 rl) (("1" (assert) (("1" (skosimp*) (("1" (replace -8) (("1" (inst -2 "Pb!1`seq(1) - Pb!1`seq(0)") (("1" (assert) (("1" (replace -7 + rl) (("1" (assert) (("1" (inst 1 "0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) (("2" (typepred "max(LB)") (("2" (replace -6 -1 rl) (("2" (assert) (("2" (skosimp*) (("2" (replace -6) (("2" (inst -2 "Pb!1`seq(2 - length(Pa!1) + ii!1) - Pb!1`seq(1 - length(Pa!1) + ii!1)") (("2" (assert) (("2" (replace -5 1 rl) (("2" (assert) (("2" (inst 1 "1-length(Pa!1)+ii!1") (("1" (assert) nil nil) ("2" (assert) (("2" (hide -5 -6 -8) (("2" (hide -2 -3 -4 -5 -6) (("2" (typepred "ii!1") (("2" (assert) (("2" (expand "UUPart") (("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) ("2" (replace -2 * rl) (("2" (hide-all-but 1) (("2" (split +) (("1" (lemma "is_finite_surj") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (inst + "length(Pb!1)-1" "(LAMBDA (ii: below(length(Pb!1) - 1)): seq(Pb!1)(1 + ii) - seq(Pb!1)(ii))") (("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 - "seq(Pb!1)(1) - seq(Pb!1)(0)") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -2 * rl) (("2" (hide-all-but 1) (("2" (split +) (("1" (lemma "is_finite_surj") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (inst + "length(Pa!1)-1" "(LAMBDA (ii: below(length(Pa!1) - 1)): seq(Pa!1)(1 + ii) - seq(Pa!1)(ii))") (("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" (inst - "seq(Pa!1)(1) - seq(Pa!1)(0)") (("2" (expand "member") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (hide-all-but 1) (("2" (split +) (("1" (lemma "is_finite_surj") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (inst + "length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))-1" "(LAMBDA (ii: below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)): seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(1 + ii) - seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(ii))") (("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) ("3" (lemma "connected_domain") (("3" (skosimp*) nil nil)) nil) ("4" (expand "UUPart") (("4" (assert) nil nil)) nil) ("5" (lemma "connected_domain") (("5" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "connected_domain") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(1) - seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(0)") (("1" (assert) (("1" (inst + "0") (("1" (assert) nil nil) ("2" (expand "UUPart") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "UUPart") (("2" (assert) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil) ("4" (expand "UUPart") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2) (("2" (expand "Rie_sum") (("2" (assert) (("2" (case " length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) = length(Pa!1) + length(Pb!1) - 1") (("1" (same-name "sigma[below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)]" "sigma[below(length(Pa!1) + length(Pb!1) - 2)]") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (lemma "sigma_split[below(length(Pa!1) + length(Pb!1) - 2)]") (("1" (inst?) (("1" (assert) (("1" (inst - "length(Pa!1) - 2") (("1" (assert) (("1" (replace -2) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "sigma[below(length(Pa!1) + length(Pb!1) - 2)].sigma(0, length(Pa!1) - 2, LAMBDA (n: below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)): UUPart(a!1, b!1, c!1, Pa!1, Pb!1)`seq(1 + n) * f!1((xisa!1 o xisb!1)(n)) - UUPart(a!1, b!1, c!1, Pa!1, Pb!1)`seq(n) * f!1((xisa!1 o xisb!1)(n))) = sigma[below(length(Pa!1) - 1)] (0, length(Pa!1) - 2, LAMBDA (n: below(length(Pa!1) - 1)): Pa!1`seq(1 + n) * f!1(xisa!1(n)) - Pa!1`seq(n) * f!1(xisa!1(n)))") (("1" (assert) (("1" (hide -1) (("1" (lemma "sigma_diff_shift[length(Pb!1) - 1,length(Pa!1) + length(Pb!1) - 2 ]") (("1" (inst - "(LAMBDA (n: below(length(Pb!1) - 1)): Pb!1`seq(1 + n) * f!1(xisb!1(n)) - Pb!1`seq(n) * f!1(xisb!1(n)))" "(LAMBDA (n: below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)): UUPart(a!1, b!1, c!1, Pa!1, Pb!1)`seq(1 + n) * f!1((xisa!1 o xisb!1)(n)) - UUPart(a!1, b!1, c!1, Pa!1, Pb!1)`seq(n) * f!1((xisa!1 o xisb!1)(n)))" "length(Pa!1) - 1" "length(Pb!1) - 2" "0") (("1" (assert) (("1" (hide 2) (("1" (skosimp*) (("1" (expand "UUPart") (("1" (assert) (("1" (expand "o ") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (ground) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "connected_domain") (("3" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_diff_eq[length(Pa!1) + length(Pb!1) - 2 ,length(Pa!1) - 1]") (("2" (inst?) (("1" (assert) (("1" (hide 2) (("1" (skosimp*) (("1" (expand "UUPart") (("1" (assert) (("1" (expand "o ") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (ground) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "connected_domain") (("3" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (lemma "connected_domain") (("4" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (hide 2) (("3" (replace -1) (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (lemma "connected_domain") (("4" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "UUPart") (("2" (propax) 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) ("2" (expand "UUPart") (("2" (propax) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (skosimp*) (("1" (expand "UUPart") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "o") (("2" (assert) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (typepred "ii!1") (("3" (expand "UUPart") (("3" (expand "o") (("3" (case-replace "ii!1 < length(Pa!1) - 1") (("1" (inst -4 "ii!1") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (inst -2 "1 - length(Pa!1) + ii!1") (("2" (assert) (("2" (flatten) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((partition type-eq-decl nil integral_def nil) (xis? const-decl "bool" integral_def nil) (O const-decl "below_array[n + m, T]" concat_arrays "structures/") (below_array type-eq-decl nil below_arrays "structures/") (UUPart const-decl "partition[T](a, c)" step_fun_props nil) (sigma_split formula-decl nil sigma "reals/") (sigma_diff_eq formula-decl nil sigma_below_sub "reals/") (sigma_diff_shift formula-decl nil sigma_below_sub "reals/") (sigma def-decl "real" sigma "reals/") (Rie_sum const-decl "real" integral_def nil) (is_finite_surj formula-decl nil finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (max const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" finite_sets_minmax "finite_sets/") (is_finite const-decl "bool" finite_sets nil) (width const-decl "posreal" integral_def nil)) nil) (partition_join-1 nil 3281886253 ("" (skosimp*) (("" (typepred "xisa!1") (("" (typepred "xisb!1") (("" (expand "xis?") (("" (assert) (("" (inst + "UUPart(a!1,b!1,c!1,Pa!1,Pb!1)" "xisa!1 o xisb!1") (("1" (split +) (("1" (hide -1 -2) (("1" (expand "width") (("1" (lemma "connected_domain") (("1" (name "LUU" "{l: real | EXISTS (ii: below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)): l = seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(1 + ii) - seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(ii)}") (("1" (replace -1) (("1" (case "is_finite[real](LUU) AND NOT empty?[real](LUU)") (("1" (name "LA" "{l: real | EXISTS (ii: below(length(Pa!1) - 1)): l = seq(Pa!1)(1 + ii) - seq(Pa!1)(ii)}") (("1" (replace -1) (("1" (name "LB" "{l: real | EXISTS (ii: below(length(Pb!1) - 1)): l = seq(Pb!1)(1 + ii) - seq(Pb!1)(ii)}") (("1" (replace -1) (("1" (case "is_finite[real](LA) AND NOT empty?[real](LA)") (("1" (case "is_finite[real](LB) AND NOT empty?[real](LB)") (("1" (typepred "max(LUU)") (("1" (replace -8 -1 rl) (("1" (assert) (("1" (skosimp*) (("1" (replace -8) (("1" (replace -1) (("1" (hide -1) (("1" (expand "UUPart") (("1" (ground) (("1" (lift-if) (("1" (case "1 + ii!1 < length(Pa!1)") (("1" (assert) (("1" (typepred "max(LA)") (("1" (inst -2 "Pa!1`seq(1 + ii!1) - Pa!1`seq(ii!1)") (("1" (assert) (("1" (replace -7 + rl) (("1" (assert) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lift-if) (("2" (case-replace "ii!1 = length(Pa!1) - 1") (("1" (case-replace "Pa!1`seq(length(Pa!1) - 1) = Pb!1(0)") (("1" (assert) (("1" (typepred "max(LB)") (("1" (replace -8 -1 rl) (("1" (assert) (("1" (skosimp*) (("1" (replace -8) (("1" (inst -2 "Pb!1`seq(1) - Pb!1`seq(0)") (("1" (assert) (("1" (replace -7 + rl) (("1" (assert) (("1" (inst 1 "0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) (("2" (typepred "max(LB)") (("2" (replace -6 -1 rl) (("2" (assert) (("2" (skosimp*) (("2" (replace -6) (("2" (inst -2 "Pb!1`seq(2 - length(Pa!1) + ii!1) - Pb!1`seq(1 - length(Pa!1) + ii!1)") (("1" (assert) (("1" (replace -5 1 rl) (("1" (assert) (("1" (inst 1 "1-length(Pa!1)+ii!1") (("1" (assert) nil nil) ("2" (assert) (("2" (typepred "ii!1") (("2" (expand "UUPart") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "ii!1") (("2" (expand "UUPart") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "ii!1") (("3" (expand "UUPart") (("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) ("2" (propax) nil nil)) nil) ("2" (replace -2 * rl) (("2" (hide-all-but 1) (("2" (split +) (("1" (lemma "is_finite_surj") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (inst + "length(Pb!1)-1" "(LAMBDA (ii: below(length(Pb!1) - 1)): seq(Pb!1)(1 + ii) - seq(Pb!1)(ii))") (("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 - "seq(Pb!1)(1) - seq(Pb!1)(0)") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -2 * rl) (("2" (hide-all-but 1) (("2" (split +) (("1" (lemma "is_finite_surj") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (inst + "length(Pa!1)-1" "(LAMBDA (ii: below(length(Pa!1) - 1)): seq(Pa!1)(1 + ii) - seq(Pa!1)(ii))") (("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" (inst - "seq(Pa!1)(1) - seq(Pa!1)(0)") (("2" (expand "member") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (hide-all-but 1) (("2" (split +) (("1" (lemma "is_finite_surj") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (inst + "length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))-1" "(LAMBDA (ii: below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)): seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(1 + ii) - seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(ii))") (("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) ("3" (lemma "connected_domain") (("3" (skosimp*) nil nil)) nil) ("4" (expand "UUPart") (("4" (assert) nil nil)) nil) ("5" (lemma "connected_domain") (("5" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "connected_domain") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(1) - seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(0)") (("1" (assert) (("1" (inst + "0") (("1" (assert) nil nil) ("2" (expand "UUPart") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "UUPart") (("2" (assert) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil) ("4" (expand "UUPart") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2) (("2" (expand "Rie_sum") (("2" (assert) (("2" (case " length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) = length(Pa!1) + length(Pb!1) - 1") (("1" (same-name "sigma[below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)]" "sigma[below(length(Pa!1) + length(Pb!1) - 2)]") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (lemma "sigma_split[below(length(Pa!1) + length(Pb!1) - 2)]") (("1" (inst?) (("1" (assert) (("1" (inst - "length(Pa!1) - 2") (("1" (assert) (("1" (replace -2) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "sigma[below(length(Pa!1) + length(Pb!1) - 2)].sigma(0, length(Pa!1) - 2, LAMBDA (n: below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)): UUPart(a!1, b!1, c!1, Pa!1, Pb!1)`seq(1 + n) * f!1((xisa!1 o xisb!1)(n)) - UUPart(a!1, b!1, c!1, Pa!1, Pb!1)`seq(n) * f!1((xisa!1 o xisb!1)(n))) = sigma[below(length(Pa!1) - 1)] (0, length(Pa!1) - 2, LAMBDA (n: below(length(Pa!1) - 1)): Pa!1`seq(1 + n) * f!1(xisa!1(n)) - Pa!1`seq(n) * f!1(xisa!1(n)))") (("1" (assert) (("1" (hide -1) (("1" (lemma "sigma_diff_shift[length(Pb!1) - 1,length(Pa!1) + length(Pb!1) - 2 ]") (("1" (inst - "(LAMBDA (n: below(length(Pb!1) - 1)): Pb!1`seq(1 + n) * f!1(xisb!1(n)) - Pb!1`seq(n) * f!1(xisb!1(n)))" "(LAMBDA (n: below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)): UUPart(a!1, b!1, c!1, Pa!1, Pb!1)`seq(1 + n) * f!1((xisa!1 o xisb!1)(n)) - UUPart(a!1, b!1, c!1, Pa!1, Pb!1)`seq(n) * f!1((xisa!1 o xisb!1)(n)))" "length(Pa!1) - 1" "length(Pb!1) - 2" "0") (("1" (assert) (("1" (hide 2) (("1" (skosimp*) (("1" (expand "UUPart") (("1" (assert) (("1" (expand "o ") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (ground) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "connected_domain") (("3" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_diff_eq[length(Pa!1) + length(Pb!1) - 2 ,length(Pa!1) - 1]") (("2" (inst?) (("1" (assert) (("1" (hide 2) (("1" (skosimp*) (("1" (expand "UUPart") (("1" (assert) (("1" (expand "o ") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (ground) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "connected_domain") (("3" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (lemma "connected_domain") (("4" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (hide 2) (("3" (replace -1) (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (lemma "connected_domain") (("4" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "UUPart") (("2" (propax) 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) ("2" (expand "UUPart") (("2" (propax) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (skosimp*) (("1" (expand "UUPart") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "o") (("2" (assert) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (typepred "ii!1") (("3" (expand "UUPart") (("3" (expand "o") (("3" (case-replace "ii!1 < length(Pa!1) - 1") (("1" (inst -4 "ii!1") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (inst -2 "1 - length(Pa!1) + ii!1") (("2" (assert) (("2" (flatten) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((partition type-eq-decl nil integral_def nil) (xis? const-decl "bool" integral_def nil) (UUPart const-decl "partition[T](a, c)" step_fun_props nil) (sigma_split formula-decl nil sigma "reals/") (sigma_diff_eq formula-decl nil sigma_below_sub "reals/") (sigma_diff_shift formula-decl nil sigma_below_sub "reals/") (sigma def-decl "real" sigma "reals/") (Rie_sum const-decl "real" integral_def nil) (max const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" finite_sets_minmax "finite_sets/") (width const-decl "posreal" integral_def nil)) shostak)) (iss_prep_TCC1 0 (iss_prep_TCC1-1 nil 3282395953 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (iss_prep 0 (OWRE "FIX" 3399972591 ("" (skosimp*) (("" (assert) (("" (case "(EXISTS (jj: below(length(P!1))): seq(P!1)(jj) = b!1)") (("1" (skosimp*) (("1" (inst + "P!1") (("1" (assert) (("1" (inst?) nil nil)) nil)) nil)) nil) ("2" (name "ab" "min_nat.min({ii: below(length(P!1)) | seq(P!1)(ii) > b!1})") (("1" (inst 2 " LET N = length(P!1)+1 IN (# length := N, seq := (LAMBDA (ii: below(N)): IF ii < ab THEN P!1`seq(ii) ELSIF ii = ab THEN b!1 ELSE P!1`seq(ii-1) ENDIF) #)") (("1" (split +) (("1" (hide 2) (("1" (expand "step_function_on?") (("1" (skosimp*) (("1" (case "ii!1 < ab") (("1" (assert) (("1" (inst - "ii!1") (("1" (skosimp*) (("1" (inst + "fv!1") (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (typepred "x!1") (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "ii!1 = ab") (("1" (inst -5 "ab-1") (("1" (skosimp*) (("1" (inst + "fv!1") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (typepred "x!1") (("1" (lift-if) (("1" (assert) (("1" (case "seq(P!1)(ab - 1) < b!1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (typepred "P!1") (("2" (inst - "ab-1") (("2" (assert) (("2" (typepred "ab") (("2" (inst -3 "ab-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (inst - "ii!1-1") (("1" (skosimp*) (("1" (inst + "fv!1") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (typepred "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst 1 "ab") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (lift-if) (("2" (lift-if) (("2" (ground) (("2" (skosimp*) (("2" (lift-if) (("2" (lift-if) (("2" (ground) (("1" (typepred "P!1") (("1" (inst - "ii!1") nil nil)) nil) ("2" (case-replace "ii!1 = ab - 1") (("1" (typepred "ab") (("1" (inst - "ab-1") (("1" (assert) (("1" (inst + "ab-1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("3" (typepred "P!1") (("3" (inst + "ii!1-1") (("3" (inst - "ii!1-1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "P!1") (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("2" (hide 2 3) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "length(P!1)-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (step_function_on? const-decl "bool" step_fun_def nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (open_interval type-eq-decl nil intervals_real "reals/") (ii!1 skolem-const-decl "below(length(P!1))" integral_split nil) (x!1 skolem-const-decl "open_interval [T](IF ii!1 < ab THEN P!1`seq(ii!1) ELSIF ii!1 = ab THEN b!1 ELSE P!1`seq(ii!1 - 1) ENDIF, IF 1 + ii!1 < ab THEN P!1`seq(1 + ii!1) ELSIF 1 + ii!1 = ab THEN b!1 ELSE P!1`seq(ii!1) ENDIF)" integral_split nil) (x!1 skolem-const-decl "open_interval [T](IF ii!1 < ab THEN P!1`seq(ii!1) ELSIF ii!1 = ab THEN b!1 ELSE P!1`seq(ii!1 - 1) ENDIF, IF 1 + ii!1 < ab THEN P!1`seq(1 + ii!1) ELSIF 1 + ii!1 = ab THEN b!1 ELSE P!1`seq(ii!1) ENDIF)" integral_split nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (x!1 skolem-const-decl "open_interval [T](IF ii!1 < ab THEN P!1`seq(ii!1) ELSIF ii!1 = ab THEN b!1 ELSE P!1`seq(ii!1 - 1) ENDIF, IF 1 + ii!1 < ab THEN P!1`seq(1 + ii!1) ELSIF 1 + ii!1 = ab THEN b!1 ELSE P!1`seq(ii!1) ENDIF)" integral_split nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posint nonempty-type-eq-decl nil integers nil) (a!1 skolem-const-decl "T" integral_split nil) (c!1 skolem-const-decl "T" integral_split nil) (P!1 skolem-const-decl "partition[T](a!1, c!1)" integral_split nil) (b!1 skolem-const-decl "T" integral_split nil) (ab skolem-const-decl "{a | seq(P!1)(a) > b!1 AND (FORALL (x: below(length(P!1))): seq(P!1)(x) > b!1 IMPLIES a <= x)}" integral_split nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (T_pred const-decl "[real -> boolean]" integral_split nil) (T formal-nonempty-subtype-decl nil integral_split 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) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil)) shostak) (iss_prep-2 nil 3399972563 (";;; Proof iss_prep-2 for formula integral_split.iss_prep" (skosimp*) ((";;; Proof iss_prep-2 for formula integral_split.iss_prep" (assert) ((";;; Proof iss_prep-2 for formula integral_split.iss_prep" (case "(EXISTS (jj: below(length(P!1))): seq(P!1)(jj) = b!1)") (("1" (skosimp*) (("1" (inst + "P!1") (("1" (assert) (("1" (inst?) nil))))))) ("2" (name "ab" "min_nat.min({ii: below(length(P!1)) | seq(P!1)(ii) > b!1})") (("1" (inst 2 " LET N = length(P!1)+1 IN (# length := N, seq := (LAMBDA (ii: below(N)): IF ii < ab THEN P!1`seq(ii) ELSIF ii = ab THEN b!1 ELSE P!1`seq(ii-1) ENDIF) #)") (("1" (split +) (("1" (hide 2) (("1" (expand "step_function_on?") (("1" (skosimp*) (("1" (case "ii!1 < ab") (("1" (assert) (("1" (inst - "ii!1") (("1" (skosimp*) (("1" (inst + "fv!1") (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (typepred "x!1") (("1" (assert) (("1" (lift-if) (("1" (ground) nil))))))))))))))))))))) ("2" (case "ii!1 = ab") (("1" (inst -5 "ab-1") (("1" (skosimp*) (("1" (inst + "fv!1") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (typepred "x!1") (("1" (lift-if) (("1" (assert) (("1" (case "seq(P!1)(ab - 1) < b!1") (("1" (assert) nil) ("2" (hide 2) (("2" (typepred "P!1") (("2" (inst - "ab-1") (("2" (assert) (("2" (typepred "ab") (("2" (inst -3 "ab-1") (("2" (assert) nil))))))))))))))))))))))))))))) ("2" (assert) nil))) ("2" (inst - "ii!1-1") (("1" (skosimp*) (("1" (inst + "fv!1") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (typepred "x!1") (("1" (assert) nil))))))))))) ("2" (assert) nil))))))))))))) ("2" (inst 1 "ab") (("1" (assert) nil) ("2" (assert) nil))))) ("2" (skosimp*) (("2" (lift-if) (("2" (lift-if) (("2" (ground) (("2" (skosimp*) (("2" (lift-if) (("2" (lift-if) (("2" (ground) (("1" (typepred "P!1") (("1" (inst - "ii!1") nil))) ("2" (case-replace "ii!1 = ab - 1") (("1" (typepred "ab") (("1" (inst - "ab-1") (("1" (assert) (("1" (inst + "ab-1") (("1" (assert) nil))))))))) ("2" (assert) nil))) ("3" (typepred "P!1") (("3" (inst + "ii!1-1") (("3" (inst - "ii!1-1") (("3" (assert) nil))))))))))))))))))))))) ("3" (typepred "P!1") (("3" (skosimp*) (("3" (assert) nil))))) ("4" (skosimp*) (("4" (assert) nil))))) ("2" (hide 2 3) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "length(P!1)-1") (("2" (assert) nil)))))))))))))))))) ";;; developed with shostak decision procedures") ((partition type-eq-decl nil integral_def nil) (step_function_on? const-decl "bool" step_fun_def nil)) nil) (iss_prep-1 nil 3282319775 ("" (skosimp*) (("" (assert) (("" (case "(EXISTS (jj: below(length(P!1))): seq(P!1)(jj) = b!1)") (("1" (skosimp*) (("1" (inst + "P!1") (("1" (assert) (("1" (inst?) nil nil)) nil)) nil)) nil) ("2" (name "ab" "min_nat.min({ii: below(length(P!1)) | seq(P!1)(ii) > b!1})") (("1" (inst 2 " LET N = length(P!1)+1 IN (# length := N, seq := (LAMBDA (ii: below(N)): IF ii < ab THEN P!1`seq(ii) ELSIF ii = ab THEN b!1 ELSE P!1`seq(ii-1) ENDIF) #)") (("1" (split +) (("1" (hide 2) (("1" (expand "step_function_on?") (("1" (skosimp*) (("1" (case "ii!1 < ab") (("1" (assert) (("1" (inst - "ii!1") (("1" (skosimp*) (("1" (inst + "fv!1") (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (typepred "x!1") (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "ii!1 = ab") (("1" (inst -5 "ab-1") (("1" (skosimp*) (("1" (inst + "fv!1") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (typepred "x!1") (("1" (lift-if) (("1" (assert) (("1" (case "seq(P!1)(ab - 1) < b!1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (typepred "P!1") (("2" (inst - "ab-1") (("2" (assert) (("2" (typepred "ab") (("2" (inst -3 "ab-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (inst - "ii!1-1") (("1" (skosimp*) (("1" (inst + "fv!1") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (typepred "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst 1 "ab") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (split +) (("1" (skosimp*) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (lift-if) (("2" (ground) nil nil)) nil) ("3" (lift-if) (("3" (ground) nil nil)) nil) ("4" (skosimp*) (("4" (lift-if) (("4" (lift-if) (("4" (ground) (("1" (typepred "P!1") (("1" (inst - "ii!1") nil nil)) nil) ("2" (case-replace "ii!1 = ab - 1") (("1" (typepred "ab") (("1" (inst - "ab-1") (("1" (assert) (("1" (inst + "ab-1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("3" (typepred "P!1") (("3" (inst + "ii!1-1") (("3" (inst - "ii!1-1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("2" (hide 2 3) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "length(P!1)-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((step_function_on? const-decl "bool" step_fun_def nil) (partition type-eq-decl nil integral_def nil)) shostak)) (integrable_split_step_TCC1 0 (integrable_split_step_TCC1-1 nil 3276447547 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (integrable_split_step 0 (integrable_split_step-5 nil 3282396607 ("" (skosimp*) (("" (lemma "step_function_integrable?[T]") (("1" (inst - "a!1" "c!1" "f!1") (("1" (assert) (("1" (hide -1) (("1" (lemma "iss_prep") (("1" (inst - "a!1" "b!1" "c!1" "f!1") (("1" (assert) (("1" (expand "step_function?") (("1" (skosimp*) (("1" (inst - "P!1") (("1" (split -1) (("1" (skosimp*) (("1" (hide -7) (("1" (case-replace "step_function_on?(a!1, b!1, f!1, PP!1^(0,ib!1))") (("1" (case-replace "step_function_on?(b!1, c!1, f!1, PP!1^(ib!1,length(PP!1)-1))") (("1" (name "LP" "PP!1 ^ (0, ib!1)") (("1" (replace -1) (("1" (name "UP" "PP!1 ^ (ib!1, length(PP!1) - 1)") (("1" (replace -1) (("1" (case "length(LP) = ib!1+1") (("1" (case "length(UP) = length(PP!1)-ib!1") (("1" (lemma "step_function_on_integral[T]") (("1" (inst - "a!1" "b!1" "f!1") (("1" (assert) (("1" (inst - "LP") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "step_function_on_integral[T]") (("1" (inst - "b!1" "c!1" "f!1") (("1" (assert) (("1" (inst - "UP") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (hide -1 -2) (("1" (lemma "step_function_on_integral[T]") (("1" (inst - "a!1" "c!1" "f!1") (("1" (assert) (("1" (inst - "PP!1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (hide -3 -4 -5 -9 -10) (("1" (lemma "sigma_split[below[length(PP!1)-1]]") (("1" (inst?) (("1" (inst - "ib!1 - 1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "sigma[below(length(LP) - 1)].sigma (0, length(LP) - 2, LAMBDA (ii: below(length(LP) - 1)): LP`seq(1 + ii) * integral_step[T].val_in(a!1, b!1, LP, ii, f!1) - LP`seq(ii) * integral_step[T].val_in(a!1, b!1, LP, ii, f!1)) = sigma[below[length(PP!1) - (0, ib!1 - 1, LAMBDA (ii: below(length(PP!1) - 1)): PP!1`seq(1 + ii) * integral_step[T].val_in(a!1, c!1, PP!1, ii, f!1) - PP!1`seq(ii) * integral_step[T].val_in(a!1, c!1, PP!1, ii, f!1))") (("1" (assert) (("1" (hide -1) (("1" (lemma "sigma_diff_shift[length(UP)-1,length(PP!1)-1]") (("1" (inst?) (("1" (inst - "(LAMBDA (ii: below(length(PP!1) - 1)): PP!1`seq(1 + ii) * val_in(a!1, c!1, PP!1, ii, f!1) - PP!1`seq(ii) * val_in(a!1, c!1, PP!1, ii, f!1))" "ib!1") (("1" (assert) (("1" (hide 2) (("1" (skosimp*) (("1" (replace -2 * rl) (("1" (hide -2 -3) (("1" (case-replace "val_in(b!1, c!1, PP!1 ^ (ib!1, length(PP!1) - 1), i!1, f!1) = val_in(a!1, c!1, PP!1, i!1 + ib!1 (("1" (assert) (("1" (hide -1) (("1" (expand "^") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "val_in") (("2" (name-replace "P1" "pick(b!1, c!1, PP!1 ^ (ib!1, length(PP!1) - 1), i!1)") (("2" (typepred "P1") (("2" (name-replace "P2" "pick(a!1, c!1, PP!1, i!1 + ib!1)") (("2" (typepred "P2") (("2" (reveal -13) (("2" (expand "step_function_on?") (("2" (expand "^") (("2" (expand "min") (("2" (inst - "i!1+ib!1") (("1" (skosimp*) (("1" (inst-cp - "P1") (("1" (inst - "P2") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (lemma "connected_domain") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (skosimp*) (("2" (assert) (("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (hide 2) (("3" (split +) (("1" (skosimp*) (("1" (assert) (("1" (typepred "x1!1") (("1" (replace -2 * rl) (("1" (hide -2 -3) (("1" (grind) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "c!1" "PP!1" "ib!1" "x1!1+ib!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (hide -1 -2) (("2" (grind) nil nil)) nil)) nil) ("3" (replace -1 * rl) (("3" (hide -1 -2) (("3" (grind) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (replace -1 * rl) (("4" (hide -1 -2) (("4" (grind) (("4" (typepred "PP!1") (("4" (inst - "ib!1+ii!2") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sigma_diff_eq[length(LP) - 1,length(PP!1) - 1]") (("2" (inst?) (("1" (assert) (("1" (hide 2) (("1" (skosimp*) (("1" (hide -2) (("1" (replace -2 * rl) (("1" (hide -2) (("1" (case-replace "integral_step[T].val_in(a!1, b!1, PP!1 ^ (0, ib!1), i!1, f!1) = integral_step[T].val_in( (("1" (hide -1) (("1" (expand "^") (("1" (propax) nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "val_in") (("2" (reveal -9) (("2" (expand "step_function_on?") (("2" (inst - "i!1") (("2" (skosimp*) (("2" (name-replace "P1" "pick(a!1, b!1, PP!1 ^ (0, ib!1), i!1)") (("2" (typepred "P1") (("2" (name-replace "P2" "pick(a!1, c!1, PP!1, i!1)") (("2" (typepred "P2") (("2" (inst-cp - "P1") (("1" (inst - "P2") (("1" (assert) nil nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil) ("4" (hide 2 3) (("4" (skosimp*) (("4" (split +) (("1" (skosimp*) (("1" (replace -2 * rl) (("1" (typepred "x1!1") (("1" (grind) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "c!1" "PP!1" "x1!1" "ib!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -2 * rl) (("2" (hide -1 -2) (("2" (grind) nil nil)) nil)) nil) ("3" (replace -2 * rl) (("3" (hide -1 -2) (("3" (grind) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (replace -2 * rl) (("4" (hide -1 -2) (("4" (grind) (("4" (typepred "PP!1") (("4" (inst - "ii!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "connected_domain") (("3" (skosimp*) nil nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("5" (lemma "connected_domain") (("5" (skosimp*) nil nil)) nil) ("6" (hide 2) (("6" (skosimp*) (("6" (prop) (("1" (skosimp*) (("1" (typepred "x1!1") (("1" (replace -3 * rl) (("1" (assert) (("1" (hide -2 -3) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "c!1" "PP!1" "x1!1" "ib!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -2 * rl) (("2" (assert) (("2" (expand "^") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (replace -2 * rl) (("3" (expand "^") (("3" (assert) (("3" (expand "min") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (assert) (("4" (replace -2 * rl) (("4" (expand "^") (("4" (assert) (("4" (typepred "PP!1") (("4" (inst - "ii!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (propax) 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)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -3 -4 -5 -6 -9 -10 -11 2) (("2" (grind) nil nil)) nil)) nil) ("2" (hide -1 -3 -4 -5 -9 -10 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2 -6 -7) (("2" (expand "step_function_on?") (("2" (skosimp*) (("2" (typepred "ii!1") (("2" (inst - "ii!1+ib!1") (("1" (skosimp*) (("1" (inst + "fv!1") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (typepred "x!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (hide -1 -2 -6 -7) (("3" (prop) (("1" (skosimp*) (("1" (typepred "x1!1") (("1" (grind) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "c!1" "PP!1" "ib!1" "ib!1+x1!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (skosimp*) (("5" (typepred "ii!1") (("5" (grind) (("5" (lemma "parts_order[T]") (("5" (inst - "a!1" "c!1" "PP!1" "ib!1+ii!1" "ib!1+ii!1+1") (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "step_function_on?") (("2" (skosimp*) (("2" (inst - "ii!1") (("1" (skosimp*) (("1" (inst + "fv!1") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (hide -4 -5) (("1" (typepred "x!1") (("1" (typepred "ii!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "ii!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 -5 -6 2) (("3" (prop) (("1" (skosimp*) (("1" (typepred "x1!1") (("1" (grind) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "c!1" "PP!1" "x1!1" "ib!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (skosimp*) (("5" (typepred "ii!1") (("5" (grind) (("5" (lemma "parts_order[T]") (("5" (inst - "a!1" "c!1" "PP!1" "ii!1" "ii!1+1") (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil) ((T formal-nonempty-subtype-decl nil integral_split nil) (T_pred const-decl "[real -> boolean]" integral_split 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) (step_function_integrable? formula-decl nil integral_step nil) (connected? const-decl "bool" deriv_domain_def nil) (not_one_element? const-decl "bool" deriv_domain_def nil) (bool nonempty-type-eq-decl nil booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (iss_prep formula-decl nil integral_split nil) (real_plus_real_is_real application-judgement "real" reals nil) (x!1 skolem-const-decl "open_interval[T](seq(PP!1 ^ (0, ib!1))(ii!1), seq(PP!1 ^ (0, ib!1))(1 + ii!1))" integral_split nil) (ii!1 skolem-const-decl "below(length(PP!1 ^ (0, ib!1)) - 1)" integral_split 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) (sigma_split formula-decl nil sigma "reals/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (sigma def-decl "real" sigma "reals/") (UP skolem-const-decl "finseq[closed_interval[T](a!1, c!1)]" integral_split nil) (b!1 skolem-const-decl "T" integral_split nil) (connected_domain formula-decl nil integral_split nil) (int_plus_int_is_int application-judgement "int" integers nil) (pick const-decl "{t: T | seq(P)(j) < t AND t < seq(P)(j + 1)}" integral_step nil) (i!1 skolem-const-decl "nat" integral_split nil) (ib!1 skolem-const-decl "below(length(PP!1))" integral_split nil) (P1 skolem-const-decl "{t: T | seq(PP!1 ^ (ib!1, length(PP!1) - 1))(i!1) < t AND t < seq(PP!1 ^ (ib!1, length(PP!1) - 1))(1 + i!1)}" integral_split nil) (open_interval type-eq-decl nil intervals_real "reals/") (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (NOT const-decl "[bool -> bool]" booleans nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (parts_order formula-decl nil integral_def nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (sigma_diff_shift formula-decl nil sigma_below_sub "reals/") (LP skolem-const-decl "finseq[closed_interval[T](a!1, c!1)]" integral_split nil) (i!1 skolem-const-decl "nat" integral_split nil) (P1 skolem-const-decl "{t: T | seq(PP!1 ^ (0, ib!1))(i!1) < t AND t < seq(PP!1 ^ (0, ib!1))(1 + i!1)}" integral_split nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (sigma_diff_eq formula-decl nil sigma_below_sub "reals/") (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (not_one_element formula-decl nil integral_split nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (val_in const-decl "real" integral_step nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (PP!1 skolem-const-decl "partition[T](a!1, c!1)" integral_split nil) (c!1 skolem-const-decl "T" integral_split nil) (a!1 skolem-const-decl "T" integral_split nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (step_function_on_integral formula-decl nil integral_step nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (x!1 skolem-const-decl "open_interval[T](seq(PP!1 ^ (ib!1, length(PP!1) - 1))(ii!1), seq(PP!1 ^ (ib!1, length(PP!1) - 1))(1 + ii!1))" integral_split nil) (ii!1 skolem-const-decl "below(length(PP!1 ^ (ib!1, length(PP!1) - 1)) - 1)" integral_split nil) (step_function_on? const-decl "bool" step_fun_def nil) (finseq type-eq-decl nil finite_sequences nil) (^ const-decl "finseq" finite_sequences 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) (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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (step_function? const-decl "bool" step_fun_def nil)) nil) (integrable_split_step-4 nil 3282324191 ("" (skosimp*) (("" (lemma "step_function_integrable?[T]") (("1" (inst - "a!1" "c!1" "f!1") (("1" (assert) (("1" (hide -1) (("1" (lemma "iss_prep") (("1" (inst - "a!1" "b!1" "c!1" "f!1") (("1" (assert) (("1" (expand "step_function?") (("1" (skosimp*) (("1" (inst - "P!1") (("1" (split -1) (("1" (skosimp*) (("1" (hide -7) (("1" (case-replace "step_function_on?(a!1, b!1, f!1, PP!1^(0,ib!1))") (("1" (case-replace "step_function_on?(b!1, c!1, f!1, PP!1^(ib!1,length(PP!1)-1))") (("1" (lemma "step_function_on_integral[T]") (("1" (inst - "a!1" "b!1" "f!1") (("1" (assert) (("1" (inst - "PP!1 ^ (0, ib!1)") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "step_function_on_integral[T]") (("1" (inst - "b!1" "c!1" "f!1") (("1" (assert) (("1" (inst - "PP!1 ^ (ib!1, length(PP!1) - 1)") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (hide -1 -2) (("1" (lemma "step_function_on_integral[T]") (("1" (inst - "a!1" "c!1" "f!1") (("1" (assert) (("1" (inst - "PP!1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (hide -1 -5 -6) (("1" (lemma "sigma_split[below[length(PP!1)-1]]") (("1" (inst?) (("1" (expand "^") (("1" (expand "min") (("1" (inst - "ib!1 - 1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (same-name "sigma[below(length(PP!1 ^ (0, ib!1)) - 1)]" "sigma[below[ib!1]]") (("1" (replace -1) (("1" (name-replace "LLA" " LAMBDA (ii: below(length(PP!1 ^ (0, ib!1)) - 1)): PP!1`seq(1 + ii) * val_in(a!1, b!1, (# length := 1 + ib!1, seq := LAMBDA (x: below[min(1 + ib!1, PP!1`length)]): PP!1`seq(x) #), ii, f!1) - PP!1`seq(ii) * val_in(a!1, b!1, (# length := 1 + ib!1, seq := LAMBDA (x: below[min(1 + ib!1, PP!1`length)]): PP!1`seq(x) #), ii, f!1)") (("1" (postpone) nil nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (typepred "ii!1") (("2" (postpone) nil nil)) nil)) nil)) 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)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (grind) 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)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "connected_domain") (("2" (skosimp*) 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) ("2" (hide 2) (("2" (hide -1 -2 -3 -7 -8) (("2" (prop) (("1" (skosimp*) (("1" (typepred "x1!1") (("1" (grind) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "c!1" "PP!1" "ib!1" "ib!1+x1!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "not_one_element") (("2" (grind) nil nil)) nil)) nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (skosimp*) (("5" (typepred "ii!1") (("5" (grind) (("5" (lemma "parts_order[T]") (("5" (inst - "a!1" "c!1" "PP!1" "ib!1+ii!1" "ib!1+ii!1+1") (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 -7 -8 2) (("2" (prop) (("1" (skosimp*) (("1" (typepred "x1!1") (("1" (grind) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "c!1" "PP!1" "x1!1" "ib!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (skosimp*) (("5" (typepred "ii!1") (("5" (grind) (("5" (lemma "parts_order[T]") (("5" (inst - "a!1" "c!1" "PP!1" "ii!1" "ii!1+1") (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2 -6 -7) (("2" (expand "step_function_on?") (("2" (skosimp*) (("2" (typepred "ii!1") (("2" (inst - "ii!1+ib!1") (("1" (skosimp*) (("1" (inst + "fv!1") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (typepred "x!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (hide -1 -2 -6 -7) (("3" (prop) (("1" (skosimp*) (("1" (typepred "x1!1") (("1" (grind) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "c!1" "PP!1" "ib!1" "ib!1+x1!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (skosimp*) (("5" (typepred "ii!1") (("5" (grind) (("5" (lemma "parts_order[T]") (("5" (inst - "a!1" "c!1" "PP!1" "ib!1+ii!1" "ib!1+ii!1+1") (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "step_function_on?") (("2" (skosimp*) (("2" (inst - "ii!1") (("1" (skosimp*) (("1" (inst + "fv!1") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (hide -4 -5) (("1" (typepred "x!1") (("1" (typepred "ii!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "ii!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 -5 -6 2) (("3" (prop) (("1" (skosimp*) (("1" (typepred "x1!1") (("1" (grind) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "c!1" "PP!1" "x1!1" "ib!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (skosimp*) (("5" (typepred "ii!1") (("5" (grind) (("5" (lemma "parts_order[T]") (("5" (inst - "a!1" "c!1" "PP!1" "ii!1" "ii!1+1") (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "step_function_on?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil) nil nil) (integrable_split_step-3 nil 3282324134 ("" (skosimp*) (("" (lemma "iss_prep") (("" (inst - "a!1" "b!1" "c!1" "f!1") (("" (assert) (("" (expand "step_function?") (("" (skosimp*) (("" (inst - "P!1") (("" (split -1) (("1" (skosimp*) (("1" (hide -7) (("1" (case-replace "step_function_on?(a!1, b!1, f!1, PP!1^(0,ib!1))") (("1" (case-replace "step_function_on?(b!1, c!1, f!1, PP!1^(ib!1,length(PP!1)-1))") (("1" (postpone) nil nil) ("2" (hide 2) (("2" (postpone) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil) ("4" (hide 2) (("4" (assert) (("4" (hide -1 -2 -6 -7) (("4" (prop) (("1" (skosimp*) (("1" (typepred "x1!1") (("1" (grind) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "c!1" "PP!1" "ib!1" "ib!1+x1!1") (("1" (assert) nil nil)) nil) ("2" (lemma "not_one_element") (("2" (assert) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (grind) nil nil)) nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (skosimp*) (("5" (typepred "ii!1") (("5" (grind) (("5" (lemma "parts_order[T]") (("1" (inst - "a!1" "c!1" "PP!1" "ib!1+ii!1" "ib!1+ii!1+1") (("1" (assert) nil nil)) nil) ("2" (lemma "not_one_element") (("2" (assert) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (postpone) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil) ("4" (hide -1 -5 -6 2) (("4" (assert) (("4" (case "0 < ib!1 AND ib!1 < length(P!1)") (("1" (flatten) (("1" (prop) (("1" (skosimp*) (("1" (typepred "x1!1") (("1" (grind) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "c!1" "PP!1" "x1!1" "ib!1") (("1" (assert) nil nil)) nil) ("2" (lemma "not_one_element") (("2" (assert) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (skosimp*) (("5" (typepred "ii!1") (("5" (grind) (("5" (lemma "parts_order[T]") (("1" (inst - "a!1" "c!1" "PP!1" "ii!1" "ii!1+1") (("1" (assert) nil nil)) nil) ("2" (lemma "not_one_element") (("2" (assert) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (assert) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "step_function_on?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil) (integrable_split_step-2 nil 3282323551 ("" (skosimp*) (("" (lemma "iss_prep") (("" (inst - "a!1" "b!1" "c!1" "f!1") (("" (assert) (("" (expand "step_function?") (("" (skosimp*) (("" (inst - "P!1") (("" (split -1) (("1" (skosimp*) (("1" (hide -7) (("1" (case-replace "step_function_on?(a!1, b!1, f!1, PP!1^(0,ib!1))") (("1" (case-replace "step_function_on?(b!1, c!1, f!1, PP!1^(ib!1,length(PP!1)-1))") (("1" (postpone) nil nil) ("2" (hide 2) (("2" (postpone) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil) ("4" (hide 2) (("4" (assert) (("4" (hide -1 -2 -6 -7) (("4" (prop) (("1" (skosimp*) (("1" (typepred "x1!1") (("1" (grind) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "c!1" "PP!1" "ib!1" "ib!1+x1!1") (("1" (assert) nil nil)) nil) ("2" (lemma "not_one_element") (("2" (assert) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (grind) nil nil)) nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (skosimp*) (("5" (typepred "ii!1") (("5" (grind) (("5" (lemma "parts_order[T]") (("1" (inst - "a!1" "c!1" "PP!1" "ib!1+ii!1" "ib!1+ii!1+1") (("1" (assert) nil nil)) nil) ("2" (lemma "not_one_element") (("2" (assert) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (postpone) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil) ("4" (hide -1 -5 -6 2) (("4" (assert) (("4" (case "0 < ib!1 AND ib!1 < length(P!1) -1") (("1" (flatten) (("1" (prop) (("1" (skosimp*) (("1" (typepred "x1!1") (("1" (grind) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "c!1" "PP!1" "x1!1" "ib!1") (("1" (assert) nil nil)) nil) ("2" (lemma "not_one_element") (("2" (assert) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (skosimp*) (("5" (typepred "ii!1") (("5" (grind) (("5" (lemma "parts_order[T]") (("1" (inst - "a!1" "c!1" "PP!1" "ii!1" "ii!1+1") (("1" (assert) nil nil)) nil) ("2" (lemma "not_one_element") (("2" (assert) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "step_function_on?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil) (integrable_split_step-1 nil 3280840285 ("" (skosimp*) (("" (lemma "iss_prep") (("" (inst - "a!1" "b!1" "c!1" "f!1") (("" (assert) (("" (expand "step_function?") (("" (skosimp*) (("" (inst - "P!1") (("" (split -1) (("1" (skosimp*) (("1" (hide -7) (("1" (case-replace "step_function_on?(a!1, b!1, f!1, PP!1^(0,ib!1))") (("1" (case-replace "step_function_on?(b!1, c!1, f!1, PP!1^(ib!1,c!1))") (("1" (postpone) nil nil) ("2" (hide 2) (("2" (postpone) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil) ("4" (hide 2) (("4" (assert) (("4" (prop) (("1" (postpone) nil nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil) ("5" (postpone) nil nil)) nil)) nil)) nil) ("5" (postpone) nil nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil)) nil)) nil)) nil) ("2" (expand "step_function_on?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (integrable_split 0 (integrable_split-13 nil 3477657599 (";;; Proof integrable_split-12 for formula integral_split.integrable_split" (stop-rewrite "abs_0") ((";;; Proof integrable_split-12 for formula integral_split.integrable_split" (skosimp*) ((";;; Proof integrable_split-12 for formula integral_split.integrable_split" (lemma "steps_exist[T]") (("1" (inst - "a!1" "b!1" "f!1") (("1" (assert) (("1" (lemma "steps_exist[T]") (("1" (inst - "b!1" "c!1" "f!1") (("1" (assert) (("1" (lemma "step_to_integrable[T]") (("1" (inst - "a!1" "c!1" "f!1") (("1" (assert) (("1" (skosimp*) (("1" (inst - "eps!1/2") (("1" (inst - "eps!1/2") (("1" (skosimp*) (("1" (name "FF1" "(LAMBDA (x: T): IF x < a!1 OR x > c!1 THEN 0 ELSIF x <= b!1 THEN f1!2(x) ELSE f1!1(x) ENDIF)") (("1" (name "FF2" "(LAMBDA (x: T): IF x < a!1 OR x > c!1 THEN 0 ELSIF x <= b!1 THEN f2!2(x) ELSE f2!1(x) ENDIF)") (("1" (inst + "FF1" "FF2") (("1" (case "step_function?(a!1, c!1, FF1)") (("1" (case "step_function?(a!1, c!1, FF2)") (("1" (assert) (("1" (prop) (("1" (skosimp*) (("1" (replace -3 * rl) (("1" (hide -3) (("1" (replace -3 * rl) (("1" (hide -3) (("1" (assert) (("1" (hide -1 -2) (("1" (lift-if) (("1" (ground) (("1" (inst -9 "xx!1") (("1" (assert) nil))) ("2" (inst -9 "xx!1") (("2" (assert) nil))) ("3" (inst -3 "xx!1") (("3" (assert) nil))) ("4" (inst -3 "xx!1") (("4" (assert) nil))))))))))))))))))))) ("2" (hide 2) (("2" (lemma "diff_step_is_step[T]") (("2" (inst?) (("2" (inst -1 "FF1") (("2" (assert) (("2" (lemma "step_function_integrable?[T]") (("2" (inst?) (("2" (assert) nil))))))))))))))) ("3" (hide 2) (("3" (lemma "integrable_split_step") (("3" (inst - "a!1" "b!1" "c!1" "FF2 - FF1") (("3" (assert) (("3" (case "step_function?(a!1, c!1, FF2 - FF1)") (("1" (assert) (("1" (case "integrable?(a!1, b!1, FF2 - FF1) AND integral(a!1, b!1, FF2 - FF1) = integral(a!1, b!1, f2!2 - (("1" (flatten) (("1" (assert) (("1" (case "integrable?(b!1, c!1, FF2 - FF1) AND integral(b!1, c!1, FF2 - FF1) = integral(b!1, c!1, f2!1 - (("1" (flatten) (("1" (assert) nil))) ("2" (hide 2) (("2" (replace -7 * rl) (("2" (hide -7) (("2" (replace -7 * rl) (("2" (hide -7) (("2" (hide -1 -2 -3 -4 -5 -6 -7 -8) (("2" (lemma "integral_restr_eq[T]") (("2" (inst?) (("2" (assert) (("2" (split -1) (("1" (propax) nil) ("2" (assert) (("2" (hide 2) (("2" (skosimp*) (("2" (expand "-") (("2" (assert) nil))))))))))))))))))))))))))))) ("3" (flatten) (("3" (skosimp*) (("3" (lemma "connected_domain") (("3" (expand "connected?") (("3" (inst?) (("3" (inst?) (("3" (assert) nil))))))))))))))))))) ("2" (hide 2) (("2" (hide -1 -2 -3 -4 -7 -8 -9 -10 -11 -12 -13 -14) (("2" (lemma "integral_restrict_eq[T]") (("2" (inst?) (("2" (assert) (("2" (split -1) (("1" (propax) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (replace -3 * rl) (("2" (hide -3) (("2" (replace -3 * rl) (("2" (hide -3) (("2" (expand "-") (("2" (assert) nil))))))))))))))))))))))))))) ("3" (flatten) (("3" (lemma "connected_domain") (("3" (expand "connected?") (("3" (propax) nil))))))))))) ("2" (inst?) (("2" (hide 2) (("2" (rewrite "diff_step_is_step[T]") nil))))))))))))))))))) ("2" (hide 2 3) (("2" (hide -1) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (hide -1) (("2" (hide-all-but (-1 -2 -6 -7 1)) (("2" (hide -1 -3) (("2" (rewrite "split_step_is_step[T]") nil))))))))))))))))) ("2" (hide 2 3) (("2" (hide -1) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (hide-all-but (-1 -2 -6 -7 1)) (("2" (hide -2 -4) (("2" (rewrite "split_step_is_step[T]") nil))))))))))))))))))))))))))))))))))))))))))))) ("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (expand "connected?") (("2" (inst?) (("2" (inst?) (("2" (assert) nil)))))))))))))))) ";;; developed with shostak decision procedures") ((= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (real_gt_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) (closed_interval type-eq-decl nil intervals_real "reals/") (AND const-decl "[bool, bool -> bool]" booleans nil) (diff_step_is_step formula-decl nil step_fun_props nil) (step_function_integrable? formula-decl nil integral_step nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (integrable_split_step formula-decl nil integral_split nil) (integral_restrict_eq formula-decl nil integral_def nil) (real_minus_real_is_real application-judgement "real" reals nil) (integral_restr_eq formula-decl nil integral_prep nil) (connected_domain formula-decl nil integral_split nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (split_step_is_step formula-decl nil step_fun_props nil) (step_function? const-decl "bool" step_fun_def nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal 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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (step_to_integrable formula-decl nil integral_step nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (bool nonempty-type-eq-decl nil booleans nil) (not_one_element? const-decl "bool" deriv_domain_def nil) (connected? const-decl "bool" deriv_domain_def nil) (steps_exist formula-decl nil integral_split_scaf 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_split nil) (T formal-nonempty-subtype-decl nil integral_split nil)) nil) (integrable_split-12 nil 3319994299 ("" (stop-rewrite "abs_0") (("" (skosimp*) (("" (lemma "steps_exist[T]") (("1" (inst - "a!1" "b!1" "f!1") (("1" (assert) (("1" (lemma "steps_exist[T]") (("1" (inst - "b!1" "c!1" "f!1") (("1" (assert) (("1" (lemma "step_to_integrable[T]") (("1" (inst - "a!1" "c!1" "f!1") (("1" (assert) (("1" (skosimp*) (("1" (inst - "eps!1/2") (("1" (inst - "eps!1/2") (("1" (skosimp*) (("1" (name "FF1" "(LAMBDA (x: T): IF x < a!1 OR x > c!1 THEN 0 ELSIF x <= b!1 THEN f1!2(x) ELSE f1!1(x) ENDIF)") (("1" (name "FF2" "(LAMBDA (x: T): IF x < a!1 OR x > c!1 THEN 0 ELSIF x <= b!1 THEN f2!2(x) ELSE f2!1(x) ENDIF)") (("1" (inst + "FF1" "FF2") (("1" (case "step_function?(a!1, c!1, FF1)") (("1" (case "step_function?(a!1, c!1, FF2)") (("1" (assert) (("1" (prop) (("1" (skosimp*) (("1" (replace -3 * rl) (("1" (hide -3) (("1" (replace -3 * rl) (("1" (hide -3) (("1" (assert) (("1" (hide -1 -2) (("1" (lift-if) (("1" (ground) (("1" (inst -9 "xx!1") (("1" (assert) nil nil)) nil) ("2" (inst -9 "xx!1") (("2" (assert) nil nil)) nil) ("3" (inst -3 "xx!1") (("3" (assert) nil nil)) nil) ("4" (inst -3 "xx!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "diff_step_is_step[T]") (("2" (inst?) (("2" (inst -1 "FF1") (("2" (assert) (("2" (lemma "step_function_integrable?[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "integrable_split_step") (("3" (inst - "a!1" "b!1" "c!1" "FF2 - FF1") (("3" (assert) (("3" (case "step_function?(a!1, c!1, FF2 - FF1)") (("1" (assert) (("1" (case "integrable?(a!1, b!1, FF2 - FF1) AND integral(a!1, b!1, FF2 - FF1) = integral(a!1, b!1, f2!2 - (("1" (flatten) (("1" (assert) (("1" (case "integrable?(b!1, c!1, FF2 - FF1) AND integral(b!1, c!1, FF2 - FF1) = integral(b!1, c!1, f2!1 - (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (replace -7 * rl) (("2" (hide -7) (("2" (replace -7 * rl) (("2" (hide -7) (("2" (hide -1 -2 -3 -4 -5 -6 -7 -8) (("2" (lemma "integral_restr_eq[T]") (("2" (inst?) (("2" (assert) (("2" (split -1) (("1" (propax) nil nil) ("2" (assert) (("2" (hide 2) (("2" (skosimp*) (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (skosimp*) (("3" (lemma "connected_domain") (("3" (inst?) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1 -2 -3 -4 -7 -8 -9 -10 -11 -12 -13 -14) (("2" (lemma "integral_restrict_eq[T]") (("2" (inst?) (("2" (assert) (("2" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp*) (("2" (replace -3 * rl) (("2" (hide -3) (("2" (replace -3 * rl) (("2" (hide -3) (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (hide 2) (("2" (rewrite "diff_step_is_step[T]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (hide -1) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (hide -1) (("2" (hide-all-but (-1 -2 -6 -7 1)) (("2" (hide -1 -3) (("2" (rewrite "split_step_is_step[T]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (hide -1) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (hide-all-but (-1 -2 -6 -7 1)) (("2" (hide -2 -4) (("2" (rewrite "split_step_is_step[T]") 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" (lemma "connected_domain") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((steps_exist formula-decl nil integral_split_scaf nil) (step_to_integrable formula-decl nil integral_step nil) (step_function? const-decl "bool" step_fun_def nil) (split_step_is_step formula-decl nil step_fun_props 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) (integral_restr_eq formula-decl nil integral_prep nil) (integral_restrict_eq formula-decl nil integral_def nil) (step_function_integrable? formula-decl nil integral_step nil) (diff_step_is_step formula-decl nil step_fun_props nil)) nil) (integrable_split-11 nil 3306071102 ("" (skosimp*) (("" (lemma "steps_exist[T]") (("1" (inst - "a!1" "b!1" "f!1") (("1" (assert) (("1" (lemma "steps_exist[T]") (("1" (inst - "b!1" "c!1" "f!1") (("1" (assert) (("1" (lemma "step_to_integrable[T]") (("1" (inst - "a!1" "c!1" "f!1") (("1" (assert) (("1" (skosimp*) (("1" (inst - "eps!1/2") (("1" (inst - "eps!1/2") (("1" (skosimp*) (("1" (name "FF1" "(LAMBDA (x: T): IF x < a!1 OR x > c!1 THEN 0 ELSIF x <= b!1 THEN f1!2(x) ELSE f1!1(x) ENDIF)") (("1" (name "FF2" "(LAMBDA (x: T): IF x < a!1 OR x > c!1 THEN 0 ELSIF x <= b!1 THEN f2!2(x) ELSE f2!1(x) ENDIF)") (("1" (inst + "FF1" "FF2") (("1" (case "step_function?(a!1, c!1, FF1)") (("1" (case "step_function?(a!1, c!1, FF2)") (("1" (assert) (("1" (prop) (("1" (skosimp*) (("1" (replace -3 * rl) (("1" (hide -3) (("1" (replace -3 * rl) (("1" (hide -3) (("1" (assert) (("1" (hide -1 -2) (("1" (lift-if) (("1" (ground) (("1" (inst -9 "xx!1") (("1" (assert) nil nil)) nil) ("2" (inst -9 "xx!1") (("2" (assert) nil nil)) nil) ("3" (inst -3 "xx!1") (("3" (assert) nil nil)) nil) ("4" (inst -3 "xx!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "diff_step_is_step[T]") (("2" (inst?) (("2" (inst -1 "FF1") (("2" (assert) (("2" (lemma "step_function_integrable?[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "integrable_split_step") (("3" (inst - "a!1" "b!1" "c!1" "FF2 - FF1") (("3" (assert) (("3" (case "step_function?(a!1, c!1, FF2 - FF1)") (("1" (assert) (("1" (case "integrable?(a!1, b!1, FF2 - FF1) AND integral(a!1, b!1, FF2 - FF1) = integral(a!1, b!1, f2!2 - (("1" (flatten) (("1" (assert) (("1" (case "integrable?(b!1, c!1, FF2 - FF1) AND integral(b!1, c!1, FF2 - FF1) = integral(b!1, c!1, f2!1 - (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (replace -7 * rl) (("2" (hide -7) (("2" (replace -7 * rl) (("2" (hide -7) (("2" (hide -1 -2 -3 -4 -5 -6 -7 -8) (("2" (lemma "integral_restr_eq[T]") (("2" (inst?) (("2" (assert) (("2" (split -1) (("1" (propax) nil nil) ("2" (assert) (("2" (hide 2) (("2" (skosimp*) (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (skosimp*) (("3" (lemma "connected_domain") (("3" (inst?) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1 -2 -3 -4 -7 -8 -9 -10 -11 -12 -13 -14) (("2" (lemma "integral_restrict_eq[T]") (("2" (inst?) (("2" (assert) (("2" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp*) (("2" (replace -3 * rl) (("2" (hide -3) (("2" (replace -3 * rl) (("2" (hide -3) (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (hide 2) (("2" (rewrite "diff_step_is_step[T]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (hide -1) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (hide -1) (("2" (hide-all-but (-1 -2 -6 -7 1)) (("2" (hide -1 -3) (("2" (rewrite "split_step_is_step[T]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (hide -1) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (hide-all-but (-1 -2 -6 -7 1)) (("2" (hide -2 -4) (("2" (rewrite "split_step_is_step[T]") 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" (lemma "connected_domain") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((steps_exist formula-decl nil integral_split_scaf nil) (step_to_integrable formula-decl nil integral_step nil) (step_function? const-decl "bool" step_fun_def nil) (split_step_is_step formula-decl nil step_fun_props 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) (integral_restr_eq formula-decl nil integral_prep nil) (integral_restrict_eq formula-decl nil integral_def nil) (step_function_integrable? formula-decl nil integral_step nil) (diff_step_is_step formula-decl nil step_fun_props nil)) nil) (integrable_split-10 nil 3280055345 ("" (skosimp*) (("" (lemma "steps_exist[T]") (("1" (inst - "a!1" "b!1" "f!1") (("1" (assert) (("1" (lemma "steps_exist[T]") (("1" (inst - "b!1" "c!1" "f!1") (("1" (assert) (("1" (lemma "step_to_integrable[T]") (("1" (inst - "a!1" "c!1" "f!1") (("1" (assert) (("1" (skosimp*) (("1" (inst - "eps!1/2") (("1" (inst - "eps!1/2") (("1" (skosimp*) (("1" (name "FF1" "(LAMBDA (x: T): IF x < a!1 OR x > c!1 THEN 0 ELSIF x <= b!1 THEN f1!2(x) ELSE f1!1(x) ENDIF)") (("1" (name "FF2" "(LAMBDA (x: T): IF x < a!1 OR x > c!1 THEN 0 ELSIF x <= b!1 THEN f2!2(x) ELSE f2!1(x) ENDIF)") (("1" (inst + "FF1" "FF2") (("1" (case "step_function?(a!1, c!1, FF1)") (("1" (case "step_function?(a!1, c!1, FF2)") (("1" (assert) (("1" (prop) (("1" (skosimp*) (("1" (replace -3 * rl) (("1" (hide -3) (("1" (replace -3 * rl) (("1" (hide -3) (("1" (assert) (("1" (hide -1 -2) (("1" (lift-if) (("1" (ground) (("1" (inst -9 "xx!1") (("1" (assert) nil nil)) nil) ("2" (inst -9 "xx!1") (("2" (assert) nil nil)) nil) ("3" (inst -3 "xx!1") (("3" (assert) nil nil)) nil) ("4" (inst -3 "xx!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "diff_step_is_step[T]") (("2" (inst?) (("2" (inst -1 "FF1") (("2" (assert) (("2" (lemma "step_function_integrable?[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "integrable_split_step[T]") (("3" (inst - "a!1" "b!1" "c!1" "FF2 - FF1") (("3" (assert) (("3" (case "step_function?(a!1, c!1, FF2 - FF1)") (("1" (assert) (("1" (case "integrable?(a!1, b!1, FF2 - FF1) AND integral(a!1, b!1, FF2 - FF1) = integral(a!1, b!1, f2!2 - (("1" (flatten) (("1" (assert) (("1" (case "integrable?(b!1, c!1, FF2 - FF1) AND integral(b!1, c!1, FF2 - FF1) = integral(b!1, c!1, f2!1 - (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (replace -7 * rl) (("2" (hide -7) (("2" (replace -7 * rl) (("2" (hide -7) (("2" (hide -1 -2 -3 -4 -5 -6 -7 -8) (("2" (lemma "integral_restr_eq[T]") (("2" (inst?) (("2" (assert) (("2" (split -1) (("1" (propax) nil nil) ("2" (assert) (("2" (hide 2) (("2" (skosimp*) (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (skosimp*) (("3" (lemma "connected_domain") (("3" (inst?) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1 -2 -3 -4 -7 -8 -9 -10 -11 -12 -13 -14) (("2" (lemma "integral_restrict_eq[T]") (("2" (inst?) (("2" (assert) (("2" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp*) (("2" (replace -3 * rl) (("2" (hide -3) (("2" (replace -3 * rl) (("2" (hide -3) (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (hide 2) (("2" (rewrite "diff_step_is_step[T]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (hide -1) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (hide -1) (("2" (hide-all-but (-1 -2 -6 -7 1)) (("2" (hide -1 -3) (("2" (rewrite "split_step_is_step[T]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (hide -1) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (hide-all-but (-1 -2 -6 -7 1)) (("2" (hide -2 -4) (("2" (rewrite "split_step_is_step[T]") 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" (lemma "connected_domain") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((diff_step_is_step formula-decl nil step_fun_props nil) (step_function_integrable? formula-decl nil integral_step nil) (integral_restrict_eq formula-decl nil integral_def nil) (integral_restr_eq formula-decl nil integral_prep 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) (split_step_is_step formula-decl nil step_fun_props nil) (step_function? const-decl "bool" step_fun_def nil) (step_to_integrable formula-decl nil integral_step nil) (steps_exist formula-decl nil integral_split_scaf nil)) nil) (integrable_split-9 nil 3272798711 ("" (skosimp*) (("" (lemma "steps_exist") (("" (inst - "a!1" "b!1" "f!1") (("" (assert) (("" (lemma "steps_exist") (("" (inst - "b!1" "c!1" "f!1") (("" (assert) (("" (lemma "step_to_integrable[T]") (("1" (inst - "a!1" "c!1" "f!1") (("1" (assert) (("1" (skosimp*) (("1" (inst - "eps!1/2") (("1" (inst - "eps!1/2") (("1" (skosimp*) (("1" (name "FF1" "(LAMBDA (x: T): IF x < a!1 OR x > c!1 THEN 0 ELSIF x <= b!1 THEN f1!2(x) ELSE f1!1(x) ENDIF)") (("1" (name "FF2" "(LAMBDA (x: T): IF x < a!1 OR x > c!1 THEN 0 ELSIF x <= b!1 THEN f2!2(x) ELSE f2!1(x) ENDIF)") (("1" (inst + "FF1" "FF2") (("1" (case "step_function?(a!1, c!1, FF1)") (("1" (case "step_function?(a!1, c!1, FF2)") (("1" (assert) (("1" (prop) (("1" (skosimp*) (("1" (replace -3 * rl) (("1" (hide -3) (("1" (replace -3 * rl) (("1" (hide -3) (("1" (assert) (("1" (hide -1 -2) (("1" (lift-if) (("1" (ground) (("1" (inst -9 "xx!1") (("1" (assert) nil nil)) nil) ("2" (inst -9 "xx!1") (("2" (assert) nil nil)) nil) ("3" (inst -3 "xx!1") (("3" (assert) nil nil)) nil) ("4" (inst -3 "xx!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "diff_step_is_step") (("2" (inst?) (("2" (inst -1 "FF1") (("2" (assert) (("2" (lemma "step_function_integrable?[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "integrable_split_step") (("3" (inst - "a!1" "b!1" "c!1" "FF2 - FF1") (("3" (assert) (("3" (case "step_function?(a!1, c!1, FF2 - FF1)") (("1" (assert) (("1" (case "integrable?(a!1, b!1, FF2 - FF1) AND integral(a!1, b!1, FF2 - FF1) = integral(a!1, b!1, f2!2 - (("1" (flatten) (("1" (assert) (("1" (case "integrable?(b!1, c!1, FF2 - FF1) AND integral(b!1, c!1, FF2 - FF1) = integral(b!1, c!1, f2!1 - (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (replace -7 * rl) (("2" (hide -7) (("2" (replace -7 * rl) (("2" (hide -7) (("2" (hide -1 -2 -3 -4 -5 -6 -7 -8) (("2" (lemma "integral_restr_eq") (("2" (inst?) (("2" (assert) (("2" (split -1) (("1" (propax) nil nil) ("2" (assert) (("2" (hide 2) (("2" (skosimp*) (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" --> -------------------- --> maximum size reached --> --------------------
¤ Dauer der Verarbeitung: 0.985 Sekunden (vorverarbeitet am 2026-04-29) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26