Quelle sturm_tarski_examples.prf Sprache: Lisp

(sturm_tarski_examples
(example_1a_TCC1 0
  (example_1a_TCC1-1 nil 3624181697 ("" (subtype-tcc) nil nil)
   (([\|\|] const-decl "Interval" interval "interval_arith/")
    (|##| const-decl "bool" interval "interval_arith/")
    (/= const-decl "boolean" notequal nil))
   nil))
(example_1a_TCC2 0
  (example_1a_TCC2-1 nil 3624181697 ("" (subtype-tcc) nil nil)
   (([\|\|] const-decl "Interval" interval "interval_arith/")
    (|##| const-decl "bool" interval "interval_arith/")
    (/= const-decl "boolean" notequal nil))
   nil))
(example_1a 0
  (example_1a-1 nil 3624181697 ("" (sturm) nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (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/")
    (Interval type-eq-decl nil interval "interval_arith/")
    ([\|\|] const-decl "Interval" interval "interval_arith/")
    (|##| const-decl "bool" interval "interval_arith/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (contains? const-decl "bool" RealInt "reals/")
    (polylist_sum formula-decl nil polylist "Sturm/")
    (polylist_minus formula-decl nil polylist "Sturm/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_monom formula-decl nil polylist "Sturm/")
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (polylist_sat_rational const-decl "bool" polylist "Sturm/")
    (stu__1 skolem-const-decl "{pql: Polylist |
         FORALL (x):
           polylist(pql)(x) =
            polylist(pconst(1))(x) +
             polylist(pminus(pmonom(1, 120), pmonom(2, 60)))(x)}"
            sturm_tarski_examples nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (polylist_sat_rational_def formula-decl nil polylist "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_list "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (polylist const-decl "real" polylist "Sturm/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (length def-decl "nat" list_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/"))
   shostak))
(example_1b 0
  (example_1b-1 nil 3624181697 ("" (sturm) 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)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (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/")
    (Interval type-eq-decl nil interval "interval_arith/")
    ([\|\|] const-decl "Interval" interval "interval_arith/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (|##| const-decl "bool" interval "interval_arith/")
    (polylist_monom formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (polylist_minus formula-decl nil polylist "Sturm/")
    (polylist_sum formula-decl nil polylist "Sturm/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (contains? const-decl "bool" RealInt "reals/")
    (FALSE const-decl "bool" booleans nil)
    (polylist_sat_rational const-decl "bool" polylist "Sturm/")
    (stu__4 skolem-const-decl "{pql: Polylist |
         FORALL (x):
           polylist(pql)(x) =
            polylist(pconst(1))(x) +
             polylist(pminus(pmonom(1, 120), pmonom(2, 60)))(x)}"
            sturm_tarski_examples nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (polylist_sat_rational_def formula-decl nil polylist "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_list "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (polylist const-decl "real" polylist "Sturm/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (length def-decl "nat" list_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/"))
   shostak))
(example_2a_TCC1 0
  (example_2a_TCC1-1 nil 3624181697 ("" (subtype-tcc) nil nil)
   ((- const-decl "nInf" RealInt "reals/")
    ([\|\|] const-decl "RealInt" RealInt "reals/")
    (contains? const-decl "bool" RealInt "reals/")
    (|##| const-decl "bool" RealInt "reals/")
    (/= const-decl "boolean" notequal nil))
   nil))
(example_2a_TCC2 0
  (example_2a_TCC2-1 nil 3624181697 ("" (subtype-tcc) nil nil)
   ((- const-decl "nInf" RealInt "reals/")
    ([\|\|] const-decl "RealInt" RealInt "reals/")
    (contains? const-decl "bool" RealInt "reals/")
    (|##| const-decl "bool" RealInt "reals/")
    (/= const-decl "boolean" notequal nil))
   nil))
(example_2a 0
  (example_2a-1 nil 3624181697 ("" (sturm) 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_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (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/")
    (open? adt-recognizer-decl "[RealInf -> boolean]" RealInt "reals/")
    (open adt-constructor-decl "[real -> (open?)]" RealInt "reals/")
    (polylist_monom formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (polylist_minus formula-decl nil polylist "Sturm/")
    (polylist_sum formula-decl nil polylist "Sturm/")
    (contains? const-decl "bool" RealInt "reals/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (|##| const-decl "bool" RealInt "reals/")
    (polylist_sat_rational const-decl "bool" polylist "Sturm/")
    (stu__7 skolem-const-decl "{pql: Polylist |
         FORALL (x):
           polylist(pql)(x) =
            polylist(pconst(1/9))(x) +
             polylist(pminus(pmonom(1, 120), pmonom(2/3, 60)))(x)}"
            sturm_tarski_examples nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (polylist_sat_rational_def formula-decl nil polylist "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_list "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (polylist const-decl "real" polylist "Sturm/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (length def-decl "nat" list_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (pconst const-decl "Polylist" polylist "Sturm/")
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil))
   shostak))
(example_2b 0
  (example_2b-1 nil 3624181697 ("" (sturm) 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_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (RealInf type-decl nil RealInt "reals/")
    ([\|\|] const-decl "RealInt" RealInt "reals/")
    (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/")
    (open? adt-recognizer-decl "[RealInf -> boolean]" RealInt "reals/")
    (open adt-constructor-decl "[real -> (open?)]" RealInt "reals/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (polylist_sum formula-decl nil polylist "Sturm/")
    (polylist_minus formula-decl nil polylist "Sturm/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_monom formula-decl nil polylist "Sturm/")
    (|##| const-decl "bool" RealInt "reals/")
    (contains? const-decl "bool" RealInt "reals/")
    (polylist_sat_rational const-decl "bool" polylist "Sturm/")
    (stu__10 skolem-const-decl "{pql: Polylist |
         FORALL (x):
           polylist(pql)(x) =
            polylist(pconst(1/9))(x) +
             polylist(pminus(pmonom(1, 120), pmonom(2/3, 60)))(x)}"
             sturm_tarski_examples nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (polylist_sat_rational_def formula-decl nil polylist "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_list "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (polylist const-decl "real" polylist "Sturm/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (length def-decl "nat" list_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (pconst const-decl "Polylist" polylist "Sturm/")
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil))
   shostak))
(legendre_2_TCC1 0
  (legendre_2_TCC1-1 nil 3624181697 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(legendre_3_TCC1 0
  (legendre_3_TCC1-1 nil 3624181697 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(legendre_4_TCC1 0
  (legendre_4_TCC1-1 nil 3624181697 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(legendre_5_TCC1 0
  (legendre_5_TCC1-1 nil 3624181697 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(legendre_6_TCC1 0
  (legendre_6_TCC1-1 nil 3624181697 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(legendre_8_TCC1 0
  (legendre_8_TCC1-1 nil 3624181697 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(legendre_9_TCC1 0
  (legendre_9_TCC1-1 nil 3624181697 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(legendre_9_TCC2 0
  (legendre_9_TCC2-1 nil 3624181697 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(legendre_10_TCC1 0
  (legendre_10_TCC1-1 nil 3624181697 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(Turan_9_TCC1 0
  (Turan_9_TCC1-1 nil 3624181697 ("" (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))
(Turan_9 0
  (Turan_9-1 nil 3624181697 ("" (sturm) nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_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)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (contains? const-decl "bool" RealInt "reals/")
    (expt_x1 formula-decl nil exponentiation nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_sum formula-decl nil polylist "Sturm/")
    (polylist_pow formula-decl nil polylist "Sturm/")
    (polylist_div formula-decl nil polylist "Sturm/")
    (polylist_prod formula-decl nil polylist "Sturm/")
    (polylist_minus formula-decl nil polylist "Sturm/")
    (abs_lt formula-decl nil abs_lems "reals/")
    (polylist_sat_rational const-decl "bool" polylist "Sturm/")
    (stu__13 skolem-const-decl "Polylist" sturm_tarski_examples nil)
    (polylist_sat_rational_def formula-decl nil polylist "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_list "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (ppow def-decl "Polylist" polylist "Sturm/")
    (/= const-decl "boolean" notequal nil)
    (nzrat nonempty-type-eq-decl nil rationals nil)
    (pdiv const-decl "Polylist" polylist "Sturm/")
    (polylist const-decl "real" polylist "Sturm/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/")
    (length def-decl "nat" list_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (pprod const-decl "Polylist" polylist "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/"))
   shostak))
(Legendre_10_TCC1 0
  (Legendre_10_TCC1-1 nil 3624181697 ("" (subtype-tcc) nil nil)
   (([\|\|] const-decl "Interval" interval "interval_arith/")
    (|##| const-decl "bool" interval "interval_arith/")
    (/= const-decl "boolean" notequal nil))
   nil))
(Legendre_10_TCC2 0
  (Legendre_10_TCC2-1 nil 3624181697 ("" (subtype-tcc) nil nil)
   (([\|\|] const-decl "Interval" interval "interval_arith/")
    (|##| const-decl "bool" interval "interval_arith/")
    (/= const-decl "boolean" notequal nil))
   nil))
(Legendre_10_TCC3 0
  (Legendre_10_TCC3-1 nil 3624181697 ("" (subtype-tcc) nil nil)
   (([\|\|] const-decl "Interval" interval "interval_arith/")
    (|##| const-decl "bool" interval "interval_arith/")
    (/= const-decl "boolean" notequal nil))
   nil))
(Legendre_10_TCC4 0
  (Legendre_10_TCC4-1 nil 3624181697 ("" (subtype-tcc) nil nil)
   (([\|\|] const-decl "Interval" interval "interval_arith/")
    (|##| const-decl "bool" interval "interval_arith/")
    (/= const-decl "boolean" notequal nil))
   nil))
(Legendre_10_TCC5 0
  (Legendre_10_TCC5-1 nil 3624181697 ("" (subtype-tcc) nil nil)
   (([\|\|] const-decl "Interval" interval "interval_arith/")
    (|##| const-decl "bool" interval "interval_arith/")
    (/= const-decl "boolean" notequal nil))
   nil))
(Legendre_10 0
  (Legendre_10-1 nil 3624181698 ("" (mono-poly) 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)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields 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)
    (compute_poly_monotonic_def formula-decl nil compute_sturm
     "Sturm/")
    (compute_poly_monotonic const-decl "bool" compute_sturm "Sturm/")
    (Interval type-eq-decl nil interval "interval_arith/")
    ([\|\|] const-decl "Interval" interval "interval_arith/")
    (contains? const-decl "bool" RealInt "reals/")
    (|##| const-decl "bool" interval "interval_arith/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (xval__19 skolem-const-decl "[# bounded_above: bool,
   bounded_below: bool,
   closed_above: bool,
   closed_below: bool,
   lb: nzrat,
   ub: nzrat #]" sturm_tarski_examples nil)
    (lp__20 skolem-const-decl "[nat -> rat]" sturm_tarski_examples nil)
    (pl__18 skolem-const-decl "(cons?[numfield])" sturm_tarski_examples
            nil)
    (polylist_div formula-decl nil polylist "Sturm/")
    (polylist_minus formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_sum formula-decl nil polylist "Sturm/")
    (polylist_monom formula-decl nil polylist "Sturm/")
    (minus_even_is_even application-judgement "even_int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (p1__16 skolem-const-decl "Polylist" sturm_tarski_examples nil)
    (p2__17 skolem-const-decl "Polylist" sturm_tarski_examples nil)
    (polylist_eval formula-decl nil polylist "Sturm/")
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (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__23 skolem-const-decl "RealOrder" sturm_tarski_examples
                nil)
    (rel__22 skolem-const-decl "RealOrder" sturm_tarski_examples nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (deg__21 skolem-const-decl "int" sturm_tarski_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)
    (> 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_div_nzreal_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
    (list2array def-decl "T" array2list "structures/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_list "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/")
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (^ const-decl "real" exponentiation nil)
    (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)
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (pdiv const-decl "Polylist" polylist "Sturm/")
    (nzrat nonempty-type-eq-decl nil rationals nil)
    (/= const-decl "boolean" notequal nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (every adt-def-decl "boolean" list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (list type-decl nil list_adt nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
(Legendre_2_6 0
  (Legendre_2_6-1 nil 3624181698 ("" (tarski) nil)
   ((number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (rational nonempty-type-from-decl nil rationals nil)
    (/= const-decl "boolean" notequal nil)
    (nzrat nonempty-type-eq-decl nil rationals nil)
    (pdiv const-decl "Polylist" polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (polylist const-decl "real" polylist "Sturm/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/")
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (length def-decl "nat" list_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/")
    (null adt-constructor-decl "(null?)" list_adt nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_list "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (compute_solvable_rat_def formula-decl nil poly_system_strategy
     "Tarski/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (> const-decl "bool" reals nil)
    (upto nonempty-type-eq-decl nil naturalnumbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (pl_30 skolem-const-decl "Polylist" sturm_tarski_examples nil)
    (pl_29 skolem-const-decl "Polylist" sturm_tarski_examples nil)
    (pl_28 skolem-const-decl "Polylist" sturm_tarski_examples nil)
    (pl_27 skolem-const-decl "Polylist" sturm_tarski_examples nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (rel5 const-decl "bool" poly_system_strategy "Tarski/")
    (pl_26 skolem-const-decl "Polylist" sturm_tarski_examples nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (polylist_monom formula-decl nil polylist "Sturm/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (polylist_sum formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_minus formula-decl nil polylist "Sturm/")
    (polylist_div formula-decl nil polylist "Sturm/")
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (polylist_eval formula-decl nil polylist "Sturm/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (FALSE const-decl "bool" booleans nil)
    (compute_solvable_rat const-decl "bool" poly_system_strategy
                          "Tarski/")
    (naturalnumber type-eq-decl nil naturalnumbers nil)
    (polyl__36 skolem-const-decl "[nat -> [nat -> rat]]"
     sturm_tarski_examples nil)
    (subrange type-eq-decl nil integers nil)
    (degl__37 skolem-const-decl "[nat -> int]" sturm_tarski_examples
     nil)
    (rell__38 skolem-const-decl "[nat -> even_int]"
              sturm_tarski_examples nil)
    (<= const-decl "bool" reals nil)
    (even? const-decl "bool" integers nil)
    (even_int nonempty-type-eq-decl nil integers nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (list2array def-decl "T" array2list "structures/")
    (zero_pol const-decl "rat" polylist "Sturm/"))
   shostak))
(conflict?_TCC1 0
  (conflict?_TCC1-1 nil 3624181697 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(yes_conflict 0
  (yes_conflict-1 nil 3624181698 ("" (tarski) nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (polylist const-decl "real" polylist "Sturm/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/")
    (pprod const-decl "Polylist" polylist "Sturm/")
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (length def-decl "nat" list_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_list "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (compute_solvable_rat_def formula-decl nil poly_system_strategy
     "Tarski/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (> const-decl "bool" reals nil)
    (upto nonempty-type-eq-decl nil naturalnumbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (rel5 const-decl "bool" poly_system_strategy "Tarski/")
    (polylist_eval formula-decl nil polylist "Sturm/")
    (pl_43 skolem-const-decl "{pql: Polylist |
         FORALL (x):
           polylist(pql)(x) =
            polylist(pconst(305))(x) +
             polylist(psum(pconst(144), pprod(pmonom(1, 1), pconst(1/25))))
                     (x)}" sturm_tarski_examples nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (polylist_prod formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_sum formula-decl nil polylist "Sturm/")
    (dot_scal_left formula-decl nil vectors_2D "vectors/")
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (pl_44 skolem-const-decl "Polylist" sturm_tarski_examples nil)
    (polylist_minus formula-decl nil polylist "Sturm/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (pl_45 skolem-const-decl "Polylist" sturm_tarski_examples nil)
    (pl_46 skolem-const-decl "Polylist" sturm_tarski_examples nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (pl_47 skolem-const-decl "{pl: Polylist |
         length(pl) = 2 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 1)}"
           sturm_tarski_examples nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (H const-decl "real" sturm_tarski_examples nil)
    (vz const-decl "real" sturm_tarski_examples nil)
    (sz const-decl "real" sturm_tarski_examples nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (D const-decl "real" sturm_tarski_examples nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (* const-decl "real" vectors_2D "vectors/")
    (- const-decl "Vector" vectors_2D "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (vo const-decl "Vect2" sturm_tarski_examples nil)
    (vi const-decl "Vect2" sturm_tarski_examples nil)
    (* const-decl "Vector" vectors_2D "vectors/")
    (so const-decl "Vect2" sturm_tarski_examples nil)
    (si const-decl "Vect2" sturm_tarski_examples nil)
    (Interval type-eq-decl nil interval "interval_arith/")
    ([\|\|] const-decl "Interval" interval "interval_arith/")
    (abs_lt formula-decl nil abs_lems "reals/")
    (x_59 skolem-const-decl "real" sturm_tarski_examples nil)
    (|##| const-decl "bool" interval "interval_arith/")
    (compute_solvable_rat const-decl "bool" poly_system_strategy
                          "Tarski/")
    (polyl__53 skolem-const-decl "[nat -> [nat -> rat]]"
     sturm_tarski_examples nil)
    (subrange type-eq-decl nil integers nil)
    (degl__54 skolem-const-decl "[nat -> int]" sturm_tarski_examples
     nil)
    (rell__55 skolem-const-decl "[nat -> naturalnumber]"
              sturm_tarski_examples nil)
    (<= const-decl "bool" reals nil)
    (naturalnumber type-eq-decl nil naturalnumbers nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (list2array def-decl "T" array2list "structures/")
    (zero_pol const-decl "rat" polylist "Sturm/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (pminus const-decl "Polylist" polylist "Sturm/"))
   shostak))
(no_conflict_TCC1 0
  (no_conflict_TCC1-1 nil 3624181697 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(no_conflict 0
  (no_conflict-1 nil 3624181698 ("" (tarski) nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (polylist const-decl "real" polylist "Sturm/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/")
    (pprod const-decl "Polylist" polylist "Sturm/")
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (length def-decl "nat" list_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_list "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (compute_solvable_rat_def formula-decl nil poly_system_strategy
     "Tarski/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (> const-decl "bool" reals nil)
    (upto nonempty-type-eq-decl nil naturalnumbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (polylist_eval formula-decl nil polylist "Sturm/")
    (polylist_sum formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_prod formula-decl nil polylist "Sturm/")
    (polylist_monom formula-decl nil polylist "Sturm/")
    (expt_x1 formula-decl nil exponentiation nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (pl_60 skolem-const-decl "{pql: Polylist |
         FORALL (x):
           polylist(pql)(x) =
            polylist(pconst(305))(x) +
             polylist(psum(pconst(144), pprod(pmonom(1, 1), pconst(1/25))))
                     (x)}" sturm_tarski_examples nil)
    (rel5 const-decl "bool" poly_system_strategy "Tarski/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (polylist_minus formula-decl nil polylist "Sturm/")
    (pl_61 skolem-const-decl "Polylist" sturm_tarski_examples nil)
    (pl_62 skolem-const-decl "Polylist" sturm_tarski_examples nil)
    (pl_63 skolem-const-decl "Polylist" sturm_tarski_examples nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (pl_64 skolem-const-decl "{pl: Polylist |
         length(pl) = 2 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 1)}"
           sturm_tarski_examples nil)
    (abs_lt formula-decl nil abs_lems "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_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (si const-decl "Vect2" sturm_tarski_examples nil)
    (so const-decl "Vect2" sturm_tarski_examples nil)
    (* const-decl "Vector" vectors_2D "vectors/")
    (vi const-decl "Vect2" sturm_tarski_examples nil)
    (vo const-decl "Vect2" sturm_tarski_examples nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (- const-decl "Vector" vectors_2D "vectors/")
    (* const-decl "real" vectors_2D "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (D const-decl "real" sturm_tarski_examples nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sz const-decl "real" sturm_tarski_examples nil)
    (vz const-decl "real" sturm_tarski_examples nil)
    (H const-decl "real" sturm_tarski_examples nil)
    (Interval type-eq-decl nil interval "interval_arith/")
    (|##| const-decl "bool" interval "interval_arith/")
    ([\|\|] const-decl "Interval" interval "interval_arith/")
    (FALSE const-decl "bool" booleans nil)
    (compute_solvable_rat const-decl "bool" poly_system_strategy
                          "Tarski/")
    (polyl__70 skolem-const-decl "[nat -> [nat -> rat]]"
     sturm_tarski_examples nil)
    (subrange type-eq-decl nil integers nil)
    (degl__71 skolem-const-decl "[nat -> int]" sturm_tarski_examples
     nil)
    (rell__72 skolem-const-decl "[nat -> naturalnumber]"
              sturm_tarski_examples nil)
    (<= const-decl "bool" reals nil)
    (naturalnumber type-eq-decl nil naturalnumbers nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (list2array def-decl "T" array2list "structures/")
    (zero_pol const-decl "rat" polylist "Sturm/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (pminus const-decl "Polylist" polylist "Sturm/"))
   shostak)))

quality100%

¤ Dauer der Verarbeitung: 0.27 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.