| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/trig/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 161 kB |
|
SSL trig_extra.prf Sprache: Lisp |
|||||||||
|
(trig_extra
(sin_minus_2pi 0 (sin_minus_2pi-1 nil 3269431996 ("" (skosimp) (("" (rewrite "sin_minus") (("" (rewrite "sin_2pi") (("" (rewrite "cos_2pi") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sin_minus formula-decl nil trig_basic 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) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (cos_range application-judgement "trig_range" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (cos_2pi formula-decl nil trig_basic nil) (sin_2pi formula-decl nil trig_basic nil)) nil)) (cos_minus_2pi 0 (cos_minus_2pi-1 nil 3269431996 ("" (skosimp) (("" (rewrite "cos_minus") (("" (rewrite "cos_2pi") (("" (rewrite "sin_2pi") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_minus formula-decl nil trig_basic 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) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sin_2pi formula-decl nil trig_basic nil) (cos_2pi formula-decl nil trig_basic nil)) nil)) (tan_minus_2pi_TCC1 0 (tan_minus_2pi_TCC1-1 nil 3269431996 ("" (skosimp) (("" (expand "Tan?") (("" (rewrite "cos_minus_2pi") (("" (assert) nil nil)) nil)) nil)) nil) ((Tan? const-decl "bool" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (minus_even_is_even application-judgement "even_int" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types 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) (cos_minus_2pi formula-decl nil trig_extra nil)) nil)) (tan_minus_2pi_TCC2 0 (tan_minus_2pi_TCC2-1 nil 3269431996 ("" (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) (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 "boolean" notequal nil) (Tan? const-decl "bool" trig_basic nil)) nil)) (tan_minus_2pi 0 (tan_minus_2pi-1 nil 3269431996 ("" (skosimp) (("" (expand "tan") (("" (rewrite "sin_minus_2pi") (("" (rewrite "cos_minus_2pi") nil nil)) nil)) nil)) nil) ((tan const-decl "real" trig_basic nil) (cos_minus_2pi formula-decl nil trig_extra nil) (sin_range application-judgement "trig_range" trig_basic nil) (minus_even_is_even application-judgement "even_int" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (cos_range application-judgement "trig_range" trig_basic nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types 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) (sin_minus_2pi formula-decl nil trig_extra nil)) nil)) (sin_minus_3pi2 0 (sin_minus_3pi2-1 nil 3269431996 ("" (skosimp) (("" (rewrite "sin_minus") (("" (rewrite "sin_3pi2") (("" (rewrite "cos_3pi2") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sin_minus formula-decl nil trig_basic 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) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (cos_3pi2 formula-decl nil trig_basic nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sin_3pi2 formula-decl nil trig_basic nil)) nil)) (cos_minus_3pi2 0 (cos_minus_3pi2-1 nil 3269431996 ("" (skosimp) (("" (rewrite "cos_minus") (("" (rewrite "cos_3pi2") (("" (rewrite "sin_3pi2") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_minus formula-decl nil trig_basic 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) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sin_3pi2 formula-decl nil trig_basic nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (cos_3pi2 formula-decl nil trig_basic nil)) nil)) (tan_minus_3pi2_TCC1 0 (tan_minus_3pi2_TCC1-1 nil 3269431996 ("" (expand "Tan?") (("" (skosimp*) (("" (lemma "sin_shift" ("a" "a!1-3*pi/2")) (("" (lemma "sin_period" ("a" "-a!1" "j" "1")) (("" (rewrite "sin_neg" -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((minus_real_is_real application-judgement "real" reals nil) (sin_period formula-decl nil trig_basic nil) (- const-decl "[numfield -> numfield]" number_fields 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) (integer nonempty-type-from-decl nil integers nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_plus_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (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) (posint_times_posint_is_posint application-judgement "posint" integers nil) (sin_neg formula-decl nil trig_basic nil) (real_minus_real_is_real application-judgement "real" reals nil) (sin_shift formula-decl nil trig_basic 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (Tan? const-decl "bool" trig_basic nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil)) nil)) (tan_minus_3pi2_TCC2 0 (tan_minus_3pi2_TCC2-1 nil 3269431996 ("" (skosimp) (("" (expand "tan") (("" (lemma "div_eq_zero") (("" (inst -1 "cos(a!1)" "sin(a!1)") (("1" (replace -1 * lr) (("1" (propax) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((tan const-decl "real" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic 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) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (cos const-decl "real" trig_basic nil) (sin const-decl "real" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (div_eq_zero formula-decl nil real_props nil)) nil)) (tan_minus_3pi2 0 (tan_minus_3pi2-1 nil 3269431996 ("" (skosimp) (("" (expand "tan") (("" (rewrite "sin_minus_3pi2") (("" (rewrite "cos_minus_3pi2") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (tan const-decl "real" trig_basic nil) (cos_minus_3pi2 formula-decl nil trig_extra nil) (minus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (minus_odd_is_odd application-judgement "odd_int" integers 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) (sin_minus_3pi2 formula-decl nil trig_extra nil)) nil)) (sin_minus_pi 0 (sin_minus_pi-1 nil 3269431996 ("" (skosimp) (("" (rewrite "sin_minus") (("" (rewrite "sin_pi") (("" (rewrite "cos_pi") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((sin_minus formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cos_range application-judgement "trig_range" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (cos_pi formula-decl nil trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (sin_pi formula-decl nil trig_basic nil)) nil)) (cos_minus_pi 0 (cos_minus_pi-1 nil 3269431996 ("" (skosimp) (("" (rewrite "cos_minus") (("" (rewrite "cos_pi") (("" (rewrite "sin_pi") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((cos_minus formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sin_pi formula-decl nil trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (cos_pi formula-decl nil trig_basic nil)) nil)) (tan_minus_pi_TCC1 0 (tan_minus_pi_TCC1-1 nil 3269431996 ("" (skosimp*) (("" (expand "Tan?") (("" (lemma "neg_cos" ("a" "a!1-pi")) (("" (assert) nil nil)) nil)) nil)) nil) ((Tan? const-decl "bool" trig_basic nil) (real_plus_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (neg_cos formula-decl nil trig_basic 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil)) nil)) (tan_minus_pi 0 (tan_minus_pi-1 nil 3269431996 ("" (skosimp) (("" (expand "tan") (("" (rewrite "sin_minus_pi") (("" (rewrite "cos_minus_pi") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((tan const-decl "real" trig_basic nil) (cos_minus_pi formula-decl nil trig_extra nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cos_range application-judgement "trig_range" trig_basic 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) (sin_minus_pi formula-decl nil trig_extra nil)) nil)) (sin_minus_pi2 0 (sin_minus_pi2-1 nil 3269431996 ("" (skosimp) (("" (rewrite "sin_minus") (("" (rewrite "cos_pi2") (("" (rewrite "sin_pi2") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sin_minus formula-decl nil trig_basic 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) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (sin_pi2 formula-decl nil trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (cos_pi2 formula-decl nil trig_basic nil)) nil)) (cos_minus_pi2 0 (cos_minus_pi2-1 nil 3269431996 ("" (skosimp) (("" (rewrite "cos_minus") (("" (rewrite "cos_pi2") (("" (rewrite "sin_pi2") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_minus formula-decl nil trig_basic 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) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sin_pi2 formula-decl nil trig_basic nil) (cos_pi2 formula-decl nil trig_basic nil)) nil)) (tan_minus_pi2_TCC1 0 (tan_minus_pi2_TCC1-1 nil 3269431996 ("" (skolem 1 ("a")) (("" (flatten) (("" (expand "Tan?") (("" (lemma "cos_neg" ("a" "a-pi/2")) (("" (lemma "cos_shift" ("a" "a")) (("" (replace -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (cos_neg formula-decl nil trig_basic nil) (real_minus_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_shift formula-decl nil trig_basic nil) (Tan? const-decl "bool" trig_basic nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) nil)) (tan_minus_pi2 0 (tan_minus_pi2-1 nil 3269431996 ("" (skosimp) (("" (expand "tan") (("" (rewrite "sin_minus_pi2") (("" (rewrite "cos_minus_pi2") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (tan const-decl "real" trig_basic nil) (cos_minus_pi2 formula-decl nil trig_extra nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (minus_odd_is_odd application-judgement "odd_int" integers 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) (sin_minus_pi2 formula-decl nil trig_extra nil)) nil)) (sin_2pi_minus 0 (sin_2pi_minus-1 nil 3269431996 ("" (skosimp) (("" (rewrite "sin_minus") (("" (rewrite "sin_2pi") (("" (rewrite "cos_2pi") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sin_minus formula-decl nil trig_basic 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) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (cos_2pi formula-decl nil trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (sin_2pi formula-decl nil trig_basic nil)) nil)) (cos_2pi_minus 0 (cos_2pi_minus-1 nil 3269431996 ("" (skosimp) (("" (rewrite "cos_minus") (("" (rewrite "cos_2pi") (("" (rewrite "sin_2pi") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_minus formula-decl nil trig_basic 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) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sin_2pi formula-decl nil trig_basic nil) (cos_2pi formula-decl nil trig_basic nil)) nil)) (tan_2pi_minus_TCC1 0 (tan_2pi_minus_TCC1-1 nil 3269431996 ("" (skosimp) (("" (expand "Tan?") (("" (rewrite "cos_2pi_minus") (("" (assert) nil nil)) nil)) nil)) nil) ((Tan? const-decl "bool" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types 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) (cos_2pi_minus formula-decl nil trig_extra nil)) nil)) (tan_2pi_minus 0 (tan_2pi_minus-1 nil 3269431996 ("" (skosimp) (("" (expand "tan") (("" (rewrite "sin_2pi_minus") (("" (rewrite "cos_2pi_minus") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((tan const-decl "real" trig_basic nil) (cos_2pi_minus formula-decl nil trig_extra nil) (minus_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types 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) (sin_2pi_minus formula-decl nil trig_extra nil)) nil)) (sin_3pi2_minus 0 (sin_3pi2_minus-1 nil 3269431996 ("" (skosimp) (("" (rewrite "sin_minus") (("" (rewrite "sin_3pi2") (("" (rewrite "cos_3pi2") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sin_minus formula-decl nil trig_basic 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) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (cos_3pi2 formula-decl nil trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sin_3pi2 formula-decl nil trig_basic nil)) nil)) (cos_3pi2_minus 0 (cos_3pi2_minus-1 nil 3269431996 ("" (skosimp) (("" (rewrite "cos_minus") (("" (rewrite "cos_3pi2") (("" (rewrite "sin_3pi2") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_minus formula-decl nil trig_basic 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) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sin_3pi2 formula-decl nil trig_basic nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (cos_3pi2 formula-decl nil trig_basic nil)) nil)) (tan_3pi2_minus_TCC1 0 (tan_3pi2_minus_TCC1-1 nil 3269431996 ("" (skosimp*) (("" (expand "Tan?") (("" (lemma "cos_sin" ("a" "3*pi/2-a!1")) (("" (lemma "sin_period" ("a" "-a!1" "j" "1")) (("" (replace -1 -2 rl) (("" (rewrite "sin_neg" -2) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (Tan? const-decl "bool" trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (sin_period formula-decl nil trig_basic nil) (- const-decl "[numfield -> numfield]" number_fields 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) (integer nonempty-type-from-decl nil integers nil) (sin_neg formula-decl nil trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_plus_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (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) (posint_times_posint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (cos_sin formula-decl nil trig_basic 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil)) nil)) (tan_3pi2_minus 0 (tan_3pi2_minus-1 nil 3269431996 ("" (skosimp) (("" (expand "tan") (("" (rewrite "sin_3pi2_minus") (("" (rewrite "cos_3pi2_minus") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (tan const-decl "real" trig_basic nil) (cos_3pi2_minus formula-decl nil trig_extra nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types 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) (sin_3pi2_minus formula-decl nil trig_extra nil)) nil)) (sin_pi_minus 0 (sin_pi_minus-1 nil 3269431996 ("" (skosimp) (("" (rewrite "sin_minus") (("" (rewrite "sin_pi") (("" (rewrite "cos_pi") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((sin_minus formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (cos_pi formula-decl nil trig_basic nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sin_pi formula-decl nil trig_basic nil)) nil)) (cos_pi_minus 0 (cos_pi_minus-1 nil 3269431996 ("" (skosimp) (("" (rewrite "cos_minus") (("" (rewrite "cos_pi") (("" (rewrite "sin_pi") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((cos_minus formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sin_pi formula-decl nil trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cos_pi formula-decl nil trig_basic nil)) nil)) (tan_pi_minus_TCC1 0 (tan_pi_minus_TCC1-1 nil 3269431996 ("" (skosimp*) (("" (expand "Tan?") (("" (lemma "neg_cos" ("a" "-a!1")) (("" (rewrite "cos_neg" -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((Tan? const-decl "bool" trig_basic nil) (cos_neg formula-decl nil trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (neg_cos formula-decl nil trig_basic 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil)) nil)) (tan_pi_minus 0 (tan_pi_minus-1 nil 3269431996 ("" (skosimp) (("" (expand "tan") (("" (rewrite "sin_pi_minus") (("" (rewrite "cos_pi_minus") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((tan const-decl "real" trig_basic nil) (cos_pi_minus formula-decl nil trig_extra nil) (minus_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic 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) (sin_pi_minus formula-decl nil trig_extra nil)) nil)) (sin_pi2_minus 0 (sin_pi2_minus-1 nil 3269431996 ("" (skosimp) (("" (rewrite "sin_minus") (("" (rewrite "sin_pi2") (("" (rewrite "cos_pi2") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sin_minus formula-decl nil trig_basic 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) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (cos_pi2 formula-decl nil trig_basic nil) (sin_pi2 formula-decl nil trig_basic nil)) nil)) (cos_pi2_minus 0 (cos_pi2_minus-1 nil 3269431996 ("" (skosimp) (("" (rewrite "cos_minus") (("" (rewrite "cos_pi2") (("" (rewrite "sin_pi2") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_minus formula-decl nil trig_basic 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) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sin_pi2 formula-decl nil trig_basic nil) (cos_pi2 formula-decl nil trig_basic nil)) nil)) (tan_pi2_minus_TCC1 0 (tan_pi2_minus_TCC1-1 nil 3269431996 ("" (skosimp*) (("" (expand "Tan?") (("" (lemma "sin_cos" ("a" "-a!1")) (("" (rewrite "sin_neg" -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((Tan? const-decl "bool" trig_basic nil) (sin_neg formula-decl nil trig_basic nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_range application-judgement "trig_range" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (sin_cos formula-decl nil trig_basic 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil)) nil)) (tan_pi2_minus 0 (tan_pi2_minus-1 nil 3269431996 ("" (skosimp) (("" (expand "tan") (("" (rewrite "sin_pi2_minus") (("" (rewrite "cos_pi2_minus") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((tan const-decl "real" trig_basic nil) (cos_pi2_minus formula-decl nil trig_extra nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types 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) (sin_pi2_minus formula-decl nil trig_extra nil)) nil)) (sin_times_cos 0 (sin_times_cos-1 nil 3269431996 ("" (skosimp) (("" (rewrite "sin_plus") (("" (rewrite "sin_minus") (("" (assert) nil nil)) nil)) nil)) nil) ((sin_plus formula-decl nil trig_basic 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cos_range application-judgement "trig_range" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (sin_minus formula-decl nil trig_basic nil)) nil)) (cos_times_cos 0 (cos_times_cos-1 nil 3269431996 ("" (skosimp) (("" (rewrite "cos_plus") (("" (rewrite "cos_minus") (("" (assert) nil nil)) nil)) nil)) nil) ((cos_plus formula-decl nil trig_basic 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) (real_plus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (cos_minus formula-decl nil trig_basic nil)) nil)) (sin_times_sin 0 (sin_times_sin-1 nil 3269431996 ("" (skosimp) (("" (rewrite "cos_plus") (("" (rewrite "cos_minus") (("" (assert) nil nil)) nil)) nil)) nil) ((cos_plus formula-decl nil trig_basic 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (cos_minus formula-decl nil trig_basic nil)) nil)) (sin_sum 0 (sin_sum-1 nil 3269431996 ("" (skosimp*) (("" (lemma "sin_plus" ("a" "(a!1+b!1)/2" "b" "(a!1-b!1)/2")) (("" (lemma "sin_minus" ("a" "(a!1+b!1)/2" "b" "(a!1-b!1)/2")) (("" (assert) nil nil)) nil)) nil)) nil) ((- const-decl "[numfield, numfield -> numfield]" number_fields 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) (numfield nonempty-type-eq-decl nil number_fields 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) (sin_plus formula-decl nil trig_basic nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (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) (sin_range application-judgement "trig_range" trig_basic nil) (sin_minus formula-decl nil trig_basic nil)) nil)) (sin_diff 0 (sin_diff-1 nil 3269431996 ("" (skosimp*) (("" (lemma "sin_plus" ("a" "(a!1+b!1)/2" "b" "(a!1-b!1)/2")) (("" (lemma "sin_minus" ("a" "(a!1+b!1)/2" "b" "(a!1-b!1)/2")) (("" (assert) nil nil)) nil)) nil)) nil) ((- const-decl "[numfield, numfield -> numfield]" number_fields 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) (numfield nonempty-type-eq-decl nil number_fields 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) (sin_plus formula-decl nil trig_basic nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (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) (sin_range application-judgement "trig_range" trig_basic nil) (sin_minus formula-decl nil trig_basic nil)) nil)) (cos_sum 0 (cos_sum-1 nil 3269431996 ("" (skosimp*) (("" (lemma "cos_plus" ("a" "(a!1+b!1)/2" "b" "(a!1-b!1)/2")) (("" (lemma "cos_minus" ("a" "(a!1+b!1)/2" "b" "(a!1-b!1)/2")) (("" (assert) (("" (replace -1) (("" (replace -2) (("" (assert) (("" (name-replace "K1" "cos((a!1 + b!1) / 2)") (("" (name-replace "K2" "cos((a!1 - b!1) / 2)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((- const-decl "[numfield, numfield -> numfield]" number_fields 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) (numfield nonempty-type-eq-decl nil number_fields 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) (cos_plus formula-decl nil trig_basic nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (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) (cos_range application-judgement "trig_range" trig_basic nil) (trig_range type-eq-decl nil trig_basic nil) (- const-decl "[numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (cos const-decl "real" trig_basic nil) (= const-decl "[T, T -> boolean]" equalities nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cos_minus formula-decl nil trig_basic nil)) nil)) (cos_diff 0 (cos_diff-1 nil 3269431996 ("" (skosimp*) (("" (lemma "cos_plus" ("a" "(a!1+b!1)/2" "b" "(a!1-b!1)/2")) (("" (lemma "cos_minus" ("a" "(a!1+b!1)/2" "b" "(a!1-b!1)/2")) (("" (replace -1) (("" (replace -2) (("" (assert) (("" (name-replace "K1" "sin((a!1 + b!1) / 2)") (("" (name-replace "K2" "sin((a!1 - b!1) / 2)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((- const-decl "[numfield, numfield -> numfield]" number_fields 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) (numfield nonempty-type-eq-decl nil number_fields 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) (cos_plus formula-decl nil trig_basic nil) (real_div_nzreal_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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cos_range application-judgement "trig_range" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (sin const-decl "real" trig_basic nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (trig_range type-eq-decl nil trig_basic nil) (cos_minus formula-decl nil trig_basic nil)) nil)) (tan_diff_TCC1 0 (tan_diff_TCC1-1 nil 3269431996 ("" (skosimp*) (("" (expand "Tan?") (("" (rewrite "zero_times3") (("" (ground) nil nil)) nil)) nil)) nil) ((Tan? const-decl "bool" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (cos const-decl "real" trig_basic nil) (real nonempty-type-from-decl nil reals nil) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.69 Sekunden (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28