Impressum atanx.prf
Sprache: Lisp
(atanxnil 3288497283"" (expand "cauchy_ssmallreal?" )"" (inst + "0" )"" (expand "cauchy_prop" ) (("" (propax) nil nil )) nil )) nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil atanx nil )"bool" cauchy nil )"posint" exponentiation nil )"bool" atanx nil )"odd_int" integers nil ))nil 3288497283"" (skosimp*)"" (typepred "x!1" )"" (expand "cauchy_ssmallreal?" )"" (skosimp*)"" (expand "cauchy_real?" ) (("" (inst + "x!2" ) nil nil ))nil ))nil ))nil ))nil ))nil )nil atanx nil )"bool" atanx nil )nil naturalnumbers nil )"bool" reals 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 numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil atanx nil )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" cauchy nil )"odd_int" integers nil ))nil 3288497283"" (expand "cauchy_vsmallreal?" )"" (inst + "0" )"" (expand "cauchy_prop" ) (("" (propax) nil nil )) nil )) nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil atanx nil )"bool" cauchy nil )"posint" exponentiation nil )"bool" atanx nil ))nil 3288497283"" (skosimp*)"" (typepred "x!1" )"" (expand "cauchy_vsmallreal?" )"" (expand "cauchy_real?" )"" (skosimp*) (("" (inst + "x!2" ) nil nil )) nil )) nil ))nil ))nil ))nil )nil atanx nil )"bool" atanx nil )nil naturalnumbers nil )"bool" reals 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 numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" cauchy nil )nil atanx nil )"bool" reals nil ) (<= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil ))nil 3392689913"" (skosimp)"" (expand "cauchy_nzreal?" )"" (inst + "1+2*n!1" )"" (expand "cauchy_prop" )"" (skosimp)"" (expand "cauchy_int" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"bool" cauchy nil )"posint" exponentiation nil )"bool" cauchy nil )"int" integers nil )"cauchy_real" 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 )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posint" nil )"odd_int" integersnil ))nil ))nil 3392689913"" (skosimp)"" (hide 1)"" (expand "cauchy_nzreal?" )"" (inst + "1+2*n!1" )"" (expand "cauchy_prop" )"" (skosimp)"" (expand "cauchy_int" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"odd_int" integers 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 )"boolean" notequal nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"cauchy_real" int nil )"int" integers nil )"bool" cauchy nil )"posint" exponentiation nil )"bool" cauchy nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"int" integers nil ))nil ))nil 3288496910"" (expand "atan_series_coef" )"" (expand "cauchy_atan_drx_series" )"" (skosimp*)"" (lemma "int_lemma" ("n" "1+2*n!1" ))"" (lemma "int_lemma" ("n" "1" ))"" (lemma "int_lemma" ("n" "-1" ))"" (assert )"" (typepred "n!1" )"" (lemma "expt_minus1" ("i" "n!1" ))"" (case-replace "even?(n!1)" )"1" (assert )"1" (flatten)"1" (replace -2)"1" "div_lemma" "x" "1" "cx" "cauchy_int(1)" "nzy" "1+2*n!1" "nzcy" "cauchy_int(1 + 2 * n!1)" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (assert )"2" (rewrite "even_or_odd" )"2" (assert )"2" (replace -2)"2" "div_lemma" "x" "-1" "cx" "cauchy_int(-1)" "nzy" "1+2*n!1" "nzcy" "cauchy_int(1 + 2 * n!1)" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"cauchy_real" atanx nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 int nil )"odd_int" integers nil )"[numfield -> numfield]" number_fields nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" integers nil )nil div nil )"bool" cauchy nil )nil cauchy nil )"cauchy_real" int nil )"bool" cauchy nil )nil cauchy nil )"boolean" notequal nil )nil reals nil )"posrat" nil )"(total_order?[real])" nil )nil naturalnumbers nil )nil prelude_aux nil )"nzrat" rationalsnil )"rat" atan "trig_fnd/" )"odd_int" integers nil )"posint" nil )"nzreal" exponentiation nil )"int" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"int" integers nil ))nil 3288497284"" (expand "cauchys_real?" )"" (inst + "atan_series_coef" )"" (expand "cauchys_prop" )"" (skosimp*)"" (lemma "atan_series_lemma" ("n" "n!1" ))"" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil rationals nil )"rat" atan "trig_fnd/" )nil atanx nil )"bool" sum nil )"bool" sum nil ))nil 3288506197"" (skosimp*) (("" (typepred "vsx!1" ) (("" (assert ) nil nil )) nil ))nil )nil atanx nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil 3288506197"" (skosimp*)"" (typepred "vsx!1" )"" (lemma "sqrt_eq_0" )"" (inst - "vsx!1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil atanx nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )nil real_types nil )"bool" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil sqrt "reals/" ))nil 3288524114"" (skosimp*)"" (typepred "vsx!1" )"" (expand "cauchy_atan_drxx" )"" "powerseries_lemma" "x" "vsx!1" "cx" "cvsx!1" "xs" "atan_series_coef" "cxs" "cauchy_atan_drx_series" ))"" (replace -4)"" (lemma "atan_series_lemma" )"" (replace -1)"" (hide -1)"" (expand "cauchy_prop" )"" (skosimp*)"" (inst -1 "2+p!1" )"" (inst -1 "2+p!1" )"" (flatten -1)"" "CPS" "cauchy_powerseries(cvsx!1, cauchy_atan_drx_series, 2 + p!1)(2 + p!1)" )"" "2^(2+p!1)=4*2^p!1" )"1" "lemma_A2" "r" "round(CPS/4)" "p" "CPS" "q" "4" ))"1" assert )"1" "1" "atan_series" "x" "sqrt(vsx!1)" "n" "2+p!1" ))"1" expand "atan_series_n" )"1" expand "atan_series_term" )"1" case "FORALL (n:nat): sqrt(vsx!1) ^ (1 + 2 * n) = sqrt(vsx!1)* vsx!1^n" )"1" "sigma(0, 2 + p!1, LAMBDA (n: nat):LAMBDA (n: nat): vsx!1^n * atan_series_coef(n))") "1" "1" "3+p!1" )"1" replace -1 -2)"1" expand "powerseries" )"1" "(LAMBDA (i:nat): IF i = 0 THEN atan_series_coef(i)LAMBDA (n: nat): vsx!1 ^ n * atan_series_coef(n))") "1" "1" "PS" "sigma(0, 2 + p!1, LAMBDA (n: nat): vsx!1 ^ n * atan_series_coef(n))") "1" "RR" "round(CPS / 4)" )"1" expand "<=" "1" "1" assert )"1" "sqrt_pos" "px" "vsx!1" ))"1" "expt_pos" "px" "vsx!1" "i" "3+p!1" ))"1" "sqrt_lt" "nny" "vsx!1" "nnz" "sq(1/2)" ))"1" rewrite "sqrt_sq" )"1" expand "sq" "1" rewrite "abs_mult" "1" expand "abs" "1" expand "abs" "1" assert )"1" "both_sides_div_pos_le1" "x" "abs(atan(sqrt(vsx!1)) - sqrt(vsx!1) * PS)" "y" "(sqrt(vsx!1) * vsx!1 ^ (3 + p!1)) / (7 + 2 * p!1)" "pz" "sqrt(vsx!1)" ))"1" replace "1" "1" "(sqrt(vsx!1) * vsx!1 ^ (3 + p!1)) / (7 + 2 * p!1) / sqrt(vsx!1) = vsx!1 ^ (3 + p!1) / (7 + 2 * p!1)" )"1" "1" "abs(atan(sqrt(vsx!1)) - sqrt(vsx!1) * PS) / sqrt(vsx!1) = abs(atan(sqrt(vsx!1)) / sqrt(vsx!1) -PS)" )"1" "1" "TMP1" "atan(sqrt(vsx!1)) / sqrt(vsx!1)" )"1" "both_sides_expt_pos_lt" "px" "vsx!1" "py" "1/4" "pm" "3+p!1" ))"1" assert )"1" "1" case "abs(TMP1 - PS)*2^p!1 < 1/4" )"1" expand "abs" "1" case "TMP1<PS" )"1" assert )"1" "posreal_times_posreal_is_posreal" "px" "-(TMP1 - PS)" "py" "2 ^ p!1" ))"1" assert )nil nil ))nil ))nil )"2" assert )"2" "posreal_times_posreal_is_posreal" "px" "TMP1-PS" "py" "2 ^ p!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "both_sides_div_pos_lt2" "pz" "vsx!1 ^ (3 + p!1)" "px" "7 + 2 * p!1" "py" "1" ))"2" "2" assert )"2" "both_sides_expt_pos_lt" "px" "1/4" "py" "1/2" "pm" "3+p!1" ))"2" assert )"2" "both_sides_expt_lt1_lt" "lt1x" "1/2" "i" "3+p!1" "j" "2+p!1" ))"2" assert )"2" "inv_expt" "n0x" "2" "i" "2+p!1" ))"2" "expt_pos" "px" "2" "i" "p!1" ))"2" "div_mult_pos_lt2" "py" "2^p!1" "x" "abs(TMP1 - PS)" "z" "1/4" ))"2" replace "2" "1 / 4 / 2 ^ p!1 = 1 / 2 ^ (2 + p!1)" )"1" assert )nil nil )"2" "2" "2 ^ (2 + p!1) = 4*2^p!1" )"1" "TMP4" "2^p!1" )"1" assert )nil nil ))nil )"2" "2" "expt_plus" "n0x" "2" "i" "2" "j" "p!1" ))"2" replace "2" expand "^" "2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "abs_div" )"2" "sqrt(vsx!1)" "atan(sqrt(vsx!1)) - sqrt(vsx!1) * PS" )"2" expand "abs" "2" assert )nil 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 )"2" replace "2" rewrite "sqrt_0" )"2" expand "PS" )"2" "sigma(0, 2 + p!1, LAMBDA (n: nat): vsx!1 ^ n * atan_series_coef(n)) =1") "1" assert )nil nil )"2" "2" case "FORALL (m:nat): sigma(0,m,LAMBDA (n: nat): 0 ^ n * atan_series_coef(n)) =1" )"1" "2+p!1" )"1" replace "1" nil nil ))nil ))nil )"2" "2" "m" )"1" expand "sigma" )"1" expand "atan_series_coef" )"1" expand "^" )"1" expand "expt" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "sigma" "2" replace "2" "2" expand "^" )"2" expand "expt" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "extensionality" "2" "2" "2" case "x!1=0" )"1" replace "1" expand "^" "1" expand "expt" "1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "FORALL (m:nat): sigma(0, m, LAMBDA (n: nat):LAMBDA (n: nat): vsx!1 ^ n * atan_series_coef(n))") "1" "2+p!1" )nil nil )"2" "2" "m" )"1" expand "sigma" )"1" expand "^" "1" expand "expt" )"1" expand "expt" )"1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "sigma" "2" replace "2" "1+j!1" )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n" )"1" expand "^" 1)"1" expand "expt" 1)"1" expand "expt" "1" nil nil ))nil ))nil ))nil )"2" "2" expand "<=" -2)"2" "1" "expt_plus" )"1" "1+2*j!1" "2" "sqrt(vsx!1)" )"1" "j!1" "1" "vsx!1" )"1" replace "1" replace "1" replace "1" rewrite "expt_x1" )"1" "sqrt(vsx!1) ^ 2 = vsx!1" )"1" assert )"1" assert )nil nil ))nil )"2" "2" expand "^" )"2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" rewrite "sq_rew" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "sqrt_pos" )"2" "vsx!1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace "2" rewrite "sqrt_0" )"2" expand "^" "2" expand "expt" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "expt_plus" "n0x" "2" "i" "2" "j" "p!1" ))"2" expand "^" -1 2)"2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil atanx nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"rat" atan "trig_fnd/" )nil rationals nil )"cauchy_real" atanx nil )nil atanx nil )"bool" atanx nil )nil cauchy nil )"bool" cauchy nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil powerseries nil )nil atanx nil )"cauchy_real" powerseries nil )nil sum nil )"bool" sum nil )"[T, T -> boolean]" equalities nil )"rat" rationals nil )nil appendix nil )nil integers nil )"bool" reals nil )nil integers nil )"int" prelude_aux nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" atan "trig_fnd/" )"odd_int" integers nil )"real" reals nil )"nnreal" exponentiation nil )"[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"nat" exponentiation nil )"real" atanx nil )"int" exponentiation nil )"nzreal" exponentiation nil )"nat" exponentiation nil )nil sigma_nat "reals/" )"nzrat" rationalsnil )"nzreal" exponentiation nil )"int" exponentiation nil )nil naturalnumbers nil )nil defined_types nil )"nonneg_rat" nil )"{j: nonneg_int | j >= i}" nil )nil sqrt "reals/" )"real" reals nil )"even_int" integersnil )"even_int" integersnil )"nzreal" real_typesnil )"nnreal" nil )nil exponentiation nil )nil sqrt "reals/" )nil real_props nil )"nnreal" nil )nil real_props nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" atan "trig_fnd/" )nil atan "trig_fnd/" )"real_abs_lt_pi2" atan "trig_fnd/" )nil reals nil )nil real_props nil )nil exponentiation nil )nil real_props nil )"posnat" exponentiation nil )"real" exponentiation nil )nil exponentiation nil )nil integers nil )nil real_props nil )nil reals nil )nil exponentiation nil )nil exponentiation nil )"real" reals nil )nil real_types nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"odd_int" integers nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"nonneg_real" sq "reals/" )nil sqrt "reals/" )"(strict_total_order?[real])" real_props nil )nil real_types nil )nil sqrt "reals/" )nil functions nil )"real" powerseries nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )"odd_int" integersnil )"even_int" integersnil )nil exponentiation nil )nil sq "reals/" )nil sqrt "reals/" )"posint" nil )"vsmallreal" atanx nil )"[nat -> real]" atan "trig_fnd/" )"(total_order?[real])" nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )nil real_types nil )nil real_types nil )nil atan "trig_fnd/" )"nnreal" exponentiation nil )"nonneg_int" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"int" integers nil )"(total_order?[real])" nil )"rat" rationals nil )"rat" rationals nil )"posrat" nil )"rat" rationals nil )"int" integers nil )"int" integers nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"bool" cauchy nil )"posint" exponentiation nil )"[nat -> int]" atanx nil ))nil 3288505102"" (skosimp*)"" (typepred "cssx!1" )"" (expand "cauchy_ssmallreal?" )"" (skosimp*)"" "mul_lemma" "x" "x!1" "y" "x!1" "cx" "cssx!1" "cy" "cssx!1" ))"" (rewrite "sq_rew" )"" (assert )"" (expand "cauchy_vsmallreal?" )"" (typepred "x!1" )"" (case "0 <= sq(x!1) & sq(x!1) < 1/4" )"1" (flatten -1)"1" (inst + "sq(x!1)" )"1" (assert ) nil nil )) nil ))nil )"2" (hide -3 -4 2)"2" (lemma "sq_pos" ("a" "x!1" ))"2" (assert )"2" (case "0 <= x!1" )"1" "sq_lt" "nna" "x!1" "nnb" "1/2" ))"1" expand "sq" -1 2)"1" (propax) nil nil ))nil )"2" (assert ) nil nil ))nil )"2" "sq_neg" ("a" "x!1" ))"2" "sq_lt" "nna" "-x!1" "nnb" "1/2" ))"1" expand "sq" -1 2)"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil atanx nil )"bool" atanx nil )nil naturalnumbers nil )"bool" reals 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 numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil sq "reals/" )"bool" atanx nil )"posrat" nil )"bool" reals nil )nil real_types nil )"nonneg_real" sq "reals/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil atanx nil )"ssmallreal" atanx nil )nil sq "reals/" )nil sq "reals/" )"real" reals nil )nil sq "reals/" )"(total_order?[real])" nil )"nzrat" rationalsnil )nil mul nil )"bool" cauchy nil )nil cauchy nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil atanx nil )"odd_int" integers nil ))nil 3288506197"" (skosimp*)"" (expand "cauchy_real?" )"" (typepred "cssx!1" )"" (expand "cauchy_ssmallreal?" )"" (skosimp*)"" "mul_lemma" "x" "x!1" "y" "x!1" "cx" "cssx!1" "cy" "cssx!1" ))"" (typepred "x!1" )"" (assert )"" (rewrite "sq_rew" )"" "cauchy_atan_drxx_prop" "vsx" "sq(x!1)" "cvsx" "cauchy_mul(cssx!1, cssx!1)" ))"1" (assert )"1" "IF sq(x!1) = 0 THEN 1 ") "1" (skosimp*)"1" (rewrite "sqrt_sq" -1)"1" replace -1)"1" (rewrite "sq_0" 1) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 -1 -2))"2" (case "0<=x!1" )"1" "sq_lt" ("nna" "x!1" "nnb" "1/2" ))"1" (expand "sq" -1 2)"1" (propax) nil nil )) nil )"2" (assert ) nil nil ))nil )"2" (lemma "sq_neg" ("a" "x!1" ))"2" "sq_lt" "nna" "-x!1" "nnb" "1/2" ))"1" expand "sq" -1 2)"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (expand "cauchy_vsmallreal?" )"3" (case "0<=sq(x!1) & sq(x!1) < 1/4" )"1" (flatten -1)"1" "sq(x!1)" )"1" (assert ) nil nil ))nil ))nil )"2" (hide -3 -4 2)"2" "sq_pos" ("a" "x!1" ))"2" assert )"2" case "0<=x!1" )"1" "sq_lt" "nna" "x!1" "nnb" "1/2" ))"1" expand "sq" -1 2)"1" (propax) nil nil ))nil )"2" (assert ) nil nil ))nil )"2" "sq_neg" ("a" "x!1" ))"2" "sq_lt" "nna" "-x!1" "nnb" "1/2" ))"1" expand "sq" -1 2)"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" cauchy nil )"odd_int" integers nil )nil atanx nil )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil cauchy nil )nil mul nil )"nzrat" rationalsnil )"(strict_total_order?[real])" real_props nil )"nonneg_real" sq "reals/" )nil real_types nil )nil atanx nil )"bool" reals nil )"cauchy_real" mul nil )nil atanx nil )"bool" atanx nil )nil atanx nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" reals nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"real_abs_lt_pi2" atan "trig_fnd/" )nil atan "trig_fnd/" )"posreal" atan "trig_fnd/" )nil real_types nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[bool, bool -> bool]" booleans nil )"ssmallreal" atanx nil )nil sqrt "reals/" )nil sqrt "reals/" )"real" reals nil )nil sq "reals/" )nil sq "reals/" )"posrat" nil )nil sq "reals/" )nil sq "reals/" )nil sq "reals/" )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" atanx nil )nil atanx nil ))nil 3288506281"" (skosimp*)"" (expand "cauchy_atan_dr" )"" "cauchy_atan_drxx_prop" "vsx" "sq(ssx!1)" "cvsx" "cauchy_mul(cssx!1, cssx!1)" ))"1" "mul_lemma" "x" "ssx!1" "cx" "cssx!1" "y" "ssx!1" "cy" "cssx!1" ))"1" (case-replace "sqrt(sq(ssx!1)) = abs(ssx!1)" )"1" (replace -4)"1" (rewrite "sq_eq_0" )"1" (expand "sq" -3)"1" (replace -2)"1" "mul_lemma" "x" "ssx!1" "cx" "cssx!1" "y" "IF ssx!1 = 0 THEN 1 ELSE atan(abs(ssx!1)) / abs(ssx!1) ENDIF" "cy" "cauchy_atan_drxx(cauchy_mul(cssx!1, cssx!1))" ))"1" (assert )"1" (replace -4 -1)"1" "ssx!1 * IF ssx!1 = 0 THEN 1") "1" (hide-all-but 1)"1" expand "abs" )"1" "trichotomy" ("x" "ssx!1" ))"1" "1" (assert ) nil nil )"2" assert )"2" replace -1)"2" rewrite "atan_0" )nil nil ))nil ))nil )"3" assert )"3" rewrite "atan_neg" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil )"3" (hide 2)"3" (expand "cauchy_real?" )"3" "IF ssx!1 = 0 THEN 1 ") "3" (hide-all-but 1)"3" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (typepred "ssx!1" )"2" (case "0<= ssx!1" )"1" (expand "abs" )"1" (rewrite "sqrt_sq" ) (("1" (assert ) nil nil ))nil ))nil )"2" (expand "abs" )"2" (lemma "sq_neg" )"2" (inst - "ssx!1" )"2" (replace -1 2 rl)"2" (rewrite "sqrt_sq" 2)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (lemma "sq_pos" )"2" (inst - "ssx!1" )"2" (typepred "ssx!1" )"2" (assert )"2" (case "0<=ssx!1" )"1" (lemma "sq_lt" )"1" (inst - "ssx!1" "1/2" )"1" (expand "sq" -1 2)"1" (propax) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil )"2" (lemma "sq_neg" ("a" "ssx!1" ))"2" (lemma "sq_lt" )"2" (inst - "-ssx!1" "1/2" )"1" (expand "sq" -1 2)"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (expand "cauchy_vsmallreal?" )"3" (inst + "sq(ssx!1)" )"1" "mul_lemma" "x" "ssx!1" "cx" "cssx!1" "y" "ssx!1" "cy" "cssx!1" ))"1" (expand "sq" 1) (("1" (assert ) nil nil )) nil ))nil )"2" (hide -1)"2" (lemma "sq_pos" ("a" "ssx!1" ))"2" (assert )"2" (typepred "ssx!1" )"2" (case "0<= ssx!1" )"1" "sq_lt" ("nna" "ssx!1" "nnb" "1/2" ))"1" (expand "sq" -1 2)"1" (propax) nil nil )) nil )"2" (assert ) nil nil ))nil )"2" (lemma "sq_neg" ("a" "ssx!1" ))"2" "sq_lt" "nna" "-ssx!1" "nnb" "1/2" ))"1" (expand "sq" -1 2)"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"cauchy_real" atanx nil )nil sq "reals/" )"ssmallreal" atanx nil )"posrat" nil )nil sq "reals/" )nil mul nil )nil sqrt "reals/" )"nzrat" rationalsnil )nil sq "reals/" )"real" reals nil )"[nat -> int]" atanx nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil )nil real_types nil )"posreal" atan "trig_fnd/" )nil atan "trig_fnd/" )"real_abs_lt_pi2" atan "trig_fnd/" )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil real_axioms nil )"real" reals nil )nil atan "trig_fnd/" )nil atan "trig_fnd/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"nzreal" real_typesnil )nil sq "reals/" )"[T, T -> boolean]" equalities nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil atanx 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 )"bool" atanx nil )nil atanx nil )"bool" cauchy nil )nil cauchy nil )"cauchy_real" mul nil )"bool" atanx nil )nil atanx nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil atanx nil )nil real_types nil )"nonneg_real" sq "reals/" )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil atanx nil )"odd_int" integers nil ))nil 3288505102"" (expand "cauchy_nzreal?" )"" (inst + "5" )"" (expand "cauchy_int" )"" (expand "cauchy_prop" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil )nil reals nil )"posint" exponentiation nil )"int" integers nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"bool" cauchy nil )"cauchy_real" int nil )"bool" cauchy nil ))nil 3288505102"" (expand "cauchy_ssmallreal?" )"" (inst + "1/5" )"" "div_lemma" "x" "1" "nzy" "5" "cx" "cauchy_int(1)" "nzcy" "cauchy_int(5)" ))"" (rewrite "int_lemma" ) (("" (rewrite "int_lemma" ) nil nil ))nil ))nil ))nil ))nil )"posrat" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil atanx nil )nil int nil )nil div nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" cauchy nil )nil cauchy nil )"cauchy_real" int nil )"bool" cauchy nil )nil cauchy nil )nil reals nil )"bool" atanx nil )"odd_int" integers nil ))nil 3392689913 ("" (subtype-tcc) 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 )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" cauchy nil )"bool" cauchy nil )"cauchy_real" int nil )"real" exponentiation nil )"posnat" exponentiation nil )"int" integers nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil ))nil ))nil 3392689913"" (expand "cauchy_ssmallreal?" )"" (inst + "1/239" )"" "div_lemma" "x" "1" "nzy" "239" "cx" "cauchy_int(1)" "nzcy" "cauchy_int(239)" ))"" (rewrite "int_lemma" ) (("" (rewrite "int_lemma" ) nil nil ))nil ))nil ))nil ))nil )"posrat" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil atanx nil )nil int nil )nil div nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" cauchy nil )nil cauchy nil )"cauchy_real" int nil )"bool" cauchy nil )nil cauchy nil )nil reals nil )"bool" atanx nil )"odd_int" integers nil ))nil ))nil 3288503798"" (expand "cauchy_pi" )"" (lemma "atan_1" )"" "div_lemma" "x" "1" "cx" "cauchy_int(1)" "nzy" "5" "nzcy" "cauchy_int(5)" ))"" "div_lemma" "x" "1" "cx" "cauchy_int(1)" "nzy" "239" "nzcy" "cauchy_int(239)" ))"" (rewrite "int_lemma" )"" (rewrite "int_lemma" )"" (rewrite "int_lemma" )"" "R5" "cauchy_div(cauchy_int(1), cauchy_int(5))" )"" "R239" "cauchy_div(cauchy_int(1), cauchy_int(239))" )"" "atan_dr_lemma" ("ssx" "1/5" "cssx" "R5" ))"" "atan_dr_lemma" "ssx" "1/239" "cssx" "R239" ))"" (assert )"" (hide -1 -6)"" "lemma_mul2n" "x" "atan(1/5)" "cx" "cauchy_atan_dr(R5)" "n" "4" ))"" "lemma_mul2n" "x" "atan(1/239)" "cx" "cauchy_atan_dr(R239)" "n" "2" ))"" assert )"" expand "mul2n" )"" rewrite "expt_x2" )"" rewrite "expt_x4" )"" "sub_lemma" "x" "16*atan(1/5)" "cx" "cauchy_mul2n(cauchy_atan_dr(R5),4)" "y" "4*atan(1/239)" "cy" "cauchy_mul2n(cauchy_atan_dr(R239),2)" ))"" assert )"" expand "pi" 1)"" assert )"" expand "atan" "" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil atan "trig_fnd/" )"cauchy_real" div nil )"[T, T -> boolean]" equalities nil )"posrat" nil )nil atanx nil )"bool" atanx nil )nil atanx nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil atanx nil )"nzreal" real_typesnil )"real" reals nil )"real" reals nil )nil shift nil )"cauchy_real" atanx nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan "trig_fnd/" )nil atan "trig_fnd/" )"real_abs_lt_pi2" atan "trig_fnd/" )nil inv nil )"posint" exponentiation nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )"int" integers nil )nil sub nil )"cauchy_real" shift nil )"[numfield, numfield -> numfield]" number_fields nil )"(divides(m))" divides nil )nil exponentiation nil )"real" shift nil )nil int nil )nil div 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 )"bool" cauchy nil )nil cauchy nil )"cauchy_real" int nil )"bool" cauchy nil )nil cauchy nil )"boolean" notequal nil )nil reals nil )"cauchy_real" atanx nil ))nil 3288505106"" (skosimp*)"" (replace -1)"" (hide-all-but (-5 1))"" (typepred "cx!1" )"" (expand "cauchy_nzreal?" )"" (expand "cauchy_real?" )"" (skosimp)"" (expand "cauchy_prop" )"" (inst-cp - "3" )"" (rewrite "expt_x3" )"" (flatten)"" (case "x!1<-19/8" )"1" (inst + "x!1" ) (("1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil cauchy nil )"bool" cauchy nil )nil naturalnumbers nil )"bool" reals 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 numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"posint" exponentiation nil )"bool" cauchy nil )nil exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )"int" integers nil )"nzrat" rationalsnil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )"real" atanx nil )nil reals nil )"int" integers nil )"real" reals nil )"int" integers nil )"(total_order?[real])" nil )"nzint" integers nil )"even_int" integers nil )"bool" cauchy nil ))nil 3288505106"" (skosimp*)"" (replace -1)"" (hide-all-but (-5 1))"" (typepred "cx!1" )"" (expand "cauchy_real?" )"" (expand "cauchy_ssmallreal?" )"" (skosimp)"" (expand "cauchy_prop" )"" (inst-cp - "3" )"" (rewrite "expt_x3" )"" (flatten)"" (case "x!1<-19/8" )"1" (inst + "-(1/x!1)" )"1" (skosimp)"1" "inv_lemma" "nzx" "x!1" "nzcx" "cx!1" ))"1" "1" "neg_lemma" "x" "1/x!1" "cx" "cauchy_inv(cx!1)" ))"1" assert )"1" expand "cauchy_prop" )"1" (inst - "p!1" ) nil nil ))nil ))nil ))nil )"2" expand "cauchy_prop" )"2" (propax) nil nil ))nil ))nil )"2" (assert ) nil nil )"3" "3" expand "cauchy_nzreal?" )"3" "x!1" )"1" expand "cauchy_prop" )"1" (propax) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" rewrite "div_mult_pos_lt1" 1)"2" rewrite "div_mult_pos_lt2" 1)"2" "both_sides_div_neg_lt3" "nz" "-1" "nx" "x!1" "ny" "-19 / 8" ))"2" assert )"2" "negreal_div_negreal_is_posreal" "nx" "-1" "ny" "x!1" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil cauchy nil )"bool" cauchy nil )nil naturalnumbers nil )"bool" reals 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 numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"odd_int" integers nil )"bool" atanx nil )"posint" exponentiation nil )"bool" cauchy nil )nil exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )"int" integers nil )"nzrat" rationalsnil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil real_props nil )nil real_props nil )nil real_types nil )"bool" reals nil )nil real_types nil )"nzreal" nil )"cauchy_nzreal" neg nil )"even_int" integers nil )"nzint" integers nil )"(total_order?[real])" nil )"int" integers nil )"real" reals nil )"int" integers nil )"cauchy_nzreal" inv nil )nil neg nil )nil reals nil )nil cauchy nil )"bool" cauchy nil )nil inv nil )nil atanx nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" atanx nil )"nzreal" real_typesnil )"(strict_total_order?[real])" real_props nil )"nzreal" nil ))nil 3288505107"" (skosimp*)"" (case "-19 <= t!1" )"1" (replace -2)"1" (hide-all-but (-1 -3 -6 2))"1" (typepred "cx!1" )"1" (expand "cauchy_real?" )"1" (skosimp)"1" (copy -1)"1" (expand "cauchy_prop" -1)"1" (inst - "3" )"1" (flatten)"1" (rewrite "expt_x3" )"1" (case "-20/8<x!1&x!1<-3/8" )"1" (flatten)"1" "sub_lemma" "x" "x!1" "cx" "cx!1" "y" "1" "cy" "cauchy_int(1)" ))"1" rewrite "int_lemma" )"1" assert )"1" expand "cauchy_nzreal?" )"1" "x!1-1" )"1" replace -8 * rl)"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"odd_int" integers nil )nil exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )"int" integers nil )nil int nil )"bool" cauchy nil )nil reals nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"nzint" integers nil )"even_int" integers nil )"int" integers nil )"real" reals nil )"int" integers nil )"(total_order?[real])" nil )"cauchy_real" int nil )nil sub nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nzrat" rationalsnil )"bool" cauchy nil )"posint" exponentiation nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" cauchy nil )nil cauchy nil ))nil 3288505107"" (skosimp*)"" (case "-19<=t!1" )"1" (replace -2)"1" (hide (-2 1 -5 -7))"1" (typepred "cx!1" )"1" (expand "cauchy_real?" )"1" (skosimp)"1" (copy -1)"1" (expand "cauchy_prop" -1)"1" (inst - "3" )"1" (rewrite "expt_x3" )"1" (flatten)"1" (case "-20/8<x!1&x!1<-3/8" )"1" (flatten)"1" "1" "sub_lemma" "x" "x!1" "cx" "cx!1" "y" "1" "cy" "cauchy_int(1)" ))"1" "add_lemma" "x" "x!1" "cx" "cx!1" "y" "1" "cy" "cauchy_int(1)" ))"1" assert )"1" rewrite "int_lemma" )"1" "div_lemma" "x" "1+x!1" "cx" "cauchy_add(cx!1, cauchy_int(1))" "nzy" "x!1-1" "nzcy" "cauchy_sub(cx!1, cauchy_int(1))" ))"1" assert )"1" expand "cauchy_ssmallreal?" )"1" "(1 + x!1) / (x!1 - 1)" )"1" (assert ) nil nil )"2" "2" "div_mult_neg_lt1" "ny" "x!1-1" "z" "1+x!1" "x" "1/2" ))"2" "div_mult_neg_lt2" "ny" "x!1-1" "z" "1+x!1" "x" "-1/2" ))"2" replace -1)"2" replace -2)"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "cauchy_nzreal?" )"2" "x!1-1" )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 )"2" (assert ) nil nil ))nil ))nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"odd_int" integers nil )"int" integers nil )"int" integers nil )nil sub nil )"cauchy_real" int nil )"even_int" integers nil )"nzint" integers nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil )nil div nil )"cauchy_real" add nil )"bool" cauchy nil )nil cauchy nil )"cauchy_real" sub nil )nil reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" atanx nil )nil real_props nil )"even_int" integersnil )"odd_int" integersnil )"real" reals nil )"(total_order?[real])" nil )nil real_types nil )nil real_types nil )nil real_props nil )"posrat" nil )nil atanx nil )"real" atanx nil )"real" reals nil )nil reals nil )nil int nil )nil add nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nzrat" rationalsnil )"int" integers nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil exponentiation nil )"bool" cauchy nil )"posint" exponentiation nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" cauchy nil )nil cauchy nil ))nil 3288505107"" (skosimp*)"" (case "-3<=t!1" )"1" (replace -2)"1" (hide-all-but (-1 -6 3))"1" (typepred "cx!1" )"1" (expand "cauchy_real?" )"1" (skosimp)"1" (copy -1)"1" (expand "cauchy_prop" -1)"1" (inst - "3" )"1" (rewrite "expt_x3" )"1" (flatten)"1" (case "-1/2<x!1&x!1<1/2" )"1" (flatten)"1" expand "cauchy_ssmallreal?" )"1" "x!1" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )nil atanx nil )"real" atanx nil )"int" integers nil )"real" reals nil )"int" integers nil )"(total_order?[real])" nil )"bool" atanx nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posrat" nil )"nzrat" rationalsnil )"int" integers nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil exponentiation nil )"bool" cauchy nil )"posint" exponentiation nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" cauchy nil )nil cauchy nil )"nzint" integers nil )"even_int" integers nil ))nil 3392689913"" (skosimp*)"" (case "4<=t!1" )"1" (replace -2)"1" (typepred "cx!1" )"1" (expand "cauchy_real?" )"1" (skosimp)"1" (copy -1)"1" (expand "cauchy_prop" -1)"1" (inst - "3" )"1" (rewrite "expt_x3" )"1" (flatten)"1" (case "3/8<x!1&x!1<20/8" )"1" (flatten)"1" "1" "add_lemma" "x" "x!1" "cx" "cx!1" "y" "1" "cy" "cauchy_int(1)" ))"1" rewrite "int_lemma" )"1" assert )"1" expand "cauchy_nzreal?" )"1" "1+x!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))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 cauchy nil )"bool" cauchy nil )nil naturalnumbers nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"posint" exponentiation nil )"bool" cauchy nil )nil exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )"int" integers nil )"posrat" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil int nil )"bool" cauchy nil )nil reals nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"cauchy_real" int nil )nil add nil )"int" integers nil )"real" reals nil )"int" integers nil )"(total_order?[real])" nil )"nzint" integers nil )"even_int" integers nil ))nil ))nil 3392689913"" (skosimp*)"" (case "4<=t!1" )"1" (replace -2)"1" (typepred "cx!1" )"1" (expand "cauchy_real?" )"1" (skosimp)"1" (copy -1)"1" (expand "cauchy_prop" -1)"1" (inst - "3" )"1" (rewrite "expt_x3" )"1" (flatten)"1" (case "3/8<x!1&x!1<20/8" )"1" (flatten)"1" (hide -3 -4 -6 -7 -10 -11 -12 1 2 3)"1" "add_lemma" "x" "x!1" "cx" "cx!1" "y" "1" "cy" "cauchy_int(1)" ))"1" "sub_lemma" "x" "x!1" "cx" "cx!1" "y" "1" "cy" "cauchy_int(1)" ))"1" rewrite "int_lemma" )"1" assert )"1" "div_lemma" "x" "x!1-1" "cx" "cxm1!1" "nzy" "1+x!1" "nzcy" "cxp1!1" ))"1" assert )"1" expand "cauchy_ssmallreal?" )"1" "(x!1 - 1) / (1 + x!1)" )"1" "1" rewrite "div_mult_pos_lt1" )"1" rewrite "div_mult_pos_lt1" )"1" "div_mult_pos_lt2" "py" "1+x!1" "z" "2*(x!1-1)" "x" "-1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))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 cauchy nil )"bool" cauchy nil )nil naturalnumbers nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"posint" exponentiation nil )"bool" cauchy nil )nil exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )"int" integers nil )"posrat" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil sub nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil atanx nil )"[numfield -> numfield]" number_fields nil )"real" atanx nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_props nil )"real" reals nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" atanx nil )"odd_int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )nil cauchy nil )"bool" cauchy nil )nil div nil )"real" reals nil )"real" reals nil )nil int nil )"cauchy_real" int nil )nil add nil )"int" integers nil )"int" integers nil )"(total_order?[real])" nil )"nzint" integers nil )"even_int" integers nil ))nil ))nil 3392689913"" (skosimp*)"" (case "20<=cx!1(3)" )"1" (typepred "cx!1" )"1" (expand "cauchy_real?" )"1" (skosimp)"1" (copy -1)"1" (expand "cauchy_prop" -1)"1" (inst - "3" )"1" (rewrite "expt_x3" )"1" (flatten)"1" (case "19/8<x!1" )"1" (hide -2 -3 -5 -6 -7 -8 -9 -10 1 2 3 4)"1" (expand "cauchy_nzreal?" )"1" (inst + "x!1" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )nil cauchy nil )"bool" cauchy 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 )"(total_order?[real])" nil )"int" integers nil )"real" reals nil )"int" integers nil )nil reals nil )"real" atanx nil )"(strict_total_order?[real])" real_props nil )"bool" cauchy nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )"posrat" nil )"int" integers nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil exponentiation nil )"bool" cauchy nil )"posint" exponentiation nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3392689913"" (skosimp*)"" (case "20<=cx!1(3)" )"1" (hide-all-but (-1 5))"1" (typepred "cx!1" )"1" (expand "cauchy_real?" )"1" (skosimp)"1" (copy -1)"1" (expand "cauchy_prop" -1)"1" (inst - "3" )"1" (rewrite "expt_x3" )"1" (flatten)"1" (case "19/8<x!1" )"1" (hide -2 -3 -5)"1" "inv_lemma" "nzx" "x!1" "nzcx" "cx!1" ))"1" assert )"1" expand "cauchy_ssmallreal?" )"1" "1/x!1" )"1" rewrite "div_mult_pos_lt2" 1)"1" rewrite "div_mult_pos_lt1" 1)nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )nil cauchy nil )"bool" cauchy 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 )NOT const-decl "[bool -> bool]" booleans nil )"posint" exponentiation nil )"bool" cauchy nil )nil exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )"int" integers nil )"posrat" nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil inv nil )"bool" cauchy nil )nil cauchy nil )nil reals nil )"odd_int" integers nil )"bool" atanx nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_props nil )"real" reals nil )nil real_props nil )"real" atanx nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )nil atanx nil )"nzreal" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3287978357"" (skosimp)"" (expand "cauchy_atan" )"" (case-replace "cx!1(3)<=-20" )"1" (copy -2)"1" (expand "cauchy_prop" -1)"1" (inst - "3" )"1" (rewrite "expt_x3" )"1" (flatten)"1" (case "x!1<-19/8" )"1" (hide -2 -3 -4)"1" "inv_lemma" ("nzx" "x!1" "nzcx" "cx!1" ))"1" (assert )"1" "neg_lemma" "x" "1/x!1" "cx" "cauchy_inv(cx!1)" ))"1" (assert )"1" "atan_dr_lemma" "ssx" "-(1 / x!1)" "cssx" "cauchy_neg(cauchy_inv(cx!1))" ))"1" assert )"1" "lemma_div2n" "x" "pi" "cx" "cauchy_pi" "n" "1" ))"1" rewrite "pi_lemma" )"1" expand "div2n" )"1" rewrite "expt_x1" )"1" "sub_lemma" "x" "atan(-(1 / x!1))" "cx" "cauchy_atan_dr(cauchy_neg(cauchy_inv(cx!1)))" "y" "pi/2" "cy" "cauchy_div2n(cauchy_pi, 1)" ))"1" assert )"1" "atan_inv" "px" "-x!1" ))"1" replace -1)"1" assert )"1" rewrite "atan_neg" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "-8/19<1/x!1&1/x!1<0" )"1" "1" (assert ) nil nil ))nil )"2" assert )"2" "2" "1" rewrite "div_mult_neg_lt2" nil nil )"2" assert )"2" rewrite "div_mult_neg_lt1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case-replace "cx!1(3)<=-4" )"1" (assert )"1" (case "-19<=cx!1(3)" )"1" (hide 1)"1" (copy -3)"1" (expand "cauchy_prop" -1)"1" (inst - "3" )"1" (rewrite "expt_x3" )"1" (flatten)"1" (case "-20/8<x!1&x!1<-3/8" )"1" (hide -2 -3 -4 -5)"1" "1" "int_lemma" ("n" "1" ))"1" "add_lemma" "x" "x!1" "y" "1" "cx" "cx!1" "cy" "cauchy_int(1)" ))"1" "sub_lemma" "x" "x!1" "y" "1" "cx" "cx!1" "cy" "cauchy_int(1)" ))"1" assert )"1" "div_lemma" "x" "1 + x!1" "cx" "cauchy_add(cx!1, cauchy_int(1))" "nzy" "x!1 - 1" "nzcy" "cauchy_sub(cx!1, cauchy_int(1))" ))"1" assert )"1" "atan_dr_lemma" "ssx" "(1 + x!1) / (x!1 - 1)" "cssx" "cauchy_div(cauchy_add(cx!1, cauchy_int(1)), ")) "1" assert )"1" "1" "lemma_div2n" "x" "pi" "cx" "cauchy_pi" "n" "2" ))"1" rewrite "pi_lemma" )"1" expand "div2n" )"1" rewrite "expt_x2" )"1" "neg_lemma" "x" "pi/4" "cx" "cauchy_div2n(cauchy_pi, 2)" ))"1" assert )"1" "atan_plus" "x" "x!1" "y" "1" ))"1" assert )"1" "atan_neg" "x" "(1 + x!1) / (1 - x!1)" ))"1" assert )"1" "-((1 + x!1) / (1 - x!1)) = (1 + x!1) / (x!1 - 1)" )"1" assert )"1" expand "pi" )"1" assert )"1" expand "atan" "1" assert )"1" "sub_lemma" "x" "-atan_value(1)" "y" "atan((1 + x!1) / (x!1 - 1))" "cx" "cauchy_neg(cauchy_div2n(cauchy_pi, 2))" "cy" "cauchy_atan_dr(cauchy_div(cauchy_add ")) "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "times_div1" "x" "-1" "y" "1+x!1" "n0z" "1-x!1" ))"2" replace "2" "2" rewrite "cross_mult" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" rewrite "div_mult_neg_lt2" nil nil )"2" rewrite "div_mult_neg_lt1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (case-replace "cx!1(3)<=3" )"1" (assert )"1" (case "-3<=cx!1(3)" )"1" (hide 1 2)"1" (copy -3)"1" (expand "cauchy_prop" -1)"1" (inst - "3" )"1" (rewrite "expt_x3" )"1" (flatten)"1" (case "-1/2<x!1&x!1<1/2" )"1" "1" "1" "atan_dr_lemma" "ssx" "x!1" "cssx" "cx!1" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (case-replace "cx!1(3)<=19" )"1" (assert )"1" (case "4<=cx!1(3)" )"1" (hide 1 2 3)"1" (copy -3)"1" (expand "cauchy_prop" -1)"1" (inst - "3" )"1" (flatten)"1" (rewrite "expt_x3" )"1" case "3/8<x!1&x!1<20/8" )"1" "1" "1" "int_lemma" ("n" "1" ))"1" "add_lemma" "x" "x!1" "y" "1" "cx" "cx!1" "cy" "cauchy_int(1)" ))"1" "sub_lemma" "x" "x!1" "y" "1" "cx" "cx!1" "cy" "cauchy_int(1)" ))"1" assert )"1" "div_lemma" "x" "x!1-1" "cx" "cauchy_sub(cx!1, cauchy_int(1))" "nzy" "1 + x!1" "nzcy" "cauchy_add(cx!1, cauchy_int(1))" ))"1" assert )"1" "atan_dr_lemma" "ssx" "(x!1 - 1) / (1 + x!1)" "cssx" "cauchy_div(cauchy_sub(cx!1, cauchy_int(1)), ")) "1" assert )"1" "1" "lemma_div2n" "x" "pi" "cx" "cauchy_pi" "n" "2" ))"1" rewrite "pi_lemma" )"1" expand "div2n" )"1" rewrite "expt_x2" )"1" assert )"1" "atan_minus" "x" "x!1" "y" "1" ))"1" assert )"1" expand "pi" )"1" assert )"1" expand "atan" "1" assert )"1" "add_lemma" "x" "atan_value(1)" "y" "atan((x!1 - 1) / (1 + x!1))" "cx" "cauchy_div2n(cauchy_pi, 2)" "cy" "cauchy_atan_dr(cauchy_div(cauchy_sub ")) "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" rewrite "div_mult_pos_lt2" nil nil )"2" rewrite "div_mult_pos_lt1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (case "20<=cx!1(3)" )"1" (assert )"1" (hide 1 2 3 4)"1" (copy -2)"1" (expand "cauchy_prop" -1)"1" (inst - "3" )"1" (rewrite "expt_x3" )"1" (flatten)"1" case "19/8<x!1" )"1" "1" "inv_lemma" "nzx" "x!1" "nzcx" "cx!1" ))"1" assert )"1" "atan_dr_lemma" "ssx" "1/x!1" "cssx" "cauchy_inv(cx!1)" ))"1" assert )"1" rewrite "atan_inv" )"1" "lemma_div2n" "x" "pi" "cx" "cauchy_pi" "n" "1" ))"1" rewrite "pi_lemma" )"1" expand "div2n" )"1" rewrite "expt_x1" )"1" "sub_lemma" "x" "pi / 2" "cx" "cauchy_div2n(cauchy_pi, 1)" "y" "pi / 2 - atan(x!1)" "cy" "cauchy_atan_dr(cauchy_inv(cx!1))" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "0<1/x!1&1/x!1<8/19" )"1" "1" (assert ) nil nil ))nil )"2" assert )"2" "2" "1" assert )"1" rewrite "div_mult_pos_lt2" nil nil ))nil )"2" rewrite "div_mult_pos_lt1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"cauchy_real" atanx nil )nil int nil )"real" reals nil )nil div nil )"cauchy_real" add nil )"cauchy_real" sub nil )nil reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"cauchy_real" div nil )nil inv nil )nil real_props nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"real" atan "trig_fnd/" )"[T, T -> boolean]" equalities nil )nil atan "trig_fnd/" )"odd_int" integersnil )"cauchy_real" int nil )nil add nil )nil atan "trig_fnd/" )nil real_props nil )nil real_props nil )"posrat" nil )"int" integers nil )"int" integers nil )"nzreal" real_typesnil )"cauchy_nzreal" neg nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil real_types nil )nil real_types nil )"(total_order?[real])" nil )"real" reals nil )nil real_props nil )"[bool, bool -> bool]" booleans nil )nil atanx nil )nil exponentiation nil )nil atan "trig_fnd/" )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil atan "trig_fnd/" )"real" reals nil )"real_abs_lt_pi2" atan "trig_fnd/" )nil atan "trig_fnd/" )"cauchy_real" shift nil )"cauchy_real" atanx nil )nil sub nil )"posreal" nil )"real" shift nil )"posreal" atan "trig_fnd/" )nil real_types nil )"bool" reals nil )nil real_types nil )"cauchy_real" atanx nil )nil shift nil )nil atanx nil )AND const-decl "[bool, bool -> bool]" booleans nil )"cauchy_real" neg nil )nil atanx nil )"bool" atanx nil )nil atanx nil )"cauchy_nzreal" inv nil )nil neg nil )"nzreal" nil )nil reals nil )nil cauchy nil )"bool" cauchy nil )nil inv nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"bool" reals nil )"nzrat" rationalsnil )"int" integers nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil exponentiation nil )"bool" cauchy nil )"posint" exponentiation nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil cauchy nil )"bool" cauchy 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 )"even_int" integers nil )"nzint" integers nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.298Angebot
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-27)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
