| products/Sources/formale Sprachen/PVS/ACCoRD/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: kb.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(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)") --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.68 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
