(ln_seriesnil 3302450959"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil ))nil 3320163563 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3322477326 ("" (assuming-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"boolean" notequal nil ))nil ))nil 3302450959"" (skosimp*) (("" (assert ) nil nil )) nil )"real" reals nil )"(total_order?[real])" nil ))nil 3302450959"" (skosimp*) (("" (typepred "c!1" ) (("" (grind) nil nil )) nil ))nil )nil taylor_help nil )"[T, T -> boolean]" equalities nil )nil ln_series nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"[bool, bool -> bool]" booleans 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 )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil ))nil 3302450959"" (skosimp*) (("" (assert ) nil nil )) nil )"posint" nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil ))nil 3302450340"" (skosimp*)"" "Taylors[posreal]" "f" "ln" "n" "n!1" "bb" "xgm1!1+1" "aa" "1" ))"1" (lemma "nderiv_ln" ("n" "n!1+1" ))"1" (replace -1)"1" (skosimp*)"1" (inst + "c!1" )"1" (lemma "ln_nderiv" ("n" "n!1+1" ))"1" (simplify -1)"1" (replace -1 -3)"1" (simplify -3)"1" (rewrite "div_expt" 1)"1" (expand "ln_estimate" 1)"1" "sigma_eq[nat]" "low" "0" "high" "n!1" "F" "LAMBDA (nn:nat): IF nn > n!1 THEN 0" " G" " LAMBDA (nn: nat):IF nn = 0 THEN 0 ELSE -(-xgm1!1) ^ nn / nn ENDIF")) "1" (split -1)"1" replace -1 -4)"1" "K1" "sigma(0, n!1, LAMBDA (nn: nat):IF nn = 0 THEN 0 ELSE -(-xgm1!1) ^ nn / nn ENDIF)") "1" replace -4 1)"1" "1" "c!1" )"1" "1" expand "factorial" 1 2)"1" "K2" "factorial(n!1)" )"1" "div_cancel1" "x" "((-1/ (-c!1) ^ (1 + n!1)) * xgm1!1 ^ (1 + n!1)) / (1+n!1)" "n0z" "K2" ))"1" rewrite "div_div2" "1" case "K2 * (((-1 / (-c!1) ^ (1 + n!1)) * xgm1!1 ^ (1 + n!1)) / (K2 + K2 * n!1)) = ((-K2 / (-c!1) ^ (1 + n!1)) * xgm1!1 ^ (1 + n!1)) / (K2 + K2 * n!1)" )"1" replace -1)"1" replace -2)"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "K3" "K2 + K2 * n!1" )"2" "K4" "xgm1!1 ^ (1 + n!1)" )"2" "K5" "(-c!1) ^ (1 + n!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "n!2" )"2" assert )"2" "2" "2" "ln_nderiv" )"2" "2" replace -1)"2" "2" assert )"2" "2" "cross_mult" "x" "-factorial(n!2 - 1) / (-1) ^ n!2 * xgm1!1 ^ n!2" "n0x" "factorial(n!2)" "y" "-(-xgm1!1) ^ n!2" "n0y" "n!2" ))"2" replace "2" expand "factorial" "2" "xgm1!1=0" )"1" expand "^" "1" expand "^" "1" expand "expt" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" "2" expand "^" )"2" "expt_of_mult" )"2" "n!2" "-xgm1!1" "-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 )"2" (hide-all-but 1)"2" (skosimp*) nil nil )) nil )"3" (skosimp*)"3" "nderiv_ln" )"3" (inst?) nil nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (flatten)"2" (replace -1)"2" rewrite "ln_1" )"2" expand "^" 1)"2" expand "expt" 1)"2" assert )"2" rewrite "zero_times1" )"2" "2" expand "ln_estimate" )"2" "2" "sigma_zero[nat]" "low" "0" "high" "n!1" ))"2" "sigma_eq[nat]" "low" "0" "high" "n!1" "F" "LAMBDA (i: nat): 0" "G" "LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-0) ^ nn / nn ENDIF" ))"1" "1" assert )nil nil )"2" "2" "2" case "n!2=0" )"1" assert )nil nil )"2" assert )"2" expand "^" )"2" expand "expt" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 -2)"2" (typepred "xgm1!1" )"2" (typepred "c!1" )"2" (replace -3)"2" (replace -4) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (inst + "x!1+1" ) (("2" (assert ) nil nil )) nil )) nil ))nil )"3" (hide 2) (("3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil )"real" ln_exp nil )nil sigma "reals/" )"real" sigma "reals/" )nil sigma "reals/" )nil ln_exp nil ))nil )nil 3302449853"" (skosimp*)"" "Taylors[posreal]" "f" "ln" "n" "n!1" "bb" "xgm1!1+1" "aa" "1" ))"1" (lemma "ln_derivable_n_times" ("n" "n!1+1" ))"1" (replace -1)"1" (skosimp*)"1" (inst + "c!1" )"1" (lemma "ln_nderiv" ("n" "n!1+1" ))"1" (simplify -1)"1" (replace -1 -3)"1" (simplify -3)"1" (rewrite "div_expt" 1)"1" (expand "ln_series_n" 1)"1" "sigma_eq[nat]" "low" "0" "high" "n!1" "F" "LAMBDA (nn:nat): IF nn > n!1 THEN 0" " G" " LAMBDA (nn: nat):IF nn = 0 THEN 0 ELSE -(-xgm1!1) ^ nn / nn ENDIF")) "1" (split -1)"1" replace -1 -4)"1" "K1" "sigma(0, n!1, LAMBDA (nn: nat):IF nn = 0 THEN 0 ELSE -(-xgm1!1) ^ nn / nn ENDIF)") "1" replace -4 1)"1" "1" "c!1" )"1" "1" expand "factorial" 1 2)"1" "K2" "factorial(n!1)" )"1" "div_cancel1" "x" "((-1/ (-c!1) ^ (1 + n!1)) * xgm1!1 ^ (1 + n!1)) / (1+n!1)" "n0z" "K2" ))"1" rewrite "div_div2" "1" case "K2 * (((-1 / (-c!1) ^ (1 + n!1)) * xgm1!1 ^ (1 + n!1)) / (K2 + K2 * n!1)) = ((-K2 / (-c!1) ^ (1 + n!1)) * xgm1!1 ^ (1 + n!1)) / (K2 + K2 * n!1)" )"1" replace -1)"1" replace -2)"1" "1" assert )nil )))))))"2" "2" "K3" "K2 + K2 * n!1" )"2" "K4" "xgm1!1 ^ (1 + n!1)" )"2" "K5" "(-c!1) ^ (1 + n!1)" )"2" assert )nil )))))))))))))))))))))))))))))))"2" "2" "2" "n!2" )"2" assert )"2" rewrite "ln_1" )"2" case "n!2=0" )"1" (assert ) nil )"2" assert )"2" "ln_nderiv" "n" "n!2" ))"2" assert )"2" replace -1 2)"2" "2" "2" "cross_mult" "x" "-factorial(n!2 - 1) / (-1) ^ n!2 * xgm1!1 ^ n!2" "n0x" "factorial(n!2)" "y" "-(-xgm1!1) ^ n!2" "n0y" "n!2" ))"2" replace "2" expand "factorial" "2" "xgm1!1=0" )"1" expand "^" "1" expand "^" "1" expand "expt" )"1" assert )nil )))))))"2" "div_expt" "n0x" "xgm1!1" "n0y" "-1" "i" "n!2" ))"1" assert )nil )"2" assert )nil )))))))))))))))))))))))))))))))))))))"2" (hide-all-but 1)"2" "2" assert )"2" "ln_derivable_n_times" "n" "nn!1" ))"2" (propax) nil )))))))))))))"2" (expand "/=" 1)"2" (replace -1)"2" (rewrite "ln_1" )"2" expand "^" 1)"2" expand "expt" 1)"2" assert )"2" rewrite "zero_times1" )"2" "2" expand "ln_series_n" )"2" "2" "sigma_zero[nat]" "low" "0" "high" "n!1" ))"2" "sigma_eq[nat]" "low" "0" "high" "n!1" "F" "LAMBDA (i: nat): 0" "G" "LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-0) ^ nn / nn ENDIF" ))"2" "1" (assert ) nil )"2" "2" "2" case "n!2=0" )"1" assert )nil )"2" assert )"2" expand "^" )"2" expand "expt" )"2" assert )nil )))))))))))))))))))))))))))))))))))))))))))))))))"2" (hide -1 -2)"2" (typepred "xgm1!1" )"2" (typepred "c!1" )"2" (replace -3)"2" (replace -4)"2" (propax) nil )))))))))))))))))))"2" (hide 2)"2" (skosimp*)"2" (inst + "x!1+1" ) (("2" (assert ) nil )))))))"3" (hide 2) (("3" (skosimp*) (("3" (assert ) nil ))))))))nil )nil nil ))nil 3321095836 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil ln_series nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil ))nil )))quality 98%
¤ Dauer der Verarbeitung: 0.23 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
