sincos_phase.prf
Interaktion und
(sincos_phasenil 3264603198 ("" (assert ) nil nil )"(strict_total_order?[real])" real_props nil )"posreal" nil ))nil 3264597671"" (skosimp*)"" (replace -2)"" (hide -2)"" (lemma "floor_def" ("x" "(2*x!1)/pi" ))"" (flatten)"" (assert )"" (replace -3)"" (hide -3)"" (expand "abs" )"" "div_mult_pos_le1" "z" "x!1" "x" "1" "py" "pi/2" ))"" (replace -1 1 rl)"" (hide -1)"" (rewrite "div_div1" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nzreal" real_typesnil )nil sincos_phase 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 booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil floor_ceil nil )"nnreal" nil )"nzreal" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"nat" floor_ceil nil )"(total_order?[real])" nil )nil reals nil )nil real_props nil )"posint" nil )"odd_int" integers nil )nil real_props nil )"posreal" nil )"nnreal" nil ))nil 3264597671"" (skosimp*)"" (replace -2)"" (hide -2 1)"" (lemma "floor_def" ("x" "(2 * x!1) / pi" ))"" (replace -2 * rl)"" (flatten)"" (replace -3)"" (hide -3)"" (expand "abs" )"" "div_mult_pos_lt1" "x" "1" "z" "x!1" "py" "pi" ))"" "both_sides_times_pos_lt1" "x" "x!1/pi" "y" "1" "pz" "2" ))"" (replace -1 -2 rl)"" (replace -4 -2)"" (flatten -2)"" "" assert )"" "div_mult_pos_le2" "x" "1" "z" "2*x!1" "py" "pi" ))"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nzreal" real_typesnil )nil sincos_phase 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 booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil floor_ceil nil )"nnreal" nil )nil real_props nil )"odd_int" integersnil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil real_props nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"(total_order?[real])" nil )"nzreal" nil )"real" reals nil )nil real_props nil )"nat" floor_ceil nil )"nnreal" nil ))nil 3264597671"" (skosimp*)"" (replace -2)"" (hide -2 1 2)"" (lemma "floor_def" ("x" "(2*x!1)/pi" ))"" (flatten)"" (replace -3)"" (hide -3)"" "div_mult_pos_le2" "x" "2" "z" "2*x!1" "py" "pi" ))"" "both_sides_times_pos_le1" "x" "pi" "y" "x!1" "pz" "2" ))"" (expand "abs" 1)"" (assert )"" "div_mult_pos_lt1" "z" "2*x!1" "py" "pi" "x" "3" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nzreal" real_typesnil )nil sincos_phase 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 booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil floor_ceil nil )"nnreal" nil )"nat" floor_ceil nil )nil real_props nil )"real" reals nil )"nzreal" nil )"posreal" nil )"odd_int" integers nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posreal" nil )nil real_props nil )nil real_props nil )"nnreal" nil ))"fix" 3399981374"" (skosimp*)"" (case "floor((2 * x!1) / pi) = 0" )"1" (replace -1) (("1" (propax) nil nil )) nil )"2" (assert )"2" (case "floor((2 * x!1) / pi) = 1" )"1" (replace -1) (("1" (propax) nil nil )) nil )"2" (case "floor((2 * x!1) / pi) = 2" )"1" (rewrite "abs_neg" ) (("1" (assert ) nil nil )) nil )"2" (lemma "floor_def" ("x" "(2*x!1)/pi" ))"2" (flatten)"2" (replace -3)"2" "div_mult_pos_le2" "z" "2*x!1" "py" "pi" "x" "2" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sincos_phase nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_types nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil ) (<= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"nnreal" nil )"nat" floor_ceil nil )nil floor_ceil nil )"posint" nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"(total_order?[real])" nil )"odd_int" integers nil )"real" reals nil )"real" reals nil )"nnreal" nil ))nil 3399981363";;; Proof sin_phase_TCC4-2 for formula sincos_phase.sin_phase_TCC4" ";;; Proof sin_phase_TCC4-2 for formula sincos_phase.sin_phase_TCC4" case "floor((2 * x!1) / pi) = 0" )"1" (replace -1) (("1" (propax) nil )))"2" (assert )"2" (case "floor((2 * x!1) / pi) = 1" )"1" (replace -1) (("1" (propax) nil )))"2" (case "floor((2 * x!1) / pi) = 2" )"1" (rewrite "abs_neg" ) (("1" (assert ) nil )))"2" (lemma "floor_def" ("x" "(2*x!1)/pi" ))"2" (flatten)"2" (replace -3)"2" "div_mult_pos_le2" "z" "2*x!1" "py" "pi" "x" "2" ))"2" (assert ) nil ))))))))))))))))))";;; developed with shostak decision procedures") nil asin nil )nil asin nil )"[real_abs_le_pi2 -> real_abs_le1]" nil )"posreal" atan nil ))nil )nil 3264597671"" (skosimp*)"" (lemma "floor_def" ("x" "(2 * x!1) / pi" ))"" (replace -2 * rl)"" (flatten)"" (hide -3)"" "div_mult_pos_le2" "x" "i!1" "py" "pi" "z" "2*x!1" ))"" "div_mult_pos_lt1" "x" "i!1+1" "py" "pi" "z" "2*x!1" ))"" (typepred "x!1" )"" (replace -6)"" (replace -5)"" (flatten)"" (expand "abs" )"" "both_sides_times_pos_lt1" "x" "x!1" "y" "2*pi" "pz" "2" ))"" (replace -3 -1)"" "" "div_mult_pos_le2" "z" "pi" "py" "2" "x" "2*pi-x!1" ))"" replace -1 4)"" "" "both_sides_plus_le1" "x" "(2*pi-x!1)*2" "y" "pi" "z" "2*x!1-pi" ))"" replace -1 4 rl)"" "" assert )"" case "i!1 < 0" )"1" (assert ) nil nil )"2" case "i!1 = 3" )"1" assert )nil nil )"2" case "i!1=4" )"1" assert )nil nil )"2" case "i!1>4" )"1" assert )"1" "div_mult_pos_le2" "x" "4" "z" "2*x!1" "py" "pi" ))"1" assert )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 )"posreal" atan nil )) shostak))nil 3399981395"" (skosimp*)"" (lemma "floor_def" ("x" "(2 * x!1) / pi" ))"" (replace -2 * rl)"" (flatten)"" (hide -3)"" "div_mult_pos_le2" "x" "i!1" "py" "pi" "z" "2*x!1" ))"" "div_mult_pos_lt1" "x" "i!1+1" "py" "pi" "z" "2*x!1" ))"" (typepred "x!1" )"" (replace -6)"" (replace -5)"" (flatten)"" (expand "abs" )"" "both_sides_times_pos_lt1" "x" "x!1" "y" "2*pi" "pz" "2" ))"" (replace -3 -1)"" "" "div_mult_pos_le2" "z" "pi" "py" "2" "x" "2*pi-x!1" ))"" replace -1 4)"" "" "both_sides_plus_le1" "x" "(2*pi-x!1)*2" "y" "pi" "z" "2*x!1-pi" ))"" replace -1 4 rl)"" "" assert )"" case "i!1 < 0" )"1" (assert ) nil nil )"2" case "i!1 = 3" )"1" assert )nil nil )"2" case "i!1=4" )"1" assert )nil nil )"2" case "i!1>4" )"1" assert )"1" "div_mult_pos_le2" "x" "4" "z" "2*x!1" "py" "pi" ))"1" assert )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 sincos_phase 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 booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil floor_ceil nil )"nnreal" nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil real_props nil )"real" reals nil )nil real_props nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"[T, T -> boolean]" equalities nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"nzreal" nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )nil real_props nil )"int" integers nil )"posreal" nil )"nzreal" real_typesnil )"nat" floor_ceil nil )"nnreal" nil ))nil )nil 3264597671"" (skosimp*)"" (case "floor((2 * x!1) / pi) = 0" )"1" (replace -1) (("1" (assert ) nil nil )) nil )"2" (case "floor((2 * x!1) / pi) = 1" )"1" (replace -1) (("1" (assert ) nil nil )) nil )"2" (case "floor((2 * x!1) / pi) = 2" )"1" (assert )"1" (assert )"1" (rewrite "abs_neg" )"1" (assert ) nil nil )"2" (lemma "floor_def" ("x" "(2*x!1)/pi" ))"2" (flatten)"2" (replace -3)"2" "div_mult_pos_le2" "z" "2*x!1" "py" "pi" "x" "2" ))"2" (expand "abs" 1)"2" (assert )"2" "div_mult_pos_lt1" "z" "x!1" "py" "pi/2" "x" "3" ))"2" rewrite "div_div1" -1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (typepred "x!1" )"2" (case "floor((2 * x!1) / pi) = 3" )"1" (lemma "floor_def" ("x" "(2*x!1)/pi" ))"1" (flatten)"1" (replace -3)"1" "div_mult_pos_lt1" "z" "x!1" "py" "pi/2" "x" "4" ))"1" "div_mult_pos_le2" "z" "x!1" "py" "pi/2" "x" "3" ))"1" (rewrite "div_div1" )"1" (replace -4)"1" replace -3)"1" "1" rewrite "abs_neg" )"1" "sin_value(2 * pi - x!1)" )"1" (propax) nil nil )"2" expand "abs" 1)"2" (assert ) nil nil ))nil ))nil )"2" expand "abs" 1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 5)"2" (case "floor((2 * x!1) / pi) < 0" )"1" (lemma "floor_def" ("x" "(2*x!1)/pi" ))"1" (flatten) (("1" (assert ) nil nil )) nil ))nil )"2" (lemma "floor_def" ("x" "(2*x!1)/pi" ))"2" (flatten)"2" (case "floor((2 * x!1) / pi) = 4" )"1" (replace -1)"1" (rewrite "div_mult_pos_le2" ) nil nil ))nil )"2" (case "floor((2 * x!1) / pi) > 4" )"1" "div_mult_pos_le2" "x" "4" "z" "x!1" "py" "pi/2" ))"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" atan nil )nil asin nil )"[real_abs_le_pi2 -> real_abs_le1]" nil ))nil 3399981423"" (skosimp*)"" (case "floor((2 * x!1) / pi) = 0" )"1" (replace -1) (("1" (propax) nil nil )) nil )"2" (assert )"2" (case "floor((2 * x!1) / pi) = 1" )"1" (replace -1) (("1" (propax) nil nil )) nil )"2" (case "floor((2 * x!1) / pi) = 2" )"1" (assert ) nil nil )"2" (rewrite "abs_neg" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil sincos_phase nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_types nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil ) (<= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"nnreal" nil )"nat" floor_ceil nil )"posreal" nil )"(total_order?[real])" nil )"odd_int" integers nil )"real" reals nil )"real" reals nil )"nnreal" nil ))nil )nil 3399976753 ("" (subtype-tcc) nil nil ) nil nil ))nil 3264597671"" (skosimp*)"" (replace -2)"" (lemma "floor_def" ("x" "x!1/pi" ))"" (flatten)"" (replace -3 * rl)"" (rewrite "div_mult_pos_lt1" -2)"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"posreal" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"nnreal" nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"posint" nil )"nat" floor_ceil nil )"nnreal" nil )nil floor_ceil 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 )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil ))nil 3264597671"" (skosimp*)"" (case "i!1 = 1" )"1" (replace -1)"1" (lemma "floor_def" ("x" "x!1/pi" ))"1" (replace -3 * rl)"1" (flatten)"1" (rewrite "div_mult_pos_le2" )"1" "div_mult_pos_lt1" "z" "x!1" "py" "pi" "x" "2" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (case "i!1<0" )"1" (assert ) nil nil )"2" (case "i!1 = 2" )"1" (lemma "floor_def" ("x" "x!1/pi" ))"1" (replace -3 * rl)"1" (replace -2)"1" (flatten)"1" (rewrite "div_mult_pos_le2" -1) nil nil )) nil ))nil ))nil ))nil )"2" (case "i!1>2" )"1" (lemma "floor_def" ("x" "x!1/pi" ))"1" (replace -3 -1 rl)"1" (flatten)"1" (rewrite "div_mult_pos_le2" -1)"1" (rewrite "div_mult_pos_lt1" -2)"1" (assert )"1" "both_sides_times_pos_lt1" "x" "2" "y" "i!1" "pz" "pi" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )nil sincos_phase nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields 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 number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"nnreal" nil )nil floor_ceil nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"even_int" integersnil )"(total_order?[real])" nil )"real" reals nil )"(total_order?[real])" nil )nil real_props nil )"nat" floor_ceil nil )"posreal" nil )"int" integers nil )nil real_props nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil ))nil 3264623984"" (skosimp*)"" (lemma "floor_def" ("x" "(2 * x!1) / pi" ))"" (flatten)"" (name-replace "K1" "floor((2 * x!1) / pi)" )"" (lemma "trichotomy" ("x" "K1" ))"" (split -1)"1" (case "K1=1" )"1" (replace -1)"1" "div_mult_pos_le2" "x" "1" "z" "2*x!1" "py" "pi" ))"1" "div_mult_pos_lt1" "x" "2" "z" "2*x!1" "py" "pi" ))"1" (assert ) nil nil )) nil ))nil ))nil )"2" (case "K1>1" )"1" (assert )"1" (rewrite "div_mult_pos_le2" )"1" "both_sides_times_pos_lt1" "x" "1" "y" "K1" "pz" "pi" ))"1" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (replace -1)"2" (rewrite "div_mult_pos_le2" )"2" (rewrite "div_mult_pos_lt1" )"2" (assert ) nil nil )) nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sincos_phase 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 booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil floor_ceil nil )"nnreal" nil )"nat" floor_ceil nil )"[T, T -> boolean]" equalities nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"{i | i <= x & x < i + 1}" floor_ceil nil )nil real_props nil )"posint" nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"even_int" integersnil )"posreal" nil )"posreal" nil )nil real_props nil )"odd_int" integers nil )nil real_axioms nil )"nnreal" nil ))nil 3264624534"" (skosimp*)"" (lemma "floor_def" ("x" "(2 * x!1) / pi" ))"" (flatten)"" (name-replace "K1" "floor((2 * x!1) / pi)" )"" (lemma "trich_lt" ("x" "K1" "y" "1" ))"" (split -1)"1" (assert )"1" (flatten)"1" (rewrite "div_mult_pos_le2" )"1" (rewrite "div_mult_pos_lt1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (replace -1)"2" (rewrite "div_mult_pos_lt1" )"2" (rewrite "div_mult_pos_le2" )"2" (assert ) nil nil )) nil ))nil ))nil )"3" (assert )"3" (rewrite "div_mult_pos_le2" )"3" (rewrite "div_mult_pos_lt1" )"3" (assert )"3" (flatten)"3" "both_sides_times_pos_lt1" "x" "1" "y" "K1" "pz" "pi" ))"3" (assert )"3" (case "K1=2" )"1" replace -1)"1" (assert ) nil nil ))nil )"2" case "K1>2" )"1" "both_sides_times_pos_lt1" "x" "2" "y" "K1" "pz" "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 )"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 booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil floor_ceil nil )"nnreal" nil )"nat" floor_ceil nil )"[T, T -> boolean]" equalities nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"{i | i <= x & x < i + 1}" floor_ceil nil )nil real_props nil )"posint" nil )"posreal" nil )"posreal" nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil )"posreal" nil )"even_int" integersnil )nil real_props nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"nnreal" nil ))nil 3264675279"" (skosimp*)"" (lemma "floor_def" ("x" "(2*x!1)/pi" ))"" (flatten)"" (name-replace "K1" "floor((2 * x!1) / pi)" )"" (rewrite "div_mult_pos_le2" -1)"" "both_sides_times_pos_le1" "x" "pi" "y" "x!1" "pz" "2" ))"" (replace -1 1 rl)"" (rewrite "div_mult_pos_lt1" -3)"" (rewrite "div_mult_pos_lt2" 1)"" (lemma "trich_lt" ("x" "K1" "y" "2" ))"" (split -1)"1" "both_sides_times_pos_lt1" "x" "K1" "y" "2" "pz" "pi" ))"1" (assert ) nil nil )) nil )"2" (replace -1) (("2" (assert ) nil nil ))nil )"3" (case "3=K1" )"1" (replace -1 * rl)"1" (assert ) nil nil )) nil )"2" (case "3<K1" )"1" "both_sides_times_pos_lt1" "x" "K1" "y" "3" "pz" "pi" ))"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sincos_phase 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 booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil floor_ceil nil )"nnreal" nil )"nat" floor_ceil nil )"[T, T -> boolean]" equalities nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"posreal" nil )nil real_props nil )nil real_props nil )"posint" nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"posreal" nil )nil real_props nil )"posreal" nil )nil real_props nil )"(total_order?[real])" nil )nil real_props nil )"nnreal" nil ))nil 3264675711"" (skosimp*)"" (lemma "floor_def" ("x" "(2*x!1)/pi" ))"" (flatten)"" (name-replace "K1" "floor((2 * x!1) / pi)" )"" (lemma "trich_lt" ("x" "K1" "y" "3" ))"" (rewrite "div_mult_pos_le2" -2)"" (rewrite "div_mult_pos_lt1" -3)"" (rewrite "div_mult_pos_le1" 1)"" (split -1)"1" "both_sides_times_pos_lt1" "x" "K1" "y" "3" "pz" "pi" ))"1" (assert ) nil nil )) nil )"2" (replace -1) (("2" (assert ) nil nil )) nil )"3" (case "K1=4" )"1" (replace -1) (("1" (assert ) nil nil )) nil )"2" (case "K1>4" )"1" "both_sides_times_pos_lt1" "x" "K1" "y" "4" "pz" "pi" ))"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sincos_phase 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 booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil floor_ceil nil )"nnreal" nil )"nat" floor_ceil nil )"[T, T -> boolean]" equalities nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"posreal" nil )nil real_props nil )"(total_order?[real])" nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )nil real_props nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )nil real_props nil )nil real_props nil )"nnreal" nil ))nil 3264623778"" (skosimp*)"" (rewrite "phase_sin_q1" )"" (rewrite "phase_sin_q2" )"" (rewrite "phase_sin_q3" )"" (rewrite "phase_sin_q4" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sincos_phase nil )"posreal" nil )nil sincos_phase nil )nil sincos_phase nil )"nnreal" nil ))nil 3264686873"" (skosimp*)"" (rewrite "phase_sin_q1" )"" (expand "abs" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"nzreal" nil )"nzreal" real_typesnil )"nnreal" nil ))nil 3264683531"" (skosimp*)"" (expand "sin_phase" ) (("" (assert ) nil nil )) nil )) nil )"real_abs_le1" sincos_phase nil )"nat" floor_ceil nil )"nnreal" nil )"nnreal" nil ))nil 3264686873"" (skosimp*)"" (rewrite "phase_sin_q2" )"" (assert ) (("" (flatten) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" reals nil )"nnreal" nil ))nil 3264683552"" (skosimp*)"" (expand "sin_phase" )"" (assert )"" (rewrite "phase_sin_q2" )"" (flatten)"" (rewrite "sin_eqv_cos_value" 1)"1" (lemma "cos_value_neg" ("xc" "x!1-pi/2" ))"1" (replace -1 1) (("1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil )"2" (expand "abs" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" nil )"real_abs_le1" sincos_phase nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sincos_quad nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil asin nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )nil acos nil )nil sincos_quad nil )"nat" floor_ceil nil )"nnreal" nil )"real" reals nil )"nnreal" nil ))nil 3264686874"" (skosimp*)"" (rewrite "phase_sin_q3" )"" (flatten) (("" (expand "abs" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil )"posreal" nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"nzreal" real_typesnil )"nzreal" nil )"nnreal" nil ))nil 3264683931"" (skosimp*)"" (expand "sin_phase" ) (("" (assert ) nil nil )) nil )) nil )"real_abs_le1" sincos_phase nil )"nat" floor_ceil nil )"nnreal" nil )"real" reals nil )"real" reals nil )"nnreal" nil ))nil 3264686875"" (skosimp*)"" (rewrite "phase_sin_q4" ) (("" (assert ) nil nil )) nil )) nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"posreal" nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" reals nil )"nnreal" nil ))nil 3264683957"" (skosimp*)"" (expand "sin_phase" )"" (assert )"" (rewrite "phase_sin_q4" )"" (lemma "sin_eqv_cos_value" ("xs" "2*pi-x!1" ))"1" (replace -1 1)"1" (lemma "cos_value_neg" ("xc" "x!1-3*pi/2" ))"1" (replace -1 1) (("1" (propax) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil )"2" (expand "abs" 1) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"posreal" nil )"posreal" nil )"real_abs_le1" sincos_phase nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"(total_order?[real])" nil )nil acos nil )nil sincos_quad nil )"[numfield, numfield -> numfield]" number_fields nil )nil asin nil )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil sincos_quad nil )"nat" floor_ceil nil )"nnreal" nil )"real" reals nil )"real" reals nil )"nnreal" nil ))nil 3264616587"" (skosimp*)"" (lemma "floor_def" ("x" "x!1/pi" ))"" (flatten)"" (name-replace "K1" "floor(x!1/pi)" )"" (rewrite "div_mult_pos_le2" -1)"" (rewrite "div_mult_pos_lt1" -2)"" (lemma "trichotomy" ("x" "K1" ))"" (split -1)"1" (case "K1=1" )"1" (replace -1) (("1" (assert ) nil nil )) nil )"2" (case "K1>1" )"1" "both_sides_times_pos_lt1" "x" "1" "y" "K1" "pz" "pi" ))"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sincos_phase nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil floor_ceil nil )"nnreal" nil )"nat" floor_ceil nil )"[T, T -> boolean]" equalities nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"{i | i <= x & x < i + 1}" floor_ceil nil )nil real_props nil )"posint" nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )nil real_axioms nil )"(total_order?[real])" nil )"nnreal" nil )nil real_props nil ))nil 3264617408"" (skosimp*)"" (typepred "x!1" )"" (replace -2)"" (lemma "floor_def" ("x" "x!1/pi" ))"" (flatten)"" (name-replace "K1" "floor(x!1/pi)" )"" (rewrite "div_mult_pos_le2" -1)"" "div_mult_pos_lt1" "z" "x!1" "py" "pi" "x" "K1+1" ))"" (replace -3 -1)"" (flatten -1)"" (case "K1<1" )"1" (assert ) nil nil )"2" (case "K1=1" )"1" (replace -1) (("1" (assert ) nil nil ))nil )"2" (case "K1>1" )"1" (case "K1=2" )"1" replace -1)"1" (assert ) nil nil ))nil )"2" case "K1>2" )"1" "both_sides_times_pos_lt1" "x" "2" "y" "K1" "pz" "pi" ))"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sincos_phase 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 )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil floor_ceil nil )"nnreal" nil )"nat" floor_ceil nil )"[T, T -> boolean]" equalities nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"posint" nil )nil real_props nil )"even_int" integersnil )"posint" nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"(total_order?[real])" nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"nnreal" nil )nil real_props nil ))nil 3264616276"" (skosimp*)"" (rewrite "phase_cos_q1" )"" (rewrite "phase_cos_q2" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posreal" nil )nil sincos_phase nil ))nil 3264686878"" (skosimp*)"" (rewrite "phase_sin_q1" ) (("" (assert ) nil nil )) nil )) nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"nnreal" nil ))nil 3264684459"" (skosimp*)"" (expand "cos_phase" )"" (assert )"" (rewrite "phase_sin_q1" )"" (rewrite "phase_cos_q1" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"real_abs_le1" sincos_phase nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sincos_phase nil )"nat" floor_ceil nil )"nnreal" nil )"nnreal" nil ))nil 3264686878"" (skosimp*)"" (rewrite "phase_sin_q2" )"" (flatten) (("" (expand "abs" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"(total_order?[real])" nil )"real" reals nil )"nzreal" real_typesnil )"nzreal" nil )"nnreal" nil ))nil 3264684553"" (skosimp*)"" (expand "cos_phase" )"" (rewrite "phase_sin_q2" )"" (flatten)"" (rewrite "phase_cos_q1" )"" (assert )"" (lemma "sin_eqv_cos_value" ("xs" "x!1-pi/2" ))"1" (replace -1) (("1" (assert ) nil nil )) nil )"2" (expand "abs" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" nil )"real_abs_le1" sincos_phase nil )"real" reals nil )"real" reals nil )"real" reals nil )nil sincos_quad nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil asin nil )"[numfield, numfield -> numfield]" number_fields nil )nil sincos_phase nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil sincos_phase 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 )nil sincos_phase nil )"nnreal" nil ))nil 3264686878"" (skosimp*)"" (rewrite "phase_sin_q3" )"" (flatten) (("" (assert ) nil nil )) nil )) nil ))nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil )"posreal" nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"(total_order?[real])" nil )"nnreal" nil ))nil 3264685624"" (skosimp*)"" (rewrite "phase_sin_q3" -1)"" (flatten)"" (expand "cos_phase" )"" (lemma "phase_cos_q1" ("x" "x!1" ))"" (replace -1 1)"" (assert )"" (lemma "cos_value_neg" ("xc" "x!1-pi" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil )"posreal" nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real_abs_le1" sincos_phase nil )nil sincos_quad nil )"bool" reals nil )nil acos nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"nat" floor_ceil nil )"nnreal" nil )"real" reals nil )"real" reals nil )nil sincos_phase nil )"nnreal" nil ))nil 3264686878"" (skosimp*)"" (rewrite "phase_sin_q4" )"" (expand "abs" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"posreal" nil )"(total_order?[real])" nil )"nzreal" nil )"nzreal" real_typesnil )"real" reals nil )"nnreal" nil ))nil 3264685991"" (skosimp*)"" (expand "cos_phase" )"" (rewrite "phase_sin_q4" )"" (rewrite "phase_cos_q1" )"" (assert )"" (lemma "sin_value_neg" ("xs" "3*pi/2-x!1" ))"1" (replace -1)"1" (lemma "sin_eqv_cos_value" ("xs" "3*pi/2-x!1" ))"1" (assert ) nil nil )) nil ))nil )"2" (expand "abs" )"2" (assert )"2" (expand "<=" -1)"2" (split -1)"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" nil )"posreal" nil )"real_abs_le1" sincos_phase nil )nil sincos_phase nil )"[numfield, numfield -> numfield]" number_fields nil )nil asin nil )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil sincos_quad nil )"nzreal" nil )"nzreal" real_typesnil )nil sincos_quad nil )"real" reals nil )"real" reals nil )"posreal" nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil sincos_phase 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 )nil sincos_phase nil )"nnreal" nil ))nil 3264838737"" (skosimp*)"" (rewrite "phase_cos_q2" ) (("" (assert ) nil nil )) nil )) nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" reals nil ))nil 3264837795"" (skosimp*)"" (rewrite "phase_cos_q2" )"" (lemma "phases_sin" ("x" "x!1" ))"" (split -1)"1" (rewrite "phase_sin_q1" ) (("1" (assert ) nil nil )) nil )"2" (rewrite "phase_sin_q2" ) (("2" (assert ) nil nil )) nil )"3" (lemma "sin_q3" ("x" "x!1" ))"3" (assert )"3" (lemma "sin_q1" ("x" "x!1-pi" ))"3" (rewrite "phase_sin_q1" )"3" (rewrite "phase_sin_q3" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"4" (lemma "sin_q4" ("x" "x!1" ))"4" (assert )"4" (lemma "sin_q2" ("x" "x!1-pi" ))"4" (rewrite "phase_sin_q4" )"4" (rewrite "phase_sin_q2" )"4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posreal" nil )nil sincos_phase nil )"real" reals nil )"real" reals nil )nil sincos_phase nil )"nnreal" nil )"nat" floor_ceil nil )"real" reals nil )"odd_int" integers nil )nil sincos_phase nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )"nzreal" nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )"nnreal" nil ))nil 3264838765"" (skosimp*)"" (rewrite "phase_cos_q1" ) (("" (assert ) nil nil )) nil )) nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posreal" nil )"posreal" nil ))nil 3264838368"" (skosimp*)"" (lemma "sin_h2" ("x" "x!1+pi" ))"1" (rewrite "phase_cos_q1" )"1" (rewrite "phase_cos_q2" ) (("1" (assert ) nil nil )) nil ))nil )"2" (assert ) (("2" (rewrite "phase_cos_q1" ) nil nil )) nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )nil sincos_phase 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 )nil sincos_phase nil )"posreal" nil )"posreal" nil )nil sincos_phase nil )"posreal" nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil sincos_phase nil ))nil 3264838539"" (skosimp*)"" (expand "cos_phase" )"" (assert )"" (rewrite "phase_cos_q1" )"" (rewrite "phase_cos_q1" )"" (rewrite "cos_value_neg" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" nil )"real_abs_le1" sincos_phase nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil acos nil )"bool" reals nil )nil sincos_quad nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" nil )"nat" floor_ceil nil )"nnreal" nil )"real" reals nil )"posreal" nil ))nil 3264838643"" (skosimp*)"" (rewrite "phase_cos_q2" )"" (lemma "cos_h1" ("x" "x!1-pi" ))"1" (rewrite "phase_cos_q1" ) (("1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sincos_phase nil )"real" reals nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil sincos_phase nil )"real" reals nil ))nil 3264604314"" (skosimp*) (("" (typepred "px!1" ) (("" (assert ) nil nil )) nil ))nil )"posreal" atan nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"real" reals nil ))nil 3264603635"" (skosimp*)"" (typepred "px!1" )"" (hide -1)"" (expand "sin_phase" )"" (lemma "phases_sin" ("x" "px!1" ))"" (split -1)"1" (assert )"1" (lemma "phase_sin_q1" ("x" "px!1" ))"1" (replace -2)"1" (flatten -1)"1" (lemma "phase_sin_q4" ("x" "2*pi-px!1" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (lemma "floor_def" ("x" "(2 * px!1) / pi" ))"2" (replace -2)"2" (flatten -1)"2" (expand "<=" -1)"2" (split -1)"1" "phase_sin_q3" ("x" "2*pi-px!1" ))"1" (assert ) nil nil )) nil )"2" "both_sides_times1" "x" "1" "y" "(2 * px!1) / pi" "n0z" "pi/2" ))"2" (flatten -1)"2" replace -3 -2 rl)"2" "2" replace -1 * rl)"2" "minus_div2" "x" "4*pi" "y" "2*px!1" "n0x" "pi" ))"2" replace -1 * rl)"2" replace -2 * rl)"2" "div_cancel1" "x" "4" "n0z" "pi" ))"2" replace -1)"2" rewrite "floor_int" 1)"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert )"3" (lemma "floor_def" ("x" "(2 * px!1) / pi" ))"3" (flatten)"3" (replace -3)"3" (rewrite "div_mult_pos_le2" -1)"3" (rewrite "div_mult_pos_lt1" -2)"3" (expand "<=" -1)"3" (split -1)"1" "phase_sin_q2" "x" "2*pi-px!1" ))"1" (assert ) nil nil ))nil )"2" replace -1 * rl)"2" "2" "div_cancel1" "x" "2" "n0z" "pi" ))"2" replace -1)"2" rewrite "floor_int" 1)"2" assert )"2" "sin_value_neg" "xs" "px!1-pi" ))"1" replace -1 1)"1" (propax) nil nil ))nil )"2" "2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (assert )"4" (lemma "floor_def" ("x" "(2 * px!1) / pi" ))"4" (flatten)"4" (replace -3)"4" (rewrite "div_mult_pos_le2" -1)"4" "div_mult_pos_lt1" "z" "2*px!1" "py" "pi" "x" "4" ))"4" (replace -3 -1)"4" (flatten -1)"4" "phase_sin_q1" "x" "2*pi-px!1" ))"4" expand "<=" -3)"4" "1" (assert ) nil nil )"2" replace -1 * rl)"2" "2" rewrite "div_simp" 1)"2" rewrite "floor_int" 1)"2" "2" "both_sides_div1" "x" "3 * pi" "y" "2 * px!1" "n0z" "2" ))"2" "2" "div_cancel1" "x" "px!1" "n0z" "2" ))"2" replace -1)"2" replace "2" "2" replace "2" "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 ))nil )"posreal" atan nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 )"posreal" nil )"real" reals nil )"real_abs_le1" sincos_phase nil )nil sincos_phase nil )"real" reals nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil sincos_phase nil )"nat" floor_ceil nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil )nil floor_ceil nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"even_int" integersnil )"posint" nil )nil sincos_phase nil )nil real_props nil )"odd_int" integersnil )nil floor_ceil nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil real_props nil )nil reals nil )nil real_props nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"odd_int" integers nil )nil sincos_phase nil )nil asin nil )"[numfield -> numfield]" number_fields nil )nil sincos_quad nil )nil real_props nil )nil real_props nil )"odd_int" integers nil )nil real_props nil )nil sincos_phase nil )nil real_types nil )nil sincos_phase nil ))nil 3264622320"" (skosimp*)"" (expand "cos_phase" )"" (lemma "phases_cos" ("x" "px!1" ))"" (split -1)"1" (assert )"1" (lemma "phase_cos_q1" ("x" "px!1" ))"1" (replace -2 -1)"1" (flatten -1)"1" (typepred "px!1" )"1" (hide -1 -4)"1" (hide -2) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (lemma "phase_cos_q2" ("x" "px!1" ))"2" (assert )"2" (typepred "px!1" )"2" (assert )"2" (expand ">=" )"2" (expand "<=" -4)"2" (split -4)"1" "phase_cos_q1" ("x" "2*pi-px!1" ))"1" (assert ) nil nil )) nil )"2" (replace -1 * rl)"2" (simplify 1) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" nil )"real" reals nil )"real_abs_le1" sincos_phase nil )nil sincos_phase nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"nat" floor_ceil nil )"posreal" nil )"real" reals nil )nil sincos_phase nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil ))nil 3264605210"" (skosimp*) (("" (assert ) nil nil )) nil )"posreal" nil )"posreal" nil )"posreal" nil )"(strict_total_order?[real])" real_props nil ))nil 3264605272"" (skosimp*) (("" (typepred "x!1" ) (("" (assert ) nil nil )) nil ))nil )nil sincos_phase 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 )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"posreal" nil )"real" reals nil ))nil 3264610766"" (skosimp*)"" (expand "sin_phase" )"" (expand "cos_phase" )"" (lemma "phases_sin" ("x" "x!1" ))"" (split -1)"1" (replace -1)"1" (lemma "phase_sin_q1" ("x" "x!1" ))"1" (replace -2)"1" (flatten -1)"1" (lemma "phase_cos_q1" ("x" "pi/2+x!1" ))"1" (assert )"1" (rewrite "sin_eqv_cos_value" )"1" (expand "abs" 1)"1" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1 1)"2" (simplify 1)"2" (lemma "phase_sin_q2" ("x" "x!1" ))"2" (replace -2 -1)"2" (flatten -1)"2" (assert )"2" (lemma "phase_cos_q2" ("x" "pi/2+x!1" ))"2" (assert )"2" "sin_eqv_cos_value" "xs" "pi - x!1" ))"1" (assert ) nil nil )"2" expand "abs" 1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert )"3" (lemma "phase_sin_q3" ("x" "x!1" ))"3" (replace -2 -1)"3" (flatten -1)"3" (lemma "phase_cos_q2" ("x" "x!1+pi/2" ))"1" (assert )"1" (lemma "sin_value_neg" ("xs" "pi-x!1" ))"1" (replace -1 1)"1" (rewrite "sin_eqv_cos_value" 1)"1" (assert ) nil nil )) nil ))nil )"2" (expand "abs" 1)"2" (expand "<=" -2)"2" "1" (assert ) nil nil )"2" replace -1 * rl)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" (assert )"4" (lemma "phase_sin_q4" ("x" "x!1" ))"4" (replace -2 -1)"4" (flatten -1)"4" (assert )"4" (expand "<=" -1)"4" (split -1)"1" "sin_value_neg" ("xs" "2*pi-x!1" ))"1" (replace -1 1 rl)"1" "1" rewrite "sin_eqv_cos_value" 1)"1" "1" (assert ) nil nil ))nil )"2" expand "abs" 1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (expand "abs" 1)"2" (assert ) nil nil )) nil ))nil )"2" (replace -1 * rl)"2" (simplify 1)"2" rewrite "floor_int" 1)"2" rewrite "cos_value_0" )"2" rewrite "sin_value_pi2" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" nil )"posreal" nil )"posreal" nil )"real_abs_le1" sincos_phase nil )nil sincos_phase 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 )nil sincos_phase nil )"real" reals nil )nil sincos_quad nil )nil sincos_quad nil )nil floor_ceil nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"odd_int" integers nil )nil sincos_phase nil )"posreal" nil )nil sincos_quad nil )"nzreal" nil )"nzreal" real_typesnil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"nzreal" nil )nil sincos_phase nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )nil asin nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil sincos_quad nil )"(total_order?[real])" nil )"nat" floor_ceil nil )"nnreal" nil )"real" reals nil )nil sincos_phase nil )"real_abs_le1" sincos_phase nil )"real" reals nil )"posreal" nil ))nil 3264846233"" (skosimp*)"" (case "x!1 < 3 * pi / 2" )"1" (assert )"1" (lemma "sin_eqv_cos_phase" ("x" "pi/2+x!1" ))"1" (case "x!1<pi" )"1" (assert )"1" (lemma "div_cancel1" ("x" "pi" "n0z" "2" ))"1" (replace -1)"1" (replace -3 1)"1" (hide -1 -3 -4)"1" (expand "cos_phase" )"1" (rewrite "phase_cos_q1" )"1" (rewrite "phase_cos_q1" )"1" (lemma "cos_value_neg" ("xc" "x!1" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (case "pi / 2 - 3 * pi / 2 + x!1 = x!1-pi" )"1" (replace -1)"1" (replace -2)"1" (case "x!1>=pi" )"1" (hide -2 -3 1)"1" (expand "cos_phase" )"1" (rewrite "phase_cos_q1" )"1" (rewrite "phase_cos_q1" )"1" "cos_value_neg" ("xc" "x!1-pi" ))"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (lemma "sin_eqv_cos_phase" ("x" "x!1-3 * pi / 2" ))"2" (assert )"2" (replace -1 2)"2" (case "x!1>=3*pi/2" )"1" (case "pi / 2 - 3 * pi / 2 + x!1 = x!1-pi" )"1" (replace -1)"1" (hide -1 -3 1)"1" (expand "cos_phase" )"1" (rewrite "phase_cos_q1" )"1" (rewrite "phase_cos_q1" )"1" "cos_value_neg" ("xc" "x!1-pi" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil sincos_phase 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 )nil real_types nil )"bool" reals nil ) (< const-decl "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 )nil sincos_phase nil )"[numfield, numfield -> numfield]" number_fields nil )"odd_int" integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"real" reals nil )nil sincos_phase nil )"(total_order?[real])" nil )nil sincos_quad nil )"bool" reals nil )nil acos nil )"real" reals nil )"real_abs_le1" sincos_phase nil )nil reals nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"posreal" nil ))nil 3264852379"" (skosimp*) (("" (assert ) nil nil )) nil )"posreal" nil )"posreal" nil )"(strict_total_order?[real])" real_props nil ))nil 3264852379"" (skosimp*) (("" (assert ) nil nil )) nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3264852009"" (skosimp*)"" (rewrite "sin_eqv_cos_phase" )"" (case "x!1<pi" )"1" (assert )"1" (rewrite "cos_eqv_sin_phase" ) (("1" (assert ) nil nil ))nil ))nil )"2" (assert )"2" (case "x!1 < 3 * pi / 2" )"1" (assert )"1" (rewrite "cos_eqv_sin_phase" )"1" (assert ) nil nil )) nil ))nil )"2" (assert )"2" (rewrite "cos_eqv_sin_phase" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sincos_phase 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil sincos_phase nil )"odd_int" integers nil )"posreal" nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"real" reals nil )"posreal" nil )"posreal" nil )"real" reals nil )nil sincos_phase nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil ))nil 3264852196"" (skosimp*)"" (case "x!1<pi" )"1" (rewrite "cos_eqv_sin_phase" )"1" (assert )"1" (rewrite "sin_eqv_cos_phase" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (rewrite "cos_eqv_sin_phase" )"2" (case "x!1 < 3 * pi / 2" )"1" (assert )"1" (rewrite "sin_eqv_cos_phase" )"1" (assert ) nil nil )) nil ))nil )"2" (assert )"2" (rewrite "sin_eqv_cos_phase" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil sincos_phase 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 )nil real_types nil )"bool" reals nil ) (< const-decl "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 )"real" reals nil )"posreal" nil )nil sincos_phase nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"posreal" nil )"odd_int" integers nil )nil sincos_phase nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3264621137 ("" (assert ) nil nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"posreal" nil ))nil 3264621852"" (expand "sin_phase" )"" (lemma "div_cancel1" ("x" "3*pi" "n0z" "2" ))"" (replace -1)"" (lemma "div_cancel2" ("x" "3" "n0z" "pi" ))"" (replace -1)"" (rewrite "floor_int" 1)"" (assert ) (("" (rewrite "sin_value_pi2" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 )nil real_props nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil floor_ceil nil )nil sincos_quad nil )"real" reals nil )"real" reals nil )"odd_int" integers nil )"real_abs_le1" sincos_phase nil )"posreal" nil )"posreal" nil ))nil 3264603991"" (expand "sin_phase" )"" (rewrite "sin_value_0" )"" (lemma "floor_int" ("i" "0" ))"" (replace -1) (("" (propax) nil nil )) nil )) nil ))nil ))nil )nil sincos_quad nil )nil floor_ceil nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"real_abs_le1" sincos_phase nil ))nil 3264605320 ("" (assert ) nil nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"posreal" nil ))nil 3264620487"" (rewrite "sin_phase" )"" (rewrite "sin_value_pi4" )"" (lemma "div_cancel1" ("x" "2/4" "n0z" "pi" ))"" (replace -1 1)"" (lemma "floor_val" ("i" "2" "j" "4" "k" "0" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil sincos_quad nil )"odd_int" integers nil )"posrat" nil )"posreal" sqrt "reals/" )"odd_int" integers nil )"posint" nil )"even_int" integersnil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"(total_order?[real])" nil )nil integers nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil floor_ceil nil )nil reals nil )nil real_props nil )"nat" floor_ceil nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil sincos_phase 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 )"real_abs_le1" sincos_phase nil )"posreal" nil )"posreal" nil ))nil 3264605328 ("" (assert ) nil nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"posreal" nil ))nil 3264621187"" (expand "sin_phase" )"" (lemma "div_cancel1" ("x" "pi" "n0z" "2" ))"" (replace -1)"" (rewrite "div_simp" )"" (rewrite "floor_int" )"" (rewrite "sin_value_pi2" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" atan 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 )nil real_props nil )nil sincos_quad nil )nil floor_ceil nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"real_abs_le1" sincos_phase nil )"posreal" nil )"posreal" nil ))nil 3264621060"" (expand "cos_phase" )"" (rewrite "floor_int" )"1" (rewrite "cos_value_0" ) (("1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nnreal" nil )nil floor_ceil nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers 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 )"nat" floor_ceil nil )nil sincos_quad nil )"real_abs_le1" sincos_phase nil ))nil 3264621363"" (expand "cos_phase" )"" (rewrite "div_div2" 1)"" (lemma "div_cancel1" ("x" "1/4" "n0z" "pi" ))"" (replace -1 1)"" (lemma "floor_val" ("i" "1" "j" "4" "k" "0" ))"" (assert ) (("" (rewrite "cos_value_pi4" ) nil nil ))nil ))nil ))nil ))nil ))nil ))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 )"posreal" atan nil )"posreal" nil )"posreal" sqrt "reals/" )"nat" floor_ceil nil )"odd_int" integers nil )"posint" nil )"even_int" integersnil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"(total_order?[real])" nil )nil sincos_quad nil )nil integers nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil floor_ceil nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil real_props nil )"posrat" nil )"real_abs_le1" sincos_phase nil )"posreal" nil ))nil 3264621525"" (expand "cos_phase" )"" (rewrite "div_div2" )"" (lemma "floor_val" ("i" "1" "j" "2" "k" "0" ))"" (lemma "div_cancel1" ("x" "1/2" "n0z" "pi" ))"" (rewrite "div_div2" )"" (replace -1 1)"" (assert ) (("" (rewrite "cos_value_pi2" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 )"posreal" atan nil )"posreal" nil )"posrat" nil )nil real_props nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil sincos_quad nil )"(total_order?[real])" nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"even_int" integersnil )"nat" floor_ceil nil )"odd_int" integers nil )"posint" nil )nil integers nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil floor_ceil nil )"real_abs_le1" sincos_phase nil )"posreal" nil ))nil 3264605342 ("" (assert ) nil nil )"(strict_total_order?[real])" real_props nil )"posreal" nil ))nil 3264621665"" (expand "cos_phase" ) (("" (rewrite "cos_value_pi" ) nil nil ))nil )nil sincos_quad nil )"real_abs_le1" sincos_phase nil ))nil 3264625616"" (skosimp*)"" (typepred "xa!1" )"" (expand "abs" )"" (assert )"" (lemma "asin_strict_increasing" )"" (expand "strict_increasing?" )"" (inst-cp - "xa!1" "0" )"1" (rewrite "asin_0" )"1" (case "xa!1=-1" )"1" (replace -1)"1" (rewrite "asin_minus1" )"1" (assert ) nil nil )) nil ))nil )"2" (inst - "-1" "xa!1" )"1" (rewrite "asin_minus1" )"1" (assert ) nil nil )) nil )"2" (expand "abs" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (expand "abs" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil asin nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil asin nil )"[T, T -> boolean]" equalities nil )nil asin nil )"nzreal" nil )nil asin nil )"bool" real_fun_preds "reals/" )"(total_order?[real])" nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"posreal" nil )"nzreal" real_typesnil ))nil 3264628114"" (skosimp*)"" (lemma "asin_strict_increasing" )"" (expand "strict_increasing?" )"" (case "xa!1=0" )"1" (replace -1)"1" (rewrite "asin_0" )"1" (assert )"1" (typepred "pi" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (inst - "0" "xa!1" )"1" (rewrite "asin_0" )"1" (assert )"1" (typepred "asin(xa!1)" )"1" (expand "abs" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (expand "abs" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil asin 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 )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )nil asin nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"bool" real_fun_preds "reals/" ))nil 3264628447"" (skosimp*)"" (case "xa!1<0" )"1" (assert )"1" (expand "sin_phase" )"1" (typepred "asin(xa!1)" )"1" (lemma "asin_strict_increasing" )"1" (expand "strict_increasing?" )"1" (inst-cp - "xa!1" "0" )"1" (rewrite "asin_0" )"1" (assert )"1" "phase_sin_q4" ("x" "2*pi+asin(xa!1)" ))"1" (assert )"1" "sin_value_neg" ("xs" "asin(xa!1)" ))"1" (replace -1 1)"1" rewrite "sin_value_asin" 1)nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "sin_phase" )"2" (typepred "asin(xa!1)" )"2" (lemma "asin_strict_increasing" )"2" (expand "strict_increasing?" )"2" (case "xa!1=0" )"1" (replace -1)"1" (rewrite "asin_0" )"1" (rewrite "sin_value_0" )"1" (assert )"1" (rewrite "floor_int" 2)"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (inst-cp - "0" "xa!1" )"2" (inst - "xa!1" "1" )"2" (rewrite "asin_1" )"2" (rewrite "asin_0" )"2" (assert )"2" (expand "<=" -4)"2" "1" "phase_sin_q1" "x" "asin(xa!1)" ))"1" assert )"1" rewrite "sin_value_asin" )nil nil ))nil ))nil )"2" case "floor((2 * asin(xa!1)) / pi) = 1" )"1" assert )"1" "asin_1" )"1" "asin_bij" )"1" expand "bijective?" )"1" expand "injective?" )"1" "1" "xa!1" "1" )"1" assert )"1" replace -5)"1" rewrite "sin_value_pi2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -1 1)"2" "div_cancel1" "x" "pi" "n0z" "2" ))"2" replace -1)"2" rewrite "div_simp" 1)"2" rewrite "floor_int" 1)nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil asin nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans 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_abs_le1" sincos_phase nil )nil asin nil )"real" reals nil )"posreal" nil )"nzreal" nil )"(total_order?[real])" nil )"real" reals nil )nil sincos_quad nil )nil sincos_quad nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil sincos_phase nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil sincos_phase nil )nil asin nil )"bool" real_fun_preds "reals/" )NOT const-decl "[bool -> bool]" booleans 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" asin nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"posreal" nil )"nzreal" real_typesnil )"[T, T -> boolean]" equalities nil )"odd_int" integers nil )"nnreal" nil )"nat" floor_ceil nil )nil floor_ceil nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil sincos_quad nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"bool" functions nil )nil sincos_quad nil )"bool" functions nil )nil asin nil )"real" reals nil )nil real_props nil )nil reals nil )nil real_props nil )nil sincos_phase nil )nil asin nil ))nil 3264625616"" (skosimp*)"" (typepred "acos(xa!1)" ) (("" (assert ) nil nil )) nil )) nil )"nnreal_le_pi" acos nil )nil acos nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_types nil )nil asin nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans 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 )"(strict_total_order?[real])" real_props nil )"posreal" nil ))nil 3264677087"" (skosimp*)"" (typepred "xa!1" )"" (typepred "acos(xa!1)" )"" (expand "cos_phase" )"" (rewrite "phase_cos_q1" 1)"" (expand ">=" )"" (replace -1)"" (expand "<=" -2)"" (split)"1" (assert )"1" (rewrite "cos_value_acos" ) nil nil )) nil )"2" (replace -1)"2" (assert )"2" (rewrite "cos_value_pi" )"2" (lemma "acos_bij" )"2" (expand "bijective?" )"2" expand "injective?" )"2" "2" "-1" "xa!1" )"1" rewrite "acos_minus1" )"1" (assert ) nil nil ))nil )"2" expand "abs" 1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil asin nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"real_abs_le1" sincos_phase nil )nil sincos_quad nil )"bool" functions nil )nil acos nil )"bool" functions nil )nil acos nil )"real" reals nil )"odd_int" integers nil )nil sincos_quad nil )"(total_order?[real])" nil )nil sincos_phase nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil sincos_phase nil )"(strict_total_order?[real])" real_props nil )"posreal" 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 )"nnreal_le_pi" acos nil ))nil 3264625668"" (skosimp*)"" (expand "sin_phase" )"" (expand "cos_phase" )"" (lemma "phases_sin" ("x" "x!1" ))"" (split -1)"1" (lemma "phase_sin_q1" ("x" "x!1" ))"1" (replace -2)"1" (flatten -1)"1" (lemma "phase_cos_q1" ("x" "x!1" ))"1" (assert )"1" (lemma "sin2_cos2_value" ("q1" "x!1" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "phase_sin_q2" ("x" "x!1" ))"2" (replace -2)"2" (flatten -1)"2" (lemma "phase_cos_q1" ("x" "x!1" ))"2" (assert )"2" (lemma "sin2_cos2_value" ("q1" "pi-x!1" ))"2" (rewrite "cos_value_neg" -1)"2" (rewrite "sq_neg" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "phase_sin_q3" ("x" "x!1" ))"3" (replace -2)"3" (flatten -1)"3" (lemma "phase_cos_q2" ("x" "x!1" ))"3" (assert )"3" (lemma "sin2_cos2_value" ("q1" "x!1-pi" ))"3" (lemma "cos_value_neg" ("xc" "x!1-pi" ))"3" (replace -1 1)"3" (rewrite "sq_neg" 1)"3" assert )"3" rewrite "sq_neg" 1)"3" expand "abs" 1)"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (lemma "phase_sin_q4" ("x" "x!1" ))"4" (replace -2)"4" (flatten -1)"4" (lemma "phase_cos_q2" ("x" "x!1" ))"4" (assert )"4" (lemma "sin2_cos2_value" ("q1" "2*pi-x!1" ))"4" (assert )"4" (rewrite "sq_neg" 1)"4" (expand "abs" 1)"4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" nil )"real_abs_le1" sincos_phase nil )nil sincos_phase 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 )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )"[real_abs_le_pi2 -> real_abs_le1]" nil )nil asin nil )nil sincos_phase nil )nil sincos_phase nil )"real" reals nil )nil acos nil )nil sincos_quad nil )"real" reals nil )nil sq "reals/" )"[numfield -> numfield]" number_fields nil )nil asin nil )"[nnreal_le_pi -> real_abs_le1]" sincos_quadnil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil sincos_phase nil )"nnreal" nil )"nnreal" nil )"nat" floor_ceil nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sincos_quad nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"bool" reals nil )nil sincos_quad nil )nil sincos_phase nil )"posreal" nil )"real_abs_le1" sincos_phase nil ))nil 3264625616"" (skosimp*)"" (typepred "x!1" )"" (typepred "y!1" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil sincos_phase 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 )"real" reals nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil 3264628358"" (skosimp*)"" (typepred "x!1" )"" (typepred "y!1" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil sincos_phase 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 )"real" reals nil )"real" reals nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil 3264836972"" case "FORALL (x,y:{x:nnreal|x<pi}): sin_phase(x) * cos_phase(y) - cos_phase(x) * sin_phase(y) = IF x - y < 0 THEN sin_phase(x - y + 2 * pi)") "1" (skosimp*)"1" (lemma "phases_cos" ("x" "x!1" ))"1" (lemma "phases_cos" ("x" "y!1" ))"1" (split -1)"1" (split -2)"1" (inst - "x!1" "y!1" )"1" (rewrite "phase_cos_q1" -2)"1" (case "x!1 - y!1 < 0" )"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil )"2" (rewrite "phase_cos_q1" -1)"2" (rewrite "phase_cos_q1" -2) nil nil )) nil )"3" (rewrite "phase_cos_q1" -1) nil nil ))nil )"2" (inst - "x!1-pi" "y!1" )"1" (lemma "cos_h2" ("x" "x!1" ))"1" (lemma "sin_h2" ("x" "x!1" ))"1" (assert )"1" (replace -1 1)"1" (replace -2 1)"1" (case "x!1<y!1" )"1" (assert )"1" "sin_h1" ("x" "pi - y!1 + x!1" ))"1" rewrite "phase_cos_q1" )"1" rewrite "phase_cos_q1" )"1" rewrite "phase_cos_q2" )"1" (assert ) nil nil ))nil ))nil )"2" rewrite "phase_cos_q2" )nil nil ))nil )"2" rewrite "phase_cos_q2" )"2" rewrite "phase_cos_q1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert )"2" case "x!1-y!1<pi" )"1" assert )"1" "phase_cos_q1" "x" "x!1-y!1" ))"1" replace -2 -1)"1" case "0 <= x!1-y!1" )"1" replace -1 -2)"1" "1" "sin_h1" "x" "x!1-y!1" ))"1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "phase_cos_q2" "x" "x!1-y!1" ))"2" assert )"2" "sin_h2" "x" "x!1-y!1" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "phase_cos_q1" -2) nil nil )"3" (rewrite "phase_cos_q2" -1)"3" (assert ) nil nil )) nil ))nil ))nil )"2" (split -2)"1" (inst - "x!1" "y!1-pi" )"1" (lemma "sin_h2" ("x" "y!1" ))"1" (lemma "cos_h1" ("x" "x!1" ))"1" (assert )"1" (replace -1)"1" (replace -2)"1" (hide -1 -2)"1" (rewrite "phase_cos_q1" -1)"1" rewrite "phase_cos_q2" -2)"1" assert )"1" "cos_h2" ("x" "y!1" ))"1" rewrite "phase_cos_q2" -1)"1" replace -1)"1" "1" case "pi - y!1 + x!1 < 0" )"1" assert )"1" "sin_h2" "x" "3 * pi - y!1 + x!1" ))"1" rewrite "phase_cos_q2" "1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "sin_h1" "x" "pi - y!1 + x!1" ))"2" rewrite "phase_cos_q1" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "phase_cos_q2" -2)"2" (assert ) nil nil )) nil )"3" (rewrite "phase_cos_q1" -1) nil nil ))nil )"2" (inst - "x!1-pi" "y!1-pi" )"1" (lemma "sin_h2" ("x" "x!1" ))"1" (lemma "cos_h2" ("x" "x!1" ))"1" (lemma "cos_h2" ("x" "y!1" ))"1" (lemma "sin_h2" ("x" "y!1" ))"1" (assert )"1" (replace -1)"1" (replace -2)"1" replace -3)"1" replace -4)"1" "1" case "x!1<y!1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "phase_cos_q2" -2)"2" (assert ) nil nil )) nil )"3" (rewrite "phase_cos_q2" -1)"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (typepred "x!1" )"2" (typepred "y!1" )"2" (expand "cos_phase" )"2" (rewrite "phase_cos_q1" )"2" (rewrite "phase_cos_q1" )"2" (lemma "phases_sin" ("x" "x!1" ))"2" (split -1)"1" (lemma "sin_q1" ("x" "x!1" ))"1" (assert )"1" (replace -1)"1" (lemma "phases_sin" ("x" "y!1" ))"1" "1" "sin_q1" ("x" "y!1" ))"1" assert )"1" replace -1)"1" "sin_value_diff" "q1" "x!1" "q2" "y!1" ))"1" replace -1 1 rl)"1" case "x!1-y!1<0" )"1" assert )"1" "phase_sin_q4" "x" "2 * pi - y!1 + x!1" ))"1" rewrite "phase_sin_q1" "1" rewrite "phase_sin_q1" "1" assert )"1" "sin_q4" "x" "2 * pi - y!1 + x!1" ))"1" assert )"1" replace "1" replace "1" "sin_phase_neg" "px" "y!1-x!1" ))"1" replace "1" "sin_value_neg" "xs" "y!1-x!1" ))"1" replace "1" "sin_q1" "x" "y!1-x!1" ))"1" rewrite "phase_sin_q1" "1" assert )nil nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "sin_q1" "x" "x!1-y!1" ))"2" rewrite "phase_sin_q1" "2" assert )"2" rewrite "phase_sin_q1" "2" rewrite "phase_sin_q1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "phase_sin_q1" -2)"2" (assert ) nil nil ))nil )"3" rewrite "phase_sin_q1" -4)"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "x!1<pi/2" )"1" case "pi/2<=y!1" )"1" "1" "sin_q2" ("x" "y!1" ))"1" assert )"1" replace -1 1)"1" "1" "sin_phase_neg" "px" "y!1-x!1" ))"1" replace -1 1)"1" "1" case "y!1-x!1<pi/2" )"1" "sin_q1" "x" "y!1-x!1" ))"1" rewrite "phase_sin_q1" "1" assert )"1" replace "1" "1" case "cos_value(y!1) = -sin_value(y!1 - pi / 2)" )"1" replace "1" "1" "cos_value_diff" "q1" "x!1" "q2" "y!1-pi/2" ))"1" assert )"1" "sin_eqv_cos_quad" "q1" "y!1-x!1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "cos_value_neg" "xc" "y!1" ))"2" "cos_eqv_sin_quad" "q1" "pi-y!1" ))"2" assert )nil nil ))nil ))nil ))nil )"3" expand "abs" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "sin_q2" "x" "y!1-x!1" ))"2" rewrite "phase_sin_q2" "2" assert )"2" replace "2" "2" case "cos_value(y!1) = -sin_value(y!1 - pi / 2)" )"1" replace "1" "cos_value_diff" "q1" "x!1" "q2" "y!1-pi/2" ))"1" assert )"1" case "pi / 2 - y!1 + x!1 < 0" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "cos_value_neg" "xc" "y!1" ))"2" "cos_eqv_sin_quad" "q1" "pi-y!1" ))"2" assert )nil nil ))nil ))nil ))nil )"3" expand "abs" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "phase_sin_q2" -2)nil nil ))nil )"2" rewrite "phase_sin_q1" -2)nil nil ))nil ))nil )"3" rewrite "phase_sin_q3" -1)nil nil )"4" rewrite "phase_sin_q4" -1)nil nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "sin_q2" ("x" "x!1" ))"2" (assert )"2" (replace -1 1)"2" (case "pi/2<= x!1" )"1" "1" "phases_sin" ("x" "y!1" ))"1" "1" case "y!1<pi/2" )"1" "1" assert )"1" case "cos_value(x!1) = -sin_value(x!1 - pi / 2)" )"1" replace -1)"1" "1" "sin_q1" "x" "y!1" ))"1" assert )"1" replace -1)"1" "1" "cos_value_diff" "q1" "x!1-pi/2" "q2" "y!1" ))"1" case "x!1 - pi / 2 - y!1 < 0" )"1" assert )"1" replace "1" "1" "sin_q1" "x" "x!1-y!1" ))"1" rewrite "phase_sin_q1" "1" rewrite "sin_eqv_cos_quad" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" replace "2" "2" "sin_q2" "x" "x!1-y!1" ))"2" rewrite "phase_sin_q2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "cos_value_neg" "xc" "x!1" ))"2" "cos_eqv_sin_quad" "q1" "pi-x!1" ))"2" assert )nil nil ))nil ))nil ))nil )"3" expand "abs" 1)"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" rewrite "phase_sin_q1" -1)nil nil ))nil )"2" case "pi/2<= y!1" )"1" "1" "sin_q2" ("x" "y!1" ))"1" assert )"1" replace -1 1)"1" "1" case "FORALL (x:real): pi/2<=x & x < pi => cos_value(x) = -sin_value(x-pi/2)" )"1" "x!1" )"1" "y!1" )"1" assert )"1" replace -1)"1" replace "1" "sin_value_diff" "q1" "x!1-pi/2" "q2" "y!1-pi/2" ))"1" case "x!1<y!1" )"1" "sin_phase_neg" "px" "y!1-x!1" ))"1" assert )"1" replace "1" "sin_q1" "x" "y!1-x!1" ))"1" rewrite "phase_sin_q1" "1" "sin_value_neg" "xs" "y!1-x!1" ))"1" assert )nil nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )"2" "sin_q1" "x" "x!1-y!1" ))"2" rewrite "phase_sin_q1" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "cos_value_neg" "xc" "x!2" ))"1" "cos_eqv_sin_quad" "q1" "pi-x!2" ))"1" assert )nil nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"3" "3" expand "abs" 1)"3" assert )nil nil ))nil ))nil )"4" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "phase_sin_q2" -1)nil nil ))nil )"3" rewrite "phase_sin_q3" -1)nil nil )"4" rewrite "phase_sin_q4" -1)nil nil ))nil ))nil ))nil )"2" rewrite "phase_sin_q2" -2)nil nil ))nil ))nil ))nil ))nil )"3" (rewrite "phase_sin_q3" -1) nil nil )"4" (rewrite "phase_sin_q4" -1) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2) (("3" (skosimp*) (("3" (assert ) nil nil )) nil )) nil )"4" (hide 2) (("4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_quad nil )nil sincos_quad nil )nil sincos_quad nil )nil sincos_quad nil )"[real_abs_le_pi2 -> real_abs_le1]" nil )"[nnreal_le_pi -> real_abs_le1]" sincos_quadnil )nil acos nil )nil sincos_phase nil )"nzreal" real_typesnil )"nzreal" nil )nil asin nil )nil sincos_quad nil )"(strict_total_order?[real])" real_props nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )"posreal" nil )nil sincos_quad nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil sincos_quad nil )nil sincos_phase nil )nil sincos_phase nil )"nnreal" nil )"posreal" nil )nil sincos_phase nil )nil sincos_phase nil )"real" reals nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"nnreal" nil )"nat" floor_ceil nil )"trig_phase" sincos_phase nil )"trig_phase" sincos_phase nil )"(strict_total_order?[real])" real_props nil )nil sincos_phase nil )"nzreal" nil )"real" reals nil )"real" reals nil )nil sincos_phase nil )nil sincos_phase nil )"odd_int" integers nil )nil sincos_phase nil )nil sincos_phase nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"posreal" nil )"real" reals nil )"real" reals 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" reals nil )nil real_types nil )"posreal" atan nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil sincos_phase nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )nil asin nil )"real_abs_le1" sincos_phase nil )"real_abs_le1" sincos_phase nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3264625616"" (skosimp*)"" (typepred "x!1" )"" (typepred "y!1" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil sincos_phase 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 )"real" reals nil )"nnreal" nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil 3264629773"" case "FORALL (x,y:{x:nnreal|x<pi}): cos_phase(x) * cos_phase(y) - sin_phase(x) * sin_phase(y) = cos_phase(x + y)" )"1" (skosimp*)"1" (lemma "phases_cos" ("x" "x!1" ))"1" (lemma "phases_cos" ("x" "y!1" ))"1" (split -2)"1" (split -2)"1" (case "x!1<pi" )"1" (case "y!1<pi" )"1" (inst - "x!1" "y!1" ) (("1" (assert ) nil nil ))nil )"2" (rewrite "phase_cos_q1" -2) nil nil ))nil )"2" (rewrite "phase_cos_q1" -2) nil nil ))nil )"2" (case "pi<=y!1" )"1" (case "x!1<pi" )"1" (inst - "x!1" "y!1-pi" )"1" case "cos_phase(y!1 - pi) = -cos_phase(y!1)" )"1" case "sin_phase(y!1 - pi) = -sin_phase(y!1)" )"1" (replace -1)"1" (replace -2)"1" (hide -1 -2)"1" case "x!1+y!1<2*pi" )"1" assert )"1" case "cos_phase(x!1 + y!1)=-cos_phase(x!1 - pi + y!1)" )"1" (assert ) nil nil )"2" "2" rewrite "cos_phase_inv" 1)nil nil ))nil ))nil ))nil )"2" assert )"2" "cos_phase_inv" "x" "x!1 - pi + y!1" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (rewrite "sin_phase_inv" 1) nil nil ))nil )"3" (assert ) nil nil ))nil )"2" (hide 2)"2" (rewrite "cos_phase_inv" 1) nil nil ))nil )"3" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil )"2" (rewrite "phase_cos_q1" -3) nil nil ))nil )"2" (rewrite "phase_cos_q2" -1) nil nil ))nil ))nil )"2" (case "pi<=x!1" )"1" (split -3)"1" (case "y!1< pi" )"1" (case "x!1 + y!1 < 2 * pi" )"1" (assert )"1" (inst - "x!1-pi" "y!1" )"1" (lemma "cos_phase_inv" ("x" "x!1-pi" ))"1" (lemma "sin_phase_inv" ("x" "x!1-pi" ))"1" "cos_phase_inv" ("x" "x!1+y!1" ))"1" assert )"1" replace -2)"1" replace -3)"1" replace -1)"1" replace -9 1 rl)"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst - "x!1-pi" "y!1" )"1" (lemma "cos_phase_inv" ("x" "x!1-pi" ))"1" (lemma "sin_phase_inv" ("x" "x!1-pi" ))"1" "cos_phase_inv" ("x" "x!1+y!1-pi" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (rewrite "phase_cos_q1" -1) nil nil ))nil )"2" (case "pi<=y!1" )"1" (inst - "x!1-pi" "y!1-pi" )"1" (assert )"1" (lemma "sin_phase_inv" ("x" "x!1" ))"1" (lemma "cos_phase_inv" ("x" "x!1" ))"1" (lemma "sin_phase_inv" ("x" "y!1" ))"1" (lemma "cos_phase_inv" ("x" "y!1" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil )"2" (rewrite "phase_cos_q2" -1) nil nil ))nil ))nil )"2" (rewrite "phase_cos_q2" -1) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (lemma "phases_sin" ("x" "x!1" ))"2" (split -1)"1" (case "x!1<pi/2" )"1" (lemma "phases_sin" ("x" "y!1" ))"1" (split -1)"1" (case "y!1<pi/2" )"1" (lemma "sin_q1" ("x" "x!1" ))"1" (lemma "sin_q1" ("x" "y!1" ))"1" (lemma "cos_q1" ("x" "x!1" ))"1" (lemma "cos_q1" ("x" "y!1" ))"1" (assert )"1" replace -1)"1" replace -2)"1" replace -3)"1" replace -4)"1" "1" "cos_value_sum" "q1" "x!1" "q2" "y!1" ))"1" replace -1 1 rl)"1" "1" expand "cos_phase" 1)"1" rewrite "phase_cos_q1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "phase_sin_q1" -1) nil nil ))nil )"2" (case "pi/2<= y!1" )"1" (lemma "sin_q1" ("x" "x!1" ))"1" (lemma "cos_q1" ("x" "x!1" ))"1" (lemma "sin_q2" ("x" "y!1" ))"1" (lemma "cos_q2" ("x" "y!1" ))"1" (assert )"1" replace -1)"1" replace -2)"1" replace -3)"1" replace -4)"1" "1" "sin_value_sum" "q1" "x!1" "q2" "y!1-pi/2" ))"1" expand "cos_phase" 1)"1" rewrite "phase_cos_q1" "1" "trich_lt" "x" "x!1+y!1" "y" "pi" ))"1" "1" assert )"1" "sin_eqv_cos_value" "xs" "x!1 - pi / 2 + y!1" ))"1" assert )nil nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil )"2" replace -1)"2" assert )"2" "sin_value_pi2" )"2" case "x!1=pi-y!1" )"1" replace "1" "1" rewrite "cos_value_pi" )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" assert )"3" "cos_value_neg" "xc" "x!1+y!1-pi" ))"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "phase_sin_q2" -1) nil nil ))nil )"3" (rewrite "phase_sin_q3" -1) nil nil )"4" (rewrite "phase_sin_q4" -1) nil nil ))nil ))nil )"2" (rewrite "phase_sin_q1" -1) nil nil ))nil )"2" (case "pi/2<=x!1" )"1" (lemma "phases_sin" ("x" "y!1" ))"1" (split -1)"1" (case "y!1<pi/2" )"1" (lemma "sin_q2" ("x" "x!1" ))"1" (lemma "cos_q2" ("x" "x!1" ))"1" (lemma "sin_q1" ("x" "y!1" ))"1" (lemma "cos_q1" ("x" "y!1" ))"1" (assert )"1" "cos_q2" ("x" "x!1+y!1" ))"1" "cos_q3" ("x" "x!1+y!1" ))"1" replace -3)"1" replace -4)"1" replace -5)"1" replace -6)"1" rewrite "phase_sin_q2" -2)"1" rewrite "phase_sin_q3" "1" case "x!1+y!1<pi" )"1" assert )"1" "1" "sin_value_sum" "q1" "x!1-pi/2" "q2" "y!1" ))"1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "2" "sin_value_sum" "q1" "x!1-pi/2" "q2" "y!1" ))"2" assert )"2" case "x!1=pi-y!1" )"1" replace "1" assert )"1" rewrite "sin_value_pi2" "1" rewrite "cos_value_0" )"1" 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 )"2" (rewrite "phase_sin_q1" -1) nil nil ))nil )"2" (case "pi/2<=y!1" )"1" "cos_value_sum" "q1" "x!1-pi/2" "q2" "y!1-pi/2" ))"1" (simplify -1)"1" "div_cancel1" ("x" "pi" "n0z" "2" ))"1" (replace -1)"1" (hide -1)"1" "sin_q2" ("x" "x!1" ))"1" "cos_q2" ("x" "x!1" ))"1" "sin_q2" ("x" "y!1" ))"1" "cos_q2" ("x" "y!1" ))"1" assert )"1" replace -1)"1" replace -2)"1" replace -3)"1" replace -4)"1" rewrite "cos_phase_inv" "1" "1" expand "cos_phase" "1" rewrite "phase_cos_q1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil )"2" (rewrite "phase_sin_q2" -1) nil nil ))nil )"3" (rewrite "phase_sin_q3" -1) nil nil )"4" (rewrite "phase_sin_q4" -1) nil nil ))nil ))nil )"2" (rewrite "phase_sin_q2" -1) nil nil ))nil )"3" (rewrite "phase_sin_q3" -1) nil nil )"4" (rewrite "phase_sin_q4" -1) nil nil ))nil ))nil ))nil ))nil ))nil )"nnreal" nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_quad nil )nil real_props nil )nil reals nil )"posreal" nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_quad nil )nil sincos_quad nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_quad nil )nil sincos_quad nil )nil asin nil )"real" reals nil )nil sincos_quad nil )nil sincos_quad nil )"nzreal" nil )nil sincos_quad nil )nil acos nil )nil real_props nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )"posreal" nil )"real" reals nil )"nnreal" nil )"nat" floor_ceil nil )"trig_phase" sincos_phase nil )"trig_phase" sincos_phase nil )"(strict_total_order?[real])" real_props nil )nil sincos_phase nil )"(total_order?[real])" nil )nil sincos_phase nil )"real" reals nil )nil sincos_phase nil )"odd_int" integers nil )"real" reals nil )nil sincos_phase nil )"even_int" integers nil )"nzint" integers nil )"(total_order?[real])" nil )nil sincos_phase nil )"real" reals nil )"nnreal" 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" reals nil )nil real_types nil )"posreal" atan nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil sincos_phase nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )nil asin nil )"real_abs_le1" sincos_phase nil )"real_abs_le1" sincos_phase nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3264848363"" (skosimp*)"" (case "y!1=0" )"1" (replace -1)"1" (rewrite "cos_phase_0" )"1" (rewrite "sin_phase_0" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (lemma "cos_phase_sum" ("x" "x!1" "y" "2*pi-y!1" ))"1" (lemma "sin_phase_neg" ("px" "y!1" ))"1" (lemma "cos_phase_neg" ("px" "y!1" ))"1" (replace -1)"1" (replace -2)"1" (hide -1 -2)"1" (replace -1 2)"1" (case "x!1 - y!1 >= 0" )"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )nil sincos_phase 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 )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )nil sincos_phase nil )"(total_order?[real])" nil )"real" reals nil )nil sincos_phase nil )"posreal" nil )"real" reals nil )"real" reals nil )nil sincos_phase nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"nzint" integers nil )"even_int" integers nil )"real" reals nil )nil sincos_phase nil )"(strict_total_order?[real])" real_props nil )nil sincos_phase nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3264847615"" (skosimp*)"" (lemma "sin_phase_diff" ("x" "x!1" "y" "2*pi-y!1" ))"1" (case "x!1 + y!1 < 2 * pi" )"1" (assert )"1" (case "y!1=0" )"1" (replace -1)"1" (rewrite "sin_phase_0" )"1" (rewrite "cos_phase_0" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (lemma "sin_phase_neg" ("px" "y!1" ))"1" (lemma "cos_phase_neg" ("px" "y!1" ))"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil )"2" (typepred "y!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (assert )"2" (lemma "sin_phase_neg" ("px" "y!1" ))"2" (lemma "cos_phase_neg" ("px" "y!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (case "y!1=0" )"1" (replace -1)"1" (rewrite "cos_phase_0" )"1" (rewrite "sin_phase_0" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )nil sincos_phase 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 )nil sincos_phase nil )"real" reals nil )"(total_order?[real])" nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" reals nil )"real" reals nil )nil sincos_phase nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil sincos_phase nil )NOT const-decl "[bool -> bool]" booleans nil )nil sincos_phase nil )nil sincos_phase nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"nnreal" nil )"nzint" integers nil )"even_int" integers 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.324Bemerkung:
(vorverarbeitet am 2026-04-27)
¤ *Bot Zugriff
2026-05-26
