Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 

products/Sources/formale Sprachen/PVS/Sturm/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 7.10.2014 mit Größe 155 kB image not shown  

Quelle  examples.prf   Sprache: 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)
--> --------------------

--> maximum size reached

--> --------------------

100%


¤ Dauer der Verarbeitung: 0.16 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




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.





                                                                                                                                                                                                                                                                                                                                                                                                     

Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder
Jenseits des Üblichen ....

Besucherstatistik

Besucherstatistik

Monitoring

Montastic status badge