| products/Sources/formale Sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: rs_partition.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(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), st (("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) EN (("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`s (("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`se (("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 (("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)) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.49 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
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.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
