SSL vs_bands.prf
Interaktion und
(vs_bandsnil 3477244353"" (skeep)"" (split +)"1" (flatten)"1" (split -)"1" (flatten)"1" (replace -1)"1" (hide -1)"1" (replace -1)"1" (hide -1)"1" (expand "abs" )"1" (lift-if)"1" (split -2)"1" (flatten)"1" (neg-formula -2)"1" replace -1)"1" case "vsp - viz < 0" )"1" case "sz + B*(vsp-viz) > -H" )"1" "1" expand "conflict_vertical?" )"1" "B" )"1" case "sz + B*(vsp-viz) >= H" )"1" "newt" "-sz/(vsp-viz)" )"1" case "B <= newt and newt <= T" )"1" "1" "newt" )"1" case "sz + newt*(vsp-viz) = 0" )"1" assert )nil )"2" replace "2" "const3" "vsp-viz" )"2" replace "2" "-" "sz" "1" assert )"1" nil )))"2" assert )nil )))))))))))"2" assert )nil )))))"2" replace -1 :dir rl)"2" "1" "1" "T" )"1" "viz-vsp" )"1" assert )nil )))))))"2" "2" "T" )"2" "viz-vsp" )"2" assert )nil )))))))))))))"2" (assert ) nil )))"2" expand "abs" 2)"2" "2" nil )))))))))))))"2" "T-B" )"2" (assert ) nil )))))"2" "H" )"2" "H" )"2" (assert ) nil )))))))))))))"2" (flatten)"2" (replace -1)"2" case "vsp > viz" )"1" case "sz + B*(vsp-viz) < H" )"1" "1" "1" expand "conflict_vertical?" )"1" "B" )"1" case "sz + B*(vsp-viz) <= -H" )"1" "newt" "-sz/(vsp-viz)" )"1" case "B <= newt and newt <= T" )"1" "1" "newt" )"1" case "sz + newt*(vsp-viz) = 0" )"1" assert )nil )"2" replace "2" "const3" "vsp-viz" )"2" replace "2" "-" "sz" "1" assert )"1" nil )))"2" assert )nil )))))))))))"2" assert )nil )))))"2" replace -1 :dir rl)"2" "1" "1" "T" )"1" "vsp-viz" )"1" assert )nil )))))))"2" "2" "T" )"2" "vsp-viz" )"2" assert )nil )))))))))))))"2" (assert ) nil )))"2" expand "abs" 2)"2" "2" nil )))))))"2" (assert ) nil )))))))))"2" "T" )"2" "vsp-viz" )"2" (assert ) nil )))))))"2" "H" )"2" "H" )"2" assert )nil )))))))))))))))))))))))))))"2" (flatten)"2" (replace -1)"2" (hide -1)"2" (replace -1)"2" (hide -1)"2" (expand "abs" )"2" (lift-if)"2" (split -)"1" (flatten)"1" (neg-formula -2)"1" replace -1)"1" case "vsp>viz" )"1" case "sz + T*(vsp-viz) > -H" )"1" "1" expand "conflict_vertical?" )"1" "T" )"1" case "sz + T*(vsp-viz) >= H" )"1" "newt" "-sz/(vsp-viz)" )"1" case "B <= newt and newt <= T" )"1" "1" case "sz + newt*(vsp-viz) = 0" )"1" "newt" )"1" assert )nil )"2" assert )nil )))"2" replace "2" "const3" "vsp-viz" )"2" replace -1)"2" "-" "sz" "1" assert )"1" nil )))"2" assert )nil )))))))))))))"2" replace -1 :dir rl)"2" "1" "1" "T" )"1" "vsp-viz" )"1" assert )nil )))))))"2" "2" "T" )"2" "vsp-viz" )"2" assert )nil )))))))))))))"2" (assert ) nil )))"2" expand "abs" 2)"2" "2" nil )))))))"2" (assert ) nil )))))))"2" "T" )"2" "vsp-viz" )"2" (assert ) nil )))))))"2" "H" )"2" "H" )"2" (assert ) nil )))))))))))))"2" (flatten)"2" (replace -1)"2" "2" case "vsp < viz" )"1" case "sz + T*(vsp-viz) < H" )"1" "1" expand "conflict_vertical?" )"1" "T" )"1" case "sz + T*(vsp-viz) <= -H" )"1" "newt" "-sz/(vsp-viz)" )"1" case "B <= newt and newt <= T" )"1" "1" case "sz + newt*(vsp-viz) = 0" )"1" "newt" )"1" assert )nil )"2" assert )nil )))"2" replace "2" "const3" "vsp-viz" )"2" replace -1)"2" "-" "sz" "1" assert )"1" nil )))"2" assert )nil )))))))))))))"2" replace -1 :dir rl)"2" "1" "1" "T" )"1" "viz-vsp" )"1" assert )nil )))))))"2" "2" "T" )"2" "viz-vsp" )"2" assert )nil )))))))))))))"2" (assert ) nil )))"2" expand "abs" )"2" "2" nil )))))))"2" (assert ) nil )))))))"2" "T" )"2" "viz-vsp" )"2" (assert ) nil )))))))"2" "H" )"2" "H" )"2" assert )nil )))))))))))))))))))))))))))))))))"2" (flatten)"2" (case "vsp - viz = 0" )"1" (replace -1) (("1" (assert ) nil )))"2" (replace 1)"2" (split -)"1" (flatten)"1" (replace -1)"1" (hide -1)"1" (replace -1)"1" (hide -1)"1" (expand "abs" )"1" (lift-if)"1" (split -)"1" "1" expand "conflict_vertical?" )"1" "1" "1" replace -1)"1" case "vsp < viz" )"1" "H" )"1" (assert ) nil )))"2" "T-t!1" )"2" expand "abs" )"2" "2" nil )))))))))))))))))))"2" "2" replace -1)"2" case "vsp > viz" )"1" "H" )"1" (assert ) nil )))"2" expand "conflict_vertical?" )"2" "2" "T-t!1" )"2" expand "abs" )"2" "2" nil )))))))))))))))))))))))))))))))))"2" (flatten)"2" (replace -1)"2" (hide -1)"2" (replace -1)"2" (hide -1)"2" (expand "abs" )"2" (lift-if)"2" (split -)"1" "1" "1" replace -1)"1" case "vsp > viz" )"1" "H" )"1" (assert ) nil )))"2" expand "conflict_vertical?" )"2" "2" "t!1-B" )"2" expand "abs" )"2" "2" nil )))))))))))))))))))"2" "2" replace -1)"2" case "vsp < viz" )"1" "H" )"1" (assert ) nil )))"2" expand "conflict_vertical?" )"2" "2" "t!1-B" )"2" expand "abs" )"2" "2" nil ))))))))))))))))))))))))))))))))))))))))))))nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil extra_tegies nil )nil extra_tegies nil )"nzreal" nil )"nzreal" real_typesnil )"posreal" nil )"odd_int" integers nil )"real" reals nil )nil extra_real_props nil )"posreal" vs_bands nil )"{AB: posreal | AB > B}" vs_bands nil )"nnreal" vs_bands nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil booleans nil )nil booleans nil )"bool" reals nil )nil real_props nil )"(total_order?[real])" nil )nil Lookahead nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" reals nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil real_props nil )nil real_props nil )nil real_types nil )nil real_types nil )"real" vs_bands nil )"real" vs_bands nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil abs_lems "reals/" )NOT const-decl "[bool -> bool]" booleans nil )nil real_props nil )nil reals nil )"real" vs_bands nil )"(total_order?[real])" nil )"bool" cd_vertical nil )nil extra_real_propsnil )"nnreal" nil )nil real_props nil )nil extra_real_propsnil )nil real_props nil )nil real_props nil )nil real_props nil )"real" vs_bands nil )"real" vs_bands nil )"real" vs_bands nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))"stop infinite loop on mult-by -1" 3508591107"" (skeep)"" (case "B = 0" )"1" (replace -1)"1" (assert )"1" (hide -1)"1" (expand "sign" -3)"1" (case "T * vsp1 - T * viz + sz >= 0" )"1" (assert )"1" (lift-if)"1" (ground)"1" (expand "abs" (-1 -2 -3 -4))"1" (hide -1)"1" (hide -1)"1" (case "sz + tlh*(vsp2-viz) < H" )"1" "1" "newt" "(H-sz+T*viz)/T" )"1" case "sz + T*(newt-viz) = H" )"1" "newt" )"1" expand "abs" +)"1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "T" "1" "sz" "viz" "newt" )"1" expand "abs" -1)"1" expand "conflict_vertical?" )"1" "1" case "newt-viz = (H-sz)/T" )"1" "t!1" )"1" replace -1)"1" "1" case "sz + ((H-sz)/T)*t!1<H" )"1" "1" "T" )"1" "T-t!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "T" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "vsp2 < viz" )"1" case "sz + T*(vsp2-viz) < H" )"1" "band" )"1" "vsp2" "vsp1" "newt" )"1" assert )"1" replace -4 :dir rl)"1" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "T-tlh" )"2" (assert ) nil nil ))nil ))nil )"2" "tlh" )"2" (assert ) nil nil ))nil ))nil ))nil )"2" replace -1 :dir rl)"2" "T" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" )"2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (ground)"2" (expand "abs" (-1 -2))"2" (neg-formula -1)"2" (neg-formula -2)"2" (case "sz + tlh*(vsp2-viz) > -H" )"1" (assert )"1" (case "sz >= 0" )"1" (assert ) nil nil )"2" assert )"2" "2" "newt" "(-H-sz+T*viz)/T" )"2" case "sz + T*(newt-viz) = -H" )"1" "newt" )"1" expand "abs" +)"1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "T" "1" "sz" "viz" "newt" )"1" expand "abs" -1)"1" expand "conflict_vertical?" )"1" "1" case "newt-viz = (-H-sz)/T" )"1" case "newt*t!1 - viz*t!1 = (-H - sz) / T*t!1" )"1" "1" "1" case "sz + ((-H-sz)/T)*t!1>-H" )"1" "1" case " sz*T + ((-H - sz)) * t!1 > -H*T" )"1" "1" "T-t!1" )"1" assert )nil nil ))nil ))nil )"2" "2" "div_T" "(-H - sz) / T" )"2" "T" )"2" expand "div_T" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "vsp2 > viz" )"1" case "sz + T*(vsp2-viz) > -H" )"1" "band" )"1" "vsp1" "vsp2" "newt" )"1" assert )"1" replace "1" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "T-tlh" )"2" (assert ) nil nil ))nil ))nil )"2" "tlh" )"2" (assert ) nil nil ))nil ))nil ))nil )"2" replace -1 :dir rl)"2" "T" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "abs" -)"2" (lift-if) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "sign" -)"2" (lift-if)"2" (lift-if)"2" (ground)"1" (expand "abs" (-1 -2 -3 -4))"1" (hide -1)"1" (hide -1)"1" (case "sz + tlh*(vsp2-viz) < H" )"1" (hide -4)"1" (name "newtb" "(H-sz+B*viz)/B" )"1" (label "newtbname" -1)"1" case "sz + B*(newtb-viz) = H" )"1" "newtt" "(H-sz+T*viz)/T" )"1" "newttname" -1)"1" case "sz + T*(newtt-viz) = H" )"1" case "vsp2 >= viz" )"1" case "sz + B*(vsp2-viz) < H" )"1" "newtb" )"1" "1" "1" expand "abs" +)"1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "B" "-1" "sz" "viz" "newtb" )"1" expand "abs" "1" expand "conflict_vertical?" )"1" "1" case "sz + t!1*(newtb - viz) < H" )"1" "1" case "newtb - viz = (H-sz)/B" )"1" replace "1" "1" "-" "sz" "1" assert )"1" "1" case "H < sz" )"1" "B" )"1" assert )nil nil ))nil )"2" "(t!1-B)" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" replace "newtbname" "2" "B" )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "band" )"2" "vsp2" "vsp1" "newtb" )"2" assert )"2" replace "newtbname" "2" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "tlh-B" )"2" (assert ) nil nil ))nil ))nil )"2" case "vsp2 < viz" )"1" "1" case "H>sz" )"1" case "sz + B*(vsp2-viz) < H" )"1" "newtb" )"1" "1" "1" expand "abs" "1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "B" "-1" "sz" "viz" "newtb" )"1" expand "abs" "1" expand "conflict_vertical?" )"1" "1" case "sz + t!1*(newtb - viz) < H" )"1" "1" case "newtb - viz = (H-sz)/B" )"1" replace "1" "1" "-" "sz" "1" assert )"1" "1" "t!1-B" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" replace "newtbname" "2" "B" )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "band" )"2" "vsp2" "vsp1" "newtb" )"2" assert )"2" replace "newtbname" "2" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "B" )"2" assert )nil nil ))nil ))nil )"2" case "sz + T*(vsp2-viz) < H" )"1" "newtt" )"1" "1" "1" expand "abs" "1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "T" "1" "sz" "viz" "newtt" )"1" expand "abs" "1" expand "conflict_vertical?" )"1" "1" case "sz + t!1*(newtt-viz) < H" )"1" "1" case "newtt - viz = (H-sz)/T" )"1" replace "1" "1" assert )"1" case "t!1 * ((H - sz) / T) + sz - sz < H - sz" )"1" "1" assert )"1" "T-t!1" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" expand "abs" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "band" )"2" "vsp2" "vsp1" "newtt" )"2" "1" nil nil )"2" replace "newttname" "2" "2" assert )nil nil ))nil ))nil )"3" replace "newttname" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "T-tlh" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" replace "newttname" + :dir rl)"2" "T" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace "newtbname" + :dir rl)"2" "B" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "abs" -)"2" (lift-if) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lift-if)"2" (ground)"2" (expand "abs" (-1 -2))"2" (neg-formula -1)"2" (neg-formula -2)"2" (hide 1)"2" (hide 1)"2" case "sz + tlh*(vsp2-viz) > -H" )"1" "1" "newtb" "(-H-sz+B*viz)/B" )"1" "newtbname" -1)"1" case "sz + B*(newtb-viz) = -H" )"1" "newtt" "(-H-sz+T*viz)/T" )"1" "newttname" -1)"1" case "sz + T*(newtt-viz) = -H" )"1" case "vsp2 <= viz" )"1" case "sz + B*(vsp2-viz) > -H" )"1" "newtb" )"1" "1" "1" expand "abs" "1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "B" "-1" "sz" "viz" "newtb" )"1" expand "abs" "1" expand "conflict_vertical?" )"1" "1" case "sz + t!1*(newtb - viz) > -H" )"1" "1" case "newtb - viz = (-H-sz)/B" )"1" replace "1" "1" "-" "sz" "1" assert )"1" "1" case "-H > sz" )"1" "B" )"1" assert )nil nil ))nil )"2" "(t!1-B)" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" replace "newtbname" "2" "B" )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "band" )"2" "vsp1" "vsp2" "newtb" )"2" assert )"2" replace "newtbname" "2" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "tlh-B" )"2" assert )nil nil ))nil ))nil )"2" case "vsp2 > viz" )"1" "1" case "-H < sz" )"1" case "sz + B*(vsp2-viz) > -H" )"1" "newtb" )"1" "1" "1" expand "abs" "1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "B" "-1" "sz" "viz" "newtb" )"1" expand "abs" "1" expand "conflict_vertical?" )"1" "1" case "sz + t!1*(newtb - viz) > -H" )"1" "1" case "newtb - viz = (-H-sz)/B" )"1" replace "1" "1" case "sz + t!1 * ((-H - sz) / B) - sz > -H - sz" )"1" "1" assert )"1" "1" "t!1-B" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" replace "newtbname" "2" "B" )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "band" )"2" "vsp1" "vsp2" "newtb" )"2" assert )"2" replace "newtbname" "2" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "B" )"2" assert )nil nil ))nil ))nil )"2" case "sz + T*(vsp2-viz) > -H" )"1" "newtt" )"1" "1" "1" expand "abs" "1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "T" "1" "sz" "viz" "newtt" )"1" expand "abs" "1" expand "conflict_vertical?" )"1" "1" case "sz + t!1*(newtt-viz) > -H" )"1" "1" case "newtt - viz = (-H-sz)/T" )"1" replace "1" "1" case "sz + t!1 * ((-H - sz) / T) - sz > -H - sz" )"1" "1" assert )"1" "T-t!1" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" replace "newttname" "2" "T" )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "band" )"2" "vsp1" "vsp2" "newtt" )"2" "1" nil nil )"2" replace "newttname" "2" nil nil ))nil )"3" replace "newttname" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "T-tlh" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" replace "newttname" "2" "T" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace "newtbname" "2" "B" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" -)"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" vs_bands nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"Sign" sign "reals/" )nil extra_tegies nil )"nzreal" nil )"nzreal" real_typesnil )nil extra_real_propsnil )nil real_types nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )nil extra_real_propsnil )nil real_props nil )nil real_props nil )"real" vs_bands nil )"real" vs_bands nil )nil extra_tegies nil )"bool" reals nil )nil Lookahead nil )"posreal" vs_bands nil )"real" reals nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"Connected" vs_bands nil )"real" vs_bands nil )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" cd_vertical nil )nil real_props nil )"posreal" nil )"nnreal" nil )nil extra_real_propsnil )"real" reals nil )nil extra_real_props nil )nil reals nil )nil real_props nil )nil real_props nil )nil vs_bands nil )nil real_props nil )nil real_props nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"Lookahead[B, T]" vs_bands nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"{AB: posreal | AB > B}" vs_bands nil )set type-eq-decl nil sets nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil connected_set "reals/" )"odd_int" integers nil )"real" vs_bands nil )nil real_props nil )nil extra_real_props nil )"real" vs_bands nil )"real" vs_bands nil )nil real_props nil )nil real_props nil )nil real_props nil )"real" vs_bands nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil )"stop infinite loop on mult-by -1" 3508523193"" (skeep) (("" (postpone) nil nil )) nil ) nil shostak)"" 3504767507"" (skeep)"" (case "B = 0" )"1" (replace -1)"1" (assert )"1" (hide -1)"1" (expand "sign" -3)"1" (lift-if)"1" (lift-if)"1" (lift-if)"1" (split)"1" (flatten)"1" (assert )"1" (prop)"1" (ground)"1" expand "abs" (-1 -2 -3 -4))"1" "1" "1" case "sz + tlh*(vsp2-viz) < H" )"1" "1" "newt" "(H-sz+T*viz)/T" )"1" case "sz + T*(newt-viz) = H" )"1" "newt" )"1" expand "abs" +)"1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "T" "1" "sz" "viz" "newt" )"1" expand "abs" "1" expand "conflict_vertical?" )"1" "1" case "newt-viz = (H-sz)/T" )"1" "t!1" )"1" replace "1" "1" case "sz + ((H-sz)/T)*t!1<H" )"1" "1" "T" )"1" "T-t!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "T" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "vsp2 < viz" )"1" case "sz + T*(vsp2-viz) < H" )"1" "band" )"1" "vsp2" "vsp1" "newt" )"1" assert )"1" replace "1" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "T-tlh" )"2" assert )nil nil ))nil ))nil )"2" "tlh" )"2" assert )nil nil ))nil ))nil ))nil )"2" replace -1 :dir rl)"2" "T" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" )"2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (ground)"2" (expand "abs" (-1 -2))"2" (neg-formula -1)"2" "2" case "sz + tlh*(vsp2-viz) > -H" )"1" "1" "newt" "(-H-sz+T*viz)/T" )"1" case "sz + T*(newt-viz) = -H" )"1" "newt" )"1" expand "abs" +)"1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "T" "1" "sz" "viz" "newt" )"1" expand "abs" -1)"1" expand "conflict_vertical?" )"1" "1" case "newt-viz = (-H-sz)/T" )"1" "t!1" )"1" replace "1" "1" case "sz + ((-H-sz)/T)*t!1>-H" )"1" "1" "T" )"1" "T-t!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "T" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "vsp2 > viz" )"1" case "sz + T*(vsp2-viz) > -H" )"1" "band" )"1" "vsp1" "vsp2" "newt" )"1" assert )"1" replace "1" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "T-tlh" )"2" assert )nil nil ))nil ))nil )"2" "tlh" )"2" (assert ) nil nil ))nil ))nil ))nil )"2" replace -1 :dir rl)"2" "T" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" -)"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "sign" -)"2" (lift-if)"2" (lift-if)"2" (ground)"1" (expand "abs" (-1 -2 -3 -4))"1" (hide -1)"1" (hide -1)"1" (case "sz + tlh*(vsp2-viz) < H" )"1" (hide -4)"1" (name "newtb" "(H-sz+B*viz)/B" )"1" (label "newtbname" -1)"1" case "sz + B*(newtb-viz) = H" )"1" "newtt" "(H-sz+T*viz)/T" )"1" "newttname" -1)"1" case "sz + T*(newtt-viz) = H" )"1" case "vsp2 >= viz" )"1" case "sz + B*(vsp2-viz) < H" )"1" "newtb" )"1" "1" "1" expand "abs" +)"1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "B" "-1" "sz" "viz" "newtb" )"1" expand "abs" "1" expand "conflict_vertical?" )"1" "1" case "sz + t!1*(newtb - viz) < H" )"1" "1" case "newtb - viz = (H-sz)/B" )"1" replace "1" "1" "-" "sz" "1" assert )"1" "1" case "H < sz" )"1" "B" )"1" assert )nil nil ))nil )"2" "(t!1-B)" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" replace "newtbname" "2" "B" )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "band" )"2" "vsp2" "vsp1" "newtb" )"2" assert )"2" replace "newtbname" "2" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "tlh-B" )"2" (assert ) nil nil ))nil ))nil )"2" case "vsp2 < viz" )"1" "1" case "H>sz" )"1" case "sz + B*(vsp2-viz) < H" )"1" "newtb" )"1" "1" "1" expand "abs" "1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "B" "-1" "sz" "viz" "newtb" )"1" expand "abs" "1" expand "conflict_vertical?" )"1" "1" case "sz + t!1*(newtb - viz) < H" )"1" "1" case "newtb - viz = (H-sz)/B" )"1" replace "1" "1" "-" "sz" "1" assert )"1" "1" "t!1-B" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" replace "newtbname" "2" "B" )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "band" )"2" "vsp2" "vsp1" "newtb" )"2" assert )"2" replace "newtbname" "2" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "B" )"2" assert )nil nil ))nil ))nil )"2" case "sz + T*(vsp2-viz) < H" )"1" "newtt" )"1" "1" "1" expand "abs" "1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "T" "1" "sz" "viz" "newtt" )"1" expand "abs" "1" expand "conflict_vertical?" )"1" "1" case "sz + t!1*(newtt-viz) < H" )"1" "1" case "newtt - viz = (H-sz)/T" )"1" replace "1" "1" assert )"1" case "t!1 * ((H - sz) / T) + sz - sz < H - sz" )"1" "1" assert )"1" "T-t!1" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" expand "abs" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "band" )"2" "vsp2" "vsp1" "newtt" )"2" "1" nil nil )"2" replace "newttname" "2" "2" assert )nil nil ))nil ))nil )"3" replace "newttname" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "T-tlh" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" replace "newttname" + :dir rl)"2" "T" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace "newtbname" + :dir rl)"2" "B" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "abs" -)"2" (lift-if) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lift-if)"2" (ground)"2" (expand "abs" (-1 -2))"2" (neg-formula -1)"2" (neg-formula -2)"2" (hide 1)"2" (hide 1)"2" case "sz + tlh*(vsp2-viz) > -H" )"1" "1" "newtb" "(-H-sz+B*viz)/B" )"1" "newtbname" -1)"1" case "sz + B*(newtb-viz) = -H" )"1" "newtt" "(-H-sz+T*viz)/T" )"1" "newttname" -1)"1" case "sz + T*(newtt-viz) = -H" )"1" case "vsp2 <= viz" )"1" case "sz + B*(vsp2-viz) > -H" )"1" "newtb" )"1" "1" "1" expand "abs" "1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "B" "-1" "sz" "viz" "newtb" )"1" expand "abs" "1" expand "conflict_vertical?" )"1" "1" case "sz + t!1*(newtb - viz) > -H" )"1" "1" case "newtb - viz = (-H-sz)/B" )"1" replace "1" "1" "-" "sz" "1" assert )"1" "1" case "-H > sz" )"1" "B" )"1" assert )nil nil ))nil )"2" "(t!1-B)" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" replace "newtbname" "2" "B" )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "band" )"2" "vsp1" "vsp2" "newtb" )"2" assert )"2" replace "newtbname" "2" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "tlh-B" )"2" assert )nil nil ))nil ))nil )"2" case "vsp2 > viz" )"1" "1" case "-H < sz" )"1" case "sz + B*(vsp2-viz) > -H" )"1" "newtb" )"1" "1" "1" expand "abs" "1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "B" "-1" "sz" "viz" "newtb" )"1" expand "abs" "1" expand "conflict_vertical?" )"1" "1" case "sz + t!1*(newtb - viz) > -H" )"1" "1" case "newtb - viz = (-H-sz)/B" )"1" replace "1" "1" case "sz + t!1 * ((-H - sz) / B) - sz > -H - sz" )"1" "1" assert )"1" "1" "t!1-B" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" replace "newtbname" "2" "B" )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "band" )"2" "vsp1" "vsp2" "newtb" )"2" assert )"2" replace "newtbname" "2" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "B" )"2" assert )nil nil ))nil ))nil )"2" case "sz + T*(vsp2-viz) > -H" )"1" "newtt" )"1" "1" "1" expand "abs" "1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "T" "1" "sz" "viz" "newtt" )"1" expand "abs" "1" expand "conflict_vertical?" )"1" "1" case "sz + t!1*(newtt-viz) > -H" )"1" "1" case "newtt - viz = (-H-sz)/T" )"1" replace "1" "1" case "sz + t!1 * ((-H - sz) / T) - sz > -H - sz" )"1" "1" assert )"1" "T-t!1" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" replace "newttname" "2" "T" )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "band" )"2" "vsp1" "vsp2" "newtt" )"2" "1" nil nil )"2" replace "newttname" "2" nil nil ))nil )"3" replace "newttname" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "T-tlh" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" replace "newttname" "2" "T" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace "newtbname" "2" "B" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" -)"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"Sign" sign "reals/" )nil connected_set "reals/" )nil Lookahead nil )nil sign "reals/" )"bool" cd_vertical nil ))nil 3477244369"" (skeep)"" (case "B = 0" )"1" (replace -1)"1" (assert )"1" (hide -1)"1" (expand "sign" -3)"1" (lift-if)"1" (lift-if)"1" (split)"1" (flatten)"1" (ground)"1" (expand "abs" (-1 -2 -3 -4))"1" (hide -2)"1" (hide -1)"1" case "sz + tlh*(vsp2-viz) < H" )"1" "1" "newt" "(H-sz+T*viz)/T" )"1" case "sz + T*(newt-viz) = H" )"1" "newt" )"1" expand "abs" +)"1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "T" "1" "sz" "viz" "newt" )"1" expand "abs" -1)"1" expand "conflict_vertical?" )"1" "1" case "newt-viz = (H-sz)/T" )"1" "t!1" )"1" replace "1" "1" case "sz + ((H-sz)/T)*t!1<H" )"1" "1" "T" )"1" "T-t!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "T" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "vsp2 < viz" )"1" case "sz + T*(vsp2-viz) < H" )"1" "band" )"1" "vsp2" "vsp1" "newt" )"1" assert )"1" replace "1" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "T-tlh" )"2" (assert ) nil nil ))nil ))nil )"2" "tlh" )"2" (assert ) nil nil ))nil ))nil ))nil )"2" replace -1 :dir rl)"2" "T" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" )"2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (ground)"2" (expand "abs" (-1 -2))"2" (neg-formula -1)"2" (neg-formula -2)"2" case "sz + tlh*(vsp2-viz) > -H" )"1" "1" "newt" "(-H-sz+T*viz)/T" )"1" case "sz + T*(newt-viz) = -H" )"1" "newt" )"1" expand "abs" +)"1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "T" "1" "sz" "viz" "newt" )"1" expand "abs" -1)"1" expand "conflict_vertical?" )"1" "1" case "newt-viz = (-H-sz)/T" )"1" "t!1" )"1" replace "1" "1" case "sz + ((-H-sz)/T)*t!1>-H" )"1" "1" "T" )"1" "T-t!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "T" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "vsp2 > viz" )"1" case "sz + T*(vsp2-viz) > -H" )"1" "band" )"1" "vsp1" "vsp2" "newt" )"1" assert )"1" replace "1" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "T-tlh" )"2" (assert ) nil nil ))nil ))nil )"2" "tlh" )"2" (assert ) nil nil ))nil ))nil ))nil )"2" replace -1 :dir rl)"2" "T" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" -)"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "sign" -)"2" (lift-if)"2" (lift-if)"2" (ground)"1" (expand "abs" (-1 -2 -3 -4))"1" (hide -1)"1" (hide -1)"1" (case "sz + tlh*(vsp2-viz) < H" )"1" (hide -4)"1" (name "newtb" "(H-sz+B*viz)/B" )"1" (label "newtbname" -1)"1" case "sz + B*(newtb-viz) = H" )"1" "newtt" "(H-sz+T*viz)/T" )"1" "newttname" -1)"1" case "sz + T*(newtt-viz) = H" )"1" case "vsp2 >= viz" )"1" case "sz + B*(vsp2-viz) < H" )"1" "newtb" )"1" "1" "1" expand "abs" +)"1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "B" "-1" "sz" "viz" "newtb" )"1" expand "abs" "1" expand "conflict_vertical?" )"1" "1" case "sz + t!1*(newtb - viz) < H" )"1" "1" case "newtb - viz = (H-sz)/B" )"1" replace "1" "1" "-" "sz" "1" assert )"1" "1" case "H < sz" )"1" "B" )"1" assert )nil nil ))nil )"2" "(t!1-B)" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" replace "newtbname" "2" "B" )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "band" )"2" "vsp2" "vsp1" "newtb" )"2" assert )"2" replace "newtbname" "2" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "tlh-B" )"2" (assert ) nil nil ))nil ))nil )"2" case "vsp2 < viz" )"1" "1" case "H>sz" )"1" case "sz + B*(vsp2-viz) < H" )"1" "newtb" )"1" "1" "1" expand "abs" "1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "B" "-1" "sz" "viz" "newtb" )"1" expand "abs" "1" expand "conflict_vertical?" )"1" "1" case "sz + t!1*(newtb - viz) < H" )"1" "1" case "newtb - viz = (H-sz)/B" )"1" replace "1" "1" "-" "sz" "1" assert )"1" "1" "t!1-B" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" replace "newtbname" "2" "B" )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "band" )"2" "vsp2" "vsp1" "newtb" )"2" assert )"2" replace "newtbname" "2" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "B" )"2" assert )nil nil ))nil ))nil )"2" case "sz + T*(vsp2-viz) < H" )"1" "newtt" )"1" "1" "1" expand "abs" "1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "T" "1" "sz" "viz" "newtt" )"1" expand "abs" "1" expand "conflict_vertical?" )"1" "1" case "sz + t!1*(newtt-viz) < H" )"1" "1" case "newtt - viz = (H-sz)/T" )"1" replace "1" "1" "-" "sz" "1" assert )"1" "T-t!1" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" replace "newttname" "2" "T" )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "band" )"2" "vsp2" "vsp1" "newtt" )"2" "1" nil nil )"2" replace "newttname" "2" "2" assert )nil nil ))nil ))nil )"3" replace "newttname" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "T-tlh" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" replace "newttname" + :dir rl)"2" "T" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace "newtbname" + :dir rl)"2" "B" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "abs" -)"2" (lift-if) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "abs" (-1 -2))"2" (neg-formula -1)"2" (neg-formula -2)"2" (hide 1)"2" (hide 1)"2" (case "sz + tlh*(vsp2-viz) > -H" )"1" (hide -4)"1" "newtb" "(-H-sz+B*viz)/B" )"1" "newtbname" -1)"1" case "sz + B*(newtb-viz) = -H" )"1" "newtt" "(-H-sz+T*viz)/T" )"1" "newttname" -1)"1" case "sz + T*(newtt-viz) = -H" )"1" case "vsp2 <= viz" )"1" case "sz + B*(vsp2-viz) > -H" )"1" "newtb" )"1" "1" "1" expand "abs" +)"1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "B" "-1" "sz" "viz" "newtb" )"1" expand "abs" "1" expand "conflict_vertical?" )"1" "1" case "sz + t!1*(newtb - viz) > -H" )"1" "1" case "newtb - viz = (-H-sz)/B" )"1" replace "1" "1" "-" "sz" "1" assert )"1" "1" case "-H > sz" )"1" "B" )"1" assert )nil nil ))nil )"2" "(t!1-B)" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" replace "newtbname" "2" "B" )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "band" )"2" "vsp1" "vsp2" "newtb" )"2" assert )"2" replace "newtbname" "2" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "tlh-B" )"2" assert )nil nil ))nil ))nil )"2" case "vsp2 > viz" )"1" "1" case "-H < sz" )"1" case "sz + B*(vsp2-viz) > -H" )"1" "newtb" )"1" "1" "1" expand "abs" "1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "B" "-1" "sz" "viz" "newtb" )"1" expand "abs" "1" expand "conflict_vertical?" )"1" "1" case "sz + t!1*(newtb - viz) > -H" )"1" "1" case "newtb - viz = (-H-sz)/B" )"1" replace "1" "1" "-" "sz" "1" assert )"1" "1" "t!1-B" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" replace "newtbname" "2" "B" )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "band" )"2" "vsp1" "vsp2" "newtb" )"2" assert )"2" replace "newtbname" "2" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "B" )"2" assert )nil nil ))nil ))nil )"2" case "sz + T*(vsp2-viz) > -H" )"1" "newtt" )"1" "1" "1" expand "abs" "1" assert )"1" "vs_bands_vertical_dir_exclusive" )"1" "T" "1" "sz" "viz" "newtt" )"1" expand "abs" "1" expand "conflict_vertical?" )"1" "1" case "sz + t!1*(newtt-viz) > -H" )"1" "1" case "newtt - viz = (-H-sz)/T" )"1" replace "1" "1" "-" "sz" "1" assert )"1" "T-t!1" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" replace "newttname" "2" "T" )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "band" )"2" "vsp1" "vsp2" "newtt" )"2" "1" nil nil )"2" replace "newttname" "2" "2" assert )nil nil ))nil ))nil )"3" replace "newttname" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "T-tlh" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" replace "newttname" "2" "T" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace "newtbname" + :dir rl)"2" "B" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "abs" -)"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"Sign" sign "reals/" )nil connected_set "reals/" )nil Lookahead nil )nil sign "reals/" )"bool" cd_vertical nil ))nil ))nil 3477244741"" (skeep)"" (expand "sign" +)"" (lift-if)"" (split +)"1" (flatten)"1" (expand "abs" )"1" (assert )"1" (hide -1)"1" (copy -1)"1" (mult-by -1 "(vsp-viz)" )"1" (assert )"1" (replace -1)"1" (case "vsp >= viz" )"1" (copy -1)"1" "B" )"1" "H" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (copy 1)"2" "B" )"2" "H" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "abs" )"2" (assert )"2" (neg-formula -1)"2" (copy -1)"2" (mult-by -1 "vsp-viz" )"2" (assert )"2" (replace -1)"2" (case "vsp <= viz" )"1" (copy -1)"1" "B" )"1" "H" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (copy 1)"2" "B" )"2" "H" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"Sign" sign "reals/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil extra_real_props nil )"posreal" vs_bands nil )nil real_types nil )"bool" reals nil )nil real_types nil )"nnreal" vs_bands nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"odd_int" integers nil )nil real_props nil )nil extra_real_propsnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil extra_tegies nil )nil extra_tegies nil )"nzreal" nil )"nzreal" real_typesnil )"posreal" nil )"[numfield -> numfield]" number_fields nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )nil real_props nil )nil extra_real_propsnil )"bool" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3477244755"" (skeep)"" (expand "sign" 1)"" (lift-if)"" (split)"1" (flatten)"1" (expand "abs" )"1" (assert )"1" (hide -1)"1" (copy -1)"1" (mult-by -1 "viz-vsp" )"1" (assert )"1" (replace -1)"1" (case "viz >= vsp" )"1" (copy -1)"1" "T" )"1" "H" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (copy 1)"2" "T" )"2" "H" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "abs" )"2" (assert )"2" (copy -1)"2" (mult-by -1 "vsp-viz" )"2" (assert )"2" (replace -1)"2" (case "vsp >= viz" )"1" (copy -1)"1" (mult-by -1 "T" )"1" "H" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (copy 1)"2" (mult-by 1 "T" )"2" "H" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"Sign" sign "reals/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil extra_real_props nil )"posreal" vs_bands nil )"{AB: posreal | AB > B}" vs_bands nil )"nnreal" vs_bands nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"odd_int" integers nil )nil real_props nil )nil extra_real_propsnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"[numfield -> numfield]" number_fields nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3477244772"" (skosimp*)"" (expand "vs_band?" )"" (split)"1" (flatten)"1" (expand "vs_green?" )"1" (skosimp*)"1" case "sign(sz!1 + B*(vsp!1-viz!1)) = sign(sz!1 + T*(vsp!1-viz!1))" )"1" (lemma "cd_vertical" )"1" (inst-cp - "sz!1" "vsp!1-viz!1" )"1" (inst - "sz!1" "vsp!2-viz!1" )"1" (assert )"1" (copy 1)"1" (copy 1)"1" (expand "conflict_vertical?" 1)"1" expand "conflict_vertical?" 2)"1" "B" )"1" "T" )"1" expand "conflict_vertical?" -)"1" "1" "band_critical_on_H" )"1" "band!1" "sz!1" "viz!1" "vsp!1" "vsp!2" "t!1" )"1" assert )"1" "1" "vsp!3" )"1" expand "vs_critical?" )"1" "vs_circle_at_complete" )"1" "1" assert )"1" "1" "1" "-1" )"1" "1" )"1" "vs_at_complete" )"1" "-1" "T" "sz!1" "vsp!3-viz!1" )"1" "1" "T" "sz!1" "vsp!3-viz!1" )"1" case "B = 0" )"1" assert )"1" expand "abs" "1" "1" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "vs_at_complete" )"2" "-1" "B" "sz!1" "vsp!3-viz!1" )"1" "1" "B" "sz!1" "vsp!3-viz!1" )"1" assert )"1" "1" "-1" )"1" "1" )"1" expand "abs" "1" "1" "1" "1" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil 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 ))nil ))nil ))nil ))nil )"2" (lemma "cd_vertical" )"2" (inst - "sz!1" "vsp!1-viz!1" )"2" (assert )"2" (hide 3)"2" (expand "conflict_vertical?" +)"2" (case "vsp!1-viz!1 = 0" )"1" (copy -1)"1" "B" )"1" "T" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (name "newt" "-sz!1/(vsp!1-viz!1)" )"2" case "sz!1 + newt*(vsp!1-viz!1) = 0" )"1" "newt" )"1" (assert ) nil nil )"2" case "B <= newt AND newt <= T" )"1" "1" (assert ) nil nil ))nil )"2" "2" replace -2 + :dir rl)"2" "1" case "vsp!1 > viz!1" )"1" "1" expand "sign" +)"1" "1" "1" "1" "T" )"1" "vsp!1-viz!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "sign" +)"2" "2" "2" "2" "T" )"2" "viz!1-vsp!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "vsp!1 > viz!1" )"1" "1" expand "sign" +)"1" "1" "1" "1" "T" )"1" "vsp!1-viz!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "sign" +)"2" "2" "2" "2" "T" )"2" "viz!1-vsp!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1 :dir rl)"2" "const1" "vsp!1-viz!1" )"2" replace -1)"2" "-" "sz!1" 1)"1" assert )"1" nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (lemma "cd_vertical" )"2" (inst - "sz!1" "vsp!1-viz!1" )"2" (assert )"2" (expand "vs_green?" )"2" (inst - "vsp!1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" vs_bands nil )"real" reals nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil real_props nil )nil reals nil )nil real_props nil )"real" vs_bands nil )nil abs_lems "reals/" )nil real_props nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil real_props nil )"real" vs_bands nil )"(band!1)" vs_bands nil )"Connected" vs_bands nil )NOT const-decl "[bool -> bool]" booleans nil )nil real_props nil )nil real_props nil )nil real_props nil )"nnreal" nil )nil extra_real_props nil )nil cd_vertical nil )"posreal" vs_bands nil )"bool" cd_vertical nil )"(total_order?[real])" nil )nil Lookahead nil )nil vs_bands nil )"(strict_total_order?[real])" real_props nil )nil vertical nil )"(strict_total_order?[real])" real_props nil )nil reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" reals nil )"posreal" nil )"nzreal" nil )nil vertical nil )"odd_int" integers nil )"bool" vs_bands nil )"real" reals nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )nil numbers nil )nil booleans 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 )"boolean" notequal nil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"Sign" sign "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"nnreal" vs_bands nil )"[numfield, numfield -> numfield]" number_fields nil )set type-eq-decl nil sets nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil connected_set "reals/" )nil real_types nil )"bool" reals nil )nil real_types nil )"{AB: posreal | AB > B}" vs_bands nil )"bool" vs_bands nil ))nil ))nil 3477244803"" (skosimp*)"" (expand "vs_band?" )"" (split)"1" (flatten)"1" (expand "vs_red?" )"1" (skosimp*)"1" case "sign(sz!1 + B*(vsp!2-viz!1)) = sign(sz!1 + T*(vsp!2-viz!1))" )"1" (lemma "cd_vertical" )"1" (inst-cp - "sz!1" "vsp!1-viz!1" )"1" (inst - "sz!1" "vsp!2-viz!1" )"1" (assert )"1" (hide 1)"1" (hide -3)"1" (copy 1)"1" "1" expand "conflict_vertical?" 1)"1" expand "conflict_vertical?" 2)"1" "B" )"1" "T" )"1" expand "conflict_vertical?" "1" "1" "band_critical_on_H" )"1" "band!1" "sz!1" "viz!1" "vsp!2" "vsp!1" "t!1" )"1" assert )"1" "1" "vsp!3" )"1" expand "vs_critical?" )"1" "vs_circle_at_complete" )"1" "1" assert )"1" "1" "1" "-1" )"1" "1" )"1" "vs_at_complete" )"1" "-1" "T" "sz!1" "vsp!3-viz!1" )"1" "1" "T" "sz!1" "vsp!3-viz!1" )"1" case "B = 0" )"1" assert )"1" expand "abs" "1" "1" "1" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "vs_at_complete" )"2" "-1" "B" "sz!1" "vsp!3-viz!1" )"1" "1" "B" "sz!1" "vsp!3-viz!1" )"1" assert )"1" "1" "-1" )"1" "1" )"1" expand "abs" "1" "1" "1" "1" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil 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 ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "cd_vertical" )"2" (inst - "sz!1" "vsp!2-viz!1" )"2" (assert )"2" (hide 3)"2" (case "vsp!2-viz!1 = 0" )"1" (copy -1)"1" (mult-by -1 "B" )"1" "T" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (name "newt" "-sz!1/(vsp!2-viz!1)" )"2" case "sz!1 + newt*(vsp!2-viz!1) = 0" )"1" "cd_vertical" )"1" "sz!1" "vsp!2-viz!1" )"1" replace -1 :dir rl)"1" "1" expand "conflict_vertical?" )"1" "newt" )"1" (assert ) nil nil )"2" case "B <= newt AND newt <= T" )"1" "1" (assert ) nil nil ))nil )"2" "2" replace -2 + :dir rl)"2" "1" case "vsp!2 > viz!1" )"1" "1" expand "sign" "1" "1" "1" "1" "T" )"1" "vsp!2-viz!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "sign" "2" "2" "2" "2" "T" )"2" "viz!1-vsp!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "vsp!2 > viz!1" )"1" "1" expand "sign" "1" "1" "1" "1" "T" )"1" "vsp!2-viz!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "sign" "2" "2" "2" "2" "T" )"2" "viz!1-vsp!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1 :dir rl)"2" "const1" "vsp!2-viz!1" )"2" replace -1)"2" "-" "sz!1" 1)"1" assert )"1" (cross-mult 1) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (lemma "cd_vertical" )"2" (inst - "sz!1" "vsp!1-viz!1" )"2" (assert )"2" (expand "vs_red?" )"2" (inst - "vsp!1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" vs_bands nil )nil extra_real_props nil )"nnreal" nil )"real" vs_bands nil )nil abs_lems "reals/" )nil real_props nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil real_props nil )"real" vs_bands nil )"(band!1)" vs_bands nil )"Connected" vs_bands nil )NOT const-decl "[bool -> bool]" booleans nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil reals nil )nil real_props nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"real" reals nil )nil cd_vertical nil )"posreal" vs_bands nil )"bool" cd_vertical nil )"(total_order?[real])" nil )nil Lookahead nil )nil vs_bands nil )"(strict_total_order?[real])" real_props nil )nil vertical nil )"(strict_total_order?[real])" real_props nil )nil reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" reals nil )"posreal" nil )"nzreal" nil )nil vertical nil )"odd_int" integers nil )"bool" vs_bands nil )"real" reals nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )nil numbers nil )nil booleans 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 )"boolean" notequal nil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"Sign" sign "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"nnreal" vs_bands nil )"[numfield, numfield -> numfield]" number_fields nil )set type-eq-decl nil sets nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil connected_set "reals/" )nil real_types nil )"bool" reals nil )nil real_types nil )"{AB: posreal | AB > B}" vs_bands nil )"bool" vs_bands nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.0.784Bemerkung:
(vorverarbeitet am 2026-04-26)
¤ *Bot Zugriff
2026-05-26
