Impressum asin.prf
Sprache: Lisp
(asin (real_abs_le_pi2_TCC1 0nil 3323019118"" (subtype-tcc) nil nil )"nzreal" nil )"nzreal" nil )"posreal" real_types nil )"(total_order?[real])" nil ))nil ))nil 3262199128"" (skolem 1 ("x" ))"" (flatten)"" (typepred "x" )"" (expand "abs" )"" (assert )"" "le_times_le_pos" "nnx" "-x" "y" "1" "nnz" "-x" "w" "1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"nzreal" nil )"nzreal" nil )"odd_int" integersnil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil asin nil ))nil 3262199262"" (grind)"1" (lemma "sq_lt_abs" ("a" "-x!1" "b" "1" ))"1" (grind) nil nil )) nil )"2" (rewrite "sq_rew" )"2" (lemma "sq_lt" ("nna" "x!1" "nnb" "1" ))"2" (grind) nil nil )) nil ))nil ))nil )"real" reals nil )nil sq "reals/" )"{r: posrat | r >= q}" nil )"{j: nonneg_int | j >= i}" real_defs nil )"{j: posint | j >= i}" nil )"{n: nonneg_real | n >= m AND n >= -m}" nil )"nonneg_real" sq "reals/" )"posreal" sq "reals/" )"real" realsnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"odd_int" integersnil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil asin nil )"real" realsnil ))nil 3262199449"" (skolem 1 ("x" ))"" (flatten)"" (typepred "x" )"" (expand "abs" )"" (case "x < 0" )"1" (assert )"1" "lt_times_lt_pos1" "px" "-x" "y" "1" "nnz" "-x" "w" "1" ))"1" (assert ) nil nil )) nil ))nil )"2" (assert )"2" "lt_times_lt_pos1" "px" "x" "y" "1" "nnz" "x" "w" "1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )"real" reals nil )nil real_props nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"odd_int" integersnil )"real" realsnil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil asin nil )"real" realsnil ))nil 3262199280"" (skolem 1 ("x" ))"" (flatten)"" (typepred "x" )"" (assert )"" (typepred "atan(x / sqrt(1 - x * x))" )"1" (rewrite "pi_value" 2)"1" (expand "atan" 2 4)"1" (assert )"1" (expand "atan" -2 2)"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (hide 3)"2" (lemma "sqrt_pos" ("px" "1-x*x" ))"1" (assert ) nil nil )"2" (hide 2)"2" (lemma "sq_lt_abs" ("a" "x" "b" "1" ))"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" realsnil )"real" realsnil )"nzreal" nil )"nzreal" nil )"(strict_total_order?[real])" real_props nil )"odd_int" integersnil )"(total_order?[real])" nil )"posreal" sq "reals/" )"{j: posint | j >= i}" nil )"{j: nonneg_int | j >= i}" real_defs nil )"{r: posrat | r >= q}" nil )"{n: nonneg_real | n >= m AND n >= -m}" nil )"nonneg_real" sq "reals/" )nil sq "reals/" )"(strict_total_order?[real])" real_props nil )nil sqrt "reals/" )nil atan nil )"real" reals nil )"(total_order?[real])" nil )"bool" reals nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" trig_basic nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" nil )nil atan nil )"real_abs_lt_pi2" atan nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fieldsnil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt"reals/" )"[numfield, numfield -> numfield]" number_fieldsnil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil asin nil )"real" realsnil ))nil 3262199369"" (expand "abs" )"" (skolem!)"" (flatten)"" (typepred "pi" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posreal" real_types nil )"nzreal" nil )"nzreal" nil )"(total_order?[real])" nil )"odd_int" integersnil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals 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}" nil ))nil 3262231650"" (skolem!)"" (typepred "nx!1" )"" (expand "abs" )"" (lemma "sq_le_abs" ("a" "-nx!1" "b" "1" ))"" (grind) nil nil )) nil ))nil ))nil ))nil )"bool" reals nil )nil asin nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"real" realsnil )"posreal" sq "reals/" )"(strict_total_order?[real])" real_props nil )"{j: posint | j >= i}" nil )"{j: nonneg_int | j >= i}" real_defs nil )"{r: posrat | r >= q}" nil )"odd_int" integersnil )"(total_order?[real])" nil )"real" realsnil )"{n: nonneg_real | n >= m AND n >= -m}" nil )"nonneg_real" sq "reals/" )nil sq "reals/" )"real" reals nil ))nil 3262231879 ("" (grind) nil nil )nil shostak))nil 3322498655"" (skolem 1 ("nx" ))"" (typepred "nx" )"" (expand "<=" )"" (expand "asin" )"" (split -1)"1" (assert )"1" "both_sides_times_neg_lt1" "nz" "-1" "x" "nx" "y" "-1" ))"1" "lt_times_lt_neg1" "x" "-1" "ny" "nx" "z" "-1" "npw" "nx" ))"1" (assert )"1" "sqrt_lt" "nny" "0" "nnz" "1-nx*nx" ))"1" (rewrite "sqrt_0" -1)"1" "atan_inv_neg" "nx" "sqrt(1 - nx * nx) / nx" ))"1" rewrite "pi_value" 1)"1" "div_div1" "x" "1" "n0y" "sqrt(1-nx*nx)" "n0z" "nx" ))"1" replace -1 -2)"1" (assert ) nil nil ))nil ))nil ))nil )"2" "both_sides_div_neg_lt1" "y" "0" "x" "sqrt(1-nx*nx)" "nz" "nx" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (case "nx = -1" )"1" (replace -1)"1" (rewrite "sqrt_0" )"1" (rewrite "atan_0" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )nil asin nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"nzreal" nil )"real_abs_le_pi2" asin nil )nil atan nil )"even_int" nil )"(divides(m))" dividesnil )"nzreal" nil )"real" realsnil )"real" realsnil )"odd_int" integersnil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"(total_order?[real])" nil )nil sqrt "reals/" )"bool" reals nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )"(total_order?[real])" nil )nil atan nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil real_types nil )"[T, T -> boolean]" equalities nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt"reals/" )nil real_props nil )nil reals nil )"real" reals nil )nil atan nil )nil real_props nil )nil sqrt "reals/" )"odd_int" integersnil )"(divides(n))" dividesnil )nil real_types nil )nil real_types nil )nil real_props nil )"real" realsnil ))nil ))nil 3262251224"" (skosimp*)"" (typepred "px!1" )"" (expand "abs" )"" "le_times_le_pos" "nnx" "px!1" "y" "1" "nnz" "px!1" "w" "1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil )"bool" reals nil )nil asin nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"real" realsnil )"real" realsnil )"(strict_total_order?[real])" real_props nil )"odd_int" integersnil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil real_props nil )"bool" reals nil )nil real_types nil ))nil 3262251224 ("" (grind) nil nil )nil shostak))nil 3408901117"" (skolem 1 ("px" ))"" (case "abs(px) <= 1" )"1" (expand "<=" )"1" (split -1)"1" (expand "asin" )"1" (assert )"1" (lemma "sq_nz_pos" ("nz" "px" ))"1" (expand "sq" )"1" "lt_times_lt_pos1" "px" "px" "y" "1" "nnz" "px" "w" "1" ))"1" (assert )"1" "sqrt_lt" "nny" "0" "nnz" "1-px*px" ))"1" (rewrite "sqrt_0" )"1" "atan_inv" "px" "sqrt(1 - px * px) / px" ))"1" "div_div1" "x" "1" "n0y" "sqrt(1-px*px)" "n0z" "px" ))"1" replace -1 -2)"1" rewrite "pi_value" 1)"1" (assert ) nil nil ))nil ))nil ))nil )"2" "posreal_div_posreal_is_posreal" "px" "sqrt(1-px*px)" "py" "px" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "asin" )"2" (assert )"2" (lift-if)"2" (expand "abs" )"2" (assert )"2" (replace -1)"2" (assert )"2" (rewrite "atan_0" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "px" )"2" (hide 2) (("2" (grind) nil nil )) nil )) nil ))nil ))nil )"bool" reals nil )nil asin nil )"{n: nonneg_real | n >= m AND n >= -m}" nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )"nzreal" nil )"posreal" real_types nil )"real" realsnil )"real" realsnil )"(strict_total_order?[real])" real_props nil )"nonneg_real" sq "reals/" )"(total_order?[real])" nil )nil sqrt "reals/" )nil real_typesnil )nil real_props nil )nil reals nil )nil atan nil )"nzreal" nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt"reals/" )"[T, T -> boolean]" equalities nil )nil real_types nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )nil atan nil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )nil sqrt "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil real_types nil )"bool" reals nil )nil real_props nil )nil reals nil )"boolean" notequal nil )nil sq "reals/" )"real_abs_le_pi2" asin nil )nil atan nil )"even_int" nil )"(divides(m))" dividesnil )"nnreal" nil )"even_int" nil )"posint" nil )"odd_int" integersnil )"(divides(n))" dividesnil )"odd_int" integersnil )NOT const-decl "[bool -> bool]" booleans nil )"real" realsnil ))nil )nil 3322498693"" (skolem 1 ("px" ))"" (typepred "px" )"" (expand "abs" -1)"" (expand "<=" -1)"" (split -1)"1" (expand "asin" )"1" (assert )"1" (lemma "sq_nz_pos" ("nz" "px" ))"1" (expand "sq" )"1" "lt_times_lt_pos1" "px" "px" "y" "1" "nnz" "px" "w" "1" ))"1" (assert )"1" "sqrt_lt" "nny" "0" "nnz" "1-px*px" ))"1" rewrite "sqrt_0" )"1" "atan_inv_value" "px" "sqrt(1 - px * px) / px" ))"1" "div_div1" "x" "1" "n0y" "sqrt(1-px*px)" "n0z" "px" ))"1" replace -1 -2)"1" rewrite "pi_value" 1)"1" expand "atan" 1)"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "posreal_div_posreal_is_posreal" "px" "sqrt(1-px*px)" "py" "px" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "asin" )"2" (replace -1)"2" (hide -1 -2)"2" (rewrite "sqrt_0" )"2" (rewrite "atan_0" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nonneg_real" sq "reals/" )nil sqrt "reals/" )nil atan nil )"real_abs_lt_pi2" atan nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt"reals/" )nil sqrt "reals/" )nil sq "reals/" )nil atan nil ))nil ))nil 3262232045"" (expand "asin" )"" (rewrite "sqrt_1" ) (("" (rewrite "atan_0" ) nil nil ))nil ))nil )nil sqrt "reals/" )"posreal" sqrt "reals/" )nil atan nil )"real_abs_le_pi2" asin nil ))nil 3263820156"" (expand "abs" )"" (typepred "sqrt(1/2)" )"" (assert )"" (lemma "sqrt_le" ("nny" "1/2" "nnz" "1" ))"" (rewrite "sqrt_1" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"odd_int" integersnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posreal" real_types nil )"(total_order?[real])" nil )nil sqrt "reals/" )nil sqrt "reals/" )"posrat" nil )"posreal" sqrt "reals/" )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )nil real_types nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt"reals/" )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"bool" reals nil ))nil 3322498751"" (expand "asin" )"" (typepred "sqrt(1/2)" )"" (lemma "sqrt_lt" ("nny" "1/2" "nnz" "1" ))"" (rewrite "sqrt_1" -1)"" (assert )"" (rewrite "sq_rew" 1)"" (rewrite "div_simp" 1)"" (rewrite "pi_value" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt"reals/" )"[numfield, numfield -> numfield]" number_fieldsnil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"posrat" nil )nil sqrt "reals/" )"nzreal" nil )"odd_int" integersnil )nil sq "reals/" )"posreal" sq "reals/" )nil sqrt "reals/" )nil atan nil )"real" realsnil )"real" realsnil )nil real_props nil )nil reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"real" realsnil )"posreal" real_types nil )nil sqrt "reals/" )"real_abs_le_pi2" asin nil )"posreal" real_types nil )"posreal" sqrt "reals/" ))nil ))nil 3262276037"" (expand "asin" ) (("" (propax) nil nil )) nil )"real_abs_le_pi2" asin nil )) shostak))nil 3262231915 ("" (grind) nil nil ) nil nil 3262232085"" (skolem 1 ("x" ))"" (expand "asin" )"" (case "x = -1" )"1" (assert ) nil nil )"2" (case "x = 1" )"1" (assert ) nil nil )"2" (case "-1 < x & x < 1" )"1" (flatten -1)"1" (assert )"1" "atan_neg" ("x" "x / sqrt(1 - -x * -x)" ))"1" (assert ) nil nil )"2" (hide 4)"2" (lemma "asin_TCC3" ("x" "x" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 4)"2" (assert )"2" (typepred "x" ) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" realsnil )"real_abs_le_pi2" asin nil )"[numfield, numfield -> numfield]" number_fieldsnil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt"reals/" )"[numfield, numfield -> numfield]" number_fieldsnil )nil real_types nil )nil real_types nil )"bool" reals nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )nil atan nil )"(total_order?[real])" nil )"real" realsnil )"real" realsnil )"bool" reals nil )"nzreal" nil )"nzreal" nil )"posreal" real_types nil )"(strict_total_order?[real])" real_props nil )"odd_int" integersnil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" nil )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 )"[numfield -> numfield]" number_fields nil )nil asin nil ))nil 3262276084"" (expand "asin" ) (("" (propax) nil nil )) nil )"real_abs_le_pi2" asin nil )) shostak))nil 3263821369"" (expand "abs" )"" (typepred "sqrt(1/2)" )"" (assert )"" (lemma "sqrt_le" ("nny" "1/2" "nnz" "1" ))"" (rewrite "sqrt_1" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"nzreal" nil )"odd_int" integersnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posreal" real_types nil )"(total_order?[real])" nil )nil sqrt "reals/" )nil sqrt "reals/" )"posrat" nil )"posreal" sqrt "reals/" )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )nil real_types nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt"reals/" )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"bool" reals nil ))nil 3263819795"" (lemma "asin_sqrt_half" )"" (rewrite "asin_neg" 1)"1" (assert ) nil nil )"2" (hide-all-but 1)"2" (expand "abs" )"2" (lemma "sqrt_le" ("nny" "1/2" "nnz" "1" ))"2" (rewrite "sqrt_1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"posrat" nil )"posreal" sqrt "reals/" )nil asin nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )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 )"[numfield -> numfield]" number_fields nil )nil asin nil )"bool" reals nil )nil real_types nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fieldsnil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt"reals/" )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"nzreal" nil )"real" reals nil )"posreal" real_types nil )"nzreal" nil )nil asin nil ))nil 3322498826"" (lemma "atan_strict_increasing" )"" (expand "strict_increasing?" )"" (skolem 1 ("x" "y" ))"" (flatten)"" (expand "asin" )"" (case "abs(x) <= 1" )"1" (case "abs(y) <= 1" )"1" case "FORALL (z:real): abs(z) < 1 => 0 < sqrt(1-z*z)" )"1" (expand "<=" (-2 -3))"1" (split -3)"1" (inst-cp -2 "x" )"1" (assert )"1" case "y = -1" )"1" "1" "trichotomy" ("x" "x" ))"1" "1" (assert ) nil nil )"2" (assert ) nil nil )"3" expand "abs" -3)"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" case "y < 1" )"1" assert )"1" case "x= -1" )"1" (assert ) nil nil )"2" expand "abs" -3)"2" assert )"2" "y" )"2" "1" assert )"1" "x / sqrt(1 - x * x)" "y / sqrt(1 - y * y)" )"1" "1" nil nil )"2" "2" "div_mult_pos_lt1" "z" "x" "py" "sqrt(1-x*x)" "x" "y / sqrt(1 - y * y)" ))"2" replace "2" "div_mult_pos_lt2" "x" "x" "z" "y*sqrt(1-x*x)" "py" "sqrt(1-y*y)" ))"1" replace "1" "1" "trichotomy" "x" "x" ))"1" "1" "sq_lt" "nna" "x * sqrt(1 - y * y)" "nnb" "y * sqrt(1 - x * x)" ))"1" replace "1" rewrite "sq_times" "1" rewrite "sq_times" "1" expand "sq" "1" "sq_lt" "nna" "x" "nnb" "y" ))"1" expand "sq" "1" assert )nil nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "posreal_times_posreal_is_posreal" "px" "y" "py" "sqrt(1-x*x)" ))"1" assert )nil nil )"2" assert )nil nil ))nil )"3" "posreal_times_posreal_is_posreal" "px" "x" "py" "sqrt(1-y*y)" ))"1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" replace "2" rewrite "sqrt_1" "2" assert )nil nil ))nil ))nil )"3" case "y < 0" )"1" "both_sides_times_neg_lt1" "nz" "-1" "y" "x * sqrt(1 - y * y)" "x" "y * sqrt(1 - x * x)" ))"1" replace "1" "sq_lt" "nna" "(-1 *y) * sqrt(1 - x * x)" "nnb" "(-1*x) * sqrt(1 - y * y)" ))"1" replace "1" rewrite "sq_times" "1" expand "sq" "1" rewrite "sq_times" "1" rewrite "sq_times" "1" expand "sq" "1" "1" assert )"1" "sq_lt" "nna" "-1*y" "nnb" "-1*x" ))"1" expand "sq" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "posreal_times_posreal_is_posreal" "px" "-1*x" "py" "sqrt(1-y*y)" ))"1" assert )nil nil )"2" assert )nil nil ))nil )"3" "posreal_times_posreal_is_posreal" "px" "-1*y" "py" "sqrt(1-x*x)" ))"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "nnreal_times_nnreal_is_nnreal" "nnx" "y" "nny" "sqrt(1 - x * x)" ))"1" "both_sides_times_pos_lt1" "x" "x" "y" "0" "pz" "sqrt(1 - y * y)" ))"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "trichotomy" "x" "y" ))"2" "1" assert )nil nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "x= -1" )"1" nil nil )"2" expand "abs" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "abs" )"2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (hide 2)"2" (hide -2 -3 -4 -5)"2" (expand "abs" )"2" "2" "1" "sq" )"1" assert )"1" "sq" )"1" (grind) nil nil )"2" rewrite "sq_lt" )nil nil ))nil ))nil ))nil )"2" "sq" )"2" assert )"2" "sq" )"1" (grind) nil nil )"2" rewrite "sq_lt" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (assert )"3" (hide -2 -3 -4 2)"3" (expand "abs" )"3" "3" "1" "sq" )"1" (grind) nil nil )"2" (rewrite "sq_lt" ) nil nil ))nil )"2" "1" (assert ) nil nil )"2" "sq" )"1" (grind) nil nil )"2" rewrite "sq_lt" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "abs" )"2" (lift-if) (("2" (ground) nil nil )) nil ))nil ))nil )"2" (hide-all-but 1)"2" (typepred "x" ) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" real_fun_preds "reals/" )nil asin nil )"{n: nonneg_real | n >= m AND n >= -m}" nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )"[numfield, numfield -> numfield]" number_fieldsnil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt"reals/" )"[numfield, numfield -> numfield]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil real_types nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )"real" realsnil )"nzreal" nil )"real" realsnil )"odd_int" integersnil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )"real" reals nil )"posreal" sq "reals/" )nil real_types nil )nil real_types nil )nil real_props nil )nil real_props nil )nil real_typesnil )"nonneg_int" nil )"even_int" nil )"(divides(n))" dividesnil )nil sqrt "reals/" )nil sq "reals/" )nil sq "reals/" )"nnreal" nil )nil sqrt "reals/" )"nonneg_real" sq "reals/" )nil real_typesnil )nil real_props nil )nil real_types nil )"bool" reals nil )nil real_props nil )"posreal" real_types nil )"(strict_total_order?[real])" real_props nil )nil real_axioms nil )"nzreal" nil )nil sq "reals/" )NOT const-decl "[bool -> bool]" booleans nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )"(total_order?[real])" nil )nil extra_real_props nil )"posint" nil )"odd_int" integersnil )"real_abs_le_pi2" asin nil )"real" realsnil )nil atan nil ))nil ))nil 3322498893"" (expand "bijective?" )"" (split 1)"1" (expand "injective?" )"1" (skolem 1 ("x" "y" ))"1" (flatten)"1" (lemma "asin_strict_increasing" )"1" (expand "strict_increasing?" )"1" (lemma "trich_lt" ("x" "x" "y" "y" ))"1" (split -1)"1" (inst - "x" "y" )"1" (assert ) nil nil )) nil )"2" (propax) nil nil )"3" (inst - "y" "x" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "atan_bij" )"2" (expand "bijective?" )"2" (flatten)"2" (hide -1)"2" (expand "surjective?" )"2" (skosimp*)"2" (expand "asin" )"2" (case "abs(y!1) <= pi/2" )"1" (expand "<=" -1)"1" (split -1)"1" "y!1" )"1" "1" "x!1/sqrt(1+x!1*x!1)" )"1" "sq_pos" ("a" "x!1" ))"1" expand "sq" -1)"1" "sqrt_pos" "px" "1+x!1*x!1" ))"1" case "abs(x!1 / sqrt(1 + x!1 * x!1)) < 1" )"1" case "x!1 / sqrt(1 + x!1 * x!1) /= -1" )"1" assert )"1" case "x!1 / sqrt(1 + x!1 * x!1) * (x!1 / sqrt(1 + x!1 * x!1)) = sq(x!1)/(1+sq(x!1))" )"1" replace -1 1)"1" case "sqrt(1 - sq(x!1) / (1 + sq(x!1))) = 1/sqrt(1+x!1*x!1)" )"1" replace -1 1)"1" "div_div2" "x" "x!1" "n0y" "sqrt(1 + x!1 * x!1)" "n0z" "1 / sqrt(1 + x!1 * x!1)" ))"1" replace "1" "sq_sqrt" "x" "sqrt(1 + x!1 * x!1)" ))"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "minus_div1" "x" "1" "n0x" "1" "y" "sq(x!1)" "n0y" "1+sq(x!1)" ))"2" replace "2" "2" rewrite "sqrt_div" "2" expand "sq" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "div_mult_pos_le1" "z" "sq(x!1)" "py" "1+sq(x!1)" "x" "1" ))"3" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "sq_rew" "2" rewrite "sq_rew" "2" rewrite "sq_div" "2" rewrite "sq_sqrt" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" "2" "sq" )"1" (grind) nil nil )"2" rewrite "sq_lt" )nil nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "sq_pos" ("a" "x!1" ))"2" expand "sq" -1)"2" case "abs(x!1) / abs(sqrt(1 + x!1 * x!1)) <= 1" )"1" "1" nil nil )"2" nil nil ))nil )"2" "2" "sqrt_pos" "px" "1+x!1*x!1" ))"2" expand "abs" 1 2)"2" assert )"2" "div_mult_pos_le1" "z" "abs(x!1)" "py" "sqrt(1 + x!1 * x!1)" "x" "1" ))"2" "2" "sq_le" "nna" "abs(x!1)" "nnb" "sqrt(1 + x!1 * x!1)" ))"2" replace "2" rewrite "sq_sqrt" "2" "2" expand "abs" )"2" expand "sq" )"2" case "x!1<0" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "sq_pos" "a" "x!1" ))"3" expand "sq" -1)"3" "sqrt_pos" "px" "1+x!1*x!1" ))"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "sqrt_pos" "px" "1+x!1*x!1" ))"3" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" expand "abs" -1)"2" case "y!1<0" )"1" assert )"1" "-1" )"1" (assert ) nil nil ))nil ))nil )"2" assert )"2" "1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (typepred "y!1" )"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil asin nil )nil asin nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"bool" real_fun_preds "reals/" )"bool" functions nil )nil asin nil )"{r: posreal | r > pi_lb AND r < pi_ub}" nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )nil real_types nil )"bool" reals nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )"{n: nonneg_real | n >= m AND n >= -m}" nil )nil real_types nil )"bool" reals nil )"posreal" real_types nil )nil sq "reals/" )nil extra_real_props nil )nil real_props nil )nil sq "reals/" )nil sqrt "reals/" )"(strict_total_order?[real])" real_props nil )nil sq "reals/" )"real" reals nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"odd_int" integersnil )"nnreal" nil )"posreal" real_types nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil real_props nil )nil reals nil )nil sqrt "reals/" )nil real_props nil )"posreal" real_types nil )"nnreal" nil )nil sqrt "reals/" )"posreal" sqrt "reals/" )nil sqrt "reals/" )"posrat" nil )nil real_props nil )nil sq "reals/" )"posreal" sq "reals/" )nil sq "reals/" )"real" realsnil )"nonneg_real" sq "reals/" )"real" asin nil )"[numfield, numfield -> numfield]" number_fieldsnil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt"reals/" )"[numfield, numfield -> numfield]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil real_types nil )"real" realsnil )"real" realsnil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil atan nil )"real_abs_le_pi2" asin nil )"nzreal" nil )"real_abs_le_pi2" asin nil )"real" realsnil )"bool" functions nil )nil atan nil )"bool" functions nil ))nil ))nil 3263658797"" (skosimp*)"" (typepred "nnx!1" ) (("" (assert ) nil nil )) nil )) nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"odd_int" integersnil ))nil 3263658941"" (skosimp*)"" (typepred "nny!1" )"" (lemma "sq_le" ("nna" "0" "nnb" "nny!1" ))"" (lemma "sq_le" ("nnb" "1" "nna" "nny!1" ))"" (rewrite "sq_0" )"" (rewrite "sq_1" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil sq "reals/" )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" realsnil )nil sq "reals/" )nil sq "reals/" )nil real_types nil ))nil 3263820296"" (skosimp*)"" (typepred "nnx!1" )"" (typepred "nny!1" )"" (expand ">=" )"" (lemma "sq_le" ("nna" "0" "nnb" "nnx!1" ))"" (lemma "sq_le" ("nna" "0" "nnb" "nny!1" ))"" (lemma "sq_le" ("nnb" "1" "nna" "nny!1" ))"" (lemma "sq_le" ("nnb" "1" "nna" "nnx!1" ))"" (rewrite "sq_0" )"" (rewrite "sq_1" )"" (replace -5 -3)"" (simplify -3)"" replace -6 -2)"" replace -7 -4)"" replace -8 -1)"" "" "" "" "sqrt(1-sq(nnx!1))" )"1" "sqrt(1-sq(nny!1))" )"1" "sqrt_le" "nny" "1-sq(nnx!1)" "nnz" "1" ))"1" "sqrt_le" "nny" "1-sq(nny!1)" "nnz" "1" ))"1" assert )"1" rewrite "sqrt_1" )"1" "le_times_le_pos" "nnx" "nnx!1" "y" "1" "nnz" "sqrt(1 - sq(nny!1))" "w" "1" ))"1" "le_times_le_pos" "nnx" "nny!1" "y" "1" "nnz" "sqrt(1 - sq(nnx!1))" "w" "1" ))"1" assert )"1" "nnreal_times_nnreal_is_nnreal" "nnx" "nnx!1" "nny" "(sqrt(1 - sq(nny!1)))" ))"1" "nnreal_times_nnreal_is_nnreal" "nnx" "nny!1" "nny" "(sqrt(1 - sq(nnx!1)))" ))"1" "le_minus_le" "z" "nny!1 * sqrt(1 - sq(nnx!1))" "w" "0" "x" "nnx!1 * sqrt(1 - sq(nny!1))" "y" "1" ))"1" "le_minus_le" "w" "nny!1 * sqrt(1 - sq(nnx!1))" "z" "1" "y" "nnx!1 * sqrt(1 - sq(nny!1))" "x" "0" ))"1" expand "abs" "1" case "nnx!1 * (sqrt(1 - sq(nny!1))) - nny!1 * (sqrt(1 - sq(nnx!1))) < 0" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil sq "reals/" )"(total_order?[real])" nil )nil real_props nil )nil sqrt "reals/" )"posreal" sqrt "reals/" )"odd_int" integersnil )nil sqrt "reals/" )"(total_order?[real])" nil )"real" realsnil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt"reals/" )"[numfield, numfield -> numfield]" number_fieldsnil )"nonneg_real" sq "reals/" )"nnreal" nil )nil sq "reals/" )nil sq "reals/" )nil real_types nil ))nil 3322498939"" (skolem 1 ("nnx" "nny" ))"" (typepred "nnx" )"" (typepred "nny" )"" (expand ">=" )"" (expand "<=" (-4 -1))"" (split -4)"1" (expand "<=" -4)"1" (split -4)"1" (split -3)"1" (expand "<=" -4)"1" (split -4)"1" (expand "asin" )"1" "sq_lt" "nna" "nnx" "nnb" "1" ))"1" "sq_lt" "nna" "nny" "nnb" "1" ))"1" rewrite "sq_1" )"1" "sq_lt" "nnb" "nnx" "nna" "0" ))"1" "sq_lt" "nnb" "nny" "nna" "0" ))"1" rewrite "sq_0" )"1" assert )"1" rewrite "sq_rew" 1)"1" rewrite "sq_rew" 1)"1" rewrite "sq_rew" 1)"1" rewrite "sq_rew" "1" "1" rewrite "sq_rew" "1" rewrite "sq_rew" "1" "sqrt_pos" "px" "1-sq(nnx)" ))"1" "sqrt_pos" "px" "1-sq(nny)" ))"1" "sqrt_lt" "nny" "1-sq(nnx)" "nnz" "1" ))"1" "sqrt_lt" "nny" "1-sq(nny)" "nnz" "1" ))"1" rewrite "sqrt_1" )"1" assert )"1" "lt_times_lt_pos1" "px" "nny" "y" "1" "nnz" "(sqrt(1 - sq(nnx)))" "w" "1" ))"1" assert )"1" "lt_times_lt_pos1" "px" "nnx" "y" "1" "nnz" "(sqrt(1 - sq(nny)))" "w" "1" ))"1" assert )"1" "atan_minus" "x" "nnx / sqrt(1 - sq(nnx))" "y" "nny / sqrt(1 - sq(nny))" ))"1" "posreal_div_posreal_is_posreal" "px" "nnx" "py" "sqrt(1-sq(nnx))" ))"1" "posreal_div_posreal_is_posreal" "px" "nny" "py" "sqrt(1-sq(nny))" ))"1" assert )"1" "1" "posreal_times_posreal_is_posreal" "px" "nnx / sqrt(1 - sq(nnx))" "py" "nny / sqrt(1 - sq(nny))" ))"1" assert )"1" "1" "SQX" "sqrt(1 - sq(nnx))" )"1" "SQY" "sqrt(1 - sq(nny))" )"1" "minus_div1" "x" "nnx" "n0x" "SQX" "y" "nny" "n0y" "SQY" ))"1" replace "1" rewrite "div_div2" "1" "div_cancel1" "n0z" "SQX*SQY" "x" "nnx*nny" ))"1" replace "1" case "sq(SQX * SQY + nnx * nny) = 1 - sq(nnx) - sq(nny) + sq(nnx) * nny * nny + ") "1" replace "1" rewrite "sqrt_sq" nil nil ))nil )"2" "2" expand "SQX" "2" expand "SQY" "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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1)"2" rewrite "asin_1" )"2" rewrite "sq_1" )"2" rewrite "sqrt_0" )"2" "2" "2" "asin_neg" "x" "sqrt(1 - sq(nnx))" ))"1" replace -1 1)"1" expand "asin" )"1" "1" "sq_lt" "nna" "0" "nnb" "nnx" ))"1" "sq_lt" "nnb" "1" "nna" "nnx" ))"1" rewrite "sq_0" )"1" rewrite "sq_1" )"1" assert )"1" rewrite "sq_rew" "1" rewrite "sq_rew" "1" "1" "sqrt_lt" "nny" "1-sq(nnx)" "nnz" "1" ))"1" rewrite "sqrt_1" )"1" assert )"1" rewrite "pi_value" "1" "sq_lt" "nna" "0" "nnb" "nnx" ))"1" rewrite "sq_0" )"1" "sqrt_pos" "px" "1-sq(nnx)" ))"1" "posreal_div_posreal_is_posreal" "px" "sqrt(1-sq(nnx))" "py" "nnx" ))"1" "atan_inv" "px" "sqrt(1 - sq(nnx)) / nnx" ))"1" rewrite "div_div1" "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 ))nil )"2" "2" "sqrt_le" )"2" "1-sq(nnx)" "1" )"2" rewrite "sqrt_1" )"2" "sq_le" "nna" "0" "nnb" "nnx" ))"2" rewrite "sq_0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1 * rl)"2" (rewrite "asin_0" )"2" (rewrite "sq_0" )"2" rewrite "sqrt_1" )"2" "2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1 * rl)"2" (rewrite "asin_0" )"2" (rewrite "sq_0" )"2" (rewrite "sqrt_1" )"2" "2" "asin_neg" ("x" "nny" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1)"2" (rewrite "sq_1" )"2" (rewrite "sqrt_0" )"2" (rewrite "asin_1" )"2" "sq_le" ("nna" "nny" "nnb" "1" ))"2" (expand "sq" -1 2)"2" expand "asin" )"2" expand "<=" -4)"2" "1" assert )"1" "sqrt(1 - sq(nny))" )"1" assert )"1" "1" "1" "sq_lt" "nna" "0" "nnb" "nny" ))"1" "sq_lt" "nnb" "1" "nna" "nny" ))"1" assert )"1" rewrite "sq_rew" "1" rewrite "sq_rew" "1" "1" rewrite "sqrt_sq" "1" "sqrt_lt" )"1" "1-sq(nny)" "1" )"1" rewrite "sqrt_1" "1" assert )"1" rewrite "pi_value" )"1" "atan_inv" "px" "(sqrt(1 - sq(nny))) / nny" ))"1" assert )nil nil )"2" "2" "sqrt_lt" )"2" "0" "1-sq(nny)" )"2" rewrite "sqrt_0" "2" "posreal_div_posreal_is_posreal" "px" "sqrt(1 - sq(nny))" "py" "nny" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1 * rl)"2" rewrite "sq_0" 1)"2" rewrite "sqrt_1" )"2" rewrite "atan_0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" rewrite "sq_1" )"2" "2" rewrite "sqrt_0" )"2" rewrite "sqrt_1" )"2" rewrite "atan_0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil asin nil )"posreal" sq "reals/" )nil asin nil )"[numfield -> numfield]" number_fields nil )nil asin nil )"real" reals nil )nil atan nil )nil real_props nil )nil atan nil )nil sqrt "reals/" )nil sq "reals/" )nil sqrt "reals/" )"posreal" real_types nil )nil asin nil )"nnreal" nil )"real" realsnil )"real" realsnil )"real_abs_le_pi2" asin nil )nil sq "reals/" )nil sq "reals/" )"(total_order?[real])" nil )"nonneg_real" sq "reals/" )"[numfield, numfield -> numfield]" number_fieldsnil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt"reals/" )"[numfield, numfield -> numfield]" number_fieldsnil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil sqrt "reals/" )"(total_order?[real])" nil )nil real_typesnil )nil real_typesnil )nil real_props nil )"nnreal" nil )nil sqrt "reals/" )"{nnz: nnreal | nnz * nnz = 1 - sq(nnx)}" asin nil )"{nnz: nnreal | nnz * nnz = 1 - sq(nny)}" asin nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil reals nil )nil real_props nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )nil atan nil )nil real_props nil )nil sqrt "reals/" )nil sqrt "reals/" )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"bool" reals nil )nil sqrt "reals/" )"(strict_total_order?[real])" real_props nil )"real" realsnil )"odd_int" integersnil )"real" realsnil )"nzreal" nil )nil sq "reals/" )nil real_types nil )nil sq "reals/" )"even_int" nil )"odd_int" nil )"odd_int" integersnil )"posint" nil )nil atan nil )"posreal" real_types nil )"posreal" sqrt "reals/" )"nonneg_int" nil )"even_int" nil )"(divides(n))" dividesnil )"nzreal" nil ))nil ))nil 3263659929"" (skosimp*)"" (typepred "px!1" )"" (expand "abs" -1)"" (expand "abs" 1)"" (assert )"" "posreal_times_posreal_is_posreal" "px" "px!1" "py" "px!1" ))"" (case "px!1 = 1" )"1" (replace -1) (("1" (assert ) nil nil )) nil )"2" "posreal_div_posreal_is_posreal" "px" "px!1 * px!1" "py" "6" ))"2" "both_sides_minus_lt2" "z" "1" "y" "0" "x" "px!1*px!1/6" ))"2" (expand ">" -2)"2" (replace -2 -1)"2" (flatten -1)"2" "lt_times_lt_pos1" "px" "px!1" "y" "1" "nnz" "1 - px!1 * px!1 / 6" "w" "1" ))"1" (assert ) nil nil )"2" assert )"2" "posreal_div_posreal_is_posreal" "px" "px!1 - px!1 * px!1 / 6 * px!1" "py" "px!1" ))"2" "minus_div2" "x" "px!1" "y" "px!1*px!1/6*px!1" "n0x" "px!1" ))"2" replace -1 -2 rl)"2" "2" rewrite "div_simp" -1)"2" case "px!1 * px!1 / 6 * px!1 / px!1 = px!1 * px!1 / 6" )"1" replace -1)"1" assert )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 ))nil ))nil ))nil )"bool" reals nil )nil asin nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil real_typesnil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"(total_order?[real])" nil )nil real_typesnil )"[numfield, numfield -> numfield]" number_fieldsnil )nil real_props nil )nil reals nil )nil real_props nil )"odd_int" nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil real_props nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )nil real_props nil )"[T, T -> boolean]" equalities nil )"(total_order?[real])" nil )"odd_int" integersnil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"(strict_total_order?[real])" real_props nil )"real" realsnil )"real" realsnil )"real" realsnil ))nil 3307805790"" (skosimp*)"" (split)"1" (lemma "asin_derivable2" )"1" (lemma "deriv_asin_fun" )"1" (lemma "identity_derivable_fun[real_abs_lt1]" )"1" (lemma "deriv_id_fun[real_abs_lt1]" )"1" (expand "I" )"1" (expand "const_fun" )"1" "diff_derivable_fun[real_abs_lt1]" "f1" "LAMBDA (x: real_abs_lt1): asin(x)" "f2" "LAMBDA (x: real_abs_lt1): x" ))"1" (assert )"1" (expand "-" )"1" "deriv_diff_fun[real_abs_lt1]" "ff1" "LAMBDA (x: real_abs_lt1): asin(x)" "ff2" "LAMBDA (x: real_abs_lt1): x" ))"1" replace -5 -1)"1" replace -3 -1)"1" expand "-" )"1" "px!1" )"1" expand "abs" -1)"1" expand "<=" -1)"1" "1" "minimum_derivative[{x:nnreal| x < 1}]" "g" "LAMBDA (x_1:{x:nnreal| x < 1} ): asin(x_1) - x_1" "x" "0" "y1" "px!1" ))"1" "1" "1" rewrite "asin_0" )"1" assert )nil nil ))nil ))nil )"2" "restrict2_deriv[{x: nnreal | x < 1},real_abs_lt1]" "f" "LAMBDA (x_1: real_abs_lt1): asin(x_1) - x_1" "a" "0" ))"1" replace -4 -1)"1" "1" expand "restrict2" "1" replace "1" expand "sq" "1" rewrite "sqrt_1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" "3" "x!1" )"3" assert )"3" expand "abs" )"3" assert )nil nil ))nil ))nil ))nil ))nil )"4" "4" case "x!1=0" )"1" "px!1" )"1" assert )nil nil )"2" expand "abs" "2" nil nil ))nil ))nil )"2" "0" )"1" assert )nil nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil )"5" "5" nil nil ))nil ))nil )"3" assert )nil nil )"4" "4" "y!1" )"4" expand ">=" -1)"4" expand "<=" "4" "1" "restrict2_deriv[{x: nnreal | x < 1},real_abs_lt1]" "f" "LAMBDA (x_1: real_abs_lt1): asin(x_1) - x_1" "a" "y!1" ))"1" replace "1" "1" expand "restrict2" "1" replace "1" "1" "sq_lt" "nna" "0" "nnb" "y!1" ))"1" "sq_lt" "nna" "y!1" "nnb" "1" ))"1" expand "sq" "1" expand "sq" "1" assert )"1" "sqrt_pos" "px" "1-sq(y!1)" ))"1" "div_mult_pos_gt2" "z" "1" "py" "sqrt(1-sq(y!1))" "x" "1" ))"1" "sqrt_lt" "nny" "1-sq(y!1)" "nnz" "1" ))"1" rewrite "sqrt_1" )"1" assert )"1" "posreal_times_posreal_is_posreal" "px" "1 / sqrt(1 - sq(y!1))-1" "py" "y!1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" "3" "x!1" )"3" expand "abs" )"3" assert )nil nil ))nil ))nil ))nil )"4" "4" case "x!1 = 0" )"1" "1/2" )"1" assert )nil nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil )"2" "0" )"1" assert )nil nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil )"5" "5" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil )"3" "restrict2_derivable[{x: nnreal | x < 1},real_abs_lt1]" "f" "LAMBDA (x_1: real_abs_lt1): asin(x_1) - x_1" ))"1" expand "restrict2" "1" nil nil ))nil )"2" nil nil )"3" "3" "x!1" )"3" "x!1" )"3" expand "abs" )"3" nil nil ))nil ))nil ))nil ))nil )"4" "4" case "x!1=0" )"1" "1/2" )"1" assert )nil nil )"2" expand "abs" )"2" assert )nil nil ))nil ))nil )"2" "0" )"1" assert )nil nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil )"5" "5" case "x!1=0" )"1" "1/2" )"1" assert )nil nil ))nil )"2" "0" )"2" assert )nil nil ))nil ))nil ))nil )"6" "6" nil nil ))nil )"7" "7" nil nil ))nil ))nil )"4" "4" expand "abs" )"4" nil nil ))nil ))nil )"5" "5" case "x!1=0" )"1" "1/2" )"1" assert )nil nil ))nil )"2" "0" )"2" assert )nil nil ))nil ))nil ))nil )"6" "6" nil nil ))nil ))nil )"2" replace -1)"2" rewrite "asin_1" )"2" "pi_bnds" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (case "px!1 < sqrt(6)" )"1" (typepred "px!1" )"1" (expand "abs" -1)"1" "identity_derivable_fun[{x:nnreal| x <= 1}]" )"1" (lemma "deriv_id_fun[{x:nnreal| x <= 1}]" )"1" (expand "I" )"1" "const_derivable_fun[{x:nnreal| x <= 1}]" "b" "1" ))"1" "deriv_const_fun[{x:nnreal| x <= 1}]" "b" "1" ))"1" (expand "const_fun" )"1" "prod_derivable_fun" "f1" "LAMBDA (x: {x: nnreal | x <= 1}): x" "f2" "LAMBDA (x: {x: nnreal | x <= 1}): x" ))"1" assert )"1" expand "*" -1)"1" "deriv_prod_fun" "ff1" "LAMBDA (x: {x: nnreal | x <= 1}): x" "ff2" "LAMBDA (x: {x: nnreal | x <= 1}): x" ))"1" replace -5 -1)"1" expand "*" )"1" expand "+" )"1" "scal_derivable_fun" "f" "LAMBDA (x_1: {x: nnreal | x <= 1}): x_1 * x_1" "b" "1/6" ))"1" assert )"1" expand "*" )"1" "deriv_scal_fun" "ff" "LAMBDA (x_1: {x: nnreal | x <= 1}): x_1 * x_1" "b" "1/6" ))"1" replace -3 -1)"1" expand "*" "1" "diff_derivable_fun" "f1" "LAMBDA (x: {x: nnreal | x <= 1}): 1" "f2" "LAMBDA (x: {x: nnreal | x <= 1}): 1 / 6 * (x * x)" ))"1" assert )"1" expand "-" )"1" "deriv_diff_fun" "ff1" "LAMBDA (x: {x: nnreal | x <= 1}): 1" "ff2" "LAMBDA (x: {x: nnreal | x <= 1}): 1 / 6 * (x * x)" ))"1" replace "1" replace "1" expand "-" )"1" "prod_derivable_fun" "f1" "LAMBDA (x: {x: nnreal | x <= 1}): x" "f2" "LAMBDA (x_1: {x: nnreal | x <= 1}): 1 - 1 / 6 * (x_1 * x_1)" ))"1" assert )"1" expand "*" )"1" "deriv_prod_fun" "ff1" "LAMBDA (x: {x: nnreal | x <= 1}): x" "ff2" "LAMBDA (x_1: {x: nnreal | x <= 1}): 1 - 1 / 6 * (x_1 * x_1)" ))"1" replace "1" replace "1" expand "*" )"1" expand "+" )"1" "asin_derivable2" )"1" "deriv_asin_fun" )"1" "composition_derivable_fun[{x: nnreal | x <= 1},real_abs_lt1]" "f" "LAMBDA (x_1: {x: nnreal | x <= 1}): x_1 - x_1 * x_1 * x_1 * (1 / 6)" "g" "LAMBDA (x: real_abs_lt1): asin(x)" ))"1" assert )"1" expand "o" )"1" "deriv_comp_fun[{x: nnreal | x <= 1},real_abs_lt1]" "ff" "LAMBDA (x_1: {x: nnreal | x <= 1}): x_1 - x_1 * x_1 * x_1 * (1 / 6)" "gg" "LAMBDA (x: real_abs_lt1): asin(x)" ))"1" replace "1" replace "1" expand "o" )"1" expand "*" )"1" "diff_derivable_fun" "f1" "LAMBDA (x: {x: nnreal | x <= 1}): x" "f2" "LAMBDA (x_1: {x: nnreal | x <= 1}): asin(x_1 - x_1 * x_1 * x_1 * (1 / 6))" ))"1" expand "-" )"1" assert )"1" "deriv_diff_fun" "ff1" "LAMBDA (x: {x: nnreal | x <= 1}): x" "ff2" "LAMBDA (x_1: {x: nnreal | x <= 1}): asin(x_1 - x_1 * x_1 * x_1 * (1 / 6))" ))"1" replace "1" replace "1" expand "-" )"1" "minimum_derivative[{x: nnreal | x <= 1}]" "g" "LAMBDA (x_1: {x: nnreal | x <= 1}): x_1 - asin(x_1 - x_1 * x_1 * x_1 * (1 / 6))" "x" "0" "y1" "px!1" ))"1" "1" "1" assert )"1" rewrite "asin_0" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" replace "2" "2" rewrite "sq_0" )"2" rewrite "sqrt_1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" assert )nil nil )"4" replace "4" "4" "4" "y!1" )"4" expand ">=" "4" expand "<=" "4" "1" "1" "AP" "y!1 - y!1 * y!1 * y!1 * (1 / 6)" )"1" replace "1" "sq_le" "nna" "y!1" "nnb" "1" ))"1" expand "sq" "1" "posreal_times_posreal_is_posreal" "px" "y!1" "py" "1-y!1 * y!1 / 6" ))"1" expand "<=" "1" "1" "sq_lt" "nna" "y!1" "nnb" "1" ))"1" rewrite "sq_rew" )"1" rewrite "sq_1" )"1" "1" replace "1" "1" "1" "lt_times_lt_pos1" "px" "y!1" "y" "1" "nnz" "1 - sq(y!1) / 6" "w" "1" ))"1" "1" replace "1" "sq_lt" "nna" "AP" "nnb" "1" ))"1" expand "sq" "1" assert )"1" rewrite "sq_rew" "1" "sq_lt" "nna" "0" "nnb" "AP" ))"1" rewrite "sq_0" )"1" assert )"1" case "1-sq(AP) > 0" )"1" "sqrt_lt" "nny" "0" "nnz" "1-sq(AP)" ))"1" rewrite "sqrt_0" )"1" "1" expand ">" "1" replace "1" "1" "posreal_times_posreal_is_posreal" "px" "(sq(y!1)/2-1)/sqrt(1 - sq(AP))+1" "py" "y!1" ))"1" assert )nil nil )"2" "2" case "1-sq(y!1)/2 > 0" )"1" "div_mult_pos_lt1" "x" "1" "z" "1 - sq(y!1) / 2" "py" "sqrt(1 - sq(AP))" ))"1" "sq_lt" "nna" "1 - sq(y!1) / 2" "nnb" "sqrt(1 - sq(AP))" ))"1" rewrite "sq_sqrt" "1" case "sq(1 - sq(y!1) / 2) < 1 - sq(AP)" )"1" assert )nil nil )"2" "2" expand "AP" "2" expand "sq" "2" "2" expand "sq" "2" "div_cancel1" "x" "y!1*y!1" "n0z" "2" ))"2" replace "2" "both_sides_minus_lt1" "x" "1 + y!1 * y!1 / 2 * (y!1 * y!1 / 2) - y!1 * y!1" "y" "1 - (1 / 6) * (1 / 6) * y!1 * y!1 * y!1 * y!1 * y!1 * y!1 - " "z" "1-y!1*y!1" ))"2" replace "2" "2" "2" "both_sides_times_pos_lt1" "x" "1/4" "y" "1/3-y!1*y!1/36" "pz" "y!1 * y!1 * y!1 * y!1" ))"1" replace "1" "1" case "y!1 * y!1 / 36 < 1/12" )"1" assert )nil nil )"2" "2" expand "sq" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "sq_lt" "nna" "0" "nnb" "sq(y!1)" ))"2" rewrite "sq_0" )"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 )"2" "2" assert )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" assert )nil nil )"3" "3" assert )"3" "sq_lt" "nna" "0" "nnb" "y!1" ))"3" rewrite "sq_0" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "sq_lt" "nna" "0" "nnb" "y!1" ))"2" rewrite "sq_0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" replace "2" "2" "2" expand "sq" )"2" assert )"2" "K1" "2 * (1 / 6) - (1 / 6) * (1 / 6)" )"2" "div_mult_pos_gt1" "x" "1" "z" "1/2" "py" "sqrt(K1)" ))"1" rewrite "div_div2" "1" assert )"1" "sq_gt" "nna" "sqrt(K1)" "nnb" "1/2" ))"1" rewrite "sq_sqrt" "1" expand "sq" "1" expand "K1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "sqrt_lt" "nny" "0" "nnz" "2 * (1 / 6) - (1 / 6) * (1 / 6)" ))"2" rewrite "sqrt_0" )"2" expand "K1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" expand "K1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "posreal_times_posreal_is_posreal" "px" "y!1" "py" "y!1" ))"1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"3" 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 ))nil ))nil ))nil )"2" "2" "2" "x!1" )"2" expand ">=" )"2" expand "<=" "2" "1" "posreal_times_posreal_is_posreal" "px" "x!1" "py" "x!1" ))"1" "posreal_times_posreal_is_posreal" "px" "x!1" "py" "x!1*x!1" ))"1" "posreal_div_posreal_is_posreal" "px" "x!1*x!1*x!1" "py" "6" ))"1" "lt_minus_lt1" "x" "x!1" "y" "1" "w" "0" "z" "x!1 * x!1 * x!1 / 6" ))"1" "1" expand "abs" "1" "sq_le" "nna" "x!1" "nnb" "1" ))"1" expand "sq" )"1" "posreal_times_posreal_is_posreal" "px" "1-x!1*x!1/6" "py" "x!1" ))"1" assert )nil nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil )"2" nil nil ))nil )"2" assert )nil nil ))nil )"2" replace "2" expand "abs" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!1" )"2" expand ">=" )"2" expand "<=" "2" "1" "posreal_times_posreal_is_posreal" "px" "1-x!1*x!1/6" "py" "x!1" ))"1" expand "abs" )"1" assert )nil nil ))nil )"2" assert )nil nil )"3" "3" "sq_le" "nna" "x!1" "nnb" "1" ))"3" expand "sq" )"3" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace "2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" case "x!1 = 0" )"1" "1/2" )"1" assert )nil nil )"2" expand "abs" )"2" assert )nil nil ))nil ))nil )"2" "0" )"1" assert )nil nil )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"4" "4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp*)"2" (case "x!1=0" )"1" (inst + "1" ) (("1" (assert ) nil nil ))nil )"2" (inst + "0" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1) (("3" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "sq_le" ("nnb" "px!1" "nna" "sqrt(6)" ))"2" (flatten)"2" (rewrite "sq_sqrt" )"2" (assert )"2" (hide -1)"2" (typepred "px!1" )"2" (expand "abs" )"2" assert )"2" "sq_le" "nna" "px!1" "nnb" "1" ))"2" rewrite "sq_1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sq "reals/" )nil sq "reals/" )nil sqrt "reals/" )nil sqrt "reals/" )nil sq "reals/" )nil sq "reals/" )"nonneg_real" sq "reals/" )nil sq "reals/" )nil sqrt "reals/" )nil sq "reals/" )"{nnz: nnreal | nnz * nnz = nnx}" sqrt"reals/" )nil sqrt "reals/" )nil sqrt "reals/" )nil atan nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.349 Sekunden
(vorverarbeitet am 2026-04-26)
¤ *© Formatika GbR, Deutschland
2026-05-26
