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

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

Quelle  interval_examples.prf   Sprache: Lisp

 
(interval_examples
 (sqrt23 0
  (sqrt23-1 nil 3600857800 ("" (numerical (! 1 1) :verbose? t) nil nil)
   ((IntervalExpr type-decl nil IntervalExpr_adt "interval_arith/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (RealExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]"
     IntervalExpr_adt "interval_arith/")
    (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]"
     IntervalExpr_adt "interval_arith/")
    (Precondition? const-decl "bool" interval "interval_arith/")
    (FUN adt-constructor-decl
     "[[pre: (Precondition?), opf: [real -> real],
  {F: [Interval -> Interval] |
           Inclusion?(pre, opf)(F) AND Fundamental?(pre)(F)},
  RealExpr] ->
   (fun?)]" IntervalExpr_adt "interval_arith/")
    (r2E const-decl "RealExpr" interval_expr "interval_arith/")
    (Unit type-decl nil Unit_adt "structures/")
    (Includes? const-decl "bool" interval "interval_arith/")
    (unit? adt-recognizer-decl "[Unit -> boolean]" Unit_adt
           "structures/")
    (unit adt-constructor-decl "(unit?)" Unit_adt "structures/")
    (CONST adt-constructor-decl
     "[[opc: [Unit -> real], (Includes?(opc(unit)))] -> (const?)]"
     IntervalExpr_adt "interval_arith/")
    (pi_safe const-decl "[Unit -> real]" interval_expr_trig
             "interval_arith/")
    (Pos? const-decl "bool" interval "interval_arith/")
    (Pi const-decl "(Pos?)" interval_trig "interval_arith/")
    (NonNeg_Precondition name-judgement "(Precondition?)" interval
     "interval_arith/")
    (Sqrt_Fundamental application-judgement "(Fundamental?(NonNeg?))"
     interval_expr_sqrt "interval_arith/")
    (Sqrt_Inclusion application-judgement
     "(Inclusion?(NonNeg?, sqrt_safe))" interval_expr_sqrt
     "interval_arith/")
    (Pi_Inclusion application-judgement "(Includes?(pi_safe(unit)))"
     interval_expr_trig "interval_arith/")
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (Fundamental? const-decl "bool" interval "interval_arith/")
    (Sqrt const-decl "(NonNeg?)" interval_sqrt "interval_arith/")
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (sqrt_safe const-decl "real" interval_expr_sqrt "interval_arith/")
    (NonNeg? const-decl "bool" interval "interval_arith/")
    (Inclusion? const-decl "bool" interval "interval_arith/")
    (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)
    (PRED type-eq-decl nil defined_types nil)
    (Interval type-eq-decl nil interval "interval_arith/")
    (real nonempty-type-from-decl nil reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx "trig_fnd/")
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (numerical_soundness formula-decl nil numerical_bandb
     "interval_arith/")
    (sound? const-decl "bool" numerical_bandb "interval_arith/")
    (listn_0 name-judgement "listn[real](0)" simple_bandb
     "interval_arith/")
    (Env type-eq-decl nil box "interval_arith/")
    (vars_in_box? const-decl "bool" box "interval_arith/")
    (every adt-def-decl "boolean" list_adt nil)
    (list2array def-decl "T" array2list "structures/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (nonneg_rat_max application-judgement
     "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil)
    (int_max application-judgement "{k: int | i <= k AND j <= k}"
     real_defs nil)
    (nat_max application-judgement "{k: nat | i <= k AND j <= k}"
     real_defs nil)
    (nml_49 skolem-const-decl "(sub?)" interval_examples nil)
    (|##| const-decl "bool" interval "interval_arith/")
    ([\|\|] const-decl "Interval" interval "interval_arith/")
    (lb_interval formula-decl nil interval "interval_arith/")
    (ub_interval formula-decl nil interval "interval_arith/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (eval def-decl "real" interval_expr "interval_arith/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnreal type-eq-decl nil real_types nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (pi const-decl "posreal" atan "trig_fnd/")
    (FALSE const-decl "bool" booleans nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (altdir_maxvar const-decl "DirVar" numerical_bandb
                   "interval_arith/")
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numerical const-decl "Output" numerical_bandb "interval_arith/")
    (Output type-eq-decl nil branch_and_bound "structures/")
    (DirVarSelector type-eq-decl nil branch_and_bound "structures/")
    (DirVarStack type-eq-decl nil branch_and_bound "structures/")
    (length def-decl "nat" list_props nil)
    (stack type-eq-decl nil stack "structures/")
    (DirVar type-eq-decl nil branch_and_bound "structures/")
    (ProperBox? const-decl "bool" box "interval_arith/")
    (IntervalMinMax type-eq-decl nil numerical_bandb "interval_arith/")
    (ProperBox type-eq-decl nil box "interval_arith/")
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (Box type-eq-decl nil box "interval_arith/")
    (list type-decl nil list_adt nil))
   shostak))
 (sin6sqrt2 0
  (sin6sqrt2-1 nil 3600857800 ("" (numerical (! 1 1)) nil nil)
   ((IntervalExpr type-decl nil IntervalExpr_adt "interval_arith/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (RealExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]"
     IntervalExpr_adt "interval_arith/")
    (FUN adt-constructor-decl
     "[[pre: (Precondition?), opf: [real -> real],
  {F: [Interval -> Interval] |
           Inclusion?(pre, opf)(F) AND Fundamental?(pre)(F)},
  RealExpr] ->
   (fun?)]" IntervalExpr_adt "interval_arith/")
    (DIV adt-constructor-decl "[[RealExpr, RealExpr] -> (div?)]"
     IntervalExpr_adt "interval_arith/")
    (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]"
     IntervalExpr_adt "interval_arith/")
    (r2E const-decl "RealExpr" interval_expr "interval_arith/")
    (Unit type-decl nil Unit_adt "structures/")
    (Includes? const-decl "bool" interval "interval_arith/")
    (unit? adt-recognizer-decl "[Unit -> boolean]" Unit_adt
           "structures/")
    (unit adt-constructor-decl "(unit?)" Unit_adt "structures/")
    (CONST adt-constructor-decl
     "[[opc: [Unit -> real], (Includes?(opc(unit)))] -> (const?)]"
     IntervalExpr_adt "interval_arith/")
    (pi_safe const-decl "[Unit -> real]" interval_expr_trig
             "interval_arith/")
    (Pos? const-decl "bool" interval "interval_arith/")
    (Pi const-decl "(Pos?)" interval_trig "interval_arith/")
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Sqrt_Inclusion application-judgement
     "(Inclusion?(NonNeg?, sqrt_safe))" interval_expr_sqrt
     "interval_arith/")
    (Sqrt_Fundamental application-judgement "(Fundamental?(NonNeg?))"
     interval_expr_sqrt "interval_arith/")
    (NonNeg_Precondition name-judgement "(Precondition?)" interval
     "interval_arith/")
    (Pi_Inclusion application-judgement "(Includes?(pi_safe(unit)))"
     interval_expr_trig "interval_arith/")
    (Sin_Inclusion application-judgement "(Inclusion?(PreTrue, sin))"
     interval_expr_trig "interval_arith/")
    (Sin_Fundamental application-judgement "(Fundamental?(PreTrue))"
     interval_expr_trig "interval_arith/")
    (Sqrt const-decl "(NonNeg?)" interval_sqrt "interval_arith/")
    (sqrt_safe const-decl "real" interval_expr_sqrt "interval_arith/")
    (NonNeg? const-decl "bool" interval "interval_arith/")
    (Fundamental? const-decl "bool" interval "interval_arith/")
    (Sin const-decl "Interval" interval_trig "interval_arith/")
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (sin const-decl "real" sincos_def "trig_fnd/")
    (PreTrue const-decl "(Precondition?)" interval_expr
             "interval_arith/")
    (Precondition? const-decl "bool" interval "interval_arith/")
    (Inclusion? const-decl "bool" interval "interval_arith/")
    (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)
    (PRED type-eq-decl nil defined_types nil)
    (Interval type-eq-decl nil interval "interval_arith/")
    (real nonempty-type-from-decl nil reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx "trig_fnd/")
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (numerical_soundness formula-decl nil numerical_bandb
     "interval_arith/")
    (sound? const-decl "bool" numerical_bandb "interval_arith/")
    (listn_0 name-judgement "listn[real](0)" simple_bandb
     "interval_arith/")
    (Env type-eq-decl nil box "interval_arith/")
    (vars_in_box? const-decl "bool" box "interval_arith/")
    (every adt-def-decl "boolean" list_adt nil)
    (list2array def-decl "T" array2list "structures/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (nonneg_rat_max application-judgement
     "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil)
    (int_max application-judgement "{k: int | i <= k AND j <= k}"
     real_defs nil)
    (nat_max application-judgement "{k: nat | i <= k AND j <= k}"
     real_defs nil)
    (nml_50 skolem-const-decl "(add?)" interval_examples nil)
    (|##| const-decl "bool" interval "interval_arith/")
    ([\|\|] const-decl "Interval" interval "interval_arith/")
    (lb_interval formula-decl nil interval "interval_arith/")
    (ub_interval formula-decl nil interval "interval_arith/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (eval def-decl "real" interval_expr "interval_arith/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (pi const-decl "posreal" atan "trig_fnd/")
    (nnreal type-eq-decl nil real_types nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (FALSE const-decl "bool" booleans nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (altdir_maxvar const-decl "DirVar" numerical_bandb
                   "interval_arith/")
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numerical const-decl "Output" numerical_bandb "interval_arith/")
    (Output type-eq-decl nil branch_and_bound "structures/")
    (DirVarSelector type-eq-decl nil branch_and_bound "structures/")
    (DirVarStack type-eq-decl nil branch_and_bound "structures/")
    (length def-decl "nat" list_props nil)
    (stack type-eq-decl nil stack "structures/")
    (DirVar type-eq-decl nil branch_and_bound "structures/")
    (ProperBox? const-decl "bool" box "interval_arith/")
    (IntervalMinMax type-eq-decl nil numerical_bandb "interval_arith/")
    (ProperBox type-eq-decl nil box "interval_arith/")
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (Box type-eq-decl nil box "interval_arith/")
    (list type-decl nil list_adt nil))
   shostak))
 (sqrtx3_TCC1 0
  (sqrtx3_TCC1-1 nil 3600857800 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    ([\|\|] const-decl "Interval" interval "interval_arith/")
    (|##| const-decl "bool" interval "interval_arith/"))
   nil))
 (sqrtx3 0
  (sqrtx3-1 nil 3600857800 ("" (interval) nil nil)
   ((listn_0 name-judgement "listn[real](0)" simple_bandb
     "interval_arith/")
    (Maybe type-decl nil Maybe "structures/")
    (list type-decl nil list_adt nil)
    (every adt-def-decl "boolean" list_adt nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (some? adt-recognizer-decl "[Maybe -> boolean]" Maybe
     "structures/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (val adt-accessor-decl "[(some?) -> T]" Maybe "structures/")
    (IntervalOutput type-eq-decl nil interval_bandb "interval_arith/")
    (Box type-eq-decl nil box "interval_arith/")
    (ProperBox? const-decl "bool" box "interval_arith/")
    (ProperBox type-eq-decl nil box "interval_arith/")
    (DirVar type-eq-decl nil branch_and_bound "structures/")
    (stack type-eq-decl nil stack "structures/")
    (length def-decl "nat" list_props nil)
    (DirVarStack type-eq-decl nil branch_and_bound "structures/")
    (DirVarSelector type-eq-decl nil branch_and_bound "structures/")
    (Output type-eq-decl nil branch_and_bound "structures/")
    (interval const-decl "Output" interval_bandb "interval_arith/")
    (alt_max const-decl "DirVar" interval_bandb "interval_arith/")
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (Some adt-constructor-decl "[T -> (some?)]" Maybe "structures/")
    (FALSE const-decl "bool" booleans nil)
    (vars_in_box formula-decl nil box "interval_arith/")
    (length_singleton formula-decl nil more_list_props "structures/")
    (vars_in_box_rec def-decl
     "{b: bool | b = (FORALL (k: subrange(i, n - 1)): vs(k) ## nth(box, k - i))}"
     box "interval_arith/")
    (iar_51 skolem-const-decl "(bimplies?)" interval_examples nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (nonneg_rat_max application-judgement
     "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil)
    (int_max application-judgement "{k: int | i <= k AND j <= k}"
     real_defs nil)
    (nat_max application-judgement "{k: nat | i <= k AND j <= k}"
     real_defs nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (eval def-decl "real" interval_expr "interval_arith/")
    (beval def-decl "bool" interval_bexpr "interval_arith/")
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx "trig_fnd/")
    (x_52 skolem-const-decl "real" interval_examples nil)
    (list2array def-decl "T" array2list "structures/")
    (vars_in_box? const-decl "bool" box "interval_arith/")
    (Env type-eq-decl nil box "interval_arith/")
    (sound? const-decl "bool" interval_bandb "interval_arith/")
    (interval_soundness formula-decl nil interval_bandb
     "interval_arith/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (Fundamental? const-decl "bool" interval "interval_arith/")
    (Sqrt const-decl "(NonNeg?)" interval_sqrt "interval_arith/")
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (sqrt_safe const-decl "real" interval_expr_sqrt "interval_arith/")
    (NonNeg? const-decl "bool" interval "interval_arith/")
    (Inclusion? const-decl "bool" interval "interval_arith/")
    (PRED type-eq-decl nil defined_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (NonNeg_Precondition name-judgement "(Precondition?)" interval
     "interval_arith/")
    (Sqrt_Fundamental application-judgement "(Fundamental?(NonNeg?))"
     interval_expr_sqrt "interval_arith/")
    (Sqrt_Inclusion application-judgement
     "(Inclusion?(NonNeg?, sqrt_safe))" interval_expr_sqrt
     "interval_arith/")
    (Pi_Inclusion application-judgement "(Includes?(pi_safe(unit)))"
     interval_expr_trig "interval_arith/")
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (Pi const-decl "(Pos?)" interval_trig "interval_arith/")
    (Pos? const-decl "bool" interval "interval_arith/")
    (pi_safe const-decl "[Unit -> real]" interval_expr_trig
             "interval_arith/")
    (CONST adt-constructor-decl
     "[[opc: [Unit -> real], (Includes?(opc(unit)))] -> (const?)]"
     IntervalExpr_adt "interval_arith/")
    (unit adt-constructor-decl "(unit?)" Unit_adt "structures/")
    (unit? adt-recognizer-decl "[Unit -> boolean]" Unit_adt
           "structures/")
    (Includes? const-decl "bool" interval "interval_arith/")
    (Unit type-decl nil Unit_adt "structures/")
    (r2E const-decl "RealExpr" interval_expr "interval_arith/")
    (FUN adt-constructor-decl
     "[[pre: (Precondition?), opf: [real -> real],
  {F: [Interval -> Interval] |
           Inclusion?(pre, opf)(F) AND Fundamental?(pre)(F)},
  RealExpr] ->
   (fun?)]" IntervalExpr_adt "interval_arith/")
    (Precondition? const-decl "bool" interval "interval_arith/")
    (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]"
     IntervalExpr_adt "interval_arith/")
    (< const-decl "bool" reals nil)
    (BREL adt-constructor-decl
     "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt
     "interval_arith/")
    (RealOrder type-eq-decl nil real_orders "reals/")
    (realorder? const-decl "bool" real_orders "reals/")
    (X const-decl "RealExpr" interval_expr "interval_arith/")
    (BINCLUDES adt-constructor-decl
     "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt
     "interval_arith/")
    (RealExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (BIMPLIES adt-constructor-decl
     "[[BoolExpr, BoolExpr] -> (bimplies?)]" IntervalExpr_adt
     "interval_arith/")
    (BoolExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bite? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (brel? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bor? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (band? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IntervalExpr type-decl nil IntervalExpr_adt "interval_arith/")
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (Interval type-eq-decl nil interval "interval_arith/")
    (|##| const-decl "bool" interval "interval_arith/")
    ([\|\|] const-decl "Interval" interval "interval_arith/")
    (>= const-decl "bool" reals nil))
   shostak))
 (tr_TCC1 0
  (tr_TCC1-1 nil 3600857800
   ("" (skeep :preds? t) (("" (replaces -6) nil nil)) nil)
   ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx "trig_fnd/")
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
 (tr_250_35_TCC1 0
  (tr_250_35_TCC1-1 nil 3600857800
   ("" (skeep :preds? t)
    (("" (replaces -5)
      (("" (expand "Tan?") (("" (interval -5) nil nil)) nil)) nil))
    nil)
   ((posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (IntervalExpr type-decl nil IntervalExpr_adt "interval_arith/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (band? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bor? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (brel? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bite? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (BoolExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (BAND adt-constructor-decl "[[BoolExpr, BoolExpr] -> (band?)]"
     IntervalExpr_adt "interval_arith/")
    (realorder? const-decl "bool" real_orders "reals/")
    (RealOrder type-eq-decl nil real_orders "reals/")
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (RealExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (BREL adt-constructor-decl
     "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt
     "interval_arith/")
    (<= const-decl "bool" reals nil)
    (FUN adt-constructor-decl
     "[[pre: (Precondition?), opf: [real -> real],
  {F: [Interval -> Interval] |
           Inclusion?(pre, opf)(F) AND Fundamental?(pre)(F)},
  RealExpr] ->
   (fun?)]" IntervalExpr_adt "interval_arith/")
    (DIV adt-constructor-decl "[[RealExpr, RealExpr] -> (div?)]"
     IntervalExpr_adt "interval_arith/")
    (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]"
     IntervalExpr_adt "interval_arith/")
    (r2E const-decl "RealExpr" interval_expr "interval_arith/")
    (Unit type-decl nil Unit_adt "structures/")
    (Includes? const-decl "bool" interval "interval_arith/")
    (unit? adt-recognizer-decl "[Unit -> boolean]" Unit_adt
           "structures/")
    (unit adt-constructor-decl "(unit?)" Unit_adt "structures/")
    (CONST adt-constructor-decl
     "[[opc: [Unit -> real], (Includes?(opc(unit)))] -> (const?)]"
     IntervalExpr_adt "interval_arith/")
    (pi_safe const-decl "[Unit -> real]" interval_expr_trig
             "interval_arith/")
    (Pos? const-decl "bool" interval "interval_arith/")
    (Pi const-decl "(Pos?)" interval_trig "interval_arith/")
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (Pi_Inclusion application-judgement "(Includes?(pi_safe(unit)))"
     interval_expr_trig "interval_arith/")
    (Cos_Inclusion application-judgement "(Inclusion?(PreTrue, cos))"
     interval_expr_trig "interval_arith/")
    (Cos_Fundamental application-judgement "(Fundamental?(PreTrue))"
     interval_expr_trig "interval_arith/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (Fundamental? const-decl "bool" interval "interval_arith/")
    (Cos const-decl "Interval" interval_trig "interval_arith/")
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (cos const-decl "real" sincos_def "trig_fnd/")
    (PreTrue const-decl "(Precondition?)" interval_expr
             "interval_arith/")
    (Precondition? const-decl "bool" interval "interval_arith/")
    (Inclusion? const-decl "bool" interval "interval_arith/")
    (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)
    (PRED type-eq-decl nil defined_types nil)
    (Interval type-eq-decl nil interval "interval_arith/")
    (real nonempty-type-from-decl nil reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx "trig_fnd/")
    (interval_soundness formula-decl nil interval_bandb
     "interval_arith/")
    (sound? const-decl "bool" interval_bandb "interval_arith/")
    (Env type-eq-decl nil box "interval_arith/")
    (vars_in_box? const-decl "bool" box "interval_arith/")
    (list2array def-decl "T" array2list "structures/")
    (beval def-decl "bool" interval_bexpr "interval_arith/")
    (eval def-decl "real" interval_expr "interval_arith/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (iar_53 skolem-const-decl "(band?)" interval_examples nil)
    (Some adt-constructor-decl "[T -> (some?)]" Maybe "structures/")
    (null adt-constructor-decl "(null?)" list_adt nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (BNOT adt-constructor-decl "[BoolExpr -> (bnot?)]" IntervalExpr_adt
     "interval_arith/")
    (alt_max const-decl "DirVar" interval_bandb "interval_arith/")
    (interval const-decl "Output" interval_bandb "interval_arith/")
    (Output type-eq-decl nil branch_and_bound "structures/")
    (DirVarSelector type-eq-decl nil branch_and_bound "structures/")
    (DirVarStack type-eq-decl nil branch_and_bound "structures/")
    (length def-decl "nat" list_props nil)
    (stack type-eq-decl nil stack "structures/")
    (DirVar type-eq-decl nil branch_and_bound "structures/")
    (ProperBox type-eq-decl nil box "interval_arith/")
    (ProperBox? const-decl "bool" box "interval_arith/")
    (Box type-eq-decl nil box "interval_arith/")
    (IntervalOutput type-eq-decl nil interval_bandb "interval_arith/")
    (val adt-accessor-decl "[(some?) -> T]" Maybe "structures/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (some? adt-recognizer-decl "[Maybe -> boolean]" Maybe
     "structures/")
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (every adt-def-decl "boolean" list_adt nil)
    (list type-decl nil list_adt nil)
    (Maybe type-decl nil Maybe "structures/")
    (listn_0 name-judgement "listn[real](0)" simple_bandb
     "interval_arith/")
    (Tan? const-decl "bool" sincos_def "trig_fnd/"))
   nil))
 (tr_250_35 0
  (tr_250_35-1 nil 3600857800 ("" (interval) nil nil)
   ((listn_0 name-judgement "listn[real](0)" simple_bandb
     "interval_arith/")
    (Maybe type-decl nil Maybe "structures/")
    (list type-decl nil list_adt nil)
    (every adt-def-decl "boolean" list_adt nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (some? adt-recognizer-decl "[Maybe -> boolean]" Maybe
     "structures/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (val adt-accessor-decl "[(some?) -> T]" Maybe "structures/")
    (IntervalOutput type-eq-decl nil interval_bandb "interval_arith/")
    (Box type-eq-decl nil box "interval_arith/")
    (ProperBox? const-decl "bool" box "interval_arith/")
    (ProperBox type-eq-decl nil box "interval_arith/")
    (DirVar type-eq-decl nil branch_and_bound "structures/")
    (stack type-eq-decl nil stack "structures/")
    (length def-decl "nat" list_props nil)
    (DirVarStack type-eq-decl nil branch_and_bound "structures/")
    (DirVarSelector type-eq-decl nil branch_and_bound "structures/")
    (Output type-eq-decl nil branch_and_bound "structures/")
    (interval const-decl "Output" interval_bandb "interval_arith/")
    (alt_max const-decl "DirVar" interval_bandb "interval_arith/")
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (Some adt-constructor-decl "[T -> (some?)]" Maybe "structures/")
    (Env type-eq-decl nil box "interval_arith/")
    (vars_in_box? const-decl "bool" box "interval_arith/")
    (list2array def-decl "T" array2list "structures/")
    (beval def-decl "bool" interval_bexpr "interval_arith/")
    (realexpr? const-decl "bool" interval_expr "interval_arith/")
    (eval def-decl "real" interval_expr "interval_arith/")
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (V_0_55 skolem-const-decl "(const?)" interval_examples nil)
    (V_1_56 skolem-const-decl "(letin?)" interval_examples nil)
    (iar_54 skolem-const-decl "(bletin?)" interval_examples nil)
    (g const-decl "posreal" interval_examples nil)
    (sound? const-decl "bool" interval_bandb "interval_arith/")
    (interval_soundness formula-decl nil interval_bandb
     "interval_arith/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (band? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bor? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (brel? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bite? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (BoolExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (BLETIN adt-constructor-decl
     "[[IntervalExpr, BoolExpr] -> (bletin?)]" IntervalExpr_adt
     "interval_arith/")
    (BAND adt-constructor-decl "[[BoolExpr, BoolExpr] -> (band?)]"
     IntervalExpr_adt "interval_arith/")
    (realorder? const-decl "bool" real_orders "reals/")
    (RealOrder type-eq-decl nil real_orders "reals/")
    (BREL adt-constructor-decl
     "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt
     "interval_arith/")
    (<= const-decl "bool" reals nil)
    (Fundamental? const-decl "bool" interval "interval_arith/")
    (Tan const-decl "Interval" interval_trig "interval_arith/")
    (tan_safe const-decl "real" interval_expr_trig "interval_arith/")
    (TAN? const-decl "bool" interval_trig "interval_arith/")
    (Inclusion? const-decl "bool" interval "interval_arith/")
    (PRED type-eq-decl nil defined_types nil)
    (TAN_Precondition application-judgement "(Precondition?)"
     interval_expr_trig "interval_arith/")
    (Tan_Fundamental application-judgement "(Fundamental?(TAN?(n)))"
     interval_expr_trig "interval_arith/")
    (Tan_Inclusion application-judgement
     "(Inclusion?(TAN?(n), tan_safe))" interval_expr_trig
     "interval_arith/")
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (RealExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (LETIN adt-constructor-decl "[[RealExpr, RealExpr] -> (letin?)]"
     IntervalExpr_adt "interval_arith/")
    (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]"
     IntervalExpr_adt "interval_arith/")
    (DIV adt-constructor-decl "[[RealExpr, RealExpr] -> (div?)]"
     IntervalExpr_adt "interval_arith/")
    (r2E const-decl "RealExpr" interval_expr "interval_arith/")
    (X const-decl "RealExpr" interval_expr "interval_arith/")
    (Precondition? const-decl "bool" interval "interval_arith/")
    (FUN adt-constructor-decl
     "[[pre: (Precondition?), opf: [real -> real],
  {F: [Interval -> Interval] |
           Inclusion?(pre, opf)(F) AND Fundamental?(pre)(F)},
  RealExpr] ->
   (fun?)]" IntervalExpr_adt "interval_arith/")
    (Pi_Inclusion application-judgement "(Includes?(pi_safe(unit)))"
     interval_expr_trig "interval_arith/")
    (IntervalExpr type-decl nil IntervalExpr_adt "interval_arith/")
    (Unit type-decl nil Unit_adt "structures/")
    (Interval type-eq-decl nil interval "interval_arith/")
    (Includes? const-decl "bool" interval "interval_arith/")
    (unit? adt-recognizer-decl "[Unit -> boolean]" Unit_adt
           "structures/")
    (unit adt-constructor-decl "(unit?)" Unit_adt "structures/")
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (CONST adt-constructor-decl
     "[[opc: [Unit -> real], (Includes?(opc(unit)))] -> (const?)]"
     IntervalExpr_adt "interval_arith/")
    (pi_safe const-decl "[Unit -> real]" interval_expr_trig
             "interval_arith/")
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (Pos? const-decl "bool" interval "interval_arith/")
    (Pi const-decl "(Pos?)" interval_trig "interval_arith/")
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx "trig_fnd/")
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (pi_lb const-decl "posreal" atan_approx "trig_fnd/")
    (pi_ub const-decl "posreal" atan_approx "trig_fnd/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (pi const-decl "posreal" atan "trig_fnd/")
    (Tan? const-decl "bool" sincos_def "trig_fnd/")
    (numfield nonempty-type-eq-decl nil number_fields 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 "[numfield, numfield -> numfield]" number_fields
       nil))
   shostak))
 (tr_200_250_abs_35 0
  (tr_200_250_abs_35-1 nil 3600857800
   ("" (then (skeep) (interval)) nil nil)
   ((posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx "trig_fnd/")
    (listn_0 name-judgement "listn[real](0)" simple_bandb
     "interval_arith/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (Maybe type-decl nil Maybe "structures/")
    (list type-decl nil list_adt nil)
    (every adt-def-decl "boolean" list_adt nil)
    (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (band? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bor? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bite? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (BoolExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (some? adt-recognizer-decl "[Maybe -> boolean]" Maybe
     "structures/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (val adt-accessor-decl "[(some?) -> T]" Maybe "structures/")
    (IntervalOutput type-eq-decl nil interval_bandb "interval_arith/")
    (Box type-eq-decl nil box "interval_arith/")
    (ProperBox? const-decl "bool" box "interval_arith/")
    (ProperBox type-eq-decl nil box "interval_arith/")
    (DirVar type-eq-decl nil branch_and_bound "structures/")
    (stack type-eq-decl nil stack "structures/")
    (length def-decl "nat" list_props nil)
    (DirVarStack type-eq-decl nil branch_and_bound "structures/")
    (DirVarSelector type-eq-decl nil branch_and_bound "structures/")
    (Output type-eq-decl nil branch_and_bound "structures/")
    (interval const-decl "Output" interval_bandb "interval_arith/")
    (alt_max const-decl "DirVar" interval_bandb "interval_arith/")
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    ([\|\|] const-decl "Interval" interval "interval_arith/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (Some adt-constructor-decl "[T -> (some?)]" Maybe "structures/")
    (FALSE const-decl "bool" booleans nil)
    (Env type-eq-decl nil box "interval_arith/")
    (vars_in_box? const-decl "bool" box "interval_arith/")
    (list2array def-decl "T" array2list "structures/")
    (v skolem-const-decl "posreal" interval_examples nil)
    (phi skolem-const-decl "{deg: real | Tan?(pi * deg / 180)}"
     interval_examples nil)
    (beval def-decl "bool" interval_bexpr "interval_arith/")
    (eval def-decl "real" interval_expr "interval_arith/")
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (|##| const-decl "bool" interval "interval_arith/")
    (V_0_58 skolem-const-decl "(const?)" interval_examples nil)
    (iar_57 skolem-const-decl "(brel?)" interval_examples nil)
    (vars_in_box formula-decl nil box "interval_arith/")
    (vars_in_box_rec def-decl
     "{b: bool | b = (FORALL (k: subrange(i, n - 1)): vs(k) ## nth(box, k - i))}"
     box "interval_arith/")
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (abs_le formula-decl nil abs_lems "reals/")
    (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
    (tan const-decl "real" sincos_def "trig_fnd/")
    (lb_interval formula-decl nil interval "interval_arith/")
    (ub_interval formula-decl nil interval "interval_arith/")
    (g const-decl "posreal" interval_examples nil)
    (sound? const-decl "bool" interval_bandb "interval_arith/")
    (interval_soundness formula-decl nil interval_bandb
     "interval_arith/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (Fundamental? const-decl "bool" interval "interval_arith/")
    (Tan const-decl "Interval" interval_trig "interval_arith/")
    (tan_safe const-decl "real" interval_expr_trig "interval_arith/")
    (TAN? const-decl "bool" interval_trig "interval_arith/")
    (Inclusion? const-decl "bool" interval "interval_arith/")
    (PRED type-eq-decl nil defined_types nil)
    (TAN_Precondition application-judgement "(Precondition?)"
     interval_expr_trig "interval_arith/")
    (Tan_Fundamental application-judgement "(Fundamental?(TAN?(n)))"
     interval_expr_trig "interval_arith/")
    (Tan_Inclusion application-judgement
     "(Inclusion?(TAN?(n), tan_safe))" interval_expr_trig
     "interval_arith/")
    (realorder? const-decl "bool" real_orders "reals/")
    (RealOrder type-eq-decl nil real_orders "reals/")
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (RealExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (brel? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (BREL adt-constructor-decl
     "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt
     "interval_arith/")
    (<= const-decl "bool" reals nil)
    (ABS adt-constructor-decl "[RealExpr -> (abs?)]" IntervalExpr_adt
     "interval_arith/")
    (LETIN adt-constructor-decl "[[RealExpr, RealExpr] -> (letin?)]"
     IntervalExpr_adt "interval_arith/")
    (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]"
     IntervalExpr_adt "interval_arith/")
    (DIV adt-constructor-decl "[[RealExpr, RealExpr] -> (div?)]"
     IntervalExpr_adt "interval_arith/")
    (r2E const-decl "RealExpr" interval_expr "interval_arith/")
    (X const-decl "RealExpr" interval_expr "interval_arith/")
    (Precondition? const-decl "bool" interval "interval_arith/")
    (FUN adt-constructor-decl
     "[[pre: (Precondition?), opf: [real -> real],
  {F: [Interval -> Interval] |
           Inclusion?(pre, opf)(F) AND Fundamental?(pre)(F)},
  RealExpr] ->
   (fun?)]" IntervalExpr_adt "interval_arith/")
    (Pi_Inclusion application-judgement "(Includes?(pi_safe(unit)))"
     interval_expr_trig "interval_arith/")
    (IntervalExpr type-decl nil IntervalExpr_adt "interval_arith/")
    (Unit type-decl nil Unit_adt "structures/")
    (Interval type-eq-decl nil interval "interval_arith/")
    (Includes? const-decl "bool" interval "interval_arith/")
    (unit? adt-recognizer-decl "[Unit -> boolean]" Unit_adt
           "structures/")
    (unit adt-constructor-decl "(unit?)" Unit_adt "structures/")
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (CONST adt-constructor-decl
     "[[opc: [Unit -> real], (Includes?(opc(unit)))] -> (const?)]"
     IntervalExpr_adt "interval_arith/")
    (pi_safe const-decl "[Unit -> real]" interval_expr_trig
             "interval_arith/")
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (Pos? const-decl "bool" interval "interval_arith/")
    (Pi const-decl "(Pos?)" interval_trig "interval_arith/")
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (pi_lb const-decl "posreal" atan_approx "trig_fnd/")
    (pi_ub const-decl "posreal" atan_approx "trig_fnd/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (pi const-decl "posreal" atan "trig_fnd/")
    (Tan? const-decl "bool" sincos_def "trig_fnd/")
    (numfield nonempty-type-eq-decl nil number_fields 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 "[numfield, numfield -> numfield]" number_fields
       nil))
   shostak))
 (G_TCC1 0
  (G_TCC1-1 nil 3600857800 ("" (subtype-tcc) nil nil) nil nil))
 (A_and_S_TCC1 0
  (A_and_S_TCC1-1 nil 3600857800 ("" (subtype-tcc) nil nil)
   ((lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (X const-decl "posreal" interval_examples nil))
   nil))
 (A_and_S_TCC2 0
  (A_and_S_TCC2-1 nil 3600857800 ("" (subtype-tcc) nil nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (X const-decl "posreal" interval_examples nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/"))
   nil))
 (A_and_S 0
  (A_and_S-1 nil 3600857800 ("" (interval) nil nil)
   ((listn_0 name-judgement "listn[real](0)" simple_bandb
     "interval_arith/")
    (Maybe type-decl nil Maybe "structures/")
    (list type-decl nil list_adt nil)
    (every adt-def-decl "boolean" list_adt nil)
    (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (band? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bor? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bite? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (BoolExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (some? adt-recognizer-decl "[Maybe -> boolean]" Maybe
     "structures/")
    (val adt-accessor-decl "[(some?) -> T]" Maybe "structures/")
    (IntervalOutput type-eq-decl nil interval_bandb "interval_arith/")
    (Box type-eq-decl nil box "interval_arith/")
    (ProperBox? const-decl "bool" box "interval_arith/")
    (ProperBox type-eq-decl nil box "interval_arith/")
    (DirVar type-eq-decl nil branch_and_bound "structures/")
    (stack type-eq-decl nil stack "structures/")
    (length def-decl "nat" list_props nil)
    (DirVarStack type-eq-decl nil branch_and_bound "structures/")
    (DirVarSelector type-eq-decl nil branch_and_bound "structures/")
    (Output type-eq-decl nil branch_and_bound "structures/")
    (interval const-decl "Output" interval_bandb "interval_arith/")
    (alt_max const-decl "DirVar" interval_bandb "interval_arith/")
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (Some adt-constructor-decl "[T -> (some?)]" Maybe "structures/")
    (Env type-eq-decl nil box "interval_arith/")
    (vars_in_box? const-decl "bool" box "interval_arith/")
    (list2array def-decl "T" array2list "structures/")
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (beval def-decl "bool" interval_bexpr "interval_arith/")
    (eval def-decl "real" interval_expr "interval_arith/")
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (iar_59 skolem-const-decl "(brel?)" interval_examples nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sound? const-decl "bool" interval_bandb "interval_arith/")
    (interval_soundness formula-decl nil interval_bandb
     "interval_arith/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Fundamental? const-decl "bool" interval "interval_arith/")
    (Ln const-decl "Interval" interval_lnexp "interval_arith/")
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (ln_safe const-decl "real" interval_expr_lnexp "interval_arith/")
    (Pos? const-decl "bool" interval "interval_arith/")
    (Inclusion? const-decl "bool" interval "interval_arith/")
    (PRED type-eq-decl nil defined_types nil)
    (Interval type-eq-decl nil interval "interval_arith/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (Pos_Precondition name-judgement "(Precondition?)" interval
     "interval_arith/")
    (Ln_Fundamental application-judgement "(Fundamental?(Pos?))"
     interval_expr_lnexp "interval_arith/")
    (Ln_Inclusion application-judgement "(Inclusion?(Pos?, ln_safe))"
     interval_expr_lnexp "interval_arith/")
    (FUN adt-constructor-decl
     "[[pre: (Precondition?), opf: [real -> real],
  {F: [Interval -> Interval] |
           Inclusion?(pre, opf)(F) AND Fundamental?(pre)(F)},
  RealExpr] ->
   (fun?)]" IntervalExpr_adt "interval_arith/")
    (Precondition? const-decl "bool" interval "interval_arith/")
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (r2E const-decl "RealExpr" interval_expr "interval_arith/")
    (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]"
     IntervalExpr_adt "interval_arith/")
    (BREL adt-constructor-decl
     "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt
     "interval_arith/")
    (brel? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (RealExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
--> --------------------

--> maximum size reached

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

95%


¤ Dauer der Verarbeitung: 0.37 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