|
(law_cos_pos_2D
(law_cosines 0
(law_cosines-1 nil 3254574496
("" (skosimp*)
(("" (assert)
(("" (flatten)
(("" (expand "dist")
(("" (expand "sq_dist")
(("" (replace -1)
(("" (hide -1)
(("" (expand "sq")
(("" (ground) (("" (grind) 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_times_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(dist const-decl "nnreal" distance_2D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(- const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_dist const-decl "nnreal" distance_2D nil))
nil))
(law_cosines_alt 0
(law_cosines_alt-1 nil 3254574496
("" (skosimp*)
(("" (assert)
(("" (expand "dist")
(("" (expand "sq_dist")
(("" (expand "sq") (("" (ground) (("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
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)
(sq_dist const-decl "nnreal" distance_2D nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(* const-decl "real" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(sq const-decl "nonneg_real" sq "reals/")
(real_plus_real_is_real application-judgement "real" reals nil)
(dist const-decl "nnreal" distance_2D nil))
nil))
(angle_exists 0
(angle_exists-1 nil 3254574496
("" (skosimp*)
(("" (assert)
((""
(case-replace "dist(v1!1, v0!1) = 0 OR dist(v2!1, v1!1) = 0 ")
(("1" (split -1)
(("1" (replace -1)
(("1" (assert)
(("1" (lemma "dist_eq_0")
(("1" (inst?)
(("1" (flatten)
(("1" (assert)
(("1" (replace -1) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -1)
(("2" (lemma "dist_eq_0")
(("2" (inst?)
(("2" (assert)
(("2" (replace -1) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2"
(case " -1 <=
(v1!1 - v0!1) * (v1!1 - v2!1) /
(dist(v1!1, v0!1) * dist(v2!1, v1!1))
AND
(v1!1 - v0!1) * (v1!1 - v2!1) /
(dist(v1!1, v0!1) * dist(v2!1, v1!1))
<= 1")
(("1"
(inst +
"arccos((v1!1 - v0!1) * (v1!1 - v2!1)/(dist(v1!1, v0!1)*dist(v2!1, v1!1)))")
(("1" (assert) nil nil)
("2" (flatten) (("2" (assert) nil nil)) nil))
nil)
("2" (hide 4)
(("2" (rewrite "dist_norm")
(("2" (rewrite "dist_norm")
(("2" (lemma "dot_norm")
(("2" (inst?)
(("2" (flatten)
(("2" (prop)
(("1" (cross-mult 1)
(("1" (ground)
(("1"
(lemma "norm_sym")
(("1"
(inst -1 "v1!1" "v2!1")
(("1"
(replace -1)
(("1"
(hide -1)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (mult-cases 1) nil nil))
nil))
nil)
("2" (cross-mult 1)
(("2" (ground)
(("1"
(lemma "norm_sym")
(("1"
(inst -1 "v1!1" "v2!1")
(("1"
(replace -1)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (mult-cases 1) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (flatten) (("3" (mult-cases -2) nil nil)) nil)
("4" (assert)
(("4" (flatten) (("4" (mult-cases -1) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(zero_times3 formula-decl nil real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(norm_sym formula-decl nil vectors_2D nil)
(pos_times_gt formula-decl nil real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(norm const-decl "nnreal" vectors_2D nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(div_mult_pos_neg_le2 formula-decl nil extra_real_props nil)
(div_mult_pos_neg_le1 formula-decl nil extra_real_props nil)
(dot_norm formula-decl nil vectors_2D nil)
(dist_norm formula-decl nil distance_2D nil)
(v1!1 skolem-const-decl "Vect2" law_cos_pos_2D nil)
(v0!1 skolem-const-decl "Vect2" law_cos_pos_2D nil)
(v2!1 skolem-const-decl "Vect2" law_cos_pos_2D nil)
(real_abs_le1 nonempty-type-eq-decl nil asin "trig/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(pi_lb const-decl "posreal" trig_basic "trig/")
(< const-decl "bool" reals nil)
(pi_ub const-decl "posreal" trig_basic "trig/")
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(nnreal_le_pi nonempty-type-eq-decl nil acos "trig/")
(cos const-decl "real" trig_basic "trig/")
(arccos const-decl "{x: nnreal_le_pi | y = cos(x)}" trig_inverses
"trig/")
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(Vector type-eq-decl nil vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(dist_eq_args formula-decl nil distance_2D nil)
(sub_eq_args formula-decl nil vectors_2D nil)
(dot_zero_left formula-decl nil vectors_2D nil)
(dist_eq_0 formula-decl nil distance_2D nil)
(dot_zero_right formula-decl nil vectors_2D nil)
(dist const-decl "nnreal" distance_2D nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" 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)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(real nonempty-type-from-decl nil reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(angle_between_TCC1 0
(angle_between_TCC1-2 nil 3430759676
("" (skosimp*)
(("" (lemma "dot_norm")
(("" (inst?)
(("" (assert)
(("" (ground)
(("1" (cross-mult 1) (("1" (assert) nil nil)) nil)
("2" (cross-mult 1) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((dot_norm formula-decl nil vectors_2D nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(div_mult_pos_le1 formula-decl nil real_props nil)
(div_mult_pos_le2 formula-decl nil real_props nil)
(* const-decl "real" vectors_2D nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(norm const-decl "nnreal" vectors_2D nil)
(nnreal type-eq-decl nil real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-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)
(Nz_vect2 type-eq-decl nil vectors_2D 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)
(minus_real_is_real application-judgement "real" reals nil))
nil)
(angle_between_TCC1-1 nil 3254574496
("" (skosimp*) (("" (mult-cases -1) nil nil)) nil)
((Nz_vect2 type-eq-decl nil vectors_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil))
nil))
(law_cosines_bnd 0
(law_cosines_bnd-1 nil 3254574496
("" (skosimp*)
(("" (skoletin 1)
(("" (skoletin 1)
(("" (skoletin 1)
(("" (lemma "angle_exists")
(("" (inst -1 "v0!1" "v1!1" "v2!1")
(("" (skosimp*)
(("" (assert)
(("" (lemma "law_cosines")
(("" (inst?)
(("" (inst -1 "ab!1")
(("" (assert)
(("" (replace -5 * rl)
(("" (replace -4 * rl)
((""
(replace -3 * rl)
((""
(case
"sq(a) + sq(b) - 2 * (cos(ab!1) * a * b) >=
sq(a) + sq(b) - 2 * a * b")
(("1"
(case-replace
"sq(a) + sq(b) - 2 * a * b = sq(a - b)")
(("1" (assert) nil nil)
("2"
(hide-all-but 1)
(("2" (grind) nil nil))
nil))
nil)
("2"
(assert)
(("2"
(hide-all-but 1)
(("2"
(typepred "cos(ab!1)")
(("2"
(mult-by -2 "2*a*b")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((IFF const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(dist const-decl "nnreal" distance_2D nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types 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_times_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(cos const-decl "real" trig_basic "trig/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(<= const-decl "bool" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(law_cosines formula-decl nil law_cos_pos_2D nil)
(angle_exists formula-decl nil law_cos_pos_2D nil))
nil))
(law_cosines_bnd_abs 0
(law_cosines_bnd_abs-1 nil 3254574496
("" (skosimp*)
(("" (skoletin 1)
(("" (skoletin 1)
(("" (skoletin 1)
(("" (lemma "law_cosines_bnd")
(("" (inst -1 "v0!1" "v1!1" "v2!1")
(("" (assert)
(("" (replace -2 * rl)
(("" (replace -3 * rl)
(("" (replace -4 * rl)
(("" (case "a-b>=0")
(("1" (rewrite "sq_ge" -)
(("1" (expand "abs") (("1" (assert) nil nil))
nil))
nil)
("2" (rewrite "sq_neg_minus")
(("2" (rewrite "sq_ge" -)
(("2" (expand "abs")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((IFF const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(dist const-decl "nnreal" distance_2D nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sq_neg_minus formula-decl nil sq "reals/")
(minus_real_is_real application-judgement "real" reals nil)
(sq_ge formula-decl nil sq "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(law_cosines_bnd formula-decl nil law_cos_pos_2D nil))
nil))
(law_cosines_le 0
(law_cosines_le-1 nil 3254574496
("" (skosimp*)
(("" (skoletin 1)
(("" (reveal "a" "b" "c")
(("" (rewrite "dist_norm")
(("" (rewrite "dist_norm")
(("" (rewrite "dist_norm")
(("" (replace -1)
(("" (hide -1)
(("" (replace -1)
(("" (hide -1)
(("" (replace -1)
(("" (hide -1)
(("" (lemma "norm_sub_le")
(("" (inst -1 "v2!1 - v1!1" "v0!1 - v1!1")
((""
(case-replace
"v2!1 - v1!1 - (v0!1 - v1!1) = v2!1 - v0!1")
(("1"
(hide -1)
(("1"
(lemma "norm_sym")
(("1"
(inst -1 "v1!1" "v0!1")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((IFF const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(dist const-decl "nnreal" distance_2D nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<= const-decl "bool" reals nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(norm_sub_le formula-decl nil vectors_2D nil)
(norm_sym formula-decl nil vectors_2D nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(dist_norm formula-decl nil distance_2D nil))
nil)))
¤ Dauer der Verarbeitung: 0.24 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.
|
