|
(tarski_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_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
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_15 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_14 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_13 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)
(compute_solvable_rat const-decl "bool" poly_system_strategy nil)
(polyl__19 skolem-const-decl "[nat -> [nat -> rat]]" examples nil)
(subrange type-eq-decl nil integers nil)
(degl__20 skolem-const-decl "[nat -> int]" examples nil)
(rell__21 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_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)
(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__32 skolem-const-decl "[nat -> even_int]" examples nil)
(degl__31 skolem-const-decl "[nat -> int]" examples nil)
(subrange type-eq-decl nil integers nil)
(polyl__30 skolem-const-decl "[nat -> [nat -> rat]]" examples nil)
(naturalnumber type-eq-decl nil naturalnumbers nil)
(compute_solvable_rat const-decl "bool" poly_system_strategy nil)
(pl_27 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_26 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)
(compute_solvable_rat_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_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
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_37 skolem-const-decl "Polylist" examples nil)
(rel5 const-decl "bool" poly_system_strategy nil)
(polylist_sum formula-decl nil polylist "Sturm/")
(pl_38 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_39 skolem-const-decl "Polylist" examples nil)
(pl_40 skolem-const-decl "Polylist" examples nil)
(pl_41 skolem-const-decl "Polylist" examples nil)
(FALSE const-decl "bool" booleans nil)
(compute_solvable_rat const-decl "bool" poly_system_strategy nil)
(polyl__47 skolem-const-decl "[nat -> [nat -> rat]]" examples nil)
(subrange type-eq-decl nil integers nil)
(degl__48 skolem-const-decl "[nat -> int]" examples nil)
(rell__49 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_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)
(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__66 skolem-const-decl "[nat -> naturalnumber]" examples nil)
(degl__65 skolem-const-decl "[nat -> int]" examples nil)
(subrange type-eq-decl nil integers nil)
(polyl__64 skolem-const-decl "[nat -> [nat -> rat]]" examples nil)
(compute_solvable_rat 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_56 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_57 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_58 skolem-const-decl "Polylist" examples nil)
(pl_59 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)
(compute_solvable_rat_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_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
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_71 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_72 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_73 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_74 skolem-const-decl "Polylist" examples nil)
(pl_75 skolem-const-decl "Polylist" examples nil)
(compute_solvable_rat const-decl "bool" poly_system_strategy nil)
(polyl__81 skolem-const-decl "[nat -> [nat -> rat]]" examples nil)
(subrange type-eq-decl nil integers nil)
(degl__82 skolem-const-decl "[nat -> int]" examples nil)
(rell__83 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_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_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__98 skolem-const-decl "[nat -> naturalnumber]" examples nil)
(degl__97 skolem-const-decl "[nat -> int]" examples nil)
(subrange type-eq-decl nil integers nil)
(polyl__96 skolem-const-decl "[nat -> [nat -> rat]]" examples nil)
(compute_solvable_rat const-decl "bool" poly_system_strategy nil)
(pl_91 skolem-const-decl "Polylist" examples nil)
(minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
(expt_x1 formula-decl nil exponentiation nil)
(pl_90 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_89 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_88 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)
(compute_solvable_rat_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_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
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_103 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_104 skolem-const-decl "Polylist" examples nil)
(pl_105 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)
(compute_solvable_rat const-decl "bool" poly_system_strategy nil)
(polyl__109 skolem-const-decl "[nat -> [nat -> rat]]" examples nil)
(subrange type-eq-decl nil integers nil)
(degl__110 skolem-const-decl "[nat -> int]" examples nil)
(rell__111 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)))
¤ Dauer der Verarbeitung: 0.16 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.
|
