|
(simple_bandb
(altvar_TCC1 0
(altvar_TCC1-1 nil 3547136696
("" (skeep :preds? t) (("" (grind) nil nil)) nil)
((ProperBox? const-decl "bool" box nil)
(length def-decl "nat" list_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
nil))
(altvar_TCC2 0
(altvar_TCC2-1 nil 3547136696
("" (skeep :preds? t)
(("" (lemma "mod_pos")
(("" (inst?)
(("1" (assert) nil nil)
("2" (hide 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil)
((mod_pos formula-decl nil mod nil)
(mod const-decl "{k | abs(k) < abs(j)}" mod nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" real_orders "reals/")
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(DirVarStack type-eq-decl nil branch_and_bound "structures/")
(= const-decl "[T, T -> boolean]" equalities nil)
(stack type-eq-decl nil stack "structures/")
(DirVar type-eq-decl nil branch_and_bound "structures/")
(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)
(IntervalExpr type-decl nil IntervalExpr_adt nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(> const-decl "bool" reals nil)
(Interval type-eq-decl nil interval nil)
(list type-decl nil list_adt nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(length def-decl "nat" list_props nil)
(Box type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(ProperBox type-eq-decl nil box nil)
(box skolem-const-decl "ProperBox" simple_bandb nil)
(gt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(simple_interval_soundness 0
(simple_interval_soundness-2 nil 3579702999
("" (skeep)
(("" (lemma "b_and_b_id_sound")
(("" (expand "simple_interval")
(("" (inst?)
(("" (assert)
(("" (hide 2)
(("" (split)
(("1" (expand "accomodates?")
(("1" (skeep)
(("1" (expand "sound?")
(("1" (flatten)
(("1" (expand "evaluate")
(("1" (skeep)
(("1" (lemma "Eval_inclusion_Proper")
(("1"
(inst?)
(("1"
(beta)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "subdiv_presound?")
(("2" (skeep)
(("2" (expand "denorm")
(("2" (expand "branch")
(("2" (expand "subdivide")
(("2" (expand "sound?")
(("2" (flatten)
(("2"
(expand "combine")
(("2"
(use "Proper_Safe2")
(("2"
(assert)
(("2"
(flatten)
(("2"
(replaces -3)
(("2"
(assert)
(("2"
(skeep :preds? t)
(("2"
(inst - "vs")
(("2"
(rewrite
"Union_inclusion")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "subdiv_sound?")
(("3" (skeep)
(("3" (expand "denorm")
(("3" (expand "branch")
(("3" (expand "subdivide")
(("3" (expand "sound?")
(("3" (flatten)
(("3"
(expand "combine")
(("3"
(use "Proper_Safe2")
(("3"
(assert)
(("3"
(flatten)
(("3"
(replaces -3)
(("3"
(assert)
(("3"
(skeep :preds? t)
(("3"
(lemma
"split_vars_in_box")
(("3"
(inst? -1)
(("3"
(inst?)
(("3"
(beta)
(("3"
(split -1)
(("1"
(inst? -5)
(("1"
(rewrite
"Union_inclusion")
nil
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(inst? -6)
(("1"
(rewrite
"Union_inclusion")
nil
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(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)
(ProperBox type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(Box type-eq-decl nil box nil) (list type-decl nil list_adt nil)
(Interval type-eq-decl nil interval nil)
(real nonempty-type-from-decl nil reals 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)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(IntervalExpr type-decl nil IntervalExpr_adt nil)
(b_and_b_id_sound formula-decl nil branch_and_bound "structures/")
(Accumulator type-eq-decl nil branch_and_bound "structures/")
(accumulate const-decl "Interval" simple_bandb nil)
(Brancher type-eq-decl nil branch_and_bound "structures/")
(branch const-decl "[RealExpr, RealExpr]" simple_bandb nil)
(Combiner type-eq-decl nil branch_and_bound "structures/")
(combine const-decl "Interval" simple_bandb nil)
(DirVar type-eq-decl nil branch_and_bound "structures/")
(DenormAns type-eq-decl nil branch_and_bound "structures/")
(denorm const-decl "Interval" simple_bandb nil)
(Evaluator type-eq-decl nil branch_and_bound "structures/")
(evaluate const-decl "Interval" simple_bandb nil)
(stack type-eq-decl nil stack "structures/")
(= const-decl "[T, T -> boolean]" equalities nil)
(length def-decl "nat" list_props nil)
(DirVarStack type-eq-decl nil branch_and_bound "structures/")
(ExitPred type-eq-decl nil branch_and_bound "structures/")
(ge const-decl "bool" simple_bandb nil)
(LocalExitPred type-eq-decl nil branch_and_bound "structures/")
(le const-decl "bool" simple_bandb nil)
(prune const-decl "bool" simple_bandb nil)
(DirVarSelector type-eq-decl nil branch_and_bound "structures/")
(altvar const-decl "DirVar" simple_bandb nil)
(SoundPred type-eq-decl nil branch_and_bound "structures/")
(sound? const-decl "bool" simple_bandb nil)
(SubdivDomain type-eq-decl nil branch_and_bound "structures/")
(subdivide const-decl "[ProperBox, ProperBox]" simple_bandb nil)
(subdiv_sound? const-decl "bool" branch_and_bound "structures/")
(split_vars_in_box formula-decl nil interval_expr nil)
(vs skolem-const-decl "(vars_in_box?(dom))" simple_bandb nil)
(dom skolem-const-decl "ProperBox" simple_bandb nil)
(v skolem-const-decl "nat" simple_bandb nil)
(split def-decl "{lrb: [Box, Box] |
LET (lb, rb) = lrb IN
length(lb) = length(box) AND
length(rb) = length(box) AND
(FORALL (i: below(length(box))):
IF i = v
THEN nth(lb, i) = HalfLeft(nth(box, i)) AND
nth(rb, i) = HalfRight(nth(box, i))
ELSE nth(lb, i) = nth(box, i) AND nth(rb, i) = nth(box, i)
ENDIF)}" interval_expr nil)
(HalfRight const-decl "Interval" interval nil)
(HalfLeft const-decl "Interval" interval nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(subdiv_presound? const-decl "bool" branch_and_bound "structures/")
(Proper_Safe2 formula-decl nil safe_arith nil)
(Union const-decl "Interval" interval nil)
(Union_inclusion formula-decl nil interval nil)
(eval def-decl "real" interval_expr nil)
(split_Proper application-judgement "[ProperBox, ProperBox]"
interval_expr nil)
(accomodates? const-decl "bool" branch_and_bound "structures/")
(Eval_inclusion_Proper formula-decl nil interval_expr nil)
(Env type-eq-decl nil box nil)
(vars_in_box? const-decl "bool" box nil)
(simple_interval const-decl "Output" simple_bandb nil))
nil))
(simple_test 0
(simple_test-1 nil 3567532399
("" (skeep)
(("" (name-label "sia" "MULT(X(0),SUB(r2E(1),X(0)))" :hide? t)
((""
(eval-expr "simple_interval(9,sia,(: [|0,1|] :))" :safe? nil)
(("" (lemma "simple_interval_soundness")
(("" (inst? -1)
(("" (replaces -2)
(("" (beta -1)
(("" (expand "sound?" -1)
(("" (split -1)
(("1" (inst -1 "list2array(0)((:x:))")
(("1"
(invoke (case "%1 = %2") (! -1 1)
"(x * (1 - x))")
(("1" (replaces -1)
(("1" (decimalize -1 3) nil nil)) nil)
("2" (interval-eq__ "sia" 1) nil nil))
nil)
("2" (vars-in-box__) nil nil))
nil)
("2" (eval-formula) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((r2E const-decl "RealExpr" interval_expr nil)
(SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]"
IntervalExpr_adt nil)
(X const-decl "RealExpr" interval_expr 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)
(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)
(MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]"
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)
(bool nonempty-type-eq-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(IntervalExpr type-decl nil IntervalExpr_adt nil)
(simple_interval_soundness formula-decl nil simple_bandb nil)
(sound? const-decl "bool" simple_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)
(PRED type-eq-decl nil defined_types nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(list2array def-decl "T" array2list "structures/")
(x skolem-const-decl "real" simple_bandb nil)
(sia skolem-const-decl "(mult?)" simple_bandb nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(|##| const-decl "bool" 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/")
(real_times_real_is_real application-judgement "real" reals nil)
(eval def-decl "real" interval_expr nil)
(length def-decl "nat" list_props nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(vars_in_box_rec def-decl
"{b: bool | b = (FORALL (k: subrange(i, n - 1)): vs(k) ## nth(box, k - i))}"
box nil)
(length_singleton formula-decl nil more_list_props "structures/")
(vars_in_box formula-decl nil box nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(Interval type-eq-decl nil interval nil)
(list type-decl nil list_adt nil) (Box type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(ProperBox type-eq-decl nil box nil)
(Output type-eq-decl nil branch_and_bound "structures/")
(simple_interval const-decl "Output" simple_bandb nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
([\|\|] const-decl "Interval" interval nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(null adt-constructor-decl "(null?)" list_adt nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(FALSE const-decl "bool" booleans nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil))
shostak)))
¤ Dauer der Verarbeitung: 0.29 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.
|
