Quelle wedge_optimum_2D.prf
Sprache: Lisp
(wedge_optimum_2Dnil 3530552207"" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"(strict_total_order?[real])" real_props nil )"real" vectors_2D "vectors/" )"real" reals nil ))nil ))nil 3530552207"" (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 )nil vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"(strict_total_order?[real])" real_props nil )"Vector" vectors_2D "vectors/" )"real" vectors_2D "vectors/" )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3530552207"" (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 )nil vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"(strict_total_order?[real])" real_props nil )"Vector" vectors_2D "vectors/" )"real" vectors_2D "vectors/" )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3530552207"" (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 )nil vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"(strict_total_order?[real])" real_props nil )"Vector" vectors_2D "vectors/" )"real" vectors_2D "vectors/" )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3530552296"" case "FORALL (p,w,v,a,b,e1,e2): intersects_segment_fun?(p,w,v,a,b,e1,e2) = intersects_segment?(p,w,v,a,b,e1,e2)" )"1" (decompose-equality) nil nil )"2" (hide 2)"2" (skeep)"2" (expand "intersects_segment_fun?" )"2" "tlow1" "IF v * e1 > 0 THEN ((p - w) * e1) / (v * e1) AND (w - p) * e1 < 0 THEN 1 + b") "1" (replace -1)"1" "thigh1" "IF v * e1 < 0 THEN ((p - w) * e1) / (v * e1) AND (w - p) * e1 < 0 THEN a - 1") "1" (replace -1)"1" "tlow2" "IF v * e2 > 0 THEN ((p - w) * e2) / (v * e2) AND (w - p) * e2 < 0 THEN 2 + b") "1" (replace -1)"1" "thigh2" "IF v * e2 < 0 THEN ((p - w) * e2) / (v * e2) AND (w - p) * e2 < 0 THEN a - 2") "1" (replace -1)"1" (name "tlow" "max(max(tlow1,tlow2),a)" )"1" (replace -1)"1" "thigh" "min(min(thigh1,thigh2),b)" )"1" replace -1)"1" case "NOT (FORALL (t:real): (a<=t AND t<=b AND (w+t*v-p)*e1>=0 AND (w+t*v-p)*e2>=0) IFF (tlow <= t AND t<=thigh))" )"1" "1" "1" "1" expand "tlow" )"1" case "t>=tlow1 AND t>=tlow2" )"1" "1" expand "max" )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "tlow1" )"1" "1" assert )"1" "1" "1" "1" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "tlow2" )"2" "2" assert )"2" "1" "1" "1" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" assert )"3" "3" expand "tlow2" 1)"3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "thigh" )"2" case "t<=thigh1 AND t<=thigh2" )"1" "1" expand "min" )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "thigh1" )"1" "1" assert )"1" "1" "1" "1" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "thigh2" )"2" "2" assert )"2" "1" "1" "1" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" expand "thigh2" 1)"3" nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "tlow" )"3" expand "thigh" )"3" case "t>=tlow1 AND t<=thigh1" )"1" "1" "1" expand "thigh1" )"1" expand "tlow1" )"1" "1" "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" "1" "1" assert )nil nil ))nil )"2" "2" assert )"2" "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "1" nil nil )"2" case "v*e1 = 0" )"1" "t" )"1" "1" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "min" )"2" expand "max" )"2" "2" "2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "thigh1" +)"3" nil nil ))nil ))nil ))nil ))nil ))nil )"4" expand "thigh" )"4" expand "tlow" )"4" case "tlow2 <= t AND t<=thigh2" )"1" "1" "1" expand "thigh2" )"1" expand "tlow2" )"1" "1" "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" "1" "1" assert )nil nil ))nil )"2" "2" assert )"2" "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" "2" case "v*e2 = 0" )"1" "t" )"1" "1" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "min" )"2" expand "max" )"2" "2" "2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "thigh2" +)"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" "tlow" )"1" expand "intersects_segment?" )"1" assert )"1" "1" "tlow" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "intersects_segment?" )"2" "2" "t" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "thigh2" )"2" (ground) nil nil ))nil ))nil )"3" "3" expand "thigh1" )"3" (ground) nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" expand "tlow2" )"2" (ground) nil nil ))nil ))nil )"3" (hide-all-but 1)"3" expand "tlow1" )"3" (ground) nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (ground) nil nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (ground) nil nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (ground) nil nil )) nil ))nil ))nil )"2" (hide-all-but 1) (("2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" reals nil )nil real_types nil )nil real_types nil )nil real_props nil )"numfield" wedge_optimum_2D nil )"numfield" wedge_optimum_2D nil )"{p: real | p >= max(tlow1, tlow2) AND p >= a}" wedge_optimum_2Dnil )nil real_types nil )nil real_types nil )nil real_props nil )"numfield" wedge_optimum_2D nil )"numfield" wedge_optimum_2D nil )"{p: real | p <= min(thigh1, thigh2) AND p <= b}" wedge_optimum_2Dnil )nil extra_real_props nil )"Vect2" wedge_optimum_2D nil )"Nz_vect2" wedge_optimum_2D nil )"Nz_vect2" wedge_optimum_2D nil )nil real_props nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil )nil number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil )"real" vectors_2D "vectors/" )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"Vector" vectors_2D "vectors/" )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )nil vectors_2D_def "vectors/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil booleans nil )"[T, T -> boolean]" equalities nil )"bool" wedge_optimum_2D nil )"bool" wedge_optimum_2D nil ))nil )nil 3530552265"" (skeep)"" "mspis" "max_segment_point_in_slice(p, w, v, a, b, e1, e2)" )"" (label "mspisdef" -1)"" (replace -1)"" (assert )"" (expand "max_segment_point_in_slice" )"" "tlow1" "IF v * e1 > 0 THEN ((p - w) * e1) / (v * e1) AND (w - p) * e1 < 0 THEN 1 + b") "1" (replace -1)"1" "thigh1" "IF v * e1 < 0 THEN ((p - w) * e1) / (v * e1) AND (w - p) * e1 < 0 THEN a - 1") "1" (replace -1)"1" "tlow2" "IF v * e2 > 0 THEN ((p - w) * e2) / (v * e2) AND (w - p) * e2 < 0 THEN 2 + b") "1" (replace -1)"1" "thigh2" "IF v * e2 < 0 THEN ((p - w) * e2) / (v * e2) AND (w - p) * e2 < 0 THEN a - 2") "1" (replace -1)"1" case "v = zero" )"1" replace -1)"1" assert )"1" replace "mspisdef" :dir rl)"1" "1" "1" expand "on_segment_in_wedge?" )"1" assert )"1" expand "intersects_segment?" )"1" "1" assert )"1" "t" )"1" assert )nil )))))))))))))))"2" "2" expand "on_segment_in_wedge?" )"2" "2" assert )nil )))))))))))))))"2" "vnz" 1)"2" "vnz" )"2" "tlow" "max(max(tlow1,tlow2),a)" )"1" replace -1)"1" "thigh" "min(min(thigh1,thigh2),b)" )"1" replace -1)"1" "aa" "sqv(v)" )"1" replace -1)"1" "bb" "2*(v*(w-p))" )"1" "1" "tlow" )"1" replace -1)"1" "1" "thigh" )"1" replace "1" "1" "cc" "sqv(w-p)" )"1" case "NOT (FORALL (t:real): (a<=t AND t<=b AND (w+t*v-p)*e1>=0 AND (w+t*v-p)*e2>=0) IFF (tlow <= t AND t<=thigh))" )"1" "1" "1" "1" expand "tlow" )"1" case "t>=tlow1 AND t>=tlow2" )"1" "1" expand "max" )"1" "1" "1" "1" assert )nil )))))))))))"2" "2" "1" expand "tlow1" )"1" "1" assert )"1" "1" "1" "1" nil )))))"2" "2" nil )))))))))))"2" expand "tlow2" )"2" "2" assert )"2" "1" "1" "1" nil )))))"2" "2" nil )))))))))))))))"3" assert )"3" "3" expand "tlow2" "3" nil )))))))))))"2" expand "thigh" )"2" case "t<=thigh1 AND t<=thigh2" )"1" "1" expand "min" )"1" "1" "1" "1" assert )nil )))))))))))"2" "2" "1" expand "thigh1" )"1" "1" assert )"1" "1" "1" "1" nil )))))"2" "2" nil )))))))))))"2" expand "thigh2" )"2" "2" assert )"2" "1" "1" "1" nil )))))"2" "2" nil )))))))))))))))"3" "3" "3" expand "thigh2" "3" nil )))))))))))"3" expand "tlow" )"3" expand "thigh" )"3" case "t>=tlow1 AND t<=thigh1" )"1" "1" "1" expand "thigh1" )"1" expand "tlow1" )"1" "1" "1" "1" "1" "1" nil )))))))"2" "2" "1" "1" assert )nil )))"2" "2" assert )"2" "1" "1" "1" "1" nil )))))))"2" "2" assert )"2" "1" nil )"2" case "v*e1 = 0" )"1" "t" )"1" "1" nil )))))"2" assert )nil )))))))))))))))))))))))))))))))"2" expand "min" )"2" expand "max" )"2" "2" "2" "2" assert )"2" nil )))))))))))))"3" "3" expand "thigh1" "3" nil )))))))))))"4" expand "thigh" )"4" expand "tlow" )"4" case "tlow2 <= t AND t<=thigh2" )"1" "1" "1" expand "thigh2" )"1" expand "tlow2" )"1" "1" "1" "1" "1" "1" nil )))))))"2" "2" "1" "1" assert )nil )))"2" "2" assert )"2" "1" "1" "1" "1" nil )))))))"2" "2" "2" case "v*e2 = 0" )"1" "t" )"1" "1" nil )))))"2" assert )nil )))))))))))))))))))))))))))))"2" expand "min" )"2" expand "max" )"2" "2" "2" "2" assert )"2" nil )))))))))))))"3" "3" expand "thigh2" "3" nil )))))))))))))))))"2" "intdef" "2" "ff" "quadratic(aa,bb,cc)" )"2" "ffdef" "2" case "aa * tlow ^ 2 + bb * tlow <= aa * thigh ^ 2 + bb * thigh IFF ff(tlow)<=ff(thigh)" )"1" replace "1" "maxt" "IF ff(tlow) <= ff(thigh) THEN thigh ELSE tlow ENDIF" )"1" "maxtname" "1" replace "1" "1" "1" expand "intersects_segment?" )"1" "1" "intdef" )"1" "t" )"1" assert )"1" "1" expand "on_segment_in_wedge?" )"1" "maxt" )"1" "maxt" )"1" assert )"1" case "tlow <= maxt AND maxt <= thigh" )"1" replace "1" assert )"1" "1" nil )))))))"2" "2" "2" expand "maxt" "2" "2" nil )))))))))))))))))))))))))))))))))"2" "2" expand "on_segment_in_wedge?" )"2" "2" "intdef" )"2" "t" )"2" assert )"2" "2" case "ff(t)<=ff(maxt)" )"1" rewrite "sq_le" "1" rewrite "sq_norm" )"1" rewrite "sq_norm" )"1" replace "1" replace "mspisdef" "1" "1" expand "ff" )"1" expand "aa" )"1" expand "bb" )"1" expand "cc" )"1" nil )))))))))))))))))))))"2" "maxtname" "2" case "tlow <= maxt AND maxt <= thigh" )"1" "quad_intv_max_at_endpoint" )"1" "aa" "bb" "cc" "tlow" "thigh" )"1" assert )"1" case "aa > 0" )"1" assert )"1" "1" "1" "t" )"1" assert )"1" expand "ff" )"1" "1" nil )))))))))"2" "t" )"2" assert )"2" expand "ff" )"2" "2" nil )))))))))))))))"2" "vnz" )"2" expand "aa" "2" "sqv_eq_0" )"2" "2" assert )nil )))))))))))))"2" "vnz" )"2" expand "aa" "2" "sqv_eq_0" )"2" "2" assert )nil )))))))))))))"2" "2" nil )))))))))))))))))))))))))))))))))"2" "2" expand "ff" )"2" nil )))))))))))))))))))))))))))))))))))))))"2" "2" "mspisdef" )"2" expand "thigh2" +)"2" nil )))))))"3" "3" expand "thigh1" +)"3" nil )))))))))"2" "2" expand "tlow2" +)"2" (ground) nil )))))"3" "3" expand "tlow1" +)"3" nil )))))))))))))))"2" (hide-all-but 1)"2" (ground) nil )))))))"2" (hide-all-but 1)"2" (ground) nil )))))))"2" (hide-all-but 1) (("2" (ground) nil )))))))"2" (hide-all-but 1)"2" (ground) nil ))))))))))))))))nil )nil nil )nil 3530552209"" case "FORALL (p,w,v,a,b,e1,e2): intersects_segment_fun?(p,w,v,a,b,e1,e2) = intersects_segment?(p,w,v,a,b,e1,e2)" )"1" (decompose-equality) nil nil )"2" (hide 2) (("2" (postpone) nil nil )) nil ))nil )nil shostak))nil 3530541790"" (skeep)"" (ground)"1" (expand "intersects_segment?" )"1" (skeep -1)"1" (inst + "t" ) (("1" (assert ) nil nil )) nil )) nil ))nil )"2" (expand "intersects_segment?" )"2" (skeep -1)"2" (inst + "t" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" wedge_optimum_2D nil ))nil 3530541841"" (skeep)"" (decompose-equality)"" (iff)"" (ground)"1" (expand "on_segment_in_wedge?" )"1" (skeep -1)"1" (inst + "t" ) (("1" (assert ) nil nil )) nil )) nil ))nil )"2" (expand "on_segment_in_wedge?" )"2" (skeep -1)"2" (inst + "t" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil booleans nil )"bool" wedge_optimum_2D nil )nil booleans nil )nil vectors_2D_def "vectors/" )nil reals nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil 3530522510"" (skosimp*)"" (lemma "sqv_eq_0" ) (("" (inst?) (("" (assert ) nil nil )) nil ))nil ))nil )nil vectors_2D "vectors/" )"nnreal" nil )"real" reals nil )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )nil reals nil ))nil ))nil 3530522510"" (subtype-tcc) nil nil )"real" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"boolean" notequal nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3530522510"" (subtype-tcc) nil nil )"real" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"boolean" notequal nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3530525223"" (skeep)"" "mspis" "max_segment_point_in_slice(p, w, v, a, b, e1, e2)" )"" (label "mspisdef" -1)"" (replace -1)"" (assert )"" (expand "max_segment_point_in_slice" )"" "tlow1" "IF v * e1 > 0 THEN ((p - w) * e1) / (v * e1) AND (w - p) * e1 < 0 THEN 1 + b") "1" (replace -1)"1" "thigh1" "IF v * e1 < 0 THEN ((p - w) * e1) / (v * e1) AND (w - p) * e1 < 0 THEN a - 1") "1" (replace -1)"1" "tlow2" "IF v * e2 > 0 THEN ((p - w) * e2) / (v * e2) AND (w - p) * e2 < 0 THEN 2 + b") "1" (replace -1)"1" "thigh2" "IF v * e2 < 0 THEN ((p - w) * e2) / (v * e2) AND (w - p) * e2 < 0 THEN a - 2") "1" (replace -1)"1" case "v = zero" )"1" replace -1)"1" assert )"1" replace "mspisdef" :dir rl)"1" "1" "1" expand "on_segment_in_wedge?" )"1" assert )"1" expand "intersects_segment?" )"1" "1" assert )"1" "t" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "on_segment_in_wedge?" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "vnz" 1)"2" "vnz" )"2" "tlow" "max(max(tlow1,tlow2),a)" )"1" replace -1)"1" "thigh" "min(min(thigh1,thigh2),b)" )"1" replace -1)"1" "aa" "sqv(v)" )"1" replace -1)"1" "bb" "2*(v*(w-p))" )"1" "1" "tlow" )"1" replace -1)"1" "1" "thigh" )"1" replace "1" "1" "cc" "sqv(w-p)" )"1" case "NOT (FORALL (t:real): (a<=t AND t<=b AND (w+t*v-p)*e1>=0 AND (w+t*v-p)*e2>=0) IFF (tlow <= t AND t<=thigh))" )"1" "1" "1" "1" expand "tlow" )"1" case "t>=tlow1 AND t>=tlow2" )"1" "1" expand "max" )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "tlow1" )"1" "1" assert )"1" "1" "1" "1" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "tlow2" )"2" "2" assert )"2" "1" "1" "1" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" assert )"3" "3" expand "tlow2" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "thigh" )"2" case "t<=thigh1 AND t<=thigh2" )"1" "1" expand "min" )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "thigh1" )"1" "1" assert )"1" "1" "1" "1" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "thigh2" )"2" "2" assert )"2" "1" "1" "1" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" expand "thigh2" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "tlow" )"3" expand "thigh" )"3" case "t>=tlow1 AND t<=thigh1" )"1" "1" "1" expand "thigh1" )"1" expand "tlow1" )"1" "1" "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" "1" "1" assert )nil nil ))nil )"2" "2" assert )"2" "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "1" nil nil )"2" case "v*e1 = 0" )"1" "t" )"1" "1" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "min" )"2" expand "max" )"2" "2" "2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "thigh1" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"4" expand "thigh" )"4" expand "tlow" )"4" case "tlow2 <= t AND t<=thigh2" )"1" "1" "1" expand "thigh2" )"1" expand "tlow2" )"1" "1" "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" "1" "1" assert )nil nil ))nil )"2" "2" assert )"2" "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" "2" case "v*e2 = 0" )"1" "t" )"1" "1" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "min" )"2" expand "max" )"2" "2" "2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "thigh2" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "intdef" "2" "ff" "quadratic(aa,bb,cc)" )"2" "ffdef" "2" case "aa * tlow ^ 2 + bb * tlow <= aa * thigh ^ 2 + bb * thigh IFF ff(tlow)<=ff(thigh)" )"1" replace "1" "maxt" "IF ff(tlow) <= ff(thigh) THEN thigh ELSE tlow ENDIF" )"1" "maxtname" "1" replace "1" "1" "1" expand "intersects_segment?" )"1" "1" "intdef" )"1" "t" )"1" assert )"1" "1" expand "on_segment_in_wedge?" )"1" "maxt" )"1" "maxt" )"1" assert )"1" case "tlow <= maxt AND maxt <= thigh" )"1" replace "1" assert )"1" "1" nil nil ))nil ))nil ))nil )"2" "2" "2" expand "maxt" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "on_segment_in_wedge?" )"2" "2" "intdef" )"2" "t" )"2" assert )"2" "2" case "ff(t)<=ff(maxt)" )"1" rewrite "sq_le" "1" rewrite "sq_norm" )"1" rewrite "sq_norm" )"1" replace "1" replace "mspisdef" "1" "1" expand "ff" )"1" expand "aa" )"1" expand "bb" )"1" expand "cc" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "maxtname" "2" case "tlow <= maxt AND maxt <= thigh" )"1" "quad_intv_max_at_endpoint" )"1" "aa" "bb" "cc" "tlow" "thigh" )"1" assert )"1" case "aa > 0" )"1" assert )"1" "1" "1" "t" )"1" assert )"1" expand "ff" )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "t" )"2" assert )"2" expand "ff" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "vnz" )"2" expand "aa" "2" "sqv_eq_0" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "vnz" )"2" expand "aa" "2" "sqv_eq_0" )"2" "2" assert )nil 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 )"2" "2" expand "ff" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "mspisdef" )"2" expand "thigh2" +)"2" nil nil ))nil ))nil ))nil )"3" "3" expand "thigh1" +)"3" (ground) nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "tlow2" +)"2" (ground) nil nil ))nil ))nil )"3" "3" expand "tlow1" +)"3" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (ground) nil nil )) nil ))nil ))nil )"2" (hide-all-but 1) (("2" (ground) nil nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (ground) nil nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"Vect2" wedge_optimum_2Dnil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil vectors_2D_def "vectors/" )nil reals nil )"bool" reals nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil real_types nil )"nnreal" vectors_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )nil extra_real_props nil )"nnreal" nil )"real" exponentiation nil )"real" wedge_optimum_2D nil )nil vectors_2D "vectors/" )"nnreal" wedge_optimum_2D nil )"nnreal" wedge_optimum_2D nil )"nonneg_real" sq "reals/" )"real" wedge_optimum_2D nil )"[real -> real]" wedge_optimum_2D nil )nil sq "reals/" )"nnreal" vectors_2D "vectors/" )nil reals nil )nil vectors_2D "vectors/" )nil quad_minmax "reals/" )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"real" quadratic "reals/" )nil real_types nil )nil real_types nil )nil real_props nil )"numfield" wedge_optimum_2D nil )"numfield" wedge_optimum_2D nil )"{p: real | p >= max(tlow1, tlow2) AND p >= a}" wedge_optimum_2Dnil )nil real_types nil )nil real_types nil )nil real_props nil )"numfield" wedge_optimum_2D nil )"numfield" wedge_optimum_2D nil )"{p: real | p <= min(thigh1, thigh2) AND p <= b}" wedge_optimum_2Dnil )"Vect2" wedge_optimum_2D nil )"Nz_vect2" wedge_optimum_2D nil )"Nz_vect2" wedge_optimum_2D nil )nil real_props nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"bool" wedge_optimum_2D nil )"bool" wedge_optimum_2D nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil )nil number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil booleans nil )"bool" reals nil )"real" vectors_2D "vectors/" )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"Vector" vectors_2D "vectors/" )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil )nil 3530525066"" (skeep)"" "mspis" "max_segment_point_in_slice(p, w, v, a, b, e1, e2)" )"" (label "mspisdef" -1)"" (replace -1)"" (assert )"" (expand "max_segment_point_in_slice" )"" (case "NOT (v*e1 = 0 OR v*e2=0)" )"1" (label "vdotnz" 1)"1" (hide "vdotnz" )"1" "tlow1" "IF v * e1 > 0 THEN ((p - w) * e1) / (v * e1) ") "1" (replace -1)"1" "thigh1" "IF v*e1<0 THEN ((p-w)*e1)/(v*e1) ELSE b ENDIF" )"1" (replace -1)"1" "tlow2" "IF v*e2>0 THEN ((p-w)*e2)/(v*e2) ELSE a ENDIF" )"1" replace -1)"1" "thigh2" "IF v * e2 < 0 THEN ((p - w) * e2) / (v * e2) ") "1" replace -1)"1" "tlow" "max(max(tlow1,tlow2),a)" )"1" replace -1)"1" "thigh" "min(min(thigh1,thigh2),b)" )"1" replace -1)"1" "aa" "sqv(v)" )"1" replace -1)"1" "bb" "2*(v*(w-p))" )"1" "1" "tlow" )"1" replace -1)"1" "1" "thigh" )"1" replace "1" "1" "cc" "sqv(w-p)" )"1" case "NOT (FORALL (t:real): (a<=t AND t<=b AND (w+t*v-p)*e1>=0 AND (w+t*v-p)*e2>=0) IFF (tlow <= t AND t<=thigh))" )"1" "1" "1" "1" expand "tlow" )"1" case "t>=tlow1 AND t>=tlow2" )"1" "1" expand "max" )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "tlow1" )"1" "1" assert )"1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "tlow2" )"2" "2" assert )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" assert )"3" "3" expand "tlow2" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "thigh" )"2" case "t<=thigh1 AND t<=thigh2" )"1" "1" expand "min" )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "thigh1" )"1" "1" assert )"1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "thigh2" )"2" "2" assert )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" expand "thigh2" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "tlow" )"3" expand "thigh" )"3" case "t>=tlow1 AND t<=thigh1" )"1" "1" "1" expand "thigh1" )"1" expand "tlow1" )"1" "1" "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" "vdotnz" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "min" )"2" expand "max" )"2" "2" "2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "thigh1" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"4" expand "thigh" )"4" expand "tlow" )"4" case "tlow2 <= t AND t<=thigh2" )"1" "1" "1" expand "thigh2" )"1" expand "tlow2" )"1" "1" "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" "vdotnz" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "min" )"2" expand "max" )"2" "2" "2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "thigh2" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "intdef" "2" "ff" "quadratic(aa,bb,cc)" )"2" "ffdef" "2" case "aa * tlow ^ 2 + bb * tlow <= aa * thigh ^ 2 + bb * thigh IFF ff(tlow)<=ff(thigh)" )"1" replace "1" "maxt" "IF ff(tlow) <= ff(thigh) THEN thigh ELSE tlow ENDIF" )"1" replace "1" "1" "1" expand "intersects_segment?" )"1" "1" "intdef" )"1" "t" )"1" assert )"1" "1" expand "on_segment_in_wedge?" )"1" "maxt" )"1" "maxt" )"1" assert )"1" case "tlow <= maxt AND maxt <= thigh" )"1" replace "1" assert )"1" "1" nil nil ))nil ))nil ))nil )"2" "2" "2" expand "maxt" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "on_segment_in_wedge?" )"2" "2" "intdef" )"2" "t" )"2" assert )"2" "2" case "ff(t)<=ff(maxt)" )"1" rewrite "sq_le" "1" rewrite "sq_norm" )"1" rewrite "sq_norm" )"1" replace "1" replace "mspisdef" "1" "1" expand "ff" )"1" expand "aa" )"1" expand "bb" )"1" expand "cc" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil )"3" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil )"3" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil 3530524985"" (skeep)"" "mspis" "max_segment_point_in_slice(p, w, v, a, b, e1, e2)" )"" (replace -1)"" (assert )"" (expand "max_segment_point_in_slice" )"" (case "NOT (v*e1 = 0 OR v*e2=0)" )"1" (label "vdotnz" 1)"1" (hide "vdotnz" )"1" "tlow1" "IF v * e1 > 0 THEN ((p - w) * e1) / (v * e1) ") "1" (replace -1)"1" "thigh1" "IF v*e1<0 THEN ((p-w)*e1)/(v*e1) ELSE b ENDIF" )"1" (replace -1)"1" "tlow2" "IF v*e2>0 THEN ((p-w)*e2)/(v*e2) ELSE a ENDIF" )"1" (replace -1)"1" "thigh2" "IF v * e2 < 0 THEN ((p - w) * e2) / (v * e2) ") "1" replace -1)"1" "tlow" "max(max(tlow1,tlow2),a)" )"1" replace -1)"1" "thigh" "min(min(thigh1,thigh2),b)" )"1" replace -1)"1" "aa" "sqv(v)" )"1" replace -1)"1" "bb" "2*(v*(w-p))" )"1" "1" "tlow" )"1" replace -1)"1" "1" "thigh" )"1" replace "1" "1" "cc" "sqv(w-p)" )"1" case "NOT (FORALL (t:real): (a<=t AND t<=b AND (w+t*v-p)*e1>=0 AND (w+t*v-p)*e2>=0) IFF (tlow <= t AND t<=thigh))" )"1" "1" "1" "1" expand "tlow" )"1" case "t>=tlow1 AND t>=tlow2" )"1" "1" expand "max" )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "tlow1" )"1" "1" assert )"1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "tlow2" )"2" "2" assert )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" assert )"3" "3" expand "tlow2" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "thigh" )"2" case "t<=thigh1 AND t<=thigh2" )"1" "1" expand "min" )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "thigh1" )"1" "1" assert )"1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "thigh2" )"2" "2" assert )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" expand "thigh2" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "tlow" )"3" expand "thigh" )"3" case "t>=tlow1 AND t<=thigh1" )"1" "1" "1" expand "thigh1" )"1" expand "tlow1" )"1" "1" "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" "vdotnz" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "min" )"2" expand "max" )"2" "2" "2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "thigh1" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"4" expand "thigh" )"4" expand "tlow" )"4" case "tlow2 <= t AND t<=thigh2" )"1" "1" "1" expand "thigh2" )"1" expand "tlow2" )"1" "1" "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" "vdotnz" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "min" )"2" expand "max" )"2" "2" "2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "thigh2" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "intdef" "2" "ff" "quadratic(aa,bb,cc)" )"2" "ffdef" "2" case "aa * tlow ^ 2 + bb * tlow <= aa * thigh ^ 2 + bb * thigh IFF ff(tlow)<=ff(thigh)" )"1" replace "1" "maxt" "IF ff(tlow) <= ff(thigh) THEN thigh ELSE tlow ENDIF" )"1" replace "1" "1" "1" expand "intersects_segment?" )"1" "1" "intdef" )"1" "t" )"1" assert )"1" "1" expand "on_segment_in_wedge?" )"1" "maxt" )"1" "maxt" )"1" assert )"1" case "tlow <= maxt AND maxt <= thigh" )"1" replace "1" assert )"1" "1" nil nil ))nil ))nil ))nil )"2" "2" "2" expand "maxt" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "on_segment_in_wedge?" )"2" "2" "intdef" )"2" "t" )"2" assert )"2" "2" case "ff(t)<=ff(maxt)" )"1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil )"3" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil )"3" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil 3530522984"" (skeep)"" "mspis" "max_segment_point_in_slice(p, w1, v, a, b, e1, e2)" )"" (replace -1)"" (assert )"" (expand "max_segment_point_in_slice" )"" (case "NOT (v*e1 = 0 OR v*e2=0)" )"1" (label "vdotnz" 1)"1" (hide "vdotnz" )"1" "tlow1" "IF v * e1 > 0 THEN ((p - w1) * e1) / (v * e1) ") "1" (replace -1)"1" "thigh1" "IF v*e1<0 THEN ((p-w1)*e1)/(v*e1) ELSE b ENDIF" )"1" (replace -1)"1" "tlow2" "IF v*e2>0 THEN ((p-w1)*e2)/(v*e2) ELSE a ENDIF" )"1" (replace -1)"1" "thigh2" "IF v * e2 < 0 THEN ((p - w1) * e2) / (v * e2) ") "1" replace -1)"1" "tlow" "max(max(tlow1,tlow2),a)" )"1" replace -1)"1" "thigh" "min(min(thigh1,thigh2),b)" )"1" replace -1)"1" "aa" "sqv(v)" )"1" replace -1)"1" "bb" "2*(v*(w1-p))" )"1" "1" "tlow" )"1" replace -1)"1" "1" "thigh" )"1" replace "1" "1" "cc" "sqv(w1-p)" )"1" case "NOT (FORALL (t:real): (a<=t AND t<=b AND (w1+t*v-p)*e1>=0 AND (w1+t*v-p)*e2>=0) IFF (tlow <= t AND t<=thigh))" )"1" "1" "1" "1" expand "tlow" )"1" case "t>=tlow1 AND t>=tlow2" )"1" "1" expand "max" )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "tlow1" )"1" "1" assert )"1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "tlow2" )"2" "2" assert )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" assert )"3" "3" expand "tlow2" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "thigh" )"2" case "t<=thigh1 AND t<=thigh2" )"1" "1" expand "min" )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "thigh1" )"1" "1" assert )"1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "thigh2" )"2" "2" assert )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" expand "thigh2" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "tlow" )"3" expand "thigh" )"3" case "t>=tlow1 AND t<=thigh1" )"1" "1" "1" expand "thigh1" )"1" expand "tlow1" )"1" "1" "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" "vdotnz" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "min" )"2" expand "max" )"2" "2" "2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "thigh1" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"4" expand "thigh" )"4" expand "tlow" )"4" case "tlow2 <= t AND t<=thigh2" )"1" "1" "1" expand "thigh2" )"1" expand "tlow2" )"1" "1" "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" "vdotnz" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "min" )"2" expand "max" )"2" "2" "2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "thigh2" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "intdef" "2" "ff" "quadratic(aa,bb,cc)" )"2" "ffdef" "2" case "aa * tlow ^ 2 + bb * tlow <= aa * thigh ^ 2 + bb * thigh IFF ff(tlow)<=ff(thigh)" )"1" replace "1" "maxt" "IF ff(tlow) <= ff(thigh) THEN thigh ELSE tlow ENDIF" )"1" replace "1" "1" "1" expand "intersects_segment?" )"1" "1" "intdef" )"1" "t" )"1" assert )"1" "1" expand "on_segment_in_wedge?" )"1" "maxt" )"1" "maxt" )"1" assert )"1" case "tlow <= maxt AND maxt <= thigh" )"1" replace "1" assert )"1" "1" nil nil ))nil ))nil ))nil )"2" "2" "2" expand "maxt" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "on_segment_in_wedge?" )"2" "2" "intdef" )"2" "t" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil )"3" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil )"3" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak))nil 3530539881"" (skeep)"" (lemma "max_segment_point_in_slice_def" )"" (inst?)"" (assert )"" (flatten)"" (skeep)"" (split -)"1" (propax) nil nil )"2" (hide (-1 2))"2" (expand "intersects_segment?" )"2" (expand "on_segment_in_wedge?" )"2" (skeep -1)"2" (inst + "t" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil wedge_optimum_2Dnil )"bool" wedge_optimum_2D nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"bool" wedge_optimum_2D nil )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))
Messung V0.5 C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.871 Sekunden
¤ *© Formatika GbR, Deutschland
2026-04-08
