|
(intersections_2D
(det_line 0
(det_line-1 nil 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_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(+ const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(det const-decl "real" det_2D nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(Line2D type-eq-decl nil lines_2D nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(both_sides_times1_imp formula-decl nil extra_real_props nil))
nil))
(intersect_pt_TCC1 0
(intersect_pt_TCC1-1 nil 3267433756 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(/= const-decl "boolean" notequal nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(Line2D type-eq-decl nil lines_2D nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(- const-decl "Vector" vectors_2D nil)
(det const-decl "real" det_2D nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(same_line_sym 0
(same_line_sym-1 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"
(hide -4)
(("1"
(replace -1)
(("1"
(assert)
(("1"
(typepred "L0!1`v")
(("1"
(flatten)
(("1"
(lemma "norm_xy_eq_0")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(typepred "L0!1`v")
(("2"
(flatten)
(("2"
(lemma "norm_xy_eq_0")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace -1)
(("2"
(assert)
(("2"
(factor 1 l)
(("2"
(reveal -3)
(("2"
(assert)
(("2"
(replace -2)
(("2"
(replace -3)
(("2"
(assert)
(("2"
(factor 1 l)
(("2"
(factor -1 l)
(("2"
(mult-cases -1)
(("2"
(typepred
"L0!1`v")
(("2"
(flatten)
(("2"
(lemma
"norm_xy_eq_0")
(("2"
(inst?)
(("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)
((same_line? const-decl "bool" intersections_2D nil)
(both_sides_times1_imp formula-decl nil extra_real_props nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(Line2D type-eq-decl nil lines_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(both_sides_times1 formula-decl nil real_props nil)
(/= const-decl "boolean" notequal nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(L0!1 skolem-const-decl "Line2D" intersections_2D nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(zero_times3 formula-decl nil real_props nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
(norm_xy_eq_0 formula-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(det const-decl "real" det_2D nil)
(- const-decl "Vector" vectors_2D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil))
shostak))
(intersect_not_parallel 0
(intersect_not_parallel-1 nil 3267453794
("" (skosimp*)
(("" (expand "intersect?")
(("" (expand "parallel?")
(("" (flatten) (("" (skosimp*) (("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
((intersect? const-decl "bool" intersections_2D nil)
(nz_nzv application-judgement "Nz_vector" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(det const-decl "real" det_2D nil)
(* const-decl "Vector" vectors_2D nil)
(parallel? const-decl "bool" vectors_2D nil))
shostak))
(intersection_lem 0
(intersection_lem-2 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_div_nzreal_is_real application-judgement "real" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "Vector" vectors_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(Line2D type-eq-decl nil lines_2D nil)
(number nonempty-type-decl nil numbers nil)
(/= const-decl "boolean" notequal nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(det const-decl "real" det_2D nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(+ const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(both_sides_times1 formula-decl nil real_props nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil)
(intersection_lem-1 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)
((Line2D type-eq-decl nil lines_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(Vector type-eq-decl nil vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil))
nil))
(lines_intersection_TCC1 0
(lines_intersection_TCC1-1 nil 3543442415 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(number nonempty-type-decl nil numbers nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(- const-decl "Vector" vectors_2D nil)
(det const-decl "real" det_2D nil)
(/= const-decl "boolean" notequal nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(lines_intersection_sound 0
(lines_intersection_sound-1 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)
((intersection_lem formula-decl nil intersections_2D nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(lines_intersection const-decl "[real, real]" intersections_2D nil)
(det const-decl "real" det_2D nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(zero const-decl "Vector" vectors_2D nil)
(/= const-decl "boolean" notequal nil)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Line2D type-eq-decl nil lines_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil))
nil))
(pt_intersect 0
(pt_intersect-9 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"
(hide -1 2)
(("2"
(replace -1 * rl)
(("2"
(hide -1)
(("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"
(hide -1)
(("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"
(hide -2)
(("2"
(apply-extensionality 1 :hide? t)
(("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)
((on_line? const-decl "bool" lines_2D nil)
(intersect? const-decl "bool" intersections_2D nil)
(Line2D type-eq-decl nil lines_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(- const-decl "Vector" vectors_2D nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(add_move_right formula-decl nil vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(det const-decl "real" det_2D nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(same_line? const-decl "bool" intersections_2D nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(* const-decl "Vector" vectors_2D nil))
nil)
(pt_intersect-8 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"
(hide -1 2)
(("2"
(replace -1 * rl)
(("2"
(hide -1)
(("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"
(hide -1)
(("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"
(hide -2)
(("2"
(apply-extensionality 1 :hide? t)
(("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)
((on_line? const-decl "bool" lines_2D nil)
(Line2D type-eq-decl nil lines_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(Vector type-eq-decl nil vectors_2D nil)
(add_move_right formula-decl nil vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil))
nil)
(pt_intersect-7 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"
(hide -1 2)
(("2"
(replace -1 * rl)
(("2"
(hide -1)
(("2"
(expand "cross")
(("2"
(assert)
(("2"
(expand "-")
(("2"
(expand "*")
(("2"
(assert)
nil)))))))))))))))))
("2" (hide 2)
(("2"
(replace -1 * rl)
(("2"
(hide -1)
(("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"
(inst -1 "p(L1!1)" "x!2 * v(L1!1)"
"p(L0!1) + x!1 * v(L0!1)")
(("2"
(assert)
(("2"
(hide -2)
(("2"
(apply-extensionality 1 :hide? t)
(("1"
(expand "-")
(("1"
(expand "*")
(("1"
(expand "+")
(("1"
(lemma "comp_eq_x")
(("1"
(inst?)
(("1"
(assert)
nil)))))))))))
("2"
(expand "-")
(("2"
(expand "+ ")
(("2"
(expand "*")
(("2"
(lemma "comp_eq_y")
(("2"
(inst?)
(("2"
(assert)
nil))))))))))))))))))))))))))))))))))))))))))))
nil)
nil nil)
(pt_intersect-6 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"
(hide -1 2)
(("2"
(replace -1 * rl)
(("2"
(hide -1)
(("2"
(expand "cross")
(("2"
(assert)
(("2"
(expand "-")
(("2"
(expand "*")
(("2"
(assert)
nil)))))))))))))))))
("2" (hide 2)
(("2"
(replace -1 * rl)
(("2"
(hide -1)
(("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"
(inst -1 "p(L1!1)" "x!2 * v(L1!1)"
"p(L0!1) + x!1 * v(L0!1)")
(("2"
(assert)
(("2"
(hide -2)
(("2"
(apply-extensionality 1 :hide? t)
(("1"
(expand "-")
(("1"
(expand "*")
(("1"
(expand "+")
(("1"
(lemma "comp_eq_x")
(("1"
(inst?)
(("1"
(assert)
nil)))))))))))
("2"
(expand "-")
(("2"
(expand "+ ")
(("2"
(expand "*")
(("2"
(lemma "comp_eq_y")
(("2"
(inst?)
(("2"
(assert)
nil))))))))))))))))))))))))))))))))))))))))))))
nil)
nil nil)
(pt_intersect-5 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"
(hide -1 2)
(("2"
(replace -1 * rl)
(("2"
(hide -1)
(("2"
(expand "cross")
(("2"
(assert)
(("2"
(expand "-")
(("2"
(expand "*")
(("2"
(assert)
nil)))))))))))))))))
("2" (hide 2)
(("2"
(replace -1 * rl)
(("2"
(hide -1)
(("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"
(inst -1 "p(L1!1)" "x!2 * v(L1!1)"
"p(L0!1) + x!1 * v(L0!1)")
(("2"
(assert)
(("2"
(hide -2)
(("2"
(apply-extensionality 1 :hide? t)
(("1"
(expand "-")
(("1"
(expand "*")
(("1"
(expand "+")
(("1"
(lemma "comp_x_eq")
(("1"
(inst?)
(("1"
(assert)
nil)))))))))))
("2"
(expand "-")
(("2"
(expand "+ ")
(("2"
(expand "*")
(("2"
(lemma "comp_y_eq")
(("2"
(inst?)
(("2"
(assert)
nil))))))))))))))))))))))))))))))))))))))))))))
nil)
nil nil)
(pt_intersect-4 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"
(hide -1 2)
(("2"
(replace -1 * rl)
(("2"
(hide -1)
(("2"
(expand "cross")
(("2"
(assert)
(("2"
(expand "-")
(("2"
(expand "*")
(("2"
(assert)
nil)))))))))))))))))
("2" (hide 2)
(("2"
(replace -1 * rl)
(("2"
(hide -1)
(("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"
(inst -1 "p(L1!1)" "x!2 * v(L1!1)"
"p(L0!1) + x!1 * v(L0!1)")
(("2"
(assert)
(("2"
(hide -2)
(("2"
(apply-extensionality 1 :hide? t)
(("1"
(expand "-")
(("1"
(expand "*")
(("1"
(expand "+")
(("1"
(lemma "comp_eq_x")
(("1"
(inst?)
(("1"
(assert)
nil)))))))))))
("2"
(expand "-")
(("2"
(expand "+ ")
(("2"
(expand "*")
(("2"
(lemma "comp_eq_y")
(("2"
(inst?)
(("2"
(assert)
nil))))))))))))))))))))))))))))))))))))))))))))
nil)
nil nil)
(pt_intersect-3 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"
(hide -1 2)
(("2"
(replace -1 * rl)
(("2"
(hide -1)
(("2"
(expand "cross")
(("2"
(assert)
(("2"
(expand "-")
(("2"
(expand "*")
(("2"
(assert)
nil)))))))))))))))))
("2" (hide 2)
(("2"
(replace -1 * rl)
(("2"
(hide -1)
(("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"
(inst -1 "p(L1!1)" "x!2 * v(L1!1)"
"p(L0!1) + x!1 * v(L0!1)")
(("2"
(assert)
(("2"
(hide -2)
(("2"
(apply-extensionality 1 :hide? t)
(("1"
(expand "-")
(("1"
(expand "*")
(("1"
(expand "+")
(("1"
(lemma "comp_eq_x")
(("1"
(inst?)
(("1"
(assert)
nil)))))))))))
("2"
(expand "-")
(("2"
(expand "+ ")
(("2"
(expand "*")
(("2"
(lemma "comp_eq_y")
(("2"
(inst?)
(("2"
(assert)
nil))))))))))))))))))))))))))))))))))))))))))))
nil)
nil nil)
(pt_intersect-2 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"
(hide -1 2)
(("2"
(replace -1 * rl)
(("2"
(hide -1)
(("2"
(expand "cross")
(("2"
(assert)
(("2"
(expand "-")
(("2"
(expand "*")
(("2"
(assert)
nil)))))))))))))))))
("2" (hide 2)
(("2"
(replace -1 * rl)
(("2"
(hide -1)
(("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"
(inst -1 "p(L1!1)" "x!2 * v(L1!1)"
"p(L0!1) + x!1 * v(L0!1)")
(("2"
(assert)
(("2"
(hide -2)
(("2"
(apply-extensionality 1 :hide? t)
(("1"
(expand "-")
(("1"
(expand "*")
(("1"
(expand "+")
(("1"
(lemma "comp_eq_x")
(("1"
(inst?)
(("1"
(assert)
nil)))))))))))
("2"
(expand "-")
(("2"
(expand "+ ")
(("2"
(expand "*")
(("2"
(lemma "comp_eq_y")
(("2"
(inst?)
(("2"
(assert)
nil))))))))))))))))))))))))))))))))))))))))))))
nil)
nil nil)
(pt_intersect-1 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"
(hide -1 2)
(("2"
(replace -1 * rl)
(("2"
(hide -1)
(("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"
(hide -1)
(("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"
(inst -1 "p(L1!1)" "x!2 * v(L1!1)"
"p(L0!1) + x!1 * v(L0!1)")
(("2"
(assert)
(("2"
(hide -2)
(("2"
(apply-extensionality 1 :hide? t)
(("1"
(expand "-")
(("1"
(expand "*")
(("1"
(expand
"+
")
(("1"
(lemma "comp_eq_x")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "-")
(("2"
(expand "+ ")
(("2"
(expand "*")
(("2"
(lemma "comp_eq_y")
(("2"
(inst?)
(("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)
((add_move_right formula-decl nil vectors_2D nil)
(comp_eq_y formula-decl nil vectors_2D nil)
(comp_eq_x formula-decl nil vectors_2D nil)
(on_line? const-decl "bool" lines_2D nil)
(Line2D type-eq-decl nil lines_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil))
shostak))
(intersect_pt_unique_TCC1 0
(intersect_pt_unique_TCC1-1 nil 3267450311
("" (skosimp*)
(("" (expand "intersect?") (("" (assert) nil nil)) nil)) nil)
((intersect? const-decl "bool" intersections_2D nil)) shostak))
(intersect_pt_unique 0
(intersect_pt_unique-1 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"
(hide -1)
(("2"
(lemma "scal_cancel")
(("2"
(hide -2 -3)
(("2"
(inst?)
(("2"
(inst -1 "L1!1`v")
(("2"
(assert)
(("2"
(hide 2)
(("2"
(lemma
"add_cancel_left")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.66 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
