Quelle sincos_quad.prf
Sprache: Lisp
(sincos_quadnil 3263653658 ("" (assert ) nil nil )"(total_order?[real])" nil )"posreal" nil ))nil 3269611563 ("" (assert ) nil nil )"(strict_total_order?[real])" real_props nil )"posreal" nil ))nil 3265387997 ("" (assert ) nil nil )"(strict_total_order?[real])" real_props nil )"posreal" nil ))nil 3477834241"" (expand "not_one_element?" )"" (skosimp*)"" (inst-cp + "pi/4" )"" (inst + "pi/8" )"" (flatten) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil atan nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"bool" deriv_domain_def "analysis/" )"nzreal" real_typesnil ))nil 3477834289"" (expand "not_one_element?" )"" (skosimp*)"" (inst-cp + "0" )"" (inst + "1/2" )"" (flatten) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"posrat" nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil asin nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" deriv_domain_def "analysis/" ))nil 3477834336"" (expand "not_one_element?" )"" (skosimp*)"" (inst-cp + "pi/2" )"" (inst + "pi/4" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil sincos_quad nil )"posreal" atan nil ) (< const-decl "bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"bool" deriv_domain_def "analysis/" ))nil ))nil 3477834383"" (expand "not_one_element?" )"" (skosimp*)"" (inst-cp + "pi/4" )"" (inst + "pi/8" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil atan nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"bool" deriv_domain_def "analysis/" )"nzreal" real_typesnil ))nil ))nil 3477834403"" (expand "not_one_element?" )"" (skosimp*)"" (inst-cp + "pi/8" )"" (inst + "pi/6" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posreal" atan nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"bool" deriv_domain_def "analysis/" ))nil ))nil 3477834411"" (expand "connected?" )"" (skosimp*) (("" (assert ) nil nil )) nil )) nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"bool" deriv_domain_def "analysis/" )"nzreal" real_typesnil ))nil 3477834437"" (expand "connected?" )"" (skosimp*) (("" (assert ) nil nil )) nil )) nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"bool" deriv_domain_def "analysis/" ))nil 3477834446"" (expand "connected?" )"" (skosimp*) (("" (assert ) nil nil )) nil )) nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"bool" deriv_domain_def "analysis/" ))nil 3472550428"" (lemma "deriv_domain_open" ) (("" (inst - "-1" "1" ) nil nil ))nil )"odd_int" integers nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil deriv_domain "analysis/" ))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 )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )"boolean" notequal nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sincos_quad nil )nil intervals_real "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"bool" deriv_domain_def "analysis/" )"real" reals nil )nil deriv_domain "analysis/" ))nil 3477834559"" (lemma "deriv_domain_open" )"" (inst - "-pi/2" "pi/2" ) nil nil )) nil )"nzreal" nil )"posreal" nil )"nzreal" real_typesnil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil deriv_domain "analysis/" ))nil 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" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )"real" reals nil )"bool" deriv_domain_def "analysis/" )"(strict_total_order?[real])" real_props nil )nil intervals_real "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )nil deriv_domain "analysis/" ))nil 3262932114"" (expand "sin_value" )"" (lemma "asin_bij" )"" "bij_inv_is_bij[real_abs_le1, real_abs_le_pi2]" "f" "asin" ))"" (assert ) nil nil )) nil ))nil ))nil )nil asin nil )nil function_inverse nil )"real_abs_le_pi2" asin nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil asin nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil asin nil )"[real_abs_le_pi2 -> real_abs_le1]" nil ))nil 3262932269"" (lemma "acos_bij" )"" "bij_inv_is_bij[real_abs_le1, nnreal_le_pi]" ("f" "acos" ))"" (expand "cos_value" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil acos nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil asin nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"nnreal_le_pi" acos nil )nil function_inverse nil )"[nnreal_le_pi -> real_abs_le1]" sincos_quadnil )nil acos nil ))nil 3264344138"" (lemma "asin_strict_increasing" )"" (expand "strict_increasing?" )"" (skosimp*)"" (expand "sin_value" )"" (lemma "asin_bij" )"" "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" "inverse(asin)(y!1)" "inverse(asin)(x!1)" )"3" (assert )"3" "comp_inverse_right[real_abs_le1, real_abs_le_pi2]" "f" "asin" "y" "x!1" ))"3" "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 )"nzreal" real_typesnil )"bool" real_fun_preds "reals/" )"[real_abs_le_pi2 -> real_abs_le1]" nil )"real_abs_le_pi2" asin nil )"D" function_inverse nil )nil asin nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil asin nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )nil function_inverse nil )nil function_inverse nil )"bool" functions nil )"bool" functions nil )"(strict_total_order?[real])" real_props nil )nil asin nil )nil asin nil ))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 )"nzreal" real_typesnil )"bool" real_fun_preds "reals/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil asin nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" reals nil )"bool" real_fun_preds "reals/" )nil sincos_quad nil ))nil 3263493549"" (expand "cos_value" )"" (lemma "acos_strict_decreasing" )"" (expand "strict_decreasing?" )"" (skosimp*)"" "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" "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 )nil acos nil )"bool" functions nil )"(strict_total_order?[real])" real_props nil )"bool" functions nil )nil sincos_quad nil )nil function_inverse nil )nil acos nil )nil real_props nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil asin nil )"bool" reals nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil acos nil )"D" function_inverse nil )"nnreal_le_pi" acos nil )"bool" real_fun_preds "reals/" )"[nnreal_le_pi -> real_abs_le1]" sincos_quadnil ))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 )"bool" real_fun_preds "reals/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil acos nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" reals nil )"bool" real_fun_preds "reals/" )nil sincos_quad nil ))nil 3262931820"" (skosimp*) (("" (typepred "xs!1" ) (("" (grind) nil nil )) nil ))nil )nil asin nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"real" integral_def "analysis/" )"real" atan nil )"posreal" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"nzreal" nil )"(total_order?[real])" nil )"nzreal" real_typesnil ))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" "trichotomy" ("x" "z" ))"2" "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" "inverse[real_abs_le1, real_abs_le_pi2](asin)(z)" )"2" (expand "abs" (-1 1))"2" "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 )"[real_abs_le_pi2 -> real_abs_le1]" nil )"bool" functions nil )"bool" functions nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"nzreal" nil )"posreal" nil )nil real_axioms nil )NOT const-decl "[bool -> bool]" booleans nil )nil asin nil )nil function_inverse nil )nil booleans nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil asin nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil asin nil )"D" function_inverse nil )"real_abs_le_pi2" asin nil )"real_abs_le_pi2" sincos_quad nil )"real" reals nil )"(total_order?[real])" nil )nil asin nil )"nzreal" real_typesnil ))nil 3262931846"" (skosimp*) (("" (typepred "xc!1" ) (("" (assert ) nil nil )) nil ))nil )nil acos nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" reals nil ))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" "comp_inverse_right[real_abs_le1, nnreal_le_pi]" "f" "acos" "y" "pi-z" ))"1" (replace -1)"1" "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 )nil acos nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil acos nil )"bool" functions nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )"nnreal_le_pi" sincos_quad nil )"[numfield, numfield -> numfield]" number_fields nil )"nnreal_le_pi" acos nil )"D" function_inverse nil )nil acos nil )nil function_inverse nil )"odd_int" integers nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" reals nil )nil real_types nil )nil extra_real_propsnil )"odd_int" integers nil )"bool" functions nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil asin nil )"[nnreal_le_pi -> real_abs_le1]" sincos_quadnil ))nil 3262931867"" (skosimp*)"" (typepred "xs!1" )"" (expand "abs" )"" (case "xs!1<0" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil ))nil )nil asin nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"real" reals nil )"(total_order?[real])" nil )"posreal" nil )"nzreal" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"nzreal" real_typesnil ))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" "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" "comp_inverse_right[real_abs_le1, nnreal_le_pi]" "f" "acos" "y" "pi/2+z" ))"1" replace -1)"1" "asin_bij" )"1" expand "acos" 1)"1" "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 )nil asin nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil acos nil )"(total_order?[real])" nil )"real" reals nil )"D" function_inverse nil )"nnreal_le_pi" acos nil )"real_abs_le_pi2" sincos_quad nil )"real_abs_le_pi2" asin nil )"nzreal" nil )nil asin nil )nil function_inverse nil )"real" reals nil )nil acos nil )"odd_int" integers nil )"nzreal" nil )nil abs_lems "reals/" )"bool" functions nil )"bool" functions nil )"[real_abs_le_pi2 -> real_abs_le1]" nil )"posreal" nil )"(total_order?[real])" nil )"real" reals nil )nil real_types nil )nil acos nil )nil asin nil )"[nnreal_le_pi -> real_abs_le1]" sincos_quadnil )"[numfield, numfield -> numfield]" number_fields nil )"nzreal" real_typesnil ))nil 3264746830"" (skosimp*) (("" (assert ) nil nil )) nil )"nzreal" real_typesnil )"nzreal" nil )"(total_order?[real])" nil ))nil 3264746830"" (skosimp*) (("" (assert ) nil nil )) nil )"posreal" nil )"real" reals nil )"(total_order?[real])" nil ))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 )nil sincos_quad nil )nil real_types nil )nil asin nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sincos_quad nil )"real" reals nil )nil sincos_quad nil )nil acos nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"real" reals nil )"posreal" nil )"posreal" nil ))nil 3264746830"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil ))nil 3264746830"" (skosimp*) (("" (assert ) nil nil )) nil )"posreal" nil )"real" reals nil )"nzreal" real_typesnil )"nzreal" nil )"(total_order?[real])" nil ))nil 3264746754"" (skosimp*)"" (lemma "sin_eqv_cos_quad" ("q1" "pi/2-q1!1" ))"" (assert ) nil nil )) nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )nil sincos_quad nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sincos_quad nil )"real" reals nil )"(total_order?[real])" nil )"posreal" nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil ))nil 3262955945"" (expand "abs" )"" (typepred "pi" ) (("" (assert ) nil nil )) nil )) nil )"nzreal" real_typesnil )"nzreal" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil ))nil 3262955592"" (lemma "asin_bij" )"" (expand "sin_value" )"" (lemma "asin_minus1" )"" "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 )"[real_abs_le_pi2 -> real_abs_le1]" nil )nil asin nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil asin nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real_abs_le_pi2" asin nil )"bool" functions nil )nil function_inverse nil )"nzreal" nil )"odd_int" integers nil )"nzreal" real_typesnil )nil asin nil )nil asin nil ))nil 3262955946"" (assert ) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"nzreal" nil )"nzreal" real_typesnil ))nil 3262955772"" (expand "sin_value" )"" (lemma "asin_0" )"" (lemma "asin_bij" )"" "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 )nil asin nil )nil asin nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil asin nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real_abs_le_pi2" asin nil )"bool" functions nil )nil function_inverse nil )"nzreal" real_typesnil )nil asin nil )"[real_abs_le_pi2 -> real_abs_le1]" nil ))nil 3264489358"" (expand "abs" )"" (typepred "pi" ) (("" (assert ) nil nil )) nil )) nil )"posreal" nil )"nzreal" real_typesnil )"nzreal" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil ))nil 3264488902"" (lemma "asin_sqrt_half" )"" (lemma "asin_bij" )"" (expand "sin_value" )"" "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 )nil asin nil )nil asin nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil asin nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real_abs_le_pi2" asin nil )"bool" functions nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )nil real_types nil )quality 100%
¤ Dauer der Verarbeitung: 0.25 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-03-28
