Impressum sincos.prf
Interaktion und
(sincosnil 3477822201"" (expand "not_one_element?" )"" (skosimp*)"" (inst-cp + "pi/4" )"" (inst + "pi/8" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"bool" deriv_domain_def "analysis/" )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil 3477822300"" (expand "not_one_element?" )"" (skosimp*)"" (inst-cp + "pi/4" )"" (inst + "pi/8" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil atan nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"bool" deriv_domain_def "analysis/" )"nzreal" real_typesnil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil ))nil 3477822312"" (expand "not_one_element?" )"" (skosimp*)"" (inst-cp + "pi/4" )"" (inst + "pi/8" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil sincos_quad nil )"posreal" atan nil ) (< const-decl "bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"bool" deriv_domain_def "analysis/" ))nil ))nil 3477822324"" (expand "not_one_element?" )"" (skosimp*)"" (inst-cp + "3*pi/4" )"" (inst-cp + "pi/2" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil ) (pi const-decl "posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" nil )"(total_order?[real])" nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"bool" deriv_domain_def "analysis/" )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil ))nil 3477822372"" (expand "not_one_element?" )"" (skosimp*)"" (inst-cp + "3*pi/4" )"" (inst + "pi/2" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil ) (pi const-decl "posreal" atan nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" nil )"(total_order?[real])" nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"bool" deriv_domain_def "analysis/" )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil ))nil 3477822408"" (expand "not_one_element?" )"" (skosimp*)"" (inst-cp + "pi/8" )"" (inst + "pi/10" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"bool" deriv_domain_def "analysis/" )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil ))nil 3477822445"" (expand "not_one_element?" )"" (skosimp*)"" (inst-cp + "pi/8" )"" (inst + "0" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"bool" deriv_domain_def "analysis/" )"nzreal" real_typesnil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil ))nil 3477822472"" (expand "connected?" )"" (skosimp*) (("" (assert ) nil nil )) nil )) nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"bool" deriv_domain_def "analysis/" )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil 3477822481"" (expand "connected?" )"" (skosimp*) (("" (assert ) nil nil )) nil )) nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"bool" deriv_domain_def "analysis/" )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil 3477822492"" (expand "connected?" )"" (skosimp*) (("" (assert ) nil nil )) nil )) nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"bool" deriv_domain_def "analysis/" )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil 3477822502"" (expand "connected?" )"" (skosimp*) (("" (assert ) nil nil )) nil )) nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"bool" deriv_domain_def "analysis/" )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil 3477822510"" (lemma "deriv_domain_co" )"" (inst - "0" "pi/2" )"" (assert )"" (expand "deriv_domain?" )"" (skosimp*)"" (inst - "e!1" "x!1" )"" (skosimp*) (("" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )"real" reals nil )"bool" deriv_domain_def "analysis/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil real_types nil )"bool" reals nil ) (<= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )nil deriv_domain "analysis/" ))nil 3477822569"" (lemma "deriv_domain_open" )"" (inst - "-pi/2" "pi/2" ) nil nil )) nil )"nzreal" nil )"posreal" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"nzreal" real_typesnil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil deriv_domain "analysis/" ))nil 3477822648"" (lemma "deriv_domain_co" )"" (inst - "pi/2" "pi" )"" (assert )"" (expand "deriv_domain?" )"" (skosimp*)"" (inst - "e!1" "x!1" )"" (skosimp*) (("" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )"real" reals nil )"bool" deriv_domain_def "analysis/" )"bool" reals nil ) (<= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil deriv_domain "analysis/" ))nil 3477822724"" (lemma "deriv_domain_open" )"" (inst - "0" "pi" )"" (assert )"" (expand "deriv_domain?" )"" (skosimp*)"" (inst - "e!1" "x!1" )"" (skosimp*) (("" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"nzreal" real_typesnil )nil sincos_quad nil )nil deriv_domain "analysis/" ))nil 3477822763"" (lemma "deriv_domain_co" )"" (inst - "pi/4" "pi" )"" (expand "deriv_domain?" )"" (skosimp*)"" (inst - "e!1" "x!1" )"" (skosimp*) (("" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil real_types nil )"bool" deriv_domain_def "analysis/" )"real" reals nil )nil deriv_domain "analysis/" ))nil 3477822797"" (lemma "deriv_domain_co" )"" (inst - "0" "pi/4" )"" (expand "deriv_domain?" )"" (skosimp*)"" (inst - "e!1" "x!1" )"" (skosimp*) (("" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil real_types nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" deriv_domain_def "analysis/" )"real" reals nil )nil deriv_domain "analysis/" ))nil 3477822834"" (lemma "deriv_domain_open" )"" (inst - "-pi/4" "pi/4" ) nil nil )) nil )"nzreal" nil )"posreal" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"nzreal" real_typesnil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil deriv_domain "analysis/" ))nil 3265619589"" (skosimp*)"" (typepred "cos(x!1)" ) (("" (propax) nil nil )) nil ))nil )"real" sincos_def nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"trig_range" sincos_defnil ))nil 3425655889"" (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" rewrite "sin_q1" )"1" "1" "sin_value_derivable_fun" )"1" "deriv_sin_value" )"1" "identity_derivable_fun[real_abs_lt_pi2]" )"1" "deriv_id_fun[real_abs_lt_pi2]" )"1" expand "I" )"1" expand "const_fun" )"1" "diff_derivable_fun[real_abs_lt_pi2]" "f1" "LAMBDA (x: real_abs_lt_pi2): x" "f2" "LAMBDA (x: real_abs_lt_pi2): sin_value(x)" ))"1" "deriv_diff_fun[real_abs_lt_pi2]" "ff1" "LAMBDA (x: real_abs_lt_pi2): x" "ff2" "LAMBDA (x: real_abs_lt_pi2): sin_value(x)" ))"1" replace -3 -1)"1" replace "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_pi2]" "f" "LAMBDA (x: {x: nnreal | x < pi / 2}): x" "g" "LAMBDA (x_1: real_abs_lt_pi2): x_1 - sin_value(x_1)" ))"1" replace "1" replace "1" expand "o" )"1" "deriv_comp_fun[{x: nnreal | x < pi / 2},real_abs_lt_pi2]" "ff" "LAMBDA (x: {x: nnreal | x < pi / 2}): x" "gg" "LAMBDA (x_1: real_abs_lt_pi2): x_1 - sin_value(x_1)" ))"1" expand "o" )"1" replace "1" replace "1" expand "*" "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" rewrite "sin_value_0" )"1" assert )nil nil ))nil ))nil )"2" replace "2" assert )"2" expand "abs" )"2" rewrite "cos_value_0" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" assert )nil nil )"4" replace "4" "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 )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "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" "3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "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" "3" "3" 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 real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil ) (<= const-decl "bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" atan nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil floor_ceil nil )"posreal" nil )nil real_props nil )"(total_order?[real])" nil )nil real_axioms nil )nil sincos_quad nil )nil derivatives "analysis/" )nil derivatives "analysis/" )nil asin nil )nil asin nil )"[real_abs_le_pi2 -> real_abs_le1]" nil )"[T -> real]" real_fun_ops "reals/" )"T3" function_props nil )nil derivative_props "analysis/" )"bool" deriv_domain_def "analysis/" )nil sincos_quad nil )nil acos nil )"(total_order?[real])" nil )"[nnreal_le_pi -> real_abs_le1]" sincos_quadnil )nil real_types nil )"bool" real_fun_preds "reals/" )"real" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"even_int" integersnil )nil sincos_quad nil )"{j: nonneg_int | j >= i}" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )nil sincos_quad nil )"[T -> real]" real_fun_ops "reals/" )nil chain_rule "analysis/" )"[numfield, numfield -> numfield]" number_fields nil )nil chain_rule "analysis/" )nil derivatives "analysis/" )"bool" derivatives "analysis/" )nil derivatives "analysis/" )"(bijective?[T, T])" identity nil )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def "analysis/" )"nzreal" real_typesnil )nil atan nil )"[numfield -> numfield]" number_fields nil )nil derivatives "analysis/" )nil sincos_quad nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil real_types nil )nil sincos_phase nil )"[T, T -> boolean]" equalities nil )"posrat" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )nil atan nil )"real" reals nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"posint" nil )"real" sincos_def nil )"nnreal" nil )"nat" floor_ceil nil )"posreal" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"odd_int" integers nil )"trig_range" sincos_def nil )NOT const-decl "[bool -> bool]" booleans nil ))nil )nil 3408979329"" (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" rewrite "sin_q1" )"1" "1" "sin_value_derivable2" )"1" "deriv_sin_value" )"1" "identity_derivable_fun[real_abs_lt_pi2]" )"1" "deriv_id_fun[real_abs_lt_pi2]" )"1" expand "I" )"1" expand "const_fun" )"1" "diff_derivable_fun[real_abs_lt_pi2]" "f1" "LAMBDA (x: real_abs_lt_pi2): x" "f2" "LAMBDA (x: real_abs_lt_pi2): sin_value(x)" ))"1" "deriv_diff_fun[real_abs_lt_pi2]" "ff1" "LAMBDA (x: real_abs_lt_pi2): x" "ff2" "LAMBDA (x: real_abs_lt_pi2): sin_value(x)" ))"1" replace -3 -1)"1" replace "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_pi2]" "f" "LAMBDA (x: {x: nnreal | x < pi / 2}): x" "g" "LAMBDA (x_1: real_abs_lt_pi2): x_1 - sin_value(x_1)" ))"1" replace "1" replace "1" expand "o" )"1" "deriv_comp_fun[{x: nnreal | x < pi / 2},real_abs_lt_pi2]" "ff" "LAMBDA (x: {x: nnreal | x < pi / 2}): x" "gg" "LAMBDA (x_1: real_abs_lt_pi2): x_1 - sin_value(x_1)" ))"1" expand "o" )"1" replace "1" replace "1" expand "*" "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" rewrite "sin_value_0" )"1" assert )nil nil ))nil ))nil )"2" replace "2" assert )"2" expand "abs" )"2" rewrite "cos_value_0" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" assert )nil nil )"4" replace "4" "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 ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "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" "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" "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" "3" "3" "x!1" )"3" "y!1" )"3" "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 )"posreal" atan nil )nil sincos_quad nil )"real" integral_def "analysis/" )"real" atan nil )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivative_props "analysis/" )nil sincos_quad nil )nil acos nil )"[nnreal_le_pi -> real_abs_le1]" sincos_quadnil )"bool" real_fun_preds "reals/" )nil sincos_quad nil )nil sincos_quad nil )nil chain_rule "analysis/" )nil chain_rule "analysis/" )"[real_abs_le_pi2 -> real_abs_le1]" nil )nil asin nil )nil asin nil )nil derivatives "analysis/" )nil atan nil )nil derivatives "analysis/" )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil atan nil )"real" sincos_def nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"trig_range" sincos_def nil ))nil )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" rewrite "sin_q1" )"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[real_abs_lt_pi]" "f1" "LAMBDA (x: real_abs_lt_pi): x" "f2" "LAMBDA (x: real_abs_lt_pi): sin_value(x)" ))"1" "deriv_diff_fun[real_abs_lt_pi]" "ff1" "LAMBDA (x: real_abs_lt_pi): x" "ff2" "LAMBDA (x: real_abs_lt_pi): sin_value(x)" ))"1" replace -3 -1)"1" replace "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 "1" replace "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 "1" replace "1" expand "*" "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" rewrite "sin_value_0" )"1" assert )nil nil ))nil ))nil )"2" replace "2" assert )"2" expand "abs" )"2" rewrite "cos_value_0" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" assert )nil nil )"4" replace "4" "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 ))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" "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" "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 )"2" "2" assert )"2" "x!1" )"2" expand "abs" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "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" "3" "3" "x!1" )"3" "y!1" )"3" "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 )"posreal" atan nil )nil sincos_quad nil )"real" integral_def "analysis/" )"real" atan nil )"real_abs_lt_pi2" atan nil )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivative_props "analysis/" )nil sincos_quad nil )nil acos nil )"[nnreal_le_pi -> real_abs_le1]" sincos_quadnil )"bool" real_fun_preds "reals/" )nil sincos_quad nil )nil sincos_quad nil )nil chain_rule "analysis/" )nil chain_rule "analysis/" )"[real_abs_le_pi2 -> real_abs_le1]" nil )nil asin nil )nil asin nil )nil derivatives "analysis/" )nil derivatives "analysis/" )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil atan nil )"real" sincos_def nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"trig_range" sincos_def nil ))nil )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" rewrite "sin_q1" )"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 "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 "1" replace "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 "1" replace "1" expand "*" "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" rewrite "sin_value_0" )"1" assert )nil nil ))nil ))nil )"2" replace "2" assert )"2" expand "abs" )"2" rewrite "cos_value_0" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" assert )nil nil )"4" replace "4" "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" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" expand "abs" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "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" "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" "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" "3" "3" "x!1" )"3" "y!1" )"3" "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 )"posreal" atan nil )nil sincos_quad nil )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil sincos_quad nil )nil acos nil )"[nnreal_le_pi -> real_abs_le1]" sincos_quadnil )"bool" real_fun_preds "reals/" )nil sincos_quad nil )nil sincos_quad nil )nil chain_rule "analysis/" )nil chain_rule "analysis/" )"[real_abs_le_pi2 -> real_abs_le1]" nil )nil asin nil )nil derivatives "analysis/" )nil derivatives "analysis/" )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil atan nil ))nil 3445347248"" (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" "prod_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "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[{x: real | -pi / 4 < x & x < pi / 4}]" "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[{x: real | -pi / 4 < x & x < pi / 4}]" "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[{x: real | -pi / 4 < x & x < pi / 4}]" "b" "1/2" "ff" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1 * x_1" ))"1" replace "1" expand "*" )"1" "diff_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "f1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 1" "f2" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): ")) "1" assert )"1" expand "-" )"1" "deriv_diff_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "ff1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 1" "ff2" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): ")) "1" expand "-" )"1" replace "1" replace "1" "1" "diff_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "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" assert )"1" expand "-" )"1" "deriv_diff_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "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" replace "1" replace "1" expand "-" )"1" "1" "identity_derivable_fun[{x:nnreal|x<pi/4}]" )"1" "deriv_id_fun[{x:nnreal|x<pi/4}]" )"1" expand "I" )"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 "1" replace "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" rewrite "cos_0" )"1" assert )nil nil ))nil ))nil )"2" replace "2" "2" rewrite "sin_0" )"2" assert )nil nil ))nil ))nil ))nil )"3" assert )nil nil )"4" "4" "4" replace "4" "4" "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 ))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" "floor_0" ("x" "px / (2 * pi)" ))"3" (flatten -1)"3" "3" "1" replace -1)"1" "floor_0" "x" "pi / 4 / (2 * pi)" ))"1" "1" "1" "1" replace -1)"1" "1" "1" rewrite "cos_phase_pi4" )"1" expand "cos_phase" )"1" rewrite "phase_cos_q1" "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" "prod_derivable_fun[{x: nnreal | pi / 4 <= x & x < pi}]" "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[{x: nnreal | pi / 4 <= x & x < pi}]" "ff1" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): x" "ff2" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): x" ))"1" replace "1" expand "*" )"1" expand "+" )"1" "scal_derivable_fun[{x: nnreal | pi / 4 <= x & x < pi}]" "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[{x: nnreal | pi / 4 <= x & x < pi}]" "b" "1/2" "ff" "LAMBDA (x_1: {x: nnreal | pi / 4 <= x & x < pi}): x_1 * x_1" ))"1" replace "1" expand "*" )"1" "diff_derivable_fun[{x: nnreal | pi / 4 <= x & x < pi}]" "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[{x: nnreal | pi / 4 <= x & x < pi}]" "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 "1" replace "1" expand "-" )"1" "cos_value_derivable_fun" )"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 "1" replace "1" expand "*" )"1" "1" "diff_derivable_fun[{x: nnreal | pi / 4 <= x & x < pi}]" "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[{x: nnreal | pi / 4 <= x & x < pi}]" "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 "1" replace "1" expand "-" )"1" "positive_derivative[{x: nnreal | pi / 4 <= x & x < pi}]" "g" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): ")) "1" "1" expand "strict_increasing?" )"1" "1" "pi/4" "px" )"1" rewrite "cos_value_pi4" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "deriv" "2" "1" "x!1" )"1" "1" "1" case "x!1 < pi / 2" )"1" "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" replace "1" "1" rewrite "sin_q1" "1" assert )nil nil )"2" rewrite "phase_sin_q1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "pi/2<=x!1" )"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" replace "1" "1" "1" case "sin_value(pi - x!1) = sin_phase(x!1)" )"1" replace "1" assert )nil nil ))nil )"2" "2" rewrite "sin_q2" "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 )"2" expand "derivable?" "2" 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 ))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" "2" rewrite "div_div2" )"2" "div_cancel1" "x" "1/8" "n0z" "pi" ))"2" replace -1)"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" "div_cancel1" "x" "1/8" "n0z" "pi" ))"3" rewrite "div_div2" "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" "floor_0" ("x" "pi / 4 / (2 * pi)" ))"2" (rewrite "div_div2" )"2" "div_cancel1" "x" "1/8" "n0z" "pi" ))"2" (replace -1)"2" "2" "2" "2" "1" replace -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" rewrite "sq_sqrt" )"1" "1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"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" "sin_value_derivable_fun" )"1" "cos_value_derivable_fun" )"1" "deriv_sin_value" )"1" "deriv_cos_value" )"1" "sum_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "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[{x: real | -pi / 4 < x & x < pi / 4}]" "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_pi2]" "f" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1+pi/4" "g" "LAMBDA (x: real_abs_lt_pi2): sin_value(x)" ))"1" assert )"1" expand "o" )"1" "deriv_comp_fun[{x: real | -pi / 4 < x & x < pi / 4},real_abs_lt_pi2]" "ff" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1+pi/4" "gg" "LAMBDA (x: real_abs_lt_pi2): 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 "1" replace "1" replace "1" expand "o" )"1" expand "*" )"1" "sum_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "f1" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): " "f2" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): ")) "1" expand "+" )"1" "1" assert )"1" "deriv_sum_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "ff1" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): " "ff2" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): ")) "1" replace "1" replace "1" expand "abs" "1" expand "+" )"1" "scal_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): " "b" "sqrt(1/2)" ))"1" assert )"1" expand "*" )"1" "deriv_scal_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "ff" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): " "b" "sqrt(1/2)" ))"1" replace "1" expand "*" )"1" "1" "extensionality" "f" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): " "g" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): ")) "1" "1" replace "1" "extensionality" "f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): " "g" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): -sin(x)" ))"1" "1" replace "1" assert )nil nil ))nil )"2" "2" "2" "sin_minus" "a" "x!1+pi/4" "b" "pi/4" ))"2" replace "2" "2" expand "sin" )"2" expand "cos" )"2" rewrite "div_div2" )"2" "div_cancel1" "x" "1/8" "n0z" "pi" ))"2" replace "2" "floor_0" "x" "1/8" ))"2" "2" "2" "1" replace "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" rewrite "div_mult_pos_le2" "1" "1" replace "1" "1" rewrite "sin_q1" )"1" rewrite "cos_q1" )"1" assert )nil nil )"2" "2" assert )"2" "phase_sin_q1" "x" "(pi / 4) + x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "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" "2" "2" expand "cos" )"2" expand "sin" )"2" "floor_0" "x" "(pi / 4 + x!1) / (2 * pi)" ))"2" "2" "1" replace "1" "1" "1" rewrite "sin_q1" )"1" rewrite "cos_q1" )"1" "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" "2" assert )"2" rewrite "div_mult_pos_le2" )nil nil ))nil ))nil )"3" rewrite "div_mult_pos_lt1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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" "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" "2" "2" "1" replace -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))" ))"2" (split -1)"1" (replace -1 1)"1" (hide-all-but 1)"1" (lemma "cos_value_derivable_fun" )"1" (lemma "sin_value_derivable_fun" )"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" "sum_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "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[{x: real | -pi / 4 < x & x < pi / 4}]" "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_pi2]" "f" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1 + pi / 4" "g" "LAMBDA (x: real_abs_lt_pi2): 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[{x: real | -pi / 4 < x & x < pi / 4}]" "f1" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): " "f2" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): ")) "1" assert )"1" expand "+" )"1" "scal_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "b" "sqrt(1/2)" "f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): ")) "1" assert )"1" expand "*" )"1" nil nil ))nil ))nil ))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 )"2" (hide-all-but 1)"2" (skosimp*)"2" "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" "2" "2" "2" replace -1)"2" "2" "floor_0" "x" "(pi / 4 + x!1) / (2 * pi)" ))"2" "2" "2" "1" replace "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" rewrite "cos_q1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "div_mult_pos_le2" "z" "pi / 4 + x!1" "py" "2*pi" "x" "0" ))"2" assert )nil nil ))nil ))nil )"3" "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 ))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 )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )"real" reals nil )"[T, T -> boolean]" equalities nil )nil derivatives "analysis/" )"[T -> real]" derivatives "analysis/" )"real" sincos_def nil )"trig_range" sincos_defnil )nil real_props nil )nil sqrt "reals/" )"posreal" sq "reals/" )"nonneg_real" sq "reals/" )"{nnz: nnreal | nnz * nnz = nnx}" sqrt"reals/" )nil sq "reals/" )"posreal" atan_approx nil )"posreal" atan_approx nil )nil real_props nil )nil floor_ceil nil )nil sincos_phase nil )"posreal" sqrt "reals/" )nil sincos_phase nil )nil sincos_phase nil )"(total_order?[real])" real_props nil )"bool" reals nil )nil sincos_quad nil )nil sincos_quad nil )"bool" real_fun_preds"reals/" )nil sincos nil )nil sincos nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"[real_abs_le_pi2 -> real_abs_le1]" nil )nil asin nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" derivatives_def "analysis/" )"bool" derivatives_def "analysis/" )nil sincos_phase nil )nil sincos_phase nil )nil real_props nil )"nnreal" nil )nil sincos_phase nil )nil sincos_quad nil )nil sincos_quad nil )nil sincos_phase nil )"real_abs_le1" sincos_phase nil )nil derivative_props"analysis/" )nil sincos_quad nil )"[nnreal_le_pi -> real_abs_le1]" nil )nil asin nil )nil acos nil )nil sincos_quad nil )"real_abs_le1" sincos_phase nil )nil reals nil )nil real_props nil )nil real_props nil )"nat" floor_ceilnil )nil derivatives"analysis/" )"(bijective?[T, T])" identity nil )nil derivatives "analysis/" )"posreal" real_types nil )"trig_range" sincos_defnil )"(strict_total_order?[real])" real_props nil )nil derivatives "analysis/" )"posrat" nil )"real" realsnil )nil derivatives"analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives"analysis/" )"[T -> real]" real_fun_ops "reals/" )nil real_types nil )nil chain_rule "analysis/" )nil trig_basic nil )"even_int" nil )"nonneg_rat" rationals nil )"even_int" nil )nil trig_basic nil )"(strict_total_order?[real])" real_props nil )nil sincos nil )"(total_order?[real])" real_props nil )nil nil )"bool" deriv_domain_def "analysis/" )nil derivative_props"analysis/" )"T3" function_props nil )"nnreal" real_types nil )"[numfield, numfield -> numfield]" nil )nil chain_rule"analysis/" )"real" realsnil )nil derivatives "analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives"analysis/" )nil derivatives"analysis/" )nil derivatives "analysis/" )"[numfield, numfield -> numfield]" nil )"[numfield, numfield -> numfield]" nil )"real" realsnil )nil functions nil )nil trig_basic nil )"odd_int" integersnil )nil derivatives "analysis/" )"{n: nonneg_real | n >= m AND n >= -m}" nil )nil trig_basic nil )"real" realsnil )nil sincos_phase nil )nil real_props nil )nil sincos_phase nil )"nzint" integersnil )nil atan nil )nil derivatives "analysis/" )nil sincos_quad nil )nil sincos_quad nil )"bool" deriv_domain_def"analysis/" )"bool" deriv_domain_def"analysis/" )"{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil )"nzreal" nil )"nzreal" nil )"posreal" real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"[numfield -> numfield]" number_fields nil )"bool" derivatives "analysis/" )"real" sincos_def nil )nil real_props nil )nil atan nil ))nil )nil 3425655957"" (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[{x: real | -pi / 4 < x & x < pi / 4}]" "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[{x: real | -pi / 4 < x & x < pi / 4}]" "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[{x: real | -pi / 4 < x & x < pi / 4}]" "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[{x: real | -pi / 4 < x & x < pi / 4}]" "b" "1/2" "ff" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1 * x_1" ))"1" replace "1" expand "*" )"1" "diff_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "f1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 1" "f2" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): ")) "1" assert )"1" expand "-" )"1" "deriv_diff_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "ff1" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): 1" "ff2" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): ")) "1" expand "-" )"1" replace "1" replace "1" "1" "diff_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "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" assert )"1" expand "-" )"1" "deriv_diff_fun[{x: real | -pi / 4 < x & x < pi / 4}]" "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" replace "1" replace "1" expand "-" )"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 "1" replace "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" rewrite "cos_0" )"1" assert )nil nil ))nil ))nil )"2" replace "2" "2" rewrite "sin_0" )"2" assert )nil nil ))nil ))nil ))nil )"3" assert )nil nil )"4" "4" "4" replace "4" "4" "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" "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" "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" "floor_0" ("x" "px / (2 * pi)" ))"3" (flatten -1)"3" "3" "1" replace -1)"1" "floor_0" "x" "pi / 4 / (2 * pi)" ))"1" "1" "1" "1" replace -1)"1" "1" "1" rewrite "cos_phase_pi4" )"1" expand "cos_phase" )"1" rewrite "phase_cos_q1" "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[{x: nnreal | pi / 4 <= x & x < pi}]" "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[{x: nnreal | pi / 4 <= x & x < pi}]" "ff1" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): x" "ff2" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): x" ))"1" replace "1" expand "*" )"1" expand "+" )"1" "scal_derivable_fun[{x: nnreal | pi / 4 <= x & x < pi}]" "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[{x: nnreal | pi / 4 <= x & x < pi}]" "b" "1/2" "ff" "LAMBDA (x_1: {x: nnreal | pi / 4 <= x & x < pi}): x_1 * x_1" ))"1" replace "1" expand "*" )"1" "diff_derivable_fun[{x: nnreal | pi / 4 <= x & x < pi}]" "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[{x: nnreal | pi / 4 <= x & x < pi}]" "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 "1" replace "1" expand "-" )"1" "cos_value_derivable_fun" )"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 "1" replace "1" expand "*" )"1" "1" "diff_derivable_fun[{x: nnreal | pi / 4 <= x & x < pi}]" "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[{x: nnreal | pi / 4 <= x & x < pi}]" "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 "1" replace "1" expand "-" )"1" "positive_derivative[{x: nnreal | pi / 4 <= x & x < pi}]" "g" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): ")) "1" "1" expand "strict_increasing?" )"1" "1" "pi/4" "px" )"1" rewrite "cos_value_pi4" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "deriv" "2" "extensionality_postulate" "f" "(LAMBDA (x_1: {x: nnreal | pi / 4 <= x & x < pi}): LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}):" "g" "(LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): IF x < pi / 2 THEN -sin_value(x) ELSE -sin_value(pi - x) ENDIF +")) "1" replace "1" "x!1" )"1" replace "1" "1" case "x!1 < pi / 2" )"1" "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" replace "1" "1" rewrite "sin_q1" "1" assert )nil nil )"2" rewrite "phase_sin_q1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "pi/2<=x!1" )"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" replace "1" "1" "1" case "sin_value(pi - x!1) = sin_phase(x!1)" )"1" replace "1" assert )nil nil ))nil )"2" "2" rewrite "sin_q2" "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" "2" "2" assert )nil nil ))nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil )"4" "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" "5" "5" assert )nil nil ))nil ))nil )"6" "6" "6" expand "derivable" "6" "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" "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" "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" "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" "3" "3" assert )nil nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.513 Sekunden
(vorverarbeitet am 2026-04-29)
¤ *© Formatika GbR, Deutschland
2026-05-26
