| products/sources/formale sprachen/PVS/trig_fnd/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: sincos_quad.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(sincos_quad
(nnreal_quad1_closed_TCC1 0 (nnreal_quad1_closed_TCC1-1 nil 3263653658 ("" (assert) nil nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (nnreal_quad1_open_TCC1 0 (nnreal_quad1_open_TCC1-1 nil 3269611563 ("" (assert) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (posreal_lt_pi_TCC1 0 (posreal_lt_pi_TCC1-1 nil 3265387997 ("" (assert) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (noa_real_lt_pi2 0 (noa_real_lt_pi2-1 nil 3477834241 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst-cp + "pi/4") (("" (inst + "pi/8") (("" (flatten) (("" (assert) nil 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)) shostak)) (noa_real_abs_lt1 0 (noa_real_abs_lt1-1 nil 3477834289 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst-cp + "0") (("" (inst + "1/2") (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (real_abs_lt1 nonempty-type-eq-decl nil asin nil) (- const-decl "[numfield -> numfield]" number_fields 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) (not_one_element? const-decl "bool" deriv_domain_def "analysis/")) shostak)) (noa_posreal_lt_pi 0 (noa_posreal_lt_pi-1 nil 3477834336 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst-cp + "pi/2") (("" (inst + "pi/4") (("" (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) (not_one_element? const-decl "bool" deriv_domain_def "analysis/")) nil)) (noa_real_abs_lt_pi2 0 (noa_real_abs_lt_pi2-1 nil 3477834383 ("" (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)) nil)) (noa_posreal_lt_pi4 0 (noa_posreal_lt_pi4-1 nil 3477834403 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst-cp + "pi/8") (("" (inst + "pi/6") (("" (assert) nil nil)) nil)) nil)) nil)) 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) (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) (not_one_element? const-decl "bool" deriv_domain_def "analysis/")) nil)) (conn_real_lt_pi2 0 (conn_real_lt_pi2-1 nil 3477834411 ("" (expand "connected?") (("" (skosimp*) (("" (assert) nil nil)) nil)) 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) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (connected? const-decl "bool" deriv_domain_def "analysis/") (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) shostak)) (conn_real_abs_lt1 0 (conn_real_abs_lt1-1 nil 3477834437 ("" (expand "connected?") (("" (skosimp*) (("" (assert) nil nil)) nil)) 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (connected? const-decl "bool" deriv_domain_def "analysis/")) shostak)) (conn_posreal_lt_pi 0 (conn_posreal_lt_pi-1 nil 3477834446 ("" (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/")) shostak)) (deriv_domain_real_abs_lt1 0 (deriv_domain_real_abs_lt1-1 nil 3472550428 ("" (lemma "deriv_domain_open") (("" (inst - "-1" "1") nil nil)) nil) ((minus_odd_is_odd application-judgement "odd_int" integers 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 "[numfield -> numfield]" number_fields nil) (deriv_domain_open formula-decl nil deriv_domain "analysis/")) shostak)) (deriv_domain_posreal_lt_pi 0 (deriv_domain_posreal_lt_pi-1 nil 3477834481 ("" (lemma "deriv_domain_open") (("" (inst - "0" "pi") (("" (expand "deriv_domain?") (("" (skosimp*) (("" (inst - "e!1" "x!1") (("" (skosimp*) (("" (inst + "y!1") 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) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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) (posreal_lt_pi nonempty-type-eq-decl nil sincos_quad nil) (open_interval type-eq-decl nil intervals_real "reals/") (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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_open formula-decl nil deriv_domain "analysis/")) shostak)) (deriv_domain_abs_lt_pi2 0 (deriv_domain_abs_lt_pi2-1 nil 3477834559 ("" (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) (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_lt_pi4 0 (deriv_domain_posreal_lt_pi4-1 nil 3477834580 ("" (lemma "deriv_domain_open") (("" (inst - "0" "pi/4") (("" (assert) (("" (expand "deriv_domain?") (("" (skosimp*) (("" (inst - "e!1" "x!1") (("" (skosimp*) (("" (inst + "y!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (open_interval type-eq-decl nil intervals_real "reals/") (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_ge_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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nzreal nonempty-type-eq-decl nil reals nil) (deriv_domain_open formula-decl nil deriv_domain "analysis/")) shostak)) (sin_value_bij 0 (sin_value_bij-1 nil 3262932114 ("" (expand "sin_value") (("" (lemma "asin_bij") (("" (lemma "bij_inv_is_bij[real_abs_le1, real_abs_le_pi2]" ("f" "asin")) (("" (assert) nil nil)) nil)) nil)) nil) ((asin_bij formula-decl nil asin nil) (bij_inv_is_bij formula-decl nil function_inverse nil) (asin const-decl "real_abs_le_pi2" asin 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_abs_le1 nonempty-type-eq-decl nil asin 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 "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_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]" sincos_quad nil)) shostak)) (cos_value_bij 0 (cos_value_bij-1 nil 3262932269 ("" (lemma "acos_bij") (("" (lemma "bij_inv_is_bij[real_abs_le1, nnreal_le_pi]" ("f" "acos")) (("" (expand "cos_value") (("" (assert) nil nil)) nil)) nil)) nil) ((nnreal_le_pi nonempty-type-eq-decl nil acos 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) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (- const-decl "[numfield -> numfield]" number_fields 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) (acos const-decl "nnreal_le_pi" acos nil) (bij_inv_is_bij formula-decl nil function_inverse nil) (cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad nil) (acos_bij formula-decl nil acos nil)) shostak)) (sin_value_strict_increasing 0 (sin_value_strict_increasing-1 nil 3264344138 ("" (lemma "asin_strict_increasing") (("" (expand "strict_increasing?") (("" (skosimp*) (("" (expand "sin_value") (("" (lemma "asin_bij") (("" (lemma "trich_lt" ("x" "inverse(asin)(x!1)" "y" "inverse(asin)(y!1)")) (("" (split -1) (("1" (propax) nil nil) ("2" (lemma "bij_inv_is_bij" ("f" "asin")) (("2" (assert) (("2" (expand "bijective?" -1) (("2" (expand "injective?" -1) (("2" (flatten -1) (("2" (inst - "x!1" "y!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (inst - "inverse(asin)(y!1)" "inverse(asin)(x!1)") (("3" (assert) (("3" (lemma "comp_inverse_right[real_abs_le1, real_abs_le_pi2]" ("f" "asin" "y" "x!1")) (("3" (lemma "comp_inverse_right[real_abs_le1, real_abs_le_pi2]" ("f" "asin" "y" "y!1")) (("3" (replace -1) (("3" (replace -2) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]" sincos_quad nil) (asin const-decl "real_abs_le_pi2" asin nil) (inverse const-decl "D" function_inverse nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin 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, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (- const-decl "[numfield -> numfield]" number_fields 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) (trich_lt formula-decl nil real_props nil) (comp_inverse_right formula-decl nil function_inverse nil) (bij_inv_is_bij formula-decl nil function_inverse nil) (bijective? const-decl "bool" functions nil) (injective? const-decl "bool" functions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (asin_bij formula-decl nil asin nil) (asin_strict_increasing formula-decl nil asin nil)) shostak)) (sin_value_increasing 0 (sin_value_increasing-1 nil 3263653554 ("" (lemma "sin_value_strict_increasing") (("" (expand "strict_increasing?") (("" (expand "increasing?") (("" (skosimp*) (("" (expand "<=" -2) (("" (split -2) (("1" (inst - "x!1" "y!1") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (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) (real_abs_le_pi2 nonempty-type-eq-decl nil asin 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) (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) (<= const-decl "bool" reals nil) (increasing? const-decl "bool" real_fun_preds "reals/") (sin_value_strict_increasing formula-decl nil sincos_quad nil)) shostak)) (cos_value_strict_decreasing 0 (cos_value_strict_decreasing-1 nil 3263493549 ("" (expand "cos_value") (("" (lemma "acos_strict_decreasing") (("" (expand "strict_decreasing?") (("" (skosimp*) (("" (lemma "trich_lt" ("x" "inverse(acos)(y!1)" "y" "inverse(acos)(x!1)")) (("" (split -1) (("1" (propax) nil nil) ("2" (lemma "cos_value_bij") (("2" (expand "bijective?") (("2" (expand "injective?") (("2" (flatten) (("2" (inst - "x!1" "y!1") (("2" (expand "cos_value") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (inst - "inverse(acos)(x!1)" "inverse(acos)(y!1)") (("3" (assert) (("3" (lemma "acos_bij") (("3" (lemma "comp_inverse_right[real_abs_le1, nnreal_le_pi]" ("f" "acos")) (("1" (inst-cp - "x!1") (("1" (inst - "y!1") (("1" (assert) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((acos_strict_decreasing formula-decl nil acos nil) (bijective? const-decl "bool" functions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (injective? const-decl "bool" functions nil) (cos_value_bij formula-decl nil sincos_quad nil) (comp_inverse_right formula-decl nil function_inverse nil) (acos_bij formula-decl nil acos nil) (trich_lt formula-decl nil real_props 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types 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) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (inverse const-decl "D" function_inverse nil) (acos const-decl "nnreal_le_pi" acos nil) (strict_decreasing? const-decl "bool" real_fun_preds "reals/") (cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad nil)) shostak)) (cos_value_decreasing 0 (cos_value_decreasing-1 nil 3263653470 ("" (lemma "cos_value_strict_decreasing") (("" (expand "strict_decreasing?") (("" (expand "decreasing?") (("" (skosimp*) (("" (expand "<=" -2) (("" (split -2) (("1" (inst - "x!1" "y!1") (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((strict_decreasing? const-decl "bool" real_fun_preds "reals/") (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) (nnreal_le_pi nonempty-type-eq-decl nil acos 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) (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) (<= const-decl "bool" reals nil) (decreasing? const-decl "bool" real_fun_preds "reals/") (cos_value_strict_decreasing formula-decl nil sincos_quad nil)) shostak)) (sin_value_neg_TCC1 0 (sin_value_neg_TCC1-1 nil 3262931820 ("" (skosimp*) (("" (typepred "xs!1") (("" (grind) nil nil)) nil)) nil) ((real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (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) (Integral const-decl "real" integral_def "analysis/") (atan_value const-decl "real" atan nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) shostak)) (sin_value_neg 0 (sin_value_neg-1 nil 3262931930 ("" (skolem 1 ("z")) (("" (expand "sin_value") (("" (lemma "asin_bij") (("" (expand "bijective?") (("" (flatten) (("" (expand "injective?") (("" (inst - "inverse(asin)(-z)" "-inverse(asin)(z)") (("1" (rewrite "asin_neg" -1) (("1" (lemma "asin_bij") (("1" (lemma "comp_inverse_right" ("f" "asin")) (("1" (inst-cp - "z") (("1" (inst - "-z") (("1" (replace -1) (("1" (replace -2) (("1" (propax) nil nil)) nil)) nil) ("2" (typepred "z") (("2" (hide-all-but (-1 1)) (("2" (expand "abs") (("2" (lemma "trichotomy" ("x" "z")) (("2" (split -1) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "z") (("2" (typepred "inverse[real_abs_le1, real_abs_le_pi2](asin)(z)") (("2" (expand "abs" (-1 1)) (("2" (lemma "trichotomy" ("x" "inverse[real_abs_le1, real_abs_le_pi2](asin)(z)")) (("2" (split -1) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 2) (("3" (typepred "z") (("3" (rewrite "abs_neg") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]" sincos_quad nil) (bijective? const-decl "bool" functions nil) (injective? const-decl "bool" functions nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (trichotomy formula-decl nil real_axioms nil) (NOT const-decl "[bool -> bool]" booleans nil) (asin_neg formula-decl nil asin nil) (comp_inverse_right formula-decl nil function_inverse nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_abs_le1 nonempty-type-eq-decl nil asin 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 "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_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (inverse const-decl "D" function_inverse nil) (asin const-decl "real_abs_le_pi2" asin nil) (z skolem-const-decl "real_abs_le_pi2" sincos_quad nil) (minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (asin_bij formula-decl nil asin nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) shostak)) (cos_value_neg_TCC1 0 (cos_value_neg_TCC1-1 nil 3262931846 ("" (skosimp*) (("" (typepred "xc!1") (("" (assert) nil nil)) nil)) nil) ((nnreal_le_pi nonempty-type-eq-decl nil acos 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) (nnreal type-eq-decl nil real_types 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) (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_minus_real_is_real application-judgement "real" reals nil)) shostak)) (cos_value_neg 0 (cos_value_neg-1 nil 3262936217 ("" (skolem 1 ("z")) (("" (typepred "z") (("" (typepred "cos_value(z)") (("" (lemma "acos_bij") (("" (expand "bijective?") (("" (expand "injective?") (("" (flatten) (("" (inst - "cos_value(pi - z)" "-cos_value(z)") (("1" (expand "cos_value" (-1 1)) (("1" (rewrite "acos_neg" -1) (("1" (lemma "acos_bij") (("1" (lemma "comp_inverse_right[real_abs_le1, nnreal_le_pi]" ("f" "acos" "y" "pi-z")) (("1" (replace -1) (("1" (lemma "comp_inverse_right[real_abs_le1, nnreal_le_pi]" ("f" "acos" "y" "z")) (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (mult-by -2 "-1" -) (("2" (mult-by -3 "-1" -) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnreal_le_pi nonempty-type-eq-decl nil acos 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) (nnreal type-eq-decl nil real_types 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) (acos_bij formula-decl nil acos nil) (injective? const-decl "bool" functions 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) (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (z skolem-const-decl "nnreal_le_pi" sincos_quad nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (acos const-decl "nnreal_le_pi" acos nil) (inverse const-decl "D" function_inverse nil) (acos_neg formula-decl nil acos nil) (comp_inverse_right formula-decl nil function_inverse nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (real_times_real_is_real application-judgement "real" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (both_sides_times_neg_le1_imp formula-decl nil extra_real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (bijective? const-decl "bool" functions nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad nil)) shostak)) (sin_eqv_cos_value_TCC1 0 (sin_eqv_cos_value_TCC1-1 nil 3262931867 ("" (skosimp*) (("" (typepred "xs!1") (("" (expand "abs") (("" (case "xs!1<0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (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) (real_plus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" 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) (< const-decl "bool" reals nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) shostak)) (sin_eqv_cos_value 0 (sin_eqv_cos_value-1 nil 3262933457 ("" (skolem 1 ("z")) (("" (typepred "z") (("" (typepred "cos_value(pi / 2 + z)") (("1" (expand "cos_value") (("1" (expand "sin_value") (("1" (lemma "acos_bij") (("1" (expand "bijective?") (("1" (flatten) (("1" (expand "injective?") (("1" (inst - "inverse(asin)(z)" "-inverse(acos)(pi / 2 + z)") (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (rewrite "acos_neg" 1) (("2" (lemma "acos_bij") (("2" (lemma "comp_inverse_right[real_abs_le1, nnreal_le_pi]" ("f" "acos" "y" "pi/2+z")) (("1" (replace -1) (("1" (lemma "asin_bij") (("1" (expand "acos" 1) (("1" (lemma "comp_inverse_right" ("f" "asin" "y" "z")) (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "abs" -3) (("2" (lift-if) (("2" (lemma "abs_neg") (("2" (inst?) (("1" (assert) nil nil) ("2" (assert) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (expand "abs" -3) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "abs") (("2" (case "z<0") (("1" (assert) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (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) (acos_bij formula-decl nil acos nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (inverse const-decl "D" function_inverse nil) (acos const-decl "nnreal_le_pi" acos nil) (z skolem-const-decl "real_abs_le_pi2" sincos_quad nil) (asin const-decl "real_abs_le_pi2" asin nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (asin_bij formula-decl nil asin nil) (comp_inverse_right formula-decl nil function_inverse nil) (real_minus_real_is_real application-judgement "real" reals nil) (acos_neg formula-decl nil acos nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (abs_neg formula-decl nil abs_lems "reals/") (injective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]" sincos_quad nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnreal type-eq-decl nil real_types nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) shostak)) (sin_eqv_cos_quad_TCC1 0 (sin_eqv_cos_quad_TCC1-1 nil 3264746830 ("" (skosimp*) (("" (assert) nil nil)) nil) ((minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (sin_eqv_cos_quad_TCC2 0 (sin_eqv_cos_quad_TCC2-1 nil 3264746830 ("" (skosimp*) (("" (assert) nil nil)) nil) ((posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (sin_eqv_cos_quad 0 (sin_eqv_cos_quad-1 nil 3264746643 ("" (skosimp*) (("" (lemma "sin_eqv_cos_value" ("xs" "q1!1")) (("1" (replace -1) (("1" (lemma "cos_value_neg" ("xc" "pi/2-q1!1")) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil) ((nnreal_quad1_closed nonempty-type-eq-decl nil sincos_quad nil) (nnreal type-eq-decl nil real_types nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin 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) (sin_eqv_cos_value formula-decl nil sincos_quad nil) (real_minus_real_is_real application-judgement "real" reals nil) (cos_value_neg formula-decl nil sincos_quad nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (cos_eqv_sin_quad_TCC1 0 (cos_eqv_sin_quad_TCC1-1 nil 3264746830 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (cos_eqv_sin_quad_TCC2 0 (cos_eqv_sin_quad_TCC2-1 nil 3264746830 ("" (skosimp*) (("" (assert) nil nil)) nil) ((posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (cos_eqv_sin_quad 0 (cos_eqv_sin_quad-1 nil 3264746754 ("" (skosimp*) (("" (lemma "sin_eqv_cos_quad" ("q1" "pi/2-q1!1")) (("" (assert) nil nil)) nil)) nil) ((- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal_quad1_closed nonempty-type-eq-decl nil sincos_quad 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) (sin_eqv_cos_quad formula-decl nil sincos_quad nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (AND const-decl "[bool, bool -> bool]" booleans nil)) shostak)) (sin_value_minus_pi2_TCC1 0 (sin_value_minus_pi2_TCC1-1 nil 3262955945 ("" (expand "abs") (("" (typepred "pi") (("" (assert) nil nil)) nil)) nil) ((minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types 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) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (>= 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)) shostak)) (sin_value_minus_pi2 0 (sin_value_minus_pi2-1 nil 3262955592 ("" (lemma "asin_bij") (("" (expand "sin_value") (("" (lemma "asin_minus1") (("" (lemma "bijective_inverse[real_abs_le1, real_abs_le_pi2]" ("f" "asin" "y" "-pi/2" "x" "-1")) (("1" (assert) nil nil) ("2" (propax) nil nil) ("3" (expand "abs" 1) (("3" (assert) nil nil)) nil) ("4" (expand "abs" 1) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) 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) (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, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (- const-decl "[numfield -> numfield]" number_fields 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) (asin const-decl "real_abs_le_pi2" asin nil) (bijective? const-decl "bool" functions nil) (bijective_inverse formula-decl nil function_inverse nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (asin_minus1 formula-decl nil asin nil) (asin_bij formula-decl nil asin nil)) shostak)) (sin_value_0_TCC1 0 (sin_value_0_TCC1-1 nil 3262955946 ("" (assert) (("" (assert) nil nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) shostak)) (sin_value_0 0 (sin_value_0-1 nil 3262955772 ("" (expand "sin_value") (("" (lemma "asin_0") (("" (lemma "asin_bij") (("" (lemma "bijective_inverse[real_abs_le1, real_abs_le_pi2]" ("f" "asin" "y" "0" "x" "0")) (("1" (assert) nil nil) ("2" (propax) nil nil) ("3" (expand "abs") (("3" (assert) nil nil)) nil) ("4" (expand "abs") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((asin_0 formula-decl nil asin nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin 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, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (- const-decl "[numfield -> numfield]" number_fields 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) (asin const-decl "real_abs_le_pi2" asin nil) (bijective? const-decl "bool" functions nil) (bijective_inverse formula-decl nil function_inverse nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (asin_bij formula-decl nil asin nil) (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]" sincos_quad nil)) shostak)) (sin_value_pi4_TCC1 0 (sin_value_pi4_TCC1-1 nil 3264489358 ("" (expand "abs") (("" (typepred "pi") (("" (assert) nil nil)) nil)) nil) ((posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types 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) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (>= 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)) shostak)) (sin_value_pi4 0 (sin_value_pi4-1 nil 3264488902 ("" (lemma "asin_sqrt_half") (("" (lemma "asin_bij") (("" (expand "sin_value") (("" (lemma "bijective_inverse[real_abs_le1, real_abs_le_pi2]" ("f" "asin" "y" "pi/4" "x" "sqrt(1/2)")) (("1" (assert) nil nil) ("2" (propax) nil nil) ("3" (expand "abs" 1) (("3" (typepred "pi") (("3" (assert) nil nil)) nil)) nil) ("4" (expand "abs") (("4" (typepred "sqrt(1/2)") (("4" (assert) (("4" (lemma "sqrt_le" ("nny" "1/2" "nnz" "1")) (("4" (rewrite "sqrt_1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((asin_bij formula-decl nil asin nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin 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, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (- const-decl "[numfield -> numfield]" number_fields 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) (asin const-decl "real_abs_le_pi2" asin nil) (bijective? const-decl "bool" functions nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.38 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
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.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
