(hyperbolicnil 3477842243"" (expand "not_one_element?" )"" (skosimp*)"" (inst-cp + "x!1/2" )"" (inst + "1/2" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posrat" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal 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 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 )"(strict_total_order?[real])" real_props nil )"bool" deriv_domain_def "analysis/" ))nil 3477842295"" (expand "not_one_element?" )"" (skosimp*) (("" (inst + "x!1+1" ) (("" (assert ) nil nil )) nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 )"real" reals nil )"(strict_total_order?[real])" real_props nil )"bool" deriv_domain_def "analysis/" ))nil 3477842234"" (expand "connected?" )"" (skosimp*) (("" (assert ) nil nil )) nil )) nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"bool" deriv_domain_def "analysis/" ))nil 3477842343"" (expand "connected?" ) (("" (propax) nil nil )) nil )"bool" deriv_domain_def "analysis/" ))nil 3477842313"" (lemma "deriv_domain_open" ) (("" (inst - "-1" "1" ) nil nil ))nil )"odd_int" integers nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil deriv_domain "analysis/" ))nil 3477842351"" (expand "deriv_domain?" )"" (skosimp*)"" (typepred "x!1" )"" (inst + "e!1/2" ) (("" (grind) nil nil )) nil )) nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"boolean" notequal nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )"{y: posreal | y >= x}" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )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 )"bool" deriv_domain_def "analysis/" )"real" reals nil ))nil 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" (assert ) (("1" (cross-mult 1) 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 )"even_int" integersnil )"rat" rationals nil )"(total_order?[real])" nil )"real" reals nil )nil extra_real_props 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 )"[numfield, numfield -> numfield]" number_fields 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 )"boolean" notequal 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 )nil abs_lems "reals/" )"real" reals nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )"(total_order?[real])" 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 )"(total_order?[real])" 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 )nil abs_lems "reals/" )"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 3270127577"" (lemma "deriv_domain_real" ) (("" (propax) nil nil )) nil )nil deriv_domain "analysis/" ))nil 3270127577"" (skosimp*) (("" (inst + "x!1+1" ) (("" (assert ) nil nil )) nil ))nil )nil deriv_domain "analysis/" ))nil 3352437912"" (expand "sinh" )"" (lemma "identity_derivable_fun[real]" )"" (expand "I" )"" "neg_derivable_fun[real]" ("f" "LAMBDA (x: real): x" ))"" (assert )"" (expand "-" )"" (lemma "exp_deriv" )"" (flatten -1)"" (hide -2)"" "composition_derivable_fun[real,real]" "f" "LAMBDA (x_1: real): -x_1" "g" "exp" ))"1" (assert )"1" (expand "o" )"1" "diff_derivable_fun[real]" "f1" "exp" "f2" "LAMBDA (x: real): exp(-x)" ))"1" (assert )"1" expand "-" )"1" "scal_derivable_fun[real]" "f" "LAMBDA (x: real): exp(x) - exp(-x)" "b" "1/2" ))"1" assert )"1" expand "*" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst + "x!1+1" ) (("2" (assert ) nil nil ))nil ))nil )"3" (lemma "deriv_domain_real" )"3" (propax) 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 derivatives "analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )"{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]" number_fields nil )nil number_fields nil )nil chain_rule "analysis/" )"real" reals nil )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def "analysis/" )"T3" function_props nil )"posrat" nil )nil derivatives "analysis/" )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[T -> real]" real_fun_ops "reals/" )"posreal" nil )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )nil ln_exp nil )"real" reals nil )"(bijective?[T, T])" identity nil )"real" hyperbolic nil )"real" reals nil ))nil )nil 3270135166"" (expand "sinh" )"" (lemma "identity_derivable_fun[real]" )"" (expand "I" )"" (lemma "neg_derivable_fun" ("f" "LAMBDA (x: real): x" ))"" (assert )"" (expand "-" )"" (lemma "exp_deriv" )"" (flatten -1)"" (hide -2)"" "composition_derivable_fun" "f" "LAMBDA (x_1: real): -x_1" "g" "exp" ))"" (assert )"" (expand "o" )"" "diff_derivable_fun" "f1" "exp" "f2" "LAMBDA (x: real): exp(-x)" ))"" (assert )"" expand "-" )"" "scal_derivable_fun" "f" "LAMBDA (x: real): exp(x) - exp(-x)" "b" "1/2" ))"" assert )"" expand "*" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil derivatives "analysis/" )nil derivatives "analysis/" )"{py | x = ln(py)}" ln_exp nil )"real" ln_exp nil )nil chain_rule "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil ln_exp nil ))nil 3352437975"" (expand "cosh" )"" (lemma "identity_derivable_fun[real]" )"" (expand "I" )"" "neg_derivable_fun[real]" ("f" "LAMBDA (x: real): x" ))"" (assert )"" (expand "-" )"" (lemma "exp_deriv" )"" (flatten -1)"" (hide -2)"" "composition_derivable_fun[real,real]" "f" "LAMBDA (x_1: real): -x_1" "g" "exp" ))"1" (assert )"1" (expand "o" )"1" "sum_derivable_fun[real]" "f1" "exp" "f2" "LAMBDA (x: real): exp(-x)" ))"1" (assert )"1" expand "+" )"1" "scal_derivable_fun[real]" "f" "LAMBDA (x_1: real): exp(x_1) + exp(-x_1)" "b" "1/2" ))"1" assert )"1" expand "*" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst + "x!1+1" ) (("2" (assert ) nil nil ))nil ))nil )"3" (lemma "deriv_domain_real" )"3" (propax) 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 derivatives "analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )"{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]" number_fields nil )nil number_fields nil )nil chain_rule "analysis/" )"real" reals nil )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def "analysis/" )"T3" function_props nil )"posrat" nil )nil derivatives "analysis/" )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[T -> real]" real_fun_ops "reals/" )"posreal" nil )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )nil ln_exp nil )"posreal" nil )"(bijective?[T, T])" identity nil )"posreal_ge1" hyperbolic nil )"posreal" nil ))nil )nil 3270138126"" (expand "cosh" )"" (lemma "identity_derivable_fun[real]" )"" (expand "I" )"" (lemma "neg_derivable_fun" ("f" "LAMBDA (x: real): x" ))"" (assert )"" (expand "-" )"" (lemma "exp_deriv" )"" (flatten -1)"" (hide -2)"" "composition_derivable_fun" "f" "LAMBDA (x_1: real): -x_1" "g" "exp" ))"" (assert )"" (expand "o" )"" "sum_derivable_fun" "f1" "exp" "f2" "LAMBDA (x: real): exp(-x)" ))"" (assert )"" expand "+" )"" "scal_derivable_fun" "f" "LAMBDA (x_1: real): exp(x_1) + exp(-x_1)" "b" "1/2" ))"" assert )"" expand "*" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil derivatives "analysis/" )nil derivatives "analysis/" )"{py | x = ln(py)}" ln_exp nil )"real" ln_exp nil )nil chain_rule "analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )nil ln_exp nil ))nil 3352439298"" (expand "tanh" )"" (lemma "sinh_derivable2" )"" (lemma "cosh_derivable2" )"" (lemma "div_derivable_fun[real]" ("f" "sinh" "g" "cosh" ))"1" (assert )"1" (expand "/" ) (("1" (propax) nil nil )) nil )) nil )"2" (hide-all-but 1)"2" (skosimp*)"2" (typepred "cosh(x1!1)" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 )"posreal_ge1" hyperbolic nil )nil hyperbolic nil )"bool" reals nil )nil booleans nil )nil reals nil )"boolean" notequal nil )"real" hyperbolic nil )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )nil hyperbolic nil )"real_abs_lt1" hyperbolic nil )"real" reals nil ))nil )nil 3270138327"" (expand "tanh" )"" (lemma "sinh_derivable2" )"" (lemma "cosh_derivable2" )"" (lemma "div_derivable_fun" ("f" "sinh" "g" "cosh" ))"1" (assert )"1" (expand "/" ) (("1" (propax) nil nil )) nil )) nil )"2" (hide-all-but 1)"2" (skosimp*)"2" (typepred "cosh(x1!1)" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil derivatives "analysis/" ))nil 3270127577"" (lemma "sinh_derivable2" ) (("" (propax) nil nil )) nil )nil hyperbolic nil )) shostak))nil 3352439354"" (lemma "exp_deriv" )"" (flatten -1)"" (expand "sinh" )"" (expand "cosh" )"" (lemma "identity_derivable_fun[real]" )"" (lemma "deriv_id_fun[real]" )"" (expand "I" )"" "neg_derivable_fun[real]" "f" "LAMBDA (x: real): x" ))"" (assert )"" (expand "-" )"" "deriv_neg_fun[real]" "ff" "LAMBDA (x: real): x" ))"" (replace -3)"" (expand "-" )"" "composition_derivable_fun[real,real]" "f" "LAMBDA (x: real): -x" "g" "exp" ))"" assert )"" expand "o" )"" "deriv_comp_fun[real,real]" "ff" "LAMBDA (x: real): -x" "gg" "exp" ))"" replace -8)"" replace -3)"" expand "o" )"" expand "*" )"" "diff_derivable_fun[real]" "f1" "exp" "f2" "LAMBDA (x: real): exp(-x)" ))"" assert )"" expand "-" )"" "deriv_diff_fun[real]" "ff1" "exp" "ff2" "LAMBDA (x: real): exp(-x)" ))"" replace -10)"" replace -3)"" expand "-" )"" "scal_derivable_fun[real]" "f" "LAMBDA (x_1: real): exp(x_1) - exp(-x_1)" "b" "1/2" ))"" assert )"" expand "*" )"" "deriv_scal_fun[real]" "ff" "LAMBDA (x_1: real): exp(x_1) - exp(-x_1)" "b" "1/2" ))"" replace "" expand "*" )"" 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 )"posreal_ge1" hyperbolic nil )nil derivatives "analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )nil chain_rule "analysis/" )nil number_fields nil )"[numfield -> numfield]" number_fields 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 )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def "analysis/" )"T3" function_props nil )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )"posreal" nil )"[T -> real]" real_fun_ops "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil derivatives "analysis/" )"posrat" nil )nil derivatives "analysis/" )"nzreal" nil )"[T -> real]" real_fun_ops "reals/" )nil chain_rule "analysis/" )"odd_int" integers nil )nil derivatives "analysis/" )"bool" derivatives "analysis/" )nil booleans nil )nil derivatives "analysis/" )"real" reals nil )"posreal" nil )"real" reals nil )"posreal" nil )"(bijective?[T, T])" identity nil )nil derivatives "analysis/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" hyperbolic nil )nil ln_exp nil ))nil )nil 3270138870"" (lemma "exp_deriv" )"" (flatten -1)"" (expand "sinh" )"" (expand "cosh" )"" (lemma "identity_derivable_fun[real]" )"" (lemma "deriv_id_fun[real]" )"" (expand "I" )"" (expand "const_fun" )"" "neg_derivable_fun" "f" "LAMBDA (x: real): x" ))"" (assert )"" (expand "-" )"" "deriv_neg_fun" "ff" "LAMBDA (x: real): x" ))"" (replace -3)"" (expand "-" )"" "composition_derivable_fun" "f" "LAMBDA (x: real): -x" "g" "exp" ))"" assert )"" expand "o" )"" "deriv_comp_fun" "ff" "LAMBDA (x: real): -x" "gg" "exp" ))"" replace -8)"" replace -3)"" expand "o" )"" expand "*" )"" "diff_derivable_fun" "f1" "exp" "f2" "LAMBDA (x: real): exp(-x)" ))"" assert )"" expand "-" )"" "deriv_diff_fun" "ff1" "exp" "ff2" "LAMBDA (x: real): exp(-x)" ))"" replace -10)"" replace -3)"" expand "-" )"" "scal_derivable_fun" "f" "LAMBDA (x_1: real): exp(x_1) - exp(-x_1)" "b" "1/2" ))"" assert )"" expand "*" )"" "deriv_scal_fun" "ff" "LAMBDA (x_1: real): exp(x_1) - exp(-x_1)" "b" "1/2" ))"" replace "" expand "*" )"" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil chain_rule "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )"{py | x = ln(py)}" ln_exp nil )"real" ln_exp nil )nil chain_rule "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil ln_exp nil ))nil 3270127577"" (lemma "cosh_derivable2" ) (("" (propax) nil nil )) nil )nil hyperbolic nil )) shostak))nil 3352442863"" (expand "cosh" )"" (expand "sinh" )"" (lemma "exp_deriv" )"" (flatten -1)"" (lemma "identity_derivable_fun[real]" )"" (lemma "deriv_id_fun[real]" )"" (expand "I" )"" (expand "const_fun" )"" "neg_derivable_fun[real]" "f" "LAMBDA (x: real): x" ))"" (assert )"" (expand "-" )"" "deriv_neg_fun[real]" "ff" "LAMBDA (x: real): x" ))"" (replace -3)"" (expand "-" )"" "composition_derivable_fun[real,real]" "f" "LAMBDA (x_1: real): -x_1" "g" "exp" ))"1" assert )"1" expand "o" )"1" "deriv_comp_fun[real,real]" "ff" "LAMBDA (x_1: real): -x_1" "gg" "exp" ))"1" replace -8)"1" replace -3)"1" expand "o" )"1" expand "*" )"1" "sum_derivable_fun[real]" "f1" "exp" "f2" "LAMBDA (x: real): exp(-x)" ))"1" assert )"1" expand "+" )"1" "deriv_sum_fun[real]" "ff1" "exp" "ff2" "LAMBDA (x: real): exp(-x)" ))"1" replace -10)"1" replace -3)"1" expand "+" )"1" "scal_derivable_fun[real]" "f" "LAMBDA (x_1: real): exp(x_1) + exp(-x_1)" "b" "1/2" ))"1" assert )"1" expand "*" )"1" "deriv_scal_fun[real]" "ff" "LAMBDA (x_1: real): exp(x_1) + exp(-x_1)" "b" "1/2" ))"1" replace "1" expand "*" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1+1" )"2" (assert ) nil nil ))nil ))nil )"3" "deriv_domain_real" )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" hyperbolic nil )nil derivatives "analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )nil chain_rule "analysis/" )nil number_fields nil )"[numfield -> numfield]" number_fields 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 )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def "analysis/" )"T3" function_props nil )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )nil derivatives "analysis/" )"posreal" nil )"[T -> real]" real_fun_ops "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil derivatives "analysis/" )"posrat" nil )nil derivatives "analysis/" )"nzreal" nil )"[T -> real]" real_fun_ops "reals/" )nil chain_rule "analysis/" )"odd_int" integers nil )nil derivatives "analysis/" )"bool" derivatives "analysis/" )nil booleans nil )nil derivatives "analysis/" )"posreal" nil )"real" reals nil )"posreal" nil )"real" reals nil )"(bijective?[T, T])" identity nil )nil derivatives "analysis/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil ln_exp nil )"posreal_ge1" hyperbolic nil ))nil )nil 3270139324"" (expand "cosh" )"" (expand "sinh" )"" (lemma "exp_deriv" )"" (flatten -1)"" (lemma "identity_derivable_fun[real]" )"" (lemma "deriv_id_fun[real]" )"" (expand "I" )"" (expand "const_fun" )"" "neg_derivable_fun" "f" "LAMBDA (x: real): x" ))"" (assert )"" (expand "-" )"" "deriv_neg_fun" "ff" "LAMBDA (x: real): x" ))"" (replace -3)"" (expand "-" )"" "composition_derivable_fun" "f" "LAMBDA (x_1: real): -x_1" "g" "exp" ))"" assert )"" expand "o" )"" "deriv_comp_fun" "ff" "LAMBDA (x_1: real): -x_1" "gg" "exp" ))"" replace -8)"" replace -3)"" expand "o" )"" expand "*" )"" "sum_derivable_fun" "f1" "exp" "f2" "LAMBDA (x: real): exp(-x)" ))"" assert )"" expand "+" )"" "deriv_sum_fun" "ff1" "exp" "ff2" "LAMBDA (x: real): exp(-x)" ))"" replace -10)"" replace -3)"" expand "+" )"" "scal_derivable_fun" "f" "LAMBDA (x_1: real): exp(x_1) + exp(-x_1)" "b" "1/2" ))"" assert )"" expand "*" )"" "deriv_scal_fun" "ff" "LAMBDA (x_1: real): exp(x_1) + exp(-x_1)" "b" "1/2" ))"" replace "" expand "*" )"" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil chain_rule "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )"{py | x = ln(py)}" ln_exp nil )"real" ln_exp nil )nil chain_rule "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil ln_exp nil ))nil 3270127577"" (lemma "tanh_derivable2" ) (("" (propax) nil nil )) nil )nil hyperbolic nil )) shostak))nil 3352442896"" (lemma "sinh_derivable2" )"" (lemma "cosh_derivable2" )"" (lemma "deriv_sinh" )"" (lemma "deriv_cosh" )"" (expand "tanh" )"" (expand "sech" )"" (expand "*" )"" "div_derivable_fun[real]" "f" "sinh" "g" "cosh" ))"1" (assert )"1" "deriv_div_fun[real]" "ff" "sinh" "gg" "cosh" ))"1" (expand "/" )"1" (replace -3)"1" (replace -4)"1" (expand "*" )"1" expand "-" )"1" replace -1)"1" "1" "extensionality" "f" "LAMBDA (x: real): " "g" "LAMBDA (x_1: real): 1 / cosh(x_1) * (1 / cosh(x_1))" ))"1" "1" (propax) nil nil )"2" "2" "2" rewrite "sq_rew" )"2" rewrite "sq_rew" )"2" rewrite "sq_rew" )"2" rewrite "sq_div" )"2" rewrite "cosh_sinh_one" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "cosh(x!1)" )"2" rewrite "sq_rew" )"2" "sq_nz_pos" "nz" "cosh(x!1)" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (typepred "cosh(x1!1)" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil hyperbolic nil )nil hyperbolic 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 )"posreal_ge1" hyperbolic nil )nil hyperbolic nil )"bool" reals nil )nil booleans nil )nil reals nil )"boolean" notequal nil )"real" hyperbolic nil )nil derivatives "analysis/" )nil derivatives "analysis/" )"bool" derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil functions nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil sq "reals/" )"real" reals nil )"odd_int" integers nil )"posreal" sq "reals/" )nil hyperbolic nil )nil sq "reals/" )nil sq "reals/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil sq "reals/" )NOT const-decl "[bool -> bool]" booleans nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"nzreal" nil )"nzreal" nil )"[T -> real]" real_fun_ops "reals/" )"real_abs_lt1" hyperbolic nil )nil hyperbolic nil )nil hyperbolic nil ))nil )nil 3270138468"" (lemma "sinh_derivable2" )"" (lemma "cosh_derivable2" )"" (lemma "deriv_sinh" )"" (lemma "deriv_cosh" )"" (expand "tanh" )"" (expand "sech" )"" (expand "*" )"" "div_derivable_fun" ("f" "sinh" "g" "cosh" ))"1" (assert )"1" "deriv_div_fun" ("ff" "sinh" "gg" "cosh" ))"1" (expand "/" )"1" (replace -3)"1" (replace -4)"1" (expand "*" )"1" expand "-" )"1" replace -1)"1" "1" "extensionality" "f" "LAMBDA (x: real): " "g" "LAMBDA (x_1: real): 1 / cosh(x_1) * (1 / cosh(x_1))" ))"1" "1" (propax) nil nil )"2" "2" "2" rewrite "sq_rew" )"2" rewrite "sq_rew" )"2" rewrite "sq_rew" )"2" rewrite "sq_div" )"2" rewrite "sq_1" )"2" rewrite "cosh_sinh_one" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "cosh(x!1)" )"2" rewrite "sq_rew" )"2" "sq_nz_pos" "nz" "cosh(x!1)" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (typepred "cosh(x1!1)" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (skosimp*)"2" (typepred "cosh(x1!1)" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil sq "reals/" )nil sq "reals/" )nil sq "reals/" )nil sq "reals/" ))nil 3271096134 ("" (grind) nil nil ) nil nil 3374502269 ("" (subtype-tcc) nil nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"boolean" notequal nil ))nil ))nil 3445352631"" (expand "connected?" ) (("" (propax) nil nil )) nil )"bool" deriv_domain_def "analysis/" )) nil )nil 3271096155"" (skosimp*)"" (lemma "deriv_sinh" )"" (lemma "deriv_cosh" )"" (lemma "cosh_derivable2" )"" (lemma "sinh_derivable2" )"" (expand "derivable_n_times?" )"" (replace -4)"" (replace -1)"" case "FORALL (n:nat): derivable_n_times[real](cosh, 2 * n)" )"1" (inst - "1+n!1" ) (("1" (assert ) 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" replace -4)"2" replace -5)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak))nil 3471688886"" (skosimp*) (("" (typepred "n!1" ) (("" (assert ) nil nil )) nil ))nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals 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 )"posint" nil )"odd_int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil ))nil ))nil 3445352988"" (skosimp*)"" "Taylors[real]" "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[real]" "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 )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"real" hyperbolic nil )nil taylors "analysis/" )"even_int" integersnil )"posint" nil )"even_int" integersnil )nil naturalnumbers nil )"int" hyperbolic nil )nil nth_derivatives"analysis/" )"bool" integers nil )"int" hyperbolic nil )"(total_order?[real])" nil )"bool" integers nil )nil hyperbolic nil )nil hyperbolic nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"[T, T -> boolean]" equalities nil )nil nth_derivatives "analysis/" )"[T -> real]" nth_derivatives "analysis/" )"real" reals nil )"real" reals nil )"int" integers nil )"posint" nil )nil hyperbolic nil )"(strict_total_order?[real])" real_props nil )nil sigma_nat "reals/" )nil factorial "ints/" )nil hyperbolic nil )nil naturalnumbers nil )nil defined_types nil )"nat" hyperbolic nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"posnat" factorial "ints/" )nil integers nil )nil integers nil )"real" exponentiation nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"odd_int" integers nil )"real" hyperbolic nil )"real" reals nil )"real" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil taylors "analysis/" )"posint" nil )"posreal_ge1" hyperbolic nil )nil hyperbolic nil )"odd_int" integers nil )nil hyperbolic nil )nil hyperbolic nil )"bool" nth_derivatives "analysis/" ))nil )nil 3352442990"" (skosimp*)"" "Taylors[real]" "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[real]" "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 )nil taylors "analysis/" )nil nth_derivatives"analysis/" )nil nth_derivatives "analysis/" )"[T -> real]" nth_derivatives "analysis/" )nil sigma_nat "reals/" )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )nil taylors "analysis/" ))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 3352436939"" (expand "asinh" )"" (expand "sq" )"" (lemma "identity_derivable_fun[real]" )"" (expand "I" )"" "prod_derivable_fun[real]" "f1" "LAMBDA (x: real): x" "f2" "LAMBDA (x: real): x" ))"" (assert )"" (expand "*" )"" (lemma "const_derivable_fun[real]" ("b" "1" ))"" (expand "const_fun" )"" "sum_derivable_fun[real]" "f1" "LAMBDA (x: real): 1" "f2" "LAMBDA (x_1: real): x_1 * x_1" ))"" (assert )"" (expand "+" )"" (lemma "sqrt_derivable_fun" )"" "composition_derivable_fun[real,posreal]" "f" "LAMBDA (x: real): 1+x*x" "g" "LAMBDA (x:posreal): sqrt(x)" ))"1" assert )"1" expand "restrict" -2)"1" replace -2 -1)"1" expand "o" )"1" "sum_derivable_fun[real]" "f1" "LAMBDA (x: real): x" "f2" "LAMBDA (x_1: real): sqrt(1 + x_1 * x_1)" ))"1" assert )"1" expand "+" )"1" "composition_derivable_fun[real,posreal]" "f" "LAMBDA (x_1: real): x_1 + sqrt(1 + x_1 * x_1)" "g" "ln" ))"1" "ln_derivable" )"1" "1" replace -1)"1" assert )"1" expand "o" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "sq_rew" )"2" "sqrt_pos" "px" "1+sq(x!1)" ))"2" "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 )"2" "2" "2" "x!1+1" )"2" (assert ) nil nil ))nil ))nil ))nil )"3" "3" "deriv_domain_posreal" )"3" (propax) nil nil ))nil ))nil )"4" "4" "4" "x!1+1" )"4" (assert ) nil nil ))nil ))nil ))nil )"5" "deriv_domain_real" )"5" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"nonneg_real" sq "reals/" )"(bijective?[T, T])" identity nil )nil derivatives "analysis/" )nil sqrt_derivative "analysis/" )"posreal" sqrt "reals/" )nil sq "reals/" )nil real_axioms nil )"real" reals nil )nil sq "reals/" )"[numfield -> numfield]" number_fields nil )nil sqrt "reals/" )nil sq "reals/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil sqrt "reals/" )"posreal" nil )nil ln_exp nil )"posreal" nil )"real" ln_exp nil )"T3" function_props nil )"R" restrict nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def "analysis/" )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"[T, T -> boolean]" equalities nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )nil chain_rule "analysis/" )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" hyperbolic nil ))nil )nil 3270189876"" (expand "asinh" )"" (expand "sq" )"" (lemma "identity_derivable_fun[real]" )"" (expand "I" )"" "prod_derivable_fun" "f1" "LAMBDA (x: real): x" "f2" "LAMBDA (x: real): x" ))"" (assert )"" (expand "*" )"" (lemma "const_derivable_fun[real]" ("b" "1" ))"" (expand "const_fun" )"" "sum_derivable_fun" "f1" "LAMBDA (x: real): 1" "f2" "LAMBDA (x_1: real): x_1 * x_1" ))"" (assert )"" (expand "+" )"" (lemma "sqrt_derivable_fun" )"" "composition_derivable_fun[real,posreal]" "f" "LAMBDA (x: real): 1+x*x" "g" "LAMBDA (x:posreal): sqrt(x)" ))"1" assert )"1" expand "restrict" -2)"1" replace -2 -1)"1" expand "o" )"1" "sum_derivable_fun" "f1" "LAMBDA (x: real): x" "f2" "LAMBDA (x_1: real): sqrt(1 + x_1 * x_1)" ))"1" assert )"1" expand "+" )"1" "composition_derivable_fun[real,posreal]" "f" "LAMBDA (x_1: real): x_1 + sqrt(1 + x_1 * x_1)" "g" "ln" ))"1" "ln_derivable" )"1" "1" replace -1)"1" assert )"1" expand "o" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "sq_rew" )"2" "sqrt_pos" "px" "1+sq(x!1)" ))"2" "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 )"2" "2" "2" "x!1+1" )"2" (assert ) nil nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil )"4" "4" "4" "x!1+1" )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nonneg_real" sq "reals/" )nil derivatives "analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil chain_rule "analysis/" )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"real" ln_exp nil )nil ln_exp nil )nil sqrt "reals/" )nil sq "reals/" )nil sqrt "reals/" )nil sq "reals/" )nil sq "reals/" )nil sqrt_derivative "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )nil derivatives "analysis/" ))nil 3270188619 ("" (grind) nil nil ) nil nil 3270188627"" (expand "deriv_domain?" )"" (skosimp*) (("" (inst + "e!1/2" ) (("" (grind) nil nil )) nil ))nil ))nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"{y: posreal | y >= x}" nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )nil real_types nil )"bool" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil hyperbolic nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil booleans 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 )"posreal" nil )"(strict_total_order?[real])" real_props nil )"bool" deriv_domain_def "analysis/" )"real" reals nil ))nil 3270189616"" (skosimp*) (("" (inst + "x!1+1" ) (("" (assert ) nil nil )) nil ))nil )nil hyperbolic nil )) shostak))nil 3352437065"" (expand "acosh" )"" (lemma "identity_derivable_fun[posreal_gt1]" )"" (lemma "const_derivable_fun[posreal_gt1]" ("b" "1" ))"" (expand "I" )"" (expand "const_fun" )"" (expand "sq" )"" "prod_derivable_fun[posreal_gt1]" "f1" "LAMBDA (x: posreal_gt1): x" "f2" "LAMBDA (x: posreal_gt1): x" ))"" (assert )"" (expand "*" )"" "diff_derivable_fun[posreal_gt1]" "f1" "LAMBDA (x_1: posreal_gt1): x_1 * x_1" "f2" "LAMBDA (x_1: posreal_gt1): 1" ))"" (assert )"" (expand "-" )"" (lemma "sqrt_derivable_fun" )"" (expand "restrict" )"" "composition_derivable_fun[posreal_gt1,posreal]" "f" "LAMBDA (x: posreal_gt1): x * x - 1" "g" "LAMBDA (x:posreal): sqrt(x)" ))"1" assert )"1" expand "o" )"1" "sum_derivable_fun[posreal_gt1]" "f1" "LAMBDA (x: posreal_gt1): x" "f2" "LAMBDA (x_1: posreal_gt1): sqrt(x_1 * x_1 - 1)" ))"1" assert )"1" expand "+" )"1" "ln_derivable" )"1" "1" "composition_derivable_fun[posreal_gt1,posreal]" "f" "LAMBDA (x_1: posreal_gt1): x_1 + sqrt(x_1 * x_1 - 1)" "g" "ln" ))"1" assert )"1" expand "o" )"1" nil nil ))nil ))nil )"2" "2" "2" rewrite "sq_rew" )"2" "sq_gt" "nna" "x!1" "nnb" "1" ))"2" rewrite "sq_1" )"2" "sqrt_pos" "px" "sq(x!1)-1" ))"1" assert )nil nil )"2" assert )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "sq_rew" )"2" "sq_gt" "nna" "x!1" "nnb" "1" ))"2" rewrite "sq_1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "sq_rew" )"2" "sq_gt" "nna" "x!1" "nnb" "1" ))"2" rewrite "sq_1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "x!1+1" )"3" (assert ) nil nil ))nil ))nil ))nil )"4" "4" "deriv_domain_posreal" )"4" (propax) nil nil ))nil ))nil )"5" "5" "5" "x!1+1" )"5" (assert ) nil nil ))nil ))nil ))nil )"6" "6" expand "deriv_domain?" )"6" "6" "e!1/2" )"6" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 derivatives "analysis/" )"(bijective?[T, T])" identity nil )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil sqrt_derivative "analysis/" )"real" reals nil )nil chain_rule "analysis/" )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"bool" reals nil )nil real_types nil )nil real_types nil )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def "analysis/" )AND const-decl "[bool, bool -> bool]" booleans nil )"T3" function_props nil )nil ln_exp nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"real" ln_exp nil )"posreal" nil )nil sq "reals/" )"(total_order?[real])" nil )nil sqrt "reals/" )"(strict_total_order?[real])" real_props nil )nil sq "reals/" )nil sq "reals/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )"posreal" sqrt "reals/" )"R" restrict nil )"[T -> real]" real_fun_ops "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil derivatives "analysis/" )"nonneg_real" sq "reals/" )"real" reals nil )nil derivatives "analysis/" )"nnreal" hyperbolic nil ))nil )nil 3270191512"" (expand "acosh" )"" (lemma "identity_derivable_fun[posreal_gt1]" )"" (lemma "const_derivable_fun[posreal_gt1]" ("b" "1" ))"" (expand "I" )"" (expand "const_fun" )"" (expand "sq" )"" "prod_derivable_fun" "f1" "LAMBDA (x: posreal_gt1): x" "f2" "LAMBDA (x: posreal_gt1): x" ))"" (assert )"" (expand "*" )"" "diff_derivable_fun" "f1" "LAMBDA (x_1: posreal_gt1): x_1 * x_1" "f2" "LAMBDA (x_1: posreal_gt1): 1" ))"" (assert )"" (expand "-" )"" (lemma "sqrt_derivable_fun" )"" (expand "restrict" )"" "composition_derivable_fun[posreal_gt1,posreal]" "f" "LAMBDA (x: posreal_gt1): x * x - 1" "g" "LAMBDA (x:posreal): sqrt(x)" ))"1" assert )"1" expand "o" )"1" "sum_derivable_fun" "f1" "LAMBDA (x: posreal_gt1): x" "f2" "LAMBDA (x_1: posreal_gt1): sqrt(x_1 * x_1 - 1)" ))"1" assert )"1" expand "+" )"1" "ln_derivable" )"1" "1" "composition_derivable_fun[posreal_gt1,posreal]" "f" "LAMBDA (x_1: posreal_gt1): x_1 + sqrt(x_1 * x_1 - 1)" "g" "ln" ))"1" assert )"1" expand "o" )"1" nil nil ))nil ))nil )"2" "2" "2" rewrite "sq_rew" )"2" "sq_gt" "nna" "x!1" "nnb" "1" ))"2" rewrite "sq_1" )"2" "sqrt_pos" "px" "sq(x!1)-1" ))"1" assert )nil nil )"2" assert )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "sq_rew" )"2" "sq_gt" "nna" "x!1" "nnb" "1" ))"2" rewrite "sq_1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "sq_rew" )"2" "sq_gt" "nna" "x!1" "nnb" "1" ))"2" rewrite "sq_1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "x!1+1" )"3" (assert ) nil nil ))nil ))nil ))nil )"4" "4" (grind) nil nil ))nil )"5" "5" "5" "x!1+1" )"5" (assert ) nil nil ))nil ))nil ))nil )"6" "6" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil derivatives "analysis/" )"nonneg_real" sq "reals/" )nil derivatives "analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil sq "reals/" )nil sq "reals/" )nil sqrt "reals/" )nil sq "reals/" )"real" ln_exp nil )nil ln_exp nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )nil chain_rule "analysis/" )nil sqrt_derivative "analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" ))nil 3270188647"" (lemma "deriv_domain_open" ) (("" (inst - "-1" "1" ) nil nil ))nil )"odd_int" integers nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil deriv_domain "analysis/" ))nil 3270188654 ("" (assert ) nil nil )nil hyperbolic nil )) shostak))nil 3352437461"" (expand "atanh" )"" (lemma "identity_derivable_fun[real_abs_lt1]" )"" (expand "I" )"" (lemma "const_derivable_fun[real_abs_lt1]" ("b" "1" ))"" (expand "const_fun" )"" "diff_derivable_fun[real_abs_lt1]" "f1" "LAMBDA (x: real_abs_lt1): 1" "f2" "LAMBDA (x: real_abs_lt1): x" ))"" "sum_derivable_fun[real_abs_lt1]" "f1" "LAMBDA (x: real_abs_lt1): 1" "f2" "LAMBDA (x: real_abs_lt1): x" ))"" (assert )"" (expand "-" )"" (expand "+" )"" "div_derivable_fun[real_abs_lt1]" "f" "LAMBDA (x: real_abs_lt1): 1+x" "g" "LAMBDA (x: real_abs_lt1): 1-x" ))"" (assert )"" (expand "/" )"" (lemma "ln_derivable" )"" "" "composition_derivable_fun[real_abs_lt1,posreal]" "f" "LAMBDA (x_1: real_abs_lt1): (1 + x_1) / (1 - x_1)" "g" "ln" ))"1" assert )"1" expand "o" )"1" "scal_derivable_fun[real_abs_lt1]" "f" "LAMBDA (x: real_abs_lt1): ln((1 + x) / (1 - x))" "b" "1/2" ))"1" expand "*" )"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "posreal_div_posreal_is_posreal" "px" "1+x!1" "py" "1-x!1" ))"2" (assert ) nil nil ))nil ))nil ))nil )"3" "3" "3" "x!1+1" )"3" (assert ) nil nil ))nil ))nil ))nil )"4" "4" "deriv_domain_posreal" )"4" (propax) nil nil ))nil ))nil )"5" "5" "5" case "x!1=0" )"1" "1/2" )"1" (assert ) nil nil ))nil )"2" "x!1/2" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"6" "6" "deriv_domain_open" )"6" (inst - "-1" "1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 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 derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[T -> real]" real_fun_ops "reals/" )nil real_types nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"posrat" nil )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )"T3" function_props nil )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def "analysis/" )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil ) (ln const-decl "real" ln_exp nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil chain_rule "analysis/" )nil ln_exp nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"real" reals nil )nil derivatives "analysis/" )"(bijective?[T, T])" identity nil )"real" hyperbolic nil )"real" reals nil ))nil )nil 3270190972"" (expand "atanh" )"" (lemma "identity_derivable_fun[real_abs_lt1]" )"" (expand "I" )"" (lemma "const_derivable_fun[real_abs_lt1]" ("b" "1" ))"" (expand "const_fun" )"" "diff_derivable_fun" "f1" "LAMBDA (x: real_abs_lt1): 1" "f2" "LAMBDA (x: real_abs_lt1): x" ))"" "sum_derivable_fun" "f1" "LAMBDA (x: real_abs_lt1): 1" "f2" "LAMBDA (x: real_abs_lt1): x" ))"" (assert )"" (expand "-" )"" (expand "+" )"" "div_derivable_fun" "f" "LAMBDA (x: real_abs_lt1): 1+x" "g" "LAMBDA (x: real_abs_lt1): 1-x" ))"" (assert )"" (expand "/" )"" (lemma "ln_derivable" )"" "" "composition_derivable_fun[real_abs_lt1,posreal]" "f" "LAMBDA (x_1: real_abs_lt1): (1 + x_1) / (1 - x_1)" "g" "ln" ))"1" assert )"1" expand "o" )"1" "scal_derivable_fun" "f" "LAMBDA (x: real_abs_lt1): ln((1 + x) / (1 - x))" "b" "1/2" ))"1" expand "*" )"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "posreal_div_posreal_is_posreal" "px" "1+x!1" "py" "1-x!1" ))"2" (assert ) nil nil ))nil ))nil ))nil )"3" "3" "3" "x!1+1" )"3" (assert ) nil nil ))nil ))nil ))nil )"4" "4" (grind) nil nil ))nil )"5" "5" "5" case "x!1=0" )"1" "1/2" )"1" (assert ) nil nil ))nil )"2" "x!1/2" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"6" "6" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil ln_exp nil )nil chain_rule "analysis/" )"real" ln_exp nil )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" ))nil 3270188719"" (lemma "asinh_derivable2" ) (("" (propax) nil nil )) nil )nil hyperbolic nil )) shostak))nil 3352443164"" (expand "asinh" )"" (expand "sq" )"" (lemma "identity_derivable_fun[real]" )"" (lemma "deriv_id_fun[real]" )"" (expand "I" )"" (lemma "const_derivable_fun[real]" ("b" "1" ))"" (lemma "deriv_const_fun[real]" ("b" "1" ))"" (expand "const_fun" )"" "prod_derivable_fun[real]" "f1" "LAMBDA (x: real): x" "f2" "LAMBDA (x: real): x" ))"" (assert )"" (expand "*" )"" "deriv_prod_fun[real]" "ff1" "LAMBDA (x: real): x" "ff2" "LAMBDA (x: real): x" ))"" (replace -5)"" (expand "*" )"" expand "+" )"" "sum_derivable_fun[real]" "f1" "LAMBDA (x: real): 1" "f2" "LAMBDA (x: real): x * x" ))"" assert )"" expand "+" )"" "deriv_sum_fun[real]" "ff1" "LAMBDA (x: real): 1" "ff2" "LAMBDA (x: real): x * x" ))"" replace -5)"" replace -3)"" expand "+" )"" "ln_derivable" )"" "" "sqrt_derivable_fun" )"" "deriv_sqrt_fun" )"" "composition_derivable_fun[real,posreal]" "f" "LAMBDA (x_1: real): 1 + x_1 * x_1" "g" "LAMBDA (x:posreal): sqrt(x)" ))"1" assert )"1" expand "restrict" )"1" replace "1" expand "o" )"1" "deriv_comp_fun[real,posreal]" "ff" "LAMBDA (x: real): 1+x*x" "gg" "LAMBDA (x:posreal): sqrt(x)" ))"1" replace "1" replace "1" expand
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.1.12Bemerkung:
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-30)
¤ *Eine klare Vorstellung vom Zielzustand
