|
(ln_exp_series_alt
(noa_posreal 0
(noa_posreal-1 nil 3477844115
("" (expand "not_one_element?")
(("" (skosimp*) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil))
nil))
nil)
((+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(not_one_element? const-decl "bool" deriv_domain_def "analysis/"))
shostak))
(conn_posreal 0
(conn_posreal-1 nil 3477844124
("" (expand "connected?")
(("" (skosimp*) (("" (assert) nil nil)) nil)) nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(connected? const-decl "bool" deriv_domain_def "analysis/"))
shostak))
(noa_gt_m1 0
(noa_gt_m1-1 nil 3477844134
("" (expand "not_one_element?")
(("" (skosimp*) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil))
nil))
nil)
((+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(not_one_element? const-decl "bool" deriv_domain_def "analysis/"))
shostak))
(conn_gt_m1 0
(conn_gt_m1-1 nil 3477844144
("" (expand "connected?")
(("" (skosimp*) (("" (assert) nil nil)) nil)) nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(connected? const-decl "bool" deriv_domain_def "analysis/"))
shostak))
(deriv_domain_gtm1 0
(deriv_domain_gtm1-1 nil 3477844153
("" (expand "deriv_domain?")
(("" (skosimp*) (("" (inst + "e!1/2") (("" (grind) nil nil)) nil))
nil))
nil)
((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
(real_plus_real_is_real application-judgement "real" reals nil))
shostak))
(nderiv_ln_TCC1 0
(nderiv_ln_TCC1-1 nil 3279382887
("" (lemma "deriv_domain_posreal") (("" (propax) nil nil)) nil)
((deriv_domain_posreal formula-decl nil deriv_domain "analysis/"))
shostak))
(nderiv_ln_TCC2 0
(nderiv_ln_TCC2-1 nil 3279382887
("" (expand "not_one_element?")
(("" (skosimp*) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil))
nil))
nil)
((+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(not_one_element? const-decl "bool" deriv_domain_def "analysis/"))
shostak))
(nderiv_ln 0
(nderiv_ln-2 nil 3445353631
(""
(case "FORALL (n: nat): derivable_n_times?[posreal](ln, n) & nderiv[posreal](n,ln) = IF n = 0 THEN ln ELSE (LAMBDA (x:posreal): -factorial(n-1)/(-x)^n) ENDIF")
(("1" (skosimp*)
(("1" (inst - "n!1") (("1" (flatten) nil nil)) nil)) nil)
("2" (hide 2)
(("2" (induct "n")
(("1" (expand "derivable_n_times?") (("1" (propax) nil nil))
nil)
("2" (expand "nderiv") (("2" (propax) nil nil)) nil)
("3" (skosimp*)
(("3" (case-replace "j!1=0")
(("1" (lemma "ln_derivable")
(("1" (flatten -1)
(("1" (expand "derivable_n_times?")
(("1" (expand "derivable_n_times?")
(("1" (expand "nderiv" 1)
(("1" (expand "nderiv" 1)
(("1"
(lemma "extensionality"
("f" "deriv(ln)" "g"
"(LAMBDA (x: posreal): -factorial(1) / (-x) ^ 1)"))
(("1" (split -1)
(("1" (assert) nil nil)
("2" (hide 2)
(("2"
(replace -2)
(("2"
(skosimp*)
(("2"
(expand "factorial")
(("2"
(expand "factorial")
(("2"
(rewrite "expt_x1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (lemma "ln_derivable")
(("2" (flatten -1)
(("2" (lemma "identity_derivable_fun[posreal]")
(("2"
(lemma "const_derivable_fun[posreal]"
("b" "-factorial(j!1)"))
(("2" (lemma "deriv_id_fun[posreal]")
(("2"
(lemma "deriv_const_fun[posreal]"
("b" "-factorial(j!1)"))
(("2" (expand "I")
(("2" (expand "const_fun")
(("2"
(lemma
"neg_derivable_fun[posreal]"
("f" "LAMBDA (x: posreal): x"))
(("2"
(assert)
(("2"
(expand "-")
(("2"
(lemma
"deriv_neg_fun[posreal]"
("ff" "LAMBDA (x: posreal): x"))
(("2"
(replace -4)
(("2"
(expand "-" -1)
(("2"
(lemma
"inv_derivable_fun[posreal]"
("g"
"LAMBDA (x_1: posreal): -x_1"))
(("2"
(assert)
(("2"
(expand "/")
(("2"
(lemma
"deriv_inv_fun[posreal]"
("gg"
"LAMBDA (x_1: posreal): -x_1"))
(("2"
(replace -3)
(("2"
(expand "/")
(("2"
(expand "*")
(("2"
(expand
"-"
-1)
(("2"
(lemma
"extensionality"
("f"
"LAMBDA (x: posreal): --1 / (-x * -x)"
"g"
"LAMBDA (x: posreal): 1 / (x * x)"))
(("2"
(split
-1)
(("1"
(replace
-1)
(("1"
(hide
-1)
(("1"
(lemma
"deriv_exp_fun[posreal]"
("f"
"LAMBDA (x: posreal): 1 / -x"
"n"
"j!1"))
(("1"
(assert)
(("1"
(flatten
-1)
(("1"
(lemma
"scal_derivable_fun[posreal]"
("f"
"(LAMBDA (x: posreal): 1 / -x) ^ j!1"
"b"
"-factorial(j!1 - 1)"))
(("1"
(replace
-2)
(("1"
(lemma
"deriv_scal_fun[posreal]"
("ff"
"(LAMBDA (x: posreal): 1 / -x) ^ j!1"
"b"
"-factorial(j!1 - 1)"))
(("1"
(replace
-4
-1)
(("1"
(replace
-5)
(("1"
(lemma
"extensionality"
("f"
"-factorial(j!1 - 1) * (LAMBDA (x: posreal): 1 / -x) ^ j!1"
"g"
"LAMBDA (x: posreal): -factorial(j!1 - 1) / (-x) ^ j!1"))
(("1"
(split
-1)
(("1"
(replace
-1
*
rl)
(("1"
(replace
-17
*
rl)
(("1"
(lemma
"extensionality"
("f"
"-factorial(j!1 - 1) *
(j!1 * (LAMBDA (x: posreal): 1 / -x) ^ (j!1 - 1) *
(LAMBDA (x: posreal): 1 / (x * x)))"
"g"
"LAMBDA (x: posreal): -factorial(j!1) / (-x) ^ (1 + j!1)"))
(("1"
(split
-1)
(("1"
(replace
-1)
(("1"
(lemma
"nderiv_derivable_eqv[posreal]"
("f"
"ln"
"n"
"j!1"))
(("1"
(replace
-18
-1)
(("1"
(replace
-5
-1)
(("1"
(flatten
-1)
(("1"
(lemma
"nderiv_derivable_aux[posreal]"
("f"
"ln"
"n"
"j!1"))
(("1"
(replace
-2)
(("1"
(replace
-5
-1)
(("1"
(replace
-1
2)
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
3)
(("2"
(skosimp*)
(("2"
(expand
"factorial"
1
2)
(("2"
(expand
"*"
1)
(("2"
(expand
"^"
1
1)
(("2"
(rewrite
"div_expt"
1)
(("2"
(rewrite
"expt_1i")
(("2"
(hide-all-but
(1
2))
(("2"
(lemma
"expt_plus"
("n0x"
"-x!1"
"i"
"j!1-1"
"j"
"2"))
(("2"
(replace
-1)
(("2"
(case
"(-x!1) ^ 2=x!1*x!1")
(("1"
(replace
-1)
(("1"
(assert)
nil
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
3)
(("2"
(skosimp*)
(("2"
(expand
"*"
1)
(("2"
(expand
"^"
1
1)
(("2"
(rewrite
"div_expt"
1)
(("2"
(rewrite
"expt_1i"
1)
(("2"
(assert)
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"
(grind)
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)
("4" (skosimp*) (("4" (assert) nil nil)) nil)
("5" (hide 1) (("5" (skosimp*) (("5" (assert) nil nil)) nil))
nil))
nil))
nil)
("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil))
nil))
nil)
((const_derivable_fun formula-decl nil derivatives "analysis/")
(deriv_const_fun formula-decl nil derivatives "analysis/")
(neg_derivable_fun formula-decl nil derivatives "analysis/")
(- const-decl "[T -> real]" real_fun_ops "reals/")
(inv_derivable_fun formula-decl nil derivatives "analysis/")
(nzreal nonempty-type-eq-decl nil reals nil)
(/ const-decl "[T -> real]" real_fun_ops "reals/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(deriv_exp_fun formula-decl nil derivatives "analysis/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(posint_exp application-judgement "posint" exponentiation nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(expt_1i formula-decl nil exponentiation nil)
(expt_plus formula-decl nil exponentiation nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(expt def-decl "real" exponentiation nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(minus_int_is_int application-judgement "int" integers nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(div_expt formula-decl nil exponentiation nil)
(nderiv_derivable_aux formula-decl nil nth_derivatives "analysis/")
(nderiv_derivable_eqv formula-decl nil nth_derivatives "analysis/")
(deriv_scal_fun formula-decl nil derivatives "analysis/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(^ const-decl "[T -> real]" real_fun_ops "reals/")
(scal_derivable_fun formula-decl nil derivatives "analysis/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/ const-decl "[T -> real]" real_fun_ops "reals/")
(nz_deriv_fun type-eq-decl nil derivatives "analysis/")
(deriv_inv_fun formula-decl nil derivatives "analysis/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(deriv_neg_fun formula-decl nil derivatives "analysis/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(I const-decl "(bijective?[T, T])" identity nil)
(deriv_id_fun formula-decl nil derivatives "analysis/")
(identity_derivable_fun formula-decl nil derivatives "analysis/")
(ln_derivable formula-decl nil ln_exp nil)
(extensionality formula-decl nil functions nil)
(derivable? const-decl "bool" derivatives "analysis/")
(deriv_fun type-eq-decl nil derivatives "analysis/")
(deriv const-decl "[T -> real]" derivatives "analysis/")
(expt_x1 formula-decl nil exponentiation nil)
(factorial_1 formula-decl nil factorial "ints/")
(factorial_0 formula-decl nil factorial "ints/")
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(derivable_n_times? def-decl "bool" nth_derivatives "analysis/")
(ln const-decl "real" ln_exp nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nderiv_fun type-eq-decl nil nth_derivatives "analysis/")
(nderiv def-decl "[T -> real]" nth_derivatives "analysis/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(factorial def-decl "posnat" factorial "ints/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(^ const-decl "real" exponentiation nil))
nil)
(nderiv_ln-1 nil 3270048547
(""
(case "FORALL (n: nat): derivable_n_times[posreal](ln, n) & nderiv[posreal](n,ln) = IF n = 0 THEN ln ELSE (LAMBDA (x:posreal): -factorial(n-1)/(-x)^n) ENDIF")
(("1" (skosimp*)
(("1" (inst - "n!1") (("1" (flatten) nil nil)) nil)) nil)
("2" (hide 2)
(("2" (induct "n")
(("1" (expand "derivable_n_times?") (("1" (propax) nil nil))
nil)
("2" (expand "nderiv") (("2" (propax) nil nil)) nil)
("3" (skosimp*)
(("3" (case-replace "j!1=0")
(("1" (lemma "ln_derivable")
(("1" (flatten -1)
(("1" (expand "derivable_n_times?")
(("1" (expand "derivable_n_times?")
(("1" (expand "nderiv" 1)
(("1" (expand "nderiv" 1)
(("1"
(lemma "extensionality"
("f" "deriv(ln)" "g"
"(LAMBDA (x: posreal): -factorial(1) / (-x) ^ 1)"))
(("1" (split -1)
(("1" (assert)
(("1"
(expand "factorial" -1)
(("1" (assert) nil nil))
nil))
nil)
("2" (hide 2)
(("2"
(replace -2)
(("2"
(skosimp*)
(("2"
(expand "factorial")
(("2"
(expand "factorial")
(("2"
(rewrite "expt_x1")
(("2" (assert) 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" (skosimp*) (("3" (assert) nil nil))
nil)
("4" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (lemma "ln_derivable")
(("2" (flatten -1)
(("2" (lemma "identity_derivable_fun[posreal]")
(("1"
(lemma "const_derivable_fun[posreal]"
("b" "-factorial(j!1)"))
(("1" (lemma "deriv_id_fun[posreal]")
(("1"
(lemma "deriv_const_fun[posreal]"
("b" "-factorial(j!1)"))
(("1" (expand "I")
(("1" (expand "const_fun")
(("1"
(lemma
"neg_derivable_fun[posreal]"
("f" "LAMBDA (x: posreal): x"))
(("1"
(assert)
(("1"
(expand "-")
(("1"
(lemma
"deriv_neg_fun[posreal]"
("ff" "LAMBDA (x: posreal): x"))
(("1"
(replace -4)
(("1"
(expand "-" -1)
(("1"
(lemma
"inv_derivable_fun[posreal]"
("g"
"LAMBDA (x_1: posreal): -x_1"))
(("1"
(assert)
(("1"
(expand "/")
(("1"
(lemma
"deriv_inv_fun[posreal]"
("gg"
"LAMBDA (x_1: posreal): -x_1"))
(("1"
(replace -3)
(("1"
(expand "/")
(("1"
(expand "*")
(("1"
(expand
"-"
-1)
(("1"
(lemma
"extensionality"
("f"
"LAMBDA (x: posreal): --1 / (-x * -x)"
"g"
"LAMBDA (x: posreal): 1 / (x * x)"))
(("1"
(split
-1)
(("1"
(replace
-1)
(("1"
(hide
-1)
(("1"
(lemma
"deriv_exp_fun[posreal]"
("f"
"LAMBDA (x: posreal): 1 / -x"
"n"
"j!1"))
(("1"
(assert)
(("1"
(flatten
-1)
(("1"
(lemma
"scal_derivable_fun[posreal]"
("f"
"(LAMBDA (x: posreal): 1 / -x) ^ j!1"
"b"
"-factorial(j!1 - 1)"))
(("1"
(replace
-2)
(("1"
(lemma
"deriv_scal_fun[posreal]"
("ff"
"(LAMBDA (x: posreal): 1 / -x) ^ j!1"
"b"
"-factorial(j!1 - 1)"))
(("1"
(replace
-4
-1)
(("1"
(replace
-5)
(("1"
(lemma
"extensionality"
("f"
"-factorial(j!1 - 1) * (LAMBDA (x: posreal): 1 / -x) ^ j!1"
"g"
"LAMBDA (x: posreal): -factorial(j!1 - 1) / (-x) ^ j!1"))
(("1"
(split
-1)
(("1"
(replace
-1
*
rl)
(("1"
(replace
-17
*
rl)
(("1"
(lemma
"extensionality"
("f"
"-factorial(j!1 - 1) *
(j!1 * (LAMBDA (x: posreal): 1 / -x) ^ (j!1 - 1) *
(LAMBDA (x: posreal): 1 / (x * x)))"
"g"
"LAMBDA (x: posreal): -factorial(j!1) / (-x) ^ (1 + j!1)"))
(("1"
(split
-1)
(("1"
(replace
-1)
(("1"
(lemma
"nderiv_derivable_eqv[posreal]"
("f"
"ln"
"n"
"j!1"))
(("1"
(replace
-18
-1)
(("1"
(replace
-5
-1)
(("1"
(flatten
-1)
(("1"
(lemma
"nderiv_derivable_aux[posreal]"
("f"
"ln"
"n"
"j!1"))
(("1"
(replace
-2)
(("1"
(replace
-5
-1)
(("1"
(replace
-1
2)
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
3)
(("2"
(skosimp*)
(("2"
(expand
"factorial"
1
2)
(("2"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.32 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
