|
(angles_2D_scaf
(trig_prop2 0
(trig_prop2-1 nil 3408794701
("" (skeep)
(("" (cross-mult -1)
(("" (lemma "sq_eq_abs")
(("" (inst - "sin(a) * u`x" "u`y * cos(a)")
(("" (flatten)
(("" (hide -1)
(("" (split -1)
(("1" (rewrite "sq_times")
(("1" (rewrite "sq_times")
(("1" (copy -1)
(("1" (lemma "sin2")
(("1" (inst?)
(("1" (replace -1 -2)
(("1" (assert)
(("1"
(move-terms -2 l 2)
(("1"
(hide -1)
(("1"
(lemma "cos2")
(("1"
(inst?)
(("1"
(replace -1 -3)
(("1"
(assert)
(("1"
(hide -1)
(("1"
(move-terms -2 r 2)
(("1"
(factor -1)
(("1"
(factor -2)
(("1"
(case-replace
"sq(u`x) + sq(u`y) = sq(norm(u))")
(("1"
(hide -1)
(("1"
(assert)
nil
nil))
nil)
("2"
(hide 4)
(("2"
(lemma
"dot_sq_norm")
(("2"
(inst?)
(("2"
(expand
"*")
(("2"
(expand
"sq")
(("2"
(propax)
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)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_div_nzreal_is_real application-judgement "real" reals nil)
(div_cancel3 formula-decl nil real_props nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(sin const-decl "real" trig_basic "trig/")
(cos const-decl "real" trig_basic "trig/")
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(real_times_real_is_real application-judgement "real" reals nil)
(times_div2 formula-decl nil real_props nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(div_cancel4 formula-decl nil real_props nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_times formula-decl nil sq "reals/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(* const-decl "real" vectors_2D nil)
(dot_sq_norm formula-decl nil vectors_2D nil)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_2D nil)
(cos2 formula-decl nil trig_basic "trig/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq "reals/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sin2 formula-decl nil trig_basic "trig/")
(sq_eq_abs formula-decl nil sq "reals/"))
nil))
(trig_prop 0
(trig_prop-2 nil 3408789322
("" (skeep)
(("" (lemma "trig_prop2")
(("" (inst?)
(("" (assert)
(("" (replace -2)
(("" (flatten)
(("" (real-props -3)
(("" (rewrite "sq_times" :dir rl)
(("" (rewrite "sq_times" :dir rl)
(("" (case "u`x >= 0")
(("1" (lemma "sq_eq")
(("1" (inst - " u`x" " norm(u) * cos(a)")
(("1" (assert)
(("1" (replaces -1)
(("1" (cancel-by -3 "cos(a)") nil nil))
nil))
nil)
("2" (lemma "sq_eq")
(("2" (inst - " u`x" "-norm(u) * cos(a)")
(("1"
(assert)
(("1"
(lemma "sq_neg")
(("1"
(inst - "norm(u) * cos(a)")
(("1"
(assert)
(("1"
(replaces -2)
(("1"
(cancel-by -5 "cos(a)")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (lemma "sq_eq")
(("2" (inst - "-u`x" " norm(u) * cos(a)")
(("1" (rewrite "sq_neg")
(("1" (assert)
(("1"
(neg-formula -1)
(("1"
(replaces -1)
(("1"
(cancel-by -3 "cos(a)")
nil
nil))
nil))
nil))
nil))
nil)
("2" (lemma "sq_eq")
(("2" (inst - "-u`x" "-norm(u) * cos(a)")
(("1"
(assert)
(("1"
(rewrite "sq_neg")
(("1"
(lemma "sq_neg")
(("1"
(inst - "norm(u) * cos(a)")
(("1"
(assert)
(("1"
(neg-formula -2)
(("1"
(replaces -1)
(("1"
(cancel-by -3 "cos(a)")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil)
("3" (assert) nil nil))
nil))
nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((trig_prop2 formula-decl nil angles_2D_scaf nil)
(minus_real_is_real application-judgement "real" reals nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(cos const-decl "real" trig_basic "trig/")
(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)
(sq_times formula-decl nil sq "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(u skolem-const-decl "Nz_vect2" angles_2D_scaf nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(a skolem-const-decl "real" angles_2D_scaf nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(trig_range type-eq-decl nil trig_basic "trig/")
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(both_sides_times1_imp formula-decl nil extra_real_props nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(CBD_14 skolem-const-decl "trig_range" angles_2D_scaf nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(sq_neg formula-decl nil sq "reals/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(neg_one_times formula-decl nil extra_tegies nil)
(CBD_15 skolem-const-decl "trig_range" angles_2D_scaf nil)
(sq_eq formula-decl nil sq "reals/")
(CBD_16 skolem-const-decl "trig_range" angles_2D_scaf nil)
(neg_neg formula-decl nil extra_tegies nil)
(mult_neg formula-decl nil extra_tegies nil)
(neg_mult formula-decl nil extra_tegies nil)
(CBD_17 skolem-const-decl "trig_range" angles_2D_scaf nil)
(sin const-decl "real" trig_basic "trig/")
(real_times_real_is_real application-judgement "real" reals nil)
(cross_mult formula-decl nil real_props 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)
(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)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(sq_nz_pos application-judgement "posreal" sq "reals/"))
nil)
(trig_prop-1 nil 3408734330
("" (skeep)
(("" (cross-mult -1)
(("" (lemma "sq_eq")
(("" (inst?)
(("1" (flatten)
(("1" (hide -1)
(("1" (split -1)
(("1" (hide -2)
(("1" (rewrite "sq_times")
(("1" (rewrite "sq_times")
(("1" (copy -1)
(("1" (lemma "sin2")
(("1" (inst?)
(("1" (replace -1 -2)
(("1"
(assert)
(("1"
(move-terms -2 l 2)
(("1"
(hide -1)
(("1"
(lemma "cos2")
(("1"
(inst?)
(("1"
(replace -1 -3)
(("1"
(assert)
(("1"
(hide -1)
(("1"
(move-terms -2 r 2)
(("1"
(factor -1)
(("1"
(factor -2)
(("1"
(case-replace
"sq(v`y) + sq(v`x) = sq(norm(v))")
(("1"
(hide -1)
(("1"
(rewrite
"sq_times"
:dir
rl)
(("1"
(rewrite
"sq_times"
:dir
rl)
(("1"
(split +)
(("1"
(hide
-1)
(("1"
(postpone)
nil
nil))
nil)
("2"
(hide
-2)
(("2"
(postpone)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -1 -2 2)
(("2"
(expand
"norm")
(("2"
(lemma
"sq_sqrt")
(("2"
(inst?)
(("2"
(split
-1)
(("1"
(replace
-1)
(("1"
(hide
-1)
(("1"
(expand
"sqv")
(("1"
(expand
"*")
(("1"
(expand
"sq")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(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)
("2" (propax) nil nil))
nil))
nil))
nil)
("2" (postpone) nil nil) ("3" (postpone) nil nil))
nil))
nil))
nil))
nil)
nil shostak))
(sin_cos_angle 0
(sin_cos_angle-1 nil 3409051564
("" (skeep)
(("" (case-replace "pa * cos(alpha) = pb * cos(beta)")
(("1" (case-replace "pa * sin(alpha) = pb * sin(beta)")
(("1" (case-replace "pa = pb ")
(("1" (lemma "sin_cos_eq")
(("1" (inst - "alpha" "beta")
(("1" (assert)
(("1" (prop)
(("1" (mult-by 1 "pb") (("1" (assert) nil nil)) nil)
("2" (mult-by 1 "pb") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(case " sq(pa) * sq(cos(alpha)) +
sq(pa) * sq(sin(alpha)) = sq(pb) * sq(cos(beta))
+ sq(pb) * sq(sin(beta))")
(("1" (hide -2 -3)
(("1" (factor -1)
(("1" (lemma "sin2_cos2")
(("1" (inst?)
(("1" (replace -1)
(("1" (hide -1)
(("1" (lemma "sin2_cos2")
(("1" (inst?)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(lemma "sq_eq_abs")
(("1"
(inst - "pa" "pb")
(("1"
(assert)
(("1"
(expand "abs")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "sq_times" :dir rl)
(("2" (rewrite "sq_times" :dir rl)
(("2" (rewrite "sq_times" :dir rl)
(("2" (rewrite "sq_times" :dir rl)
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(cos const-decl "real" trig_basic "trig/")
(nnreal type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans 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_lt_2pi nonempty-type-eq-decl nil atan2 "trig/")
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(both_sides_times1 formula-decl nil real_props nil)
(sin_cos_eq formula-decl nil trig_extra "trig/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sq const-decl "nonneg_real" sq "reals/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_eq_abs formula-decl nil sq "reals/")
(sin2_cos2 formula-decl nil trig_basic "trig/")
(sq_times formula-decl nil sq "reals/")
(sin const-decl "real" trig_basic "trig/"))
shostak)))
¤ Dauer der Verarbeitung: 0.34 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.
|
