|
(angles_2D
(v_from_k_1 0
(v_from_k_1-1 nil 3408798342 ("" (grind) nil nil)
((v_from const-decl "Vect2" angles_2D nil)
(v_from const-decl "Vect2" angles_2D nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/"))
shostak))
(norm_v_from 0
(norm_v_from-1 nil 3408798349
("" (skosimp*)
(("" (expand "v_from")
(("" (expand "norm")
(("" (expand "sqv")
(("" (expand "*")
(("" (rewrite "sq_rew")
(("" (rewrite "sq_rew")
((""
(case-replace
"sq(cos(a!1)) * k!1 * k!1 + sq(sin(a!1)) * k!1 * k!1 = sq(k!1)")
(("1" (rewrite "sqrt_sq") nil nil)
("2" (hide 2)
(("2" (factor 1)
(("2" (lemma "sin2_cos2")
(("2" (inst?)
(("2" (replace -1)
(("2" (hide -1)
(("2"
(expand "sq")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((v_from const-decl "Vect2" angles_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(sq_rew formula-decl nil sq "reals/")
(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)
(real nonempty-type-from-decl nil reals nil)
(cos const-decl "real" trig_basic "trig/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sqrt_sq formula-decl nil sqrt "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sin2_cos2 formula-decl nil trig_basic "trig/")
(sin const-decl "real" trig_basic "trig/")
(* const-decl "real" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(norm const-decl "nnreal" vectors_2D nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/"))
shostak))
(angle_exists_x 0
(angle_exists_x-1 nil 3408886152
("" (skeep)
(("" (copy 1)
(("" (case "u`x = 0")
(("1" (case "u`y >= 0")
(("1" (inst + "pi/2")
(("1" (hide 2)
(("1" (rewrite "cos_pi2")
(("1" (rewrite "sin_pi2") (("1" (grind) nil nil)) nil))
nil))
nil))
nil)
("2" (inst + "3*pi/2")
(("2" (hide 3)
(("2" (rewrite "sin_3pi2")
(("2" (rewrite "cos_3pi2")
(("2" (grind)
(("2" (rewrite "sq_rew")
(("2" (rewrite "sqrt_sq_abs")
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst + "arctan(u`y/u`x)")
(("1" (inst + "arctan(u`y/u`x)+pi")
(("1" (name "A" "arctan(u`y / u`x)")
(("1" (replace -1)
(("1" (case "cos(A) = 0")
(("1" (typepred "arctan(u`y / u`x)")
(("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`y/u`x")
(("1" (hide -2)
(("1" (lemma "trig_prop")
(("1" (expand "tan")
(("1" (inst?)
(("1" (assert)
(("1"
(replace -2)
(("1"
(split -1)
(("1"
(assert)
(("1"
(flatten)
(("1" (assert) nil nil))
nil))
nil)
("2"
(flatten)
(("2"
(hide 3)
(("2"
(lemma "neg_cos")
(("2"
(inst?)
(("2"
(lemma "neg_sin")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "arctan(u`y / u`x)")
(("2" (assert) nil nil)) nil)
("3" (assert)
(("3" (expand "Tan?") (("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
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" angles_2D 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)
(neg_sin formula-decl nil trig_basic "trig/")
(neg_cos formula-decl nil trig_basic "trig/")
(trig_prop formula-decl nil angles_2D_scaf nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields 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)
(sin_pi2 formula-decl nil trig_basic "trig/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types 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/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(* 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)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
(cos_pi2 formula-decl nil trig_basic "trig/")
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(pi_ub const-decl "posreal" trig_basic "trig/")
(< const-decl "bool" reals nil)
(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)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_3pi2 formula-decl nil trig_basic "trig/")
(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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sin_3pi2 formula-decl nil trig_basic "trig/")
(* const-decl "[numfield, numfield -> numfield]" number_fields 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_2D nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil))
nil))
(norm_vec_from 0
(norm_vec_from-1 nil 3408981811
("" (skosimp*)
(("" (expand "vec_from") (("" (rewrite "norm_v_from") nil nil))
nil))
nil)
((norm_v_from formula-decl nil angles_2D 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)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> 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/")
(pi_ub const-decl "posreal" trig_basic "trig/")
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(Angle nonempty-type-eq-decl nil angles_2D nil))
shostak))
(vec_from_inj 0
(vec_from_inj-1 nil 3408983003
("" (expand "v_from")
(("" (expand "injective?")
(("" (skeep)
(("" (lemma "sin_cos_angle")
(("" (inst - "x1`1" "x2`1" "x1`2" "x2`2")
(("" (assert)
(("" (flatten) (("" (decompose-equality 1) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cos_range application-judgement "trig_range" trig_basic "trig/")
(sin_range application-judgement "trig_range" trig_basic "trig/")
(injective? const-decl "bool" functions nil)
(sin_cos_angle formula-decl nil angles_2D_scaf nil)
(real_times_real_is_real application-judgement "real" reals nil)
(Angle nonempty-type-eq-decl nil angles_2D nil)
(nnreal_lt_2pi nonempty-type-eq-decl nil atan2 "trig/")
(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, numfield -> numfield]" 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)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(v_from const-decl "Vect2" angles_2D nil))
shostak))
(angle_exists 0
(angle_exists-1 nil 3408886194
("" (skeep)
(("" (copy 1)
(("" (case "u`x = 0")
(("1" (case "u`y >= 0")
(("1" (inst + "pi/2")
(("1" (hide 2)
(("1" (rewrite "cos_pi2")
(("1" (rewrite "sin_pi2") (("1" (grind) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (inst + "3*pi/2")
(("1" (hide 3)
(("1" (rewrite "sin_3pi2")
(("1" (rewrite "cos_3pi2")
(("1" (grind)
(("1" (rewrite "sq_rew")
(("1" (rewrite "sqrt_sq_abs")
(("1" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (name "A" "arctan(u`y / u`x)")
(("1" (case "cos(A) = 0")
(("1" (typepred "arctan(u`y / u`x)")
(("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`y/u`x")
(("1" (hide -2)
(("1" (assert)
(("1" (lemma "trig_prop")
(("1" (expand "tan")
(("1" (inst?)
(("1" (assert)
(("1" (replace -2)
(("1" (split -1)
(("1"
(assert)
(("1"
(flatten)
(("1"
(assert)
(("1"
(mult-by -1 "norm(u)")
(("1"
(mult-by -2 "norm(u)")
(("1"
(assert)
(("1"
(inst 3 "A")
(("1" (assert) nil nil)
("2"
(inst 4 "A+2*pi")
(("1"
(lemma "cos_period")
(("1"
(inst?)
(("1"
(assert)
(("1"
(inst -1 "1")
(("1"
(assert)
(("1"
(lemma
"sin_period")
(("1"
(inst?)
(("1"
(inst
-1
"1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(inst + "A + pi")
(("2"
(lemma "neg_cos")
(("2"
(inst?)
(("2"
(lemma "neg_sin")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "arctan(u`y / u`x)")
(("2" (assert) nil nil)) nil)
("3" (assert)
(("3" (expand "Tan?") (("3" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
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)
(sin const-decl "real" trig_basic "trig/")
(div_cancel2 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(integer nonempty-type-from-decl nil integers 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/")
(A skolem-const-decl
"{x_1: real_abs_lt_pi2 | u`y / u`x = tan(x_1)}" angles_2D nil)
(u skolem-const-decl "Nz_vect2" angles_2D nil)
(neg_sin formula-decl nil trig_basic "trig/")
(neg_cos formula-decl nil trig_basic "trig/")
(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/")
(>= 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)
(sin_pi2 formula-decl nil trig_basic "trig/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types 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/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(* 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)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
(cos_pi2 formula-decl nil trig_basic "trig/")
(Angle nonempty-type-eq-decl nil angles_2D nil)
(nnreal type-eq-decl nil real_types nil)
(< const-decl "bool" reals 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/")
(pi_ub const-decl "posreal" trig_basic "trig/")
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(posreal_div_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_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_3pi2 formula-decl nil trig_basic "trig/")
(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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sin_3pi2 formula-decl nil trig_basic "trig/")
(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_2D nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil))
nil))
(angle_TCC1 0
(angle_TCC1-3 nil 3430818182
("" (skeep :preds? t)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member")
(("" (lemma "angle_exists")
(("" (inst?)
(("" (skeep -1)
(("" (inst -3 "alpha")
(("" (expand "v_from")
(("" (decompose-equality 2) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(number nonempty-type-decl nil numbers 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)
(< const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> 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/")
(pi_ub const-decl "posreal" trig_basic "trig/")
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(Angle nonempty-type-eq-decl nil angles_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(cos const-decl "real" trig_basic "trig/")
(sin const-decl "real" trig_basic "trig/")
(real_times_real_is_real application-judgement "real" reals nil)
(v_from const-decl "Vect2" angles_2D nil)
(angle_exists formula-decl nil angles_2D nil)
(empty? const-decl "bool" sets nil))
nil)
(angle_TCC1-2 nil 3408874847
("" (skosimp*)
(("" (typepred "u!1") (("" (flatten) (("" (assert) nil nil)) 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)
(angle_TCC1-1 nil 3408732987
("" (skosimp*)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member")
(("" (lemma "trig_prop3")
(("" (inst?)
(("" (skosimp*)
(("" (inst - "A!1")
(("" (apply-extensionality 1 :hide? t)
(("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Vector type-eq-decl nil vectors_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(Vect2 type-eq-decl nil vectors_2D_def nil))
nil))
(vec_from_angle 0
(vec_from_angle-1 nil 3430821363
("" (skosimp*)
(("" (typepred "angle(u!1)") (("" (assert) nil nil)) nil)) nil)
((angle const-decl "{alpha: Angle | u = v_from(alpha, norm(u))}"
angles_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(v_from const-decl "Vect2" angles_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Angle nonempty-type-eq-decl nil angles_2D 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, numfield -> numfield]" 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)
(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)
(>= const-decl "bool" reals 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)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil))
nil))
(angle_vec_from_TCC1 0
(angle_vec_from_TCC1-1 nil 3430821261
("" (skeep :preds? t)
(("" (lemma "norm_eq_0")
(("" (inst?)
(("" (assert)
(("" (rewrite "norm_vec_from") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((norm_eq_0 formula-decl nil vectors_2D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(norm_vec_from formula-decl nil angles_2D nil)
(Angle nonempty-type-eq-decl nil angles_2D 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)
(* const-decl "[numfield, numfield -> numfield]" 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)
(v_from const-decl "Vect2" angles_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil))
nil))
(angle_vec_from 0
(angle_vec_from-1 nil 3430821261
("" (skeep)
(("" (typepred "angle(v_from(alpha,k))")
(("" (rewrite "norm_vec_from")
(("" (lemma "vec_from_inj")
(("" (expand "injective?")
(("" (inst -1 "(alpha,k)" "(angle(v_from(alpha, k)),k)")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((angle const-decl "{alpha: Angle | u = v_from(alpha, norm(u))}"
angles_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(v_from const-decl "Vect2" angles_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Angle nonempty-type-eq-decl nil angles_2D 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, numfield -> numfield]" 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)
(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)
(>= const-decl "bool" reals 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)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(vec_from_inj formula-decl nil angles_2D nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(injective? const-decl "bool" functions nil)
(norm_vec_from formula-decl nil angles_2D nil))
nil))
(Angle_TCC1 0
(Angle_TCC1-1 nil 3414420480
("" (skeep :preds? t) (("" (decompose-equality 1) nil nil)) nil)
((Vector type-eq-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(comp_zero_x formula-decl nil vectors_2D nil)
(comp_zero_y formula-decl nil vectors_2D 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))
nil))
(angle_Angle 0
(angle_Angle-1 nil 3414423401
("" (skeep)
(("" (expand "angle")
(("" (expand "Angle")
((""
(name-replace "beta"
"choose({a: Angle | u = vec_from(a, norm(u))})")
(("1" (typepred "beta")
(("1" (expand "v_from")
(("1" (replace -3)
(("1" (assert)
(("1" (lemma "atan2_cancel_pos")
(("1" (inst - "norm(u)" "cos(beta)" " sin(beta)")
(("1" (assert)
(("1" (split -1)
(("1" (replace -1)
(("1" (rewrite "atan2_cos_sin") nil nil))
nil)
("2" (flatten)
(("2" (lemma "sin_eq_0")
(("2"
(inst?)
(("2"
(assert)
(("2"
(lemma "cos_eq_0")
(("2"
(inst?)
(("2"
(assert)
(("2"
(skeep -1)
(("2"
(skolem -2 "j")
(("2"
(replaces -1)
(("2"
(hide-all-but -1)
(("2"
(cancel-by -1 "pi")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "angle_exists")
(("2" (inst?)
(("2" (skeep -1)
(("2" (expand "nonempty?")
(("2" (expand "empty?")
(("2" (expand "member")
(("2" (expand "v_from")
(("2" (inst?)
(("2" (decompose-equality 1) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((angle const-decl "{alpha: Angle | u = v_from(alpha, norm(u))}"
angles_2D nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> 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/")
(pi_ub const-decl "posreal" trig_basic "trig/")
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(Angle nonempty-type-eq-decl nil angles_2D nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(choose const-decl "(p)" sets nil)
(Vector type-eq-decl nil vectors_2D nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(v_from const-decl "Vect2" angles_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(nil application-judgement "nnreal_lt_2pi" atan2 "trig/")
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(real_times_real_is_real application-judgement "real" reals nil)
(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)
(sin const-decl "real" trig_basic "trig/")
(cos const-decl "real" trig_basic "trig/")
(atan2_cos_sin formula-decl nil atan2 "trig/")
(sin_eq_0 formula-decl nil trig_basic "trig/")
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions 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)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(both_sides_times1_imp formula-decl nil extra_real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_eq_0 formula-decl nil trig_basic "trig/")
(atan2_cancel_pos formula-decl nil atan2 "trig/")
(NOT const-decl "[bool -> bool]" booleans nil)
(angle_exists formula-decl nil angles_2D nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(Angle const-decl "Angle" angles_2D nil))
shostak))
(vec_from_Angle 0
(vec_from_Angle-1 nil 3430821413
("" (skosimp*)
(("" (lemma "angle_Angle")
(("" (inst?)
(("" (replace -1 * rl)
(("" (rewrite "vec_from_angle") nil nil)) nil))
nil))
nil))
nil)
((angle_Angle formula-decl nil angles_2D nil)
(vec_from_angle formula-decl nil angles_2D 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))
nil))
(angle_x0_TCC1 0
(angle_x0_TCC1-1 nil 3414486625
("" (skeep)
(("" (decompose-equality -1) (("" (assert) nil nil)) nil)) nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers 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)
(>= 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)
(Vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(comp_zero_x formula-decl nil vectors_2D nil))
nil))
(angle_x0 0
(angle_x0-1 nil 3414486628
("" (skeep)
(("" (rewrite "angle_Angle")
(("" (expand "Angle")
(("" (expand "atan2") (("" (rewrite "atan_0") nil nil)) nil))
nil))
nil))
nil)
((angle_Angle formula-decl nil angles_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(number nonempty-type-decl nil numbers 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)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(atan2 const-decl "real" atan2 "trig/")
(atan_0 formula-decl nil atan "trig/")
(Angle const-decl "Angle" angles_2D nil))
shostak))
(angle_0x_TCC1 0
(angle_0x_TCC1-1 nil 3414486489
("" (skeep)
(("" (decompose-equality -1) (("" (assert) nil nil)) nil)) nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers 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)
(>= 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)
(Vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(comp_zero_y formula-decl nil vectors_2D nil)
(comp_zero_x formula-decl nil vectors_2D nil))
nil))
(angle_0x 0
(angle_0x-1 nil 3414486495
("" (skeep)
(("" (rewrite "angle_Angle")
(("" (expand "Angle")
(("" (expand "atan2") (("" (postpone) nil nil)) nil)) nil))
nil))
nil)
((angle_Angle formula-decl nil angles_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(number nonempty-type-decl nil numbers 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)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(atan2 const-decl "real" atan2 "trig/")
(Angle const-decl "Angle" angles_2D nil))
shostak))
(angle_xx_TCC1 0
(angle_xx_TCC1-3 nil 3431180811
("" (skeep)
(("" (decompose-equality -1) (("" (assert) nil nil)) nil)) nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers 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)
(>= 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)
(Vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(comp_zero_x formula-decl nil vectors_2D nil))
nil)
(angle_xx_TCC1-2 nil 3431180799
(";;; Proof angle_0x_TCC1-1 for formula angles_2D.angle_0x_TCC1"
(skeep)
((";;; Proof angle_0x_TCC1-1 for formula angles_2D.angle_0x_TCC1"
(rewrite "nzv_xy_neq_0") nil))
";;; developed with shostak decision procedures")
nil nil)
(angle_xx_TCC1-1 nil 3414486827
("" (skeep) (("" (rewrite "nzv_xy_neq_0") nil nil)) nil)
((nzv_xy_neq_0 formula-decl nil vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil))
nil))
(angle_xx 0
(angle_xx-1 nil 3414486832
("" (skeep)
(("" (rewrite "angle_Angle")
(("" (expand "Angle")
(("" (expand "atan2")
(("" (assert)
(("" (lemma "atan_tan")
(("" (inst - "pi/4")
(("" (rewrite "tan_pi4") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((angle_Angle formula-decl nil angles_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(number nonempty-type-decl nil numbers 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)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(atan2 const-decl "real" atan2 "trig/")
(atan_tan formula-decl nil trig_inverses "trig/")
(tan_pi4 formula-decl nil trig_values "trig/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(< const-decl "bool" reals 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)
(- const-decl "[numfield -> numfield]" number_fields 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/")
(real_abs_lt_pi2 nonempty-type-eq-decl nil atan "trig/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(Angle const-decl "Angle" angles_2D nil))
shostak))
(angle_n0_TCC1 0
(angle_n0_TCC1-2 nil 3431180821
("" (skeep)
(("" (decompose-equality -1) (("" (assert) nil nil)) nil)) nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers 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)
(<= const-decl "bool" reals nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(comp_zero_x formula-decl nil vectors_2D nil))
nil)
(angle_n0_TCC1-1 nil 3414487843
("" (skeep) (("" (rewrite "nzv_xy_neq_0") nil nil)) nil)
((nzv_xy_neq_0 formula-decl nil vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil))
nil))
(angle_n0 0
(angle_n0-1 nil 3414487848
("" (skeep)
(("" (rewrite "angle_Angle")
(("" (expand "Angle")
(("" (expand "atan2") (("" (rewrite "atan_0") nil nil)) nil))
nil))
nil))
nil)
((angle_Angle formula-decl nil angles_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(number nonempty-type-decl nil numbers 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)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(atan2 const-decl "real" atan2 "trig/")
(atan_0 formula-decl nil atan "trig/")
(Angle const-decl "Angle" angles_2D nil))
shostak))
(angle_0n_TCC1 0
(angle_0n_TCC1-2 nil 3431180834
("" (skeep)
(("" (decompose-equality -1) (("" (assert) nil nil)) nil)) nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers 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)
(<= const-decl "bool" reals nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(comp_zero_y formula-decl nil vectors_2D nil)
(comp_zero_x formula-decl nil vectors_2D nil))
nil)
(angle_0n_TCC1-1 nil 3414487843
("" (skeep) (("" (rewrite "nzv_xy_neq_0") nil nil)) nil)
((nzv_xy_neq_0 formula-decl nil vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil))
nil))
(angle_0n 0
(angle_0n-1 nil 3414487912
("" (skeep)
(("" (rewrite "angle_Angle")
(("" (expand "Angle")
(("" (expand "atan2") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((angle_Angle formula-decl nil angles_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D nil)
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(number nonempty-type-decl nil numbers 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)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(atan2 const-decl "real" atan2 "trig/")
(Angle const-decl "Angle" angles_2D nil))
nil))
(angle_nx_TCC1 0
(angle_nx_TCC1-2 nil 3431180840
("" (skeep)
(("" (decompose-equality -1) (("" (assert) nil nil)) nil)) nil)
((minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers 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]" 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)
(>= 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)
(Vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(comp_zero_x formula-decl nil vectors_2D nil))
nil)
(angle_nx_TCC1-1 nil 3414488036
("" (skeep) (("" (rewrite "nzv_xy_neq_0") nil nil)) nil)
((nzv_xy_neq_0 formula-decl nil vectors_2D nil)
(Vector type-eq-decl nil vectors_2D nil))
nil))
(angle_nx 0
(angle_nx-1 nil 3414488044
("" (skeep)
(("" (rewrite "angle_Angle")
(("" (expand "Angle")
(("" (expand "atan2")
(("" (lemma "atan_neg")
(("" (inst - "1")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.198 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.
|
