|
(vectors_3D_cos
(cosines_law 0
(cosines_law-2 nil 3254160440
("" (skosimp*)
(("" (skoletin* +)
(("" (flatten)
(("" (both-sides-f -1 "sqv")
(("" (expand "sqv" -1)
((""
(case-replace "(va!1 - vb!1)*(va!1 - vb!1) =
va!1*va!1 + vb!1*vb!1 - 2*va!1*vb!1")
(("1" (hide -1)
(("1" (rewrite "dot_sq_norm")
(("1" (rewrite "dot_sq_norm")
(("1" (rewrite "dot_sq_norm")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (hide-all-but 1)
(("2" (rewrite "dot_sub_right")
(("2" (rewrite "dot_sub_left")
(("2" (rewrite "dot_sub_left")
(("2" (assert)
(("2" (rewrite "dot_comm")
(("2" (rewrite "dot_comm")
(("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)
(Vector type-eq-decl nil vectors_3D 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)
(norm const-decl "nnreal" vectors_3D nil)
(Vect3 type-eq-decl nil vectors_3D_def nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(* const-decl "real" vectors_3D nil)
(cos const-decl "real" trig_basic "trig/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "Vector" vectors_3D nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sqv const-decl "nnreal" vectors_3D nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(* const-decl "Vector" vectors_3D nil)
(dot_sq_norm 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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(dot_sub_left formula-decl nil vectors_3D nil)
(dot_comm formula-decl nil vectors_3D nil)
(dot_sub_right formula-decl nil vectors_3D nil))
nil)
(cosines_law-1 nil 3254160430
("" (skosimp*)
(("" (skoletin 1)
(("" (flatten)
(("" (assert)
(("" (replace -2)
(("" (hide -2)
(("" (transform-both -1 "sqv(%1)")
(("1" (expand "sqv" -1)
(("1"
(case-replace "(va!1 - vb!1)*(va!1 - vb!1) =
va!1*va!1 + vb!1*vb!1 - 2*va!1*vb!1")
(("1" (hide -1)
(("1" (rewrite "dot_sq_norm")
(("1" (rewrite "dot_sq_norm")
(("1" (rewrite "dot_sq_norm")
(("1" (reveal "a" "b" "c")
(("1"
(assert)
(("1"
(replace -1 * rl)
(("1"
(hide -1)
(("1"
(replace -1 * rl)
(("1"
(hide -1)
(("1"
(replace -1 * rl)
(("1"
(hide -1)
(("1"
(assert)
(("1"
(rewrite
"dot_scal_left")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (hide-all-but 1) (("2" (grind) nil nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (replace -1) (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil nil))
(angle_exists 0
(angle_exists-1 nil 3254160430
("" (skosimp*)
(("" (assert)
(("" (case "norm(va!1)*norm(vb!1) = 0")
(("1" (assert)
(("1" (inst + "0")
(("1" (rewrite "cos_0")
(("1" (mult-cases -1)
(("1" (lemma "norm_eq_0")
(("1" (inst?)
(("1" (assert)
(("1" (replace -1)
(("1" (hide -1)
(("1" (replace -1)
(("1" (hide -1) (("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "norm_eq_0")
(("2" (inst?)
(("2" (assert)
(("2" (replace -1)
(("2" (hide -1)
(("2" (replace -1)
(("2" (hide -1)
(("2"
(assert)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "dot_norm")
(("2" (inst?)
(("2" (flatten)
(("2"
(case " -1 <= va!1 * vb!1 / (norm(va!1) * norm(vb!1)) AND
va!1 * vb!1 / (norm(va!1) * norm(vb!1)) <= 1")
(("1" (flatten)
(("1" (hide -3 -4)
(("1"
(inst +
"arccos(va!1 * vb!1/( norm(va!1) * norm(vb!1))) ")
(("1" (rewrite "cos_arccos")
(("1" (cross-mult 2) nil nil)) nil)
("2" (ground) nil nil) ("3" (assert) nil nil))
nil))
nil))
nil)
("2" (prop)
(("1" (cross-mult 1) (("1" (assert) nil nil)) nil)
("2" (cross-mult 1) (("2" (assert) nil nil)) nil))
nil)
("3" (assert) nil nil) ("4" (assert) 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)
(dot_norm formula-decl nil vectors_3D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(div_mult_pos_le2 formula-decl nil real_props nil)
(div_mult_pos_le1 formula-decl nil real_props nil)
(va!1 skolem-const-decl "Vect3" vectors_3D_cos nil)
(vb!1 skolem-const-decl "Vect3" vectors_3D_cos 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/")
(nonzero_real nonempty-type-eq-decl nil reals nil)
(times_div2 formula-decl nil real_props nil)
(cos_arccos formula-decl nil trig_inverses "trig/")
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(cos_0 formula-decl nil trig_basic "trig/")
(dot_zero_right formula-decl nil vectors_3D nil)
(norm_eq_0 formula-decl nil vectors_3D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(zero const-decl "Vector" vectors_3D nil)
(sqv const-decl "nnreal" vectors_3D nil)
(* const-decl "real" vectors_3D nil)
(zero_times3 formula-decl nil real_props nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_3D 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)
(norm const-decl "nnreal" vectors_3D nil)
(Vect3 type-eq-decl nil vectors_3D_def nil))
nil))
(angle_between_TCC1 0
(angle_between_TCC1-2 nil 3430841585
("" (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_3D 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_3D 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_3D nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(norm const-decl "nnreal" vectors_3D 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_vect3 type-eq-decl nil vectors_3D nil)
(zero const-decl "Vector" vectors_3D nil)
(/= const-decl "boolean" notequal nil)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_3D nil)
(real nonempty-type-from-decl nil reals nil)
(minus_real_is_real application-judgement "real" reals nil))
nil)
(angle_between_TCC1-1 nil 3254160430
("" (skosimp*) (("" (mult-cases -1) nil nil)) nil)
((Vector type-eq-decl nil vectors_3D nil)
(norm const-decl "nnreal" vectors_3D nil)
(Nz_vect3 type-eq-decl nil vectors_3D nil))
nil))
(cosines_law_bnd 0
(cosines_law_bnd-2 nil 3254160561
("" (skosimp*)
(("" (skoletin 1)
(("" (skoletin 1)
(("" (skoletin 1)
(("" (flatten)
(("" (lemma "cosines_law")
(("" (inst?)
(("" (assert)
(("" (lemma "angle_exists")
(("" (inst?)
(("" (skosimp*)
(("" (assert)
(("" (inst - "ab!1")
(("" (assert)
((""
(replace -3 * rl)
((""
(hide -3)
((""
(replace -4 * rl)
((""
(hide -4)
((""
(replace -4 * rl)
((""
(hide -4)
((""
(typepred "cos(ab!1)")
((""
(mult-by -2 "2*a*b")
((""
(expand "sq")
(("" (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)
((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)
(Vector type-eq-decl nil vectors_3D 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)
(norm const-decl "nnreal" vectors_3D nil)
(Vect3 type-eq-decl nil vectors_3D_def 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)
(- const-decl "Vector" vectors_3D nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(cosines_law formula-decl nil vectors_3D_cos 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/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(cos const-decl "real" trig_basic "trig/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(angle_exists formula-decl nil vectors_3D_cos nil))
nil)
(cosines_law_bnd-1 nil 3254160430
("" (skosimp*)
(("" (skoletin 1)
(("" (flatten)
(("" (lemma "cosines_law")
(("" (inst?)
(("" (assert)
(("" (lemma "angle_exists")
(("" (inst?)
(("" (skosimp*)
(("" (assert)
(("" (inst - "ab!1")
(("" (assert)
(("" (reveal "a" "b" "c")
(("" (replace -1 * rl)
((""
(hide -1)
((""
(replace -1 * rl)
((""
(hide -1)
((""
(replace -1 * rl)
((""
(hide -1)
((""
(typepred "cos(ab!1)")
((""
(mult-by -2 "2*a*b")
((""
(expand "sq")
(("" (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))
(cosines_law_ge 0
(cosines_law_ge-1 nil 3254160430
("" (skosimp*)
(("" (assert)
(("" (flatten)
(("" (lemma "cosines_law_bnd")
(("" (inst?)
(("" (assert)
(("" (assert)
(("" (expand "abs")
(("" (lift-if)
(("" (ground)
(("1" (lemma "sq_ge")
(("1" (inst?)
(("1" (inst -1 "-(norm(va!1)- norm(vb!1))")
(("1" (assert)
(("1" (rewrite "sq_neg") nil nil)) nil))
nil))
nil))
nil)
("2" (lemma "sq_ge")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(cosines_law_bnd formula-decl nil vectors_3D_cos nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_real_is_real application-judgement "real" reals 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_3D nil)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_3D nil)
(sq_neg formula-decl nil sq "reals/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sq_ge formula-decl nil sq "reals/")
(real nonempty-type-from-decl nil reals nil)
(Vect3 type-eq-decl nil vectors_3D_def nil))
nil))
(cosines_law_le 0
(cosines_law_le-1 nil 3254160430
("" (skosimp*)
(("" (assert)
(("" (flatten)
(("" (replace -1) (("" (rewrite "norm_sub_le") nil nil)) nil))
nil))
nil))
nil)
((nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(norm_sub_le formula-decl nil vectors_3D nil))
nil)))
¤ Dauer der Verarbeitung: 0.9 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.
|
