Quellcode-Bibliothek intersections_2D.prf
Sprache: Lisp
(intersections_2Dnil 3430227348"" (skosimp*)"" (assert )"" (flatten)"" (split +)"1" (expand "det" )"1" (assert ) (("1" (grind) nil nil )) nil )) nil )"2" (expand "det" )"2" (assert )"2" (grind)"2" (move-terms -1 r 1)"2" (mult-by -1 "L0!1`v`y" )"2" (replace -1 * rl)"2" (hide -1)"2" (assert )"2" (move-terms -1 r 1)"2" (mult-by -1 "L0!1`v`x" )"2" replace -1 * rl)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil )"real" det_2D nil )nil booleans nil )nil booleans nil )"[bool, bool -> bool]" booleans nil )nil numbers nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_2D_def nil )nil vectors_2D nil )nil lines_2D nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil extra_real_props nil ))nil ))nil 3267433756 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"boolean" notequal nil )nil reals nil )nil vectors_2D_def nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil vectors_2D nil )nil lines_2D nil )"real" reals nil )"Vector" vectors_2D nil )"real" det_2D nil )"real" reals nil ))nil 3267891274"" (skosimp*)"" (expand "same_line?" )"" (flatten)"" (rewrite "cross_asym" +)"" (assert )"" (expand "cross" )"" (grind)"" (mult-by -2 "L1!1`v`y" )"" (assert )"" (mult-by 1 "L0!1`v`y" )"1" (assert ) nil nil )"2" (replace -1)"2" (assert )"2" (assert )"2" (mult-cases -3)"1" replace -1)"1" assert )"1" case "L1!1`v`y = 0" )"1" "1" replace -1)"1" assert )"1" "L0!1`v" )"1" "1" "norm_xy_eq_0" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "L0!1`v" )"2" "2" "norm_xy_eq_0" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" assert )"2" "2" "2" assert )"2" replace -2)"2" replace -3)"2" assert )"2" "2" "2" "2" "L0!1`v" )"2" "2" "norm_xy_eq_0" )"2" "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 )"bool" intersections_2D nil )nil extra_real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil lines_2D nil )nil vectors_2D nil )nil vectors_2D_def nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )"boolean" notequal nil )nil reals nil )"Line2D" intersections_2D nil )"[T, T -> boolean]" equalities nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil real_props nil )"posreal" vectors_2D nil )nil vectors_2D nil )"Vector" vectors_2D nil )nil vectors_2D nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"real" det_2D nil )"Vector" vectors_2D nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil 3267453794"" (skosimp*)"" (expand "intersect?" )"" (expand "parallel?" )"" (flatten) (("" (skosimp*) (("" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" intersections_2D nil )"Nz_vector" vectors_2D nil )"real" reals nil )"real" reals nil )"real" det_2D nil )"Vector" vectors_2D nil )"bool" vectors_2D nil ))nil 3430226638"" (skosimp*)"" (skoletin* 2)"" (replace -1)"" (replace -2)"" (hide -1 -2)"" (apply-extensionality 1 :hide? t)"1" (expand "*" )"1" (expand "+" )"1" (field 1)"1" (replace -1)"1" (expand "det" )"1" (assert )"1" (expand "-" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "*" )"2" (expand "+" )"2" (field 1)"2" (replace -1)"2" (expand "-" )"2" (expand "det" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )nil booleans nil )nil booleans nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )nil vectors_2D nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"Vector" vectors_2D nil )nil vectors_2D_def nil )nil vectors_2D nil )nil lines_2D nil )nil numbers nil )"boolean" notequal nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"real" det_2D nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[bool, bool -> bool]" booleans nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"real" reals nil ))nil )nil 3267438142"" (skosimp*)"" (skoletin 2)"" (skoletin 1)"" (skoletin 1)"" (replace -1)"" (replace -2)"" (hide -1 -2)"" (apply-extensionality 1 :hide? t)"1" (expand "*" )"1" (expand "+" )"1" (field 1)"1" (replace -2)"1" (expand "cross" )"1" (assert )"1" expand "-" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "*" )"2" (expand "+" )"2" (field 1)"2" (replace -2)"2" (expand "-" )"2" (expand "cross" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil lines_2D nil )nil vectors_2D nil )nil vectors_2D_def nil )nil vectors_2D nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil ))nil 3543442415 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil vectors_2D nil )"Vector" vectors_2D nil )nil vectors_2D nil )nil numbers nil )nil vectors_2D_def nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"real" reals nil )"Vector" vectors_2D nil )"real" det_2D nil )"boolean" notequal nil )"real" reals nil ))nil ))nil 3543444841"" (skeep :preds? t)"" (lemma "intersection_lem" )"" (inst -1 "(so,vo)" "(si,vi)" )"" (assert )"" (expand "lines_intersection" ) (("" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )nil intersections_2D nil )"real" reals nil )"[real, real]" intersections_2D nil )"real" det_2D nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"Vector" vectors_2D nil )"boolean" notequal nil )nil booleans nil )nil vectors_2D nil )nil reals nil )nil lines_2D nil )nil vectors_2D nil )nil vectors_2D_def nil ))nil ))nil 3430227167"" (skosimp*)"" (expand "on_line?" )"" (skosimp*)"" (expand "intersect?" )"" (flatten)"" (replace -1)"" (hide -1)"" (name "DELTA" "L1!1`p - L0!1`p" )"" (case "x!1 * v(L0!1) - x!2 * v(L1!1) = DELTA" )"1" (hide -3)"1" (expand "same_line?" )"1" (assert )"1" case "det(L0!1`v,L1!1`v)*x!2 = det(DELTA,L0!1`v) " )"1" case "det(L0!1`v,L1!1`v)*x!1 = det(DELTA,L1!1`v) " )"1" replace -5)"1" (assert ) nil nil ))nil )"2" "2" replace -1 * rl)"2" "2" expand "det" )"2" assert )"2" expand "-" )"2" expand "*" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" replace -1 * rl)"2" "2" expand "det" )"2" expand "-" )"2" expand "*" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (replace -1 * rl)"2" (lemma "add_move_right" )"2" (hide -2)"2" (inst?)"2" assert )"2" replace -1)"2" "2" "1" expand "-" )"1" expand "*" )"1" expand "+" )"1" (propax) nil nil ))nil ))nil ))nil )"2" expand "-" )"2" expand "+ " )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" lines_2D nil )"bool" intersections_2D nil )nil lines_2D nil )nil vectors_2D nil )nil vectors_2D_def nil )"Vector" vectors_2D nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil vectors_2D nil )nil reals nil )nil vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil )"real" reals nil )"real" det_2D nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" reals nil )"bool" intersections_2D nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"Vector" vectors_2D nil ))nil )nil 3269337859"" (skosimp*)"" (expand "on_line?" )"" (skosimp*)"" (expand "intersect?" )"" (flatten)"" (replace -1)"" (hide -1)"" (name "DELTA" "L1!1`p - L0!1`p" )"" (case "x!1 * v(L0!1) - x!2 * v(L1!1) = DELTA" )"1" (hide -3)"1" (expand "same_line?" )"1" (assert )"1" case "cross(L0!1`v,L1!1`v)*x!2 = cross(DELTA,L0!1`v) " )"1" case "cross(L0!1`v,L1!1`v)*x!1 = cross(DELTA,L1!1`v) " )"1" replace -5)"1" (assert ) nil nil ))nil )"2" "2" replace -1 * rl)"2" "2" expand "cross" )"2" assert )"2" expand "-" )"2" expand "*" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" replace -1 * rl)"2" "2" expand "cross" )"2" expand "-" )"2" expand "*" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (replace -1 * rl)"2" (lemma "add_move_right" )"2" (hide -2)"2" (inst?)"2" assert )"2" replace -1)"2" "2" "1" expand "-" )"1" expand "*" )"1" expand "+" )"1" (propax) nil nil ))nil ))nil ))nil )"2" expand "-" )"2" expand "+ " )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" lines_2D nil )nil lines_2D nil )nil vectors_2D nil )nil vectors_2D_def nil )nil vectors_2D nil )nil vectors_2D nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil )nil 3269337834"" (skosimp*)"" (expand "on_line?" )"" (skosimp*)"" (expand "intersect?" )"" (flatten)"" (replace -1)"" (hide -1)"" (name "DELTA" "L1!1`p - L0!1`p" )"" (case "x!1 * v(L0!1) - x!2 * v(L1!1) = DELTA" )"1" (hide -3)"1" (expand "same_line?" )"1" (assert )"1" case "cross(L0!1`v,L1!1`v)*x!2 = cross(DELTA,L0!1`v) " )"1" case "cross(L0!1`v,L1!1`v)*x!1 = cross(DELTA,L1!1`v) " )"1" (replace -5) (("1" (assert ) nil )))"2" "2" replace -1 * rl)"2" "2" expand "cross" )"2" assert )"2" expand "-" )"2" expand "*" )"2" assert )nil )))))))))))))))))"2" (hide 2)"2" replace -1 * rl)"2" "2" expand "cross" )"2" expand "-" )"2" expand "*" )"2" assert )nil )))))))))))))))))))))"2" (assert )"2" (replace -1 * rl)"2" (lemma "add_move_left" )"2" (hide -2)"2" "p(L1!1)" "x!2 * v(L1!1)" "p(L0!1) + x!1 * v(L0!1)" )"2" assert )"2" "2" "1" expand "-" )"1" expand "*" )"1" expand "+" )"1" "comp_eq_x" )"1" "1" assert )nil )))))))))))"2" expand "-" )"2" expand "+ " )"2" expand "*" )"2" "comp_eq_y" )"2" "2" assert )nil ))))))))))))))))))))))))))))))))))))))))))))nil )nil nil )nil 3269337779"" (skosimp*)"" (expand "on_line?" )"" (skosimp*)"" (expand "intersect?" )"" (flatten)"" (replace -1)"" (hide -1)"" (name "DELTA" "L1!1`p - L0!1`p" )"" (case "x!1 * v(L0!1) - x!2 * v(L1!1) = DELTA" )"1" (hide -3)"1" (expand "same_line?" )"1" (assert )"1" case "cross(L0!1`v,L1!1`v)*x!2 = cross(DELTA,L0!1`v) " )"1" case "cross(L0!1`v,L1!1`v)*x!1 = cross(DELTA,L1!1`v) " )"1" (replace -5) (("1" (assert ) nil )))"2" "2" replace -1 * rl)"2" "2" expand "cross" )"2" assert )"2" expand "-" )"2" expand "*" )"2" assert )nil )))))))))))))))))"2" (hide 2)"2" replace -1 * rl)"2" "2" expand "cross" )"2" expand "-" )"2" expand "*" )"2" assert )nil )))))))))))))))))))))"2" (assert )"2" (replace -1 * rl)"2" (lemma "add_move_right" )"2" (hide -2)"2" "p(L1!1)" "x!2 * v(L1!1)" "p(L0!1) + x!1 * v(L0!1)" )"2" assert )"2" "2" "1" expand "-" )"1" expand "*" )"1" expand "+" )"1" "comp_eq_x" )"1" "1" assert )nil )))))))))))"2" expand "-" )"2" expand "+ " )"2" expand "*" )"2" "comp_eq_y" )"2" "2" assert )nil ))))))))))))))))))))))))))))))))))))))))))))nil )nil nil )nil 3269337644"" (skosimp*)"" (expand "on_line?" )"" (skosimp*)"" (expand "intersect?" )"" (flatten)"" (replace -1)"" (hide -1)"" (name "DELTA" "L1!1`p - L0!1`p" )"" (case "x!1 * v(L0!1) - x!2 * v(L1!1) = DELTA" )"1" (hide -3)"1" (expand "same_line?" )"1" (assert )"1" case "cross(L0!1`v,L1!1`v)*x!2 = cross(DELTA,L0!1`v) " )"1" case "cross(L0!1`v,L1!1`v)*x!1 = cross(DELTA,L1!1`v) " )"1" (replace -5) (("1" (assert ) nil )))"2" "2" replace -1 * rl)"2" "2" expand "cross" )"2" assert )"2" expand "-" )"2" expand "*" )"2" assert )nil )))))))))))))))))"2" (hide 2)"2" replace -1 * rl)"2" "2" expand "cross" )"2" expand "-" )"2" expand "*" )"2" assert )nil )))))))))))))))))))))"2" (assert )"2" (replace -1 * rl)"2" (lemma "add_move_right" )"2" (hide -2)"2" "p(L1!1)" "x!2 * v(L1!1)" "p(L0!1) + x!1 * v(L0!1)" )"2" assert )"2" "2" "1" expand "-" )"1" expand "*" )"1" expand "+" )"1" "comp_x_eq" )"1" "1" assert )nil )))))))))))"2" expand "-" )"2" expand "+ " )"2" expand "*" )"2" "comp_y_eq" )"2" "2" assert )nil ))))))))))))))))))))))))))))))))))))))))))))nil )nil nil )nil 3269337590"" (skosimp*)"" (expand "on_line?" )"" (skosimp*)"" (expand "intersect?" )"" (flatten)"" (replace -1)"" (hide -1)"" (name "DELTA" "L1!1`p - L0!1`p" )"" (case "x!1 * v(L0!1) - x!2 * v(L1!1) = DELTA" )"1" (hide -3)"1" (expand "same_line?" )"1" (assert )"1" case "cross(L0!1`v,L1!1`v)*x!2 = cross(DELTA,L0!1`v) " )"1" case "cross(L0!1`v,L1!1`v)*x!1 = cross(DELTA,L1!1`v) " )"1" (replace -5) (("1" (assert ) nil )))"2" "2" replace -1 * rl)"2" "2" expand "cross" )"2" assert )"2" expand "-" )"2" expand "*" )"2" assert )nil )))))))))))))))))"2" (hide 2)"2" replace -1 * rl)"2" "2" expand "cross" )"2" expand "-" )"2" expand "*" )"2" assert )nil )))))))))))))))))))))"2" (assert )"2" (replace -1 * rl)"2" (lemma "add_move_right" )"2" (hide -2)"2" "p(L1!1)" "x!2 * v(L1!1)" "p(L0!1) + x!1 * v(L0!1)" )"2" assert )"2" "2" "1" expand "-" )"1" expand "*" )"1" expand "+" )"1" "comp_eq_x" )"1" "1" assert )nil )))))))))))"2" expand "-" )"2" expand "+ " )"2" expand "*" )"2" "comp_eq_y" )"2" "2" assert )nil ))))))))))))))))))))))))))))))))))))))))))))nil )nil nil )nil 3269337494"" (skosimp*)"" (expand "on_line?" )"" (skosimp*)"" (expand "intersect?" )"" (flatten)"" (replace -1)"" (hide -1)"" (name "DELTA" "L1!1`p - L0!1`p" )"" (case "x!1 * v(L0!1) - x!2 * v(L1!1) = DELTA" )"1" (hide -3)"1" (expand "same_line?" )"1" (assert )"1" case "cross(L0!1`v,L1!1`v)*x!2 = cross(DELTA,L0!1`v) " )"1" case "cross(L0!1`v,L1!1`v)*x!1 = cross(DELTA,L1!1`v) " )"1" (replace -5) (("1" (assert ) nil )))"2" "2" replace -1 * rl)"2" "2" expand "cross" )"2" assert )"2" expand "-" )"2" expand "*" )"2" assert )nil )))))))))))))))))"2" (hide 2)"2" replace -1 * rl)"2" "2" expand "cross" )"2" expand "-" )"2" expand "*" )"2" assert )nil )))))))))))))))))))))"2" (assert )"2" (replace -1 * rl)"2" (lemma "add_cancel_left" )"2" (hide -2)"2" "p(L1!1)" "x!2 * v(L1!1)" "p(L0!1) + x!1 * v(L0!1)" )"2" assert )"2" "2" "1" expand "-" )"1" expand "*" )"1" expand "+" )"1" "comp_eq_x" )"1" "1" assert )nil )))))))))))"2" expand "-" )"2" expand "+ " )"2" expand "*" )"2" "comp_eq_y" )"2" "2" assert )nil ))))))))))))))))))))))))))))))))))))))))))))nil )nil nil )nil 3269337451"" (skosimp*)"" (expand "on_line?" )"" (skosimp*)"" (expand "intersect?" )"" (flatten)"" (replace -1)"" (hide -1)"" (name "DELTA" "L1!1`p - L0!1`p" )"" (case "x!1 * v(L0!1) - x!2 * v(L1!1) = DELTA" )"1" (hide -3)"1" (expand "same_line?" )"1" (assert )"1" case "cross(L0!1`v,L1!1`v)*x!2 = cross(DELTA,L0!1`v) " )"1" case "cross(L0!1`v,L1!1`v)*x!1 = cross(DELTA,L1!1`v) " )"1" (replace -5) (("1" (assert ) nil )))"2" "2" replace -1 * rl)"2" "2" expand "cross" )"2" assert )"2" expand "-" )"2" expand "*" )"2" assert )nil )))))))))))))))))"2" (hide 2)"2" replace -1 * rl)"2" "2" expand "cross" )"2" expand "-" )"2" expand "*" )"2" assert )nil )))))))))))))))))))))"2" (assert )"2" (replace -1 * rl)"2" (lemma "add_move_left" )"2" (hide -2)"2" "p(L1!1)" "x!2 * v(L1!1)" "p(L0!1) + x!1 * v(L0!1)" )"2" assert )"2" "2" "1" expand "-" )"1" expand "*" )"1" expand "+" )"1" "comp_eq_x" )"1" "1" assert )nil )))))))))))"2" expand "-" )"2" expand "+ " )"2" expand "*" )"2" "comp_eq_y" )"2" "2" assert )nil ))))))))))))))))))))))))))))))))))))))))))))nil )nil nil )nil 3267457715"" (skosimp*)"" (expand "on_line?" )"" (skosimp*)"" (expand "intersect?" )"" (flatten)"" (replace -1)"" (hide -1)"" (name "DELTA" "L1!1`p - L0!1`p" )"" (case "x!1 * v(L0!1) - x!2 * v(L1!1) = DELTA" )"1" (hide -3)"1" (expand "same_line?" )"1" (assert )"1" case "cross(L0!1`v,L1!1`v)*x!2 = cross(DELTA,L0!1`v) " )"1" case "cross(L0!1`v,L1!1`v)*x!1 = cross(DELTA,L1!1`v) " )"1" replace -5)"1" (assert ) nil nil ))nil )"2" "2" replace -1 * rl)"2" "2" expand "cross" )"2" assert )"2" expand "-" )"2" expand "*" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" replace -1 * rl)"2" "2" expand "cross" )"2" expand "-" )"2" expand "*" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (replace -1 * rl)"2" (lemma "move_left" )"2" (hide -2)"2" "p(L1!1)" "x!2 * v(L1!1)" "p(L0!1) + x!1 * v(L0!1)" )"2" assert )"2" "2" "1" expand "-" )"1" expand "*" )"1" expand "+ ") "1" "comp_eq_x" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "-" )"2" expand "+ " )"2" expand "*" )"2" "comp_eq_y" )"2" "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 vectors_2D nil )nil vectors_2D nil )nil vectors_2D nil )"bool" lines_2D nil )nil lines_2D nil )nil vectors_2D nil )nil vectors_2D nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil 3267450311"" (skosimp*)"" (expand "intersect?" ) (("" (assert ) nil nil )) nil )) nil )"bool" intersections_2D nil )) shostak))nil 3267438517"" (skosimp*)"" (expand "on_line?" )"" (skosimp*)"" (expand "intersect?" )"" (expand "intersect_pt" )"" (replace -2)"" (hide -2)"" (name "DELTA" "L1!1`p - L0!1`p" )"" (replace -1)"" case "x!1 = det(DELTA,L1!1`v)/det(L0!1`v,L1!1`v)" )"1" case "x!2 = det(DELTA,L0!1`v)/det(L0!1`v,L1!1`v)" )"1" (replace -2) (("1" (propax) nil nil ))nil )"2" (hide 2)"2" (lemma "intersection_lem" )"2" (inst?)"2" assert )"2" replace -3)"2" replace -2 * rl)"2" replace -1)"2" "2" "scal_cancel" )"2" "2" "2" "L1!1`v" )"2" assert )"2" "2" "add_cancel_left" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (cross-mult 1)"2" (replace -1 * rl)"2" (hide -1)"2" expand "det" )"2" expand "-" )"2" case "p(L0!1)`x + x!1 * v(L0!1)`x = p(L1!1)`x + x!2 * v(L1!1)`x" )"1" case "p(L0!1)`y + x!1 * v(L0!1)`y = p(L1!1)`y + x!2 * v(L1!1)`y" )"1" "1" "L1!1`v`x" )"1" "L1!1`v`y" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "comp_eq_y" )"2" "2" "1" expand "+ " )"1" assert )"1" expand "*" )"1" nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "comp_eq_x" )"2" "2" expand "*" )"2" expand "+ " )"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 )"bool" lines_2D nil )"bool" intersections_2D nil )nil lines_2D nil )nil vectors_2D nil )nil vectors_2D_def nil )"Vector" vectors_2D nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil vectors_2D nil )nil reals nil )"real" det_2D nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"real" reals nil )nil vectors_2D nil )nil vectors_2D nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )nil vectors_2D nil )nil intersections_2D nil )nil real_props nil )nil reals nil )"real" reals nil )nil vectors_2D nil )nil extra_real_props nil )"real" reals nil )nil vectors_2D nil )"Vector" vectors_2D nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"Vect2" intersections_2D nil ))nil 3440252936"" (skosimp*)"" (lemma "pt_intersect" )"" (inst - "L0!1" "L1!1" "p1!1" )"" (assert )"" (expand "intersect?" )"" (flatten)"" (expand "same_line?" )"" (hide 3)"" (expand "det" )"" (expand "on_line?" )"" (skosimp*)"" (replace -1)"" (hide -1)"" (replace -2)"" "" " x!1 * v(L0!1) - x!2 * v(L1!1) = p(L1!1) - p(L0!1)" )"1" "1" " x!3 * v(L0!1) - x!4 * v(L1!1) = p(L1!1) - p(L0!1)" )"1" "1" replace -1 * rl)"1" "1" assert )"1" "(x!1 - x!3)*v(L0!1) = (x!2 - x!4) * v(L1!1)" )"1" "(x!2 - x!4) = 0" )"1" assert )"1" "1" assert )"1" replace -1)"1" "1" "x!1 = x!3" )"1" "v(L0!1) = zero" )"1" assert )nil nil )"2" "2" "scal_eq_zero" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "v(L1!1) = ((x!1 - x!3)/(x!2 - x!4))* v(L0!1)" )"1" "comp_eq_x" )"1" "1" expand "*" "1" assert )"1" "1" replace "1" "1" "comp_eq_y" )"1" "1" expand "*" "1" "1" replace "1" assert )nil nil ))nil )"2" replace "2" "1" assert )"1" expand "*" )"1" nil nil ))nil ))nil )"2" expand "*" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "*" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "*" )"2" nil nil ))nil ))nil )"3" assert )nil nil ))nil ))nil )"2" "1" "1" "comp_eq_x" )"1" "x!1 * v(L0!1) - x!2 * v(L1!1)" "x!3 * v(L0!1) - x!4 * v(L1!1)" )"1" expand "-" )"1" expand "*" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "comp_eq_y" )"2" "x!1 * v(L0!1) - x!2 * v(L1!1)" "x!3 * v(L0!1) - x!4 * v(L1!1)" )"2" expand "*" )"2" expand "-" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" "comp_eq_x" )"1" "p(L0!1) + x!3 * v(L0!1)" "p(L1!1) + x!4 * v(L1!1)" )"1" expand "+ " )"1" expand "*" )"1" assert )"1" expand "-" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "comp_eq_y" )"2" "p(L0!1) + x!3 * v(L0!1)" "p(L1!1) + x!4 * v(L1!1)" )"2" expand "*" )"2" expand "-" )"2" expand "+ " )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "comp_eq_x" )"1" "1" expand "*" )"1" expand "-" )"1" expand "+ " )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "comp_eq_y" )"2" "2" expand "*" )"2" expand "-" )"2" expand "+ " )"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 intersections_2D nil )"bool" lines_2D nil )nil vectors_2D nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"Vector" vectors_2D nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"Vector" vectors_2D nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[bool, bool -> bool]" booleans nil )nil booleans nil )"real" reals nil )nil vectors_2D nil )"Vector" vectors_2D nil )nil vectors_2D nil )nil vectors_2D nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_2D nil )nil vectors_2D nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"real" reals nil )"odd_int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"Vector" vectors_2D nil )"real" det_2D nil )"real" reals nil )"bool" intersections_2D nil )"bool" intersections_2D nil )nil reals nil )nil lines_2D nil )nil vectors_2D nil )nil vectors_2D_def nil ))nil )nil 3440246298"" (skosimp*)"" (lemma "pt_intersect" )"" (inst - "L0!1" "L1!1" "p1!1" )"" (assert )"" (expand "intersect?" )"" (flatten)"" (expand "same_line?" )"" (hide 3)"" (expand "det" )"" (expand "on_line?" )"" (skosimp*)"" (replace -1)"" (hide -1)"" (replace -2)"" "" " x!1 * v(L0!1) - x!2 * v(L1!1) = p(L1!1) - p(L0!1)" )"1" "1" " x!3 * v(L0!1) - x!4 * v(L1!1) = p(L1!1) - p(L0!1)" )"1" "1" replace -1 * rl)"1" "1" assert )"1" "(x!1 - x!3)*v(L0!1) = (x!2 - x!4) * v(L1!1)" )"1" "(x!2 - x!4) = 0" )"1" assert )"1" "1" assert )"1" replace -1)"1" "1" "x!1 = x!3" )"1" "v(L0!1) = zero" )"1" assert )nil nil )"2" "2" "scal_eq_0" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "v(L1!1) = ((x!1 - x!3)/(x!2 - x!4))* v(L0!1)" )"1" "comp_eq_x" )"1" "1" expand "*" "1" assert )"1" "1" replace "1" "1" "comp_eq_y" )"1" "1" expand "*" "1" "1" replace "1" assert )nil nil ))nil )"2" replace "2" "1" assert )"1" expand "*" )"1" nil nil ))nil ))nil )"2" expand "*" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "*" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "*" )"2" nil nil ))nil ))nil )"3" assert )nil nil ))nil ))nil )"2" "1" "1" "comp_eq_x" )"1" "x!1 * v(L0!1) - x!2 * v(L1!1)" "x!3 * v(L0!1) - x!4 * v(L1!1)" )"1" expand "-" )"1" expand "*" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "comp_eq_y" )"2" "x!1 * v(L0!1) - x!2 * v(L1!1)" "x!3 * v(L0!1) - x!4 * v(L1!1)" )"2" expand "*" )"2" expand "-" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" "comp_eq_x" )"1" "p(L0!1) + x!3 * v(L0!1)" "p(L1!1) + x!4 * v(L1!1)" )"1" expand "+ " )"1" expand "*" )"1" assert )"1" expand "-" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "comp_eq_y" )"2" "p(L0!1) + x!3 * v(L0!1)" "p(L1!1) + x!4 * v(L1!1)" )"2" expand "*" )"2" expand "-" )"2" expand "+ " )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "comp_eq_x" )"1" "1" expand "*" )"1" expand "-" )"1" expand "+ " )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "comp_eq_y" )"2" "2" expand "*" )"2" expand "-" )"2" expand "+ " )"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 vectors_2D_def nil )nil vectors_2D nil )nil lines_2D nil )"real" det_2D nil )"Vector" vectors_2D nil )nil vectors_2D nil )nil vectors_2D nil )nil vectors_2D nil )nil vectors_2D nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )nil vectors_2D nil )"bool" lines_2D nil ))nil )nil 3430227209"" (skosimp*)"" (lemma "pt_intersect" )"" (inst - "L0!1" "L1!1" "p1!1" )"" (assert )"" (expand "intersect?" )"" (flatten)"" (expand "same_line?" )"" (hide 3)"" (expand "det" )"" (expand "on_line?" )"" (skosimp*)"" (replace -1)"" (hide -1)"" (replace -2)"" "" " x!1 * v(L0!1) - x!2 * v(L1!1) = p(L1!1) - p(L0!1)" )"1" "1" " x!3 * v(L0!1) - x!4 * v(L1!1) = p(L1!1) - p(L0!1)" )"1" "1" replace -1 * rl)"1" "1" assert )"1" "(x!1 - x!3)*v(L0!1) = (x!2 - x!4) * v(L1!1)" )"1" "(x!2 - x!4) = 0" )"1" assert )"1" "1" assert )"1" replace -1)"1" "1" "x!1 = x!3" )"1" "v(L0!1) = zero" )"1" assert )nil nil )"2" "2" "scal_eq_zero" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "v(L1!1) = ((x!1 - x!3)/(x!2 - x!4))* v(L0!1)" )"1" "comp_eq_x" )"1" "1" expand "*" "1" assert )"1" "1" replace "1" "1" "comp_eq_y" )"1" "1" expand "*" "1" "1" replace "1" assert )nil nil ))nil )"2" replace "2" "1" assert )"1" expand "*" )"1" nil nil ))nil ))nil )"2" expand "*" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "*" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "*" )"2" nil nil ))nil ))nil )"3" assert )nil nil ))nil ))nil )"2" "1" "1" "comp_eq_x" )"1" "x!1 * v(L0!1) - x!2 * v(L1!1)" "x!3 * v(L0!1) - x!4 * v(L1!1)" )"1" expand "-" )"1" expand "*" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "comp_eq_y" )"2" "x!1 * v(L0!1) - x!2 * v(L1!1)" "x!3 * v(L0!1) - x!4 * v(L1!1)" )"2" expand "*" )"2" expand "-" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" "comp_eq_x" )"1" "p(L0!1) + x!3 * v(L0!1)" "p(L1!1) + x!4 * v(L1!1)" )"1" expand "+ " )"1" expand "*" )"1" assert )"1" expand "-" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "comp_eq_y" )"2" "p(L0!1) + x!3 * v(L0!1)" "p(L1!1) + x!4 * v(L1!1)" )"2" expand "*" )"2" expand "-" )"2" expand "+ " )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "comp_eq_x" )"1" "1" expand "*" )"1" expand "-" )"1" expand "+ " )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "comp_eq_y" )"2" "2" expand "*" )"2" expand "-" )"2" expand "+ " )"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 )"bool" lines_2D nil )nil vectors_2D nil )"Vector" vectors_2D nil )"nnreal" vectors_2D nil )"Vector" vectors_2D nil )nil vectors_2D nil )nil vectors_2D nil )nil vectors_2D nil )"Vector" vectors_2D nil )"real" det_2D nil )nil lines_2D nil )nil vectors_2D nil )nil vectors_2D_def nil ))nil )nil 3267536081"" (skosimp*)"" (lemma "pt_intersect" )"" (inst - "L0!1" "L1!1" "p1!1" )"" (assert )"" (expand "intersect?" )"" (flatten)"" (expand "same_line?" )"" (hide 3)"" (expand "cross" )"" (expand "on_line?" )"" (skosimp*)"" (replace -1)"" (hide -1)"" (replace -2)"" "" " x!1 * v(L0!1) - x!2 * v(L1!1) = p(L1!1) - p(L0!1)" )"1" "1" " x!3 * v(L0!1) - x!4 * v(L1!1) = p(L1!1) - p(L0!1)" )"1" "1" replace -1 * rl)"1" "1" assert )"1" "(x!1 - x!3)*v(L0!1) = (x!2 - x!4) * v(L1!1)" )"1" "(x!2 - x!4) = 0" )"1" assert )"1" "1" assert )"1" replace -1)"1" "1" "x!1 = x!3" )"1" "v(L0!1) = zero" )"1" assert )nil nil )"2" "2" "scal_eq_zero" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "v(L1!1) = ((x!1 - x!3)/(x!2 - x!4))* v(L0!1)" )"1" "comp_eq_x" )"1" "1" expand "*" "1" assert )"1" "1" replace "1" "1" "comp_eq_y" )"1" "1" expand "*" "1" "1" replace "1" assert )nil nil ))nil )"2" replace "2" "1" assert )"1" expand "*" )"1" nil nil ))nil ))nil )"2" expand "*" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "*" )"2" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "2" expand "*" )"2" nil nil ))nil ))nil )"3" assert )nil nil ))nil ))nil )"2" "1" "1" "comp_eq_x" )"1" "x!1 * v(L0!1) - x!2 * v(L1!1)" "x!3 * v(L0!1) - x!4 * v(L1!1)" )"1" expand "-" )"1" expand "*" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "comp_eq_y" )"2" "x!1 * v(L0!1) - x!2 * v(L1!1)" "x!3 * v(L0!1) - x!4 * v(L1!1)" )"2" expand "*" )"2" expand "-" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" "comp_eq_x" )"1" "p(L0!1) + x!3 * v(L0!1)" "p(L1!1) + x!4 * v(L1!1)" )"1" expand "+ " )"1" expand "*" )"1" assert )"1" expand "-" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "comp_eq_y" )"2" "p(L0!1) + x!3 * v(L0!1)" "p(L1!1) + x!4 * v(L1!1)" )"2" expand "*" )"2" expand "-" )"2" expand "+ " )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "comp_eq_x" )"1" "1" expand "*" )"1" expand "-" )"1" expand "+ " )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "comp_eq_y" )"2" "2" expand "*" )"2" expand "-" )"2" expand "+ " )"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 )"bool" lines_2D nil )nil vectors_2D nil )"Vector" vectors_2D nil )"nnreal" vectors_2D nil )"Vector" vectors_2D nil )nil vectors_2D nil )nil vectors_2D nil )nil vectors_2D nil )"Vector" vectors_2D nil )nil lines_2D nil )nil vectors_2D nil )nil vectors_2D_def nil ))nil 3430227235"" (skeep)"" (expand "on_line?" )"" (skeep -1)"" (expand "same_line?" )"" (flatten)"" (lemma "parallel_det_0" )"" (inst?)"" (assert )"" (hide -3)"" (expand "parallel?" )"" (skeep -1)"" (lemma "parallel_det_0" )"" (inst?)"1" (assert )"1" "1" expand "parallel?" )"1" "nzk2" )"1" "1" "1" "nzk*(x-nzk2)" )"1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nz_vector?" )"2" "2" "2" "2" rewrite "sub_eq_zero" )"2" "2" "2" "x*nzk" )"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 )"bool" lines_2D nil )"bool" intersections_2D nil )nil parallel_2D nil )"bool" vectors_2D nil )nil vectors_2D nil )nil vectors_2D nil )"Nz_vector" vectors_2D nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil )"real" reals nil )"nzreal" nil )"Line2D" intersections_2D nil )"Line2D" intersections_2D nil )"Vector" vectors_2D nil )nil lines_2D nil )nil vectors_2D nil )nil vectors_2D_def nil )nil vectors_2D nil )"Vector" vectors_2D nil )"boolean" notequal nil )nil booleans nil )nil vectors_2D nil )nil reals nil ))nil )nil 3267869462"" (skosimp*)"" (expand "on_line?" )"" (skosimp*)"" (expand "same_line?" )"" (flatten)"" (replace -1)"" (hide -1)"" (name "DELTA" "L1!1`p - L0!1`p" )"" case "EXISTS (x: real): x!1 * v(L0!1) = DELTA + x * v(L1!1)" )"1" (skosimp*)"1" (inst + "x!2" )"1" (assert )"1" (replace -2)"1" (replace -2 * rl)"1" replace -1)"1" "1" "1" (grind) nil nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (replace -1)"2" (expand "cross" )"2" (hide -1)"2" (case "v(L1!1)`x = 0" )"1" replace -1)"1" assert )"1" case "v(L1!1)`y = 0" )"1" case "v(L1!1) = zero" )"1" (assert ) nil nil )"2" nil nil ))nil )"2" "(x!1 * v(L0!1)`y - DELTA`y)/ v(L1!1)`y" )"1" "1" expand "*" )"1" expand "+ ") "1" "1" "1" "1" replace -2)"1" assert )"1" replace -1)"1" assert )"1" "1" "1" case "v(L0!1) = zero" )"1" replace "1" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "+ " )"2" expand "*" )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "(x!1 * v(L0!1)`x - DELTA`x)/ v(L1!1)`x" )"1" "1" expand "+ " )"1" expand "*" )"1" (assert ) nil nil ))nil ))nil )"2" expand "*" )"2" expand "+ ") "2" "2" assert )"2" "2" "2" assert )"2" "v(L1!1)`x" )"2" replace -2 + rl)"2" assert )"2" "v(L1!1)`x * (L0!1`v`x * L1!1`v`y / v(L1!1)`x) = L0!1`v`x * L1!1`v`y " )"1" case "L0!1`v`x = 0" )"1" replace "1" assert )"1" case "L0!1`v`y = 0" )"1" replace "1" assert )"1" case "v(L0!1) = zero" )"1" replace "1" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" "L0!1`v`x" )"2" replace "2" assert )"2" replace "2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))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 ))nil )"bool" lines_2D nil )nil lines_2D nil )nil vectors_2D nil )nil vectors_2D_def nil )nil vectors_2D nil )"nnreal" vectors_2D nil )"Vector" vectors_2D nil )nil vectors_2D nil )nil vectors_2D nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil 3430227382"" (skosimp*)"" (expand "on_line?" )"" (skosimp*)"" (replace -2)"" (hide -2)"" (lemma "det_line" )"" (inst?)"" (assert )"" (replace -2)"" (flatten)"" (expand "same_line?" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" lines_2D nil )nil intersections_2D nil )"real" reals nil )"bool" intersections_2D nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil lines_2D nil )nil vectors_2D nil )nil vectors_2D_def nil ))nil )nil 3268038074"" (skosimp*)"" (expand "on_line?" )"" (skosimp*)"" (replace -2)"" (hide -2)"" (lemma "cross_lem" )"" (inst?)"" (assert )"" (replace -2)"" (flatten)"" (expand "same_line?" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" lines_2D nil )nil lines_2D nil )nil vectors_2D nil )nil vectors_2D_def nil ))nil 3267804562"" (skosimp*)"" (lemma "intersect_pt_unique" )"" (inst - "L0!1" "L1!1" "pnot!1" )"" (assert )"" (expand "intersect?" )"" (expand "same_line?" )"" (assert )"" (flatten)"" (lemma "pt_intersect" )"" (inst - "L0!1" "L1!1" "pnot!1" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil intersections_2D nil )"bool" intersections_2D nil )nil intersections_2D nil )"bool" intersections_2D nil )nil reals nil )nil lines_2D nil )nil vectors_2D nil )nil vectors_2D_def nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.150Bemerkung:
(vorverarbeitet am 2026-04-27)
¤ *Bot Zugriff
2026-05-26
