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