|
(perpendicular_2D
(neg_perpL 0
(neg_perpL-1 nil 3442581238 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)
(perpL const-decl "Vect2" perpendicular_2D nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(neg_perpR 0
(neg_perpR-1 nil 3442581264 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)
(perpR const-decl "Vect2" perpendicular_2D nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(perpL_perpR 0
(perpL_perpR-1 nil 3442582173 ("" (grind) nil nil)
((perpL const-decl "Vect2" perpendicular_2D nil)
(perpR const-decl "Vect2" perpendicular_2D nil)
(- const-decl "Vector" vectors_2D nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(dot_perpR_eq_0 0
(dot_perpR_eq_0-1 nil 3460107211 ("" (grind) nil nil)
((perpR const-decl "Vect2" perpendicular_2D nil)
(* const-decl "real" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(dot_perpL_eq_0 0
(dot_perpL_eq_0-1 nil 3460107216 ("" (grind) nil nil)
((perpL const-decl "Vect2" perpendicular_2D nil)
(* const-decl "real" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(dot_perpR_scal_eq_0 0
(dot_perpR_scal_eq_0-1 nil 3460107956 ("" (grind) nil nil)
((* const-decl "Vector" vectors_2D nil)
(perpR const-decl "Vect2" perpendicular_2D nil)
(* const-decl "real" vectors_2D nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(dot_perpL_scal_eq_0 0
(dot_perpL_scal_eq_0-1 nil 3460107271 ("" (grind) nil nil)
((* const-decl "Vector" vectors_2D nil)
(perpL const-decl "Vect2" perpendicular_2D nil)
(* const-decl "real" vectors_2D nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(sqv_perpR 0
(sqv_perpR-1 nil 3460109954 ("" (grind) nil nil)
((perpR const-decl "Vect2" perpendicular_2D nil)
(* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(sqv_perpL 0
(sqv_perpL-1 nil 3460109958 ("" (grind) nil nil)
((perpL const-decl "Vect2" perpendicular_2D nil)
(* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(perpR_add 0
(perpR_add-1 nil 3459875820 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_2D nil)
(perpR const-decl "Vect2" perpendicular_2D nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
shostak))
(perpR_sub 0
(perpR_sub-1 nil 3459875827 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)
(perpR const-decl "Vect2" perpendicular_2D nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(perpR_scal 0
(perpR_scal-1 nil 3459875832 ("" (grind) nil nil)
((* const-decl "Vector" vectors_2D nil)
(perpR const-decl "Vect2" perpendicular_2D nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(perpR_neg 0
(perpR_neg-1 nil 3459875836 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)
(perpR const-decl "Vect2" perpendicular_2D nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(perpR_eq_zero 0
(perpR_eq_zero-1 nil 3442582386
("" (decompose-equality)
(("1" (grind) nil nil) ("2" (grind) nil nil)) nil)
((minus_real_is_real application-judgement "real" reals nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(zero const-decl "Vector" vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil)
(perpR const-decl "Vect2" perpendicular_2D nil)
(comp_zero_y formula-decl nil vectors_2D nil)
(comp_zero_x formula-decl nil vectors_2D nil))
shostak))
(perpL_add 0
(perpL_add-1 nil 3459875886 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_2D nil)
(perpL const-decl "Vect2" perpendicular_2D nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
shostak))
(perpL_sub 0
(perpL_sub-1 nil 3459875891 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)
(perpL const-decl "Vect2" perpendicular_2D nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(perpL_scal 0
(perpL_scal-1 nil 3459875895 ("" (grind) nil nil)
((* const-decl "Vector" vectors_2D nil)
(perpL const-decl "Vect2" perpendicular_2D nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(perpL_neg 0
(perpL_neg-1 nil 3459875900 ("" (grind) nil nil)
((- const-decl "Vector" vectors_2D nil)
(perpL const-decl "Vect2" perpendicular_2D nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(perpL_eq_zero 0
(perpL_eq_zero-1 nil 3442582363
("" (decompose-equality)
(("1" (grind) nil nil) ("2" (grind) nil nil)) nil)
((minus_real_is_real application-judgement "real" reals nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(zero const-decl "Vector" vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil)
(perpL const-decl "Vect2" perpendicular_2D nil)
(comp_zero_y formula-decl nil vectors_2D nil)
(comp_zero_x formula-decl nil vectors_2D nil))
shostak))
(perpL_plus_perpR 0
(perpL_plus_perpR-1 nil 3442582869
("" (skeep)
(("" (rewrite "perpL_perpR") (("" (assert) nil nil)) nil)) nil)
((perpL_perpR formula-decl nil perpendicular_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(neg_add_left formula-decl nil vectors_2D nil))
shostak))
(perpR_perpR 0
(perpR_perpR-1 nil 3459876336 ("" (grind) nil nil)
((perpR const-decl "Vect2" perpendicular_2D nil)
(- const-decl "Vector" vectors_2D nil))
shostak))
(perpR_perpL 0
(perpR_perpL-1 nil 3459876356
("" (grind) (("" (decompose-equality 1) nil nil)) nil)
((real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-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)
(minus_real_is_real application-judgement "real" reals nil)
(perpR const-decl "Vect2" perpendicular_2D nil)
(perpL const-decl "Vect2" perpendicular_2D nil))
shostak))
(perpL_nz 0
(perpL_nz-1 nil 3442582362
("" (skeep)
(("" (typepred "nzv")
(("" (lemma "nzv_xy_neq_0")
(("" (inst?)
(("" (assert)
(("" (hide -2)
(("" (lemma "nzv_xy_neq_0")
(("" (inst -1 "perpL(nzv)")
(("" (assert)
(("" (hide -2) (("" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Nz_vect2 type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(perpL const-decl "Vect2" perpendicular_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(minus_real_is_real application-judgement "real" reals nil)
(nzv_xy_neq_0 formula-decl nil vectors_2D nil))
nil))
(perpR_nz 0
(perpR_nz-2 nil 3442582740
("" (skeep)
(("" (typepred "nzv")
(("" (lemma "nzv_xy_neq_0")
(("" (inst?)
(("" (assert)
(("" (hide -2)
(("" (lemma "nzv_xy_neq_0")
(("" (inst -1 "perpR(nzv)")
(("" (assert)
(("" (hide -2) (("" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Nz_vect2 type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(perpR const-decl "Vect2" perpendicular_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(minus_real_is_real application-judgement "real" reals nil)
(nzv_xy_neq_0 formula-decl nil vectors_2D nil))
nil)
(perpR_nz-1 nil 3442582362 ("" (judgement-tcc) nil nil) nil nil))
(perp_pt_TCC1 0
(perp_pt_TCC1-1 nil 3256494399
("" (skosimp*)
(("" (rewrite "dot_sq_norm")
(("" (rewrite "sq_eq_0") (("" (assert) nil nil)) nil)) nil))
nil)
((dot_sq_norm formula-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(norm const-decl "nnreal" vectors_2D nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(sq_eq_0 formula-decl nil sq "reals/"))
shostak))
(perp_is_normal 0
(perp_is_normal-3 nil 3256497716
("" (skosimp*)
(("" (name "W" "Q!1 - P0!1")
(("" (assert)
(("" (factor 1 l)
(("" (name-replace "tmt" "t!1 - tp!1" "")
((""
(case-replace
"(P0!1 + tp!1 * nzv!1) - Q!1 = tp!1*nzv!1 - W")
(("1" (hide -1)
(("1" (replace -2)
(("1" (hide -2)
(("1" (expand "perp_pt")
(("1" (replace -1)
(("1" (assert)
(("1" (lemma "dot_comm")
(("1" (inst -1 "W" "nzv!1")
(("1"
(replace -1)
(("1"
(rewrite "dot_sub_right")
(("1" (assert) nil nil)
("2"
(hide-all-but (-2 1))
(("2"
(flatten)
(("2"
(rewrite "dot_sq_norm")
(("2"
(lemma "sq_eq_0")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -2 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
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)
(number nonempty-type-decl nil numbers 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)
(* 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)
(* const-decl "real" vectors_2D nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(perp_pt const-decl "real" perpendicular_2D nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(dot_sub_right formula-decl nil vectors_2D nil)
(dot_scal_right formula-decl nil vectors_2D nil)
(dot_comm formula-decl nil vectors_2D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(dot_scal_left formula-decl nil vectors_2D nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil)
(perp_is_normal-2 nil 3256476685
("" (skosimp*)
(("" (case-replace "v!1*v!1 > 0")
(("1" (hide -3)
(("1" (replace -4)
(("1" (hide -4)
(("1"
(case-replace
"(P0!1 + tp!1 * v!1) - Q!1 = tp!1*v!1 - w!1")
(("1" (hide -1)
(("1" (replace -4)
(("1" (hide -4)
(("1" (name-replace "tmt" "t!1 - tp!1" "")
(("1" (replace -3)
(("1" (hide -3)
(("1" (lemma "dot_comm")
(("1" (inst -1 "w!1" "v!1")
(("1"
(replace -1)
(("1"
(assert)
(("1"
(rewrite "dot_sub_right")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-2 1)) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-2 1))
(("2" (rewrite "dot_sq_norm")
(("2" (lemma "sq_eq_0")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((Vector type-eq-decl nil vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(dot_scal_left formula-decl nil vectors_2D nil)
(dot_scal_right formula-decl nil vectors_2D nil)
(dot_sub_right formula-decl nil vectors_2D nil)
(dot_comm formula-decl nil vectors_2D nil)
(dot_sq_norm formula-decl nil vectors_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(sq_eq_0 formula-decl nil sq "reals/"))
nil)
(perp_is_normal-1 nil 3256470818
("" (skosimp*)
(("" (case-replace "v!1*v!1 > 0")
(("1" (hide -5)
(("1" (replace -6)
(("1" (hide -6)
(("1"
(case-replace
"(P0!1 + tp!1 * v!1) - Q!1 = tp!1*v!1 - w!1")
(("1" (hide -1)
(("1" (replace -3)
(("1" (hide -3)
(("1" (replace -3)
(("1" (hide -3)
(("1" (rewrite "scal_sub_left" :dir rl)
(("1" (name-replace "tmt" "t!1 - tp!1" "")
(("1" (replace -4)
(("1"
(hide -4)
(("1"
(lemma "dot_comm")
(("1"
(inst -1 "w!1" "v!1")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(replace -3)
(("1"
(hide -3)
(("1"
(assert)
(("1"
(rewrite
"dot_sub_right")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-4 1))
(("2" (rewrite "dot_sq_norm")
(("2" (lemma "sq_eq_0")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((sq_eq_0 formula-decl nil sq "reals/")
(norm const-decl "nnreal" vectors_2D nil)
(dot_sq_norm formula-decl nil vectors_2D nil)
(dot_sub_right formula-decl nil vectors_2D nil)
(dot_scal_right formula-decl nil vectors_2D nil)
(dot_scal_left formula-decl nil vectors_2D nil)
(dot_comm formula-decl nil vectors_2D nil)
(scal_sub_left formula-decl nil vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil))
shostak))
(perp_is_min 0
(perp_is_min-4 nil 3256497729
("" (skosimp*)
(("" (lemma "sq_norm_dist")
((""
(inst -1 "Q!1" "(P0!1 + tp!1 * nzv!1)" "(P0!1 + t!1 * nzv!1)")
(("" (assert)
(("" (name "DEL" "(t!1-tp!1)*nzv!1")
((""
(case-replace
"(P0!1 + tp!1 * nzv!1) - (P0!1 + t!1 * nzv!1) = -DEL")
(("1" (name "C" "(P0!1 + tp!1 * nzv!1) - Q!1")
(("1" (replace -1)
(("1" (lemma "perp_is_normal")
(("1" (inst -1 "P0!1" "Q!1" "nzv!1" "t!1" "tp!1")
(("1" (assert)
(("1" (case-replace "(C * -DEL) = 0")
(("1" (assert)
(("1" (lemma "sq_ge")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 -2 -3 1))
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sq_norm_dist formula-decl nil vectors_2D nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(dot_scal_left formula-decl nil vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(sq_ge formula-decl nil sq "reals/")
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_2D nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(norm_neg formula-decl nil vectors_2D nil)
(perp_is_normal formula-decl nil perpendicular_2D nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(/= const-decl "boolean" notequal nil)
(* const-decl "Vector" vectors_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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(+ const-decl "Vector" vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(real nonempty-type-from-decl nil reals nil))
nil)
(perp_is_min-3 nil 3256496154
("" (skosimp*)
(("" (lemma "sq_norm_dist")
((""
(inst -1 "Q!1" "(P0!1 + tp!1 * nzv!1)" "(P0!1 + t!1 * nzv!1)")
(("" (assert)
(("" (name "DEL" "(t!1-tp!1)*nzv!1")
((""
(case-replace
"(P0!1 + tp!1 * nzv!1) - (P0!1 + t!1 * nzv!1) = -DEL")
(("1" (name "C" "(P0!1 + tp!1 * nzv!1) - Q!1")
(("1" (replace -1)
(("1" (lemma "perp_is_normal2")
(("1" (inst -1 "P0!1" "Q!1" "nzv!1" "t!1" "tp!1")
(("1" (assert)
(("1" (case-replace "(C * -DEL) = 0")
(("1" (assert)
(("1" (lemma "sq_ge")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 -2 -3 1))
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((dot_scal_left formula-decl nil vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(sq_ge formula-decl nil sq "reals/")
(norm_neg formula-decl nil vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil))
nil)
(perp_is_min-2 nil 3256476748
("" (skosimp*)
(("" (lemma "sq_norm_dist")
(("" (inst -1 "Q!1" "(P0!1 + tp!1 * v!1)" "(P0!1 + t!1 * v!1)")
(("" (assert)
(("" (replace -6 * rl)
(("" (hide -6)
(("" (replace -3 * rl)
(("" (hide -3)
(("" (name "DEL" "(t!1-tp!1)*v!1")
((""
(case-replace
"(P0!1 + tp!1 * v!1) - (P0!1 + t!1 * v!1) = -DEL")
(("1" (lemma "perp_is_normal")
(("1"
(inst -1 "P0!1" "Q!1" "c!1" "DEL" "t!1"
"tp!1" "v!1" "w!1")
(("1" (assert)
(("1" (case-replace "(c!1 * -DEL) = 0")
(("1"
(assert)
(("1"
(lemma "sq_ge")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide-all-but (-1 1))
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 1))
(("2" (replace -1 * rl)
(("2" (hide -1) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((dot_scal_left formula-decl nil vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(sq_ge formula-decl nil sq "reals/")
(norm const-decl "nnreal" vectors_2D nil)
(norm_neg formula-decl nil vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil))
nil)
(perp_is_min-1 nil 3256472762
("" (skosimp*)
(("" (lemma "sq_norm_dist")
(("" (inst -1 "Q!1" "(P0!1 + tp!1 * v!1)" "(P0!1 + t!1 * v!1)")
(("" (assert)
(("" (replace -6 * rl)
(("" (hide -6)
(("" (replace -3 * rl)
(("" (hide -3)
(("" (name "DEL" "(t!1-tp!1)*v!1")
((""
(case-replace
"(P0!1 + tp!1 * v!1) - (P0!1 + t!1 * v!1) = -DEL")
(("1" (lemma "perp_is_normal2")
(("1"
(inst -1 "P0!1" "Q!1" "c!1" "DEL" "t!1"
"tp!1" "v!1" "w!1")
(("1" (assert)
(("1" (case-replace "(c!1 * -DEL) = 0")
(("1"
(assert)
(("1"
(lemma "sq_ge")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide-all-but (-1 1))
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 1))
(("2" (replace -1 * rl)
(("2" (hide -1) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((norm_sym formula-decl nil vectors_2D nil)
(dot_comm formula-decl nil vectors_2D nil)
(dot_scal_left formula-decl nil vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(sq_ge formula-decl nil sq "reals/")
(norm const-decl "nnreal" vectors_2D nil)
(norm_neg formula-decl nil vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil))
shostak))
(perp_gt_del 0
(perp_gt_del-5 nil 3256497744
("" (skosimp*)
(("" (assert)
(("" (lemma "sq_norm_dist")
((""
(inst -1 "Q!1" "(P0!1 + tp!1 * nzv!1)"
"(P0!1 + t!1 * nzv!1)")
(("" (assert)
(("" (name "DEL" "(t!1-tp!1)*nzv!1")
(("" (replace -1)
(("" (name "C" "(P0!1 + tp!1 * nzv!1) - Q!1")
(("" (replace -1)
((""
(case-replace
"(P0!1 + tp!1 * nzv!1) - (P0!1 + t!1 * nzv!1) = -DEL")
(("1" (lemma "perp_is_normal")
(("1"
(inst -1 "P0!1" "Q!1" "nzv!1" "t!1" "tp!1")
(("1" (assert)
(("1" (factor -1 l)
(("1"
(replace -3)
(("1"
(case-replace "(C * -DEL) = 0")
(("1"
(assert)
(("1"
(lemma "sq_ge")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide-all-but (-1 -4 1))
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-2 1))
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(Vector type-eq-decl nil vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sq_ge formula-decl nil sq "reals/")
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_2D nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(norm_neg formula-decl nil vectors_2D nil)
(perp_is_normal formula-decl nil perpendicular_2D nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(dot_scal_left formula-decl nil vectors_2D nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sq_norm_dist formula-decl nil vectors_2D nil))
nil)
(perp_gt_del-4 nil 3256496395
("" (skosimp*)
(("" (assert)
(("" (lemma "sq_norm_dist")
((""
(inst -1 "Q!1" "(P0!1 + tp!1 * nzv!1)"
"(P0!1 + t!1 * nzv!1)")
(("" (assert)
(("" (name "DEL" "(t!1-tp!1)*nzv!1")
(("" (replace -1)
(("" (name "C" "(P0!1 + tp!1 * nzv!1) - Q!1")
(("" (replace -1)
((""
(case-replace
"(P0!1 + tp!1 * nzv!1) - (P0!1 + t!1 * nzv!1) = -DEL")
(("1" (lemma "perp_is_normal2")
(("1"
(inst -1 "P0!1" "Q!1" "nzv!1" "t!1" "tp!1")
(("1" (assert)
(("1" (factor -1 l)
(("1"
(replace -3)
(("1"
(case-replace "(C * -DEL) = 0")
(("1"
(assert)
(("1"
(lemma "sq_ge")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide-all-but (-1 -4 1))
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-2 1))
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Vector type-eq-decl nil vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(sq_ge formula-decl nil sq "reals/")
(norm_neg formula-decl nil vectors_2D nil)
(dot_scal_left formula-decl nil vectors_2D nil))
nil)
(perp_gt_del-3 nil 3256476774
("" (skosimp*)
(("" (lemma "sq_norm_dist")
(("" (inst -1 "Q!1" "(P0!1 + tp!1 * v!1)" "(P0!1 + t!1 * v!1)")
(("" (assert)
(("" (replace -3 * rl)
(("" (hide -3)
((""
(case-replace
"(P0!1 + tp!1 * v!1) - (P0!1 + t!1 * v!1) = -del!1")
(("1" (hide -1)
(("1" (name-replace "C" "(P0!1 + tp!1 * v!1) - Q!1")
(("1" (rewrite "norm_neg")
(("1" (lemma "perp_is_normal")
(("1"
(inst -1 "P0!1" "Q!1" "C" "del!1" "t!1"
"tp!1" "v!1" "w!1")
(("1" (assert)
(("1" (reveal -2)
(("1"
(assert)
(("1"
(hide -1)
(("1"
(case-replace "(C * -del!1) = 0")
(("1"
(assert)
(("1"
(lemma "sq_ge")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide-all-but (-1 1))
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-5 1)) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((dot_scal_left formula-decl nil vectors_2D nil)
(norm_neg formula-decl nil vectors_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(sq_ge formula-decl nil sq "reals/")
(* const-decl "real" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil))
nil)
(perp_gt_del-2 nil 3256475340
("" (skosimp*)
(("" (lemma "sq_norm_dist")
(("" (inst -1 "Q!1" "(P0!1 + tp!1 * v!1)" "(P0!1 + t!1 * v!1)")
(("" (assert)
(("" (replace -3 * rl)
(("" (hide -3)
((""
(case-replace
"(P0!1 + tp!1 * v!1) - (P0!1 + t!1 * v!1) = -del!1")
(("1" (hide -1)
(("1" (name-replace "C" "(P0!1 + tp!1 * v!1) - Q!1")
(("1" (rewrite "norm_neg")
(("1" (lemma "perp_is_normal2")
(("1"
(inst -1 "P0!1" "Q!1" "C" "del!1" "t!1"
"tp!1" "v!1" "w!1")
(("1" (assert)
(("1" (reveal -2)
(("1"
(assert)
(("1"
(hide -1)
(("1"
(case-replace "(C * -del!1) = 0")
(("1"
(assert)
(("1"
(lemma "sq_ge")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide-all-but (-1 1))
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-5 1)) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Vector type-eq-decl nil vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(sq_ge formula-decl nil sq "reals/")
(norm const-decl "nnreal" vectors_2D nil)
(norm_neg formula-decl nil vectors_2D nil)
(dot_scal_left formula-decl nil vectors_2D nil))
nil)
(perp_gt_del-1 nil 3256470708
("" (skosimp*) (("" (postpone) nil nil)) nil) nil shostak))
(perp_comps 0
(perp_comps-2 nil 3256497762
("" (skosimp*)
(("" (assert)
(("" (lemma "sq_norm_dist")
((""
(inst -1 "Q!1" "(P0!1 + tp!1 * nzv!1)"
"(P0!1 + t!1 * nzv!1)")
(("" (assert)
(("" (lemma "perp_is_normal")
(("" (inst -1 "P0!1" "Q!1" "nzv!1" "t!1" "tp!1")
(("" (assert)
(("" (factor -1 l)
(("" (name "DEL" "(t!1 - tp!1) * nzv!1")
(("" (name "C" "(P0!1 + tp!1 * nzv!1) - Q!1")
(("" (replace -1)
(("" (replace -2)
((""
(case-replace
"(P0!1 + tp!1 * nzv!1) - (P0!1 + t!1 * nzv!1) = -DEL")
(("1"
(hide -1)
(("1"
(case-replace "C*-DEL = 0")
(("1" (assert) nil nil)
("2"
(hide-all-but (-1 -2 -3 1))
(("2" (grind) nil nil))
nil))
nil))
nil)
("2"
(hide-all-but (-1 -2 1))
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(Vector type-eq-decl nil vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(perp_is_normal formula-decl nil perpendicular_2D nil)
(- const-decl "Vector" vectors_2D nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(norm_neg formula-decl nil vectors_2D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(- const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(dot_scal_left formula-decl nil vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sq_norm_dist formula-decl nil vectors_2D nil))
nil)
(perp_comps-1 nil 3256493866
("" (skosimp*)
(("" (assert)
(("" (lemma "sq_norm_dist")
((""
(inst -1 "Q!1" "(P0!1 + tp!1 * nzv!1)"
"(P0!1 + t!1 * nzv!1)")
(("" (assert)
(("" (lemma "perp_is_normal2")
(("" (inst -1 "P0!1" "Q!1" "nzv!1" "t!1" "tp!1")
(("" (assert)
(("" (factor -1 l)
(("" (name "DEL" "(t!1 - tp!1) * nzv!1")
(("" (name "C" "(P0!1 + tp!1 * nzv!1) - Q!1")
(("" (replace -1)
(("" (replace -2)
((""
(case-replace
"(P0!1 + tp!1 * nzv!1) - (P0!1 + t!1 * nzv!1) = -DEL")
(("1"
(hide -1)
(("1"
(case-replace "C*-DEL = 0")
(("1" (assert) nil nil)
("2"
(hide-all-but (-1 -2 -3 1))
(("2" (grind) nil nil))
nil))
nil))
nil)
("2"
(hide-all-but (-1 -2 1))
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Vector type-eq-decl nil vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(norm_neg formula-decl nil vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(dot_scal_left formula-decl nil vectors_2D nil))
shostak))
(perp_pt_TCC2 0
(perp_pt_TCC2-1 nil 3256899624
("" (skosimp*)
(("" (mult-cases -1)
(("" (rewrite "dot_sq_norm")
(("" (lemma "norm_eq_0")
(("" (inst?)
(("" (assert)
(("" (lemma "sq_eq_0")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((norm_eq_0 formula-decl nil vectors_2D nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
(Line 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)
(real nonempty-type-from-decl nil reals nil)
(dot_sq_norm formula-decl nil vectors_2D nil))
shostak))
(dist_is_min 0
(dist_is_min-2 nil 3275737482
("" (skosimp*)
(("" (expand "on_line?")
(("" (skosimp*)
(("" (rewrite "dist_norm")
(("" (expand "dist")
(("" (lemma "perp_is_min")
(("" (assert)
((""
(inst -1 "p(L!1)" "q!1" "v(L!1)" "x!1"
"perp_pt(q!1, p(L!1), v(L!1))")
(("" (assert)
(("" (replace -2 * rl)
(("" (rewrite "norm_sym")
(("" (rewrite "dist_norm")
((""
(case-replace
"perp_pt(q!1,p(L!1), v(L!1)) = perp_pt(q!1, L!1)")
(("" (hide 2)
((""
(expand "perp_pt")
(("" (propax) 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)
(dist_norm formula-decl nil distance_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(perp_is_min formula-decl nil perpendicular_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(Line type-eq-decl nil lines_2D nil)
(Vector type-eq-decl nil vectors_2D nil)
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_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)
(perp_pt const-decl "real" perpendicular_2D nil)
(perp_pt const-decl "real" perpendicular_2D nil)
(* const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(norm_sym formula-decl nil vectors_2D nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(dist const-decl "nnreal" perpendicular_2D nil))
nil)
(dist_is_min-1 nil 3256581494
("" (skosimp*)
(("" (expand "on_line?")
(("" (skosimp*)
(("" (rewrite "dist_norm")
(("" (expand "dist")
(("" (lemma "perp_is_min")
(("" (assert)
(("" (inst -1 "p(L!1)" "q!1" "v(L!1)" "x!1")
(("" (assert)
(("" (replace -2 * rl)
(("" (rewrite "norm_sym")
(("" (rewrite "dist_norm")
((""
(case-replace
"perp_pt(q!1 - p(L!1), v(L!1)) = perp_pt(q!1, L!1)")
(("" (hide 2)
((""
(expand "perp_pt")
(("" (propax) 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)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(Line type-eq-decl nil lines_2D nil)
(Vector type-eq-decl nil vectors_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(norm_sym formula-decl nil vectors_2D nil))
shostak))
(perp_pt_perp_TCC1 0
(perp_pt_perp_TCC1-1 nil 3306141333 ("" (subtype-tcc) nil nil)
((- const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(perp_pt const-decl "real" perpendicular_2D nil)
(* const-decl "Vector" vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil))
nil))
(perp_pt_perp 0
(perp_pt_perp-1 nil 3256908342
("" (skosimp*)
(("" (hide 1)
(("" (expand "perpendicular?")
(("" (expand "orthogonal?")
(("" (expand "line_from")
(("" (expand "vec_from")
(("" (assert)
(("" (auto-rewrite "dot_add_right")
(("" (auto-rewrite "dot_add_left")
(("" (auto-rewrite "dot_sub_right")
(("" (assert)
(("" (auto-rewrite "dot_sub_left")
(("" (expand "perp_pt")
(("" (assert)
((""
(field 1)
(("1"
(rewrite "dot_comm")
(("1" (assert) nil nil))
nil)
("2" (rewrite "dot_comm") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((orthogonal? const-decl "bool" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(dot_scal_right formula-decl nil vectors_2D nil)
(dot_add_right formula-decl nil vectors_2D nil)
(dot_sub_right formula-decl nil vectors_2D nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(perp_pt const-decl "real" perpendicular_2D 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)
(Vector type-eq-decl nil vectors_2D 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 "real" vectors_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(Line type-eq-decl nil lines_2D nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(dot_comm formula-decl nil vectors_2D nil)
(dot_sub_left formula-decl nil vectors_2D nil)
(line_from const-decl "Line" lines_2D nil)
(perpendicular? const-decl "bool" perpendicular_2D nil))
shostak)))
¤ Dauer der Verarbeitung: 0.47 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.
|
