Quelle examples.prf Sprache: Lisp

(examples
(example_fall_TCC1 0
  (example_fall_TCC1-1 nil 3622559096 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(example_fall_TCC2 0
  (example_fall_TCC2-1 nil 3623084779 ("" (subtype-tcc) nil nil)
   ((^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
(example_fall 0
  (example_fall-1 nil 3622558914 ("" (tarski) nil nil)
   ((number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (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 "Sturm/")
    (* 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/")
    (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_coeff "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)
    (tarski_def formula-decl nil poly_system_strategy nil)
    (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_3 skolem-const-decl "{pl: Polylist |
         length(pl) = 4 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 3)}"
          examples nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (pl_2 skolem-const-decl "Polylist" examples nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (polylist_prod formula-decl nil polylist "Sturm/")
    (rel5 const-decl "bool" poly_system_strategy nil)
    (pl_1 skolem-const-decl "{pl: Polylist |
         length(pl) = 3 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 2)}"
          examples nil)
    (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_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/")
    (polylist_eval formula-decl nil polylist "Sturm/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (FALSE const-decl "bool" booleans nil)
    (tarski const-decl "bool" poly_system_strategy nil)
    (polyl__7 skolem-const-decl "[nat -> [nat -> rat]]" examples nil)
    (subrange type-eq-decl nil integers nil)
    (degl__8 skolem-const-decl "[nat -> int]" examples nil)
    (rell__9 skolem-const-decl "[nat -> naturalnumber]" 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/")
    (pprod const-decl "Polylist" polylist "Sturm/"))
   shostak))
(example_ex_TCC1 0
  (example_ex_TCC1-1 nil 3623084779 ("" (subtype-tcc) nil nil)
   ((^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil))
   nil))
(example_ex 0
  (example_ex-1 nil 3622670079 ("" (tarski) nil 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)
    (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 "Sturm/")
    (* 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/")
    (null adt-constructor-decl "(null?)" list_adt nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (minus_odd_is_odd application-judgement "odd_int" integers 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_coeff "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)
    (zero_pol const-decl "rat" polylist "Sturm/")
    (list2array def-decl "T" array2list "structures/")
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (even_int nonempty-type-eq-decl nil integers nil)
    (even? const-decl "bool" integers nil)
    (<= const-decl "bool" reals nil)
    (rell__20 skolem-const-decl "[nat -> even_int]" examples nil)
    (degl__19 skolem-const-decl "[nat -> int]" examples nil)
    (subrange type-eq-decl nil integers nil)
    (polyl__18 skolem-const-decl "[nat -> [nat -> rat]]" examples nil)
    (naturalnumber type-eq-decl nil naturalnumbers nil)
    (tarski const-decl "bool" poly_system_strategy nil)
    (pl_15 skolem-const-decl "Polylist" examples nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (polylist_minus formula-decl nil polylist "Sturm/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (expt_x1 formula-decl nil exponentiation nil)
    (pl_14 skolem-const-decl "Polylist" examples nil)
    (polylist_eval formula-decl nil polylist "Sturm/")
    (rel5 const-decl "bool" poly_system_strategy nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (upto nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (tarski_def formula-decl nil poly_system_strategy nil))
   shostak))
(example_1_TCC1 0
  (example_1_TCC1-1 nil 3622740489 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(example_1_TCC2 0
  (example_1_TCC2-1 nil 3622740489 ("" (subtype-tcc) nil nil)
   ((^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil))
   nil))
(example_1_TCC3 0
  (example_1_TCC3-1 nil 3622740489 ("" (subtype-tcc) nil nil)
   ((^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil))
   nil))
(example_1_TCC4 0
  (example_1_TCC4-1 nil 3622740489 ("" (subtype-tcc) nil nil)
   ((minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (^ const-decl "real" exponentiation nil))
   nil))
(example_1_TCC5 0
  (example_1_TCC5-1 nil 3623084779 ("" (subtype-tcc) nil nil)
   ((minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (^ const-decl "real" exponentiation nil))
   nil))
(example_1 0
  (example_1-1 nil 3622740492 ("" (tarski) nil 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/")
    (pprod const-decl "Polylist" polylist "Sturm/")
    (pneg 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/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (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 "Sturm/")
    (* 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/")
    (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)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (minus_odd_is_odd application-judgement "odd_int" integers 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_coeff "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)
    (tarski_def formula-decl nil poly_system_strategy nil)
    (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)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (polylist_eval formula-decl nil polylist "Sturm/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (polylist_prod formula-decl nil polylist "Sturm/")
    (polylist_pow formula-decl nil polylist "Sturm/")
    (polylist_neg formula-decl nil polylist "Sturm/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (polylist_minus formula-decl nil polylist "Sturm/")
    (polylist_const 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)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (pl_25 skolem-const-decl "Polylist" examples nil)
    (rel5 const-decl "bool" poly_system_strategy nil)
    (polylist_sum formula-decl nil polylist "Sturm/")
    (pl_26 skolem-const-decl "{pql: Polylist |
         FORALL (x):
           polylist(pql)(x) =
            polylist(pconst(1))(x) +
             polylist(pneg(ppow(pminus(pmonom(1, 1), pconst(3)), 2)))(x)}"
           examples nil)
    (pl_27 skolem-const-decl "Polylist" examples nil)
    (pl_28 skolem-const-decl "Polylist" examples nil)
    (pl_29 skolem-const-decl "Polylist" examples nil)
    (FALSE const-decl "bool" booleans nil)
    (tarski const-decl "bool" poly_system_strategy nil)
    (polyl__35 skolem-const-decl "[nat -> [nat -> rat]]" examples nil)
    (subrange type-eq-decl nil integers nil)
    (degl__36 skolem-const-decl "[nat -> int]" examples nil)
    (rell__37 skolem-const-decl "[nat -> naturalnumber]" 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_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/"))
   shostak))
(example_2_TCC1 0
  (example_2_TCC1-1 nil 3622740489 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(example_2_TCC2 0
  (example_2_TCC2-1 nil 3622740489 ("" (subtype-tcc) nil nil)
   ((^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil))
   nil))
(example_2 0
  (example_2-1 nil 3622740608 ("" (tarski) nil nil)
   ((minus_odd_is_odd application-judgement "odd_int" integers nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (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 "Sturm/")
    (* 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/")
    (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_coeff "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)
    (pconst const-decl "Polylist" polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (zero_pol const-decl "rat" polylist "Sturm/")
    (list2array def-decl "T" array2list "structures/")
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (naturalnumber type-eq-decl nil naturalnumbers nil)
    (<= const-decl "bool" reals nil)
    (rell__54 skolem-const-decl "[nat -> naturalnumber]" examples nil)
    (degl__53 skolem-const-decl "[nat -> int]" examples nil)
    (subrange type-eq-decl nil integers nil)
    (polyl__52 skolem-const-decl "[nat -> [nat -> rat]]" examples nil)
    (tarski const-decl "bool" poly_system_strategy nil)
    (FALSE const-decl "bool" booleans nil)
    (polylist_eval formula-decl nil polylist "Sturm/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (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)
    (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)
    (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 "{pl: Polylist |
         length(pl) = 13 AND
          (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 12)}" examples
           nil)
    (rel5 const-decl "bool" poly_system_strategy nil)
    (pl_45 skolem-const-decl "{pl: Polylist |
         length(pl) = 5 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 4)}"
           examples nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (polylist_minus formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (expt_x1 formula-decl nil exponentiation nil)
    (pl_46 skolem-const-decl "Polylist" examples nil)
    (pl_47 skolem-const-decl "Polylist" examples nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (upto nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (tarski_def formula-decl nil poly_system_strategy nil))
   shostak))
(example_3 0
  (example_3-1 nil 3622740584 ("" (tarski) nil nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_minus_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/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (pprod const-decl "Polylist" polylist "Sturm/")
    (pneg 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/")
    (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 "Sturm/")
    (* 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/")
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (minus_odd_is_odd application-judgement "odd_int" integers 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_coeff "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)
    (tarski_def formula-decl nil poly_system_strategy nil)
    (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 nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (polylist_eval formula-decl nil polylist "Sturm/")
    (pl_59 skolem-const-decl "Polylist" examples nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (polylist_neg formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_pow formula-decl nil polylist "Sturm/")
    (polylist_prod formula-decl nil polylist "Sturm/")
    (polylist_minus formula-decl nil polylist "Sturm/")
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (pl_60 skolem-const-decl "{pql: Polylist |
         FORALL (x):
           polylist(pql)(x) =
            polylist(pconst(1))(x) +
             polylist(pneg(ppow(pminus(pmonom(1, 1), pconst(3)), 2)))(x)}"
           examples nil)
    (polylist_sum formula-decl nil polylist "Sturm/")
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (pl_61 skolem-const-decl "Polylist" examples nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (pl_62 skolem-const-decl "Polylist" examples nil)
    (pl_63 skolem-const-decl "Polylist" examples nil)
    (tarski const-decl "bool" poly_system_strategy nil)
    (polyl__69 skolem-const-decl "[nat -> [nat -> rat]]" examples nil)
    (subrange type-eq-decl nil integers nil)
    (degl__70 skolem-const-decl "[nat -> int]" examples nil)
    (rell__71 skolem-const-decl "[nat -> naturalnumber]" 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_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/"))
   shostak))
(example_4_TCC1 0
  (example_4_TCC1-1 nil 3622740489 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(example_4_TCC2 0
  (example_4_TCC2-1 nil 3623084779 ("" (subtype-tcc) nil nil)
   ((^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(example_4_TCC3 0
  (example_4_TCC3-1 nil 3623084779 ("" (subtype-tcc) nil nil)
   ((^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(example_4_TCC4 0
  (example_4_TCC4-1 nil 3623084779 ("" (subtype-tcc) nil nil)
   ((^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(example_4_TCC5 0
  (example_4_TCC5-1 nil 3623084779 ("" (subtype-tcc) nil nil)
   ((^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(example_4_TCC6 0
  (example_4_TCC6-1 nil 3623084779 ("" (subtype-tcc) nil nil)
   ((^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(example_4_TCC7 0
  (example_4_TCC7-1 nil 3623084779 ("" (subtype-tcc) nil nil)
   ((^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(example_4_TCC8 0
  (example_4_TCC8-1 nil 3623084779 ("" (subtype-tcc) nil nil)
   ((^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(example_4_TCC9 0
  (example_4_TCC9-1 nil 3623084779 ("" (subtype-tcc) nil nil)
   ((^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(example_4_TCC10 0
  (example_4_TCC10-1 nil 3623084779 ("" (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 "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil))
   nil))
(example_4_TCC11 0
  (example_4_TCC11-1 nil 3623084779 ("" (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 "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil))
   nil))
(example_4 0
  (example_4-1 nil 3622740608 ("" (tarski) nil 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)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" 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_coeff "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_even_is_even application-judgement "even_int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (zero_pol const-decl "rat" polylist "Sturm/")
    (list2array def-decl "T" array2list "structures/")
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (naturalnumber type-eq-decl nil naturalnumbers nil)
    (<= const-decl "bool" reals nil)
    (rell__86 skolem-const-decl "[nat -> naturalnumber]" examples nil)
    (degl__85 skolem-const-decl "[nat -> int]" examples nil)
    (subrange type-eq-decl nil integers nil)
    (polyl__84 skolem-const-decl "[nat -> [nat -> rat]]" examples nil)
    (tarski const-decl "bool" poly_system_strategy nil)
    (pl_79 skolem-const-decl "Polylist" examples nil)
    (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (pl_78 skolem-const-decl "Polylist" examples nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (pl_77 skolem-const-decl "Polylist" examples nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (polylist_sum formula-decl nil polylist "Sturm/")
    (polylist_minus formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_monom formula-decl nil polylist "Sturm/")
    (pl_76 skolem-const-decl "{pql: Polylist |
         FORALL (x):
           polylist(pql)(x) =
            polylist(pconst(1948))(x) +
             polylist(pminus(pminus(pmonom(1, 22), pmonom(26/63, 20)),
                             pmonom(419, 10)))
                     (x)}" examples nil)
    (polylist_eval formula-decl nil polylist "Sturm/")
    (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)
    (rel5 const-decl "bool" poly_system_strategy nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (upto nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (tarski_def formula-decl nil poly_system_strategy nil))
   shostak))
(example_5_TCC1 0
  (example_5_TCC1-1 nil 3622740375 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(example_5 0
  (example_5-1 nil 3622740375 ("" (tarski) nil 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/")
    (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/")
    (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_coeff "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)
    (tarski_def formula-decl nil poly_system_strategy nil)
    (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/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (polylist_sum formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (expt_x1 formula-decl nil exponentiation nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (pl_91 skolem-const-decl "{pql: Polylist |
         FORALL (x):
           polylist(pql)(x) =
            polylist(pconst(1))(x) + polylist(pmonom(1, 1))(x)}"
           examples nil)
    (rel5 const-decl "bool" poly_system_strategy nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (polylist_minus formula-decl nil polylist "Sturm/")
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (pl_92 skolem-const-decl "Polylist" examples nil)
    (pl_93 skolem-const-decl "Polylist" examples nil)
    (abs_ge formula-decl nil abs_lems "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (FALSE const-decl "bool" booleans nil)
    (tarski const-decl "bool" poly_system_strategy nil)
    (polyl__97 skolem-const-decl "[nat -> [nat -> rat]]" examples nil)
    (subrange type-eq-decl nil integers nil)
    (degl__98 skolem-const-decl "[nat -> int]" examples nil)
    (rell__99 skolem-const-decl "[nat -> naturalnumber]" examples nil)
    (<= const-decl "bool" reals nil)
    (naturalnumber type-eq-decl nil naturalnumbers nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (list2array def-decl "T" array2list "structures/")
    (zero_pol const-decl "rat" polylist "Sturm/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (pminus const-decl "Polylist" polylist "Sturm/"))
   shostak)))

quality100%

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.