|
(perpendicular_3D
(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_3D nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_3D nil)
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_3D nil)
(Nz_vect3 type-eq-decl nil vectors_3D nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_3D nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(norm const-decl "nnreal" vectors_3D 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)
((Vect3 type-eq-decl nil vectors_3D_def nil)
(- const-decl "Vector" vectors_3D nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_3D 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_3D nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_3D nil)
(Nz_vect3 type-eq-decl nil vectors_3D nil)
(+ const-decl "Vector" vectors_3D nil)
(* const-decl "Vector" vectors_3D nil)
(perp_pt const-decl "real" perpendicular_3D 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_3D nil)
(dot_scal_right formula-decl nil vectors_3D nil)
(dot_comm formula-decl nil vectors_3D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(dot_scal_left formula-decl nil vectors_3D 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_3D nil)
(* const-decl "real" vectors_3D nil)
(+ const-decl "Vector" vectors_3D nil)
(* const-decl "Vector" vectors_3D nil)
(dot_scal_left formula-decl nil vectors_3D nil)
(dot_scal_right formula-decl nil vectors_3D nil)
(dot_sub_right formula-decl nil vectors_3D nil)
(dot_comm formula-decl nil vectors_3D nil)
(dot_sq_norm formula-decl nil vectors_3D nil)
(norm const-decl "nnreal" vectors_3D 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_3D nil)
(dot_sq_norm formula-decl nil vectors_3D nil)
(dot_sub_right formula-decl nil vectors_3D nil)
(dot_scal_right formula-decl nil vectors_3D nil)
(dot_scal_left formula-decl nil vectors_3D nil)
(dot_comm formula-decl nil vectors_3D nil)
(scal_sub_left formula-decl nil vectors_3D nil)
(* const-decl "Vector" vectors_3D nil)
(+ const-decl "Vector" vectors_3D nil)
(* const-decl "real" vectors_3D nil)
(Vector type-eq-decl nil vectors_3D 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_3D 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_3D nil)
(- const-decl "Vector" vectors_3D nil)
(- const-decl "Vector" vectors_3D nil)
(* const-decl "real" vectors_3D 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_3D 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_3D nil)
(perp_is_normal formula-decl nil perpendicular_3D 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_vect3 type-eq-decl nil vectors_3D nil)
(zero const-decl "Vector" vectors_3D nil)
(/= const-decl "boolean" notequal nil)
(* const-decl "Vector" vectors_3D 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_3D nil)
(Vector type-eq-decl nil vectors_3D nil)
(Vect3 type-eq-decl nil vectors_3D_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_3D nil)
(* const-decl "real" vectors_3D nil)
(sq_ge formula-decl nil sq "reals/")
(norm_neg formula-decl nil vectors_3D nil)
(norm const-decl "nnreal" vectors_3D nil)
(* const-decl "Vector" vectors_3D nil)
(+ const-decl "Vector" vectors_3D nil)
(Vector type-eq-decl nil vectors_3D 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_3D nil)
(* const-decl "real" vectors_3D nil)
(sq_ge formula-decl nil sq "reals/")
(norm const-decl "nnreal" vectors_3D nil)
(norm_neg formula-decl nil vectors_3D nil)
(* const-decl "Vector" vectors_3D nil)
(+ const-decl "Vector" vectors_3D nil)
(Vector type-eq-decl nil vectors_3D 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_3D nil)
(dot_comm formula-decl nil vectors_3D nil)
(dot_scal_left formula-decl nil vectors_3D nil)
(* const-decl "real" vectors_3D nil)
(sq_ge formula-decl nil sq "reals/")
(norm const-decl "nnreal" vectors_3D nil)
(norm_neg formula-decl nil vectors_3D nil)
(* const-decl "Vector" vectors_3D nil)
(+ const-decl "Vector" vectors_3D nil)
(Vector type-eq-decl nil vectors_3D 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)
(Vect3 type-eq-decl nil vectors_3D_def nil)
(Vector type-eq-decl nil vectors_3D nil)
(+ const-decl "Vector" vectors_3D 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_3D nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_3D nil)
(Nz_vect3 type-eq-decl nil vectors_3D 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_3D nil)
(- const-decl "Vector" vectors_3D nil)
(* const-decl "real" vectors_3D 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_3D 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_3D nil)
(perp_is_normal formula-decl nil perpendicular_3D nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(dot_scal_left formula-decl nil vectors_3D 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_3D 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_3D nil)
(+ const-decl "Vector" vectors_3D nil)
(* const-decl "Vector" vectors_3D nil)
(norm const-decl "nnreal" vectors_3D nil)
(* const-decl "real" vectors_3D nil)
(sq_ge formula-decl nil sq "reals/")
(norm_neg formula-decl nil vectors_3D nil)
(dot_scal_left formula-decl nil vectors_3D 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_3D nil)
(norm_neg formula-decl nil vectors_3D nil)
(norm const-decl "nnreal" vectors_3D nil)
(sq_ge formula-decl nil sq "reals/")
(* const-decl "real" vectors_3D nil)
(* const-decl "Vector" vectors_3D nil)
(+ const-decl "Vector" vectors_3D nil)
(Vector type-eq-decl nil vectors_3D 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_3D nil)
(+ const-decl "Vector" vectors_3D nil)
(* const-decl "Vector" vectors_3D nil)
(* const-decl "real" vectors_3D nil)
(sq_ge formula-decl nil sq "reals/")
(norm const-decl "nnreal" vectors_3D nil)
(norm_neg formula-decl nil vectors_3D nil)
(dot_scal_left formula-decl nil vectors_3D 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)
(Vect3 type-eq-decl nil vectors_3D_def nil)
(Vector type-eq-decl nil vectors_3D nil)
(+ const-decl "Vector" vectors_3D 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_3D nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_3D nil)
(Nz_vect3 type-eq-decl nil vectors_3D nil)
(perp_is_normal formula-decl nil perpendicular_3D nil)
(- const-decl "Vector" vectors_3D 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_3D 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_3D nil)
(* const-decl "real" vectors_3D 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_3D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sq_norm_dist formula-decl nil vectors_3D 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_3D nil)
(+ const-decl "Vector" vectors_3D nil)
(* const-decl "Vector" vectors_3D nil)
(norm const-decl "nnreal" vectors_3D nil)
(norm_neg formula-decl nil vectors_3D nil)
(* const-decl "real" vectors_3D nil)
(dot_scal_left formula-decl nil vectors_3D 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_3D nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nz_norm_gt_0 application-judgement "posreal" vectors_3D nil)
(Line type-eq-decl nil lines_3D nil)
(Nz_vect3 type-eq-decl nil vectors_3D nil)
(Vect3 type-eq-decl nil vectors_3D_def nil)
(Vector type-eq-decl nil vectors_3D nil)
(real nonempty-type-from-decl nil reals nil)
(dot_sq_norm formula-decl nil vectors_3D nil))
shostak))
(dist_is_min 0
(dist_is_min-2 nil 3275737649
("" (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_3D nil)
(dist_norm formula-decl nil distance_3D nil)
(real nonempty-type-from-decl nil reals nil)
(Vect3 type-eq-decl nil vectors_3D_def nil)
(perp_is_min formula-decl nil perpendicular_3D nil)
(Nz_vect3 type-eq-decl nil vectors_3D nil)
(Line type-eq-decl nil lines_3D nil)
(Vector type-eq-decl nil vectors_3D nil)
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_3D 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_3D nil)
(perp_pt const-decl "real" perpendicular_3D nil)
(* const-decl "Vector" vectors_3D nil)
(+ const-decl "Vector" vectors_3D nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(norm_sym formula-decl nil vectors_3D nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(dist const-decl "nnreal" perpendicular_3D 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)
((Nz_vect3 type-eq-decl nil vectors_3D nil)
(on_line? const-decl "bool" lines_3D nil)
(Line type-eq-decl nil lines_3D nil)
(Vector type-eq-decl nil vectors_3D nil)
(norm const-decl "nnreal" vectors_3D nil)
(* const-decl "Vector" vectors_3D nil)
(+ const-decl "Vector" vectors_3D nil)
(norm_sym formula-decl nil vectors_3D nil))
shostak))
(perp_pt_perp_TCC1 0
(perp_pt_perp_TCC1-1 nil 3306141400 ("" (subtype-tcc) nil nil)
((- const-decl "Vector" vectors_3D nil)
(* const-decl "real" vectors_3D nil)
(perp_pt const-decl "real" perpendicular_3D nil)
(* const-decl "Vector" vectors_3D nil)
(+ const-decl "Vector" vectors_3D 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_3D nil)
(vec_from const-decl "Vect3" lines_3D nil)
(dot_sub_left formula-decl nil vectors_3D nil)
(dot_comm formula-decl nil vectors_3D nil)
(minus_odd_is_odd application-judgement "odd_int" integers 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)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Line type-eq-decl nil lines_3D nil)
(Nz_vect3 type-eq-decl nil vectors_3D nil)
(Vect3 type-eq-decl nil vectors_3D_def nil)
(* const-decl "real" vectors_3D 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)
(Vector type-eq-decl nil vectors_3D nil)
(real nonempty-type-from-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(perp_pt const-decl "real" perpendicular_3D nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(dot_sub_right formula-decl nil vectors_3D nil)
(dot_add_right formula-decl nil vectors_3D nil)
(dot_scal_right formula-decl nil vectors_3D nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(line_from const-decl "Line" lines_3D nil)
(perpendicular? const-decl "bool" perpendicular_3D nil))
shostak)))
¤ Dauer der Verarbeitung: 0.174 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.
|
