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