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