| products/sources/formale Sprachen/PVS/Sturm/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: examples.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(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 --> -------------------- ¤ Dauer der Verarbeitung: 0.232 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
