Impressum atan2.prf
Sprache: Lisp
(atan2nil 3269553691 ("" (grind) nil 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, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil ))nil 3269553735 ("" (grind) nil 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, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil ))nil 3269553749 ("" (grind) nil 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, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil ))nil 3269553757 ("" (grind) nil 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 )"boolean" notequal nil ))nil 3269553764 ("" (grind) nil 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 )"real" reals nil )"boolean" notequal nil )"real" integral_def "analysis/" )"real" atan nil )"real_abs_lt_pi2" atan nil )"posreal" atan nil )"real" atan2 nil ))nil 3269553778"" (skosimp*) (("" (assert ) nil nil )) nil )"(strict_total_order?[real])" real_props nil ))nil 3269554070"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3269554130"" (skosimp*)"" (lemma "trichotomy" ("x" "x!1" ))"" (expand "atan2" )"" (split -1)"1" (assert )"1" (lemma "trichotomy" ("x" "y!1" ))"1" (split -1)"1" (assert )"1" (typepred "atan(y!1 / x!1)" )"1" (expand "pi" )"1" (expand "pi" )"1" (lemma "atan_strict_increasing" )"1" (expand "strict_increasing?" )"1" (inst - "0" "y!1/x!1" )"1" "posreal_div_posreal_is_posreal" "px" "y!1" "py" "x!1" ))"1" assert )"1" rewrite "atan_0" )"1" expand "abs" )"1" assert )"1" expand "atan" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1)"2" (assert )"2" (rewrite "atan_0" ) (("2" (assert ) nil nil ))nil ))nil ))nil )"3" (assert )"3" (lemma "atan_strict_increasing" )"3" (expand "strict_increasing?" )"3" (typepred "atan(y!1 / x!1)" )"3" (inst - "y!1/x!1" "0" )"3" "both_sides_div_pos_gt1" "x" "0" "y" "y!1" "pz" "x!1" ))"3" (assert )"3" rewrite "atan_0" )"3" expand "abs" )"3" assert )"3" expand "pi" )"3" expand "pi" )"3" expand "atan" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1)"2" (assert )"2" (lemma "trichotomy" ("x" "y!1" ))"2" (split -1)"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (assert )"3" (hide -2)"3" (lemma "trichotomy" ("x" "y!1" ))"3" (split -1)"1" (assert )"1" (lemma "both_sides_div_neg_gt1" )"1" (inst - "x!1" "0" "y!1" )"1" (assert )"1" (lemma "atan_strict_increasing" )"1" (expand "strict_increasing?" )"1" "y!1/x!1" "0" )"1" rewrite "atan_0" )"1" "atan(y!1/x!1)" )"1" expand "abs" )"1" assert )"1" assert )"1" expand "pi" )"1" expand "pi" )"1" expand "atan" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (replace -1)"2" (rewrite "atan_0" ) (("2" (assert ) nil nil ))nil ))nil ))nil )"3" "negreal_div_negreal_is_posreal" "nx" "y!1" "ny" "x!1" ))"1" (lemma "atan_strict_increasing" )"1" (expand "strict_increasing?" )"1" (inst - "0" "y!1/x!1" )"1" (rewrite "atan_0" )"1" (assert )"1" "atan(y!1/x!1)" )"1" expand "abs" )"1" expand "pi" )"1" expand "pi" )"1" expand "atan" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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_axioms nil )"real" reals nil )"nzreal" nil )nil real_props nil )"nzreal" real_typesnil )"posreal" nil )"real" reals nil )"real" reals nil )"bool" real_fun_preds "reals/" )nil real_types nil )nil atan nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil atan nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil atan nil )"real_abs_lt_pi2" atan nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"posreal" nil )nil real_props nil )"bool" reals nil )nil real_types nil )nil real_types nil )"posreal" nil )nil real_types nil )"real" atan2 nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil 3269553812 ("" (grind) nil 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 )"boolean" notequal nil ))nil 3269552776"" (skosimp*)"" (lemma "atan2_0_2pi" ("x" "x!1" "y" "y!1" ))"" (replace -2 -1)"" (flatten -1)"" (lemma "trichotomy" ("x" "x!1" ))"" (split -1)"1" (assert )"1" (hide -3 -4 -6)"1" (case "y!1>=0" )"1" (assert )"1" (flatten -3) (("1" (assert ) nil nil )) nil ))nil )"2" (assert )"2" (flatten -3) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (lemma "trichotomy" ("x" "y!1" ))"2" (split -1)"1" (assert )"1" (flatten (-3 -4)) (("1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil )"3" (assert )"3" (flatten (-5 -6)) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (assert )"3" (hide -2 -5 -6)"3" (case "y!1>=0" )"1" (assert )"1" (flatten -3) (("1" (assert ) nil nil )) nil ))nil )"2" (assert )"2" (flatten -3) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil atan2 nil )"posreal" nil )"(total_order?[real])" nil )"bool" reals nil )nil booleans nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )nil real_axioms nil ))nil ))nil 3414423407"" (inst + "0" ) (("" (assert ) nil nil )) nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields 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 )"(strict_total_order?[real])" real_props nil )"posreal" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil ))nil 3414423407"" (skosimp*)"" (typepred "y!1" )"" (rewrite "atan2_ge_0_lt_2pi" ) (("" (ground) nil nil )) nil ))nil ))nil )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil numbers nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )nil atan2 nil ))nil ))nil 3269628375"" (skosimp*)"" (assert )"" (split -1)"1" "both_sides_times1" ("x" "x!1" "y" "0" "n0z" "pz!1" ))"1" (assert ) nil nil )) nil )"2" "both_sides_times1" ("x" "y!1" "y" "0" "n0z" "pz!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"real" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"boolean" notequal 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 )"nnreal" nil ))nil 3269616367"" (skosimp*)"" (expand "atan2" )"" "both_sides_times_pos_gt1" "x" "x!1" "y" "0" "pz" "pz!1" ))"" (replace -1)"" (case "x!1>0" )"1" (assert )"1" "both_sides_times_pos_ge1" "x" "y!1" "y" "0" "pz" "pz!1" ))"1" (replace -1)"1" (case "y!1>=0" )"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (case "x!1=0" )"1" (assert )"1" "both_sides_times_pos_gt1" "x" "y!1" "y" "0" "pz" "pz!1" ))"1" (replace -1) (("1" (propax) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"real" atan2 nil )"[T, T -> boolean]" equalities nil )"(total_order?[real])" nil )"nnreal" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"real" reals nil )"real" reals nil )nil real_props 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 )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil ))nil 3269628375"" (skosimp*)"" (lemma "both_sides_times1" ("x" "y!1" "y" "0" "n0z" "nz!1" ))"" (lemma "both_sides_times1" ("x" "x!1" "y" "0" "n0z" "nz!1" ))"" (assert ) nil nil )) nil ))nil ))nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"boolean" notequal 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 )"real" reals nil ))nil 3269628659"" (skosimp*)"" (expand "atan2" )"" (lemma "both_sides_times1" ("x" "x!1" "y" "0" "n0z" "nz!1" ))"" (replace -1)"" (case "y!1=0" )"1" (replace -1)"1" (rewrite "atan_0" )"1" (simplify 1)"1" (case "x!1>0" )"1" (assert )"1" "both_sides_times_neg_lt1" "x" "x!1" "y" "0" "nz" "nz!1" ))"1" (assert ) nil nil )) nil ))nil )"2" (assert )"2" "both_sides_times_neg_lt1" "x" "x!1" "y" "0" "nz" "nz!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (case "y!1>0" )"1" (hide -2)"1" (assert )"1" "both_sides_times_neg_gt1" "x" "0" "y" "y!1" "nz" "nz!1" ))"1" (assert )"1" (case "x!1>0" )"1" (assert )"1" "both_sides_times_neg_gt1" "x" "0" "y" "x!1" "nz" "nz!1" ))"1" (assert ) nil nil )) nil ))nil )"2" "both_sides_times_neg_gt1" "x" "0" "y" "x!1" "nz" "nz!1" ))"2" (assert )"2" case "x!1=0" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (case "x!1=0" )"1" (assert )"1" "both_sides_times_neg_gt1" "x" "0" "y" "y!1" "nz" "nz!1" ))"1" (assert ) nil nil )) nil ))nil )"2" (assert )"2" (case "x!1>0" )"1" (assert )"1" "both_sides_times_neg_gt1" "x" "0" "y" "x!1" "nz" "nz!1" ))"1" (assert ) nil nil )) nil ))nil )"2" (assert )"2" "both_sides_times_neg_gt1" "y" "0" "x" "x!1" "nz" "nz!1" ))"2" (assert )"2" "both_sides_times_neg_gt1" "y" "0" "x" "y!1" "nz" "nz!1" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"real" atan2 nil )"(total_order?[real])" nil )nil real_props nil )"real" reals nil )"nzreal" real_typesnil )"real" reals nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"bool" reals nil ) (atan_0 formula-decl nil atan nil )"[T, T -> boolean]" equalities 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 )"boolean" notequal nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil ))nil 3514306973 ("" (subtype-tcc) nil 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 )"(strict_total_order?[real])" real_props nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"boolean" notequal nil ))nil ))nil 3514306973 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3514306973 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3514306973 ("" (subtype-tcc) nil 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 )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )"real" reals nil ))nil ))nil 3514306980"" (skeep)"" (case "x > 0 AND y > 0" )"1" (flatten)"1" (hide -3)"1" (expand "atan2" )"1" (assert )"1" (lemma "atan_sub_swap" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"2" (case "x < 0 AND y < 0" )"1" (flatten)"1" (hide -3 1)"1" (expand "atan2" )"1" (assert )"1" (lemma "atan_sub_swap" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 3) (("2" (grind-reals) nil nil )) nil ))nil ))nil ))nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"nzreal" real_typesnil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil atan nil )"real" atan2 nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil ))nil 3514306973 ("" (subtype-tcc) nil 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 )"(strict_total_order?[real])" real_props nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"boolean" notequal nil ))nil ))nil 3514306973 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3514306973 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3514306973 ("" (subtype-tcc) nil 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 )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )"real" reals nil ))nil ))nil 3514307142"" (skeep)"" (case "x > 0 AND y < 0" )"1" (hide -2)"1" (flatten)"1" (expand "atan2" )"1" (assert )"1" (expand "sign" )"1" (lemma "atan_sub_swap" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (case "x < 0 AND y > 0" )"1" (hide -2 1)"1" (flatten)"1" (expand "sign" )"1" (assert )"1" (expand "atan2" )"1" (lemma "atan_sub_swap" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3) (("2" (grind-reals) nil nil )) nil ))nil ))nil ))nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"nzreal" real_typesnil )"nzreal" nil )"real" reals nil )"real" reals nil )"posreal" nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil atan nil )"Sign" sign "reals/" )"real" atan2 nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )nil real_props nil )nil application-judgement "nnreal_lt_2pi" atan2 nil )"odd_int" integers nil ))nil 3514306973 ("" (subtype-tcc) nil 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 )"boolean" notequal nil ))nil ))nil 3514306973 ("" (subtype-tcc) nil 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 )"boolean" notequal nil )"real" integral_def "analysis/" )"real" atan nil )"posreal" atan nil )"real" reals nil )nil application-judgement "nnreal_lt_2pi" atan2 nil )"real" reals nil ))nil ))nil 3514307173"" (skeep)"" (lemma "atan_0" )"" (split)"1" (flatten)"1" (replaces -1)"1" (case "y > 0" )"1" (expand "atan2" ) (("1" (assert ) nil nil )) nil )"2" (expand "atan2" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (flatten)"2" (replaces -1)"2" (case "x > 0" )"1" (expand "atan2" ) (("1" (assert ) nil nil )) nil )"2" (expand "atan2" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil atan nil )"real" reals 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 )"real" reals nil )"real" reals nil )"nzreal" real_typesnil )"(strict_total_order?[real])" real_props nil )"real" atan2 nil )"posreal" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )nil application-judgement "nnreal_lt_2pi" atan2 nil )"posreal" nil ))nil 3269553823"" (skosimp*)"" (typepred "a!1" )"" (lemma "sin_eq_0_2pi" ("a" "a!1" ))"" (lemma "cos_eq_0_2pi" ("a" "a!1" ))"" (assert )"" (split -1)"1" (split -2)"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil )"2" (split -2)"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 trig_basic nil )"posreal" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"trig_range" sincos_def nil )"trig_range" sincos_def nil )"(total_order?[real])" nil )nil trig_basic nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil 3279154016"" (case "FORALL (x:posreal): x < pi => sin(x) > 0" )"1" case "FORALL (x: nnreal): x < pi => atan2(cos(x), sin(x)) = x" )"1" (skolem 1 ("a" ))"1" (case "a < pi" )"1" (inst -2 "a" ) (("1" (assert ) nil nil )) nil )"2" (inst -1 "a-pi" )"1" (assert )"1" (rewrite "cos_minus" )"1" (rewrite "sin_minus" )"1" (rewrite "sin_pi" )"1" (rewrite "cos_pi" )"1" (assert )"1" "atan2_cancel_neg" "x" "cos(a)" "y" "sin(a)" "nz" "-1" ))"1" (case-replace "a=pi" )"1" (rewrite "sin_pi" )"1" rewrite "cos_pi" )"1" (assert ) nil nil ))nil ))nil )"2" (lemma "sin_eq_0_2pi" ("a" "a" ))"2" assert )"2" "a-pi" )"2" assert )"2" rewrite "sin_minus" -3)"2" rewrite "cos_pi" )"2" rewrite "sin_pi" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (skolem 1 ("a" ))"2" (flatten)"2" (inst - "a" )"1" (assert )"1" (expand "atan2" )"1" (lemma "trichotomy" ("x" "cos(a)" ))"1" (split)"1" (assert )"1" (case "a<pi/2" )"1" (rewrite "tan_rew" )"1" (rewrite "atan_tan" )"1" expand "abs" )"1" (propax) nil nil ))nil ))nil )"2" (expand "Tan?" )"2" (assert ) nil nil )) nil ))nil )"2" (lemma "cos_value_strict_decreasing" )"2" (case-replace "a=pi/2" )"1" rewrite "cos_pi2" )"1" (assert ) nil nil ))nil )"2" expand "strict_decreasing?" )"2" "pi/2" "a" )"2" rewrite "cos_value_pi2" )"2" assert )"2" "cos_cos_value" "a" "a" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1)"2" (lemma "cos_eq_0_2pi" ("a" "a" ))"2" (assert ) nil nil )) nil ))nil )"3" (assert )"3" (lemma "cos_value_strict_decreasing" )"3" (expand "strict_decreasing?" )"3" "trich_lt" ("x" "a" "y" "pi/2" ))"3" "1" "a" "pi/2" )"1" rewrite "cos_value_pi2" )"1" assert )"1" rewrite "cos_cos_value" -3)"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" rewrite "cos_pi2" )"2" (assert ) nil nil ))nil ))nil )"3" "3" "b" "a-pi/2" )"3" "sin_plus" )"3" "cos_plus" )"3" "b" "pi/2" )"3" "b" "pi/2" )"3" rewrite "cos_pi2" )"3" rewrite "sin_pi2" )"3" assert )"3" replace -3 -1 rl)"3" replace "3" assert )"3" replace -3)"3" replace "3" replace "3" "3" "atan_neg" "x" "cos(b)/sin(b)" ))"3" replace "3" "posreal_div_posreal_is_posreal" "px" "cos(b)" "py" "sin(b)" ))"3" "atan_inv" "px" "cos(b) / sin(b)" ))"1" rewrite "div_div1" "1" assert )"1" "((1 * sin(b)) / cos(b))=tan(b)" )"1" rewrite "atan_tan" "1" assert )nil nil )"2" expand "abs" )"2" assert )nil nil ))nil ))nil )"2" expand "tan" )"2" assert )nil nil ))nil )"3" expand "Tan?" )"3" assert )nil nil ))nil ))nil ))nil ))nil )"2" 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 )"2" (assert )"2" (case-replace "a=0" )"1" (rewrite "cos_0" )"1" (rewrite "sin_0" )"1" (expand "atan2" )"1" (rewrite "atan_0" ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp)"3" (lemma "sin2_cos2" ("a" "x!1" ))"3" (replace -3)"3" (replace -4)"3" (expand "sq" ) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (case "x!1<=pi/2" )"1" (rewrite "sin_sin_value" )"1" (lemma "sin_value_strict_increasing" )"1" (expand "strict_increasing?" )"1" (inst - "0" "x!1" )"1" (rewrite "sin_value_0" )"1" (assert ) nil nil )) nil )"2" (expand "abs" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (rewrite "sin_sin_phase" )"2" (expand "sin_phase" )"2" (lemma "floor_div" ("x" "2*x!1" "py" "pi" "i" "1" ))"2" (assert )"2" (lemma "sin_value_strict_increasing" )"2" (expand "strict_increasing?" )"2" (inst - "0" "pi-x!1" )"1" (rewrite "sin_value_0" )"1" (assert ) nil nil )) nil )"2" (expand "abs" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sincos_quad nil )nil asin nil )nil sincos_quad nil )"bool" real_fun_preds "reals/" )nil sincos_def nil )"real_abs_le1" sincos_phase nil )"even_int" integersnil )"posint" nil )"nat" floor_ceil nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil floor_ceil nil )nil sincos_def nil )"real" sincos_def nil )"real" atan2 nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"trig_range" sincos_def nil )nil application-judgement "nnreal_lt_2pi" atan2 nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"trig_range" sincos_def nil )"(strict_total_order?[real])" real_props nil )nil trig_basic nil )nil trig_basic nil )nil atan2 nil )"bool" reals nil )nil real_types nil )nil real_types nil )"[numfield -> numfield]" number_fields nil )nil trig_basic nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posreal" nil )"(divides(m))" divides nil )"even_int" integersnil )"(divides(n))" divides nil )"odd_int" integers nil )nil trig_basic nil )"real" reals nil )"real" reals nil )"odd_int" integers nil )nil trig_basic nil )"{z: nnreal | z < 2 * pi}" atan2 nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"(total_order?[real])" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"nnreal" atan2 nil )"posreal" nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"nzreal" nil )nil atan nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil sincos_def nil )nil sincos_def nil )"bool" sincos_def nil )nil trig_basic nil )nil acos nil )nil sincos_def nil )nil sincos_quad nil )"bool" real_fun_preds "reals/" )nil sincos_quad nil )"real" reals nil )"nzreal" real_typesnil )nil trig_basic nil )nil real_props nil )nil trig_basic nil )nil atan nil )nil real_types nil )nil reals nil )nil real_props nil )"real" reals nil )"real" sincos_def nil )nil atan nil )nil trig_basic nil )nil trig_basic nil )nil real_axioms nil )nil trig_basic nil )nil atan nil )nil trig_basic nil )"nonneg_real" sq "reals/" )nil trig_basic 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 )"[bool, bool -> bool]" booleans nil )"bool" reals nil ) (pi const-decl "posreal" atan nil )"real" sincos_def nil ))nil )nil 3269555632"" (skosimp*)"" (expand "atan2" )"" (typepred "a!1" )"" (expand "pi" )"" (expand "cos" )"" (expand "sin" )"" (case "floor(a!1 / (2 * pi)) = 0" )"1" (replace -1)"1" (simplify 1)"1" (hide -1)"1" (lemma "phases_sin" ("x" "a!1" ))"1" (hide -2 -3)"1" (split -1)"1" (lemma "sin_q1" ("x" "a!1" ))"1" "cos_q1" ("x" "a!1" ))"1" replace -3)"1" replace -1)"1" replace -2)"1" "phase_sin_q1" "x" "a!1" ))"1" replace -4)"1" "1" "1" expand "<=" -1)"1" "1" "sin_value_strict_increasing" )"1" expand "strict_increasing?" )"1" "cos_value_strict_decreasing" )"1" expand "strict_decreasing?" )"1" "a!1" "pi/2" )"1" "0" "a!1" )"1" rewrite "sin_value_0" )"1" rewrite "cos_value_pi2" )"1" assert )"1" rewrite "atan_tan_value" )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil )"3" expand "abs" "3" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1 * rl)"2" rewrite "cos_value_0" )"2" rewrite "sin_value_0" )"2" assert )"2" rewrite "atan_0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "phase_sin_q2" ("x" "a!1" ))"2" assert )"2" "sin_q2" ("x" "a!1" ))"2" "cos_q2" ("x" "a!1" ))"2" replace -4)"2" "2" replace -1)"2" replace -2)"2" "sin_value_strict_increasing" )"2" expand "strict_increasing?" )"2" "cos_value_strict_decreasing" )"2" expand "strict_decreasing?" )"2" expand "<=" -5)"2" "1" "0" "a!1-pi/2" )"1" "a!1-pi/2" "pi/2" )"1" "0" "a!1-pi/2" )"1" "a!1-pi/2" "pi/2" )"1" assert )"1" rewrite "sin_value_0" )"1" rewrite "sin_value_pi2" )"1" rewrite "cos_value_0" )"1" rewrite "cos_value_pi2" )"1" assert )"1" "atan_neg" "x" "cos_value(a!1 - pi / 2) / sin_value(a!1 - pi / 2)" ))"1" replace "1" "acos_cos_value" "xc" "a!1-pi/2" ))"1" "1" expand "acos" "1" expand "asin" )"1" rewrite "sq_rew" )"1" rewrite "sin_eqv_sqrt_cos_value" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil )"3" expand "abs" "3" assert )nil nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil )"3" expand "abs" "3" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil )"2" replace "2" assert )"2" rewrite "sin_value_0" )"2" rewrite "cos_value_0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "phase_sin_q3" ("x" "a!1" ))"3" "sin_q3" ("x" "a!1" ))"3" "cos_q3" ("x" "a!1" ))"3" replace -4)"3" "3" replace -1)"3" replace -2)"3" "3" "sin_value_strict_increasing" )"3" expand "strict_increasing?" )"3" "cos_value_strict_decreasing" )"3" expand "strict_decreasing?" )"3" expand "<=" -3)"3" "1" "0" "a!1-pi" )"1" "a!1-pi" "pi/2" )"1" "0" "a!1-pi" )"1" "a!1-pi" "pi/2" )"1" rewrite "sin_value_0" )"1" rewrite "cos_value_pi2" )"1" assert )"1" "atan_tan_value" "qo1" "a!1-pi" ))"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil )"3" expand "abs" "3" assert )nil nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil )"3" expand "abs" "3" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil )"2" replace "2" rewrite "cos_value_0" )"2" rewrite "sin_value_0" )"2" rewrite "atan_0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (lemma "phase_sin_q4" ("x" "a!1" ))"4" "sin_q4" ("x" "a!1" ))"4" "cos_q4" ("x" "a!1" ))"4" replace -4)"4" "4" replace -1)"4" replace -2)"4" "4" expand "<=" -1)"4" "1" "sin_value_strict_increasing" )"1" expand "strict_increasing?" )"1" "0" "a!1-3*pi/2" )"1" rewrite "sin_value_0" )"1" "cos_value_strict_decreasing" )"1" expand "strict_decreasing?" )"1" "a!1-3*pi/2" "pi/2" )"1" rewrite "cos_value_pi2" )"1" assert )"1" "atan_neg" "x" "cos_value(a!1 - 3 * pi / 2) / sin_value(a!1 - 3 * pi / 2)" ))"1" replace "1" "acos_cos_value" "xc" "a!1 - 3 * pi / 2" ))"1" expand "acos" )"1" expand "asin" )"1" "cos_value_strict_decreasing" )"1" expand "strict_decreasing?" )"1" "0" "a!1-3*pi/2" )"1" rewrite "cos_value_0" )"1" assert )"1" rewrite "sq_rew" )"1" rewrite "sin_eqv_sqrt_cos_value" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil )"3" expand "abs" "3" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace -1 * rl)"2" rewrite "sin_value_0" )"2" rewrite "cos_value_0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "floor_def" ("x" "a!1 / (2 * pi)" ))"2" (rewrite "div_mult_pos_lt1" -1)"2" (rewrite "div_mult_pos_le2" -1)"2" (flatten)"2" "K1" "floor(a!1 / (2 * pi))" )"2" (case "K1>=1" )"1" "both_sides_times_pos_le1" "x" "1" "y" "K1" "pz" "2*pi" ))"1" (assert ) nil nil ))nil )"2" case "K1<= -1" )"1" "both_sides_times_pos_le1" "y" "-1" "x" "K1" "pz" "2*pi" ))"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_quad nil )nil atan nil )nil asin nil )"[nnreal_le_pi -> real_abs_le1]" sincos_quadnil )"[real_abs_le_pi2 -> real_abs_le1]" nil )nil sincos_quad nil )"nnreal_le_pi" acos nil )nil sq "reals/" )nil sincos_quad nil )nil sincos_quad nil )"real_abs_le_pi2" asin nil )nil sincos_phase nil )nil sincos_phase nil )"bool" real_fun_preds "reals/" )"bool" real_fun_preds "reals/" )nil sincos_quad nil )nil sincos_quad nil )nil sincos_quad nil )nil sincos_quad nil )nil acos nil )nil sincos_quad nil )nil sincos_quad nil )nil sincos_quad nil )nil atan nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )"posreal" atan nil ))nil 3269552798 ("" (skosimp*) nil nil ) nil nil 3269616826"" (skosimp*)"" (case "FORALL (x:real): sin(atan(x)) = x/sqrt(1+sq(x))" )"1" (expand "atan2" )"1" (case "x!1>0" )"1" (assert )"1" (case "y!1>=0" )"1" (inst - "y!1/x!1" ) (("1" (assert ) nil nil )) nil )"2" (inst - "y!1/x!1" )"2" "sin_period" ("a" "atan(y!1 / x!1)" "j" "1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (assert )"2" (case "x!1=0" )"1" (assert )"1" (replace -1)"1" (rewrite "sin_pi2" )"1" (rewrite "sin_3pi2" ) nil nil )) nil ))nil ))nil )"2" (assert )"2" (rewrite "neg_sin" :dir rl)"2" (inst - "y!1/x!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp*)"2" case "FORALL (px:posreal):sin(atan(px)) = px / sqrt(1 + sq(px))" )"1" (lemma "trichotomy" ("x" "x!2" ))"1" (split -1)"1" (inst - "x!2" ) (("1" (assert ) nil nil )) nil )"2" (replace -1)"2" (rewrite "atan_0" )"2" (rewrite "sin_0" )"2" (rewrite "sq_0" )"2" (rewrite "sqrt_1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (inst - "-x!2" )"1" (rewrite "atan_neg" )"1" (rewrite "sin_neg" )"1" (rewrite "sq_neg" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (expand "sin" )"2" (case "floor(atan(px!1) / (2 * pi)) = 0" )"1" (replace -1)"1" (simplify)"1" (hide -1)"1" (lemma "atan_strict_increasing" )"1" (expand "strict_increasing?" )"1" "0" "px!1" )"1" rewrite "atan_0" )"1" assert )"1" case "atan(px!1)<pi/2" )"1" "phase_sin_q1" "x" "atan(px!1)" ))"1" assert )"1" "sin_q1" "x" "atan(px!1)" ))"1" assert )"1" "sin_value_atan" "x" "px!1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "floor_def" "x" "atan(px!1) / (2 * pi)" ))"2" (rewrite "div_mult_pos_lt1" )"2" (rewrite "div_mult_pos_le2" )"2" (flatten)"2" "K1" "floor(atan(px!1) / (2 * pi))" )"2" "atan(px!1)" )"2" expand "abs" )"2" "atan_strict_increasing" )"2" expand "strict_increasing?" )"2" "0" "px!1" )"2" rewrite "atan_0" )"2" assert )"2" expand "pi" )"2" expand "atan" )"2" case "K1>=1" )"1" "both_sides_times_pos_ge1" "x" "K1" "y" "1" "pz" "8*atan_value(1)" ))"1" assert )nil nil )"2" "both_sides_times_pos_le1" "x" "K1" "y" "-1" "pz" "8*atan_value(1)" ))"1" case "K1<=-1" )"1" assert )nil nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil )"2" assert )"2" "both_sides_times_pos_le1" "x" "K1" "y" "-1" "pz" "8*atan_value(1)" ))"2" case "K1<=-1" )"1" assert )nil nil )"2" 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 )"nonneg_real" sq "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"real_abs_lt_pi2" atan 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 )"real" sincos_def nil )"[T, T -> boolean]" equalities nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" sqrt "reals/" )"posreal" nil )"real" reals nil )"trig_range" sincos_def nil )"nzreal" real_typesnil )nil trig_basic nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"real" reals nil )"posreal" nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil trig_basic nil )nil trig_basic nil )"odd_int" integers nil )nil trig_basic nil )"real" reals nil )"real" atan2 nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"real" reals nil )nil real_props nil )"int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )nil real_props nil )"real" atan nil )nil real_props nil )"nzreal" nil )nil real_props nil )nil floor_ceil nil )"bool" real_fun_preds "reals/" )"(total_order?[real])" nil )nil sincos_quad nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )"(strict_total_order?[real])" real_props nil )nil atan nil )"nnreal" nil )"real" reals nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"bool" reals nil )nil real_axioms nil )nil trig_basic nil )nil sq "reals/" )nil atan nil )nil trig_basic nil )nil sqrt "reals/" )nil sq "reals/" )nil atan nil )"real" atan2 nil )"posreal" nil )"posreal" sq "reals/" ))nil 3269632456"" (skosimp*)"" (case "FORALL (x:real): cos(atan(x)) = 1/sqrt(1+sq(x))" )"1" (expand "atan2" )"1" (lemma "trichotomy" ("x" "x!1" ))"1" (split -1)"1" (assert )"1" "cos_period" ("a" "atan(y!1 / x!1)" "j" "1" ))"1" (replace -1 1 rl)"1" (case "y!1>=0" )"1" (assert )"1" (expand ">=" -1)"1" (expand "<=" -1)"1" (split -1)"1" "both_sides_div_pos_lt1" "x" "0" "y" "y!1" "pz" "x!1" ))"1" (inst - "y!1/x!1" ) nil nil )) nil )"2" (replace -1 * rl)"2" rewrite "atan_0" )"2" rewrite "sq_0" )"2" rewrite "sqrt_1" )"2" rewrite "cos_0" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (case "y!1<0" )"1" "both_sides_div_pos_lt1" "y" "0" "x" "y!1" "pz" "x!1" ))"1" (inst - "-(y!1/x!1)" )"1" (rewrite "atan_neg" -5)"1" rewrite "cos_neg" -5)"1" case "sq(-(y!1 / x!1)) =sq(y!1 / x!1)" )"1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1)"2" (assert )"2" (case "y!1>0" )"1" (assert ) (("1" (rewrite "cos_pi2" ) nil nil ))nil )"2" (rewrite "cos_3pi2" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (assert )"3" (rewrite "neg_cos" :dir rl)"3" (inst - "y!1/x!1" ) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp*)"2" case "FORALL (px:posreal): cos(atan(px)) = cos_value(atan(px))" )"1" (lemma "trichotomy" ("x" "x!2" ))"1" (split -1)"1" (inst - "x!2" )"1" (lemma "cos_value_atan" ("nnx" "x!2" ))"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil )"2" (replace -1)"2" (rewrite "atan_0" )"2" (rewrite "cos_0" )"2" (rewrite "sq_0" )"2" (rewrite "sqrt_1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (inst - "-x!2" )"1" (lemma "cos_value_atan" ("nnx" "-x!2" ))"1" (replace -1 -3)"1" (rewrite "atan_neg" -3)"1" (rewrite "cos_neg" -3)"1" (rewrite "sq_neg" -3) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (case "0 < atan(px!1) & atan(px!1) < pi/2" )"1" (flatten)"1" (name-replace "K1" "atan(px!1)" )"1" (expand "cos" )"1" (case "floor(K1 / (2 * pi)) = 0" )"1" (replace -1)"1" (lemma "phase_sin_q1" ("x" "K1" ))"1" assert )"1" "cos_q1" ("x" "K1" ))"1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" (lemma "floor_def" ("x" "K1/(2*pi)" ))"2" rewrite "div_mult_pos_lt1" )"2" rewrite "div_mult_pos_le2" )"2" "2" "K2" "floor(K1 / (2 * pi))" )"2" case "K2>=1" )"1" "both_sides_times_pos_ge1" "x" "K2" "y" "1" "pz" "2*pi" ))"1" (assert ) nil nil ))nil )"2" case "K2<=-1" )"1" "both_sides_times_pos_le1" "x" "K2" "y" "-1" "pz" "2*pi" ))"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "atan_strict_increasing" )"2" (expand "strict_increasing?" )"2" (inst - "0" "px!1" )"2" (rewrite "atan_0" )"2" (assert )"2" "atan(px!1)" )"2" expand "abs" )"2" expand "pi" )"2" expand "atan" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp*)"3" (lemma "atan_strict_increasing" )"3" (expand "strict_increasing?" )"3" (inst - "0" "px!1" )"3" (rewrite "atan_0" )"3" (typepred "atan(px!1)" )"3" (expand "abs" )"3" (expand "pi" )"3" expand "atan" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nonneg_real" sq "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"real_abs_lt_pi2" atan 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 )"real" sincos_def nil )"[T, T -> boolean]" equalities nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" sqrt "reals/" )"posreal" nil )"posreal" nil )"trig_range" sincos_def nil )nil real_axioms nil )"odd_int" integers nil )"nzreal" nil )nil trig_basic nil )nil trig_basic nil )nil trig_basic nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"posreal" nil )nil atan nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil trig_basic nil )"real" reals nil )"nzreal" real_typesnil )"real" reals nil )"bool" reals nil )nil sq "reals/" )nil trig_basic nil )nil sqrt "reals/" )nil atan nil )nil real_props nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil trig_basic nil )"real" atan2 nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )NOT const-decl "[bool -> bool]" booleans nil )"{i | i <= x & x < i + 1}" floor_ceil nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )"real" reals nil )"nnreal" nil )"(total_order?[real])" nil )nil floor_ceil nil )nil real_props nil )"nzreal" nil )nil real_props nil )nil real_props nil )"int" integers nil )nil real_props nil )nil atan nil )"bool" real_fun_preds "reals/" )nil sq "reals/" )"real" atan2 nil )nil sincos_quad nil )"[nnreal_le_pi -> real_abs_le1]" sincos_quadnil )nil asin nil )nil acos nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.147Bemerkung:
(vorverarbeitet am 2026-04-28)
¤ *Bot Zugriff
2026-05-26
