Quelle space_3D.prf
Sprache: Lisp
(space_3Dnil 3471198645"" (skeep)"" case "FORALL (s,v) : conflict?(s,v) IMPLIES conflict?(-s,-v)" )"1" (split)"1" (flatten)"1" (inst -2 "-s" "-v" ) (("1" (assert ) nil nil )) nil )) nil )"2" (inst? -1) nil nil ))nil )"2" (hide 2)"2" (skolem 1 ("sp" "vp" ))"2" (flatten)"2" (expand "conflict?" )"2" (skeep -1)"2" (inst 1 "nnt" )"2" (split 1)"1" (hide -2) (("1" (grind) nil nil )) nil )"2" (hide -1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"bool" space_3D nil )"[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil vectors_3D_def "vectors/" )nil reals nil )nil vectors_3D "vectors/" )"real" reals nil )"real" reals nil )nil real_types nil )"bool" reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"posreal" sq "reals/" )"posreal" nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )"real" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(strict_total_order?[real])" real_props nil )"real" reals nil ))nil 3470158403"" (skeep)"" (expand * "conflict?" "conflict_ever?" )"" (skeep -1) (("" (inst? 1) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )"bool" space_3D nil )"real" reals nil )"real" reals nil )"bool" space_3D nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posreal" sq "reals/" ))nil ))nil 3470158447"" (skeep)"" (split)"1" (flatten)"1" (expand "conflict_ever?" )"1" (skolem -1 "tt" )"1" (inst 1 "tt-t" )"1" (flatten)"1" (split)"1" (hide -2)"1" (expand * "+" "*" ) (("1" (assert ) nil nil ))nil ))nil )"2" (hide -1)"2" (rewrite "vect2_add" )"2" (rewrite "vect2_scal" )"2" "vect2(s) + tt * vect2(v) = vect2(s) + t * vect2(v) + (tt - t) * vect2(v)" )"2" (hide-all-but 1)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "conflict_ever?" )"2" (skolem -1 "tt" )"2" (inst 1 "tt+t" )"2" (flatten)"2" (split)"1" (hide -2)"1" (expand * "+" "*" ) (("1" (assert ) nil nil ))nil ))nil )"2" (hide -1)"2" "vect2(s + t * v) + tt * vect2(v) = vect2(s) + (tt + t) * vect2(v)" )"2" (hide-all-but 1)"2" (rewrite "vect2_add" )"2" (rewrite "vect2_scal" )"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )"bool" space_3D nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil vectors_3D "vectors/" )nil vectors_3D_def "vectors/" )nil vect_3D_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )"Vector" vectors_2D "vectors/" )"[T, T -> boolean]" equalities nil )nil vectors_2D "vectors/" )nil vect_3D_2D "vectors/" )"[numfield, numfield -> numfield]" number_fieldsnil ))nil ))nil 3467454344"" (skeep)"" (expand "conflict?" )"" (skosimp*)"" (case "nnt!1 = 0 and nnt!2 = 0" )"1" (flatten)"1" (inst + "0" )"1" (assert )"1" (replace -1) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (name "tt" "nnt!2/(nnt!1 + nnt!2)" )"1" (label "ttname" -1)"1" (case "0<=tt AND tt<=1" )"1" (flatten)"1" (name "newt" "(nnt!1*nnt!2)/(nnt!1 + nnt!2)" )"1" (label "newtname" -1)"1" case "tt*nnt!1 = newt AND (1-tt)*nnt!2 = newt" )"1" (flatten)"1" (label "newttt" -1)"1" (label "newtomtt" -2)"1" "newt" )"1" "VV" "vect2(s) + nnt!1 * vect2(v)" )"1" "vvname" -1)"1" "WW" "vect2(s) + nnt!2 * vect2(w)" )"1" "wwname" -1)"1" "VVz" "s`z + nnt!1 * v`z" )"1" "vvzname" -1)"1" "WWz" "s`z + nnt!2 * w`z" )"1" "wwzname" -1)"1" "VVt" "s+nnt!1*v" )"1" "vvtname" "1" "WWt" "s+nnt!2*w" )"1" "wwtname" "1" replace "wwzname" )"1" replace "vvzname" )"1" replace "wwname" )"1" replace "vvname" )"1" "horiz_dist_convex_scaf" )"1" "VVt" "WWt-VVt" )"1" case "s`z + newt * (v + w)`z = tt*VVz + (1-tt)*WWz AND vect2(s) + newt * vect2(v + w) = tt*VV+(1-tt)*WW" )"1" "1" "zfin" "1" "vectfin" "1" replace "zfin" )"1" replace "vectfin" )"1" case "convex?(LAMBDA (t): abs(t)-H)" )"1" assert )"1" "convex_wtd_av_lt" )"1" "0" "LAMBDA (t): abs(t) - H" "VVz" "WWz" )"1" "0" "LAMBDA (t): horiz_dist_scaf(VVt)(t, WWt - VVt)" "0" "1" )"1" assert )"1" expand "horiz_dist_scaf" "1" expand "horiz_dist_scaf" "1" assert )"1" case "vect2(VVt) = VV AND vect2(VVt)+vect2(WWt-VVt) = WW" )"1" "1" assert )"1" "tt" )"1" "tt" )"1" assert )"1" expand "horiz_dist_scaf" )"1" "vect2(VVt) + (1 - tt) * vect2(WWt - VVt) = tt * VV + (1 - tt) * WW" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "vvtname" "vvname" "wwtname" "wwname" "2" replace "wwtname" "2" replace "vvtname" "2" replace "vvname" "2" replace "wwname" "2" rewrite "vect2_add" )"2" rewrite "vect2_sub" )"2" rewrite "vect2_add" )"2" rewrite "vect2_add" )"2" rewrite "vect2_scal" )"2" rewrite "vect2_scal" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "abs_linear_convex" )"2" "H" "0" "1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "vvname" "2" replace "wwname" "2" replace "vvzname" "2" replace "wwzname" "2" assert )"2" "2" "1" "newtomtt" )"1" "w`z" )"1" assert )"1" replace "1" "1" replace "newttt" "1" rewrite "vz_distr_add" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "newttt" "newtomtt" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "nnreal_div_posreal_is_nnreal" )"2" "(nnt!1*nnt!2)" "nnt!1 + nnt!2" )"1" "newtname" 1))"1" (grind) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace "newtname" + rl)"2" (replace "ttname" + rl)"2" (hide-all-but (1 2))"2" "2" (field 2) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "nnreal_div_posreal_is_nnreal" )"2" (inst - "nnt!2" "nnt!1 + nnt!2" )"1" (replace "ttname" -)"1" (assert )"1" (replace "ttname" + rl)"1" (cross-mult 1) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )"bool" space_3D nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posreal" sq "reals/" )nil real_props nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil real_props nil )nil reals nil )nil real_props nil )"odd_int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )nil real_types nil )"nnreal" space_3D nil )"nnreal" space_3D nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )nil vectors_2D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"real" reals nil )"nnreal" nil )nil horizontal_dist_convexitynil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" space_3D nil )"bool" convex_functions "reals/" )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"posreal" space_3D nil )nil convex_functions "reals/" )"real" horizontal_dist_convexity nil )nil vectors_2D "vectors/" )nil vect_3D_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vect_3D_2D "vectors/" )nil vect_3D_2D "vectors/" )"(total_order?[real])" nil )nil convex_functions "reals/" )nil vectors_3D "vectors/" )nil extra_real_props nil )"Vector" vectors_3D "vectors/" )"real" space_3D nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"real" reals nil )"nnreal" nil ))nil )nil 3467382877"" (skeep)"" (expand "conflict?" )"" (skolem -1 "ntt1" )"" (skolem -2 "ntt2" )"" (flatten)"" (rewrite "vect2_add" ) (("" (postpone) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil shostak))nil 3566319824"" (skeep)"" (expand "conflict?" -1)"" (skosimp*)"" (label "underH" -1)"" (label "underD" -2)"" (case "nnt!1 /= 0" )"1" (flatten)"1" (name "del1" "H - abs(ss`z + nnt!1 * vv`z)" )"1" (label "del1name" -1)"1" "del2" "D - norm(vect2(ss) + nnt!1 * vect2(vv))" )"1" (label "del2name" -1)"1" (case "del2 > 0" )"1" (label "del2pos" -1)"1" (hide "del2pos" )"1" "delta" "min(del1,del2)" )"1" "deltaname" -1)"1" "delta/(2*nnt!1)" )"1" "1" case "norm(ww) >= abs(ww`z) AND norm(ww) >= norm(vect2(ww))" )"1" "normlem" -1)"1" "normlem" )"1" expand "conflict?" )"1" "nnt!1" )"1" "1" "triangle" )"1" rewrite "vz_distr_add" )"1" assert )"1" "ss`z + vv`z*nnt!1" "ww`z*nnt!1" )"1" case "abs(ww`z*nnt!1) < del1" )"1" assert )nil nil )"2" "2" rewrite "abs_mult" )"2" case "abs(nnt!1) = nnt!1" )"1" replace "1" "normlem" )"1" "1" "nnt!1" )"1" case "del1 / nnt!1 >= delta / (2 * nnt!1)" )"1" assert )nil nil )"2" "2" "2" "nnt!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "norm(vect2(ss) + nnt!1 * vect2(vv + ww)) < D" )"1" "sq_lt" )"1" "1" assert )"1" "vectors_2D.sqrt_sqv_norm" )"1" "1" replace "1" rewrite "vect2_add" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "vect2_add" )"2" "vectors_2D.norm_add_le" )"2" "vect2(ss) + nnt!1*vect2(vv)" "nnt!1*vect2(ww)" )"2" assert )"2" case "norm(nnt!1 * vect2(ww)) + norm(vect2(ss) + nnt!1 * vect2(vv)) < D" )"1" case "vect2(ss) + nnt!1 * vect2(vv) + nnt!1 * vect2(ww) = vect2(ss) + nnt!1 * (vect2(vv) + vect2(ww))" )"1" assert )nil nil )"2" "2" "2" nil nil ))nil ))nil ))nil )"2" case "norm(nnt!1*vect2(ww)) < del2" )"1" assert )nil nil )"2" "2" "2" rewrite "norm_scal" )"2" case "abs(nnt!1) = nnt!1" )"1" replace "1" "nnt!1" )"1" case "del2 / nnt!1 >= delta/(2*nnt!1)" )"1" "normlem" )"1" "1" assert )nil nil ))nil ))nil )"2" "2" "2" "nnt!1" )"2" case "2*del2 >= delta" )"1" assert )nil nil )"2" case "del2 > 0" )"1" "deltaname" "1" nil nil ))nil )"2" replace "del2name" "2" "underD" "2" case "sqv(vect2(ss) + nnt!1 * vect2(vv)) = sq(norm(vect2(ss) + nnt!1 * vect2(vv)))" )"1" replace "1" "1" "sq_lt" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "cvect1" "vect2(ss) + nnt!1 * vect2(vv)" )"2" replace "2" "2" expand "norm" )"2" "sq_sqrt" )"2" "2" "1" assert )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 )"2" expand "abs" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "norm" )"1" expand "sqv" )"1" "sq_ge" )"1" "1" assert )"1" "1" expand "*" )"1" expand "sq" "1" "sqrt_ge" )"1" "ww`x * ww`x + ww`y * ww`y + ww`z * ww`z" "ww`z*ww`z" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "sqv(ww)" )"2" expand "sqv" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "norm" )"2" expand "sqv" )"2" "sqrt_ge" )"2" "1" assert )"1" "1" nil nil ))nil ))nil )"2" "sqv(vect2(ww))" )"2" expand "sqv" )"2" nil nil ))nil ))nil )"3" "sqv(ww)" )"3" expand "sqv" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "delta /( 2*nnt!1) > 0" )"1" (assert ) nil nil )"2" "2" "2" "del2pos" )"2" case "delta = del1 or delta = del2" )"1" (ground) nil nil )"2" "deltaname" 1))"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "sq_lt" )"2" "norm(vect2(ss) + nnt!1 * vect2(vv))" "D" )"2" assert )"2" "cvect3" "vect2(ss) + nnt!1 * vect2(vv)" )"2" replace -1)"2" case "sqv(cvect3) = sq(norm(cvect3))" )"1" (assert ) nil nil )"2" "2" "vectors_2D.sqrt_sqv_norm" )"2" "2" replace -1 :dir rl)"2" "2" "sq_sqrt" )"2" "2" "1" assert )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 )"2" (flatten)"2" (replace -1)"2" (assert )"2" (inst + "1" )"2" (skeep)"2" (expand "conflict?" )"2" (inst + "0" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )"bool" space_3D 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 )"boolean" notequal nil )nil booleans nil )nil numbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_3D_def "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" space_3D nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"posreal" space_3D nil )nil vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil extra_real_props nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" vectors_2D "vectors/" )nil sq "reals/" )NOT const-decl "[bool -> bool]" booleans nil )nil sq "reals/" )nil sqrt "reals/" )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"Vect3" space_3D nil )"real" vectors_3D "vectors/" )"nnreal" vectors_3D "vectors/" )nil vectors_3D "vectors/" )nil real_props nil )nil extra_real_props nil )nil reals nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )"nnreal" nil )"(total_order?[real])" nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"posreal" sq "reals/" )nil real_props nil )nil vectors_2D "vectors/" )nil extra_real_props nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil sq "reals/" )nil vect_3D_2D "vectors/" )nil sqrt "reals/" )nil vectors_2D "vectors/" )"Vector" vectors_3D "vectors/" )"nnreal" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"{p: real | p <= del1 AND p <= del2}" nil )"real" space_3D nil )"real" space_3D nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"nnreal" space_3D nil )"nnreal" nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" ))nil ))nil 3432042079"" (skeep)"" (expand "conflict?" )"" (skeep -1)"" (split)"1" (expand "vertical_conflict?" ) (("1" (inst? 1) nil nil ))nil )"2" (expand "horizontal_conflict?" )"2" (inst? 1) nil nil )) nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )"bool" space_3D 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 )nil booleans nil )nil numbers nil )"bool" vertical nil )"bool" horizontal nil ))nil 3451660364 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil vectors_3D_def "vectors/" )"bool" reals nil )nil real_types nil )"posreal" space_3D nil )nil space_3D nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"Vector" vectors_3D "vectors/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil ))nil ))nil 3471185533 ("" (judgement-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil vectors_2D "vectors/" )nil real_types nil )nil vectors_3D_def "vectors/" )nil vectors_2D_def "vectors/" )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" space_3D nil )nil space_3D nil )"(total_order?[real])" nil )"real" reals nil )"posreal" sq "reals/" )"posreal" nil )"Vector" vectors_3D "vectors/" )"Vect2" vect_3D_2D "vectors/" )"real" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )"real" reals nil )"real" reals nil ))nil ))nil 3471185533 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil vectors_3D_def "vectors/" )"bool" reals nil )nil real_types nil )"posreal" space_3D nil )nil vectors_2D "vectors/" )nil real_types nil )nil vectors_2D_def "vectors/" )"posreal" space_3D nil )nil space_3D nil )"(total_order?[real])" nil )"real" reals nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"Vector" vectors_3D "vectors/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"Vect2" vect_3D_2D "vectors/" )"real" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )"real" reals nil )"real" reals nil ))nil ))nil 3471198643 ("" (judgement-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil vectors_2D "vectors/" )nil real_types nil )nil vectors_3D_def "vectors/" )nil vectors_2D_def "vectors/" )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" space_3D nil )nil space_3D nil )"(total_order?[real])" nil )"real" reals nil )"posreal" sq "reals/" )"posreal" nil )"Vect2" vect_3D_2D "vectors/" )"real" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )"real" reals nil ))nil ))nil 3432553796 ("" (skosimp :preds? t) nil nil )nil space_3D nil )"posreal" space_3D nil )nil real_types nil )"nonneg_real" sq "reals/" )nil real_types nil )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )nil vectors_3D_def "vectors/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )"bool" reals nil )nil vectors_2D "vectors/" )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3466172996 ("" (judgement-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil vectors_3D_def "vectors/" )"bool" reals nil )nil real_types nil )"posreal" space_3D nil )nil vectors_2D "vectors/" )nil real_types nil )"nnreal" vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )"nonneg_real" sq "reals/" )"posreal" space_3D nil )nil space_3D nil )"(strict_total_order?[real])" real_props nil )"{j: nonneg_int | j >= i}" nil )"(total_order?[real])" nil )"real" vectors_2D "vectors/" )"posreal" nil )"Vector" vectors_3D "vectors/" ))nil ))nil 3470498979"" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"Vect2" vect_3D_2D "vectors/" )"real" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )"Vector" vectors_3D "vectors/" )"real" reals nil )"posreal" nil )"real" reals nil ))nil ))"" 3504835285"" (skeep)"" (expand "verticalCoordinationConflict" )"" (rewrite "vz_neg" )"" (rewrite "vect2_neg" )"" (rewrite "vect2_neg" )"" (rewrite "sqv_neg" )"" (rewrite "sqv_neg" )"" (rewrite "neg_dot_neg" )"" (rewrite "vz_neg" )"" (rewrite "sqv_eq_0" :dir rl)"" (rewrite "sqv_eq_0" :dir rl)"" case "v`z = 0 OR OR OR eq (v`z,") "1" (assert )"1" (replace -1)"1" case "sqv(s) = 0" )"1" assert )"1" "1" "break_symmetry_neg" )"1" "v" )"1" "vectors_3D.sqv_eq_0" )"1" "s" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1)"2" "2" case "s /= zero" )"1" "1" "1" "1" "break_symmetry_neg" )"1" "s" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" (assert ) nil nil )"2" replace -1)"2" assert )nil nil ))nil )"3" (propax) nil nil )"4" "eq_neg" )"4" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (assert )"2" case "gt(v`z, ") "1" replace -1)"1" "1" "1" "1" case "s /= zero" )"1" "1" "vectors_3D.sqv_eq_0" )"1" "s" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" replace -1)"2" assert )"2" "break_symmetry_neg" )"2" "v" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" "1" "1" expand "zero" )"1" nil nil ))nil ))nil )"2" "eq_neg" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "eq_correct_1" )"2" rewrite "eq_correct_1" )"2" rewrite "gt_correct_1" )"2" rewrite "gt_correct_1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1)"2" case "s = zero" )"1" replace -1)"1" assert )"1" "break_symmetry_neg" )"1" (inst - "v" ) nil nil ))nil ))nil ))nil )"2" "2" "vectors_3D.sqv_eq_0" )"2" "s" )"2" assert )"2" "2" assert )"2" "1" "1" "1" "1" expand "zero" )"1" nil nil ))nil ))nil )"2" "eq_neg" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "1" nil nil )"2" rewrite "eq_correct_1" )"2" rewrite "gt_correct_1" )"2" rewrite "eq_correct_1" )"2" rewrite "gt_correct_1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert )"3" (flatten)"3" "3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" sq "reals/" )"nnreal" nil )"nnreal" nil )"real" reals nil )"Sign" space_3D nil )nil vect_3D_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )eq const-decl "bool" util nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )"posreal" space_3D nil )nil real_types nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"real" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )nil real_types nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"Vector" vectors_2D "vectors/" )"[T, T -> boolean]" equalities nil )nil numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"Vect3" space_3D nil )nil vectors_2D "vectors/" )nil util nil )nil vectors_3D "vectors/" )nil definitions_3D nil )"Vect3" space_3D nil )"boolean" notequal nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"nnreal" vectors_3D "vectors/" )"Sign" sign "reals/" )nil vectors_3D "vectors/" )nil vectors_2D "vectors/" )nil sq "reals/" )nil vectors_2D "vectors/" )nil vect_3D_2D "vectors/" )"Vector" vectors_2D "vectors/" )"[numfield -> numfield]" number_fields nil )nil util nil )nil util nil )"(strict_total_order?[real])" real_props nil )"bool" util nil )"real" reals nil )"odd_int" integers nil )nil vectors_3D "vectors/" )nil reals nil )nil vectors_3D "vectors/" )nil vectors_3D_def "vectors/" ))nil 3470395632"" (skeep)"" (expand "verticalCoordinationConflict" )"" (rewrite "vz_neg" )"" (rewrite "vect2_neg" )"" (rewrite "vect2_neg" )"" (rewrite "sqv_neg" )"" (rewrite "sqv_neg" )"" (rewrite "neg_dot_neg" )"" (rewrite "vz_neg" )"" (rewrite "sqv_eq_0" :dir rl)"" (rewrite "sqv_eq_0" :dir rl)"" (lift-if)"" (lift-if)"" (assert )"" "1" "1" "1" "1" "break_symmetry_neg" )"1" "v" )"1" (assert ) nil nil )"2" "vectors_3D.sqv_eq_0" )"2" "s" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "s /= zero" )"1" "1" "1" "1" "break_symmetry_neg" )"1" "s" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" (assert ) nil nil )"2" replace -1)"2" assert )nil nil ))nil )"3" (propax) nil nil )"4" "eq_neg" )"4" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" "1" "1" case "s /= zero" )"1" "1" "vectors_3D.sqv_eq_0" )"1" "s" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" replace -1)"2" assert )"2" "break_symmetry_neg" )"2" "v" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" "1" "1" expand "zero" )"1" nil nil ))nil ))nil )"2" "eq_neg" )"2" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "eq_correct_1" )"2" rewrite "eq_correct_1" )"2" rewrite "gt_correct_1" )"2" rewrite "gt_correct_1" )"2" "1" assert )nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "s = zero" )"1" replace -1)"1" assert )"1" "break_symmetry_neg" )"1" "v" )nil nil ))nil ))nil ))nil )"2" "2" "vectors_3D.sqv_eq_0" )"2" "s" )"2" assert )"2" "1" "1" "1" "1" expand "zero" )"1" nil nil ))nil ))nil )"2" "eq_neg" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "1" nil nil )"2" rewrite "eq_correct_1" )"2" rewrite "gt_correct_1" )"2" rewrite "eq_correct_1" )"2" rewrite "gt_correct_1" )"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 )"posreal" sq "reals/" )nil vect_3D_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )eq const-decl "bool" util nil )"nnreal" vectors_2D "vectors/" )"real" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil util nil )nil vectors_3D "vectors/" )nil definitions_3D nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"nnreal" vectors_3D "vectors/" )"Sign" sign "reals/" )nil vectors_3D "vectors/" )nil vectors_2D "vectors/" )nil sq "reals/" )nil vectors_2D "vectors/" )nil vect_3D_2D "vectors/" )nil util nil )nil util nil )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )nil vectors_3D_def "vectors/" ))nil ))nil 3470395677"" (inst 1 "verticalCoordinationConflict" )"" (skeep)"" (rewrite "verticalCoordinationConflict_asymm" ) nil nil ))nil ))nil )nil space_3D nil )"Sign" space_3D nil )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"[bool, bool -> bool]" booleans nil )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"boolean" notequal nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vectors_3D_def "vectors/" )nil reals nil ))nil ))nil 3550260298"" (skeep)"" (rewrite "verticalCoordinationConflict_asymm" ) nil nil )) nil )nil space_3D nil )nil reals nil )nil vectors_3D_def "vectors/" ))nil )nil 3550260273"" (judgement-tcc) nil nil ) nil nil ))nil 3470415887"" (skosimp*)"" (lemma "Delta_gt_0_nzv" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )"posreal" space_3D nil )nil real_types nil )"bool" reals 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 )nil booleans nil )nil numbers nil )nil horizontal nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D_def "vectors/" )nil vectors_3D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_3D "vectors/" )"boolean" notequal nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" ))nil ))nil 3478621317"" (skeep)"" (skoletin 1)"" (flatten)"" (lemma "Delta_gt_0_nzv" )"" (inst?)"" (assert )"" (flatten)"" (expand "verticalCoordinationConflict" )"" (case-replace "v`z = 0" )"1" (assert )"1" (replaces -2)"1" (hide-all-but (2 3))"1" (grind) nil nil )) nil ))nil ))nil )"2" (assert )"2" (lemma "Delta_discr2b" )"2" (inst?)"2" (rewrite "sqv_eq_0" :dir rl)"2" (skoletin* -1)"2" replace -4 :dir rl)"2" replace -3 :dir rl)"2" "dd" "sq(b) + sq(D) * a - sqv(vect2(nzs)) * a" nil )"2" "discr2b(a,b,c)=dd" )"1" case "dd > 0" )"1" assert )"1" rewrite "eq_correct_1" )"1" rewrite "gt_correct_1" )"1" "1" expand "Theta_D" )"1" replace "1" replace "1" replace "1" expand "root2b" )"1" assert )"1" case "nzs`z + (-b - sqrt(dd)) / a * v`z > 0" )"1" expand "sign" )"1" assert )"1" "1" "1" "1" assert )nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" expand "sign" )"2" assert )"2" "1" nil nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" "2" expand "discr2b" )"2" assert )"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 )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )nil vectors_3D_def "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"real" reals nil )"odd_int" integers nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" space_3D nil )"real" horizontal nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"[bool, bool -> bool]" booleans nil )"real" reals nil )"(total_order?[real])" nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_2D "vectors/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"real" horizontal nil )"[bool, bool -> bool]" booleans nil )"Sign" space_3D nil )"Sign" sign "reals/" )nil horizontal nil )"(strict_total_order?[real])" real_props nil )"Vertical_Strategy" space_3D nil )"posreal" sq "reals/" )"nnreal" nil )"nnreal" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"real" vectors_2D "vectors/" )nil reals nil )"real" quadratic_2b "reals/" )nil util nil )"real" reals nil )"real" reals nil )"real" quadratic_2b "reals/" )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )nil extra_real_props nil )nil reals nil )nil real_props nil )nil util nil )nil vectors_2D "vectors/" )nil horizontal nil )"Sign" definitions_3D nil ))nil )nil 3470416043"" (skeep)"" (skoletin 1)"" (flatten)"" (lemma "Delta_gt_0_nzv" )"" (inst?)"" (assert )"" (flatten)"" (expand "verticalCoordinationConflict" )"" (case-replace "v`z = 0" )"1" (assert )"1" (replaces -2)"1" (hide-all-but (2 3))"1" (grind) nil nil )) nil ))nil ))nil )"2" (assert )"2" (lemma "Delta_discr2b" )"2" (inst?)"2" (rewrite "sqv_eq_0" :dir rl)"2" (skoletin* -1)"1" replace -4 :dir rl)"1" replace -3 :dir rl)"1" "dd" "sq(b) + sq(D) * a - sqv(vect2(nzs)) * a" nil )"1" "discr2b(a,b,c)=dd" )"1" case "dd > 0" )"1" assert )"1" rewrite "eq_correct_1" )"1" rewrite "gt_correct_1" )"1" "1" expand "Theta_D" )"1" replace "1" replace "1" replace "1" expand "root2b" )"1" replace "1" assert )"1" case "nzs`z + (-b - sqrt(dd)) / a * v`z > 0" )"1" expand "sign" )"1" assert )"1" "1" "1" "1" assert )nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" expand "sign" )"2" assert )"2" "1" nil nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" "2" expand "discr2b" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"Sign" definitions_3D nil )nil horizontal nil )nil vectors_2D "vectors/" )nil util nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"real" quadratic_2b "reals/" )nil util nil )"nnreal" vectors_2D "vectors/" )"real" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )"real" quadratic_2b "reals/" )"posreal" sq "reals/" )nil horizontal nil )"Sign" sign "reals/" )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"real" horizontal nil )nil sign "reals/" )"real" horizontal nil )nil vectors_3D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" ))nil 3478949740 ("" (subtype-tcc) nil nil )"Vect2" vect_3D_2D "vectors/" )"real" vectors_2D "vectors/" )"real" reals nil ))nil ))nil 3478949740"" (skeep)"" (expand "vs_los_strategy" 1 1)"" (label "svnz" -1)"" (lift-if)"" (split +)"1" (flatten)"1" case "1*(vect2(s)*vect2(v)) >= 0 OR vect2(v) = zero" )"1" (label "entryorzero" -1)"1" (split +)"1" (flatten)"1" (rewrite "vz_neg" )"1" (expand "vs_los_strategy" )"1" (assert )"1" (replace -1)"1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (case "s`z = 0" )"1" (label "szzero" -1)"1" (split +)"1" (flatten)"1" rewrite "vz_neg" )"1" expand "vs_los_strategy" )"1" replace -3)"1" "1" assert )"1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" case "v`z = 0" )"1" "1" "1" expand "vs_los_strategy" )"1" "1" assert )"1" replace "entryorzero" )"1" case "s /= zero" )"1" assert )"1" "break_symmetry_neg" )"1" "s" )nil nil ))nil ))nil )"2" "2" "2" expand "zero" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "s = zero" )"1" assert )"1" case "-v /= zero" )"1" assert )"1" expand "vs_los_strategy" )"1" "1" replace "entryorzero" )"1" "break_symmetry_neg" )"1" "v" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "svnz" 1 -3))"2" "2" expand "zero" )"2" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "zero" )"2" "1" (grind) nil nil )"2" (grind) nil nil )"3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "vz_neg" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "vz_neg" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (flatten)"2" (split -)"1" (grind) nil nil )"2" (expand "zero" ) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" case "NOT (1*(vect2(s)*vect2(v)) >= 0 OR vect2(v) = zero)" )"1" (flatten)"1" "tca" "horizontal_tca(vect2(-s),vect2(-v))" )"1" (label "tcaname" -1)"1" (case "tca > 0" )"1" (case "tca = horizontal_tca(s,v)" )"1" (label "tcaeq" -1)"1" (replace "tcaname" )"1" case "(-s+tca*-v)`z = - (s + tca*v)`z" )"1" "1" "1" replace -1)"1" expand "vs_los_strategy" )"1" "1" assert )"1" replace "tcaeq" :dir rl)"1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" rewrite "vz_neg" )"1" expand "vs_los_strategy" )"1" "1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "vz_neg" )"2" "1" "1" expand "vs_los_strategy" )"1" "1" assert )"1" case "s /= zero" )"1" assert )"1" "break_symmetry_neg" )"1" "s" )nil nil ))nil ))nil )"2" "2" "2" expand "zero" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" case "v /= zero" )"1" expand "vs_los_strategy" )"1" "1" assert )"1" case "s = zero" )"1" assert )"1" "break_symmetry_neg" )"1" "v" )nil nil ))nil ))nil )"2" "2" expand "zero" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "zero" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "v = zero" )"1" assert )"1" "svnz" ))"1" "1" expand "zero" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "zero" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (replace "tcaname" :dir rl)"2" (expand "horizontal_tca" )"2" "2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil ))nil )"2" (replace "tcaname" :dir rl)"2" (expand "horizontal_tca" )"2" (case "sqv(vect2(-v)) > 0" )"1" "1" (assert ) nil nil ))nil )"2" "vectors_2D.sqv_eq_0" )"2" "-v" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (hide-all-but (-1 1 2))"2" (split -)"1" (grind) nil nil )"2" (hide 1)"2" (expand "zero" ) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"Sign" space_3D nil )"even_int" integers nil )"nnreal" nil )"Vect3" space_3D nil )nil real_types nil )nil real_types nil )nil extra_real_props nil )nil vectors_2D "vectors/" )"(strict_total_order?[real])" real_props nil )"[numfield -> numfield]" number_fields nil )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil real_props nil )nil real_props nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil reals nil )nil real_props nil )"real" reals nil )"bool" reals nil )"real" definitions nil )nil vectors_2D "vectors/" )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"boolean" notequal nil )"Vector" vectors_3D "vectors/" )nil definitions_3D nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"odd_int" integers nil )"Sign" sign "reals/" )"(total_order?[real])" nil )"Sign" sign "reals/" )"real" reals nil )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )"real" reals nil )nil booleans nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_2D "vectors/" )"real" vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )nil vectors_2D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )"[T, T -> boolean]" equalities nil )"Vector" vectors_2D "vectors/" ))nil )nil 3478949740"" (judgement-tcc) nil nil ) nil nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.170 Sekunden
(vorverarbeitet am 2026-04-28)
¤ *© Formatika GbR, Deutschland
2026-05-26
