|
(ln_series
(noa_posreal 0
(noa_posreal-1 nil 3477843250
("" (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))
(noa_gt_m1 0
(noa_gt_m1-1 nil 3477843265
("" (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 3477843280
("" (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))
(conn_posreal 0
(conn_posreal-1 nil 3477843288
("" (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))
(conn_abslt1 0
(conn_abslt1-1 nil 3477843296
("" (expand "connected?")
(("" (skosimp*)
(("" (assert)
(("" (typepred "y!1")
(("" (typepred "x!1") (("" (grind) nil nil)) nil)) nil))
nil))
nil))
nil)
((abslt1 type-eq-decl nil ln_series nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil) (< const-decl "bool" reals 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)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(connected? const-decl "bool" deriv_domain_def "analysis/"))
shostak))
(noa_abslt1 0
(noa_abslt1-1 nil 3477843230
("" (expand "not_one_element?")
(("" (skosimp*)
(("" (inst-cp + "1/2")
(("1" (inst + "1/4")
(("1" (assert) nil nil) ("2" (grind) nil nil)) nil)
("2" (grind) nil nil))
nil))
nil))
nil)
((/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(abslt1 type-eq-decl nil ln_series 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)
(bool nonempty-type-eq-decl nil booleans nil)
(< const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}"
real_defs nil)
(not_one_element? const-decl "bool" deriv_domain_def "analysis/"))
nil))
(deriv_domain_gtm1 0
(deriv_domain_gtm1-1 nil 3477843360
("" (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 3563622659 ("" (assert) nil nil)
((deriv_domain_posreal formula-decl nil deriv_domain "analysis/"))
nil))
(nderiv_ln_TCC2 0
(nderiv_ln_TCC2-1 nil 3563622659 ("" (assert) nil nil)
((noa_posreal formula-decl nil ln_series nil)) nil))
(nderiv_ln 0
(nderiv_ln-2 nil 3445354085
(""
(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)
("2" (hide 2)
(("2" (skosimp*)
(("2"
(inst + "x!1+1")
(("2" (assert) nil nil))
nil))
nil))
nil)
("3" (assert) 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"
(expand
"*"
1)
(("2"
(expand
"^"
1
1)
(("2"
(rewrite
"div_expt"
1)
(("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)
("2"
(hide
3)
(("2"
(skosimp*)
(("2"
(expand
"*"
1)
(("2"
(expand
"^"
1
1)
(("2"
(rewrite
"div_expt"
1)
(("2"
(assert)
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)
("2" (skosimp*)
(("2" (assert)
(("2" (hide 3)
(("2" (inst + "x!1+1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil)
("3" (assert)
(("3" (lemma "deriv_domain_posreal")
(("3" (propax) 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)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(expt def-decl "real" exponentiation nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(expt_plus formula-decl nil exponentiation nil)
(expt_1i formula-decl nil exponentiation 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/")
(deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
(not_one_element? const-decl "bool" deriv_domain_def "analysis/")
(factorial_1 formula-decl nil factorial "ints/")
(expt_x1 formula-decl nil exponentiation nil)
(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 3302280454
(""
(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)
("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))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.59 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.
|
