(hyperbolicnil 3253390561"" (skosimp*)"" (lemma "trichotomy" ("x" "x!1" ))"" (lemma "exp_diff" ("x" "0" "y" "x!1" ))"" (rewrite "exp_0" )"" (replace -1 1)"" (lemma "div_mult_pos_ge1" )"" (inst - "2" "1" "exp(x!1) + 1 / exp(x!1)" )"" (replace -1 1)"" (split -3)"1" (lemma "exp_strict_increasing" )"1" (expand "strict_increasing?" )"1" (inst - "0" "x!1" )"1" (rewrite "exp_0" )"1" (assert )"1" "sq_lt" "nnb" "exp(x!1)-1" "nna" "0" ))"1" expand "sq" )"1" "div_mult_pos_lt1" "z" "-1" "py" "exp(x!1)" "x" "exp(x!1)-2" ))"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1)"2" (rewrite "exp_0" ) (("2" (assert ) nil nil ))nil ))nil )"3" (lemma "exp_strict_increasing" )"3" (expand "strict_increasing?" )"3" (inst - "x!1" "0" )"3" (rewrite "exp_0" )"3" (assert )"3" "sq_lt" "nna" "0" "nnb" "1-exp(x!1)" ))"3" expand "sq" )"3" "div_mult_pos_lt1" "py" "exp(x!1)" "z" "-1" "x" "exp(x!1)-2" ))"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_axioms nil )nil ln_exp nil )"odd_int" integers nil )"posreal" nil )nil real_props nil )"posrat" nil )"posrat" nil )nil ln_exp nil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"nonneg_real" sq "reals/" )"nzreal" nil )"real" reals nil )"real" reals nil )"[numfield -> numfield]" number_fields nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil sq "reals/" )"posreal" nil )"bool" real_fun_preds "reals/" )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"{py | x = ln(py)}" ln_exp nil )"real" ln_exp nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil ln_exp nil ))nil 3253429443"" (skosimp*)"" (typepred "cosh(x!1)" ) (("" (assert ) nil nil )) nil )) nil )"posreal_ge1" hyperbolic nil )nil hyperbolic 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 3253429443"" (skosimp*)"" (lemma "div_mult_pos_lt1" )"" (inst - "cosh(x!1)" "1" "sinh(x!1)" )"1" (lemma "div_mult_pos_lt2" )"1" (inst - "cosh(x!1)" "-1" "sinh(x!1)" )"1" (replace -1)"1" (replace -2)"1" (hide (-1 -2))"1" (expand "cosh" )"1" (expand "sinh" )"1" (typepred "exp(x!1)" )"1" (typepred "exp(-x!1)" )"1" (name-replace "EPX" "exp(x!1)" )"1" (name-replace "EMX" "exp(-x!1)" )"1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "cosh(x!1)" ) (("2" (assert ) nil nil )) nil ))nil ))nil )"2" (typepred "cosh(x!1)" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )nil real_props nil )nil real_props nil )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"posreal" nil )"nzreal" nil )"{py | x = ln(py)}" ln_exp nil )"real" ln_exp nil )"[T, T -> boolean]" equalities nil )NOT const-decl "[bool -> bool]" booleans nil )"posreal" nil )"posreal" nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"odd_int" integers nil )"real" hyperbolic nil )nil real_types nil )nil real_types nil )nil booleans nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil hyperbolic nil )"posreal_ge1" hyperbolic nil )"real" hyperbolic nil )"bool" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3253429443"" (skosimp*)"" (expand "sinh" )"" (lemma "exp_diff" ("x" "0" "y" "n0x!1" ))"" (lemma "exp_0" )"" (replace -1 -2)"" (replace -2 -3)"" (rewrite "div_cancel3" -3)"" "minus_div1" "x" "exp(n0x!1)" "y" "1" "n0x" "1" "n0y" "exp(n0x!1)" ))"" (replace -1 -4)"" (rewrite "div_cancel3" -4)"" (lemma "exp_strict_increasing" )"" (expand "strict_increasing?" )"" (lemma "trichotomy" ("x" "2*n0x!1" ))"" "exp_sum" "x" "n0x!1" "y" "n0x!1" ))"" replace -1 -7 rl)"" "1" "0" "2*n0x!1" )"1" (assert ) nil nil ))nil )"2" (assert ) nil nil )"3" "n0x!1" "0" )"3" replace -2)"3" "3" assert )"3" replace -6)"3" assert )"3" "3" "3" assert )"3" replace -3 * rl)"3" "3" "exp_neg" )"3" "3" 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 )"real" hyperbolic nil )nil ln_exp nil )"real" reals nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" nil )"nnreal" nil )"odd_int" integers nil )"posint" nil )"bool" real_fun_preds "reals/" )nil ln_exp nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )"[numfield, numfield -> numfield]" number_fields nil )"[bool, bool -> bool]" booleans nil )"posreal" nil )nil ln_exp nil )nil real_props nil )"nzreal" real_typesnil )nil real_axioms nil )"nzreal" nil )nil ln_exp nil )"posreal" nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"{py | x = ln(py)}" ln_exp nil )"real" ln_exp nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )nil real_props nil )"odd_int" integers nil )nil ln_exp 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 3253429443"" (skosimp*)"" (typepred "cosh(x!1)" )"" "both_sides_div_pos_ge2" "py" "cosh(x!1)" "px" "1" "pz" "1" ))"1" "posreal_div_posreal_is_posreal" "px" "1" "py" "cosh(x!1)" ))"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil )"posreal_ge1" hyperbolic nil )nil hyperbolic nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil real_types nil )"nzreal" nil )"posrat" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil real_props nil )nil real_types nil )"bool" reals nil )nil real_types nil ))nil 3253429443"" (skosimp*)"" (expand "tanh" )"" (expand "sinh" )"" (lemma "exp_diff" ("x" "0" "y" "n0x!1" ))"" (lemma "exp_0" )"" (replace -1 -2)"" (replace -2 -3)"" (rewrite "div_div2" -3)"" "minus_div1" "x" "exp(n0x!1)" "n0x" "1" "y" "1" "n0y" "exp(n0x!1)" ))"" (replace -1 -4)"" (rewrite "div_div2" -4)"" "exp_sum" ("x" "n0x!1" "y" "n0x!1" ))"" (replace -1 -5 rl)"" (hide -1 -2 -4)"" "exp_strict_increasing" )"" expand "strict_increasing?" )"" "trichotomy" "x" "2*n0x!1" ))"" "1" "0" "2*n0x!1" )"1" (assert ) nil nil ))nil )"2" (assert ) nil nil )"3" "2*n0x!1" "0" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real_abs_lt1" hyperbolic nil )nil reals nil )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil ln_exp nil )"odd_int" integers nil )nil real_props nil )nil reals nil )nil booleans nil )"bool" reals nil )nil hyperbolic nil )"posreal_ge1" hyperbolic nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"real" ln_exp nil )"{py | x = ln(py)}" ln_exp nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" reals nil )"posreal" nil )nil ln_exp nil )"bool" real_fun_preds "reals/" )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil real_axioms nil )"nzreal" nil )nil ln_exp nil )"posint" nil )"odd_int" integers nil )"(divides(n))" divides nil )"posreal" nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"real" reals nil )"real" reals nil )nil ln_exp nil )"real" hyperbolic nil ))nil 3253429443"" (skosimp*)"" (typepred "tanh(n0x!1)" )"" (lemma "coth_TCC1" ("nzx" "n0x!1" ))"" (lemma "trichotomy" ("x" "n0x!1" ))"" (case "strict_increasing?(sinh)" )"1" (expand "strict_increasing?" )"1" (case "sinh(0)=0" )"1" (expand "tanh" )"1" (typepred "cosh(n0x!1)" )"1" (split -4)"1" (inst - "0" "n0x!1" )"1" (rewrite "div_div1" )"1" (assert )"1" (replace -3 -4)"1" "div_mult_pos_lt1" )"1" "sinh(n0x!1)" "-1" "cosh(n0x!1)" )"1" "div_mult_pos_lt2" )"1" "sinh(n0x!1)" "1" "cosh(n0x!1)" )"1" replace -1)"1" replace -2)"1" "1" expand "cosh" )"1" expand "sinh" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (inst - "n0x!1" "0" )"3" (replace -3 -4)"3" (assert )"3" (lemma "div_mult_neg_lt1" )"3" rewrite "div_div1" )"3" "sinh(n0x!1)" "-1" "cosh(n0x!1)" )"3" "div_mult_neg_lt2" )"3" "sinh(n0x!1)" "1" "cosh(n0x!1)" )"3" replace -1)"3" replace -2)"3" "3" expand "sinh" )"3" expand "cosh" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "sinh" 1)"2" (rewrite "exp_0" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (lemma "exp_strict_increasing" )"2" (expand "strict_increasing?" )"2" (expand "sinh" )"2" (skosimp*)"2" (inst-cp - "x!1" "y!1" )"2" (inst - "-y!1" "-x!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )"boolean" notequal nil )"real_abs_lt1" hyperbolic nil )nil hyperbolic nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" real_fun_preds "reals/" )"real" hyperbolic nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )nil hyperbolic nil )"posreal_ge1" hyperbolic nil )nil real_props nil )"bool" reals nil )nil real_types nil )nil real_types nil )"(total_order?[real])" nil )nil real_props nil )nil real_props nil )nil real_props nil )"posreal" nil )"posreal" nil )"nzreal" real_typesnil )"real" reals nil )"even_int" integers nil )nil ln_exp nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" reals nil )"nzreal" nil )"real" reals nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil reals nil )"rat" rationals nil )"even_int" integersnil )nil ln_exp nil )"real" reals nil )nil real_axioms nil ))nil 3253435075"" (skosimp*)"" (expand "csch" )"" "div_mult_pos_lt2" ("z" "1" "x" "0" "py" "sinh(px!1)" ))"1" (assert ) nil nil )"2" (hide 2)"2" (expand "sinh" )"2" (lemma "exp_diff" ("x" "0" "y" "px!1" ))"2" (rewrite "exp_0" )"2" (rewrite -1)"2" (lemma "div_mult_pos_lt2" )"2" (inst - "2" "0" "exp(px!1)-1/exp(px!1)" )"2" "minus_div1" "x" "exp(px!1)" "n0x" "1" "y" "1" "n0y" "exp(px!1)" ))"2" (lemma "exp_strict_increasing" )"2" (expand "strict_increasing?" )"2" (inst - "0" "2*px!1" )"2" rewrite "exp_0" )"2" "exp_sum" "x" "px!1" "y" "px!1" ))"2" replace -1 -3 rl)"2" expand ">=" 1)"2" expand ">" 1)"2" expand "<=" 1)"2" assert )"2" replace -4 1)"2" replace -3 1)"2" "posreal_div_posreal_is_posreal" "px" "exp(2*px!1)-1" "py" "exp(px!1)" ))"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 )"real" hyperbolic nil )nil ln_exp nil )"posreal" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"{py | x = ln(py)}" ln_exp nil )"real" ln_exp nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil ln_exp nil )"posreal" nil )"[numfield, numfield -> numfield]" number_fields nil )nil ln_exp nil )"bool" reals nil )nil real_types nil )"posreal" nil )"real" reals nil )"nonneg_int" nil )"even_int" integersnil )"(divides(m))" divides nil )"(divides(n))" divides nil )"odd_int" integers nil )"posint" nil )"bool" real_fun_preds "reals/" )nil reals nil )nil real_props nil )"odd_int" integers nil )nil ln_exp nil )"real" reals nil )"real" reals nil )"nzreal" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil real_props nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" hyperbolic nil ))nil 3253435075"" (expand "coth" )"" (skosimp*)"" (typepred "tanh(px!1)" )"" (case "strict_increasing?(tanh)" )"1" (expand "strict_increasing?" )"1" (inst - "0" "px!1" )"1" (assert )"1" (expand "tanh" -1 1)"1" (expand "sinh" -1 1)"1" (expand "cosh" -1 1)"1" (rewrite "exp_0" )"1" (rewrite "div_div2" )"1" (grind-reals)"1" (cross-mult 1) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "strict_increasing?" )"2" (skosimp*)"2" (expand "tanh" )"2" (rewrite "div_mult_pos_lt1" 1)"2" "div_mult_pos_lt2" "z" "sinh(y!1)*cosh(x!1)" "py" "cosh(y!1)" "x" "sinh(x!1)" ))"2" (replace -1)"2" (hide -1)"2" (expand "sinh" )"2" (expand "cosh" )"2" assert )"2" "both_sides_times_pos_lt1" "pz" "4" "x" "(exp(x!1) - exp(-x!1)) / 2 * ((exp(-y!1) + exp(y!1)) / 2)" "y" "(exp(y!1) - exp(-y!1)) / 2 * ((exp(-x!1) + exp(x!1)) / 2)" ))"2" replace -1 1 rl)"2" "2" "(exp(x!1) - exp(-x!1)) / 2 * ((exp(-y!1) + exp(y!1)) / 2) * 4 = (exp(x!1) - exp(-x!1))*(exp(-y!1) + exp(y!1))" )"1" "(exp(y!1) - exp(-y!1)) / 2 * ((exp(-x!1) + exp(x!1)) / 2) * 4 = (exp(y!1) - exp(-y!1))*(exp(-x!1) + exp(x!1))" )"1" "1" assert )"1" "K1" "-1 * (exp(-x!1) * exp(-y!1))" )"1" "K2" "exp(x!1) * exp(y!1)" )"1" "exp_sum" "x" "-x!1" "y" "y!1" ))"1" replace -1 1 rl)"1" "exp_sum" "x" "-y!1" "y" "x!1" ))"1" replace "1" "K1 - exp(-x!1 + y!1) + (exp(-y!1 + x!1) + K2) < ") "1" "1" "exp_strict_increasing" )"1" expand "strict_increasing?" )"1" "x!1-y!1" "y!1-x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "both_sides_times_pos_lt1" "x" "exp(-y!1 + x!1)" "y" "exp(-x!1 + y!1)" "pz" "2" ))"2" replace "2" assert )"2" "K3" "exp(-y!1 + x!1)" )"2" "K4" "exp(-x!1 + y!1)" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "EXPX" "(exp(-x!1) + exp(x!1))" )"2" "EXPY" "(exp(y!1)-exp(-y!1))" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "EXPY" "(exp(-y!1)+exp(y!1))" )"2" "EXPX" "(exp(x!1)-exp(-x!1))" )"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 )"bool" real_fun_preds "reals/" )"posreal_ge1" hyperbolic nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )"boolean" notequal nil )nil real_props nil )"even_int" integersnil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )"rat" rationals nil )nil extra_real_props nil )"real" reals nil )"(total_order?[real])" nil )"posreal" nil )"real" reals nil )"posreal" nil )"real" reals nil )nil ln_exp nil )"real" hyperbolic nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"[T, T -> boolean]" equalities nil )"real" ln_exp nil )"{py | x = ln(py)}" ln_exp nil )"[numfield, numfield -> numfield]" number_fields nil )"nzreal" nil )"posreal" nil )"real" reals nil )nil ln_exp nil )"[bool, bool -> bool]" booleans nil )nil ln_exp nil )nil reals nil )"real" reals nil )nil real_props nil )nil hyperbolic nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )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 )"bool" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil hyperbolic nil )"real_abs_lt1" hyperbolic nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real_abs_gt1" hyperbolic nil ))nil 3253386551"" (expand "strict_increasing?" )"" (expand "sinh" )"" (skosimp*)"" "both_sides_div_pos_lt1" "x" "exp(x!1)-exp(-x!1)" "y" "exp(y!1)-exp(-y!1)" "pz" "2" ))"" (lemma "exp_strict_increasing" )"" (expand "strict_increasing?" )"" (inst-cp - "x!1" "y!1" )"" (inst - "-y!1" "-x!1" )"" (name-replace "EPX" "exp(x!1)" )"" (name-replace "EMX" "exp(-x!1)" )"" (name-replace "EMY" "exp(-y!1)" )"" (name-replace "EPY" "exp(y!1)" )"" "both_sides_times_neg_lt1" "x" "y!1" "y" "x!1" "nz" "-1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" hyperbolic nil )"[numfield -> numfield]" number_fields nil )"{py | x = ln(py)}" ln_exp nil )"real" ln_exp nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )"real" reals nil )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_props nil )"odd_int" integers nil )nil ln_exp nil )"bool" real_fun_preds "reals/" ))nil 3253395203"" (expand "strict_increasing?" )"" (skosimp*)"" (typepred "x!1" )"" (typepred "y!1" )"" (expand "nnreal_cosh" )"" (expand "cosh" )"" "both_sides_div_pos_lt1" "x" "exp(-x!1) + exp(x!1)" "y" "exp(-y!1) + exp(y!1)" "pz" "2" ))"" (replace -1 1)"" (lemma "exp_diff" ("x" "0" "y" "x!1" ))"" (rewrite "exp_0" )"" (replace -1 1)"" (lemma "exp_diff" ("x" "0" "y" "y!1" ))"" (rewrite "exp_0" )"" (replace -1 1)"" "both_sides_times_pos_lt1" "x" "1/exp(x!1)+exp(x!1)" "y" "1/exp(y!1)+exp(y!1)" "pz" "exp(x!1)*exp(y!1)" ))"" replace -1 1 rl)"" "" "div_cancel1" )"" "exp(x!1)" "1" )"" "exp(y!1)" "1" )"" "exp_strict_increasing" )"" expand "strict_increasing?" )"" "x!1" "y!1" )"" assert )"" "exp_increasing" )"" expand "increasing?" )"" "0" "x!1" )"" assert )"" rewrite "exp_0" )"" "EPX" "exp(x!1)" )"" "EPY" "exp(y!1)" )"" "" "posreal_times_posreal_is_posreal" "px" "EPX*EPY-1" "py" "EPY-EPX" ))"1" assert )nil nil )"2" assert )nil nil )"3" "lt_times_lt_pos1" )"3" "1" "1" "EPY" "EPX" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal_ge1" hyperbolic nil )nil ln_exp nil )"odd_int" integers nil )nil real_props nil )"(total_order?[real])" nil )"real" reals nil )"bool" real_fun_preds "reals/" )"(total_order?[real])" nil )"real" reals nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_props nil )nil ln_exp nil )nil ln_exp nil )nil reals nil )"(strict_total_order?[real])" real_props nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"posreal" nil )"posreal" nil )nil ln_exp nil )"real" reals nil )"posreal" nil )nil real_props nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"real" ln_exp nil )"{py | x = ln(py)}" ln_exp nil )"[numfield -> numfield]" number_fields nil )"posreal_ge1" hyperbolic nil )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 )"bool" reals nil )nil real_types nil )"bool" real_fun_preds "reals/" ))nil 3253525103"" (lemma "exp_strict_increasing" )"" (expand "strict_increasing?" )"" (expand "tanh" )"" (expand "sinh" )"" (expand "cosh" )"" (skosimp*)"" (rewrite "div_div1" 1)"" (rewrite "div_div1" 1)"" (rewrite "div_cancel1" 1)"" (rewrite "div_cancel1" 1)"" (case "exp(-x!1)+exp(x!1) > 0" )"1" (case "exp(-y!1)+exp(y!1) > 0" )"1" (lemma "div_mult_pos_lt1" )"1" "exp(-x!1) + exp(x!1)" "(exp(y!1) - exp(-y!1)) / (exp(-y!1) + exp(y!1))" "exp(x!1) - exp(-x!1)" )"1" replace -1 1)"1" "div_mult_pos_lt2" )"1" "exp(-y!1) + exp(y!1)" "exp(x!1) - exp(-x!1)" "(exp(y!1) - exp(-y!1))*(exp(-x!1) + exp(x!1))" )"1" replace -1 1)"1" "1" "x!1" "y!1" )"1" "-y!1" "-x!1" )"1" "x!1-y!1" "y!1-x!1" )"1" "exp_sum" )"1" "x!1" "-y!1" )"1" "y!1" "-x!1" )"1" 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 )"bool" real_fun_preds "reals/" )"real" reals nil )"real" reals nil )"real" hyperbolic nil )nil real_props nil )"nzreal" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"real" reals nil )nil ln_exp nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )nil real_props nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{py | x = ln(py)}" ln_exp nil )"real" ln_exp nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )"real" reals nil )"posreal_ge1" hyperbolic nil )"posreal" nil )"posreal" nil )"real_abs_lt1" hyperbolic nil )nil ln_exp nil ))nil 3253526140"" (lemma "sinh_strict_increasing" )"" (expand "strict_decreasing?" )"" (skosimp*)"" (typepred "x!1" )"" (expand "strict_increasing?" )"" (expand "posreal_csch" )"" (expand "csch" )"" (inst-cp - "x!1" "y!1" )"" (inst - "0" "x!1" )"" (name-replace "SX" "sinh(x!1)" )"" (name-replace "SY" "sinh(y!1)" )"" (expand "sinh" )"" (rewrite "exp_0" )"" (assert )"" "both_sides_div_pos_lt2" "pz" "1" "py" "SX" "px" "SY" ))"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" real_fun_preds "reals/" )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"posreal" hyperbolic nil )"real" hyperbolic nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"nzreal" nil )"even_int" integersnil )"rat" rationals nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_props nil )"odd_int" integers nil )nil ln_exp nil )"real" hyperbolic nil )"bool" real_fun_preds "reals/" )nil hyperbolic nil ))nil 3253526566"" (expand "strict_decreasing?" )"" (skosimp*)"" (typepred "x!1" )"" (expand "nnreal_sech" )"" (expand "sech" )"" (lemma "cosh_strict_increasing" )"" (expand "strict_increasing?" )"" (inst - "x!1" "y!1" )"" (expand "nnreal_cosh" )"" "both_sides_div_pos_lt2" "pz" "1" "py" "cosh(x!1)" "px" "cosh(y!1)" ))"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal_le1" hyperbolic nil )nil hyperbolic nil )nil real_props nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil hyperbolic nil )"posreal_ge1" hyperbolic nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"posreal_ge1" hyperbolic nil )"bool" real_fun_preds "reals/" )"posreal_le1" hyperbolic nil )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 )"bool" reals nil )nil real_types nil )"bool" real_fun_preds "reals/" ))nil 3253526884"" (expand "strict_decreasing?" )"" (skosimp*)"" (expand "posreal_coth" )"" (expand "coth" )"" (lemma "tanh_strict_increasing" )"" (expand "strict_increasing?" )"" (inst-cp - "0" "x!1" )"" (inst - "x!1" "y!1" )"" (assert )"" (name-replace "TX" "tanh(x!1)" )"" (name-replace "TY" "tanh(y!1)" )"" (expand "tanh" )"" (expand "cosh" )"" (expand "sinh" )"" rewrite "exp_0" )"" "both_sides_div_pos_lt2" "pz" "1" "py" "TX" "px" "TY" ))"1" (assert ) nil nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real_abs_gt1" hyperbolic nil )"bool" real_fun_preds "reals/" )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil hyperbolic nil )"real_abs_lt1" hyperbolic nil )"real" hyperbolic nil )nil real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"rat" rationals nil )"even_int" integersnil )"odd_int" integers nil )"posreal" nil )"real" reals nil )"posreal" nil )"real" reals nil )nil ln_exp nil )"posreal_ge1" hyperbolic nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil )"posreal_gt1" hyperbolic nil )"bool" real_fun_preds "reals/" ))nil 3253386258"" (expand "sinh" )"" (rewrite "exp_0" ) (("" (assert ) nil nil )) nil )) nil )nil ln_exp nil )"real" reals nil )"odd_int" integers nil )"rat" rationals nil )"even_int" integersnil )"real" hyperbolic nil ))nil 3253386284"" (expand "cosh" ) (("" (rewrite "exp_0" ) nil nil )) nil )"posreal" nil )nil ln_exp nil )"posreal_ge1" hyperbolic nil ))nil 3253452832"" (expand "tanh" )"" (rewrite "sinh_0" ) (("" (assert ) nil nil )) nil )) nil )nil hyperbolic nil )"real" reals nil )"real_abs_lt1" hyperbolic nil ))nil 3253452862"" (expand "sech" )"" (rewrite "cosh_0" ) (("" (assert ) nil nil )) nil )) nil )nil hyperbolic nil )"posreal_le1" hyperbolic nil ))nil 3253453151"" (skosimp*)"" (expand "cosh" )"" (expand "sinh" )"" (lemma "exp_sum" ("x" "x!1" "y" "-x!1" ))"" (rewrite "exp_0" -1)"" (name-replace "EPX" "exp(x!1)" )"" (name-replace "EMX" "exp(-x!1)" )"" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" nil )"posreal_ge1" hyperbolic nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil ln_exp nil )"real" reals nil )"{py | x = ln(py)}" ln_exp nil )"real" ln_exp nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"odd_int" integers nil )"nonneg_real" sq "reals/" )"real" reals nil )"real" reals nil )"posreal" nil )"posreal" nil )"posreal" sq "reals/" )nil ln_exp nil )"real" hyperbolic nil )"real" reals nil ))nil 3253453367"" (skosimp*)"" (expand "tanh" )"" (expand "sech" )"" (typepred "cosh(x!1)" )"" (lemma "cosh_sinh_one" ("x" "x!1" ))"" (lemma "sq_div" ("d" "cosh(x!1)" ))"" (inst-cp - "1" )"" (inst - "sinh(x!1)" )"" (assert )"" (replace -1)"" (replace -2)"" "both_sides_div1" "n0z" "sq(cosh(x!1))" "x" "sq(cosh(x!1)) - sq(sinh(x!1))" "y" "1" ))"" "minus_div2" "x" "sq(cosh(x!1))" "y" "sq(sinh(x!1))" "n0x" "sq(cosh(x!1))" ))"" (replace -2 -5 rl)"" rewrite "sq_1" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real_abs_lt1" hyperbolic nil )"posreal_ge1" hyperbolic nil )nil hyperbolic nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil sq "reals/" )"real" hyperbolic nil )nil real_props nil )"boolean" notequal nil )nil reals nil )nil real_types nil )"nonneg_real" sq "reals/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )nil real_props nil )nil sq "reals/" )"real" reals nil )"(total_order?[real])" nil )"posreal" nil )"posreal" sq "reals/" )"nzreal" nil )"real" reals nil )nil hyperbolic nil )"posreal_le1" hyperbolic nil ))nil 3253454037"" (expand "coth" )"" (expand "csch" )"" (skosimp*)"" (expand "tanh" )"" (case "sinh(n0x!1) /= 0" )"1" (rewrite "div_div1" )"1" (lemma "sq_div" ("d" "sinh(n0x!1)" ))"1" (replace -2 -1)"1" (inst-cp - "cosh(n0x!1)" )"1" (inst - "1" )"1" (rewrite "sq_1" )"1" (lemma "cosh_sinh_one" ("x" "n0x!1" ))"1" "both_sides_div1" "x" "sq(cosh(n0x!1)) - sq(sinh(n0x!1))" "y" "1" "n0z" "sq(sinh(n0x!1))" ))"1" "minus_div2" "n0x" "sq(sinh(n0x!1))" "x" "sq(cosh(n0x!1))" "y" "sq(sinh(n0x!1))" ))"1" rewrite "div_simp" -1)"1" (assert ) nil nil ))nil ))nil )"2" (lemma "sq_eq_0" ("a" "sinh(n0x!1)" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "sinh_strict_increasing" )"2" (expand "strict_increasing?" )"2" (lemma "sinh_0" )"2" (case "n0x!1>0" )"1" (inst - "0" "n0x!1" ) (("1" (assert ) nil nil ))nil )"2" (inst - "n0x!1" "0" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" hyperbolic nil )"real" reals nil )"real_abs_lt1" hyperbolic nil )nil hyperbolic nil )nil hyperbolic nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"bool" real_fun_preds "reals/" )nil real_props nil )nil reals nil )nil booleans nil )"bool" reals nil )nil hyperbolic nil )"posreal_ge1" hyperbolic nil )"real" reals nil )nil hyperbolic nil )nil real_props nil )"nzreal" nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nonneg_real" sq "reals/" )nil real_types nil )nil real_props nil )"real" reals nil )nil sq "reals/" )nil sq "reals/" )nil numbers nil )nil booleans nil )"boolean" notequal nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" hyperbolic nil )nil reals nil )"real_abs_gt1" hyperbolic nil )"posreal" sq "reals/" ))nil 3253453296"" (expand "cosh" )"" (expand "sinh" ) (("" (propax) nil nil )) nil )) nil )"real" reals nil )"real" reals nil )"real" hyperbolic nil )"posreal_ge1" hyperbolic nil )"posreal" nil )"posreal" nil ))nil 3253453312"" (expand "cosh" )"" (expand "sinh" ) (("" (propax) nil nil )) nil )) nil )"real" reals nil )"real" reals nil )"real" hyperbolic nil )"posreal_ge1" hyperbolic nil )"posreal" nil )"posreal" nil ))nil 3253452903"" (expand "sinh" ) (("" (propax) nil nil )) nil )"real" hyperbolic nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil 3253452917"" (expand "cosh" ) (("" (propax) nil nil )) nil )"posreal_ge1" hyperbolic nil )"posreal" nil )"real" reals nil ))nil 3253452927"" (expand "tanh" )"" (skosimp*)"" (rewrite "sinh_neg" )"" (rewrite "cosh_neg" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil hyperbolic nil )"real" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil )"real_abs_lt1" hyperbolic nil )"real" reals nil ))nil 3253452986"" (expand "csch" )"" (skosimp*)"" (rewrite "sinh_neg" ) (("" (assert ) nil nil )) nil )) nil ))nil )"nzreal" real_typesnil )"real" reals nil )nil reals nil )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil )"real" hyperbolic nil )"nzreal" nil ))nil 3253453063"" (skosimp*)"" (expand "sech" ) (("" (rewrite "cosh_neg" ) nil nil )) nil )) nil )"posreal_le1" hyperbolic nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil ))nil 3253453083"" (skosimp*)"" (expand "coth" )"" (rewrite "tanh_neg" ) (("" (assert ) nil nil )) nil )) nil ))nil )"real_abs_gt1" hyperbolic nil )"nzreal" real_typesnil )"real" reals nil )"nzreal" nil )nil reals nil )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil ))nil 3253474598"" (skosimp*)"" (expand "sinh" )"" (expand "cosh" )"" (lemma "exp_sum" ("x" "x!1" "y" "y!1" ))"" (lemma "exp_diff" ("x" "0" ))"" (rewrite "exp_0" )"" (inst-cp - "x!1+y!1" )"" (inst-cp - "y!1" )"" (inst - "x!1" )"" (replace -1)"" (replace -2)"" (replace -3)"" (lemma "exp_sum" ("x" "x!1" "y" "y!1" ))"" (replace -1 1)"" "EPX" "exp(x!1)" )"" "EPY" "exp(y!1)" )"" "" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" hyperbolic nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil ln_exp nil )nil ln_exp nil )"odd_int" integers nil )"real" reals nil )"posreal" nil )"[T, T -> boolean]" equalities nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" ln_exp nil )"{py | x = ln(py)}" ln_exp nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil ln_exp nil )"posreal_ge1" hyperbolic nil )"posreal" nil )"posreal" nil ))nil 3270964764"" (skosimp*)"" (lemma "sinh_sum" ("x" "x!1" "y" "-y!1" ))"" (rewrite "sinh_neg" )"" (rewrite "cosh_neg" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil )"real" reals nil )nil hyperbolic nil )"real" reals nil )"real" reals nil )"real" reals nil )nil hyperbolic nil ))nil 3253475454"" (skosimp*)"" (expand "cosh" )"" (expand "sinh" )"" (lemma "exp_diff" ("x" "0" ))"" (inst-cp - "x!1" )"" (inst-cp - "y!1" )"" (inst - "x!1+y!1" )"" (lemma "exp_sum" ("x" "x!1" "y" "y!1" ))"" (replace -1)"" (rewrite "exp_0" )"" (replace -2 1)"" (replace -3)"" (replace -4)"" (hide-all-but 1)"" "EPX" "exp(x!1)" )"" "EPY" "exp(y!1)" )"" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"posreal" nil )"posreal" nil )"posreal_ge1" hyperbolic nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil ln_exp nil )nil ln_exp nil )nil ln_exp nil )"odd_int" integers nil )"[T, T -> boolean]" equalities nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" ln_exp nil )"{py | x = ln(py)}" ln_exp nil )"posreal" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"real" hyperbolic nil )"real" reals nil )"real" reals nil ))nil 3270964814"" (skosimp*)"" (lemma "cosh_sum" ("x" "x!1" "y" "-y!1" ))"" (rewrite "sinh_neg" )"" (rewrite "cosh_neg" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil )"real" reals nil )nil hyperbolic nil )"real" reals nil )"real" reals nil )"real" reals nil )nil hyperbolic nil ))nil 3253471676"" (skosimp*)"" (typepred "tanh(x!1)" )"" (typepred "tanh(y!1)" )"" (name-replace "TX" "tanh(x!1)" )"" (name-replace "TY" "tanh(y!1)" )"" (lemma "abs_mult" ("x" "TX" "y" "TY" ))"" (case "TX=0" )"1" (assert ) nil nil )"2" (lemma "lt_times_lt_pos1" )"2" (inst - "abs(TY)" "abs(TX)" "1" "1" )"1" (split -1)"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (grind) nil nil ))nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real_abs_lt1" hyperbolic nil )nil hyperbolic nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"real" reals nil )nil real_props nil )nil real_props nil )"real" reals nil )"posint" nil )"odd_int" integers nil )"(divides(n))" divides nil )"(total_order?[real])" nil )nil real_types nil )"real_abs_lt1" hyperbolic nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil real_types nil )"bool" reals nil ) (> const-decl "bool" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil ))nil 3253577464"" (expand "tanh" )"" (skosimp*)"" (typepred "cosh(x!1)" )"" (typepred "cosh(y!1)" )"" (typepred "cosh(x!1+y!1)" )"" (rewrite "sinh_sum" )"" (rewrite "cosh_sum" )"" (name-replace "CX" "cosh(x!1)" )"" (name-replace "CY" "cosh(y!1)" )"" (name-replace "SY" "sinh(y!1)" )"" (name-replace "SX" "sinh(x!1)" )"" (lemma "add_div" )"" (inst-cp - "CX" "CY" "SX" "SY" )"1" (inst - "1" "CX*CY" "1" "SX*SY" )"1" "div_div1" )"1" "CX*CY + SX*SY" "CX*CY" "(SX*CY+SY*CX) / (CX * CY)" )"1" "div_cancel2" )"1" "CX*CY" "SX*CY+SY*CX" )"1" replace -1 -2)"1" replace -3 1)"1" replace -4 1)"1" "CXCY" "CX*CY" )"1" "SXSY" "SX*SY" )"1" "SYCX" "SY*CX" )"1" "SXCY" "SX*CY" )"1" "NUMER" "SYCX+SXCY" )"1" "DENOM" "CXCY+SXSY" )"1" replace "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "both_sides_times_pos_ge1" "pz" "CX" "x" "CY" "y" "1" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" "both_sides_times_pos_ge1" "pz" "CX" "x" "CY" "y" "1" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"3" (assert ) nil nil ))nil ))nil )"2" "both_sides_times_pos_ge1" "pz" "CX" "x" "CY" "y" "1" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil hyperbolic nil )"[T, T -> boolean]" equalities nil )"real" hyperbolic nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"posrat" nil )nil real_props nil )nil real_props nil )"boolean" notequal nil )nil reals nil )nil hyperbolic nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )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 )"bool" reals nil )nil hyperbolic nil )"posreal_ge1" hyperbolic nil )"real_abs_lt1" hyperbolic nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil 3253471683"" (skosimp*)"" (expand "coth" )"" (lemma "tanh_strict_increasing" )"" (expand "strict_increasing?" )"" (case "FORALL (nzx:nzreal): tanh(nzx) /= 0" )"1" (inst-cp - "n0x!1" )"1" (inst - "n0y!1" )"1" "both_sides_div2" "n0x" "tanh(n0x!1)" "n0y" "-tanh(n0y!1)" "n0z" "1" ))"1" (lemma "tanh_neg" ("x" "-n0x!1" ))"1" (replace -1 -2)"1" case "FORALL (x,y:real): tanh(x) = tanh(y) => x = y" )"1" (inst - "-n0x!1" "n0y!1" )"1" (assert ) nil nil )) nil )"2" (hide-all-but 1)"2" (skosimp*)"2" (lemma "tanh_strict_increasing" )"2" expand "strict_increasing?" )"2" "trich_lt" "x" "x!1" "y" "y!1" ))"2" "1" "x!1" "y!1" )"1" (assert ) nil nil ))nil )"2" (propax) nil nil )"3" "y!1" "x!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (propax) nil nil ))nil ))nil ))nil )"2" (skosimp*)"2" (hide -3 1)"2" (case "nzx!1>0" )"1" (inst - "0" "nzx!1" )"1" (rewrite "tanh_0" ) (("1" (assert ) nil nil ))nil ))nil )"2" (inst - "nzx!1" "0" )"2" (rewrite "tanh_0" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real_abs_gt1" hyperbolic nil )"bool" real_fun_preds "reals/" )"bool" reals nil )nil hyperbolic nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil real_props nil )nil reals nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"nzreal" nil )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )nil hyperbolic nil )"nzreal" real_typesnil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil )nil reals nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil hyperbolic nil )"real_abs_lt1" hyperbolic nil )nil hyperbolic nil ))nil 3253528669"" (skosimp*)"" (expand "coth" )"" (lemma "tanh_sum" ("x" "n0x!1" "y" "n0y!1" ))"" (case "FORALL (x:real): tanh(x) = 0 IFF x = 0" )"1" (inst-cp - "n0x!1" )"1" (inst-cp - "n0y!1" )"1" (inst - "n0x!1+n0y!1" )"1" (replace -1 1 rl)"1" (replace -4)"1" (typepred "tanh(n0x!1)" )"1" (typepred "tanh(n0y!1)" )"1" (name-replace "TX" "tanh(n0x!1)" )"1" (name-replace "TY" "tanh(n0y!1)" )"1" "abs_mult" ("x" "TX" "y" "TY" ))"1" "1" case "0 < abs(TX) & abs(TX) < 1 & 0 < abs(TY) & abs(TY) < 1" )"1" "1" "lt_times_lt_pos1" "px" "abs(TX)" "y" "1" "nnz" "abs(TY)" "w" "1" ))"1" expand "<=" -1)"1" replace -3 -1)"1" replace -5 -1)"1" case "1+TX*TY > 0" )"1" rewrite "div_div1" 2)"1" rewrite "div_times" "1" rewrite "add_div" "1" case "TX*TY /= 0" )"1" rewrite "div_div1" "1" "div_cancel2" "x" "1" "n0z" "TX*TY" ))"1" replace "1" assert )nil nil ))nil )"2" nil nil ))nil ))nil )"2" "2" expand "/=" )"2" "zero_times3" "x" "TX" "y" "TY" ))"2" replace "2" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp*)"2" (split)"1" (flatten)"1" (lemma "tanh_strict_increasing" )"1" (expand "strict_increasing?" )"1" (lemma "trichotomy" ("x" "x!1" ))"1" (lemma "tanh_0" )"1" (split -2)"1" (inst - "0" "x!1" )"1" (assert ) nil nil )) nil )"2" (propax) nil nil )"3" (inst - "x!1" "0" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (lemma "tanh_0" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nzreal" nil )"real_abs_gt1" hyperbolic nil )"real_abs_lt1" hyperbolic nil )nil hyperbolic nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"real" reals nil )nil real_props nil )"bool" reals nil )nil real_types nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil real_props nil )"bool" reals nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )nil reals nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )"odd_int" integers nil )"real" reals nil )"bool" reals nil )"nzreal" nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"bool" real_fun_preds "reals/" )nil hyperbolic nil )nil real_axioms nil )nil hyperbolic nil )nil hyperbolic 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 3270840661"" (skosimp*) (("" (assert ) nil nil )) nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil ))nil 3270838066"" (skosimp*)"" (assert )"" (lemma "trichotomy" ("x" "x!1" ))"" (split -1)"1" (lemma "sinh_strict_increasing" )"1" (expand "strict_increasing?" )"1" (inst - "0" "x!1/2" )"1" (rewrite "sinh_0" )"1" (assert )"1" "sq_eq" "nna" "sinh(x!1 / 2)" "nnb" "sqrt((cosh(x!1) - 1) / 2) ")) "1" (replace -1 1 rl)"1" (hide -1)"1" (rewrite "sq_sqrt" )"1" (expand "sinh" 1)"1" rewrite "sq_div" 1)"1" rewrite "sq_minus" 1)"1" "exp_sum" "x" "x!1/2" "y" "x!1/2" ))"1" "exp_sum" "x" "x!1/2" "y" "-x!1/2" ))"1" "exp_sum" "x" "-x!1/2" "y" "-x!1/2" ))"1" expand "sq" 1)"1" replace -1 1 rl)"1" replace -2 1 rl)"1" replace -3 1 rl)"1" rewrite "exp_0" 1)"1" expand "cosh" 1)"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1)"2" (rewrite "sinh_0" )"2" (rewrite "cosh_0" )"2" (rewrite "sqrt_0" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (lemma "sinh_strict_increasing" )"3" (expand "strict_increasing?" )"3" (inst - "x!1/2" "0" )"3" (rewrite "sinh_0" )"3" (assert )"3" "sq_eq" "nna" "-sinh(x!1/2)" "nnb" "sqrt((cosh(x!1) - 1) / 2)" ))"3" (assert )"3" (hide 2)"3" (rewrite "sq_sqrt" )"3" (expand "sinh" 1)"3" rewrite "sq_neg" 1)"3" rewrite "sq_div" 1)"3" rewrite "sq_minus" 1)"3" "exp_sum" "x" "x!1/2" "y" "x!1/2" ))"3" "exp_sum" "x" "x!1/2" "y" "-x!1/2" ))"3" "exp_sum" "x" "-x!1/2" "y" "-x!1/2" ))"3" expand "sq" 1)"3" expand "cosh" 1)"3" replace -1 1 rl)"3" replace -2 1 rl)"3" replace -3 1 rl)"3" rewrite "exp_0" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"real" reals nil )"bool" real_fun_preds "reals/" )nil hyperbolic nil )"posreal_ge1" hyperbolic nil )nil hyperbolic nil )"[numfield, numfield -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"real" hyperbolic nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil sq "reals/" )nil sq "reals/" )"posreal" nil )"real" reals nil )"nonneg_real" sq "reals/" )nil ln_exp nil )"posreal" nil )"real" reals nil )"even_int" integers nil )"nzint" integers nil )"posreal" nil )nil ln_exp nil )"nnreal" nil )"posreal" sq "reals/" )"real" reals nil )nil sq "reals/" )"bool" reals nil )nil real_types nil )"real" ln_exp nil )"{py | x = ln(py)}" ln_exp nil )"[numfield -> numfield]" number_fields nil )nil sqrt "reals/" )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil hyperbolic nil )nil sqrt "reals/" )"even_int" integersnil )nil hyperbolic nil )nil sq "reals/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )nil real_axioms nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" reals nil ))nil 3270840674"" (skosimp*) (("" (assert ) nil nil )) nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil ))nil 3270840028"" (skosimp*)"" "sq_eq" "nna" "cosh(x!1 / 2)" "nnb" "sqrt((cosh(x!1) + 1) / 2)" ))"1" (replace -1 1 rl)"1" (hide -1)"1" (rewrite "sq_sqrt" )"1" (expand "cosh" )"1" (rewrite "sq_div" )"1" (rewrite "sq_plus" 1)"1" (lemma "exp_sum" ("x" "x!1/2" "y" "x!1/2" ))"1" (lemma "exp_sum" ("x" "x!1/2" "y" "-x!1/2" ))"1" "exp_sum" ("x" "-x!1/2" "y" "-x!1/2" ))"1" (expand "sq" 1)"1" (replace -1 1 rl)"1" (replace -2 1 rl)"1" replace -3 1 rl)"1" rewrite "exp_0" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"posreal_ge1" hyperbolic nil )nil hyperbolic nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sq "reals/" )"real" reals nil )"(total_order?[real])" nil )"posreal" nil )nil sq "reals/" )"posreal" nil )"nonneg_real" sq "reals/" )nil ln_exp nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil ln_exp nil )"posreal" nil )"posreal" sq "reals/" )"real" reals nil )nil sq "reals/" )"bool" reals nil )nil real_types nil )"real" ln_exp nil )"{py | x = ln(py)}" ln_exp nil )"[numfield -> numfield]" number_fields nil )nil sqrt "reals/" )"real" reals nil ))nil 3270840688"" (skosimp*) (("" (assert ) nil nil )) nil )"real" reals nil ))nil 3270840700"" (skosimp*)"" (rewrite "div_mult_pos_ge1" ) (("" (assert ) nil nil )) nil ))nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )nil real_props nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil hyperbolic nil )"posreal_ge1" hyperbolic nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"real" reals nil ))nil 3270839611"" (skosimp*)"" (expand "tanh" 1)"" (rewrite "sinh_half" )"" (rewrite "cosh_half" )"" (case "x!1>=0" )"1" (assert )"1" (rewrite "sqrt_div" 1)"1" (rewrite "sqrt_div" 1)"1" (rewrite "sqrt_div" 1)"1" (name-replace "K1" "sqrt((cosh(x!1) - 1))" )"1" (name-replace "K2" "sqrt((cosh(x!1) + 1))" )"1" (rewrite "div_div1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (rewrite "sqrt_div" )"2" (rewrite "sqrt_div" )"2" (rewrite "sqrt_div" )"2" (name-replace "K1" "sqrt((cosh(x!1) - 1))" )"2" (name-replace "K2" "sqrt((cosh(x!1) +1))" )"2" (rewrite "div_div1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real_abs_lt1" hyperbolic nil )nil hyperbolic nil )"real" reals nil )"real" reals nil )"real" reals nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"nnreal" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"boolean" notequal nil )nil real_props nil )"odd_int" integersnil )"nnreal" nil )"posreal" sqrt "reals/" )nil sqrt "reals/" )nil real_types nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil hyperbolic nil )"posreal_ge1" hyperbolic nil )"bool" reals nil )nil booleans nil )"(total_order?[real])" nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil )"real" reals nil )"real" reals nil ))nil 3270841163"" (skosimp*)"" (case "sinh(n0x!1) /=0" )"1" (expand "tanh" 1)"1" "cross_mult" "x" "sinh(n0x!1 / 2)" "n0x" "cosh(n0x!1 / 2)" "y" "cosh(n0x!1) - 1" "n0y" "sinh(n0x!1)" ))"1" (replace -1 1)"1" (hide -1 -2)"1" (expand "sinh" )"1" (expand "cosh" )"1" (lemma "exp_sum" ("x" "n0x!1/2" "y" "n0x!1" ))"1" "exp_sum" ("x" "n0x!1/2" "y" "-n0x!1" ))"1" "exp_sum" "x" "-(n0x!1/2)" "y" "-n0x!1" ))"1" "exp_sum" "x" "-(n0x!1/2)" "y" "n0x!1" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ) ("3" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" (lemma "sinh_strict_increasing" )"2" (expand "strict_increasing?" )"2" (lemma "trichotomy" ("x" "n0x!1" ))"2" (split -1)"1" (inst - "0" "n0x!1" )"1" (rewrite "sinh_0" ) (("1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil )"3" (inst - "n0x!1" "0" )"3" (rewrite "sinh_0" ) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )"real" hyperbolic nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"boolean" notequal nil )nil booleans nil )nil numbers nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"posreal_ge1" hyperbolic nil )nil hyperbolic nil )"bool" reals nil )nil booleans nil )nil reals nil )nil real_props nil )"real" reals nil )"nzreal" nil )"posreal" nil )"posreal" nil )"nzreal" real_typesnil )"[numfield -> numfield]" number_fields nil )"real" reals nil )"posreal" nil )"real" reals nil )"real" reals nil )nil ln_exp nil )"real_abs_lt1" hyperbolic nil )nil hyperbolic nil )nil real_axioms nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil hyperbolic nil )"bool" real_fun_preds "reals/" ))nil 3270840252"" (skosimp*)"" (expand "tanh" )"" "cross_mult" "x" "sinh(x!1 / 2)" "n0x" "cosh(x!1 / 2)" "y" "sinh(x!1)" "n0y" "1 + cosh(x!1)" ))"1" (replace -1 1)"1" (hide -1)"1" (expand "sinh" )"1" (expand "cosh" )"1" (lemma "exp_sum" ("x" "-x!1" "y" "x!1/2" ))"1" (lemma "exp_sum" ("x" "-x!1" "y" "-(x!1/2)" ))"1" (lemma "exp_sum" ("x" "x!1" "y" "-(x!1/2)" ))"1" (lemma "exp_sum" ("x" "x!1" "y" "x!1/2" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil )"real_abs_lt1" hyperbolic nil )"real" reals nil )"real" reals nil )nil ln_exp nil )"[numfield -> numfield]" number_fields nil )"real" reals nil )"posreal" nil )"posreal" nil )"posreal" nil )"real" reals nil )"real" reals nil )nil real_props nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil )nil reals nil )nil booleans nil )"bool" reals nil )nil hyperbolic nil )"posreal_ge1" hyperbolic nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" hyperbolic nil ))nil 3270912654"" (skosimp*)"" (expand "sinh" )"" (expand "cosh" )"" (lemma "exp_sum" ("x" "x!1" "y" "x!1" ))"" (lemma "exp_sum" ("x" "x!1" "y" "-x!1" ))"" (lemma "exp_sum" ("x" "-x!1" "y" "-x!1" ))"" (lemma "exp_sum" ("x" "-x!1" "y" "x!1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" hyperbolic nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil ln_exp nil )nil ln_exp nil )"posreal" nil )"posreal" nil )"posreal" nil )"real" reals nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"real" reals nil )"posreal_ge1" hyperbolic nil ))nil 3270912427"" (skosimp*)"" (case "tanh(x!1)>=0" )"1" (lemma "sq_lt" ("nna" "tanh(x!1)" "nnb" "1" ))"1" (rewrite "sq_1" ) (("1" (assert ) nil nil )) nil )"2" (propax) nil nil ))nil )"2" (lemma "sq_lt" ("nna" "-tanh(x!1)" "nnb" "1" ))"1" (rewrite "sq_1" )"1" (rewrite "sq_neg" ) (("1" (assert ) nil nil )) nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil )"real_abs_lt1" hyperbolic nil )nil hyperbolic nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sq "reals/" )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sq "reals/" )nil real_types nil )nil sq "reals/" )"real" reals nil ))nil 3270912781"" (skosimp*)"" (rewrite "div_cancel4" )"1" (expand "tanh" )"1" (rewrite "sq_div" )"1" "both_sides_times1" "x" "sinh(2 * x!1) - sinh(2 * x!1) * (sq(sinh(x!1)) / sq(cosh(x!1)))" "y" "2 * (sinh(x!1) / cosh(x!1))" "n0z" "sq(cosh(x!1))" ))"1" (replace -1 1 rl)"1" (hide -1)"1" (assert )"1" "div_cancel1" "x" "sq(sinh(x!1))" "n0z" "sq(cosh(x!1))" ))"1" (replace -1 1)"1" "K101" "sq(sinh(x!1)) / sq(cosh(x!1))" )"1" "sinh(2 * x!1) * sq(cosh(x!1)) * K101 = sinh(2*x!1)*sq(sinh(x!1))" )"1" (hide -1 -2)"1" "2 * (sq(cosh(x!1)) * (sinh(x!1) / cosh(x!1))) = 2*cosh(x!1)*sinh(x!1)" )"1" "1" expand "sq" )"1" expand "cosh" )"1" expand "sinh" )"1" "exp_sum" "x" "x!1" "y" "x!1" ))"1" "exp_sum" "x" "x!1" "y" "-x!1" ))"1" "exp_sum" "x" "-x!1" "y" "-x!1" ))"1" "exp_sum" "x" "-x!1" "y" "x!1" ))"1" "exp_sum" "x" "2*x!1" "y" "2*x!1" ))"1" "exp_sum" "x" "2*x!1" "y" "x!1" ))"1" "exp_sum" "x" "2*x!1" "y" "-x!1" ))"1" "exp_sum" "x" "2*x!1" "y" "-(2*x!1)" ))"1" "exp_0" )"1" "exp_sum" "x" "-(2*x!1)" "y" "2*x!1" ))"1" "exp_sum" "x" "-(2*x!1)" "y" "x!1" ))"1" "exp_sum" "x" "-(2*x!1)" "y" "-x!1" ))"1" "exp_sum" "x" "-(2*x!1)" "y" "-(2*x!1)" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "sq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "sq_nz_pos" ("nz" "cosh(x!1)" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (case "tanh(x!1)>=0" )"1" (lemma "sq_gt" ("nna" "1" "nnb" "tanh(x!1)" ))"1" (rewrite "sq_1" ) (("1" (assert ) nil nil )) nil )"2" (propax) nil nil ))nil )"2" (lemma "sq_gt" ("nna" "1" "nnb" "-tanh(x!1)" ))"1" (rewrite "sq_1" )"1" (rewrite "sq_neg" ) (("1" (assert ) nil nil )) nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )nil real_props nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"nonneg_real" sq "reals/" )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )nil hyperbolic nil )"real_abs_lt1" hyperbolic nil )"real" hyperbolic nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal_ge1" hyperbolic nil )nil hyperbolic nil )nil sq "reals/" )"real" reals nil )"real" reals nil )"real" reals nil )nil ln_exp nil )nil ln_exp nil )"posreal" nil )"posreal" nil )"posreal" nil )"[T, T -> boolean]" equalities nil )nil real_props nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil real_props nil ))nil 3270915543"" (skosimp*)"" (expand "cosh" )"" (expand "sq" )"" (lemma "exp_sum" ("x" "x!1" "y" "x!1" ))"" (lemma "exp_sum" ("x" "x!1" "y" "-x!1" ))"" (lemma "exp_sum" ("x" "-x!1" "y" "-x!1" ))"" (lemma "exp_sum" ("x" "-x!1" "y" "x!1" ))"" (rewrite "exp_0" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"posreal" nil )"posreal" sq "reals/" )"posreal_ge1" hyperbolic nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil ln_exp nil )nil ln_exp nil )"real" reals nil )"real" reals nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"real" reals nil )"nonneg_real" sq "reals/" )"posreal" nil )"posreal" nil ))nil 3270915986"" (skosimp*)"" (lemma "cosh2x" ("x" "x!1" ))"" (lemma "cosh_sinh_one" ("x" "x!1" )) (("" (assert ) nil nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil )"posreal" nil )"nnreal" nil )"real" reals nil )"real" reals nil )nil hyperbolic nil ))nil 3270916242"" (skosimp*)"" (lemma "cosh2x_B" ("x" "x!1" ))"" (lemma "cosh2x" ("x" "x!1" )) (("" (assert ) nil nil )) nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil )"nnreal" nil )"posreal" nil )"nnreal" nil )"real" reals nil )"real" reals nil )nil hyperbolic nil ))nil 3270916617"" (skosimp*)"" (rewrite "div_cancel4" )"" (expand "tanh" )"" (rewrite "sq_div" )"" (rewrite "div_times" 1)"1" (rewrite "add_div" )"1" "cross_mult" "x" "(sinh(2 * x!1) * (sq(cosh(x!1)) * cosh(2 * x!1)) + " " n0x" "(cosh(2 * x!1) * (sq(cosh(x!1)) * cosh(2 * x!1)))" "y" "2*sinh(x!1)" "n0y" "cosh(x!1)" ))"1" (replace -1 1)"1" (hide -1)"1" (expand "sq" )"1" (rewrite "sinh2x" )"1" (rewrite "cosh2x" )"1" (expand "sq" )"1" (lemma "cosh_sinh_one" ("x" "x!1" ))"1" expand "sq" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "sq_nz_pos" ("nz" "cosh(2*x!1)" ))"2" (lemma "sq_nz_pos" ("nz" "cosh(x!1)" ))"2" "posreal_times_posreal_is_posreal" "px" "sq(cosh(x!1))" "py" "sq(cosh(2 * x!1))" ))"1" (expand "sq" ) (("1" (assert ) nil nil ))nil )"2" (propax) nil nil ) ("3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "sq_nz_pos" ("nz" "cosh(x!1)" ))"2" "posreal_times_posreal_is_posreal" "px" "sq(cosh(x!1))" "py" "cosh(2*x!1)" ))"1" (assert ) nil nil ) ("2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (lemma "sq_nz_pos" ("nz" "cosh(x!1)" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"posreal" nil )"real" reals nil )nil real_props nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"nonneg_real" sq "reals/" )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )nil hyperbolic nil )"real_abs_lt1" hyperbolic nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal_ge1" hyperbolic nil )nil hyperbolic nil )"real" hyperbolic nil )nil sq "reals/" )nil real_props nil )"real" reals nil )nil hyperbolic nil )"nnreal" nil )"real" reals nil )nil hyperbolic nil )nil hyperbolic nil )nil real_props nil )nil real_props nil )"real" reals nil ))nil 3270920091"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil ))nil 3270918363"" (skosimp*)"" (lemma "sinh_sum" ("x" "2*x!1" "y" "x!1" ))"" (replace -1 1)"" (hide -1)"" (rewrite "sinh2x" )"" (rewrite "cosh2x" )"" (lemma "cosh_sinh_one" ("x" "x!1" ))"" (expand "sq" )"" (assert )"" (expand "^" )"" (expand "expt" )"" (expand "expt" )"" (expand "expt" )"" (expand "expt" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil )"real" reals nil )nil hyperbolic nil )"nnreal" nil )"real" reals nil )"nonneg_real" sq "reals/" )"real" exponentiation nil )"real" exponentiation nil )"real" reals nil )nil hyperbolic nil )nil hyperbolic nil ))nil 3270919010"" (skosimp*)"" (lemma "cosh_sum" ("x" "x!1" "y" "2*x!1" ))"" (replace -1)"" (rewrite "cosh2x" )"" (rewrite "sinh2x" )"" (hide -1)"" (expand "^" )"" (expand "expt" )"" (expand "expt" )"" (expand "expt" )"" (expand "expt" )"" (expand "sq" )"" (lemma "cosh_sinh_one" ("x" "x!1" ))"" (expand "sq" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil )"real" reals nil )nil hyperbolic nil )"nnreal" nil )"real" reals nil )"real" exponentiation nil )"nonneg_real" sq "reals/" )"real" reals nil )nil hyperbolic nil )"real" exponentiation nil )nil hyperbolic nil ))nil 3270919340"" (skosimp*)"" (lemma "sinh2x" ("x" "2*x!1" ))"" (rewrite "sinh2x" )"" (rewrite "cosh2x" )"" (expand "sq" )"" (lemma "cosh_sinh_one" ("x" "x!1" ))"" (expand "sq" )"" (assert )"" (rewrite "sinh2x" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil )"real" reals nil )nil hyperbolic nil )"nnreal" nil )"real" reals nil )nil hyperbolic nil )"real" reals nil )"nonneg_real" sq "reals/" )"nnreal" nil ))nil 3270912606"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil ))nil 3270919895"" (skosimp*)"" (lemma "cosh2x" ("x" "2*x!1" ))"" (replace -1 1)"" (hide -1)"" (rewrite "cosh2x" )"" (expand "sq" )"" (expand "^" )"" (expand "expt" )"" (expand "expt" )"" (expand "expt" )"" (expand "expt" )"" (expand "expt" )"" (lemma "cosh_sinh_one" ("x" "x!1" ))"" (expand "sq" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil )"real" reals nil )"nonneg_real" sq "reals/" )"real" exponentiation nil )nil hyperbolic nil )"real" exponentiation nil )"real" reals nil )"real" reals nil )"nnreal" nil ))nil 3270964579"" (skosimp*)"" (rewrite "cosh_sum" )"" (rewrite "cosh_diff" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil hyperbolic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" reals nil )"odd_int" integers nil )"real" reals nil )"real" reals nil )"real" reals nil )nil hyperbolic nil ))nil 3270964883"" (skosimp*)"" (rewrite "cosh_sum" )"" (rewrite "cosh_diff" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil hyperbolic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"odd_int" integers nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )nil hyperbolic nil ))nil 3270964906"" (skosimp*)"" (rewrite "sinh_sum" )"" (rewrite "sinh_diff" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil hyperbolic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"odd_int" integers nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )nil hyperbolic nil ))nil 3270965915"" (skosimp*)"" "sinh_times_cosh" "x" "(x!1 + y!1) / 2" "y" "(x!1 - y!1) / 2" ))"" (assert ) nil nil )) nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil 3270966111"" (skosimp*)"" (lemma "sum_sinh" ("x" "x!1" "y" "-y!1" ))"" (rewrite "sinh_neg" ) (("" (assert ) nil nil )) nil )) nil ))nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )nil hyperbolic nil ))nil 3270966232"" (skosimp*)"" "cosh_times_cosh" ("x" "(x!1+y!1)/2" "y" "(x!1-y!1)/2" ))"" (name-replace "K1" "cosh(x!1)" )"" (name-replace "K2" "cosh(y!1)" )"" (name-replace "K3" "cosh((x!1+y!1)/2)" )"" (name-replace "K4" "cosh((x!1-y!1)/2)" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil )"real" reals nil )"odd_int" integers nil )"real" reals nil )"real" reals nil )"real" reals nil )"[T, T -> boolean]" equalities nil )nil booleans nil )"bool" reals nil )nil hyperbolic nil )"posreal_ge1" hyperbolic nil ))nil 3270966462"" (skosimp*)"" "sinh_times_sinh" ("x" "(x!1+y!1)/2" "y" "(x!1-y!1)/2" ))"" (name-replace "K1" "cosh(x!1)" )"" (name-replace "K2" "cosh(y!1)" )"" (name-replace "K3" "sinh((x!1 + y!1) / 2)" )"" (name-replace "K4" "sinh((x!1 - y!1) / 2)" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil )"real" reals nil )"real" hyperbolic nil )"real" reals nil )"real" reals nil )"odd_int" integers nil )"real" reals nil )"[T, T -> boolean]" equalities nil )nil booleans nil )"bool" reals nil )nil hyperbolic nil )"posreal_ge1" hyperbolic nil ))nil 3270965627"" (skosimp*)"" "posreal_times_posreal_is_posreal" "px" "cosh(x!1)" "py" "cosh(y!1)" ))"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil )"posreal_ge1" hyperbolic nil )nil hyperbolic nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_types nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" reals nil ))nil 3270966616"" (skosimp*)"" (expand "tanh" )"" (rewrite "sinh_sum" )"" "add_div" "x" "sinh(x!1)" "n0x" "cosh(x!1)" "y" "sinh(y!1)" "n0y" "cosh(y!1)" ))"" (replace -1 1) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )"real_abs_lt1" hyperbolic nil )"real" hyperbolic nil )"posreal_ge1" hyperbolic nil )nil hyperbolic nil )"bool" reals nil )nil booleans nil )nil reals nil )"boolean" notequal nil )nil real_props nil )"real" reals nil )"real" reals nil )"real" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil ))nil 3270965675"" (case "FORALL (x:nzreal): sinh(x) /=0" )"1" (skosimp*)"1" (inst-cp - "n0x!1" )"1" (inst - "n0y!1" )"1" "nzreal_times_nzreal_is_nzreal" "nzx" "sinh(n0x!1)" "nzy" "sinh(n0y!1)" ))"1" (assert ) nil nil ) ("2" (propax) nil nil )"3" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (lemma "trichotomy" ("x" "x!1" ))"2" (lemma "sinh_strict_increasing" )"2" (expand "strict_increasing?" )"2" (lemma "sinh_0" )"2" (split)"1" (inst - "0" "x!1" ) (("1" (assert ) nil nil ))nil )"2" (assert ) nil nil )"3" (inst - "x!1" "0" ) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_axioms nil )"bool" real_fun_preds "reals/" )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil hyperbolic nil )nil hyperbolic nil )"real" reals nil )nil real_types 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 )"real" hyperbolic nil ))nil 3270966876"" (skosimp*)"" (expand "coth" )"" (case "FORALL (x:nzreal): sinh(x) /= 0" )"1" (inst-cp - "n0x!1" )"1" (inst - "n0y!1" )"1" "nzreal_times_nzreal_is_nzreal" "nzx" "sinh(n0x!1)" "nzy" "sinh(n0y!1)" ))"1" (expand "tanh" )"1" (rewrite "div_div1" )"1" (rewrite "div_div1" )"1" "add_div" "x" "cosh(n0x!1)" "n0x" "sinh(n0x!1)" "y" "cosh(n0y!1)" "n0y" "sinh(n0y!1)" ))"1" (rewrite "sinh_sum" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ) ("3" (propax) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (lemma "sinh_strict_increasing" )"2" (expand "strict_increasing?" )"2" (lemma "sinh_0" )"2" (lemma "trichotomy" ("x" "x!1" ))"2" (split)"1" (inst - "0" "x!1" ) (("1" (assert ) nil nil ))nil )"2" (assert ) nil nil )"3" (inst - "x!1" "0" ) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real_abs_gt1" hyperbolic nil )nil hyperbolic nil )nil hyperbolic nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil real_axioms nil )"bool" real_fun_preds "reals/" )nil real_types nil )nil real_props nil )nil reals nil )nil booleans nil )"bool" reals nil )nil hyperbolic nil )"posreal_ge1" hyperbolic nil )"nzreal" nil )"real" reals nil )nil real_props nil )"real" reals nil )nil hyperbolic nil )"real_abs_lt1" hyperbolic nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil )nil reals nil )"real" hyperbolic nil ))nil 3270997686"" (skosimp*)"" (rewrite "sinh_times_sinh" )"" (lemma "sum_sinh" ("x" "x!1" "y" "y!1" ))"" (lemma "diff_sinh" ("x" "x!1" "y" "y!1" ))"" "cosh_times_cosh" "x" "(x!1+y!1)/2" "y" "(x!1-y!1)/2" ))"" "sinh_times_sinh" "x" "(x!1+y!1)/2" "y" "(x!1-y!1)/2" ))"" "sq(sinh(x!1)) - sq(sinh(y!1)) = 2 * cosh((x!1 + y!1) / 2) * sinh((x!1 - y!1) / 2)*2 * sinh((x!1 + y!1) / 2) * cosh((x!1 - y!1) / 2)" )"1" (hide -4 -5 -1)"1" "2 * cosh((x!1 + y!1) / 2) * sinh((x!1 - y!1) / 2) * 2 * ") "1" (hide -1 -2 -3)"1" (simplify 1)"1" "(x!1 + y!1) / 2 - (x!1 - y!1) / 2 = y!1" )"1" "(x!1 - y!1) / 2 + (x!1 + y!1) / 2 = x!1" )"1" (rewrite "cosh2x" )"1" rewrite "cosh2x" )"1" rewrite "sq_rew" )"1" rewrite "sq_rew" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert )"2" (hide 2)"2" "(x!1 + y!1) / 2 - (x!1 - y!1) / 2=y!1" )"1" "(x!1 - y!1) / 2 + (x!1 + y!1) / 2=x!1" )"1" (assert )"1" "(cosh((x!1 - y!1) / 2) * cosh((x!1 + y!1) / 2) * h((x!1 - y!1) / 2))") "1" replace -4 1)"1" replace -5 1)"1" (assert ) nil nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 -2 2)"2" (expand "sq" 1) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )nil hyperbolic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )nil hyperbolic nil )"odd_int" integers nil )nil hyperbolic nil )"nnreal" nil )nil sq "reals/" )"posreal_ge1" hyperbolic nil )nil hyperbolic nil )"[numfield, numfield -> numfield]" number_fields nil )"real" hyperbolic nil )"nonneg_real" sq "reals/" )nil real_types nil )"bool" reals nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil hyperbolic nil )nil hyperbolic nil ))nil 3270998756"" (skosimp*)"" (lemma "diff_sinh_sq" ("x" "x!1" "y" "y!1" ))"" (lemma "cosh_sinh_one" )"" (inst-cp - "x!1" )"" (inst - "y!1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil )"real" reals nil )"real" reals nil )"real" reals nil )nil hyperbolic nil ))nil 3270998894"" (skosimp*)"" (rewrite "cosh_times_cosh" )"" (rewrite "div_cancel4" )"" (rewrite "cosh2x" )"" (rewrite "cosh2x" )"" (lemma "cosh_sinh_one" )"" (inst-cp - "x!1" )"" (inst - "y!1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )nil hyperbolic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )nil hyperbolic nil )nil hyperbolic nil )"nnreal" nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal_ge1" hyperbolic nil )nil hyperbolic nil )"real" hyperbolic nil )"nonneg_real" sq "reals/" )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"boolean" notequal nil )nil real_props nil )"real" reals nil )"nnreal" nil ))nil 3270921451"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"real" reals nil ))nil 3270921235"" (skosimp*)"" (rewrite "cosh_plus_sinh" )"" (rewrite "cosh_plus_sinh" )"" (rewrite "exp_scal" ) nil nil )) nil ))nil ))nil )nil hyperbolic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"nzreal" exponentiation nil )"posreal" exponentiation nil )nil integers nil )nil ln_exp nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" reals nil ))nil 3271096134 ("" (grind) nil nil ) nil nil 3322476122 ("" (assuming-tcc) nil nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"boolean" notequal nil ))nil ))nil 3271096155"" (skosimp*) (("" (assert ) nil nil )) nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"odd_int" integers nil )"posint" nil )"(total_order?[real])" nil ))nil 3271096747"" (skosimp*)"" "Taylors" ("aa" "0" "bb" "x!1" "f" "sinh" "n" "2*n!1+2" ))"" (case "FORALL (n:nat): derivable_n_times(sinh,n)" )"1" (lemma "deriv_sinh" )"1" (lemma "deriv_cosh" )"1" (lemma "sinh_derivable2" )"1" (lemma "cosh_derivable2" )"1" (case "FORALL (n:nat): nderiv(2*n,sinh) = sinh" )"1" case "FORALL (n:nat): nderiv(2*n+1,sinh) = cosh" )"1" (inst-cp -7 "2*n!1+3" )"1" (replace -8)"1" (skolem! -9)"1" (inst + "c!1" )"1" (replace -9 1)"1" "n!1+1" )"1" replace -2)"1" "1" "1" expand "sinh_series_n" )"1" rewrite "sinh_0" )"1" case "FORALL (i:nat): i <= n!1 => sigma(0, 2 + 2 * i, LAMBDA (nn:nat):IF nn > 2 + 2 * n!1 THEN 0LAMBDA (i: nat): (x!1 ^ (1 + 2 * i)) / factorial(1 + 2 * i))") "1" "n!1" )"1" (assert ) nil nil ))nil )"2" "2" "i" )"1" expand "sigma" 1)"1" expand "sigma" 1)"1" expand "sigma" "1" expand "nderiv" "1" expand "nderiv" "1" expand "nderiv" "1" replace "1" replace "1" rewrite "sinh_0" )"1" rewrite "cosh_0" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "sigma" 1)"2" expand "sigma" "2" assert )"2" replace "2" "2" "2" "1+j!1" )"2" replace "2" "2+j!1" )"2" replace "2" rewrite "sinh_0" )"2" rewrite "cosh_0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "nn!1" )nil nil ))nil ))nil ))nil ))nil )"3" "3" "3" "nn!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -7 2)"2" (induct "n" )"1" (expand "nderiv" 1)"1" (expand "nderiv" 1)"1" (propax) nil nil )) nil ))nil )"2" (skosimp*)"2" (expand "nderiv" 1)"2" (expand "nderiv" 1)"2" replace -6)"2" replace -5)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (inst - "1+2*n!3" ) nil nil )) nil ))nil ))nil )"3" (skosimp*)"3" (inst -6 "1+2*n!2" ) nil nil )) nil ))nil )"2" (hide -6 2)"2" (copy -5)"2" (induct "n" 1)"1" (expand "nderiv" 1)"1" (propax) nil nil )) nil )"2" (skolem! 1)"2" (flatten 1)"2" (expand "nderiv" 1)"2" expand "nderiv" 1)"2" replace -6)"2" replace -5)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (inst - "2*n!3" ) nil nil )) nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (inst -5 "2*n!2" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp*)"2" (case "FORALL (n:nat): derivable_n_times(sinh, n*2)" )"1" (case "even?(n!2)" )"1" (expand "even?" )"1" (skosimp*)"1" (replace -1)"1" (inst - "j!1" )"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (rewrite "even_or_odd" )"2" (expand "odd?" )"2" (skosimp*)"2" (replace -1)"2" (inst - "2+2*j!1" )"1" "derivable_n_times_lem" "f" "sinh" "n" "(2 + 2 * j!1) * 2" "m" "1 + 2 * j!1" ))"1" (assert ) nil nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "n" )"1" (expand "derivable_n_times" )"1" (propax) nil nil )) nil )"2" (skosimp*)"2" (expand "derivable_n_times" 1)"2" (expand "derivable_n_times" 1)"2" (lemma "sinh_derivable2" )"2" (lemma "cosh_derivable2" )"2" (lemma "deriv_cosh" )"2" "deriv_sinh" )"2" replace -1)"2" replace -2)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" sigma "reals/" )) shostak))nil 3253579641"" (skosimp*)"" (case "x!1 < 0" )"1" (lemma "sqrt_lt" ("nny" "sq(-x!1)" "nnz" "sq(x!1)+1" ))"1" (rewrite "sqrt_sq" -1)"1" (rewrite "sq_neg" -1) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (case "x!1=0" )"1" (replace -1)"1" (rewrite "sq_0" )"1" (rewrite "sqrt_1" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (lemma "sqrt_lt" ("nny" "0" "nnz" "sq(x!1)+1" ))"2" (flatten)"2" (split -2)"1" (rewrite "sqrt_0" ) (("1" (assert ) nil nil )) nil )"2" "both_sides_times_pos_lt1" "x" "0" "y" "x!1" "pz" "x!1" ))"1" (hide -2 4) (("1" (grind) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sqrt "reals/" )"posreal" sqrt "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )nil sq "reals/" )"real" reals nil )"posreal" nil )nil sqrt "reals/" )"bool" reals nil )nil real_types nil )"nonneg_real" sq "reals/" )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil sqrt "reals/" )"real" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"bool" reals nil )nil real_props nil )nil sqrt "reals/" )nil sq "reals/" )"[T, T -> boolean]" equalities nil ))nil 3253579641"" (skosimp*)"" (typepred "x!1" )"" (lemma "le_times_le_pos" )"" (inst - "1" "1" "x!1" "x!1" )"" (expand "sq" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil hyperbolic nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil real_types nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )"nonneg_real" sq "reals/" )nil real_props nil ))nil 3253579641"" (skosimp*)"" (typepred "sqrt(sq(x!1)-1)" )"1" (assert ) nil nil )"2" (lemma "acosh_TCC1" ("x" "x!1" )) (("2" (propax) nil nil ))nil ))nil ))nil )nil hyperbolic nil )"nonneg_real" sq "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"[numfield, numfield -> numfield]" number_fields nil )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]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"real" reals nil )"(total_order?[real])" nil )"nnreal" nil )"real" reals nil )nil hyperbolic nil ))nil 3253579641"" (skosimp*)"" (lemma "acosh_TCC2" ("x" "x!1" ))"" (flatten)"" (lemma "ln_increasing" )"" (expand "increasing?" )"" "le_times_le_pos" "nnx" "1" "y" "x!1" "nnz" "1" "w" "x!1" ))"" (assert )"" (case "x!1 = 1" )"1" (replace -1)"1" (rewrite "sq_1" )"1" (rewrite "sqrt_0" )"1" (rewrite "ln_1" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (case "x!1 > 1" )"1" "lt_times_lt_pos1" "px" "1" "y" "x!1" "nnz" "1" "w" "x!1" ))"1" (assert )"1" "sqrt_lt" "nny" "0" "nnz" "sq(x!1)-1" ))"1" (rewrite "sqrt_0" )"1" (expand "sq" )"1" "1" "x!1+sqrt(x!1*x!1-1)" )"1" rewrite "ln_1" )"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil hyperbolic 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 hyperbolic nil )nil ln_exp nil )nil real_props nil )nil real_types nil )"[T, T -> boolean]" equalities nil )nil sq "reals/" )nil ln_exp nil )"posint" nil )"odd_int" integers nil )"(divides(n))" divides nil )"posint" nil )"odd_int" integers nil )nil sqrt "reals/" )"posreal" sq "reals/" )nil real_props nil )nil real_types nil )nil sqrt "reals/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_real" sq "reals/" )"posreal_ge1" hyperbolic nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"bool" real_fun_preds "reals/" ))nil 3253579641 ("" (grind) nil nil ) nil shostak))nil 3253579641"" (skosimp*)"" (typepred "x!1" )"" (lemma "div_mult_pos_lt2" )"" (inst - "1-x!1" "0" "1+x!1" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )nil hyperbolic nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"real" reals nil )"real" reals nil )nil real_props nil ))nil 3286017244"" (stop-rewrite "sq_sqrt" )"" (expand "bijective?" )"" (expand "injective?" )"" (split)"1" (skosimp*)"1" (lemma "trich_lt" ("x" "x1!1" "y" "x2!1" ))"1" (lemma "sinh_strict_increasing" )"1" (expand "strict_increasing?" )"1" (split -2)"1" (inst - "x1!1" "x2!1" )"1" (assert ) nil nil )) nil )"2" (propax) nil nil )"3" (inst - "x2!1" "x1!1" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "surjective?" )"2" (skosimp*)"2" (case "y!1+sqrt(1+sq(y!1)) > 0" )"1" (inst + "ln(y!1+sqrt(1+sq(y!1)))" )"1" (expand "sinh" )"1" "exp_diff" "x" "0" "y" "ln(sqrt(1 + sq(y!1))+y!1)" ))"1" (rewrite "exp_0" )"1" (replace -1 1)"1" (rewrite "exp_ln" )"1" (hide -1)"1" "div_cancel3" "x" "sqrt(1 + sq(y!1)) + y!1 - 1 / (sqrt(1 + sq(y!1)) + y!1)" "y" "y!1" "n0z" "2" ))"1" replace -1 1)"1" "1" "minus_div1" "x" "sqrt(1 + sq(y!1)) + y!1" "n0y" "sqrt(1 + sq(y!1)) + y!1" "n0x" "1" "y" "1" ))"1" replace -1)"1" "div_cancel3" "x" "(sqrt(1 + sq(y!1)) + y!1) * (sqrt(1 + sq(y!1)) + y!1) - 1 * 1" "n0z" "sqrt(1 + sq(y!1)) + y!1" "y" "y!1*2" ))"1" replace -1 1)"1" "sq_sqrt" )"1" "1+sq(y!1)" )"1" assert )"1" expand "sq" -1 1)"1" replace -1 1)"1" expand "sq" 1)"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (hide 2)"2" (lemma "trichotomy" ("x" "y!1" ))"2" (split -1)"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" "sq_lt" "nna" "-y!1" "nnb" "sqrt(1+sq(y!1))" ))"1" (rewrite "sq_sqrt" )"1" (rewrite "sq_neg" )"1" (assert ) nil nil )) nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" functions nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )"bool" real_fun_preds "reals/" )"(strict_total_order?[real])" real_props nil )nil hyperbolic nil )nil sq "reals/" )"[numfield -> numfield]" number_fields nil )nil sq "reals/" )"real" reals nil )nil real_axioms nil )"(strict_total_order?[real])" real_props nil )"posreal" sqrt "reals/" )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" hyperbolic nil )"real" ln_exp nil )nil real_types nil )nil ln_exp nil )nil real_props nil )"real" reals nil )nil sqrt "reals/" )"(divides(n))" divides nil )"odd_int" integers nil )"posint" nil )"posreal" nil )"nzreal" nil )"real" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )"boolean" notequal nil )nil real_props nil )"posreal" nil )nil ln_exp nil )"real" reals nil )"odd_int" integers nil )nil ln_exp nil )"real" hyperbolic nil )"posreal" nil )"real" reals nil )nil booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"nonneg_real" sq "reals/" )"bool" functions nil )"bool" functions nil ))nil )nil 3253387007"" (expand "bijective?" )"" (expand "injective?" )"" (split)"1" (skosimp*)"1" (lemma "trich_lt" ("x" "x1!1" "y" "x2!1" ))"1" (lemma "sinh_strict_increasing" )"1" (expand "strict_increasing?" )"1" (split -2)"1" (inst - "x1!1" "x2!1" ) (("1" (assert ) nil nil ))nil )"2" (propax) nil nil )"3" (inst - "x2!1" "x1!1" ) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "surjective?" )"2" (skosimp*)"2" (case "y!1+sqrt(1+sq(y!1)) > 0" )"1" (inst + "ln(y!1+sqrt(1+sq(y!1)))" )"1" (expand "sinh" )"1" "exp_diff" "x" "0" "y" "ln(sqrt(1 + sq(y!1))+y!1)" ))"1" (rewrite "exp_0" )"1" (replace -1 1)"1" (rewrite "exp_ln" )"1" (hide -1)"1" "div_cancel3" "x" "sqrt(1 + sq(y!1)) + y!1 - 1 / (sqrt(1 + sq(y!1)) + y!1)" "y" "y!1" "n0z" "2" ))"1" replace -1 1)"1" "1" "minus_div1" "x" "sqrt(1 + sq(y!1)) + y!1" "n0y" "sqrt(1 + sq(y!1)) + y!1" "n0x" "1" "y" "1" ))"1" replace -1)"1" "div_cancel3" "x" "(sqrt(1 + sq(y!1)) + y!1) * (sqrt(1 + sq(y!1)) + y!1) - 1 * 1" "n0z" "sqrt(1 + sq(y!1)) + y!1" "y" "y!1*2" ))"1" replace -1 1)"1" "sq_sqrt" )"1" "1+sq(y!1)" )"1" assert )"1" expand "sq" -1 1)"1" replace -1 1)"1" expand "sq" 1)"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (hide 2)"2" (lemma "trichotomy" ("x" "y!1" ))"2" (split -1)"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" "sq_lt" "nna" "-y!1" "nnb" "sqrt(1+sq(y!1))" ))"1" (rewrite "sq_sqrt" )"1" (rewrite "sq_neg" )"1" (assert ) nil nil )) nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nonneg_real" sq "reals/" )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )nil ln_exp nil )nil ln_exp nil )nil sqrt "reals/" )nil ln_exp nil )"real" ln_exp nil )nil sq "reals/" )nil sq "reals/" )"bool" real_fun_preds "reals/" ))nil 3253394558"" (expand "bijective?" )"" (expand "injective?" )"" (expand "surjective?" )"" (expand "nnreal_cosh" )"" (split)"1" (skosimp*)"1" (lemma "cosh_strict_increasing" )"1" (expand "nnreal_cosh" )"1" (expand "strict_increasing?" )"1" (lemma "trich_lt" ("x" "x1!1" "y" "x2!1" ))"1" (split -1)"1" (inst - "x1!1" "x2!1" )"1" (assert ) nil nil )) nil )"2" (propax) nil nil )"3" (inst - "x2!1" "x1!1" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst + "acosh(y!1)" )"2" (expand "cosh" )"2" (expand "acosh" )"2" (lemma "acosh_TCC1" ("x" "y!1" ))"2" (lemma "acosh_TCC2" ("x" "y!1" ))"2" (flatten -1)"2" "exp_diff" "x" "0" "y" "ln(sqrt(sq(y!1) - 1) + y!1)" ))"1" (rewrite "exp_0" )"1" replace -1 1)"1" rewrite "exp_ln" )"1" rewrite "div_cancel3" 1)"1" "cross_mult" "x" "y!1-sqrt(sq(y!1) - 1)" "n0x" "1" "y" "1" "n0y" "sqrt(sq(y!1) - 1) + y!1" ))"1" "1" "1" "1" (assert ) nil nil )"2" "2" assert )"2" rewrite "sq_rew" 1)"2" rewrite "sq_sqrt" )"2" rewrite "sq_rew" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" functions nil )"posreal_ge1" hyperbolic nil )"posreal_ge1" hyperbolic nil )nil hyperbolic nil )nil ln_exp nil )"odd_int" integers nil )"posreal" nil )nil ln_exp nil )"posreal" nil )nil real_props nil )nil sq "reals/" )nil sqrt "reals/" )"nnreal" nil )"posint" nil )"odd_int" integers nil )"(divides(n))" divides nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"nzreal" nil )"real" reals nil )nil real_props nil )"boolean" notequal nil )nil reals nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )nil ln_exp nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" ln_exp nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_real" sq "reals/" )nil hyperbolic nil )"nnreal" hyperbolic nil )nil hyperbolic nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"bool" real_fun_preds "reals/" )nil hyperbolic nil )"bool" functions nil )"bool" functions nil ))nil 3253584394"" (expand "bijective?" )"" (expand "injective?" )"" (expand "surjective?" )"" (split)"1" (skosimp*)"1" (lemma "tanh_strict_increasing" )"1" (expand "strict_increasing?" )"1" (lemma "trich_lt" ("x" "x1!1" "y" "x2!1" ))"1" (split -1)"1" (inst - "x1!1" "x2!1" )"1" (assert ) nil nil )) nil )"2" (propax) nil nil )"3" (inst - "x2!1" "x1!1" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst + "atanh(y!1)" )"2" (expand "tanh" )"2" (expand "sinh" )"2" (expand "cosh" )"2" (typepred "y!1" )"2" (typepred "exp(atanh(y!1))" )"2" (typepred "exp(-atanh(y!1))" )"2" (hide -1 -3 -4 -6)"2" (rewrite "div_div1" )"2" "div_cancel1" "x" "exp(atanh(y!1)) - exp(-atanh(y!1))" "n0z" "2" ))"2" replace -1)"2" "2" case "(exp(atanh(y!1)) - exp(-atanh(y!1))) / (exp(atanh(y!1)) + exp(-atanh(y!1))) = (exp(2*atanh(y!1)) - 1)/(exp(2*atanh(y!1)) + 1)" )"1" replace -1)"1" "1" rewrite "div_cancel3" 1)"1" expand "atanh" 1)"1" "div_cancel1" "x" "ln((1 + y!1) / (1 - y!1))" "n0z" "2" ))"1" replace -1)"1" "1" "exp_ln" )"1" "posreal_div_posreal_is_posreal" "px" "1+y!1" "py" "1-y!1" ))"1" "(1 + y!1) / (1 - y!1)" )"1" replace "1" "both_sides_times1" "x" "(1 + y!1) / (1 - y!1) - 1" "y" "(1 + y!1) / (1 - y!1) * y!1 + y!1" "n0z" "1 - y!1" ))"1" replace "1" "1" "div_cancel1" "x" "1+y!1" "n0z" "1-y!1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "posreal_div_posreal_is_posreal" "px" "1+y!1" "py" "1-y!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "cross_mult" "x" "(exp(atanh(y!1)) - exp(-atanh(y!1)))" "n0x" "(exp(atanh(y!1)) + exp(-atanh(y!1)))" "y" "(exp(2 * atanh(y!1)) - 1)" "n0y" "(exp(2 * atanh(y!1)) + 1)" ))"2" replace -1)"2" "2" "K1" "atanh(y!1)" )"2" assert )"2" "exp_sum" "x" "-K1" "y" "2*K1" ))"2" replace -1 * rl)"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 )"bool" functions nil )nil hyperbolic nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"bool" real_fun_preds "reals/" )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil hyperbolic nil )"real" hyperbolic nil )"real" hyperbolic nil )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )"boolean" notequal nil )nil real_props nil )"real" reals nil )"posreal" nil )"posreal" nil )"real" reals nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )nil ln_exp nil )"real_abs_lt1" hyperbolic nil )nil real_props nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"(total_order?[real])" nil )nil real_props nil )nil real_props nil )"nzreal" nil )"posreal" nil )nil ln_exp nil )nil real_props nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"real" ln_exp nil )"{py | x = ln(py)}" ln_exp nil )"posreal_ge1" hyperbolic nil )"real_abs_lt1" hyperbolic nil )"bool" functions nil )"bool" functions nil ))nil 3270128162"" (lemma "sinh_bij" )"" (expand "posreal_csch" )"" (expand "csch" )"" (expand "bijective?" )"" (flatten -1)"" (split 1)"1" (hide -2)"1" (expand "injective?" )"1" (skosimp*)"1" (typepred "x1!1" )"1" (typepred "x2!1" )"1" (hide -1 -3)"1" (lemma "sinh_strict_increasing" )"1" (expand "strict_increasing?" )"1" "0" "x1!1" )"1" "0" "x2!1" )"1" rewrite "sinh_0" )"1" expand ">" (-4 -5))"1" replace -4)"1" replace -5)"1" "cross_mult" "x" "1" "y" "1" "n0x" "sinh(x1!1)" "n0y" "sinh(x2!1)" ))"1" replace -7)"1" "1" "x1!1" "x2!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (expand "surjective?" )"2" (skosimp*)"2" (inst - "1/y!1" )"2" (skosimp*)"2" (lemma "sinh_strict_increasing" )"2" (expand "strict_increasing?" )"2" "posreal_div_posreal_is_posreal" "px" "1" "py" "y!1" ))"2" "trichotomy" ("x" "x!1" ))"2" "1" "0" "x!1" )"1" rewrite "sinh_0" )"1" assert )"1" "x!1" )"1" rewrite "div_cancel3" )"1" replace -4)"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" rewrite "sinh_0" )"2" (assert ) nil nil ))nil ))nil )"3" "x!1" "0" )"3" rewrite "sinh_0" )"3" assert )"3" "K1" "sinh(x!1)" )"3" "K2" "1/y!1" )"3" replace -4)"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" hyperbolic nil )"bool" functions nil )"bool" functions nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" real_fun_preds "reals/" )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" hyperbolic nil )nil reals nil )"boolean" notequal nil )nil real_props nil )nil hyperbolic nil )nil hyperbolic nil )"bool" functions nil )"posreal" nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil real_types nil )"(total_order?[real])" nil )"posreal" nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"[T, T -> boolean]" equalities nil )nil real_axioms nil )"real" hyperbolic nil )"nzreal" nil )nil hyperbolic nil ))nil 3270130610"" (expand "nnreal_sech" )"" (expand "sech" )"" (lemma "cosh_bij" )"" (expand "bijective?" )"" (flatten -1)"" (lemma "cosh_strict_increasing" )"" (expand "strict_increasing?" )"" (split 1)"1" (hide -3)"1" (expand "injective?" )"1" (skosimp*)"1" "trich_lt" ("x" "x1!1" "y" "x2!1" ))"1" (split -1)"1" (inst-cp - "x1!1" "x2!1" )"1" replace -1)"1" expand "nnreal_cosh" )"1" "cosh(x1!1)" )"1" "cosh(x2!1)" )"1" "cross_mult" "x" "1" "y" "1" "n0x" "cosh(x1!1)" "n0y" "cosh(x2!1)" ))"1" (assert ) nil nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil )"3" (inst - "x2!1" "x1!1" )"3" expand "nnreal_cosh" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2)"2" (expand "surjective?" )"2" (expand "nnreal_cosh" )"2" (skosimp*)"2" (typepred "y!1" )"2" (hide -1)"2" "1/y!1" )"1" "1" "cosh(x!1)" )"1" rewrite "div_cancel4" )"1" "x!1" )"1" "x!1" )"1" rewrite "div_cancel3" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "both_sides_div_pos_le2" "pz" "1" "py" "y!1" "px" "1" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nzreal" nil )"posreal_le1" hyperbolic nil )"bool" functions nil )nil hyperbolic nil )"bool" functions nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )"posreal_ge1" hyperbolic nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil reals nil )"boolean" notequal nil )nil real_props nil )"posreal_ge1" hyperbolic nil )nil hyperbolic nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" functions nil )"posrat" nil )nil real_props nil )nil real_props nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"posreal_le1" hyperbolic nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"posreal" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil hyperbolic nil )"bool" real_fun_preds "reals/" )nil hyperbolic nil )"posreal_le1" hyperbolic nil ))nil 3270131384"" (expand "posreal_coth" )"" (expand "coth" )"" (lemma "tanh_bij" )"" (expand "bijective?" )"" (flatten -1)"" (lemma "tanh_strict_increasing" )"" (expand "strict_increasing?" )"" (split 1)"1" (hide -3)"1" (expand "injective?" )"1" (skosimp*)"1" (typepred "x1!1" )"1" (typepred "x2!1" )"1" (hide -1 -3)"1" "0" "x1!1" )"1" "0" "x2!1" )"1" rewrite "tanh_0" )"1" expand ">" (-1 -2))"1" replace -1)"1" replace -2)"1" "cross_mult" "x" "1" "y" "1" "n0x" "tanh(x1!1)" "n0y" "tanh(x2!1)" ))"1" replace -4 -1)"1" "1" "1" "x1!1" "x2!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2)"2" (expand "surjective?" )"2" (skosimp*)"2" (typepred "y!1" )"2" "posreal_div_posreal_is_posreal" "px" "1" "py" "y!1" ))"2" "both_sides_div_pos_gt2" "pz" "1" "py" "y!1" "px" "1" ))"2" replace -3 -1)"2" "2" "1/y!1" )"1" "1" "trichotomy" "x" "x!1" ))"1" "1" "x!1" )"1" rewrite "div_cancel4" "1" rewrite "div_cancel3" "1" assert )nil nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" replace -1)"2" rewrite "tanh_0" )"2" (assert ) nil nil ))nil ))nil )"3" "x!1" "0" )"3" rewrite "tanh_0" )"3" expand ">" -1)"3" replace -1)"3" replace -6)"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nzreal" nil )"real_abs_gt1" hyperbolic nil )"bool" functions nil )nil hyperbolic nil )"bool" functions nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real_abs_lt1" hyperbolic nil )nil hyperbolic nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"boolean" notequal nil )nil real_props nil )nil hyperbolic nil )"bool" functions nil )nil hyperbolic nil )nil real_props nil )nil real_props nil )"posrat" nil )nil real_props nil )"real" hyperbolic nil )nil real_axioms nil )"posreal_gt1" hyperbolic nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil real_types nil )"bool" real_fun_preds "reals/" )nil hyperbolic nil )"posreal_gt1" hyperbolic nil ))nil 3253394002"" (skosimp*)"" (lemma "sinh_bij" )"" "bijective_inverse" "f" "sinh" "y" "x!1" "x" "asinh(x!1)" ))"1" (flatten -1)"1" (hide -1)"1" (split -1)"1" (assert ) nil nil )"2" (hide 2)"2" (expand "asinh" )"2" (hide -1)"2" (expand "sinh" )"2" (lemma "sqrt_pos" ("px" "1+sq(x!1)" ))"2" (case "sqrt(1 + sq(x!1)) + x!1 >0" )"1" (rewrite "div_cancel4" 1)"1" "exp_diff" "x" "0" "y" "ln(sqrt(1 + sq(x!1)) + x!1)" ))"1" rewrite "exp_0" )"1" replace -1)"1" rewrite "exp_ln" )"1" "1" "div_cancel3" "y" "sqrt(1 + sq(x!1))-x!1" "x" "1" "n0z" "sqrt(1 + sq(x!1)) + x!1" ))"1" "1" "1" "1" (assert ) nil nil )"2" "2" assert )"2" rewrite "sq_rew" )"2" rewrite "sq_rew" )"2" rewrite "sq_sqrt" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" (lemma "trichotomy" ("x" "x!1" ))"2" "1" (assert ) nil nil )"2" (assert ) nil nil )"3" "sq_gt" "nna" "sqrt(1 + sq(x!1))" "nnb" "-x!1" ))"1" rewrite "sq_sqrt" )"1" rewrite "sq_neg" )"1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil )nil hyperbolic nil )"posreal" sqrt "reals/" )"real" reals nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )nil ln_exp nil )"nzreal" nil )"posreal" nil )"posreal" sq "reals/" )nil sqrt "reals/" )nil sq "reals/" )nil real_props nil )"posreal" nil )nil ln_exp nil )"odd_int" integers nil )nil ln_exp nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil )nil real_props nil )"boolean" notequal nil )nil reals nil )"[numfield, numfield -> numfield]" number_fields nil )"real" ln_exp nil )"{py | x = ln(py)}" ln_exp nil )"[numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )nil real_axioms nil )nil sq "reals/" )nil sq "reals/" )"posreal" nil )nil sqrt "reals/" )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_real" sq "reals/" )nil function_inverse nil )"real" hyperbolic nil )nil booleans nil )"bool" functions nil )"real" hyperbolic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))nil 3253392586"" (skosimp*)"" (lemma "asinh_alt_def" ("x" "sinh(x!1)" ))"" (lemma "sinh_bij" )"" (lemma "comp_inverse_left" ("f" "sinh" "x" "x!1" ))"1" (assert ) nil nil ) ("2" (propax) nil nil )) nil ))nil ))nil ))nil )"real" hyperbolic nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic nil )"bool" functions nil )nil booleans nil )nil function_inverse nil )nil hyperbolic nil ))nil 3253392742"" (skosimp*)"" (lemma "sinh_bij" )"" (expand "sinh" )"" (hide -1)"" (rewrite "div_cancel3" )"" (lemma "exp_diff" ("x" "0" "y" "asinh(x!1)" ))"" (rewrite "exp_0" )"" (replace -1 1)"" (hide -1)"" (expand "asinh" )"" (lemma "sqrt_pos" ("px" "1+sq(x!1)" ))"" (case "sqrt(1 + sq(x!1)) + x!1 > 0" )"1" (rewrite "exp_ln" )"1" (field 1)"1" "sqrt_def" )"1" "1 + sq(x!1)" )"1" assert )"1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "trichotomy" ("x" "x!1" ))"2" "1" (assert ) nil nil )"2" (assert ) nil nil )"3" "sq_gt" "nna" "sqrt(1 + sq(x!1))" "nnb" "-x!1" ))"1" rewrite "sq_neg" )"1" rewrite "sq_sqrt" )"1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil hyperbolic nil )nil ln_exp nil )"posreal" sqrt "reals/" )"posreal" nil )"real" reals nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )NOT const-decl "[bool -> bool]" booleans nil )"nzreal" nil )nil real_props nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )"posreal" nil )nil sqrt "reals/" )"(strict_total_order?[real])" real_props nil )nil ln_exp nil )"(total_order?[real])" nil )nil real_axioms nil )nil sq "reals/" )nil sqrt "reals/" )nil sq "reals/" )"nonneg_real" sq "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sqrt "reals/" )"posreal" nil )"odd_int" integers nil )nil ln_exp nil )"real" reals nil )"[numfield -> numfield]" number_fields nil )"real" hyperbolic nil )"{py | x = ln(py)}" ln_exp nil )"real" ln_exp nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )"real" reals nil )"real" reals nil )"real" hyperbolic nil ))nil 3253392937"" (lemma "sinh_strict_increasing" )"" (expand "strict_increasing?" )"" (skosimp*)"" (lemma "trich_lt" ("x" "asinh(x!1)" "y" "asinh(y!1)" ))"" (split -1)"1" (propax) nil nil )"2" (lemma "sinh_asinh" ("x" "x!1" ))"2" (lemma "sinh_asinh" ("x" "y!1" ))"2" (assert ) nil nil )) nil ))nil )"3" (inst - "asinh(y!1)" "asinh(x!1)" )"3" (rewrite "sinh_asinh" )"3" (rewrite "sinh_asinh" ) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" real_fun_preds "reals/" )"real" hyperbolic nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )nil hyperbolic nil )"(strict_total_order?[real])" real_props nil )nil hyperbolic nil ))nil 3253392824"" (lemma "sinh_bij" )"" (lemma "bij_inv_is_bij" ("f" "sinh" ))"" (lemma "extensionality" ("f" "asinh" "g" "inverse(sinh)" ))"" (split -1)"1" (assert ) nil nil )"2" (hide 2)"2" (skosimp*)"2" (lemma "asinh_alt_def" ("x" "x!1" ))"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" hyperbolic nil )nil function_inverse nil )nil hyperbolic nil )nil functions nil )"real" hyperbolic nil )"D" function_inverse nil )nil hyperbolic nil ))nil 3270360522 ("" (grind) nil nil )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 )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"odd_int" integers nil )"posint" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"bool" integers nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nonneg_int" nil ))nil 3270387408"" (skosimp*) (("" (assert ) nil nil )) nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"odd_int" integers nil )"posint" nil )"(total_order?[real])" nil )"real" reals nil ))nil 3270540315"" (skosimp*)"" (expand "atanhD" )"" (lemma "expt_nonzero" ("n0x" "1-sq(x!1)" "i" "1+2*n!1" ))"1" (assert ) nil nil )"2" (hide -1)"2" (case "x!1>=0" )"1" (lemma "sq_gt" ("nna" "1" "nnb" "x!1" ))"1" (rewrite "sq_1" ) (("1" (assert ) nil nil )) nil )"2" (propax) nil nil ))nil )"2" (lemma "sq_gt" ("nna" "1" "nnb" "-x!1" ))"1" (rewrite "sq_neg" )"1" (rewrite "sq_1" ) (("1" (assert ) nil nil )) nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" hyperbolic nil )"real" reals nil )nil sq "reals/" )nil sq "reals/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil sq "reals/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"posint" nil )"odd_int" integers nil )"real" reals nil )nil exponentiation nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"boolean" notequal nil )nil reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"nonneg_real" sq "reals/" )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )nil hyperbolic nil ))nil 3270387408"" (skosimp*) (("" (assert ) nil nil )) nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"odd_int" integers nil )"posint" nil )"(total_order?[real])" nil ))nil 3270812866"" (skosimp*) (("" (assert ) nil nil )) nil )"real" reals nil ))nil 3270812866"" (skosimp*)"" (case "1-sq(z!1)>0" )"1" (lemma "expt_pos" ("px" "1-sq(z!1)" "i" "2*n!1+3" ))"1" "posreal_times_posreal_is_posreal" "px" "2*(2*n!1+3)" "py" "(1 - sq(z!1)) ^ (2 * n!1 + 3)" ))"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil )"2" (hide -1)"2" (case "z!1>=0" )"1" (lemma "sq_gt" ("nna" "1" "nnb" "z!1" ))"1" (rewrite "sq_1" ) (("1" (assert ) nil nil )) nil )"2" (propax) nil nil ))nil )"2" (lemma "sq_gt" ("nna" "1" "nnb" "-z!1" ))"1" (rewrite "sq_1" )"1" (rewrite "sq_neg" ) (("1" (assert ) nil nil )) nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil hyperbolic nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nonneg_real" sq "reals/" )nil real_types nil )"bool" reals nil )"[numfield, 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 )"real" reals nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil real_types nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )"nonneg_int" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil )"odd_int" integers nil )nil exponentiation nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )nil real_types nil )nil sq "reals/" )nil sq "reals/" )nil sq "reals/" )"real" reals nil ))nil 3322476122"" (skosimp*)"" (mult-cases -1)"" (lemma "expt_pos" )"" (inst?)"1" (assert ) nil nil )"2" (hide 1)"2" (lemma "expt_pos" )"2" (inst?)"1" (assert ) nil nil )"2" (typepred "z!1" )"2" (hide -3)"2" (case-replace "(1 - sq(z!1)) > 0" )"1" (assert ) nil nil )"2" (hide 2)"2" (expand "sq" )"2" (mult-ineq -2 -2)"1" (assert ) nil nil )"2" (hide 3) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nonneg_int" nil )nil hyperbolic nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nonneg_real" sq "reals/" )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )"odd_int" integers nil )"posint" nil )"real" reals nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )"posint" nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real_abs_lt1" hyperbolic nil )"bool" reals nil )nil real_types nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"real" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"{r: posrat | r >= q}" nil )"{j: nonneg_int | j >= i}" nil )"{j: posint | j >= i}" nil )"(total_order?[real])" nil )nil extra_real_props nil )"odd_int" integers nil )nil exponentiation nil ))nil ))nil 3270272425"" (skosimp*)"" (lemma "atanh_taylors" ("z" "z!1" "n" "n!1" ))"" (skosimp*)"" (replace -1 1)"" (simplify 1)"" (hide -1)"" (lemma "atanh_nderiv" ("n" "3+2*n!1" ))"" (simplify -1)"" (expand "even?" -1)"" (lemma "div_cancel1" ("x" "1+n!1" "n0z" "2" ))"" (replace -1 -2)"" (replace -2 1)"" (hide -1 -2)"" (case "1-sq(z!1)>0" )"1" case "abs(z!1^(3+2*n!1))<1" )"1" rewrite "abs_div" 1)"1" rewrite "abs_mult" 1)"1" expand "abs" 1 3)"1" "expt_pos" "px" "1-sq(z!1)" "i" "3+2*n!1" ))"1" "posreal_times_posreal_is_posreal" "px" "6+4*n!1" "py" "(1 - sq(z!1)) ^ (3 + 2 * n!1)" ))"1" case "atanhND(1 + n!1)(c!1)>0" )"1" case "abs(atanhND(1 + n!1)(c!1)) <= atanhND(1 + n!1)(z!1)" )"1" case "atanhND(1 + n!1)(z!1) = factorial(2+2*n!1)*(((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1)) / (2 * (1 - sq(z!1)) ^ (3 + 2 * n!1)))" )"1" rewrite "div_mult_pos_le1" "1" expand "abs" 1 1)"1" expand "abs" -2)"1" assert )"1" "K10" "1 - sq(z!1)" )"1" "K11" "K10^(3+2*n!1)" )"1" "K12" "(1-z!1)^(3+2*n!1)+(1+z!1)^(3+2*n!1)" )"1" replace "1" "lt_times_lt_pos1" "px" "atanhND(1 + n!1)(c!1)" "y" "factorial(2 + 2 * n!1) * (K12 / (2 * K11))" "nnz" "abs(z!1 ^ (3 + 2 * n!1))" "w" "1" ))"1" replace "1" replace "1" expand "factorial" "1" "factorial(2 + 2 * n!1) * (K12 / (2 * K11)) * 1 = 3 * (factorial(2 + 2 * n!1) * (K12 / (6 * K11 + 4 * (K11 * n!1)))) + ") "1" assert )nil nil )"2" "2" "div_cancel1" "x" "factorial(2 + 2 * n!1) * (K12 / (2 * K11))" "n0z" "3+2*n!1" ))"2" replace "2" "2" "K13" "factorial(2 + 2 * n!1)" )"2" "(K13 * (K12 / (2 * K11)) / (3 + 2 * n!1))=(K13 * (K12 / (6 * K11 + 4 * (K11 * n!1))))" )"1" assert )nil nil )"2" "2" "cross_mult" "x" "K13 * (K12 / (2 * K11))" "n0x" "3+2*n!1" "y" "K13*K12" "n0y" "6 * K11 + 4 * (K11 * n!1)" ))"2" replace "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "atanhND" )"2" expand "atanhN" )"2" expand "atanhD" )"2" "cross_mult" "x" "polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1)" "n0x" "(1 - sq(z!1)) ^ (3 + 2 * n!1)" "y" "factorial(2 + 2 * n!1) * ((1 - z!1) ^ (3 + 2 * n!1) + (1 + z!1) ^ (3 + 2 * n!1))" "n0y" "2 * (1 - sq(z!1)) ^ (3 + 2 * n!1)" ))"2" replace "2" "2" "both_sides_times1" "x" "polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1) * 2" "n0z" "(1 - sq(z!1)) ^ (3 + 2 * n!1)" "y" "factorial(2 + 2 * n!1) * ")) "1" replace "1" "1" "1" "power_polynomial" "pn" "3+2*n!1" ))"1" "neg_power_polynomial" "pn" "3+2*n!1" ))"1" "(1 - z!1) ^ (3 + 2 * n!1) = polynomial(neg_power_fs(3 + 2 * n!1), 3 + 2 * n!1)(z!1)" )"1" "(1 + z!1) ^ (3 + 2 * n!1) = polynomial(power_fs(3 + 2 * n!1), 3 + 2 * n!1)(z!1)" )"1" "1" expand "polynomial" )"1" "sigma_scal[nat]" "low" "0" "high" "2+2*n!1" "a" "2" "F" "LAMBDA (i: nat): IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF)")) "1" replace "1" "1" "sigma_scal[nat]" "low" "0" "high" "3+2*n!1" "a" "factorial(2 + 2 * n!1)" "F" "LAMBDA (i: nat):power_fs(3 + 2 * n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF)" ))"1" replace "1" "1" "sigma_scal[nat]" "low" "0" "high" "3+2*n!1" "a" "factorial(2 + 2 * n!1)" "F" "LAMBDA (i: nat):neg_power_fs(3 + 2 * n!1)(i) * (IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF)" ))"1" replace "1" "1" "sigma_sum" "low" "0" "high" "3+2*n!1" "F" "LAMBDA (i: nat): LAMBDA (i: nat):IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))(i)" "G" "LAMBDA (i: nat): LAMBDA (i: nat):IF i = 0 THEN 1 ELSE z!1 ^ i ENDIF))(i)")) "1" replace "1" "1" "1" "sigma_last" "low" "0" "high" "3+2*n!1" "F" "LAMBDA (i_1: nat): IF i_1 = 0 THEN 1 ELSE z!1 ^ i_1 ENDIF))IF i_1 = 0 THEN 1 ELSE z!1 ^ i_1 ENDIF))")) "1" assert )"1" replace "1" "1" expand "neg_power_fs" "1" expand "power_fs" "1" "(-1) ^ (3 + 2 * n!1)=-1" )"1" "sigma(0, 2 + 2 * n!1, LAMBDA (i_1: nat):IF i_1 = 0 THEN 1 ELSE z!1 ^ i_1 ENDIF))IF i_1 = 0 THEN 1 ELSE z!1 ^ i_1 ENDIF)))LAMBDA (i_1: nat):IF i_1 = 0 THEN 1 ELSE z!1 ^ i_1 ENDIF))IF i_1 = 0 THEN 1 ELSE z!1 ^ i_1 ENDIF)))") "1" "1" "sigma_eq[nat]" "low" "0" "high" "2+2*n!1" "F" "LAMBDA (i_1: nat): IF i_1 = 0 THEN 1 ELSE z!1 ^ i_1 ENDIF))" "G" "LAMBDA (i_1: nat): IF i_1 = 0 THEN 1 ELSE z!1 ^ i_1 ENDIF))IF i_1 = 0 THEN 1 ELSE z!1 ^ i_1 ENDIF))")) "1" "1" nil nil )"2" "2" "2" expand "atanhF" )"2" expand "power_fs" )"2" expand "neg_power_fs" )"2" "K400" "factorial(2 + 2 * n!1)" )"2" "K401" "C(3 + 2 * n!1, n!2)" )"2" "K402" "(IF n!2 = 0 THEN 1 ELSE z!1 ^ n!2 ENDIF)" )"2" case "even?(n!2)" )"1" "even_or_odd" "x" "n!2" ))"1" assert )"1" expand "even?" )"1" "1" replace "1" "expt_times" "n0x" "-1" "i" "2" "j" "j!1" ))"1" "(-1)^2=1" )"1" rewrite "expt_1i" )"1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "even_or_odd" "2" assert )"2" expand "odd?" )"2" "2" replace "2" "expt_plus" "n0x" "-1" "i" "1" "j" "2*j!1" ))"2" rewrite "expt_x1" )"2" "expt_times" "n0x" "-1" "i" "2" "j" "j!1" ))"2" "(-1)^2=1" )"1" rewrite "expt_1i" )"1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "K300" "sigma(0, 2 + 2 * n!1, LAMBDA (i_1: nat):IF i_1 = 0 THEN 1 ELSE z!1 ^ i_1 ENDIF))IF i_1 = 0 THEN 1 ELSE z!1 ^ i_1 ENDIF)))") nil nil ))nil ))nil )"2" "2" "expt_plus" "n0x" "-1" "i" "1" "j" "2+2*n!1" ))"2" rewrite "expt_x1" )"2" "expt_times" )"2" "2" "1+n!1" "-1" )"2" replace "2" "(-1)^2=1" )"1" rewrite "expt_1i" "1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" nil nil ))nil ))nil ))nil )"2" replace "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" assert )nil nil ))nil )"2" "2" expand "abs" 1)"2" assert )"2" "2" "2" expand "atanhND" )"2" expand "atanhN" )"2" expand "atanhD" )"2" case "1-sq(c!1)>0" )"1" "expt_pos" "px" "1-sq(c!1)" "i" "3+2*n!1" ))"1" rewrite "div_mult_pos_le1" "1" "div_mult_pos_le2" "z" "polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(z!1)*(1 - sq(c!1)) ^ (3 + 2 * n!1)" "py" "(1 - sq(z!1)) ^ (3 + 2 * n!1)" "x" "polynomial(atanhF(1 + n!1), 2 + 2 * n!1)(c!1)" ))"1" replace "1" "1" "even_polynomial" "a" "atanhF(1 + n!1)" "n" "1 + n!1" ))"1" case "even_fs?(atanhF(1 + n!1))" )"1" replace "1" "c!1" )"1" "z!1" )"1" replace "1" replace "1" "1" case "FORALL (x:real): x^2 = sq(x)" )"1" "c!1" )"1" "z!1" )"1" replace "1" replace "1" case "sq(c!1)<=sq(z!1)" )"1" "both_sides_expt_pos_le" "px" "1-sq(z!1)" "py" "1-sq(c!1)" "pm" "3+2*n!1" ))"1" assert )"1" case "FORALL (n:nat): polynomial(LAMBDA (i: nat): atanhF(1 + n!1)(2 * i), n)(sq(c!1)) > 0" )"1" "1+n!1" )"1" case "FORALL (n:nat): polynomial(LAMBDA (i: nat): atanhF(1 + n!1)(2 * i), n)(sq(c!1)) LAMBDA (i: nat): atanhF(1 + n!1)(2 * i), n)(sq(z!1))") "1" "1+n!1" )"1" "le_times_le_pos" "nnx" "polynomial(LAMBDA (i: nat): atanhF(1 + n!1)(2 * i), 1 + n!1)(sq(c!1))" "nnz" "(1 - sq(z!1)) ^ (3 + 2 * n!1)" "y" "polynomial(LAMBDA (i: nat): atanhF(1 + n!1)(2 * i), 1 + n!1)(sq(z!1))" "w" "(1 - sq(c!1)) ^ (3 + 2 * n!1)" ))"1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" "2" "n" )"1" rewrite "polynomial_n0" )"1" "1" assert )nil nil ))nil ))nil )"2" "2" expand "polynomial" )"2" expand "sigma" "2" "K100" "sigma(0, j!1, LAMBDA (i_1: nat):IF i_1 = 0 THEN 1 ELSE sq(c!1) ^ i_1 ENDIF))") "2" "K101" "sigma(0, j!1, LAMBDA (i_1: nat):IF i_1 = 0 THEN 1 ELSE sq(z!1) ^ i_1 ENDIF))") "2" "sq(c!1)=0" )"1" expand "^" "1" expand "expt" "1" "expt_pos" "px" "sq(z!1)" "i" "1+j!1" ))"1" expand "atanhF" )"1" expand "odd?" )"1" case "j!1>n!1" )"1" assert )nil nil )"2" assert )"2" "posreal_times_posreal_is_posreal" "px" "factorial(2 + 2 * n!1) * C(3 + 2 * n!1, 2 + 2 * j!1)" "py" "sq(z!1) ^ (1 + j!1)" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "both_sides_expt_pos_le" "px" "sq(c!1)" "py" "sq(z!1)" "pm" "1+j!1" ))"1" case "0 <= atanhF(1 + n!1)(2 + 2 * j!1)" )"1" expand "<=" "1" "1" "both_sides_times_pos_le1" "x" "sq(c!1) ^ (1 + j!1)" "y" "sq(z!1) ^ (1 + j!1)" "pz" "atanhF(1 + n!1)(2 + 2 * j!1)" ))"1" assert )nil nil )"2" assert )nil nil ))nil )"2" replace "2" assert )nil nil ))nil ))nil ))nil )"2" "2" expand "atanhF" )"2" expand "odd?" )"2" case "j!1>n!1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "sq(c!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n" )"1" rewrite "polynomial_n0" )"1" "1" expand "atanhF" )"1" expand "odd?" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "polynomial" )"2" expand "sigma" "2" "K103" "sigma(0, j!1, LAMBDA (i_1: nat):IF i_1 = 0 THEN 1 ELSE sq(c!1) ^ i_1 ENDIF))") "2" "sq(c!1)" )"2" expand ">=" "2" expand "<=" "2" "1" "expt_pos" "px" "sq(c!1)" "i" "1+j!1" ))"1" expand "atanhF" )"1" expand "odd?" )"1" case "j!1>n!1" )"1" assert )nil nil )"2" assert )"2" "posreal_times_posreal_is_posreal" "px" "factorial(2 + 2 * n!1) * C(3 + 2 * n!1, 2 + 2 * j!1)" "py" "sq(c!1) ^ (1 + j!1)" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" replace "2" expand "^" "2" expand "expt" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "c!1" )"2" "trichotomy" "x" "z!1" ))"2" "1" assert )"1" "1" "sq_lt" "nna" "c!1" "nnb" "z!1" ))"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil )"3" "sq_lt" "nna" "-c!1" "nnb" "-z!1" ))"1" rewrite "sq_neg" )"1" rewrite "sq_neg" )"1" assert )nil nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "even_fs?" )"2" expand "atanhF" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "2" case "c!1>=0" )"1" "sq_gt" "nna" "1" "nnb" "c!1" ))"1" rewrite "sq_1" )"1" assert )nil nil ))nil )"2" nil nil ))nil )"2" "sq_gt" "nna" "1" "nnb" "-c!1" ))"1" rewrite "sq_1" )"1" rewrite "sq_neg" )"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "atanhND" )"2" expand "atanhN" )"2" expand "atanhD" )"2" "2" "c!1=0" )"1" rewrite "polynomial_x0" )"1" expand "atanhF" )"1" expand "odd?" )"1" rewrite "C_0" )"1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "even_polynomial" "a" "atanhF(1 + n!1)" "n" "1 + n!1" "x" "c!1" ))"2" "1" replace "1" "1" case "c!1^2>0" )"1" expand "polynomial" )"1" "KC" "c!1^2" )"1" case "FORALL (n:nat): sigma(0, n, LAMBDA (i_1: nat):IF i_1 = 0 THEN 1 ELSE KC ^ i_1 ENDIF))") "1" "1+n!1" )"1" "SS" "sigma(0, 1 + n!1, LAMBDA (i_1: nat):IF i_1 = 0 THEN 1 ELSE KC ^ i_1 ENDIF))") "1" case "(1 - sq(c!1)) ^ (3 + 2 * n!1) > 0" )"1" "1" assert )nil nil ))nil )"2" "c!1" )"2" "2" "expt_pos_aux" )"2" "3+2*n!1" "1 - sq(c!1)" )"1" expand "^" )"1" nil nil ))nil )"2" "2" "neg_pos_sq_lt" )"2" "2" rewrite "sq_1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n" )"1" expand "sigma" "1" expand "atanhF" "1" expand "odd?" "1" rewrite "C_0" )
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 1.94 Sekunden
(vorverarbeitet am 2026-04-27)
¤ *© Formatika GbR, Deutschland
