|
(benchmarks
(Heart_TCC1 0
(Heart_TCC1-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Heart_TCC2 0
(Heart_TCC2-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Heart_forall__TCC1 0
(Heart_forall__TCC1-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil))
nil))
(Heart_forall__TCC2 0
(Heart_forall__TCC2-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil))
nil))
(Heart_forall__TCC3 0
(Heart_forall__TCC3-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil))
nil))
(Heart_forall__TCC4 0
(Heart_forall__TCC4-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil))
nil))
(Heart_forall__TCC5 0
(Heart_forall__TCC5-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil))
nil))
(Heart_forall__TCC6 0
(Heart_forall__TCC6-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil))
nil))
(Heart_forall_ 0
(Heart_forall_-1 nil 3517578450
("" (skeep)
(("" (minmax (! 1 l) :precision "0.01" :equiv? nil)
(("1" (postpone) nil nil) ("2" (postpone) nil nil)) nil))
nil)
((FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans 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)
(/= const-decl "boolean" notequal nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(MVars type-eq-decl nil strat_util nil)
(Vars type-eq-decl nil util nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IntervalEndpoints type-eq-decl nil util nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(ge_realorder name-judgement "RealOrder" util nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Coeff type-eq-decl nil util nil)
(DegreeMono type-eq-decl nil util nil)
(MultiPolynomial type-eq-decl nil util nil)
(RealOrder type-eq-decl nil util nil)
(MPolyRel type-eq-decl nil strat_util nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(multipoly_strategy_true formula-decl nil strategy nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(boxbetween? const-decl "bool" util nil)
(lt_realorder name-judgement "RealOrder" util nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(interval_between? const-decl "bool" util nil)
(multipoly_eval const-decl "real" multi_polynomial nil)
(polyproduct_eval const-decl "real" multi_polynomial nil) nil nil
(polynomial const-decl "[real -> real]" polynomials "reals/")
(expt_x1 formula-decl nil exponentiation nil)
(le_realorder name-judgement "RealOrder" util nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
nil nil (product def-decl "real" product "reals/")
(sigma def-decl "real" sigma "reals/") nil nil
(forall_X_poly_interval const-decl "bool" multi_polynomial nil)
(Outcome type-decl nil Outcome_adt nil)
(Polynomial type-eq-decl nil util nil)
(Polyproduct type-eq-decl nil util nil)
(MultiBernstein type-eq-decl nil util nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(VarSelector type-eq-decl nil vardirselector nil)
(multipoly_strategy const-decl "Outcome" strategy nil)
(MaxVarMinDir const-decl "[bool, nat]" vardirselector nil)
(istrue? adt-recognizer-decl "[Outcome -> boolean]" Outcome_adt
nil)
(IsTrue adt-constructor-decl "(istrue?)" Outcome_adt nil))
shostak))
(Heart_exists_ 0
(Heart_exists_-1 nil 3517578450 ("" (bernstein) nil nil)
((FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans 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)
(/= const-decl "boolean" notequal nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(MVars type-eq-decl nil strat_util nil)
(Vars type-eq-decl nil util nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IntervalEndpoints type-eq-decl nil util nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(gt_realorder name-judgement "RealOrder" util nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Coeff type-eq-decl nil util nil)
(DegreeMono type-eq-decl nil util nil)
(MultiPolynomial type-eq-decl nil util nil)
(RealOrder type-eq-decl nil util nil)
(MPolyRel type-eq-decl nil strat_util nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(> const-decl "bool" reals nil)
(list2array const-decl "T" array2list "structures/")
(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)
(Counterexample adt-constructor-decl "[(cons?) -> (isfalse?)]"
Outcome_adt nil)
(isfalse? adt-recognizer-decl "[Outcome -> boolean]" Outcome_adt
nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(MaxVarMinDir const-decl "[bool, nat]" vardirselector nil)
(multipoly_strategy const-decl "Outcome" strategy nil)
(VarSelector type-eq-decl nil vardirselector nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(MultiBernstein type-eq-decl nil util nil)
(Polyproduct type-eq-decl nil util nil)
(Polynomial type-eq-decl nil util nil)
(Outcome type-decl nil Outcome_adt nil))
shostak))
(Magnetism_forall__TCC1 0
(Magnetism_forall__TCC1-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Magnetism_forall__TCC2 0
(Magnetism_forall__TCC2-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Magnetism_forall__TCC3 0
(Magnetism_forall__TCC3-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Magnetism_forall__TCC4 0
(Magnetism_forall__TCC4-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Magnetism_forall__TCC5 0
(Magnetism_forall__TCC5-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Magnetism_forall__TCC6 0
(Magnetism_forall__TCC6-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Magnetism_forall_ 0
(Magnetism_forall_-1 nil 3517578451 ("" (bernstein) nil nil)
((FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(MVars type-eq-decl nil strat_util nil)
(Vars type-eq-decl nil util nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IntervalEndpoints type-eq-decl nil util nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(MPolyRel type-eq-decl nil strat_util nil)
(RealOrder type-eq-decl nil util nil)
(MultiPolynomial type-eq-decl nil util nil)
(DegreeMono type-eq-decl nil util nil)
(Coeff type-eq-decl nil util nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(multipoly_strategy_true formula-decl nil strategy nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(boxbetween? const-decl "bool" util nil)
(lt_realorder name-judgement "RealOrder" util nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(interval_between? const-decl "bool" util nil)
(multipoly_eval const-decl "real" multi_polynomial nil)
(polyproduct_eval const-decl "real" multi_polynomial nil)
(polynomial const-decl "[real -> real]" polynomials "reals/")
(expt_x1 formula-decl nil exponentiation nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(le_realorder name-judgement "RealOrder" util nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
(product def-decl "real" product "reals/")
(sigma def-decl "real" sigma "reals/")
(forall_X_poly_interval const-decl "bool" multi_polynomial nil)
(Outcome type-decl nil Outcome_adt nil)
(Polynomial type-eq-decl nil util nil)
(Polyproduct type-eq-decl nil util nil)
(MultiBernstein type-eq-decl nil util nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(VarSelector type-eq-decl nil vardirselector nil)
(multipoly_strategy const-decl "Outcome" strategy nil)
(MaxVarMinDir const-decl "[bool, nat]" vardirselector nil)
(istrue? adt-recognizer-decl "[Outcome -> boolean]" Outcome_adt
nil)
(IsTrue adt-constructor-decl "(istrue?)" Outcome_adt nil))
shostak))
(Magnetism_exists_ 0
(Magnetism_exists_-1 nil 3517578451 ("" (bernstein) nil nil)
((FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(MVars type-eq-decl nil strat_util nil)
(Vars type-eq-decl nil util nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IntervalEndpoints type-eq-decl nil util nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(> const-decl "bool" reals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(MPolyRel type-eq-decl nil strat_util nil)
(RealOrder type-eq-decl nil util nil)
(MultiPolynomial type-eq-decl nil util nil)
(DegreeMono type-eq-decl nil util nil)
(Coeff type-eq-decl nil util nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" util nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(list2array const-decl "T" array2list "structures/")
(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)
(Counterexample adt-constructor-decl "[(cons?) -> (isfalse?)]"
Outcome_adt nil)
(isfalse? adt-recognizer-decl "[Outcome -> boolean]" Outcome_adt
nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(MaxVarMinDir const-decl "[bool, nat]" vardirselector nil)
(multipoly_strategy const-decl "Outcome" strategy nil)
(VarSelector type-eq-decl nil vardirselector nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(MultiBernstein type-eq-decl nil util nil)
(Polyproduct type-eq-decl nil util nil)
(Polynomial type-eq-decl nil util nil)
(Outcome type-decl nil Outcome_adt nil))
shostak))
(Butcher_forall__TCC1 0
(Butcher_forall__TCC1-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil))
nil))
(Butcher_forall__TCC2 0
(Butcher_forall__TCC2-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil))
nil))
(Butcher_forall__TCC3 0
(Butcher_forall__TCC3-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil))
nil))
(Butcher_forall__TCC4 0
(Butcher_forall__TCC4-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil))
nil))
(Butcher_forall_ 0
(Butcher_forall_-1 nil 3517578451 ("" (bernstein) nil nil)
((FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(MVars type-eq-decl nil strat_util nil)
(Vars type-eq-decl nil util nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IntervalEndpoints type-eq-decl nil util nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(ge_realorder name-judgement "RealOrder" util nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Coeff type-eq-decl nil util nil)
(DegreeMono type-eq-decl nil util nil)
(MultiPolynomial type-eq-decl nil util nil)
(RealOrder type-eq-decl nil util nil)
(MPolyRel type-eq-decl nil strat_util nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(multipoly_strategy_true formula-decl nil strategy nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(boxbetween? const-decl "bool" util nil)
(lt_realorder name-judgement "RealOrder" util nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(interval_between? const-decl "bool" util nil)
(multipoly_eval const-decl "real" multi_polynomial nil)
(polyproduct_eval const-decl "real" multi_polynomial nil)
(polynomial const-decl "[real -> real]" polynomials "reals/")
(expt_x1 formula-decl nil exponentiation nil)
(le_realorder name-judgement "RealOrder" util nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
(product def-decl "real" product "reals/")
(sigma def-decl "real" sigma "reals/")
(forall_X_poly_interval const-decl "bool" multi_polynomial nil)
(Outcome type-decl nil Outcome_adt nil)
(Polynomial type-eq-decl nil util nil)
(Polyproduct type-eq-decl nil util nil)
(MultiBernstein type-eq-decl nil util nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(VarSelector type-eq-decl nil vardirselector nil)
(multipoly_strategy const-decl "Outcome" strategy nil)
(MaxVarMinDir const-decl "[bool, nat]" vardirselector nil)
(istrue? adt-recognizer-decl "[Outcome -> boolean]" Outcome_adt
nil)
(IsTrue adt-constructor-decl "(istrue?)" Outcome_adt nil))
shostak))
(Butcher_exists_ 0
(Butcher_exists_-1 nil 3517578451 ("" (bernstein) nil nil)
((FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(MVars type-eq-decl nil strat_util nil)
(Vars type-eq-decl nil util nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IntervalEndpoints type-eq-decl nil util nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(gt_realorder name-judgement "RealOrder" util nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Coeff type-eq-decl nil util nil)
(DegreeMono type-eq-decl nil util nil)
(MultiPolynomial type-eq-decl nil util nil)
(RealOrder type-eq-decl nil util nil)
(MPolyRel type-eq-decl nil strat_util nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(> const-decl "bool" reals nil)
(list2array const-decl "T" array2list "structures/")
(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)
(Counterexample adt-constructor-decl "[(cons?) -> (isfalse?)]"
Outcome_adt nil)
(isfalse? adt-recognizer-decl "[Outcome -> boolean]" Outcome_adt
nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(MaxVarMinDir const-decl "[bool, nat]" vardirselector nil)
(multipoly_strategy const-decl "Outcome" strategy nil)
(VarSelector type-eq-decl nil vardirselector nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(MultiBernstein type-eq-decl nil util nil)
(Polyproduct type-eq-decl nil util nil)
(Polynomial type-eq-decl nil util nil)
(Outcome type-decl nil Outcome_adt nil))
shostak))
(Trid_TCC1 0
(Trid_TCC1-1 nil 3506073909 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Trid_forall__TCC1 0
(Trid_forall__TCC1-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Trid_forall__TCC2 0
(Trid_forall__TCC2-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Trid_forall__TCC3 0
(Trid_forall__TCC3-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Trid_forall_ 0
(Trid_forall_-1 nil 3517578451 ("" (bernstein) nil nil)
((FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(MVars type-eq-decl nil strat_util nil)
(Vars type-eq-decl nil util nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IntervalEndpoints type-eq-decl nil util nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(ge_realorder name-judgement "RealOrder" util nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Coeff type-eq-decl nil util nil)
(DegreeMono type-eq-decl nil util nil)
(MultiPolynomial type-eq-decl nil util nil)
(RealOrder type-eq-decl nil util nil)
(MPolyRel type-eq-decl nil strat_util nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(multipoly_strategy_true formula-decl nil strategy nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(boxbetween? const-decl "bool" util nil)
(lt_realorder name-judgement "RealOrder" util nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(interval_between? const-decl "bool" util nil)
(multipoly_eval const-decl "real" multi_polynomial nil)
(polyproduct_eval const-decl "real" multi_polynomial nil)
(polynomial const-decl "[real -> real]" polynomials "reals/")
(expt_x1 formula-decl nil exponentiation nil)
(expt def-decl "real" exponentiation nil)
(^ const-decl "real" exponentiation nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(le_realorder name-judgement "RealOrder" util nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
(product def-decl "real" product "reals/")
(sigma def-decl "real" sigma "reals/")
(forall_X_poly_interval const-decl "bool" multi_polynomial nil)
(Outcome type-decl nil Outcome_adt nil)
(Polynomial type-eq-decl nil util nil)
(Polyproduct type-eq-decl nil util nil)
(MultiBernstein type-eq-decl nil util nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(VarSelector type-eq-decl nil vardirselector nil)
(multipoly_strategy const-decl "Outcome" strategy nil)
(MaxVarMinDir const-decl "[bool, nat]" vardirselector nil)
(istrue? adt-recognizer-decl "[Outcome -> boolean]" Outcome_adt
nil)
(IsTrue adt-constructor-decl "(istrue?)" Outcome_adt nil))
shostak))
(Trid_exists_ 0
(Trid_exists_-1 nil 3517578451 ("" (bernstein) nil nil)
((FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(MVars type-eq-decl nil strat_util nil)
(Vars type-eq-decl nil util nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IntervalEndpoints type-eq-decl nil util nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(ge_realorder name-judgement "RealOrder" util nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Coeff type-eq-decl nil util nil)
(DegreeMono type-eq-decl nil util nil)
(MultiPolynomial type-eq-decl nil util nil)
(RealOrder type-eq-decl nil util nil)
(MPolyRel type-eq-decl nil strat_util nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(list2array const-decl "T" array2list "structures/")
(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)
(Counterexample adt-constructor-decl "[(cons?) -> (isfalse?)]"
Outcome_adt nil)
(isfalse? adt-recognizer-decl "[Outcome -> boolean]" Outcome_adt
nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(MaxVarMinDir const-decl "[bool, nat]" vardirselector nil)
(multipoly_strategy const-decl "Outcome" strategy nil)
(VarSelector type-eq-decl nil vardirselector nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(MultiBernstein type-eq-decl nil util nil)
(Polyproduct type-eq-decl nil util nil)
(Polynomial type-eq-decl nil util nil)
(Outcome type-decl nil Outcome_adt nil))
shostak))
(AdaptiveLV_forall__TCC1 0
(AdaptiveLV_forall__TCC1-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(AdaptiveLV_forall__TCC2 0
(AdaptiveLV_forall__TCC2-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(AdaptiveLV_forall__TCC3 0
(AdaptiveLV_forall__TCC3-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(AdaptiveLV_forall_ 0
(AdaptiveLV_forall_-1 nil 3517578451 ("" (bernstein) nil nil)
((FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(MVars type-eq-decl nil strat_util nil)
(Vars type-eq-decl nil util nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IntervalEndpoints type-eq-decl nil util nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(ge_realorder name-judgement "RealOrder" util nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Coeff type-eq-decl nil util nil)
(DegreeMono type-eq-decl nil util nil)
(MultiPolynomial type-eq-decl nil util nil)
(RealOrder type-eq-decl nil util nil)
(MPolyRel type-eq-decl nil strat_util nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(multipoly_strategy_true formula-decl nil strategy nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(boxbetween? const-decl "bool" util nil)
(lt_realorder name-judgement "RealOrder" util nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(interval_between? const-decl "bool" util nil)
(multipoly_eval const-decl "real" multi_polynomial nil)
(polyproduct_eval const-decl "real" multi_polynomial nil)
(polynomial const-decl "[real -> real]" polynomials "reals/")
(expt_x1 formula-decl nil exponentiation nil)
(le_realorder name-judgement "RealOrder" util nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
(product def-decl "real" product "reals/")
(sigma def-decl "real" sigma "reals/")
(forall_X_poly_interval const-decl "bool" multi_polynomial nil)
(Outcome type-decl nil Outcome_adt nil)
(Polynomial type-eq-decl nil util nil)
(Polyproduct type-eq-decl nil util nil)
(MultiBernstein type-eq-decl nil util nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(VarSelector type-eq-decl nil vardirselector nil)
(multipoly_strategy const-decl "Outcome" strategy nil)
(MaxVarMinDir const-decl "[bool, nat]" vardirselector nil)
(istrue? adt-recognizer-decl "[Outcome -> boolean]" Outcome_adt
nil)
(IsTrue adt-constructor-decl "(istrue?)" Outcome_adt nil))
shostak))
(AdaptiveLV_exists_ 0
(AdaptiveLV_exists_-1 nil 3517578451 ("" (bernstein) nil nil)
((FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(MVars type-eq-decl nil strat_util nil)
(Vars type-eq-decl nil util nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IntervalEndpoints type-eq-decl nil util nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(gt_realorder name-judgement "RealOrder" util nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Coeff type-eq-decl nil util nil)
(DegreeMono type-eq-decl nil util nil)
(MultiPolynomial type-eq-decl nil util nil)
(RealOrder type-eq-decl nil util nil)
(MPolyRel type-eq-decl nil strat_util nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(> const-decl "bool" reals nil)
(list2array const-decl "T" array2list "structures/")
(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)
(Counterexample adt-constructor-decl "[(cons?) -> (isfalse?)]"
Outcome_adt nil)
(isfalse? adt-recognizer-decl "[Outcome -> boolean]" Outcome_adt
nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(MaxVarMinDir const-decl "[bool, nat]" vardirselector nil)
(multipoly_strategy const-decl "Outcome" strategy nil)
(VarSelector type-eq-decl nil vardirselector nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(MultiBernstein type-eq-decl nil util nil)
(Polyproduct type-eq-decl nil util nil)
(Polynomial type-eq-decl nil util nil)
(Outcome type-decl nil Outcome_adt nil))
shostak))
(Caprasse_forall__TCC1 0
(Caprasse_forall__TCC1-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil))
nil))
(Caprasse_forall__TCC2 0
(Caprasse_forall__TCC2-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil))
nil))
(Caprasse_forall__TCC3 0
(Caprasse_forall__TCC3-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil))
nil))
(Caprasse_forall__TCC4 0
(Caprasse_forall__TCC4-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil))
nil))
(Caprasse_forall_ 0
(Caprasse_forall_-1 nil 3517578452 ("" (bernstein) nil nil)
((FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans 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)
(/= const-decl "boolean" notequal nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(MVars type-eq-decl nil strat_util nil)
(Vars type-eq-decl nil util nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IntervalEndpoints type-eq-decl nil util nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(ge_realorder name-judgement "RealOrder" util nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Coeff type-eq-decl nil util nil)
(DegreeMono type-eq-decl nil util nil)
(MultiPolynomial type-eq-decl nil util nil)
(RealOrder type-eq-decl nil util nil)
(MPolyRel type-eq-decl nil strat_util nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(multipoly_strategy_true formula-decl nil strategy nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(boxbetween? const-decl "bool" util nil)
(lt_realorder name-judgement "RealOrder" util nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(interval_between? const-decl "bool" util nil)
(multipoly_eval const-decl "real" multi_polynomial nil)
(polyproduct_eval const-decl "real" multi_polynomial nil)
(polynomial const-decl "[real -> real]" polynomials "reals/")
(expt_x1 formula-decl nil exponentiation nil)
(le_realorder name-judgement "RealOrder" util nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
(product def-decl "real" product "reals/")
(sigma def-decl "real" sigma "reals/")
(forall_X_poly_interval const-decl "bool" multi_polynomial nil)
(Outcome type-decl nil Outcome_adt nil)
(Polynomial type-eq-decl nil util nil)
(Polyproduct type-eq-decl nil util nil)
(MultiBernstein type-eq-decl nil util nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(VarSelector type-eq-decl nil vardirselector nil)
(multipoly_strategy const-decl "Outcome" strategy nil)
(MaxVarMinDir const-decl "[bool, nat]" vardirselector nil)
(istrue? adt-recognizer-decl "[Outcome -> boolean]" Outcome_adt
nil)
(IsTrue adt-constructor-decl "(istrue?)" Outcome_adt nil))
shostak))
(Caprasse_exists__TCC1 0
(Caprasse_exists__TCC1-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Caprasse_exists__TCC2 0
(Caprasse_exists__TCC2-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Caprasse_exists_ 0
(Caprasse_exists_-1 nil 3517578452 ("" (bernstein) nil nil)
((FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(MVars type-eq-decl nil strat_util nil)
(Vars type-eq-decl nil util nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IntervalEndpoints type-eq-decl nil util nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(gt_realorder name-judgement "RealOrder" util nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Coeff type-eq-decl nil util nil)
(DegreeMono type-eq-decl nil util nil)
(MultiPolynomial type-eq-decl nil util nil)
(RealOrder type-eq-decl nil util nil)
(MPolyRel type-eq-decl nil strat_util nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(> const-decl "bool" reals nil)
(list2array const-decl "T" array2list "structures/")
(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)
(Counterexample adt-constructor-decl "[(cons?) -> (isfalse?)]"
Outcome_adt nil)
(isfalse? adt-recognizer-decl "[Outcome -> boolean]" Outcome_adt
nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(MaxVarMinDir const-decl "[bool, nat]" vardirselector nil)
(multipoly_strategy const-decl "Outcome" strategy nil)
(VarSelector type-eq-decl nil vardirselector nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(MultiBernstein type-eq-decl nil util nil)
(Polyproduct type-eq-decl nil util nil)
(Polynomial type-eq-decl nil util nil)
(Outcome type-decl nil Outcome_adt nil))
shostak))
(Schwefel_TCC1 0
(Schwefel_TCC1-1 nil 3506074742 ("" (subtype-tcc) nil nil)
((^ const-decl "real" exponentiation nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil))
nil))
(Schwefel_forall__TCC1 0
(Schwefel_forall__TCC1-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Schwefel_forall__TCC2 0
(Schwefel_forall__TCC2-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Schwefel_forall__TCC3 0
(Schwefel_forall__TCC3-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Schwefel_forall__TCC4 0
(Schwefel_forall__TCC4-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((^ const-decl "real" exponentiation nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil))
nil))
(Schwefel_forall__TCC5 0
(Schwefel_forall__TCC5-1 nil 3517578450 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Schwefel_forall_ 0
(Schwefel_forall_-1 nil 3517578452 ("" (bernstein) nil nil)
((FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(MVars type-eq-decl nil strat_util nil)
(Vars type-eq-decl nil util nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IntervalEndpoints type-eq-decl nil util nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(ge_realorder name-judgement "RealOrder" util nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Coeff type-eq-decl nil util nil)
(DegreeMono type-eq-decl nil util nil)
(MultiPolynomial type-eq-decl nil util nil)
(RealOrder type-eq-decl nil util nil)
(MPolyRel type-eq-decl nil strat_util nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(multipoly_strategy_true formula-decl nil strategy nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(boxbetween? const-decl "bool" util nil)
(lt_realorder name-judgement "RealOrder" util nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(interval_between? const-decl "bool" util nil)
(multipoly_eval const-decl "real" multi_polynomial nil)
(polyproduct_eval const-decl "real" multi_polynomial nil)
(polynomial const-decl "[real -> real]" polynomials "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(expt_x1 formula-decl nil exponentiation nil)
(expt def-decl "real" exponentiation nil)
(^ const-decl "real" exponentiation nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(le_realorder name-judgement "RealOrder" util nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(product def-decl "real" product "reals/")
(sigma def-decl "real" sigma "reals/")
(forall_X_poly_interval const-decl "bool" multi_polynomial nil)
(Outcome type-decl nil Outcome_adt nil)
(Polynomial type-eq-decl nil util nil)
(Polyproduct type-eq-decl nil util nil)
(MultiBernstein type-eq-decl nil util nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(VarSelector type-eq-decl nil vardirselector nil)
(multipoly_strategy const-decl "Outcome" strategy nil)
(MaxVarMinDir const-decl "[bool, nat]" vardirselector nil)
(istrue? adt-recognizer-decl "[Outcome -> boolean]" Outcome_adt
nil)
(IsTrue adt-constructor-decl "(istrue?)" Outcome_adt nil))
shostak))
(Schwefel_exists_ 0
(Schwefel_exists_-1 nil 3517578452 ("" (bernstein) nil nil)
((FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(MVars type-eq-decl nil strat_util nil)
(Vars type-eq-decl nil util nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IntervalEndpoints type-eq-decl nil util nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(> const-decl "bool" reals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(MPolyRel type-eq-decl nil strat_util nil)
(RealOrder type-eq-decl nil util nil)
(MultiPolynomial type-eq-decl nil util nil)
(DegreeMono type-eq-decl nil util nil)
(Coeff type-eq-decl nil util nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" util nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(list2array const-decl "T" array2list "structures/")
(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)
(Counterexample adt-constructor-decl "[(cons?) -> (isfalse?)]"
Outcome_adt nil)
(isfalse? adt-recognizer-decl "[Outcome -> boolean]" Outcome_adt
nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(MaxVarMinDir const-decl "[bool, nat]" vardirselector nil)
(multipoly_strategy const-decl "Outcome" strategy nil)
(VarSelector type-eq-decl nil vardirselector nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(MultiBernstein type-eq-decl nil util nil)
(Polyproduct type-eq-decl nil util nil)
(Polynomial type-eq-decl nil util nil)
(Outcome type-decl nil Outcome_adt nil))
shostak))
(ReactionDiffusion_forall_ 0
(ReactionDiffusion_forall_-1 nil 3517578452 ("" (bernstein) nil nil)
((FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(MVars type-eq-decl nil strat_util nil)
(Vars type-eq-decl nil util nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IntervalEndpoints type-eq-decl nil util nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(ge_realorder name-judgement "RealOrder" util nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Coeff type-eq-decl nil util nil)
(DegreeMono type-eq-decl nil util nil)
(MultiPolynomial type-eq-decl nil util nil)
(RealOrder type-eq-decl nil util nil)
(MPolyRel type-eq-decl nil strat_util nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(multipoly_strategy_true formula-decl nil strategy nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(boxbetween? const-decl "bool" util nil)
(lt_realorder name-judgement "RealOrder" util nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(interval_between? const-decl "bool" util nil)
(multipoly_eval const-decl "real" multi_polynomial nil)
(polyproduct_eval const-decl "real" multi_polynomial nil)
(polynomial const-decl "[real -> real]" polynomials "reals/")
(expt_x1 formula-decl nil exponentiation nil)
(expt def-decl "real" exponentiation nil)
(^ const-decl "real" exponentiation nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(le_realorder name-judgement "RealOrder" util nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
(product def-decl "real" product "reals/")
(sigma def-decl "real" sigma "reals/")
(forall_X_poly_interval const-decl "bool" multi_polynomial nil)
(Outcome type-decl nil Outcome_adt nil)
(Polynomial type-eq-decl nil util nil)
(Polyproduct type-eq-decl nil util nil)
(MultiBernstein type-eq-decl nil util nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(VarSelector type-eq-decl nil vardirselector nil)
(multipoly_strategy const-decl "Outcome" strategy nil)
(MaxVarMinDir const-decl "[bool, nat]" vardirselector nil)
(istrue? adt-recognizer-decl "[Outcome -> boolean]" Outcome_adt
nil)
(IsTrue adt-constructor-decl "(istrue?)" Outcome_adt nil))
shostak))
(ReactionDiffusion_exists_ 0
(ReactionDiffusion_exists_-1 nil 3517578452 ("" (bernstein) nil nil)
((FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-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)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(MVars type-eq-decl nil strat_util nil)
(Vars type-eq-decl nil util nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IntervalEndpoints type-eq-decl nil util nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(> const-decl "bool" reals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(MPolyRel type-eq-decl nil strat_util nil)
(RealOrder type-eq-decl nil util nil)
(MultiPolynomial type-eq-decl nil util nil)
(DegreeMono type-eq-decl nil util nil)
(Coeff type-eq-decl nil util nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" util nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(list2array const-decl "T" array2list "structures/")
(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)
(Counterexample adt-constructor-decl "[(cons?) -> (isfalse?)]"
Outcome_adt nil)
(isfalse? adt-recognizer-decl "[Outcome -> boolean]" Outcome_adt
nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(MaxVarMinDir const-decl "[bool, nat]" vardirselector nil)
(multipoly_strategy const-decl "Outcome" strategy nil)
(VarSelector type-eq-decl nil vardirselector nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.79 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.
|
