| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/examples/ (Beweissystem der NASA Version 6.0.9©) Datei vom 8.10.2014 mit Größe 158 kB |
|
Quelle sturm_examples.prfSprache: Lisp |
|||||||||||||||
|
(sturm_examples (example_1_TCC1 0 (example_1_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil) nil nil)) (example_1_TCC2 0 (example_1_TCC2-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_1_TCC3 0 (example_1_TCC3-1 nil 3622997593 ("" (subtype-tcc) nil nil) nil nil)) (example_1 0 (example_1-1 nil 3622997593 ("" (sturm) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (expt_x1 formula-decl nil exponentiation nil) (polylist_minus formula-decl nil polylist "Sturm/") (real_minus_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist "Sturm/") (polylist_pow formula-decl nil polylist "Sturm/") (polylist_sum formula-decl nil polylist "Sturm/") (polylist_const formula-decl nil polylist "Sturm/") (polylist_prod formula-decl nil polylist "Sturm/") (contains? const-decl "bool" RealInt "reals/") (sturm const-decl "bool" poly_strategy "Sturm/") (stu__89 skolem-const-decl "Polylist" sturm_examples nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (pprod const-decl "Polylist" polylist "Sturm/") (pconst const-decl "Polylist" polylist "Sturm/") (polylist const-decl "real" polylist "Sturm/") (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (psum def-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}" polylist "Sturm/") (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) (ppow def-decl "Polylist" polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (length def-decl "nat" list_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil)) shostak)) (example_2 0 (example_2-1 nil 3622997593 ("" (sturm) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (polylist_prod formula-decl nil polylist "Sturm/") (polylist_pow formula-decl nil polylist "Sturm/") (real_plus_real_is_real application-judgement "real" reals nil) (polylist_sum formula-decl nil polylist "Sturm/") (polylist_const formula-decl nil polylist "Sturm/") (polylist_monom formula-decl nil polylist "Sturm/") (real_minus_real_is_real application-judgement "real" reals nil) (polylist_minus formula-decl nil polylist "Sturm/") (expt_x1 formula-decl nil exponentiation nil) (contains? const-decl "bool" RealInt "reals/") (sturm const-decl "bool" poly_strategy "Sturm/") (stu__92 skolem-const-decl "Polylist" sturm_examples nil) (real_times_real_is_real application-judgement "real" reals nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (pprod const-decl "Polylist" polylist "Sturm/") (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) (ppow def-decl "Polylist" polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (pconst const-decl "Polylist" polylist "Sturm/") (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (psum def-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}" polylist "Sturm/") (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil)) shostak)) (example_3_TCC1 0 (example_3_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC2 0 (example_3_TCC2-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC3 0 (example_3_TCC3-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC4 0 (example_3_TCC4-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC5 0 (example_3_TCC5-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC6 0 (example_3_TCC6-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC7 0 (example_3_TCC7-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC8 0 (example_3_TCC8-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC9 0 (example_3_TCC9-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC10 0 (example_3_TCC10-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC11 0 (example_3_TCC11-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC12 0 (example_3_TCC12-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC13 0 (example_3_TCC13-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC14 0 (example_3_TCC14-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (^ const-decl "real" exponentiation nil)) nil)) (example_3 0 (example_3-1 nil 3622997593 ("" (sturm) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (contains? const-decl "bool" RealInt "reals/") (polylist_pow formula-decl nil polylist "Sturm/") (polylist_sum formula-decl nil polylist "Sturm/") (polylist_const formula-decl nil polylist "Sturm/") (polylist_minus formula-decl nil polylist "Sturm/") (polylist_monom formula-decl nil polylist "Sturm/") (expt_x1 formula-decl nil exponentiation nil) (sturm const-decl "bool" poly_strategy "Sturm/") (stu__95 skolem-const-decl "Polylist" sturm_examples nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (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) (ppow def-decl "Polylist" polylist "Sturm/") (polylist const-decl "real" polylist "Sturm/") (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (psum def-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}" polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (length def-decl "nat" list_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (pconst const-decl "Polylist" polylist "Sturm/")) shostak)) (example_4_TCC1 0 (example_4_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_4 0 (example_4-1 nil 3622997593 ("" (sturm) nil nil) ((minus_real_is_real application-judgement "real" reals nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (contains? const-decl "bool" RealInt "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (polylist_minus formula-decl nil polylist "Sturm/") (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist "Sturm/") (polylist_neg formula-decl nil polylist "Sturm/") (expt_x1 formula-decl nil exponentiation nil) (sturm const-decl "bool" poly_strategy "Sturm/") (stu__98 skolem-const-decl "Polylist" sturm_examples nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (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) (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (pneg const-decl "Polylist" polylist "Sturm/")) shostak)) (example_5 0 (example_5-1 nil 3622997593 ("" (sturm) nil nil) ((real_minus_real_is_real application-judgement "real" reals nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (contains? const-decl "bool" RealInt "reals/") (polylist_minus formula-decl nil polylist "Sturm/") (polylist_const formula-decl nil polylist "Sturm/") (polylist_monom formula-decl nil polylist "Sturm/") (sturm const-decl "bool" poly_strategy "Sturm/") (stu__101 skolem-const-decl "Polylist" sturm_examples nil) (real_times_real_is_real application-judgement "real" reals nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (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) (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (pconst const-decl "Polylist" polylist "Sturm/")) shostak)) (example_6_TCC1 0 (example_6_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_6 0 (example_6-1 nil 3622997593 ("" (sturm) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (contains? const-decl "bool" RealInt "reals/") (expt_x1 formula-decl nil exponentiation nil) (polylist_monom formula-decl nil polylist "Sturm/") (polylist_const formula-decl nil polylist "Sturm/") (polylist_minus formula-decl nil polylist "Sturm/") (polylist_sum formula-decl nil polylist "Sturm/") (real_plus_real_is_real application-judgement "real" reals nil) (sturm const-decl "bool" poly_strategy "Sturm/") (stu__104 skolem-const-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pconst(1))(x) + polylist(pminus(pmonom(1, 2), pmonom(2, 1)))(x)}" sturm_examples nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (polylist const-decl "real" polylist "Sturm/") (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (psum def-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}" polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (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) (length def-decl "nat" list_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (pconst const-decl "Polylist" polylist "Sturm/")) shostak)) (example_7 0 (example_7-1 nil 3622997593 ("" (sturm) nil nil) ((real_times_real_is_real application-judgement "real" reals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (SturmRel? const-decl "bool" compute_sturm "Sturm/") (<= const-decl "bool" reals nil) (FALSE const-decl "bool" booleans nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (contains? const-decl "bool" RealInt "reals/") (expt_x1 formula-decl nil exponentiation nil) (polylist_monom formula-decl nil polylist "Sturm/") (polylist_const formula-decl nil polylist "Sturm/") (polylist_prod formula-decl nil polylist "Sturm/") (polylist_minus formula-decl nil polylist "Sturm/") (sturm const-decl "bool" poly_strategy "Sturm/") (stu__107 skolem-const-decl "Polylist" sturm_examples nil) (real_minus_real_is_real application-judgement "real" reals nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (pprod const-decl "Polylist" polylist "Sturm/") (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) (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (pconst const-decl "Polylist" polylist "Sturm/") (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)) shostak)) (example_8 0 (example_8-1 nil 3622997593 ("" (sturm) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (polylist_minus formula-decl nil polylist "Sturm/") (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist "Sturm/") (expt_x1 formula-decl nil exponentiation nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (contains? const-decl "bool" RealInt "reals/") (sturm const-decl "bool" poly_strategy "Sturm/") (stu__110 skolem-const-decl "Polylist" sturm_examples nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (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) (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/")) shostak)) (example_n8 0 (example_n8-1 nil 3622997593 ("" (sturm -1) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (polylist_minus formula-decl nil polylist "Sturm/") (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist "Sturm/") (expt_x1 formula-decl nil exponentiation nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (contains? const-decl "bool" RealInt "reals/") (sturm const-decl "bool" poly_strategy "Sturm/") (stu__113 skolem-const-decl "Polylist" sturm_examples nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (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) (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/")) shostak)) (example_80 0 (example_80-1 nil 3622997593 ("" (sturm) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (polylist_minus formula-decl nil polylist "Sturm/") (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist "Sturm/") (expt_x1 formula-decl nil exponentiation nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (contains? const-decl "bool" RealInt "reals/") (sturm const-decl "bool" poly_strategy "Sturm/") (stu__116 skolem-const-decl "Polylist" sturm_examples nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (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) (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/")) shostak)) (example_n80 0 (example_n80-1 nil 3622997593 ("" (sturm -1) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (polylist_minus formula-decl nil polylist "Sturm/") (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist "Sturm/") (expt_x1 formula-decl nil exponentiation nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (contains? const-decl "bool" RealInt "reals/") (sturm const-decl "bool" poly_strategy "Sturm/") (stu__119 skolem-const-decl "Polylist" sturm_examples nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (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) (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/")) shostak)) (example_9 0 (example_9-1 nil 3622997593 ("" (sturm) nil nil) ((minus_real_is_real application-judgement "real" reals nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (contains? const-decl "bool" RealInt "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (polylist_minus formula-decl nil polylist "Sturm/") (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist "Sturm/") (polylist_neg formula-decl nil polylist "Sturm/") (expt_x1 formula-decl nil exponentiation nil) (sturm const-decl "bool" poly_strategy "Sturm/") (stu__122 skolem-const-decl "Polylist" sturm_examples nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (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) (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (pneg const-decl "Polylist" polylist "Sturm/")) shostak)) (example_n9 0 (example_n9-1 nil 3622997593 ("" (sturm -1) nil nil) ((minus_real_is_real application-judgement "real" reals nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (contains? const-decl "bool" RealInt "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (polylist_minus formula-decl nil polylist "Sturm/") (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist "Sturm/") (polylist_neg formula-decl nil polylist "Sturm/") (expt_x1 formula-decl nil exponentiation nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sturm const-decl "bool" poly_strategy "Sturm/") (stu__125 skolem-const-decl "Polylist" sturm_examples nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (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) (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (pneg const-decl "Polylist" polylist "Sturm/")) shostak)) (example_90 0 (example_90-1 nil 3622997593 ("" (sturm) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (contains? const-decl "bool" RealInt "reals/") (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist "Sturm/") (sturm const-decl "bool" poly_strategy "Sturm/") (stu__128 skolem-const-decl "{pl: Polylist | length(pl) = 6 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 5)}" sturm_examples nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/")) shostak)) (example_n90 0 (example_n90-1 nil 3622997593 ("" (sturm -1) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (contains? const-decl "bool" RealInt "reals/") (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist "Sturm/") (sturm const-decl "bool" poly_strategy "Sturm/") (stu__131 skolem-const-decl "{pl: Polylist | length(pl) = 6 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 5)}" sturm_examples nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/")) shostak)) (example_10 0 (example_10-1 nil 3622997593 ("" (sturm -1) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (RealInt type-eq-decl nil RealInt "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (contains? const-decl "bool" RealInt "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (polylist_monom formula-decl nil polylist "Sturm/") (nzreal_exp application-judgement "nzreal" exponentiation nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (sturm const-decl "bool" poly_strategy "Sturm/") (stu__134 skolem-const-decl "{pl: Polylist | length(pl) = 4 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 3)}" sturm_examples nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/")) shostak)) (example_11 0 (example_11-1 nil 3622997593 ("" (sturm) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (SturmRel? const-decl "bool" compute_sturm "Sturm/") (<= const-decl "bool" reals nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (contains? const-decl "bool" RealInt "reals/") (expt_x1 formula-decl nil exponentiation nil) (polylist_monom formula-decl nil polylist "Sturm/") (polylist_const formula-decl nil polylist "Sturm/") (polylist_minus formula-decl nil polylist "Sturm/") (polylist_sum formula-decl nil polylist "Sturm/") (polylist_prod formula-decl nil polylist "Sturm/") (real_times_real_is_real application-judgement "real" reals nil) (abs_le formula-decl nil abs_lems "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sturm const-decl "bool" poly_strategy "Sturm/") (stu__137 skolem-const-decl "Polylist" sturm_examples nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (pprod const-decl "Polylist" polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (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) (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (pconst const-decl "Polylist" polylist "Sturm/") (psum def-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}" polylist "Sturm/")) shostak)) (example_12_TCC1 0 (example_12_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_12_TCC2 0 (example_12_TCC2-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_12 0 (example_12-1 nil 3622997593 ("" (sturm) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (contains? const-decl "bool" RealInt "reals/") (polylist_monom formula-decl nil polylist "Sturm/") (polylist_const formula-decl nil polylist "Sturm/") (polylist_minus formula-decl nil polylist "Sturm/") (polylist_sum formula-decl nil polylist "Sturm/") (real_plus_real_is_real application-judgement "real" reals nil) (sturm const-decl "bool" poly_strategy "Sturm/") (stu__140 skolem-const-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pconst(1))(x) + polylist(pminus(pmonom(1, 120), pmonom(2, 60)))(x)}" sturm_examples nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (polylist const-decl "real" polylist "Sturm/") (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (psum def-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}" polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (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) (length def-decl "nat" list_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (pconst const-decl "Polylist" polylist "Sturm/")) shostak)) (legendre_TCC1 0 (legendre_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (legendre_TCC2 0 (legendre_TCC2-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (legendre_TCC3 0 (legendre_TCC3-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (legendre 0 (legendre-1 nil 3622997593 ("" (sturm) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (RealInt type-eq-decl nil RealInt "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (abs_lt formula-decl nil abs_lems "reals/") (polylist_minus formula-decl nil polylist "Sturm/") (polylist_monom formula-decl nil polylist "Sturm/") (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (polylist_sum formula-decl nil polylist "Sturm/") (polylist_const formula-decl nil polylist "Sturm/") (contains? const-decl "bool" RealInt "reals/") (sturm const-decl "bool" poly_strategy "Sturm/") (stu__143 skolem-const-decl "Polylist" sturm_examples nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (polylist const-decl "real" polylist "Sturm/") (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (psum def-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}" polylist "Sturm/") (pconst const-decl "Polylist" polylist "Sturm/") (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields 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) (length def-decl "nat" list_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil)) shostak)) (legendre3_TCC1 0 (legendre3_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (^ const-decl "real" exponentiation nil)) nil)) (legendre3 0 (legendre3-1 nil 3622997593 ("" (sturm) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (RealInt type-eq-decl nil RealInt "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (abs_lt formula-decl nil abs_lems "reals/") (polylist_pow formula-decl nil polylist "Sturm/") (polylist_minus formula-decl nil polylist "Sturm/") (polylist_monom formula-decl nil polylist "Sturm/") (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (polylist_sum formula-decl nil polylist "Sturm/") (polylist_const formula-decl nil polylist "Sturm/") (contains? const-decl "bool" RealInt "reals/") (sturm const-decl "bool" poly_strategy "Sturm/") (stu__146 skolem-const-decl "Polylist" sturm_examples nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (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) (ppow def-decl "Polylist" polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (polylist const-decl "real" polylist "Sturm/") (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (psum def-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}" polylist "Sturm/") (pconst const-decl "Polylist" polylist "Sturm/") (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (length def-decl "nat" list_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil)) shostak)) (harrison_sos_TCC1 0 (harrison_sos_TCC1-1 nil 3624270611 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (harrison_sos_TCC2 0 (harrison_sos_TCC2-1 nil 3624270611 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (harrison_sos 0 (harrison_sos-1 nil 3624270612 ("" (sturm) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (contains? const-decl "bool" RealInt "reals/") (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) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nat_exp application-judgement "nat" exponentiation nil) (expt_x1 formula-decl nil exponentiation nil) (polylist_monom formula-decl nil polylist "Sturm/") (polylist_prod formula-decl nil polylist "Sturm/") (polylist_pow formula-decl nil polylist "Sturm/") (polylist_sum formula-decl nil polylist "Sturm/") (polylist_const formula-decl nil polylist "Sturm/") (polylist_minus formula-decl nil polylist "Sturm/") (polylist_div formula-decl nil polylist "Sturm/") (real_div_nzreal_is_real application-judgement "real" reals nil) (sturm const-decl "bool" poly_strategy "Sturm/") (stu__149 skolem-const-decl "Polylist" sturm_examples nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (rational nonempty-type-from-decl nil rationals nil) (/= const-decl "boolean" notequal nil) (nzrat nonempty-type-eq-decl nil rationals nil) (pdiv const-decl "Polylist" polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (polylist const-decl "real" polylist "Sturm/") (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (psum def-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}" polylist "Sturm/") (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) (ppow def-decl "Polylist" polylist "Sturm/") (length def-decl "nat" list_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (pconst const-decl "Polylist" polylist "Sturm/") (pprod const-decl "Polylist" polylist "Sturm/")) shostak)) (example_13 0 (example_13-1 nil 3622997593 ("" (sturm) nil nil) ((real_plus_real_is_real application-judgement "real" reals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (minus_even_is_even application-judgement "even_int" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (<= const-decl "bool" reals nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (expt_x1 formula-decl nil exponentiation nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (polylist_monom formula-decl nil polylist "Sturm/") (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (polylist_sum formula-decl nil polylist "Sturm/") (polylist_const formula-decl nil polylist "Sturm/") (polylist_minus formula-decl nil polylist "Sturm/") (contains? const-decl "bool" RealInt "reals/") (Interval type-eq-decl nil interval "interval_arith/") (|##| const-decl "bool" interval "interval_arith/") ([\|\|] const-decl "Interval" interval "interval_arith/") (sturm const-decl "bool" poly_strategy "Sturm/") (stu__152 skolem-const-decl "Polylist" sturm_examples nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (polylist const-decl "real" polylist "Sturm/") (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (psum def-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}" polylist "Sturm/") (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) (length def-decl "nat" list_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (pconst const-decl "Polylist" polylist "Sturm/") (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)) shostak)) (example_14 0 (example_14-1 nil 3622997594 ("" (sturm) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (SturmRel? const-decl "bool" compute_sturm "Sturm/") (<= const-decl "bool" reals nil) (FALSE const-decl "bool" booleans nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (RealInf type-decl nil RealInt "reals/") ([\|\|] const-decl "RealInt" RealInt "reals/") (inf? adt-recognizer-decl "[RealInf -> boolean]" RealInt "reals/") (oo adt-constructor-decl "(inf?)" RealInt "reals/") (|##| const-decl "bool" RealInt "reals/") (contains? const-decl "bool" RealInt "reals/") (minus_real_is_real application-judgement "real" reals nil) (polylist_neg formula-decl nil polylist "Sturm/") (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist "Sturm/") (sturm const-decl "bool" poly_strategy "Sturm/") (stu__155 skolem-const-decl "Polylist" sturm_examples nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (pneg const-decl "Polylist" polylist "Sturm/") (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) (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/")) shostak)) (example_15 0 (example_15-1 nil 3622997594 ("" (sturm) nil nil) ((minus_real_is_real application-judgement "real" reals nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (RealInf type-decl nil RealInt "reals/") ([\|\|] const-decl "RealInt" RealInt "reals/") (open? adt-recognizer-decl "[RealInf -> boolean]" RealInt "reals/") (open adt-constructor-decl "[real -> (open?)]" RealInt "reals/") (inf? adt-recognizer-decl "[RealInf -> boolean]" RealInt "reals/") (oo adt-constructor-decl "(inf?)" RealInt "reals/") (|##| const-decl "bool" RealInt "reals/") (contains? const-decl "bool" RealInt "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (polylist_minus formula-decl nil polylist "Sturm/") (polylist_const formula-decl nil polylist "Sturm/") (polylist_neg formula-decl nil polylist "Sturm/") (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist "Sturm/") (sturm const-decl "bool" poly_strategy "Sturm/") (stu__158 skolem-const-decl "Polylist" sturm_examples nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (pneg const-decl "Polylist" polylist "Sturm/") (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) (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (pconst const-decl "Polylist" polylist "Sturm/")) shostak)) (example_16 0 (example_16-1 nil 3622997594 ("" (sturm) nil nil) ((real_times_real_is_real application-judgement "real" reals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (SturmRel? const-decl "bool" compute_sturm "Sturm/") (<= const-decl "bool" reals nil) (FALSE const-decl "bool" booleans nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (RealInf type-decl nil RealInt "reals/") ([\|\|] const-decl "RealInt" RealInt "reals/") (inf? adt-recognizer-decl "[RealInf -> boolean]" RealInt "reals/") (Inf type-eq-decl nil RealInt "reals/") (ninf? adt-recognizer-decl "[RealInf -> boolean]" RealInt "reals/") (nInf type-eq-decl nil RealInt "reals/") (- const-decl "nInf" RealInt "reals/") (oo adt-constructor-decl "(inf?)" RealInt "reals/") (expt_x1 formula-decl nil exponentiation nil) (polylist_monom formula-decl nil polylist "Sturm/") (polylist_const formula-decl nil polylist "Sturm/") (polylist_prod formula-decl nil polylist "Sturm/") (polylist_minus formula-decl nil polylist "Sturm/") (contains? const-decl "bool" RealInt "reals/") (|##| const-decl "bool" RealInt "reals/") (sturm const-decl "bool" poly_strategy "Sturm/") (stu__161 skolem-const-decl "Polylist" sturm_examples nil) (real_minus_real_is_real application-judgement "real" reals nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (pprod const-decl "Polylist" polylist "Sturm/") (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) (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (pconst const-decl "Polylist" polylist "Sturm/") (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)) shostak)) (example_17_TCC1 0 (example_17_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_17_TCC2 0 (example_17_TCC2-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_17_TCC3 0 (example_17_TCC3-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_17_TCC4 0 (example_17_TCC4-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_17 0 (example_17-1 nil 3622997594 ("" (sturm) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (SturmRel? const-decl "bool" compute_sturm "Sturm/") (FALSE const-decl "bool" booleans nil) (RealInt type-eq-decl nil RealInt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (contains? const-decl "bool" RealInt "reals/") (polylist_prod formula-decl nil polylist "Sturm/") (polylist_pow formula-decl nil polylist "Sturm/") (real_minus_real_is_real application-judgement "real" reals nil) (polylist_minus formula-decl nil polylist "Sturm/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (polylist_const formula-decl nil polylist "Sturm/") (polylist_monom formula-decl nil polylist "Sturm/") (expt_x1 formula-decl nil exponentiation nil) (sturm const-decl "bool" poly_strategy "Sturm/") (stu__164 skolem-const-decl "Polylist" sturm_examples nil) (real_times_real_is_real application-judgement "real" reals nil) (sturm_def formula-decl nil poly_strategy "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (deg const-decl "{d: below(length(pl)) | (d > 0 IFF (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0)) AND (d > 0 IMPLIES (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0)) AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist "Sturm/") (pprod const-decl "Polylist" polylist "Sturm/") (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) (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (ppow def-decl "Polylist" polylist "Sturm/") (pminus const-decl "Polylist" polylist "Sturm/") (pconst const-decl "Polylist" polylist "Sturm/")) shostak)) (mono_example_1_TCC1 0 (mono_example_1_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil) nil nil)) (mono_example_1 0 (mono_example_1-1 nil 3622997594 ("" (mono-poly) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (mono_def formula-decl nil compute_sturm "Sturm/") (mono const-decl "bool" compute_sturm "Sturm/") (lp__171 skolem-const-decl "[nat -> rat]" sturm_examples nil) (pl__169 skolem-const-decl "(cons?[numfield])" sturm_examples nil) (polylist_sum formula-decl nil polylist "Sturm/") (polylist_minus formula-decl nil polylist "Sturm/") (polylist_prod formula-decl nil polylist "Sturm/") (polylist_pow formula-decl nil polylist "Sturm/") (polylist_const formula-decl nil polylist "Sturm/") (polylist_monom formula-decl nil polylist "Sturm/") (expt_x1 formula-decl nil exponentiation nil) (p1__167 skolem-const-decl "Polylist" sturm_examples nil) (p2__168 skolem-const-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pconst(1/16))(x) + polylist(pminus(pprod(pmonom(1, 1), pmonom(1, 1)), pmonom(1/2, 1))) (x)}" sturm_examples nil) (polylist_eval formula-decl nil polylist "Sturm/") (xval__170 skolem-const-decl "[# bounded_above: bool, bounded_below: bool, closed_above: bool, closed_below: bool, lb: posint, ub: posint #]" sturm_examples nil) (contains? const-decl "bool" RealInt "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (RealInt type-eq-decl nil RealInt "reals/") (posnat nonempty-type-eq-decl nil integers nil) (relvar__174 skolem-const-decl "RealOrder" sturm_examples nil) (rel__173 skolem-const-decl "RealOrder" sturm_examples nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (deg__172 skolem-const-decl "int" sturm_examples nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (<= const-decl "bool" reals nil) (realorder? const-decl "bool" real_orders "reals/") (RealOrder type-eq-decl nil real_orders "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_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) (list2array def-decl "T" array2list "structures/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posint nonempty-type-eq-decl nil integers nil) (FALSE const-decl "bool" booleans nil) (pprod const-decl "Polylist" polylist "Sturm/") (psum def-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}" polylist "Sturm/") (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (pconst const-decl "Polylist" polylist "Sturm/") (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (length def-decl "nat" list_props nil) (pminus const-decl "Polylist" polylist "Sturm/") (ppow def-decl "Polylist" polylist "Sturm/") (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) (Polylist type-eq-decl nil polylist "Sturm/") (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (rat nonempty-type-eq-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) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil)) shostak)) (mono_example_2_TCC1 0 (mono_example_2_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (mono_example_2 0 (mono_example_2-1 nil 3622997594 ("" (mono-poly) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (mono_def formula-decl nil compute_sturm "Sturm/") (mono const-decl "bool" compute_sturm "Sturm/") (contains? const-decl "bool" RealInt "reals/") (xval__180 skolem-const-decl "[# bounded_above: bool, bounded_below: bool, closed_above: bool, closed_below: bool, lb: odd_int, ub: posint #]" sturm_examples nil) (polylist_eval formula-decl nil polylist "Sturm/") (p2__178 skolem-const-decl "{pl: Polylist | length(pl) = 6 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 5)}" sturm_examples nil) (p1__177 skolem-const-decl "{pl: Polylist | length(pl) = 6 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 5)}" sturm_examples nil) (polylist_monom formula-decl nil polylist "Sturm/") (real_times_real_is_real application-judgement "real" reals nil) (pl__179 skolem-const-decl "(cons?)" sturm_examples nil) (lp__181 skolem-const-decl "[nat -> rat]" sturm_examples nil) (RealInt type-eq-decl nil RealInt "reals/") (posnat nonempty-type-eq-decl nil integers nil) (relvar__184 skolem-const-decl "RealOrder" sturm_examples nil) (rel__183 skolem-const-decl "[[real, real] -> boolean]" sturm_examples nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (deg__182 skolem-const-decl "int" sturm_examples nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (realorder? const-decl "bool" real_orders "reals/") (RealOrder type-eq-decl nil real_orders "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (list2array def-decl "T" array2list "structures/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (odd? const-decl "bool" integers nil) (odd_int nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posint nonempty-type-eq-decl nil integers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (FALSE const-decl "bool" booleans nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (length def-decl "nat" list_props nil) (Polylist type-eq-decl nil polylist "Sturm/") (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types 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) (rat nonempty-type-eq-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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil)) shostak)) (mono_example_3_TCC1 0 (mono_example_3_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (mono_example_3_TCC2 0 (mono_example_3_TCC2-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (mono_example_3 0 (mono_example_3-1 nil 3622997594 ("" (mono-poly) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (mono_def formula-decl nil compute_sturm "Sturm/") (mono const-decl "bool" compute_sturm "Sturm/") (lp__191 skolem-const-decl "[nat -> rat]" sturm_examples nil) (pl__189 skolem-const-decl "(cons?[numfield])" sturm_examples nil) (polylist_sum formula-decl nil polylist "Sturm/") (polylist_minus formula-decl nil polylist "Sturm/") (polylist_prod formula-decl nil polylist "Sturm/") (polylist_div formula-decl nil polylist "Sturm/") (polylist_monom formula-decl nil polylist "Sturm/") (expt_x1 formula-decl nil exponentiation nil) (polylist_const formula-decl nil polylist "Sturm/") (p1__187 skolem-const-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pdiv(pmonom(1, 1), 5))(x) + polylist(pminus(pmonom(1, 5), pmonom(1, 3)))(x)}" sturm_examples nil) (p2__188 skolem-const-decl "Polylist" sturm_examples nil) (polylist_eval formula-decl nil polylist "Sturm/") (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (xval__190 skolem-const-decl "[# bounded_above: bool, bounded_below: bool, closed_above: bool, closed_below: bool, lb: posrat, ub: posrat #]" sturm_examples nil) (contains? const-decl "bool" RealInt "reals/") (RealInt type-eq-decl nil RealInt "reals/") (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (relvar__194 skolem-const-decl "RealOrder" sturm_examples nil) (rel__193 skolem-const-decl "RealOrder" sturm_examples nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (deg__192 skolem-const-decl "int" sturm_examples nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (realorder? const-decl "bool" real_orders "reals/") (RealOrder type-eq-decl nil real_orders "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (list2array def-decl "T" array2list "structures/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (nonneg_rat nonempty-type-eq-decl nil rationals nil) (> const-decl "bool" reals nil) (posrat nonempty-type-eq-decl nil rationals nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (pconst const-decl "Polylist" polylist "Sturm/") (pprod const-decl "Polylist" polylist "Sturm/") (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (pdiv const-decl "Polylist" polylist "Sturm/") (nzrat nonempty-type-eq-decl nil rationals nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (length def-decl "nat" list_props 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) (pminus const-decl "Polylist" polylist "Sturm/") (psum def-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}" polylist "Sturm/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (polylist const-decl "real" polylist "Sturm/") (Polylist type-eq-decl nil polylist "Sturm/") (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (rat nonempty-type-eq-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) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil)) shostak)) (mono_example_4_TCC1 0 (mono_example_4_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (mono_example_4 0 (mono_example_4-1 nil 3622997594 ("" (mono-poly) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (mono_def formula-decl nil compute_sturm "Sturm/") (< const-decl "bool" reals nil) (mono const-decl "bool" compute_sturm "Sturm/") (contains? const-decl "bool" RealInt "reals/") (xval__200 skolem-const-decl "[# bounded_above: bool, bounded_below: bool, closed_above: bool, closed_below: bool, lb: odd_int, ub: posint #]" sturm_examples nil) (polylist_eval formula-decl nil polylist "Sturm/") (p2__198 skolem-const-decl "{pl: Polylist | length(pl) = 4 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 3)}" sturm_examples nil) (p1__197 skolem-const-decl "{pl: Polylist | length(pl) = 4 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 3)}" sturm_examples nil) (polylist_monom formula-decl nil polylist "Sturm/") (real_times_real_is_real application-judgement "real" reals nil) (pl__199 skolem-const-decl "(cons?)" sturm_examples nil) (lp__201 skolem-const-decl "[nat -> rat]" sturm_examples nil) (RealInt type-eq-decl nil RealInt "reals/") (posnat nonempty-type-eq-decl nil integers nil) (relvar__204 skolem-const-decl "[[real, real] -> boolean]" sturm_examples nil) (rel__203 skolem-const-decl "[[real, real] -> boolean]" sturm_examples nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (deg__202 skolem-const-decl "int" sturm_examples nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (list2array def-decl "T" array2list "structures/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (odd? const-decl "bool" integers nil) (odd_int nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posint nonempty-type-eq-decl nil integers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (FALSE const-decl "bool" booleans nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (length def-decl "nat" list_props nil) (Polylist type-eq-decl nil polylist "Sturm/") (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types 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) (rat nonempty-type-eq-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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil)) shostak)) (mono_example_5 0 (mono_example_5-1 nil 3622997594 ("" (mono-poly) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (mono_def formula-decl nil compute_sturm "Sturm/") (mono const-decl "bool" compute_sturm "Sturm/") (contains? const-decl "bool" RealInt "reals/") (lp__211 skolem-const-decl "[nat -> rat]" sturm_examples nil) (xval__210 skolem-const-decl "[# bounded_above: bool, bounded_below: bool, closed_above: bool, closed_below: bool, lb: odd_int, ub: posint #]" sturm_examples nil) (polylist_eval formula-decl nil polylist "Sturm/") (p2__208 skolem-const-decl "Polylist" sturm_examples nil) (p1__207 skolem-const-decl "{pl: Polylist | length(pl) = 3 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 2)}" sturm_examples nil) (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist "Sturm/") (polylist_sq formula-decl nil polylist "Sturm/") (expt_x1 formula-decl nil exponentiation nil) (pl__209 skolem-const-decl "(cons?)" sturm_examples nil) (RealInt type-eq-decl nil RealInt "reals/") (posnat nonempty-type-eq-decl nil integers nil) (relvar__214 skolem-const-decl "RealOrder" sturm_examples nil) (rel__213 skolem-const-decl "RealOrder" sturm_examples nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (deg__212 skolem-const-decl "int" sturm_examples nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (realorder? const-decl "bool" real_orders "reals/") (RealOrder type-eq-decl nil real_orders "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (list2array def-decl "T" array2list "structures/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (odd? const-decl "bool" integers nil) (odd_int nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posint nonempty-type-eq-decl nil integers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (FALSE const-decl "bool" booleans nil) (psq const-decl "Polylist" polylist "Sturm/") (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (length def-decl "nat" list_props nil) (Polylist type-eq-decl nil polylist "Sturm/") (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types 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) (rat nonempty-type-eq-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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil)) shostak)) (mono_example_6_TCC1 0 (mono_example_6_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (mono_example_6 0 (mono_example_6-1 nil 3622997594 ("" (mono-poly) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (mono_def formula-decl nil compute_sturm "Sturm/") (< const-decl "bool" reals nil) (mono const-decl "bool" compute_sturm "Sturm/") (contains? const-decl "bool" RealInt "reals/") (lp__221 skolem-const-decl "[nat -> rat]" sturm_examples nil) (xval__220 skolem-const-decl "[# bounded_above: bool, bounded_below: bool, closed_above: bool, closed_below: bool, lb: odd_int, ub: naturalnumber #]" sturm_examples nil) (polylist_eval formula-decl nil polylist "Sturm/") (p2__218 skolem-const-decl "{pl: Polylist | length(pl) = 5 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 4)}" sturm_examples nil) (p1__217 skolem-const-decl "{pl: Polylist | length(pl) = 5 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 4)}" sturm_examples nil) (x_226 skolem-const-decl "real" sturm_examples nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (polylist_monom formula-decl nil polylist "Sturm/") (real_times_real_is_real application-judgement "real" reals nil) (pl__219 skolem-const-decl "(cons?)" sturm_examples nil) (RealInt type-eq-decl nil RealInt "reals/") (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (relvar__224 skolem-const-decl "RealOrder" sturm_examples nil) (rel__223 skolem-const-decl "RealOrder" sturm_examples nil) (SturmRel? const-decl "bool" compute_sturm "Sturm/") (deg__222 skolem-const-decl "int" sturm_examples nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (> const-decl "bool" reals nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (realorder? const-decl "bool" real_orders "reals/") (RealOrder type-eq-decl nil real_orders "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (list2array def-decl "T" array2list "structures/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (odd? const-decl "bool" integers nil) (odd_int nonempty-type-eq-decl nil integers nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (FALSE const-decl "bool" booleans nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist "Sturm/") (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist "Sturm/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (length def-decl "nat" list_props nil) (Polylist type-eq-decl nil polylist "Sturm/") (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types 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) (rat nonempty-type-eq-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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil)) shostak)))
¤ Dauer der Verarbeitung: 0.58 Sekunden (vorverarbeitet am 2026-05-01) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26