|
(trackAngles_2D
(v_from_TCC1 0
(v_from_TCC1-1 nil 3521387835
("" (skeep :preds? t)
(("" (decompose-equality -4)
(("" (assert)
(("" (grind-reals)
(("" (lemma "sin2_cos2")
(("" (inst?)
(("" (replaces (-2 -3)) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals 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 -> 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)
(sin const-decl "real" trig_basic "trig/")
(cos const-decl "real" trig_basic "trig/")
(Vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(sin_range application-judgement "trig_range" trig_basic "trig/")
(nonzero_times1 formula-decl nil real_props nil)
(sq_0 formula-decl nil sq "reals/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sin2_cos2 formula-decl nil trig_basic "trig/")
(comp_zero_y formula-decl nil vectors_2D nil)
(comp_zero_x formula-decl nil vectors_2D nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(trk_TCC1 0
(trk_TCC1-1 nil 3476204880
("" (skosimp*)
(("" (typepred "u!1")
(("" (flatten) (("" (apply-extensionality 1 :hide? t) 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(comp_zero_y formula-decl nil vectors_2D nil)
(comp_zero_x formula-decl nil vectors_2D nil))
nil))
(track_TCC1 0
(track_TCC1-3 nil 3430818182
(""
(inst +
"(LAMBDA (u: Nz_vect2): choose({alpha: Track | u = vec_from(alpha, norm(u))}))")
(("" (skosimp*)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member")
(("" (lemma "track_exists")
(("" (inst?)
(("" (skeep -1)
(("" (inst -3 "alpha")
(("" (apply-extensionality 1 :hide? t)
(("1" (expand "vec_from")
(("1" (propax) nil nil)) nil)
("2" (expand "vec_from")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(track_exists formula-decl nil trackAngles_scaf nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(member const-decl "bool" sets nil)
(choose const-decl "(p)" sets nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(norm const-decl "nnreal" vectors_2D nil)
(vec_from const-decl "Vect2" trackAngles_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Track nonempty-type-eq-decl nil trackAngles_scaf 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)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(Nz_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)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil))
nil)
(track_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)
(track_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)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(sin_range application-judgement "trig_range" trig_basic "trig/")
(Vect2 type-eq-decl nil vectors_2D_def nil))
nil))
(norm_v_from 0
(norm_v_from-1 nil 3476441524
("" (skosimp*)
(("" (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" (expand "sq")
(("2" (lemma "sin2_cos2")
(("2" (inst?)
(("2" (expand "sq") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(norm const-decl "nnreal" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "real" vectors_2D nil)
(sin const-decl "real" trig_basic "trig/")
(real_plus_real_is_real application-judgement "real" reals nil)
(sin2_cos2 formula-decl nil trig_basic "trig/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqrt_sq formula-decl nil sqrt "reals/")
(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)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(cos const-decl "real" trig_basic "trig/")
(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)
(sq_rew formula-decl nil sq "reals/")
(sqv const-decl "nnreal" vectors_2D nil))
nil))
(vec_from_nz 0
(vec_from_nz-1 nil 3476444591
("" (skosimp*)
(("" (expand "vec_from")
(("" (lemma "comps_eq")
(("" (inst?)
(("" (assert)
(("" (flatten)
(("" (hide -3)
(("" (mult-cases -1)
(("" (mult-cases -2)
(("" (lemma "sin_eq_0")
(("" (inst?)
(("" (lemma "cos_eq_0")
(("" (inst?)
(("" (assert)
((""
(skosimp*)
((""
(hide -3 -4)
((""
(replace -1)
((""
(hide -1)
((""
(assert)
((""
(case-replace
"1/ 2 + i!1 = i!2")
(("1" (assert) nil nil)
("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))
nil))
nil))
nil))
nil))
nil)
((vec_from const-decl "Vect2" trackAngles_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_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)
(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)
(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)
(sin 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/")
(Track nonempty-type-eq-decl nil trackAngles_scaf nil)
(cos const-decl "real" trig_basic "trig/")
(zero const-decl "Vector" vectors_2D nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(comps_eq formula-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)
((vec_from const-decl "Vect2" trackAngles_2D nil)
(Track nonempty-type-eq-decl nil trackAngles_scaf 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)
(>= 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)
(norm_v_from formula-decl nil trackAngles_2D nil))
shostak))
(vec_from_inj 0
(vec_from_inj-1 nil 3408983003
("" (expand "vec_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)
((sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_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)
(Track nonempty-type-eq-decl nil trackAngles_scaf 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)
(vec_from const-decl "Vect2" trackAngles_2D nil))
shostak))
(vec_from_track 0
(vec_from_track-1 nil 3430821363
("" (skosimp*)
(("" (typepred "track(u!1)") (("" (assert) nil nil)) nil)) nil)
((track const-decl "{alpha: Track | u = vec_from(alpha, norm(u))}"
trackAngles_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(vec_from const-decl "Vect2" trackAngles_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Track nonempty-type-eq-decl nil trackAngles_scaf 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))
(track_vec_from_TCC1 0
(track_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 trackAngles_2D nil)
(vec_from const-decl "Vect2" trackAngles_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(Track nonempty-type-eq-decl nil trackAngles_scaf 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)
(>= 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))
(track_vec_from 0
(track_vec_from-1 nil 3430821261
("" (skeep)
(("" (auto-rewrite "vec_from")
(("" (typepred "track(v_from(alpha,k))")
(("1" (lemma "norm_vec_from")
(("1" (expand "vec_from")
(("1" (inst?)
(("1" (replace -1)
(("1" (assert)
(("1" (lemma "vec_from_inj")
(("1" (expand "injective?")
(("1"
(inst -1 "(alpha,k)"
"(track(v_from(alpha, k)),k)")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "vec_from")
(("2" (assert)
(("2" (hide +)
(("2" (lemma "vec_from_nz")
(("2" (expand "vec_from")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((norm_vec_from formula-decl nil trackAngles_2D 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)
(injective? const-decl "bool" functions nil)
(vec_from_inj formula-decl nil trackAngles_2D nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
(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)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" 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)
(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/")
(Track nonempty-type-eq-decl nil trackAngles_scaf nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(vec_from const-decl "Vect2" trackAngles_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(track const-decl "{alpha: Track | u = vec_from(alpha, norm(u))}"
trackAngles_2D nil)
(sin const-decl "real" trig_basic "trig/")
(cos const-decl "real" trig_basic "trig/"))
nil))
(track_trk 0
(track_trk-1 nil 3476205015
("" (skeep)
(("" (typepred "track(u)")
(("" (expand "trk")
(("" (expand "vec_from")
(("" (lemma "comps_eq")
(("" (inst?)
(("" (flatten)
(("" (hide -2)
(("" (split -1)
(("1" (flatten)
(("1" (replace -1)
(("1" (hide -1)
(("1" (replace -1)
(("1" (hide -1)
(("1"
(lemma "atan2_cos_sin")
(("1"
(inst?)
(("1"
(lemma "atan2_cancel_pos")
(("1"
(inst
-
"norm(u)"
"cos(track(u))"
"sin(track(u))")
(("1"
(assert)
(("1"
(lemma "cos_eq_0")
(("1"
(inst?)
(("1"
(assert)
(("1"
(lemma "sin_eq_0")
(("1"
(inst?)
(("1"
(flatten)
(("1"
(assert)
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))
nil))
nil))
nil))
nil))
nil))
nil)
((track const-decl "{alpha: Track | u = vec_from(alpha, norm(u))}"
trackAngles_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(vec_from const-decl "Vect2" trackAngles_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Track nonempty-type-eq-decl nil trackAngles_scaf 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_times_real_is_real application-judgement "real" reals nil)
(cos const-decl "real" trig_basic "trig/")
(sin const-decl "real" trig_basic "trig/")
(cos_eq_0 formula-decl nil trig_basic "trig/")
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sin_eq_0 formula-decl nil trig_basic "trig/")
(nil application-judgement "nnreal_lt_2pi" atan2 "trig/")
(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)
(atan2_cancel_pos formula-decl nil atan2 "trig/")
(atan2_cos_sin formula-decl nil atan2 "trig/")
(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)
(comps_eq formula-decl nil vectors_2D nil)
(trk const-decl "Track" trackAngles_2D nil))
nil))
(vec_from_trk 0
(vec_from_trk-1 nil 3476205263
("" (skosimp*)
(("" (lemma "track_trk")
(("" (inst?)
(("" (replace -1 * rl)
(("" (rewrite "vec_from_track") nil nil)) nil))
nil))
nil))
nil)
((track_trk formula-decl nil trackAngles_2D nil)
(vec_from_track formula-decl nil trackAngles_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))
(track_x0_TCC1 0
(track_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))
(track_x0 0
(track_x0-1 nil 3414486628
("" (skeep)
(("" (rewrite "track_trk")
(("" (expand "trk")
(("" (expand "atan2") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((track_trk formula-decl nil trackAngles_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/")
(trk const-decl "Track" trackAngles_2D nil))
shostak))
(track_0x_TCC1 0
(track_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))
(track_0x 0
(track_0x-2 nil 3476205095
("" (skeep)
(("" (rewrite "track_trk")
(("" (expand "trk")
(("" (expand "atan2") (("" (rewrite "atan_0") nil nil)) nil))
nil))
nil))
nil)
((track_trk formula-decl nil trackAngles_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/")
(trk const-decl "Track" trackAngles_2D nil))
nil)
(track_0x-1 nil 3414486495
("" (skeep)
(("" (rewrite "track_Track")
(("" (expand "Track")
(("" (expand "atan2") (("" (rewrite "atan_0") nil nil)) nil))
nil))
nil))
nil)
((Vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(atan2 const-decl "real" atan2 "trig/")
(atan_0 formula-decl nil atan "trig/")
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/"))
shostak))
(track_xx_TCC1 0
(track_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)
(track_xx_TCC1-2 nil 3431180799
(";;; Proof track_0x_TCC1-1 for formula trackTracks.track_0x_TCC1"
(skeep)
((";;; Proof track_0x_TCC1-1 for formula trackTracks.track_0x_TCC1"
(rewrite "nzv_xy_neq_0") nil))
";;; developed with shostak decision procedures")
nil nil)
(track_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))
(track_xx 0
(track_xx-2 nil 3476205117
("" (skeep)
(("" (rewrite "track_trk")
(("" (expand "trk")
(("" (expand "atan2")
(("" (assert)
(("" (lemma "atan_tan")
(("" (inst - "pi/4")
(("" (rewrite "tan_pi4") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((track_trk formula-decl nil trackAngles_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)
(trk const-decl "Track" trackAngles_2D nil))
nil)
(track_xx-1 nil 3414486832
("" (skeep)
(("" (rewrite "track_Track")
(("" (expand "Track")
(("" (expand "atan2")
(("" (assert)
(("" (lemma "atan_tan")
(("" (inst - "pi/4")
(("" (rewrite "tan_pi4") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(atan2 const-decl "real" atan2 "trig/")
(atan_tan formula-decl nil trig_inverses "trig/")
(tan_pi4 formula-decl nil trig_values "trig/")
(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/")
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/"))
shostak))
(track_n0_TCC1 0
(track_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)
(track_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))
(track_n0 0
(track_n0-2 nil 3476205134
("" (skeep)
(("" (rewrite "track_trk")
(("" (expand "trk")
(("" (expand "atan2") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((track_trk formula-decl nil trackAngles_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/")
(trk const-decl "Track" trackAngles_2D nil))
nil)
(track_n0-1 nil 3414487848
("" (skeep)
(("" (rewrite "track_Track")
(("" (expand "Track")
(("" (expand "atan2") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((Vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(atan2 const-decl "real" atan2 "trig/")
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/"))
shostak))
(track_0n_TCC1 0
(track_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)
(track_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))
(track_0n 0
(track_0n-1 nil 3414487912
("" (skeep)
(("" (rewrite "track_trk")
(("" (expand "trk")
(("" (expand "atan2") (("" (rewrite "atan_0") nil nil)) nil))
nil))
nil))
nil)
((track_trk formula-decl nil trackAngles_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/")
(trk const-decl "Track" trackAngles_2D nil))
nil))
(track_nx_TCC1 0
(track_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)
(track_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))
(track_nx 0
(track_nx-1 nil 3414488044
("" (skeep)
(("" (rewrite "track_trk")
(("" (expand "trk")
(("" (expand "atan2")
(("" (lemma "atan_neg")
(("" (inst - "1")
(("" (assert)
(("" (case "tan(-pi/4) = -1")
(("1" (lemma "atan_tan")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (hide 2)
(("2" (expand "tan")
(("2" (lemma "cos_neg")
(("2" (inst - "pi/4")
(("2" (replace -1)
(("2" (hide -1)
(("2"
(lemma "sin_neg")
(("2"
(inst - "pi/4")
(("2"
(replace -1)
(("2"
(rewrite "cos_pi4")
(("2"
(rewrite "sin_pi4")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "Tan?")
(("3" (flatten)
(("3" (lemma "cos_neg")
(("3" (inst - "pi/4")
(("3" (assert)
(("3" (lemma "cos_pi4")
(("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(track_trk formula-decl nil trackAngles_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)
(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)
(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)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(atan2 const-decl "real" atan2 "trig/")
(= const-decl "[T, T -> boolean]" equalities nil)
(Tan? const-decl "bool" trig_basic "trig/")
(tan const-decl "real" trig_basic "trig/")
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields 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/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_abs_lt_pi2 nonempty-type-eq-decl nil atan "trig/")
(atan_tan formula-decl nil trig_inverses "trig/")
(cos_pi4 formula-decl nil trig_values "trig/")
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(sin_pi4 formula-decl nil trig_values "trig/")
(sin_neg formula-decl nil trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_neg formula-decl nil trig_basic "trig/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(atan_neg formula-decl nil atan "trig/")
(trk const-decl "Track" trackAngles_2D nil))
nil))
(track_xn_TCC1 0
(track_xn_TCC1-2 nil 3431180851
("" (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)
(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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields 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)
(track_xn_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))
(track_xn 0
(track_xn-2 nil 3476205203
("" (skeep)
(("" (rewrite "track_trk")
(("" (expand "trk")
(("" (expand "atan2")
(("" (lemma "atan_neg")
(("" (inst - "1")
(("" (assert)
(("" (case "tan(-pi/4) = -1")
(("1" (lemma "atan_tan")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (hide 2)
(("2" (expand "tan")
(("2" (lemma "cos_neg")
(("2" (inst - "pi/4")
(("2" (replace -1)
(("2" (hide -1)
(("2"
(lemma "sin_neg")
(("2"
(inst - "pi/4")
(("2"
(replace -1)
(("2"
(rewrite "cos_pi4")
(("2"
(rewrite "sin_pi4")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "Tan?")
(("3" (flatten)
(("3" (lemma "cos_neg")
(("3" (inst - "pi/4")
(("3" (lemma "cos_pi4")
(("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(track_trk formula-decl nil trackAngles_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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(atan2 const-decl "real" atan2 "trig/")
(= const-decl "[T, T -> boolean]" equalities nil)
(Tan? const-decl "bool" trig_basic "trig/")
(tan const-decl "real" trig_basic "trig/")
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields 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/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_abs_lt_pi2 nonempty-type-eq-decl nil atan "trig/")
(atan_tan formula-decl nil trig_inverses "trig/")
(cos_pi4 formula-decl nil trig_values "trig/")
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(sin_pi4 formula-decl nil trig_values "trig/")
(sin_neg formula-decl nil trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_neg formula-decl nil trig_basic "trig/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(atan_neg formula-decl nil atan "trig/")
(trk const-decl "Track" trackAngles_2D nil))
nil)
(track_xn-1 nil 3414491645
("" (skeep)
(("" (rewrite "track_Track")
(("" (expand "Track")
(("" (expand "atan2")
(("" (lemma "atan_neg")
(("" (inst - "1")
(("" (assert)
(("" (case "tan(-pi/4) = -1")
(("1" (lemma "atan_tan")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (hide 2)
(("2" (expand "tan")
(("2" (lemma "cos_neg")
(("2" (inst - "pi/4")
(("2" (replace -1)
(("2" (hide -1)
(("2"
(lemma "sin_neg")
(("2"
(inst - "pi/4")
(("2"
(replace -1)
(("2"
(rewrite "cos_pi4")
(("2"
(rewrite "sin_pi4")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "Tan?")
(("3" (flatten)
(("3" (lemma "cos_neg")
(("3" (inst - "pi/4")
(("3" (lemma "cos_pi4")
(("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(atan2 const-decl "real" atan2 "trig/")
(Tan? const-decl "bool" trig_basic "trig/")
(tan const-decl "real" trig_basic "trig/")
(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/")
(atan_tan formula-decl nil trig_inverses "trig/")
(cos_pi4 formula-decl nil trig_values "trig/")
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(sin_pi4 formula-decl nil trig_values "trig/")
(sin_neg formula-decl nil trig_basic "trig/")
(cos_neg formula-decl nil trig_basic "trig/")
(atan_neg formula-decl nil atan "trig/")
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/"))
nil))
(track_nn_TCC1 0
(track_nn_TCC1-2 nil 3431180858
("" (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)
(track_nn_TCC1-1 nil 3414491763
("" (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))
(track_nn 0
(track_nn-1 nil 3414491772
("" (skeep)
(("" (rewrite "track_trk")
(("" (expand "trk")
(("" (expand "atan2")
(("" (lemma "atan_neg")
(("" (inst - "1")
(("" (assert)
(("" (case "tan(-pi/4) = -1")
(("1" (lemma "atan_tan")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (hide 2)
(("2" (expand "tan")
(("2" (lemma "cos_neg")
(("2" (inst - "pi/4")
(("2" (replace -1)
(("2" (hide -1)
(("2"
(lemma "sin_neg")
(("2"
(inst - "pi/4")
(("2"
(replace -1)
(("2"
(rewrite "cos_pi4")
(("2"
(rewrite "sin_pi4")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "Tan?")
(("3" (flatten)
(("3" (lemma "cos_neg")
(("3" (inst - "pi/4")
(("3" (lemma "cos_pi4")
(("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.110 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.
|
