| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/Sturm/ (Beweissystem der NASA Version 6.0.9©) Datei vom 7.10.2014 mit Größe 155 kB |
|
SSL examples.prfSprache: Lisp |
|||||||||||||||
|
(examples (example_1_TCC1 0 (example_1_TCC1-1 nil 3622995204 ("" (subtype-tcc) nil nil) nil nil)) (example_1_TCC2 0 (example_1_TCC2-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_1_TCC3 0 (example_1_TCC3-1 nil 3622995204 ("" (subtype-tcc) nil nil) nil nil)) (example_1 0 (example_1-1 nil 3623007006 ("" (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 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/") (expt_x1 formula-decl nil exponentiation nil) (polylist_minus formula-decl nil polylist nil) (real_minus_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist nil) (polylist_pow formula-decl nil polylist nil) (polylist_sum formula-decl nil polylist nil) (polylist_const formula-decl nil polylist nil) (polylist_prod formula-decl nil polylist nil) (contains? const-decl "bool" RealInt "reals/") (sturm const-decl "bool" poly_strategy nil) (stu__1 skolem-const-decl "Polylist" 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 nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (pprod const-decl "Polylist" polylist nil) (pconst const-decl "Polylist" polylist nil) (polylist const-decl "real" polylist nil) (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 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) (ppow def-decl "Polylist" polylist nil) (pminus const-decl "Polylist" polylist 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 nil) (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 3623007006 ("" (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 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/") (polylist_prod formula-decl nil polylist nil) (polylist_pow formula-decl nil polylist nil) (real_plus_real_is_real application-judgement "real" reals nil) (polylist_sum formula-decl nil polylist nil) (polylist_const formula-decl nil polylist nil) (polylist_monom formula-decl nil polylist nil) (real_minus_real_is_real application-judgement "real" reals nil) (polylist_minus formula-decl nil polylist nil) (expt_x1 formula-decl nil exponentiation nil) (contains? const-decl "bool" RealInt "reals/") (sturm const-decl "bool" poly_strategy nil) (stu__4 skolem-const-decl "Polylist" examples nil) (real_times_real_is_real application-judgement "real" reals nil) (sturm_def formula-decl nil poly_strategy nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (pprod const-decl "Polylist" polylist 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) (ppow def-decl "Polylist" polylist nil) (pminus const-decl "Polylist" polylist 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 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 nil) (pconst const-decl "Polylist" polylist nil) (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 nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil)) shostak)) (example_3_TCC1 0 (example_3_TCC1-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC2 0 (example_3_TCC2-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC3 0 (example_3_TCC3-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC4 0 (example_3_TCC4-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC5 0 (example_3_TCC5-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC6 0 (example_3_TCC6-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC7 0 (example_3_TCC7-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC8 0 (example_3_TCC8-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC9 0 (example_3_TCC9-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC10 0 (example_3_TCC10-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC11 0 (example_3_TCC11-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC12 0 (example_3_TCC12-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC13 0 (example_3_TCC13-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_3_TCC14 0 (example_3_TCC14-1 nil 3622995204 ("" (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 3623007006 ("" (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 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/") (polylist_pow formula-decl nil polylist nil) (polylist_sum formula-decl nil polylist nil) (polylist_const formula-decl nil polylist nil) (polylist_minus formula-decl nil polylist nil) (polylist_monom formula-decl nil polylist nil) (expt_x1 formula-decl nil exponentiation nil) (sturm const-decl "bool" poly_strategy nil) (stu__7 skolem-const-decl "Polylist" 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 nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 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) (ppow def-decl "Polylist" polylist nil) (polylist const-decl "real" polylist nil) (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 nil) (pminus const-decl "Polylist" polylist 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 nil) (pconst const-decl "Polylist" polylist nil)) shostak)) (example_4_TCC1 0 (example_4_TCC1-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_4 0 (example_4-1 nil 3623007006 ("" (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 nil) (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 nil) (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist nil) (polylist_neg formula-decl nil polylist nil) (expt_x1 formula-decl nil exponentiation nil) (sturm const-decl "bool" poly_strategy nil) (stu__10 skolem-const-decl "Polylist" examples nil) (sturm_def formula-decl nil poly_strategy nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (pminus const-decl "Polylist" polylist 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist 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 nil) (pneg const-decl "Polylist" polylist nil)) shostak)) (example_5 0 (example_5-1 nil 3623007006 ("" (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 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/") (contains? const-decl "bool" RealInt "reals/") (polylist_minus formula-decl nil polylist nil) (polylist_const formula-decl nil polylist nil) (polylist_monom formula-decl nil polylist nil) (sturm const-decl "bool" poly_strategy nil) (stu__13 skolem-const-decl "Polylist" examples nil) (real_times_real_is_real application-judgement "real" reals nil) (sturm_def formula-decl nil poly_strategy nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (pminus const-decl "Polylist" polylist 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist 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 nil) (pconst const-decl "Polylist" polylist nil)) shostak)) (example_6_TCC1 0 (example_6_TCC1-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_6 0 (example_6-1 nil 3623007006 ("" (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 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 nil) (polylist_const formula-decl nil polylist nil) (polylist_minus formula-decl nil polylist nil) (polylist_sum formula-decl nil polylist nil) (real_plus_real_is_real application-judgement "real" reals nil) (sturm const-decl "bool" poly_strategy nil) (stu__16 skolem-const-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pconst(1))(x) + polylist(pminus(pmonom(1, 2), pmonom(2, 1)))(x)}" 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 nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (polylist const-decl "real" polylist nil) (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 nil) (pminus const-decl "Polylist" polylist 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 "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 nil) (pconst const-decl "Polylist" polylist nil)) shostak)) (example_7 0 (example_7-1 nil 3623007006 ("" (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 nil) (<= 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 nil) (polylist_const formula-decl nil polylist nil) (polylist_prod formula-decl nil polylist nil) (polylist_minus formula-decl nil polylist nil) (sturm const-decl "bool" poly_strategy nil) (stu__19 skolem-const-decl "Polylist" examples nil) (real_minus_real_is_real application-judgement "real" reals nil) (sturm_def formula-decl nil poly_strategy nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (pminus const-decl "Polylist" polylist nil) (pprod const-decl "Polylist" polylist 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist 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 nil) (pconst const-decl "Polylist" polylist nil) (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 3623007006 ("" (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 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/") (real_minus_real_is_real application-judgement "real" reals nil) (polylist_minus formula-decl nil polylist nil) (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist nil) (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 nil) (stu__22 skolem-const-decl "Polylist" examples nil) (sturm_def formula-decl nil poly_strategy nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (pminus const-decl "Polylist" polylist 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist 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 nil)) shostak)) (example_n8 0 (example_n8-1 nil 3623007006 ("" (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 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/") (real_minus_real_is_real application-judgement "real" reals nil) (polylist_minus formula-decl nil polylist nil) (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist nil) (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 nil) (stu__25 skolem-const-decl "Polylist" examples nil) (sturm_def formula-decl nil poly_strategy nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (pminus const-decl "Polylist" polylist 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist 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 nil)) shostak)) (example_80 0 (example_80-1 nil 3623007006 ("" (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 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/") (real_minus_real_is_real application-judgement "real" reals nil) (polylist_minus formula-decl nil polylist nil) (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist nil) (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 nil) (stu__28 skolem-const-decl "Polylist" examples nil) (sturm_def formula-decl nil poly_strategy nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (pminus const-decl "Polylist" polylist 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist 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 nil)) shostak)) (example_n80 0 (example_n80-1 nil 3623007006 ("" (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 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/") (real_minus_real_is_real application-judgement "real" reals nil) (polylist_minus formula-decl nil polylist nil) (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist nil) (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 nil) (stu__31 skolem-const-decl "Polylist" examples nil) (sturm_def formula-decl nil poly_strategy nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (pminus const-decl "Polylist" polylist 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist 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 nil)) shostak)) (example_9 0 (example_9-1 nil 3623007006 ("" (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 nil) (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 nil) (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist nil) (polylist_neg formula-decl nil polylist nil) (expt_x1 formula-decl nil exponentiation nil) (sturm const-decl "bool" poly_strategy nil) (stu__34 skolem-const-decl "Polylist" examples nil) (sturm_def formula-decl nil poly_strategy nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (pminus const-decl "Polylist" polylist 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist 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 nil) (pneg const-decl "Polylist" polylist nil)) shostak)) (example_n9 0 (example_n9-1 nil 3623007006 ("" (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 nil) (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 nil) (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist nil) (polylist_neg formula-decl nil polylist nil) (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 nil) (stu__37 skolem-const-decl "Polylist" examples nil) (sturm_def formula-decl nil poly_strategy nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (pminus const-decl "Polylist" polylist 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist 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 nil) (pneg const-decl "Polylist" polylist nil)) shostak)) (example_90 0 (example_90-1 nil 3623007006 ("" (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 nil) (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 nil) (sturm const-decl "bool" poly_strategy nil) (stu__40 skolem-const-decl "{pl: Polylist | length(pl) = 6 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 5)}" examples nil) (sturm_def formula-decl nil poly_strategy nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (< 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 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) (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 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 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 nil)) shostak)) (example_n90 0 (example_n90-1 nil 3623007006 ("" (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 nil) (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 nil) (sturm const-decl "bool" poly_strategy nil) (stu__43 skolem-const-decl "{pl: Polylist | length(pl) = 6 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 5)}" examples nil) (sturm_def formula-decl nil poly_strategy nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (< 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 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) (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 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 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 nil)) shostak)) (example_10 0 (example_10-1 nil 3623007006 ("" (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 nil) (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 nil) (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 nil) (stu__46 skolem-const-decl "{pl: Polylist | length(pl) = 4 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 3)}" examples nil) (sturm_def formula-decl nil poly_strategy nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (< 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 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) (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 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 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 nil)) shostak)) (example_11 0 (example_11-1 nil 3623007006 ("" (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 nil) (<= 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 nil) (polylist_const formula-decl nil polylist nil) (polylist_minus formula-decl nil polylist nil) (polylist_sum formula-decl nil polylist nil) (polylist_prod formula-decl nil polylist nil) (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 nil) (stu__49 skolem-const-decl "Polylist" 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 nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (pprod const-decl "Polylist" polylist nil) (pminus const-decl "Polylist" polylist 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist 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 nil) (pconst const-decl "Polylist" polylist nil) (psum def-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}" polylist nil)) shostak)) (example_12_TCC1 0 (example_12_TCC1-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_12_TCC2 0 (example_12_TCC2-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_12 0 (example_12-1 nil 3623007006 ("" (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 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/") (polylist_monom formula-decl nil polylist nil) (polylist_const formula-decl nil polylist nil) (polylist_minus formula-decl nil polylist nil) (polylist_sum formula-decl nil polylist nil) (real_plus_real_is_real application-judgement "real" reals nil) (sturm const-decl "bool" poly_strategy nil) (stu__52 skolem-const-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pconst(1))(x) + polylist(pminus(pmonom(1, 120), pmonom(2, 60)))(x)}" 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 nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (polylist const-decl "real" polylist nil) (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 nil) (pminus const-decl "Polylist" polylist 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 "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 nil) (pconst const-decl "Polylist" polylist nil)) shostak)) (legendre_TCC1 0 (legendre_TCC1-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (legendre_TCC2 0 (legendre_TCC2-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (legendre_TCC3 0 (legendre_TCC3-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (legendre 0 (legendre-1 nil 3623007006 ("" (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 nil) (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 nil) (polylist_monom formula-decl nil polylist nil) (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (polylist_sum formula-decl nil polylist nil) (polylist_const formula-decl nil polylist nil) (contains? const-decl "bool" RealInt "reals/") (sturm const-decl "bool" poly_strategy nil) (stu__55 skolem-const-decl "Polylist" 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 nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (pminus const-decl "Polylist" polylist nil) (polylist const-decl "real" polylist nil) (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 nil) (pconst const-decl "Polylist" polylist nil) (/= 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 nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil)) shostak)) (legendre3_TCC1 0 (legendre3_TCC1-1 nil 3622995204 ("" (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 3623007006 ("" (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 nil) (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 nil) (polylist_minus formula-decl nil polylist nil) (polylist_monom formula-decl nil polylist nil) (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (polylist_sum formula-decl nil polylist nil) (polylist_const formula-decl nil polylist nil) (contains? const-decl "bool" RealInt "reals/") (sturm const-decl "bool" poly_strategy nil) (stu__58 skolem-const-decl "Polylist" 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 nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 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) (ppow def-decl "Polylist" polylist nil) (pminus const-decl "Polylist" polylist nil) (polylist const-decl "real" polylist nil) (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 nil) (pconst const-decl "Polylist" polylist nil) (/= 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 nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil)) shostak)) (harrison_sos_TCC1 0 (harrison_sos_TCC1-1 nil 3624270495 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (harrison_sos_TCC2 0 (harrison_sos_TCC2-1 nil 3624270495 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (harrison_sos 0 (harrison_sos-1 nil 3624270496 ("" (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 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/") (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 nil) (polylist_prod formula-decl nil polylist nil) (polylist_pow formula-decl nil polylist nil) (polylist_sum formula-decl nil polylist nil) (polylist_const formula-decl nil polylist nil) (polylist_minus formula-decl nil polylist nil) (polylist_div formula-decl nil polylist nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (sturm const-decl "bool" poly_strategy nil) (stu__61 skolem-const-decl "Polylist" 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 nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (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 nil) (pminus const-decl "Polylist" polylist nil) (polylist const-decl "real" polylist nil) (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 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 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 nil) (pconst const-decl "Polylist" polylist nil) (pprod const-decl "Polylist" polylist nil)) shostak)) (example_13 0 (example_13-1 nil 3623007006 ("" (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 nil) (<= 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 nil) (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (polylist_sum formula-decl nil polylist nil) (polylist_const formula-decl nil polylist nil) (polylist_minus formula-decl nil polylist nil) (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 nil) (stu__64 skolem-const-decl "Polylist" 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 nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (pminus const-decl "Polylist" polylist nil) (polylist const-decl "real" polylist nil) (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 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 "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 nil) (pconst const-decl "Polylist" polylist nil) (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 3623007006 ("" (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 nil) (<= 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 nil) (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist nil) (sturm const-decl "bool" poly_strategy nil) (stu__67 skolem-const-decl "Polylist" examples nil) (sturm_def formula-decl nil poly_strategy nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (pneg const-decl "Polylist" polylist 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist 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 nil)) shostak)) (example_15 0 (example_15-1 nil 3623007006 ("" (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 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/") (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 nil) (polylist_const formula-decl nil polylist nil) (polylist_neg formula-decl nil polylist nil) (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist nil) (sturm const-decl "bool" poly_strategy nil) (stu__70 skolem-const-decl "Polylist" examples nil) (sturm_def formula-decl nil poly_strategy nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (pminus const-decl "Polylist" polylist nil) (pneg const-decl "Polylist" polylist 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist 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 nil) (pconst const-decl "Polylist" polylist nil)) shostak)) (example_16 0 (example_16-1 nil 3623007006 ("" (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 nil) (<= 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 nil) (polylist_const formula-decl nil polylist nil) (polylist_prod formula-decl nil polylist nil) (polylist_minus formula-decl nil polylist nil) (contains? const-decl "bool" RealInt "reals/") (|##| const-decl "bool" RealInt "reals/") (sturm const-decl "bool" poly_strategy nil) (stu__73 skolem-const-decl "Polylist" examples nil) (real_minus_real_is_real application-judgement "real" reals nil) (sturm_def formula-decl nil poly_strategy nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (pminus const-decl "Polylist" polylist nil) (pprod const-decl "Polylist" polylist 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist 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 nil) (pconst const-decl "Polylist" polylist nil) (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 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_17_TCC2 0 (example_17_TCC2-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_17_TCC3 0 (example_17_TCC3-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_17_TCC4 0 (example_17_TCC4-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (example_17 0 (example_17-1 nil 3623007006 ("" (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 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/") (polylist_prod formula-decl nil polylist nil) (polylist_pow formula-decl nil polylist nil) (real_minus_real_is_real application-judgement "real" reals nil) (polylist_minus formula-decl nil polylist nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (polylist_const formula-decl nil polylist nil) (polylist_monom formula-decl nil polylist nil) (expt_x1 formula-decl nil exponentiation nil) (sturm const-decl "bool" poly_strategy nil) (stu__76 skolem-const-decl "Polylist" examples nil) (real_times_real_is_real application-judgement "real" reals nil) (sturm_def formula-decl nil poly_strategy nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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 nil) (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 nil) (pprod const-decl "Polylist" polylist 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist 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 nil) (ppow def-decl "Polylist" polylist nil) (pminus const-decl "Polylist" polylist nil) (pconst const-decl "Polylist" polylist nil)) shostak)) (mono_example_1_TCC1 0 (mono_example_1_TCC1-1 nil 3622995204 ("" (subtype-tcc) nil nil) nil nil)) (mono_example_1 0 (mono_example_1-1 nil 3623007006 ("" (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 nil) (mono const-decl "bool" compute_sturm nil) (lp__83 skolem-const-decl "[nat -> rat]" examples nil) (pl__81 skolem-const-decl "(cons?[numfield])" examples nil) (polylist_sum formula-decl nil polylist nil) (polylist_minus formula-decl nil polylist nil) (polylist_prod formula-decl nil polylist nil) (polylist_pow formula-decl nil polylist nil) (polylist_const formula-decl nil polylist nil) (polylist_monom formula-decl nil polylist nil) (expt_x1 formula-decl nil exponentiation nil) (p1__79 skolem-const-decl "Polylist" examples nil) (p2__80 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)}" examples nil) (polylist_eval formula-decl nil polylist nil) (xval__82 skolem-const-decl "[# bounded_above: bool, bounded_below: bool, closed_above: bool, closed_below: bool, lb: posint, ub: posint #]" 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__86 skolem-const-decl "RealOrder" examples nil) (rel__85 skolem-const-decl "RealOrder" examples nil) (SturmRel? const-decl "bool" compute_sturm nil) (deg__84 skolem-const-decl "int" 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 nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (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 nil) (psum def-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}" polylist nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (pconst const-decl "Polylist" polylist nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist nil) (^ 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 nil) (+ 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 nil) (ppow def-decl "Polylist" polylist 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) (Polylist type-eq-decl nil polylist nil) (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 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (mono_example_2 0 (mono_example_2-1 nil 3623007006 ("" (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 nil) (mono const-decl "bool" compute_sturm nil) (contains? const-decl "bool" RealInt "reals/") (xval__92 skolem-const-decl "[# bounded_above: bool, bounded_below: bool, closed_above: bool, closed_below: bool, lb: odd_int, ub: posint #]" examples nil) (polylist_eval formula-decl nil polylist nil) (p2__90 skolem-const-decl "{pl: Polylist | length(pl) = 6 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 5)}" examples nil) (p1__89 skolem-const-decl "{pl: Polylist | length(pl) = 6 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 5)}" examples nil) (polylist_monom formula-decl nil polylist nil) (real_times_real_is_real application-judgement "real" reals nil) (pl__91 skolem-const-decl "(cons?[real])" examples nil) (lp__93 skolem-const-decl "[nat -> rat]" examples nil) (RealInt type-eq-decl nil RealInt "reals/") (posnat nonempty-type-eq-decl nil integers nil) (relvar__96 skolem-const-decl "RealOrder" examples nil) (rel__95 skolem-const-decl "[[real, real] -> boolean]" examples nil) (SturmRel? const-decl "bool" compute_sturm nil) (deg__94 skolem-const-decl "int" 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 nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (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 nil) (^ 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 nil) (+ 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 nil) (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 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (mono_example_3_TCC2 0 (mono_example_3_TCC2-1 nil 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (mono_example_3 0 (mono_example_3-1 nil 3623007006 ("" (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 nil) (mono const-decl "bool" compute_sturm nil) (lp__103 skolem-const-decl "[nat -> rat]" examples nil) (pl__101 skolem-const-decl "(cons?[numfield])" examples nil) (polylist_sum formula-decl nil polylist nil) (polylist_minus formula-decl nil polylist nil) (polylist_prod formula-decl nil polylist nil) (polylist_div formula-decl nil polylist nil) (polylist_monom formula-decl nil polylist nil) (expt_x1 formula-decl nil exponentiation nil) (polylist_const formula-decl nil polylist nil) (p1__99 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)}" examples nil) (p2__100 skolem-const-decl "Polylist" examples nil) (polylist_eval formula-decl nil polylist nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (xval__102 skolem-const-decl "[# bounded_above: bool, bounded_below: bool, closed_above: bool, closed_below: bool, lb: posrat, ub: posrat #]" 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__106 skolem-const-decl "RealOrder" examples nil) (rel__105 skolem-const-decl "RealOrder" examples nil) (SturmRel? const-decl "bool" compute_sturm nil) (deg__104 skolem-const-decl "int" 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 nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (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 nil) (pprod const-decl "Polylist" polylist nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (pdiv const-decl "Polylist" polylist nil) (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 nil) (^ 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 nil) (psum def-decl "{pql: Polylist | FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}" polylist nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (polylist const-decl "real" polylist nil) (Polylist type-eq-decl nil polylist nil) (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 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (mono_example_4 0 (mono_example_4-1 nil 3623007006 ("" (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 nil) (< const-decl "bool" reals nil) (mono const-decl "bool" compute_sturm nil) (contains? const-decl "bool" RealInt "reals/") (xval__112 skolem-const-decl "[# bounded_above: bool, bounded_below: bool, closed_above: bool, closed_below: bool, lb: odd_int, ub: posint #]" examples nil) (polylist_eval formula-decl nil polylist nil) (p2__110 skolem-const-decl "{pl: Polylist | length(pl) = 4 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 3)}" examples nil) (p1__109 skolem-const-decl "{pl: Polylist | length(pl) = 4 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 3)}" examples nil) (polylist_monom formula-decl nil polylist nil) (real_times_real_is_real application-judgement "real" reals nil) (pl__111 skolem-const-decl "(cons?[real])" examples nil) (lp__113 skolem-const-decl "[nat -> rat]" examples nil) (RealInt type-eq-decl nil RealInt "reals/") (posnat nonempty-type-eq-decl nil integers nil) (relvar__116 skolem-const-decl "[[real, real] -> boolean]" examples nil) (rel__115 skolem-const-decl "[[real, real] -> boolean]" examples nil) (SturmRel? const-decl "bool" compute_sturm nil) (deg__114 skolem-const-decl "int" 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 nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (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 nil) (^ 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 nil) (+ 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 nil) (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 3623007006 ("" (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 nil) (mono const-decl "bool" compute_sturm nil) (contains? const-decl "bool" RealInt "reals/") (lp__123 skolem-const-decl "[nat -> rat]" examples nil) (xval__122 skolem-const-decl "[# bounded_above: bool, bounded_below: bool, closed_above: bool, closed_below: bool, lb: odd_int, ub: posint #]" examples nil) (polylist_eval formula-decl nil polylist nil) (p2__120 skolem-const-decl "Polylist" examples nil) (p1__119 skolem-const-decl "{pl: Polylist | length(pl) = 3 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 2)}" examples nil) (real_times_real_is_real application-judgement "real" reals nil) (polylist_monom formula-decl nil polylist nil) (polylist_sq formula-decl nil polylist nil) (expt_x1 formula-decl nil exponentiation nil) (pl__121 skolem-const-decl "(cons?[real])" examples nil) (RealInt type-eq-decl nil RealInt "reals/") (posnat nonempty-type-eq-decl nil integers nil) (relvar__126 skolem-const-decl "RealOrder" examples nil) (rel__125 skolem-const-decl "RealOrder" examples nil) (SturmRel? const-decl "bool" compute_sturm nil) (deg__124 skolem-const-decl "int" 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 nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (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 nil) (pmonom def-decl "{pl: Polylist | length(pl) = deg + 1 AND (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist nil) (^ 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 nil) (+ 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 nil) (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 3622995204 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (mono_example_6 0 (mono_example_6-1 nil 3623007006 ("" (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 nil) (< const-decl "bool" reals nil) (mono const-decl "bool" compute_sturm nil) (contains? const-decl "bool" RealInt "reals/") (lp__133 skolem-const-decl "[nat -> rat]" examples nil) (xval__132 skolem-const-decl "[# bounded_above: bool, bounded_below: bool, closed_above: bool, closed_below: bool, lb: odd_int, ub: naturalnumber #]" examples nil) (polylist_eval formula-decl nil polylist nil) (p2__130 skolem-const-decl "{pl: Polylist | length(pl) = 5 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 4)}" examples nil) (p1__129 skolem-const-decl "{pl: Polylist | length(pl) = 5 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 4)}" examples nil) (x_138 skolem-const-decl "real" 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 nil) (real_times_real_is_real application-judgement "real" reals nil) (pl__131 skolem-const-decl "(cons?[real])" 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__136 skolem-const-decl "RealOrder" examples nil) (rel__135 skolem-const-decl "RealOrder" examples nil) (SturmRel? const-decl "bool" compute_sturm nil) (deg__134 skolem-const-decl "int" 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 nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (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 nil) (^ 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 nil) (+ 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 nil) (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.77 Sekunden (vorverarbeitet am 2026-04-28) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26