Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 

products/Sources/formale Sprachen/PVS/Bernstein/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 73 kB image not shown  

Quelle  benchmarks.prf   Sprache: Lisp

 
(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

--> --------------------

100%


¤ Dauer der Verarbeitung: 0.35 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.





                                                                                                                                                                                                                                                                                                                                                                                                     

Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder
Jenseits des Üblichen ....

Besucherstatistik

Besucherstatistik

Monitoring

Montastic status badge