|
(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)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.50 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.
|
