| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/interval_arith/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 156 kB |
|
Quelle examples.prfSprache: Lisp |
|||||||||||||||
|
(examples (sqrt23 0 (sqrt23-1 nil 3600857800 ("" (numerical (! 1 1) :verbose? t) nil nil) ((IntervalExpr type-decl nil IntervalExpr_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]" IntervalExpr_adt nil) (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]" IntervalExpr_adt nil) (Precondition? const-decl "bool" interval 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 nil) (r2E const-decl "RealExpr" interval_expr nil) (Unit type-decl nil Unit_adt "structures/") (Includes? const-decl "bool" interval nil) (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 nil) (pi_safe const-decl "[Unit -> real]" interval_expr_trig nil) (Pos? const-decl "bool" interval nil) (Pi const-decl "(Pos?)" interval_trig nil) (NonNeg_Precondition name-judgement "(Precondition?)" interval nil) (Sqrt_Fundamental application-judgement "(Fundamental?(NonNeg?))" interval_expr_sqrt nil) (Sqrt_Inclusion application-judgement "(Inclusion?(NonNeg?, sqrt_safe))" interval_expr_sqrt nil) (Pi_Inclusion application-judgement "(Includes?(pi_safe(unit)))" interval_expr_trig 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) (Fundamental? const-decl "bool" interval nil) (Sqrt const-decl "(NonNeg?)" interval_sqrt nil) (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 nil) (NonNeg? const-decl "bool" interval nil) (Inclusion? const-decl "bool" interval 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) (PRED type-eq-decl nil defined_types nil) (Interval type-eq-decl nil interval nil) (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 nil) (sound? const-decl "bool" numerical_bandb nil) (listn_0 name-judgement "listn[real](0)" simple_bandb nil) (Env type-eq-decl nil box nil) (vars_in_box? const-decl "bool" box nil) (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_10 skolem-const-decl "(sub?)" examples nil) (|##| const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (lb_interval formula-decl nil interval nil) (ub_interval formula-decl nil interval nil) (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 nil) (- 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 nil) (/ 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 nil) (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 nil) (IntervalMinMax type-eq-decl nil numerical_bandb nil) (ProperBox type-eq-decl nil box nil) (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 nil) (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 nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]" IntervalExpr_adt 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 nil) (DIV adt-constructor-decl "[[RealExpr, RealExpr] -> (div?)]" IntervalExpr_adt nil) (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]" IntervalExpr_adt nil) (r2E const-decl "RealExpr" interval_expr nil) (Unit type-decl nil Unit_adt "structures/") (Includes? const-decl "bool" interval nil) (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 nil) (pi_safe const-decl "[Unit -> real]" interval_expr_trig nil) (Pos? const-decl "bool" interval nil) (Pi const-decl "(Pos?)" interval_trig 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) (Sqrt_Inclusion application-judgement "(Inclusion?(NonNeg?, sqrt_safe))" interval_expr_sqrt nil) (Sqrt_Fundamental application-judgement "(Fundamental?(NonNeg?))" interval_expr_sqrt nil) (NonNeg_Precondition name-judgement "(Precondition?)" interval nil) (Pi_Inclusion application-judgement "(Includes?(pi_safe(unit)))" interval_expr_trig nil) (Sin_Inclusion application-judgement "(Inclusion?(PreTrue, sin))" interval_expr_trig nil) (Sin_Fundamental application-judgement "(Fundamental?(PreTrue))" interval_expr_trig nil) (Sqrt const-decl "(NonNeg?)" interval_sqrt nil) (sqrt_safe const-decl "real" interval_expr_sqrt nil) (NonNeg? const-decl "bool" interval nil) (Fundamental? const-decl "bool" interval nil) (Sin const-decl "Interval" interval_trig nil) (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 nil) (Precondition? const-decl "bool" interval nil) (Inclusion? const-decl "bool" interval 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) (PRED type-eq-decl nil defined_types nil) (Interval type-eq-decl nil interval nil) (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 nil) (sound? const-decl "bool" numerical_bandb nil) (listn_0 name-judgement "listn[real](0)" simple_bandb nil) (Env type-eq-decl nil box nil) (vars_in_box? const-decl "bool" box nil) (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_11 skolem-const-decl "(add?)" examples nil) (|##| const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (lb_interval formula-decl nil interval nil) (ub_interval formula-decl nil interval nil) (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 nil) (+ 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 nil) (/ 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 nil) (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 nil) (IntervalMinMax type-eq-decl nil numerical_bandb nil) (ProperBox type-eq-decl nil box nil) (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 nil) (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 nil) (|##| const-decl "bool" interval nil)) nil)) (sqrtx3 0 (sqrtx3-1 nil 3600857800 ("" (interval) nil nil) ((listn_0 name-judgement "listn[real](0)" simple_bandb nil) (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 nil) (Box type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (ProperBox type-eq-decl nil box nil) (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 nil) (alt_max const-decl "DirVar" interval_bandb nil) (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 nil) (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 nil) (iar_12 skolem-const-decl "(bimplies?)" 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 nil) (beval def-decl "bool" interval_bexpr 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/") (x_13 skolem-const-decl "real" examples nil) (list2array def-decl "T" array2list "structures/") (vars_in_box? const-decl "bool" box nil) (Env type-eq-decl nil box nil) (sound? const-decl "bool" interval_bandb nil) (interval_soundness formula-decl nil interval_bandb nil) (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 nil) (Sqrt const-decl "(NonNeg?)" interval_sqrt nil) (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 nil) (NonNeg? const-decl "bool" interval nil) (Inclusion? const-decl "bool" interval nil) (PRED type-eq-decl nil defined_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NonNeg_Precondition name-judgement "(Precondition?)" interval nil) (Sqrt_Fundamental application-judgement "(Fundamental?(NonNeg?))" interval_expr_sqrt nil) (Sqrt_Inclusion application-judgement "(Inclusion?(NonNeg?, sqrt_safe))" interval_expr_sqrt nil) (Pi_Inclusion application-judgement "(Includes?(pi_safe(unit)))" interval_expr_trig nil) (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 nil) (Pos? const-decl "bool" interval nil) (pi_safe const-decl "[Unit -> real]" interval_expr_trig nil) (CONST adt-constructor-decl "[[opc: [Unit -> real], (Includes?(opc(unit)))] -> (const?)]" IntervalExpr_adt nil) (unit adt-constructor-decl "(unit?)" Unit_adt "structures/") (unit? adt-recognizer-decl "[Unit -> boolean]" Unit_adt "structures/") (Includes? const-decl "bool" interval nil) (Unit type-decl nil Unit_adt "structures/") (r2E const-decl "RealExpr" interval_expr 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 nil) (Precondition? const-decl "bool" interval nil) (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]" IntervalExpr_adt nil) (< const-decl "bool" reals nil) (BREL adt-constructor-decl "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt nil) (RealOrder type-eq-decl nil real_orders "reals/") (realorder? const-decl "bool" real_orders "reals/") (X const-decl "RealExpr" interval_expr nil) (BINCLUDES adt-constructor-decl "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BIMPLIES adt-constructor-decl "[[BoolExpr, BoolExpr] -> (bimplies?)]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (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 nil) (|##| const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (>= 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 nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (BAND adt-constructor-decl "[[BoolExpr, BoolExpr] -> (band?)]" IntervalExpr_adt nil) (realorder? const-decl "bool" real_orders "reals/") (RealOrder type-eq-decl nil real_orders "reals/") (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (BREL adt-constructor-decl "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt nil) (<= 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 nil) (DIV adt-constructor-decl "[[RealExpr, RealExpr] -> (div?)]" IntervalExpr_adt nil) (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]" IntervalExpr_adt nil) (r2E const-decl "RealExpr" interval_expr nil) (Unit type-decl nil Unit_adt "structures/") (Includes? const-decl "bool" interval nil) (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 nil) (pi_safe const-decl "[Unit -> real]" interval_expr_trig nil) (Pos? const-decl "bool" interval nil) (Pi const-decl "(Pos?)" interval_trig 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) (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 nil) (Cos_Inclusion application-judgement "(Inclusion?(PreTrue, cos))" interval_expr_trig nil) (Cos_Fundamental application-judgement "(Fundamental?(PreTrue))" interval_expr_trig nil) (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 nil) (Cos const-decl "Interval" interval_trig nil) (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 nil) (Precondition? const-decl "bool" interval nil) (Inclusion? const-decl "bool" interval 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) (PRED type-eq-decl nil defined_types nil) (Interval type-eq-decl nil interval nil) (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 nil) (sound? const-decl "bool" interval_bandb nil) (Env type-eq-decl nil box nil) (vars_in_box? const-decl "bool" box nil) (list2array def-decl "T" array2list "structures/") (beval def-decl "bool" interval_bexpr nil) (eval def-decl "real" interval_expr nil) (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_14 skolem-const-decl "(band?)" 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 nil) (alt_max const-decl "DirVar" interval_bandb nil) (interval const-decl "Output" interval_bandb nil) (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 nil) (ProperBox? const-decl "bool" box nil) (Box type-eq-decl nil box nil) (IntervalOutput type-eq-decl nil interval_bandb nil) (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 nil) (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 nil) (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 nil) (Box type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (ProperBox type-eq-decl nil box nil) (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 nil) (alt_max const-decl "DirVar" interval_bandb 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/") (Env type-eq-decl nil box nil) (vars_in_box? const-decl "bool" box nil) (list2array def-decl "T" array2list "structures/") (beval def-decl "bool" interval_bexpr nil) (realexpr? const-decl "bool" interval_expr nil) (eval def-decl "real" interval_expr nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (V_0_16 skolem-const-decl "(const?)" examples nil) (V_1_17 skolem-const-decl "(letin?)" examples nil) (iar_15 skolem-const-decl "(bletin?)" examples nil) (g const-decl "posreal" examples nil) (sound? const-decl "bool" interval_bandb nil) (interval_soundness formula-decl nil interval_bandb nil) (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 nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (BLETIN adt-constructor-decl "[[IntervalExpr, BoolExpr] -> (bletin?)]" IntervalExpr_adt nil) (BAND adt-constructor-decl "[[BoolExpr, BoolExpr] -> (band?)]" IntervalExpr_adt nil) (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 nil) (<= const-decl "bool" reals nil) (Fundamental? const-decl "bool" interval nil) (Tan const-decl "Interval" interval_trig nil) (tan_safe const-decl "real" interval_expr_trig nil) (TAN? const-decl "bool" interval_trig nil) (Inclusion? const-decl "bool" interval nil) (PRED type-eq-decl nil defined_types nil) (TAN_Precondition application-judgement "(Precondition?)" interval_expr_trig nil) (Tan_Fundamental application-judgement "(Fundamental?(TAN?(n)))" interval_expr_trig nil) (Tan_Inclusion application-judgement "(Inclusion?(TAN?(n), tan_safe))" interval_expr_trig nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (LETIN adt-constructor-decl "[[RealExpr, RealExpr] -> (letin?)]" IntervalExpr_adt nil) (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]" IntervalExpr_adt nil) (DIV adt-constructor-decl "[[RealExpr, RealExpr] -> (div?)]" IntervalExpr_adt nil) (r2E const-decl "RealExpr" interval_expr nil) (X const-decl "RealExpr" interval_expr nil) (Precondition? const-decl "bool" interval 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 nil) (Pi_Inclusion application-judgement "(Includes?(pi_safe(unit)))" interval_expr_trig nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (Unit type-decl nil Unit_adt "structures/") (Interval type-eq-decl nil interval nil) (Includes? const-decl "bool" interval nil) (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 nil) (CONST adt-constructor-decl "[[opc: [Unit -> real], (Includes?(opc(unit)))] -> (const?)]" IntervalExpr_adt nil) (pi_safe const-decl "[Unit -> real]" interval_expr_trig nil) (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 nil) (Pi const-decl "(Pos?)" interval_trig nil) (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 ("" (skeep) (("" (interval) nil nil)) nil) ((* const-decl "[numfield, 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) (numfield nonempty-type-eq-decl nil number_fields nil) (Tan? const-decl "bool" sincos_def "trig_fnd/") (pi const-decl "posreal" atan "trig_fnd/") (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pi_ub const-decl "posreal" atan_approx "trig_fnd/") (pi_lb const-decl "posreal" atan_approx "trig_fnd/") (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (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) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (Pi const-decl "(Pos?)" interval_trig nil) (Pos? const-decl "bool" interval nil) (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) (pi_safe const-decl "[Unit -> real]" interval_expr_trig nil) (CONST adt-constructor-decl "[[opc: [Unit -> real], (Includes?(opc(unit)))] -> (const?)]" IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (unit adt-constructor-decl "(unit?)" Unit_adt "structures/") (unit? adt-recognizer-decl "[Unit -> boolean]" Unit_adt "structures/") (Includes? const-decl "bool" interval nil) (Interval type-eq-decl nil interval nil) (Unit type-decl nil Unit_adt "structures/") (IntervalExpr type-decl nil IntervalExpr_adt nil) (Pi_Inclusion application-judgement "(Includes?(pi_safe(unit)))" interval_expr_trig 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 nil) (Precondition? const-decl "bool" interval nil) (X const-decl "RealExpr" interval_expr nil) (r2E const-decl "RealExpr" interval_expr nil) (DIV adt-constructor-decl "[[RealExpr, RealExpr] -> (div?)]" IntervalExpr_adt nil) (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]" IntervalExpr_adt nil) (LETIN adt-constructor-decl "[[RealExpr, RealExpr] -> (letin?)]" IntervalExpr_adt nil) (ABS adt-constructor-decl "[RealExpr -> (abs?)]" IntervalExpr_adt nil) (<= const-decl "bool" reals nil) (BREL adt-constructor-decl "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (RealOrder type-eq-decl nil real_orders "reals/") (realorder? const-decl "bool" real_orders "reals/") (Tan_Inclusion application-judgement "(Inclusion?(TAN?(n), tan_safe))" interval_expr_trig nil) (Tan_Fundamental application-judgement "(Fundamental?(TAN?(n)))" interval_expr_trig nil) (TAN_Precondition application-judgement "(Precondition?)" interval_expr_trig nil) (PRED type-eq-decl nil defined_types nil) (Inclusion? const-decl "bool" interval nil) (TAN? const-decl "bool" interval_trig nil) (tan_safe const-decl "real" interval_expr_trig nil) (Tan const-decl "Interval" interval_trig nil) (Fundamental? const-decl "bool" interval nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (interval_soundness formula-decl nil interval_bandb nil) (sound? const-decl "bool" interval_bandb nil) (g const-decl "posreal" examples nil) (ub_interval formula-decl nil interval nil) (lb_interval formula-decl nil interval nil) (tan const-decl "real" sincos_def "trig_fnd/") (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (abs_le formula-decl nil abs_lems "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (vars_in_box_rec def-decl "{b: bool | b = (FORALL (k: subrange(i, n - 1)): vs(k) ## nth(box, k - i))}" box nil) (vars_in_box formula-decl nil box nil) (iar_18 skolem-const-decl "(brel?)" examples nil) (V_0_19 skolem-const-decl "(const?)" examples nil) (|##| const-decl "bool" interval nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (eval def-decl "real" interval_expr nil) (beval def-decl "bool" interval_bexpr nil) (phi skolem-const-decl "{deg: real | Tan?(pi * deg / 180)}" examples nil) (v skolem-const-decl "posreal" examples nil) (list2array def-decl "T" array2list "structures/") (vars_in_box? const-decl "bool" box nil) (Env type-eq-decl nil box nil) (FALSE const-decl "bool" booleans 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) (- const-decl "[numfield -> numfield]" number_fields nil) ([\|\|] const-decl "Interval" interval nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (alt_max const-decl "DirVar" interval_bandb nil) (interval const-decl "Output" interval_bandb nil) (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 nil) (ProperBox? const-decl "bool" box nil) (Box type-eq-decl nil box nil) (IntervalOutput type-eq-decl nil interval_bandb nil) (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) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (every adt-def-decl "boolean" list_adt nil) (list type-decl nil list_adt nil) (Maybe type-decl nil Maybe "structures/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (listn_0 name-judgement "listn[real](0)" simple_bandb nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types 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" 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" 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 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 nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (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 nil) (Box type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (ProperBox type-eq-decl nil box nil) (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 nil) (alt_max const-decl "DirVar" interval_bandb 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/") (Env type-eq-decl nil box nil) (vars_in_box? const-decl "bool" box nil) (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 nil) (eval def-decl "real" interval_expr nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (iar_20 skolem-const-decl "(brel?)" 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 nil) (interval_soundness formula-decl nil interval_bandb nil) (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 nil) (Ln const-decl "Interval" interval_lnexp nil) (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 nil) (Pos? const-decl "bool" interval nil) (Inclusion? const-decl "bool" interval nil) (PRED type-eq-decl nil defined_types nil) (Interval type-eq-decl nil interval nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (Pos_Precondition name-judgement "(Precondition?)" interval nil) (Ln_Fundamental application-judgement "(Fundamental?(Pos?))" interval_expr_lnexp nil) (Ln_Inclusion application-judgement "(Inclusion?(Pos?, ln_safe))" interval_expr_lnexp 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 nil) (Precondition? const-decl "bool" interval nil) (/ 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 nil) (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]" IntervalExpr_adt nil) (BREL adt-constructor-decl "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (RealOrder type-eq-decl nil real_orders "reals/") (realorder? const-decl "bool" real_orders "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (X const-decl "posreal" examples nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (> const-decl "bool" reals 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_minus_real_is_real application-judgement "real" reals nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil)) shostak)) (common_point_TCC1 0 (common_point_TCC1-1 nil 3600857800 ("" (subtype-tcc) nil nil) (([\|\|] const-decl "Interval" interval nil) (|##| const-decl "bool" interval nil) (/= const-decl "boolean" notequal nil)) nil)) (common_point_TCC2 0 (common_point_TCC2-1 nil 3600857800 ("" (subtype-tcc) nil nil) (([\|\|] const-decl "Interval" interval nil) (|##| const-decl "bool" interval nil) (/= const-decl "boolean" notequal nil)) nil)) (common_point_TCC3 0 (common_point_TCC3-1 nil 3600857800 ("" (subtype-tcc) nil nil) ((^ const-decl "real" exponentiation nil) ([\|\|] const-decl "Interval" interval nil) (|##| const-decl "bool" interval nil) (Integral const-decl "real" integral_def "analysis/") (atan_value const-decl "real" atan "trig_fnd/") (pi const-decl "posreal" atan "trig_fnd/") (cos const-decl "real" sincos_def "trig_fnd/") (real_minus_real_is_real application-judgement "real" reals 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/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sqrt_pos application-judgement "posreal" sqrt "reals/")) nil)) (common_point_TCC4 0 (common_point_TCC4-1 nil 3600857800 ("" (subtype-tcc) nil nil) ((^ const-decl "real" exponentiation nil) ([\|\|] const-decl "Interval" interval nil) (|##| const-decl "bool" interval nil) (Integral const-decl "real" integral_def "analysis/") (atan_value const-decl "real" atan "trig_fnd/") (pi const-decl "posreal" atan "trig_fnd/") (sin const-decl "real" sincos_def "trig_fnd/") (real_minus_real_is_real application-judgement "real" reals 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/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sqrt_pos application-judgement "posreal" sqrt "reals/")) nil)) (common_point 0 (common_point-1 nil 3600857800 ("" (interval) nil nil) ((nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (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) (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 nil) (Box type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (ProperBox type-eq-decl nil box nil) (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 nil) (alt_max const-decl "DirVar" interval_bandb nil) (FALSE const-decl "bool" booleans nil) (BNOT adt-constructor-decl "[BoolExpr -> (bnot?)]" IntervalExpr_adt nil) (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/") (iar_21 skolem-const-decl "(band?)" examples nil) (list2array def-decl "T" array2list "structures/") (posrat_plus_nnrat_is_posrat application-judgement "posrat" rationals nil) (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs nil) (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) (eval def-decl "real" interval_expr nil) (beval def-decl "bool" interval_bexpr nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (sound? const-decl "bool" interval_bandb nil) (interval_soundness formula-decl nil interval_bandb 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (Sin const-decl "Interval" interval_trig nil) (Cos const-decl "Interval" interval_trig nil) (PreTrue const-decl "(Precondition?)" interval_expr nil) (Precondition? const-decl "bool" interval nil) (Fundamental? const-decl "bool" interval nil) (Sqrt const-decl "(NonNeg?)" interval_sqrt nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (sqrt_safe const-decl "real" interval_expr_sqrt nil) (NonNeg? const-decl "bool" interval nil) (Inclusion? const-decl "bool" interval nil) (PRED type-eq-decl nil defined_types nil) (NonNeg_Precondition name-judgement "(Precondition?)" interval nil) (Sqrt_Fundamental application-judgement "(Fundamental?(NonNeg?))" interval_expr_sqrt nil) (Sqrt_Inclusion application-judgement "(Inclusion?(NonNeg?, sqrt_safe))" interval_expr_sqrt nil) (Cos_Fundamental application-judgement "(Fundamental?(PreTrue))" interval_expr_trig nil) (Cos_Inclusion application-judgement "(Inclusion?(PreTrue, cos))" interval_expr_trig nil) (Sin_Fundamental application-judgement "(Fundamental?(PreTrue))" interval_expr_trig nil) (Sin_Inclusion application-judgement "(Inclusion?(PreTrue, sin))" interval_expr_trig 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 nil) (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]" IntervalExpr_adt nil) (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]" IntervalExpr_adt nil) (POW adt-constructor-decl "[[RealExpr, nat] -> (pow?)]" IntervalExpr_adt nil) (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]" IntervalExpr_adt nil) (BINCLUDES adt-constructor-decl "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt nil) (r2E const-decl "RealExpr" interval_expr nil) (X const-decl "RealExpr" interval_expr nil) (ABS adt-constructor-decl "[RealExpr -> (abs?)]" IntervalExpr_adt nil) (BREL adt-constructor-decl "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealOrder type-eq-decl nil real_orders "reals/") (realorder? const-decl "bool" real_orders "reals/") (BAND adt-constructor-decl "[[BoolExpr, BoolExpr] -> (band?)]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (sin_range application-judgement "trig_range" sincos_def "trig_fnd/") (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" sincos_def "trig_fnd/") (real_plus_real_is_real application-judgement "real" reals 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) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (AND const-decl "[bool, 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (Interval type-eq-decl nil interval nil) (|##| const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (<= const-decl "bool" reals 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) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (< const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (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) (^ const-decl "real" exponentiation nil) (- 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 "[T, T -> boolean]" equalities nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (cos const-decl "real" sincos_def "trig_fnd/") (sin const-decl "real" sincos_def "trig_fnd/")) shostak)) (r_TCC1 0 (r_TCC1-1 nil 3600857800 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (r_TCC2 0 (r_TCC2-1 nil 3600857800 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (atan_implementation 0 (atan_implementation-1 nil 3600857800 ("" (interval) nil nil) ((listn_0 name-judgement "listn[real](0)" simple_bandb nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (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 nil) (Box type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (ProperBox type-eq-decl nil box nil) (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 nil) (alt_max const-decl "DirVar" interval_bandb nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) ([\|\|] const-decl "Interval" interval 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 nil) (length_singleton formula-decl nil more_list_props "structures/") (|##| const-decl "bool" interval nil) (ub_interval formula-decl nil interval nil) (lb_interval formula-decl nil interval nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs_le formula-decl nil abs_lems "reals/") (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (vars_in_box_rec def-decl "{b: bool | b = (FORALL (k: subrange(i, n - 1)): vs(k) ## nth(box, k - i))}" box nil) (iar_22 skolem-const-decl "(bimplies?)" examples nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (eval def-decl "real" interval_expr nil) (beval def-decl "bool" interval_bexpr nil) (x_23 skolem-const-decl "real" examples nil) (list2array def-decl "T" array2list "structures/") (vars_in_box? const-decl "bool" box nil) (Env type-eq-decl nil box nil) (^ const-decl "real" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (sound? const-decl "bool" interval_bandb nil) (interval_soundness formula-decl nil interval_bandb nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (Interval type-eq-decl nil interval nil) (PRED type-eq-decl nil defined_types nil) (Inclusion? const-decl "bool" interval nil) (Precondition? const-decl "bool" interval nil) (PreTrue const-decl "(Precondition?)" interval_expr nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (pi const-decl "posreal" atan "trig_fnd/") (real_abs_lt_pi2 nonempty-type-eq-decl nil atan "trig_fnd/") (atan const-decl "real_abs_lt_pi2" atan "trig_fnd/") (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) (Atan const-decl "Interval" interval_trig nil) (Fundamental? const-decl "bool" interval nil) (Atan_Fundamental application-judgement "(Fundamental?(PreTrue))" interval_expr_trig nil) (Atan_Inclusion application-judgement "(Inclusion?(PreTrue, atan))" interval_expr_trig nil) (POW adt-constructor-decl "[[RealExpr, nat] -> (pow?)]" IntervalExpr_adt nil) (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]" IntervalExpr_adt 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 nil) (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]" IntervalExpr_adt nil) (r2E const-decl "RealExpr" interval_expr nil) (X const-decl "RealExpr" interval_expr nil) (ABS adt-constructor-decl "[RealExpr -> (abs?)]" IntervalExpr_adt nil) (BREL adt-constructor-decl "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (RealOrder type-eq-decl nil real_orders "reals/") (realorder? const-decl "bool" real_orders "reals/") (BIMPLIES adt-constructor-decl "[[BoolExpr, BoolExpr] -> (bimplies?)]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals 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) (AND const-decl "[bool, 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals 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) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil)) shostak)) (ex1_ba_TCC1 0 (ex1_ba_TCC1-1 nil 3600857800 ("" (subtype-tcc) nil nil) (([\|\|] const-decl "Interval" interval nil) (|##| const-decl "bool" interval nil) (/= const-decl "boolean" notequal nil)) nil)) (ex1_ba_TCC2 0 (ex1_ba_TCC2-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_plus_real_is_real application-judgement "real" 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 nil) (|##| const-decl "bool" interval nil)) nil)) (ex1_ba 0 (ex1_ba-1 nil 3600857801 ("" (interval) nil nil) ((listn_0 name-judgement "listn[real](0)" simple_bandb nil) (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 nil) (Box type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (ProperBox type-eq-decl nil box nil) (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 nil) (alt_max const-decl "DirVar" interval_bandb nil) (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 nil) (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 nil) (iar_24 skolem-const-decl "(bimplies?)" examples nil) (eval def-decl "real" interval_expr nil) (beval def-decl "bool" interval_bexpr nil) (x_25 skolem-const-decl "real" examples nil) (list2array def-decl "T" array2list "structures/") (vars_in_box? const-decl "bool" box nil) (Env type-eq-decl nil box nil) (epsilon const-decl "real" examples nil) (sound? const-decl "bool" interval_bandb nil) (interval_soundness formula-decl nil interval_bandb nil) (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 nil) (Ln const-decl "Interval" interval_lnexp nil) (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 nil) (Pos? const-decl "bool" interval nil) (Inclusion? const-decl "bool" interval nil) (PRED type-eq-decl nil defined_types nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (Pos_Precondition name-judgement "(Precondition?)" interval nil) (Ln_Fundamental application-judgement "(Fundamental?(Pos?))" interval_expr_lnexp nil) (Ln_Inclusion application-judgement "(Inclusion?(Pos?, ln_safe))" interval_expr_lnexp nil) (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]" IntervalExpr_adt 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 nil) (Precondition? const-decl "bool" interval nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (r2E const-decl "RealExpr" interval_expr nil) (POW adt-constructor-decl "[[RealExpr, nat] -> (pow?)]" IntervalExpr_adt nil) (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]" IntervalExpr_adt nil) (<= const-decl "bool" reals nil) (BREL adt-constructor-decl "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt nil) (RealOrder type-eq-decl nil real_orders "reals/") (realorder? const-decl "bool" real_orders "reals/") (X const-decl "RealExpr" interval_expr nil) (BINCLUDES adt-constructor-decl "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BIMPLIES adt-constructor-decl "[[BoolExpr, BoolExpr] -> (bimplies?)]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals 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) (AND const-decl "[bool, 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (Interval type-eq-decl nil interval nil) (|##| const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (>= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (> const-decl "bool" reals nil)) shostak)) (ex2_ba_TCC1 0 (ex2_ba_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_minus_real_is_real application-judgement "real" 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 nil) (|##| const-decl "bool" interval nil)) nil)) (ex2_ba 0 (ex2_ba-1 nil 3600857801 ("" (interval) nil nil) ((listn_0 name-judgement "listn[real](0)" simple_bandb nil) (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 nil) (Box type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (ProperBox type-eq-decl nil box nil) (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 nil) (alt_max const-decl "DirVar" interval_bandb nil) (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 nil) (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 nil) (iar_26 skolem-const-decl "(bimplies?)" examples nil) (eval def-decl "real" interval_expr nil) (beval def-decl "bool" interval_bexpr nil) (x_27 skolem-const-decl "real" examples nil) (list2array def-decl "T" array2list "structures/") (vars_in_box? const-decl "bool" box nil) (Env type-eq-decl nil box nil) (epsilon const-decl "real" examples nil) (sound? const-decl "bool" interval_bandb nil) (interval_soundness formula-decl nil interval_bandb nil) (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 nil) (Ln const-decl "Interval" interval_lnexp nil) (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 nil) (Pos? const-decl "bool" interval nil) (Inclusion? const-decl "bool" interval nil) (PRED type-eq-decl nil defined_types nil) (Pos_Precondition name-judgement "(Precondition?)" interval nil) (Ln_Fundamental application-judgement "(Fundamental?(Pos?))" interval_expr_lnexp nil) (Ln_Inclusion application-judgement "(Inclusion?(Pos?, ln_safe))" interval_expr_lnexp nil) (NEG adt-constructor-decl "[RealExpr -> (neg?)]" IntervalExpr_adt nil) (r2E const-decl "RealExpr" interval_expr 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 nil) (Precondition? const-decl "bool" interval nil) (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]" IntervalExpr_adt nil) (<= const-decl "bool" reals nil) (BREL adt-constructor-decl "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt nil) (RealOrder type-eq-decl nil real_orders "reals/") (realorder? const-decl "bool" real_orders "reals/") (X const-decl "RealExpr" interval_expr nil) (BINCLUDES adt-constructor-decl "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BIMPLIES adt-constructor-decl "[[BoolExpr, BoolExpr] -> (bimplies?)]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals 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 nil) (|##| const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (> const-decl "bool" reals nil)) shostak)) (ex3_ba_TCC1 0 (ex3_ba_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_minus_real_is_real application-judgement "real" 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 nil) (|##| const-decl "bool" interval nil)) nil)) (ex3_ba 0 (ex3_ba-1 nil 3600857801 ("" (interval) nil nil) ((listn_0 name-judgement "listn[real](0)" simple_bandb nil) (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 nil) (Box type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (ProperBox type-eq-decl nil box nil) (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 nil) (alt_max const-decl "DirVar" interval_bandb nil) (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 nil) (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 nil) (iar_28 skolem-const-decl "(bimplies?)" examples nil) (real_times_real_is_real application-judgement "real" reals nil) (eval def-decl "real" interval_expr nil) (beval def-decl "bool" interval_bexpr nil) (minus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (x_29 skolem-const-decl "real" examples nil) (list2array def-decl "T" array2list "structures/") (vars_in_box? const-decl "bool" box nil) (Env type-eq-decl nil box nil) (epsilon const-decl "real" examples nil) (sound? const-decl "bool" interval_bandb nil) (interval_soundness formula-decl nil interval_bandb nil) (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 nil) (Ln const-decl "Interval" interval_lnexp nil) (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 nil) (Pos? const-decl "bool" interval nil) (Inclusion? const-decl "bool" interval nil) (PRED type-eq-decl nil defined_types nil) (Pos_Precondition name-judgement "(Precondition?)" interval nil) (Ln_Fundamental application-judgement "(Fundamental?(Pos?))" interval_expr_lnexp nil) (Ln_Inclusion application-judgement "(Inclusion?(Pos?, ln_safe))" interval_expr_lnexp 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 nil) (Precondition? const-decl "bool" interval nil) (SQ adt-constructor-decl "[RealExpr -> (sq?)]" IntervalExpr_adt nil) (r2E const-decl "RealExpr" interval_expr nil) (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]" IntervalExpr_adt nil) (NEG adt-constructor-decl "[RealExpr -> (neg?)]" IntervalExpr_adt nil) (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]" IntervalExpr_adt nil) (<= const-decl "bool" reals nil) (BREL adt-constructor-decl "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt nil) (RealOrder type-eq-decl nil real_orders "reals/") (realorder? const-decl "bool" real_orders "reals/") (X const-decl "RealExpr" interval_expr nil) (BINCLUDES adt-constructor-decl "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BIMPLIES adt-constructor-decl "[[BoolExpr, BoolExpr] -> (bimplies?)]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (real_minus_real_is_real application-judgement "real" reals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals 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 nil) (|##| const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (> const-decl "bool" reals nil)) shostak)) (ex4_ba 0 (ex4_ba-1 nil 3600857801 ("" (interval) nil nil) ((listn_0 name-judgement "listn[real](0)" simple_bandb nil) (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 nil) (Box type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (ProperBox type-eq-decl nil box nil) (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 nil) (alt_max const-decl "DirVar" interval_bandb nil) (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 nil) (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 nil) (iar_30 skolem-const-decl "(bimplies?)" examples nil) (eval def-decl "real" interval_expr nil) (beval def-decl "bool" interval_bexpr nil) (x_31 skolem-const-decl "real" examples nil) (list2array def-decl "T" array2list "structures/") (vars_in_box? const-decl "bool" box nil) (Env type-eq-decl nil box nil) (epsilon const-decl "real" examples nil) (sound? const-decl "bool" interval_bandb nil) (interval_soundness formula-decl nil interval_bandb nil) (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 nil) (Ln const-decl "Interval" interval_lnexp nil) (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 nil) (Pos? const-decl "bool" interval nil) (Inclusion? const-decl "bool" interval nil) (PRED type-eq-decl nil defined_types nil) (Pos_Precondition name-judgement "(Precondition?)" interval nil) (Ln_Fundamental application-judgement "(Fundamental?(Pos?))" interval_expr_lnexp nil) (Ln_Inclusion application-judgement "(Inclusion?(Pos?, ln_safe))" interval_expr_lnexp nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (SQ adt-constructor-decl "[RealExpr -> (sq?)]" IntervalExpr_adt nil) (/ 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 nil) (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]" IntervalExpr_adt 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 nil) (Precondition? const-decl "bool" interval nil) (ABS adt-constructor-decl "[RealExpr -> (abs?)]" IntervalExpr_adt nil) (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]" IntervalExpr_adt nil) (<= const-decl "bool" reals nil) (BREL adt-constructor-decl "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt nil) (RealOrder type-eq-decl nil real_orders "reals/") (realorder? const-decl "bool" real_orders "reals/") (X const-decl "RealExpr" interval_expr nil) (BINCLUDES adt-constructor-decl "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BIMPLIES adt-constructor-decl "[[BoolExpr, BoolExpr] -> (bimplies?)]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals 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 nil) (|##| const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (> const-decl "bool" reals nil)) shostak)) (ex5_ba_TCC1 0 (ex5_ba_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_plus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (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 nil) (|##| const-decl "bool" interval nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (ex5_ba 0 (ex5_ba-1 nil 3600857801 ("" (interval) nil nil) ((listn_0 name-judgement "listn[real](0)" simple_bandb nil) (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 nil) (Box type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (ProperBox type-eq-decl nil box nil) (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 nil) (alt_max const-decl "DirVar" interval_bandb nil) (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 nil) (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 nil) (iar_32 skolem-const-decl "(bimplies?)" examples nil) (eval def-decl "real" interval_expr nil) (beval def-decl "bool" interval_bexpr nil) (x_33 skolem-const-decl "real" examples nil) (list2array def-decl "T" array2list "structures/") (vars_in_box? const-decl "bool" box nil) (Env type-eq-decl nil box nil) (epsilon const-decl "real" examples nil) (sound? const-decl "bool" interval_bandb nil) (interval_soundness formula-decl nil interval_bandb nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (Fundamental? const-decl "bool" interval nil) (Ln const-decl "Interval" interval_lnexp nil) (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 nil) (Pos? const-decl "bool" interval nil) (Inclusion? const-decl "bool" interval nil) (PRED type-eq-decl nil defined_types nil) (Pos_Precondition name-judgement "(Precondition?)" interval nil) (Ln_Fundamental application-judgement "(Fundamental?(Pos?))" interval_expr_lnexp nil) (Ln_Inclusion application-judgement "(Inclusion?(Pos?, ln_safe))" interval_expr_lnexp nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (SQ adt-constructor-decl "[RealExpr -> (sq?)]" IntervalExpr_adt nil) (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]" IntervalExpr_adt nil) (r2E const-decl "RealExpr" interval_expr nil) (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]" IntervalExpr_adt 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 nil) (Precondition? const-decl "bool" interval nil) (ABS adt-constructor-decl "[RealExpr -> (abs?)]" IntervalExpr_adt nil) (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]" IntervalExpr_adt nil) (<= const-decl "bool" reals nil) (BREL adt-constructor-decl "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt nil) (RealOrder type-eq-decl nil real_orders "reals/") (realorder? const-decl "bool" real_orders "reals/") (X const-decl "RealExpr" interval_expr nil) (BINCLUDES adt-constructor-decl "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BIMPLIES adt-constructor-decl "[[BoolExpr, BoolExpr] -> (bimplies?)]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (real_minus_real_is_real application-judgement "real" reals 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 nil) (|##| const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (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]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (> const-decl "bool" reals nil)) shostak)) (ex6_ba 0 (ex6_ba-1 nil 3600857801 ("" (interval) nil nil) ((listn_0 name-judgement "listn[real](0)" simple_bandb nil) (Maybe type-decl nil Maybe "structures/") (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (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/") (NOT const-decl "[bool -> bool]" booleans nil) (val adt-accessor-decl "[(some?) -> T]" Maybe "structures/") (IntervalOutput type-eq-decl nil interval_bandb nil) (Box type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (ProperBox type-eq-decl nil box nil) (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 nil) (alt_max const-decl "DirVar" interval_bandb nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) ([\|\|] const-decl "Interval" interval 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 nil) (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 nil) (iar_34 skolem-const-decl "(bimplies?)" examples nil) (|##| const-decl "bool" interval nil) (real_minus_real_is_real application-judgement "real" reals nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (eval def-decl "real" interval_expr nil) (beval def-decl "bool" interval_bexpr nil) (real_plus_real_is_real application-judgement "real" reals nil) (x_35 skolem-const-decl "real" examples nil) (list2array def-decl "T" array2list "structures/") (vars_in_box? const-decl "bool" box nil) (Env type-eq-decl nil box nil) (epsilon const-decl "real" examples nil) (sound? const-decl "bool" interval_bandb nil) (interval_soundness formula-decl nil interval_bandb nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (AND const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (Interval type-eq-decl nil interval nil) (PRED type-eq-decl nil defined_types 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) (Inclusion? const-decl "bool" interval nil) (Precondition? const-decl "bool" interval nil) (PreTrue const-decl "(Precondition?)" interval_expr 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) (exp_safe const-decl "posreal" interval_expr_lnexp nil) (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 nil) (Exp const-decl "(Pos?)" interval_lnexp nil) (Fundamental? const-decl "bool" interval 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) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (Exp_Inclusion application-judgement "(Inclusion?(PreTrue, exp_safe))" interval_expr_lnexp nil) (Exp_Fundamental application-judgement "(Fundamental?(PreTrue))" interval_expr_lnexp nil) (SQ adt-constructor-decl "[RealExpr -> (sq?)]" IntervalExpr_adt nil) (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]" IntervalExpr_adt 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) (r2E const-decl "RealExpr" interval_expr 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 nil) (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]" IntervalExpr_adt nil) (<= const-decl "bool" reals nil) (BREL adt-constructor-decl "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt nil) (RealOrder type-eq-decl nil real_orders "reals/") (realorder? const-decl "bool" real_orders "reals/") (X const-decl "RealExpr" interval_expr nil) (BINCLUDES adt-constructor-decl "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BIMPLIES adt-constructor-decl "[[BoolExpr, BoolExpr] -> (bimplies?)]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (IntervalExpr type-decl nil IntervalExpr_adt nil)) shostak)) (ex7_ba 0 (ex7_ba-1 nil 3600857801 ("" (interval) nil nil) ((listn_0 name-judgement "listn[real](0)" simple_bandb nil) (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 nil) (Box type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (ProperBox type-eq-decl nil box nil) (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 nil) (alt_max const-decl "DirVar" interval_bandb nil) (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 nil) (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 nil) (iar_36 skolem-const-decl "(bimplies?)" examples nil) (eval def-decl "real" interval_expr nil) (beval def-decl "bool" interval_bexpr nil) (x_37 skolem-const-decl "real" examples nil) (list2array def-decl "T" array2list "structures/") (vars_in_box? const-decl "bool" box nil) (Env type-eq-decl nil box nil) (epsilon const-decl "real" examples nil) (sound? const-decl "bool" interval_bandb nil) (interval_soundness formula-decl nil interval_bandb nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (AND const-decl "[bool, bool -> bool]" booleans nil) (PRED type-eq-decl nil defined_types nil) (Inclusion? const-decl "bool" interval nil) (Precondition? const-decl "bool" interval nil) (PreTrue const-decl "(Precondition?)" interval_expr 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) (exp_safe const-decl "posreal" interval_expr_lnexp nil) (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 nil) (Exp const-decl "(Pos?)" interval_lnexp nil) (Fundamental? const-decl "bool" interval nil) (Exp_Fundamental application-judgement "(Fundamental?(PreTrue))" interval_expr_lnexp nil) (Exp_Inclusion application-judgement "(Inclusion?(PreTrue, exp_safe))" interval_expr_lnexp nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]" IntervalExpr_adt nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (r2E const-decl "RealExpr" interval_expr nil) (POW adt-constructor-decl "[[RealExpr, nat] -> (pow?)]" IntervalExpr_adt 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 nil) (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]" IntervalExpr_adt nil) (<= const-decl "bool" reals nil) (BREL adt-constructor-decl "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt nil) (RealOrder type-eq-decl nil real_orders "reals/") (realorder? const-decl "bool" real_orders "reals/") (X const-decl "RealExpr" interval_expr nil) (BINCLUDES adt-constructor-decl "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BIMPLIES adt-constructor-decl "[[BoolExpr, BoolExpr] -> (bimplies?)]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (IntervalExpr type-decl nil IntervalExpr_adt nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals 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 nil) (|##| const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (>= const-decl "bool" reals nil)) shostak)) (Tunnel_3_IL 0 (Tunnel_3_IL-1 nil 3600857801 ("" (interval) nil nil) ((posint_exp application-judgement "posint" exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (listn_0 name-judgement "listn[real](0)" simple_bandb nil) (Maybe type-decl nil Maybe "structures/") (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (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/") (NOT const-decl "[bool -> bool]" booleans nil) (val adt-accessor-decl "[(some?) -> T]" Maybe "structures/") (IntervalOutput type-eq-decl nil interval_bandb nil) (Box type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (ProperBox type-eq-decl nil box nil) (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 nil) (alt_max const-decl "DirVar" interval_bandb nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) ([\|\|] const-decl "Interval" interval 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) (nnrat_exp application-judgement "nnrat" exponentiation nil) (vars_in_box_rec def-decl "{b: bool | b = (FORALL (k: subrange(i, n - 1)): vs(k) ## nth(box, k - i))}" box nil) (ub_interval formula-decl nil interval nil) (lb_interval formula-decl nil interval nil) (length_singleton formula-decl nil more_list_props "structures/") (vars_in_box formula-decl nil box nil) (iar_38 skolem-const-decl "(bimplies?)" examples nil) (real_plus_real_is_real application-judgement "real" reals nil) (eval def-decl "real" interval_expr nil) (beval def-decl "bool" interval_bexpr nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (x_39 skolem-const-decl "{x: real | x ## [|0, 2.39 * 10 ^ (-9)|]}" examples nil) (|##| const-decl "bool" interval nil) (list2array def-decl "T" array2list "structures/") (vars_in_box? const-decl "bool" box nil) (Env type-eq-decl nil box nil) (^ const-decl "real" exponentiation nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (sound? const-decl "bool" interval_bandb nil) (interval_soundness formula-decl nil interval_bandb nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (Interval type-eq-decl nil interval nil) (PRED type-eq-decl nil defined_types 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) (Inclusion? const-decl "bool" interval nil) (Precondition? const-decl "bool" interval nil) (PreTrue const-decl "(Precondition?)" interval_expr 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) (exp_safe const-decl "posreal" interval_expr_lnexp nil) (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 nil) (Exp const-decl "(Pos?)" interval_lnexp nil) (Fundamental? const-decl "bool" interval nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (Exp_Fundamental application-judgement "(Fundamental?(PreTrue))" interval_expr_lnexp nil) (Exp_Inclusion application-judgement "(Inclusion?(PreTrue, exp_safe))" interval_expr_lnexp nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers 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) (FUN adt-constructor-decl "[[pre: (Precondition?), opf: [real -> real], {F: [Interval -> Interval] | Inclusion?(pre, opf)(F) AND Fundamental?(pre)(F)}, RealExpr] -> (fun?)]" IntervalExpr_adt nil) (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]" IntervalExpr_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (r2E const-decl "RealExpr" interval_expr nil) (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]" IntervalExpr_adt nil) (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]" IntervalExpr_adt nil) (<= const-decl "bool" reals nil) (BREL adt-constructor-decl "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt nil) (RealOrder type-eq-decl nil real_orders "reals/") (realorder? const-decl "bool" real_orders "reals/") (/ 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) (X const-decl "RealExpr" interval_expr nil) (BINCLUDES adt-constructor-decl "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BIMPLIES adt-constructor-decl "[[BoolExpr, BoolExpr] -> (bimplies?)]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (IntervalExpr type-decl nil IntervalExpr_adt nil)) shostak)) (Tunnel_3_IL_LU 0 (Tunnel_3_IL_LU-1 nil 3600857801 ("" (interval) nil nil) ((posint_exp application-judgement "posint" exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (listn_0 name-judgement "listn[real](0)" simple_bandb nil) (Maybe type-decl nil Maybe "structures/") (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (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/") (NOT const-decl "[bool -> bool]" booleans nil) (val adt-accessor-decl "[(some?) -> T]" Maybe "structures/") (IntervalOutput type-eq-decl nil interval_bandb nil) (Box type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (ProperBox type-eq-decl nil box nil) (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 nil) (alt_max const-decl "DirVar" interval_bandb nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) ([\|\|] const-decl "Interval" interval 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) (nnrat_exp application-judgement "nnrat" exponentiation nil) (vars_in_box_rec def-decl "{b: bool | b = (FORALL (k: subrange(i, n - 1)): vs(k) ## nth(box, k - i))}" box nil) (ub_interval formula-decl nil interval nil) (lb_interval formula-decl nil interval nil) (length_singleton formula-decl nil more_list_props "structures/") (vars_in_box formula-decl nil box nil) (iar_40 skolem-const-decl "(bimplies?)" examples nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (eval def-decl "real" interval_expr nil) (beval def-decl "bool" interval_bexpr nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (x_41 skolem-const-decl "{x: real | x ## [|0, 8.17 * 10 ^ (-8)|]}" examples nil) (|##| const-decl "bool" interval nil) (list2array def-decl "T" array2list "structures/") (vars_in_box? const-decl "bool" box nil) (Env type-eq-decl nil box nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (^ const-decl "real" exponentiation nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (minus_even_is_even application-judgement "even_int" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (sound? const-decl "bool" interval_bandb nil) (interval_soundness formula-decl nil interval_bandb nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (Interval type-eq-decl nil interval nil) (PRED type-eq-decl nil defined_types 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) (Inclusion? const-decl "bool" interval nil) (Precondition? const-decl "bool" interval nil) (PreTrue const-decl "(Precondition?)" interval_expr 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) (exp_safe const-decl "posreal" interval_expr_lnexp nil) (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 nil) (Exp const-decl "(Pos?)" interval_lnexp nil) (Fundamental? const-decl "bool" interval nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (Exp_Fundamental application-judgement "(Fundamental?(PreTrue))" interval_expr_lnexp nil) (Exp_Inclusion application-judgement "(Inclusion?(PreTrue, exp_safe))" interval_expr_lnexp 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) (FUN adt-constructor-decl "[[pre: (Precondition?), opf: [real -> real], {F: [Interval -> Interval] | Inclusion?(pre, opf)(F) AND Fundamental?(pre)(F)}, RealExpr] -> (fun?)]" IntervalExpr_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (r2E const-decl "RealExpr" interval_expr nil) (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]" IntervalExpr_adt nil) (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]" IntervalExpr_adt nil) (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]" IntervalExpr_adt 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) (X const-decl "RealExpr" interval_expr nil) (BINCLUDES adt-constructor-decl "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt nil) (RealExpr type-eq-decl nil IntervalExpr_adt nil) (letin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (fun? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (div? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (pow? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sq? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (mult? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (sub? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (neg? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (abs? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (add? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (const? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BIMPLIES adt-constructor-decl "[[BoolExpr, BoolExpr] -> (bimplies?)]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (IntervalExpr type-decl nil IntervalExpr_adt nil)) shostak)))
¤ Dauer der Verarbeitung: 0.65 Sekunden (vorverarbeitet am 2026-04-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26