(sincos_def0 1 nil 3265619589 "" (skosimp*)"" (typepred "cos(x!1)" ) (("" (propax) nil nil )) nil )) nil )"real" trig_basic nil )"[numfield -> numfield]" number_fields nil )eq -decl nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )eq -decl nil booleans nil )nil booleans nil )"trig_range" trig_basic nil ))0 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" "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" "phases_sin" ("x" "px" ))"2" 1 )"1" rewrite "sin_q1" )"1" 1 )"1" "sin_value_derivable2" )"1" "deriv_sin_value" )"1" "identity_derivable_fun[real_abs_lt_pi]" )"1" "deriv_id_fun[real_abs_lt_pi]" )"1" expand "I" )"1" expand "const_fun" )"1" "diff_derivable_fun" "f1" "LAMBDA (x: real_abs_lt_pi): x" "f2" "LAMBDA (x: real_abs_lt_pi): sin_value(x)" ))"1" "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" "identity_derivable_fun[{x:nnreal|x<pi/2}]" )"1" "deriv_id_fun[{x:nnreal|x<pi/2}]" )"1" expand "I" )"1" expand "const_fun" )"1" "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" "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" "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" 1 )"1" 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" 1 )"4" "4" expand "abs" )"4" "cos_value_strict_decreasing" )"4" expand "strict_decreasing?" )"4" "0" "y!1" )"4" rewrite "cos_value_0" )"4" assert )"4" "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" nil nil )"3" "3" assert )"3" expand "abs" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 1 )"2" "2" case "x!1=0" )"1" "pi/4" )"1" assert )nil nil ))nil )"2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" 1 )"3" "3" "x!1" )"3" "y!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" 1 )"2" "2" case "x!1=0" )"1" "pi/4" )"1" assert )nil nil )"2" expand "abs" 1 )"2" assert )nil nil ))nil ))nil )"2" "0" )"1" assert )nil nil )"2" expand "abs" 1 )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" 1 )"3" "3" "x!1" )"3" "y!1" )"3" replace "K1" "pi/2" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "phase_sin_q2" )"2" "2" (assert ) nil nil ))nil ))nil )"3" rewrite "phase_sin_q3" )"3" "3" (assert ) nil nil ))nil ))nil )"4" rewrite "phase_sin_q4" )"4" "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 )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" "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" "phases_sin" ("x" "px" ))"1" 1 )"1" rewrite "sin_q1" )"1" 1 )"1" "sin_value_derivable2" )"1" "deriv_sin_value" )"1" "identity_derivable_fun[real_abs_lt_pi]" )"1" "deriv_id_fun[real_abs_lt_pi]" )"1" expand "I" )"1" expand "const_fun" )"1" "diff_derivable_fun" "f1" "LAMBDA (x: real_abs_lt_pi): x" "f2" "LAMBDA (x: real_abs_lt_pi): sin_value(x)" ))"1" "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" "identity_derivable_fun[{x:nnreal|x<pi/2}]" )"1" "deriv_id_fun[{x:nnreal|x<pi/2}]" )"1" expand "I" )"1" expand "const_fun" )"1" "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" "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" "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" 1 )"1" 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" 1 )"4" "4" expand "abs" )"4" "cos_value_strict_decreasing" )"4" expand "strict_decreasing?" )"4" "0" "y!1" )"4" rewrite "cos_value_0" )"4" assert )"4" "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" nil nil )"3" expand "abs" 1 )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" expand "abs" 1 )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" 1 )"2" "2" case "x!1=0" )"1" "pi/4" )"1" assert )nil nil ))nil )"2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" 1 )"3" "3" "x!1" )"3" "y!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" 1 )"2" "2" case "x!1=0" )"1" "pi/4" )"1" assert )nil nil )"2" expand "abs" 1 )"2" assert )nil nil ))nil ))nil )"2" "0" )"1" assert )nil nil )"2" expand "abs" 1 )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" 1 )"3" "3" "x!1" )"3" "y!1" )"3" replace "K1" "pi/2" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "phase_sin_q2" )"2" "2" (assert ) nil nil ))nil ))nil )"3" rewrite "phase_sin_q3" )"3" "3" (assert ) nil nil ))nil ))nil )"4" rewrite "phase_sin_q4" )"4" "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))0 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)) = (LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): -sin(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" "identity_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" )"1" "deriv_id_fun[{x: real | -pi / 4 < x & x < pi / 4}]" )"1" (expand "I" )"1" "const_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "b" "1" ))"1" "deriv_const_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "b" "1" ))"1" expand "const_fun" )"1" "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" "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" "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" "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" "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" "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" 1 )"1" "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" "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" 1 2 13 1 ))"1" "identity_derivable_fun[{x:nnreal|x<pi/4}]" )"1" "deriv_id_fun[{x:nnreal|x<pi/4}]" )"1" expand "I" )"1" expand "const_fun" )"1" "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" "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" "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" 1 )"1" 1 )"1" rewrite "cos_0" )"1" assert )nil nil ))nil ))nil )"2" replace 1 1 )"2" 1 )"2" rewrite "sin_0" )"2" assert )nil nil ))nil ))nil ))nil )"3" assert )nil nil )"4" 2 )"4" "4" replace 1 )"4" 2 )"4" 1 2 ))"4" "sin_ub" "px" "y!1" ))"1" "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" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 1 )"2" "2" case "x!1=0" )"1" "pi/8" )"1" assert )nil nil ))nil )"2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" 1 )"3" "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" "floor_0" "x" "pi / 4 / (2 * pi)" ))"1" 1 )"1" 1 )"1" 1 )"1" replace -1 )"1" 4 1 ))"1" 1 -2 )"1" rewrite "cos_phase_pi4" )"1" expand "cos_phase" )"1" rewrite "phase_cos_q1" 1 )"1" assert )"1" "identity_derivable_fun[{x:nnreal|pi/4<=x&x<pi}]" )"1" "deriv_id_fun[{x:nnreal|pi/4<=x&x<pi}]" )"1" "const_derivable_fun[{x:nnreal|pi/4<=x&x<pi}]" "b" "1" ))"1" "deriv_const_fun[{x:nnreal|pi/4<=x&x<pi}]" "b" "1" ))"1" expand "I" )"1" expand "const_fun" )"1" "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" "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" "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" "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" "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" "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" "cos_value_derivable2" )"1" "deriv_cos_value" )"1" "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" "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" 7 8 9 10 11 12 13 14 )"1" "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" "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" "positive_derivative[{x: nnreal | pi / 4 <= x & x < pi}]" "g" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): 1 + 1 / 2 * (x * x)")) "1" 1 )"1" expand "strict_increasing?" )"1" 1 10 11 12 1 ))"1" "pi/4" "px" )"1" rewrite "cos_value_pi4" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" 2 )"2" expand "deriv" 1 )"2" "extensionality_postulate" "f" "(LAMBDA (x_1: {x: nnreal | pi / 4 <= x & x < pi}): LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}):1 + 1 / 2 * (x * x)," "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 "1" 2 "x!1" )"1" replace 2 1 )"1" 10 11 12 1 ))"1" case "x!1 < pi / 2" )"1" 2 3 4 )"1" assert )"1" "sin_ub" "px" "x!1" ))"1" expand "sin" )"1" "floor_0" "x" "x!1/(2*pi)" ))"1" assert )"1" rewrite "div_mult_pos_lt1" 1 )"1" 1 )"1" replace 1 )"1" 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" 2 3 4 1 )"1" "sin_ub" "px" "x!1" ))"1" expand "sin" )"1" "floor_0" "x" "x!1 / (2 * pi)" ))"1" assert )"1" rewrite "div_mult_pos_lt1" 1 )"1" 1 )"1" replace 1 )"1" 2 )"1" 1 )"1" case "sin_value(pi - x!1) = sin_phase(x!1)" )"1" replace 1 )"1" assert )nil nil ))nil )"2" 1 2 )"2" rewrite "sin_q2" 1 )"1" rewrite "sin_eqv_cos_value" )"1" "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" 1 )"2" "2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil )"3" 1 )"3" "3" expand "abs" 1 )"3" assert )nil nil ))nil ))nil ))nil )"4" 1 )"4" "4" "x!3" )"4" case "x!3=pi/4" )"1" "pi/2" )"1" assert )nil nil ))nil )"2" "pi/4" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"5" 1 )"5" "5" assert )nil nil ))nil ))nil )"6" 2 )"6" "6" expand "derivable" 2 )"6" 2 "x!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 1 )"2" "2" case "x!1=pi/2" )"1" "pi/3" )"1" assert )nil nil ))nil )"2" "pi/2" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" 1 )"3" "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" 1 )"2" "2" case "x!1=pi/4" )"1" "pi/2" )"1" assert )nil nil ))nil )"2" "pi/4" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" 1 )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 1 )"2" rewrite "div_div2" )"2" "div_cancel1" "x" "1/8" "n0z" "pi" ))"2" replace -1 )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" 1 )"3" "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" 1 )"1" replace -1 )"1" 1 )"1" 1 )"1" rewrite "cos_phase_pi4" )"1" case "314/100<=pi&pi<=315/100" )"1" "1" "le_times_le_pos" "nnx" "pi/4" "y" "315/400" "nnz" "pi/4" "w" "315/400" ))"1" assert )"1" "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" "sq_lt" "nna" "221404 / 320000" "nnb" "sqrt(1/2)" ))"1" 1 )"1" 2 )"1" rewrite "sq_sqrt" )"1" 1 )"1" assert )nil nil )"2" 1 )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 2 )"2" "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" "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" "identity_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" )"1" "deriv_id_fun[{x: real | -pi / 4 < x & x < pi / 4}]" )"1" (expand "I" )"1" "const_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "b" "pi/4" ))"1" "deriv_const_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "b" "pi/4" ))"1" expand "const_fun" )"1" "sin_value_derivable2" )"1" "cos_value_derivable2" )"1" "deriv_sin_value" )"1" "deriv_cos_value" )"1" "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" "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" "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" "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" "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" "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" "sum_derivable_fun" "f1" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): 4 )" "f2" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): 4 )")) "1" expand "+" )"1" 8 9 10 11 12 13 14 15 ))"1" assert )"1" "deriv_sum_fun" "ff1" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): 4 )" "ff2" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): 4 )")) "1" replace 3 )"1" replace 4 )"1" expand "abs" 1 4 ))"1" expand "+" )"1" "scal_derivable_fun" "f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 4 ) + sin_value(x + pi / 4 )" "b" "sqrt(1/2)" ))"1" assert )"1" expand "*" )"1" "deriv_scal_fun" "ff" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 4 ) + sin_value(x + pi / 4 )" "b" "sqrt(1/2)" ))"1" replace 3 )"1" expand "*" )"1" 1 2 11 1 ))"1" "extensionality" "f" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): 4 ) * sqrt(1 / 2 ) +4 ) * sqrt(1 / 2 )" "g" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 4 ) * sqrt(1 / 2 ) + sin(x + pi / 4 ) * sqrt(1 / 2 )")) "1" 1 )"1" replace 1 )"1" "extensionality" "f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 4 ) * sqrt(1 / 2 ) +1 / 2 ) * -sin_value(x + pi / 4 )" "g" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): -sin(x)" ))"1" 1 )"1" replace 1 )"1" nil nil ))nil )"2" 1 )"2" "2" "sin_minus" "a" "x!1+pi/4" "b" "pi/4" ))"2" replace 1 1 )"2" 1 )"2" expand "sin" )"2" expand "cos" )"2" rewrite "div_div2" )"2" "div_cancel1" "x" "1/8" "n0z" "pi" ))"2" replace 1 )"2" "floor_0" "x" "1/8" ))"2" 1 )"2" 1 3 )"2" 1 )"1" replace 1 )"1" 1 )"1" "1" rewrite "cos_phase_pi4" )"1" rewrite "sin_phase_pi4" )"1" "x!1" )"1" "floor_0" "x" "(pi / 4 + x!1) / (2 * pi)" ))"1" rewrite "div_mult_pos_lt1" 1 )"1" rewrite "div_mult_pos_le2" 1 )"1" 1 )"1" replace 1 )"1" 1 )"1" rewrite "sin_q1" )"1" rewrite "cos_q1" )"1" assert )nil nil )"2" 2 )"2" assert )"2" "phase_sin_q1" "x" "(pi / 4) + x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" 2 3 1 ))"2" "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" 1 )"2" "2" expand "cos" )"2" expand "sin" )"2" "floor_0" "x" "(pi / 4 + x!1) / (2 * pi)" ))"2" 1 )"2" 2 )"1" replace 1 )"1" 1 2 )"1" "1" rewrite "sin_q1" )"1" rewrite "cos_q1" )"1" 2 )"1" "x!1" )"1" "phase_sin_q1" "x" "pi/4+x!1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "phase_sin_q1" "x" "pi/4+x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" 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" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" 1 )"2" nil nil ))nil )"3" 1 )"3" "3" case "x!1=0" )"1" "pi/4" )"1" assert )nil nil )"2" expand "abs" 1 )"2" "pi" )"2" assert )nil nil ))nil ))nil ))nil )"2" "0" )"1" assert )nil nil )"2" expand "abs" 1 )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"4" 1 )"4" "4" "x!1" )"4" "y!1" )"4" replace "K1" "pi/2" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 1 )"2" "2" case "x!1=pi/2" )"1" "pi/3" )"1" assert )nil nil ))nil )"2" "pi/2" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" 1 )"3" "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" "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" "div_cancel1" "x" "1/8" "n0z" "pi" ))"2" replace -1 )"2" "floor_0" ("x" "1/8" ))"2" 1 )"2" 1 -3 )"2" 1 )"1" replace -1 )"1" 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" "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/4))" ))"1" (split -1 )"1" (replace -1 1 )"1" (hide-all-but 1 )"1" (lemma "cos_value_derivable2" )"1" (lemma "sin_value_derivable2" )"1" "identity_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" )"1" "deriv_id_fun[{x: real | -pi / 4 < x & x < pi / 4}]" )"1" (expand "I" )"1" "const_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "b" "pi/4" ))"1" "deriv_const_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "b" "pi/4" ))"1" expand "const_fun" )"1" "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" "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" "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" "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" "sum_derivable_fun" "f1" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): 4 )" "f2" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): 4 )")) "1" assert )"1" expand "+" )"1" "scal_derivable_fun" "b" "sqrt(1/2)" "f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 4 ) + sin_value(x + pi / 4 )")) "1" assert )"1" expand "*" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 1 )"2" "2" case "x!1=pi/2" )"1" "pi/4" )"1" assert )nil nil ))nil )"2" "pi/2" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" 1 )"3" "3" assert )nil nil ))nil ))nil ))nil )"2" 1 )"2" "2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil )"3" 1 )"3" "3" case "x!1=0" )"1" "pi/4" )"1" assert )nil nil )"2" expand "abs" )"2" assert )"2" "pi" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "0" )"1" assert )nil nil )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"4" 1 )"4" "4" "x!1" )"4" "y!1" )"4" replace "K1" "pi/2" )"4" 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" "div_cancel1" "x" "1/8" "n0z" "pi" ))"2" replace -1 )"2" "floor_0" ("x" "1/8" ))"2" 1 )"2" 1 )"2" 1 )"2" replace -1 )"2" 1 )"2" "floor_0" "x" "(pi / 4 + x!1) / (2 * pi)" ))"2" 1 )"2" 1 -3 -4 )"2" 1 )"1" replace -1 )"1" 1 )"1" 1 )"1" rewrite "cos_phase_pi4" )"1" rewrite "sin_phase_pi4" )"1" "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" 2 )"2" "div_mult_pos_le2" "z" "pi / 4 + x!1" "py" "2*pi" "x" "0" ))"2" assert )nil nil ))nil ))nil )"3" 2 )"3" "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" "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 )nil trig_basic nil )nil trig_basic nil )nil trig_basic nil )nil trig_basic nil )"posreal" trig_basic nil )"posreal" trig_basic nil )nil sq "reals/" )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"nonneg_real" sq "reals/" )nil sqrt "reals/" ))nil )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)) = (LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): -sin(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" "identity_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" )"1" "deriv_id_fun[{x: real | -pi / 4 < x & x < pi / 4}]" )"1" (expand "I" )"1" "const_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "b" "1" ))"1" "deriv_const_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "b" "1" ))"1" expand "const_fun" )"1" "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" "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" "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" "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" "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" "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" 1 )"1" "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" "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" 1 2 13 1 ))"1" "identity_derivable_fun[{x:nnreal|x<pi/4}]" )"1" "deriv_id_fun[{x:nnreal|x<pi/4}]" )"1" expand "I" )"1" expand "const_fun" )"1" "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" "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" "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" 1 )"1" 1 )"1" rewrite "cos_0" )"1" assert )nil nil ))nil ))nil )"2" replace 1 1 )"2" 1 )"2" rewrite "sin_0" )"2" assert )nil nil ))nil ))nil ))nil )"3" assert )nil nil )"4" 2 )"4" "4" replace 1 )"4" 2 )"4" 1 2 ))"4" "sin_ub" "px" "y!1" ))"1" "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" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 1 )"2" "2" case "x!1=0" )"1" "pi/8" )"1" assert )nil nil ))nil )"2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" 1 )"3" "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" "floor_0" "x" "pi / 4 / (2 * pi)" ))"1" 1 )"1" 1 )"1" 1 )"1" replace -1 )"1" 4 1 ))"1" 1 -2 )"1" rewrite "cos_phase_pi4" )"1" expand "cos_phase" )"1" rewrite "phase_cos_q1" 1 )"1" assert )"1" "identity_derivable_fun[{x:nnreal|pi/4<=x&x<pi}]" )"1" "deriv_id_fun[{x:nnreal|pi/4<=x&x<pi}]" )"1" "const_derivable_fun[{x:nnreal|pi/4<=x&x<pi}]" "b" "1" ))"1" "deriv_const_fun[{x:nnreal|pi/4<=x&x<pi}]" "b" "1" ))"1" expand "I" )"1" expand "const_fun" )"1" "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" "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" "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" "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" "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" "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" "cos_value_derivable2" )"1" "deriv_cos_value" )"1" "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" "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" 7 8 9 10 11 12 13 14 )"1" "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" "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" "positive_derivative[{x: nnreal | pi / 4 <= x & x < pi}]" "g" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): 1 + 1 / 2 * (x * x)")) "1" 1 )"1" expand "strict_increasing?" )"1" 1 10 11 12 1 ))"1" "pi/4" "px" )"1" rewrite "cos_value_pi4" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" 2 )"2" expand "deriv" 1 )"2" "extensionality_postulate" "f" "(LAMBDA (x_1: {x: nnreal | pi / 4 <= x & x < pi}): LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}):1 + 1 / 2 * (x * x)," "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 "1" 2 "x!1" )"1" replace 2 1 )"1" 10 11 12 1 ))"1" case "x!1 < pi / 2" )"1" 2 3 4 )"1" assert )"1" "sin_ub" "px" "x!1" ))"1" expand "sin" )"1" "floor_0" "x" "x!1/(2*pi)" ))"1" assert )"1" rewrite "div_mult_pos_lt1" 1 )"1" 1 )"1" replace 1 )"1" 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" 2 3 4 1 )"1" "sin_ub" "px" "x!1" ))"1" expand "sin" )"1" "floor_0" "x" "x!1 / (2 * pi)" ))"1" assert )"1" rewrite "div_mult_pos_lt1" 1 )"1" 1 )"1" replace 1 )"1" 2 )"1" 1 )"1" case "sin_value(pi - x!1) = sin_phase(x!1)" )"1" replace 1 )"1" assert )nil nil ))nil )"2" 1 2 )"2" rewrite "sin_q2" 1 )"1" rewrite "sin_eqv_cos_value" )"1" "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" 1 )"2" "2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil )"3" 1 )"3" "3" expand "abs" 1 )"3" assert )nil nil ))nil ))nil ))nil )"4" 1 )"4" "4" "x!3" )"4" case "x!3=pi/4" )"1" "pi/2" )"1" assert )nil nil ))nil )"2" "pi/4" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"5" 1 )"5" "5" assert )nil nil ))nil ))nil )"6" 2 )"6" "6" expand "derivable" 2 )"6" 2 "x!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 1 )"2" "2" case "x!1=pi/2" )"1" "pi/3" )"1" assert )nil nil ))nil )"2" "pi/2" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" 1 )"3" "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" 1 )"2" "2" case "x!1=pi/4" )"1" "pi/2" )"1" assert )nil nil ))nil )"2" "pi/4" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" 1 )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 1 )"2" rewrite "div_div2" )"2" "div_cancel1" "x" "1/8" "n0z" "pi" ))"2" replace -1 )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" 1 )"3" "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" 1 )"1" replace -1 )"1" 1 )"1" 1 )"1" rewrite "cos_phase_pi4" )"1" case "314/100<=pi&pi<=315/100" )"1" "1" "le_times_le_pos" "nnx" "pi/4" "y" "315/400" "nnz" "pi/4" "w" "315/400" ))"1" assert )"1" "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" "sq_lt" "nna" "221404 / 320000" "nnb" "sqrt(1/2)" ))"1" 1 )"1" 2 )"1" rewrite "sq_sqrt" )"1" 1 )"1" assert )nil nil )"2" 1 )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 2 )"2" "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" "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" "identity_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" )"1" "deriv_id_fun[{x: real | -pi / 4 < x & x < pi / 4}]" )"1" (expand "I" )"1" "const_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "b" "pi/4" ))"1" "deriv_const_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "b" "pi/4" ))"1" expand "const_fun" )"1" "sin_value_derivable2" )"1" "cos_value_derivable2" )"1" "deriv_sin_value" )"1" "deriv_cos_value" )"1" "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" "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" "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" "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" "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" "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" "sum_derivable_fun" "f1" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): 4 )" "f2" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): 4 )")) "1" expand "+" )"1" 8 9 10 11 12 13 14 15 ))"1" assert )"1" "deriv_sum_fun" "ff1" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): 4 )" "ff2" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): 4 )")) "1" replace 3 )"1" replace 4 )"1" expand "abs" 1 4 ))"1" expand "+" )"1" "scal_derivable_fun" "f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 4 ) + sin_value(x + pi / 4 )" "b" "sqrt(1/2)" ))"1" assert )"1" expand "*" )"1" "deriv_scal_fun" "ff" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 4 ) + sin_value(x + pi / 4 )" "b" "sqrt(1/2)" ))"1" replace 3 )"1" expand "*" )"1" 1 2 11 1 ))"1" "extensionality" "f" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): 4 ) * sqrt(1 / 2 ) +4 ) * sqrt(1 / 2 )" "g" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 4 ) * sqrt(1 / 2 ) + sin(x + pi / 4 ) * sqrt(1 / 2 )")) "1" 1 )"1" replace 1 )"1" "extensionality" "f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 4 ) * sqrt(1 / 2 ) +1 / 2 ) * -sin_value(x + pi / 4 )" "g" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): -sin(x)" ))"1" 1 )"1" replace 1 )"1" nil nil ))nil )"2" 1 )"2" "2" "sin_minus" "a" "x!1+pi/4" "b" "pi/4" ))"2" replace 1 1 )"2" 1 )"2" expand "sin" )"2" expand "cos" )"2" rewrite "div_div2" )"2" "div_cancel1" "x" "1/8" "n0z" "pi" ))"2" replace 1 )"2" "floor_0" "x" "1/8" ))"2" 1 )"2" 1 3 )"2" 1 )"1" replace 1 )"1" 1 )"1" "1" rewrite "cos_phase_pi4" )"1" rewrite "sin_phase_pi4" )"1" "x!1" )"1" "floor_0" "x" "(pi / 4 + x!1) / (2 * pi)" ))"1" rewrite "div_mult_pos_lt1" 1 )"1" rewrite "div_mult_pos_le2" 1 )"1" 1 )"1" replace 1 )"1" 1 )"1" rewrite "sin_q1" )"1" rewrite "cos_q1" )"1" assert )nil nil )"2" 2 )"2" assert )"2" "phase_sin_q1" "x" "(pi / 4) + x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" 2 3 1 ))"2" "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" 1 )"2" "2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" 1 )"2" "2" expand "cos" )"2" expand "sin" )"2" "floor_0" "x" "(pi / 4 + x!1) / (2 * pi)" ))"2" 1 )"2" 2 )"1" replace 1 )"1" 1 2 )"1" "1" rewrite "sin_q1" )"1" rewrite "cos_q1" )"1" 2 )"1" "x!1" )"1" "phase_sin_q1" "x" "pi/4+x!1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "phase_sin_q1" "x" "pi/4+x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" 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" 1 )"2" "2" case -replace "x!1 = 0" )"1" "pi/4" )"1" assert )nil nil )"2" expand "abs" )"2" if )"2" nil nil ))nil ))nil ))nil )"2" "0" )"1" assert )nil nil )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" 1 )"3" "3" "y!1" )"3" "x!1" )"3" replace "K1" "pi/2" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 1 )"2" "2" case "x!1=pi/2" )"1" "pi/3" )"1" assert )nil nil ))nil )"2" "pi/2" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" 1 )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 2.61 Sekunden
(vorverarbeitet am 2026-06-04)
¤ *© Formatika GbR, Deutschland
