Quelle branch_and_bound_X.prf
Sprache: Lisp
(branch_and_bound_Xnil 3546959448 ("" (grind) nil nil )"nat" list_props nil )) nil ))nil 3546943024 ("" (grind) nil nil )"DirVarStack" branch_and_bound_X nil ))nil 3546959497"" (skeep :preds? t)"" (typepred "stack(dirvars)" ) (("" (grind) nil nil )) nil )) nil )"bool" branch_and_bound_X nil )nil branch_and_bound_X nil )nil stack nil )"nat" list_props nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil list_adt nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )"[T, T -> boolean]" equalities nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"Maybe[T]" stack nil )"(strict_total_order?[real])" real_props nil ))nil )nil 3546959448 ("" (subtype-tcc) nil nil ) nil nil ))nil 3546959526"" (skeep)"" (typepred "stack(dirvars)" ) (("" (grind) nil nil )) nil )) nil )nil branch_and_bound_X nil )nil stack nil )"nat" list_props nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil list_adt nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )"[T, T -> boolean]" equalities nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"posint" nil )"posint" nil )"stack" stack nil ))nil )nil 3546959448 ("" (subtype-tcc) nil nil ) nil nil ))nil 3546959448 ("" (grind) nil nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"stack" stack nil )"bool" branch_and_bound_X nil ))nil ))nil 3546959448 ("" (subtype-tcc) nil nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3546959629"" (skeep)"" (typepred "stack(dirvars)" )"" (expand "length" -1) (("" (grind) nil nil )) nil )) nil ))nil )nil branch_and_bound_X nil )nil stack nil )"nat" list_props nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil list_adt nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )"[T, T -> boolean]" equalities nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"int" integers nil )"stack" stack nil )"posint" nil ))nil )nil 3546959448 ("" (subtype-tcc) nil nil ) nil nil ))nil 3521295757 ("" (subtype-tcc) nil nil )nil nil ))nil 3521298539 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil list_adt nil )nil stack nil )"[T, T -> boolean]" equalities nil )"nat" list_props nil )nil branch_and_bound_X nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil ))nil 3521298539"" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil list_adt nil )nil stack nil )"[T, T -> boolean]" equalities nil )"nat" list_props nil )nil branch_and_bound_X nil )"int" integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"posint" nil )"stack" stack nil )"(nonempty?)" branch_and_bound_X nil ))nil ))nil 3546942913 ("" (subtype-tcc) nil nil )"stack" stack nil )"(nonempty?)" branch_and_bound_X nil )"int" integers nil ))nil ))nil 3546942913"" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil list_adt nil )nil stack nil )"[T, T -> boolean]" equalities nil )"nat" list_props nil )nil branch_and_bound_X nil )"int" integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"posint" nil )"stack" stack nil )"(nonempty?)" branch_and_bound_X nil ))nil ))nil 3547374379"" (termination-tcc) nil nil )"stack" stack nil )"(nonempty?)" branch_and_bound_X nil )"int" integers nil ))nil ))nil 3571414984"" (skeep)"" "PP" "(evaluate, branch, subdivide, " nil )"" (decompose-equality -1)"" case " FORALL (obj, dom, acc, dirvars,(depth:nat)): LET bandb = branch_and_bound(PP)(obj, dom, acc, dirvars)") "1" (skeep)"1" (inst? -)"1" (inst - "maxdepth-length(dirvars)" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (induct "depth" )"1" (assert ) nil nil )"2" (skeep)"2" (move-terms -1 r 2)"2" (assert )"2" (expand "branch_and_bound" )"2" (expand "sound_evaluate?" )"2" (inst - "dom" "obj" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"3" (skolem 1 "depth" )"3" (flatten)"3" (skeep)"3" "bandb" "branch_and_bound(PP)(obj, dom, acc,dirvars)" nil )"3" expand "branch_and_bound" -1 :assert ? none)"3" "PP" "3" (replaces "PP" :dir rl)"3" (skoletin* -1)"3" "HI" -6)"3" "HI" )"3" expand "sound_evaluate?" )"3" "dom" "obj" )"3" "length(dirvars) = maxdepth OR le(thisans) OR thisout`exit OR prune(dirvars, newacc1, thisans)" )"1" (assert ) nil nil )"2" "2" "2" "p" )"2" "2" "2" "firstout`exit" )"1" "1" assert )"1" expand "presound_combine?" )"1" "1" assert )"1" "1" case "sound(dom1,sp1,branch_and_bound(PP)(sp1,dom1,newacc1,pushDirVar((dirp, vp), dirvars))`ans)" )"1" expand "PP" )"1" "1" expand "sound_subdivide?" )"1" expand "le_subdivide?" )"1" "dom1" "dom" "obj" "vp" )"1" replace "1" replace "1" "1" expand "sound_branch?" )"1" "dom1" "obj" "nobj" "vp" )"1" assert )"1" "1" expand "sound_dir" )"1" "1" "1" assert )"1" replace "1" nil )"1" "1" expand "presound_evaluate?" )"1" "dom1" "branch(vp,nobj)`1" "branch(vp,obj)`1" "firstout`ans" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" replace "2" nil )"2" "2" expand "presound_evaluate?" )"2" "dom1" "branch(vp,nobj)`2" "branch(vp,obj)`2" "firstout`ans" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "HI" )"2" "2" assert )"2" expand "pushDirVar" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "PP" )"3" expand "pushDirVar" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" assert )"1" case "FORALL(accl,accr:AccType):sound(dom,obj,combine(vp, ") "1" expand "PP" )"1" case "dirp" )"1" assert )"1" "newacc1" "newacc2" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" "newacc2" "newacc1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "sound_combine?" )"2" "2" assert )"2" "2" replace "2" "HI" )"2" "1" "1" "1" "BAB" "branch_and_bound(PP) ") "1" replace "1" expand "sound_subdivide?" )"1" "domsplit`1" "dom" "obj" "vp" )"1" "1" expand "le_subdivide?" )"1" expand "sound_branch?" )"1" "domsplit`1" "obj" "nobj" "vp" )"1" assert )"1" "1" "1" expand "presound_evaluate?" )"1" "domsplit`1" "branch(vp,nobj)`1" "branch(vp,obj)`1" "BAB" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "pushDirVar" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "BAB" "branch_and_bound(PP) ") "1" replace "1" expand "sound_subdivide?" )"1" "domsplit`2" "dom" "obj" "vp" )"1" expand "le_subdivide?" )"1" "1" expand "sound_branch?" )"1" "domsplit`2" "obj" "nobj" "vp" )"1" assert )"1" "1" "1" expand "presound_evaluate?" )"1" "domsplit`2" "branch(vp,nobj)`2" "branch(vp,obj)`2" "BAB" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "pushDirVar" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "PP" )"3" expand "pushDirVar" "3" assert )nil nil ))nil ))nil )"4" expand "PP" )"4" expand "pushDirVar" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skosimp*) (("4" (assert ) nil nil )) nil )) nil ))nil ))nil )"3" (hide 2)"3" (skosimp*) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil booleans nil )nil booleans nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil naturalnumbers nil )nil list_adt nil )nil stack nil )nil numbers nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )"nat" list_props nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )"Output" branch_and_bound_X nil )"bool" reals nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )nil branch_and_bound_X nil )nil Maybe nil )"int" integers nil )"(total_order?[real])" nil )"DirVarStack" branch_and_bound_X nil )"nat" branch_and_bound_X nil )"(total_order?[real])" nil )"[Evaluator, Brancher, SubdivDomain, DenormAns, Combiner, ExitPred, " nil )nil defined_types nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )"[bool, bool -> bool]" booleans nil )"nonneg_int" nil )"bool" branch_and_bound_X nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"{k: nat | i <= k AND j <= k}" nil )"posint" nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )"[T -> (some?)]" Maybe nil )"(nonempty?)" branch_and_bound_X nil )"bool" branch_and_bound_X nil )nil naturalnumbers nil )"[(some?) -> T]" Maybe nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[Maybe -> boolean]" Maybe nil )"[Maybe -> boolean]" Maybe nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" booleans nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"(strict_total_order?[real])" real_props nil )"stack" stack nil )"bool" branch_and_bound_X nil )"bool" branch_and_bound_X nil )"posint" nil )"bool" branch_and_bound_X nil )"bool" branch_and_bound_X nil )"bool" branch_and_bound_X nil )"bool" branch_and_bound_X nil )"bool" branch_and_bound_X nil )"int" integers nil )AND const-decl "[bool, bool -> bool]" booleans nil ))nil )nil 3571414643"" (skeep)"" "PP" "(evaluate, branch, subdivide, " nil )"" (decompose-equality -1)"" case " FORALL (obj, dom, acc, dirvars,(depth:nat)): LET bandb = branch_and_bound(PP)(obj, dom, acc, dirvars)") "1" (skeep)"1" (inst? -)"1" (inst - "maxdepth-length(dirvars)" )"1" (assert ) nil )))))))"2" (hide 2)"2" (induct "depth" )"1" (assert ) nil )"2" (skeep)"2" (move-terms -1 r 2)"2" (assert )"2" (expand "branch_and_bound" )"2" (expand "sound_subdivide?" )"2" (inst - "dom" "obj" )"2" (flatten)"2" (assert ) nil )))))))))))))))"3" (skolem 1 "depth" )"3" (flatten)"3" (skeep)"3" "bandb" "branch_and_bound(PP)(obj, dom, acc,dirvars)" nil )"3" expand "branch_and_bound" -1 :assert ? none)"3" "PP" "3" (replaces "PP" :dir rl)"3" (skoletin* -1)"3" "HI" -6)"3" "HI" )"3" expand "sound_subdivide?" )"3" "dom" "obj" )"3" "3" "length(dirvars) = maxdepth OR le(thisans) OR thisout`exit OR prune(dirvars, newacc1, thisans)" )"1" (assert ) nil )"2" "2" "2" "p" )"2" "2" "vp" )"2" "2" nil "2" "2" nil )"2" "firstout`exit" )"1" "1" assert )"1" expand "presound_combine?" )"1" "1" assert )"1" "1" case "sound(dom1,sp1,branch_and_bound(PP)(sp1,dom1,newacc1,pushDirVar((dirp, vp), dirvars))`ans)" )"1" expand "PP" )"1" "1" replace "1" expand "sound_dir" )"1" "1" "1" assert )"1" "1" "1" "1" nil )))))))))))"2" "2" assert )"2" "2" "2" "2" nil )))))))))))))))))))))"2" "2" "HI" )"2" "2" assert )"2" expand "pushDirVar" "2" assert )nil )))))))))))"3" expand "PP" )"3" expand "pushDirVar" "3" assert )nil )))))))))))))))))))"2" "2" "2" "2" assert )"2" case "FORALL(accl,accr:AccType):sound(dom,obj,combine(vp, ") "1" expand "PP" )"1" case "dirp" )"1" assert )"1" "newacc1" "newacc2" )"1" assert )nil )))))"2" assert )"2" "newacc2" "newacc1" )"2" assert )nil )))))))))"2" "2" "2" expand "sound_combine?" )"2" "2" assert )"2" "2" replace "2" "HI" )"2" "1" "1" "1" "BAB" "branch_and_bound(PP) ") "1" "1" "1" nil )))))))"2" expand "pushDirVar" "2" assert )nil )))))))"2" "2" "1" "BAB" "branch_and_bound(PP) ") "1" "1" "1" nil )))))))"2" expand "pushDirVar" "2" assert )nil )))))))))))))))))))))))))"3" expand "PP" )"3" expand "pushDirVar" "3" assert )nil )))))"4" expand "PP" )"4" expand "pushDirVar" "4" assert )nil )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))"4" (hide 2) (("4" (skeep) (("4" (assert ) nil )))))))))"3" (hide 2) (("3" (skeep) (("3" (assert ) nil ))))))))))))nil )nil nil )nil 3571414554"" (skeep)"" "PP" "(evaluate, branch, subdivide, " nil )"" (decompose-equality -1)"" case " FORALL (obj, dom, acc, dirvars,(depth:nat)): LET bandb = branch_and_bound(PP)(obj, dom, acc, dirvars)") "1" (skeep)"1" (inst? -)"1" (inst - "maxdepth-length(dirvars)" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (induct "depth" )"1" (assert ) nil nil )"2" (skeep)"2" (move-terms -1 r 2)"2" (assert )"2" (expand "branch_and_bound" )"2" (expand "sound_subdivide?" )"2" (inst - "dom" "obj" )"2" (flatten) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skolem 1 "depth" )"3" (flatten)"3" (skeep)"3" "bandb" "branch_and_bound(PP)(obj, dom, acc,dirvars)" nil )"3" expand "branch_and_bound" -1 :assert ? none)"3" "PP" "3" (replaces "PP" :dir rl)"3" (skoletin* -1)"3" "HI" -6)"3" "HI" )"3" expand "sound_subdivide?" )"3" "dom" "obj" )"3" "3" "length(dirvars) = maxdepth OR le(thisans) OR thisout`exit OR prune(dirvars, newacc1, thisans)" )"1" (assert ) nil nil )"2" "2" "2" "p" )"2" "2" "vp" )"2" "2" nil "2" "2" nil )"2" "firstout`exit" )"1" "1" assert )"1" expand "presound_combine?" )"1" "1" assert )"1" "1" case "sound(dom1,sp1,branch_and_bound(PP)(sp1,dom1,newacc1,pushDirVar((dirp, vp), dirvars))`ans)" )"1" expand "PP" )"1" "1" replace "1" expand "sound_dir" )"1" "1" "1" assert )"1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "HI" )"2" "2" assert )"2" expand "pushDirVar" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "PP" )"3" expand "pushDirVar" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" assert )"2" case "FORALL(accl,accr:AccType):sound(dom,obj,combine(vp, ") "1" expand "PP" )"1" case "dirp" )"1" assert )"1" "newacc1" "newacc2" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" "newacc2" "newacc1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "subdiv_sound?" )"2" "2" assert )"2" "2" replace "2" "HI" )"2" "1" "1" "1" "BAB" "branch_and_bound(PP) ") "1" "1" "1" nil nil ))nil ))nil ))nil )"2" expand "pushDirVar" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "BAB" "branch_and_bound(PP) ") "1" "1" "1" nil nil ))nil ))nil ))nil )"2" expand "pushDirVar" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "PP" )"3" expand "pushDirVar" "3" assert )nil nil ))nil ))nil )"4" expand "PP" )"4" expand "pushDirVar" "4" 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 ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skeep) (("4" (assert ) nil nil )) nil )) nil ))nil ))nil )"3" (hide 2) (("3" (skeep) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil 3571413876"" (skeep)"" "PP" "(evaluate, branch, subdivide, " nil )"" (decompose-equality -1)"" case " FORALL (obj, dom, acc, dirvars,(depth:nat)): LET bandb = branch_and_bound(PP)(obj, dom, acc, dirvars)") "1" (skeep)"1" (inst? -)"1" (inst - "maxdepth-length(dirvars)" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (induct "depth" )"1" (assert ) nil nil )"2" (skeep)"2" (move-terms -1 r 2)"2" (assert )"2" (expand "branch_and_bound" )"2" (expand "sound_subdivide?" )"2" (inst - "dom" "obj" )"2" (flatten) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skolem 1 "depth" )"3" (flatten)"3" (skeep)"3" "bandb" "branch_and_bound(PP)(obj, dom, acc,dirvars)" nil )"3" expand "branch_and_bound" -1 :assert ? none)"3" "PP" "3" (replaces "PP" :dir rl)"3" (skoletin* -1)"3" "HI" -6)"3" "HI" )"3" expand "sound_subdivide?" )"3" "dom" "obj" )"3" "3" "length(dirvars) = maxdepth OR le(thisans) OR thisout`exit OR prune(dirvars, newacc1, thisans)" )"1" (assert ) nil nil )"2" "2" "2" "p" )"2" "2" "vp" )"2" "2" nil "2" "2" nil )"2" "firstout`exit" )"1" "1" assert )"1" expand "subdiv_presound?" )"1" "1" assert )"1" "1" case "sound(dom1,sp1,branch_and_bound(PP)(sp1,dom1,newacc1,pushDirVar((dirp, vp), dirvars))`ans)" )"1" expand "PP" )"1" "1" replace "1" expand "sound_dir" )"1" "1" "1" assert )"1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "HI" )"2" "2" assert )"2" expand "pushDirVar" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "PP" )"3" expand "pushDirVar" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" assert )"2" case "FORALL(accl,accr:AccType):sound(dom,obj,combine(vp, ") "1" expand "PP" )"1" case "dirp" )"1" assert )"1" "newacc1" "newacc2" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" "newacc2" "newacc1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "subdiv_sound?" )"2" "2" assert )"2" "2" replace "2" "HI" )"2" "1" "1" "1" "BAB" "branch_and_bound(PP) ") "1" "1" "1" nil nil ))nil ))nil ))nil )"2" expand "pushDirVar" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "BAB" "branch_and_bound(PP) ") "1" "1" "1" nil nil ))nil ))nil ))nil )"2" expand "pushDirVar" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "PP" )"3" expand "pushDirVar" "3" assert )nil nil ))nil ))nil )"4" expand "PP" )"4" expand "pushDirVar" "4" 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 ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skeep) (("4" (assert ) nil nil )) nil )) nil ))nil ))nil )"3" (hide 2) (("3" (skeep) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil 3571412230"" (skeep)"" "PP" "(evaluate, branch, subdivide, " nil )"" (decompose-equality -1)"" case " FORALL (obj, dom, acc, dirvars,(depth:nat)): LET bandb = branch_and_bound(PP)(obj, dom, acc, dirvars)") "1" (skeep)"1" (inst? -)"1" (inst - "maxdepth-length(dirvars)" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (induct "depth" )"1" (assert ) nil nil )"2" (skeep)"2" (move-terms -1 r 2)"2" (assert )"2" (expand "branch_and_bound" )"2" (expand "accomodates?" )"2" (inst - "dom" "obj" )"2" (flatten) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skolem 1 "depth" )"3" (flatten)"3" (skeep)"3" "bandb" "branch_and_bound(PP)(obj, dom, acc,dirvars)" nil )"3" expand "branch_and_bound" -1 :assert ? none)"3" "PP" "3" (replaces "PP" :dir rl)"3" (skoletin* -1)"3" "HI" -6)"3" "HI" )"3" expand "accomodates?" )"3" "dom" "obj" )"3" "3" "length(dirvars) = maxdepth OR le(thisans) OR thisout`exit OR prune(dirvars, newacc1, thisans)" )"1" (assert ) nil nil )"2" "2" "2" "p" )"2" "2" "vp" )"2" "2" nil "2" "2" nil )"2" "firstout`exit" )"1" "1" assert )"1" expand "subdiv_presound?" )"1" "1" assert )"1" "1" case "sound(dom1,sp1,branch_and_bound(PP)(sp1,dom1,newacc1,pushDirVar((dirp, vp), dirvars))`ans)" )"1" expand "PP" )"1" "1" replace "1" expand "sound_dir" )"1" "1" "1" assert )"1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "HI" )"2" "2" assert )"2" expand "pushDirVar" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "PP" )"3" expand "pushDirVar" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" assert )"2" case "FORALL(accl,accr:AccType):sound(dom,obj,combine(vp, ") "1" expand "PP" )"1" case "dirp" )"1" assert )"1" "newacc1" "newacc2" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" "newacc2" "newacc1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "subdiv_sound?" )"2" "2" assert )"2" "2" replace "2" "HI" )"2" "1" "1" "1" "BAB" "branch_and_bound(PP) ") "1" "1" "1" nil nil ))nil ))nil ))nil )"2" expand "pushDirVar" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "BAB" "branch_and_bound(PP) ") "1" "1" "1" nil nil ))nil ))nil ))nil )"2" expand "pushDirVar" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "PP" )"3" expand "pushDirVar" "3" assert )nil nil ))nil ))nil )"4" expand "PP" )"4" expand "pushDirVar" "4" 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 ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skeep) (("4" (assert ) nil nil )) nil )) nil ))nil ))nil )"3" (hide 2) (("3" (skeep) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil 3546959685"" (skeep)"" "PP" "(evaluate, branch, subdivide, " nil )"" (decompose-equality -1)"" case " FORALL (obj, dom, acc, dirvars,(depth:nat)): LET bandb = branch_and_bound(PP)(obj, dom, acc, dirvars)") "1" (skeep)"1" (inst? -)"1" (inst - "maxdepth-length(dirvars)" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (induct "depth" )"1" (assert ) nil nil )"2" (skeep)"2" (move-terms -1 r 2)"2" (assert )"2" (expand "branch_and_bound" )"2" (expand "accomodates?" )"2" (inst - "dom" "obj" )"2" (flatten) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skolem 1 "depth" )"3" (flatten)"3" (skeep)"3" "bandb" "branch_and_bound(PP)(obj, dom, acc,dirvars)" nil )"3" expand "branch_and_bound" -1 :assert ? none)"3" "PP" "3" (replaces "PP" :dir rl)"3" (skoletin* -1)"3" "HI" -6)"3" "HI" )"3" expand "accomodates?" )"3" "dom" "obj" )"3" "3" "length(dirvars) = maxdepth OR le(thisans) OR thisout`exit OR prune(dirvars, newacc1, thisans)" )"1" (assert ) nil nil )"2" "2" "2" "p" )"2" "2" "vp" )"2" "2" nil "2" "2" nil )"2" "firstout`exit" )"1" "1" assert )"1" expand "subdiv_presound?" )"1" "1" assert )"1" "1" case "sound(dom1,sp1,branch_and_bound(PP)(sp1,dom1,newacc1,pushDirVar((dirp, vp), dirvars))`ans)" )"1" expand "PP" )"1" "1" replace "1" expand "sound_dir" )"1" "1" "1" assert )"1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "HI" )"2" "2" assert )"2" expand "pushDirVar" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "PP" )"3" expand "pushDirVar" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" assert )"2" case "FORALL(accl,accr:AccType):sound(dom,obj,combine(vp, ") "1" expand "PP" )"1" case "dirp" )"1" assert )"1" "newacc1" "newacc2" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" "newacc2" "newacc1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "subdiv_sound?" )"2" "2" assert )"2" "2" replace "2" "HI" )"2" "1" "1" "1" "BAB" "branch_and_bound(PP) ") "1" "1" nil nil ))nil ))nil )"2" expand "pushDirVar" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "BAB" "branch_and_bound(PP) ") "1" nil nil ))nil )"2" expand "pushDirVar" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "PP" )"3" expand "pushDirVar" )"3" assert )nil nil ))nil ))nil )"4" expand "PP" )"4" expand "pushDirVar" )"4" 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 ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skeep) (("4" (assert ) nil nil )) nil )) nil ))nil ))nil )"3" (hide 2) (("3" (skeep) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil stack nil ) (Maybe type-decl nil Maybe nil )"[T -> (some?)]" Maybe nil )"[(some?) -> T]" Maybe nil )"[Maybe -> boolean]" Maybe nil )"[Maybe -> boolean]" Maybe nil )"stack" stack nil ))nil )nil 3546361375"" (skeep)"" "PP" "(simplify, evaluate, branch, subdivide, " :hide? nil )"" (decompose-equality -1)"" case " FORALL (obj, dom, acc, dirvars,(depth:nat)): LET bandb = branch_and_bound(PP)(obj, dom, acc, dirvars)") "1" (skeep)"1" (inst? -)"1" (inst - "maxdepth-length(dirvars)" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (induct "depth" )"1" (assert ) nil nil )"2" (skeep)"2" (move-terms -1 r 2)"2" (assert )"2" (expand "branch_and_bound" )"2" (expand "accomodates?" )"2" (inst - "dom" "obj" "dirvars" )"2" (expand "evaluate_simplify?" )"2" (inst - "dom" "obj" "dirvars" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skolem 1 "depth" )"3" (flatten)"3" (skeep)"3" "bandb" "branch_and_bound(PP)(obj, dom, acc,dirvars)" nil )"3" expand "branch_and_bound" -1 :assert ? none)"3" "PP" "3" (replaces "PP" :hide? nil :dir rl)"3" (skoletin* -1)"3" "length(dirvars) = maxdepth OR OR OR prune(dirvars, acc, thisans)") "1" "1" "1" assert )"1" "1" expand "accomodates?" )"1" "dom" "obj" "dirvars" )"1" expand "evaluate_simplify?" )"1" "dom" "obj" "dirvars" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace 1)"2" replace 2)"2" replace 3)"2" replace 4)"2" "p" )"2" "2" case "firstout`exit" )"1" assert )"1" "1" assert )"1" expand "subdiv_presound?" )"1" "1" assert )"1" "1" "1" expand "accomodates?" )"1" "dom" "obj" "dirvars" )"1" expand "evaluate_simplify?" )"1" "dom" "obj" "dirvars" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" case "sound(dom1,sp1,branch_and_bound(PP)(sp1,dom1,newacc1,push((dirp, vp), dirvars))`ans)" )"1" expand "sound_dir" )"1" "1" "1" assert )"1" expand "branch_simplify?" )"1" "1" expand "simplify_invariant?" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "branch_simplify?" )"2" "2" expand "simplify_invariant?" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" expand "push" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" expand "push" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1)"2" "2" "2" assert )"2" case "FORALL(accl,accr:AccType):sound(dom,obj,combine(vp, ") "1" case "dirp" )"1" assert )"1" "newacc1" "newacc2" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" "newacc2" "newacc1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" expand "subdiv_sound?" )"2" "2" assert )"2" "2" expand "branch_simplify?" )"2" "vp" "obj" )"2" "2" assert )"2" "1" expand "simplify_invariant?" "1" "1" assert )"1" "1" "simplify(branch(vp, obj)`1)" "subdivide(vp, dom)`1" "accl" "push((TRUE, vp), dirvars)" )"1" assert )"1" expand "push" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "simplify_invariant?" "2" "2" assert )"2" "2" "simplify(branch(vp, obj)`2)" "subdivide(vp, dom)`2" "accr" "push((FALSE, vp), dirvars)" )"2" assert )"2" expand "push" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "push" "3" assert )nil nil ))nil )"4" expand "push" "4" 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 )"4" (hide 2)"4" (skosimp*) (("4" (assert ) nil nil )) nil )) nil ))nil ))nil )"3" (hide 2)"3" (skosimp*) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil stack nil )) nil )nil 3546178611"" (skeep)"" "PP" "(simplify, evaluate, branch, subdivide, " :hide? nil) "" (decompose-equality -1)"" case " FORALL (obj, dom, depth, ans0, dirvars): LET bandb = branch_and_bound(PP)(obj, dom, maxdepth-depth, ans0, dirvars)") "1" (skeep)"1" (inst? -)"1" (inst - "maxdepth-depth" "ans0" "dirvars" )"1" (assert ) nil nil )"2" (hide 2) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "depth" )"1" (assert ) nil nil )"2" (assert )"2" (skeep)"2" (expand "branch_and_bound" )"2" (expand "accomodates?" )"2" (inst - "dom" "obj" "dirvars" )"2" (expand "evaluate_simplify?" )"2" (inst - "dom" "obj" "dirvars" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skolem 1 "depth" )"3" (flatten)"3" (skeep)"3" "bandb" "branch_and_bound(PP)(obj, dom, maxdepth - (depth + 1), ans0,dirvars)" nil )"1" expand "branch_and_bound" -1 :assert ? none)"1" "PP" "1" (replaces "PP" :hide? nil :dir rl)"1" (skoletin* -1)"1" "maxdepth - (depth + 1) = maxdepth OR OR OR (some?(ans0) AND prune(some(ans0), thisout`ans))") "1" "1" "1" assert )"1" "1" expand "accomodates?" )"1" "dom" "obj" "dirvars" )"1" expand "evaluate_simplify?" )"1" "dom" "obj" "dirvars" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace 1)"2" replace 2)"2" replace 3)"2" replace 4)"2" "p" )"2" "2" case "ge(firstout)" )"1" assert )"1" "1" assert )"1" expand "comb_sound_presound?" )"1" "1" assert )"1" "1" "1" "1" replace "1" expand "accomodates?" )"1" "1" "dom" "obj" "dirvars" )"1" expand "evaluate_simplify?" )"1" "dom" "obj" "dirvars" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "subdiv_presound?" "2" "2" assert )"2" "2" "2" "2" case "sound(dom1,sp1,branch_and_bound(PP)(sp1,dom1,depth_1,Some(newans1),push((dirp, vp), dirvars))`ans)" )"1" "1" "1" expand "sound_dir" )"1" "1" "1" assert )"1" "1" "1" expand "branch_simplify?" )"1" "1" expand "simplify_invariant?" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "2" expand "branch_simplify?" )"2" "2" expand "simplify_invariant?" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "2" "push((dirp,vp),dirvars)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1)"2" "2" "2" assert )"2" case "FORALL(ansl,ansr:Maybe[AnsType]):sound(dom,obj,comb(vp, ") "1" case "dirp" )"1" assert )"1" "newans1" "newans2" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" "newans2" "newans1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" expand "subdiv_sound?" )"2" "2" assert )"2" "2" expand "branch_simplify?" )"2" "vp" "obj" )"2" "2" assert )"2" "1" expand "simplify_invariant?" "1" "1" assert )"1" "1" "simplify(branch(vp, obj)`1)" "subdivide(vp, dom)`1" "ansl" "push((TRUE, vp), dirvars)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "simplify_invariant?" "2" "2" assert )"2" "2" "simplify(branch(vp, obj)`2)" "subdivide(vp, dom)`2" "ansr" "push((FALSE, vp), dirvars)" )"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 ))nil ))nil )"3" (assert ) nil nil )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skosimp*) (("4" (assert ) nil nil )) nil )) nil ))nil ))nil )"3" (hide 2)"3" (skosimp*) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil stack nil )"stack" stack nil ))nil ))nil 3546341495 ("" (subtype-tcc) nil nil )"DirVarStack" branch_and_bound_X nil ))nil ))nil 3546341520"" (skeep)"" (expand "b_and_b" )"" (lemma "branch_and_bound_sound" )"" (inst? -)"" (inst? -)"" (assert ) (("" (inst? -) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"Output" branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil booleans nil )nil booleans nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil naturalnumbers nil )nil list_adt nil )nil stack nil )nil numbers nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )"nat" list_props nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil )"(total_order?[real])" nil )nil Maybe nil )nil branch_and_bound_X nil )"[Maybe -> boolean]" Maybe nil )"(none?)" Maybe nil )"DirVarStack" branch_and_bound_X nil )nil branch_and_bound_X nil )nil branch_and_bound_X nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.308 Sekunden
(vorverarbeitet am 2026-04-28)
¤ *© Formatika GbR, Deutschland
2026-05-26
