SSL sincos_def.prf
Interaktion und
(sincos_defnil 3265619589"" (skosimp*)"" (typepred "cos(x!1)" ) (("" (propax) nil nil )) nil )) nil )"real" trig_basic 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]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"trig_range" trig_basic 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" "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)"1" "deriv_id_fun[{x:nnreal|x)"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 )"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" "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 ))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 )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)"1" "deriv_id_fun[{x:nnreal|x)"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" )quality 100%
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.31Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤ *Eine klare Vorstellung vom Zielzustand
2026-03-28
