Quelle vs_circle.prf
Sprache: Lisp
(vs_circlenil 3451136094"" (skeep) (("" (expand "vs_only?" ) (("" (assert ) nil nil )) nil ))nil )"bool" definitions_3D nil )"(total_order?[real])" nil )"Nz_vect2" definitions_3D nil )nil vect_3D_2D "vectors/" ))nil )nil 3451065822"" (skosimp :preds? t)"" (assert )"" (lemma "horizontal_conflict" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posreal" sq "reals/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil horizontal nil )nil vectors_2D_def "vectors/" )"bool" horizontal nil )nil vectors_3D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_3D "vectors/" )nil sign "reals/" ))nil ))nil 3451136002"" (skeep)"" (assert )"" (flatten)"" (lemma "Delta_gt_0_nzv" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"posreal" vs_circle 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 )nil vectors_2D_def "vectors/" )nil vectors_3D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" ))nil )nil 3451065822"" (skosimp :preds? t) (("" (assert ) nil nil )) nil )nil vectors_2D_def "vectors/" )"bool" horizontal nil )nil vectors_3D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_3D "vectors/" )nil sign "reals/" ))nil ))nil 3466271730"" (skeep)"" (skeep 2)"" (expand "vs_only?" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil vect_3D_2D "vectors/" )"Nz_vect2" definitions_3D nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"bool" definitions_3D nil ))nil )nil 3466260271"" (skeep)"" (lemma "Theta_D_exit_gt_0" )"" (inst?) (("" (ground) nil nil )) nil )) nil ))nil )nil horizontal nil )"posreal" sq "reals/" )nil vectors_2D_def "vectors/" )nil vectors_3D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_3D "vectors/" ))nil ))nil 3466260271"" (skosimp*) (("" (assert ) nil nil )) nil )"(strict_total_order?[real])" real_props nil )nil vect_3D_2D "vectors/" ))nil ))nil 3466260271"" (skosimp*) (("" (assert ) nil nil )) nil )"(strict_total_order?[real])" real_props nil )nil vect_3D_2D "vectors/" ))nil ))nil 3471192910"" (skeep)"" (expand "vs_circle?" )"" (flatten)"" (expand "vs_circle" )"" (lift-if)"" (split -)"1" (flatten)"1" (expand "vertical_criterion?" )"1" (flatten)"1" (hide 3)"1" (assert )"1" (rewrite "vect2_sub" )"1" (rewrite "vz_distr_sub" )"1" (replace -1)"1" expand "horizontal_conflict?" )"1" "1" replace -3)"1" assert )"1" "sp" )"1" assert )"1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "vertical_criterion?" )"2" (flatten)"2" (split -1)"1" (flatten)"1" (split -)"1" (flatten)"1" (assert )"1" "Delta_gt_0_nzv" )"1" "1" assert )"1" "1" "1" "1" "vso" "vs_only(sp, vect2(vo - vi), Theta_D(vect2(sp), vect2(vo - vi), 1), " nil )"1" "vsoname" -1)"1" "ddir" "IF abs(sp`z) >= H THEN eps * sign(sp`z) ") "1" "ddirname" -1)"1" case "ddir = 1 or ddir = -1" )"1" "ddirtp" "1" replace "ddirname" )"1" "1" "1" expand "closed_region_3D" )"1" assert )"1" rewrite "vect2_sub" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_add" )"1" rewrite "vect2_scal" )"1" rewrite "vz_distr_sub" )"1" case "eps*(eps*H) = H" )"1" assert )"1" "thetad" "Theta_D(vect2(sp), vect2(vo) - vect2(vi), ddir)" )"1" replace "1" "thetadname" "1" "ppoint" "vect2(sp) + thetad * vect2(vo - vi)" )"1" "ppointname" "1" replace "1" case "sqv(ppoint) = sq(D)" )"1" assert )"1" case "NOT (vect2(vo) - vect2(vi)) * ppoint = 0" )"1" assert )"1" "Theta_D_line_intersection" )"1" "ddir" "sp" "vect2(vo)-vect2(vi)" )"1" assert )"1" replace "thetadname" )"1" rewrite "vect2_sub" )"1" replace "ppointname" )"1" assert )"1" replace "1" "Theta_D_positive_conflict" )"1" "sp" "vect2(vo)-vect2(vi)" )"1" assert )"1" "td1pos" "1" case "sign((vect2(vo) - vect2(vi)) * ppoint) = ddir" )"1" assert )"1" expand "vs_only" )"1" "1" "vsoname" )"1" "1" replace "1" assert )"1" "1" "ddirtp" )"1" replace "1" assert )"1" "1" "ddirname" )"1" "1" assert )"1" "vs_at_H" )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "ddirname" )"1" "1" assert )"1" "Theta_D_entry_gt_0" )"1" "vect2(vo)-vect2(vi)" "sp" )"1" assert )"1" "vs_at_H" )"1" "eps" "thetad" "sp`z" )"1" "eps" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "Theta_D_entry_gt_0" )"2" "vect2(vo)-vect2(vi)" "sp" )"2" assert )"2" "vs_at_H" )"2" "eps" "thetad" "sp`z" )"2" "eps" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" replace "1" assert )"1" "1" "eps*sp`z = abs(sp`z)" )"1" assert )"1" case "ddir = 1" )"1" replace "1" assert )"1" "1" "vs_at_H" )"1" "1" "eps" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ddirtp" "ddirname" "2" nil nil ))nil ))nil ))nil )"2" "2" "eps" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "Theta_D_horizontal_dir" )"2" "ddir" "sp" "vect2(vo)-vect2(vi)" )"2" assert )"2" replace "thetadname" )"2" replace "ppointname" )"2" "ddirtp" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "on_D_line" )"2" "ppoint" "vo-vi" )"2" assert )"2" rewrite "vect2_sub" )"2" "vectors_2D.dot_comm" )"2" "2" assert )"2" "2" "line_solution_Delta" )"2" "ppoint" "vect2(vo)-vect2(vi)" )"2" "2" "2" "1" "1" replace "ppointname" "1" "Delta_eq" )"1" "sp" "thetad" "vect2(vo)-vect2(vi)" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "eps!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "Theta_D_on_D" )"2" "2" assert )"2" rewrite "vect2_sub" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "ddirtp" )"1" replace "1" assert )nil nil ))nil )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "eps" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "ddirtp" )"1" replace "1" assert )nil nil ))nil )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ddirname" 1))"2" "eps" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (replace -1) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (replace -1) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" vs_circle nil )"{nvo | vect2(nvo) /= zero IMPLIES vs_only?(vo)(nvo)}" vs_circlenil )"(divides(m))" divides nil )"(divides(n))" divides nil )"Sign" sign "reals/" )"odd_int" integers nil )"SignedCrit" vertical_criterionnil )nil vect_3D_2D "vectors/" )nil reals nil )nil vectors_3D_def "vectors/" )nil vectors_2D "vectors/" )nil booleans nil )"boolean" notequal nil )nil vectors_2D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil definitions_3D nil )"Nz_vect2" definitions_3D nil )"real" reals nil )"posreal" sq "reals/" )"(strict_total_order?[real])" real_props nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vect_3D_2D "vectors/" )"real" reals nil )"real" vectors_2D "vectors/" )"Sign" sign "reals/" )"Vector" vectors_2D "vectors/" )"real" reals nil )"posreal" nil )nil space_3D nil )"posreal" vs_circle nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )"posreal" vs_circle nil )nil real_types nil )"bool" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )"bool" horizontal nil )"real" reals nil )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"Vector" vectors_3D "vectors/" )"odd_int" integers nil )"real" reals nil )"bool" vertical_criterion nil )"Vector" vectors_3D "vectors/" )nil vect_3D_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil horizontal nil )nil horizontal nil )nil horizontal nil )nil line_solutions nil )nil vectors_2D "vectors/" )nil line_solutions nil )nil horizontal nil )"nzint" integersnil )nil vertical nil )nil horizontal nil )nil reals nil )"real" vertical nil )nil extra_real_props nil )nil horizontal nil )nil horizontal nil )nil horizontal nil )nil vect_3D_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )"nzreal" nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" horizontal nil )"real" horizontal nil )nil vectors_2D "vectors/" )"[bool, real]" vs_only nil )nil sign "reals/" )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T, T -> boolean]" equalities nil )nil horizontal nil )nil vect_3D_2D "vectors/" ))nil ))nil 3471104915"" (skeep)"" (label "vso" -2)"" (label "epsge" -3)"" (expand "vertical_criterion?" )"" "ddir" "IF abs(s`z) >= H THEN eps * sign(s`z) ") "" (replace -1)"" (label "ddirname" -1)"" (flatten)"" (split -2)"1" (hide 2)"1" (flatten)"1" (assert )"1" (rewrite "vz_distr_sub" )"1" (rewrite "vz_distr_sub" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 1)"2" (flatten)"2" (assert )"2" (expand "closed_region_3D" )"2" (assert )"2" "2" assert )"2" expand "vs_only?" )"2" rewrite "vect2_sub" )"2" rewrite "vect2_sub" )"2" assert )"2" "1" rewrite "vect2_add" )"1" rewrite "vect2_scal" )"1" "ppoint" "vect2(s) + Theta_D(vect2(s), vect2(v), ddir) * vect2(v)" )"1" replace -1)"1" replace "vso" "1" "tt" "(sq(D) - vect2(s) * ppoint) / ((vect2(nvo1) - vect2(vi)) * ppoint)" )"1" replace -1)"1" case "(nvo2 - vi)`z = (nvo2`z - nvo1`z) + (nvo1 - vi)`z" )"1" replace "1" "epsge" )"1" "tt" )"1" assert )nil nil ))nil ))nil ))nil )"2" rewrite "vz_distr_sub" )"2" rewrite "vz_distr_sub" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"Sign" sign "reals/" )"odd_int" integers nil )"SignedCrit" vertical_criterionnil )"nzreal" nil )"(strict_total_order?[real])" real_props nil )nil vect_3D_2D "vectors/" )"real" reals nil )nil vect_3D_2D "vectors/" )"Nz_vect2" definitions_3D nil )"real" horizontal nil )"real" horizontal nil )"posreal" vs_circle nil )nil vectors_2D "vectors/" )"Vector" vectors_3D "vectors/" )nil vect_3D_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil extra_real_propsnil )"real" vs_circle nil )"[numfield, numfield -> numfield]" number_fields nil )"Vector" vectors_3D "vectors/" )"Vector" vectors_2D "vectors/" )"real" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil vect_3D_2D "vectors/" )"bool" definitions_3D nil )"bool" vertical_criterion nil )"real" reals nil )"posreal" sq "reals/" )"real" reals nil )"(total_order?[real])" nil )"real" reals nil )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil definitions_3D 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 )nil number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil booleans nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans 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" vs_circle nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sign "reals/" )"Sign" sign "reals/" ))nil ))nil 3451908601"" (skeep)"" (lemma "vs_circle_meets_vertical_criterion" )"" (inst?)"" (assert )"" (lemma "vertical_criterion_independence" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil vs_circle nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil nil )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )nil space_3D nil )"posreal" vs_circle nil )"nonneg_real" sq "reals/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D "vectors/" )"posreal" vs_circle nil )nil real_types nil )"bool" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil vectors_3D_def "vectors/" )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 )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3470079373"" (skeep)"" (lemma "vs_circle_meets_vertical_criterion" )"" (inst-cp -1 "eps" "nvo" "sp" "vi" "vo" )"" (inst -1 "-eps" "nvi" "-sp" "vo" "vi" )"" (assert )"" (rewrite "vect2_neg" )"" (lemma "horizontal_conflict_symm" )"" (inst? -1)"" (assert )"" (replaces -1 :dir rl)"" "-vect2(vi-vo) = vect2(vo-vi)" )"1" (hide -1)"1" case "horizontal_conflict?(vect2(sp), vect2(vo - vi))" )"1" (assert )"1" expand "vs_circle?" )"1" "1" "vs_circle(sp, vo, vi, eps)" )"1" assert )"1" "vs_circle(-sp, vi, vo, -eps)" )"1" assert )"1" "1" "vertical_criterion_coordination" )"1" "eps" "nvi" "nvo" "sp" "vi" "vo" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "conflict?" )"2" expand "horizontal_conflict?" )"2" "2" (inst + "nnt!1" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil vs_circle nil )"Sp_vect3[D, H]" vs_circle nil )"Nz_vector" vectors_3D "vectors/" )"Sign" sign "reals/" )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )nil vect_3D_2D "vectors/" )"Vector" vectors_3D "vectors/" )"Vector" vectors_2D "vectors/" )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )"bool" space_3D nil )nil nil )"{nvo | vect2(nvo) /= zero IMPLIES vs_only?(vo)(nvo)}" vs_circlenil )"bool" definitions_3D nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" vs_circle nil )"bool" horizontal nil )nil vectors_2D "vectors/" )nil horizontal nil )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )nil space_3D nil )"posreal" vs_circle nil )"nonneg_real" sq "reals/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D "vectors/" )"posreal" vs_circle nil )nil real_types nil )"bool" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil vectors_3D_def "vectors/" )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 )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil )nil 3451923945"" (skeep)"" (lemma "vs_circle_satisfies_vertical_criterion" )"" (inst -1 "eps" "nvo" "sp" "vi" "vo" )"" (lemma "vertical_horizontal_conflict" )"" (inst?)"" (assert )"" (flatten)"" (assert )"" (hide -5)"" "vs_circle_satisfies_vertical_criterion" )"" (inst -1 "-eps" "nvi" "-sp" "vo" "vi" )"" (assert )"" (rewrite "vect2_neg" )"" (split -1)"1" "1" (postpone) nil nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil vectors_2D_def "vectors/" )nil vectors_3D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_3D "vectors/" )nil vectors_2D "vectors/" )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )nil space_3D nil )nil vect_3D_2D "vectors/" )nil vect_3D_2D "vectors/" )"Nz_vector" vectors_3D "vectors/" )"Sign" sign "reals/" )nil vectors_3D "vectors/" )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vect_3D_2D "vectors/" )nil vectors_2D "vectors/" )nil sign "reals/" )nil horizontal nil )"real" horizontal nil )"real" horizontal nil )nil vect_3D_2D "vectors/" )nil definitions_3D nil )nil horizontal nil )nil horizontal nil )nil definitions_3D nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.59 Sekunden
(vorverarbeitet am 2026-04-26)
¤ *© Formatika GbR, Deutschland
2026-05-26
