|
(vectors_cos
(cosines_law 0
(cosines_law-1 nil 3254159790
("" (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[n]")
(("2" (rewrite "dot_sub_left[n]")
(("2" (rewrite "dot_sub_left[n]")
(("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)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(n formal-const-decl "posnat" vectors_cos nil)
(Index type-eq-decl nil vectors nil)
(Vector type-eq-decl nil vectors nil)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors 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 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 "real" vectors 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 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 nil)
(dot_sq_norm formula-decl nil vectors nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(dot_scal_left formula-decl nil vectors nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(dot_sub_left formula-decl nil vectors nil)
(dot_comm formula-decl nil vectors nil)
(dot_sub_right formula-decl nil vectors nil))
nil))
(angle_exists 0
(angle_exists-1 nil 3254159790
("" (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[n]")
(("1" (inst?)
(("1" (assert)
(("1" (replace -1)
(("1" (hide -1)
(("1" (replace -1)
(("1" (hide -1)
(("1"
(rewrite "dot_zero_left")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "norm_eq_0[n]")
(("2" (inst?)
(("2" (assert)
(("2" (replace -1)
(("2" (hide -1)
(("2" (replace -1)
(("2" (hide -1) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "dot_norm[n]")
(("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))
nil))
nil))
nil)
("2" (assert)
(("2" (prop)
(("1" (cross-mult 1) (("1" (assert) nil nil)) nil)
("2" (cross-mult 1) (("2" (assert) nil 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 nil)
(div_mult_pos_le1 formula-decl nil real_props nil)
(div_mult_pos_le2 formula-decl nil real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(va!1 skolem-const-decl "Vector[n]" vectors_cos nil)
(vb!1 skolem-const-decl "Vector[n]" vectors_cos nil)
(real_abs_le1 nonempty-type-eq-decl nil asin "trig/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(pi_lb const-decl "posreal" trig_basic "trig/")
(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 "real" vectors 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 nil)
(norm_eq_0 formula-decl nil vectors nil)
(dot_zero_left formula-decl nil vectors 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)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(n formal-const-decl "posnat" vectors_cos nil)
(Index type-eq-decl nil vectors nil)
(Vector type-eq-decl nil vectors nil)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors nil))
nil))
(angle_between_TCC1 0
(angle_between_TCC1-2 nil 3430837199
("" (skosimp*)
(("" (lemma "dot_norm[n]")
(("" (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)
((n formal-const-decl "posnat" vectors_cos nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(dot_norm formula-decl nil vectors 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 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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(* const-decl "real" vectors nil)
(Nz_vector type-eq-decl nil vectors nil)
(zero const-decl "Vector" vectors nil)
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors nil)
(Index type-eq-decl nil vectors nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(minus_real_is_real application-judgement "real" reals nil))
nil)
(angle_between_TCC1-1 nil 3254159790
("" (skosimp*) (("" (mult-cases -1) nil nil)) nil)
((Index type-eq-decl nil vectors nil)
(Vector type-eq-decl nil vectors nil)
(norm const-decl "nnreal" vectors nil)
(Nz_vector type-eq-decl nil vectors nil))
nil))
(cosines_law_bnd 0
(cosines_law_bnd-1 nil 3254159790
("" (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)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(n formal-const-decl "posnat" vectors_cos nil)
(Index type-eq-decl nil vectors nil)
(Vector type-eq-decl nil vectors nil)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors 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 "real" vectors 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_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_cos nil))
nil))
(cosines_law_ge 0
(cosines_law_ge-1 nil 3254159790
("" (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_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)
(norm const-decl "nnreal" vectors nil)
(nnreal type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types 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/")
(Vector type-eq-decl nil vectors nil)
(Index type-eq-decl nil vectors nil)
(n formal-const-decl "posnat" vectors_cos nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil))
(cosines_law_le 0
(cosines_law_le-1 nil 3254159790
("" (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)
(n formal-const-decl "posnat" vectors_cos nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(Vector type-eq-decl nil vectors nil)
(Index type-eq-decl nil vectors nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(norm_sub_le formula-decl nil vectors nil))
nil)))
¤ Dauer der Verarbeitung: 0.26 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.
|
