(interval_trignil 3554219250"" (expand "cos_term" )"" (case "FORALL (kk:nat): even?(kk) IMPLIES (-1)^kk = 1" )"1" (skeep)"1" (inst-cp - "2+2*n" )"1" (hide -1)"1" (split -)"1" (replaces -1)"1" (assert )"1" (expand "abs" )"1" (case "pi_lbn(n)^(4+4*n) < 3.2^(4+4*n)" )"1" (mult-by -1 "1/factorial(4+4*n)" )"1" (assert ) nil nil )) nil )"2" (hide 2)"2" (lemma "both_sides_expt_pos_lt_aux" )"2" (inst - "3+4*n" "pi_lbn(n)" "3.2" )"2" (assert )"2" expand "^" )"2" assert )"2" "2" "pi_bounds" )"2" "n" )"2" "3" )"2" "pi_ubn(3)" )"2" assert )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "even?" )"2" (inst + "1+n" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (expand "even?" )"2" (skosimp*)"2" (replace -1)"2" (lemma "expt_times" )"2" (inst?)"2" (case "(-1)^2 = 1" )"1" (replaces -1)"1" (replaces -1)"1" (case "FORALL (jjj:nat): 1^jjj = 1" )"1" (inst?) (("1" (assert ) nil nil )) nil )"2" (induct "jjj" )"1" "1" (grind) nil nil ))nil )"2" "2" expand "^" )"2" expand "expt" 1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"bool" integers nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals 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 )nil booleans nil )nil numbers nil )"odd_int" integers nil )"even_int" integersnil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posrat" nil )"posreal" atan_approx "trig_fnd/" )"{y: posreal | y >= x}" nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"real" atan_approx "trig_fnd/" )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"posrat" nil )"posnat" factorial "ints/" )nil integers nil )nil integers nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_props nil )nil exponentiation nil )"posrat" exponentiation nil )"even_int" integersnil )"posreal" exponentiation nil )"nzreal" exponentiation nil )nil atan_approx "trig_fnd/" )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"real" atan_approx "trig_fnd/" )"posreal" atan_approx "trig_fnd/" )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )"odd_int" integers nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"posreal" nil )"posreal" nil )"posint" nil )"nzreal" nil )nil exponentiation nil )nil defined_types nil )nil naturalnumbers nil )"real" exponentiation nil )"posnat" exponentiation nil )"(total_order?[real])" nil )"int" interval_trig nil )"posint" exponentiation nil )"nzint" integersnil )"nzrat" rationalsnil )"int" exponentiation nil )nil reals nil )"real" trig_approx "trig_fnd/" )"posrat" exponentiation nil )"nnrat" exponentiation nil )"nzreal" nil )"posreal" exponentiation nil )"nzreal" exponentiation nil )"int" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil ))nil ))nil 3318076124"" (skeep)"" (expand "Pos?" )"" (expand "Gt" )"" (expand "[||]" )"" (split) (("1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"bool" interval nil )"Interval" interval nil )"posreal" atan_approx "trig_fnd/" )"posreal" atan_approx "trig_fnd/" )"(strict_total_order?[real])" real_props nil )"bool" interval nil ))nil ))nil 3554808246"" (skeep)"" (expand "<<" )"" (flatten)"" (split)"1" (expand "Cos" )"1" (lift-if)"1" (lift-if)"1" (lift-if)"1" (lift-if)"1" (assert )"1" (lift-if)"1" (assert )"1" (ground)"1" (expand "cos_0_pi" )"1" expand "[||]" )"1" "cos_lb_nn_strict_decreasing" )"1" "n" )"1" expand "strict_decreasing?" )"1" "ub(X)" "ub(Y)" )"1" (assert ) nil nil )"2" case "Proper?(Y)" )"1" "1" expand "Proper?" )"1" "pi_bounds" )"1" "n" )"1" "pi_lb_est_le" )"1" "n" )"1" expand "<<" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Proper?" )"2" (ground) nil nil ))nil ))nil )"3" "3" "pi_lb_est_le" )"3" "n" )"3" expand "Proper?" )"3" expand "<<" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "NOT X = [|0,0|]" )"1" "1" "1" expand "Proper?" )"1" expand "[||]" )"1" expand "<<" )"1" "1" "pi_lb_est" )nil nil )"2" "pi_lb_est" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" "2" "pi_lb_est" )nil nil ))nil ))nil ))nil )"3" (hide (-3 1 2))"3" "pi_lb_est" )nil nil ))nil )"4" (hide-all-but (- 4))"4" "pi_lb_est" )nil nil ))nil )"5" (case "NOT X = [|0,0|]" )"1" "1" "1" "pi_lbn" )nil nil )"2" "pi_lbn" )nil nil ))nil ))nil )"2" replace -1)"2" expand "Neg" )"2" expand "[||]" 1)"2" expand "cos_0_pi" 1 1)"2" expand "[||]" 1)"2" expand "cos_0_pi" )"2" expand "[||]" 1)"2" expand "cos_lb" + 2)"2" "cos_approx_a0" )"2" "2" replace -1)"2" "2" assert )"2" "cos_bounds" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" (expand "Neg" )"6" expand "cos_0_pi" )"6" expand "[||]" )"6" rewrite "cos_lb_neg" )"6" rewrite "cos_lb_neg" )"6" "cos_lb_np_strict_increasing" )"6" "n" )"6" expand "strict_increasing?" )"6" "lb(Y)" "lb(X)" )"1" (assert ) nil nil )"2" assert )"2" expand "<<" )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" assert )"3" "pi_lb_est_le" )"3" "n" )"3" "pi_bounds" )"3" "3" expand "<<" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" (hide-all-but (- 2))"7" (grind :exclude "pi_lbn" ) nil nil ))nil )"8" (hide-all-but (- 3))"8" (grind :exclude "pi_lbn" ) nil nil ))nil )"9" (expand "cos_0_pi" )"9" expand "cos_npi2_pi2" )"9" expand "[||]" 1)"9" "cos_lb_nn_strict_decreasing" )"9" "n" )"9" expand "strict_decreasing?" )"9" "ub(X)" "ub(Y)" )"1" (assert ) nil nil )"2" expand "<<" )"2" expand "[||]" )"2" "pi_bounds" )"2" "n" )"2" nil nil ))nil ))nil ))nil ))nil )"3" expand "[||]" )"3" expand "<<" )"3" "pi_bounds" )"3" "n" )"3" "3" "pi_lb_est_le" )"3" "n" )"3" "3" expand "Proper?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"10" (expand "Neg" )"10" expand "cos_0_pi" )"10" expand "cos_npi2_pi2" )"10" expand "[||]" )"10" rewrite "cos_lb_neg" )"10" "cos_lb_np_strict_increasing" )"10" "n" )"10" expand "strict_increasing?" )"10" "lb(Y)" "lb(X)" )"1" (assert ) nil nil )"2" expand "<<" )"2" "pi_bounds" )"2" "n" )"2" expand "Proper?" )"2" nil nil ))nil ))nil ))nil ))nil )"3" expand "<<" )"3" expand "Proper?" )"3" "pi_bounds" )"3" "n" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"11" (expand "cos_npi2_pi2" )"11" expand "[||]" )"11" expand "<<" )"11" "11" expand "Proper?" )"11" case "ub(X) <= 0" )"1" (assert ) nil nil )"2" assert )"2" "cos_lb_np_strict_increasing" )"2" "n" )"2" expand "strict_increasing?" )"2" "lb(Y)" "lb(X)" )"2" assert )"2" "cos_lb_nn_strict_decreasing" )"2" "n" )"2" expand "strict_decreasing?" )"2" "ub(X)" "ub(Y)" )"2" "1" "1" expand "min" )"1" assert )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "lb(Y) = lb(X)" )"1" replace "1" assert )"1" expand "min" )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" assert )"2" case "ub(X) = ub(Y)" )"1" replace "1" expand "min" )"1" "1" "1" "1" assert )nil 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 )"12" (hide-all-but (- 1))"12" "pi_lb_est" )nil nil ))nil )"13" (expand "cos_0_pi" )"13" expand "[||]" 1)"13" "cos_lb_nn_strict_decreasing" )"13" "n" )"13" expand "strict_decreasing?" )"13" "ub(X)" "pi_lbn(n)" )"1" assert )"1" case "NOT cos_lb(pi_lbn(n), n) <=cos_lb(ub(X), n)" )"1" assert )"1" "pi_lb_est_le" )"1" "n" )"1" expand "<<" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "cos_lb" )"2" "cos_approx_cos" )"2" "pi_lbn(n)" "1+2*n" )"2" "cos_error_pi_lbn_bound" )"2" "n" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "pi_bounds" )"2" "2" (assert ) nil nil ))nil ))nil )"3" "3" expand "Proper?" )"3" "pi_bounds" )"3" "n" )"3" "pi_lb_est_le" )"3" "n" )"3" "3" expand "<<" )"3" expand "[||]" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"14" (expand "Neg" )"14" expand "cos_0_pi" )"14" expand "[||]" 1)"14" expand "cos_lb" )"14" "cos_error_pi_lbn_bound" )"14" "n" )"14" "cos_lb_nn_strict_decreasing" )"14" "n" )"14" expand "strict_decreasing?" )"14" "-lb(X)" "pi_lbn(n)" )"1" case "cos_lb(pi_lbn(n), n) <= cos_lb(-lb(X), n)" )"1" "1" expand "cos_lb" )"1" assert )"1" "cos_approx_cos" )"1" "pi_lbn(n)" "1+2*n" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "<<" -2)"2" expand "[||]" "2" "pi_lb_est_le" )"2" "n" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "pi_bounds" )"2" "2" assert )nil nil ))nil ))nil )"3" expand "<<" -)"3" expand "[||]" -)"3" "3" assert )"3" expand "Proper?" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"15" (expand "cos_npi2_pi2" )"15" expand "[||]" 1)"15" case "FORALL (xr:real): -pi_lbn(n)/2 <= xr AND xr <= pi_lbn(n)/2 IMPLIES -1 - (3.2 ^ (4 + 4 * n) / factorial(4 + 4 * n)) <= cos_lb(xr,n)" )"1" "lb(X)" )"1" "ub(X)" )"1" assert )"1" expand "Proper?" )"1" expand "<<" -3)"1" "pi_lb_est_le" )"1" "n" )"1" "1" expand "[||]" -)"1" assert )"1" expand "min" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" case "xr <= 0" )"1" "cos_lb_np_strict_increasing" )"1" "n" )"1" expand "strict_increasing?" )"1" "-pi_lbn(n)" "xr" )"1" assert )"1" "cos_approx_cos" )"1" expand "cos_lb" )"1" "pi_lbn(n)" "1+2*n" )"1" "cos_error_pi_lbn_bound" )"1" assert )"1" "1" assert )"1" rewrite "cos_approx_neg" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "pi_bounds" )"2" "n" )"2" assert )nil nil ))nil ))nil ))nil )"3" "pi_bounds" )"3" "3" assert )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "cos_lb_nn_strict_decreasing" )"2" "n" )"2" expand "strict_decreasing?" )"2" "xr" "pi_lbn(n)" )"1" assert )"1" expand "cos_lb" )"1" "cos_approx_cos" )"1" "pi_lbn(n)" "1+2*n" )"1" "cos_error_pi_lbn_bound" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "pi_bounds" )"2" "2" assert )nil nil ))nil ))nil )"3" assert )"3" "pi_bounds" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "Cos" )"2" (assert )"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" (assert )"2" (case "n = 0" )"1" (replace -1)"1" assert )"1" expand "[||]" )"1" expand "<<" )"1" expand "cos_0_pi" )"1" expand "cos_npi2_pi2" )"1" expand "[||]" )"1" expand "Proper?" )"1" assert )"1" expand "cos_ub" )"1" expand "cos_approx" )"1" expand "sigma" )"1" expand "sigma" )"1" expand "cos_term" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "NOT n>=1" )"1" "1" (assert ) nil nil ))nil )"2" "2" "1" expand "cos_0_pi" )"1" expand "[||]" )"1" "cos_ub_nn_strict_decreasing" )"1" "n" )"1" expand "strict_decreasing?" )"1" "lb(Y)" "lb(X)" )"1" (assert ) nil nil )"2" expand "Proper?" )"2" expand "<<" )"2" nil nil ))nil ))nil )"3" case "Proper?(Y)" )"1" expand "<<" )"1" expand "Proper?" )"1" nil nil ))nil ))nil )"2" "2" "pi_lb_est" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOT X = [|0,0|]" )"1" "1" "1" "1" "pi_lb_est" )nil nil )"2" "pi_lb_est" )nil nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "[||]" )"2" expand "cos_0_pi" )"2" expand "[||]" )"2" expand "<<" -1)"2" "2" assert )"2" expand "Neg" )"2" expand "[||]" )"2" "cos_ub_nn_strict_decreasing" )"2" "n" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "cos_npi2_pi2" )"3" expand "cos_0_pi" )"3" expand "[||]" )"3" "cos_ub_nn_strict_decreasing" )"3" "n" )"3" assert )"3" expand "strict_decreasing?" )"3" "0" "lb(X)" )"1" assert )"1" "cos_ub_a0" )"1" "1" "1" assert )"1" expand "<<" )"1" "1" assert )"1" case "lb(X) = 0" )"1" replace "1" assert )"1" "cos_ub_a0" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "<<" )"2" expand "Proper?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" expand "cos_0_pi" )"4" expand "[||]" )"4" expand "<<" )"4" "4" "cos_ub_nn_strict_decreasing" )"4" "n" )"4" assert )"4" expand "strict_decreasing?" )"4" "0" "lb(X)" )"1" assert )"1" case "lb(X) = 0" )"1" "cos_ub_a0" )"1" "1" assert )nil nil ))nil ))nil )"2" assert )"2" "cos_ub_a0" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Proper?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" case "NOT X = [|0,0|]" )"1" "1" "1" "pi_lb_est" )nil nil )"2" "pi_lb_est" )nil nil ))nil ))nil )"2" replace -1)"2" expand "[||]" )"2" expand "<<" )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"6" expand "Neg" )"6" expand "cos_0_pi" )"6" expand "[||]" )"6" rewrite "cos_ub_neg" )"6" rewrite "cos_ub_neg" )"6" "cos_ub_np_strict_increasing" )"6" "n" )"6" assert )"6" expand "strict_increasing?" )"6" "ub(X)" "ub(Y)" )"1" assert )nil nil )"2" expand "<<" )"2" expand "Proper?" )"2" nil nil ))nil ))nil )"3" expand "<<" )"3" expand "Proper?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" expand "Neg" )"7" expand "[||]" )"7" expand "<<" )"7" "7" expand "cos_npi2_pi2" )"7" expand "cos_0_pi" )"7" expand "[||]" )"7" "cos_ub_nn_strict_decreasing" )"7" "n" )"7" assert )"7" expand "strict_decreasing?" )"7" "0" "-ub(X)" )"1" assert )"1" case "ub(X) = 0" )"1" replace "1" rewrite "cos_ub_a0" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" rewrite "cos_ub_a0" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "Proper?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"8" "8" expand "<<" )"8" expand "[||]" )"8" "8" expand "Neg" )"8" expand "[||]" )"8" expand "cos_0_pi" )"8" expand "[||]" )"8" "cos_ub_nn_strict_decreasing" )"8" expand "Proper?" )"8" "n" )"8" assert )"8" expand "strict_decreasing?" )"8" "0" "-ub(X)" )"8" "cos_ub_a0" )"8" "8" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"9" "9" "pi_lb_est" )nil nil ))nil )"10" "10" "pi_lb_est" )nil nil ))nil )"11" "11" expand "cos_npi2_pi2" )"11" expand "[||]" )"11" (assert ) nil nil ))nil ))nil ))nil )"12" "12" expand "[||]" )"12" expand "<<" )"12" "12" expand "cos_npi2_pi2" )"12" expand "[||]" )"12" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"13" "13" "pi_lb_est" )nil nil ))nil )"14" "14" "14" "pi_lb_est" )nil nil ))nil ))nil )"15" "15" "pi_lb_est" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" interval nil )"rat" rationals nil )"(total_order?[real])" nil )nil interval nil )"posnat" factorial "ints/" )nil integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[bool, bool -> bool]" booleans nil )"odd_int" integers nil )nil trig_approx "trig_fnd/" )"real" interval_trig nil )nil trig_approx "trig_fnd/" )nil interval_trig nil )"even_int" integersnil )"posint" nil )"nat" interval_trig nil )"real" atan_approx "trig_fnd/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"(strict_total_order?[real])" real_props nil )"Interval" interval_trig nil )"nzreal" nil )"posreal" nil )"real" reals nil )nil real_types nil )"bool" real_fun_preds "reals/" )nil trig_approx"trig_fnd/" )nil trig_approx "trig_fnd/" )nil interval nil )"nzreal" real_typesnil )"real" exponentiation nil )"real" exponentiation nil )"{rr: nnreal | rr < pi}" trig_approx"trig_fnd/" )"Interval" interval nil )"real" trig_approx "trig_fnd/" )"odd_int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil trig_approx "trig_fnd/" )"trig_range" sincos_def"trig_fnd/" )"[numfield -> numfield]" number_fields nil )nil trig_approx "trig_fnd/" )NOT const-decl "[bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"Interval" interval_trig nil )nil trig_approx"trig_fnd/" )"bool" real_fun_preds "reals/" )"bool" interval nil )"posreal" atan_approx "trig_fnd/" )"posreal" atan_approx "trig_fnd/" )nil trig_approx "trig_fnd/" )nil atan_approx "trig_fnd/" )"(strict_total_order?[real])" real_props nil )nil real_types nil )"Interval" interval_trig nil )"posreal" atan "trig_fnd/" )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"Interval" interval_trig nil )nil interval nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )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 booleans nil )"bool" reals nil )nil naturalnumbers nil )"Interval" interval nil )"even_int" integersnil )"posint" nil )"nnreal" nil )"real" reals nil )"Interval" interval_trig nil )"posrat" nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"real" reals nil )"bool" reals nil )nil trig_approx"trig_fnd/" )nil trig_approx "trig_fnd/" )nil trig_approx "trig_fnd/" )nil trig_approx"trig_fnd/" )"real" trig_approx "trig_fnd/" )"real" trig_approx "trig_fnd/" )"real" sigma "reals/" )"real" trig_approx "trig_fnd/" ))nil )nil 3554808171"" (skeep)"" (expand "<<" )"" (flatten)"" (split)"1" (expand "Cos2" )"1" (lift-if)"1" (lift-if)"1" (lift-if)"1" (lift-if)"1" (assert )"1" (lift-if)"1" (assert )"1" (ground)"1" (expand "cos_0_pi" )"1" expand "[||]" )"1" "cos_lb_nn_strict_decreasing" )"1" "n" )"1" expand "strict_decreasing?" )"1" "ub(X)" "ub(Y)" )"1" (assert ) nil )"2" case "Proper?(Y)" )"1" "1" expand "Proper?" )"1" "pi_bounds" )"1" "1" expand "<<" )"1" nil )))))))))))"2" expand "Proper?" )"2" (ground) nil )))))"3" "3" "pi_bounds" )"3" "3" expand "Proper?" )"3" expand "<<" )"3" nil )))))))))))))))))))))))"2" (case "NOT X = [|0,0|]" )"1" "1" "1" expand "Proper?" )"1" expand "[||]" )"1" expand "<<" )"1" "1" "pi_lbn" )nil )"2" "pi_lbn" )nil )))))))))))))"2" replace -1)"2" "2" "pi_lbn" )nil )))))))"3" (hide (-3 1 2))"3" (grind :exclude "pi_lbn" ) nil )))"4" (hide-all-but (- 4))"4" (grind :exclude "pi_lbn" ) nil )))"5" (case "NOT X = [|0,0|]" )"1" "1" "1" (grind) nil )"2" "pi_lbn" )nil )))))"2" expand "Neg" )"2" expand "[||]" 1)"2" expand "cos_0_pi" 1 1)"2" expand "[||]" 1)"2" expand "cos_0_pi" )"2" expand "[||]" 1)"2" replace -1 1)"2" expand "[||]" 1)"2" expand "cos_lb" + 2)"2" "cos_approx_a0" )"2" "2" replace -1)"2" "2" assert )"2" "cos_bounds" )"2" "2" nil )))))))))))))))))))))))))))))))))))"6" (expand "Neg" )"6" expand "cos_0_pi" )"6" expand "[||]" )"6" rewrite "cos_lb_neg" )"6" rewrite "cos_lb_neg" )"6" "cos_lb_np_strict_increasing" )"6" "n" )"6" expand "strict_increasing?" )"6" "lb(Y)" "lb(X)" )"1" (assert ) nil )"2" assert )"2" expand "<<" )"2" "2" assert )"2" assert )"2" "pi_bounds" )"2" "2" nil )))))))))))))))"3" "pi_bounds" )"3" "3" expand "<<" )"3" nil )))))))))))))))))))))))))"7" (hide-all-but (- 2))"7" (grind :exclude "pi_lbn" ) nil )))"8" (hide-all-but (- 3))"8" (grind :exclude "pi_lbn" ) nil )))"9" (expand "cos_0_pi" )"9" expand "cos_npi2_pi2" )"9" expand "[||]" 1)"9" "cos_lb_nn_strict_decreasing" )"9" "n" )"9" expand "strict_decreasing?" )"9" "ub(X)" "ub(Y)" )"1" (assert ) nil )"2" expand "<<" )"2" expand "[||]" )"2" "pi_bounds" )"2" "2" nil )))))))))"3" expand "[||]" )"3" expand "<<" )"3" "pi_bounds" )"3" "3" expand "Proper?" )"3" nil )))))))))))))))))))))))))"10" (expand "Neg" )"10" expand "cos_0_pi" )"10" expand "cos_npi2_pi2" )"10" expand "[||]" )"10" rewrite "cos_lb_neg" )"10" "cos_lb_np_strict_increasing" )"10" "n" )"10" expand "strict_increasing?" )"10" "lb(Y)" "lb(X)" )"1" (assert ) nil )"2" expand "<<" )"2" "pi_bounds" )"2" "2" expand "Proper?" )"2" nil )))))))))"3" expand "<<" )"3" expand "Proper?" )"3" "pi_bounds" )"3" "3" nil )))))))))))))))))))))))))))"11" (expand "cos_npi2_pi2" )"11" expand "[||]" )"11" expand "<<" )"11" "11" expand "Proper?" )"11" case "ub(X) <= 0" )"1" (assert ) nil )"2" assert )"2" "cos_lb_np_strict_increasing" )"2" "n" )"2" expand "strict_increasing?" )"2" "lb(Y)" "lb(X)" )"1" assert )"1" "cos_lb_nn_strict_decreasing" )"1" "n" )"1" expand "strict_decreasing?" )"1" "ub(X)" "ub(Y)" )"1" "1" "1" expand "min" )"1" assert )"1" "1" "1" "1" assert )nil )))))))))))"2" case "lb(Y) = lb(X)" )"1" replace "1" assert )"1" expand "min" )"1" "1" "1" "1" assert )nil )))))))))))))"2" assert )nil )))))"2" assert )"2" case "ub(X) = ub(Y)" )"1" replace "1" expand "min" )"1" "1" "1" "1" assert )nil )))))))))))"2" assert )nil )))))))"2" assert )"2" "pi_bounds" )"2" "2" nil )))))))"3" "pi_bounds" )"3" "3" nil )))))))))))))))"2" "pi_bounds" )"2" "2" assert )nil )))))"3" "pi_bounds" )"3" "3" nil )))))))))))))))))))))))))))"12" (hide-all-but (- 1))"12" (grind :exclude "pi_lbn" ) nil )))"13" (expand "cos_0_pi" )"13" expand "[||]" 1)"13" "cos_lb_nn_strict_decreasing" )"13" "n" )"13" expand "strict_decreasing?" )"13" "ub(X)" "pi_lbn(n)" )"1" assert )"1" case "NOT cos_lb(pi_lbn(n), n) <=cos_lb(ub(X), n)" )"1" assert )"1" expand "<<" -1)"1" expand "[||]" -1)"1" nil )))))))"2" "2" expand "cos_lb" )"2" "cos_approx_cos" )"2" "pi_lbn(n)" "1+2*n" )"2" "cos_error_pi_lbn_bound" )"2" "n" )"2" assert )nil )))))))))))))))))"2" "pi_bounds" )"2" "2" (assert ) nil )))))"3" "3" expand "Proper?" )"3" "pi_bounds" )"3" "3" "3" expand "<<" )"3" expand "[||]" )"3" nil )))))))))))))))))))))))))))"14" (expand "Neg" )"14" expand "cos_0_pi" )"14" expand "[||]" 1)"14" expand "cos_lb" )"14" "cos_error_pi_lbn_bound" )"14" "n" )"14" "cos_lb_nn_strict_decreasing" )"14" "14" expand "strict_decreasing?" )"14" "-lb(X)" "pi_lbn(n)" )"1" case "cos_lb(pi_lbn(n), n) <= cos_lb(-lb(X), n)" )"1" "1" expand "cos_lb" )"1" assert )"1" "cos_approx_cos" )"1" "pi_lbn(n)" "1+2*n" )"1" assert )nil )))))))))))"2" assert )"2" expand "<<" -2)"2" expand "[||]" "2" nil )))))))))"2" "pi_bounds" )"2" "2" assert )nil )))))"3" expand "<<" -)"3" expand "[||]" -)"3" "3" assert )"3" expand "Proper?" )"3" assert )"3" "pi_bounds" )"3" "3" nil )))))))))))))))))))))))))))))))))))))"15" (expand "cos_npi2_pi2" )"15" expand "[||]" 1)"15" case "FORALL (xr:real): -pi_lbn(n)/2 <= xr AND xr <= pi_lbn(n)/2 IMPLIES -1 - (3.2 ^ (4 + 4 * n) / factorial(4 + 4 * n)) <= cos_lb(xr,n)" )"1" "lb(X)" )"1" "ub(X)" )"1" assert )"1" expand "Proper?" )"1" expand "<<" -3)"1" "1" expand "[||]" -)"1" assert )"1" expand "min" )"1" "1" nil )))))))))))))))))))))"2" "2" "2" case "xr <= 0" )"1" "cos_lb_np_strict_increasing" )"1" "n" )"1" expand "strict_increasing?" )"1" "-pi_lbn(n)" "xr" )"1" assert )"1" "cos_approx_cos" )"1" expand "cos_lb" )"1" "pi_lbn(n)" "1+2*n" )"1" "cos_error_pi_lbn_bound" )"1" assert )"1" "1" assert )"1" rewrite "cos_approx_neg" )"1" assert )nil )))))))))))))))))))"2" assert )"2" "pi_bounds" )"2" "n" )"2" assert )nil )))))))"3" "pi_bounds" )"3" "3" assert )nil )))))))))))))"2" "cos_lb_nn_strict_decreasing" )"2" "n" )"2" expand "strict_decreasing?" )"2" "xr" "pi_lbn(n)" )"1" assert )"1" expand "cos_lb" )"1" "cos_approx_cos" )"1" "pi_lbn(n)" "1+2*n" )"1" "cos_error_pi_lbn_bound" )"1" "1" assert )nil )))))))))))))"2" "pi_bounds" )"2" "2" assert )nil )))))"3" assert )"3" "pi_bounds" )"3" "3" assert )nil )))))))))))))))))))))))))))))))))))))))))))))"2" (expand "Cos2" )"2" (assert )"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" (assert )"2" (ground)"1" (expand "cos_0_pi" )"1" (postpone) nil )))"2" (postpone) nil ) ("3" (postpone) nil )"4" (postpone) nil ) ("5" (postpone) nil )"6" (postpone) nil ) ("7" (postpone) nil )"8" (postpone) nil ) ("9" (postpone) nil )"10" (postpone) nil )"11" (postpone) nil )"12" (postpone) nil )"13" (postpone) nil )"14" (postpone) nil )"15" (postpone)nil ))))))))))))))))))))))))))nil )nil nil )nil 3552043684"" (skeep)"" (expand "<<" )"" (flatten)"" (split)"1" (expand "Cos" )"1" (lift-if)"1" (lift-if)"1" (lift-if)"1" (lift-if)"1" (assert )"1" (lift-if)"1" (assert )"1" (ground)"1" (expand "cos_0_pi" )"1" expand "[||]" )"1" "cos_lb_nn_strict_decreasing" )"1" "n" )"1" expand "strict_decreasing?" )"1" "ub(X)" "ub(Y)" )"1" (assert ) nil nil )"2" case "Proper?(Y)" )"1" "1" expand "Proper?" )"1" "pi_bounds" )"1" "1" expand "<<" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Proper?" )"2" (ground) nil nil ))nil ))nil )"3" "3" "pi_bounds" )"3" "3" expand "Proper?" )"3" expand "<<" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "NOT X = [|0,0|]" )"1" "1" "1" expand "Proper?" )"1" expand "[||]" )"1" expand "<<" )"1" "1" "pi_lbn" )nil nil )"2" "pi_lbn" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" "2" "pi_lbn" )nil nil ))nil ))nil ))nil )"3" (hide (-3 1 2))"3" (grind :exclude "pi_lbn" ) nil nil ))nil )"4" (hide-all-but (- 4))"4" (grind :exclude "pi_lbn" ) nil nil ))nil )"5" (case "NOT X = [|0,0|]" )"1" "1" "1" (grind) nil nil )"2" "pi_lbn" )nil nil ))nil ))nil )"2" expand "Neg" )"2" expand "[||]" 1)"2" expand "cos_0_pi" 1 1)"2" expand "[||]" 1)"2" expand "cos_0_pi" )"2" expand "[||]" 1)"2" replace -1 1)"2" expand "[||]" 1)"2" expand "cos_lb" + 2)"2" "cos_approx_a0" )"2" "2" replace -1)"2" "2" assert )"2" "cos_bounds" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" (expand "Neg" )"6" expand "cos_0_pi" )"6" expand "[||]" )"6" rewrite "cos_lb_neg" )"6" rewrite "cos_lb_neg" )"6" "cos_lb_np_strict_increasing" )"6" "n" )"6" expand "strict_increasing?" )"6" "lb(Y)" "lb(X)" )"1" (assert ) nil nil )"2" assert )"2" expand "<<" )"2" "2" assert )"2" assert )"2" "pi_bounds" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "pi_bounds" )"3" "3" expand "<<" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" (hide-all-but (- 2))"7" (grind :exclude "pi_lbn" ) nil nil ))nil )"8" (hide-all-but (- 3))"8" (grind :exclude "pi_lbn" ) nil nil ))nil )"9" (expand "cos_0_pi" )"9" expand "cos_npi2_pi2" )"9" expand "[||]" 1)"9" "cos_lb_nn_strict_decreasing" )"9" "n" )"9" expand "strict_decreasing?" )"9" "ub(X)" "ub(Y)" )"1" (assert ) nil nil )"2" expand "<<" )"2" expand "[||]" )"2" "pi_bounds" )"2" "2" nil nil ))nil ))nil ))nil ))nil )"3" expand "[||]" )"3" expand "<<" )"3" "pi_bounds" )"3" "3" expand "Proper?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"10" (expand "Neg" )"10" expand "cos_0_pi" )"10" expand "cos_npi2_pi2" )"10" expand "[||]" )"10" rewrite "cos_lb_neg" )"10" "cos_lb_np_strict_increasing" )"10" "n" )"10" expand "strict_increasing?" )"10" "lb(Y)" "lb(X)" )"1" (assert ) nil nil )"2" expand "<<" )"2" "pi_bounds" )"2" "2" expand "Proper?" )"2" nil nil ))nil ))nil ))nil ))nil )"3" expand "<<" )"3" expand "Proper?" )"3" "pi_bounds" )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"11" (expand "cos_npi2_pi2" )"11" expand "[||]" )"11" expand "<<" )"11" "11" expand "Proper?" )"11" case "ub(X) <= 0" )"1" (assert ) nil nil )"2" assert )"2" "cos_lb_np_strict_increasing" )"2" "n" )"2" expand "strict_increasing?" )"2" "lb(Y)" "lb(X)" )"1" assert )"1" "cos_lb_nn_strict_decreasing" )"1" "n" )"1" expand "strict_decreasing?" )"1" "ub(X)" "ub(Y)" )"1" "1" "1" expand "min" )"1" assert )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "lb(Y) = lb(X)" )"1" replace "1" assert )"1" expand "min" )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" assert )"2" case "ub(X) = ub(Y)" )"1" replace "1" expand "min" )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "pi_bounds" )"2" "2" nil nil ))nil ))nil ))nil )"3" "pi_bounds" )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "pi_bounds" )"2" "2" assert )nil nil ))nil ))nil )"3" "pi_bounds" )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"12" (hide-all-but (- 1))"12" "pi_lbn" )nil nil ))nil )"13" (expand "cos_0_pi" )"13" expand "[||]" )"13" expand "<<" )"13" "13" "sign(cos_lb(pi_lbn(10),10)+1)" )"13" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil )"14" (postpone) nil nil )"15" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil )nil shostak))nil 3555173443"" (skeep)"" (expand "Proper?" )"" (expand "<<" )"" (flatten)"" (split)"1" (expand "Sin" )"1" (assert )"1" (lift-if)"1" (lift-if)"1" (lift-if)"1" (lift-if)"1" (lift-if)"1" (lift-if)"1" (lift-if)"1" assert )"1" "1" "1" "1" "1" "1" "1" "1" "1" "1" assert )"1" "1" "1" "1" "1" assert )"1" "1" expand "Union" )"1" expand "[||]" )"1" case "FORALL (r1,r2,s1,s2:real): (r1<=s1 AND r2<=s2) IMPLIES min(r1,r2)<=min(s1,s2)" )"1" rewrite "1" "1" "Cos_fundamental" )"1" expand "<<" "1" "1" assert )"1" "1" "1" "pi_bounds" )"1" "n" )"1" "pi_ubn" "pi_lbn" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "Neg" )"2" expand "[||]" )"2" expand "Add" )"2" expand "Intersection" )"2" expand "[||]" )"2" case "FORALL (r1,r2:real): (-r1 <= -r2) IFF (r2 <= r1)" )"1" rewrite "1" "1" "Cos_fundamental" )"1" expand "<<" "1" "1" assert )"1" "1" "1" "pi_bounds" )"1" "n" )"1" "pi_ubn" "pi_lbn" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" expand "Neg" )"2" expand "[||]" )"2" expand "Union" )"2" expand "[||]" )"2" case "FORALL (s1,s2:real,s3:real): s3<=s2 IMPLIES min(s1,-s2)<=-s3" )"1" rewrite "1" "1" "Cos_fundamental" )"1" expand "<<" "1" "1" assert )"1" "1" "1" "pi_bounds" )"1" "n" )"1" "pi_ubn" "pi_lbn" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" nil nil ))nil ))nil )"4" case "FORALL (s1,s2:real,s3:real): s2<=s3 IMPLIES min(s2,s1)<=s3" )"1" expand "Union" )"1" expand "[||]" )"1" rewrite "1" "1" "Cos_fundamental" )"1" expand "<<" "1" "1" assert )"1" "1" "1" "pi_bounds" )"1" "n" )"1" "pi_ubn" "pi_lbn" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil )"5" "5" nil nil ))nil )"6" "6" nil nil ))nil )"7" expand "Neg" )"7" expand "[||]" )"7" expand "Add" )"7" expand "Intersection" )"7" expand "[||]" )"7" case "FORALL (r1,r2:real): (-r1 <= -r2) IFF (r2 <= r1)" )"1" rewrite "1" "1" "Cos_fundamental" )"1" expand "<<" "1" "1" assert )"1" "1" "pi_bounds" )"1" "n" )"1" "pi_ubn" "pi_lbn" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"8" "8" nil nil ))nil )"9" "9" nil nil ))nil )"10" "10" nil nil ))nil )"11" "11" nil nil ))nil )"12" "12" nil nil ))nil )"13" "13" nil nil ))nil )"14" "14" nil nil ))nil )"15" "15" nil nil ))nil )"16" "16" nil nil ))nil )"17" "Cos_fundamental" )"17" expand "<<" "17" "17" assert )"17" "17" "pi_bounds" )"17" "n" )"17" "pi_ubn" "pi_lbn" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"18" "18" nil nil ))nil )"19" "19" nil nil ))nil )"20" "20" nil nil ))nil )"21" "21" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "Sin" )"2" (assert )"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" assert )"2" "2" "2" "2" "2" "2" "2" "2" "2" "2" assert )"2" "2" "2" "2" "2" assert )"2" "1" expand "Union" )"1" expand "[||]" )"1" case "FORALL (r1,r2,s1,s2:real): (r1<=s1 AND r2<=s2) IMPLIES max(r1,r2)<=max(s1,s2)" )"1" rewrite "1" "1" "Cos_fundamental" )"1" expand "<<" "1" "1" assert )"1" "1" "1" "pi_bounds" )"1" "n" )"1" "pi_ubn" "pi_lbn" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "Neg" )"2" expand "[||]" )"2" expand "Add" )"2" expand "Intersection" )"2" expand "[||]" )"2" case "FORALL (r1,r2:real): (-r1 <= -r2) IFF (r2 <= r1)" )"1" rewrite "1" "1" "Cos_fundamental" )"1" expand "<<" "1" "1" assert )"1" "1" "1" "pi_bounds" )"1" "n" )"1" "pi_ubn" "pi_lbn" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil )"4" "4" nil nil ))nil )"5" "5" nil nil ))nil )"6" expand "Neg" )"6" expand "Union" )"6" expand "[||]" )"6" case "FORALL (s1,s2:real,s3:real): s2<=s3 IMPLIES -s3<=max(s1,-s2)" )"1" rewrite "1" "1" "Cos_fundamental" )"1" expand "<<" "1" "1" assert )"1" "1" "1" "pi_bounds" )"1" "n" )"1" "pi_ubn" "pi_lbn" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"7" expand "Neg" )"7" expand "[||]" )"7" case "FORALL (r1,r2:real): (-r1 <= -r2) IFF (r2 <= r1)" )"1" rewrite "1" "1" "Cos_fundamental" )"1" expand "<<" "1" "1" assert )"1" "1" "pi_bounds" )"1" "n" )"1" "pi_ubn" "pi_lbn" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"8" "8" nil nil ))nil )"9" "9" nil nil ))nil )"10" "10" nil nil ))nil )"11" "11" nil nil ))nil )"12" "12" nil nil ))nil )"13" "13" nil nil ))nil )"14" expand "Neg" )"14" expand "Union" )"14" expand "[||]" )"14" expand "Add" )"14" expand "Intersection" )"14" expand "[||]" )"14" case "FORALL (s1,s2:real,s3:real): s3<=s1 IMPLIES s3<=max(s1,s2)" )"1" "1" "1" nil nil )"2" "2" "Cos_fundamental" )"2" expand "<<" "2" "2" assert )"2" "2" "pi_bounds" )"2" "n" )"2" "pi_ubn" "pi_lbn" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"15" "15" nil nil ))nil )"16" "16" nil nil ))nil )"17" expand "[||]" )"17" expand "Add" )"17" expand "Intersection" )"17" expand "[||]" )"17" "Cos_fundamental" )"17" expand "<<" "17" "17" assert )"17" "17" "pi_bounds" )"17" "n" )"17" "pi_ubn" "pi_lbn" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"18" "18" nil nil ))nil )"19" "19" nil nil ))nil )"20" "20" nil nil ))nil )"21" "21" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" interval nil )nil interval nil )"Interval" interval_trig nil )"Interval" interval nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"real" reals nil )"real" reals nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"posreal" atan "trig_fnd/" )"real" atan "trig_fnd/" )"real" integral_def "analysis/" )"(strict_total_order?[real])" real_props nil )nil atan_approx "trig_fnd/" )nil interval_trig nil )"Interval" interval nil )"real" atan_approx "trig_fnd/" )"real" atan_approx "trig_fnd/" )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"Interval" interval nil )"Interval" interval nil )"Interval" interval_trig nil )nil interval nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"Interval" interval nil )"nzreal" nil )"posreal" atan_approx "trig_fnd/" )"nzreal" real_typesnil )"posreal" atan_approx "trig_fnd/" )nil interval nil )"(total_order?[real])" nil )"bool" interval nil ))nil 3301931278"" (skosimp*) (("" (assert ) nil nil )) nil )"(strict_total_order?[real])" real_props nil ))nil 3301931279"" (skosimp*) (("" (assert ) nil nil )) nil )"(strict_total_order?[real])" real_props nil ))nil 3304702393"" (skosimp*) (("" (assert ) nil nil )) nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3302134474"" (skosimp*) (("" (assert ) nil nil )) nil )"(strict_total_order?[real])" real_props nil ))nil 3559305084"" (skeep)"" (decompose-equality +)"1" (expand "Union" )"1" (expand "[||]" )"1" (invoke (case "%1 = %2" ) (! 1 2) (! 1 2 1))"1" (replaces -1)"1" (expand "Neg" )"1" (expand "[||]" )"1" (expand "tan_npi2_pi2" )"1" (expand "<<" )"1" (flatten)"1" (assert )"1" (expand "##" )"1" (flatten)"1" assert )"1" case "%1" ) (! 1 1 1))"1" "1" assert )"1" case "Intersection(X, ") "1" replace -1)"1" assert )"1" expand "tan_0_pi2" )"1" rewrite "cos_lb_neg" )"1" assert )"1" rewrite "cos_ub_a0" )"1" assert )"1" rewrite "sin_ub_neg" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "cos_lb" "pi_lb_est" ))nil nil ))nil ))nil ))nil ))nil )"2" "2" "cos_lb_nn_strict_decreasing" )"2" "n" )"2" expand "strict_decreasing?" )"2" "-lb(X)" "pi_lbn(n)/2" )"1" "ub(X)" "pi_lbn(n)/2" )"1" assert )"1" "cos_lb_pi2_pos" )"1" "n" )"1" assert )"1" assert )"1" case "pi_lb_est(n) <= pi_lbn(n)" )"1" assert )"1" rewrite "cos_lb_neg" )"1" "1" case "-lb(X) = pi_lbn(n)/2" )"1" replace "1" rewrite "cos_lb_neg" )nil nil ))nil )"2" assert )nil nil ))nil )"2" case "-lb(X) = pi_lbn(n)/2" )"1" replace "1" rewrite "cos_lb_neg" )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "pi_lb_est" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "pi_bounds" )"2" "2" nil nil ))nil ))nil ))nil )"2" "pi_bounds" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" case "FORALL (a,b:real): a<=b IMPLIES min(a,b) = a" )"1" (rewrite -1)"1" (hide (-1 2))"1" case "FORALL (a,b:real): a<=0 AND b>=0 IMPLIES a<=b" )"1" (inst?)"1" (assert )"1" (hide 2)"1" (split)"1" expand "Neg" )"1" expand "[||]" )"1" expand "tan_0_pi2" )"1" expand "[||]" )"1" case "%1" ) (! 1 1 1))"1" assert )"1" "1" assert )"1" "1" "sin_ub_increasing" )"1" "n" )"1" expand "strict_increasing?" )"1" "1" "0" "%1" )"1" rewrite "sin_ub_a0" )"1" assert )"1" case "FORALL (a1:nnreal): (NOT a1=0) IMPLIES 0<a1" )"1" rewrite "1" replace "1" rewrite "sin_ub_a0" )"1" assert )nil nil ))nil ))nil )"2" "2" "pi_lb_est" )nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "pi_lb_est" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "NOT ub(Intersection(X, (# lb := -pi_lb_est(n) / 2, ub := 0 #))) = 0" )"1" "1" "pi_lb_est" )nil nil ))nil )"2" replace -1)"2" rewrite "cos_ub_a0" )"2" assert )"2" "cos_lb_nn_strict_decreasing" )"2" "n" )"2" expand "strict_decreasing?" )"2" "%1" "pi_lbn(n)/2" )"1" assert )"1" case "%1 = %2" )"1" "cos_lb_pi2_pos" )"1" "n" )"1" assert )nil nil ))nil ))nil )"2" "cos_lb_pi2_pos" )"2" "n" )"2" assert )"2" case "pi_lb_est(n) <= pi_lbn(n)" )"1" "pi_lb_est" "pi_lbn" "cos_lb" ))nil nil )"2" "2" expand "pi_lb_est" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "pi_bounds" )"2" "n" )"2" assert )nil nil ))nil ))nil ))nil )"3" assert )"3" "3" case "pi_lb_est(n) <= pi_lbn(n)" )"1" "pi_bounds" )"1" "n" )"1" assert )"1" "1" "pi_lb_est" "pi_lbn" "cos_lb" "pi_ubn" ))nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "pi_lb_est" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "tan_0_pi2" )"2" expand "[||]" )"2" case "%1" ) (! 1 1 1))"1" assert )"1" "1" assert )"1" "1" "sin_lb_increasing" )"1" "n" )"1" expand "strict_increasing?" )"1" "0" "%1" )"1" case "%1 = %2" )"1" replace "1" rewrite "sin_lb_a0" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" rewrite "sin_lb_a0" )"2" assert )"2" "pi_lb_est" "pi_lbn" "cos_lb" "pi_ubn" "sin_lb" "cos_ub" ))nil nil ))nil ))nil ))nil ))nil )"2" "pi_lb_est" "pi_lbn" "cos_lb" "pi_ubn" "sin_lb" "cos_ub" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "%1 = 0" )"1" "1" rewrite "cos_ub_a0" )"1" assert )"1" "cos_lb_nn_strict_decreasing" )"1" "n" )"1" expand "strict_decreasing?" )"1" "%1" "pi_lbn(n)/2" )"1" "cos_lb_pi2_pos" )"1" "n" )"1" assert )"1" case "%1 = %2" )"1" assert )nil nil )"2" case "pi_lb_est(n) <= pi_lbn(n)" )"1" "pi_lb_est" "pi_lbn" "cos_lb" "pi_ubn" "sin_lb" "cos_ub" ))nil nil )"2" "2" expand "pi_lb_est" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "pi_bounds" )"2" "n" )"2" nil nil ))nil ))nil )"3" assert )"3" case "pi_lb_est(n) <= pi_lbn(n)" )"1" "pi_bounds" )"1" "n" )"1" "pi_lb_est" "pi_lbn" "cos_lb" "pi_ubn" "sin_lb" "cos_ub" "pi" ))nil nil ))nil ))nil )"2" "2" expand "pi_lb_est" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "pi_lb_est" "pi_lbn" "cos_lb" "pi_ubn" "sin_lb" "cos_ub" "pi" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "tan_npi2_pi2" )"2" (expand "<<" )"2" (flatten)"2" (assert )"2" (expand "##" )"2" (flatten)"2" (assert )"2" (invoke (case "%1" ) (! 1 1 1))"1" (flatten)"1" (assert )"1" case "Intersection(X, ") "1" (expand "[||]" )"1" expand "Neg" )"1" replace -1)"1" expand "[||]" )"1" assert )"1" expand "tan_0_pi2" )"1" rewrite "cos_lb_neg" )"1" rewrite "cos_ub_a0" )"1" rewrite "sin_lb_a0" )"1" expand "[||]" )"1" assert )"1" rewrite "sin_ub_neg" )"1" expand "Union" )"1" expand "[||]" )"1" case "%1" )"1" "1" assert )"1" replace "1" replace "1" case "FORALL (b:real): 0<=b IMPLIES max(0,b) = b" )"1" rewrite "1" "1" case "%1 = %2" )"1" replace "1" nil nil ))nil )"2" "pi_lb_est" "pi_lbn" "cos_lb" "pi_ubn" "sin_lb" "cos_ub" "pi" "sin_ub" ))nil nil ))nil ))nil )"2" "2" "2" "sin_bounds" )"2" "2" "2" "sin_ge_0" )"2" "2" assert )"2" "2" "pi_bounds" )"2" "n" )"2" "2" case "pi_lb_est(n) <= pi_lbn(n)" )"1" "pi_lb_est" "pi_lbn" "cos_lb" "pi_ubn" "sin_lb" "cos_ub" "pi" "sin_ub" ))nil nil )"2" "2" expand "pi_lb_est" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "%1 = 0" )"1" replace "1" rewrite "cos_ub_a0" )"1" assert )"1" "cos_lb_nn_strict_decreasing" )"1" "n" )"1" expand "strict_decreasing?" )"1" "%1" "pi_lbn(n)/2" )"1" "cos_lb_pi2_pos" )"1" "n" )"1" assert )"1" "pi_lb_est_le" )"1" "n" )"1" "1" "pi_lb_est" "pi_lbn" "cos_lb" "pi_ubn" "sin_lb" "cos_ub" "pi" "sin_ub" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "pi_bounds" )"2" "n" )"2" nil nil ))nil ))nil )"3" "3" "pi_lb_est_le" )"3" "n" )"3" "3" "pi_lb_est" "pi_lbn" "cos_lb" "pi_ubn" "sin_lb" "cos_ub" "pi" "sin_ub" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "pi_lb_est" "pi_lbn" "cos_lb" "pi_ubn" "sin_lb" "cos_ub" "pi" "sin_ub" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "pi_lb_est" "pi_lbn" "cos_lb" "pi_ubn" "sin_lb" "cos_ub" "pi" "sin_ub" ))nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "pi_lb_est_le" )"2" (inst - "n" )"2" (flatten)"2" "cos_lb_pi2_pos" )"2" "n" )"2" assert )"2" "cos_lb_nn_strict_decreasing" )"2" "n" )"2" expand "strict_decreasing?" )"2" "pi_lbn(n)/2" )"1" "-lb(X)" )"1" "ub(X)" )"1" assert )"1" rewrite "cos_lb_neg" )"1" "1" case "-lb(X) = pi_lbn(n)/2" )"1" replace "1" rewrite "cos_lb_neg" )nil nil ))nil )"2" assert )nil nil ))nil )"2" case "-lb(X) = pi_lbn(n)/2" )"1" replace "1" rewrite "cos_lb_neg" )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "pi_bounds" )"2" "n" )"2" 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 )"(total_order?[real])" nil )"real" reals nil )"nnreal" nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"Interval" interval_trig nil )"Interval" interval nil )"Interval" interval nil )"Interval" interval_trig nil )"Interval" interval nil )"Interval" interval nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan "trig_fnd/" )"{rr: nnreal | rr < pi}" trig_approx"trig_fnd/" )nil interval nil )nil reals nil )"real" integral_def "analysis/" )"real" atan "trig_fnd/" )nil trig_approx "trig_fnd/" )"bool" real_fun_preds "reals/" )"Interval" interval_trig nil )nil trig_approx "trig_fnd/" )nil real_props nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )"real" trig_approx "trig_fnd/" )nil real_types nil )nil real_types nil )nil real_props nil )"odd_int" integers nil )"real" reals nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )nil extra_tegies nil )nil extra_tegies nil )nil extra_tegies nil )NOT const-decl "[bool -> bool]" booleans nil )"real" trig_approx "trig_fnd/" )nil trig_approx "trig_fnd/" )nil trig_approx "trig_fnd/" )"real" trig_approx "trig_fnd/" )nil real_props nil )"[bool, bool -> bool]" booleans nil )"bool" interval nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil interval nil )"real" trig_approx "trig_fnd/" )"(strict_total_order?[real])" real_props nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil interval nil )nil trig_approx "trig_fnd/" )nil trig_approx "trig_fnd/" )nil trig_approx "trig_fnd/" )"even_int" integers nil )nil trig_approx"trig_fnd/" )"bool" real_fun_preds "reals/" )nil trig_approx "trig_fnd/" )"nat" exponentiation nil )"posint" nil )"posrat" nil )"real" reals nil )"posreal" atan_approx "trig_fnd/" )nil atan_approx "trig_fnd/" )"nat" interval_trig nil )"real" atan_approx "trig_fnd/" )"posreal" nil )"posreal" atan_approx "trig_fnd/" )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"bool" interval nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"Interval" interval nil )nil trig_ineq "trig_fnd/" )"trig_range" sincos_def"trig_fnd/" )nil trig_approx "trig_fnd/" )nil trig_approx "trig_fnd/" ))nil 3559394623"" case "NOT FORALL (X: Interval, n: nat): AND ") "1" (hide 2)"1" (skeep)"1" (expand "Tan" )"1" (ground)"1" (expand "tan_0_pi2" )"1" (invoke (case "%1" ) (! 1 1))"1" (flatten)"1" (assert )"1" (expand "[||]" )"1" (expand "Proper?" )"1" case "FORALL (a,c:nnreal,b,d:posreal): a<=c AND b>=d IMPLIES a/b<=c/d" )"1" (inst?)"1" (assert )"1" "1" "sin_bounds" )"1" "1" "lb(X)" "5+n" )"1" "ub(X)" "5+n" )"1" "1" "sin_increasing" )"1" "ub(X)" "lb(X)" )"1" assert )"1" expand "<<" )"1" "1" "pi_lb_est_le" )"1" "5+n" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "cos_bounds" )"2" "lb(X)" "5+n" )"2" "ub(X)" "5+n" )"2" "2" "cos_decreasing" )"2" "ub(X)" "lb(X)" )"2" assert )"2" expand "<<" )"2" "2" "pi_lb_est_le" )"2" "5+n" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "sin_ub_increasing" )"2" "5+n" )"2" expand "strict_increasing?" )"2" "0" "ub(X)" )"1" assert )"1" "sin_ub_a0" )"1" "1" assert )"1" expand "<<" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "<<" )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "sin_lb_increasing" )"3" "5+n" )"3" expand "strict_increasing?" )"3" "0" "lb(X)" )"1" assert )"1" "sin_lb_a0" )"1" "5+n" )"1" assert )"1" expand "<<" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "<<" )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skeep)"2" "2" (cross-mult 1) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (split +)"1" (lemma "cos_bounds" )"1" (inst?)"1" (flatten)"1" (lemma "cos_gt_0" )"1" (inst?)"1" assert )"1" "pi_lb_est_le" )"1" "5+n" )"1" "1" expand "<<" )"1" expand "[||]" )"1" "1" assert )"1" expand "Proper?" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "cos_lb_nn_strict_decreasing" )"2" (inst - "5+n" )"2" (expand "strict_decreasing?" )"2" (inst - "ub(X)" "pi_lbn(5+n)/2" )"1" (lemma "pi_lb_est_le" )"1" "5+n" )"1" "1" assert )"1" expand "<<" )"1" expand "[||]" )"1" "1" assert )"1" expand "Proper?" )"1" "cos_lb_pi2_pos" )"1" "5+n" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "pi_bounds" )"2" "2" (ground) nil nil ))nil ))nil )"3" (expand "Proper?" )"3" "pi_lb_est_le" )"3" "5+n" )"3" "3" assert )"3" expand "<<" )"3" expand "[||]" )"3" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOT FORALL (X: Interval, n: nat): AND OR X << [| -pi_lb_est(n + 5) / 2,0 |])") "1" (hide 2)"1" (skeep)"1" (inst-cp - "X" "n" )"1" (assert )"1" (assert )"1" (expand "Tan" 1)"1" (inst - "Neg(X)" "n" )"1" (assert )"1" (invoke (case "%1" ) (! -3 1))"1" (flatten)"1" (assert )"1" (expand "Tan" )"1" "tan_0_pi2" "pi_lb_est" ))nil nil ))nil ))nil ))nil )"2" (hide -3)"2" "tan_0_pi2" "pi_lb_est" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (inst-cp - "X" "n" )"2" (hide -3)"2" (assert )"2" (flatten)"2" (expand "Tan" )"2" (assert )"2" (rewrite "tan_npi2_pi2_union" )"1" case "NOT FORALL (XX,YY:Interval): Proper?(YY) IMPLIES Proper?(Union(XX,YY))" )"1" (hide-all-but 1) (("1" (grind) nil nil ))nil )"2" (inst?)"2" (assert )"2" (hide 4)"2" "Intersection(X, [| 0, pi_lb_est(5 + n) / 2 |])" "n" )"2" assert )"2" "1" (propax) nil nil )"2" "2" "2" "tan_0_pi2" "pi_lb_est" ))nil nil ))nil ))nil )"3" "3" "tan_0_pi2" "pi_lb_est" ))nil nil ))nil )"4" "4" "4" "tan_0_pi2" "pi_lb_est" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" "tan_0_pi2" "pi_lb_est" "tan_npi2_pi2" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )OR const-decl "[bool, bool -> bool]" booleans nil )"Interval" interval nil )nil interval_trig nil )"int" integers nil )"Interval" interval nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"Interval" interval nil )"bool" interval nil )"real" reals nil )"Interval" interval_trig nil )nil trig_approx"trig_fnd/" )"bool" real_fun_preds "reals/" )nil atan_approx "trig_fnd/" )"posreal" atan_approx "trig_fnd/" )nil trig_approx "trig_fnd/" )"real" atan_approx "trig_fnd/" )nil trig_ineq "trig_fnd/" )"bool" reals nil )nil trig_approx "trig_fnd/" )nil trig_approx "trig_fnd/" )nil trig_approx "trig_fnd/" )"bool" real_fun_preds "reals/" )"(strict_total_order?[real])" real_props nil )nil trig_approx "trig_fnd/" )"[numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )nil trig_approx "trig_fnd/" )"trig_range" sincos_def"trig_fnd/" )nil trig_ineq "trig_fnd/" )nil trig_approx "trig_fnd/" )nil trig_approx "trig_fnd/" )"posreal" atan_approx "trig_fnd/" )"trig_range" sincos_def"trig_fnd/" )"posreal" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"nzreal" nil )"nzreal" real_typesnil )nil trig_ineq "trig_fnd/" )"real" trig_approx "trig_fnd/" )"nat" interval_trig nil )"Interval" interval_trig nil )"real" trig_approx "trig_fnd/" )"(total_order?[real])" nil )nil reals nil )nil real_props nil )nil real_props nil )nil real_props nil )nil extra_real_props nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"nnreal" nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"real" trig_approx "trig_fnd/" )"real" trig_approx "trig_fnd/" )"real" reals nil )"posint" nil )"posint" nil )"nnreal" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil interval nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" interval nil )"bool" interval nil )"Interval" interval nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan "trig_fnd/" )"{rr: nnreal | rr < pi}" trig_approx"trig_fnd/" )"[numfield, numfield -> numfield]" number_fields nil )"Interval" interval_trig nil ))nil 3559665648"" (skeep)"" (expand "Atan" )"" (lemma "atan_lb_increasing" )"" (lemma "atan_ub_increasing" )"" (inst - "n" )"" (inst - "n" )"" (expand "increasing?" )"" (inst - "ub(X)" "ub(Y)" )"" (inst - "lb(Y)" "lb(X)" )"" (assert )"" (expand "<<" )"" (expand "[||]" ) (("" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"Interval" interval_trig nil )nil atan_approx "trig_fnd/" )nil interval nil )"(total_order?[real])" nil )"Interval" interval nil )"bool" interval nil )"bool" real_fun_preds "reals/" )nil naturalnumbers nil )"bool" reals 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 )nil booleans nil )nil numbers nil )nil atan_approx "trig_fnd/" ))nil 3306165185"" (skeep)"" (expand "Pi" )"" (expand "##" )"" (expand "[||]" )"" (lemma "pi_bounds" )"" (inst?) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"(Pos?)" interval_trig nil )"Interval" interval 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 booleans nil )"bool" reals nil )nil naturalnumbers nil )"posreal" atan_approx "trig_fnd/" )"(strict_total_order?[real])" real_props nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"posreal" atan_approx "trig_fnd/" )"(total_order?[real])" nil )nil atan_approx "trig_fnd/" )"bool" interval nil ))nil 3567426319"" (skeep)"" (lemma "Pi_inclusion" )"" (inst? -1)"" (lemma "Member_Proper" )"" (inst? -1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil interval_trig nil )nil interval nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"posreal" atan "trig_fnd/" )nil real_types nil )"bool" reals nil )nil real_types nil )"(Pos?)" interval_trig nil )"bool" interval nil )nil interval nil )nil naturalnumbers nil )"bool" reals 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 )nil booleans nil )nil numbers nil ))nil ))nil 3321631707"" (skeep)"" (expand "<<" )"" (flatten)"" (expand "sin_npi2_pi2" )"" (assert )"" (expand "##" )"" (assert )"" (lemma "sin_bounds" )"" (inst-cp -1 "ub(X)" "n" )"" (inst -1 "lb(X)" "n" )"" (grind-reals)"1" (lemma "sin_incr" )"1" (inst -1 "ub(X)" "x" )"1" (assert )"1" "pi_bounds" )"1" "1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "sin_incr" )"2" (inst -1 "x" "lb(X)" )"2" (assert )"2" "pi_bounds" )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" atan_approx "trig_fnd/" )"nzreal" real_typesnil )"bool" interval nil )"Interval" interval_trig nil )"bool" interval nil )nil trig_approx "trig_fnd/" )nil trig_ineq "trig_fnd/" )"(total_order?[real])" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )nil real_props nil )"posreal" atan_approx "trig_fnd/" )nil atan_approx "trig_fnd/" )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil real_props nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil interval nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil interval nil )nil interval nil )"(total_order?[real])" nil )"nzreal" nil )"posreal" nil )"trig_range" sincos_def"trig_fnd/" ))nil ))nil 3321631733"" (skeep)"" (expand * "<<" "##" "sin_pi2_pi" )"" (assert )"" (flatten)"" (split)"1" (case "sin(ub(X)) <= sin(x)" )"1" (lemma "sin_bounds" )"1" (inst -1 "ub(X)" "n" ) (("1" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" (grind-reals)"2" (lemma "sin_decr" )"2" (inst -1 "ub(X)" "x" )"2" (assert )"2" (lemma "pi_bounds" )"2" (inst?)"2" (flatten) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "sin(x)<= sin(lb(X))" )"1" (lemma "sin_bounds" )"1" (inst -1 "lb(X)" "n" ) (("1" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" (lemma "sin_decr" )"2" (inst -1 "x" "lb(X)" )"2" (assert )"2" (lemma "pi_bounds" )"2" (inst?)"2" (flatten) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" interval nil )"Interval" interval_trig nil )"posreal" atan_approx "trig_fnd/" )"bool" interval nil )nil interval nil )"real" sincos_def "trig_fnd/" )"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 naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil trig_approx "trig_fnd/" )nil real_props nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil atan_approx "trig_fnd/" )nil real_props nil )nil real_props nil )"posreal" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"(total_order?[real])" nil )nil trig_ineq "trig_fnd/" )nil interval nil )nil interval nil )"(total_order?[real])" nil )"posreal" nil )"posreal" atan_approx "trig_fnd/" )"trig_range" sincos_def"trig_fnd/" ))nil ))nil 3312224255"" (skeep)"" (expand * "<<" "##" "sin_0_pi" )"" (flatten)"" (assert )"" (split)"1" (case "x <= pi/2" )"1" (case "sin_lb(lb(X),n) <= sin(x)" )"1" (expand "min" )"1" (lift-if) (("1" (assert ) nil nil )) nil )) nil )"2" (hide 2)"2" (lemma "sin_bounds" )"2" (inst -1 "lb(X)" "n" )"2" (assert )"2" (flatten)"2" (hide -2)"2" (case "sin(lb(X)) <= sin(x)" )"1" (assert ) nil nil )"2" "2" "sin_incr" )"2" "x" "lb(X)" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "sin_lb(ub(X), n) <= sin(x)" )"1" (expand "min" )"1" (lift-if) (("1" (assert ) nil nil )) nil )) nil )"2" (hide 3)"2" (lemma "sin_bounds" )"2" (inst -1 "ub(X)" "n" )"2" (assert )"2" (flatten)"2" (case "sin(ub(X)) <= sin(x)" )"1" (assert ) nil nil )"2" (hide -1 -2 2)"2" "sin_decr" )"2" "ub(X)" "x" )"2" assert )"2" "pi_bounds" )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"bool" interval nil )"Interval" interval_trig nil )"bool" interval nil )"trig_range" sincos_def"trig_fnd/" )"posreal" atan_approx "trig_fnd/" )"(total_order?[real])" nil )nil interval nil )nil interval nil )"posreal" atan "trig_fnd/" )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" nil )nil trig_ineq "trig_fnd/" )"nzreal" real_typesnil )"nzreal" nil )"(total_order?[real])" nil )nil trig_approx "trig_fnd/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"(strict_total_order?[real])" real_props nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"real" sincos_def "trig_fnd/" )nil interval nil )"real" trig_approx "trig_fnd/" )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil atan_approx "trig_fnd/" )"(strict_total_order?[real])" real_props nil )"posreal" atan_approx "trig_fnd/" )"posreal" nil )nil trig_ineq "trig_fnd/" ))nil ))nil 3312226151"" (skeep)"" (case-replace "sin(x)=--sin(x)" )"1" (hide -1)"1" (rewrite "Neg_inclusion" )"1" (hide 2)"1" (lemma "sin_neg" )"1" (inst -1 "x" )"1" (replaces -1 :dir rl)"1" (rewrite "sin_0_pi" )"1" (hide -2 2)"1" (lemma "Neg_Incl" )"1" (inst? -1 :where -2)"1" (assert )"1" (rewrite "Neg_interval" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (rewrite "Neg_inclusion" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"trig_range" sincos_def"trig_fnd/" )"real" reals nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" sincos_def "trig_fnd/" )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"posreal" atan_approx "trig_fnd/" )nil interval nil )nil interval nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"Interval" interval_trig nil )"Interval" interval nil )"nzreal" real_typesnil )nil trig_basic "trig_fnd/" )"real" atan_approx "trig_fnd/" )"Interval" interval nil )nil interval nil )"even_int" integers nil )nil interval nil )nil interval_trig nil ))nil ))nil 3320434600"" (skeep)"" (case-replace "sin(x)=--sin(x)" )"1" (hide -1)"1" (rewrite "Neg_inclusion" )"1" (hide 2)"1" (lemma "sin_neg" )"1" (inst -1 "x" )"1" (replaces -1 :dir rl)"1" (rewrite "sin_pi2_pi" )"1" (hide -2 2)"1" (lemma "Neg_Incl" )"1" (inst? -1 :where -2)"1" (assert )"1" (rewrite "Neg_interval" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (rewrite "Neg_inclusion" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"trig_range" sincos_def"trig_fnd/" )"real" reals nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" sincos_def "trig_fnd/" )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"nzreal" real_typesnil )"posreal" atan_approx "trig_fnd/" )"posreal" atan_approx "trig_fnd/" )nil interval nil )nil interval nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"Interval" interval_trig nil )"Interval" interval nil )"nzreal" nil )nil trig_basic "trig_fnd/" )"real" atan_approx "trig_fnd/" )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"real" atan_approx "trig_fnd/" )"Interval" interval nil )nil interval nil )nil interval nil )"posreal" nil )nil interval_trig nil ))nil ))nil 3312234582"" (skeep)"" (expand * "<<" "##" "cos_0_pi" "cos_0_pi2" )"" (flatten)"" (split 1)"1" (case "cos(ub(X)) <= cos(x)" )"1" (lemma "cos_bounds" )"1" (inst -1 "ub(X)" "n" ) (("1" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" (lemma "cos_decr" )"2" (inst -1 "ub(X)" "x" )"2" (assert )"2" (lemma "pi_bounds" )"2" (inst?)"2" (flatten) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "cos(x) <= cos(lb(X))" )"1" (lemma "cos_bounds" )"1" (inst -1 "lb(X)" "n" ) (("1" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" (lemma "cos_decr" )"2" (inst -1 "x" "lb(X)" )"2" (assert )"2" (lemma "pi_bounds" )"2" (inst?)"2" (flatten) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" interval nil )"Interval" interval_trig nil )"bool" interval nil )nil atan_approx "trig_fnd/" )"(strict_total_order?[real])" real_props nil )"posreal" atan_approx "trig_fnd/" )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"(total_order?[real])" nil )nil trig_ineq "trig_fnd/" )nil trig_approx "trig_fnd/" )nil interval nil )nil interval nil )"posreal" atan_approx "trig_fnd/" )"trig_range" sincos_def"trig_fnd/" )"(total_order?[real])" nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals 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 )"real" sincos_def "trig_fnd/" )nil interval nil ))nil ))nil 3579704427"" (skeep)"" (lemma "cos_0_pi" )"" (inst -1 "Neg(X)" "n" "-x" )"" (assert )"" (rewrite "cos_neg" )"" (expand "cos_0_pi" )"" (assert )"" (hide 2)"" (expand "<<" )"" (flatten)"" (expand "Neg" )"" (assert )"" (expand "##" )"" (flatten) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil interval_trig nil )"trig_range" sincos_def"trig_fnd/" )"posreal" atan_approx "trig_fnd/" )"nzreal" real_typesnil )"Interval" interval_trig nil )"(total_order?[real])" nil )nil interval nil )nil interval nil )"bool" interval nil )"bool" interval nil )nil trig_basic "trig_fnd/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"Interval" interval nil )nil interval nil )nil reals nil )"real" reals nil ))nil ))nil 3305037654"" (skeep)"" (expand "<<" )"" (flatten)"" (expand "cos_npi2_pi2" )"" (expand "##" )"" (flatten)"" (split)"1" (case "x >= 0" )"1" (case "cos_lb(ub(X),n) <= cos(x)" )"1" (expand "min" )"1" (lift-if) (("1" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (lemma "cos_bounds" )"2" (inst -1 "ub(X)" "n" )"2" (flatten)"2" (case "cos(ub(X)) <= cos(x)" )"1" (assert ) nil nil )"2" "2" "cos_decr" )"2" "ub(X)" "x" )"2" assert )"2" "pi_bounds" )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "cos_lb(lb(X),n) <= cos(x)" )"1" (expand "min" )"1" (lift-if) (("1" (assert ) nil nil )) nil ))nil )"2" (hide 3)"2" (lemma "cos_bounds" )"2" (inst -1 "lb(X)" "n" )"2" (flatten)"2" (case "cos(lb(X))<=cos(x)" )"1" (assert ) nil nil )"2" "2" "cos_decr" )"2" "-x" "-lb(X)" )"2" rewrite "cos_neg" )"2" rewrite "cos_neg" )"2" assert )"2" "pi_bounds" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" atan_approx "trig_fnd/" )"nzreal" real_typesnil )"bool" interval nil )"Interval" interval_trig 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 trig_ineq "trig_fnd/" )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"posreal" atan_approx "trig_fnd/" )"(strict_total_order?[real])" real_props nil )nil atan_approx "trig_fnd/" )nil trig_approx "trig_fnd/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil interval nil )nil interval nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"nzreal" nil )"(total_order?[real])" nil )"trig_range" sincos_def"trig_fnd/" )"(total_order?[real])" nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"real" trig_approx "trig_fnd/" )nil interval nil )"real" sincos_def "trig_fnd/" )nil trig_basic "trig_fnd/" )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"real" reals nil )"bool" interval nil ))nil ))nil 3304702817"" (skeep)"" (expand "Cos" )"" (lift-if)"" (bddsimp)"1" (rewrite "cos_0_pi" )"1" (hide 2)"1" (grind :exclude ("pi_lbn" "^" )) nil nil )) nil ))nil )"2" (rewrite "cos_npi_0" )"2" (hide (2 3))"2" (grind :exclude ("pi_lbn" "^" )) nil nil )) nil ))nil )"3" (rewrite "cos_npi2_pi2" )"3" (hide (2 3 4))"3" (grind :exclude ("pi_lbn" "^" )) nil nil )) nil ))nil )"4" (hide-all-but 4)"4" (assert )"4" (typepred "cos(x)" )"4" (expand "##" ) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"posrat" nil )"Interval" interval_trig nil )"posint" nil )"nat" exponentiation nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"Interval" interval nil )"bool" interval nil )"bool" interval nil )"{rr: nnreal | rr < pi}" trig_approx"trig_fnd/" )"real" reals nil )"odd_int" integers nil )"posreal" atan_approx "trig_fnd/" )"trig_range" sincos_def"trig_fnd/" )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil interval nil )nil reals nil )nil interval_trig nil )"nzreal" real_typesnil )nil interval_trig nil )"nzreal" nil )"posreal" nil )"real" reals nil )"nnreal" nil )nil interval_trig nil )"even_int" integersnil )"rat" rationals nil )nil interval nil )nil interval nil )"real" sincos_def "trig_fnd/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3304702653"" (expand "Sin" )"" (skeep)"" (name "Xpos" "Intersection(X, [| 0, ub(X) |])" )"" (replace -1)"" (name "Xneg" "Intersection(X, [| lb(X), 0 |])" )"" (replace -1)"" "piint" "[| -pi_ubn(n) / 2, -pi_lbn(n) / 2 |]" )"" (replace -1)"" (case "x>=0" )"1" (case "x ## Xpos" )"1" (assert )"1" (case "Proper?(Xpos)" )"1" (assert )"1" case "sin(x) ## Cos(n)(Add(Xpos, piint))" )"1" "1" "cos" "Cos" "sin" "Sin" "pi_lbn" "pi_ubn" "pi" ))nil nil ))nil )"2" "2" rewrite "sin_cos" )"2" "cos_neg" )"2" "pi/2+x" )"2" "2" rewrite "neg_cos" )"2" assert )"2" rewrite "cos_neg" "2" assert )"2" case "NOT -(-(pi / 2 + x) + pi) = x-pi/2" )"1" assert )nil nil )"2" "2" "Cos_inclusion" )"2" "2" assert )"2" "pi_bounds" )"2" "n" )"2" "2" "cos" "Cos" "sin" "Sin" "pi_lbn" "pi_ubn" "pi" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (hide-all-but (-1 1))"2" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (hide-all-but (-1 -5 1))"2" (expand "Xpos" ) (("2" (grind) nil nil ))nil ))nil ))nil )"2" (case "Proper?(Xneg)" )"1" (assert )"1" case "sin(x) ## Neg(Cos(n)(Add(Neg(Xneg), piint)))" )"1" (hide-all-but (-1 +))"1" "cos" "Cos" "sin" "Sin" "pi_lbn" "pi_ubn" "pi" ))nil nil ))nil )"2" (hide 3)"2" (rewrite "sin_cos" )"2" rewrite "Neg_inclusion" )"2" "2" rewrite "cos_neg" :dir rl)"2" "Cos_inclusion" )"2" "2" assert )"2" "2" "pi_bounds" )"2" "n" )"2" "2" "cos" "Cos" "sin" "Sin" "pi_lbn" "pi_ubn" "pi" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "x ## Xneg" )"1" (hide-all-but (-1 1))"1" (grind) nil nil )) nil )"2" (hide 4)"2" (hide -1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" atan_approx "trig_fnd/" )"nzreal" real_typesnil )nil interval nil )"real" sincos_def "trig_fnd/" )"bool" interval nil )"bool" interval nil )"real" sincos_def "trig_fnd/" )"Interval" interval_trig nil )"Interval" interval nil )"Interval" interval nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"Interval" interval nil )"real" reals nil )"(total_order?[real])" nil )"real" reals nil )nil trig_basic "trig_fnd/" )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"posreal" nil )"trig_range" sincos_def"trig_fnd/" )"posreal" atan "trig_fnd/" )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )nil trig_basic "trig_fnd/" )"real" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil interval_trig nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil atan_approx "trig_fnd/" )nil trig_basic "trig_fnd/" )"(total_order?[real])" nil )"posreal" atan_approx "trig_fnd/" )"trig_range" sincos_def"trig_fnd/" )"Interval" interval_trig nil )"nzreal" nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"real" atan_approx "trig_fnd/" )"real" atan_approx "trig_fnd/" )nil reals nil )nil interval nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"Interval" interval nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"Interval" interval nil )"Interval" interval_trig nil ))nil ))nil 3321636958"" (skeep)"" (expand * "##" "<<" )"" (flatten)"" (lemma "pi_bounds" )"" (inst?)"" (flatten)"" (assert ) (("" (rewrite "tan_pi2_def" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" interval nil )"nzreal" real_typesnil )"posreal" atan_approx "trig_fnd/" )"bool" interval nil )nil atan_approx "trig_fnd/" )nil trig_ineq "trig_fnd/" )nil interval nil )nil interval nil )"(strict_total_order?[real])" real_props nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"posreal" atan_approx "trig_fnd/" )"(total_order?[real])" nil )"nzreal" nil )"posreal" nil )nil naturalnumbers nil )"bool" reals 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 )nil booleans nil )nil numbers nil ))nil ))nil 3321632423"" (skeep)"" (case "x=0" )"1" (replaces -1)"1" (hide -1)"1" (rewrite "cos_lb_a0" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (lemma "cos_lb_pi2_pos" )"2" (inst?)"2" (assert )"2" (lemma "cos_lb_nn_strict_decreasing" )"2" (inst -1 "n" )"2" (expand "strict_decreasing?" )"2" (inst -1 "x" "pi_lbn(n)/2" )"1" (assert )"1" (expand "##" ) (("1" (assert ) nil nil ))nil ))nil )"2" (lemma "pi_bounds" )"2" (inst?)"2" (flatten) (("2" (assert ) nil nil )) nil ))nil ))nil )"3" (expand "##" )"3" (flatten)"3" (assert )"3" (lemma "pi_bounds" )"3" (inst?)"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil trig_approx "trig_fnd/" )"posreal" atan_approx "trig_fnd/" )nil trig_approx"trig_fnd/" )"bool" real_fun_preds "reals/" )nil atan_approx "trig_fnd/" )"posreal" atan_approx "trig_fnd/" )"(strict_total_order?[real])" real_props nil )nil interval nil )nil interval nil )"bool" interval nil )nil real_types nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" atan_approx "trig_fnd/" )"nat" interval_trig nil )"posreal" atan "trig_fnd/" )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"real" interval_trig nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"posreal" nil )nil trig_approx "trig_fnd/" ))nil 3321635963"" (skeep)"" (case "x > 0" )"1" (lemma "cos_lb_gt_0_pos" )"1" (inst?)"1" (assert )"1" (hide-all-but (-2 1))"1" (expand "##" ) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"2" (lemma "cos_lb_gt_0_pos" )"2" (inst -1 "n" "-x" )"2" (rewrite "cos_lb_neg" )"2" (assert )"2" (hide-all-but (-1 1))"2" (expand "##" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil interval nil )nil interval nil )"(total_order?[real])" nil )"bool" interval nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"nzreal" real_typesnil )"posreal" atan_approx "trig_fnd/" )"posreal" nil )"(total_order?[real])" nil )nil interval_trig nil )"real" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil trig_approx "trig_fnd/" ))nil 3304702463"" (skeep)"" (lemma "cos_bounds" )"" (inst? -1)"" (expand "##" ) (("" (flatten) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil trig_approx "trig_fnd/" )"posreal" atan_approx "trig_fnd/" )"nzreal" real_typesnil )"bool" interval nil )nil interval nil )nil interval nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"nzreal" nil )"trig_range" sincos_def"trig_fnd/" )"(total_order?[real])" nil )nil naturalnumbers nil )"bool" reals 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 )nil booleans nil )nil numbers nil ))nil ))nil 3321637451"" (skeep)"" (expand * "Proper?" "<<" )"" (flatten)"" (assert )"" (splash 1)"1" (rewrite "cos_ub_gt_0" )"1" (expand "##" ) (("1" (assert ) nil nil )) nil )) nil )"2" (rewrite "cos_ub_gt_0" )"2" (expand "##" ) (("2" (assert ) nil nil )) nil )) nil )"3" (rewrite "cos_lb_gt_0" )"3" (expand "##" ) (("3" (assert ) nil nil )) nil )) nil )"4" (rewrite "cos_lb_gt_0" )"4" (expand "##" ) (("4" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" interval nil )"nzreal" real_typesnil )"posreal" atan_approx "trig_fnd/" )"bool" interval nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posreal" nil )"nzreal" nil )"(total_order?[real])" nil )nil interval nil )nil interval nil )nil interval_trig nil )nil interval_trig nil )"bool" interval nil )"real" trig_approx "trig_fnd/" )nil interval nil )"real" trig_approx "trig_fnd/" )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals 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 3318076124"" (skeep)"" (lemma "Tan_pi2_def" )"" (inst?)"" (inst?)"" (expand "<<" )"" (assert ) (("" (flatten) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil interval_trig nil )"nzreal" real_typesnil )"posreal" atan_approx "trig_fnd/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"posreal" nil )"nzreal" nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil interval nil )nil interval nil )"bool" interval nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil interval nil )nil reals nil ))nil ))nil 3304702837"" (skeep)"" (lemma "cos_lb_ub_gt_0" )"" (inst -1 "X" "n" )"" (case "Proper?(X)" )"1" (expand * "<<" "##" "tan_0_pi2" )"1" (assert )"1" (flatten)"1" (assert )"1" (flatten)"1" (split)"1" (lift-if)"1" (split)"1" (flatten)"1" (lemma "tan_bounds_0_pi2" )"1" "lb(X)" "n" )"1" "1" "1" expand "tan_lb_ub" )"1" "tan_incr" )"1" "x" "lb(X)" )"1" assert )"1" assert )"1" "pi_bounds" )"1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil )"3" "pi_bounds" )"3" "3" "3" (assert ) nil nil ))nil ))nil ))nil )"4" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (lift-if)"2" (split 1)"1" (flatten)"1" (lemma "tan_bounds_0_pi2" )"1" "ub(X)" "n" )"1" "1" "1" expand "tan_ub_lb" )"1" "tan_incr" )"1" "ub(X)" "x" )"1" assert )"1" assert )"1" "pi_bounds" )"1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" "pi_bounds" )"3" "3" "3" (assert ) nil nil ))nil ))nil ))nil )"4" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (lemma "Member_Proper" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil interval_trig nil )"bool" interval nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"nzreal" nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil interval nil )nil interval nil )nil tan_approx "trig_fnd/" )"real" tan_approx "trig_fnd/" )"posreal" atan_approx "trig_fnd/" )nil atan_approx "trig_fnd/" )"(strict_total_order?[real])" real_props nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )nil trig_ineq "trig_fnd/" )"real" tan_approx "trig_fnd/" )"bool" interval nil )"nzreal" real_typesnil )"posreal" atan_approx "trig_fnd/" )"Interval" interval_trig nil )"bool" interval nil )nil interval nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil interval nil )nil reals nil ))nil ))nil 3318077125"" (skeep)"" (lemma "Tan_pi2_def" )"" (inst?)"" (inst?)"" (expand "<<" )"" (assert ) (("" (flatten) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil interval_trig nil )"posreal" atan_approx "trig_fnd/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"posreal" nil )"nzreal" nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil interval nil )nil interval nil )"bool" interval nil )"nzreal" real_typesnil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil interval nil )nil reals nil ))nil ))nil 3579704469"" (skeep)"" (lemma "tan_0_pi2" )"" (inst -1 "Neg(X)" "n" "-x" )"" (rewrite "tan_neg" )"" (split)"1" (lemma "Neg_inclusion" )"1" (inst -1 "tan_0_pi2(n)(Neg(X))" "-tan(x)" )"1" (assert ) nil nil )) nil ))nil )"2" (hide-all-but (-1 1))"2" (expand "<<" )"2" (expand "Neg" )"2" (flatten) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil )"3" (propax) nil nil )"4" (rewrite "Neg_inclusion" ) nil nil ))nil ))nil ))nil ))nil ))nil )nil interval_trig nil )"bool" sincos_def "trig_fnd/" )nil trig_basic "trig_fnd/" )"posreal" atan_approx "trig_fnd/" )"nzreal" real_typesnil )nil interval nil )nil interval nil )"posreal" nil )"(total_order?[real])" nil )"bool" interval nil )nil interval nil )"(total_order?[real])" nil )"nzreal" nil )"Interval" interval_trig nil )"real" sincos_def "trig_fnd/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"Interval" interval nil )nil interval nil )nil reals nil )"real" reals nil ))nil ))nil 3318077435"" (skeep)"" (lemma "Tan_pi2_def" )"" (inst?) (("" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil interval_trig nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"(total_order?[real])" nil )"nzreal" nil )"nzreal" real_typesnil )"posreal" atan_approx "trig_fnd/" )"posreal" nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil interval nil )nil reals nil ))nil ))"" 3545778271"" (skeep)"" (expand "Zeroin?" )"" (lemma "cos_lb_ub_gt_0" )"" (inst -1 "X" "n" )"" (case "Proper?(X)" )"1" (expand * "<<" "##" )"1" (assert )"1" (flatten)"1" (assert )"1" (flatten)"1" (expand "tan_npi2_pi2" )"1" (assert )"1" (split)"1" (lemma "tan_bounds_npi2_0" )"1" "lb(X)" "n" )"1" "1" "1" expand "tan_lb_lb" )"1" case "tan(lb(X)) <= tan(x)" )"1" (assert ) nil nil )"2" "2" "tan_incr" )"2" "x" "lb(X)" )"2" assert )"2" assert )"2" "pi_bounds" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "pi_bounds" )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil )"4" (propax) nil nil ))nil ))nil ))nil )"2" (lemma "tan_bounds_0_pi2" )"2" "ub(X)" "n" )"2" "1" "1" expand "tan_ub_lb" )"1" case "tan(x) <= tan(ub(X))" )"1" (assert ) nil nil )"2" "2" "tan_incr" )"2" "ub(X)" "x" )"2" assert )"2" assert )"2" "pi_bounds" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" assert )"3" "pi_bounds" )"3" "3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (lemma "Member_Proper" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" interval nil )nil reals nil )nil interval nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil interval nil )"bool" interval nil )"posreal" atan_approx "trig_fnd/" )"nzreal" real_typesnil )"bool" interval nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil tan_approx "trig_fnd/" )"real" tan_approx "trig_fnd/" )nil tan_approx "trig_fnd/" )"real" tan_approx "trig_fnd/" )"posreal" atan_approx "trig_fnd/" )nil atan_approx "trig_fnd/" )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )nil trig_ineq "trig_fnd/" )"real" sincos_def "trig_fnd/" )"bool" sincos_def "trig_fnd/" )"bool" reals nil )"Interval" interval_trig nil )nil interval nil )nil interval nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"nzreal" nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"bool" interval nil )nil interval_trig nil ))nil )"" 3320522103"" (skeep)"" (lemma "cos_lb_ub_gt_0" )"" (inst -1 "X" "n" )"" (case "Proper?(X)" )"1" (expand * "<<" "##" )"1" (assert )"1" (flatten)"1" (assert )"1" (flatten)"1" (expand "tan_npi2_pi2" )"1" (assert )"1" (split)"1" (lemma "tan_bounds_npi2_0" )"1" (inst -1 "lb(X)" "n" )"1" "1" "1" expand "tan_lb_lb" )"1" case "tan(lb(X)) <= tan(x)" )"1" (assert ) nil nil )"2" "2" "tan_incr" )"2" "x" "lb(X)" )"2" assert )"2" assert )"2" "pi_bounds" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "pi_bounds" )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil )"4" (propax) nil nil ))nil ))nil ))nil )"2" (lemma "tan_bounds_0_pi2" )"2" (inst -1 "ub(X)" "n" )"2" "1" "1" expand "tan_ub_lb" )"1" case "tan(x) <= tan(ub(X))" )"1" (assert ) nil nil )"2" "2" "tan_incr" )"2" "ub(X)" "x" )"2" assert )"2" assert )"2" "pi_bounds" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" assert )"3" "pi_bounds" )"3" "3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (lemma "Member_Proper" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" interval nil )nil interval nil )nil interval nil )"bool" sincos_def "trig_fnd/" )"real" sincos_def "trig_fnd/" )nil trig_ineq "trig_fnd/" )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )nil atan_approx "trig_fnd/" )"posreal" atan_approx "trig_fnd/" )"real" tan_approx "trig_fnd/" )nil tan_approx "trig_fnd/" )"real" tan_approx "trig_fnd/" )nil tan_approx "trig_fnd/" )"bool" interval nil )"posreal" atan_approx "trig_fnd/" )nil interval nil )nil interval nil ))nil ))nil 3567426319 ("" (subtype-tcc) nil nil ) nil nil ))nil 3567449799"" (skeep)"" (expand "TAN?" )"" (lemma "pi_lb_est_le" )"" (inst?)"" (flatten)"" (lemma "Tan_pi2_def" )"" (inst? -1)"" (inst? -1)"" (assert )"" (hide-all-but (-3 1))"" (grind :exclude ("pi_lb_est" "pi_lbn" )) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" interval_trig nil )"(total_order?[real])" nil )"int" integers nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil interval_trig nil )"nzreal" real_typesnil )"posreal" atan_approx "trig_fnd/" )"Interval" interval nil )"bool" interval nil )"(total_order?[real])" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"real" reals nil )"real" reals nil )"nnreal" nil )"nzreal" nil )"posreal" nil )nil interval nil )nil trig_approx "trig_fnd/" ))nil )nil 3567449719 ("" (postpone) nil nil ) nil shostak))nil 3302520141"" (skeep)"" (lemma "TAN_Tan" )"" (inst?) (("" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil interval_trig nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil interval nil )nil reals nil ))nil ))nil 3567451111"" (skeep)"" (expand "Tan" )"" (case "X << [|0, pi_lb_est(5 + n) / 2|]" )"1" (assert )"1" (rewrite "tan_0_pi2" )"1" (lemma "pi_lb_est_le" )"1" (inst?)"1" (flatten)"1" (expand "<<" )"1" (expand "[||]" ) (("1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace 1)"2" (case "X << [|-pi_lb_est(5 + n) / 2, 0|]" )"1" (assert )"1" (rewrite "tan_npi2_0" )"1" (lemma "pi_lb_est_le" )"1" (inst?)"1" (expand "<<" )"1" (expand "[||]" )"1" (flatten) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "TAN?" )"2" (assert )"2" (rewrite "tan_npi2_pi2" )"1" (lemma "pi_lb_est_le" )"1" (inst?)"1" (expand "<<" )"1" (expand "[||]" )"1" (flatten) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-2 4))"2" (grind :exclude "pi_lb_est" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"Interval" interval_trig nil )"bool" interval_trig nil )nil interval_trig nil )"bool" interval nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"nzreal" real_typesnil )nil interval_trig nil )"[numfield -> numfield]" number_fields nil )"real" reals nil )nil trig_approx "trig_fnd/" )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"(total_order?[real])" nil )"posreal" nil )"posreal" atan_approx "trig_fnd/" )nil interval_trig nil )"(total_order?[real])" nil )"int" integers nil )"nnreal" nil )nil reals nil )nil interval nil )nil booleans nil )nil booleans nil )"bool" interval nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"Interval" interval nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan "trig_fnd/" )"{rr: nnreal | rr < pi}" trig_approx"trig_fnd/" )"[numfield, numfield -> numfield]" number_fieldsnil ))nil )nil 3545778321"" (skeep)"" (expand "Tan" )"" (case "X << [|0, pi_lb_est(5 + n) / 2|]" )"1" (assert )"1" (rewrite "tan_0_pi2" )"1" (lemma "pi_lb_est_le" )"1" (inst?)"1" (flatten)"1" (expand "<<" )"1" (expand "[||]" ) (("1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace 1)"2" (case "X << [|-pi_lb_est(5 + n) / 2, 0|]" )"1" (assert )"1" (rewrite "tan_npi2_0" )"1" (lemma "pi_lb_est_le" )"1" (inst?)"1" (expand "<<" )"1" (expand "[||]" )"1" (flatten) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (rewrite "tan_npi2_pi2" )"1" (lemma "pi_lb_est_le" )"1" (inst?)"1" (expand "<<" )"1" (expand "[||]" )"1" (flatten) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 4)"2" (grind :exclude "pi_lb_est" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" interval nil )"bool" interval nil )nil trig_approx "trig_fnd/" )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"posreal" atan_approx "trig_fnd/" )nil interval nil )"bool" interval nil )"posreal" atan "trig_fnd/" )"{rr: nnreal | rr < pi}" trig_approx"trig_fnd/" ))nil )nil 3302519966"" (skeep)"" (expand "Tan" )"" (lift-if)"" (bddsimp)"1" (rewrite "tan_0_pi2" ) nil nil )"2" (rewrite "tan_npi2_0" ) nil nil )"3" (rewrite "tan_npi2_pi2" )"1" (expand "<<" ) (("1" (assert ) nil nil )) nil )"2" (expand "<<" ) (("2" (assert ) nil nil )) nil ))nil )"4" (assert ) nil nil ))nil ))nil ))nil ))nil )"posreal" atan_approx "trig_fnd/" )nil interval nil )"bool" interval nil )nil interval nil )
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 1.814 Sekunden
(vorverarbeitet am 2026-04-27)
¤ *© Formatika GbR, Deutschland
