Quelle vs_bands.prf
Sprache: Lisp
(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)"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" quality 100%
¤ Dauer der Verarbeitung: 0.59 Sekunden
(vorverarbeitet)
¤ *Bot Zugriff
2026-03-28
