Quellcode-Bibliothek derivatives_def.prf
Sprache: Lisp
(derivatives_defnil 3253536989 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_def nil )nil derivatives_def nil )"boolean" notequal nil )nil reals nil )nil defined_types nil )"setof[nzreal]" derivatives_def nil )"real" reals nil ))nil ))nil 3471267100"" (skosimp*)"" (lemma "deriv_domain" )"" (expand "adh" )"" (expand "deriv_domain?" )"" (expand "fullset" )"" (skosimp*)"" (inst - "e!1" "x!1" )"" (skosimp*)"" (inst?)"" (expand "A" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil derivatives_def nil )"real" reals nil )"bool" deriv_domain_def nil )"{u: nzreal | T_pred(u + x!1)}" nil )"T" derivatives_def nil )"boolean" notequal nil )nil reals nil )nil defined_types nil )"setof[nzreal]" derivatives_def nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil derivatives_def nil )"[real -> boolean]" derivatives_def 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 )"set" sets nil )"setof[real]" convergence_functions nil )"real" reals nil ))nil )nil 3471261300"" (skosimp*)"" (lemma "nearzero" )"" (expand "adh" )"" (expand "fullset" )"" (skosimp*)"" (inst - "e!1" "x!1" )"" (skosimp*)"" (inst?)"" (expand "A" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"setof[real]" convergence_functions nil )) nil )nil 3253536989"" (skosimp*)"" (expand "adh" )"" (expand "fullset" )"" (skosimp*) (("" (postpone) nil nil )) nil )) nil ))nil ))nil )"setof[real]" convergence_functions nil )) nil ))nil 3471267122"" (skosimp*)"" (lemma "deriv_domain" )"" (expand "deriv_domain?" )"" (expand "adh" )"" (skosimp*)"" (inst?)"" (inst - "x!1" )"" (skosimp*)"" (inst + "y!1" )"1" (expand "fullset" ) (("1" (propax) nil nil ))nil )"2" (expand "A" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil derivatives_def nil )"real" reals nil )"setof[real]" convergence_functions 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 )"set" sets nil )"{u: nzreal | T_pred(u + x!1)}" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"T" derivatives_def nil )"setof[nzreal]" derivatives_def nil )nil defined_types nil )nil reals nil )"boolean" notequal nil )"[real -> boolean]" derivatives_def nil )nil derivatives_def nil )"bool" deriv_domain_def nil )"real" reals nil ))nil )nil 3297610627"" (skosimp*)"" (lemma "nearzero" )"" (expand "adh" )"" (skosimp*)"" (inst?)"" (inst - "x!1" )"" (skosimp*)"" (inst + "y!1" )"1" (expand "fullset" ) (("1" (propax) nil nil ))nil )"2" (expand "A" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"setof[real]" convergence_functions nil )) nil )nil 3297610566"" (skosimp*) (("" (postpone) nil nil )) nil ) nil shostak))nil 3253536989"" "abs" "adh" ) :rewrites"deriv_TCC" "adherence_fullset[T]" ) :if-match nil )"1" (inst? -4)"1" (skolem!)"1" (inst + "delta!1" )"1" (skosimp)"1" (inst - "x!2 - x!1" )"1" (assert ) nil nil )"2" (delete -5) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (inst? -4)"2" (skolem!)"2" (inst + "delta!1" )"2" (skosimp :preds? t)"2" (assert ) (("2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"{y: posreal | y >= x}" nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"T" derivatives_def nil )"T" derivatives_def nil )"setof[nzreal]" derivatives_def nil )nil defined_types nil )nil reals nil )"boolean" notequal nil )"(strict_total_order?[real])" real_props nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals 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 )"[real -> boolean]" derivatives_def nil )nil derivatives_def nil )"real" reals nil )"bool" continuous_functions nil )"bool" lim_of_functions nil )"bool" convergence_functions nil )"set" sets nil )nil derivatives_def nil ))nil ))nil 3253536989"" (skosimp)"" (rewrite "continuous_lim" :dir rl)"" "(LAMBDA (h: (A(x!1))): f!1(h + x!1)) = ") "1" (delete -1)"1" "lim_of_functions[(A(x!1))]" :exclude"convergence" "convergence_def" "convergent?" "lim" "lim_fun_lemma" "lim_fun_def" )"1" (auto-rewrite "deriv_TCC" )"1" (grind :defs nil ) nil nil )) nil ))nil ))nil )"2" (delete -1 2)"2" (apply-extensionality :hide? t)"1" (grind) nil nil ) ("2" (grind) nil nil )) nil ))nil )"3" (delete -1 2) (("3" (grind) nil nil )) nil ))nil ))nil ))nil )nil derivatives_def nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_def nil )nil derivatives_def nil )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"T" derivatives_def nil )"real" reals nil )nil lim_of_functions nil )nil lim_of_functions nil )nil lim_of_functions nil )nil lim_of_functions nil )nil lim_of_functions nil )nil lim_of_functions nil )nil lim_of_functions nil )nil lim_of_functions nil )nil lim_of_functions nil )nil derivatives_def nil )nil lim_of_functions nil )"real" reals nil )"real" derivatives_def nil )"(bijective?[T, T])" identity nil )"bool" functions nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"setof[nzreal]" derivatives_def nil )nil defined_types nil )nil booleans nil )nil reals nil )"boolean" notequal nil )"real" reals nil )"continuous_fun" nil )"continuous_fun" nil ))nil ))nil 3253536989"" (expand "derivable?" )"" (expand "convergent?" )"" (skosimp*) (("" (forward-chain "deriv_continuous" ) nil nil ))nil ))nil ))nil )"bool" lim_of_functions nil )nil derivatives_def nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_def nil )nil derivatives_def nil )"bool" derivatives_def nil ))nil ))nil 3253536989"" (skolem!)"" (apply-extensionality) (("" (grind) nil nil )) nil )) 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 -> boolean]" derivatives_def nil )nil derivatives_def nil )nil booleans nil )nil defined_types nil )"setof[nzreal]" derivatives_def nil )"[T -> real]" real_fun_ops "reals/" )"real" derivatives_def nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3442585851"" (skolem!)"" (apply-extensionality) (("" (grind) nil nil )) nil )) 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 -> boolean]" derivatives_def nil )nil derivatives_def nil )nil booleans nil )nil defined_types nil )"setof[nzreal]" derivatives_def nil )"[T -> real]" real_fun_ops "reals/" )"real" derivatives_def nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil 3253536989"" (skolem!)"" (apply-extensionality) (("" (grind) nil nil )) nil )) 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 -> boolean]" derivatives_def nil )nil derivatives_def nil )nil booleans nil )nil defined_types nil )"setof[nzreal]" derivatives_def nil )"[T -> real]" real_fun_ops "reals/" )"real" derivatives_def nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3253536989"" (skolem!)"" (apply-extensionality) (("" (grind) nil nil )) nil )) 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 -> boolean]" derivatives_def nil )nil derivatives_def nil )nil booleans nil )nil defined_types nil )"setof[nzreal]" derivatives_def nil )"[T -> real]" real_fun_ops "reals/" )"real" derivatives_def nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3253536989"" (skolem!)"" (apply-extensionality) (("" (grind) nil nil )) nil )) 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 -> boolean]" derivatives_def nil )nil derivatives_def nil )nil booleans nil )nil defined_types nil )"setof[nzreal]" derivatives_def nil )"[T -> real]" real_fun_ops "reals/" )"real" derivatives_def nil )"continuous_fun" nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3253536989"" (skolem!)"" (apply-extensionality) (("" (grind) nil nil )) nil )) 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 -> boolean]" derivatives_def nil )nil derivatives_def nil )nil booleans nil )nil defined_types nil )"setof[nzreal]" derivatives_def nil )"[T -> real]" real_fun_ops "reals/" )"(bijective?[T, T])" identity nil )"bool" functions nil )"real" derivatives_def nil )"continuous_fun" nil )"continuous_fun" nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3253536989 ("" (grind) nil nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" derivatives_def nil )"[T -> real]" real_fun_ops "reals/" ))nil ))nil 3253536989"" (auto-rewrite "deriv_TCC" )"" (skosimp)"" (name "F" "LAMBDA (h : (A(x!1))) : f1!1(x!1 + h)" )"1" "NQ(f1!1 * f2!1, x!1) = f2!1(x!1) * NQ(f1!1, x!1) + F * NQ(f2!1, x!1)" )"1" "lim_of_functions[(A(x!1))]" :exclude"convergence" "convergence_def" "convergent?" "lim" "lim_fun_def" "lim_e_del" )"1" (forward-chain "deriv_continuous" -3)"1" (use "continuous_lim" )"1" (replace *) (("1" (grind :defs nil ) nil nil ))nil ))nil ))nil ))nil )"2" (replace -1 + rl)"2" (delete -1 -2 -3 2)"2" (apply-extensionality :hide? t)"1" (grind) nil nil )"2" (delete 2) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (delete -1 -2 2) (("2" (grind) nil nil )) nil ))nil ))nil ))nil )"real" derivatives_def nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives_def nil )"real" reals nil )nil lim_of_functions nil )nil lim_of_functions nil )nil lim_of_functions nil )nil lim_of_functions nil )nil lim_of_functions nil )nil lim_of_functions nil )nil lim_of_functions nil )nil derivatives_def nil )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"real" reals nil )"T" derivatives_def 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 -> boolean]" derivatives_def nil )nil derivatives_def nil )nil booleans nil )nil defined_types nil )"setof[nzreal]" derivatives_def nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil ))nil 3253536989 ("" (grind) nil nil )"nzreal" nil )"real" reals nil )"real" reals nil )"real" reals nil )"nzreal" nil )"real" derivatives_def nil )"[T -> real]" real_fun_ops "reals/" ))nil ))nil 3442586093"" (auto-rewrite "deriv_TCC" )"" (skosimp)"" (name "F" "LAMBDA (h : (A(x!1))) : g!1(x!1 + h)" )"1" "NQ(1/g!1, x!1) = - NQ(g!1, x!1) / (g!1(x!1) * F)" )"1" (rewrite "cv_div[(A(x!1))]" )"1" (rewrite "cv_neg[(A(x!1))]" ) nil nil )"2" (rewrite "cv_scal[(A(x!1))]" )"2" (use "continuous_lim" ("f" "g!1" ))"2" (ground)"2" (forward-chain "deriv_continuous" ) nil nil ))nil ))nil ))nil ))nil )"2" (replace -1 + rl)"2" (delete -1 -2 2)"2" (apply-extensionality :hide? t)"1" (grind) nil nil )"2" (delete 2)"2" (grind :rewrites "zero_times3" ) nil nil )) nil ))nil ))nil ))nil )"3" (replace -1 + rl)"3" (delete -1 -2 2)"3" (grind :rewrites "zero_times3" ) nil nil )) nil ))nil ))nil )"2" (delete -1 2) (("2" (grind) nil nil )) nil ))nil ))nil ))nil )"real" derivatives_def nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )nil lim_of_functions nil )nil derivatives_def nil )nil derivatives_def nil )nil lim_of_functions nil )"real" reals nil )"real" reals nil )"nzreal" nil )nil lim_of_functions nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )NOT const-decl "[bool -> bool]" booleans nil )"nzreal" nil )"real" reals nil )"T" derivatives_def nil )nil real_props 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 -> boolean]" derivatives_def nil )nil derivatives_def nil )nil booleans nil )nil defined_types nil )"setof[nzreal]" derivatives_def nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil )nil 3253536989"" (auto-rewrite "deriv_TCC" )"" (skosimp)"" (name "F" "LAMBDA (h : (A(x!1))) : g!1(x!1 + h)" )"1" "NQ(1/g!1, x!1) = - NQ(g!1, x!1) / (g!1(x!1) * F)" )"1" (rewrite "cv_div[(A(x!1))]" )"1" (rewrite "cv_opp[(A(x!1))]" ) nil nil )"2" (rewrite "cv_scal[(A(x!1))]" )"2" (use "continuous_lim" ("f" "g!1" ))"2" (ground)"2" (forward-chain "deriv_continuous" ) nil nil ))nil ))nil ))nil )"3" (replace -2 1 rl)"3" (delete -1 -2 -3 2)"3" (grind :rewrites "zero_times3" ) nil nil )) nil ))nil ))nil )"2" (replace -1 + rl)"2" (delete -1 -2 2)"2" (apply-extensionality :hide? t)"1" (grind) nil nil )"2" (delete 2)"2" (grind :rewrites "zero_times3" ) nil nil )) nil )"3" (delete 2) (("3" (grind) nil nil )) nil ))nil ))nil ))nil )"3" (replace -1 + rl)"3" (delete -1 -2 2)"3" (grind :rewrites "zero_times3" ) nil nil )) nil ))nil ))nil )"2" (delete -1 2) (("2" (grind) nil nil )) nil ))nil ))nil ))nil )nil lim_of_functions nil )nil lim_of_functions nil ))nil ))nil 3253536989"" (auto-rewrite "derivable?" "sum_NQ" "deriv_TCC" )"" (skosimp)"" (assert )"" (use "sum_fun_convergent[(A(x!1))]" )"" (assert ) nil nil )) nil ))nil ))nil ))nil )nil lim_of_functions 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 -> boolean]" derivatives_def nil )nil derivatives_def nil )nil booleans nil )nil defined_types nil )"setof[nzreal]" derivatives_def nil )"real" derivatives_def nil )"bool" derivatives_def nil )nil derivatives_def nil ))nil ))nil 3442586144"" (auto-rewrite "derivable?" "neg_NQ" "deriv_TCC" )"" (skosimp)"" (assert )"" (use "neg_fun_convergent[(A(x!1))]" )"" (assert ) nil nil )) nil ))nil ))nil ))nil )nil lim_of_functions 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 -> boolean]" derivatives_def nil )nil derivatives_def nil )nil booleans nil )nil defined_types nil )"setof[nzreal]" derivatives_def nil )"real" derivatives_def nil )"bool" derivatives_def nil )nil derivatives_def nil ))nil ))nil 3253536989"" (auto-rewrite "derivable?" "diff_NQ" "deriv_TCC" )"" (skosimp)"" (assert )"" (use "diff_fun_convergent[(A(x!1))]" )"" (assert ) nil nil )) nil ))nil ))nil ))nil )nil lim_of_functions 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 -> boolean]" derivatives_def nil )nil derivatives_def nil )nil booleans nil )nil defined_types nil )"setof[nzreal]" derivatives_def nil )"real" derivatives_def nil )"bool" derivatives_def nil )nil derivatives_def nil ))nil ))nil 3253536989"" (expand "derivable?" )"" (expand "convergent?" )"" (skosimp*)"" (use "cnv_seq_prod_NQ" )"" (assert ) (("" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil )"bool" lim_of_functions nil )nil derivatives_def nil )nil derivatives_def nil )"[real -> boolean]" derivatives_def 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 )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"bool" derivatives_def nil ))nil ))nil 3253536989"" (auto-rewrite "derivable?" "scal_NQ" "deriv_TCC" )"" (skosimp)"" (assert )"" (use "scal_fun_convergent[(A(x!1))]" )"" (assert ) nil nil )) nil ))nil ))nil ))nil )nil lim_of_functions 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 -> boolean]" derivatives_def nil )nil derivatives_def nil )nil booleans nil )nil defined_types nil )"setof[nzreal]" derivatives_def nil )"real" derivatives_def nil )"bool" derivatives_def nil )nil derivatives_def nil ))nil ))nil 3253536989"" (skolem!)"" (auto-rewrite "derivable?" "const_NQ" "deriv_TCC" )"" (assert )"" (lemma "const_fun_convergent[(A(x!1))]" )"" (inst - "0" "0" ) nil nil )) nil ))nil ))nil ))nil )"setof[nzreal]" derivatives_def nil )nil defined_types nil )nil booleans nil )nil derivatives_def nil )"[real -> boolean]" derivatives_def 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 lim_of_functions nil )"set" sets nil ) (set type-eq-decl nil sets nil )"setof[real]" convergence_functions nil )nil derivatives_def nil )nil derivatives_def nil )"bool" derivatives_def nil )"continuous_fun" nil ))nil ))nil 3253536989"" (expand "derivable?" )"" (expand "convergent?" )"" (skosimp*)"" (use "cnv_seq_inv_NQ" )"" (assert ) (("" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil )"bool" lim_of_functions nil )nil derivatives_def nil )nil reals nil )"boolean" notequal nil )nil derivatives_def nil )"[real -> boolean]" derivatives_def 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 )"nzreal" nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"bool" derivatives_def nil ))nil ))nil 3253536989"" (skosimp)"" (rewrite "div_function[T]" )"" (rewrite "prod_derivable" )"" (rewrite "inv_derivable" ) nil nil )) nil ))nil ))nil )nil real_fun_ops "reals/" )"boolean" notequal nil )nil reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_def nil )nil derivatives_def nil )nil derivatives_def nil )"[T -> real]" real_fun_ops "reals/" )nil derivatives_def nil ))nil ))nil 3253536989"" (skolem!)"" (auto-rewrite "derivable?" "identity_NQ" "deriv_TCC" )"" (assert )"" (use "const_fun_convergent[(A(x!1))]" ("b" "1" "c" "0" ))nil nil ))nil ))nil ))nil )nil derivatives_def nil )nil lim_of_functions nil )"setof[real]" convergence_functions nil )set type-eq-decl nil sets nil ) (fullset const-decl "set" sets 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 -> boolean]" derivatives_def nil )nil derivatives_def nil )nil booleans nil )nil defined_types nil )"setof[nzreal]" derivatives_def nil )nil derivatives_def nil )"bool" derivatives_def nil )"continuous_fun" nil )"continuous_fun" nil ))nil ))nil 3253536989"" (auto-rewrite "derivable?" )"" (skosimp :preds? t) (("" (assert ) nil nil )) nil )) nil )"bool" derivatives_def nil )nil derivatives_def nil )"[real -> boolean]" derivatives_def 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 ))nil 3297521117"" (skosimp*)"" (prop)"1" (expand "derivable?" )"1" (expand "convergent?" ) (("1" (inst + "l!1" ) nil nil ))nil ))nil )"2" (expand "deriv" )"2" (rewrite "lim_fun_def" )"2" (hide 2)"2" (expand "convergent?" ) (("2" (inst + "l!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" lim_of_functions nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" derivatives_def nil )nil lim_of_functions nil )"real" derivatives_def nil )"boolean" notequal nil )nil reals nil )"[real -> boolean]" derivatives_def nil )nil derivatives_def nil )nil booleans nil )nil defined_types nil )"setof[nzreal]" derivatives_def nil )"real" derivatives_def nil ))nil 3253536989"" (skosimp) (("" (rewrite "sum_derivable" ) nil nil )) nil )nil derivatives_def nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_def nil )nil derivatives_def nil ))nil ))nil 3253536989"" (skosimp)"" "deriv_TCC" "sum_derivable" "derivable?" "deriv" "sum_NQ" "lim_sum_fun[(A(x!1))]" )"" (assert ) nil nil )) nil ))nil )"bool" derivatives_def nil )nil derivatives_def nil )"setof[nzreal]" derivatives_def nil )nil defined_types nil )nil booleans nil )nil derivatives_def nil )"[real -> boolean]" derivatives_def 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 lim_of_functions nil )"real" derivatives_def nil )"real" reals nil ))nil ))nil 3442582979"" (lemma "neg_derivable" ) (("" (propax) nil nil )) nil )nil derivatives_def nil )) shostak))nil 3442586421"" (skosimp)"" "deriv_TCC" "neg_derivable" "derivable?" "deriv" "neg_NQ" "lim_neg_fun[(A(x!1))]" )"" (assert ) nil nil )) nil ))nil )"bool" derivatives_def nil )nil derivatives_def nil )"setof[nzreal]" derivatives_def nil )nil defined_types nil )nil booleans nil )nil derivatives_def nil )"[real -> boolean]" derivatives_def 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 lim_of_functions nil )"real" derivatives_def nil )"real" reals nil ))nil )nil 3442586370";;; Proof for formula derivatives_def.deriv_opposite" (skosimp) ";;; Proof for formula derivatives_def.deriv_opposite" "deriv_TCC" "opposite_derivable" "derivable?" "deriv" "opposite_NQ" "lim_opposite_fun[(A(x!1))]" )";;; Proof for formula derivatives_def.deriv_opposite" (assert) nil ))))"" )nil nil ))nil 3253536989"" (skosimp) (("" (rewrite "diff_derivable" ) nil nil )) nil )nil derivatives_def nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_def nil )nil derivatives_def nil ))nil ))nil 3253536989"" (skosimp)"" "deriv_TCC" "diff_derivable" "derivable?" "deriv" "diff_NQ" "lim_diff_fun[(A(x!1))]" )"" (assert ) nil nil )) nil ))nil )"bool" derivatives_def nil )nil derivatives_def nil )"setof[nzreal]" derivatives_def nil )nil defined_types nil )nil booleans nil )nil derivatives_def nil )"[real -> boolean]" derivatives_def 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 lim_of_functions nil )"real" derivatives_def nil )"real" reals nil ))nil ))nil 3253536989"" (skosimp) (("" (rewrite "prod_derivable" ) nil nil )) nil )nil derivatives_def nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_def nil )nil derivatives_def nil ))nil ))nil 3253536989"" (skosimp)"" (use "prod_derivable" )"" (assert )"" "deriv" "deriv_TCC" "derivable?" "lim_fun_def[(A(x!1))]" "lim_fun_lemma[(A(x!1))]" ))"" (assert )"" "cnv_seq_prod_NQ" "l1" "lim(NQ(f1!1, x!1), 0)" "l2" "lim(NQ(f2!1, x!1), 0)" ))"" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil derivatives_def nil )nil derivatives_def nil )"[real -> boolean]" derivatives_def 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 )"real" reals nil )"real" derivatives_def nil )"{l: real | convergence(f, x0, l)}" nil )"bool" lim_of_functions nil )"bool" lim_of_functions nil )nil derivatives_def nil )nil lim_of_functions nil )"bool" derivatives_def nil )"real" derivatives_def nil )"setof[nzreal]" derivatives_def nil )nil defined_types nil )nil booleans nil )nil reals nil )"boolean" notequal nil )nil lim_of_functions nil ))nil ))nil 3253536989"" (lemma "const_derivable" ) (("" (propax) nil nil )) nil )nil derivatives_def nil )) nil ))nil 3253536989"" (skosimp)"" "deriv_TCC" "const_derivable" "derivable?" "deriv" "const_NQ" )"" (assert )"" (use "lim_const_fun[(A(x!1))]" ("b" "0" "c" "0" )) nil nil ))nil ))nil ))nil )nil derivatives_def nil )nil lim_of_functions nil )"setof[real]" convergence_functions nil )set type-eq-decl nil sets nil ) (fullset const-decl "set" sets 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 -> boolean]" derivatives_def nil )nil derivatives_def nil )nil booleans nil )nil defined_types nil )"setof[nzreal]" derivatives_def nil )nil derivatives_def nil )"real" derivatives_def nil )"continuous_fun" nil ))nil ))nil 3253536989"" (lemma "scal_derivable" ) (("" (propax) nil nil )) nil )nil derivatives_def nil )) nil ))nil 3253536989"" (skosimp)"" "deriv_TCC" "scal_derivable" "derivable?" "deriv" "scal_NQ" "lim_scal_fun[(A(x!1))]" )"" (assert ) nil nil )) nil ))nil )"bool" derivatives_def nil )nil derivatives_def nil )"setof[nzreal]" derivatives_def nil )nil defined_types nil )nil booleans nil )nil derivatives_def nil )"[real -> boolean]" derivatives_def 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 lim_of_functions nil )"real" derivatives_def nil )"real" reals nil ))nil ))nil 3253536989"" (lemma "inv_derivable" ) (("" (propax) nil nil )) nil )nil derivatives_def nil )) nil ))nil 3253536989"" (skosimp)"" (forward-chain "inv_derivable" )"" (assert )"" "deriv" "deriv_TCC" "derivable?" "lim_fun_def[(A(x!1))]" "lim_fun_lemma[(A(x!1))]" ))"" (assert )"" (use "cnv_seq_inv_NQ" ("l1" "lim(NQ(g!1, x!1), 0)" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil derivatives_def nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_def nil )nil derivatives_def nil )"boolean" notequal nil )nil reals nil )"real" derivatives_def nil )"{l: real | convergence(f, x0, l)}" nil )"bool" lim_of_functions nil )"bool" lim_of_functions nil )nil derivatives_def nil )"bool" derivatives_def nil )"real" derivatives_def nil )"setof[nzreal]" derivatives_def nil )nil defined_types nil )nil booleans nil )nil lim_of_functions nil )"real" reals nil )"real" reals nil )"nzreal" nil ))nil ))nil 3253536989"" (skosimp) (("" (rewrite "div_derivable" ) nil nil )) nil )nil derivatives_def nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_def nil )nil derivatives_def nil )"boolean" notequal nil )nil reals nil ))nil ))nil 3253536989"" nil :rewrites"inv_derivable" "deriv_inv" "deriv_prod" "div_function[T]" "/" ))nil nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil derivatives_def nil )"[T -> real]" real_fun_ops "reals/" )nil derivatives_def nil )nil derivatives_def nil )"real" reals nil )"real" reals nil )"nzreal" nil )"real" reals nil )nil derivatives_def nil )"[real -> boolean]" derivatives_def 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_fun_ops "reals/" )"real" reals nil )"real" reals nil )"nzreal" nil ))nil ))nil 3253536989"" (lemma "identity_derivable" ) (("" (propax) nil nil )) nil )nil derivatives_def nil )) nil ))nil 3253536989"" (skosimp)"" "deriv_TCC" "identity_derivable" "derivable?" "deriv" "identity_NQ" )"" (use "lim_const_fun[(A(x!1))]" ("b" "1" "c" "0" ))"" (assert ) nil nil )) nil ))nil ))nil )nil derivatives_def nil )"real" derivatives_def nil )"continuous_fun" nil )"continuous_fun" nil )"setof[nzreal]" derivatives_def nil )nil defined_types nil )nil booleans nil )nil derivatives_def nil )"[real -> boolean]" derivatives_def 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 )"set" sets nil ) (set type-eq-decl nil sets nil )"setof[real]" convergence_functions nil )nil lim_of_functions nil )nil derivatives_def nil ))nil )))quality 100%
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.13Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤ *Eine klare Vorstellung vom Zielzustand
2026-03-28
