|
(trackAngles_scaf
(track_exists_x 0
(track_exists_x-1 nil 3408886152
("" (skeep)
(("" (case "u`y = 0")
(("1" (case "u`x >= 0")
(("1" (inst + "pi/2")
(("1" (rewrite "sin_pi2")
(("1" (rewrite "cos_pi2")
(("1" (assert) (("1" (grind) nil nil)) nil)) nil))
nil))
nil)
("2" (inst + "3*pi/2")
(("2" (rewrite "cos_3pi2")
(("2" (rewrite "sin_3pi2")
(("2" (grind)
(("2" (rewrite "sq_rew")
(("2" (rewrite "sqrt_sq_abs") (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (copy 2)
(("2" (inst + "arctan(u`x/u`y)")
(("1" (inst + "arctan(u`x/u`y)+pi")
(("1" (name "A" "arctan(u`x / u`y)")
(("1" (replace -1)
(("1" (case "cos(A) = 0")
(("1" (typepred "arctan(u`x / u`y)")
(("1" (replace -5)
(("1" (lemma "cos_eq_0 ")
(("1" (inst?)
(("1" (assert)
(("1" (skosimp*)
(("1"
(hide -4 -5 -6 1 2)
(("1"
(cross-mult -2)
(("1"
(cross-mult -3)
(("1"
(mult-by -1 "2")
(("1"
(assert)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(case-replace
"-1 < 1 + 2 * (i!1)")
(("1"
(hide -2)
(("1"
(case
"1 + 2 * (i!1) < 1")
(("1"
(hide -3)
(("1"
(assert)
nil
nil))
nil)
("2"
(mult-by 1 "pi")
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(mult-by 1 "pi")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case-replace "tan(A) = u`x/u`y")
(("1" (hide -2)
(("1" (lemma "trig_prop")
(("1" (expand "tan")
(("1" (inst - "A" "(u`y,u`x)")
(("1" (assert)
(("1"
(replace -2)
(("1"
(case-replace
"norm((# x := u`y, y := u`x #)) = norm(u)"
"")
(("1"
(assert)
(("1"
(split -1)
(("1"
(flatten)
(("1" (assert) nil nil))
nil)
("2"
(flatten)
(("2"
(hide 3)
(("2"
(lemma "neg_sin")
(("2"
(inst?)
(("2"
(lemma "neg_cos")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(rewrite "norms_eq_sqv")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2"
(assert)
(("2"
(lemma "comps_eq")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "arctan(u`x / u`y)")
(("2" (assert) nil nil)) nil)
("3" (expand "Tan?") (("3" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
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)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sin_3pi2 formula-decl nil trig_basic "trig/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sq_rew formula-decl nil sq "reals/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sqrt_sq_abs formula-decl nil sqrt "reals/")
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(cos_3pi2 formula-decl nil trig_basic "trig/")
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields 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)
(AND const-decl "[bool, bool -> bool]" booleans 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/")
(cos_pi2 formula-decl nil trig_basic "trig/")
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(sqrt_square formula-decl nil sqrt "reals/")
(mult_divides1 application-judgement "(divides(n))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(sin_range application-judgement "trig_range" trig_basic "trig/")
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
(sin_pi2 formula-decl nil trig_basic "trig/")
(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)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(u skolem-const-decl "Nz_vect2" trackAngles_scaf nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(real_abs_lt_pi2 nonempty-type-eq-decl nil atan "trig/")
(Tan? const-decl "bool" trig_basic "trig/")
(tan const-decl "real" trig_basic "trig/")
(arctan const-decl "{x: real_abs_lt_pi2 | y = tan(x)}"
trig_inverses "trig/")
(cos const-decl "real" trig_basic "trig/")
(div_mult_pos_lt1 formula-decl nil real_props nil)
(both_sides_times1_imp formula-decl nil extra_real_props 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)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
nil)
(div_mult_pos_lt2 formula-decl nil real_props nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(cos_eq_0 formula-decl nil trig_basic "trig/")
(NOT const-decl "[bool -> bool]" booleans nil)
(comps_eq formula-decl nil vectors_2D nil)
(comp_zero_x formula-decl nil vectors_2D nil)
(comp_zero_y formula-decl nil vectors_2D nil)
(nnreal type-eq-decl nil real_types nil)
(neg_cos formula-decl nil trig_basic "trig/")
(neg_sin formula-decl nil trig_basic "trig/")
(norms_eq_sqv formula-decl nil vectors_2D nil)
(trig_prop formula-decl nil angles_2D_scaf nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields
nil))
nil))
(track_exists 0
(track_exists-1 nil 3408886194
("" (skeep)
(("" (case "u`y = 0")
(("1" (case "u`x >= 0")
(("1" (inst + "pi/2")
(("1" (rewrite "sin_pi2")
(("1" (rewrite "cos_pi2") (("1" (grind) nil nil)) nil))
nil)
("2" (assert) nil nil))
nil)
("2" (inst + "3*pi/2")
(("1" (rewrite "cos_3pi2")
(("1" (rewrite "sin_3pi2")
(("1" (grind)
(("1" (rewrite "sq_rew")
(("1" (rewrite "sqrt_sq_abs") (("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (copy 2)
(("2" (name "A" "arctan(u`x / u`y)")
(("1" (case "cos(A) = 0")
(("1" (typepred "arctan(u`x / u`y)")
(("1" (replace -5)
(("1" (lemma "cos_eq_0 ")
(("1" (inst?)
(("1" (assert)
(("1" (skosimp*)
(("1" (hide -4 -5 -6 1 2)
(("1" (cross-mult -2)
(("1" (cross-mult -3)
(("1"
(mult-by -1 "2")
(("1"
(assert)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(case-replace
"-1 < 1 + 2 * (i!1)")
(("1"
(hide -2)
(("1"
(case "1 + 2 * (i!1) < 1")
(("1"
(hide -3)
(("1" (assert) nil nil))
nil)
("2"
(mult-by 1 "pi")
(("2" (assert) nil nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(mult-by 1 "pi")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case-replace "tan(A) = u`x/u`y")
(("1" (hide -2)
(("1" (assert)
(("1" (lemma "trig_prop")
(("1" (expand "tan")
(("1" (inst - "A" "(u`y,u`x)")
(("1" (assert)
(("1"
(case-replace
"norm((# x := u`y, y := u`x #)) = norm(u)"
"")
(("1" (split -1)
(("1"
(assert)
(("1"
(flatten)
(("1"
(cross-mult -1)
(("1"
(cross-mult -2)
(("1"
(inst + "A")
(("1" (assert) nil nil)
("2"
(assert)
(("2"
(inst + "A + 2*pi")
(("2"
(lemma "sin_period")
(("2"
(inst?)
(("2"
(assert)
(("2"
(inst -1 "1")
(("2"
(assert)
(("2"
(lemma
"cos_period")
(("2"
(inst?)
(("2"
(inst
-1
"1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(inst + "A + pi")
(("2"
(lemma "neg_sin")
(("2"
(inst?)
(("2"
(lemma "neg_cos")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (propax) nil nil))
nil)
("2" (assert)
(("2"
(hide-all-but 1)
(("2"
(rewrite "norms_eq_sqv")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (lemma "comps_eq")
(("2" (inst?) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "arctan(u`x / u`y)")
(("2" (assert) nil nil)) nil)
("3" (expand "Tan?") (("3" (assert) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
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)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sin_3pi2 formula-decl nil trig_basic "trig/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sq_rew formula-decl nil sq "reals/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(minus_real_is_real application-judgement "real" reals nil)
(sqrt_sq_abs formula-decl nil sqrt "reals/")
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(cos_3pi2 formula-decl nil trig_basic "trig/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(pi_ub const-decl "posreal" trig_basic "trig/")
(pi_lb const-decl "posreal" trig_basic "trig/")
(AND const-decl "[bool, bool -> bool]" booleans 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 "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(Track nonempty-type-eq-decl nil trackAngles_scaf nil)
(cos_pi2 formula-decl nil trig_basic "trig/")
(sqrt_square formula-decl nil sqrt "reals/")
(mult_divides1 application-judgement "(divides(n))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(sin_range application-judgement "trig_range" trig_basic "trig/")
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
(sin_pi2 formula-decl nil trig_basic "trig/")
(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)
(arctan const-decl "{x: real_abs_lt_pi2 | y = tan(x)}"
trig_inverses "trig/")
(tan const-decl "real" trig_basic "trig/")
(Tan? const-decl "bool" trig_basic "trig/")
(real_abs_lt_pi2 nonempty-type-eq-decl nil atan "trig/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(comp_zero_y formula-decl nil vectors_2D nil)
(comp_zero_x formula-decl nil vectors_2D nil)
(comps_eq formula-decl nil vectors_2D nil)
(norms_eq_sqv formula-decl nil vectors_2D nil)
(sin_period formula-decl nil trig_basic "trig/")
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(cos_period formula-decl nil trig_basic "trig/")
(integer nonempty-type-from-decl nil integers nil)
(A skolem-const-decl
"{x_1: real_abs_lt_pi2 | u`x / u`y = tan(x_1)}" trackAngles_scaf
nil)
(sin const-decl "real" trig_basic "trig/")
(nonzero_real nonempty-type-eq-decl nil reals nil)
(div_cancel4 formula-decl nil real_props nil)
(neg_cos formula-decl nil trig_basic "trig/")
(neg_sin formula-decl nil trig_basic "trig/")
(u skolem-const-decl "Nz_vect2" trackAngles_scaf nil)
(trig_prop formula-decl nil angles_2D_scaf nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(cos_eq_0 formula-decl nil trig_basic "trig/")
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(div_mult_pos_lt2 formula-decl nil real_props nil)
(both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers 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)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(both_sides_times1_imp formula-decl nil extra_real_props nil)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(cos const-decl "real" trig_basic "trig/"))
nil)))
¤ Dauer der Verarbeitung: 0.37 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.
|
