| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/trig/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 MB |
|
SSL sincos_def.prfInteraktion undPortierbarkeitLisp |
|||||||||||||||
|
(sincos_def (cos_ub 0 (cos_ub-1 nil 3265619589 ("" (skosimp*) (("" (typepred "cos(x!1)") (("" (propax) nil nil)) nil)) nil) ((cos const-decl "real" trig_basic nil) (- const-decl "[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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (cos_range application-judgement "trig_range" trig_basic nil)) shostak)) (sin_ub 0 (sin_ub-2 nil 3307184568 ("" (skolem 1 ("px")) (("" (case "px<=1") (("1" (expand "sin") (("1" (lemma "floor_def" ("x" "px/(2*pi)")) (("1" (rewrite "div_mult_pos_lt1") (("1" (rewrite "div_mult_pos_le2") (("1" (flatten) (("1" (lemma "trichotomy" ("x" "floor(px / (2 * pi))")) (("1" (split -1) (("1" (case "floor(px / (2 * pi)) =1") (("1" (lemma "pi_bnds") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (case "floor(px / (2 * pi))>1") (("1" (lemma "pi_bnds") (("1" (flatten) (("1" (assert) (("1" (lemma "both_sides_times_pos_lt1" ("x" "1" "y" "floor(px / (2 * pi))" "pz" "2*pi")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1 -2 -3) (("2" (simplify 1) (("2" (lemma "pi_bnds") (("2" (flatten) (("2" (lemma "phases_sin" ("x" "px")) (("2" (split -1) (("1" (rewrite "sin_q1") (("1" (hide -1) (("1" (lemma "sin_value_derivable2") (("1" (lemma "deriv_sin_value") (("1" (lemma "identity_derivable_fun[real_abs_lt_pi]") (("1" (lemma "deriv_id_fun[real_abs_lt_pi]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "diff_derivable_fun" ("f1" "LAMBDA (x: real_abs_lt_pi): x" "f2" "LAMBDA (x: real_abs_lt_pi): sin_value(x)")) (("1" (lemma "deriv_diff_fun" ("ff1" "LAMBDA (x: real_abs_lt_pi): x" "ff2" "LAMBDA (x: real_abs_lt_pi): sin_value(x)")) (("1" (replace -3 -1) (("1" (replace -5 -1) (("1" (expand "-") (("1" (assert) (("1" (lemma "identity_derivable_fun[{x:nnreal|x<pi/2}]") (("1" (lemma "deriv_id_fun[{x:nnreal|x<pi/2}]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "composition_derivable_fun[{x: nnreal | x < pi / 2},real_abs_lt_pi]" ("f" "LAMBDA (x: {x: nnreal | x < pi / 2}): x" "g" "LAMBDA (x_1: real_abs_lt_pi): x_1 - sin_value(x_1)")) (("1" (replace -3) (("1" (replace -5) (("1" (expand "o") (("1" (lemma "deriv_comp_fun[{x: nnreal | x < pi / 2},real_abs_lt_pi]" ("ff" "LAMBDA (x: {x: nnreal | x < pi / 2}): x" "gg" "LAMBDA (x_1: real_abs_lt_pi): x_1 - sin_value(x_1)")) (("1" (expand "o") (("1" (replace -3 -1) (("1" (replace -5 -1) (("1" (expand "*" -1) (("1" (lemma "minimum_derivative[{x: nnreal | x < pi / 2}]" ("g" "LAMBDA (x_1: {x: nnreal | x < pi / 2}): x_1 - sin_value(x_1)" "x" "0" "y1" "px")) (("1" (split -1) (("1" (simplify -1) (("1" (rewrite "sin_value_0") (("1" (assert) nil nil)) nil)) nil) ("2" (replace -1 1) (("2" (assert) (("2" (expand "abs") (("2" (rewrite "cos_value_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil) ("4" (replace -1 1) (("4" (hide-all-but 1) (("4" (skosimp*) (("4" (expand "abs") (("4" (lemma "cos_value_strict_decreasing") (("4" (expand "strict_decreasing?") (("4" (inst - "0" "y!1") (("4" (rewrite "cos_value_0") (("4" (assert) (("4" (lemma "posreal_times_posreal_is_posreal" ("px" "1-cos_value(y!1)" "py" "y!1")) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (skosimp*) (("3" (assert) (("3" (expand "abs") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=0") (("1" (inst + "pi/4") (("1" (assert) nil nil)) nil) ("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (typepred "x!1") (("3" (typepred "y!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=0") (("1" (inst + "pi/4") (("1" (assert) nil nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil) ("2" (inst + "0") (("1" (assert) nil nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (typepred "x!1") (("3" (typepred "y!1") (("3" (name-replace "K1" "pi/2") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "phase_sin_q2") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil) ("3" (rewrite "phase_sin_q3") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil) ("4" (rewrite "phase_sin_q4") (("4" (flatten) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "sin(px)") (("2" (assert) nil nil)) nil)) nil)) nil) nil nil) (sin_ub-1 nil 3265693281 ("" (skolem 1 ("px")) (("" (case "px<=1") (("1" (expand "sin") (("1" (lemma "floor_def" ("x" "px/(2*pi)")) (("1" (rewrite "div_mult_pos_lt1") (("1" (rewrite "div_mult_pos_le2") (("1" (flatten) (("1" (lemma "trichotomy" ("x" "floor(px / (2 * pi))")) (("1" (split -1) (("1" (case "floor(px / (2 * pi)) =1") (("1" (lemma "pi_bnds") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (case "floor(px / (2 * pi))>1") (("1" (lemma "pi_bnds") (("1" (flatten) (("1" (assert) (("1" (lemma "both_sides_times_pos_lt1" ("x" "1" "y" "floor(px / (2 * pi))" "pz" "2*pi")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1 -2 -3) (("2" (simplify 1) (("2" (lemma "pi_bnds") (("2" (flatten) (("2" (lemma "phases_sin" ("x" "px")) (("1" (split -1) (("1" (rewrite "sin_q1") (("1" (hide -1) (("1" (lemma "sin_value_derivable2") (("1" (lemma "deriv_sin_value") (("1" (lemma "identity_derivable_fun[real_abs_lt_pi]") (("1" (lemma "deriv_id_fun[real_abs_lt_pi]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "diff_derivable_fun" ("f1" "LAMBDA (x: real_abs_lt_pi): x" "f2" "LAMBDA (x: real_abs_lt_pi): sin_value(x)")) (("1" (lemma "deriv_diff_fun" ("ff1" "LAMBDA (x: real_abs_lt_pi): x" "ff2" "LAMBDA (x: real_abs_lt_pi): sin_value(x)")) (("1" (replace -3 -1) (("1" (replace -5 -1) (("1" (expand "-") (("1" (assert) (("1" (lemma "identity_derivable_fun[{x:nnreal|x<pi/2}]") (("1" (lemma "deriv_id_fun[{x:nnreal|x<pi/2}]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "composition_derivable_fun[{x: nnreal | x < pi / 2},real_abs_lt_pi]" ("f" "LAMBDA (x: {x: nnreal | x < pi / 2}): x" "g" "LAMBDA (x_1: real_abs_lt_pi): x_1 - sin_value(x_1)")) (("1" (replace -3) (("1" (replace -5) (("1" (expand "o") (("1" (lemma "deriv_comp_fun[{x: nnreal | x < pi / 2},real_abs_lt_pi]" ("ff" "LAMBDA (x: {x: nnreal | x < pi / 2}): x" "gg" "LAMBDA (x_1: real_abs_lt_pi): x_1 - sin_value(x_1)")) (("1" (expand "o") (("1" (replace -3 -1) (("1" (replace -5 -1) (("1" (expand "*" -1) (("1" (lemma "minimum_derivative[{x: nnreal | x < pi / 2}]" ("g" "LAMBDA (x_1: {x: nnreal | x < pi / 2}): x_1 - sin_value(x_1)" "x" "0" "y" "px")) (("1" (split -1) (("1" (simplify -1) (("1" (rewrite "sin_value_0") (("1" (assert) nil nil)) nil)) nil) ("2" (replace -1 1) (("2" (assert) (("2" (expand "abs") (("2" (rewrite "cos_value_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil) ("4" (replace -1 1) (("4" (hide-all-but 1) (("4" (skosimp*) (("4" (expand "abs") (("4" (lemma "cos_value_strict_decreasing") (("4" (expand "strict_decreasing?") (("4" (inst - "0" "y!1") (("4" (rewrite "cos_value_0") (("4" (assert) (("4" (lemma "posreal_times_posreal_is_posreal" ("px" "1-cos_value(y!1)" "py" "y!1")) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (expand "abs" 1) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "abs" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=0") (("1" (inst + "pi/4") (("1" (assert) nil nil)) nil) ("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (typepred "x!1") (("3" (typepred "y!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=0") (("1" (inst + "pi/4") (("1" (assert) nil nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil) ("2" (inst + "0") (("1" (assert) nil nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (typepred "x!1") (("3" (typepred "y!1") (("3" (name-replace "K1" "pi/2") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "phase_sin_q2") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil) ("3" (rewrite "phase_sin_q3") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil) ("4" (rewrite "phase_sin_q4") (("4" (flatten) (("4" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "sin(px)") (("2" (assert) nil nil)) nil)) nil)) nil) nil shostak)) (cos_lb 0 (cos_lb-4 nil 3307801291 ("" (skolem 1 ("px")) (("" (case "px<pi") (("1" (case "derivable[{x:real| -pi/4<x&x<pi/4}](LAMBDA (x:{x:real| -pi/4<x&x<pi/4}): cos(x)) (("1" (case "deriv[{x: real | -pi / 4 < x & x < pi / 4}](LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos(x (("1" (case "1 - (pi/4) * (pi/4) / 2 < cos(pi/4)") (("1" (lemma "trich_lt" ("x" "px" "y" "pi/4")) (("1" (split -1) (("1" (hide -5) (("1" (hide -2) (("1" (lemma "identity_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]") (("1" (lemma "deriv_id_fun[{x: real | -pi / 4 < x & x < pi / 4}]") (("1" (expand "I") (("1" (lemma "const_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("b" "1")) (("1" (lemma "deriv_const_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("b" "1")) (("1" (expand "const_fun") (("1" (lemma "prod_derivable_fun" ("f1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): x" "f2" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): x")) (("1" (assert) (("1" (expand "*") (("1" (lemma "deriv_prod_fun" ("ff1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): x" "ff2" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): x")) (("1" (replace -5) (("1" (expand "*") (("1" (expand "+") (("1" (lemma "scal_derivable_fun" ("b" "1/2" "f" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1 * x_1")) (("1" (assert) (("1" (expand "*") (("1" (lemma "deriv_scal_fun" ("b" "1/2" "ff" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1 * x_1")) (("1" (replace -3) (("1" (expand "*") (("1" (lemma "diff_derivable_fun" ("f1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 1" "f2" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 1 / 2 * (x * x)")) (("1" (assert) (("1" (expand "-") (("1" (lemma "deriv_diff_fun" ("ff1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 1" "ff2" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 1 / 2 * (x * x)")) (("1" (expand "-") (("1" (replace -3) (("1" (replace -7) (("1" (simplify -1) (("1" (lemma "diff_derivable_fun" ("f1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos(x)" "f2" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): 1 - 1 / 2 * (x_1 * x_1)")) (("1" (assert) (("1" (expand "-") (("1" (lemma "deriv_diff_fun" ("ff1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos(x)" "ff2" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): 1 - 1 / 2 * (x_1 * x_1)")) (("1" (replace -3) (("1" (replace -14) (("1" (expand "-") (("1" (hide-all-but (-1 -2 -13 1)) (("1" (lemma "identity_derivable_fun[{x:nnreal|x<pi/4}]") (("1" (lemma "deriv_id_fun[{x:nnreal|x<pi/4}]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "composition_derivable_fun[{x: nnreal | x < pi / 4},{x: real | -pi / 4 < x & x < pi / 4}]" ("f" "LAMBDA (x: {x: nnreal | x < pi / 4}): x" "g" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): cos(x_1) - 1 + 1 / 2 * (x_1 * x_1)")) (("1" (assert) (("1" (expand "o") (("1" (lemma "deriv_comp_fun[{x: nnreal | x < pi / 4},{x: real | -pi / 4 < x & x < pi / 4}]" ("ff" "LAMBDA (x: {x: nnreal | x < pi / 4}): x" "gg" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): cos(x_1) - 1 + 1 / 2 * (x_1 * x_1)")) (("1" (replace -5) (("1" (replace -3) (("1" (expand "o") (("1" (expand "*") (("1" (lemma "minimum_derivative[{x: nnreal | x < pi / 4}]" ("g" "LAMBDA (x_1: {x: nnreal | x < pi / 4}): cos(x_1) - 1 + 1 / 2 * (x_1 * x_1)" "x" "0" "y1" "px")) (("1" (split -1) (("1" (simplify -1) (("1" (rewrite "cos_0") (("1" (assert) nil nil)) nil)) nil) ("2" (replace -1 1) (("2" (simplify 1) (("2" (rewrite "sin_0") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (assert) nil nil) ("4" (hide 2) (("4" (skosimp*) (("4" (replace -1) (("4" (simplify 2) (("4" (hide-all-but (1 2)) (("4" (lemma "sin_ub" ("px" "y!1")) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "y!1" "py" "y!1-sin(y!1)")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=0") (("1" (inst + "pi/8") (("1" (assert) nil nil)) nil) ("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (propax) nil nil)) nil) ("3" (hide -3 -4) (("3" (expand "cos") (("3" (lemma "floor_0" ("x" "px / (2 * pi)")) (("3" (flatten -1) (("3" (hide -1) (("3" (split -1) (("1" (replace -1) (("1" (lemma "floor_0" ("x" "pi / 4 / (2 * pi)")) (("1" (flatten -1) (("1" (hide -1) (("1" (split -1) (("1" (replace -1) (("1" (simplify (-4 1)) (("1" (hide -1 -2) (("1" (rewrite "cos_phase_pi4") (("1" (expand "cos_phase") (("1" (rewrite "phase_cos_q1" 1) (("1" (assert) (("1" (lemma "identity_derivable_fun[{x:nnreal|pi/4<=x&x<pi}]") (("1" (lemma "deriv_id_fun[{x:nnreal|pi/4<=x&x<pi}]") (("1" (lemma "const_derivable_fun[{x:nnreal|pi/4<=x&x<pi}]" ("b" "1")) (("1" (lemma "deriv_const_fun[{x:nnreal|pi/4<=x&x<pi}]" ("b" "1")) (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "prod_derivable_fun" ("f1" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): x" "f2" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): x")) (("1" (assert) (("1" (expand "*") (("1" (lemma "deriv_prod_fun" ("ff1" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): x" "ff2" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): x")) (("1" (replace -5) (("1" (expand "*") (("1" (expand "+") (("1" (lemma "scal_derivable_fun" ("b" "1/2" "f" "LAMBDA (x_1: {x: nnreal | pi / 4 <= x & x < pi}): x_1 * x_1")) (("1" (assert) (("1" (expand "*") (("1" (lemma "deriv_scal_fun" ("b" "1/2" "ff" "LAMBDA (x_1: {x: nnreal | pi / 4 <= x & x < pi}): x_1 * x_1")) (("1" (replace -3) (("1" (expand "*") (("1" (lemma "diff_derivable_fun" ("f1" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): 1" "f2" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): 1 / 2 * (x * x)")) (("1" (assert) (("1" (expand "-") (("1" (lemma "deriv_diff_fun" ("ff1" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): 1" "ff2" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): 1 / 2 * (x * x)")) (("1" (replace -7) (("1" (replace -3) (("1" (expand "-") (("1" (lemma "cos_value_derivable2") (("1" (lemma "deriv_cos_value") (("1" (lemma "composition_derivable_fun[{x: nnreal | pi / 4 <= x & x < pi},posreal_lt_pi]" ("f" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): x" "g" "LAMBDA (x: posreal_lt_pi): cos_value(x)")) (("1" (assert) (("1" (expand "o") (("1" (lemma "deriv_comp_fun[{x: nnreal | pi / 4 <= x & x < pi},posreal_lt_pi]" ("ff" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): x" "gg" "LAMBDA (x: posreal_lt_pi): cos_value(x)")) (("1" (expand "o") (("1" (replace -3 -1) (("1" (replace -13) (("1" (expand "*") (("1" (hide -7 -8 -9 -10 -11 -12 -13 -14) (("1" (lemma "diff_derivable_fun" ("f1" "LAMBDA (x_1: {x: nnreal | pi / 4 <= x & x < pi}): cos_value(x_1)" "f2" "LAMBDA (x_1: {x: nnreal | pi / 4 <= x & x < pi}): 1 - 1 / 2 * (x_1 * x_1)")) (("1" (assert) (("1" (expand "-") (("1" (lemma "deriv_diff_fun" ("ff1" "LAMBDA (x_1: {x: nnreal | pi / 4 <= x & x < pi}): cos_value(x_1)" "ff2" "LAMBDA (x_1: {x: nnreal | pi / 4 <= x & x < pi}): 1 - 1 / 2 * (x_1 * x_1)")) (("1" (replace -3) (("1" (replace -7) (("1" (expand "-") (("1" (lemma "positive_derivative[{x: nnreal | pi / 4 <= x & x < pi}]" ("g" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): cos_value(x) - 1 + 1 / 2 * (x * x)")) (("1" (split -1) (("1" (expand "strict_increasing?") (("1" (hide-all-but (-1 -10 -11 -12 1)) (("1" (inst - "pi/4" "px") (("1" (rewrite "cos_value_pi4") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide 2) (("2" (expand "deriv" -1) (("2" (lemma "extensionality_postulate" ("f" "(LAMBDA (x_1: {x: nnreal | pi / 4 <= x & x < pi}): deriv(LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): cos_value(x) - 1 + 1 / 2 * (x * x), x_1))" "g" "(LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): IF x < pi / 2 THEN -sin_value(x) ELSE -sin_value(pi - x) ENDIF + 2 * (x * (1 / 2)))")) (("1" (replace -1 -2 rl) (("1" (inst -2 "x!1") (("1" (replace -2 1) (("1" (hide-all-but (-10 -11 -12 1)) (("1" (case "x!1 < pi / 2") (("1" (hide -2 -3 -4) (("1" (assert) (("1" (lemma "sin_ub" ("px" "x!1")) (("1" (expand "sin") (("1" (lemma "floor_0" ("x" "x!1/(2*pi)")) (("1" (assert) (("1" (rewrite "div_mult_pos_lt1" -1) (("1" (flatten -1) (("1" (replace -1) (("1" (simplify -2) (("1" (rewrite "sin_q1" -2) (("1" (assert) nil nil) ("2" (rewrite "phase_sin_q1" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "pi/2<=x!1") (("1" (hide -2 -3 -4 1) (("1" (lemma "sin_ub" ("px" "x!1")) (("1" (expand "sin") (("1" (lemma "floor_0" ("x" "x!1 / (2 * pi)")) (("1" (assert) (("1" (rewrite "div_mult_pos_lt1" -1) (("1" (flatten -1) (("1" (replace -1) (("1" (simplify -2) (("1" (hide -1) (("1" (case "sin_value(pi - x!1) = sin_phase(x!1)") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (hide -1 2) (("2" (rewrite "sin_q2" 1) (("1" (rewrite "sin_eqv_cos_value") (("1" (lemma "cos_value_neg" ("xc" "x!1-pi/2")) (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "phase_sin_q2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (expand "abs" 1) (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (skosimp*) (("4" (typepred "x!3") (("4" (case "x!3=pi/4") (("1" (inst + "pi/2") (("1" (assert) nil nil)) nil) ("2" (inst + "pi/4") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide-all-but 1) (("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp*) (("6" (expand "derivable" -2) (("6" (inst -2 "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=pi/2") (("1" (inst + "pi/3") (("1" (assert) nil nil)) nil) ("2" (inst + "pi/2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=pi/4") (("1" (inst + "pi/2") (("1" (assert) nil nil)) nil) ("2" (inst + "pi/4") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "div_div2") (("2" (lemma "div_cancel1" ("x" "1/8" "n0z" "pi")) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (lemma "div_cancel1" ("x" "1/8" "n0z" "pi")) (("3" (rewrite "div_div2" 1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) (("3" (rewrite "div_mult_pos_lt1" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "cos") (("2" (lemma "floor_0" ("x" "pi / 4 / (2 * pi)")) (("2" (rewrite "div_div2") (("2" (lemma "div_cancel1" ("x" "1/8" "n0z" "pi")) (("2" (replace -1) (("2" (hide -1) (("2" (flatten -1) (("2" (hide -1) (("2" (split -1) (("1" (replace -1) (("1" (simplify 1) (("1" (hide -1) (("1" (rewrite "cos_phase_pi4") (("1" (case "314/100<=pi&pi<=315/100") (("1" (flatten) (("1" (lemma "le_times_le_pos" ("nnx" "pi/4" "y" "315/400" "nnz" "pi/4" "w" "315/400")) (("1" (assert) (("1" (lemma "le_times_le_pos" ("y" "pi/4" "nnx" "314/400" "w" "pi/4" "nnz" "314/400")) (("1" (assert) (("1" (case "1 - (pi / 4) * (pi / 4) / 2<=221404/320000") (("1" (lemma "sq_lt" ("nna" "221404 / 320000" "nnb" "sqrt(1/2)")) (("1" (flatten -1) (("1" (hide -2) (("1" (rewrite "sq_sqrt") (("1" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "pi") (("2" (expand "pi_lb") (("2" (expand "pi_ub") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (lemma "extensionality" ("f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos(x)" "g" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): sqrt(1/2)*(cos(x+pi/4)+sin(x+pi/4))")) (("2" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "identity_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]") (("1" (lemma "deriv_id_fun[{x: real | -pi / 4 < x & x < pi / 4}]") (("1" (expand "I") (("1" (lemma "const_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("b" "pi/4")) (("1" (lemma "deriv_const_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("b" "pi/4")) (("1" (expand "const_fun") (("1" (lemma "sin_value_derivable2") (("1" (lemma "cos_value_derivable2") (("1" (lemma "deriv_sin_value") (("1" (lemma "deriv_cos_value") (("1" (lemma "sum_derivable_fun" ("f1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): pi / 4" "f2" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): x")) (("1" (assert) (("1" (expand "+") (("1" (lemma "deriv_sum_fun" ("ff1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): pi / 4" "ff2" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): x")) (("1" (replace -9) (("1" (replace -7) (("1" (expand "+") (("1" (lemma "composition_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4},posreal_lt_pi]" ("f" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1+pi/4" "g" "LAMBDA (x: posreal_lt_pi): cos_value(x)")) (("1" (assert) (("1" (expand "o") (("1" (lemma "composition_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4},real_abs_lt_pi]" ("f" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1+pi/4" "g" "LAMBDA (x: real_abs_lt_pi): sin_value(x)")) (("1" (assert) (("1" (expand "o") (("1" (lemma "deriv_comp_fun[{x: real | -pi / 4 < x & x < pi / 4},real_abs_lt_pi]" ("ff" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1+pi/4" "gg" "LAMBDA (x: real_abs_lt_pi): sin_value(x)")) (("1" (lemma "deriv_comp_fun[{x: real | -pi / 4 < x & x < pi / 4},posreal_lt_pi]" ("ff" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1+pi/4" "gg" "LAMBDA (x: posreal_lt_pi): cos_value(x)")) (("1" (replace -5) (("1" (replace -7) (("1" (replace -8) (("1" (expand "o") (("1" (expand "*") (("1" (lemma "sum_derivable_fun" ("f1" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x_1 + pi / 4)" "f2" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): sin_value(x_1 + pi / 4)")) (("1" (expand "+") (("1" (hide (-8 -9 -10 -11 -12 -13 -14 -15)) (("1" (assert) (("1" (lemma "deriv_sum_fun" ("ff1" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x_1 + pi / 4)" "ff2" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): sin_value(x_1 + pi / 4)")) (("1" (replace -3) (("1" (replace -4) (("1" (expand "abs" (-1 -4)) (("1" (expand "+") (("1" (lemma "scal_derivable_fun" ("f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x + pi / 4) + sin_value(x + pi / 4)" "b" "sqrt(1/2)")) (("1" (assert) (("1" (expand "*") (("1" (lemma "deriv_scal_fun" ("ff" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x + pi / 4) + sin_value(x + pi / 4)" "b" "sqrt(1/2)")) (("1" (replace -3) (("1" (expand "*") (("1" (hide-all-but (-1 -2 -11 1)) (("1" (lemma "extensionality" ("f" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x_1 + pi / 4) * sqrt(1 / 2) + sin_value(x_1 + pi / 4) * sqrt(1 / 2)" "g" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos(x + pi / 4) * sqrt(1 / 2) + sin(x + pi / 4) * sqrt(1 / 2)")) (("1" (split -1) (("1" (replace -1) (("1" (lemma "extensionality" ("f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x + pi / 4) * sqrt(1 / 2) + sqrt(1 / 2) * -sin_value(x + pi / 4)" "g" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): -sin(x)")) (("1" (split -1) (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (lemma "sin_minus" ("a" "x!1+pi/4" "b" "pi/4")) (("2" (replace -1 1) (("2" (hide -1) (("2" (expand "sin") (("2" (expand "cos") (("2" (rewrite "div_div2") (("2" (lemma "div_cancel1" ("x" "1/8" "n0z" "pi")) (("2" (replace -1) (("2" (lemma "floor_0" ("x" "1/8")) (("2" (flatten -1) (("2" (hide -1 -3) (("2" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (simplify) (("1" (rewrite "cos_phase_pi4") (("1" (rewrite "sin_phase_pi4") (("1" (typepred "x!1") (("1" (lemma "floor_0" ("x" "(pi / 4 + x!1) / (2 * pi)")) (("1" (rewrite "div_mult_pos_lt1" -1) (("1" (rewrite "div_mult_pos_le2" -1) (("1" (flatten -1) (("1" (replace -1) (("1" (simplify 1) (("1" (rewrite "sin_q1") (("1" (rewrite "cos_q1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (assert) (("2" (lemma "phase_sin_q1" ("x" "(pi / 4) + x!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -3 1)) (("2" (lemma "phase_sin_q1" ("x" "(pi / 4) + x!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (expand "cos") (("2" (expand "sin") (("2" (lemma "floor_0" ("x" "(pi / 4 + x!1) / (2 * pi)")) (("2" (flatten -1) (("2" (split -2) (("1" (replace -1) (("1" (hide -1 -2) (("1" (simplify) (("1" (rewrite "sin_q1") (("1" (rewrite "cos_q1") (("1" (hide 2) (("1" (typepred "x!1") (("1" (lemma "phase_sin_q1" ("x" "pi/4+x!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "phase_sin_q1" ("x" "pi/4+x!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (assert) (("2" (rewrite "div_mult_pos_le2") nil nil)) nil)) nil) ("3" (rewrite "div_mult_pos_lt1" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "abs" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "abs" 1) (("2" (propax) nil nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (case "x!1=0") (("1" (inst + "pi/4") (("1" (assert) nil nil) ("2" (expand "abs" 1) (("2" (typepred "pi") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (inst + "0") (("1" (assert) nil nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (skosimp*) (("4" (typepred "x!1") (("4" (typepred "y!1") (("4" (name-replace "K1" "pi/2") (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=pi/2") (("1" (inst + "pi/3") (("1" (assert) nil nil)) nil) ("2" (inst + "pi/2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (skosimp*) (("2" (lemma "cos_minus" ("a" "x!1 + pi / 4" "b" "pi/4")) (("2" (replace -1 1) (("2" (hide -1) (("2" (expand "cos") (("2" (expand "sin") (("2" (rewrite "div_div2") (("2" (lemma "div_cancel1" ("x" "1/8" "n0z" "pi")) (("2" (replace -1) (("2" (lemma "floor_0" ("x" "1/8")) (("2" (flatten -1) (("2" (hide -1 -3) (("2" (split -1) (("1" (replace -1) (("1" (simplify 1) (("1" (rewrite "sin_phase_pi4") (("1" (rewrite "cos_phase_pi4") nil nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil) ("2" (lemma "extensionality" ("f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos(x)" "g" "LAMBDA (x:{x: real | -pi / 4 < x & x < pi / 4}):sqrt(1/2)*(cos_value(x+pi/4)+sin_value(x+pi (("1" (split -1) (("1" (replace -1 1) (("1" (hide-all-but 1) (("1" (lemma "cos_value_derivable2") (("1" (lemma "sin_value_derivable2") (("1" (lemma "identity_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]") (("1" (lemma "deriv_id_fun[{x: real | -pi / 4 < x & x < pi / 4}]") (("1" (expand "I") (("1" (lemma "const_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("b" "pi/4")) (("1" (lemma "deriv_const_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("b" "pi/4")) (("1" (expand "const_fun") (("1" (lemma "sum_derivable_fun" ("f1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): x" "f2" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): pi/4")) (("1" (lemma "deriv_sum_fun" ("ff1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): x" "ff2" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): pi/4")) (("1" (replace -3 -1) (("1" (replace -5 -1) (("1" (expand "+") (("1" (assert) (("1" (lemma "composition_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4},real_abs_lt_pi]" ("f" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1 + pi / 4" "g" "LAMBDA (x: real_abs_lt_pi): sin_value(x)")) (("1" (lemma "composition_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4},posreal_lt_pi]" ("f" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1 + pi / 4" "g" "LAMBDA (x: posreal_lt_pi): cos_value(x)")) (("1" (assert) (("1" (expand "o") (("1" (lemma "sum_derivable_fun" ("f1" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x_1 + pi / 4)" "f2" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): sin_value(x_1 + pi / 4)")) (("1" (assert) (("1" (expand "+") (("1" (lemma "scal_derivable_fun" ("b" "sqrt(1/2)" "f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x + pi / 4) + sin_value(x + pi / 4)")) (("1" (assert) (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=pi/2") (("1" (inst + "pi/4") (("1" (assert) nil nil)) nil) ("2" (inst + "pi/2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (case "x!1=0") (("1" (inst + "pi/4") (("1" (assert) nil nil) ("2" (expand "abs") (("2" (assert) (("2" (typepred "pi") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst + "0") (("1" (assert) nil nil) ("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (skosimp*) (("4" (typepred "x!1") (("4" (typepred "y!1") (("4" (name-replace "K1" "pi/2") (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (lemma "cos_minus" ("a" "x!1+pi/4" "b" "pi/4")) (("2" (replace -1 1) (("2" (hide -1) (("2" (typepred "x!1") (("2" (expand "cos") (("2" (expand "sin") (("2" (rewrite "div_div2" 1) (("2" (lemma "div_cancel1" ("x" "1/8" "n0z" "pi")) (("2" (replace -1) (("2" (lemma "floor_0" ("x" "1/8")) (("2" (flatten -1) (("2" (hide -1) (("2" (simplify -1) (("2" (replace -1) (("2" (simplify 1) (("2" (lemma "floor_0" ("x" "(pi / 4 + x!1) / (2 * pi)")) (("2" (flatten -1) (("2" (hide -1 -3 -4) (("2" (split -1) (("1" (replace -1) (("1" (simplify 1) (("1" (hide -1) (("1" (rewrite "cos_phase_pi4") (("1" (rewrite "sin_phase_pi4") (("1" (lemma "phase_sin_q1" ("x" "pi/4+x!1")) (("1" (assert) (("1" (rewrite "sin_q1" 1) (("1" (rewrite "cos_q1" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "div_mult_pos_le2" ("z" "pi / 4 + x!1" "py" "2*pi" "x" "0")) (("2" (assert) nil nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "div_mult_pos_lt1" ("z" "pi / 4 + x!1" "py" "2*pi" "x" "1")) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "abs") (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (case "x!1=0") (("1" (inst + "pi/8") (("1" (assert) nil nil)) nil) ("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil) ("2" (case "pi<=px") (("1" (hide 1) (("1" (lemma "pi_bnds") (("1" (flatten) (("1" (typepred "cos(px)") (("1" (lemma "lt_times_lt_pos1" ("px" "306/100" "y" "px" "nnz" "306/100" "w" "px")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((sin_minus formula-decl nil trig_basic nil) (cos_minus formula-decl nil trig_basic nil) (sin_0 formula-decl nil trig_basic nil) (cos_0 formula-decl nil trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (pi_lb const-decl "posreal" trig_basic nil) (sq_lt formula-decl nil sq "reals/") (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (sq const-decl "nonneg_real" sq "reals/") (sq_sqrt formula-decl nil sqrt "reals/")) nil) (cos_lb-3 nil 3307185889 ("" (skolem 1 ("px")) (("" (case "px<pi") (("1" (case "derivable[{x:real| -pi/4<x&x<pi/4}](LAMBDA (x:{x:real| -pi/4<x&x<pi/4}): cos(x)) (("1" (case "deriv[{x: real | -pi / 4 < x & x < pi / 4}](LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos(x (("1" (case "1 - (pi/4) * (pi/4) / 2 < cos(pi/4)") (("1" (lemma "trich_lt" ("x" "px" "y" "pi/4")) (("1" (split -1) (("1" (hide -5) (("1" (hide -2) (("1" (lemma "identity_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]") (("1" (lemma "deriv_id_fun[{x: real | -pi / 4 < x & x < pi / 4}]") (("1" (expand "I") (("1" (lemma "const_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("b" "1")) (("1" (lemma "deriv_const_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("b" "1")) (("1" (expand "const_fun") (("1" (lemma "prod_derivable_fun" ("f1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): x" "f2" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): x")) (("1" (assert) (("1" (expand "*") (("1" (lemma "deriv_prod_fun" ("ff1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): x" "ff2" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): x")) (("1" (replace -5) (("1" (expand "*") (("1" (expand "+") (("1" (lemma "scal_derivable_fun" ("b" "1/2" "f" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1 * x_1")) (("1" (assert) (("1" (expand "*") (("1" (lemma "deriv_scal_fun" ("b" "1/2" "ff" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1 * x_1")) (("1" (replace -3) (("1" (expand "*") (("1" (lemma "diff_derivable_fun" ("f1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 1" "f2" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 1 / 2 * (x * x)")) (("1" (assert) (("1" (expand "-") (("1" (lemma "deriv_diff_fun" ("ff1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 1" "ff2" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 1 / 2 * (x * x)")) (("1" (expand "-") (("1" (replace -3) (("1" (replace -7) (("1" (simplify -1) (("1" (lemma "diff_derivable_fun" ("f1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos(x)" "f2" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): 1 - 1 / 2 * (x_1 * x_1)")) (("1" (assert) (("1" (expand "-") (("1" (lemma "deriv_diff_fun" ("ff1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos(x)" "ff2" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): 1 - 1 / 2 * (x_1 * x_1)")) (("1" (replace -3) (("1" (replace -14) (("1" (expand "-") (("1" (hide-all-but (-1 -2 -13 1)) (("1" (lemma "identity_derivable_fun[{x:nnreal|x<pi/4}]") (("1" (lemma "deriv_id_fun[{x:nnreal|x<pi/4}]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "composition_derivable_fun[{x: nnreal | x < pi / 4},{x: real | -pi / 4 < x & x < pi / 4}]" ("f" "LAMBDA (x: {x: nnreal | x < pi / 4}): x" "g" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): cos(x_1) - 1 + 1 / 2 * (x_1 * x_1)")) (("1" (assert) (("1" (expand "o") (("1" (lemma "deriv_comp_fun[{x: nnreal | x < pi / 4},{x: real | -pi / 4 < x & x < pi / 4}]" ("ff" "LAMBDA (x: {x: nnreal | x < pi / 4}): x" "gg" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): cos(x_1) - 1 + 1 / 2 * (x_1 * x_1)")) (("1" (replace -5) (("1" (replace -3) (("1" (expand "o") (("1" (expand "*") (("1" (lemma "minimum_derivative[{x: nnreal | x < pi / 4}]" ("g" "LAMBDA (x_1: {x: nnreal | x < pi / 4}): cos(x_1) - 1 + 1 / 2 * (x_1 * x_1)" "x" "0" "y1" "px")) (("1" (split -1) (("1" (simplify -1) (("1" (rewrite "cos_0") (("1" (assert) nil nil)) nil)) nil) ("2" (replace -1 1) (("2" (simplify 1) (("2" (rewrite "sin_0") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (assert) nil nil) ("4" (hide 2) (("4" (skosimp*) (("4" (replace -1) (("4" (simplify 2) (("4" (hide-all-but (1 2)) (("4" (lemma "sin_ub" ("px" "y!1")) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "y!1" "py" "y!1-sin(y!1)")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=0") (("1" (inst + "pi/8") (("1" (assert) nil nil)) nil) ("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (propax) nil nil)) nil) ("3" (hide -3 -4) (("3" (expand "cos") (("3" (lemma "floor_0" ("x" "px / (2 * pi)")) (("3" (flatten -1) (("3" (hide -1) (("3" (split -1) (("1" (replace -1) (("1" (lemma "floor_0" ("x" "pi / 4 / (2 * pi)")) (("1" (flatten -1) (("1" (hide -1) (("1" (split -1) (("1" (replace -1) (("1" (simplify (-4 1)) (("1" (hide -1 -2) (("1" (rewrite "cos_phase_pi4") (("1" (expand "cos_phase") (("1" (rewrite "phase_cos_q1" 1) (("1" (assert) (("1" (lemma "identity_derivable_fun[{x:nnreal|pi/4<=x&x<pi}]") (("1" (lemma "deriv_id_fun[{x:nnreal|pi/4<=x&x<pi}]") (("1" (lemma "const_derivable_fun[{x:nnreal|pi/4<=x&x<pi}]" ("b" "1")) (("1" (lemma "deriv_const_fun[{x:nnreal|pi/4<=x&x<pi}]" ("b" "1")) (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "prod_derivable_fun" ("f1" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): x" "f2" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): x")) (("1" (assert) (("1" (expand "*") (("1" (lemma "deriv_prod_fun" ("ff1" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): x" "ff2" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): x")) (("1" (replace -5) (("1" (expand "*") (("1" (expand "+") (("1" (lemma "scal_derivable_fun" ("b" "1/2" "f" "LAMBDA (x_1: {x: nnreal | pi / 4 <= x & x < pi}): x_1 * x_1")) (("1" (assert) (("1" (expand "*") (("1" (lemma "deriv_scal_fun" ("b" "1/2" "ff" "LAMBDA (x_1: {x: nnreal | pi / 4 <= x & x < pi}): x_1 * x_1")) (("1" (replace -3) (("1" (expand "*") (("1" (lemma "diff_derivable_fun" ("f1" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): 1" "f2" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): 1 / 2 * (x * x)")) (("1" (assert) (("1" (expand "-") (("1" (lemma "deriv_diff_fun" ("ff1" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): 1" "ff2" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): 1 / 2 * (x * x)")) (("1" (replace -7) (("1" (replace -3) (("1" (expand "-") (("1" (lemma "cos_value_derivable2") (("1" (lemma "deriv_cos_value") (("1" (lemma "composition_derivable_fun[{x: nnreal | pi / 4 <= x & x < pi},posreal_lt_pi]" ("f" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): x" "g" "LAMBDA (x: posreal_lt_pi): cos_value(x)")) (("1" (assert) (("1" (expand "o") (("1" (lemma "deriv_comp_fun[{x: nnreal | pi / 4 <= x & x < pi},posreal_lt_pi]" ("ff" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): x" "gg" "LAMBDA (x: posreal_lt_pi): cos_value(x)")) (("1" (expand "o") (("1" (replace -3 -1) (("1" (replace -13) (("1" (expand "*") (("1" (hide -7 -8 -9 -10 -11 -12 -13 -14) (("1" (lemma "diff_derivable_fun" ("f1" "LAMBDA (x_1: {x: nnreal | pi / 4 <= x & x < pi}): cos_value(x_1)" "f2" "LAMBDA (x_1: {x: nnreal | pi / 4 <= x & x < pi}): 1 - 1 / 2 * (x_1 * x_1)")) (("1" (assert) (("1" (expand "-") (("1" (lemma "deriv_diff_fun" ("ff1" "LAMBDA (x_1: {x: nnreal | pi / 4 <= x & x < pi}): cos_value(x_1)" "ff2" "LAMBDA (x_1: {x: nnreal | pi / 4 <= x & x < pi}): 1 - 1 / 2 * (x_1 * x_1)")) (("1" (replace -3) (("1" (replace -7) (("1" (expand "-") (("1" (lemma "positive_derivative[{x: nnreal | pi / 4 <= x & x < pi}]" ("g" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): cos_value(x) - 1 + 1 / 2 * (x * x)")) (("1" (split -1) (("1" (expand "strict_increasing?") (("1" (hide-all-but (-1 -10 -11 -12 1)) (("1" (inst - "pi/4" "px") (("1" (rewrite "cos_value_pi4") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide 2) (("2" (expand "deriv" -1) (("2" (lemma "extensionality_postulate" ("f" "(LAMBDA (x_1: {x: nnreal | pi / 4 <= x & x < pi}): deriv(LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): cos_value(x) - 1 + 1 / 2 * (x * x), x_1))" "g" "(LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): IF x < pi / 2 THEN -sin_value(x) ELSE -sin_value(pi - x) ENDIF + 2 * (x * (1 / 2)))")) (("1" (replace -1 -2 rl) (("1" (inst -2 "x!1") (("1" (replace -2 1) (("1" (hide-all-but (-10 -11 -12 1)) (("1" (case "x!1 < pi / 2") (("1" (hide -2 -3 -4) (("1" (assert) (("1" (lemma "sin_ub" ("px" "x!1")) (("1" (expand "sin") (("1" (lemma "floor_0" ("x" "x!1/(2*pi)")) (("1" (assert) (("1" (rewrite "div_mult_pos_lt1" -1) (("1" (flatten -1) (("1" (replace -1) (("1" (simplify -2) (("1" (rewrite "sin_q1" -2) (("1" (assert) nil nil) ("2" (rewrite "phase_sin_q1" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "pi/2<=x!1") (("1" (hide -2 -3 -4 1) (("1" (lemma "sin_ub" ("px" "x!1")) (("1" (expand "sin") (("1" (lemma "floor_0" ("x" "x!1 / (2 * pi)")) (("1" (assert) (("1" (rewrite "div_mult_pos_lt1" -1) (("1" (flatten -1) (("1" (replace -1) (("1" (simplify -2) (("1" (hide -1) (("1" (case "sin_value(pi - x!1) = sin_phase(x!1)") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (hide -1 2) (("2" (rewrite "sin_q2" 1) (("1" (rewrite "sin_eqv_cos_value") (("1" (lemma "cos_value_neg" ("xc" "x!1-pi/2")) (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "phase_sin_q2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (expand "abs" 1) (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (skosimp*) (("4" (typepred "x!3") (("4" (case "x!3=pi/4") (("1" (inst + "pi/2") (("1" (assert) nil nil)) nil) ("2" (inst + "pi/4") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide-all-but 1) (("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp*) (("6" (expand "derivable" -2) (("6" (inst -2 "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=pi/2") (("1" (inst + "pi/3") (("1" (assert) nil nil)) nil) ("2" (inst + "pi/2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=pi/4") (("1" (inst + "pi/2") (("1" (assert) nil nil)) nil) ("2" (inst + "pi/4") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "div_div2") (("2" (lemma "div_cancel1" ("x" "1/8" "n0z" "pi")) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (lemma "div_cancel1" ("x" "1/8" "n0z" "pi")) (("3" (rewrite "div_div2" 1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) (("3" (rewrite "div_mult_pos_lt1" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "cos") (("2" (lemma "floor_0" ("x" "pi / 4 / (2 * pi)")) (("2" (rewrite "div_div2") (("2" (lemma "div_cancel1" ("x" "1/8" "n0z" "pi")) (("2" (replace -1) (("2" (hide -1) (("2" (flatten -1) (("2" (hide -1) (("2" (split -1) (("1" (replace -1) (("1" (simplify 1) (("1" (hide -1) (("1" (rewrite "cos_phase_pi4") (("1" (case "314/100<=pi&pi<=315/100") (("1" (flatten) (("1" (lemma "le_times_le_pos" ("nnx" "pi/4" "y" "315/400" "nnz" "pi/4" "w" "315/400")) (("1" (assert) (("1" (lemma "le_times_le_pos" ("y" "pi/4" "nnx" "314/400" "w" "pi/4" "nnz" "314/400")) (("1" (assert) (("1" (case "1 - (pi / 4) * (pi / 4) / 2<=221404/320000") (("1" (lemma "sq_lt" ("nna" "221404 / 320000" "nnb" "sqrt(1/2)")) (("1" (flatten -1) (("1" (hide -2) (("1" (rewrite "sq_sqrt") (("1" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "pi") (("2" (expand "pi_lb") (("2" (expand "pi_ub") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (lemma "extensionality" ("f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos(x)" "g" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): sqrt(1/2)*(cos(x+pi/4)+sin(x+pi/4))")) (("2" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "identity_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]") (("1" (lemma "deriv_id_fun[{x: real | -pi / 4 < x & x < pi / 4}]") (("1" (expand "I") (("1" (lemma "const_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("b" "pi/4")) (("1" (lemma "deriv_const_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("b" "pi/4")) (("1" (expand "const_fun") (("1" (lemma "sin_value_derivable2") (("1" (lemma "cos_value_derivable2") (("1" (lemma "deriv_sin_value") (("1" (lemma "deriv_cos_value") (("1" (lemma "sum_derivable_fun" ("f1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): pi / 4" "f2" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): x")) (("1" (assert) (("1" (expand "+") (("1" (lemma "deriv_sum_fun" ("ff1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): pi / 4" "ff2" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): x")) (("1" (replace -9) (("1" (replace -7) (("1" (expand "+") (("1" (lemma "composition_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4},posreal_lt_pi]" ("f" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1+pi/4" "g" "LAMBDA (x: posreal_lt_pi): cos_value(x)")) (("1" (assert) (("1" (expand "o") (("1" (lemma "composition_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4},real_abs_lt_pi]" ("f" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1+pi/4" "g" "LAMBDA (x: real_abs_lt_pi): sin_value(x)")) (("1" (assert) (("1" (expand "o") (("1" (lemma "deriv_comp_fun[{x: real | -pi / 4 < x & x < pi / 4},real_abs_lt_pi]" ("ff" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1+pi/4" "gg" "LAMBDA (x: real_abs_lt_pi): sin_value(x)")) (("1" (lemma "deriv_comp_fun[{x: real | -pi / 4 < x & x < pi / 4},posreal_lt_pi]" ("ff" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1+pi/4" "gg" "LAMBDA (x: posreal_lt_pi): cos_value(x)")) (("1" (replace -5) (("1" (replace -7) (("1" (replace -8) (("1" (expand "o") (("1" (expand "*") (("1" (lemma "sum_derivable_fun" ("f1" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x_1 + pi / 4)" "f2" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): sin_value(x_1 + pi / 4)")) (("1" (expand "+") (("1" (hide (-8 -9 -10 -11 -12 -13 -14 -15)) (("1" (assert) (("1" (lemma "deriv_sum_fun" ("ff1" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x_1 + pi / 4)" "ff2" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): sin_value(x_1 + pi / 4)")) (("1" (replace -3) (("1" (replace -4) (("1" (expand "abs" (-1 -4)) (("1" (expand "+") (("1" (lemma "scal_derivable_fun" ("f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x + pi / 4) + sin_value(x + pi / 4)" "b" "sqrt(1/2)")) (("1" (assert) (("1" (expand "*") (("1" (lemma "deriv_scal_fun" ("ff" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x + pi / 4) + sin_value(x + pi / 4)" "b" "sqrt(1/2)")) (("1" (replace -3) (("1" (expand "*") (("1" (hide-all-but (-1 -2 -11 1)) (("1" (lemma "extensionality" ("f" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x_1 + pi / 4) * sqrt(1 / 2) + sin_value(x_1 + pi / 4) * sqrt(1 / 2)" "g" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos(x + pi / 4) * sqrt(1 / 2) + sin(x + pi / 4) * sqrt(1 / 2)")) (("1" (split -1) (("1" (replace -1) (("1" (lemma "extensionality" ("f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x + pi / 4) * sqrt(1 / 2) + sqrt(1 / 2) * -sin_value(x + pi / 4)" "g" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): -sin(x)")) (("1" (split -1) (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (lemma "sin_minus" ("a" "x!1+pi/4" "b" "pi/4")) (("2" (replace -1 1) (("2" (hide -1) (("2" (expand "sin") (("2" (expand "cos") (("2" (rewrite "div_div2") (("2" (lemma "div_cancel1" ("x" "1/8" "n0z" "pi")) (("2" (replace -1) (("2" (lemma "floor_0" ("x" "1/8")) (("2" (flatten -1) (("2" (hide -1 -3) (("2" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (simplify) (("1" (rewrite "cos_phase_pi4") (("1" (rewrite "sin_phase_pi4") (("1" (typepred "x!1") (("1" (lemma "floor_0" ("x" "(pi / 4 + x!1) / (2 * pi)")) (("1" (rewrite "div_mult_pos_lt1" -1) (("1" (rewrite "div_mult_pos_le2" -1) (("1" (flatten -1) (("1" (replace -1) (("1" (simplify 1) (("1" (rewrite "sin_q1") (("1" (rewrite "cos_q1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (assert) (("2" (lemma "phase_sin_q1" ("x" "(pi / 4) + x!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -3 1)) (("2" (lemma "phase_sin_q1" ("x" "(pi / 4) + x!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (expand "cos") (("2" (expand "sin") (("2" (lemma "floor_0" ("x" "(pi / 4 + x!1) / (2 * pi)")) (("2" (flatten -1) (("2" (split -2) (("1" (replace -1) (("1" (hide -1 -2) (("1" (simplify) (("1" (rewrite "sin_q1") (("1" (rewrite "cos_q1") (("1" (hide 2) (("1" (typepred "x!1") (("1" (lemma "phase_sin_q1" ("x" "pi/4+x!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "phase_sin_q1" ("x" "pi/4+x!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (assert) (("2" (rewrite "div_mult_pos_le2") nil nil)) nil)) nil) ("3" (rewrite "div_mult_pos_lt1" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case-replace "x!1 = 0") (("1" (inst + "pi/4") (("1" (assert) nil nil) ("2" (expand "abs") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil) ("2" (inst + "0") (("1" (assert) nil nil) ("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (typepred "y!1") (("3" (typepred "x!1") (("3" (name-replace "K1" "pi/2") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=pi/2") (("1" (inst + "pi/3") (("1" (assert) nil nil)) nil) ("2" (inst + "pi/2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) --> -------------------- --> maximum size reached --> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.597Angebot (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-26) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26