| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 MB |
|
Quelle kb.prfSprache: Lisp |
|||||||||||||||
|
(kb (angle_from_to_TCC1 0 (angle_from_to_TCC1-1 nil 3483459133 ("" (skeep) (("" (typepred "to2pi((y-x)+pi)") (("" (assert) nil nil)) nil)) nil) ((- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (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/") (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 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_plus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_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/") (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) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) nil)) (angle_from_to_id 0 (angle_from_to_id-1 nil 3483703665 ("" (grind) nil 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_div_nzreal_is_real application-judgement "real" reals nil) (Integral const-decl "real" integral_def "analysis/") (atan_value const-decl "real" atan "trig_fnd/") (pi const-decl "posreal" atan "trig_fnd/") (to2pi const-decl "nnreal_lt_2pi" to2pi "trig_fnd/") (angle_from_to const-decl "{aa: real | aa >= -pi AND aa < pi}" kb nil) (real_times_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/") (real_minus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (angle_from_to_lt_pi 0 (angle_from_to_lt_pi-1 nil 3483694501 ("" (skeep) (("" (case "x-y < pi AND y-x < pi") (("1" (flatten) (("1" (expand "angle_from_to") (("1" (expand "to2pi") (("1" (case "floor((pi-x+y)/(2*pi)) = 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -3) (("2" (grind :exclude "pi") (("2" (name "zzz" "(pi-x+y)/(2*pi)") (("2" (case "zzz < 1 AND zzz > 0") (("1" (flatten) (("1" (grind) nil nil)) nil) ("2" (hide 2) (("2" (split +) (("1" (replace -1 :dir rl) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil)) nil) ("2" (replace -1 :dir rl) (("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind :exclude "pi") nil nil)) nil)) nil)) nil) ((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 "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (angle_from_to const-decl "{aa: real | aa >= -pi AND aa < pi}" kb nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (integer nonempty-type-from-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (atan_value const-decl "real" atan "trig_fnd/") (Integral const-decl "real" integral_def "analysis/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (to2pi const-decl "nnreal_lt_2pi" to2pi "trig_fnd/") (real_times_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (angle_from_to_test 0 (angle_from_to_test-1 nil 3483459994 ("" (grind :exclude "pi") nil nil) ((posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_times_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) (angle_from_to const-decl "{aa: real | aa >= -pi AND aa < pi}" kb nil) (to2pi const-decl "nnreal_lt_2pi" to2pi "trig_fnd/") (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (chirel_star_TCC1 0 (chirel_star_TCC1-1 nil 3482010022 ("" (skeep) (("" (case "s = zero") (("1" (typepred "s") (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil) ("2" (typepred "s") (("2" (split 2) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (assert) (("2" (lemma "sqrt_sqv_norm") (("2" (inst?) (("2" (replace -1 :dir rl) (("2" (lemma "sq_lt") (("2" (inst - "D" "sqrt(sqv(s))") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((zero const-decl "Vector" vectors_2D "vectors/") (Ss_vect2 type-eq-decl nil horizontal nil) (D formal-const-decl "posreal" kb nil) (posreal nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (> 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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sqv_zero formula-decl nil vectors_2D "vectors/") (NOT const-decl "[bool -> bool]" booleans nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nz_norm_gt_0 application-judgement "posreal" vectors_2D "vectors/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (norm const-decl "nnreal" vectors_2D "vectors/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (div_mult_pos_le2 formula-decl nil real_props nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (sq_lt formula-decl nil sq "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (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) (sqrt_pos application-judgement "posreal" sqrt "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (div_mult_pos_le1 formula-decl nil real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) nil)) (chirel_star_equiv_TCC1 0 (chirel_star_equiv_TCC1-2 nil 3486461825 ("" (skeep) (("" (case "s = zero") (("1" (typepred "s") (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil) ("2" (typepred "s") (("2" (split 2) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (assert) (("2" (lemma "sqrt_sqv_norm") (("2" (inst?) (("2" (replace -1 :dir rl) (("2" (lemma "sq_lt") (("2" (inst - "D" "sqrt(sqv(s))") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((zero const-decl "Vector" vectors_2D "vectors/") (Ss_vect2 type-eq-decl nil horizontal nil) (D formal-const-decl "posreal" kb nil) (posreal nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (> 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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sqv_zero formula-decl nil vectors_2D "vectors/") (NOT const-decl "[bool -> bool]" booleans nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nz_norm_gt_0 application-judgement "posreal" vectors_2D "vectors/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (norm const-decl "nnreal" vectors_2D "vectors/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (div_mult_pos_le2 formula-decl nil real_props nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (sq_lt formula-decl nil sq "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (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) (sqrt_pos application-judgement "posreal" sqrt "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (div_mult_pos_le1 formula-decl nil real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) nil) (chirel_star_equiv_TCC1-1 nil 3483695428 ("" (skeep) (("" (case "s = zero") (("1" (typepred "s") (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "zero") (("2" (decompose-equality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil) ((zero const-decl "Vector" vectors_2D "vectors/") (Ss_vect2 type-eq-decl nil horizontal nil) (sq const-decl "nonneg_real" sq "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (sq_nz_pos application-judgement "posreal" sq "reals/") (sqv_zero formula-decl nil vectors_2D "vectors/")) nil)) (chirel_star_equiv 0 (chirel_star_equiv-1 nil 3483695444 ("" (skeep) (("" (lemma "angle_from_to_lt_pi") (("" (inst - "track(v)" "(track(-s) - eps * asin(D / norm(s)))") (("" (assert) (("" (expand "chirel_star") (("" (replace -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((angle_from_to_lt_pi formula-decl nil kb nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (chirel_star const-decl "nnreal_lt_2pi" kb nil) (norm const-decl "nnreal" vectors_2D "vectors/") (asin const-decl "real_abs_le_pi2" asin "trig_fnd/") (real_abs_le_pi2 nonempty-type-eq-decl nil asin "trig_fnd/") (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (real_abs_le1 nonempty-type-eq-decl nil asin "trig_fnd/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nzint nonempty-type-eq-decl nil integers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (Ss_vect2 type-eq-decl nil horizontal nil) (D formal-const-decl "posreal" kb nil) (sq const-decl "nonneg_real" sq "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (track const-decl "nnreal_lt_2pi" track 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) (bool nonempty-type-eq-decl nil booleans 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) (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) (neg_ss application-judgement "Ss_vect2[D]" kb nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nz_norm_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (chirel_star_test_TCC1 0 (chirel_star_test_TCC1-1 nil 3483433209 ("" (subtype-tcc) nil nil) ((mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Ss_vect2 type-eq-decl nil horizontal nil) (D formal-const-decl "posreal" kb nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (> 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) (track const-decl "nnreal_lt_2pi" track nil) (Integral const-decl "real" integral_def "analysis/") (atan_value const-decl "real" atan "trig_fnd/") (pi const-decl "posreal" atan "trig_fnd/") (- const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (horizontal_conflict? const-decl "bool" horizontal nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (real_times_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (chirel_star_test 0 (chirel_star_test-1 nil 3483433209 ("" (skeep) (("" (case "NOT horizontal_conflict?(s,vo-vi)") (("1" (hide 2) (("1" (expand "horizontal_conflict?") (("1" (inst + "10") (("1" (replace -3) (("1" (replace -4) (("1" (replace -2) (("1" (expand "-") (("1" (expand "+") (("1" (grind) (("1" (case "-10/sqrt(3)*(-10/sqrt(3)) = 100/3") (("1" (replace -1) (("1" (hide-all-but 1) (("1" (case "20*10/sqrt(3)>100+100/3-25") (("1" (assert) nil nil) ("2" (hide 2) (("2" (cross-mult 1) (("2" (lemma "sq_gt") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "NOT track(vo) = pi/2") (("1" (hide 2) (("1" (replace -4) (("1" (expand "track") (("1" (expand "atan2") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (assert) (("2" (case "NOT track(vi) = pi/2") (("1" (hide 2) (("1" (replace -6) (("1" (expand "track") (("1" (expand "atan2") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "NOT track(vo-vi) = pi/2") (("1" (hide 2) (("1" (replace -6) (("1" (replace -7) (("1" (expand "-") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "NOT track(-s) = pi/2") (("1" (hide 2) (("1" (replace -6) (("1" (expand "-" +) (("1" (expand "track" +) (("1" (expand "atan2") (("1" (lift-if) (("1" (ground) (("1" (hide-all-but 1) (("1" (lemma "posreal_div_posreal_is_posreal") (("1" (inst - "10" "sqrt(3)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "NOT norm(s) = 10/sqrt(3)") (("1" (hide 2) (("1" (replace -7) (("1" (hide-all-but 1) (("1" (lemma "sqrt_sqv_norm") (("1" (inst?) (("1" (replace -1 :dir rl) (("1" (hide -) (("1" (lemma "sq_eq") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "NOT chirel_star(s, vo - vi, 1 / 2, -1) = 2 * pi / 3") (("1" (hide 2) (("1" (lemma "chirel_star_equiv") (("1" (inst?) (("1" (assert) (("1" (replace -2) (("1" (replace -3) (("1" (replace -4) (("1" (replace -8) (("1" (case "NOT asin(sqrt(3)/2) = pi/3") (("1" (hide-all-but 1) (("1" (lemma "sin_pi3") (("1" (replace -1 :dir rl) (("1" (hide -) (("1" (rewrite "asin_sin") nil nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (split -) (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "to2pi_id") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (cross-mult 1) (("3" (lemma "sq_le") (("3" (inst?) (("3" (assert) (("3" (expand "sq" 1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "NOT chirel_star(s, vo - vi, 1, -1) = 5 * pi / 6") (("1" (hide 2) (("1" (lemma "chirel_star_equiv") (("1" (inst?) (("1" (assert) (("1" (replace -3) (("1" (replace -4) (("1" (replace -9) (("1" (case "NOT asin(sqrt(3)/2) = pi/3") (("1" (hide-all-but 1) (("1" (lemma "sin_pi3") (("1" (replace -1 :dir rl) (("1" (rewrite "asin_sin") nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (replace -6) (("2" (assert) (("2" (split -) (("1" (replace -1) (("1" (rewrite "to2pi_id") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (cross-mult 1) (("3" (lemma "sq_le") (("3" (inst?) (("3" (assert) (("3" (expand "sq") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "NOT chirel_star(s, vo - vi, 0, -1) = pi / 2") (("1" (hide 2) (("1" (lemma "chirel_star_equiv") (("1" (inst?) (("1" (replace -4) (("1" (replace -6) (("1" (replace -5) (("1" (assert) (("1" (case "NOT asin(sqrt(3)/2) = pi/3") (("1" (hide-all-but 1) (("1" (lemma "sin_pi3") (("1" (replace -1 :dir rl) (("1" (rewrite "asin_sin") nil nil)) nil)) nil)) nil) ("2" (replace -11) (("2" (replace -1) (("2" (split -) (("1" (replace -1) (("1" (rewrite "to2pi_id") nil nil)) nil) ("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (cross-mult 1) (("3" (lemma "sq_le") (("3" (inst?) (("3" (assert) (("3" (expand "sq") (("3" (assert) 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) ("3" (hide 2) (("3" (replace -6) (("3" (flatten) (("3" (expand "zero") (("3" (expand "-") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (replace -6) (("3" (replace -7) (("3" (expand "-") (("3" (hide-all-but -1) (("3" (expand "zero") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (- const-decl "Vector" vectors_2D "vectors/") (Ss_vect2 type-eq-decl nil horizontal nil) (sq const-decl "nonneg_real" sq "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (Vector type-eq-decl nil vectors_2D "vectors/") (horizontal_conflict? const-decl "bool" horizontal nil) (D formal-const-decl "posreal" kb nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (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) (Vect2 type-eq-decl nil vectors_2D_def "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) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (+ const-decl "Vector" vectors_2D "vectors/") (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" 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) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (sq_gt formula-decl nil sq "reals/") (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (posrat_plus_nnrat_is_posrat application-judgement "posrat" rationals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (times_div1 formula-decl nil real_props nil) (times_div2 formula-decl nil real_props nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (div_cancel3 formula-decl nil real_props nil) (div_cancel4 formula-decl nil real_props nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (* const-decl "Vector" vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (< const-decl "bool" reals nil) (pi const-decl "posreal" atan "trig_fnd/") (nnreal_lt_2pi nonempty-type-eq-decl nil atan2 "trig_fnd/") (track const-decl "nnreal_lt_2pi" track nil) (atan2 const-decl "real" atan2 "trig_fnd/") (real_minus_real_is_real application-judgement "real" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (real_abs_le1 nonempty-type-eq-decl nil asin "trig_fnd/") (real_abs_le_pi2 nonempty-type-eq-decl nil asin "trig_fnd/") (asin const-decl "real_abs_le_pi2" asin "trig_fnd/") (sin_pi3 formula-decl nil trig_values "trig_fnd/") (asin_sin formula-decl nil sincos_def "trig_fnd/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (to2pi_id formula-decl nil to2pi "trig_fnd/") (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (div_mult_pos_le1 formula-decl nil real_props nil) (int_times_even_is_even application-judgement "even_int" integers nil) (sq_le formula-decl nil sq "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (chirel_star_equiv formula-decl nil kb nil) (chirel_star const-decl "nnreal_lt_2pi" kb nil) (Sign type-eq-decl nil sign "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (nzint nonempty-type-eq-decl nil integers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sq_sqrt formula-decl nil sqrt "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_eq formula-decl nil sq "reals/") (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/") (norm const-decl "nnreal" vectors_2D "vectors/") (nz_norm_gt_0 application-judgement "posreal" vectors_2D "vectors/") (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (- const-decl "Vector" vectors_2D "vectors/") (neg_ss application-judgement "Ss_vect2[D]" kb nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/")) shostak)) (chirel_star_0_id 0 (chirel_star_0_id-1 nil 3482222332 ("" (skeep) (("" (expand "chirel_star") (("" (rewrite "to2pi_id") nil nil)) nil)) nil) ((nz_norm_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (chirel_star const-decl "nnreal_lt_2pi" kb nil) (track const-decl "nnreal_lt_2pi" track 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/") (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) (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) (to2pi_id formula-decl nil to2pi "trig_fnd/")) shostak)) (chirel_star_1_id 0 (chirel_star_1_id-1 nil 3482571071 ("" (skeep) (("" (expand "chirel_star") (("" (expand "angle_from_to") (("" (assert) (("" (grind :exclude ("asin" "norm" "pi" "track")) nil nil)) nil)) nil)) nil)) nil) ((nz_norm_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (chirel_star const-decl "nnreal_lt_2pi" kb nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (neg_ss application-judgement "Ss_vect2[D]" kb nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (- const-decl "Vector" vectors_2D "vectors/") (to2pi const-decl "nnreal_lt_2pi" to2pi "trig_fnd/") (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (angle_from_to const-decl "{aa: real | aa >= -pi AND aa < pi}" kb nil) (real_minus_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/")) shostak)) (chirel_star_f_entry_scaf 0 (chirel_star_f_entry_scaf-2 nil 3483720866 ("" (case "FORALL (xy:real): cos(xy) < 0 IFF to2pi(xy) > pi/2 AND to2pi(xy) < 3*pi/2") (("1" (label "coslem" -1) (("1" (hide "coslem") (("1" (case "FORALL (f: nnreal, phi, r: real): phi <= pi AND phi > 0 AND cos(r) < 0 AND cos(r + phi) < 0 AND f >= 0 AND f <= 1 IMPLIES cos(r + f * phi) < 0") (("1" (skeep) (("1" (case "phi <= 0") (("1" (inst - "f" "-phi" "r") (("1" (assert) nil nil)) nil) ("2" (inst - "1-f" "phi" "r-phi") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (reveal "coslem") (("2" (inst-cp - "r+f*phi") (("2" (inst-cp - "r") (("2" (inst - "r+phi") (("2" (assert) (("2" (hide 2) (("2" (hide -5) (("2" (hide -5) (("2" (flatten) (("2" (name "zzz" "r+phi") (("2" (case "NOT r+f*phi = (1-f)*r + f*zzz") (("1" (assert) nil nil) ("2" (replace -1) (("2" (replace -2) (("2" (hide -1) (("2" (case "to2pi((1-f)*r + f*zzz) = (1-f)*to2pi(r)+f*to2pi(zzz)") (("1" (replace -1) (("1" (hide -1) (("1" (name "rt" "to2pi(r)") (("1" (replace -1) (("1" (name "zt" "to2pi(zzz)") (("1" (replace -1) (("1" (hide-all-but (-4 -5 -6 -7 -10 -11 1)) (("1" (mult-by -1 "f") (("1" (mult-by -3 "(1-f)") (("1" (add-formulas -1 -3) (("1" (assert) (("1" (mult-by -2 "f") (("1" (mult-by -3 "(1-f)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (name "n" "floor(r/(2*pi))") (("2" (name "n1" "floor(zzz/(2*pi))") (("2" (case "NOT n = n1") (("1" (name "kk" "n1-n") (("1" (case "kk > 0") (("1" (case "n1 = n+kk") (("1" (replace -1) (("1" (hide -3) (("1" (hide 1) (("1" (expand "to2pi" -) (("1" (replace -3) (("1" (replace -4) (("1" (assert) (("1" (case "kk >= 1") (("1" (assert) (("1" (mult-by -1 "2*pi") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (case "n1 > n") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -1) (("2" (typepred "n1") (("2" (typepred "n") (("2" (case "zzz > r") (("1" (mult-by -1 "1/(2*pi)") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "zf" "(1-f)*r + f*zzz") (("2" (replace -1) (("2" (name "n3" "floor(zf/(2*pi))") (("2" (case "NOT n = n3") (("1" (hide 2) (("1" (case "n3 >=n") (("1" (case "n3<=n1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -1) (("2" (typepred "n1") (("2" (typepred "n3") (("2" (case "zf <= zzz") (("1" (mult-by -1 "1/(2*pi)") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (expand "zf" 1) (("2" (case "r < zzz AND zzz<=zzz") (("1" (flatten) (("1" (mult-by -2 "f") (("1" (mult-by -2 "(1-f)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "zf >= r") (("1" (mult-by -1 "1/(2*pi)") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (expand "zf" +) (("2" (case "zzz > r AND r >= r") (("1" (flatten) (("1" (mult-by -1 "f") (("1" (mult-by -2 "(1-f)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "to2pi" +) (("2" (replace -6) (("2" (replace -5) (("2" (replace -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (name "xyz" "to2pi(xy+pi)-pi") (("2" (case "cos(xy) = cos(xyz)") (("1" (case "to2pi(xy) = to2pi(xyz)") (("1" (replace -1) (("1" (label "to2pieq" -1) (("1" (hide -1) (("1" (replace -1) (("1" (label "coseq" -1) (("1" (hide -1) (("1" (label "xyzname" -1) (("1" (hide "xyzname") (("1" (split) (("1" (flatten) (("1" (lemma "cos_ge_0") (("1" (inst - "xyz") (("1" (assert) (("1" (case "(-pi / 2 <= xyz AND xyz <= pi / 2) IFF (to2pi(xy) <= pi/2 OR to2pi(xy) >= 3*pi/2)") (("1" (replace -1) (("1" (hide -1) (("1" (reveal "to2pieq") (("1" (replace -1) (("1" (hide -1) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide 2) (("2" (hide -1) (("2" (reveal "to2pieq") (("2" (replace -1) (("2" (hide -) (("2" (case "xyz >=-pi AND xyz < pi") (("1" (ground) (("1" (case "xyz >= 0") (("1" (case "to2pi(xyz) = xyz") (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (hide 2) (("2" (expand "to2pi") (("2" (case "floor(xyz/(2*pi)) = 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (typepred "floor(xyz/(2*pi))") (("2" (case "xyz/(2*pi) < 1 AND xyz/(2*pi)>=0") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (split) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "xyz < 0") (("1" (case "floor(xyz/(2*pi)) = -1") (("1" (expand "to2pi") (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (hide 2) (("2" (hide 2) (("2" (typepred "floor(xyz/(2*pi))") (("2" (case "xyz/(2*pi) < 0 AND xyz/(2*pi)>=-1") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (split) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (case "to2pi(xyz) = xyz") (("1" (assert) nil nil) ("2" (hide 2) (("2" (case "xyz >= 0") (("1" (case "floor(xyz/(2*pi)) = 0") (("1" (expand "to2pi") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (case "xyz/(2*pi) >= 0 AND xyz/(2*pi)<1") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (split) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "floor(xyz/(2*pi)) = -1") (("1" (expand "to2pi" -) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 3) (("2" (case "xyz/(2*pi) < 0 AND xyz/(2*pi)>=-1") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (split) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (case "to2pi(xyz) = xyz") (("1" (assert) nil nil) ("2" (hide 2) (("2" (case "xyz >= 0") (("1" (case "floor(xyz/(2*pi)) = 0") (("1" (expand "to2pi" +) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (case "xyz/(2*pi) >=0 AND xyz/(2*pi)<1") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (split) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "xyz < 0") (("1" (case "floor(xyz/(2*pi)) = -1") (("1" (expand "to2pi" -) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (case "xyz/(2*pi) <0 AND xyz/(2*pi)>=-1") (("1" (assert) nil nil) ("2" (split) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (case "xyz >=0") (("1" (assert) nil nil) ("2" (case "xyz < 0") (("1" (case "floor(xyz/(2*pi)) = -1") (("1" (expand "to2pi" -) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (case "xyz/(2*pi) <0 AND xyz/(2*pi)>=-1") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (split) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("5" (case "xyz >= 0") (("1" (case "floor(xyz/(2*pi)) = 0") (("1" (expand "to2pi" -) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (case "xyz/(2*pi) >=0 AND xyz/(2*pi)<1") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (split) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "xyz < 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "xyz") (("2" (assert) (("2" (split) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "cos_lt_0") (("2" (inst - "to2pi(xyz)") (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (rewrite "cos_id_to2pi") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -2 :dir rl) (("2" (hide-all-but 1) (("2" (grind :exclude "pi") nil nil)) nil)) nil)) nil) ("2" (case "to2pi(xyz) = to2pi(xy)") (("1" (lemma "cos_id_to2pi") (("1" (inst-cp - "xyz") (("1" (inst - "xy") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1 + :dir rl) (("2" (hide-all-but 1) (("2" (grind :exclude "pi") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cos_lt_0 formula-decl nil trig_ineq "trig_fnd/") (cos_id_to2pi formula-decl nil to2pi "trig_fnd/") (OR const-decl "[bool, bool -> bool]" booleans nil) (xyz skolem-const-decl "real" kb nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (cos_ge_0 formula-decl nil trig_ineq "trig_fnd/") (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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_minus_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" sincos_def "trig_fnd/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield -> numfield]" number_fields nil) (minus_real_is_real application-judgement "real" reals nil) (f skolem-const-decl "nnreal" kb nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (zf skolem-const-decl "real" kb nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (int nonempty-type-eq-decl nil integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (integer nonempty-type-from-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (both_sides_times_pos_gt1 formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (cos const-decl "real" sincos_def "trig_fnd/") (AND const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (>= const-decl "bool" reals 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) (nonneg_real nonempty-type-eq-decl nil real_types 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/") (to2pi const-decl "nnreal_lt_2pi" to2pi "trig_fnd/") (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)) nil) (chirel_star_f_entry_scaf-1 nil 3483701902 ("" (case "FORALL (xy:real): cos(xy) < 0 IFF to2pi(xy) > pi/2 AND to2pi(xy) < 3*pi/2") (("1" (label "coslem" -1) (("1" (hide "coslem") (("1" (case "FORALL (f: nnreal, phi, r: real): phi <= pi AND phi > 0 AND cos(r) < 0 AND cos(r + phi) < 0 AND f >= 0 AND f <= 1 IMPLIES cos(r + f * phi) < 0") (("1" (skeep) (("1" (case "phi <= 0") (("1" (inst - "f" "-phi" "r") (("1" (assert) nil nil)) nil) ("2" (inst - "1-f" "phi" "r-phi") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (case "phi < pi") (("1" (hide -2) (("1" (case "cos(r+f*phi) > 0") (("1" (label "cospos" -1) (("1" (hide "cospos") (("1" (case "EXISTS (z:nnreal): z<f AND cos(r+z*phi) = 0") (("1" (case "EXISTS (b:real): b>f AND b<1 AND cos(r+b*phi) = 0") (("1" (skosimp*) (("1" (lemma "cos_eq_0") (("1" (inst-cp - "r+b!1*phi") (("1" (inst - "r+z!1*phi") (("1" (assert) (("1" (skosimp*) (("1" (case "i!2 > i!1") (("1" (case "i!2 - i!1 >=1") (("1" (hide -2) (("1" (sub-formulas -3 -2) (("1" (mult-by -2 "pi") (("1" (assert) (("1" (case "b!1-z!1 < 1") (("1" (case "(b!1-z!1)*phi < pi") (("1" (assert) nil nil) ("2" (mult-by -1 "phi") (("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) (("2" (case "z!1<b!1") (("1" (mult-by -1 "phi") (("1" (mult-by 1 "pi") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil) nil shostak)) (chirel_star_tangent 0 (chirel_star_tangent-1 nil 3482575589 ("" (skeep) (("" (lemma "line_solution_det") (("" (inst?) (("" (assert) (("" (hide 2) (("" (lemma "chirel_star_1_id") (("" (inst?) (("" (replace -1) (("" (hide -1) (("" (case "trkgs2vect(to2pi(track(-s) - eps * asin(D / norm(s))), p) = trkgs2vect(track(-s) - ep (("1" (replace -1) (("1" (hide -) (("1" (split +) (("1" (rewrite "norm_id") (("1" (case "-eps * det(s, trkgs2vect(track(-s) - eps * asin(D / norm(s)), 1)) = D") (("1" (mult-by -1 "p") (("1" (expand "trkgs2vect") (("1" (grind :exclude ("sin" "cos" "track" "asin" "norm")) nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "trkgs2vect") (("2" (lemma "cos_minus") (("2" (inst?) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "sin_minus") (("2" (inst?) (("2" (replace -1) (("2" (hide -1) (("2" (rewrite "cos_track") (("2" (rewrite "sin_track") (("2" (case "cos(eps * asin(D / norm(s))) = cos(asin(D / norm(s)))") (("1" (replace -1) (("1" (hide -1) (("1" (case "sin(eps * asin(D / norm(s))) = eps*sin(asin(D / norm(s)))") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (lemma "sin_asin") (("1" (inst?) (("1" (replace -1) (("1" (hide -1) (("1" (expand "det") (("1" (lemma "sqrt_sqv_norm") (("1" (inst?) (("1" (lemma "sq_eq") (("1" (inst?) (("1" (assert) (("1" (rewrite "vx_neg") (("1" (rewrite "vy_neg") (("1" (assert) (("1" (assert) (("1" (name "Xs" "norm(s)") (("1" (replace -1) (("1" (case "Xs > 0") (("1" (hide -4) (("1" (name "pz" "cos(asin(D/Xs))") (("1" (replace -1) (("1" (hide -1) (("1" (hide -2) (("1" (typepred "eps") (("1" (mult-by -4 "D*-eps*eps/(sq(Xs))") (("1" (grind-reals) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "eps") (("2" (ground) (("2" (replace -1) (("2" (assert) (("2" (lemma "sin_neg") (("2" (inst - "asin(D/norm(s))") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "eps") (("2" (ground) (("2" (replace -1) (("2" (lemma "cos_neg") (("2" (inst - "asin(D/norm(s))") (("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) ("2" (case "-1 * (s * trkgs2vect(track(-s) - eps * asin(D / norm(s)), 1)) >= 0") (("1" (mult-by -1 "p") (("1" (expand "trkgs2vect") (("1" (grind :exclude ("sin" "cos" "track" "asin" "norm")) nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "trkgs2vect") (("2" (lemma "sin_minus") (("2" (inst?) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "cos_minus") (("2" (inst?) (("2" (replace -1) (("2" (hide -1) (("2" (rewrite "sin_track") (("2" (rewrite "cos_track") (("2" (case "sin(eps * asin(D / norm(s))) = eps*sin(asin(D / norm(s)))") (("1" (replace -1) (("1" (case "cos(eps * asin(D / norm(s))) = cos(asin(D / norm(s)))") (("1" (replace -1) (("1" (hide -1) (("1" (hide -1) (("1" (rewrite "sin_asin") (("1" (name "rq" "cos(asin(D/norm(s)))") (("1" (case "rq >= 0") (("1" (replace -2) (("1" (hide -2) (("1" (lemma "sqrt_sqv_norm") (("1" (inst?) (("1" (lemma "sq_eq") (("1" (inst?) (("1" (assert) (("1" (hide -2) (("1" (typepred "eps") (("1" (expand "*") (("1" (rewrite "vx_neg") (("1" (rewrite "vy_neg") (("1" (real-props) (("1" (name "Xs" "norm(s)") (("1" (case "Xs > 0") (("1" (replace -2) (("1" (cancel-by 1 "Xs*Xs*Xs*Xs*rq") nil nil)) nil) ("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "asin(D/norm(s))") (("2" (name "ang" "asin(D/norm(s))") (("2" (replace -1) (("2" (hide -1) (("2" (lemma "cos_ge_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "eps") (("2" (ground) (("2" (replace -1) (("2" (lemma "cos_neg") (("2" (inst - "asin(D/norm(s))") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "eps") (("2" (ground) (("2" (replace -1) (("2" (lemma "sin_neg") (("2" (inst - "asin(D/norm(s))") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (name "vvvv" "track(-s) - eps * asin(D / norm(s))") (("2" (replace -1) (("2" (hide -1) (("2" (expand "trkgs2vect") (("2" (rewrite "cos_id_to2pi") (("2" (rewrite "sin_id_to2pi") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (case "norm(s) > 0") (("1" (split +) (("1" (cross-mult 1) nil nil) ("2" (cross-mult 1) (("2" (lemma "sqrt_sqv_norm") (("2" (inst - "s") (("2" (replace -1 :dir rl) (("2" (lemma "sq_le") (("2" (inst - "D" "sqrt(sqv(s))") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((D formal-const-decl "posreal" kb nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real 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) (line_solution_det formula-decl nil line_solutions nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nz_norm_gt_0 application-judgement "posreal" vectors_2D "vectors/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sign_neg_clos application-judgement "Sign" sign "reals/") (real_times_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/") (chirel_star_1_id formula-decl nil kb nil) (neg_ss application-judgement "Ss_vect2[D]" kb nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (to2pi const-decl "nnreal_lt_2pi" to2pi "trig_fnd/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (track const-decl "nnreal_lt_2pi" track nil) (- const-decl "Vector" vectors_2D "vectors/") (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (real_abs_le1 nonempty-type-eq-decl nil asin "trig_fnd/") (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin "trig_fnd/") (asin const-decl "real_abs_le_pi2" asin "trig_fnd/") (norm const-decl "nnreal" vectors_2D "vectors/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (cos_ge_0 formula-decl nil trig_ineq "trig_fnd/") (div_mult_pos_ge1 formula-decl nil real_props nil) (zero_times1 formula-decl nil real_props nil) (neg_times_lt formula-decl nil real_props nil) (pos_times_lt formula-decl nil real_props nil) (neg_times_le formula-decl nil real_props nil) (pos_times_le formula-decl nil real_props nil) (div_distributes_minus formula-decl nil real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (pos_times_gt formula-decl nil real_props nil) (pos_div_gt formula-decl nil real_props nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (CBD_85 skolem-const-decl "real" kb nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (norm_id formula-decl nil track nil) (cos_minus formula-decl nil trig_basic "trig_fnd/") (sin_minus formula-decl nil trig_basic "trig_fnd/") (cos_track formula-decl nil track nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (norm_neg formula-decl nil vectors_2D "vectors/") (cos const-decl "real" sincos_def "trig_fnd/") (sin_neg formula-decl nil trig_basic "trig_fnd/") (real_plus_real_is_real application-judgement "real" reals nil) (scal_1 formula-decl nil vectors_2D "vectors/") (trig_range type-eq-decl nil sincos_def "trig_fnd/") (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/") (sq_eq formula-decl nil sq "reals/") (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (sqrt_pos application-judgement "posreal" sqrt "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (vy_neg formula-decl nil vectors_2D "vectors/") (norm_eq_0 formula-decl nil vectors_2D "vectors/") (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (* const-decl "real" vectors_2D "vectors/") (both_sides_times2 formula-decl nil real_props nil) (div_distributes formula-decl nil real_props nil) (minus_div1 formula-decl nil real_props nil) (add_div formula-decl nil real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (times_div1 formula-decl nil real_props nil) (div_cancel1 formula-decl nil real_props nil) (div_cancel3 formula-decl nil real_props nil) (div_times formula-decl nil real_props nil) (times_div2 formula-decl nil real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (vx_neg formula-decl nil vectors_2D "vectors/") (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sin_asin formula-decl nil sincos_def "trig_fnd/") (sin const-decl "real" sincos_def "trig_fnd/") (cos_neg formula-decl nil trig_basic "trig_fnd/") (sin_track formula-decl nil track nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sin_range application-judgement "trig_range" sincos_def "trig_fnd/") (minus_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" sincos_def "trig_fnd/") (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (* const-decl "Vector" vectors_2D "vectors/") (det const-decl "real" det_2D "vectors/") (cos_id_to2pi formula-decl nil to2pi "trig_fnd/") (sin_id_to2pi formula-decl nil to2pi "trig_fnd/") (div_mult_pos_le1 formula-decl nil real_props nil) (sq_le formula-decl nil sq "reals/") (div_mult_pos_le2 formula-decl nil real_props nil) (chirel_star const-decl "nnreal_lt_2pi" kb nil) (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) (< const-decl "bool" reals nil) (trkgs2vect const-decl "Nz_vect2" track nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Ss_vect2 type-eq-decl nil horizontal nil) (Sp_vect2 type-eq-decl nil horizontal nil) (sq const-decl "nonneg_real" sq "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (Vector type-eq-decl nil vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nzint nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil)) shostak)) (chirel_star_f_entry 0 (chirel_star_f_entry-2 "" 3504851098 ("" (skeep) (("" (name "vf" "LAMBDA (ff:nnreal): (sin(track(s)),cos(track(s))) * trkgs2vect(chirel_star(s, v, ff, e (("" (case "vf(0) < 0 AND vf(1) < 0 IMPLIES vf(f) < 0") (("1" (split -1) (("1" (hide-all-but (-1 1)) (("1" (expand "vf") (("1" (name "nnv" "trkgs2vect(chirel_star(s, v, f, eps), p)") (("1" (replace -1) (("1" (lemma "trkgs2vect_id") (("1" (inst - "s") (("1" (replace -1 1 :dir rl) (("1" (hide -1) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (expand "trkgs2vect") (("1" (mult-by -1 "norm(s)*p") (("1" (assert) (("1" (name-replace "dd" "(# x := sin(track(s)), y := cos(track(s)) #) * (# x := sin(chirel_star(s, v, f, eps)), y := cos(chirel_star(s, v, f, eps)) #)" :hide? t) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "vf" +) (("2" (lemma "trkgs2vect_id") (("2" (inst - "s") (("2" (replace -1 -4 :dir rl) (("2" (rewrite "chirel_star_0_id") (("2" (lemma "trkgs2vect_id") (("2" (inst - "v") (("2" (replace -1 -5 :dir rl) (("2" (expand "trkgs2vect") (("2" (mult-by 1 "norm(s)*norm(v)") (("1" (assert) (("1" (name-replace "dd" "((# x := sin(track(s)), y := cos(track(s)) #) * (# x := sin(track(v)), y := cos(track(v)) #))" :hide? t) (("1" (assert) nil nil)) nil)) nil) ("2" (name-replace "dd" "((# x := sin(track(s)), y := cos(track(s)) #) * (# x := sin(track(v)), y := cos(track(v)) #))" :hide? t) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "line_solution_sep_dot_negative") (("3" (inst - "eps" "s" "trkgs2vect(chirel_star(s, v, 1, eps), 1)") (("3" (assert) (("3" (split -) (("1" (expand "vf" +) (("1" (name "nnnv" "trkgs2vect(chirel_star(s, v, 1, eps), 1)") (("1" (replace -1) (("1" (lemma "trkgs2vect_id") (("1" (inst - "s") (("1" (replace -1 -3 :dir rl) (("1" (hide-all-but (-3 1)) (("1" (expand "trkgs2vect") (("1" (mult-by 1 "norm(s)") (("1" (assert) (("1" (name-replace "dd" "(# x := sin(track(s)), y := cos(track(s)) #)" :hide? t) (("1" (assert) nil nil)) nil)) nil) ("2" (name-replace "dd" "(# x := sin(track(s)), y := cos(track(s)) #)" :hide? t) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "norm_id") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("3" (lemma "chirel_star_tangent") (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "theta" "track(v)") (("2" (name "phi1" "angle_from_to(theta, track(-s) - eps * asin(D / norm(s)))") (("1" (case "NOT (vf = (LAMBDA (ff:nnreal): cos((track(s)-theta)-ff*phi1)))") (("1" (hide 2) (("1" (decompose-equality 1) (("1" (expand "vf" 1) (("1" (expand "trkgs2vect" 1) (("1" (expand "*" 1) (("1" (expand "chirel_star" 1) (("1" (replace -2) (("1" (replace -1) (("1" (lemma "cos_minus") (("1" (inst - "track(s)" "theta+x!1*phi1") (("1" (rewrite "cos_id_to2pi") (("1" (rewrite "sin_id_to2pi") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 +) (("2" (hide-all-but (-5 1)) (("2" (typepred "f") (("2" (typepred "phi1") (("2" (assert) (("2" (flatten) (("2" (lemma "chirel_star_f_entry_scaf") (("2" (inst - "f" "phi1" "track(s)-theta") (("2" (assert) (("2" (hide-all-but (-1 -2 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (case "norm(s) > D") (("1" (split +) (("1" (cross-mult 1) nil nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sqrt_sqv_norm") (("2" (inst?) (("2" (replace -1 :dir rl) (("2" (lemma "sq_gt") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((chirel_star const-decl "nnreal_lt_2pi" kb nil) (Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nzint nonempty-type-eq-decl nil integers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (trkgs2vect const-decl "Nz_vect2" track nil) (cos const-decl "real" sincos_def "trig_fnd/") (Ss_vect2 type-eq-decl nil horizontal nil) (D formal-const-decl "posreal" kb nil) (sq const-decl "nonneg_real" sq "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (track const-decl "nnreal_lt_2pi" track 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) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (sin const-decl "real" sincos_def "trig_fnd/") (* const-decl "real" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities 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) (sq_gt formula-decl nil sq "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (sqrt_pos application-judgement "posreal" sqrt "reals/") (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (div_mult_pos_le2 formula-decl nil real_props nil) (div_mult_pos_le1 formula-decl nil real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sin_id_to2pi formula-decl nil to2pi "trig_fnd/") (cos_id_to2pi formula-decl nil to2pi "trig_fnd/") (cos_minus formula-decl nil trig_basic "trig_fnd/") (minus_real_is_real application-judgement "real" reals nil) (atan_value const-decl "real" atan "trig_fnd/") (Integral const-decl "real" integral_def "analysis/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (chirel_star_f_entry_scaf formula-decl nil kb nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (asin const-decl "real_abs_le_pi2" asin "trig_fnd/") (real_abs_le_pi2 nonempty-type-eq-decl nil asin "trig_fnd/") (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (real_abs_le1 nonempty-type-eq-decl nil asin "trig_fnd/") (- const-decl "Vector" vectors_2D "vectors/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (angle_from_to const-decl "{aa: real | aa >= -pi AND aa < pi}" kb nil) (real_minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (neg_ss application-judgement "Ss_vect2[D]" kb nil) (vf skolem-const-decl "[nnreal -> real]" kb nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (norm const-decl "nnreal" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (sin_range application-judgement "trig_range" sincos_def "trig_fnd/") (cos_range application-judgement "trig_range" sincos_def "trig_fnd/") (dot_scal_canon formula-decl nil vectors_2D "vectors/") (scal_1 formula-decl nil vectors_2D "vectors/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (nz_norm_gt_0 application-judgement "posreal" vectors_2D "vectors/") (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/") (trkgs2vect_id formula-decl nil track nil) (chirel_star_0_id formula-decl nil kb nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (line_solution_sep_dot_negative formula-decl nil line_solutions nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (chirel_star_tangent formula-decl nil kb nil) (norm_id formula-decl nil track nil) (dot_scal_left formula-decl nil vectors_2D "vectors/") (trig_range type-eq-decl nil sincos_def "trig_fnd/") (<= const-decl "bool" reals nil) (Sp_vect2 type-eq-decl nil horizontal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)) shostak) (chirel_star_f_entry-1 nil 3483107178 ("" (skeep) (("" (name "vf" "LAMBDA (ff:nnreal): (sin(track(s)),cos(track(s))) * trkgs2vect(chirel_star(s, v, ff, e (("1" (case "vf(0) < 0 AND vf(1) < 0 IMPLIES vf(f) < 0") (("1" (split -1) (("1" (hide-all-but (-1 1)) (("1" (expand "vf") (("1" (name "nnv" "trkgs2vect(chirel_star(s, v, f, eps), p)") (("1" (replace -1) (("1" (lemma "trkgs2vect_id") (("1" (inst - "s") (("1" (replace -1 1 :dir rl) (("1" (hide -1) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (expand "trkgs2vect") (("1" (mult-by -1 "norm(s)*p") (("1" (assert) nil nil) ("2" (hide 2) (("2" (div-by 1 "p") (("2" (assert) (("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) (("2" (typepred "s") (("2" (replace -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "vf" +) (("2" (lemma "trkgs2vect_id") (("2" (inst - "s") (("2" (replace -1 -4 :dir rl) (("2" (rewrite "chirel_star_0_id") (("2" (lemma "trkgs2vect_id") (("2" (inst - "v") (("2" (replace -1 -5 :dir rl) (("2" (expand "trkgs2vect") (("2" (mult-by 1 "norm(s)*norm(v)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "line_solution_sep_dot_negative") (("3" (inst - "eps" "s" "trkgs2vect(chirel_star(s, v, 1, eps), 1)") (("3" (assert) (("3" (split -) (("1" (expand "vf" +) (("1" (name "nnnv" "trkgs2vect(chirel_star(s, v, 1, eps), 1)") (("1" (replace -1) (("1" (lemma "trkgs2vect_id") (("1" (inst - "s") (("1" (replace -1 -3 :dir rl) (("1" (hide-all-but (-3 1)) (("1" (expand "trkgs2vect") (("1" (mult-by 1 "norm(s)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "norm_id") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("3" (lemma "chirel_star_tangent") (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "theta" "track(v)") (("2" (name "phi1" "angle_from_to(theta, track(-s) - eps * asin(D / norm(s)))") (("1" (case "NOT (vf = (LAMBDA (ff:nnreal): cos((track(s)-theta)-ff*phi1)))") (("1" (hide 2) (("1" (decompose-equality 1) (("1" (expand "vf" 1) (("1" (expand "trkgs2vect" 1) (("1" (expand "*" 1) (("1" (expand "chirel_star" 1) (("1" (replace -2) (("1" (replace -1) (("1" (lemma "cos_minus") (("1" (inst - "track(s)" "theta+x!1*phi1") (("1" (rewrite "cos_id_to2pi") (("1" (rewrite "sin_id_to2pi") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (typepred "s") (("2" (replace -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 +) (("2" (hide-all-but (-5 1)) (("2" (typepred "f") (("2" (typepred "phi1") (("2" (assert) (("2" (flatten) (("2" (lemma "chirel_star_f_entry_scaf") (("2" (inst - "f" "phi1" "track(s)-theta") (("2" (assert) (("2" (hide-all-but (-1 -2 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (case "norm(s) > D") (("1" (split +) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sqrt_sqv_norm") (("2" (inst?) (("2" (replace -1 :dir rl) (("2" (lemma "sq_gt") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "norm_eq_0") (("3" (inst?) (("3" (assert) (("3" (typepred "s") (("3" (replace -2) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (flatten) (("4" (case "s = zero") (("1" (typepred "s") (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "zero") (("2" (decompose-equality 1) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (typepred "s") (("2" (replace -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((Sign type-eq-decl nil sign "reals/") (trkgs2vect const-decl "Nz_vect2" track nil) (cos const-decl "real" sincos_def "trig_fnd/") (Ss_vect2 type-eq-decl nil horizontal nil) (sq const-decl "nonneg_real" sq "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (track const-decl "nnreal_lt_2pi" track nil) (nnreal_lt_2pi nonempty-type-eq-decl nil atan2 "trig_fnd/") (pi const-decl "posreal" atan "trig_fnd/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (sin const-decl "real" sincos_def "trig_fnd/") (* const-decl "real" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (sq_gt formula-decl nil sq "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (sqrt_pos application-judgement "posreal" sqrt "reals/") (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/") (sin_id_to2pi formula-decl nil to2pi "trig_fnd/") (cos_id_to2pi formula-decl nil to2pi "trig_fnd/") (cos_minus formula-decl nil trig_basic "trig_fnd/") (atan_value const-decl "real" atan "trig_fnd/") (Integral const-decl "real" integral_def "analysis/") (asin const-decl "real_abs_le_pi2" asin "trig_fnd/") (real_abs_le_pi2 nonempty-type-eq-decl nil asin "trig_fnd/") (real_abs_le1 nonempty-type-eq-decl nil asin "trig_fnd/") (neg_nzv application-judgement "Nz_vector" vectors_2D "vectors/") (norm const-decl "nnreal" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (sin_range application-judgement "trig_range" sincos_def "trig_fnd/") (cos_range application-judgement "trig_range" sincos_def "trig_fnd/") (dot_scal_canon formula-decl nil vectors_2D "vectors/") (scal_1 formula-decl nil vectors_2D "vectors/") (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/") (trkgs2vect_id formula-decl nil track nil) (line_solution_sep_dot_negative formula-decl nil line_solutions nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (norm_id formula-decl nil track nil) (dot_scal_left formula-decl nil vectors_2D "vectors/") (trig_range type-eq-decl nil sincos_def "trig_fnd/") (Sp_vect2 type-eq-decl nil horizontal nil)) shostak)) (chi_hc_TCC1 0 (chi_hc_TCC1-1 nil 3482010022 ("" (skeep) (("" (assert) nil nil)) nil) ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (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)) nil)) (chi_hc_TCC2 0 (chi_hc_TCC2-1 nil 3482010022 ("" (skosimp*) (("" (expand "abs") (("" (ground) nil nil)) nil)) nil) nil nil)) (chi_hc_TCC3 0 (chi_hc_TCC3-1 nil 3482855921 ("" (skeep) (("" (skosimp*) (("" (hide-all-but (2 3)) (("" (grind) nil nil)) nil)) nil)) nil) ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_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) (minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (chi_hc_TCC4 0 (chi_hc_TCC4-1 nil 3482855921 ("" (skosimp*) (("" (assert) nil nil)) 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_plus_real_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" sincos_def "trig_fnd/") (nz_norm_gt_0 application-judgement "posreal" vectors_2D "vectors/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_times_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/")) nil)) (sin_track_minus 0 (sin_track_minus-1 nil 3482597630 ("" (skeep) (("" (lemma "sin_minus") (("" (inst?) (("" (replace -1) (("" (hide -1) (("" (lemma "sin_minus") (("" (inst?) (("" (replace -1) (("" (hide -1) (("" (rewrite "cos_track") (("" (rewrite "cos_track") (("" (rewrite "cos_track") (("" (rewrite "sin_track") (("" (rewrite "sin_track") (("" (rewrite "sin_track") (("" (rewrite "vx_distr_sub") (("" (rewrite "vy_distr_sub") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sin_minus formula-decl nil trig_basic "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/") (sin_range application-judgement "trig_range" sincos_def "trig_fnd/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (cos_track formula-decl nil track nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (vx_distr_sub formula-decl nil vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (norm const-decl "nnreal" vectors_2D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (sqrt_pos application-judgement "posreal" sqrt "reals/") (vy_distr_sub formula-decl nil vectors_2D "vectors/") (sin_track formula-decl nil track nil) (cos_range application-judgement "trig_range" sincos_def "trig_fnd/") (- const-decl "Vector" vectors_2D "vectors/") (track const-decl "nnreal_lt_2pi" track 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) (bool nonempty-type-eq-decl nil booleans 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) (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)) shostak)) (chi_hc_sin_equivalence_2_TCC1 0 (chi_hc_sin_equivalence_2_TCC1-1 nil 3482855921 ("" (skeep) (("" (skeep) (("" (replace -1) (("" (hide-all-but (-2 -4)) (("" (expand "chi_hc") (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((chi_hc const-decl "[nnreal_lt_2pi, bool]" kb nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (real_times_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" sincos_def "trig_fnd/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nz_norm_gt_0 application-judgement "posreal" vectors_2D "vectors/")) nil)) (chi_hc_sin_equivalence_2 0 (chi_hc_sin_equivalence_2-1 nil 3482656472 ("" (skeep) (("" (skoletin 1 :postfix "a") (("" (skoletin 1 :postfix "a") (("" (flatten) (("" (label "NVOA" -2) (("" (hide "NVOA") (("" (reveal "NVOA") (("" (delabel "NVOA") (("" (copy -2) (("" (label "twotrue" -1) (("" (hide "twotrue") (("" (expand "cha" -2) (("" (expand "chi_hc" -) (("" (lift-if) (("" (ground) (("" (name "chirelstar" "chirel_star(s,vo-vi,f,eps)") (("" (replace -1) (("" (name "expr" "(norm(vi)/norm(vo))*sin(chirelstar-track(vi))") (("" (replace -1) (("" (name "asinex" "asin(expr)") (("" (replace -1) (("" (name "exsign" "sign(asinex)") (("" (replace -1) (("" (name "expidiff" "exsign*(pi/2)-asinex") (("" (mult-by -1 "irt") (("" (name "arcsindir" "exsign*(pi/2)+irt*expidiff") (("" (replace -2 :dir rl) (("" (neg-formula -1) (("" (assert) (("" (case "NOT (-1 * ((exsign * pi) / 2) - (exsign * pi) / 2 * irt + asinex * irt) = (-1 * ((pi / 2) * exsign * irt) - ex asinex * irt)") (("1" (assert) nil nil) ("2" (replace -2) (("2" (replace -8 +) (("2" (rewrite "track_id") (("2" (case "to2pi(cha`1) = cha`1") (("1" (replace -1) (("1" (hide -1) (("1" (case "expr = sin(chirelstar-cha`1)") (("1" (assert) nil nil) ("2" (hide 6) (("2" (hide 2) (("2" (hide 2) (("2" (replace -7 +) (("2" (assert) (("2" (case "sin(chirelstar - to2pi(-arcsindir + chirelstar)) = sin(arcsindir)") (("1" (replace -1) (("1" (hide -1) (("1" (expand "arcsindir" +) (("1" (replace -2 + :dir rl) (("1" (replace -4 1 :dir rl) (("1" (assert) (("1" (name "theta" "exsign * (pi / 2) + (pi / 2) * exsign * irt") (("1" (case "(pi / 2) * exsign * irt - asin(expr) * irt + exsign * (pi / 2) = theta-asinex*irt") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sin_minus") (("1" (inst?) (("1" (replace -1) (("1" (hide -1) (("1" (case "sin(theta) = 0") (("1" (replace -1) (("1" (assert) (("1" (case "sin(asinex*irt) = irt*sin(asinex)") (("1" (replace -1) (("1" (hide -1) (("1" (expand "asinex" 1) (("1" (rewrite "sin_asin") (("1" (case "cos(theta) = -irt") (("1" (case "sq(irt) = 1") (("1" (expand "sq") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "irt") (("2" (expand "sq") (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (replace -2 1 :dir rl) (("2" (hide-all-but 1) (("2" (typepred "exsign") (("2" (typepred "irt") (("2" (split -) (("1" (case "(pi / 2) * exsign * irt + exsign * (pi / 2) = exsign*pi") (("1" (replace -1) (("1" (split -) (("1" (replace -1) (("1" (lemma "cos_pi") (("1" (assert) nil nil)) nil)) nil) ("2" (replace -1) (("2" (lemma "cos_neg") (("2" (inst - "pi") (("2" (lemma "cos_pi") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (lemma "cos_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "irt") (("2" (ground) (("2" (lemma "sin_neg") (("2" (inst - "asinex") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 + :dir rl) (("2" (hide-all-but 1) (("2" (typepred "exsign") (("2" (typepred "irt") (("2" (split -) (("1" (case "exsign * (pi / 2) + (pi / 2) * exsign * irt = exsign*pi") (("1" (replace -1) (("1" (split -) (("1" (lemma "sin_pi") (("1" (assert) nil nil)) nil) ("2" (lemma "sin_neg") (("2" (inst - "pi") (("2" (lemma "sin_pi") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (case "exsign * (pi / 2) + (pi / 2) * exsign * irt = 0") (("1" (lemma "sin_0") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sin_minus") (("2" (inst?) (("2" (replace -1) (("2" (hide -1) (("2" (hide 2) (("2" (rewrite "cos_id_to2pi") (("2" (rewrite "sin_id_to2pi") (("2" (lemma "cos_minus") (("2" (inst - "chirelstar" "arcsindir") (("2" (replace -1) (("2" (hide -1) (("2" (lemma "sin_minus") (("2" (inst - "chirelstar" "arcsindir") (("2" (assert) (("2" (replace -1) (("2" (assert) (("2" (name "rvo" "trkgs2vect(chirelstar,1)") (("2" (case "not track(rvo) = to2pi(chirelstar)") (("1" (replace -1 1 :dir rl) (("1" (rewrite "track_id") nil nil)) nil) ("2" (lemma "cos_id_to2pi") (("2" (inst - "chirelstar") (("2" (replace -1 :dir rl) (("2" (hide -1) (("2" (lemma "sin_id_to2pi") (("2" (inst - "chirelstar") (("2" (replace -1 :dir rl) (("2" (hide -1) (("2" (replace -1 :dir rl) (("2" (hide -1) (("2" (case "sq(cos(track(rvo))) + sq(sin(track(rvo))) = 1") (("1" (expand "sq") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "cos_track") (("2" (rewrite "sin_track") (("2" (case "sq(norm(rvo)) = sqv(rvo)") (("1" (expand "sq") (("1" (cross-mult 1) (("1" (grind) nil nil)) nil)) nil) ("2" (lemma "sqrt_sqv_norm") (("2" (inst?) (("2" (lemma "sq_eq") (("2" (inst - "sqrt(sqv(rvo))" "norm(rvo)") (("2" (rewrite "sq_sqrt") (("1" (ground) nil nil) ("2" (hide -1) (("2" (typepred "sqv(rvo)") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "cha" 1) (("2" (typepred "chi_hc(1, eps, irt)(s, vo, vi)`1") (("2" (rewrite "to2pi_id") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (nz_norm_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_times_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/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "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) (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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (nzint nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (D formal-const-decl "posreal" kb nil) (Ss_vect2 type-eq-decl nil horizontal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (chi_hc const-decl "[nnreal_lt_2pi, bool]" kb nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (trkgs2vect const-decl "Nz_vect2" track nil) (norm const-decl "nnreal" vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (IFF const-decl "[bool, bool -> bool]" booleans nil) (sin const-decl "real" sincos_def "trig_fnd/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (chirel_star const-decl "nnreal_lt_2pi" kb nil) (track const-decl "nnreal_lt_2pi" track nil) (cha skolem-const-decl "[nnreal_lt_2pi, bool]" kb nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (real_abs_le1 nonempty-type-eq-decl nil asin "trig_fnd/") (real_abs_le_pi2 nonempty-type-eq-decl nil asin "trig_fnd/") (asin const-decl "real_abs_le_pi2" asin "trig_fnd/") (sign const-decl "Sign" sign "reals/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (mult_neg formula-decl nil extra_tegies nil) (minus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (to2pi const-decl "nnreal_lt_2pi" to2pi "trig_fnd/") (sin_id_to2pi formula-decl nil to2pi "trig_fnd/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (cos_track formula-decl nil track nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (times_div1 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (times_div2 formula-decl nil real_props nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (* const-decl "real" vectors_2D "vectors/") (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (sq_eq formula-decl nil sq "reals/") (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/") (sin_track formula-decl nil track nil) (cos_minus formula-decl nil trig_basic "trig_fnd/") (cos_id_to2pi formula-decl nil to2pi "trig_fnd/") (arcsindir skolem-const-decl "real" kb nil) (sin_minus formula-decl nil trig_basic "trig_fnd/") (sin_neg formula-decl nil trig_basic "trig_fnd/") (asinex skolem-const-decl "real_abs_le_pi2" kb nil) (sign_neg_clos application-judgement "Sign" sign "reals/") (cos const-decl "real" sincos_def "trig_fnd/") (sign_mult_clos application-judgement "Sign" sign "reals/") (mult_divides1 application-judgement "(divides(n))" divides nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sign_sq_clos application-judgement "Sign" sign "reals/") (cos_0 formula-decl nil trig_basic "trig_fnd/") (cos_pi formula-decl nil trig_basic "trig_fnd/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_neg formula-decl nil trig_basic "trig_fnd/") (sin_asin formula-decl nil sincos_def "trig_fnd/") (trig_range type-eq-decl nil sincos_def "trig_fnd/") (cos_range application-judgement "trig_range" sincos_def "trig_fnd/") (sin_0 formula-decl nil trig_basic "trig_fnd/") (sin_pi formula-decl nil trig_basic "trig_fnd/") (to2pi_id formula-decl nil to2pi "trig_fnd/") (track_id formula-decl nil track nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sign_nat formula-decl nil sign "reals/") (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sin_range application-judgement "trig_range" sincos_def "trig_fnd/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (chi_hc_track_eq 0 (chi_hc_track_eq-1 nil 3482839015 ("" (skeep) (("" (case "v`y > 0") (("1" (case "w`y > 0") (("1" (case "v`x = 0") (("1" (case "w`x = 0") (("1" (expand "track") (("1" (replace -1) (("1" (replace -2) (("1" (expand "atan2") (("1" (lift-if) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (case "v`x > 0") (("1" (case "w`x > 0") (("1" (expand "track") (("1" (expand "atan2") (("1" (lift-if) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal") (("2" (inst - "v`x" "v`y") (("1" (lemma "nnreal_div_posreal_is_nnreal") (("1" (inst - "-w`x" "w`y") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil) ("2" (case "w`x < 0") (("1" (expand "track") (("1" (expand "atan2") (("1" (lift-if) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "w`x = 0") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (lemma "nnreal_div_posreal_is_nnreal") (("2" (inst - "-v`x" "v`y") (("1" (lemma "posreal_div_posreal_is_posreal") (("1" (inst - "w`x" "w`y") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "cv" "v`x/v`y") (("2" (replace -1) (("2" (name "cw" "w`x/w`y") (("2" (replace -1) (("2" (case "w`x = 0") (("1" (case "v`x = 0") (("1" (expand "*") (("1" (replace -1) (("1" (replace -2) (("1" (assert) (("1" (case "s`y > 0") (("1" (div-by -8 "s`y") (("1" (assert) nil nil)) nil) ("2" (hide-all-but (-8 1 2)) (("2" (lemma "nnreal_times_nnreal_is_nnreal") (("2" (inst - "-s`y" "-w`y") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil) ("2" (case "v`x = 0") (("1" (assert) nil nil) ("2" (case "v`x > 0") (("1" (case "w`x < 0") (("1" (case "EXISTS (cc:negreal): w = cc*v") (("1" (skosimp*) (("1" (replace -1) (("1" (assert) (("1" (lemma "nnreal_times_nnreal_is_nnreal") (("1" (inst - "-cc!1" "-(s*v)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "w`x/v`x = w`y/v`y") (("1" (inst + "w`x/v`x") (("1" (decompose-equality) (("1" (rewrite "vx_scal") (("1" (assert) nil nil)) nil) ("2" (rewrite "vy_scal") (("2" (assert) nil nil)) nil)) nil) ("2" (real-props) nil nil)) nil) ("2" (cross-mult 1) (("2" (expand "cv") (("2" (expand "cw") (("2" (cross-mult -6) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal") (("2" (inst - "v`x" "v`y") (("1" (lemma "posreal_div_posreal_is_posreal") (("1" (inst - "w`x" "-w`y") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil) ("2" (case "w`x > 0") (("1" (case "EXISTS (cc:negreal): w = cc*v") (("1" (skosimp*) (("1" (replace -1) (("1" (assert) (("1" (lemma "nnreal_times_nnreal_is_nnreal") (("1" (inst - "-cc!1" "-(s*v)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "w`x/v`x = w`y/v`y") (("1" (inst + "w`x/v`x") (("1" (decompose-equality) (("1" (rewrite "vx_scal") (("1" (assert) nil nil)) nil) ("2" (rewrite "vy_scal") (("2" (assert) nil nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal") (("2" (inst - "w`x" "-v`x") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "cv") (("2" (expand "cw") (("2" (cross-mult -5) (("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal") (("2" (inst - "-v`x" "v`y") (("1" (lemma "posreal_div_posreal_is_posreal") (("1" (inst - "-w`x" "-w`y") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "v`y < 0") (("1" (hide 1) (("1" (case "w`y > 0") (("1" (case "w`x = 0 OR v`x = 0") (("1" (case "w`x = 0 AND v`x = 0") (("1" (hide -2) (("1" (flatten) (("1" (expand "*") (("1" (replace -1) (("1" (replace -2) (("1" (assert) (("1" (case "s`y < 0") (("1" (div-by -7 "-s`y") (("1" (assert) nil nil)) nil) ("2" (lemma "posreal_times_posreal_is_posreal") (("2" (inst - "s`y" "w`y") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split -) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (case "EXISTS (cc:negreal): w = cc*v") (("1" (skosimp*) (("1" (replace -1) (("1" (assert) (("1" (lemma "nnreal_times_nnreal_is_nnreal") (("1" (inst - "-cc!1" "-(s*v)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "w`x/v`x = w`y/v`y") (("1" (inst + "w`x/v`x") (("1" (decompose-equality) (("1" (rewrite "vx_scal") (("1" (assert) nil nil)) nil) ("2" (rewrite "vy_scal") (("2" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (case "w`x/v`x < 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (case "v`x > 0") (("1" (lemma "posreal_div_posreal_is_posreal") (("1" (inst - "v`x" "-v`y") (("1" (case "w`x < 0") (("1" (lemma "posreal_div_posreal_is_posreal") (("1" (inst - "-w`x" "v`x") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal") (("2" (inst - "w`x" "w`y") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (case "w`x > 0") (("1" (case "EXISTS (cc:negreal): w = cc*v") (("1" (skosimp*) (("1" (replace -1) (("1" (assert) (("1" (lemma "nnreal_times_nnreal_is_nnreal") (("1" (inst - "-cc!1" "-(s*v)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "w`x/v`x = w`y/v`y") (("1" (inst + "w`x/v`x") (("1" (decompose-equality) (("1" (rewrite "vx_scal") (("1" (assert) nil nil)) nil) ("2" (rewrite "vy_scal") (("2" (assert) nil nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal") (("2" (inst - "w`x" "-v`x") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal") (("2" (inst - "-v`x" "-v`y") (("1" (lemma "posreal_div_posreal_is_posreal") (("1" (inst - "-w`x" "w`y") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (cross-mult 1) (("2" (cross-mult -3) (("2" (assert) nil nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "v`x = 0 OR w`x = 0") (("1" (case "v`x = 0 AND w`x = 0") (("1" (hide -2) (("1" (flatten) (("1" (replace -1) (("1" (replace -2) (("1" (expand "*") (("1" (replace -1) (("1" (replace -2) (("1" (assert) (("1" (expand "track") (("1" (replace -1) (("1" (replace -2) (("1" (expand "atan2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split -) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (case "v`x > 0") (("1" (case "w`x > 0") (("1" (expand "track") (("1" (expand "atan2") (("1" (lift-if) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal") (("2" (inst - "v`x" "-v`y") (("1" (lemma "posreal_div_posreal_is_posreal") (("1" (inst - "-w`x" "-w`y") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil) ("2" (case "w`x < 0") (("1" (expand "track") (("1" (expand "atan2") (("1" (lift-if) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal") (("2" (inst - "-v`x" "-v`y") (("1" (lemma "posreal_div_posreal_is_posreal") (("1" (inst - "w`x" "-w`y") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) 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/") (> 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) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (* const-decl "real" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (D formal-const-decl "posreal" kb nil) (Ss_vect2 type-eq-decl nil horizontal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (times_div_cancel1 formula-decl nil extra_real_props nil) (s skolem-const-decl "Ss_vect2[D]" kb nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (both_sides_div_pos_lt1 formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal judgement-tcc nil real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/") (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (negreal nonempty-type-eq-decl nil real_types nil) (* const-decl "Vector" vectors_2D "vectors/") (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (dot_scal_right formula-decl nil vectors_2D "vectors/") (times_div2 formula-decl nil real_props nil) (div_cancel4 formula-decl nil real_props nil) (cw skolem-const-decl "real" kb nil) (cv skolem-const-decl "real" kb nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (vy_scal formula-decl nil vectors_2D "vectors/") (vx_scal formula-decl nil vectors_2D "vectors/") (div_mult_pos_lt1 formula-decl nil real_props nil) (div_mult_pos_le1 formula-decl nil real_props nil) (zero_times1 formula-decl nil real_props nil) (div_cancel3 formula-decl nil real_props nil) (cross_mult formula-decl nil real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (track const-decl "nnreal_lt_2pi" track nil) (atan_0 formula-decl nil atan "trig_fnd/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (atan2 const-decl "real" atan2 "trig_fnd/") (< const-decl "bool" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (v skolem-const-decl "Nz_vect2" kb nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (minus_real_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (w skolem-const-decl "Nz_vect2" kb nil) (nnreal_div_posreal_is_nnreal judgement-tcc nil real_types nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil)) shostak)) (chi_hc_1_chirel_TCC1 0 (chi_hc_1_chirel_TCC1-1 nil 3482593995 ("" (skeep) (("" (expand "chi_hc") (("" (lift-if) (("" (lift-if) (("" (lift-if) (("" (assert) (("" (ground) (("" (replace -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nz_norm_gt_0 application-judgement "posreal" vectors_2D "vectors/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sin_range application-judgement "trig_range" sincos_def "trig_fnd/") (real_times_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/") (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (chi_hc const-decl "[nnreal_lt_2pi, bool]" kb nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sign_nat formula-decl nil sign "reals/") (dot_zero_right formula-decl nil vectors_2D "vectors/") (minus_nzreal_is_nzreal application-judgement "nzreal" real_types 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)) (chi_hc_1_chirel_TCC2 0 (chi_hc_1_chirel_TCC2-1 nil 3482855921 ("" (subtype-tcc) nil 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) (/= const-decl "boolean" notequal 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nzint nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (> const-decl "bool" reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq "reals/") (posreal nonempty-type-eq-decl nil real_types nil) (D formal-const-decl "posreal" kb nil) (Ss_vect2 type-eq-decl nil horizontal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (* const-decl "real" vectors_2D "vectors/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (chi_hc const-decl "[nnreal_lt_2pi, bool]" kb nil) (- const-decl "Vector" vectors_2D "vectors/")) nil)) (chi_hc_1_chirel 0 (chi_hc_1_chirel-1 nil 3482593995 ("" (skeep) (("" (name "ch" "chi_hc(1,eps,irt)(s,vo,vi)") (("" (replace -1) (("" (lemma "chi_hc_sin_equivalence_2") (("" (inst?) (("" (replace -2) (("" (assert) (("" (assert) (("" (name "chirela" "chirel_star(s,vo-vi,1,eps)") (("" (replace -1) (("" (name "nvoa" "trkgs2vect(ch`1, norm(vo))") (("" (replace -1) (("" (rewrite "sin_minus") (("" (rewrite "sin_minus") (("" (name "XA" "track(nvoa)") (("" (replace -1) (("" (name "XB" "track(vi)") (("" (replace -1) (("" (case "cos(chirela) /= 0") (("1" (label "chirelanz" -1) (("1" (case "norm(vo)*cos(XA)-norm(vi)*cos(XB) /= 0") (("1" (label "Xnz" -1) (("1" (case "nvoa-vi /= zero") (("1" (label "relnz" -1) (("1" (case "norm(nvoa-vi) > 0") (("1" (label "relnorm" -1) (("1" (hide "relnorm") (("1" (hide "relnz") (("1" (case "NOT tan(chirela) = (norm(vo)*sin(XA) - norm(vi)*sin(XB))/(norm(vo)*cos(XA)-norm(vi)* (("1" (hide 2) (("1" (expand "tan" 1) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (case "NOT (norm(vo) * sin(XA) - norm(vi) * sin(XB)) = (nvoa-vi)`x") (("1" (expand "XA" +) (("1" (expand "XB" +) (("1" (rewrite "sin_track" +) (("1" (rewrite "sin_track" +) (("1" (rewrite "vx_distr_sub") (("1" (case "norm(nvoa) = norm(vo)") (("1" (replace -1 1) (("1" (assert) nil nil)) nil) ("2" (expand "nvoa" 1) (("2" (rewrite "norm_id") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT (norm(vo) * cos(XA) - norm(vi) * cos(XB)) = (nvoa-vi)`y") (("1" (expand "XA" +) (("1" (expand "XB" +) (("1" (rewrite "cos_track" 1) (("1" (rewrite "cos_track" 1) (("1" (case "norm(nvoa) = norm(vo)") (("1" (rewrite "vy_distr_sub") (("1" (assert) nil nil)) nil) ("2" (expand "nvoa" 1) (("2" (rewrite "norm_id") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (replace -2) (("2" (hide -1) (("2" (hide -1) (("2" (expand "tan" -1) (("2" (name "chiv" "trkgs2vect(chirela,norm(nvoa-vi))") (("1" (lemma "chi_hc_track_eq") (("1" (inst - "s" "nvoa-vi" "chiv") (("1" (assert) (("1" (split -) (("1" (replace -1 +) (("1" (expand "chiv" +) (("1" (rewrite "track_id") (("1" (typepred "chirela") (("1" (rewrite "to2pi_id") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "chiv" +) (("2" (expand "trkgs2vect" +) (("2" (expand "*" +) (("2" (reveal "relnorm") (("2" (lemma "nzreal_times_nzreal_is_nzreal") (("2" (inst - "norm(nvoa-vi)" "cos(chirela)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (replace -2 + :dir rl) (("3" (expand "chiv" +) (("3" (expand "trkgs2vect" +) (("3" (expand "*") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (expand "ch" -11) (("4" (hide-all-but (-11 -7 1)) (("4" (expand "ch") (("4" (expand "chi_hc") (("4" (lift-if) (("4" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (lemma "line_solution_sep_dot_negative") (("5" (inst - "eps" "s" "chiv") (("5" (assert) (("5" (lemma "chirel_star_tangent") (("5" (expand "chiv" +) (("5" (inst - "eps" "norm(nvoa-vi)" "s" "vo-vi") (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (reveal "relnorm") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil) ("4" (expand "Tan?") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-9 -5 1)) (("2" (expand "ch") (("2" (expand "chi_hc" -2) (("2" (ground) (("2" (expand "chi_hc" -) (("2" (replace -2) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT norm(vi)*sin(XB) = norm(vo)*sin(XA)") (("1" (flatten) (("1" (case "NOT cos(chirela)*norm(vi)*sin(XB) = cos(chirela)*norm(vo)*sin(XA)") (("1" (assert) nil nil) ("2" (div-by -1 "cos(chirela)") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "nvoa=vi") (("1" (hide-all-but (-1 -10 -6)) (("1" (expand "ch") (("1" (expand "chi_hc") (("1" (lift-if) (("1" (ground) (("1" (replace -1) (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "trkgs2vect_id") (("2" (inst - "vi") (("2" (lemma "trkgs2vect_id") (("2" (inst - "nvoa") (("2" (case "norm(nvoa) = norm(vo)") (("1" (replace -1) (("1" (hide -1) (("1" (replace -1 1 :dir rl) (("1" (replace -2 1 :dir rl) (("1" (expand "trkgs2vect" 1) (("1" (expand "*" +) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nvoa" 1) (("2" (rewrite "norm_id") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (assert) (("2" (case "sin(chirela) /= 0") (("1" (flatten) (("1" (case "NOT norm(vi)*cos(XB) = norm(vo)*cos(XA)") (("1" (mult-by 1 "sin(chirela)") (("1" (assert) nil nil)) nil) ("2" (case "NOT (nvoa - vi)`y = 0") (("1" (lemma "trkgs2vect_id") (("1" (inst-cp - "nvoa") (("1" (inst - "vi") (("1" (replace -1 1 :dir rl) (("1" (case "norm(nvoa) = norm(vo)") (("1" (replace -1) (("1" (replace -3 1 :dir rl) (("1" (rewrite "vy_distr_sub") (("1" (expand "trkgs2vect" 1) (("1" (expand "*" +) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nvoa" +) (("2" (rewrite "norm_id") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "chiv" "trkgs2vect(chirela,norm(nvoa-vi))") (("1" (case "s*chiv < 0") (("1" (case "s*(nvoa-vi) < 0") (("1" (case "chiv`y = 0") (("1" (case "(nvoa-vi)`x /= 0") (("1" (case "chiv`x /= 0") (("1" (case "sign((nvoa-vi)`x) = sign(chiv`x)") (("1" (case "chirela = track(chiv)") (("1" (replace -1 2) (("1" (hide -1) (("1" (hide-all-but (-1 -2 -3 -4 -5 -6 -17 2 -8)) (("1" (name "w" "nvoa-vi") (("1" (replace -1) (("1" (case "w /= zero") (("1" (expand "track") (("1" (expand "atan2") (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (expand "sign") (("1" (lift-if) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "w" +) (("2" (expand "ch") (("2" (hide-all-but (-9 1)) (("2" (expand "chi_hc") (("2" (ground) (("2" (expand "nvoa" -1) (("2" (expand "ch" -1) (("2" (expand "chi_hc") (("2" (assert) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "chiv" +) (("2" (rewrite "track_id") (("2" (rewrite "to2pi_id") nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 -3 -4 -5 -7 1)) (("2" (name "w" "nvoa-vi") (("2" (replace -1) (("2" (hide -1) (("2" (expand "*") (("2" (replace -6) (("2" (replace -3) (("2" (assert) (("2" (expand "sign" 1 1) (("2" (lift-if) (("2" (ground) (("1" (case "s`x < 0") (("1" (div-by -5 "-s`x") (("1" (assert) (("1" (expand "sign") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (lemma "nnreal_times_nnreal_is_nnreal") (("2" (inst - "s`x" "w`x") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (case "s`x > 0") (("1" (div-by -4 "s`x") (("1" (expand "sign") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "nnreal_times_nnreal_is_nnreal") (("2" (inst - "-s`x" "-w`x") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "chiv = zero") (("1" (case "norm(chiv) = norm(nvoa-vi)") (("1" (replace -2) (("1" (assert) nil nil)) nil) ("2" (expand "chiv" 1) (("2" (rewrite "norm_id") nil nil)) nil)) nil) ("2" (decompose-equality) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "nvoa-vi = zero") (("1" (hide-all-but (-1 -16)) (("1" (expand "ch") (("1" (expand "chi_hc") (("1" (ground) (("1" (expand "nvoa" -1) (("1" (expand "ch" -1) (("1" (expand "chi_hc" -1) (("1" (assert) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "w" "nvoa-vi") (("2" (replace -1) (("2" (decompose-equality 1) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "chiv" 1) (("2" (expand "trkgs2vect" 1) (("2" (expand "*" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-12 1)) (("2" (expand "ch") (("2" (expand "chi_hc" -1) (("2" (ground) (("2" (expand "nvoa") (("2" (expand "ch") (("2" (expand "chi_hc") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "chirel_star_tangent") (("2" (lemma "line_solution_sep_dot_negative") (("2" (inst - "eps" "s" "chiv") (("2" (assert) (("2" (inst - "eps" "norm(nvoa-vi)" "s" "vo-vi") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "norm_eq_0") (("2" (inst - "nvoa-vi") (("2" (assert) (("2" (hide-all-but (-11 -1)) (("2" (expand "ch") (("2" (expand "chi_hc") (("2" (ground) (("2" (expand "nvoa") (("2" (expand "ch") (("2" (expand "chi_hc") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "chiv" "trkgs2vect(chirela,norm(nvoa-vi))") (("1" (flatten) (("1" (case "track(chiv) = chirela") (("1" (lemma "norm_id") (("1" (inst - "norm(nvoa-vi)" "chirela") (("1" (case "norm(nvoa-vi) > 0") (("1" (case "chiv /= zero") (("1" (expand "trkgs2vect" -5) (("1" (expand "*") (("1" (replace -6) (("1" (replace -7) (("1" (assert) (("1" (expand "zero") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "norm_eq_0") (("2" (inst - "chiv") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "norm_eq_0") (("2" (inst - "nvoa-vi") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "chiv" +) (("2" (rewrite "track_id") (("2" (rewrite "to2pi_id") nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) (("2" (hide-all-but (-1 -9)) (("2" (expand "ch") (("2" (expand "chi_hc") (("2" (ground) (("2" (expand "nvoa") (("2" (expand "ch") (("2" (expand "chi_hc") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((chi_hc const-decl "[nnreal_lt_2pi, bool]" kb nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Ss_vect2 type-eq-decl nil horizontal nil) (D formal-const-decl "posreal" kb nil) (sq const-decl "nonneg_real" sq "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nzint nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (= const-decl "[T, T -> boolean]" equalities 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) (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) (chi_hc_sin_equivalence_2 formula-decl nil kb nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (chiv skolem-const-decl "Nz_vect2" kb nil) (* const-decl "real" vectors_2D "vectors/") (nnreal_times_nnreal_is_nnreal judgement-tcc nil real_types nil) (minus_real_is_real application-judgement "real" reals nil) (both_sides_div_pos_lt1 formula-decl nil real_props nil) (s skolem-const-decl "Ss_vect2[D]" kb nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (times_div_cancel1 formula-decl nil extra_real_props nil) (atan2 const-decl "real" atan2 "trig_fnd/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (w skolem-const-decl "Vector" kb nil) (chiv skolem-const-decl "Nz_vect2" kb nil) (sign const-decl "Sign" sign "reals/") (norm_zero formula-decl nil vectors_2D "vectors/") (comp_zero_y formula-decl nil vectors_2D "vectors/") (comp_zero_x formula-decl nil vectors_2D "vectors/") (both_sides_times1 formula-decl nil real_props nil) (chirela skolem-const-decl "nnreal_lt_2pi" kb nil) (both_sides_div1 formula-decl nil real_props nil) (sub_eq_args formula-decl nil vectors_2D "vectors/") (trkgs2vect_id formula-decl nil track nil) (dot_zero_right formula-decl nil vectors_2D "vectors/") (norm_eq_0 formula-decl nil vectors_2D "vectors/") (XB skolem-const-decl "nnreal_lt_2pi" kb nil) (norm_id formula-decl nil track nil) (nvoa skolem-const-decl "Nz_vect2" kb nil) (vx_distr_sub formula-decl nil vectors_2D "vectors/") (sin_track formula-decl nil track nil) (XA skolem-const-decl "nnreal_lt_2pi" kb nil) (chi_hc_track_eq formula-decl nil kb nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (line_solution_sep_dot_negative formula-decl nil line_solutions nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (chirel_star_tangent formula-decl nil kb nil) (Sp_vect2 type-eq-decl nil horizontal nil) (ch skolem-const-decl "[nnreal_lt_2pi, bool]" kb nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (* const-decl "Vector" vectors_2D "vectors/") (nzreal_times_nzreal_is_nzreal judgement-tcc nil real_types nil) (nzreal nonempty-type-eq-decl nil reals nil) (vi skolem-const-decl "Nz_vect2" kb nil) (track_id formula-decl nil track nil) (to2pi_id formula-decl nil to2pi "trig_fnd/") (chiv skolem-const-decl "Nz_vect2" kb nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (cos_track formula-decl nil track nil) (vy_distr_sub formula-decl nil vectors_2D "vectors/") (div_cancel3 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (times_div2 formula-decl nil real_props nil) (div_cancel4 formula-decl nil real_props nil) (sin const-decl "real" sincos_def "trig_fnd/") (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (tan const-decl "real" sincos_def "trig_fnd/") (Tan? const-decl "bool" sincos_def "trig_fnd/") (NOT const-decl "[bool -> bool]" booleans nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (cos const-decl "real" sincos_def "trig_fnd/") (cos_range application-judgement "trig_range" sincos_def "trig_fnd/") (sin_minus formula-decl nil trig_basic "trig_fnd/") (track const-decl "nnreal_lt_2pi" track nil) (norm const-decl "nnreal" vectors_2D "vectors/") (trkgs2vect const-decl "Nz_vect2" track nil) (- const-decl "Vector" vectors_2D "vectors/") (chirel_star const-decl "nnreal_lt_2pi" kb 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/") (sin_range application-judgement "trig_range" sincos_def "trig_fnd/") (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (chi_hc_f_chirel_TCC1 0 (chi_hc_f_chirel_TCC1-1 nil 3483106756 ("" (skeep) (("" (expand "chi_hc") (("" (lift-if) (("" (lift-if) (("" (lift-if) (("" (ground) (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nz_norm_gt_0 application-judgement "posreal" vectors_2D "vectors/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sin_range application-judgement "trig_range" sincos_def "trig_fnd/") (real_times_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/") (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (chi_hc const-decl "[nnreal_lt_2pi, bool]" kb nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_ge_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) (dot_zero_right formula-decl nil vectors_2D "vectors/")) nil)) (chi_hc_f_chirel_TCC2 0 (chi_hc_f_chirel_TCC2-1 nil 3483106756 ("" (subtype-tcc) nil 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) (/= const-decl "boolean" notequal 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nzint nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq "reals/") (posreal nonempty-type-eq-decl nil real_types nil) (D formal-const-decl "posreal" kb nil) (Ss_vect2 type-eq-decl nil horizontal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (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) (sq_nz_pos application-judgement "posreal" sq "reals/") (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_gt_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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (chi_hc const-decl "[nnreal_lt_2pi, bool]" kb nil) (* const-decl "real" vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (chi_hc_f_chirel 0 (chi_hc_f_chirel-1 nil 3483106782 ("" (skeep) (("" (label "dotneg" -1) (("" (hide "dotneg") (("" (name "ch" "chi_hc(f,eps,irt)(s,vo,vi)") (("" (replace -1) (("" (lemma "chi_hc_sin_equivalence_2") (("" (inst?) (("" (replace -2) (("" (assert) (("" (assert) (("" (name "chirela" "chirel_star(s,vo-vi,f,eps)") (("" (replace -1) (("" (name "nvoa" "trkgs2vect(ch`1, norm(vo))") (("" (replace -1) (("" (rewrite "sin_minus") (("" (rewrite "sin_minus") (("" (name "XA" "track(nvoa)") (("" (replace -1) (("" (name "XB" "track(vi)") (("" (replace -1) (("" (case "cos(chirela) /= 0") (("1" (label "chirelanz" -1) (("1" (case "norm(vo)*cos(XA)-norm(vi)*cos(XB) /= 0") (("1" (label "Xnz" -1) (("1" (case "nvoa-vi /= zero") (("1" (label "relnz" -1) (("1" (case "norm(nvoa-vi) > 0") (("1" (label "relnorm" -1) (("1" (hide "relnorm") (("1" (hide "relnz") (("1" (case "NOT tan(chirela) = (norm(vo)*sin(XA) - norm(vi)*sin(XB))/(norm(vo)*cos(XA)-norm(vi)* (("1" (hide 2) (("1" (expand "tan" 1) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (case "NOT (norm(vo) * sin(XA) - norm(vi) * sin(XB)) = (nvoa-vi)`x") (("1" (expand "XA" +) (("1" (expand "XB" +) (("1" (rewrite "sin_track" +) (("1" (rewrite "sin_track" +) (("1" (rewrite "vx_distr_sub") (("1" (case "norm(nvoa) = norm(vo)") (("1" (replace -1 1) (("1" (assert) nil nil)) nil) ("2" (expand "nvoa" 1) (("2" (rewrite "norm_id") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT (norm(vo) * cos(XA) - norm(vi) * cos(XB)) = (nvoa-vi)`y") (("1" (expand "XA" +) (("1" (expand "XB" +) (("1" (rewrite "cos_track" 1) (("1" (rewrite "cos_track" 1) (("1" (case "norm(nvoa) = norm(vo)") (("1" (rewrite "vy_distr_sub") (("1" (assert) nil nil)) nil) ("2" (expand "nvoa" 1) (("2" (rewrite "norm_id") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (replace -2) (("2" (hide -1) (("2" (hide -1) (("2" (expand "tan" -1) (("2" (name "chiv" "trkgs2vect(chirela,norm(nvoa-vi))") (("1" (lemma "chi_hc_track_eq") (("1" (inst - "s" "nvoa-vi" "chiv") (("1" (assert) (("1" (split -) (("1" (replace -1 +) (("1" (expand "chiv" +) (("1" (rewrite "track_id") (("1" (typepred "chirela") (("1" (rewrite "to2pi_id") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "chiv" +) (("2" (expand "trkgs2vect" +) (("2" (expand "*" +) (("2" (reveal "relnorm") (("2" (lemma "nzreal_times_nzreal_is_nzreal") (("2" (inst - "norm(nvoa-vi)" "cos(chirela)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (replace -2 + :dir rl) (("3" (expand "chiv" +) (("3" (expand "trkgs2vect" +) (("3" (expand "*") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (expand "ch" -11) (("4" (hide-all-but (-11 -7 1)) (("4" (expand "ch") (("4" (expand "chi_hc") (("4" (lift-if) (("4" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (lemma "chirel_star_f_entry") (("5" (inst?) (("5" (inst - "norm(nvoa-vi)") (("5" (assert) (("5" (reveal "dotneg") (("5" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (reveal "relnorm") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil) ("4" (expand "Tan?") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-9 -5 1)) (("2" (expand "ch") (("2" (expand "chi_hc" -2) (("2" (ground) (("2" (expand "chi_hc" -) (("2" (replace -2) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT norm(vi)*sin(XB) = norm(vo)*sin(XA)") (("1" (flatten) (("1" (case "NOT cos(chirela)*norm(vi)*sin(XB) = cos(chirela)*norm(vo)*sin(XA)") (("1" (assert) nil nil) ("2" (div-by -1 "cos(chirela)") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "nvoa=vi") (("1" (hide-all-but (-1 -10 -6)) (("1" (expand "ch") (("1" (expand "chi_hc") (("1" (lift-if) (("1" (ground) (("1" (replace -1) (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "trkgs2vect_id") (("2" (inst - "vi") (("2" (lemma "trkgs2vect_id") (("2" (inst - "nvoa") (("2" (case "norm(nvoa) = norm(vo)") (("1" (replace -1) (("1" (hide -1) (("1" (replace -1 1 :dir rl) (("1" (replace -2 1 :dir rl) (("1" (expand "trkgs2vect" 1) (("1" (expand "*" +) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nvoa" 1) (("2" (rewrite "norm_id") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (assert) (("2" (case "sin(chirela) /= 0") (("1" (flatten) (("1" (case "NOT norm(vi)*cos(XB) = norm(vo)*cos(XA)") (("1" (mult-by 1 "sin(chirela)") (("1" (assert) nil nil)) nil) ("2" (case "NOT (nvoa - vi)`y = 0") (("1" (lemma "trkgs2vect_id") (("1" (inst-cp - "nvoa") (("1" (inst - "vi") (("1" (replace -1 1 :dir rl) (("1" (case "norm(nvoa) = norm(vo)") (("1" (replace -1) (("1" (replace -3 1 :dir rl) (("1" (rewrite "vy_distr_sub") (("1" (expand "trkgs2vect" 1) (("1" (expand "*" +) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nvoa" +) (("2" (rewrite "norm_id") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "chiv" "trkgs2vect(chirela,norm(nvoa-vi))") (("1" (case "s*chiv < 0") (("1" (case "s*(nvoa-vi) < 0") (("1" (case "chiv`y = 0") (("1" (case "(nvoa-vi)`x /= 0") (("1" (case "chiv`x /= 0") (("1" (case "sign((nvoa-vi)`x) = sign(chiv`x)") (("1" (case "chirela = track(chiv)") (("1" (replace -1 2) (("1" (hide -1) (("1" --> -------------------- --> maximum size reached --> --------------------
¤ Dauer der Verarbeitung: 0.800 Sekunden (vorverarbeitet am 2026-05-05) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26