| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 636 kB |
|
Impressum rs_partition.prfSprache: Lisp |
|||||||||||||||
|
(rs_partition (partition_pred?_TCC1 0 (partition_pred?_TCC1-1 nil 3511259225 ("" (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]" rs_partition nil) (T formal-nonempty-subtype-decl nil rs_partition 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) (default const-decl "T" fseqs "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)) nil)) (partition_strictly_sort 0 (partition_strictly_sort-1 nil 3491659656 ("" (auto-rewrite + "member") (("" (skeep) (("" (skeep) (("" (assert) (("" (case "NOT strictly_sort(P)`length > 1") (("1" (hide 2) (("1" (typepred "strictly_sort(P)") (("1" (inst-cp - "a") (("1" (inst - "b") (("1" (case "member(a,P) and member(b,P)") (("1" (flatten) (("1" (replace -1) (("1" (replace -2) (("1" (expand "member") (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (split +) (("1" (inst + "0") (("1" (assert) nil nil)) nil) ("2" (inst + "P`length-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (split +) (("1" (typepred "strictly_sort(P)") (("1" (inst-cp - "strictly_sort(P)`seq(0)") (("1" (inst - "a") (("1" (case "member(a,P) AND member(strictly_sort(P)`seq(0), strictly_sort(P))") (("1" (flatten) (("1" (replace -1) (("1" (replace -2) (("1" (assert) (("1" (hide -1) (("1" (hide -1) (("1" (skosimp*) (("1" (expand "strictly_increasing?") (("1" (inst - "0" "i!1") (("1" (assert) (("1" (typepred "P") (("1" (expand "increasing?") (("1" (inst - "0" "i!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (assert) (("2" (split) (("1" (inst + "0") (("1" (assert) nil nil)) nil) ("2" (inst + "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "strictly_sort(P)") (("2" (inst-cp - "strictly_sort(P)`seq(strictly_sort(P)`length-1)") (("2" (inst - "b") (("2" (case "member(b,P) AND member(strictly_sort(P)`seq(strictly_sort(P)`length-1), stric (("1" (flatten) (("1" (replace -1) (("1" (replace -2) (("1" (assert) (("1" (hide -1) (("1" (hide -1) (("1" (skosimp*) (("1" (expand "strictly_increasing?") (("1" (inst - "i!1" "strictly_sort(P)`length-1") (("1" (assert) (("1" (typepred "P") (("1" (expand "increasing?") (("1" (inst - "i!2" "P`length-1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (assert) (("2" (split) (("1" (inst + "P`length-1") (("1" (assert) nil nil)) nil) ("2" (inst + "strictly_sort(P)`length-1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "strictly_sort(P)") (("3" (expand "strictly_increasing?") (("3" (expand "increasing?") (("3" (skeep) (("3" (inst - "i" "j") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (skeep) (("4" (typepred "strictly_sort(P)") (("4" (inst - "strictly_sort(P)`seq(i)") (("4" (case "member(strictly_sort(P)`seq(i),strictly_sort(P))") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (skolem - "iz") (("1" (replace -2) (("1" (typepred "P") (("1" (inst - "iz") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (assert) (("2" (inst + "i") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T_pred const-decl "[real -> boolean]" rs_partition nil) (T formal-nonempty-subtype-decl nil rs_partition nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (restrict const-decl "R" restrict nil) (<= const-decl "bool" reals nil) (strictly_increasing? const-decl "bool" sort_fseq "structures/") (IFF const-decl "[bool, bool -> bool]" booleans nil) (member const-decl "bool" fseqs "structures/") (strictly_sort const-decl "{ss: fseq | strictly_increasing?(ss) AND (FORALL (x: T): member(x, s) IFF member(x, ss))}" sort_fseq "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (increasing? const-decl "bool" sort_fseq "structures/") (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) (partition type-eq-decl nil rs_partition nil)) shostak)) (width_TCC1 0 (width_TCC1-1 nil 3253536795 ("" (skeep) (("" (skeep) (("" (split +) (("1" (lemma "is_finite_surj[real]") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (inst + "N" "(LAMBDA (ij:below[N]): IF ij = N-1 THEN xx(ij)-xx(ij-1) ELSE xx(ij+1)-xx(ij) ENDIF)") (("1" (expand "surjective?") (("1" (skosimp*) (("1" (typepred "y!1") (("1" (skosimp*) (("1" (inst + "ii!1") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "ij!1") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (replace -1) (("3" (assert) (("3" (inst + "N-2") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "empty?") (("2" (inst - "xx(1)-xx(0)") (("2" (assert) (("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (odd_plus_even_is_odd application-judgement "odd_int" integers 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) (is_finite_surj formula-decl nil finite_sets nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (N skolem-const-decl "nat" rs_partition nil) (below type-eq-decl nil nat_types nil) (xx skolem-const-decl "barray[T](P`length)" rs_partition nil) (P skolem-const-decl "partition(a, b)" rs_partition nil) (b skolem-const-decl "{x: T | a < x}" rs_partition nil) (a skolem-const-decl "T" rs_partition nil) (NOT const-decl "[bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_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) (surjective? const-decl "bool" functions nil) (ij!1 skolem-const-decl "below[N]" rs_partition nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (default const-decl "T" fseqs "structures/") (partition type-eq-decl nil rs_partition nil) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (> const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (width_TCC2 0 (width_TCC2-1 nil 3253536795 ("" (skosimp*) (("" (case "max[real, <=] ({l: real | EXISTS (ii: below(N!1 - 1)): l = xx!1(ii + 1) - xx!1(ii)}) > 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (typepred "P!1") (("2" (case "EXISTS (ii: below(N!1 - 1)): xx!1(ii + 1) - xx!1(ii) > 0") (("1" (name "mm" "max[real, <=] ({l: real | EXISTS (ii: below(N!1 - 1)): l = xx!1(ii + 1) - xx!1(ii)})") (("1" (replace -1) (("1" (typepred "mm") (("1" (skosimp*) (("1" (inst -2 "xx!1(ii!2 + 1) - xx!1(ii!2)") (("1" (assert) (("1" (inst + "ii!2") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "width_TCC1") (("2" (inst?) (("2" (assert) (("2" (inst - "N!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "FORALL (ii:below(N!1)): xx!1(ii) = a!1") (("1" (inst - "N!1-1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (induct "ii") (("1" (assert) nil nil) ("2" (skosimp*) (("2" (assert) (("2" (inst + "jb!1") (("2" (assert) (("2" (inst - "jb!1+1") (("2" (inst - "jb!1+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "width_TCC1") (("3" (inst?) (("3" (assert) (("3" (inst - "N!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (default const-decl "T" fseqs "structures/") (partition type-eq-decl nil rs_partition nil) (increasing? const-decl "bool" sort_fseq "structures/") (restrict const-decl "R" restrict nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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) (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) (NOT const-decl "[bool -> bool]" booleans 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 "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_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) (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) (pred type-eq-decl nil defined_types nil) (below_induction formula-decl nil bounded_nat_inductions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (N!1 skolem-const-decl "nat" rs_partition nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (width_TCC1 subtype-tcc nil rs_partition nil)) nil)) (width_lem 0 (width_lem-1 nil 3253536795 ("" (skosimp*) (("" (assert) (("" (expand "width") (("" (typepred "max({l: real | EXISTS (ii: below(P!1`length - 1)): l = P!1`seq(1 + ii) - P!1`seq(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_TCC1") (("2" (inst - "a!1" "b!1" "P!1" "P!1`seq") (("2" (inst - "P!1`length") (("2" (ground) 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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 rs_partition nil) (below type-eq-decl nil naturalnumbers nil) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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_TCC1 subtype-tcc nil rs_partition nil) (default const-decl "T" fseqs "structures/") (width const-decl "posreal" rs_partition nil)) nil)) (width_lem_exists 0 (width_lem_exists-1 nil 3489487957 ("" (skeep) (("" (skeep) (("" (expand "width") (("" (typepred "max({l: real | EXISTS (ii: below(P`length - 1)): l = P`seq(1 + ii) - P`seq(ii)})") (("1" (propax) nil nil) ("2" (hide 2) (("2" (assert) (("2" (lemma "width_TCC1") (("2" (inst - "a" "b" "P" "P`seq") (("2" (assert) (("2" (inst - "P`length") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((+ const-decl "[numfield, numfield -> numfield]" number_fields 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 rs_partition nil) (below type-eq-decl nil naturalnumbers nil) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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) (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) (default const-decl "T" fseqs "structures/") (width_TCC1 subtype-tcc nil rs_partition nil) (width const-decl "posreal" rs_partition nil)) shostak)) (parts_order 0 (parts_order-1 nil 3253536795 ("" (skeep) (("" (typepred "P") (("" (expand "increasing?") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((partition type-eq-decl nil rs_partition 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) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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 - "a!1" "b!1" "P!1" "ii!1+1" "jj!1") (("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 rs_partition nil) (below type-eq-decl nil naturalnumbers nil) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (parts_order formula-decl nil rs_partition 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) (int_minus_int_is_int application-judgement "int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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 0 (part_in-1 nil 3253536795 ("" (skeep) (("" (name "mm" "max({ij:real | (EXISTS (km:below(length(P)-1)): ij = km) AND ij >= 0 AND x>=P`seq(ij)})") (("1" (typepred "mm") (("1" (skeep -1) (("1" (inst + "km") (("1" (assert) (("1" (inst - "1+mm") (("1" (assert) (("1" (inst + "1+mm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split +) (("1" (lemma "is_finite_surj") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (inst + "P`length-1" "(LAMBDA (pz:below[P`length-1]): IF x>=P`seq(pz) THEN pz ELSE 0 ENDIF)") (("1" (expand "surjective?") (("1" (skosimp*) (("1" (typepred "y!1") (("1" (skosimp*) (("1" (inst + "km!1") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "0") nil nil)) nil) ("3" (skosimp*) (("3" (assert) (("3" (inst + "pz!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "empty?") (("2" (inst - "0") (("2" (expand "member") (("2" (assert) (("2" (inst + "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ((partition type-eq-decl nil rs_partition nil) (below type-eq-decl nil naturalnumbers nil) (increasing? const-decl "bool" sort_fseq "structures/") (restrict const-decl "R" restrict nil) (> const-decl "bool" reals nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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) (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) (NOT const-decl "[bool -> bool]" booleans 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) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (a skolem-const-decl "T" rs_partition nil) (b skolem-const-decl "T" rs_partition nil) (P skolem-const-decl "partition(a, b)" rs_partition nil) (surjective? const-decl "bool" functions nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (x skolem-const-decl "T" rs_partition nil) (below type-eq-decl nil nat_types nil) (is_finite_surj formula-decl nil finite_sets nil) (member const-decl "bool" sets nil)) nil)) (part_in_strict_left 0 (part_in_strict_left-2 nil 3491222014 ("" (skeep) (("" (name "mm" "max({ij:real | (EXISTS (km:below(length(P)-1)): ij = km) AND ij >= 0 AND x>P`seq(ij)})") (("1" (typepred "mm") (("1" (skeep -1) (("1" (inst + "km") (("1" (assert) (("1" (inst - "1+mm") (("1" (assert) (("1" (inst + "1+mm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split +) (("1" (lemma "is_finite_surj") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (inst + "P`length-1" "(LAMBDA (pz:below[P`length-1]): IF x>P`seq(pz) THEN pz ELSE 0 ENDIF)") (("1" (expand "surjective?") (("1" (skosimp*) (("1" (typepred "y!1") (("1" (skosimp*) (("1" (inst + "km!1") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "0") nil nil)) nil) ("3" (skosimp*) (("3" (assert) (("3" (inst + "pz!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "empty?") (("2" (inst - "0") (("2" (expand "member") (("2" (assert) (("2" (inst + "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ((partition type-eq-decl nil rs_partition nil) (below type-eq-decl nil naturalnumbers nil) (increasing? const-decl "bool" sort_fseq "structures/") (restrict const-decl "R" restrict nil) (> const-decl "bool" reals nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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) (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) (NOT const-decl "[bool -> bool]" booleans 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) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (a skolem-const-decl "T" rs_partition nil) (b skolem-const-decl "T" rs_partition nil) (P skolem-const-decl "partition(a, b)" rs_partition nil) (surjective? const-decl "bool" functions nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (x skolem-const-decl "T" rs_partition nil) (below type-eq-decl nil nat_types nil) (is_finite_surj formula-decl nil finite_sets nil) (member const-decl "bool" sets nil)) nil) (part_in_strict_left-1 nil 3491221650 ("" (skeep) (("" (postpone) nil nil)) nil) 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 rs_partition nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil rs_partition 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) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (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) (closed_interval type-eq-decl nil intervals_real "reals/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (partition type-eq-decl nil rs_partition nil) (below type-eq-decl nil naturalnumbers nil) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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) (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*) (("" (lemma "connected_domain") (("" (expand "connected?") (("" (inst - "a!1" "b!1" "a!1 + ii!1 * (b!1 - a!1) / (N!1 - 1)") (("" (assert) (("" (hide 2) (("" (assert) (("" (split) (("1" (typepred "b!1") (("1" (typepred "ii!1") (("1" (case "ii!1/(N!1-1) > 0") (("1" (mult-by -4 "ii!1/(N!1-1)") (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "(b!1 * ii!1 - a!1 * ii!1) / (N!1 - 1) <= b!1-a!1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (cross-mult 1) (("2" (case "N!1-1 >= ii!1") (("1" (mult-by -1 "b!1-a!1") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((connected_domain formula-decl nil rs_partition nil) (real_plus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers 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]" rs_partition nil) (T formal-nonempty-subtype-decl nil rs_partition 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 "[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) (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 "[numfield, numfield -> numfield]" number_fields nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil integers nil) (div_mult_pos_gt1 formula-decl nil extra_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) (both_sides_times_pos_lt1 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) (N!1 skolem-const-decl "above(1)" rs_partition nil) (ii!1 skolem-const-decl "nat" rs_partition nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (NOT const-decl "[bool -> bool]" booleans nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (div_mult_pos_le1 formula-decl nil real_props nil) (<= const-decl "bool" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected? const-decl "bool" deriv_domain_def nil)) nil)) (eq_partition_TCC3 0 (eq_partition_TCC3-2 nil 3489310835 ("" (skosimp*) (("" (split) (("1" (assert) (("1" (skosimp*) (("1" (ground) (("1" (name "cv" "(ii!1 * b!1 - ii!1 * a!1) / (N!1 - 1)") (("1" (case "cv >=0 AND cv <= b!1-a!1") (("1" (flatten) (("1" (lemma "connected_domain") (("1" (expand "connected?") (("1" (inst - "a!1" "b!1" "a!1+cv") (("1" (assert) (("1" (replace -4) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (expand "cv" +) (("1" (cross-mult 1) (("1" (typepred "b!1") (("1" (mult-by -2 "ii!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "cv" +) (("2" (cross-mult 1) (("2" (case "ii!1<=N!1-1") (("1" (mult-by -1 "b!1-a!1") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((above nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (< const-decl "bool" reals nil) (T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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) (* 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) (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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (div_mult_pos_le1 formula-decl nil real_props nil) (cv skolem-const-decl "real" rs_partition nil) (NOT const-decl "[bool -> bool]" booleans nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (connected? const-decl "bool" deriv_domain_def nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (connected_domain formula-decl nil rs_partition nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (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)) nil) (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" (expand "increasing?") (("2" (skosimp*) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (case "(b!1-a!1)/(N!1-1)>0") (("1" (mult-by -1 "j!1-i!1") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (case "(b!1-a!1)/(N!1-1)>0") (("1" (assert) nil nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (assert) (("4" (split +) (("1" (case "(b!1-a!1)/(N!1-1)>0") (("1" (mult-by -1 "i!1") (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil) ("2" (case "i!1/(N!1-1) < 1") (("1" (mult-by -1 "b!1-a!1") (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((increasing? const-decl "bool" sort_fseq "structures/")) nil)) (eq_partition_TCC4 0 (eq_partition_TCC4-2 nil 3494850114 ("" (skosimp*) (("" (split) (("1" (assert) nil nil) ("2" (ground) nil nil) ("3" (lift-if) (("3" (ground) (("3" (field) nil nil)) nil)) nil) ("4" (expand "increasing?") (("4" (skosimp*) (("4" (lift-if) (("4" (lift-if) (("4" (assert) (("4" (case "(b!1-a!1)/(N!1-1)>=0") (("1" (mult-by -1 "j!1-i!1") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (skosimp*) (("5" (assert) (("5" (ground) (("1" (case "i!1/(N!1-1)>0") (("1" (mult-by -1 "b!1-a!1") (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil) ("2" (case "i!1/(N!1-1)<=1") (("1" (mult-by -1 "b!1-a!1") (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (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) (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 "boolean" notequal 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) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (< const-decl "bool" reals nil) (T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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 "[numfield, numfield -> numfield]" number_fields nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (both_sides_times1 formula-decl nil real_props nil) (- const-decl "[numfield -> numfield]" number_fields nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (>= const-decl "bool" reals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (div_mult_pos_le1 formula-decl nil real_props nil) (below type-eq-decl nil naturalnumbers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (both_sides_times_pos_gt1 formula-decl nil real_props nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil)) nil) (eq_partition_TCC4-1 nil 3494850020 ("" (subtype-tcc) nil nil) nil nil)) (len_eq_part 0 (len_eq_part-1 nil 3253536795 ("" (grind) nil nil) ((T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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) (default const-decl "T" fseqs "structures/") (eq_partition const-decl "partition(a, b)" rs_partition nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (eq_part_lem_a 0 (eq_part_lem_a-1 nil 3253536795 ("" (grind) nil nil) ((T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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) (default const-decl "T" fseqs "structures/") (eq_partition const-decl "partition(a, b)" rs_partition nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (eq_part_lem_b_TCC1 0 (eq_part_lem_b_TCC1-1 nil 3253536795 ("" (subtype-tcc) nil nil) 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)" rs_partition 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-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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)") (("" (expand "width") (("" (typepred "max({l: real | EXISTS (ii: below(PP`length - 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_TCC1") (("2" (inst -1 "a!1" "b!1" "PP" "seq(PP)") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nat nonempty-type-eq-decl nil naturalnumbers 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]" rs_partition nil) (T formal-nonempty-subtype-decl nil rs_partition nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (restrict const-decl "R" restrict nil) (<= const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/") (>= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (partition type-eq-decl nil rs_partition nil) (eq_partition const-decl "partition(a, b)" rs_partition nil) (width_TCC1 subtype-tcc nil rs_partition nil) (default const-decl "T" fseqs "structures/") (b!1 skolem-const-decl "T" rs_partition nil) (a!1 skolem-const-decl "T" rs_partition 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_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (max const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" finite_sets_minmax "finite_sets/") (+ const-decl "[numfield, numfield -> numfield]" number_fields 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" rs_partition 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]" rs_partition nil) (T formal-nonempty-subtype-decl nil rs_partition 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 rs_partition 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)" rs_partition nil) (partition type-eq-decl nil rs_partition nil) (below type-eq-decl nil naturalnumbers nil) (increasing? const-decl "bool" sort_fseq "structures/") (restrict const-decl "R" restrict nil) (= const-decl "[T, T -> boolean]" equalities nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (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]" rs_partition nil) (T formal-nonempty-subtype-decl nil rs_partition 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)) (partition_exists 0 (partition_exists-1 nil 3489488404 ("" (skeep) (("" (lemma "N_from_delta") (("" (inst - "a" "b" "delta") (("" (assert) (("" (inst?) nil nil)) nil)) nil)) nil)) nil) ((N_from_delta formula-decl nil rs_partition 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) (real_div_nzreal_is_real application-judgement "real" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (AND const-decl "[bool, bool -> bool]" booleans 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) (restrict const-decl "R" restrict nil) (<= const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/") (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) (partition type-eq-decl nil rs_partition nil) (above nonempty-type-eq-decl nil integers nil) (eq_partition const-decl "partition(a, b)" rs_partition nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (integer nonempty-type-from-decl nil integers nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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)) shostak)) (partjoin_TCC1 0 (partjoin_TCC1-1 nil 3489488725 ("" (subtype-tcc) nil nil) nil nil)) (partjoin_TCC2 0 (partjoin_TCC2-1 nil 3489488725 ("" (subtype-tcc) nil nil) nil nil)) (partjoin_TCC3 0 (partjoin_TCC3-2 nil 3489488780 ("" (skosimp*) (("" (expand "increasing?") (("" (split) (("1" (expand "concat") (("1" (expand "o") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "concat") (("2" (expand "o") (("2" (assert) nil nil)) nil)) nil) ("3" (expand "concat") (("3" (expand "o") (("3" (lift-if) (("3" (assert) (("3" (ground) (("1" (case "delete[T](0,Pbc!1)`length >= 1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -1) (("2" (expand "delete") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 1) (("2" (expand "delete") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (assert) (("4" (skeep) (("4" (expand "concat") (("4" (expand "o") (("4" (expand "delete") (("4" (lift-if) (("4" (lift-if) (("4" (assert) (("4" (ground) (("1" (lemma "parts_order") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (typepred "Pab!1") (("2" (inst - "i") (("2" (typepred "Pbc!1") (("2" (inst - "1-Pab!1`length+j") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "parts_order") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (skosimp*) (("5" (typepred "i!1") (("5" (expand "concat") (("5" (expand "o") (("5" (lift-if) (("5" (assert) (("5" (ground) (("1" (typepred "Pab!1") (("1" (ground) (("1" (inst?) (("1" (flatten) nil nil)) nil)) nil)) nil) ("2" (typepred "Pab!1") (("2" (inst - "i!1") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (expand "delete") (("3" (typepred "Pbc!1") (("3" (inst - "1-Pab!1`length+i!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("4" (expand "delete") (("4" (typepred "Pbc!1") (("4" (inst - "1-Pab!1`length+i!1") (("1" (ground) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((increasing? const-decl "bool" sort_fseq "structures/") (i!1 skolem-const-decl "below((Pab!1 o delete(0, Pbc!1))`length)" rs_partition nil) (Pbc!1 skolem-const-decl "partition(b!1, c!1)" rs_partition nil) (c!1 skolem-const-decl "{cc: T | b!1 < cc}" rs_partition nil) (Pab!1 skolem-const-decl "partition(a!1, b!1)" rs_partition nil) (b!1 skolem-const-decl "{bb: T | a!1 < bb}" rs_partition nil) (a!1 skolem-const-decl "T" rs_partition nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (parts_order formula-decl nil rs_partition nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (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) (T_pred const-decl "[real -> boolean]" rs_partition nil) (T formal-nonempty-subtype-decl nil rs_partition nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (> const-decl "bool" reals nil) (ne_fseq type-eq-decl nil fseqs "structures/") (delete const-decl "fseq" fseqs_ops "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (restrict const-decl "R" restrict nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (partition type-eq-decl nil rs_partition 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) (concat macro-decl "fseq" fseqs "structures/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (O const-decl "fseq" fseqs "structures/")) nil) (partjoin_TCC3-1 nil 3489488725 ("" (subtype-tcc) nil nil) nil nil)) (partjoin_def_TCC1 0 (partjoin_def_TCC1-1 nil 3489490276 ("" (subtype-tcc) nil nil) ((bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (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) (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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (partition type-eq-decl nil rs_partition nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (> const-decl "bool" reals nil) (T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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) (delete const-decl "fseq" fseqs_ops "structures/") (default const-decl "T" fseqs "structures/") (O const-decl "fseq" fseqs "structures/") (partjoin const-decl "partition(a, c)" rs_partition nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (partjoin_def 0 (partjoin_def-1 nil 3489490276 ("" (skeep) (("" (skeep) (("" (skoletin 1) (("1" (assert) (("1" (ground) (("1" (expand "Pac") (("1" (expand "partjoin" 1) (("1" (expand "o") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (case "n = Pab`length -1") (("1" (replace -1 +) (("1" (assert) (("1" (expand "Pac" +) (("1" (expand "partjoin" +) (("1" (expand "o" +) (("1" (typepred "Pab") (("1" (typepred "Pbc") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "Pac" +) (("2" (expand "partjoin" +) (("2" (expand "o") (("2" (assert) (("2" (lift-if) (("2" (ground) (("1" (expand "delete") (("1" (propax) nil nil)) nil) ("2" (expand "delete") (("2" (expand "Pac" -2) (("2" (expand "partjoin" -2) (("2" (expand "o") (("2" (expand "delete") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (delete const-decl "fseq" fseqs_ops "structures/") (Pac skolem-const-decl "partition(a, c)" rs_partition nil) (O const-decl "fseq" fseqs "structures/") (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) (IFF const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partjoin const-decl "partition(a, c)" rs_partition nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (partition type-eq-decl nil rs_partition 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) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil)) shostak)) (partjoin_width_TCC1 0 (partjoin_width_TCC1-1 nil 3489488725 ("" (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]" rs_partition nil) (T formal-nonempty-subtype-decl nil rs_partition 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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (partition type-eq-decl nil rs_partition 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) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil)) nil)) (partjoin_width 0 (partjoin_width-2 nil 3495196567 ("" (auto-rewrite + "member") (("" (skeep) (("" (skeep) (("" (case "width(a, c, partjoin(a, b, c)(Pab, Pbc)) >= max(width(a, b, Pab), width(b, c, Pbc))") (("1" (lemma "width_lem_exists") (("1" (inst - "a" "c") (("1" (assert) (("1" (inst - "partjoin(a, b, c)(Pab, Pbc)") (("1" (skosimp*) (("1" (lemma "width_lem_exists") (("1" (inst - "a" "b") (("1" (assert) (("1" (inst - "Pab") (("1" (skosimp*) (("1" (lemma "width_lem_exists") (("1" (inst - "b" "c") (("1" (assert) (("1" (inst - "Pbc") (("1" (skosimp*) (("1" (assert) (("1" (name "PJ" "partjoin(a, b, c)(Pab, Pbc)") (("1" (replace -1) (("1" (name "wab" "width(a,b,Pab)") (("1" (replace -1) (("1" (name "wbc" "width(b,c,Pbc)") (("1" (replace -1) (("1" (name "wac" "width(a,c,PJ)") (("1" (replace -1) (("1" (expand "partjoin") (("1" (expand "o") (("1" (replace -4 -7 :dir rl) (("1" (assert) (("1" (expand "delete") (("1" (assert) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (lemma "width_lem") (("1" (inst - "a" "b" "Pab" "ii!1") (("1" (assert) nil nil)) nil)) nil) ("2" (case "1+ii!1 /= Pab`length") (("1" (assert) nil nil) ("2" (hide 2) (("2" (flatten) (("2" (case "Pab`seq(ii!1) = Pbc`seq(0)") (("1" (assert) (("1" (case "delete(0, Pbc)`seq(1 - Pab`length + ii!1) = Pbc`seq(1)") (("1" (expand "delete") (("1" (lemma "width_lem") (("1" (inst - "b" "c" "Pbc" "0") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "delete") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "Pab") (("2" (typepred "Pbc") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "width_lem") (("3" (inst - "b" "c" "Pbc" "1 - Pab`length + ii!1") (("3" (assert) nil nil)) nil)) nil) ("4" (typepred "ii!1") (("4" (expand "partjoin" -1) (("4" (expand "o" -1) (("4" (expand "delete" -1) (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "max") (("2" (lift-if) (("2" (ground) (("1" (lemma "width_lem_exists") (("1" (inst - "b" "c") (("1" (assert) (("1" (inst?) (("1" (skosimp*) (("1" (replace -1) (("1" (hide -1) (("1" (hide -1) (("1" (lemma "width_lem") (("1" (inst - "a" "c" "partjoin(a,b,c)(Pab,Pbc)" "Pab`length-1+ii!1") (("1" (assert) (("1" (lemma "partjoin_def") (("1" (inst-cp - "a" "b" "c" "Pab`length + ii!1") (("1" (inst - "a" "b" "c" "Pab`length-1 + ii!1") (("1" (assert) (("1" (inst - "Pab" "Pbc") (("1" (inst - "Pab" "Pbc") (("1" (flatten) (("1" (assert) (("1" (hide -3) (("1" (hide -1) (("1" (split -) (("1" (replace -1) (("1" (split -) (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (expand "partjoin") (("2" (expand "o" 1) (("2" (expand "delete" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "partjoin") (("2" (expand "o" 1) (("2" (expand "delete" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "partjoin" 1) (("2" (expand "o") (("2" (expand "delete") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 1) (("2" (lemma "width_lem_exists") (("2" (inst - "a" "b") (("2" (assert) (("2" (inst - "Pab") (("2" (skosimp*) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "width_lem") (("2" (inst - "a" "c" "partjoin(a, b, c)(Pab, Pbc)" "ii!1") (("1" (case "partjoin(a, b, c)(Pab, Pbc)`seq(ii!1 + 1) - partjoin(a, b, c)(Pab, Pbc)`seq(ii!1) = Pab`seq(1 + ii!1) - Pab`seq(ii!1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -1) (("2" (expand "partjoin") (("2" (expand "o") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "partjoin" 1) (("2" (expand "o") (("2" (expand "delete") (("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) ((max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (partjoin const-decl "partition(a, c)" rs_partition nil) (width const-decl "posreal" rs_partition nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (partition type-eq-decl nil rs_partition nil) (below type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (T_pred const-decl "[real -> boolean]" rs_partition nil) (T formal-nonempty-subtype-decl nil rs_partition 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (O const-decl "fseq" fseqs "structures/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (width_lem formula-decl nil rs_partition nil) (ne_fseq type-eq-decl nil fseqs "structures/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (delete const-decl "fseq" fseqs_ops "structures/") (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_max application-judgement "{z: posreal | z >= x AND z >= y}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (width_lem_exists formula-decl nil rs_partition nil) (a skolem-const-decl "T" rs_partition nil) (b skolem-const-decl "T" rs_partition nil) (Pab skolem-const-decl "partition(a, b)" rs_partition nil) (c skolem-const-decl "T" rs_partition nil) (Pbc skolem-const-decl "partition(b, c)" rs_partition nil) (ii!1 skolem-const-decl "below(Pbc`length - 1)" rs_partition nil) (partjoin_def formula-decl nil rs_partition nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (ii!1 skolem-const-decl "below(Pab`length - 1)" rs_partition nil)) nil) (partjoin_width-1 nil 3489488854 ("" (skeep) (("" (skeep) (("" (case "width(a, c, partjoin(a, b, c)(Pab, Pbc)) >= max(width(a, b, Pab), width(b, c, Pbc))") (("1" (lemma "width_lem_exists") (("1" (inst - "a" "c") (("1" (assert) (("1" (inst - "partjoin(a, b, c)(Pab, Pbc)") (("1" (skosimp*) (("1" (lemma "width_lem_exists") (("1" (inst - "a" "b") (("1" (assert) (("1" (inst - "Pab") (("1" (skosimp*) (("1" (lemma "width_lem_exists") (("1" (inst - "b" "c") (("1" (assert) (("1" (inst - "Pbc") (("1" (skosimp*) (("1" (assert) (("1" (name "PJ" "partjoin(a, b, c)(Pab, Pbc)") (("1" (replace -1) (("1" (name "wab" "width(a,b,Pab)") (("1" (replace -1) (("1" (name "wbc" "width(b,c,Pbc)") (("1" (replace -1) (("1" (name "wac" "width(a,c,PJ)") (("1" (replace -1) (("1" (expand "partjoin") (("1" (expand "o") (("1" (replace -4 -7 :dir rl) (("1" (assert) (("1" (expand "delete") (("1" (assert) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (lemma "width_lem") (("1" (inst - "a" "b" "Pab" "ii!1") (("1" (assert) nil nil)) nil)) nil) ("2" (case "1+ii!1 /= Pab`length") (("1" (assert) nil nil) ("2" (hide 2) (("2" (flatten) (("2" (case "Pab`seq(ii!1) = Pbc`seq(0)") (("1" (assert) (("1" (case "delete(0, Pbc)`seq(1 - Pab`length + ii!1) = Pbc`seq(1)") (("1" (expand "delete") (("1" (lemma "width_lem") (("1" (inst - "b" "c" "Pbc" "0") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "delete") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "Pab") (("2" (typepred "Pbc") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "width_lem") (("3" (inst - "b" "c" "Pbc" "1 - Pab`length + ii!1") (("3" (assert) nil nil)) nil)) nil) ("4" (typepred "ii!1") (("4" (expand "partjoin" -1) (("4" (expand "o" -1) (("4" (expand "delete" -1) (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "max") (("2" (lift-if) (("2" (ground) (("1" (lemma "width_lem_exists") (("1" (inst - "b" "c") (("1" (assert) (("1" (inst?) (("1" (skosimp*) (("1" (replace -1) (("1" (hide -1) (("1" (hide -1) (("1" (lemma "width_lem") (("1" (inst - "a" "c" "partjoin(a,b,c)(Pab,Pbc)" "Pab`length-1+ii!1") (("1" (assert) (("1" (lemma "partjoin_def") (("1" (inst-cp - "a" "b" "c" "Pab`length + ii!1") (("1" (inst - "a" "b" "c" "Pab`length-1 + ii!1") (("1" (assert) (("1" (inst - "Pab" "Pbc") (("1" (inst - "Pab" "Pbc") (("1" (flatten) (("1" (assert) (("1" (hide -3) (("1" (hide -1) (("1" (split -) (("1" (replace -1) (("1" (split -) (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (expand "partjoin") (("2" (expand "o" 1) (("2" (expand "delete" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "partjoin") (("2" (expand "o" 1) (("2" (expand "delete" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "partjoin" 1) (("2" (expand "o") (("2" (expand "delete") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 1) (("2" (lemma "width_lem_exists") (("2" (inst - "a" "b") (("2" (assert) (("2" (inst - "Pab") (("2" (skosimp*) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "width_lem") (("2" (inst - "a" "c" "partjoin(a, b, c)(Pab, Pbc)" "ii!1") (("1" (case "partjoin(a, b, c)(Pab, Pbc)`seq(ii!1 + 1) - partjoin(a, b, c)(Pab, Pbc)`seq(ii!1) = Pab`seq(1 + ii!1) - Pab`seq(ii!1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -1) (("2" (expand "partjoin") (("2" (expand "o") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "partjoin" 1) (("2" (expand "o") (("2" (expand "delete") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((delete const-decl "fseq" fseqs_ops "structures/") (ne_fseq type-eq-decl nil fseqs "structures/") (O const-decl "fseq" fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (increasing? const-decl "bool" sort_fseq "structures/")) shostak)) (partition_union_TCC1 0 (partition_union_TCC1-1 nil 3490961433 ("" (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]" rs_partition nil) (T formal-nonempty-subtype-decl nil rs_partition 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)) nil)) (partition_union_TCC2 0 (partition_union_TCC2-2 nil 3495198360 ("" (auto-rewrite + "member") (("" (case "(FORALL (aa1:T,(bb1:T|aa1<bb1),aa2:T,(bb2:T|aa2<bb2),P1:partition(aa1,bb1),P2 (("1" (name "xone" "LAMBDA (a:T,(b | a<b)): (LAMBDA (Pone,Ptwo:partition(a,b)): choose({PQ:partition(a,b) | (member[T](x, Pone) OR member[T](x, Ptwo))) AND strictly_increasing?(PQ)}))") (("1" (inst + "xone") nil nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (expand "nonempty?") (("3" (inst - "a!1" "b!1" "a!1" "b!1" "Pone!1" "Ptwo!1") (("3" (skosimp*) (("3" (expand "empty?") (("3" (inst -1 "PQ!1") (("1" (expand "member") (("1" (ground) nil nil)) nil) ("2" (typepred "PQ!1") (("2" (expand "min") (("2" (expand "max") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (name "PQZ" "strictly_sort(concat(P1,P2))") (("2" (case "NOT (FORALL (x:T): member(x, PQZ) IFF (member(x, P1) OR member(x, P2)))") (("1" (hide 2) (("1" (skosimp*) (("1" (typepred "PQZ") (("1" (inst - "x!1") (("1" (replace -2 :dir rl) (("1" (lemma "member_composition") (("1" (inst - "P1" "P2" "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "PQZ") (("1" (assert) nil nil) ("2" (label "PQZmember" -1) (("2" (hide "PQZmember") (("2" (replace -1 + :dir rl) (("2" (hide -1) (("2" (case "strictly_sort((P1 o P2))`length > 1") (("1" (assert) (("1" (case "strictly_sort((P1 o P2))`seq(0) = min(aa1, aa2)") (("1" (assert) (("1" (case "strictly_sort((P1 o P2))`seq(strictly_sort((P1 o P2))`length - 1) = max(bb1, bb2)") (("1" (assert) (("1" (case "increasing?[T, <=](strictly_sort((P1 o P2)))") (("1" (assert) (("1" (case "(FORALL (i: below(PQZ`length - 1)): strictly_sort((P1 o P2))`seq(i) < strictly_sort((P1 o P2))`seq(1 + i))") (("1" (assert) (("1" (case "FORALL (i: below(PQZ`length)): min(aa1, aa2) <= strictly_sort((P1 o P2))`seq(i) AND strictly_sort((P1 o P2))`seq(i) <= max(bb1, bb2)") (("1" (propax) nil nil) ("2" (hide 2) (("2" (copy -2) (("2" (skeep) (("2" (split +) (("1" (expand "increasing?" -1) (("1" (inst - "0" "i") (("1" (assert) (("1" (typepred "i") (("1" (expand "PQZ" -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "increasing?" -1) (("2" (inst - "i" "strictly_sort((P1 o P2))`length - 1") (("2" (assert) (("2" (typepred "i") (("2" (expand "PQZ" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (typepred "strictly_sort(concat(P1,P2))") (("2" (expand "strictly_increasing?") (("2" (inst - "i" "i+1") (("2" (assert) (("2" (split -1) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (typepred "i") (("2" (expand "PQZ" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (typepred "strictly_sort(concat(P1,P2))") (("2" (expand "strictly_increasing?") (("2" (expand "increasing?") (("2" (skeep) (("2" (inst - "i" "j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "strictly_sort(concat(P1,P2))") (("2" (case "member(max(bb1,bb2),strictly_sort((P1 o P2)))") (("1" (expand "member" -1) (("1" (skosimp*) (("1" (expand "strictly_increasing?") (("1" (inst - "i!1" "strictly_sort((P1 o P2))`length - 1") (("1" (assert) (("1" (replace -1 :dir rl) (("1" (reveal "PQZmember") (("1" (name "myx" "seq(strictly_sort((P1 o P2)))(strictly_sort((P1 o P2))`length - 1)") (("1" (inst - "myx") (("1" (case "NOT member(myx,PQZ)") (("1" (hide-all-but 1) (("1" (expand "PQZ") (("1" (expand "member") (("1" (expand "myx") (("1" (inst + "strictly_sort((P1 o P2))`length - 1") nil nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (replace -2) (("2" (split "PQZmember") (("1" (skosimp -1) (("1" (typepred "P1") (("1" (expand "increasing?" -) (("1" (inst - "i!2" "P1`length-1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skosimp -1) (("2" (typepred "P2") (("2" (expand "increasing?" -) (("2" (inst - "i!2" "P2`length-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "max(bb1,bb2)") (("2" (replace -2 :dir rl) (("2" (lemma "member_composition") (("2" (inst?) (("2" (replace -1) (("2" (case "member(bb1,P1) AND member(bb2,P2)") (("1" (expand "max" 1) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (split) (("1" (typepred "P1") (("1" (expand "member") (("1" (inst + "P1`length-1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "member") (("2" (typepred "P2") (("2" (inst + "P2`length-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "max") (("3" (lift-if) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "PQZmember") (("2" (copy "PQZmember") (("2" (hide "PQZmember") (("2" (inst - "min(aa1,aa2)") (("1" (case "(member(min(aa1, aa2), P1) OR member(min(aa1, aa2), P2))") (("1" (replace -1) (("1" (assert) (("1" (hide -1) (("1" (skosimp*) (("1" (replace -1) (("1" (expand "PQZ") (("1" (name "myx" "strictly_sort((P1 o P2))`seq(0)") (("1" (replace -1) (("1" (name "newx" "strictly_sort((P1 o P2))`seq(i!1)") (("1" (replace -1) (("1" (typepred "PQZ") (("1" (expand "strictly_increasing?") (("1" (inst - "0" "i!1") (("1" (inst - "myx") (("1" (case "NOT member(myx,PQZ)") (("1" (hide-all-but 1) (("1" (expand "myx") (("1" (expand "PQZ") (("1" (expand "member") (("1" (inst + "0") nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "member_composition") (("2" (inst - "P1" "P2" "myx") (("2" (replace -1) (("2" (hide -1) (("2" (replace -1) (("2" (assert) (("2" (expand "PQZ") (("2" (replace -4) (("2" (replace -5) (("2" (split -3) (("1" (skosimp -1) (("1" (typepred "P1") (("1" (expand "increasing?") (("1" (inst - "0" "i!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp -1) (("2" (typepred "P2") (("2" (expand "increasing?") (("2" (inst - "0" "i!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (flatten) (("2" (case "member(aa1,P1) AND member(aa2,P2)") (("1" (flatten) (("1" (expand "min") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (split) (("1" (typepred "P1") (("1" (expand "member") (("1" (inst + "0") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "member") (("2" (typepred "P2") (("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "min") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "strictly_sort((P1 o P2))`length /= 1") (("1" (assert) (("1" (typepred "strictly_sort(concat(P1,P2))") (("1" (inst - "P1`seq(0)") (("1" (case "member(P1`seq(0),concat(P1,P2))") (("1" (replace -1) (("1" (assert) (("1" (skosimp*) nil nil)) nil)) nil) ("2" (lemma "member_composition") (("2" (inst - "P1" "P2" "P1`seq(0)") (("2" (assert) (("2" (replace -1) (("2" (flatten) (("2" (inst + "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (typepred "strictly_sort(concat(P1,P2))") (("2" (inst-cp - "aa1") (("2" (inst - "bb1") (("2" (case "aa1 < bb1") (("1" (case "member(aa1,concat(P1,P2)) and member(bb1,concat(P1,P2))") (("1" (flatten) (("1" (replace -1) (("1" (replace -2) (("1" (assert) (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (case "member(aa1,P1) AND member(bb1,P1)") (("1" (flatten) (("1" (lemma "member_composition") (("1" (inst-cp - "P1" "P2" "aa1") (("1" (inst - "P1" "P2" "bb1") (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "P1") (("2" (expand "member") (("2" (split +) (("1" (inst + "0") (("1" (assert) nil nil)) nil) ("2" (inst + "P1`length-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "P1") (("2" (case "P1`length-1 = 1") (("1" (inst - "0") (("1" (assert) nil nil)) nil) ("2" (inst-cp -5 "0") (("2" (expand "increasing?") (("2" (inst - "1" "P1`length-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((strictly_increasing? const-decl "bool" sort_fseq "structures/") (OR const-decl "[bool, bool -> bool]" booleans nil) (member const-decl "bool" fseqs "structures/") (IFF const-decl "[bool, bool -> bool]" booleans nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (partition type-eq-decl nil rs_partition 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) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (a!1 skolem-const-decl "T" rs_partition nil) (b!1 skolem-const-decl "{b | a!1 < b}" rs_partition nil) (PQ!1 skolem-const-decl "partition(min(a!1, a!1), max(b!1, b!1))" rs_partition nil) (member const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (member_composition formula-decl nil fseqs "structures/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (myx skolem-const-decl "T" rs_partition nil) (myx skolem-const-decl "T" rs_partition nil) (/= const-decl "boolean" notequal nil) (PQZ skolem-const-decl "{ss: fseq[T] | strictly_increasing?(ss) AND (FORALL (x: T): member(x, (P1 o P2)) IFF member(x, ss))}" rs_partition nil) (P2 skolem-const-decl "partition(aa2, bb2)" rs_partition nil) (bb2 skolem-const-decl "{bb2: T | aa2 < bb2}" rs_partition nil) (aa2 skolem-const-decl "T" rs_partition nil) (P1 skolem-const-decl "partition(aa1, bb1)" rs_partition nil) (bb1 skolem-const-decl "{bb1: T | aa1 < bb1}" rs_partition nil) (aa1 skolem-const-decl "T" rs_partition nil) (O const-decl "fseq" fseqs "structures/") (strictly_sort const-decl "{ss: fseq | strictly_increasing?(ss) AND (FORALL (x: T): member(x, s) IFF member(x, ss))}" sort_fseq "structures/")) nil) (partition_union_TCC2-1 nil 3490961433 ("" (case "(FORALL (aa1:T,(bb1:T|aa1<bb1),aa2:T,(bb2:T|aa2<bb2),P1:partition(aa1,bb1),P2 (("1" (name "xone" "LAMBDA (a:T,(b | a<b)): (LAMBDA (Pone,Ptwo:partition(a,b)): choose({PQ:partition(a,b) | (member[T](x, Pone) OR member[T](x, Ptwo))) AND strictly_increasing?(PQ)}))") (("1" (inst + "xone") nil nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (expand "nonempty?") (("3" (inst - "a!1" "b!1" "a!1" "b!1" "Pone!1" "Ptwo!1") (("3" (skosimp*) (("3" (expand "empty?") (("3" (inst -1 "PQ!1") (("1" (expand "member") (("1" (ground) nil nil)) nil) ("2" (typepred "PQ!1") (("2" (expand "min") (("2" (expand "max") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (name "PQZ" "strictly_sort(concat(P1,P2))") (("2" (case "NOT (FORALL (x:T): member(x, PQZ) IFF (member(x, P1) OR member(x, P2)))") (("1" (hide 2) (("1" (skosimp*) (("1" (typepred "PQZ") (("1" (inst - "x!1") (("1" (replace -2 :dir rl) (("1" (lemma "member_composition") (("1" (inst - "P1" "P2" "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "PQZ") (("1" (assert) nil nil) ("2" (label "PQZmember" -1) (("2" (hide "PQZmember") (("2" (replace -1 + :dir rl) (("2" (hide -1) (("2" (case "strictly_sort((P1 o P2))`length > 1") (("1" (assert) (("1" (case "strictly_sort((P1 o P2))`seq(0) = min(aa1, aa2)") (("1" (assert) (("1" (case "strictly_sort((P1 o P2))`seq(strictly_sort((P1 o P2))`length - 1) = max(bb1, bb2)") (("1" (assert) (("1" (case "increasing?[T, <=](strictly_sort((P1 o P2)))") (("1" (assert) (("1" (case "(FORALL (i: below(PQZ`length - 1)): strictly_sort((P1 o P2))`seq(i) < strictly_sort((P1 o P2))`seq(1 + i))") (("1" (assert) (("1" (case "FORALL (i: below(PQZ`length)): min(aa1, aa2) <= strictly_sort((P1 o P2))`seq(i) AND strictly_sort((P1 o P2))`seq(i) <= max(bb1, bb2)") (("1" (propax) nil nil) ("2" (hide 2) (("2" (copy -2) (("2" (skeep) (("2" (split +) (("1" (expand "increasing?" -1) (("1" (inst - "0" "i") (("1" (assert) (("1" (typepred "i") (("1" (expand "PQZ" -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "increasing?" -1) (("2" (inst - "i" "strictly_sort((P1 o P2))`length - 1") (("2" (assert) (("2" (typepred "i") (("2" (expand "PQZ" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (typepred "strictly_sort(concat(P1,P2))") (("2" (expand "strictly_increasing?") (("2" (inst - "i" "i+1") (("2" (assert) (("2" (split -1) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (typepred "i") (("2" (expand "PQZ" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (typepred "strictly_sort(concat(P1,P2))") (("2" (expand "strictly_increasing?") (("2" (expand "increasing?") (("2" (skeep) (("2" (inst - "i" "j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "strictly_sort(concat(P1,P2))") (("2" (case "member(max(bb1,bb2),strictly_sort((P1 o P2)))") (("1" (expand "member" -1) (("1" (skosimp*) (("1" (expand "strictly_increasing?") (("1" (inst - "i!1" "strictly_sort((P1 o P2))`length - 1") (("1" (assert) (("1" (replace -1 :dir rl) (("1" (reveal "PQZmember") (("1" (name "myx" "seq(strictly_sort((P1 o P2)))(strictly_sort((P1 o P2))`length - 1)") (("1" (inst - "myx") (("1" (case "NOT member(myx,PQZ)") (("1" (hide-all-but 1) (("1" (expand "PQZ") (("1" (expand "member") (("1" (expand "myx") (("1" (inst + "strictly_sort((P1 o P2))`length - 1") nil nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (replace -2) (("2" (split "PQZmember") (("1" (skosimp -1) (("1" (typepred "P1") (("1" (expand "increasing?" -) (("1" (inst - "i!2" "P1`length-1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skosimp -1) (("2" (typepred "P2") (("2" (expand "increasing?" -) (("2" (inst - "i!2" "P2`length-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "max(bb1,bb2)") (("2" (replace -2 :dir rl) (("2" (lemma "member_composition") (("2" (inst?) (("2" (replace -1) (("2" (case "member(bb1,P1) AND member(bb2,P2)") (("1" (expand "max" 1) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (split) (("1" (typepred "P1") (("1" (expand "member") (("1" (inst + "P1`length-1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "member") (("2" (typepred "P2") (("2" (inst + "P2`length-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "max") (("3" (lift-if) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "PQZmember") (("2" (copy "PQZmember") (("2" (hide "PQZmember") (("2" (inst - "min(aa1,aa2)") (("1" (case "(member(min(aa1, aa2), P1) OR member(min(aa1, aa2), P2))") (("1" (replace -1) (("1" (assert) (("1" (hide -1) (("1" (skosimp*) (("1" (replace -1) (("1" (expand "PQZ") (("1" (name "myx" "strictly_sort((P1 o P2))`seq(0)") (("1" (replace -1) (("1" (name "newx" "strictly_sort((P1 o P2))`seq(i!1)") (("1" (replace -1) (("1" (typepred "PQZ") (("1" (expand "strictly_increasing?") (("1" (inst - "0" "i!1") (("1" (inst - "myx") (("1" (case "NOT member(myx,PQZ)") (("1" (hide-all-but 1) (("1" (expand "myx") (("1" (expand "PQZ") (("1" (expand "member") (("1" (inst + "0") nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "member_composition") (("2" (inst - "P1" "P2" "myx") (("2" (replace -1) (("2" (hide -1) (("2" (replace -1) (("2" (assert) (("2" (expand "PQZ") (("2" (replace -4) (("2" (replace -5) (("2" (split -3) (("1" (skosimp -1) (("1" (typepred "P1") (("1" (expand "increasing?") (("1" (inst - "0" "i!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp -1) (("2" (typepred "P2") (("2" (expand "increasing?") (("2" (inst - "0" "i!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (flatten) (("2" (case "member(aa1,P1) AND member(aa2,P2)") (("1" (flatten) (("1" (expand "min") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (split) (("1" (typepred "P1") (("1" (expand "member") (("1" (inst + "0") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "member") (("2" (typepred "P2") (("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "min") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "strictly_sort((P1 o P2))`length /= 1") (("1" (assert) (("1" (typepred "strictly_sort(concat(P1,P2))") (("1" (inst - "P1`seq(0)") (("1" (case "member(P1`seq(0),concat(P1,P2))") (("1" (replace -1) (("1" (assert) (("1" (skosimp*) nil nil)) nil)) nil) ("2" (lemma "member_composition") (("2" (inst - "P1" "P2" "P1`seq(0)") (("2" (assert) (("2" (replace -1) (("2" (flatten) (("2" (inst + "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (typepred "strictly_sort(concat(P1,P2))") (("2" (inst-cp - "aa1") (("2" (inst - "bb1") (("2" (case "aa1 < bb1") (("1" (case "member(aa1,concat(P1,P2)) and member(bb1,concat(P1,P2))") (("1" (flatten) (("1" (replace -1) (("1" (replace -2) (("1" (assert) (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (case "member(aa1,P1) AND member(bb1,P1)") (("1" (flatten) (("1" (lemma "member_composition") (("1" (inst-cp - "P1" "P2" "aa1") (("1" (inst - "P1" "P2" "bb1") (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "P1") (("2" (expand "member") (("2" (split +) (("1" (inst + "0") (("1" (assert) nil nil)) nil) ("2" (inst + "P1`length-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "P1") (("2" (case "P1`length-1 = 1") (("1" (inst - "0") (("1" (assert) nil nil)) nil) ("2" (inst-cp -5 "0") (("2" (expand "increasing?") (("2" (inst - "1" "P1`length-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((strictly_sort const-decl "{ss: fseq | strictly_increasing?(ss) AND (FORALL (x: T): member(x, s) IFF member(x, ss))}" sort_fseq "structures/") (O const-decl "fseq" fseqs "structures/") (member_composition formula-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (increasing? const-decl "bool" sort_fseq "structures/") (member const-decl "bool" fseqs "structures/") (strictly_increasing? const-decl "bool" sort_fseq "structures/")) nil)) (partition_union_sym 0 (partition_union_sym-2 nil 3495198221 ("" (auto-rewrite + "member") (("" (skeep) (("" (skeep) (("" (name "PQ" "partition_union(a,b)(P,Q)") (("" (replace -1) (("" (name "QP" "partition_union(a,b)(Q,P)") (("" (replace -1) (("" (name "Le" "min(PQ`length,QP`length)") (("" (label "Lename" -1) (("" (label "QPname" -2) (("" (label "PQname" -3) (("" (label "altb" -4) (("" (case "FORALL (mm: below(Le)): PQ`seq(mm) = QP`seq(mm)") (("1" (case "NOT PQ`length = QP`length") (("1" (hide 2) (("1" (case "PQ`length > QP`length") (("1" (expand "min") (("1" (assert) (("1" (inst - "QP`length-1") (("1" (typepred "PQ") (("1" (expand "strictly_increasing?") (("1" (inst - "QP`length-1" "PQ`length-1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "min") (("2" (assert) (("2" (inst - "PQ`length-1") (("2" (typepred "QP") (("2" (expand "strictly_increasing?") (("2" (inst - "PQ`length-1" "QP`length-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "seqeq" -2) (("2" (label "lengtheq" -1) (("2" (expand "min") (("2" (assert) (("2" (case "FORALL (mm:below(Le)): PQ`seq(mm) = QP`seq(mm)") (("1" (decompose-equality 1) (("1" (decompose-equality 1) (("1" (inst - "x!1") (("1" (assert) (("1" (typepred "x!1") (("1" (typepred "PQ") (("1" (typepred "PQ`seq") (("1" (inst - "x!1") (("1" (typepred "QP`seq") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "mm") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (skolem 1 "mm") (("2" (flatten) (("2" (name "pq" "PQ`seq(mm+1)") (("2" (replace -1) (("2" (name "qp" "QP`seq(mm+1)") (("2" (replace -1) (("2" (case "member(qp,PQ) and member(pq,QP)") (("1" (flatten) (("1" (assert) (("1" (skosimp*) (("1" (case "i!1 > mm and i!2 > mm") (("1" (flatten) (("1" (typepred "PQ") (("1" (expand "strictly_increasing?") (("1" (inst - "1+mm" "i!1") (("1" (assert) (("1" (typepred "QP") (("1" (expand "strictly_increasing?") (("1" (inst - "1+mm" "i!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (case "qp <= PQ`seq(mm)") (("1" (typepred "QP") (("1" (expand "strictly_increasing?") (("1" (inst - "mm" "1+mm") (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "PQ") (("2" (expand "increasing?") (("2" (inst - "i!1" "mm") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "pq <= QP`seq(mm)") (("1" (typepred "PQ") (("1" (expand "strictly_increasing?") (("1" (inst - "mm" "1+mm") (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "QP") (("2" (expand "increasing?") (("2" (inst - "i!2" "mm") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "member(pq,PQ) and member(qp,QP)") (("1" (flatten) (("1" (typepred "PQ") (("1" (copy -6) (("1" (inst-cp - "pq") (("1" (inst - "qp") (("1" (typepred "QP") (("1" (copy -6) (("1" (inst-cp - "qp") (("1" (inst - "pq") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (expand "member") (("1" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (expand "member") (("2" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((partition_union const-decl "{PQ: partition(a, b) | (FORALL (x: T): member(x, PQ) IFF (member(x, P) OR member(x, Q))) AND strictly_increasing?(PQ)}" rs_partition nil) (strictly_increasing? const-decl "bool" sort_fseq "structures/") (OR const-decl "[bool, bool -> bool]" booleans nil) (member const-decl "bool" fseqs "structures/") (IFF const-decl "[bool, bool -> bool]" booleans nil) (partition type-eq-decl nil rs_partition 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) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (> const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (mm skolem-const-decl "below(Le)" rs_partition nil) (below_induction formula-decl nil bounded_nat_inductions nil) (pred type-eq-decl nil defined_types nil) (NOT const-decl "[bool -> bool]" booleans 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) (Le skolem-const-decl "{k: nat | k <= PQ`length AND k <= QP`length}" rs_partition nil) (QP skolem-const-decl "{PQ: partition(a, b) | (FORALL (x: T): member(x, PQ) IFF (member(x, Q) OR member(x, P))) AND strictly_increasing?(PQ)}" rs_partition nil) (PQ skolem-const-decl "{PQ: partition(a, b) | (FORALL (x: T): member(x, PQ) IFF (member(x, P) OR member(x, Q))) AND strictly_increasing?(PQ)}" rs_partition nil) (Q skolem-const-decl "partition(a, b)" rs_partition nil) (P skolem-const-decl "partition(a, b)" rs_partition nil) (b skolem-const-decl "T" rs_partition nil) (a skolem-const-decl "T" rs_partition nil) (x!1 skolem-const-decl "nat" rs_partition nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (default const-decl "T" fseqs "structures/")) nil) (partition_union_sym-1 nil 3491567687 ("" (skeep) (("" (skeep) (("" (name "PQ" "partition_union(a,b)(P,Q)") (("" (replace -1) (("" (name "QP" "partition_union(a,b)(Q,P)") (("" (replace -1) (("" (name "Le" "min(PQ`length,QP`length)") (("" (label "Lename" -1) (("" (label "QPname" -2) (("" (label "PQname" -3) (("" (label "altb" -4) (("" (case "FORALL (mm: below(Le)): PQ`seq(mm) = QP`seq(mm)") (("1" (case "NOT PQ`length = QP`length") (("1" (hide 2) (("1" (case "PQ`length > QP`length") (("1" (expand "min") (("1" (assert) (("1" (inst - "QP`length-1") (("1" (typepred "PQ") (("1" (expand "strictly_increasing?") (("1" (inst - "QP`length-1" "PQ`length-1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "min") (("2" (assert) (("2" (inst - "PQ`length-1") (("2" (typepred "QP") (("2" (expand "strictly_increasing?") (("2" (inst - "PQ`length-1" "QP`length-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "seqeq" -2) (("2" (label "lengtheq" -1) (("2" (expand "min") (("2" (assert) (("2" (case "FORALL (mm:below(Le)): PQ`seq(mm) = QP`seq(mm)") (("1" (decompose-equality 1) (("1" (decompose-equality 1) (("1" (inst - "x!1") (("1" (assert) (("1" (typepred "x!1") (("1" (typepred "PQ") (("1" (typepred "PQ`seq") (("1" (inst - "x!1") (("1" (typepred "QP`seq") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "mm") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (skolem 1 "mm") (("2" (flatten) (("2" (name "pq" "PQ`seq(mm+1)") (("2" (replace -1) (("2" (name "qp" "QP`seq(mm+1)") (("2" (replace -1) (("2" (case "member(qp,PQ) and member(pq,QP)") (("1" (flatten) (("1" (assert) (("1" (skosimp*) (("1" (case "i!1 > mm and i!2 > mm") (("1" (flatten) (("1" (typepred "PQ") (("1" (expand "strictly_increasing?") (("1" (inst - "1+mm" "i!1") (("1" (assert) (("1" (typepred "QP") (("1" (expand "strictly_increasing?") (("1" (inst - "1+mm" "i!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (case "qp <= PQ`seq(mm)") (("1" (typepred "QP") (("1" (expand "strictly_increasing?") (("1" (inst - "mm" "1+mm") (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "PQ") (("2" (expand "increasing?") (("2" (inst - "i!1" "mm") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "pq <= QP`seq(mm)") (("1" (typepred "PQ") (("1" (expand "strictly_increasing?") (("1" (inst - "mm" "1+mm") (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "QP") (("2" (expand "increasing?") (("2" (inst - "i!2" "mm") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "member(pq,PQ) and member(qp,QP)") (("1" (flatten) (("1" (typepred "PQ") (("1" (copy -6) (("1" (inst-cp - "pq") (("1" (inst - "qp") (("1" (typepred "QP") (("1" (copy -6) (("1" (inst-cp - "qp") (("1" (inst - "pq") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (expand "member") (("1" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (expand "member") (("2" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((default const-decl "T" fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (increasing? const-decl "bool" sort_fseq "structures/") (member const-decl "bool" fseqs "structures/") (strictly_increasing? const-decl "bool" sort_fseq "structures/")) shostak)) (partition_union_unique 0 (partition_union_unique-2 nil 3495198265 ("" (auto-rewrite + "member") (("" (skeep) (("" (skeep) (("" (name "QP" "partition_union(a,b)(P,Q)") (("" (replace -1) (("" (name "Le" "min(PQ`length,QP`length)") (("" (label "Lename" -1) (("" (label "QPname" -2) (("" (ground) (("1" (case "FORALL (mm: below(Le)): PQ`seq(mm) = QP`seq(mm)") (("1" (case "NOT PQ`length = QP`length") (("1" (hide 2) (("1" (case "PQ`length > QP`length") (("1" (expand "min") (("1" (assert) (("1" (inst - "QP`length-1") (("1" (typepred "PQ") (("1" (expand "strictly_increasing?") (("1" (inst - "QP`length-1" "PQ`length-1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "min") (("2" (assert) (("2" (inst - "PQ`length-1") (("2" (typepred "QP") (("2" (expand "strictly_increasing?") (("2" (inst - "PQ`length-1" "QP`length-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "seqeq" -2) (("2" (label "lengtheq" -1) (("2" (expand "min") (("2" (assert) (("2" (case "FORALL (mm:below(Le)): PQ`seq(mm) = QP`seq(mm)") (("1" (decompose-equality 1) (("1" (decompose-equality 1) (("1" (inst - "x!1") (("1" (assert) (("1" (typepred "x!1") (("1" (typepred "PQ`seq") (("1" (inst - "x!1") (("1" (typepred "QP`seq") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "mm") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (skolem 1 "mm") (("2" (flatten) (("2" (name "pq" "PQ`seq(mm+1)") (("2" (replace -1) (("2" (name "qp" "QP`seq(mm+1)") (("2" (replace -1) (("2" (case "member(qp,PQ) and member(pq,QP)") (("1" (flatten) (("1" (assert) (("1" (skosimp*) (("1" (case "i!1 > mm and i!2 > mm") (("1" (flatten) (("1" (typepred "PQ") (("1" (expand "strictly_increasing?") (("1" (inst - "1+mm" "i!1") (("1" (assert) (("1" (typepred "QP") (("1" (expand "strictly_increasing?") (("1" (inst - "1+mm" "i!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (case "qp <= PQ`seq(mm)") (("1" (typepred "QP") (("1" (expand "strictly_increasing?") (("1" (inst - "mm" "1+mm") (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "PQ") (("2" (expand "increasing?") (("2" (inst - "i!1" "mm") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "pq <= QP`seq(mm)") (("1" (typepred "PQ") (("1" (expand "strictly_increasing?") (("1" (inst - "mm" "1+mm") (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "QP") (("2" (expand "increasing?") (("2" (inst - "i!2" "mm") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "member(pq,PQ) and member(qp,QP)") (("1" (flatten) (("1" (copy -7) (("1" (inst-cp - "pq") (("1" (inst - "qp") (("1" (typepred "QP") (("1" (copy -6) (("1" (inst-cp - "qp") (("1" (inst - "pq") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (expand "member") (("1" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (expand "member") (("2" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "QP") (("2" (skeep) (("2" (inst -6 "x") (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (skosimp*) (("1" (split -) (("1" (propax) nil nil) ("2" (propax) nil nil) ("3" (inst + "i!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split -) (("1" (assert) (("1" (replace -1) (("1" (skosimp*) (("1" (inst + "i!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (skosimp*) (("2" (inst + "i!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((partition_union const-decl "{PQ: partition(a, b) | (FORALL (x: T): member(x, PQ) IFF (member(x, P) OR member(x, Q))) AND strictly_increasing?(PQ)}" rs_partition nil) (strictly_increasing? const-decl "bool" sort_fseq "structures/") (OR const-decl "[bool, bool -> bool]" booleans nil) (member const-decl "bool" fseqs "structures/") (IFF const-decl "[bool, bool -> bool]" booleans nil) (partition type-eq-decl nil rs_partition 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) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (> const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (default const-decl "T" fseqs "structures/") (x!1 skolem-const-decl "nat" rs_partition nil) (a skolem-const-decl "T" rs_partition nil) (b skolem-const-decl "T" rs_partition nil) (PQ skolem-const-decl "partition(a, b)" rs_partition nil) (P skolem-const-decl "partition(a, b)" rs_partition nil) (Q skolem-const-decl "partition(a, b)" rs_partition nil) (QP skolem-const-decl "{PQ: partition(a, b) | (FORALL (x: T): member(x, PQ) IFF (member(x, P) OR member(x, Q))) AND strictly_increasing?(PQ)}" rs_partition nil) (Le skolem-const-decl "{k: nat | k <= PQ`length AND k <= QP`length}" rs_partition 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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (below_induction formula-decl nil bounded_nat_inductions nil) (mm skolem-const-decl "below(Le)" rs_partition nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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) (partition_union_unique-1 nil 3492190502 ("" (skeep) (("" (skeep) (("" (name "QP" "partition_union(a,b)(P,Q)") (("" (replace -1) (("" (name "Le" "min(PQ`length,QP`length)") (("" (label "Lename" -1) (("" (label "QPname" -2) (("" (ground) (("1" (case "FORALL (mm: below(Le)): PQ`seq(mm) = QP`seq(mm)") (("1" (case "NOT PQ`length = QP`length") (("1" (hide 2) (("1" (case "PQ`length > QP`length") (("1" (expand "min") (("1" (assert) (("1" (inst - "QP`length-1") (("1" (typepred "PQ") (("1" (expand "strictly_increasing?") (("1" (inst - "QP`length-1" "PQ`length-1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "min") (("2" (assert) (("2" (inst - "PQ`length-1") (("2" (typepred "QP") (("2" (expand "strictly_increasing?") (("2" (inst - "PQ`length-1" "QP`length-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "seqeq" -2) (("2" (label "lengtheq" -1) (("2" (expand "min") (("2" (assert) (("2" (case "FORALL (mm:below(Le)): PQ`seq(mm) = QP`seq(mm)") (("1" (decompose-equality 1) (("1" (decompose-equality 1) (("1" (inst - "x!1") (("1" (assert) (("1" (typepred "x!1") (("1" (typepred "PQ`seq") (("1" (inst - "x!1") (("1" (typepred "QP`seq") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "mm") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (skolem 1 "mm") (("2" (flatten) (("2" (name "pq" "PQ`seq(mm+1)") (("2" (replace -1) (("2" (name "qp" "QP`seq(mm+1)") (("2" (replace -1) (("2" (case "member(qp,PQ) and member(pq,QP)") (("1" (flatten) (("1" (assert) (("1" (skosimp*) (("1" (case "i!1 > mm and i!2 > mm") (("1" (flatten) (("1" (typepred "PQ") (("1" (expand "strictly_increasing?") (("1" (inst - "1+mm" "i!1") (("1" (assert) (("1" (typepred "QP") (("1" (expand "strictly_increasing?") (("1" (inst - "1+mm" "i!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (case "qp <= PQ`seq(mm)") (("1" (typepred "QP") (("1" (expand "strictly_increasing?") (("1" (inst - "mm" "1+mm") (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "PQ") (("2" (expand "increasing?") (("2" (inst - "i!1" "mm") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "pq <= QP`seq(mm)") (("1" (typepred "PQ") (("1" (expand "strictly_increasing?") (("1" (inst - "mm" "1+mm") (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "QP") (("2" (expand "increasing?") (("2" (inst - "i!2" "mm") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "member(pq,PQ) and member(qp,QP)") (("1" (flatten) (("1" (copy -7) (("1" (inst-cp - "pq") (("1" (inst - "qp") (("1" (typepred "QP") (("1" (copy -6) (("1" (inst-cp - "qp") (("1" (inst - "pq") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (expand "member") (("1" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (expand "member") (("2" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "QP") (("2" (skeep) (("2" (inst -6 "x") (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (skosimp*) (("1" (split -) (("1" (propax) nil nil) ("2" (propax) nil nil) ("3" (inst + "i!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split -) (("1" (assert) (("1" (replace -1) (("1" (skosimp*) (("1" (inst + "i!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (skosimp*) (("2" (inst + "i!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((default const-decl "T" fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (increasing? const-decl "bool" sort_fseq "structures/") (member const-decl "bool" fseqs "structures/") (strictly_increasing? const-decl "bool" sort_fseq "structures/")) nil)) (partition_union_width 0 (partition_union_width-2 nil 3495198286 ("" (auto-rewrite + "member") (("" (lemma "part_in_strict_left") (("" (label "partin" -1) (("" (hide "partin") (("" (skeep) (("" (skeep) (("" (expand "min") (("" (lift-if) (("" (ground) (("1" (hide -1) (("1" (name "newwid" "width(a, b, partition_union(a, b)(P, Q))") (("1" (replace -1) (("1" (name "Qwid" "width(a,b,Q)") (("1" (replace -1) (("1" (lemma "width_lem") (("1" (label "Qwidmax" -1) (("1" (label "Qwidname" -2) (("1" (label "newwidname" -3) (("1" (lemma "width_lem_exists") (("1" (inst - "a" "b") (("1" (assert) (("1" (inst - "partition_union(a, b)(P, Q)") (("1" (skolem -1 "pqi") (("1" (label "newidPQdiff" -1) (("1" (name "PQ" "partition_union(a,b)(P,Q)") (("1" (label "PQname" -1) (("1" (replace -1) (("1" (reveal "partin") (("1" (inst - "a" "b" "PQ`seq(1+pqi)" "Q") (("1" (assert) (("1" (typepred "PQ") (("1" (inst -5 "1+pqi") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (case "a < PQ`seq(1+pqi)") (("1" (assert) (("1" (hide-all-but ("partin" "PQname" "newidPQdiff" "Qwidmax" "Qwidname" "newidname" +)) (("1" (skolem -1 "ti") (("1" (flatten) (("1" (case "Q`seq(ti) <= PQ`seq(pqi) and PQ`seq(pqi) <= Q`seq(1 + ti)") (("1" (flatten) (("1" (case "NOT newwid <= Q`seq(1+ti)-Q`seq(ti)") (("1" (assert) nil nil) ("2" (name "thisid" "Q`seq(1 + ti) - Q`seq(ti)") (("2" (assert) (("2" (inst "Qwidmax" "a" "b" "Q" "ti") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "PQ") (("2" (hide (-1 -2 -3 -4 -5)) (("2" (inst - "Q`seq(ti)") (("2" (case "member(Q`seq(ti),Q)") (("1" (replace -1) (("1" (ground) (("1" (hide -1) (("1" (skolem -1 "pqti") (("1" (replace -1) (("1" (typepred "PQ") (("1" (hide (-1 -2 -3 -5 -6)) (("1" (expand "increasing?") (("1" (inst - "pqti" "pqi") (("1" (assert) (("1" (typepred "PQ") (("1" (hide (-1 -2 -3 -5 -6)) (("1" (expand "increasing?") (("1" (inst - "1+pqi" "pqti") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "member") (("2" (inst + "ti") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "PQ`seq(pqi) >= a") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (typepred "PQ") (("2" (inst - "pqi") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 1) (("2" (name "newwid" "width(a, b, partition_union(a, b)(P, Q))") (("2" (replace -1) (("2" (name "Pwid" "width(a,b,P)") (("2" (replace -1) (("2" (lemma "width_lem") (("2" (label "Pwidmax" -1) (("2" (label "Pwidname" -2) (("2" (label "newwidname" -3) (("2" (lemma "width_lem_exists") (("2" (inst - "a" "b") (("2" (assert) (("2" (inst - "partition_union(a, b)(P, Q)") (("2" (skolem -1 "pqi") (("2" (label "newidPQdiff" -1) (("2" (name "PQ" "partition_union(a,b)(P,Q)") (("2" (label "PQname" -1) (("2" (replace -1) (("2" (reveal "partin") (("2" (inst - "a" "b" "PQ`seq(1+pqi)" "P") (("2" (assert) (("2" (typepred "PQ") (("2" (inst -5 "1+pqi") (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (case "a < PQ`seq(1+pqi)") (("1" (assert) (("1" (hide-all-but ("partin" "PQname" "newidPQdiff" "Pwidmax" "Pwidname" "newidname" +)) (("1" (skolem -1 "ti") (("1" (flatten) (("1" (case "P`seq(ti) <= PQ`seq(pqi) and PQ`seq(pqi) <= P`seq(1 + ti)") (("1" (flatten) (("1" (case "NOT newwid <= P`seq(1+ti)-P`seq(ti)") (("1" (assert) nil nil) ("2" (name "thisid" "P`seq(1 + ti) - P`seq(ti)") (("2" (assert) (("2" (inst "Pwidmax" "a" "b" "P" "ti") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "PQ") (("2" (hide (-1 -2 -3 -4 -5)) (("2" (inst - "P`seq(ti)") (("2" (case "member(P`seq(ti),P)") (("1" (replace -1) (("1" (ground) (("1" (hide -1) (("1" (skolem -1 "pqti") (("1" (replace -1) (("1" (typepred "PQ") (("1" (hide (-1 -2 -3 -5 -6)) (("1" (expand "increasing?") (("1" (inst - "pqti" "pqi") (("1" (assert) (("1" (typepred "PQ") (("1" (hide (-1 -2 -3 -5 -6)) (("1" (expand "increasing?") (("1" (inst - "1+pqi" "pqti") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "member") (("2" (inst + "ti") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "PQ`seq(pqi) >= a") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (typepred "PQ") (("2" (inst - "pqi") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((part_in_strict_left formula-decl nil rs_partition nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (width_lem_exists formula-decl nil rs_partition nil) (width_lem formula-decl nil rs_partition nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (T formal-nonempty-subtype-decl nil rs_partition 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]" rs_partition nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (restrict const-decl "R" restrict nil) (<= const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/") (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) (partition type-eq-decl nil rs_partition nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (width const-decl "posreal" rs_partition nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (member const-decl "bool" fseqs "structures/") (OR const-decl "[bool, bool -> bool]" booleans nil) (strictly_increasing? const-decl "bool" sort_fseq "structures/") (partition_union const-decl "{PQ: partition(a, b) | (FORALL (x: T): member(x, PQ) IFF (member(x, P) OR member(x, Q))) AND strictly_increasing?(PQ)}" rs_partition 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)) nil) (partition_union_width-1 nil 3491045482 ("" (lemma "part_in_strict_left") (("" (label "partin" -1) (("" (hide "partin") (("" (skeep) (("" (skeep) (("" (expand "min") (("" (lift-if) (("" (ground) (("1" (hide -1) (("1" (name "newwid" "width(a, b, partition_union(a, b)(P, Q))") (("1" (replace -1) (("1" (name "Qwid" "width(a,b,Q)") (("1" (replace -1) (("1" (lemma "width_lem") (("1" (label "Qwidmax" -1) (("1" (label "Qwidname" -2) (("1" (label "newwidname" -3) (("1" (lemma "width_lem_exists") (("1" (inst - "a" "b") (("1" (assert) (("1" (inst - "partition_union(a, b)(P, Q)") (("1" (skolem -1 "pqi") (("1" (label "newidPQdiff" -1) (("1" (name "PQ" "partition_union(a,b)(P,Q)") (("1" (label "PQname" -1) (("1" (replace -1) (("1" (reveal "partin") (("1" (inst - "a" "b" "PQ`seq(1+pqi)" "Q") (("1" (assert) (("1" (typepred "PQ") (("1" (inst -5 "1+pqi") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (case "a < PQ`seq(1+pqi)") (("1" (assert) (("1" (hide-all-but ("partin" "PQname" "newidPQdiff" "Qwidmax" "Qwidname" "newidname" +)) (("1" (skolem -1 "ti") (("1" (flatten) (("1" (case "Q`seq(ti) <= PQ`seq(pqi) and PQ`seq(pqi) <= Q`seq(1 + ti)") (("1" (flatten) (("1" (case "NOT newwid <= Q`seq(1+ti)-Q`seq(ti)") (("1" (assert) nil nil) ("2" (name "thisid" "Q`seq(1 + ti) - Q`seq(ti)") (("2" (assert) (("2" (inst "Qwidmax" "a" "b" "Q" "ti") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "PQ") (("2" (hide (-1 -2 -3 -4 -5)) (("2" (inst - "Q`seq(ti)") (("2" (case "member(Q`seq(ti),Q)") (("1" (replace -1) (("1" (ground) (("1" (hide -1) (("1" (skolem -1 "pqti") (("1" (replace -1) (("1" (typepred "PQ") (("1" (hide (-1 -2 -3 -5 -6)) (("1" (expand "increasing?") (("1" (inst - "pqti" "pqi") (("1" (assert) (("1" (typepred "PQ") (("1" (hide (-1 -2 -3 -5 -6)) (("1" (expand "increasing?") (("1" (inst - "1+pqi" "pqti") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "member") (("2" (inst + "ti") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "PQ`seq(pqi) >= a") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (typepred "PQ") (("2" (inst - "pqi") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 1) (("2" (name "newwid" "width(a, b, partition_union(a, b)(P, Q))") (("2" (replace -1) (("2" (name "Pwid" "width(a,b,P)") (("2" (replace -1) (("2" (lemma "width_lem") (("2" (label "Pwidmax" -1) (("2" (label "Pwidname" -2) (("2" (label "newwidname" -3) (("2" (lemma "width_lem_exists") (("2" (inst - "a" "b") (("2" (assert) (("2" (inst - "partition_union(a, b)(P, Q)") (("2" (skolem -1 "pqi") (("2" (label "newidPQdiff" -1) (("2" (name "PQ" "partition_union(a,b)(P,Q)") (("2" (label "PQname" -1) (("2" (replace -1) (("2" (reveal "partin") (("2" (inst - "a" "b" "PQ`seq(1+pqi)" "P") (("2" (assert) (("2" (typepred "PQ") (("2" (inst -5 "1+pqi") (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (case "a < PQ`seq(1+pqi)") (("1" (assert) (("1" (hide-all-but ("partin" "PQname" "newidPQdiff" "Pwidmax" "Pwidname" "newidname" +)) (("1" (skolem -1 "ti") (("1" (flatten) (("1" (case "P`seq(ti) <= PQ`seq(pqi) and PQ`seq(pqi) <= P`seq(1 + ti)") (("1" (flatten) (("1" (case "NOT newwid <= P`seq(1+ti)-P`seq(ti)") (("1" (assert) nil nil) ("2" (name "thisid" "P`seq(1 + ti) - P`seq(ti)") (("2" (assert) (("2" (inst "Pwidmax" "a" "b" "P" "ti") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "PQ") (("2" (hide (-1 -2 -3 -4 -5)) (("2" (inst - "P`seq(ti)") (("2" (case "member(P`seq(ti),P)") (("1" (replace -1) (("1" (ground) (("1" (hide -1) (("1" (skolem -1 "pqti") (("1" (replace -1) (("1" (typepred "PQ") (("1" (hide (-1 -2 -3 -5 -6)) (("1" (expand "increasing?") (("1" (inst - "pqti" "pqi") (("1" (assert) (("1" (typepred "PQ") (("1" (hide (-1 -2 -3 -5 -6)) (("1" (expand "increasing?") (("1" (inst - "1+pqi" "pqti") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "member") (("2" (inst + "ti") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "PQ`seq(pqi) >= a") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (typepred "PQ") (("2" (inst - "pqi") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((strictly_increasing? const-decl "bool" sort_fseq "structures/") (member const-decl "bool" fseqs "structures/") (increasing? const-decl "bool" sort_fseq "structures/") (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/")) shostak)) (partition_strictly_sort_union_TCC1 0 (partition_strictly_sort_union_TCC1-1 nil 3491903086 ("" (skeep) (("" (skeep) (("" (lemma "partition_strictly_sort") (("" (inst - "a" "b") (("" (assert) (("" (inst - "P") nil nil)) nil)) nil)) nil)) nil)) 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]" rs_partition nil) (T formal-nonempty-subtype-decl nil rs_partition nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (restrict const-decl "R" restrict nil) (<= const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/") (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) (partition type-eq-decl nil rs_partition 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) (partition_strictly_sort formula-decl nil rs_partition nil)) nil)) (partition_strictly_sort_union 0 (partition_strictly_sort_union-2 nil 3495198312 ("" (auto-rewrite + "member") (("" (skeep) (("" (skeep) (("" (name "PQ" "partition_union(a, b)(P, Q)") (("" (replace -1) (("" (hide -1) (("" (name "PPQ" "partition_union(a, b)(strictly_sort(P), Q)") (("" (replace -1) (("" (hide -1) (("" (case "FORALL (x:T): member(x,PQ) IFF member(x,PPQ)") (("1" (label "memberlem" -1) (("1" (hide "memberlem") (("1" (name "ml" "min(PQ`length,PPQ`length)") (("1" (case "FORALL (nn:below(ml)): PQ`seq(nn) = PPQ`seq(nn)") (("1" (case "PQ`length = PPQ`length") (("1" (rewrite "fseqs_eq") (("1" (assert) (("1" (skeep) (("1" (inst - "n") (("1" (expand "min") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "ml-1") (("1" (expand "min") (("1" (lift-if) (("1" (ground) (("1" (replace -2 :dir rl) (("1" (case "PQ`seq(PPQ`length-1) = b") (("1" (typepred "PQ") (("1" (copy -7) (("1" (expand "strictly_increasing?" -1) (("1" (inst - "PPQ`length-1" "PQ`length-1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (replace -1 :dir rl) (("2" (case "PPQ`seq(PQ`length-1) = b") (("1" (typepred "PPQ") (("1" (copy -7) (("1" (expand "strictly_increasing?" -1) (("1" (inst - "PQ`length-1" "PPQ`length-1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "min") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "nn") (("1" (assert) nil nil) ("2" (skolem 1 "nn") (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (case "PQ`seq(1+nn) <= PPQ`seq(1+nn) AND PPQ`seq(1+nn) <= PQ`seq(1+nn)") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (split +) (("1" (reveal "memberlem") (("1" (copy "memberlem") (("1" (hide "memberlem") (("1" (inst - "PPQ`seq(1+nn)") (("1" (case "member(PPQ`seq(1+nn),PPQ)") (("1" (replace -1) (("1" (assert) (("1" (hide -1) (("1" (skosimp*) (("1" (replace -1) (("1" (typepred "PQ") (("1" (copy -7) (("1" (expand "strictly_increasing?" -1) (("1" (inst - "1+nn" "i!1") (("1" (assert) (("1" (case "1+nn<=i!1") (("1" (assert) nil nil) ("2" (case "PQ`seq(nn) < PQ`seq(i!1)") (("1" (copy -8) (("1" (expand "strictly_increasing?" -1) (("1" (inst - "i!1" "nn") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "PPQ") (("2" (copy -7) (("2" (expand "strictly_increasing?" -1) (("2" (inst - "nn" "1+nn") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "member") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (reveal "memberlem") (("2" (copy "memberlem") (("2" (hide "memberlem") (("2" (inst - "PQ`seq(1+nn)") (("2" (case "member(PQ`seq(1+nn),PQ)") (("1" (replace -1) (("1" (assert) (("1" (hide -1) (("1" (skosimp*) (("1" (replace -1) (("1" (typepred "PPQ") (("1" (copy -7) (("1" (expand "strictly_increasing?" -1) (("1" (inst - "1+nn" "i!1") (("1" (assert) (("1" (case "1+nn<=i!1") (("1" (assert) nil nil) ("2" (case "PPQ`seq(nn) < PPQ`seq(i!1)") (("1" (copy -8) (("1" (expand "strictly_increasing?" -1) (("1" (inst - "i!1" "nn") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "PQ") (("2" (copy -7) (("2" (expand "strictly_increasing?" -1) (("2" (inst - "nn" "1+nn") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "member") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "PQ") (("2" (label "pqm" -6) (("2" (typepred "PPQ") (("2" (label "ppqm" -6) (("2" (hide-all-but ("pqm" "ppqm" +)) (("2" (skeep) (("2" (inst - "x") (("2" (inst - "x") (("2" (typepred "strictly_sort(P)") (("2" (inst - "x") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((partition_union const-decl "{PQ: partition(a, b) | (FORALL (x: T): member(x, PQ) IFF (member(x, P) OR member(x, Q))) AND strictly_increasing?(PQ)}" rs_partition nil) (strictly_increasing? const-decl "bool" sort_fseq "structures/") (OR const-decl "[bool, bool -> bool]" booleans nil) (member const-decl "bool" fseqs "structures/") (IFF const-decl "[bool, bool -> bool]" booleans nil) (partition type-eq-decl nil rs_partition 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) (increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (> const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (T formal-nonempty-subtype-decl nil rs_partition nil) (T_pred const-decl "[real -> boolean]" rs_partition 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) --> -------------------- --> maximum size reached --> --------------------
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.875Bemerkung: (vorverarbeitet am 2026-04-28) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26