| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/trig_fnd/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 4 MB |
|
Quellcode-Bibliothek sincos.prfSprache: Lisp |
|||||||||||||||
|
(sincos (noa_nnreal_lt_pi2 0 (noa_nnreal_lt_pi2-1 nil 3477822201 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst-cp + "pi/4") (("" (inst + "pi/8") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((pi const-decl "posreal" atan nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil)) shostak)) (noa_real_lt_pi2 0 (noa_real_lt_pi2-1 nil 3477822300 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst-cp + "pi/4") (("" (inst + "pi/8") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil) (pi const-decl "posreal" atan nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil)) nil)) (noa_posreal_lt_pi 0 (noa_posreal_lt_pi-1 nil 3477822312 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst-cp + "pi/4") (("" (inst + "pi/8") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal_lt_pi nonempty-type-eq-decl nil sincos_quad nil) (pi const-decl "posreal" atan nil) (< const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/")) nil)) (noa_nnreal_pi4_to_pi 0 (noa_nnreal_pi4_to_pi-1 nil 3477822324 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst-cp + "3*pi/4") (("" (inst-cp + "pi/2") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((* const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (pi const-decl "posreal" atan nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil)) nil)) (noa_posreal_pi2_to_pi 0 (noa_posreal_pi2_to_pi-1 nil 3477822372 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst-cp + "3*pi/4") (("" (inst + "pi/2") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((* const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (pi const-decl "posreal" atan nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil)) nil)) (noa_nnreal_lt_pi4 0 (noa_nnreal_lt_pi4-1 nil 3477822408 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst-cp + "pi/8") (("" (inst + "pi/10") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((pi const-decl "posreal" atan nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil)) nil)) (noa_mpi4_to_pi4 0 (noa_mpi4_to_pi4-1 nil 3477822445 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst-cp + "pi/8") (("" (inst + "0") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((pi const-decl "posreal" atan nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil)) nil)) (conn_nnreal_lt_p2 0 (conn_nnreal_lt_p2-1 nil 3477822472 ("" (expand "connected?") (("" (skosimp*) (("" (assert) nil nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected? const-decl "bool" deriv_domain_def "analysis/") (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil)) shostak)) (conn_nnreal_pi4_to_pi 0 (conn_nnreal_pi4_to_pi-1 nil 3477822481 ("" (expand "connected?") (("" (skosimp*) (("" (assert) nil nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected? const-decl "bool" deriv_domain_def "analysis/") (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil)) shostak)) (conn_posreal_pi2_to_pi 0 (conn_posreal_pi2_to_pi-1 nil 3477822492 ("" (expand "connected?") (("" (skosimp*) (("" (assert) nil nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected? const-decl "bool" deriv_domain_def "analysis/") (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil)) shostak)) (conn_nnreal_lt_pi4 0 (conn_nnreal_lt_pi4-1 nil 3477822502 ("" (expand "connected?") (("" (skosimp*) (("" (assert) nil nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected? const-decl "bool" deriv_domain_def "analysis/") (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil)) shostak)) (deriv_domain_nnreal_lt_pi2 0 (deriv_domain_nnreal_lt_pi2-1 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) ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (pi const-decl "posreal" atan nil) (real_plus_real_is_real application-judgement "real" reals nil) (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nzreal nonempty-type-eq-decl nil reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (deriv_domain_co formula-decl nil deriv_domain "analysis/")) shostak)) (deriv_domain_real_abs_lt_pi2 0 (deriv_domain_real_abs_lt_pi2-1 nil 3477822569 ("" (lemma "deriv_domain_open") (("" (inst - "-pi/2" "pi/2") nil nil)) nil) ((nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (pi const-decl "posreal" atan nil) (deriv_domain_open formula-decl nil deriv_domain "analysis/")) shostak)) (deriv_domain_posreal_pi2_to_pi 0 (deriv_domain_posreal_pi2_to_pi-1 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) ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (pi const-decl "posreal" atan nil) (real_plus_real_is_real application-judgement "real" reals nil) (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nzreal nonempty-type-eq-decl nil reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (deriv_domain_co formula-decl nil deriv_domain "analysis/")) shostak)) (deriv_domain_posreal_lt_pi 0 (deriv_domain_posreal_lt_pi-1 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) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (pi const-decl "posreal" atan nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (deriv_domain_posreal_lt_pi formula-decl nil sincos_quad nil) (deriv_domain_open formula-decl nil deriv_domain "analysis/")) shostak)) (deriv_domain_nnreal_pi4_to_pi 0 (deriv_domain_nnreal_pi4_to_pi-1 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) ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (pi const-decl "posreal" atan nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nzreal nonempty-type-eq-decl nil reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (real_plus_real_is_real application-judgement "real" reals nil) (deriv_domain_co formula-decl nil deriv_domain "analysis/")) shostak)) (deriv_domain_nnreal_lt_pi4 0 (deriv_domain_nnreal_lt_pi4-1 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) ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (pi const-decl "posreal" atan nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nzreal nonempty-type-eq-decl nil reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (real_plus_real_is_real application-judgement "real" reals nil) (deriv_domain_co formula-decl nil deriv_domain "analysis/")) shostak)) (deriv_domain_mpi4_to_pi4 0 (deriv_domain_mpi4_to_pi4-1 nil 3477822834 ("" (lemma "deriv_domain_open") (("" (inst - "-pi/4" "pi/4") nil nil)) nil) ((nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (pi const-decl "posreal" atan nil) (deriv_domain_open formula-decl nil deriv_domain "analysis/")) shostak)) (cos_ub 0 (cos_ub-1 nil 3265619589 ("" (skosimp*) (("" (typepred "cos(x!1)") (("" (propax) nil nil)) nil)) nil) ((cos const-decl "real" sincos_def nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (cos_range application-judgement "trig_range" sincos_def nil)) shostak)) (sin_ub 0 (sin_ub-4 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" (lemma "both_sides_times_pos_lt1" ("x" "1" "y" "floor(px / (2 * pi))" "pz" "2*pi")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1 -2 -3) (("2" (simplify 1) (("2" (lemma "pi_bnds") (("2" (flatten) (("2" (lemma "phases_sin" ("x" "px")) (("2" (split -1) (("1" (rewrite "sin_q1") (("1" (hide -1) (("1" (lemma "sin_value_derivable_fun") (("1" (lemma "deriv_sin_value") (("1" (lemma "identity_derivable_fun[real_abs_lt_pi2]") (("1" (lemma "deriv_id_fun[real_abs_lt_pi2]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "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" (lemma "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 -5 -1) (("1" (expand "-") (("1" (assert) (("1" (lemma "identity_derivable_fun[{x:nnreal|x<pi/2}]") (("1" (lemma "deriv_id_fun[{x:nnreal|x<pi/2}]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "composition_derivable_fun[{x: nnreal | x < pi / 2},real_abs_lt_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 -3) (("1" (replace -5) (("1" (expand "o") (("1" (lemma "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 -3 -1) (("1" (replace -5 -1) (("1" (expand "*" -1) (("1" (lemma "minimum_derivative[{x: nnreal | x < pi / 2}]" ("g" "LAMBDA (x_1: {x: nnreal | x < pi / 2}): x_1 - sin_value(x_1)" "x" "0" "y1" "px")) (("1" (split -1) (("1" (simplify -1) (("1" (rewrite "sin_value_0") (("1" (assert) nil nil)) nil)) nil) ("2" (replace -1 1) (("2" (assert) (("2" (expand "abs") (("2" (rewrite "cos_value_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil) ("4" (replace -1 1) (("4" (hide-all-but 1) (("4" (skosimp*) (("4" (expand "abs") (("4" (lemma "cos_value_strict_decreasing") (("4" (expand "strict_decreasing?") (("4" (inst - "0" "y!1") (("4" (rewrite "cos_value_0") (("4" (assert) (("4" (lemma "posreal_times_posreal_is_posreal" ("px" "1-cos_value(y!1)" "py" "y!1")) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=0") (("1" (inst + "pi/4") (("1" (assert) nil nil)) nil) ("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (lemma deriv_domain_nnreal_lt) (("3" (inst - pi/2) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=0") (("1" (inst + "pi/4") (("1" (assert) nil nil)) nil) ("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (lemma deriv_domain_open) (("3" (inst - -pi/2 pi/2) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "phase_sin_q2") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil) ("3" (rewrite "phase_sin_q3") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil) ("4" (rewrite "phase_sin_q4") (("4" (flatten) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "sin(px)") (("2" (assert) nil nil)) nil)) nil)) nil) ((posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (pi const-decl "posreal" atan nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (floor_def formula-decl nil floor_ceil nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (div_mult_pos_le2 formula-decl nil real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (trichotomy formula-decl nil real_axioms nil) (deriv_sin_value formula-decl nil sincos_quad nil) (deriv_id_fun formula-decl nil derivatives "analysis/") (diff_derivable_fun formula-decl nil derivatives "analysis/") (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]" sincos_quad nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (O const-decl "T3" function_props nil) (minimum_derivative formula-decl nil derivative_props "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (cos_value_strict_decreasing formula-decl nil sincos_quad nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad nil) (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (strict_decreasing? const-decl "bool" real_fun_preds "reals/") (real_times_real_is_real application-judgement "real" reals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (cos_value_0 formula-decl nil sincos_quad nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_times_even_is_even application-judgement "even_int" integers nil) (sin_value_0 formula-decl nil sincos_quad nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (deriv_comp_fun formula-decl nil chain_rule "analysis/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (composition_derivable_fun formula-decl nil chain_rule "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (deriv_diff_fun formula-decl nil derivatives "analysis/") (I const-decl "(bijective?[T, T])" identity nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil) (- const-decl "[numfield -> numfield]" number_fields nil) (identity_derivable_fun formula-decl nil derivatives "analysis/") (sin_value_derivable_fun formula-decl nil sincos_quad nil) (sin_q1 formula-decl nil sincos_phase nil) (phase_sin_q2 formula-decl nil sincos_phase nil) (phase_sin_q3 formula-decl nil sincos_phase nil) (phase_sin_q4 formula-decl nil sincos_phase nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (nnreal type-eq-decl nil real_types nil) (phases_sin formula-decl nil sincos_phase nil) (= const-decl "[T, T -> boolean]" equalities nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (pi_bnds formula-decl nil atan nil) (real_minus_real_is_real application-judgement "real" reals nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (sin const-decl "real" sincos_def nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sin_range application-judgement "trig_range" sincos_def nil) (NOT const-decl "[bool -> bool]" booleans nil)) nil) (sin_ub-3 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" (lemma "both_sides_times_pos_lt1" ("x" "1" "y" "floor(px / (2 * pi))" "pz" "2*pi")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1 -2 -3) (("2" (simplify 1) (("2" (lemma "pi_bnds") (("2" (flatten) (("2" (lemma "phases_sin" ("x" "px")) (("2" (split -1) (("1" (rewrite "sin_q1") (("1" (hide -1) (("1" (lemma "sin_value_derivable2") (("1" (lemma "deriv_sin_value") (("1" (lemma "identity_derivable_fun[real_abs_lt_pi2]") (("1" (lemma "deriv_id_fun[real_abs_lt_pi2]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "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" (lemma "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 -5 -1) (("1" (expand "-") (("1" (assert) (("1" (lemma "identity_derivable_fun[{x:nnreal|x<pi/2}]") (("1" (lemma "deriv_id_fun[{x:nnreal|x<pi/2}]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "composition_derivable_fun[{x: nnreal | x < pi / 2},real_abs_lt_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 -3) (("1" (replace -5) (("1" (expand "o") (("1" (lemma "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 -3 -1) (("1" (replace -5 -1) (("1" (expand "*" -1) (("1" (lemma "minimum_derivative[{x: nnreal | x < pi / 2}]" ("g" "LAMBDA (x_1: {x: nnreal | x < pi / 2}): x_1 - sin_value(x_1)" "x" "0" "y1" "px")) (("1" (split -1) (("1" (simplify -1) (("1" (rewrite "sin_value_0") (("1" (assert) nil nil)) nil)) nil) ("2" (replace -1 1) (("2" (assert) (("2" (expand "abs") (("2" (rewrite "cos_value_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil) ("4" (replace -1 1) (("4" (hide-all-but 1) (("4" (skosimp*) (("4" (expand "abs") (("4" (lemma "cos_value_strict_decreasing") (("4" (expand "strict_decreasing?") (("4" (inst - "0" "y!1") (("4" (rewrite "cos_value_0") (("4" (assert) (("4" (lemma "posreal_times_posreal_is_posreal" ("px" "1-cos_value(y!1)" "py" "y!1")) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=0") (("1" (inst + "pi/4") (("1" (assert) nil nil)) nil) ("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (typepred "x!1") (("3" (typepred "y!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=0") (("1" (inst + "pi/4") (("1" (assert) nil nil)) nil) ("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (typepred "x!1") (("3" (typepred "y!1") (("3" (name-replace "K1" "pi/2") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "phase_sin_q2") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil) ("3" (rewrite "phase_sin_q3") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil) ("4" (rewrite "phase_sin_q4") (("4" (flatten) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "sin(px)") (("2" (assert) nil nil)) nil)) nil)) nil) ((pi const-decl "posreal" atan nil) (deriv_sin_value formula-decl nil sincos_quad nil) (Integral const-decl "real" integral_def "analysis/") (atan_value const-decl "real" atan nil) (deriv_id_fun formula-decl nil derivatives "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (deriv_diff_fun formula-decl nil derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (minimum_derivative formula-decl nil derivative_props "analysis/") (cos_value_strict_decreasing formula-decl nil sincos_quad nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad nil) (strict_decreasing? const-decl "bool" real_fun_preds "reals/") (cos_value_0 formula-decl nil sincos_quad nil) (sin_value_0 formula-decl nil sincos_quad nil) (deriv_comp_fun formula-decl nil chain_rule "analysis/") (composition_derivable_fun formula-decl nil chain_rule "analysis/") (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]" sincos_quad nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (diff_derivable_fun formula-decl nil derivatives "analysis/") (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil) (identity_derivable_fun formula-decl nil derivatives "analysis/") (sin_q1 formula-decl nil sincos_phase nil) (phase_sin_q2 formula-decl nil sincos_phase nil) (phase_sin_q3 formula-decl nil sincos_phase nil) (phase_sin_q4 formula-decl nil sincos_phase nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (phases_sin formula-decl nil sincos_phase nil) (pi_bnds formula-decl nil atan nil) (sin const-decl "real" sincos_def nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (sin_range application-judgement "trig_range" sincos_def nil)) nil) (sin_ub-2 nil 3307184568 ("" (skolem 1 ("px")) (("" (case "px<=1") (("1" (expand "sin") (("1" (lemma "floor_def" ("x" "px/(2*pi)")) (("1" (rewrite "div_mult_pos_lt1") (("1" (rewrite "div_mult_pos_le2") (("1" (flatten) (("1" (lemma "trichotomy" ("x" "floor(px / (2 * pi))")) (("1" (split -1) (("1" (case "floor(px / (2 * pi)) =1") (("1" (lemma "pi_bnds") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (case "floor(px / (2 * pi))>1") (("1" (lemma "pi_bnds") (("1" (flatten) (("1" (assert) (("1" (lemma "both_sides_times_pos_lt1" ("x" "1" "y" "floor(px / (2 * pi))" "pz" "2*pi")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1 -2 -3) (("2" (simplify 1) (("2" (lemma "pi_bnds") (("2" (flatten) (("2" (lemma "phases_sin" ("x" "px")) (("2" (split -1) (("1" (rewrite "sin_q1") (("1" (hide -1) (("1" (lemma "sin_value_derivable2") (("1" (lemma "deriv_sin_value") (("1" (lemma "identity_derivable_fun[real_abs_lt_pi]") (("1" (lemma "deriv_id_fun[real_abs_lt_pi]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "diff_derivable_fun[real_abs_lt_pi]" ("f1" "LAMBDA (x: real_abs_lt_pi): x" "f2" "LAMBDA (x: real_abs_lt_pi): sin_value(x)")) (("1" (lemma "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 -5 -1) (("1" (expand "-") (("1" (assert) (("1" (lemma "identity_derivable_fun[{x:nnreal|x<pi/2}]") (("1" (lemma "deriv_id_fun[{x:nnreal|x<pi/2}]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "composition_derivable_fun[{x: nnreal | x < pi / 2},real_abs_lt_pi]" ("f" "LAMBDA (x: {x: nnreal | x < pi / 2}): x" "g" "LAMBDA (x_1: real_abs_lt_pi): x_1 - sin_value(x_1)")) (("1" (replace -3) (("1" (replace -5) (("1" (expand "o") (("1" (lemma "deriv_comp_fun[{x: nnreal | x < pi / 2},real_abs_lt_pi]" ("ff" "LAMBDA (x: {x: nnreal | x < pi / 2}): x" "gg" "LAMBDA (x_1: real_abs_lt_pi): x_1 - sin_value(x_1)")) (("1" (expand "o") (("1" (replace -3 -1) (("1" (replace -5 -1) (("1" (expand "*" -1) (("1" (lemma "minimum_derivative[{x: nnreal | x < pi / 2}]" ("g" "LAMBDA (x_1: {x: nnreal | x < pi / 2}): x_1 - sin_value(x_1)" "x" "0" "y1" "px")) (("1" (split -1) (("1" (simplify -1) (("1" (rewrite "sin_value_0") (("1" (assert) nil nil)) nil)) nil) ("2" (replace -1 1) (("2" (assert) (("2" (expand "abs") (("2" (rewrite "cos_value_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil) ("4" (replace -1 1) (("4" (hide-all-but 1) (("4" (skosimp*) (("4" (expand "abs") (("4" (lemma "cos_value_strict_decreasing") (("4" (expand "strict_decreasing?") (("4" (inst - "0" "y!1") (("4" (rewrite "cos_value_0") (("4" (assert) (("4" (lemma "posreal_times_posreal_is_posreal" ("px" "1-cos_value(y!1)" "py" "y!1")) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=0") (("1" (inst + "pi/4") (("1" (assert) nil nil)) nil) ("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (typepred "x!1") (("3" (typepred "y!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (typepred "x!1") (("2" (expand "abs") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=0") (("1" (inst + "pi/4") (("1" (assert) nil nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil) ("2" (inst + "0") (("1" (assert) nil nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (typepred "x!1") (("3" (typepred "y!1") (("3" (name-replace "K1" "pi/2") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "phase_sin_q2") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil) ("3" (rewrite "phase_sin_q3") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil) ("4" (rewrite "phase_sin_q4") (("4" (flatten) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "sin(px)") (("2" (assert) nil nil)) nil)) nil)) nil) ((pi const-decl "posreal" atan nil) (deriv_sin_value formula-decl nil sincos_quad nil) (Integral const-decl "real" integral_def "analysis/") (atan_value const-decl "real" atan nil) (atan const-decl "real_abs_lt_pi2" atan nil) (deriv_id_fun formula-decl nil derivatives "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (deriv_diff_fun formula-decl nil derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (minimum_derivative formula-decl nil derivative_props "analysis/") (cos_value_strict_decreasing formula-decl nil sincos_quad nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad nil) (strict_decreasing? const-decl "bool" real_fun_preds "reals/") (cos_value_0 formula-decl nil sincos_quad nil) (sin_value_0 formula-decl nil sincos_quad nil) (deriv_comp_fun formula-decl nil chain_rule "analysis/") (composition_derivable_fun formula-decl nil chain_rule "analysis/") (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]" sincos_quad nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (diff_derivable_fun formula-decl nil derivatives "analysis/") (identity_derivable_fun formula-decl nil derivatives "analysis/") (sin_q1 formula-decl nil sincos_phase nil) (phase_sin_q2 formula-decl nil sincos_phase nil) (phase_sin_q3 formula-decl nil sincos_phase nil) (phase_sin_q4 formula-decl nil sincos_phase nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (phases_sin formula-decl nil sincos_phase nil) (pi_bnds formula-decl nil atan nil) (sin const-decl "real" sincos_def nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (sin_range application-judgement "trig_range" sincos_def nil)) nil) (sin_ub-1 nil 3265693281 ("" (skolem 1 ("px")) (("" (case "px<=1") (("1" (expand "sin") (("1" (lemma "floor_def" ("x" "px/(2*pi)")) (("1" (rewrite "div_mult_pos_lt1") (("1" (rewrite "div_mult_pos_le2") (("1" (flatten) (("1" (lemma "trichotomy" ("x" "floor(px / (2 * pi))")) (("1" (split -1) (("1" (case "floor(px / (2 * pi)) =1") (("1" (lemma "pi_bnds") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (case "floor(px / (2 * pi))>1") (("1" (lemma "pi_bnds") (("1" (flatten) (("1" (assert) (("1" (lemma "both_sides_times_pos_lt1" ("x" "1" "y" "floor(px / (2 * pi))" "pz" "2*pi")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1 -2 -3) (("2" (simplify 1) (("2" (lemma "pi_bnds") (("2" (flatten) (("2" (lemma "phases_sin" ("x" "px")) (("1" (split -1) (("1" (rewrite "sin_q1") (("1" (hide -1) (("1" (lemma "sin_value_derivable2") (("1" (lemma "deriv_sin_value") (("1" (lemma "identity_derivable_fun[real_abs_lt_pi]") (("1" (lemma "deriv_id_fun[real_abs_lt_pi]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "diff_derivable_fun" ("f1" "LAMBDA (x: real_abs_lt_pi): x" "f2" "LAMBDA (x: real_abs_lt_pi): sin_value(x)")) (("1" (lemma "deriv_diff_fun" ("ff1" "LAMBDA (x: real_abs_lt_pi): x" "ff2" "LAMBDA (x: real_abs_lt_pi): sin_value(x)")) (("1" (replace -3 -1) (("1" (replace -5 -1) (("1" (expand "-") (("1" (assert) (("1" (lemma "identity_derivable_fun[{x:nnreal|x<pi/2}]") (("1" (lemma "deriv_id_fun[{x:nnreal|x<pi/2}]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "composition_derivable_fun[{x: nnreal | x < pi / 2},real_abs_lt_pi]" ("f" "LAMBDA (x: {x: nnreal | x < pi / 2}): x" "g" "LAMBDA (x_1: real_abs_lt_pi): x_1 - sin_value(x_1)")) (("1" (replace -3) (("1" (replace -5) (("1" (expand "o") (("1" (lemma "deriv_comp_fun[{x: nnreal | x < pi / 2},real_abs_lt_pi]" ("ff" "LAMBDA (x: {x: nnreal | x < pi / 2}): x" "gg" "LAMBDA (x_1: real_abs_lt_pi): x_1 - sin_value(x_1)")) (("1" (expand "o") (("1" (replace -3 -1) (("1" (replace -5 -1) (("1" (expand "*" -1) (("1" (lemma "minimum_derivative[{x: nnreal | x < pi / 2}]" ("g" "LAMBDA (x_1: {x: nnreal | x < pi / 2}): x_1 - sin_value(x_1)" "x" "0" "y" "px")) (("1" (split -1) (("1" (simplify -1) (("1" (rewrite "sin_value_0") (("1" (assert) nil nil)) nil)) nil) ("2" (replace -1 1) (("2" (assert) (("2" (expand "abs") (("2" (rewrite "cos_value_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil) ("4" (replace -1 1) (("4" (hide-all-but 1) (("4" (skosimp*) (("4" (expand "abs") (("4" (lemma "cos_value_strict_decreasing") (("4" (expand "strict_decreasing?") (("4" (inst - "0" "y!1") (("4" (rewrite "cos_value_0") (("4" (assert) (("4" (lemma "posreal_times_posreal_is_posreal" ("px" "1-cos_value(y!1)" "py" "y!1")) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (expand "abs" 1) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "abs" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=0") (("1" (inst + "pi/4") (("1" (assert) nil nil)) nil) ("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (typepred "x!1") (("3" (typepred "y!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=0") (("1" (inst + "pi/4") (("1" (assert) nil nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil) ("2" (inst + "0") (("1" (assert) nil nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (typepred "x!1") (("3" (typepred "y!1") (("3" (name-replace "K1" "pi/2") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "phase_sin_q2") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil) ("3" (rewrite "phase_sin_q3") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil) ("4" (rewrite "phase_sin_q4") (("4" (flatten) (("4" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "sin(px)") (("2" (assert) nil nil)) nil)) nil)) nil) ((pi const-decl "posreal" atan nil) (deriv_sin_value formula-decl nil sincos_quad nil) (deriv_id_fun formula-decl nil derivatives "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (deriv_diff_fun formula-decl nil derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (cos_value_strict_decreasing formula-decl nil sincos_quad nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad nil) (strict_decreasing? const-decl "bool" real_fun_preds "reals/") (cos_value_0 formula-decl nil sincos_quad nil) (sin_value_0 formula-decl nil sincos_quad nil) (deriv_comp_fun formula-decl nil chain_rule "analysis/") (composition_derivable_fun formula-decl nil chain_rule "analysis/") (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]" sincos_quad nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (diff_derivable_fun formula-decl nil derivatives "analysis/") (identity_derivable_fun formula-decl nil derivatives "analysis/") (sin_q1 formula-decl nil sincos_phase nil) (phase_sin_q2 formula-decl nil sincos_phase nil) (phase_sin_q3 formula-decl nil sincos_phase nil) (phase_sin_q4 formula-decl nil sincos_phase nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (phases_sin formula-decl nil sincos_phase nil) (pi_bnds formula-decl nil atan nil)) shostak)) (cos_lb 0 (cos_lb-8 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 (("1" (case "1 - (pi/4) * (pi/4) / 2 < cos(pi/4)") (("1" (lemma "trich_lt" ("x" "px" "y" "pi/4")) (("1" (split -1) (("1" (hide -5) (("1" (hide -2) (("1" (lemma "identity_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]") (("1" (lemma "deriv_id_fun[{x: real | -pi / 4 < x & x < pi / 4}]") (("1" (expand "I") (("1" (lemma "const_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("b" "1")) (("1" (lemma "deriv_const_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("b" "1")) (("1" (lemma "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" (lemma "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" (lemma "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" (lemma "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 -3) (("1" (expand "*") (("1" (lemma "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 / 2 * (x * x)")) (("1" (assert) (("1" (expand "-") (("1" (lemma "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 / 2 * (x * x)")) (("1" (expand "-") (("1" (replace -3) (("1" (replace -7) (("1" (simplify -1) (("1" (lemma "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 - 1 / 2 * (x_1 * x_1)")) (("1" (assert) (("1" (expand "-") (("1" (lemma "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 - 1 / 2 * (x_1 * x_1)")) (("1" (replace -3) (("1" (replace -14) (("1" (expand "-") (("1" (hide-all-but (-1 -2 -13 1)) (("1" (lemma "identity_derivable_fun[{x:nnreal|x<pi/4}]") (("1" (lemma "deriv_id_fun[{x:nnreal|x<pi/4}]") (("1" (expand "I") (("1" (lemma "composition_derivable_fun[{x: nnreal | x < pi / 4},{x: real | -pi / 4 < x & x < pi / 4}]" ("f" "LAMBDA (x: {x: nnreal | x < pi / 4}): x" "g" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): cos(x_1) - 1 + 1 / 2 * (x_1 * x_1)")) (("1" (assert) (("1" (expand "o") (("1" (lemma "deriv_comp_fun[{x: nnreal | x < pi / 4},{x: real | -pi / 4 < x & x < pi / 4}]" ("ff" "LAMBDA (x: {x: nnreal | x < pi / 4}): x" "gg" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): cos(x_1) - 1 + 1 / 2 * (x_1 * x_1)")) (("1" (replace -5) (("1" (replace -3) (("1" (expand "o") (("1" (expand "*") (("1" (lemma "minimum_derivative[{x: nnreal | x < pi / 4}]" ("g" "LAMBDA (x_1: {x: nnreal | x < pi / 4}): cos(x_1) - 1 + 1 / 2 * (x_1 * x_1)" "x" "0" "y1" "px")) (("1" (split -1) (("1" (simplify -1) (("1" (rewrite "cos_0") (("1" (assert) nil nil)) nil)) nil) ("2" (replace -1 1) (("2" (simplify 1) (("2" (rewrite "sin_0") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (assert) nil nil) ("4" (hide 2) (("4" (skosimp*) (("4" (replace -1) (("4" (simplify 2) (("4" (hide-all-but (1 2)) (("4" (lemma "sin_ub" ("px" "y!1")) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "y!1" "py" "y!1-sin(y!1)")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (propax) nil nil)) nil) ("3" (hide -3 -4) (("3" (expand "cos") (("3" (lemma "floor_0" ("x" "px / (2 * pi)")) (("3" (flatten -1) (("3" (hide -1) (("3" (split -1) (("1" (replace -1) (("1" (lemma "floor_0" ("x" "pi / 4 / (2 * pi)")) (("1" (flatten -1) (("1" (hide -1) (("1" (split -1) (("1" (replace -1) (("1" (simplify (-4 1)) (("1" (hide -1 -2) (("1" (rewrite "cos_phase_pi4") (("1" (expand "cos_phase") (("1" (rewrite "phase_cos_q1" 1) (("1" (assert) (("1" (lemma "identity_derivable_fun[{x:nnreal|pi/4<=x&x<pi}]") (("1" (lemma "deriv_id_fun[{x:nnreal|pi/4<=x&x<pi}]") (("1" (lemma "const_derivable_fun[{x:nnreal|pi/4<=x&x<pi}]" ("b" "1")) (("1" (lemma "deriv_const_fun[{x:nnreal|pi/4<=x&x<pi}]" ("b" "1")) (("1" (expand "I") (("1" (lemma "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" (lemma "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 -5) (("1" (expand "*") (("1" (expand "+") (("1" (lemma "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" (lemma "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 -3) (("1" (expand "*") (("1" (lemma "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" (lemma "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 -7) (("1" (replace -3) (("1" (expand "-") (("1" (lemma "cos_value_derivable_fun") (("1" (lemma "deriv_cos_value") (("1" (lemma "composition_derivable_fun[{x: nnreal | pi / 4 <= x & x < pi},posreal_lt_pi]" ("f" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): x" "g" "LAMBDA (x: posreal_lt_pi): cos_value(x)")) (("1" (assert) (("1" (expand "o") (("1" (lemma "deriv_comp_fun[{x: nnreal | pi / 4 <= x & x < pi},posreal_lt_pi]" ("ff" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): x" "gg" "LAMBDA (x: posreal_lt_pi): cos_value(x)")) (("1" (expand "o") (("1" (replace -3 -1) (("1" (replace -13) (("1" (expand "*") (("1" (hide -7 -8 -9 -10 -11 -12 -13 -14) (("1" (lemma "diff_derivable_fun[{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" (lemma "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 -3) (("1" (replace -7) (("1" (expand "-") (("1" (lemma "positive_derivative[{x: nnreal | pi / 4 <= x & x < pi}]" ("g" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): cos_value(x) - 1 + 1 / 2 * (x * x)")) (("1" (split -1) (("1" (expand "strict_increasing?") (("1" (hide-all-but (-1 -10 -11 -12 1)) (("1" (inst - "pi/4" "px") (("1" (rewrite "cos_value_pi4") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide 2) (("2" (expand "deriv" -1) (("2" (decompose-equality -1) (("1" (inst -1 "x!1") (("1" (replaces -1 1) (("1" (hide-all-but (-8 -9 -10 1)) (("1" (case "x!1 < pi / 2") (("1" (hide -2 -3 -4) (("1" (assert) (("1" (lemma "sin_ub" ("px" "x!1")) (("1" (expand "sin") (("1" (lemma "floor_0" ("x" "x!1/(2*pi)")) (("1" (assert) (("1" (rewrite "div_mult_pos_lt1" -1) (("1" (flatten -1) (("1" (replace -1) (("1" (simplify -2) (("1" (rewrite "sin_q1" -2) (("1" (assert) nil nil) ("2" (rewrite "phase_sin_q1" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "pi/2<=x!1") (("1" (hide -2 -3 -4 1) (("1" (lemma "sin_ub" ("px" "x!1")) (("1" (expand "sin") (("1" (lemma "floor_0" ("x" "x!1 / (2 * pi)")) (("1" (assert) (("1" (rewrite "div_mult_pos_lt1" -1) (("1" (flatten -1) (("1" (replace -1) (("1" (simplify -2) (("1" (hide -1) (("1" (case "sin_value(pi - x!1) = sin_phase(x!1)") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (hide -1 2) (("2" (rewrite "sin_q2" 1) (("1" (rewrite "sin_eqv_cos_value") (("1" (lemma "cos_value_neg" ("xc" "x!1-pi/2")) (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "phase_sin_q2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "derivable?" -6) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "div_div2") (("2" (lemma "div_cancel1" ("x" "1/8" "n0z" "pi")) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (lemma "div_cancel1" ("x" "1/8" "n0z" "pi")) (("3" (rewrite "div_div2" 1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) (("3" (rewrite "div_mult_pos_lt1" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "cos") (("2" (lemma "floor_0" ("x" "pi / 4 / (2 * pi)")) (("2" (rewrite "div_div2") (("2" (lemma "div_cancel1" ("x" "1/8" "n0z" "pi")) (("2" (replace -1) (("2" (hide -1) (("2" (flatten -1) (("2" (hide -1) (("2" (split -1) (("1" (replace -1) (("1" (simplify 1) (("1" (hide -1) (("1" (rewrite "cos_phase_pi4") (("1" (case "314/100<=pi&pi<=315/100") (("1" (flatten) (("1" (lemma "le_times_le_pos" ("nnx" "pi/4" "y" "315/400" "nnz" "pi/4" "w" "315/400")) (("1" (assert) (("1" (lemma "le_times_le_pos" ("y" "pi/4" "nnx" "314/400" "w" "pi/4" "nnz" "314/400")) (("1" (assert) (("1" (case "1 - (pi / 4) * (pi / 4) / 2<=221404/320000") (("1" (lemma "sq_lt" ("nna" "221404 / 320000" "nnb" "sqrt(1/2)")) (("1" (flatten -1) (("1" (hide -2) (("1" (rewrite "sq_sqrt") (("1" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "pi") (("2" (expand "pi_lb") (("2" (expand "pi_ub") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (lemma "extensionality" ("f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos(x)" "g" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): sqrt(1/2)*(cos(x+pi/4)+sin(x+pi/4))")) (("2" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "identity_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]") (("1" (lemma "deriv_id_fun[{x: real | -pi / 4 < x & x < pi / 4}]") (("1" (expand "I") (("1" (lemma "const_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("b" "pi/4")) (("1" (lemma "deriv_const_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("b" "pi/4")) (("1" (lemma "sin_value_derivable_fun") (("1" (lemma "cos_value_derivable_fun") (("1" (lemma "deriv_sin_value") (("1" (lemma "deriv_cos_value") (("1" (lemma "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" (lemma "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" (lemma "composition_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4},posreal_lt_pi]" ("f" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1+pi/4" "g" "LAMBDA (x: posreal_lt_pi): cos_value(x)")) (("1" (assert) (("1" (expand "o") (("1" (lemma "composition_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4},real_abs_lt_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" (lemma "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" (lemma "deriv_comp_fun[{x: real | -pi / 4 < x & x < pi / 4},posreal_lt_pi]" ("ff" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1+pi/4" "gg" "LAMBDA (x: posreal_lt_pi): cos_value(x)")) (("1" (replace -5) (("1" (replace -7) (("1" (replace -8) (("1" (expand "o") (("1" (expand "*") (("1" (lemma "sum_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("f1" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x_1 + pi / 4)" "f2" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): sin_value(x_1 + pi / 4)")) (("1" (expand "+") (("1" (hide (-8 -9 -10 -11 -12 -13 -14 -15)) (("1" (assert) (("1" (lemma "deriv_sum_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("ff1" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x_1 + pi / 4)" "ff2" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): sin_value(x_1 + pi / 4)")) (("1" (replace -3) (("1" (replace -4) (("1" (expand "abs" (-1 -4)) (("1" (expand "+") (("1" (lemma "scal_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x + pi / 4) + sin_value(x + pi / 4)" "b" "sqrt(1/2)")) (("1" (assert) (("1" (expand "*") (("1" (lemma "deriv_scal_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("ff" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x + pi / 4) + sin_value(x + pi / 4)" "b" "sqrt(1/2)")) (("1" (replace -3) (("1" (expand "*") (("1" (hide-all-but (-1 -2 -11 1)) (("1" (lemma "extensionality" ("f" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x_1 + pi / 4) * sqrt(1 / 2) + sin_value(x_1 + pi / 4) * sqrt(1 / 2)" "g" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos(x + pi / 4) * sqrt(1 / 2) + sin(x + pi / 4) * sqrt(1 / 2)")) (("1" (split -1) (("1" (replace -1) (("1" (lemma "extensionality" ("f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x + pi / 4) * sqrt(1 / 2) + sqrt(1 / 2) * -sin_value(x + pi / 4)" "g" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): -sin(x)")) (("1" (split -1) (("1" (replace -1 :dir rl) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (lemma "sin_minus" ("a" "x!1+pi/4" "b" "pi/4")) (("2" (replace -1 1) (("2" (hide -1) (("2" (expand "sin") (("2" (expand "cos") (("2" (rewrite "div_div2") (("2" (lemma "div_cancel1" ("x" "1/8" "n0z" "pi")) (("2" (replace -1) (("2" (lemma "floor_0" ("x" "1/8")) (("2" (flatten -1) (("2" (hide -1 -3) (("2" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (simplify) (("1" (rewrite "cos_phase_pi4") (("1" (rewrite "sin_phase_pi4") (("1" (typepred "x!1") (("1" (lemma "floor_0" ("x" "(pi / 4 + x!1) / (2 * pi)")) (("1" (rewrite "div_mult_pos_lt1" -1) (("1" (rewrite "div_mult_pos_le2" -1) (("1" (flatten -1) (("1" (replace -1) (("1" (simplify 1) (("1" (rewrite "sin_q1") (("1" (rewrite "cos_q1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (assert) (("2" (lemma "phase_sin_q1" ("x" "(pi / 4) + x!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -3 1)) (("2" (lemma "phase_sin_q1" ("x" "(pi / 4) + x!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (expand "cos") (("2" (expand "sin") (("2" (lemma "floor_0" ("x" "(pi / 4 + x!1) / (2 * pi)")) (("2" (flatten -1) (("2" (split -2) (("1" (replace -1) (("1" (hide -1 -2) (("1" (simplify) (("1" (rewrite "sin_q1") (("1" (rewrite "cos_q1") (("1" (hide 2) (("1" (typepred "x!1") (("1" (lemma "phase_sin_q1" ("x" "pi/4+x!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "phase_sin_q1" ("x" "pi/4+x!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (assert) (("2" (rewrite "div_mult_pos_le2") nil nil)) nil)) nil) ("3" (rewrite "div_mult_pos_lt1" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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" (lemma "cos_minus" ("a" "x!1 + pi / 4" "b" "pi/4")) (("2" (replace -1 1) (("2" (hide -1) (("2" (expand "cos") (("2" (expand "sin") (("2" (rewrite "div_div2") (("2" (lemma "div_cancel1" ("x" "1/8" "n0z" "pi")) (("2" (replace -1) (("2" (lemma "floor_0" ("x" "1/8")) (("2" (flatten -1) (("2" (hide -1 -3) (("2" (split -1) (("1" (replace -1) (("1" (simplify 1) (("1" (rewrite "sin_phase_pi4") (("1" (rewrite "cos_phase_pi4") nil nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil) ("2" (lemma "extensionality" ("f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos(x)" "g" "LAMBDA (x:{x: real | -pi / 4 < x & x < pi / 4}):sqrt(1/2)*(cos_value(x+pi/4)+sin_value(x+pi (("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" (lemma "identity_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]") (("1" (lemma "deriv_id_fun[{x: real | -pi / 4 < x & x < pi / 4}]") (("1" (expand "I") (("1" (lemma "const_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("b" "pi/4")) (("1" (lemma "deriv_const_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("b" "pi/4")) (("1" (lemma "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" (lemma "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" (lemma "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" (lemma "composition_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4},posreal_lt_pi]" ("f" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): x_1 + pi / 4" "g" "LAMBDA (x: posreal_lt_pi): cos_value(x)")) (("1" (assert) (("1" (expand "o") (("1" (lemma "sum_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("f1" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x_1 + pi / 4)" "f2" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): sin_value(x_1 + pi / 4)")) (("1" (assert) (("1" (expand "+") (("1" (lemma "scal_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("b" "sqrt(1/2)" "f" "LAMBDA (x: {x: real | -pi / 4 < x & x < pi / 4}): cos_value(x + pi / 4) + sin_value(x + pi / 4)")) (("1" (assert) (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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" (lemma "cos_minus" ("a" "x!1+pi/4" "b" "pi/4")) (("2" (replace -1 1) (("2" (hide -1) (("2" (typepred "x!1") (("2" (expand "cos") (("2" (expand "sin") (("2" (rewrite "div_div2" 1) (("2" (lemma "div_cancel1" ("x" "1/8" "n0z" "pi")) (("2" (replace -1) (("2" (lemma "floor_0" ("x" "1/8")) (("2" (flatten -1) (("2" (hide -1) (("2" (simplify -1) (("2" (replace -1) (("2" (simplify 1) (("2" (lemma "floor_0" ("x" "(pi / 4 + x!1) / (2 * pi)")) (("2" (flatten -1) (("2" (hide -1 -3 -4) (("2" (split -1) (("1" (replace -1) (("1" (simplify 1) (("1" (hide -1) (("1" (rewrite "cos_phase_pi4") (("1" (rewrite "sin_phase_pi4") (("1" (lemma "phase_sin_q1" ("x" "pi/4+x!1")) (("1" (assert) (("1" (rewrite "sin_q1" 1) (("1" (rewrite "cos_q1" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "div_mult_pos_le2" ("z" "pi / 4 + x!1" "py" "2*pi" "x" "0")) (("2" (assert) nil nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "div_mult_pos_lt1" ("z" "pi / 4 + x!1" "py" "2*pi" "x" "1")) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "pi<=px") (("1" (hide 1) (("1" (lemma "pi_bnds") (("1" (flatten) (("1" (typepred "cos(px)") (("1" (lemma "lt_times_lt_pos1" ("px" "306/100" "y" "px" "nnz" "306/100" "w" "px")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((pi const-decl "posreal" atan nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (minus_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (deriv_fun type-eq-decl nil derivatives "analysis/") (deriv const-decl "[T -> real]" derivatives "analysis/") (sin const-decl "real" sincos_def nil) (cos_range application-judgement "trig_range" sincos_def nil) (le_times_le_pos formula-decl nil real_props nil) (sq_sqrt formula-decl nil sqrt "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/") (sq const-decl "nonneg_real" sq "reals/") (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (sq_lt formula-decl nil sq "reals/") (pi_lb const-decl "posreal" atan_approx nil) (pi_ub const-decl "posreal" atan_approx nil) (trich_lt formula-decl nil real_props nil) (floor_0 formula-decl nil floor_ceil nil) (cos_phase_pi4 formula-decl nil sincos_phase nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (phase_cos_q1 formula-decl nil sincos_phase nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (<= const-decl "bool" reals nil) (deriv_cos_value formula-decl nil sincos_quad nil) (cos_value_pi4 formula-decl nil sincos_quad nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (noa_nnreal_pi4_to_pi formula-decl nil sincos nil) (deriv_domain_nnreal_pi4_to_pi formula-decl nil sincos nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]" sincos_quad nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (deriv const-decl "real" derivatives_def "analysis/") (derivable? const-decl "bool" derivatives_def "analysis/") (phase_sin_q1 formula-decl nil sincos_phase nil) (sin_q1 formula-decl nil sincos_phase nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (phase_sin_q2 formula-decl nil sincos_phase nil) (sin_eqv_cos_value formula-decl nil sincos_quad nil) (cos_value_neg formula-decl nil sincos_quad nil) (sin_q2 formula-decl nil sincos_phase nil) (sin_phase const-decl "real_abs_le1" sincos_phase nil) (positive_derivative formula-decl nil derivative_props "analysis/") (posreal_lt_pi nonempty-type-eq-decl nil sincos_quad nil) (cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (cos_value_derivable_fun formula-decl nil sincos_quad nil) (cos_phase const-decl "real_abs_le1" sincos_phase nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_div2 formula-decl nil real_props nil) (div_cancel1 formula-decl nil real_props nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (identity_derivable_fun formula-decl nil derivatives "analysis/") (I const-decl "(bijective?[T, T])" identity nil) (deriv_const_fun formula-decl nil derivatives "analysis/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sin_range application-judgement "trig_range" sincos_def nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (deriv_prod_fun formula-decl nil derivatives "analysis/") (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (real_times_real_is_real application-judgement "real" reals nil) (scal_derivable_fun formula-decl nil derivatives "analysis/") (* const-decl "[T -> real]" real_fun_ops "reals/") (diff_derivable_fun formula-decl nil derivatives "analysis/") (- const-decl "[T -> real]" real_fun_ops "reals/") (nnreal type-eq-decl nil real_types nil) (deriv_comp_fun formula-decl nil chain_rule "analysis/") (cos_0 formula-decl nil trig_basic nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (minus_even_is_even application-judgement "even_int" integers nil) (sin_0 formula-decl nil trig_basic nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sin_ub formula-decl nil sincos nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (connected? const-decl "bool" deriv_domain_def "analysis/") (minimum_derivative formula-decl nil derivative_props "analysis/") (O const-decl "T3" function_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (composition_derivable_fun formula-decl nil chain_rule "analysis/") (real_plus_real_is_real application-judgement "real" reals nil) (deriv_diff_fun formula-decl nil derivatives "analysis/") (deriv_scal_fun formula-decl nil derivatives "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (prod_derivable_fun formula-decl nil derivatives "analysis/") (const_derivable_fun formula-decl nil derivatives "analysis/") (deriv_id_fun formula-decl nil derivatives "analysis/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (extensionality formula-decl nil functions nil) (cos_minus formula-decl nil trig_basic nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (deriv_sum_fun formula-decl nil derivatives "analysis/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sin_minus formula-decl nil trig_basic nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (sin_phase_pi4 formula-decl nil sincos_phase nil) (div_mult_pos_le2 formula-decl nil real_props nil) (cos_q1 formula-decl nil sincos_phase nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil) (sum_derivable_fun formula-decl nil derivatives "analysis/") (deriv_sin_value formula-decl nil sincos_quad nil) (sin_value_derivable_fun formula-decl nil sincos_quad nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (derivable? const-decl "bool" derivatives "analysis/") (cos const-decl "real" sincos_def nil) (lt_times_lt_pos1 formula-decl nil real_props nil) (pi_bnds formula-decl nil atan nil)) nil) (cos_lb-7 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 (("1" (case "1 - (pi/4) * (pi/4) / 2 < cos(pi/4)") (("1" (lemma "trich_lt" ("x" "px" "y" "pi/4")) (("1" (split -1) (("1" (hide -5) (("1" (hide -2) (("1" (lemma "identity_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]") (("1" (lemma "deriv_id_fun[{x: real | -pi / 4 < x & x < pi / 4}]") (("1" (expand "I") (("1" (lemma "const_derivable_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("b" "1")) (("1" (lemma "deriv_const_fun[{x: real | -pi / 4 < x & x < pi / 4}]" ("b" "1")) (("1" (expand "const_fun") (("1" (lemma "prod_derivable_fun[{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" (lemma "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" (lemma "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" (lemma "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 -3) (("1" (expand "*") (("1" (lemma "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 / 2 * (x * x)")) (("1" (assert) (("1" (expand "-") (("1" (lemma "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 / 2 * (x * x)")) (("1" (expand "-") (("1" (replace -3) (("1" (replace -7) (("1" (simplify -1) (("1" (lemma "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 - 1 / 2 * (x_1 * x_1)")) (("1" (assert) (("1" (expand "-") (("1" (lemma "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 - 1 / 2 * (x_1 * x_1)")) (("1" (replace -3) (("1" (replace -14) (("1" (expand "-") (("1" (hide-all-but (-1 -2 -13 1)) (("1" (lemma "identity_derivable_fun[{x:nnreal|x<pi/4}]") (("1" (lemma "deriv_id_fun[{x:nnreal|x<pi/4}]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "composition_derivable_fun[{x: nnreal | x < pi / 4},{x: real | -pi / 4 < x & x < pi / 4}]" ("f" "LAMBDA (x: {x: nnreal | x < pi / 4}): x" "g" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): cos(x_1) - 1 + 1 / 2 * (x_1 * x_1)")) (("1" (assert) (("1" (expand "o") (("1" (lemma "deriv_comp_fun[{x: nnreal | x < pi / 4},{x: real | -pi / 4 < x & x < pi / 4}]" ("ff" "LAMBDA (x: {x: nnreal | x < pi / 4}): x" "gg" "LAMBDA (x_1: {x: real | -pi / 4 < x & x < pi / 4}): cos(x_1) - 1 + 1 / 2 * (x_1 * x_1)")) (("1" (replace -5) (("1" (replace -3) (("1" (expand "o") (("1" (expand "*") (("1" (lemma "minimum_derivative[{x: nnreal | x < pi / 4}]" ("g" "LAMBDA (x_1: {x: nnreal | x < pi / 4}): cos(x_1) - 1 + 1 / 2 * (x_1 * x_1)" "x" "0" "y1" "px")) (("1" (split -1) (("1" (simplify -1) (("1" (rewrite "cos_0") (("1" (assert) nil nil)) nil)) nil) ("2" (replace -1 1) (("2" (simplify 1) (("2" (rewrite "sin_0") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (assert) nil nil) ("4" (hide 2) (("4" (skosimp*) (("4" (replace -1) (("4" (simplify 2) (("4" (hide-all-but (1 2)) (("4" (lemma "sin_ub" ("px" "y!1")) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "y!1" "py" "y!1-sin(y!1)")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=0") (("1" (inst + "pi/8") (("1" (assert) nil nil)) nil) ("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (propax) nil nil)) nil) ("3" (hide -3 -4) (("3" (expand "cos") (("3" (lemma "floor_0" ("x" "px / (2 * pi)")) (("3" (flatten -1) (("3" (hide -1) (("3" (split -1) (("1" (replace -1) (("1" (lemma "floor_0" ("x" "pi / 4 / (2 * pi)")) (("1" (flatten -1) (("1" (hide -1) (("1" (split -1) (("1" (replace -1) (("1" (simplify (-4 1)) (("1" (hide -1 -2) (("1" (rewrite "cos_phase_pi4") (("1" (expand "cos_phase") (("1" (rewrite "phase_cos_q1" 1) (("1" (assert) (("1" (lemma "identity_derivable_fun[{x:nnreal|pi/4<=x&x<pi}]") (("1" (lemma "deriv_id_fun[{x:nnreal|pi/4<=x&x<pi}]") (("1" (lemma "const_derivable_fun[{x:nnreal|pi/4<=x&x<pi}]" ("b" "1")) (("1" (lemma "deriv_const_fun[{x:nnreal|pi/4<=x&x<pi}]" ("b" "1")) (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "prod_derivable_fun[{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" (lemma "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 -5) (("1" (expand "*") (("1" (expand "+") (("1" (lemma "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" (lemma "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 -3) (("1" (expand "*") (("1" (lemma "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" (lemma "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 -7) (("1" (replace -3) (("1" (expand "-") (("1" (lemma "cos_value_derivable_fun") (("1" (lemma "deriv_cos_value") (("1" (lemma "composition_derivable_fun[{x: nnreal | pi / 4 <= x & x < pi},posreal_lt_pi]" ("f" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): x" "g" "LAMBDA (x: posreal_lt_pi): cos_value(x)")) (("1" (assert) (("1" (expand "o") (("1" (lemma "deriv_comp_fun[{x: nnreal | pi / 4 <= x & x < pi},posreal_lt_pi]" ("ff" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): x" "gg" "LAMBDA (x: posreal_lt_pi): cos_value(x)")) (("1" (expand "o") (("1" (replace -3 -1) (("1" (replace -13) (("1" (expand "*") (("1" (hide -7 -8 -9 -10 -11 -12 -13 -14) (("1" (lemma "diff_derivable_fun[{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" (lemma "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 -3) (("1" (replace -7) (("1" (expand "-") (("1" (lemma "positive_derivative[{x: nnreal | pi / 4 <= x & x < pi}]" ("g" "LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): cos_value(x) - 1 + 1 / 2 * (x * x)")) (("1" (split -1) (("1" (expand "strict_increasing?") (("1" (hide-all-but (-1 -10 -11 -12 1)) (("1" (inst - "pi/4" "px") (("1" (rewrite "cos_value_pi4") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide 2) (("2" (expand "deriv" -1) (("2" (lemma "extensionality_postulate" ("f" "(LAMBDA (x_1: {x: nnreal | pi / 4 <= x & x < pi}): deriv(LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): cos_value(x) - 1 + 1 / 2 * (x * x), x_1))" "g" "(LAMBDA (x: {x: nnreal | pi / 4 <= x & x < pi}): IF x < pi / 2 THEN -sin_value(x) ELSE -sin_value(pi - x) ENDIF + 2 * (x * (1 / 2)))")) (("1" (replace -1 -2 rl) (("1" (inst -2 "x!1") (("1" (replace -2 1) (("1" (hide-all-but (-10 -11 -12 1)) (("1" (case "x!1 < pi / 2") (("1" (hide -2 -3 -4) (("1" (assert) (("1" (lemma "sin_ub" ("px" "x!1")) (("1" (expand "sin") (("1" (lemma "floor_0" ("x" "x!1/(2*pi)")) (("1" (assert) (("1" (rewrite "div_mult_pos_lt1" -1) (("1" (flatten -1) (("1" (replace -1) (("1" (simplify -2) (("1" (rewrite "sin_q1" -2) (("1" (assert) nil nil) ("2" (rewrite "phase_sin_q1" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "pi/2<=x!1") (("1" (hide -2 -3 -4 1) (("1" (lemma "sin_ub" ("px" "x!1")) (("1" (expand "sin") (("1" (lemma "floor_0" ("x" "x!1 / (2 * pi)")) (("1" (assert) (("1" (rewrite "div_mult_pos_lt1" -1) (("1" (flatten -1) (("1" (replace -1) (("1" (simplify -2) (("1" (hide -1) (("1" (case "sin_value(pi - x!1) = sin_phase(x!1)") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (hide -1 2) (("2" (rewrite "sin_q2" 1) (("1" (rewrite "sin_eqv_cos_value") (("1" (lemma "cos_value_neg" ("xc" "x!1-pi/2")) (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "phase_sin_q2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (skosimp*) (("4" (typepred "x!3") (("4" (case "x!3=pi/4") (("1" (inst + "pi/2") (("1" (assert) nil nil)) nil) ("2" (inst + "pi/4") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide-all-but 1) (("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp*) (("6" (expand "derivable" -2) (("6" (inst -2 "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=pi/2") (("1" (inst + "pi/3") (("1" (assert) nil nil)) nil) ("2" (inst + "pi/2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "x!1=pi/4") (("1" (inst + "pi/2") (("1" (assert) nil nil)) nil) ("2" (inst + "pi/4") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) nil nil)) --> -------------------- --> maximum size reached --> --------------------
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.597Bemerkung: (vorverarbeitet am 2026-04-29) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26