| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Impressum integral_def.prfSprache: Lisp |
|||||||||||||||
|
(integral_def (partition_TCC1 0 (partition_TCC1-1 nil 3253536795 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (partition_TCC2 0 (partition_TCC2-1 nil 3253536795 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (partition_TCC3 0 (partition_TCC3-1 nil 3253536795 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (partition_TCC4 0 (partition_TCC4-1 nil 3253536795 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (width_TCC1 0 (width_TCC1-1 nil 3253536795 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (width_TCC2 0 (width_TCC2-1 nil 3253536795 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (width_TCC3 0 (width_TCC3-1 nil 3253536795 ("" (skosimp*) (("" (prop) (("1" (lemma "is_finite_surj") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (inst + "N!1-1" "(LAMBDA (ii: below(N!1-1)): xx!1(ii + 1) - xx!1(ii)) ") (("1" (expand "surjective?") (("1" (skosimp*) (("1" (replace -1) (("1" (typepred "y!1") (("1" (skosimp*) (("1" (inst + "ii!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (grind) nil nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "empty?") (("2" (expand "member") (("2" (inst -1 "xx!1(1) - xx!1(0)") (("2" (inst + "0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (P!1 skolem-const-decl "partition(a!1, b!1)" integral_def nil) (partition type-eq-decl nil integral_def 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/") (b!1 skolem-const-decl "{x: T | a!1 < x}" integral_def nil) (a!1 skolem-const-decl "T" integral_def nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T formal-subtype-decl nil integral_def nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (below type-eq-decl nil nat_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (N!1 skolem-const-decl "nat" integral_def nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (set type-eq-decl nil sets nil) (surjective? const-decl "bool" functions nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (xx!1 skolem-const-decl "[below[P!1`length] -> closed_interval[T](a!1, b!1)]" integral_def nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (is_finite_surj formula-decl nil finite_sets nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (member const-decl "bool" sets nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (empty? const-decl "bool" sets nil)) nil)) (width_TCC4 0 (owre "fix" 3399972853 ("" (skosimp*) (("" (typepred "max[real, <=] ({l: real | EXISTS (ii: below(N!1 - 1)): l = xx!1(ii + 1) - xx!1(ii)})") (("1" (skosimp*) (("1" (replace -1) (("1" (assert) (("1" (hide -1 -2) (("1" (typepred "P!1") (("1" (inst -4 "ii!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "width_TCC3") (("2" (inst?) (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil) ("4" (hide 2) (("4" (grind) nil nil)) nil)) nil)) nil) ((partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (T formal-subtype-decl nil integral_def nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (below type-eq-decl nil nat_types nil) (max const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" finite_sets_minmax "finite_sets/") (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (width_TCC3 subtype-tcc nil integral_def nil)) shostak) (width_TCC4-2 nil 3399972842 (";;; Proof width_TCC4-2 for formula integral_def.width_TCC4" (skosimp*) ((";;; Proof width_TCC4-2 for formula integral_def.width_TCC4" (typepred "max[real, <=] ({l: real | EXISTS (ii: below(N!1 - 1)): l = xx!1(ii + 1) - xx!1(ii)})") (("1" (skosimp*) (("1" (replace -1) (("1" (assert) (("1" (hide -1 -2) (("1" (typepred "P!1") (("1" (inst -4 "ii!1") (("1" (assert) nil))))))))))))) ("2" (hide 2) (("2" (lemma "width_TCC3") (("2" (inst?) (("2" (assert) (("2" (inst?) (("2" (assert) nil))))))))))) ("3" (hide 2) (("3" (grind) nil))) ("4" (hide 2) (("4" (grind) nil)))))) ";;; developed with shostak decision procedures") ((is_finite const-decl "bool" 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/")) nil) (width_TCC4-1 nil 3253536795 ("" (skosimp*) (("" (typepred "max[real, <=] ({l: real | EXISTS (ii: below(length(P!1) - 1)): l = seq(P!1)(ii + 1) - seq(P!1)(ii)})") (("1" (skosimp*) (("1" (replace -1) (("1" (assert) (("1" (hide -1 -2) (("1" (typepred "P!1") (("1" (inst -4 "ii!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "width_TCC3") (("2" (inst -1 "a!1" "b!1" "P!1" "seq(P!1)") (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((max const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" finite_sets_minmax "finite_sets/") (non_empty_finite_set type-eq-decl nil finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil)) nil)) (width_lem_TCC1 0 (width_lem_TCC1-1 nil 3253536795 ("" (subtype-tcc) nil nil) nil nil)) (width_lem_TCC2 0 (width_lem_TCC2-1 nil 3253536795 ("" (subtype-tcc) nil nil) nil nil)) (width_lem 0 (width_lem-1 nil 3253536795 ("" (skosimp*) (("" (assert) (("" (expand "width") (("" (typepred "max({l: real | EXISTS (ii: below(length(P!1) - 1)): l = seq(P!1)(1 + ii) - seq(P!1)(ii)})") (("1" (skosimp*) (("1" (inst -2 "P!1`seq(1 + ii!1) - P!1`seq(ii!1)") (("1" (assert) (("1" (hide -1 2) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "width_TCC3") (("2" (inst -1 "a!1" "b!1" "P!1" "seq(P!1)") (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (max const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" finite_sets_minmax "finite_sets/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (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 "[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) (T formal-subtype-decl nil integral_def nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (below type-eq-decl nil nat_types nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (width_TCC3 subtype-tcc nil integral_def nil) (width const-decl "posreal" integral_def nil)) nil)) (parts_order 0 (parts_order-1 nil 3253536795 ("" (skosimp*) (("" (case "FORALL (n: posnat): ii!1 + n < length(P!1) IMPLIES seq(P!1)(ii!1) < seq(P!1)(ii!1+n)") (("1" (inst -1 "jj!1-ii!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (hide -1 2) (("2" (induct "n") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp*) (("3" (assert) (("3" (ground) (("1" (typepred "P!1") (("1" (inst -4 "ii!1+j!1") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (case-replace "j!1 = 0") (("1" (assert) (("1" (typepred "P!1") (("1" (inst -4 "ii!1") nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((partition type-eq-decl nil integral_def nil) (below type-eq-decl nil naturalnumbers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T formal-subtype-decl nil integral_def nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ii!1 skolem-const-decl "below(length(P!1))" integral_def nil) (jj!1 skolem-const-decl "below(length(P!1))" integral_def nil) (P!1 skolem-const-decl "partition(a!1, b!1)" integral_def nil) (b!1 skolem-const-decl "T" integral_def nil) (a!1 skolem-const-decl "T" integral_def nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil)) nil)) (parts_order_le 0 (parts_order_le-1 nil 3280833323 ("" (skosimp*) (("" (lemma "parts_order") (("" (inst - "a!1" "b!1" "P!1" "ii!1" "jj!1") (("" (assert) nil nil)) nil)) nil)) nil) ((parts_order formula-decl nil integral_def nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-subtype-decl nil integral_def nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (parts_disjoint_TCC1 0 (parts_disjoint_TCC1-1 nil 3253536795 ("" (subtype-tcc) nil nil) nil nil)) (parts_disjoint_TCC2 0 (parts_disjoint_TCC2-1 nil 3253536795 ("" (subtype-tcc) nil nil) nil nil)) (parts_disjoint_TCC3 0 (parts_disjoint_TCC3-1 nil 3253536795 ("" (subtype-tcc) nil nil) nil nil)) (parts_disjoint_TCC4 0 (parts_disjoint_TCC4-1 nil 3253536795 ("" (subtype-tcc) nil nil) nil nil)) (parts_disjoint 0 (parts_disjoint-1 nil 3253536795 ("" (skosimp*) (("" (case "ii!1 < jj!1") (("1" (case-replace "seq(P!1)(ii!1+1) < seq(P!1)(jj!1)") (("1" (assert) nil nil) ("2" (case "ii!1 + 1 = jj!1") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (lemma "parts_order") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case-replace "seq(P!1)(jj!1+1) < seq(P!1)(ii!1)") (("1" (assert) nil nil) ("2" (case "jj!1 + 1 = ii!1") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (lemma "parts_order") (("2" (inst -1 "a!1" "b!1" "P!1" "jj!1+1" "ii!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) 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 "[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) (T formal-subtype-decl nil integral_def nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (below type-eq-decl nil nat_types nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (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 "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_minus_real_is_real application-judgement "real" reals nil) (parts_order formula-decl nil integral_def nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (in_sect?_TCC1 0 (in_sect?_TCC1-1 nil 3281209744 ("" (skosimp*) (("" (assert) nil nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (part_in_TCC1 0 (part_in_TCC1-1 nil 3253536795 ("" (subtype-tcc) nil nil) nil nil)) (part_in_TCC2 0 (part_in_TCC2-1 nil 3253536795 ("" (subtype-tcc) nil nil) nil nil)) (part_in 0 (part_in-1 nil 3253536795 ("" (skolem 1 ("a!1" "b!1" "x!1" "_")) (("" (measure-induct+ "length(P)" ("P")) (("" (inst-cp 1 "length(x!2) - 2") (("" (inst 1 "length(x!2) - 3") (("1" (ground) (("1" (inst -1 "(# length := length(x!2) - 1, seq := (LAMBDA (iii: below(length(x!2) - 1)): IF iii <= length(x!2) -3 THEN seq(x!2)(iii) ELSE seq(x!2)(iii+1) ENDIF) #)") (("1" (assert) (("1" (skosimp*) (("1" (ground) (("1" (reveal 1) (("1" (inst + "ii!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (ground) (("2" (lift-if) (("2" (ground) (("1" (typepred "x!2") (("1" (inst?) nil nil)) nil) ("2" (assert) (("2" (lemma "parts_order") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "x!2") (("2" (case "length(x!2) = 2") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pred type-eq-decl nil defined_types nil) (well_founded? const-decl "bool" orders nil) (measure_induction formula-decl nil measure_induction nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (wf_nat formula-decl nil naturalnumbers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (a!1 skolem-const-decl "T" integral_def nil) (b!1 skolem-const-decl "T" integral_def nil) (x!2 skolem-const-decl "partition(a!1, b!1)" integral_def 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (parts_order formula-decl nil integral_def nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (part_not_in_TCC1 0 (part_not_in_TCC1-1 nil 3280833362 ("" (skosimp*) (("" (assert) nil nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (part_not_in_TCC2 0 (part_not_in_TCC2-1 nil 3280833362 ("" (skosimp*) (("" (assert) nil nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (part_not_in 0 (part_not_in-1 nil 3280828196 ("" (skosimp*) (("" (lemma "parts_order") (("" (inst - "a!1" "b!1" "P!1" "ii!1+1" "jj!1") (("" (assert) (("" (lemma "parts_order") (("" (inst - "a!1" "b!1" "P!1" "jj!1" "ii!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((parts_order formula-decl nil integral_def nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-subtype-decl nil integral_def nil) (T_pred const-decl "[real -> boolean]" integral_def 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) shostak)) (part_induction_TCC1 0 (part_induction_TCC1-1 nil 3253536795 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (part_induction_TCC2 0 (part_induction_TCC2-1 nil 3253536795 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (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)) nil)) (part_induction 0 (part_induction-1 nil 3253536795 ("" (skosimp*) (("" (assert) (("" (skosimp*) (("" (case "(FORALL (n: below(length(P!1)-1)): (FORALL (ii: below(n + 1)): seq(P!1)(ii) <= x!1 AND (("1" (inst -1 "length(P!1)-2") (("1" (assert) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (induct "n" 1 "below_induction[length(P!1) - 1]") (("1" (assert) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (split -2) (("1" (propax) nil nil) ("2" (inst - "jb!1+1") (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((OR const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[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) (T formal-subtype-decl nil integral_def nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (below type-eq-decl nil nat_types nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (pred type-eq-decl nil defined_types nil) (below_induction formula-decl nil bounded_nat_inductions nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (eq_partition_TCC1 0 (eq_partition_TCC1-1 nil 3253536795 ("" (subtype-tcc) nil nil) nil nil)) (eq_partition_TCC2 0 (eq_partition_TCC2-1 nil 3253536795 ("" (skosimp*) (("" (case-replace "a!1 <= (b!1 * ii!1 - a!1 * ii!1) / (N!1 - 1) + a!1") (("1" (case-replace "(b!1 * ii!1 - a!1 * ii!1) / (N!1 - 1) + a!1 <= b!1") (("1" (assert) (("1" (lemma "connected_domain") (("1" (expand "connected?") (("1" (inst -1 "a!1" "b!1" "a!1 + ii!1 * (b!1 - a!1) / (N!1 - 1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (move-terms 1 l 2) (("2" (mult-by * "N!1-1") (("2" (factor 1 l) (("2" (typepred "ii!1") (("2" (name-replace "bma" "b!1-a!1") (("2" (div-by 1 "bma") (("1" (assert) nil nil) ("2" (reveal -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (move-terms 1 r 2) (("2" (assert) (("2" (mult-by * "N!1-1") (("2" (assert) (("2" (factor 1 r) (("2" (typepred "ii!1") (("2" (lemma "pos_times_ge") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (<= const-decl "bool" reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (div_cancel2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (both_sides_div_pos_le1 formula-decl nil real_props nil) (bma skolem-const-decl "real" integral_def nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (times_div_cancel1 formula-decl nil extra_real_props nil) (times_div_cancel2 formula-decl nil extra_real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected? const-decl "bool" deriv_domain_def nil) (connected_domain formula-decl nil integral_def nil) (pos_times_ge formula-decl nil real_props nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil)) nil)) (eq_partition_TCC3 0 (eq_partition_TCC3-1 nil 3253536795 ("" (skosimp*) (("" (assert) (("" (prop) (("1" (move-terms 1 l 2) (("1" (mult-by 1 "N!1-1") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (transform-both 1 "%1 - a!1") (("1" (hide 2) (("1" (assert) (("1" (mult-by 1 "N!1-1") (("1" (name-replace "N1" "N!1-1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (below type-eq-decl nil naturalnumbers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (< const-decl "bool" reals nil) (div_cancel2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (both_sides_times1 formula-decl nil real_props nil)) nil)) (xis?_TCC1 0 (xis?_TCC1-1 nil 3610719253 ("" (subtype-tcc) nil nil) nil nil)) (xis_lem_TCC1 0 (xis_lem_TCC1-1 nil 3278409541 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (xis_lem_TCC2 0 (xis_lem_TCC2-1 nil 3278409541 ("" (skosimp*) (("" (assert) (("" (typepred "xis!1") (("" (assert) nil nil)) nil)) nil)) nil) ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (xis_lem 0 (xis_lem-1 nil 3278409455 ("" (auto-rewrite "xis?") (("" (skosimp*) (("" (assert) (("" (typepred "xis!1") (("" (assert) (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ((xis? const-decl "bool" integral_def nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (T_pred const-decl "[real -> boolean]" integral_def 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) (T formal-subtype-decl nil integral_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (Rie_sum_TCC1 0 (Rie_sum_TCC1-1 nil 3278175567 ("" (skosimp*) (("" (assert) (("" (typepred "xis!1") (("" (assert) nil nil)) nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (Rie_sum_TCC2 0 (Rie_sum_TCC2-1 nil 3278691242 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (Rie_sum_TCC3 0 (Rie_sum_TCC3-1 nil 3278691242 ("" (skosimp*) (("" (assert) nil nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (Rie_sum_TCC4 0 (Rie_sum_TCC4-1 nil 3278691242 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (Rie_sum_TCC5 0 (Rie_sum_TCC5-1 nil 3278691242 ("" (skosimp*) (("" (assert) (("" (typepred "xis!1") (("" (assert) nil nil)) nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (Rie_sum_TCC6 0 (Rie_sum_TCC6-1 nil 3278691242 ("" (skosimp*) (("" (assert) nil nil)) 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) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (Rie_sec_TCC1 0 (Rie_sec_TCC1-1 nil 3278154574 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (Rie_sec_TCC2 0 (Rie_sec_TCC2-1 nil 3278154574 ("" (skosimp*) (("" (assert) nil nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (Rie_sec_TCC3 0 (Rie_sec_TCC3-1 nil 3278154574 ("" (skosimp*) (("" (assert) nil nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (Rie_sum_alt_TCC1 0 (Rie_sum_alt_TCC1-1 nil 3278324172 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (xis? const-decl "bool" integral_def nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil)) shostak)) (Rie_sum_alt_TCC2 0 (Rie_sum_alt_TCC2-1 nil 3278324172 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (xis? const-decl "bool" integral_def nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil)) shostak)) (Rie_sum_alt_TCC3 0 (Rie_sum_alt_TCC3-1 nil 3278324172 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (xis? const-decl "bool" integral_def nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (upto nonempty-type-eq-decl nil naturalnumbers nil)) shostak)) (Rie_sum_alt_TCC4 0 (Rie_sum_alt_TCC4-1 nil 3278324172 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (xis? const-decl "bool" integral_def nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (integer nonempty-type-from-decl nil integers nil)) shostak)) (Rie_sum_alt_lem 0 (Rie_sum_alt_lem-3 nil 3280252836 ("" (skosimp*) (("" (expand "Rie_sum") (("" (assert) (("" (expand "Rie_sum_alt") (("" (expand "Rie_sec") (("" (assert) (("" (case "FORALL (NN: below(length(P!1)-1)): sigma[below(length(P!1) - 1)] (0, NN, LAMBDA (n: below(length(P!1) - 1)): P!1`seq(1 + n) * f!1(xis!1(n)) - P!1`seq(n) * f!1(xis!1(n))) = sigma[upto(length(P!1) - 1)] (1, NN+1, LAMBDA (n: upto(length(P!1) - 1)): IF n = 0 THEN 0 ELSE P!1`seq(n) * f!1(xis!1(n - 1)) - P!1`seq(n - 1) * f!1(xis!1(n - 1)) ENDIF)") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "NN" 1 "below_induction[length(P!1)-1]") (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (assert) nil nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (Rie_sum const-decl "real" integral_def nil) (Rie_sum_alt const-decl "real" integral_def nil) (below_induction formula-decl nil bounded_nat_inductions nil) (pred type-eq-decl nil defined_types nil) (P!1 skolem-const-decl "partition(a!1, b!1)" integral_def nil) (b!1 skolem-const-decl "T" integral_def nil) (a!1 skolem-const-decl "T" integral_def nil) (int_plus_int_is_int application-judgement "int" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (xis? const-decl "bool" integral_def nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (Rie_sec const-decl "real" integral_def 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) (int_minus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (= const-decl "[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) (T formal-subtype-decl nil integral_def nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil) (Rie_sum_alt_lem-2 nil 3280252800 ("" (skosimp*) (("" (expand "Rie_sum") (("" (assert) (("" (expand "Rie_sum_alt") (("" (expand "Rie_sec") (("" (assert) (("" (assert) (("" (case "FORALL (NN: below(length(P!1)-1)): sigma[below(length(P!1) - 1)] (0, NN, LAMBDA (n: below(length(P!1) - 1)): P!1`seq(1 + n) * f!1(xis!1(n)) - P!1`seq(n) * f!1(xis!1(n))) = sigma[upto(length(P!1) - 1)] (1, NN+1, LAMBDA (n: upto(length(P!1) - 1)): IF n = 0 THEN 0 ELSE P!1`seq(n) * f!1(xis!1`seq(n - 1)) - P!1`seq(n - 1) * f!1(xis!1`seq(n - 1)) ENDIF)") (("1" (inst?) (("1" (assert) nil))) ("2" (hide 2) (("2" (induct "NN" 1 "below_induction[length(P!1)-1]") (("1" (assert) (("1" (expand "sigma") (("1" (propax) nil))))) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (assert) nil))))) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil))))) ("4" (skosimp*) (("4" (assert) nil))) ("5" (skosimp*) (("5" (hide 3) (("5" (assert) (("5" (typepred "xis!1") (("5" (expand "xis?") (("5" (propax) nil))))))))))) ("6" (assert) (("6" (hide 2) (("6" (skosimp*) (("6" (assert) nil))))))) ("7" (skosimp*) (("7" (assert) (("7" (hide 2) (("7" (typepred "xis!1") (("7" (assert) nil))))))))))))) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil))))) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil))))) ("5" (hide 2) (("5" (skosimp*) (("5" (assert) (("5" (typepred "xis!1") (("5" (assert) nil))))))))) ("6" (hide 2) (("6" (skosimp*) (("6" (assert) nil))))) ("7" (hide 2) (("7" (skosimp*) (("7" (assert) (("7" (typepred "xis!1") (("7" (assert) nil)))))))))))))))))))))))) nil) nil nil) (Rie_sum_alt_lem-1 nil 3278324183 ("" (skosimp*) (("" (expand "Rie_sum") (("" (assert) (("" (expand "Rie_sum_alt") (("" (expand "Rie_sec") (("" (assert) (("" (assert) (("" (case "FORALL (NN: below(length(P!1)-1)): sigma[below(length(P!1) - 1)] (0, NN, LAMBDA (n: below(length(P!1) - 1)): P!1`seq(1 + n) * f!1(xis!1`seq(n)) - P!1`seq(n) * f!1(xis!1`seq(n))) = sigma[upto(length(P!1) - 1)] (1, NN+1, LAMBDA (n: upto(length(P!1) - 1)): IF n = 0 THEN 0 ELSE P!1`seq(n) * f!1(xis!1`seq(n - 1)) - P!1`seq(n - 1) * f!1(xis!1`seq(n - 1)) ENDIF)") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "NN" 1 "below_induction[length(P!1)-1]") (("1" (assert) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (assert) nil nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (hide 3) (("5" (assert) (("5" (typepred "xis!1") (("5" (expand "xis?") (("5" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("6" (assert) (("6" (hide 2) (("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil)) nil) ("7" (skosimp*) (("7" (assert) (("7" (hide 2) (("7" (typepred "xis!1") (("7" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) (("5" (assert) (("5" (typepred "xis!1") (("5" (assert) nil nil)) nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp*) (("7" (assert) (("7" (typepred "xis!1") (("7" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma def-decl "real" sigma "reals/")) shostak)) (x_in_TCC1 0 (x_in_TCC1-1 nil 3253536795 ("" (inst + "(LAMBDA (aa: T, bb:{x: T | aa < x}): choose({t: T | aa <= t AND t <= bb}))") (("" (skosimp*) (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (inst - "(aa!1+bb!1)/2") (("1" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (expand "connected?") (("2" (inst -1 "aa!1" "bb!1" "_") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (aa!1 skolem-const-decl "T" integral_def nil) (bb!1 skolem-const-decl "{x: T | aa!1 < x}" integral_def nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected? const-decl "bool" deriv_domain_def nil) (connected_domain formula-decl nil integral_def nil) (member const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (T formal-subtype-decl nil integral_def nil)) nil)) (pick_one_TCC1 0 (pick_one_TCC1-1 nil 3277644518 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil)) shostak)) (gen_xis_TCC1 0 (gen_xis_TCC1-1 nil 3277144019 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (pick_one const-decl "real" integral_def nil) (xis? const-decl "bool" integral_def nil)) shostak)) (len_eq_part 0 (len_eq_part-1 nil 3253536795 ("" (grind) nil nil) ((real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (eq_partition const-decl "partition(a, b)" integral_def nil)) nil)) (eq_part_lem_a_TCC1 0 (eq_part_lem_a_TCC1-1 nil 3253536795 ("" (subtype-tcc) nil nil) ((real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (eq_partition const-decl "partition(a, b)" integral_def nil)) nil)) (eq_part_lem_a 0 (eq_part_lem_a-1 nil 3253536795 ("" (grind) nil nil) ((real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (eq_partition const-decl "partition(a, b)" integral_def nil)) nil)) (eq_part_lem_b_TCC1 0 (eq_part_lem_b_TCC1-1 nil 3253536795 ("" (subtype-tcc) nil nil) ((real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (eq_partition const-decl "partition(a, b)" integral_def nil)) nil)) (eq_part_lem_b 0 (eq_part_lem_b-1 nil 3253536795 ("" (skosimp*) (("" (expand "eq_partition") (("" (move-terms 1 l 2) (("" (mult-by 1 "N!1-1") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (eq_partition const-decl "partition(a, b)" integral_def nil) (both_sides_times1 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel2 formula-decl nil real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (T formal-subtype-decl nil integral_def nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (above nonempty-type-eq-decl nil integers 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) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (number_field nonempty-type-from-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) nil)) (width_eq_part_TCC1 0 (width_eq_part_TCC1-1 nil 3253536795 ("" (skosimp*) (("" (grind) nil nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (width_eq_part 0 (width_eq_part-1 nil 3253536795 ("" (skosimp*) (("" (name-replace "PP" "eq_partition(a!1, b!1, N!1)") (("" (typepred "width(a!1, b!1, PP)") (("1" (expand "width") (("1" (typepred "max({l: real | EXISTS (ii: below(length(PP) - 1)): l = seq(PP)(1 + ii) - seq(PP)(ii)})") (("1" (skosimp*) (("1" (replace -1) (("1" (reveal -1) (("1" (expand "eq_partition") (("1" (replace -1 + rl) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "width_TCC3") (("2" (inst -1 "a!1" "b!1" "PP" "seq(PP)") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil) ((nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (< const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (>= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (eq_partition const-decl "partition(a, b)" integral_def nil) (width_TCC3 subtype-tcc nil integral_def nil) (b!1 skolem-const-decl "T" integral_def nil) (a!1 skolem-const-decl "T" integral_def nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (max const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" finite_sets_minmax "finite_sets/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (width const-decl "posreal" integral_def nil)) nil)) (N_from_delta_TCC1 0 (N_from_delta_TCC1-1 nil 3282565249 ("" (skosimp*) (("" (case-replace "(b!1 - a!1) / delta!1 > 0") (("1" (assert) nil nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil) ((real_div_nzreal_is_real application-judgement "real" reals nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (> const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (N_from_delta 0 (N_from_delta-2 nil 3306078556 ("" (skosimp*) (("" (assert) (("" (case "(b!1 - a!1) / delta!1 > 0") (("1" (lemma "width_eq_part") (("1" (inst?) (("1" (assert) (("1" (name-replace "EP" "eq_partition(a!1, b!1, 2 + floor((b!1 - a!1) / delta!1))") (("1" (typepred "floor((b!1 - a!1) / delta!1)") (("1" (name-replace "FL" "floor((b!1 - a!1) / delta!1)") (("1" (replace -3) (("1" (hide -3) (("1" (cross-mult -1) (("1" (cross-mult -2) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil) ((real_div_nzreal_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (width_eq_part formula-decl nil integral_def nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (div_mult_pos_le2 formula-decl nil real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (eq_partition const-decl "partition(a, b)" integral_def nil) (partition type-eq-decl nil integral_def nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (above nonempty-type-eq-decl nil integers 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) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (> const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil) (N_from_delta-1 nil 3282497555 ("" (skosimp*) (("" (assert) (("" (case "(b!1 - a!1) / delta!1 > 0") (("1" (lemma "width_eq_part[T]") (("1" (inst?) (("1" (assert) (("1" (name-replace "EP" "eq_partition(a!1, b!1, 2 + floor((b!1 - a!1) / delta!1))") (("1" (typepred "floor((b!1 - a!1) / delta!1)") (("1" (name-replace "FL" "floor((b!1 - a!1) / delta!1)") (("1" (replace -3) (("1" (hide -3) (("1" (cross-mult -1) (("1" (cross-mult -2) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil) nil nil)) (Riemann?_Rie 0 (Riemann?_Rie-1 nil 3278177085 ("" (skosimp*) (("" (expand "Riemann_sum?") (("" (inst?) nil nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (Riemann_sum? const-decl "bool" integral_def nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil nat_types nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (xis? const-decl "bool" integral_def nil)) shostak)) (integral_unique 0 (integral_unique-1 nil 3277652331 ("" (skosimp*) (("" (expand "integral?") (("" (case-replace "(FORALL (EPS: posreal): abs(A1!1 - A2!1) < 2*EPS)") (("1" (hide -3 -4) (("1" (case "A1!1 > A2!1") (("1" (inst -2 "(A1!1 - A2!1)/2") (("1" (grind) nil nil) ("2" (assert) nil nil)) nil) ("2" (inst -1 "(A2!1 - A1!1)/2") (("1" (grind) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (inst -2 "EPS!1") (("2" (inst - "EPS!1") (("2" (skosimp*) (("2" (name "DELTA" "real_defs.min(delta!1,delta!2)") (("2" (case "2 + floor((b!1 - a!1) / DELTA) > 1") (("1" (name "NN" "2 + floor((b!1 - a!1) / DELTA)") (("1" (replace -1) (("1" (inst - "eq_partition(a!1,b!1,NN)") (("1" (inst - "eq_partition(a!1,b!1,NN)") (("1" (split -5) (("1" (split -6) (("1" (name "S" "Rie_sum(a!1, b!1, eq_partition(a!1, b!1,NN ), gen_xis(a!1,b!1,eq_partition(a!1, b!1,NN )), f!1)") (("1" (inst - "S") (("1" (inst - "S") (("1" (hide-all-but (-2 -3 1)) (("1" (grind) nil nil)) nil) ("2" (hide 2) (("2" (lemma "Riemann?_Rie") (("2" (inst - "a!1" "b!1" "f!1") (("2" (split -1) (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "Riemann?_Rie") (("2" (inst - "a!1" "b!1" "f!1") (("2" (split -1) (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (rewrite "width_eq_part") (("2" (case "DELTA <= delta!2") (("1" (hide -4) (("1" (case "(b!1 - a!1) / DELTA < NN-1") (("1" (hide -3) (("1" (mult-by -1 "DELTA") (("1" (mult-by 1 "NN-1") (("1" (mult-by -2 "NN-1") (("1" (assert) nil nil)) nil) ("2" (hide -1 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide -5 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -5 2) (("2" (rewrite "width_eq_part") (("2" (case "DELTA <= delta!1") (("1" (hide -4) (("1" (case "(b!1 - a!1) / DELTA < NN-1") (("1" (hide -3) (("1" (mult-by -1 "DELTA") (("1" (mult-by 1 "NN-1") (("1" (mult-by -2 "NN-1") (("1" (assert) nil nil)) nil) ("2" (hide -1 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3 -4 2) (("2" (mult-by 1 "DELTA") (("2" (assert) (("2" (move-terms 1 l 1) (("2" (auto-rewrite-theory "real_props") (("2" (assert) (("2" (lemma "pos_div_ge") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (integral? const-decl "bool" integral_def nil) (T formal-subtype-decl nil integral_def nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (integer nonempty-type-from-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) (int_plus_int_is_int application-judgement "int" integers nil) (Riemann_sum? const-decl "bool" integral_def nil) (f!1 skolem-const-decl "[T -> real]" integral_def nil) (S skolem-const-decl "real" integral_def nil) (Riemann?_Rie formula-decl nil integral_def nil) (gen_xis const-decl "(xis?(a, b, P))" integral_def nil) (Rie_sum const-decl "real" integral_def nil) (xis? const-decl "bool" integral_def nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (div_cancel2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (width_eq_part formula-decl nil integral_def nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil naturalnumbers nil) (partition type-eq-decl nil integral_def nil) (above nonempty-type-eq-decl nil integers nil) (eq_partition const-decl "partition(a, b)" integral_def nil) (NN skolem-const-decl "int" integral_def nil) (b!1 skolem-const-decl "T" integral_def nil) (a!1 skolem-const-decl "T" integral_def nil) (int nonempty-type-eq-decl nil integers nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (real_plus_real_is_real application-judgement "real" reals nil) (both_sides_times_pos_gt1 formula-decl nil real_props nil) (pos_div_ge formula-decl nil real_props nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (posreal_min application-judgement "{z: posreal | z <= x AND z <= y}" real_defs nil) (minus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (A1!1 skolem-const-decl "real" integral_def nil) (A2!1 skolem-const-decl "real" integral_def nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (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) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil)) nil)) (integral_TCC1 0 (integral_TCC1-1 nil 3253536795 ("" (inst + "(LAMBDA (d: [a: T, b: {x: T | a < x}, {f | integrable?(a, b, f)}]): choose({S: real | integral?(d`1 (("" (skosimp*) (("" (typepred "d!1`3") (("" (expand "integrable?") (("" (expand "nonempty?") (("" (skosimp*) (("" (expand "empty?") (("" (expand "member") (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (integral? const-decl "bool" integral_def nil) (integrable? const-decl "bool" integral_def nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (T formal-subtype-decl nil integral_def nil)) nil)) (integral_def 0 (integral_def-1 nil 3253536795 ("" (skosimp*) (("" (expand "integrable?") (("" (typepred "integral(a!1, b!1, f!1)") (("1" (ground) (("1" (lemma "integral_unique") (("1" (inst?) (("1" (inst -1 "integral(a!1, b!1, f!1)") (("1" (assert) (("1" (inst + "s!1") nil nil)) nil) ("2" (hide 2) (("2" (expand "integrable?") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "integral_unique") (("2" (inst?) (("2" (inst -1 "integral(a!1, b!1, f!1)") (("1" (assert) nil nil) ("2" (expand "integrable?") (("2" (inst + "s!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "integrable?") (("2" (inst?) (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil)) nil)) nil) ((integrable? const-decl "bool" integral_def nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (integral_unique formula-decl nil integral_def nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-subtype-decl nil integral_def nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (< const-decl "bool" reals nil) (integral? const-decl "bool" integral_def nil) (integral const-decl "{S: real | integral?(a, b, ff, S)}" integral_def nil)) nil)) (integral_restrict_eq 0 (integral_restrict_eq-3 nil 3280252877 ("" (skosimp*) (("" (rewrite "integral_def") (("" (typepred "integral(a!1, b!1, f!1)") (("1" (expand "integral?") (("1" (skosimp*) (("1" (inst - "epsi!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "P!1") (("1" (assert) (("1" (typepred "integral(a!1, b!1, f!1)") (("1" (inst - "R!1") (("1" (typepred "R!1") (("1" (hide 2) (("1" (expand "Riemann_sum?") (("1" (skosimp*) (("1" (inst + "xis!1") (("1" (assert) (("1" (replace -1) (("1" (expand "Rie_sum") (("1" (assert) (("1" (rewrite "sigma_restrict_eq") (("1" (hide 2) (("1" (hide -1) (("1" (expand "restrict") (("1" (apply-extensionality :hide? t) (("1" (inst - "xis!1(x!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil) ((integral_def formula-decl nil integral_def nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (integrable? const-decl "bool" integral_def nil) (integral? const-decl "bool" integral_def nil) (integral const-decl "{S: real | integral?(a, b, ff, S)}" integral_def nil) (real_minus_real_is_real application-judgement "real" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (int_minus_int_is_int application-judgement "int" integers nil) (xis? const-decl "bool" integral_def nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (restrict const-decl "[T -> real]" sigma "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (sigma_restrict_eq formula-decl nil 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) (R!1 skolem-const-decl "(Riemann_sum?(a!1, b!1, P!1, g!1))" integral_def nil) (g!1 skolem-const-decl "[T -> real]" integral_def nil) (f!1 skolem-const-decl "[T -> real]" integral_def nil) (P!1 skolem-const-decl "partition(a!1, b!1)" integral_def nil) (b!1 skolem-const-decl "T" integral_def nil) (a!1 skolem-const-decl "T" integral_def nil) (Riemann_sum? const-decl "bool" integral_def nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil)) nil) (integral_restrict_eq-2 nil 3277652385 ("" (skosimp*) (("" (rewrite "integral_def") (("" (typepred "integral(a!1, b!1, f!1)") (("1" (expand "integral?") (("1" (skosimp*) (("1" (inst - "epsi!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "P!1") (("1" (assert) (("1" (typepred "integral(a!1, b!1, f!1)") (("1" (inst - "R!1") (("1" (typepred "R!1") (("1" (hide 2) (("1" (expand "Riemann_sum?") (("1" (skosimp*) (("1" (inst + "xis!1") (("1" (assert) (("1" (replace -1) (("1" (expand "Rie_sum") (("1" (assert) (("1" (rewrite "sigma_restrict_eq") (("1" (hide 2) (("1" (hide -1) (("1" (expand "restrict") (("1" (apply-extensionality :hide? t) (("1" (inst - "xis!1`seq(x!1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (typepred "xis!1") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "xis!1") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (typepred "xis!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil) ((restrict const-decl "[T -> real]" sigma "reals/") (sigma_restrict_eq formula-decl nil sigma "reals/")) nil) (integral_restrict_eq-1 nil 3262002842 ("" (skosimp*) (("" (rewrite "integral_def") (("" (typepred "integral(a!1, b!1, f!1)") (("1" (expand "is_integral") (("1" (skosimp*) (("1" (inst - "epsi!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "P!1") (("1" (assert) (("1" (name "RS1" "Riemann_sum(a!1, b!1, P!1, f!1)") (("1" (replace -1) (("1" (name "RS2" "Riemann_sum(a!1, b!1, P!1, g!1)") (("1" (replace -1) (("1" (case "RS1 = RS2") (("1" (assert) nil nil) ("2" (hide -3 -7 2) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "Riemann_sum") (("2" (rewrite "sigma_restrict_eq") (("1" (hide 2) (("1" (expand "restrict") (("1" (apply-extensionality 1 :hide? t) (("1" (lift-if) (("1" (ground) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (typepred "P!1") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (typepred "P!1") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil) ((restrict const-decl "[T -> real]" sigma "reals/") (sigma_restrict_eq formula-decl nil sigma "reals/")) nil)) (Integral_TCC1 0 (Integral_TCC1-1 nil 3253536795 ("" (skosimp*) (("" (typepred "f!1") (("" (expand "Integrable?") (("" (assert) nil nil)) nil)) nil)) nil) ((Integrable_funs type-eq-decl nil integral_def nil) (Integrable? const-decl "bool" integral_def nil) (T formal-subtype-decl nil integral_def nil) (T_pred const-decl "[real -> boolean]" integral_def 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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (Integral_TCC2 0 (Integral_TCC2-1 nil 3277142737 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (Integrable? const-decl "bool" integral_def nil) (Integrable_funs type-eq-decl nil integral_def nil) (width const-decl "posreal" integral_def nil) (integral? const-decl "bool" integral_def nil) (integrable? const-decl "bool" integral_def nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (Integral_TCC3 0 (Integral_TCC3-1 nil 3277142737 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (Integrable? const-decl "bool" integral_def nil) (Integrable_funs type-eq-decl nil integral_def nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (width const-decl "posreal" integral_def nil) (integral? const-decl "bool" integral_def nil) (integrable? const-decl "bool" integral_def nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (Integrable?_rew 0 (Integrable?_rew-1 nil 3610700218 ("" (skosimp*) (("" (expand "Integrable?") (("" (assert) nil nil)) nil)) nil) ((Integrable? const-decl "bool" integral_def nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (Integral_rew_TCC1 0 (Integral_rew_TCC1-1 nil 3610459511 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_def nil) (T formal-subtype-decl nil integral_def nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (width const-decl "posreal" integral_def nil) (integral? const-decl "bool" integral_def nil) (integrable? const-decl "bool" integral_def nil) (Integrable? const-decl "bool" integral_def nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (Integral_rew 0 (Integral_rew-1 nil 3610700253 ("" (skosimp*) (("" (assert) (("" (expand "Integral") (("" (propax) nil nil)) nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Integral const-decl "real" integral_def nil)) shostak)))
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.107Bemerkung: (vorverarbeitet am 2026-05-06) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26