Quelle trig_approx.prf
Sprache: Lisp
(trig_approxnil 3320763259"" (skosimp) (("" (assert ) nil nil )) nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"odd_int" integers nil )"posint" nil )"(total_order?[real])" nil ))nil 3320769270"" (skosimp)"" (expand "sin_term" )"" (expand "^" )"" (expand "expt" 1 2)"" (expand "expt" 1 2)"" (expand "expt" 1 1)"" "X" "expt((-1), n!1) * expt(a!1, 1 + 2 * n!1)" )"" (rewrite "cross_mult" )"" (expand "factorial" 1 1)"" (expand "factorial" 1 1)"" (expand "factorial" 1 5)"" (typepred "factorial(1+2*n!1)" )"" "F" "factorial(1 + 2 * n!1)" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"int" exponentiation nil )"nzreal" exponentiation nil )"real" reals nil )"real" reals nil )"real" trig_approx nil )"real" exponentiation nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"posnat" factorial "ints/" )nil integers nil )"bool" reals nil )nil integers nil )nil reals nil )"boolean" notequal nil )nil real_props nil )"real" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"even_int" integersnil )"nonneg_int" nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" 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 )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"odd_int" integers nil )"posint" nil )"odd_int" integers nil )"real" exponentiation nil )"nzreal" exponentiation nil )"int" exponentiation nil ))nil 3320922359"" (skosimp)"" (expand "sin_term" )"" (case-replace "a!1=0" )"1" (expand "^" )"1" (name-replace "S" "expt((-1), n!1)" )"1" (expand "expt" ) (("1" (assert ) nil nil )) nil )) nil ))nil )"2" (lemma "expt_plus" ("i" "1" "j" "2*n!1" ))"2" (inst-cp - "a!1" )"1" (inst - "-a!1" )"1" (replace -1)"1" (replace -2)"1" (rewrite "expt_x1" )"1" (rewrite "expt_x1" )"1" (lemma "expt_times" ("i" "2" "j" "n!1" ))"1" (inst-cp - "a!1" )"1" (inst - "-a!1" )"1" (case-replace "(-a!1) ^ 2 = a!1 ^ 2" )"1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"real" trig_approx nil )"[numfield, numfield -> numfield]" number_fields nil )nil exponentiation nil )"real" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )nil exponentiation nil )nil exponentiation nil )nil reals nil )"real" trig_approx nil )"boolean" notequal nil )"real" exponentiation nil )"even_int" integersnil )"even_int" integers nil )"posint" nil )"odd_int" integers nil )"rat" rationals nil )"nonneg_rat" nil )"nat" exponentiation nil )"rat" rationals nil )"odd_int" integers nil )"int" exponentiation nil )"nzreal" exponentiation 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" exponentiation nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"int" exponentiation nil )"nzreal" exponentiation nil )"real" reals nil )"real" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil ))nil 3320772448"" (skosimp)"" (expand "sin_term" )"" (rewrite "div_mult_pos_gt1" 2)"" (rewrite "div_mult_pos_lt1" 2)"" (rewrite "zero_times1" )"" (rewrite "expt_plus" 2)"" (rewrite "expt_x1" )"" (name-replace "S" "(-1)^n!1" )"" "both_sides_times_neg_lt1" "nz" "-1" "x" "S * a!1 ^ (3 + 2 * n!1)" "y" "0" ))"" (replace -1 2)"" (hide -1)"" (expand ">" )"" (lemma "trichotomy" ("x" "S" ))"" (split -1)"1" "both_sides_times_pos_lt1" "pz" "S" "x" "0" ))"1" rewrite "zero_times1" -1)"1" "a!1 ^ (1 + 2 * n!1)" )"1" assert )"1" replace -2 2)"1" "a!1 ^ (3 + 2 * n!1)" )"1" replace -1 2)"1" "1" "1" expand "^" )"1" expand "expt" 2 1)"1" expand "expt" "1" "0 < expt(a!1, (1 + 2 * n!1))" )"1" assert )"1" "posreal_times_posreal_is_posreal" "px" "a!1*a!1" "py" "expt(a!1, 1 + 2 * n!1)" ))"1" assert )nil nil )"2" "2" "trichotomy" "x" "a!1" ))"2" "1" "both_sides_times_pos_lt1" "pz" "a!1" "x" "0" "y" "a!1" ))"1" assert )nil nil )"2" assert )nil nil ))nil )"2" assert )nil nil )"3" "both_sides_times_neg_lt1" "nz" "a!1" "x" "0" "y" "a!1" ))"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "0 <a!1*a!1" )"1" "both_sides_times_pos_lt1" "pz" "a!1*a!1" "x" "0" "y" "expt(a!1, 1 + 2 * n!1)" ))"1" assert )nil nil ))nil )"2" "2" "trichotomy" "x" "a!1" ))"2" "1" "both_sides_times_pos_lt1" "pz" "a!1" "x" "0" "y" "a!1" ))"1" assert )nil nil )"2" assert )nil nil ))nil )"2" assert )nil nil )"3" "both_sides_times_neg_lt1" "nz" "a!1" "x" "0" "y" "a!1" ))"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" expand "S" -1)"2" "expt_nonzero" "n0x" "-1" "i" "n!1" ))"2" (assert ) nil nil ))nil ))nil )"3" "both_sides_times_neg_lt1" "nz" "S" "x" "0" ))"1" "a!1 ^ (1 + 2 * n!1)" )"1" "a!1 ^ (3 + 2 * n!1)" )"1" assert )"1" replace -1)"1" replace -2)"1" "1" case "0<a!1*a!1" )"1" expand "^" )"1" expand "expt" 2 1)"1" expand "expt" 2 1)"1" "both_sides_times_pos_lt1" "pz" "a!1*a!1" "x" "expt(a!1, 1 + 2 * n!1)" "y" "0" ))"1" assert )"1" replace "1" rewrite "zero_times1" )"1" "1" "expt(a!1, 1 + 2 * n!1) * (a!1 * a!1) < 0" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "trichotomy" "x" "a!1" ))"2" "1" "both_sides_times_pos_lt1" "pz" "a!1" "x" "0" "y" "a!1" ))"1" assert )nil nil )"2" assert )nil nil ))nil )"2" assert )nil nil )"3" "both_sides_times_neg_lt1" "nz" "a!1" "x" "0" "y" "a!1" ))"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"int" exponentiation nil )"nzreal" exponentiation nil )"real" reals nil )"real" trig_approx nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )nil reals nil )nil exponentiation nil )"int" integers nil )"nzint" integersnil )"[T, T -> boolean]" equalities nil )"(total_order?[real])" nil )nil real_types nil )"real" exponentiation nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )nil real_props nil )nil exponentiation nil )"int" trig_approx nil )nil real_axioms nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_props nil )nil exponentiation nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"[numfield -> numfield]" number_fields nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posnat" factorial "ints/" )nil integers nil )nil integers nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil extra_real_props nil )"odd_int" integers nil )"odd_int" integers nil )"posint" nil ))nil 3320769218"" (expand "sin_term" )"" (skosimp*)"" (rewrite "div_cancel3" )"" (lemma "expt_nonzero" ("n0x" "-1" "i" "n!1" ))"" (split)"1" (flatten)"1" (replace -1)"1" (expand "^" 1 2)"1" (expand "expt" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (flatten)"2" (rewrite "zero_times1" )"2" (rewrite "zero_times3" )"2" "expt_nonzero" ("n0x" "a!1" "i" "1+2*n!1" ))"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil exponentiation nil )nil reals nil )nil real_props nil )nil real_props nil )"real" exponentiation nil )"[numfield -> numfield]" number_fields nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posnat" factorial "ints/" )nil integers nil )"bool" reals nil )nil integers 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 )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )"odd_int" integers nil )"odd_int" integers nil )"posint" nil )"real" trig_approx nil )"real" reals nil )"nzreal" exponentiation nil )"int" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil ))nil 3320924247"" (skosimp)"" (lemma "sin_term_nonzero" ("a" "a!1" "n" "n!1" ))"" (assert )"" (split)"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (flatten) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))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 trig_approx nil ))nil 3320931387"" (expand "sin_term" )"" (skosimp)"" (case-replace "a!1=0" )"1" (expand "^" 1 2)"1" (expand "expt" ) (("1" (assert ) nil nil )) nil )) nil )"2" (rewrite "expt_plus" )"2" (rewrite "expt_x1" )"2" (rewrite "expt_times" )"2" (lemma "expt_pos" ("px" "a!1^2" "i" "n!1" ))"1" "posreal_div_posreal_is_posreal" "px" "(a!1 ^ 2) ^ n!1" "py" "factorial(1 + 2 * n!1)" ))"1" "both_sides_times_pos_gt1" "pz" "(a!1 ^ 2) ^ n!1 / factorial(1 + 2 * n!1)" "x" "(-1)^n!1*a!1" "y" "0" ))"1" (rewrite "zero_times1" )"1" (replace -1 2)"1" (hide-all-but (1 2))"1" (case "forall (n:nat): (-1)^(2*n) =1" )"1" (lemma "trichotomy" ("x" "a!1" ))"1" "1" assert )"1" "1" "1" "even_or_odd" )"1" "n!1" )"1" assert )"1" "1" expand "odd?" )"1" "1" replace -1)"1" rewrite "expt_plus" )"1" rewrite "expt_x1" )"1" "j!1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "even?" )"2" "2" "j!1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil )"3" assert )"3" "1" "1" "even_or_odd" "x" "n!1" ))"1" assert )"1" "1" expand "even?" )"1" "1" "j!1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "odd?" )"2" "2" replace -1)"2" rewrite "expt_plus" )"2" rewrite "expt_x1" )"2" "j!1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" "2" rewrite "expt_times" )"2" expand "^" 1 1)"2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" rewrite "expt_1i" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil )"2" (hide-all-but (1 2))"2" (lemma "pos_times_lt" ("x" "a!1" "y" "a!1" ))"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil exponentiation nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"boolean" notequal nil )nil reals nil )nil exponentiation nil )nil real_props nil )nil real_types nil )nil integers nil )nil integers nil )"posnat" factorial "ints/" )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )nil exponentiation nil )nil real_axioms nil )"int" trig_approx nil )"int" trig_approx nil )"(strict_total_order?[real])" real_props nil )"int" trig_approx nil )"bool" integers nil )"rat" exponentiation nil )"nzrat" rationalsnil )"int" trig_approx nil )"bool" integers nil )nil naturalnumbers nil )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil real_props nil )"odd_int" integers nil )"real" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil exponentiation nil )nil exponentiation nil )"nat" exponentiation nil )"real" exponentiation nil )"odd_int" integers nil )"posint" nil )"nonneg_rat" nil )"(strict_total_order?[real])" real_props nil )"real" exponentiation 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" trig_approx nil )"real" reals nil )"nzreal" exponentiation nil )"int" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil ))nil 3320932130"" (skosimp)"" (lemma "trichotomy" ("x" "a!1" ))"" (split -1)"1" (assert )"1" (lemma "sin_term_gt0" ("a" "a!1" "n" "n!1" ))"1" (assert )"1" (rewrite "even_or_odd" )"1" (split 1)"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (flatten)"2" (assert )"2" "sin_term_nonzero" "a" "a!1" "n" "n!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1)"2" (assert )"2" (lemma "sin_term_zero" ("a" "0" "n" "n!1" ))"2" (assert ) nil nil )) nil ))nil ))nil )"3" (assert )"3" (lemma "sin_term_gt0" ("a" "a!1" "n" "n!1" ))"3" (assert )"3" (rewrite "even_or_odd" )"3" (split 1)"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (flatten)"2" (assert )"2" "sin_term_nonzero" "a" "a!1" "n" "n!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_axioms nil )nil trig_approx nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil trig_approx nil )nil naturalnumbers nil )nil trig_approx 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 3320988819"" (skosimp)"" (case-replace "a!1=0" )"1" (hide -1)"1" (expand "tends_to_0?" )"1" (skosimp)"1" (inst + "0" )"1" (skosimp)"1" (expand "sin_term" )"1" (expand "^" 1 2)"1" (assert )"1" (expand "expt" 1)"1" (rewrite "abs_div" )"1" (expand "abs" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "exp_tends_to_0" ("n0a" "a!1" ))"1" (expand "exp_term" )"1" (expand "sin_term" )"1" (expand "tends_to_0?" )"1" (skosimp*)"1" (inst - "epsilon!1" )"1" (skosimp)"1" (inst + "1+2*n!1" )"1" (skosimp)"1" (inst - "1+2*i!1" )"1" (assert )"1" (rewrite "abs_div" )"1" rewrite "abs_div" )"1" rewrite "abs_mult" )"1" "abs((-1) ^ i!1) = 1" )"1" (assert ) nil nil )"2" "2" case "(-1)^2 =1" )"1" case "even?(i!1)" )"1" expand "even?" )"1" "1" replace -1)"1" rewrite "expt_times" )"1" replace -2)"1" rewrite "expt_1i" )"1" expand "abs" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "even_or_odd" )"2" expand "odd?" )"2" "2" replace -1)"2" rewrite "expt_plus" )"2" rewrite "expt_times" )"2" replace -2)"2" rewrite "expt_x1" )"2" rewrite "expt_1i" )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil 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 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 )"bool" exp_term nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"rat" exponentiation nil )"nzreal" exponentiation nil )"nnrat" exponentiation nil )"rat" rationals nil )"rat" rationals nil )"real" trig_approx nil )"odd_int" integers nil )"nat" exponentiation nil )"odd_int" integers nil )"{r: nonneg_rat | r >= q}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posnat" factorial "ints/" )nil integers nil )"bool" reals nil )nil integers nil )nil reals nil )"boolean" notequal nil )nil real_props nil )"{j: posint | j >= i}" nil )"{j: nonneg_int | j >= i}" nil )nil abs_lems "reals/" )"real" exponentiation nil )"nonneg_rat" nil )"real" exponentiation nil )"real" exp_term nil )"real" reals nil )nil real_types nil )nil real_types nil )"posint" nil )OR const-decl "[bool, bool -> bool]" booleans nil )"nnreal" nil )nil real_props nil )"{r: posrat | r >= q}" nil )"nnreal" nil )"nzreal" exponentiation nil )"int" exponentiation nil )"nzrat" rationalsnil )"nzint" integersnil )"bool" integers nil )nil exponentiation nil )nil exponentiation nil )"posrat" exponentiation nil )"bool" integers nil )nil exponentiation nil )"nzrat" rationalsnil )nil exponentiation nil )nil naturalnumbers nil )"int" exponentiation nil )AND const-decl "[bool, bool -> bool]" booleans nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )"nonneg_int" nil )"real" reals nil )nil exp_term nil )nil reals nil ))nil 3320763259"" (skosimp) (("" (assert ) nil nil )) nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"(total_order?[real])" nil ))nil 3320770358"" (skosimp*)"" (expand "cos_term" )"" (case-replace "n!1=0" )"1" (assert )"1" (rewrite "expt_x1" )"1" (expand "factorial" )"1" (expand "factorial" )"1" (expand "factorial" )"1" (expand "^" )"1" (expand "expt" )"1" (expand "expt" )"1" (expand "expt" ) (("1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (rewrite "expt_plus" 2)"2" (name-replace "S" "(-1)^n!1" )"2" (rewrite "expt_x1" )"2" (expand "factorial" 2 1)"2" (expand "factorial" 2 2)"2" (expand "factorial" 2 1)"2" (case-replace "a!1=0" )"1" (expand "^" )"1" (expand "expt" )"1" (assert ) nil nil )) nil ))nil )"2" (rewrite "expt_plus" 3)"2" (typepred "factorial(2*n!1)" )"2" (name-replace "F" "factorial(2*n!1)" )"2" expand "^" 3 1)"2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" rewrite "cross_mult" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"int" exponentiation nil )"nzreal" exponentiation nil )"real" reals nil )"nonneg_int" nil )"(divides(n))" divides nil )"even_int" integersnil )"(divides(m))" divides nil )"real" trig_approx nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )nil reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" reals nil )nil integers nil )nil integers nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"nonneg_rat" nil )"posint" nil )"nzint" integersnil )"int" integers nil )nil exponentiation nil )"boolean" notequal nil )nil reals nil )"odd_int" integers nil )"odd_int" integers nil )"real" reals nil )"posnat" factorial "ints/" )"real" exponentiation nil )"real" exponentiation nil )nil exponentiation nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"posint" nil )"even_int" integersnil )"nonneg_int" 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 )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil ))nil 3320922908"" (expand "cos_term" )"" (skosimp)"" (case-replace "n!1=0" )"" (assert )"" (case-replace "a!1=0" )"1" (assert ) nil nil )"2" (lemma "expt_times" ("i" "2" "j" "n!1" ))"2" (inst-cp - "a!1" )"2" (inst - "-a!1" )"2" (case-replace "(-a!1) ^ 2 = a!1 ^ 2" )"1" (assert ) nil nil )"2" (hide-all-but (1 2)) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"real" reals nil )"odd_int" integers nil )"nzreal" exponentiation nil )"int" exponentiation nil )"real" reals nil )"real" reals nil )nil exponentiation nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"(total_order?[real])" nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"boolean" notequal nil )nil reals 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 )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"real" trig_approx nil ))nil 3320771767"" (skosimp)"" (expand "cos_term" )"" (case-replace "n!1=0" )"1" (assert )"1" (rewrite "expt_x1" )"1" (expand "factorial" )"1" (expand "factorial" )"1" (expand "factorial" )"1" (case "a!1^2>0" )"1" (assert ) nil nil )"2" (hide -1 3)"2" (lemma "trichotomy" ("x" "a!1" ))"2" (split -1)"1" "both_sides_times_pos_lt1" "pz" "a!1" "x" "0" "y" "a!1" ))"1" (grind) nil nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil )"3" "both_sides_times_neg_lt1" "nz" "a!1" "x" "0" "y" "a!1" ))"1" (grind) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "^" )"2" (expand "expt" 3 2)"2" (expand "expt" 3 2)"2" (expand "expt" 3 1)"2" "S" "expt((-1), n!1) * expt(a!1, (2 * n!1))" )"2" (case "a!1*a!1>0" )"1" (assert )"1" (rewrite "div_mult_pos_gt1" 3)"1" (rewrite "div_mult_pos_lt1" 3)"1" (rewrite "zero_times1" )"1" "trichotomy" ("x" "S" ))"1" "1" assert )"1" "both_sides_times_pos_lt1" "pz" "S" "x" "-1*(a!1*a!1)" "y" "0" ))"1" (assert ) nil nil ))nil ))nil )"2" expand "S" -1)"2" "expt_nonzero" "n0x" "-1" "i" "n!1" ))"2" "expt_nonzero" "n0x" "a!1" "i" "2*n!1" ))"2" expand "^" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" "both_sides_times_neg_lt1" "nz" "S" "x" "-1*(a!1*a!1)" "y" "0" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 4)"2" (lemma "trichotomy" ("x" "a!1" ))"2" (split -1)"1" "both_sides_times_pos_lt1" "pz" "a!1" "x" "0" "y" "a!1" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil )"3" "both_sides_times_neg_lt1" "nz" "a!1" "x" "0" "y" "a!1" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"int" exponentiation nil )"nzreal" exponentiation nil )"real" reals nil )"real" trig_approx nil )nil integers nil )nil integers nil )nil extra_real_props nil )nil real_props nil )nil exponentiation nil )nil reals nil )"real" trig_approx nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nzreal" exponentiation nil )"int" exponentiation nil )"(strict_total_order?[real])" real_props nil )"even_int" integersnil )"odd_int" integers nil )"posint" nil )"odd_int" integers nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"posnat" factorial "ints/" )"real" exponentiation nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )nil real_types nil )nil real_types nil )nil real_props nil )"(total_order?[real])" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_props nil )nil real_axioms nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil exponentiation nil )nil number_fields nil )"[numfield -> numfield]" 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 )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil ))nil 3320924341"" (skosimp)"" (split)"1" (flatten)"1" (replace -1)"1" (expand "cos_term" )"1" (assert )"1" (expand "^" 1)"1" (expand "expt" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (split -1)"1" (replace -1)"1" (expand "cos_term" ) (("1" (assert ) nil nil )) nil ))nil )"2" (assert )"2" (expand "cos_term" )"2" (case-replace "n!1=0" )"1" (assert ) nil nil )"2" (assert )"2" "expt_nonzero" ("n0x" "a!1" "i" "2*n!1" ))"2" (assert )"2" "expt_nonzero" ("n0x" "-1" "i" "n!1" ))"2" "div_cancel3" "x" "(-1) ^ n!1 * a!1 ^ (2 * n!1)" "n0z" "factorial(2 * n!1)" "y" "0" ))"2" (replace -1 -5)"2" (hide -1)"2" rewrite "zero_times3" -4)nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"even_int" integersnil )"nonneg_int" nil )"nat" exponentiation nil )"odd_int" integers nil )"nzreal" exponentiation nil )"int" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"rat" rationals nil )"real" exponentiation nil )"nonneg_rat" nil )"real" exponentiation nil )"real" trig_approx nil )"real" reals nil )"real" reals nil )nil real_props nil )nil reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" factorial "ints/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil real_props nil )"[numfield -> numfield]" number_fields nil )nil reals nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil exponentiation 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 )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil ))nil 3320924852"" (skosimp)"" (lemma "cos_term_nonzero" ("a" "a!1" "n" "n!1" ))"" (split)"1" (flatten)"1" (assert ) (("1" (flatten) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (flatten) (("2" (assert ) nil nil )) nil ))nil ))nil ))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 trig_approx nil ))nil 3320925011"" (skosimp)"" (expand "cos_term" )"" (case-replace "n!1=0" )"1" (assert ) nil nil )"2" (assert )"2" (rewrite "div_mult_pos_gt1" )"2" (rewrite "zero_times1" )"2" (split)"1" (flatten)"1" (expand ">" )"1" (rewrite "pos_times_lt" -1)"1" (case-replace "a!1=0" )"1" (expand "^" )"1" (expand "expt" )"1" (propax) nil nil )) nil ))nil )"2" (assert )"2" (case "a!1^2 > 0" )"1" "expt_pos" "px" "a!1^2" "i" "n!1" ))"1" rewrite "expt_times" )"1" assert )"1" "1" rewrite "even_or_odd" 1)"1" expand "odd?" )"1" "1" replace -2)"1" "1" rewrite "expt_plus" )"1" rewrite "expt_times" )"1" rewrite "expt_x1" )"1" "(-1) ^ 2 = 1" )"1" rewrite "expt_1i" )"1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (hide-all-but (1 2))"2" expand "^" )"2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" "pos_times_lt" "x" "a!1" "y" "a!1" ))"2" assert )"2" "2" "trichotomy" "x" "a!1" ))"2" "1" (assert ) nil nil )"2" (propax) nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (case-replace "(-1)^n!1=1" )"1" (rewrite "expt_times" )"1" (lemma "expt_pos" ("px" "a!1^2" "i" "n!1" ))"1" (propax) nil nil )"2" (hide-all-but (1 2))"2" (expand "^" )"2" (expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" "pos_times_lt" "x" "a!1" "y" "a!1" ))"2" assert )"2" "2" "trichotomy" "x" "a!1" ))"2" "1" (assert ) nil nil )"2" (propax) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (expand "even?" )"2" (skosimp)"2" (replace -1 1)"2" (hide -1)"2" rewrite "expt_times" )"2" "(-1)^2 =1" )"1" (rewrite "expt_1i" ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" trig_approx nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"odd_int" integers nil )"nzreal" exponentiation nil )"int" exponentiation nil )"real" reals nil )"real" reals nil )nil real_props nil )"bool" integers nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )nil real_axioms nil )nil exponentiation nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"odd_int" integers nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )nil exponentiation nil )"nzint" integersnil )"nzrat" rationalsnil )nil exponentiation nil )"nzrat" rationalsnil )"rat" exponentiation nil )nil exponentiation nil )"bool" integers nil )nil exponentiation nil )nil reals nil )"(total_order?[real])" nil )"real" exponentiation nil )"nat" exponentiation nil )"nzreal" exponentiation nil )"int" exponentiation nil )"[numfield -> numfield]" number_fields nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posnat" factorial "ints/" )nil integers nil )nil integers nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil extra_real_props nil )"(strict_total_order?[real])" 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 reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil ))nil 3320926707"" (skosimp)"" (expand "cos_term" )"" (case-replace "n!1=0" )"1" (assert )"1" (expand "odd?" ) (("1" (propax) nil nil )) nil )) nil )"2" (assert )"2" (case-replace "a!1=0" )"1" (assert )"1" (expand "^" )"1" (expand "expt" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (assert )"2" (case "(-1) ^ n!1 < 0 IFF odd?(n!1)" )"1" "both_sides_times_pos_lt1" "x" "(-1) ^ n!1" "pz" "a!1 ^ (2 * n!1) / factorial(2 * n!1)" "y" "0" ))"1" (replace -2 -1)"1" (rewrite "zero_times1" )"1" (assert )"1" (split 3)"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (flatten) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (case "a!1^2>0" )"1" (lemma "expt_pos" ("px" "a!1^2" "i" "n!1" ))"1" (rewrite "expt_times" 1)"1" (assert )"1" "posreal_div_posreal_is_posreal" "px" "(a!1 ^ 2) ^ n!1" "py" "factorial(2 * n!1)" ))"1" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (hide-all-but (1 3))"2" "pos_times_lt" ("x" "a!1" "y" "a!1" ))"2" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (case "forall (n:nat): (-1)^(2*n) = 1" )"1" (split)"1" (flatten)"1" (lemma "even_or_odd" )"1" (inst - "n!1" )"1" (assert )"1" "1" expand "even?" )"1" "1" "j!1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "odd?" )"2" (skosimp)"2" (replace -1)"2" rewrite "expt_plus" 1)"2" rewrite "expt_x1" 1)"2" "j!1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (rewrite "expt_times" )"2" (expand "^" 1 1)"2" (expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" (rewrite "expt_1i" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" trig_approx nil )"nonneg_int" nil )"odd_int" integers nil )"nzreal" exponentiation nil )"int" exponentiation nil )"real" reals nil )"real" reals nil )nil exponentiation nil )nil naturalnumbers nil )"bool" integers nil )"int" trig_approx nil )"rat" exponentiation nil )nil exponentiation nil )"odd_int" integers nil )"int" trig_approx nil )"nzrat" rationalsnil )nil exponentiation nil )nil real_props nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )nil integers nil )"posnat" factorial "ints/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_props nil )nil real_props nil )nil exponentiation nil )nil real_types nil )nil exponentiation nil )nil reals nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )"nat" exponentiation nil )"rat" rationals nil )"real" exponentiation nil )"nonneg_rat" nil )"real" exponentiation nil )"(strict_total_order?[real])" real_props nil )"bool" integers nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )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 )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil ))nil 3320988406"" (skosimp)"" (expand "cos_term" )"" (lemma "exp_tends_to_0" ("n0a" "n0x!1" ))"" (expand "exp_term" )"" (expand "tends_to_0?" )"" (skosimp*)"" (inst - "epsilon!1" )"" (skosimp)"" (inst + "2*n!1" )"" (skosimp)"" (inst - "2*i!1" )"" (assert )"" (case-replace "i!1=0" )"1" (assert ) nil nil )"2" (assert )"2" rewrite "abs_div" )"2" rewrite "abs_div" )"2" rewrite "abs_mult" )"2" "abs((-1) ^ i!1) = 1" )"1" (assert ) nil nil )"2" "2" case "(-1)^2 = 1" )"1" case "even?(i!1)" )"1" expand "even?" )"1" "1" replace -1)"1" rewrite "expt_times" )"1" replace -2)"1" rewrite "expt_1i" )"1" expand "abs" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "even_or_odd" )"2" expand "odd?" )"2" "2" replace -1)"2" rewrite "expt_plus" )"2" rewrite "expt_times" )"2" replace -2)"2" rewrite "expt_x1" )"2" rewrite "expt_1i" )"2" expand "abs" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" trig_approx nil )"real" exp_term nil )"{y: posreal | y >= x}" nil )"{j: posint | j >= i}" nil )"{j: nonneg_int | j >= i}" nil )"{r: posrat | r >= q}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil abs_lems "reals/" )"odd_int" integers nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )AND const-decl "[bool, bool -> bool]" booleans nil )"int" exponentiation nil )nil naturalnumbers nil )nil exponentiation nil )"nzrat" rationalsnil )nil exponentiation nil )"bool" integers nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )nil exponentiation nil )nil exponentiation nil )"bool" integers nil )"nzreal" exponentiation nil )"int" exponentiation nil )"nzrat" rationalsnil )"nzint" integersnil )"real" exponentiation nil )"posreal" nil )nil real_props nil )"posreal" nil )nil real_props nil )nil reals nil )nil integers nil )nil integers nil )"posnat" factorial "ints/" )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"[T, T -> boolean]" equalities nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" exp_term nil )"nzreal" nil )"rat" exponentiation nil )"nzreal" nil )"nzreal" exponentiation nil )nil exp_term nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil )nil reals nil ))nil 3403527292 ("" (subtype-tcc) nil nil ) nil nil ))nil 3321006684"" (expand "sin_approx" )"" (expand "sin_term" )"" (expand "^" 1 2)"" (expand "expt" )"" (induct "n" )"1" (expand "sigma" ) (("1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (expand "sigma" 1) (("2" (assert ) nil nil )) nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"int" exponentiation nil )"nzreal" exponentiation nil )"nat" exponentiation nil )"real" trig_approx nil )"real" exponentiation nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"nnreal" nil )"nnreal" sigma_nat "reals/" )nil factorial "ints/" )nil sigma_nat "reals/" )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posnat" factorial "ints/" )nil integers nil )"bool" reals nil )nil integers nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil defined_types 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 )"posint" nil )"odd_int" integers nil )"nonneg_rat" nil )"real" exponentiation nil )"nat" exponentiation nil )"real" trig_approx nil ))nil 3320921408"" (expand "sin_approx" )"" (induct "n" )"1" (expand "sigma" )"1" (expand "sin_term" )"1" (skosimp)"1" (rewrite "expt_x1" )"1" (rewrite "expt_x1" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "sigma" 1)"2" (inst - "a!1" )"2" (replace -1)"2" (assert )"2" (hide -1)"2" (expand "sin_term" )"2" (assert )"2" "(-a!1) ^ (3 + 2 * j!1) = - a!1 ^ (3 + 2 * j!1)" )"1" (assert ) nil nil )"2" (hide 2)"2" "expt_plus" ("i" "1" "j" "2*j!1+2" ))"2" (case-replace "a!1=0" )"1" expand "^" 1)"1" expand "expt" 1)"1" (assert ) nil nil ))nil ))nil )"2" "-a!1" )"1" "a!1" )"1" rewrite "expt_x1" )"1" rewrite "expt_x1" )"1" replace -1)"1" replace -2)"1" "1" "expt_times" "i" "2" "j" "1+j!1" ))"1" "a!1" )"1" "-a!1" )"1" replace -1)"1" replace -2)"1" "(-a!1) ^ 2 = a!1 ^ 2" )"1" assert )nil nil )"2" "2" expand "^" )"2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil ))nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )"real" trig_approx nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"int" exponentiation nil )"nzreal" exponentiation nil )"real" reals nil )"real" reals nil )nil exponentiation nil )nil sigma_nat "reals/" )nil factorial "ints/" )"odd_int" integers nil )"real" reals nil )"odd_int" integers nil )"real" exponentiation nil )"even_int" integers nil )"int" exponentiation nil )"nat" exponentiation nil )nil exponentiation nil )"posint" nil )"even_int" integersnil )nil reals nil )"real" trig_approx nil )nil exponentiation nil )"even_int" integersnil )"posint" nil )"boolean" notequal nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"real" trig_approx nil ))nil 3320919641"" (skosimp)"" (expand "sin_approx" )"" (expand "sigma" 1 1)"" (expand "sigma" 1 1)"" (expand "sin_term" )"" (expand "^" )"" (expand "expt" 1 1)"" (name-replace "S" "expt((-1), 1 + n!1)" )"" (expand "expt" 1 1)"" (expand "expt" 1 1)"" (name-replace "AA" "expt(a!1, 3 + 2 * n!1)" )"" (rewrite "div_times" )"" (assert )"" (expand "factorial" 1 1)"" expand "factorial" 1 2)"" expand "factorial" 1 1)"" "DRL100" "(20 * factorial(3 + 2 * n!1) + ") "" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nonneg_int" nil )"(divides(n))" divides nil )"even_int" integersnil )"(divides(m))" divides nil )"posint" nil )"even_int" integersnil )"nonneg_int" nil )"real" reals nil )"real" reals nil )"real" trig_approx nil )"real" exponentiation nil )"odd_int" integers 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 -> 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]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posnat" factorial "ints/" )nil integers nil )"bool" reals nil )nil integers nil )nil reals nil )"boolean" notequal nil )nil real_props nil )"even_int" integersnil )"posint" nil )nil integers nil )"odd_int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"real" exponentiation nil )"nzreal" exponentiation nil )"int" exponentiation nil )"real" trig_approx nil )"real" sigma "reals/" ))nil 3321006162"" (skosimp)"" (lemma "sin_approx_next" ("a" "a!1" "n" "n!1" ))"" (replace -2)"" (lemma "div_simp" ("n0x" "(2 * n!1 + 5) * (2 * n!1 + 4)" ))"" (replace -1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))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 trig_approx nil )nil real_props nil )"boolean" notequal nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"even_int" integersnil )"nonneg_int" nil )"posint" nil )"rat" rationals nil )"posrat" nil )"real" reals nil )"real" reals nil )"even_int" integersnil )"posint" nil )"real" reals nil )"even_int" integersnil )"odd_int" integers nil )"posint" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil ))nil 3320991568"" (skosimp)"" (lemma "sin_series" ("x" "a!1" "n" "n!1" ))"" (expand "sin_term" )"" case "forall (n:nat): sin_series_n(a!1, n) = sin_approx(a!1, n)" )"1" (inst - "n!1" )"1" (replace -1 -2)"1" (hide -1)"1" (rewrite "abs_div" )"1" (rewrite "abs_mult" )"1" (expand "abs" 1 4)"1" (case-replace "abs((-1) ^ (1 + n!1)) = 1" )"1" (assert ) nil nil )"2" (hide-all-but 1)"2" (case "(-1)^2 =1" )"1" (case "even?(1+n!1)" )"1" expand "even?" )"1" "1" replace -1)"1" rewrite "expt_times" )"1" replace -2)"1" rewrite "expt_1i" )"1" expand "abs" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "even_or_odd" )"2" expand "odd?" )"2" "2" replace -1)"2" rewrite "expt_plus" )"2" rewrite "expt_times" )"2" replace -2)"2" rewrite "expt_1i" )"2" rewrite "expt_x1" )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" expand "^" )"2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "sin_series_n" )"2" (expand "sin_approx" )"2" (expand "sin_term" )"2" (expand "sin_series_term" )"2" (induct "n" )"1" (expand "sigma" )"1" (expand "sigma" ) (("1" (propax) nil nil ))nil ))nil )"2" (skosimp*)"2" (expand "sigma" 1)"2" (replace -1 1 rl)"2" (hide -1)"2" "sigma_eq" "low" "0" "high" "j!1" "F" "LAMBDA (i: nat): IF i > 1 + j!1 THEN 0" "G" "LAMBDA (i: nat): IF i > j!1 THEN 0")) "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 sincos_def nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"[T, T -> boolean]" equalities nil )"real" sincos_def nil )"real" trig_approx nil )"[numfield -> numfield]" number_fields nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posnat" factorial "ints/" )nil integers nil )"bool" reals nil )nil integers nil )nil reals nil )"boolean" notequal nil )nil real_props nil )"odd_int" integers nil )"odd_int" integers nil )"posint" nil )"{j: posint | j >= i}" nil )"(total_order?[real])" nil )"nnreal" nil )nil abs_lems "reals/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"(total_order?[real])" nil )"posint" nil )"odd_int" integers nil )nil naturalnumbers nil )nil exponentiation nil )"nzrat" rationalsnil )nil exponentiation nil )"bool" integers nil )"int" integers nil )"even_int" integersnil )"rat" exponentiation nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )nil exponentiation nil )nil exponentiation nil )nil reals nil )"bool" integers nil )"real" exponentiation nil )"nnreal" nil )nil real_props nil )nil defined_types nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )IF const-decl "[boolean, T, T -> T]" if_def nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil sigma "reals/" )"[nat -> real]" sincos_def nil )"real" trig_approx nil )"real" reals nil )"real" reals nil )"nzreal" exponentiation nil )"int" exponentiation nil )"real" reals nil )"trig_range" trig_basic nil ))nil 3321006785"" (expand "cos_approx" )"" (expand "cos_term" )"" (induct "n" )"1" (expand "sigma" )"1" (expand "sigma" ) (("1" (propax) nil nil )) nil )) nil )"2" (skosimp*)"2" (expand "sigma" 1)"2" (expand "^" 1 4)"2" (expand "expt" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil )"real" trig_approx nil )"nat" exponentiation nil )"even_int" integersnil )"posint" nil )"nonneg_rat" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" exponentiation nil )"nat" exponentiation nil )"nzreal" exponentiation nil )"int" exponentiation nil )nil naturalnumbers nil )"posnat" factorial "ints/" )nil integers nil )"bool" reals nil )nil integers nil )"[numfield -> numfield]" number_fields nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil number_fields nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil defined_types 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 )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"rat" rationals nil )"real" trig_approx nil ))nil 3320922036"" (expand "cos_approx" )"" (induct "n" )"1" (expand "sigma" )"1" (expand "cos_term" )"1" (skosimp*)"1" (expand "sigma" ) (("1" (propax) nil nil )) nil )) nil ))nil ))nil )"2" (skosimp*)"2" (expand "sigma" 1)"2" (inst - "a!1" )"2" (replace -1)"2" (assert )"2" (hide -1)"2" (expand "cos_term" )"2" (case-replace "a!1=0" )"1" (assert ) nil nil )"2" (lemma "expt_times" ("i" "2" "j" "1+j!1" ))"2" (inst-cp - "a!1" )"2" (inst - "-a!1" )"2" (case-replace "(-a!1) ^ 2 = a!1 ^ 2" )"1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )"real" trig_approx nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"real" reals nil )"nzreal" exponentiation nil )"int" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )nil reals nil )"boolean" notequal nil )"real" exponentiation nil )"posint" nil )"real" reals nil )"odd_int" integers nil )"even_int" integersnil )"real" exponentiation nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil exponentiation nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"posint" nil )"real" trig_approx nil ))nil 3320992237"" (skosimp)"" (lemma "cos_series" ("x" "a!1" "n" "n!1" ))"" (expand "cos_term" )"" (rewrite "abs_div" )"" (expand "abs" 1 3)"" (rewrite "abs_mult" )"" (case-replace "abs((-1)^(1+n!1))=1" )"1" case "forall (n:nat): cos_series_n(a!1, n) = cos_approx(a!1, n)" )"1" (inst - "n!1" ) (("1" (assert ) nil nil )) nil )"2" (hide-all-but 1)"2" (expand "cos_approx" )"2" (expand "cos_series_n" )"2" (expand "cos_series_term" )"2" (expand "cos_term" )"2" (induct "n" )"1" expand "sigma" )"1" expand "sigma" )"1" (propax) nil nil ))nil ))nil )"2" "2" expand "sigma" 1)"2" replace -1 1 rl)"2" "2" "sigma_eq" "low" "0" "high" "j!1" "F" "LAMBDA (i: nat): IF i > 1 + j!1 THEN 0IF i = 0 THEN 1" "G" "LAMBDA (i: nat): IF i > j!1 THEN 0IF i = 0 THEN 1")) "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (case "(-1)^2=1" )"1" (case "even?(1+n!1)" )"1" (expand "even?" )"1" (skosimp)"1" (replace -1)"1" (rewrite "expt_times" )"1" replace -2)"1" rewrite "expt_1i" )"1" expand "abs" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "even_or_odd" )"2" (expand "odd?" )"2" (skosimp*)"2" (replace -1)"2" rewrite "expt_plus" )"2" rewrite "expt_times" )"2" rewrite "expt_x1" )"2" replace -2)"2" rewrite "expt_1i" )"2" expand "abs" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "^" )"2" (expand "expt" )"2" (expand "expt" )"2" (expand "expt" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 sincos_def nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"[numfield -> numfield]" number_fields nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posnat" factorial "ints/" )nil integers nil )"bool" reals nil )nil integers nil )nil reals nil )"boolean" notequal nil )nil real_props nil )"real" reals nil )"nzreal" exponentiation nil )"int" exponentiation nil )"real" reals nil )"odd_int" integers nil )"even_int" integersnil )"posint" nil )"{j: posint | j >= i}" nil )"(total_order?[real])" nil )"nnreal" nil )nil abs_lems "reals/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"[T, T -> boolean]" equalities nil )nil sigma "reals/" )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )nil naturalnumbers nil )nil defined_types nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )IF const-decl "[boolean, T, T -> T]" if_def nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[nat -> real]" sincos_def nil )"(total_order?[real])" nil )"posint" nil )"real" trig_approx nil )"real" sincos_def nil )nil naturalnumbers nil )nil exponentiation nil )"nzrat" rationalsnil )nil exponentiation nil )"bool" integers nil )"int" integers nil )"even_int" integersnil )"rat" exponentiation nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )nil exponentiation nil )nil exponentiation nil )nil reals nil )"bool" integers nil )"real" exponentiation nil )"nnreal" nil )nil real_props nil )"real" trig_approx nil )"real" reals nil )"trig_range" trig_basic nil ))nil 3320919986"" (skosimp)"" (expand "cos_approx" )"" (expand "sigma" 1 1)"" (expand "sigma" 1 1)"" (expand "cos_term" )"" (expand "^" )"" (expand "expt" 1 1)"" (name-replace "S" "expt((-1), 1 + n!1)" )"" (expand "expt" 1 1)"" (expand "expt" 1 1)"" (name-replace "AA" "expt(a!1, 2 + 2 * n!1)" )"" (expand "factorial" 1 1)"" (expand "factorial" 1 2)"" (expand "factorial" 1 1)"" rewrite "div_times" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nonneg_int" nil )"(divides(n))" divides nil )"even_int" integersnil )"(divides(m))" divides nil )"posint" nil )"even_int" integersnil )"nonneg_int" nil )"real" reals nil )"real" reals nil )"real" trig_approx nil )"real" exponentiation nil )"odd_int" integers 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 -> 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]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posnat" factorial "ints/" )"posint" nil )"even_int" integersnil )nil real_props nil )"boolean" notequal nil )nil reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )"real" exponentiation nil )"nzreal" exponentiation nil )"int" exponentiation nil )"real" trig_approx nil )"real" sigma "reals/" ))nil 3321006042"" (skosimp*)"" (lemma "cos_approx_next" ("a" "a!1" "n" "n!1" ))"" (replace -2 -1)"" (lemma "div_simp" ("n0x" "(2 * n!1 + 4) * (2 * n!1 + 3)" ))"" (replace -1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))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 trig_approx nil )nil real_props nil )"boolean" notequal nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"even_int" integersnil )"nonneg_int" nil )"posint" nil )"rat" rationals nil )"posrat" nil )"real" reals nil )"real" reals nil )"posint" nil )"real" reals nil )"odd_int" integers nil )"even_int" integersnil )"posint" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil ))nil 3321098562"" (expand "sin_lb" )"" (expand "sin_ub" )"" (skosimp)"" (lemma "trichotomy" ("x" "a!1" ))"" (split -1)"1" (assert ) (("1" (rewrite "sin_approx_neg" ) nil nil ))nil )"2" (replace -1)"2" (assert )"2" (rewrite "sin_approx_a0" )"2" (rewrite "sin_approx_a0" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (assert ) (("3" (rewrite "sin_approx_neg" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" trig_approx nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_axioms nil )"[numfield, numfield -> numfield]" number_fields nil )nil trig_approx nil )"even_int" integers nil )"posint" nil )"odd_int" integers nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"[numfield, 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 )nil trig_approx nil )"real" trig_approx nil ))nil 3321098748"" (skosimp)"" (lemma "sin_lb_neg" ("a" "-a!1" "n" "n!1" ))"" (assert ) nil nil )) nil ))nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_approx nil )"real" reals nil ))nil 3321123319"" (expand "sin_lb" )"" (skosimp) (("" (rewrite "sin_approx_a0" ) nil nil )) nil )) nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, 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 )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_approx nil )"odd_int" integers nil )"posint" nil )"real" trig_approx nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil ))nil 3321123338"" (expand "sin_ub" )"" (skosimp) (("" (rewrite "sin_approx_a0" ) nil nil )) nil )) nil )"[numfield, 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 )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_approx nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"real" trig_approx nil ))nil 3321626202"" (skosimp)"" (expand "sin_lb" )"" (expand "sin_ub" )"" (lift-if)"" (case-replace "n0x!1 < 0" )"1" (expand "sin_approx" )"1" (expand "sigma" 1 2)"1" "sin_term_gt0" ("a" "n0x!1" "n" "1+2*n!1" ))"1" (assert ) nil nil )) nil ))nil ))nil )"2" (assert )"2" (expand "sin_approx" )"2" (expand "sigma" 2 1)"2" "sin_term_lt0" ("a" "n0x!1" "n" "1+2*n!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" trig_approx nil )nil trig_approx nil )"real" trig_approx nil )"posint" nil )"odd_int" integers nil )nil trig_approx nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" sigma "reals/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )nil reals nil )"boolean" notequal 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" trig_approx nil ))nil ))nil 3321007393"" case "FORALL (n: nat, px: posreal): ") "1" (induct "pm" 1)"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (skosimp*)"3" (case-replace "j!1=0" )"1" (inst - "n!1" "px!1" ) (("1" (assert ) nil nil )) nil )"2" (inst - "n!1" "px!1" )"2" (assert )"2" (inst - "1+n!1" "px!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "sin_lb" )"2" (lemma "sin_approx_next" ("a" "px!1" "n" "1+2*n!1" ))"2" "div_mult_pos_lt1" "z" "px!1 * px!1" "py" "(4 * n!1 + 7) * (4 * n!1 + 6)" "x" "1" ))"2" (replace -1 -3 rl)"2" (hide -1)"2" "TT" "px!1 * px!1 / ((4 * n!1 + 7) * (4 * n!1 + 6))" )"2" "sin_term_gt0" "a" "px!1" "n" "2*(1+n!1)" ))"2" (assert )"2" "ST" "sin_term(px!1)(2 + 2 * n!1)" )"2" "both_sides_times_pos_lt1" "pz" "ST" "x" "0" "y" "1-TT" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_props nil )nil trig_approx nil )"real" trig_approx nil )"odd_int" integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"real" reals nil )"even_int" integersnil )"real" reals nil )"posreal" nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil trig_approx nil )"odd_int" integers nil )"nonneg_int" nil )nil defined_types nil )nil naturalnumbers nil )nil integers nil )nil integers nil )"(strict_total_order?[real])" real_props nil )"nonneg_int" nil )"even_int" integersnil )"posint" nil )"even_int" integersnil )"[T, T -> boolean]" equalities nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"posint" 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 real_types nil )"bool" reals nil )nil real_types nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" trig_approx nil ))nil 3321626241"" case "FORALL (n: nat, px: posreal): ") "1" (induct "pm" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (skosimp*)"3" (case-replace "j!1=0" )"1" (inst - "n!1" "px!1" ) (("1" (assert ) nil nil )) nil )"2" (inst - "n!1" "px!1" )"2" (assert )"2" (inst - "n!1+1" "px!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "sin_ub" )"2" (lemma "sin_approx_next" ("a" "px!1" "n" "2*n!1" ))"2" "div_mult_pos_lt1" "z" "px!1 * px!1" "py" "(4 * n!1 + 5) * (4 * n!1 + 4)" "x" "1" ))"2" "TT" "px!1 * px!1 / ((4 * n!1 + 5) * (4 * n!1 + 4))" )"2" (assert )"2" (hide -3)"2" "sin_term_lt0" ("a" "px!1" "n" "1+2*n!1" ))"2" (assert )"2" "ST" "sin_term(px!1)(1 + 2 * n!1)" )"2" "both_sides_times_neg_lt1" "nz" "ST" "y" "0" "x" "1-TT" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_props nil )"real" reals nil )"odd_int" integers nil )nil trig_approx nil )"real" trig_approx nil )"odd_int" integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil real_props nil )"real" reals nil )"posreal" nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil trig_approx nil )"nonneg_int" nil )nil defined_types nil )nil naturalnumbers nil )nil integers nil )nil integers nil )"(strict_total_order?[real])" real_props nil )"nonneg_int" nil )"even_int" integersnil )"posint" nil )"even_int" integersnil )"[T, T -> boolean]" equalities nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"posint" 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 real_types nil )"bool" reals nil )nil real_types nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" trig_approx nil ))nil ))nil 3321014972"" (skosimp)"" (name "EPS" "sin_ub(px!1,n!1+1) - sin_lb(px!1,n!1)" )"" (case "sin_term(px!1)(2*(n!1+1)) = EPS" )"1" (lemma "sin_term_gt0" ("a" "px!1" "n" "2*(n!1+1)" ))"1" (replace -2)"1" (simplify -1)"1" (lemma "sin_approx_sin" ("a" "px!1" ))"1" (expand "sin_lb" )"1" (expand "sin_ub" )"1" "SN" "sin_approx(px!1, 1 + 2 * n!1)" )"1" (inst - "2*(n!1+1)" )"1" "SN2" "sin_approx(px!1, 2 * (n!1 + 1))" )"1" (rewrite "sin_term_next" -1)"1" (replace -3)"1" "M" "(4 * n!1 + 7) * (4 * n!1 + 6)" )"1" rewrite "abs_div" )"1" rewrite "abs_mult" )"1" rewrite "abs_mult" )"1" rewrite "abs_mult" )"1" expand "abs" -1)"1" assert )"1" "div_mult_pos_lt1" "z" "px!1*px!1" "py" "M" "x" "1" ))"1" assert )"1" "both_sides_times_pos_lt1" "pz" "EPS" "x" "px!1 * px!1 / M" "y" "1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 -2)"2" (expand "sin_ub" )"2" (expand "sin_lb" )"2" (expand "sin_approx" )"2" (expand "sigma" -1 1) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" trig_approx nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" trig_approx 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 )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"real" reals nil )"posint" nil )"real" sigma "reals/" )nil trig_approx nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"real" trig_approx nil )"odd_int" integers nil )nil reals nil )"boolean" notequal nil )nil real_props nil )"{j: posint | j >= i}" nil )"(total_order?[real])" nil )"nnreal" nil )nil abs_lems "reals/" )"{y: posreal | y >= x}" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil real_props nil )nil real_props nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" nil )"posreal" nil )"(total_order?[real])" nil )"real" reals nil )"nzint" integers nil )"nnreal" nil )nil real_props nil )nil integers nil )nil integers nil )"real" reals nil )"real" reals nil )"odd_int" integers nil )"even_int" integersnil )"nonneg_int" nil )nil trig_approx nil )nil trig_approx nil )"trig_range" trig_basic nil )"even_int" integersnil )"odd_int" integers nil )"nonneg_int" nil )"[numfield, numfield -> numfield]" number_fields nil )"real" trig_approx nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil ))nil 3321016985"" (skosimp)"" (lemma "sin_ub_dec" ("px" "px!1" "n" "n!1" "pm" "1" ))"" (replace -2)"" (lemma "sin_lb_ub" ("n0x" "px!1" "n" "n!1+1" ))"" (expand "sin_lb" )"" (lemma "sin_approx_sin" ("a" "px!1" "n" "3+2*n!1" ))"" (lemma "sin_term_neg" ("a" "px!1" "n" "3+2*n!1" ))"" (simplify -1)"" (name-replace "S" "sin(px!1)" )"" case "sin_ub(px!1, 1 + n!1) - sin_approx(px!1, 3 + 2 * n!1) = -sin_term(px!1)(3+2*n!1)" )"1" (name-replace "SN" "sin_ub(px!1, n!1)" )"1" "SN1" "sin_ub(px!1, n!1+1)" )"1" "SN3" "sin_approx(px!1, 2*n!1+3)" )"1" (rewrite "sin_term_next" -3)"1" "ST" "sin_term(px!1)(3 + 2 * n!1)" )"1" rewrite "abs_div" )"1" rewrite "abs_mult" )"1" rewrite "abs_mult" )"1" rewrite "abs_mult" )"1" expand "abs" -3)"1" assert )"1" "div_mult_pos_lt1" "z" "px!1*px!1" "py" "72 + 36 * n!1 + (16 * (n!1 * n!1) + 32 * n!1)" "x" "1" ))"1" "both_sides_times_pos_lt1" "pz" "-ST" "x" "px!1 * px!1 / (72 + 36 * n!1 + (16 * (n!1 * n!1) + 32 * n!1))" "y" "1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "sin_ub" )"2" (expand "sin_approx" )"2" (expand "sigma" 1 2)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_types nil )nil real_types nil )nil integers nil )"bool" reals nil )nil integers 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 trig_approx nil )nil reals nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil trig_approx nil )"posint" nil )"posint" nil )"odd_int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"trig_range" trig_basic nil )"real" reals nil )nil trig_approx nil )"[numfield, numfield -> numfield]" number_fields nil )"nzreal" real_typesnil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"real" trig_approx nil )"real" trig_approx nil )"real" trig_approx nil )"int" integers nil )nil trig_approx nil )"even_int" integersnil )"nonneg_int" nil )"even_int" integersnil )"posint" nil )"real" reals nil )"real" reals nil )nil reals nil )nil real_props nil )"{j: posint | j >= i}" nil )"(total_order?[real])" nil )"nnreal" nil )nil abs_lems "reals/" )"{y: posreal | y >= x}" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil real_props nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"(total_order?[real])" nil )"nzint" integers nil )"nnreal" nil )nil real_props nil )"real" sigma "reals/" )"odd_int" integers nil )"odd_int" integers nil )"even_int" integersnil )"[T, T -> boolean]" equalities nil )"real" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )nil trig_basic nil )nil trig_approx nil )"real" trig_approx nil ))nil 3321010974"" (induct "n" )"1" (skosimp)"1" (expand "sin_lb" )"1" (expand "sin_approx" )"1" (expand "sigma" )"1" (expand "sin_term" )"1" (expand "sigma" )"1" (rewrite "expt_x0" )"1" (rewrite "expt_x1" )"1" (rewrite "expt_x1" )"1" (expand "factorial" )"1" (expand "factorial" )"1" (expand "factorial" )"1" (expand "factorial" )"1" assert )"1" case "px!1<=6" )"1" "le_times_le_pos" "nnx" "px!1" "y" "6" "nnz" "px!1" "w" "6" ))"1" (assert ) nil nil ))nil )"2" case "6<px!1" )"1" "1" case "1-px!1*px!1/6 < -6" )"1" "both_sides_times_pos_lt1" "pz" "px!1" "x" "1 - px!1 * px!1 / 6" "y" "-6" ))"1" assert )"1" expand "^" )"1" expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" assert )"1" expand "sigma" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "both_sides_div_pos_lt1" "pz" "6" "x" "42" "y" "px!1*px!1" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst - "px!1" )"2" (assert )"2" (expand "sin_lb" )"2" (lemma "sin_approx_next" ("a" "px!1" "n" "1+2*j!1" ))"2" "div_mult_pos_gt1" "z" "px!1*px!1" "py" "110 + 44 * j!1 + (16 * (j!1 * j!1) + 40 * j!1)" "x" "1" ))"2" (assert )"2" "SN" "sin_approx(px!1, 1 + 2 * j!1)" )"2" "SN2" "sin_approx(px!1, 3 + 2 * j!1)" )"2" "sin_term_gt0" "a" "px!1" "n" "2*(1+j!1)" ))"2" (assert )"2" "ST" "sin_term(px!1)(2 + 2 * j!1)" )"2" case "1-px!1 * px!1 / (42 + 28 * j!1 + (16 * (j!1 * j!1) + 24 * j!1))<0" )"1" "both_sides_times_pos_lt1" "pz" "ST" "x" "1 - px!1 * px!1 / (42 + 28 * j!1 + (16 * (j!1 * j!1) + 24 * j!1))" "y" "0" ))"1" assert )"1" assert )"1" "TT" "(px!1 * px!1 / (42 + 16 * (j!1 * j!1) + 52 * j!1))" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" "2" "2" "div_mult_pos_gt1" "z" "px!1*px!1" "py" "(42 + 28 * j!1 + (16 * (j!1 * j!1) + 24 * j!1))" "x" "1" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nonneg_int" nil )"odd_int" integers nil )nil trig_approx nil )"even_int" integersnil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )nil trig_approx nil )"[T, T -> boolean]" equalities nil )nil extra_real_props nil )"real" trig_approx nil )"nonneg_int" nil )"even_int" integersnil )"int" exponentiation nil )"nzreal" exponentiation nil )"posreal" exponentiation nil )"nzreal" nil )"real" trig_approx nil )nil exponentiation nil )"posint" nil )"odd_int" integers nil )"even_int" integersnil )"nzreal" nil )"real" reals nil )"even_int" integersnil )"bool" reals nil )"(total_order?[real])" nil )nil real_props nil )nil real_props nil )nil real_props nil )"nzreal" exponentiation nil )"posreal" exponentiation nil )"real" exponentiation nil )"real" exponentiation nil )"real" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )"even_int" integers nil )"nzint" integers nil )"real" reals nil )nil sigma_nat "reals/" )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"posnat" factorial "ints/" )"posint" nil )"posreal" nil )nil exponentiation nil )"real" sigma "reals/" )nil naturalnumbers nil )"[numfield -> numfield]" number_fields nil )"real" trig_approx nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil defined_types 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 )"posreal" nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"odd_int" integers nil ))nil 3321626316"" (induct "n" )"1" (skosimp)"1" (expand "sin_ub" )"1" (expand "sin_approx" )"1" (expand "sigma" )"1" (expand "sin_term" )"1" (rewrite "expt_x0" )"1" (rewrite "expt_x1" )"1" (expand "factorial" )"1" (expand "factorial" )"1" (case "px!1<=4" )"1" "le_times_le_pos" "nnx" "px!1" "y" "4" "nnz" "px!1" "w" "4" ))"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst - "px!1" )"2" (assert )"2" (expand "sin_ub" )"2" (lemma "sin_approx_next" ("a" "px!1" "n" "2*j!1" ))"2" (name-replace "SN" "sin_approx(px!1, 2 * j!1)" )"2" "SN2" "sin_approx(px!1, 2 * j!1+2)" )"2" "sin_term_lt0" ("a" "px!1" "n" "1+2*j!1" ))"2" (simplify -1)"2" "ST" "sin_term(px!1)(1 + 2 * j!1)" )"2" "negreal_times_negreal_is_posreal" "nx" "ST" "ny" "1 - px!1 * px!1 / ((2 * (2 * j!1) + 5) * (2 * (2 * j!1) + 4))" ))"1" (assert ) nil nil )"2" (hide -1 -2 -3 2)"2" "div_mult_pos_gt1" "z" "px!1*px!1" "py" "20 + 20 * j!1 + (16 * (j!1 * j!1) + 16 * j!1)" "x" "1" ))"2" (assert ) nil nil )) nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nonneg_int" nil )nil trig_approx nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" reals nil )nil extra_real_props nil )nil trig_approx nil )"odd_int" integers nil )"real" reals nil )"[T, T -> boolean]" equalities nil )"real" trig_approx nil )"nonneg_int" nil )"even_int" integersnil )"int" exponentiation nil )"nzreal" exponentiation nil )"posreal" exponentiation nil )"nzreal" nil )"real" trig_approx nil )nil exponentiation nil )"posreal" nil )nil real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil sigma_nat "reals/" )"bool" reals nil )"posnat" factorial "ints/" )"posint" nil )"nzreal" nil )"even_int" integersnil )"odd_int" integers nil )"posint" nil )"odd_int" integers nil )nil exponentiation nil )"[numfield -> numfield]" number_fields nil )"real" sigma "reals/" )nil naturalnumbers nil )"real" trig_approx nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil defined_types 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 )"posreal" nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil ))nil ))nil 3321098107"" (skosimp)"" (lemma "trichotomy" ("x" "n0x!1" ))"" (split -1)"1" "trich_lt" "x" "n0x!1*n0x!1" "y" "(4*n!1+7)*(4*n!1+6)" ))"1" (split -1)"1" (lemma "sin_lb_lt" ("px" "n0x!1" "n" "n!1" ))"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil )"2" "sin_lb(n0x!1,n!1)=sin_lb(n0x!1,n!1+1)" )"1" (lemma "sin_lb_lt" ("px" "n0x!1" "n" "n!1+1" ))"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil )"2" (hide 2)"2" (expand "sin_lb" )"2" (assert )"2" "sin_approx_eq" "a" "n0x!1" "n" "1+2*n!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (lemma "sin_lb_gt" ("px" "n0x!1" "n" "n!1" ))"1" (typepred "sin(n0x!1)" ) (("1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (lemma "sin_neg" ("a" "n0x!1" ))"3" "both_sides_times_neg_lt1" "nz" "-1" "y" "sin_lb(n0x!1, n!1)" "x" "sin(n0x!1)" ))"3" (replace -1 1 rl)"3" (replace -2 1 rl)"3" (lemma "sin_ub_neg" ("a" "n0x!1" "n" "n!1" ))"3" (replace -1 1 rl)"3" (hide -1 -2 -3)"3" "trich_lt" "x" "-n0x!1*-n0x!1" "y" "(4*n!1+5)*(4*n!1+4)" ))"3" (split -1)"1" "sin_ub_lt" "px" "-n0x!1" "n" "n!1" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" "sin_ub_lt" "px" "-n0x!1" "n" "n!1+1" ))"1" (assert )"1" "sin_ub(-n0x!1, 1 + n!1) = sin_ub(-n0x!1, n!1)" )"1" "1" expand "sin_ub" )"1" "sin_approx_eq" "a" "-n0x!1" "n" "2*n!1" ))"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"3" "sin_ub_gt" "px" "-n0x!1" "n" "n!1" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_axioms nil )nil trig_basic nil )nil trig_approx nil )nil trig_approx nil )"nzreal" real_typesnil )"int" integers nil )"real" trig_approx nil )nil trig_approx nil )nil real_props nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )"nzreal" nil )nil trig_approx nil )"odd_int" integers nil )"(total_order?[real])" nil )"real" trig_basic nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"real" trig_approx nil )"[T, T -> boolean]" equalities nil )nil trig_approx nil )"odd_int" integers nil )nil trig_approx nil )nil real_types nil )"bool" reals nil )nil real_types nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"odd_int" integers nil )"nonneg_int" nil )"even_int" integersnil )"even_int" integersnil )"posint" nil )"nonneg_int" nil )"trig_range" trig_basic nil ))nil 3321099757"" (skosimp)"" (lemma "trichotomy" ("x" "n0x!1" ))"" (split -1)"1" (lemma "sin_lb" ("n0x" "-n0x!1" "n" "n!1" ))"1" (rewrite "sin_lb_neg" )"1" (rewrite "sin_neg" )"1" "both_sides_times_neg_lt1" "nz" "-1" "y" "sin(n0x!1)" "x" "sin_ub(n0x!1, n!1)" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (lemma "sin_lb" ("n0x" "-n0x!1" "n" "n!1" ))"3" (rewrite "sin_neg" )"3" (rewrite "sin_lb_neg" )"3" "both_sides_times_neg_lt1" "nz" "-1" "y" "sin(n0x!1)" "x" "sin_ub(n0x!1, n!1)" ))"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_axioms nil )"[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 )nil trig_approx nil )"nzreal" real_typesnil )nil trig_basic nil )"trig_range" trig_basic nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"real" trig_basic nil )"real" trig_approx nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_props nil )"odd_int" integers nil )"real" reals nil )nil trig_approx nil ))nil 3321009206"" (skosimp)"" (case-replace "a!1=0" )"1" (rewrite "sin_0" )"1" (expand "sin_lb" )"1" (expand "sin_ub" )"1" (rewrite "sin_approx_a0" )"1" (rewrite "sin_approx_a0" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "sin_lb" ("n0x" "a!1" "n" "n!1" ))"1" (lemma "sin_ub" ("n0x" "a!1" "n" "n!1" ))"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))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 )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" trig_approx nil )"posint" nil )"odd_int" integers nil )nil trig_approx 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 )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"real" trig_approx nil )nil trig_basic nil )nil trig_approx nil )"(strict_total_order?[real])" real_props nil )"trig_range" trig_basic nil )nil trig_approx nil )"boolean" notequal nil )nil reals nil ))nil 3321123536"" (skosimp*)"" (case "sin_lb(px!1,0) > 0" )"1" (case-replace "n!1=0" )"1" (lemma "sin_lb_inc" ("px" "px!1" "n" "0" "pm" "n!1" ))"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (expand "sin_lb" )"2" (expand "sin_approx" )"2" (expand "sigma" )"2" (expand "sigma" )"2" (expand "sin_term" )"2" (expand "^" )"2" (expand "expt" )"2" (expand "expt" )"2" (expand "expt" )"2" (expand "expt" )"2" (expand "factorial" )"2" expand "factorial" )"2" expand "factorial" )"2" expand "factorial" )"2" "posreal_times_posreal_is_posreal" "px" "px!1/6" "py" "6-px!1*px!1" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_types nil )nil real_types nil )"real" trig_approx nil )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 integers nil )nil integers nil )nil trig_approx nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"posint" nil )"odd_int" integers nil )"nonneg_int" nil )"even_int" integersnil )"even_int" integersnil )"[T, T -> boolean]" equalities nil )"real" sigma "reals/" )"int" exponentiation nil )"nzreal" exponentiation nil )"posreal" exponentiation nil )"nzreal" nil )"real" trig_approx nil )"real" exponentiation nil )"posnat" factorial "ints/" )"posreal" nil )"real" reals nil )nil real_types nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" reals nil )"real" reals nil )"real" reals nil )"nzreal" nil )nil sigma_nat "reals/" )"even_int" integersnil )"real" exponentiation nil )"posreal" exponentiation nil )"nzreal" exponentiation nil )"int" exponentiation nil )"real" trig_approx nil ))nil 3321100129"" (skosimp)"" (expand "cos_lb" ) (("" (rewrite "cos_approx_neg" ) nil nil ))nil ))nil )"real" trig_approx nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, 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 )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_approx nil )"odd_int" integers nil )"posint" nil ))nil 3321100152"" (skosimp)"" (expand "cos_ub" ) (("" (rewrite "cos_approx_neg" ) nil nil ))nil ))nil )"real" trig_approx nil )"[numfield, 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 )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_approx nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil ))nil 3321123502"" (expand "cos_lb" )"" (skosimp) (("" (rewrite "cos_approx_a0" ) nil nil )) nil )) nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, 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 )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_approx nil )"odd_int" integers nil )"posint" nil )"real" trig_approx nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil ))nil 3321123407"" (expand "cos_ub" )"" (skosimp) (("" (rewrite "cos_approx_a0" ) nil nil )) nil )) nil )"[numfield, 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 )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_approx nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"real" trig_approx nil ))nil 3321626381"" (skosimp)"" (expand "cos_lb" )"" (expand "cos_ub" )"" (expand "cos_approx" )"" (expand "sigma" 1 1)"" (lemma "cos_term_lt0" ("a" "n0x!1" "n" "1+2*n!1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"real" trig_approx nil )"real" trig_approx nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, 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 )nil reals nil )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_approx nil )"odd_int" integers nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(total_order?[real])" nil )"real" sigma "reals/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"real" trig_approx nil ))nil ))nil 3321021787"" case "FORALL (n: nat, n0x: nzreal): ") "1" (induct "pm" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (skosimp*)"3" (inst - "n!1" "n0x!1" )"3" (replace -3)"3" (case-replace "j!1=0" )"1" (assert ) nil nil )"2" (assert )"2" (inst - "n!1+1" "n0x!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "cos_lb" )"2" (lemma "cos_approx_next" ("a" "n0x!1" "n" "1+2*n!1" ))"2" (lemma "cos_term_gt0" ("a" "n0x!1" "n" "2*(1+n!1)" ))"2" (simplify -1)"2" "CT" "cos_term(n0x!1)(2 + 2 * n!1)" )"2" "CN" "cos_approx(n0x!1, 1 + 2 * n!1)" )"2" "CN2" "cos_approx(n0x!1, 3 + 2 * n!1)" )"2" "div_mult_pos_lt1" "z" "n0x!1*n0x!1" "py" "(4 * n!1 + 6) * (4 * n!1 + 5)" "x" "1" ))"2" "TT" "n0x!1 * n0x!1 / ((4 * n!1 + 6) * (4 * n!1 + 5))" )"2" (assert )"2" "posreal_times_posreal_is_posreal" "px" "CT" "py" "1-TT" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trig_approx nil )"real" trig_approx nil )"even_int" integersnil )"real" reals nil )"nzreal" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" reals nil )"even_int" integersnil )nil real_types nil )nil real_types nil )nil real_props nil )"real" trig_approx nil )nil trig_approx nil )"odd_int" integers nil )"nonneg_int" nil )"bool" reals nil )nil defined_types nil )nil naturalnumbers nil )nil integers nil )nil integers nil )"(strict_total_order?[real])" real_props nil )"nonneg_int" nil )"posint" nil )"even_int" integersnil )"[T, T -> boolean]" equalities nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"posint" 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 )"boolean" notequal nil )nil reals nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" trig_approx nil ))nil 3321626426"" case "FORALL (n: nat, n0x: nzreal): ") "1" (induct "pm" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (skosimp*)"3" (inst - "n!1" "n0x!1" )"3" (case-replace "j!1=0" )"1" (assert ) nil nil )"2" (assert )"2" (inst - "n!1+1" "n0x!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "cos_ub" )"2" (lemma "cos_approx_next" ("a" "n0x!1" "n" "2*n!1" ))"2" "div_mult_pos_lt1" "z" "n0x!1 * n0x!1" "py" "(4 * n!1 + 4) * (4 * n!1 + 3)" "x" "1" ))"2" (lemma "cos_term_lt0" ("a" "n0x!1" "n" "1+2*n!1" ))"2" "TT" "n0x!1 * n0x!1 / ((4 * n!1 + 4) * (4 * n!1 + 3))" )"2" "CT" "cos_term(n0x!1)(1 + 2 * n!1)" )"2" (assert )"2" "both_sides_times_pos_lt1" "pz" "1-TT" "x" "CT" "y" "0" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_props nil )nil real_types nil )nil real_types nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"nzreal" nil )"real" reals nil )"even_int" integersnil )"real" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"real" trig_approx nil )nil trig_approx nil )"odd_int" integers nil )nil trig_approx nil )"nonneg_int" nil )"bool" reals nil )nil defined_types nil )nil naturalnumbers nil )nil integers nil )nil integers nil )"(strict_total_order?[real])" real_props nil )"nonneg_int" nil )"posint" nil )"even_int" integersnil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"[T, T -> boolean]" equalities nil )"nzreal" nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"posint" 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 )"boolean" notequal nil )nil reals nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" trig_approx nil ))nil ))nil 3321023357"" (skosimp)"" (lemma "cos_lb_inc" ("n0x" "n0x!1" "n" "n!1" "pm" "1" ))"" (replace -2 -1)"" (lemma "cos_lb_ub" ("n0x" "n0x!1" "n" "n!1+1" ))"" (expand "cos_lb" )"" (expand "cos_ub" )"" "cos_approx_next" "a" "n0x!1" "n" "1 + 2 * n!1" ))"" "cos_term_gt0" ("a" "n0x!1" "n" "2*(1+n!1)" ))"" (simplify -1)"" "cos_approx_cos" "a" "n0x!1" "n" "2*(1+n!1)" ))"" (name-replace "CC" "cos(n0x!1)" )"" (rewrite "cos_term_next" -1)"" case "cos_approx(n0x!1, 2 + 2 * n!1) - cos_approx(n0x!1, 3 + 2 * n!1) = -cos_term(n0x!1)(3 + 2 * n!1)" )"1" "CN1" "cos_approx(n0x!1, 1 + 2 * n!1)" )"1" "CN2" "cos_approx(n0x!1, 2 + 2 * n!1)" )"1" "CN3" "cos_approx(n0x!1, 3 + 2 * n!1)" )"1" rewrite "cos_term_next" -1)"1" "CT" "cos_term(n0x!1)(2 + 2 * n!1)" )"1" "div_mult_pos_lt1" "z" "n0x!1 * n0x!1" "py" "(4 * n!1 + 6) * (4 * n!1 + 5)" "x" "1" ))"1" replace -8 -1)"1" "1" "M" "(4 * n!1 + 6) * (4 * n!1 + 5)" )"1" "-1 * (CT * n0x!1 * n0x!1) / M = -CT*((n0x!1 * n0x!1) / M)" )"1" "posreal_div_posreal_is_posreal" "px" "n0x!1*n0x!1" "py" "M" ))"1" "TT" "n0x!1 * n0x!1 / M" )"1" rewrite "abs_mult" "1" expand "abs" "1" "CC - CN2 < 0" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" expand "cos_approx" )"2" expand "sigma" 1 2)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integers nil )"bool" reals nil )nil integers nil )nil reals nil )"boolean" notequal 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 trig_approx nil )"posint" nil )nil trig_approx nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" trig_approx nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil trig_approx nil )"trig_range" trig_basic nil )"real" reals nil )nil trig_approx nil )nil trig_approx nil )"nonneg_int" nil )"even_int" integersnil )"real" reals nil )"real" reals nil )"real" sigma "reals/" )nil integers nil )nil real_types nil )nil real_props nil )"{y: posreal | y >= x}" nil )"nnreal" nil )"bool" reals nil )"(total_order?[real])" nil )"nzreal" real_typesnil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )nil real_types nil )nil real_props nil )"odd_int" integersnil )"even_int" integersnil )"(total_order?[real])" nil )"real" trig_approx nil )"real" trig_approx nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"odd_int" integers nil )"odd_int" integers nil )"nzreal" nil )"nzreal" nil )"[T, T -> boolean]" equalities nil )"real" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )nil trig_basic nil )"even_int" integersnil )"nonneg_int" nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil trig_approx nil )"odd_int" integers nil )"posint" nil )"real" trig_approx nil ))nil 3321030211"" (skosimp)"" (lemma "cos_ub_dec" ("n0x" "n0x!1" "n" "n!1" "pm" "1" ))"" (replace -2 -1)"" (lemma "cos_lb_ub" ("n0x" "n0x!1" "n" "n!1+1" ))"" case "cos_ub(n0x!1, n!1 + 1) - cos_lb(n0x!1, n!1+1) = -cos_term(n0x!1)(3+2*n!1)" )"1" (lemma "cos_approx_cos" ("a" "n0x!1" "n" "2*n!1+3" ))"1" (expand "cos_lb" )"1" (name-replace "CC" "cos(n0x!1)" )"1" "CN3" "cos_approx(n0x!1, 2 * n!1 + 3)" )"1" (rewrite "cos_term_next" -1)"1" "cos_term_neg" "a" "n0x!1" "n" "3+2*n!1" ))"1" (simplify -1)"1" "CT" "cos_term(n0x!1)(3 + 2 * n!1)" )"1" "div_mult_pos_lt1" "z" "n0x!1 * n0x!1" "py" "(56 + 32 * n!1 + (16 * (n!1 * n!1) + 28 * n!1))" "x" "1" ))"1" assert )"1" "posreal_div_posreal_is_posreal" "px" "n0x!1 * n0x!1" "py" "(56 + 16 * (n!1 * n!1) + 60 * n!1)" ))"1" "(-1 * (CT * n0x!1 * n0x!1) / ") "1" "TT" "((n0x!1 * n0x!1) / (56 + 32 * n!1 + (16 * (n!1 * n!1) + 28 * n!1)))" )"1" "1" rewrite "abs_mult" -4)"1" expand "abs" -4)"1" assert )"1" "both_sides_times_pos_lt1" "pz" "-CT" "x" "TT" "y" "1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "cos_ub" )"2" (expand "cos_lb" )"2" (expand "cos_approx" )"2" (expand "sigma" 1 2) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integers nil )"bool" reals nil )nil integers nil )nil reals nil )"boolean" notequal 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 trig_approx nil )"posint" nil )nil trig_approx nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" sigma "reals/" )"odd_int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"trig_range" trig_basic nil )nil trig_approx nil )nil trig_basic nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" trig_basic nil )"even_int" integersnil )"odd_int" integers nil )nil trig_approx nil )"nonneg_int" nil )"even_int" integersnil )"posint" nil )"real" reals nil )"real" reals nil )"nzreal" real_typesnil )"nzreal" nil )nil real_props nil )nil real_types nil )nil real_types nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"{y: posreal | y >= x}" nil )"nnreal" nil )nil real_props nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"even_int" integersnil )nil trig_approx nil )"real" trig_approx nil )"[numfield, numfield -> numfield]" number_fields nil )"real" trig_approx nil )"[numfield -> numfield]" number_fields nil )"real" trig_approx nil )"real" trig_approx nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"odd_int" integers nil )"posint" nil )"real" reals nil )"real" reals nil ))nil 3321027181"" (induct "n" )"1" (skosimp)"1" (expand "cos_lb" )"1" (expand "cos_approx" )"1" (expand "sigma" )"1" (expand "sigma" )"1" (expand "cos_term" )"1" (rewrite "expt_x1" )"1" (expand "factorial" )"1" (expand "factorial" )"1" (expand "factorial" )"1" (expand "^" )"1" (expand "expt" )"1" (expand "expt" )"1" expand "expt" )"1" assert )"1" expand "sigma" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "cos_lb" )"2" (inst - "n0x!1" )"2" (lemma "cos_approx_next" ("a" "n0x!1" "n" "1+2*j!1" ))"2" (name-replace "CN1" "cos_approx(n0x!1, 1 + 2 * j!1)" )"2" "CN3" "cos_approx(n0x!1, 3 + 2 * j!1)" )"2" "cos_term_gt0" ("a" "n0x!1" "n" "2*(1+j!1)" ))"2" (simplify -1)"2" "CT" "cos_term(n0x!1)(1 + 2 * j!1 + 1)" )"2" (assert )"2" "div_mult_pos_gt1" "z" "n0x!1*n0x!1" "py" "(30 + 24 * j!1 + (16 * (j!1 * j!1) + 20 * j!1))" "x" "1" ))"2" (assert )"2" "TT" "n0x!1 * n0x!1 / (30 + 16 * (j!1 * j!1) + 44 * j!1)" )"2" "both_sides_times_pos_lt1" "pz" "CT" "x" "1-TT" "y" "0" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T, T -> boolean]" equalities nil )"real" reals nil )nil trig_approx nil )"even_int" integersnil )"odd_int" integersnil )nil extra_real_props nil )nil real_types nil )nil real_types nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"even_int" integersnil )"real" reals nil )nil trig_approx nil )"odd_int" integers nil )"nonneg_int" nil )"posint" nil )"real" trig_approx nil )nil exponentiation nil )"nonneg_int" nil )"posint" nil )"even_int" integersnil )"odd_int" integers nil )"real" reals nil )"nzreal" nil )"nzreal" exponentiation nil )"real" exponentiation nil )nil sigma_nat "reals/" )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"nzint" integersnil )"real" exponentiation nil )"int" exponentiation nil )"even_int" integersnil )"posnat" factorial "ints/" )"real" trig_approx nil )"nzreal" exponentiation nil )"int" exponentiation nil )"real" sigma "reals/" )nil naturalnumbers nil )"[numfield -> numfield]" number_fields nil )"real" trig_approx nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )nil reals nil )"boolean" notequal nil )nil defined_types 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 )"nzreal" nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"odd_int" integers nil ))nil 3321626563"" case "FORALL (n: nat, px: posreal): ") "1" (skosimp)"1" (lemma "trichotomy" ("x" "n0x!1" ))"1" (split -1)"1" (inst - "n!1" "n0x!1" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil )"2" (assert ) nil nil )"3" (inst - "n!1" "-n0x!1" )"1" (assert )"1" (expand "cos_ub" )"1" (rewrite "cos_approx_neg" ) nil nil )) nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "n" )"1" (skosimp) (("1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (case-replace "j!1=0" )"1" (assert )"1" (hide -1 -2 -4)"1" (expand "cos_ub" )"1" (expand "cos_approx" )"1" (expand "sigma" )"1" (expand "sigma" )"1" (expand "sigma" )"1" (expand "cos_term" )"1" (expand "factorial" )"1" expand "factorial" )"1" expand "factorial" )"1" expand "factorial" )"1" expand "factorial" )"1" rewrite "expt_x1" )"1" "expt_times" "n0x" "px!1" "i" "2" "j" "2" ))"1" "px!1^2=px!1*px!1" )"1" replace -2)"1" "X" "px!1 * px!1" )"1" "1" expand "^" )"1" expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" "posreal_times_posreal_is_posreal" "px" "X" "py" "X/24-1/2" ))"1" assert )"1" expand "sigma" )"1" assert )nil nil ))nil ))nil )"2" "2" "both_sides_times_pos_lt1" "pz" "24" "x" "0" "y" "X / 24 - 1 / 2" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst - "px!1" )"2" (expand "cos_ub" )"2" "cos_approx_next" ("a" "px!1" "n" "2*j!1" ))"2" "cos_term_lt0" ("a" "px!1" "n" "2*j!1+1" ))"2" (simplify -1)"2" "CT" "cos_term(px!1)(1 + 2 * j!1)" )"2" "div_mult_pos_gt1" "z" "px!1*px!1" "py" "(4*j!1+4)*(4*j!1+3)" "x" "1" ))"2" "TT" "px!1 * px!1 / ((4 * j!1 + 4) * (4 * j!1 + 3))" )"2" (assert )"2" "negreal_times_negreal_is_posreal" "nx" "CT" "ny" "1-TT" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trig_approx nil )"odd_int" integers nil )nil extra_real_props nil )"even_int" integersnil )"(total_order?[real])" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil trig_approx nil )"real" sigma "reals/" )"posnat" factorial "ints/" )"even_int" integersnil )nil exponentiation nil )"real" exponentiation nil )"nzint" integersnil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil sigma_nat "reals/" )"posrat" nil )"real" reals nil )"posreal" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"real" reals nil )"posreal" exponentiation nil )"nzreal" exponentiation nil )"int" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"nzreal" nil )"real" reals nil )"odd_int" integers nil )nil exponentiation nil )"real" trig_approx nil )"posreal" exponentiation nil )"nzreal" exponentiation nil )"int" exponentiation nil )"real" trig_approx nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )nil defined_types nil )"nonneg_int" nil )"posint" nil )"odd_int" integers nil )"nonneg_int" nil )"even_int" integersnil )"posint" nil )"nzreal" nil )"nzreal" trig_approx nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil trig_approx nil )"[numfield -> numfield]" number_fields nil )"nzreal" real_typesnil )nil reals nil )"boolean" notequal nil )nil real_axioms nil )"posreal" nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides 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 real_types nil )"bool" reals nil )nil real_types nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" trig_approx nil ))nil ))nil 3321021268"" (skosimp)"" "trich_lt" ("x" "n0x!1*n0x!1" "y" "(4*n!1+6)*(4*n!1+5)" ))"" (split -1)"1" (lemma "cos_lb_lt" ("n0x" "n0x!1" "n" "n!1" ))"1" (assert ) nil nil )) nil )"2" (lemma "cos_lb_lt" ("n0x" "n0x!1" "n" "n!1+1" ))"2" "cos_lb(n0x!1, n!1 + 1) = cos_lb(n0x!1, n!1)" )"1" (assert ) nil nil )"2" (hide 2 -1)"2" (expand "cos_lb" )"2" "cos_approx_eq" ("a" "n0x!1" "n" "1+2*n!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (lemma "cos_lb_gt" ("n0x" "n0x!1" "n" "n!1" ))"3" (assert ) nil nil )) nil ))nil ))nil ))nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )"nzreal" nil )nil trig_approx nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )nil trig_approx nil )"int" integers nil )"[T, T -> boolean]" equalities nil )"real" trig_approx nil )nil trig_approx nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"even_int" integersnil )"nonneg_int" nil )"odd_int" integers nil )"posint" nil )"nonneg_int" nil )"trig_range" trig_basic nil ))nil 3321029937"" (skosimp)"" "trich_lt" "x" "n0x!1*n0x!1" "y" "(4*pm!1+4)*(4*pm!1+3)" ))"" (split -1)"1" (lemma "cos_ub_lt" ("n0x" "n0x!1" "n" "pm!1" ))"1" (assert ) nil nil )) nil )"2" (lemma "cos_ub_lt" ("n0x" "n0x!1" "n" "pm!1+1" ))"2" "cos_ub(n0x!1, pm!1 + 1) = cos_ub(n0x!1, pm!1)" )"1" (assert ) nil nil )"2" (hide -1 2)"2" (expand "cos_ub" )"2" "cos_approx_eq" ("a" "n0x!1" "n" "2*pm!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (lemma "cos_ub_gt" ("n0x" "n0x!1" "n" "pm!1" ))"3" (typepred "cos(n0x!1)" ) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )"nzreal" nil )nil trig_approx nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"(total_order?[real])" nil )"real" trig_basic nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil trig_approx nil )"int" integers nil )"[T, T -> boolean]" equalities nil )"real" trig_approx nil )nil trig_approx nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"even_int" integersnil )"odd_int" integers nil )"trig_range" trig_basic nil ))nil 3321021088"" (skosimp)"" (case-replace "a!1=0" )"1" (rewrite "cos_0" )"1" (expand "cos_lb" )"1" (expand "cos_ub" )"1" (rewrite "cos_approx_a0" )"1" (rewrite "cos_approx_a0" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "cos_lb" ("n0x" "a!1" "n" "n!1" ))"1" (assert )"1" (hide -1)"1" (case "n!1=0" )"1" (expand "cos_ub" )"1" (expand "cos_approx" )"1" (replace -1)"1" (expand "sigma" )"1" (expand "cos_term" )"1" (typepred "cos(a!1)" )"1" (expand "sigma" )"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "cos_ub" ("n0x" "a!1" "pm" "n!1" ))"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))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 )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" trig_approx nil )"posint" nil )"odd_int" integers nil )nil trig_approx 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 )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"real" trig_approx nil )nil trig_basic nil )"trig_range" trig_basic nil )"(strict_total_order?[real])" real_props nil )"real" trig_approx nil )"real" sigma "reals/" )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"real" trig_basic nil )"real" trig_approx nil )"(strict_total_order?[real])" real_props nil )nil integers nil )"bool" reals nil )nil integers nil )nil trig_approx nil )nil trig_approx nil )"boolean" notequal nil )nil reals nil ))nil 3321105839"" (expand "strict_decreasing?" )"" (skosimp*)"" (typepred "x!1" )"" (typepred "y!1" )"" (expand ">=" )"" (expand "<=" -3)"" (split -3)"1" (lemma "cos_lb_deriv" ("n" "n!1" ))"1" (flatten)"1" "restrict2_derivable[{x: posreal | x <= pi},real]" "f" "LAMBDA a: cos_lb(a, n!1)" ))"1" "restrict2_deriv[{x: posreal | x <= pi},real]" "f" "LAMBDA a: cos_lb(a, n!1)" ))"1" (expand "restrict2" )"1" (replace -4)"1" (simplify -1)"1" "negative_derivative[{x:posreal | x <= pi}]" "g" "LAMBDA (a:{x:posreal | x <= pi}): cos_lb(a, n!1)" ))"1" "1" expand "strict_decreasing?" )"1" "x!1" "y!1" )"1" (assert ) nil nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil )"2" "2" "x!2" )"2" expand "deriv" -1)"2" replace -1 1 rl)"2" "2" "x!2" )"2" "sin_ub" "n0x" "x!2" "n" "n!1" ))"2" "sin_ge_0" "a" "x!2" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil )"3" (hide-all-but 1)"3" (skosimp) (("3" (inst 1 "x!2" ) nil nil ))nil ))nil )"4" (hide-all-but 1)"4" (skosimp)"4" (inst 1 "x!2+1" )"4" (assert ) nil nil )) nil ))nil ))nil )"5" (hide-all-but 1)"5" (skosimp)"5" (typepred "x!2" )"5" (case-replace "x!2=pi" )"1" "pi/2" )"1" (assert ) nil nil ))nil )"2" "pi" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"6" (hide-all-but 1)"6" (skosimp*) (("6" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (replace -1 * rl)"2" (lemma "cos_lb" ("n0x" "y!1" "n" "n!1" ))"1" (typepred "cos(y!1)" )"1" (expand "cos_lb" )"1" (rewrite "cos_approx_a0" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trig_ineq nil )"bool" real_fun_preds "reals/" ))nil 3321105605"" (skosimp)"" (lemma "cos_lb_nn_strict_decreasing" ("n" "n!1" ))"" (expand "strict_decreasing?" )"" (expand "strict_increasing?" )"" (skosimp)"" (inst - "-y!1" "-x!1" )"" (assert )"" (rewrite "cos_lb_neg" )"" (rewrite "cos_lb_neg" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 trig_approx nil )"bool" real_fun_preds "reals/" )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil real_types nil )nil trig_approx nil )"(strict_total_order?[real])" real_props nil )"bool" real_fun_preds "reals/" ))nil 3408806447"" (skosimp)"" (lemma "sin_lb" ("n0x" "px!1" "n" "0" ))"" (expand "sin_lb" )"" (expand "sin_approx" )"" (expand "sigma" )"" (expand "sigma" )"" (expand "sin_term" )"" (expand "^" )"" (expand "expt" )"" (expand "expt" )"" (expand "expt" )"" (expand "expt" )"" (expand "factorial" )"" (expand "factorial" )"" expand "factorial" )"" expand "factorial" )"" case "1 - 1 / 1500000 < 1-px!1*px!1/6" )"1" "both_sides_times_pos_lt1" "pz" "px!1" "x" "1 - 1 / 1500000" "y" "1 - px!1 * px!1 / 6" ))"1" (assert ) nil nil ))nil )"2" "2" "sq_lt" "nna" "px!1" "nnb" "1/500" ))"2" assert )"2" expand "sq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil reals nil )"boolean" notequal 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 trig_approx nil )"real" trig_approx nil )"int" exponentiation nil )"nzreal" exponentiation nil )"posreal" exponentiation nil )"real" exponentiation nil )"even_int" integersnil )"posreal" sq "reals/" )"nonneg_real" sq "reals/" )nil sq "reals/" )nil real_props nil )"(strict_total_order?[real])" real_props nil )"posrat" nil )"posreal" nil )"real" reals nil )"real" reals nil )"nzreal" nil )"trig_range" trig_basic nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil sigma_nat "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )"real" reals nil )"rat" rationals nil )"posnat" factorial "ints/" )"posint" nil )"real" exponentiation nil )"posreal" nil )"real" trig_approx nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"nzreal" nil )"posreal" exponentiation nil )"nzreal" exponentiation nil )"int" exponentiation nil )"real" sigma "reals/" )"real" trig_approx nil ))nil ))nil 3408810875"" (skosimp)"" (rewrite "sin_shift" :dir rl)"" (lemma "pi_lb_diff" ("n" "n!1" ))"" (lemma "pi_lb_inc" ("n" "n!1" "m" "n!1+1" ))"" (simplify -1)"" (lemma "pi_bounds" ("n" "n!1+1" ))"" (flatten)"" (hide -2)"" "KK" "16 * (1 / 5) ^ (4 * n!1 + 5) * ") "" (replace -1)"" (case "pi / 2 - pi_lbn(n!1) / 2 > KK / 2" )"1" (case "pi / 2 - pi_lbn(n!1) / 2 < 1/500" )"1" "sin_px" "px" "pi / 2 - pi_lbn(n!1) / 2" ))"1" (split -1)"1" case "cos_term(pi_lbn(n!1) / 2)(2 * n!1 + 2) < KK/2 * (1 - 1 / 1500000)" )"1" (assert ) nil nil )"2" "2" "2" "F" "lambda (n:nat): 8 * (1 / 5) ^ (4 * n + 5) * ") "2" "KK/2=F(n!1)" )"1" "1" expand "cos_term" )"1" "(-1) ^ (2 + 2 * n!1)=1" )"1" "both_sides_expt_pos_lt" "px" "pi_lbn(n!1) / 2" "py" "31415927/20000000" "pm" "4 + 4 * n!1" ))"1" assert )"1" "pi_ub" )"1" assert )"1" "G" "lambda (n:nat): (31415927 / 20000000) ^ (4 + 4 * n)/factorial(4 + 4 * n)" )"1" case "(1 * (pi_lbn(n!1) / 2) ^ (4 + 4 * n!1)) / factorial(4 + 4 * n!1) <G(n!1)" )"1" case "forall (m:nat): m>=5 => G(m)<F(m)*(1 - 1 / 1500000)" )"1" "n!1" )"1" assert )"1" "DRL1" "(1 * (pi_lbn(n!1) / 2) ^ (4 + 4 * n!1)) / factorial(4 + 4 * n!1)" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" case "G(5) < F(5) * (1 - 1 / 1500000)" )"1" case "FORALL (m: nat): m >= 5 & G(m) < F(m) * (1 - 1 / 1500000) => G(m+1) < F(m+1) * (1 - 1 / 1500000)" )"1" "m" )"1" "1" assert )nil nil ))nil )"2" "2" "j!1=4" )"1" assert )nil nil )"2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "LHS" "(31415927 / 20000000) ^ 4/((5+4 * m!1)*(6+4 * m!1)*(7+4 * m!1)*(8+4 * m!1))" )"2" "G(m!1 + 1)=G(m!1)*LHS" )"1" "1" case "LHS*F(m!1)<F(m!1 + 1)" )"1" "both_sides_times_pos_lt1" "pz" "LHS" "x" "G(m!1)" "y" "F(m!1) * (1 - 1 / 1500000)" ))"1" assert )nil nil ))nil )"2" "2" expand "F" "2" "expt_plus" "n0x" "1/5" "i" "4" "j" "5+4*m!1" ))"2" replace "2" "2" "FIVE" "(1 / 5) ^ (5 + 4 * m!1)" )"2" "expt_plus" "n0x" "1 / 239" "i" "4" "j" "3 + 4 * m!1" ))"2" replace "2" "2" "TWOTHREENINE" "(1 / 239) ^ (3 + 4 * m!1)" )"2" "(1 / 239) ^ 4 * TWOTHREENINE * (1 / (514089 + 228484 * m!1))= (1 / 239) ^ 6 * TWOTHREENINE * (1 / (9+4*m!1))" )"1" "1" "(TWOTHREENINE * (1 / (285605 + 228484 * m!1))) = (1/239)^2 * (TWOTHREENINE * (1 / (5 + 4 * m!1)))" )"1" "1" "(FIVE * (1 / (175 + 100 * m!1))) = (1/5)^2*FIVE*(1/(7+4*m!1))" )"1" "1" case "-2 * ((1 / 239) ^ 2 * (TWOTHREENINE * (1 / (5 + 4 * m!1))) * LHS) - ") "1" case "8 * ((FIVE * (1 / (5 + 4 * m!1))) * LHS)<8 * ((1 / 5) ^ 4 * FIVE * (1 / (9 + 4 * m!1))) + ") "1" assert )nil nil )"2" "2" "expt_plus" "n0x" "1/239" "i" "2" "j" "4" ))"2" replace "2" "2" "both_sides_times_pos_lt1" "pz" "2 * (1 / 239) ^ 4 * TWOTHREENINE" "y" "1 / (7 + 4 * m!1) -(1 / 239) ^ 2/ (9 + 4 * m!1)" "x" "0" ))"2" "2" "2" "1" case "8 * ((FIVE * (1 / (5 + 4 * m!1))) * LHS) <8 * ((1 / 5) ^ 4 * FIVE * (1 / (9 + 4 * m!1))) - 8 * ((1 / 5) ^ 4 * FIVE * (1 / (275 + 100 * m!1)))" )"1" assert )nil nil )"2" "2" "1 / (275 + 100 * m!1) = (1/5)^2*1/(11+4*m!1)" )"1" "1" "both_sides_times_pos_lt1" "pz" "8*FIVE" "x" "LHS/(5 + 4 * m!1)" "y" "(1 / 5) ^ 4*(1 / (9 + 4 * m!1) - (1 / 5) ^ 2 / (11 + 4 * m!1))" ))"1" replace "1" "1" case "(24/25)*(1 / (9 + 4 * m!1)) < (1 / (9 + 4 * m!1) - (1 / 5) ^ 2 / (11 + 4 * m!1))" )"1" case "LHS / (5 + 4 * m!1) <(1 / 5) ^ 4 *(24 / 25) * (1 / (9 + 4 * m!1))" )"1" "RHS" "(1 / (9 + 4 * m!1) - (1 / 5) ^ 2 / (11 + 4 * m!1))" )"1" "both_sides_times_pos_lt1" "pz" "(1/5)^4" "x" "(24 / 25) * (1 / (9 + 4 * m!1))" "y" "RHS" ))"1" assert )nil nil ))nil ))nil )"2" "2" "2" case "(31415927 / 20000000) ^ 4 < 609/100" )"1" "both_sides_div_pos_lt1" "pz" "((5 + 4 * m!1) * (6 + 4 * m!1) * (7 + 4 * m!1) * (8 + 4 * m!1))" "x" "(31415927 / 20000000) ^ 4" "y" "609 / 100" ))"1" replace "1" replace "1" "1" case "LHS < (1 / 5) ^ 4 * (12/15)" )"1" "1" "both_sides_div_pos_lt1" "pz" "5 + 4 * m!1" "x" "LHS" "y" "(1 / 5) ^ 4 * (12 / 15)" ))"1" replace "1" "1" "both_sides_times_pos_lt1" "pz" "(1 / 5) ^ 4" "x" "(12 / 15) / (5 + 4 * m!1)" "y" "(24 / 25) * (1 / (9 + 4 * m!1))" ))"1" "1" "1" "1" assert )nil nil )"2" "2" "both_sides_times_pos_lt1" "pz" "12/75" "x" "5/(5 + 4 * m!1)" "y" "6/(9 + 4 * m!1)" ))"2" replace "2" "2" "div_mult_pos_lt1" "py" "5 + 4 * m!1" "z" "5" "x" "6 / (9 + 4 * m!1)" ))"2" replace "2" "div_mult_pos_lt2" "py" "9 + 4 * m!1" "z" "6*(5 + 4 * m!1)" "x" "5" ))"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "(1 / 5) ^ 4 * (12 / 15) = 12/9375" )"1" "1" "both_sides_div_pos_le2" "pz" "609/100" "py" "25*26*27*28" "px" "((5 + 4 * m!1) * (6 + 4 * m!1) * (7 + 4 * m!1) * (8 + 4 * m!1))" ))"1" "1" "1" "1" "LHS2" "609 / 100 / ") "1" assert )nil nil ))nil )"2" "2" "le_times_le_pos" "nnx" "25" "y" "5 + 4 * m!1" "nnz" "26 * 27 * 28" "w" "(6 + 4 * m!1) * (7 + 4 * m!1) * (8 + 4 * m!1)" ))"2" "le_times_le_pos" "nnx" "26" "y" "6 + 4 * m!1" "nnz" "27 * 28" "w" "(7 + 4 * m!1) * (8 + 4 * m!1)" ))"2" "le_times_le_pos" "nnx" "27" "y" "7 + 4 * m!1" "nnz" "28" "w" "(8 + 4 * m!1)" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "both_sides_times_pos_lt1" "pz" "9 + 4 * m!1" "x" "(24 / 25) * (1 / (9 + 4 * m!1))" "y" "(1 / (9 + 4 * m!1) - (1 / 5) ^ 2 / (11 + 4 * m!1))" ))"2" replace "2" "2" "div_cancel2" "x" "1" "n0z" "9+4*m!1" ))"2" "associative_mult" "x" "24 / 25" "y" "1 / (9 + 4 * m!1)" "z" "9 + 4 * m!1" ))"2" replace "2" replace "2" "2" "both_sides_div_pos_lt2" "pz" "1" "py" "9 + 4 * m!1" "px" "11 + 4 * m!1" ))"2" "2" "(1 / (9 + 4 * m!1) - (1 / 5) ^ 2 / (11 + 4 * m!1)) * (9 + 4 * m!1) = 1- (1 / 5) ^ 2*(9 + 4 * m!1)/(11 + 4 * m!1)" )"1" "1" case "(1 / 5) ^ 2 * (9 + 4 * m!1) / (11 + 4 * m!1) < 1/25" )"1" assert )nil nil )"2" "2" "(1 / 5) ^ 2=1/25" )"1" rewrite "div_mult_pos_lt1" nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "cross_mult" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "div_mult_pos_lt1" "z" "(1 / 239) ^ 2" "py" "9 + 4 * m!1" "x" "1 / (7 + 4 * m!1)" ))"2" "2" "2" "1" assert )"1" "DRL1" "(1 / 239) ^ 2" )"1" assert )nil nil ))nil ))nil )"2" "2" "div_mult_pos_lt2" "py" "7 + 4 * m!1" "z" "9 + 4 * m!1" "x" "(1 / 239) ^ 2" ))"2" replace "2" "2" "lt_times_lt_pos1" "px" "(1 / 239) ^ 2" "y" "1" "nnz" "7 + 4 * m!1" "w" "9 + 4 * m!1" ))"2" "both_sides_expt_pos_lt" "px" "1/239" "py" "1" "pm" "2" ))"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "(2*TWOTHREENINE)*(1 / (3 + 4 * m!1)-(1 / 239) ^ 2*(1 / (5 + 4 * m!1))) - 8*(1 / 5) ^ 2 * FIVE * (1 / (7 + 4 * m!1))<0" )"1" "both_sides_times_pos_lt1" "pz" "LHS" "x" "(2 * TWOTHREENINE) * " "y" "0" ))"1" replace "1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" case "2 * TWOTHREENINE/(3 + 4 * m!1) < 8 * (1 / 5) ^ 2 * FIVE * (1 / (7 + 4 * m!1))" )"1" "RHS" "8 * (1 / 5) ^ 2 * FIVE * (1 / (7 + 4 * m!1))" )"1" "both_sides_times_pos_lt1" "y" "1/(3 + 4 * m!1)" "x" "(1 / (3 + 4 * m!1) - (1 / 239) ^ 2 * (1 / (5 + 4 * m!1)))" "pz" "2 * TWOTHREENINE" ))"1" assert )nil nil ))nil ))nil )"2" "2" rewrite "times_div1" )"2" "div_mult_pos_lt1" "py" "3 + 4 * m!1" "z" "2 * TWOTHREENINE" "x" "(8 * ((1 / 5) ^ 2 * FIVE))/(7 + 4 * m!1)" ))"2" replace "2" "2" "div_mult_pos_lt2" "py" "7 + 4 * m!1" "z" "(8 * ((1 / 5) ^ 2 * FIVE))*(3 + 4 * m!1)" "x" "2 * TWOTHREENINE" ))"2" replace "2" "2" expand "FIVE" )"2" expand "TWOTHREENINE" )"2" case "forall (m:nat): m>=5 => 14 * (1 / 239) ^ (3 + 4 * m) + ") "1" "m!1" )"1" assert )nil nil ))nil )"2" "2" "m" )"1" assert )nil nil )"2" "2" "j!1=4" )"1" nil nil )"2" assert )"2" "lt_times_lt_pos1" "px" "14 * (1 / 239) ^ (3 + 4 * j!1) + " "y" "24 * ((1 / 5) ^ 2 * (1 / 5) ^ (5 + 4 * j!1)) + " "nnz" "(1 / 239) ^ 4" "w" "(1/5)^4" ))"2" "1" case "8*(1 / 239) ^ (7 + 4 * j!1)<32*((1 / 5) ^ 2 * (1 / 5) ^ (9 + 4 * j!1))" )"1" "expt_plus" "n0x" "1/5" "i" "4" "j" "5+4*j!1" ))"1" replace "1" "expt_plus" "n0x" "1/239" "i" "4" "j" "3+4*j!1" ))"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "expt_plus" "n0x" "1/5" "i" "2" "j" "7+4*j!1" ))"2" replace "2" "2" case "forall (m:nat): m>=27 => 8 * (1 / 239) ^ m < ") "1" "7 + 4 * j!1" )"1" assert )nil nil ))nil )"2" "2" "m" )"1" nil nil )"2" "2" "j!2=26" )"1" nil nil )"2" assert )"2" "lt_times_lt_pos1" "px" "1/239" "y" "1/5" "nnz" "8 * (1 / 239) ^ j!2" "w" "32 * ((1 / 5) ^ 2 * ((1 / 5) ^ 2 * (1 / 5) ^ j!2))" ))"2" expand "^" )"2" expand "expt" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" "3" "both_sides_expt_pos_lt" "px" "1/239" "py" "1/5" "pm" "4" ))"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.809Angebot
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-29)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
