|
(track
(trkgs2vect_TCC1 0
(trkgs2vect_TCC1-1 nil 3460311979
("" (skeep)
(("" (use "scal_eq_zero")
(("" (assert)
(("" (hide -2)
(("" (lemma "sqv_eq_0")
(("" (inst?)
(("" (assert)
(("" (hide -2)
(("" (rewrite "sqv_sos")
(("" (expand "sos")
(("" (use "sin2_cos2") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((scal_eq_zero formula-decl nil vectors_2D "vectors/")
(cos const-decl "real" sincos_def "trig_fnd/")
(sin const-decl "real" sincos_def "trig_fnd/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(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 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)
(sos const-decl "nnreal" vectors_2D "vectors/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sin2_cos2 formula-decl nil trig_basic "trig_fnd/")
(sqv_sos formula-decl nil vectors_2D "vectors/")
(sqv_eq_0 formula-decl nil vectors_2D "vectors/")
(sin_range application-judgement "trig_range" sincos_def
"trig_fnd/")
(cos_range application-judgement "trig_range" sincos_def
"trig_fnd/"))
nil))
(track_TCC1 0
(track_TCC1-1 nil 3460312047
("" (skeep)
(("" (typepred "v")
(("" (flatten) (("" (decompose-equality 1) nil nil)) nil)) nil))
nil)
((Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(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_x formula-decl nil vectors_2D "vectors/")
(comp_zero_y formula-decl nil vectors_2D "vectors/"))
nil))
(sin_track 0
(sin_track-1 nil 3460330771
("" (skeep)
(("" (expand "track")
(("" (rewrite "sin_atan2")
(("1" (lift-if)
(("1" (ground)
(("1" (field 1)
(("1" (both-sides-f 1 "sq")
(("1" (rewrite "sq_norm")
(("1" (rewrite "sqv_sos")
(("1" (expand "sos")
(("1" (replaces -2) (("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (rewrite "sq_eq") nil nil))
nil))
nil)
("2" (field 2)
(("2" (neg-formula 2)
(("2" (both-sides-f 2 "sq")
(("1" (rewrite "sq_norm")
(("1" (rewrite "sq_neg")
(("1" (rewrite "sqv_sos")
(("1" (expand "sos")
(("1" (replaces -1) (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "sq_eq") nil nil))
nil))
nil))
nil)
("3" (field)
(("3" (cancel-by 1 "v`x")
(("3" (both-sides-f 2 "sq")
(("1" (rewrite "sq_norm")
(("1" (rewrite "sq_times")
(("1" (rewrite "sq_div")
(("1" (real-props)
(("1" (rewrite "sqv_sos")
(("1" (expand "sos")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "sq_eq")
(("2" (mult-cases 1) nil nil)) nil))
nil))
nil))
nil)
("4" (field 2)
(("4" (cancel-by 2 "v`x")
(("4" (neg-formula 3)
(("4" (both-sides-f 3 "sq")
(("1" (rewrite "sq_norm")
(("1" (rewrite "sq_neg")
(("1" (rewrite "sq_times")
(("1" (rewrite "sq_div")
(("1" (real-props)
(("1"
(rewrite "sqv_sos")
(("1"
(expand "sos")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "sq_eq")
(("2" (neg-formula 1 :auto-step (grind-reals))
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (typepred "v")
(("2" (flatten) (("2" (decompose-equality 1) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((track const-decl "nnreal_lt_2pi" track nil)
(comp_zero_y formula-decl nil vectors_2D "vectors/")
(comp_zero_x formula-decl nil vectors_2D "vectors/")
(FDX_75 skolem-const-decl "posreal" track nil)
(FDX_74 skolem-const-decl "real" track nil)
(FDX_73 skolem-const-decl
"{nnz: nnreal | nnz * nnz = 1 + sq(v`x / v`y)}" track nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(neg_times_ge formula-decl nil real_props nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(<= const-decl "bool" reals nil)
(both_sides_times_neg_ge1 formula-decl nil real_props nil)
(CBD_76 skolem-const-decl "real" track nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(nonzero_times3 formula-decl nil real_props nil)
(FDX_71 skolem-const-decl "posreal" track nil)
(FDX_70 skolem-const-decl "real" track nil)
(FDX_69 skolem-const-decl
"{nnz: nnreal | nnz * nnz = 1 + sq(v`x / v`y)}" track nil)
(v skolem-const-decl "Nz_vect2" track nil)
(sq_times formula-decl nil sq "reals/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_sqrt formula-decl nil sqrt "reals/")
(div_cancel1 formula-decl nil real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sq_div formula-decl nil sq "reals/")
(pos_times_ge formula-decl nil real_props nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(CBD_72 skolem-const-decl "real" track nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(sq_neg formula-decl nil sq "reals/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(neg_one_times formula-decl nil extra_tegies nil)
(neg_neg formula-decl nil extra_tegies nil)
(mult_neg formula-decl nil extra_tegies nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_2D "vectors/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(both_sides_times1 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil 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)
(div_cancel2 formula-decl nil real_props nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_eq formula-decl nil sq "reals/")
(sq_norm formula-decl nil vectors_2D "vectors/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(sos const-decl "nnreal" vectors_2D "vectors/")
(sq_0 formula-decl nil sq "reals/")
(sqv_sos formula-decl nil vectors_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(NOT const-decl "[bool -> bool]" booleans nil)
(sq const-decl "nonneg_real" sq "reals/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(minus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sin_range application-judgement "trig_range" sincos_def
"trig_fnd/")
(nil application-judgement "nnreal_lt_2pi" atan2 "trig_fnd/")
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D
"vectors/")
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx "trig_fnd/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sin_atan2 formula-decl nil atan2 "trig_fnd/"))
nil))
(cos_track 0
(cos_track-2 nil 3602107493
("" (skeep)
(("" (expand "track")
(("" (rewrite "cos_atan2")
(("1" (lift-if)
(("1" (split)
(("1" (flatten) (("1" (assert) nil nil)) nil)
("2" (flatten)
(("2" (split 2)
(("1" (flatten)
(("1" (field 1)
(("1" (both-sides-f 1 "sq")
(("1" (rewrite "sq_norm")
(("1" (rewrite "sq_times")
(("1" (rewrite "sq_div")
(("1" (real-props)
(("1"
(rewrite "sqv_sos")
(("1"
(expand "sos")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "sq_eq")
(("2" (mult-cases 1) nil nil)) nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (field 2)
(("2" (neg-formula 2)
(("2" (both-sides-f 2 "sq")
(("1" (rewrite "sq_norm")
(("1" (rewrite "sq_neg")
(("1" (rewrite "sq_times")
(("1"
(rewrite "sq_div")
(("1"
(real-props)
(("1"
(rewrite "sqv_sos")
(("1"
(expand "sos")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "sq_eq")
(("2"
(neg-formula 1 :auto-step (grind-reals))
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (typepred "v")
(("2" (flatten) (("2" (decompose-equality 1) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((track const-decl "nnreal_lt_2pi" track nil)
(comp_zero_y formula-decl nil vectors_2D "vectors/")
(comp_zero_x formula-decl nil vectors_2D "vectors/")
(mult_neg formula-decl nil extra_tegies nil)
(neg_neg formula-decl nil extra_tegies nil)
(neg_one_times formula-decl nil extra_tegies nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(minus_real_is_real application-judgement "real" reals nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(neg_times_ge formula-decl nil real_props nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(<= const-decl "bool" reals nil)
(both_sides_times_neg_ge1 formula-decl nil real_props nil)
(sq_neg formula-decl nil sq "reals/")
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(FDX_79 skolem-const-decl
"{nnz: nnreal | nnz * nnz = 1 + sq(v`x / v`y)}" track nil)
(FDX_80 skolem-const-decl "posreal" track nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sq_times formula-decl nil sq "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_sqrt formula-decl nil sqrt "reals/")
(div_cancel1 formula-decl nil real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sos const-decl "nnreal" vectors_2D "vectors/")
(sqv_sos formula-decl nil vectors_2D "vectors/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_div formula-decl nil sq "reals/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(sq_norm formula-decl nil vectors_2D "vectors/")
(pos_times_ge formula-decl nil real_props nil)
(sq_eq formula-decl nil sq "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(v skolem-const-decl "Nz_vect2" track nil)
(FDX_77 skolem-const-decl
"{nnz: nnreal | nnz * nnz = 1 + sq(v`x / v`y)}" track nil)
(FDX_78 skolem-const-decl "posreal" track nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(both_sides_times1 formula-decl nil real_props nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nonzero_times3 formula-decl nil real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(nnreal type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sq const-decl "nonneg_real" sq "reals/")
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(norm const-decl "nnreal" vectors_2D "vectors/")
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_range application-judgement "trig_range" sincos_def
"trig_fnd/")
(nil application-judgement "nnreal_lt_2pi" atan2 "trig_fnd/")
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D
"vectors/")
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx "trig_fnd/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(cos_atan2 formula-decl nil atan2 "trig_fnd/"))
nil)
(cos_track-1 nil 3460312258
("" (skeep)
(("" (expand "track")
(("" (rewrite "cos_atan2")
(("1" (lift-if)
(("1" (split)
(("1" (flatten) (("1" (assert) nil nil)) nil)
("2" (flatten)
(("2" (split 2)
(("1" (flatten)
(("1" (field 1)
(("1" (both-sides-f 1 "sq")
(("1" (rewrite "sq_norm")
(("1" (rewrite "sq_times")
(("1" (rewrite "sq_div")
(("1" (real-props)
(("1" (rewrite "sqv_sq") nil nil)) nil))
nil))
nil))
nil)
("2" (rewrite "sq_eq")
(("2" (mult-cases 1) nil nil)) nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (field 2)
(("2" (neg-formula 2)
(("2" (both-sides-f 2 "sq")
(("1" (rewrite "sq_norm")
(("1" (rewrite "sq_neg")
(("1" (rewrite "sq_times")
(("1"
(rewrite "sq_div")
(("1"
(real-props)
(("1" (rewrite "sqv_sq") nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "sq_eq")
(("2"
(neg-formula 1 :auto-step (grind-reals))
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (typepred "v")
(("2" (flatten) (("2" (decompose-equality 1) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((comp_zero_y formula-decl nil vectors_2D "vectors/")
(comp_zero_x formula-decl nil vectors_2D "vectors/")
(sq_neg formula-decl nil sq "reals/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sq_times formula-decl nil sq "reals/")
(sq_sqrt formula-decl nil sqrt "reals/")
(sq_div formula-decl nil sq "reals/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(sq_norm formula-decl nil vectors_2D "vectors/")
(sq_eq formula-decl nil sq "reals/")
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(sq const-decl "nonneg_real" sq "reals/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(cos_range application-judgement "trig_range" sincos_def
"trig_fnd/")
(nil application-judgement "nnreal_lt_2pi" atan2 "trig_fnd/")
(nz_norm_gt_0 application-judgement "posreal" vectors_2D
"vectors/")
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx "trig_fnd/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(cos_atan2 formula-decl nil atan2 "trig_fnd/"))
nil))
(norm_id 0
(norm_id-2 nil 3602107517
("" (skeep)
(("" (expand "trkgs2vect")
(("" (expand "norm")
(("" (rewrite "sqv_scal")
(("" (sq-simp)
(("" (rewrite "sqv_sos")
(("" (expand "sos")
(("" (lemma "sin2_cos2")
(("" (inst?)
(("" (replaces -1) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((trkgs2vect const-decl "Nz_vect2" track nil)
(sqv_scal formula-decl nil vectors_2D "vectors/")
(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)
(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 "vectors/")
(sin const-decl "real" sincos_def "trig_fnd/")
(cos const-decl "real" sincos_def "trig_fnd/")
(cos_range application-judgement "trig_range" sincos_def
"trig_fnd/")
(sin_range application-judgement "trig_range" sincos_def
"trig_fnd/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sqv_sos formula-decl nil vectors_2D "vectors/")
(sin2_cos2 formula-decl nil trig_basic "trig_fnd/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sqrt_1 formula-decl nil sqrt "reals/")
(sos const-decl "nnreal" vectors_2D "vectors/")
(sqrt_sq formula-decl nil sqrt "reals/")
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(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)
(sqrt_times formula-decl nil sqrt "reals/")
(sq const-decl "nonneg_real" sq "reals/")
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/"))
nil)
(norm_id-1 nil 3464478912
("" (skeep)
(("" (expand "trkgs2vect")
(("" (expand "norm")
(("" (rewrite "sqv_scal")
(("" (rewrite "sqv_sq")
(("" (lemma "sin2_cos2")
(("" (inst?)
(("" (replaces -1) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sqv_scal formula-decl nil vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(sin const-decl "real" sincos_def "trig_fnd/")
(cos const-decl "real" sincos_def "trig_fnd/")
(cos_range application-judgement "trig_range" sincos_def
"trig_fnd/")
(sin_range application-judgement "trig_range" sincos_def
"trig_fnd/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sin2_cos2 formula-decl nil trig_basic "trig_fnd/")
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(sqrt_sq formula-decl nil sqrt "reals/")
(norm const-decl "nnreal" vectors_2D "vectors/"))
shostak))
(track_id 0
(track_id-1 nil 3460311988
("" (skeep)
(("" (expand "trkgs2vect")
(("" (expand "track")
(("" (expand "*")
(("" (lemma "atan2_cancel_pos")
(("" (inst -1 "gsp" "cos(trk)" "sin(trk)")
(("" (split -1)
(("1" (replaces -1)
(("1" (lemma "atan2_cos_sin")
(("1" (inst -1 "to2pi(trk)")
(("1" (rewrite "cos_id_to2pi")
(("1" (rewrite "sin_id_to2pi") nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (flatten)
(("2" (lemma "sin2_cos2")
(("2" (inst? -1)
(("2" (replaces (-2 -3))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((trkgs2vect const-decl "Nz_vect2" track nil)
(* const-decl "Vector" vectors_2D "vectors/")
(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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(cos const-decl "real" sincos_def "trig_fnd/")
(sin const-decl "real" sincos_def "trig_fnd/")
(sin2_cos2 formula-decl nil trig_basic "trig_fnd/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_0 formula-decl nil sq "reals/")
(sin_range application-judgement "trig_range" sincos_def
"trig_fnd/")
(cos_range application-judgement "trig_range" sincos_def
"trig_fnd/")
(to2pi const-decl "nnreal_lt_2pi" to2pi "trig_fnd/")
(nnreal_lt_2pi nonempty-type-eq-decl nil atan2 "trig_fnd/")
(pi const-decl "posreal" atan "trig_fnd/")
(* 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)
(sin_id_to2pi formula-decl nil to2pi "trig_fnd/")
(cos_id_to2pi formula-decl nil to2pi "trig_fnd/")
(atan2_cos_sin formula-decl nil atan2 "trig_fnd/")
(atan2_cancel_pos formula-decl nil atan2 "trig_fnd/")
(track const-decl "nnreal_lt_2pi" track nil))
nil))
(trkgs2vect_id 0
(trkgs2vect_id-1 nil 3460330284
("" (skeep)
(("" (expand "trkgs2vect")
(("" (expand "*")
(("" (rewrite "sin_track")
(("" (rewrite "cos_track")
(("" (decompose-equality 1) nil nil)) nil))
nil))
nil))
nil))
nil)
((trkgs2vect const-decl "Nz_vect2" track nil)
(sin_track formula-decl nil track nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(sin_range application-judgement "trig_range" sincos_def
"trig_fnd/")
(cos_range application-judgement "trig_range" sincos_def
"trig_fnd/")
(nz_norm_gt_0 application-judgement "posreal" vectors_2D
"vectors/")
(real_div_nzreal_is_real application-judgement "real" reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(norm const-decl "nnreal" vectors_2D "vectors/")
(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)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(cos_track formula-decl nil track nil)
(* const-decl "Vector" vectors_2D "vectors/"))
shostak))
(ordered_eps_1_TCC1 0
(ordered_eps_1_TCC1-1 nil 3461513175 ("" (subtype-tcc) nil nil)
((real_div_nzreal_is_real application-judgement "real" reals nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(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)
(Integral const-decl "real" integral_def "analysis/")
(atan_value const-decl "real" atan "trig_fnd/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(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_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nil application-judgement "nnreal_lt_2pi" atan2 "trig_fnd/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_lt_2pi nonempty-type-eq-decl nil atan2 "trig_fnd/")
(pi const-decl "posreal" atan "trig_fnd/")
(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)
(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)
(det const-decl "real" det_2D "vectors/")
(* const-decl "real" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(track const-decl "nnreal_lt_2pi" track nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx "trig_fnd/"))
nil))
(ordered_eps_1 0
(ordered_eps_1-2 "" 3505030827
("" (skeep)
(("" (skoletin* 1)
((""
(case-replace
"det(nvo,s) = norm(nvo)*norm(s)*sin(track(nvo)-track(s))")
(("1" (hide -1)
(("1"
(case-replace
"norm(nvo) * norm(s) * sin(track(nvo) - track(s)) > det(vi, s) IFF
sin(track(nvo) - track(s)) > det(vi, s) / (norm(nvo)*norm(s))")
(("1" (hide -1)
(("1" (both-sides-f -3 "sin")
(("1" (rewrite "sin_asin")
(("1" (replaces -1 :dir rl)
(("1" (lemma "sin_gt_to2pi")
(("1" (inst -1 "track(nvo)-track(s)" "psi")
(("1" (assert)
(("1" (replaces -1)
(("1"
(case-replace
"psi < to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 AND
to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 < pi - psi IFF 0 < to2pi(track(nvo) - track(s) - psi) AND
to2pi(track(nvo) - track(s) - psi) < pi - 2*psi")
(("1"
(hide -1)
(("1"
(replaces (-1 -2 -3))
(("1" (assert) nil nil))
nil))
nil)
("2"
(hide 2)
(("2"
(case
"to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 - psi < 0")
(("1"
(case
"psi < to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2")
(("1"
(hide 1)
(("1" (assert) nil nil))
nil)
("2"
(case
"to2pi(track(nvo) - track(s) - psi) < pi - 2 * psi")
(("1"
(hide 1 2)
(("1"
(lemma "to2pi_neg")
(("1"
(inst
-1
"to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 - psi")
(("1"
(assert)
(("1"
(lemma "to2pi_to2pi")
(("1"
(inst
-1
"track(nvo) + pi / 2 - track(s)"
"-pi/2 - psi")
(("1"
(replaces -1)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2"
(case-replace
"psi < to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 AND
to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 < pi - psi IFF 0 < to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 - psi AND to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 - psi < pi - 2*psi")
(("1"
(hide -1)
(("1"
(lemma "to2pi_id")
(("1"
(inst
-1
"to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 - psi")
(("1"
(lemma "to2pi_to2pi")
(("1"
(inst
-1
"track(nvo) + pi / 2 - track(s)"
"-pi/2 - psi")
(("1"
(replaces -1)
(("1"
(ground)
nil
nil))
nil))
nil))
nil)
("2"
(hide 3)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (hide-all-but 1)
(("2" (grind-reals)
(("1" (mult-by 1 "(norm(nvo) * norm(s))")
(("1" (assert) nil nil)) nil)
("2" (mult-by -1 "(norm(nvo) * norm(s))")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (lemma "trkgs2vect_id")
(("2" (inst-cp -1 "nvo")
(("2" (inst -1 "s")
(("2" (expand "trkgs2vect")
(("2" (rewrite "sin_minus")
(("2" (name-replace "ts" "track(s)")
(("2" (name-replace "tnvo" "track(nvo)")
(("2" (expand "det")
(("2" (name-replace "nnvo" "norm(nvo)")
(("2" (name-replace "ns" "norm(s)")
(("2"
(replaces (-1 -2) :dir rl)
(("2"
(expand "*")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx "trig_fnd/")
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(minus_odd_is_odd application-judgement "odd_int" integers 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)
(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)
(pi const-decl "posreal" atan "trig_fnd/")
(nnreal_lt_2pi nonempty-type-eq-decl nil atan2 "trig_fnd/")
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(track const-decl "nnreal_lt_2pi" track nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(det const-decl "real" det_2D "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(real_abs_le_pi2 nonempty-type-eq-decl nil asin "trig_fnd/")
(to2pi const-decl "nnreal_lt_2pi" to2pi "trig_fnd/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_abs_le1 nonempty-type-eq-decl nil asin "trig_fnd/")
(asin const-decl "real_abs_le_pi2" asin "trig_fnd/")
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(trkgs2vect const-decl "Nz_vect2" track nil)
(* const-decl "Vector" vectors_2D "vectors/")
(cos_range application-judgement "trig_range" sincos_def
"trig_fnd/")
(sin_minus formula-decl nil trig_basic "trig_fnd/")
(trkgs2vect_id formula-decl nil track nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(div_cancel2 formula-decl nil real_props nil)
(div_mult_pos_le2 formula-decl nil real_props nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(both_sides_times_pos_gt1 formula-decl nil real_props nil)
(trig_range type-eq-decl nil sincos_def "trig_fnd/")
(sin_asin formula-decl nil sincos_def "trig_fnd/")
(sin_gt_to2pi formula-decl nil to2pi "trig_fnd/")
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(to2pi_neg formula-decl nil to2pi "trig_fnd/")
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(to2pi_to2pi formula-decl nil to2pi "trig_fnd/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nvo skolem-const-decl "Nz_vect2" track nil)
(s skolem-const-decl "Nz_vect2" track nil)
(psi skolem-const-decl "real_abs_le_pi2" track nil)
(to2pi_id formula-decl nil to2pi "trig_fnd/")
(sin_range application-judgement "trig_range" sincos_def
"trig_fnd/")
(sin const-decl "real" sincos_def "trig_fnd/")
(nz_norm_gt_0 application-judgement "posreal" vectors_2D
"vectors/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil))
shostak))
(ordered_det_ge 0
(ordered_det_ge-1 nil 3461513312
("" (skeep)
(("" (skoletin* 1)
((""
(case-replace
"det(nvo,s) = norm(nvo)*norm(s)*sin(track(nvo)-track(s))")
(("1" (hide -1)
(("1"
(case-replace
"norm(nvo) * norm(s) * sin(track(nvo) - track(s)) >= det(vi, s) IFF
sin(track(nvo) - track(s)) >= det(vi, s) / (norm(nvo)*norm(s))")
(("1" (hide -1)
(("1" (both-sides-f -3 "sin")
(("1" (rewrite "sin_asin")
(("1" (replaces -1 :dir rl)
(("1" (lemma "sin_ge_to2pi")
(("1" (inst -1 "track(nvo)-track(s)" "psi")
(("1" (assert)
(("1" (replaces -1)
(("1"
(case-replace
"psi <= to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 AND
to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 <= pi - psi IFF 0 <= to2pi(track(nvo) - track(s) - psi) AND
to2pi(track(nvo) - track(s) - psi) <= pi - 2*psi")
(("1"
(hide -1)
(("1"
(replaces (-1 -2 -3))
(("1" (assert) nil nil))
nil))
nil)
("2"
(hide 2)
(("2"
(case
"to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 - psi < 0")
(("1"
(case
"psi <= to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2")
(("1"
(hide 1)
(("1" (assert) nil nil))
nil)
("2"
(case
"to2pi(track(nvo) - track(s) - psi) <= pi - 2 * psi")
(("1"
(hide 1 2)
(("1"
(lemma "to2pi_neg")
(("1"
(inst
-1
"to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 - psi")
(("1"
(assert)
(("1"
(lemma "to2pi_to2pi")
(("1"
(inst
-1
"track(nvo) + pi / 2 - track(s)"
"-pi/2 - psi")
(("1"
(replaces -1)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2"
(case-replace
"psi <= to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 AND
to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 <= pi - psi IFF 0 <= to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 - psi AND to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 - psi <= pi - 2*psi")
(("1"
(hide -1)
(("1"
(lemma "to2pi_id")
(("1"
(inst
-1
"to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 - psi")
(("1"
(lemma "to2pi_to2pi")
(("1"
(inst
-1
"track(nvo) + pi / 2 - track(s)"
"-pi/2 - psi")
(("1"
(replaces -1)
(("1"
(ground)
nil
nil))
nil))
nil))
nil)
("2"
(hide 3)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (grind-reals) nil nil)) nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (lemma "trkgs2vect_id")
(("2" (inst-cp -1 "nvo")
(("2" (inst -1 "s")
(("2" (expand "trkgs2vect")
(("2" (rewrite "sin_minus")
(("2" (name-replace "ts" "track(s)")
(("2" (name-replace "tnvo" "track(nvo)")
(("2" (expand "det")
(("2" (name-replace "nnvo" "norm(nvo)")
(("2" (name-replace "ns" "norm(s)")
(("2"
(replaces (-1 -2) :dir rl)
(("2"
(expand "*")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx "trig_fnd/")
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(minus_odd_is_odd application-judgement "odd_int" integers 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)
(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)
(pi const-decl "posreal" atan "trig_fnd/")
(nnreal_lt_2pi nonempty-type-eq-decl nil atan2 "trig_fnd/")
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(track const-decl "nnreal_lt_2pi" track nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(det const-decl "real" det_2D "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(real_abs_le_pi2 nonempty-type-eq-decl nil asin "trig_fnd/")
(to2pi const-decl "nnreal_lt_2pi" to2pi "trig_fnd/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_abs_le1 nonempty-type-eq-decl nil asin "trig_fnd/")
(asin const-decl "real_abs_le_pi2" asin "trig_fnd/")
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(trkgs2vect const-decl "Nz_vect2" track nil)
(* const-decl "Vector" vectors_2D "vectors/")
(cos_range application-judgement "trig_range" sincos_def
"trig_fnd/")
(sin_minus formula-decl nil trig_basic "trig_fnd/")
(trkgs2vect_id formula-decl nil track nil)
(div_mult_pos_ge2 formula-decl nil real_props nil)
(trig_range type-eq-decl nil sincos_def "trig_fnd/")
(sin_asin formula-decl nil sincos_def "trig_fnd/")
(sin_ge_to2pi formula-decl nil to2pi "trig_fnd/")
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(to2pi_neg formula-decl nil to2pi "trig_fnd/")
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(to2pi_to2pi formula-decl nil to2pi "trig_fnd/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nvo skolem-const-decl "Nz_vect2" track nil)
(s skolem-const-decl "Nz_vect2" track nil)
(psi skolem-const-decl "real_abs_le_pi2" track nil)
(to2pi_id formula-decl nil to2pi "trig_fnd/")
(sin_range application-judgement "trig_range" sincos_def
"trig_fnd/")
(sin const-decl "real" sincos_def "trig_fnd/")
(nz_norm_gt_0 application-judgement "posreal" vectors_2D
"vectors/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil))
nil))
(ordered_eps_neg_1 0
(ordered_eps_neg_1-1 nil 3460980839
("" (skeep)
(("" (lemma "ordered_det_ge")
(("" (inst -1 "nvo" "s" "vi")
(("" (ground) (("" (ground) nil nil)) nil)) nil))
nil))
nil)
((ordered_det_ge formula-decl nil track nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx "trig_fnd/")
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(real nonempty-type-from-decl nil reals nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D
"vectors/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil))
nil))
(ordered_eps_1_dot_gt_0 0
(ordered_eps_1_dot_gt_0-1 nil 3461500351
("" (skeep)
(("" (skoletin* 1)
((""
(case-replace
"nvo*s = norm(nvo)*norm(s)*cos(track(nvo)-track(s))")
(("1" (hide -1)
(("1"
(case-replace
"norm(nvo) * norm(s) * cos(track(nvo) - track(s)) > 0 IFF cos(track(nvo) - track(s)) > 0")
(("1" (hide -1)
(("1" (lemma "cos_pos_to2pi")
(("1" (inst?)
(("1" (replaces -1)
(("1"
(case-replace
"-pi / 2 < to2pi(track(nvo) - track(s) + pi / 2) - pi / 2 AND
to2pi(track(nvo) - track(s) + pi / 2) - pi / 2 < pi / 2 IFF -pi / 2 - psi < to2pi(track(nvo) - track(s) + pi / 2) - pi / 2 - psi AND
to2pi(track(nvo) - track(s) + pi / 2) - pi / 2 - psi < pi/2 - psi")
(("1" (hide -1)
(("1"
(case "to2pi(track(nvo) - track(s) + pi / 2) - pi / 2 - psi >= 0")
(("1" (lemma "to2pi_id")
(("1"
(inst -1
"to2pi(track(nvo) - track(s) + pi / 2) - pi / 2 - psi")
(("1"
(replaces -1 :dir rl)
(("1"
(lemma "to2pi_to2pi")
(("1"
(inst
-1
"track(nvo) - track(s) + pi / 2"
"-pi/2 - psi")
(("1"
(replaces -1)
(("1"
(assert)
(("1"
(real-props)
(("1"
(lemma "ordered_eps_1")
(("1"
(inst?)
(("1"
(assert)
(("1"
(replaces -5 :dir rl)
(("1"
(replaces -1)
(("1"
(replaces -3)
(("1"
(assert)
(("1"
(replaces
-3
:dir
rl)
(("1"
(name-replace
"xx"
"to2pi(track(nvo) - phi - psi)")
(("1"
(hide -3)
(("1"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.237 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.
|
