Quelle nth_derivatives.prf
Sprache: Lisp
(nth_derivativesnil 3445338281"" (skosimp*)"" (lemma "deriv_domain" ) (("" (propax) nil nil )) nil )) nil )nil nth_derivatives nil )) nil ))nil 3445338281"" (skosimp*)"" (lemma "not_one_element" ) (("" (inst?) nil nil )) nil )) nil )nil nth_derivatives nil )) nil ))nil 3445338281 ("" (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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"int" integers nil )"(total_order?[real])" nil )"set" sets nil )"setof[real]" convergence_functions nil )"real" derivatives_def nil )"bool" convergence_functions nil )"bool" lim_of_functions nil )"bool" lim_of_functions nil )"bool" derivatives_def nil )"bool" derivatives nil )"real" reals nil )"real" reals nil ))nil ))nil 3445338281"" (termination-tcc) nil nil )"set" sets nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"setof[real]" convergence_functions nil )"real" derivatives_def nil )"bool" convergence_functions nil )"bool" lim_of_functions nil )"bool" lim_of_functions nil )"bool" derivatives_def nil )"bool" derivatives nil )"real" reals nil )"real" reals nil ))nil ))nil 3255355367"" (induct "n" )"1" (skolem 1 ("f" "m" ))"1" (lemma "trichotomy" ("x" "m" ))"1" (split -1)"1" (assert ) nil nil )"2" (replace -1) (("2" (flatten) nil nil )) nil )"3" (assert ) nil nil ))nil ))nil ))nil )"2" (skolem 1 ("j" ))"2" (flatten)"2" (skolem 1 ("f" "m" ))"2" (flatten)"2" (expand "<=" -3)"2" (split -3)"1" (inst - "f" "m" )"1" (split -2)"1" (propax) nil nil )"2" (hide -1 2)"2" case "FORALL (f:[T->real],k: nat): derivable_n_times?(f, k + 1) IMPLIES derivable_n_times?(f, k)" )"1" (inst - "f" "j" ) (("1" (assert ) nil nil ))nil )"2" (hide -1 2)"2" (induct "k" )"1" (expand "derivable_n_times?" )"1" (propax) nil nil )) nil )"2" (skolem 1 ("k" ))"2" "2" "g" ))"2" "2" expand "derivable_n_times?" 1)"2" expand "derivable_n_times?" "2" "2" assert )"2" "deriv(g)" )"1" (assert ) nil nil )"2" "not_one_element" )"2" expand "not_one_element?" )"2" nil nil ))nil ))nil )"3" "deriv_domain" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil )"2" (replace -1) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"bool" deriv_domain_def nil )"bool" deriv_domain_def nil )"[T -> real]" derivatives nil )nil derivatives nil )"bool" derivatives nil )nil nth_derivatives nil )nil nth_derivatives nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil real_axioms nil )nil naturalnumbers nil )"bool" reals nil )"bool" nth_derivatives nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil nth_derivatives nil )"[real -> boolean]" nth_derivatives nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3298378055"" (skosimp*)"" (lemma "derivable_n_times_lem" )"" (inst - "f!1" "1" "n!1+1" )"" (assert )"" (expand "derivable_n_times?" ) (("" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )nil nth_derivatives nil )"(total_order?[real])" nil )"bool" nth_derivatives 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 )nil nth_derivatives nil )"[real -> boolean]" nth_derivatives nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posint" nil ))nil 3298378055"" (lemma "deriv_domain" ) (("" (skosimp*) nil nil )) nil )nil nth_derivatives nil )) shostak))nil 3298378055"" (lemma "not_one_element" ) (("" (skosimp*) nil nil )) nil )nil nth_derivatives nil )) shostak))nil 3298378047"" (skosimp*)"" (expand "derivable_n_times?" -1) (("" (flatten) nil nil ))nil ))nil )"bool" nth_derivatives nil )) shostak))nil 3255355367 ("" (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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"[real -> boolean]" nth_derivatives nil )nil nth_derivatives nil )"bool" nth_derivatives nil )nil nth_derivatives nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3255355367"" (skosimp*)"" (typepred "f!1" )"" (expand "derivable_n_times?" ) (("" (ground) nil nil )) nil ))nil ))nil )nil nth_derivatives nil )"bool" nth_derivatives nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil nth_derivatives nil )"[real -> boolean]" nth_derivatives 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 3255355367"" (skosimp*)"" (typepred "f!1" )"" (expand "derivable_n_times?" -1) (("" (ground) nil nil ))nil ))nil ))nil )nil nth_derivatives nil )"bool" nth_derivatives nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil nth_derivatives nil )"[real -> boolean]" nth_derivatives 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 3255355367 ("" (termination-tcc) nil nil ) nil nil ))nil 3255355367"" (skosimp*)"" (lemma "derivable_n_times_lem" )"" (inst -1 "f!1" "m!1" "1+n!1" ) (("" (assert ) nil nil )) nil ))nil ))nil )nil nth_derivatives nil )"(total_order?[real])" 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 )nil nth_derivatives nil )"[real -> boolean]" nth_derivatives nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posint" nil ))nil ))nil 3255355367"" (skosimp*)"" (lemma "deriv_domain" ) (("" (inst?) nil nil )) nil )) nil )nil nth_derivatives nil )) nil ))nil 3255355367"" (skosimp*)"" (lemma "not_one_element" ) (("" (propax) nil nil )) nil )) nil )nil nth_derivatives nil )) nil ))nil 3255355367"" (induct "m" )"1" (expand "nderiv" )"1" (expand "derivable_n_times?" )"1" (assert ) (("1" (skosimp*) nil nil )) nil )) nil ))nil )"2" (skolem 1 ("j" ))"2" (flatten)"2" (skolem 1 ("f" "n" ))"2" (flatten 1)"2" (expand "<=" -2)"2" (split -2)"1" (expand "nderiv" 1)"1" (expand "derivable_n_times?" -3)"1" (flatten -3)"1" (inst - "deriv(f)" "n-1" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (lemma "not_one_element" )"3" (expand "not_one_element?" )"3" (propax) nil nil )) nil ))nil )"4" (lemma "deriv_domain" )"4" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "derivable_n_times?" -3)"2" (flatten -3)"2" (expand "nderiv" 1)"2" (inst - "deriv(f)" "n-1" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (lemma "not_one_element" )"3" (expand "not_one_element?" )"3" (propax) nil nil )) nil ))nil )"4" (lemma "deriv_domain" )"4" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skolem!)"3" (flatten 1)"3" (lemma "not_one_element" )"3" (expand "not_one_element?" ) (("3" (propax) nil nil ))nil ))nil ))nil ))nil )"4" (lemma "deriv_domain" )"4" (skolem! 1) (("4" (flatten 1) nil nil )) nil )) nil )"5" (lemma "derivable_n_times_lem" )"5" (hide 2)"5" (skosimp*)"5" (inst - "f!1" "m!2" "1+n!1" ) (("5" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil nth_derivatives nil )nil nth_derivatives nil )nil nth_derivatives nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil derivatives nil )"[T -> real]" derivatives nil )"nat" nth_derivatives nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"(total_order?[real])" nil )nil naturalnumbers nil )"[T -> real]" nth_derivatives nil )nil nth_derivatives nil )"bool" derivatives nil )nil defined_types nil )"bool" deriv_domain_def nil )"bool" deriv_domain_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]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[real -> boolean]" nth_derivatives nil )nil nth_derivatives nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"bool" nth_derivatives nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil ))nil ))nil 3255545563"" (skosimp*) (("" (assert ) nil nil )) nil )"posint" nil )"posint" nil ))nil 3255545563"" (skosimp*)"" "derivable_n_times_lem" ("f" "f!1" "n" "n!1+1" "m" "n!1" ))"" (assert ) nil nil )) nil ))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 )nil nth_derivatives nil )"[real -> boolean]" nth_derivatives nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nth_derivatives nil )"posint" nil )"(total_order?[real])" nil ))nil 3255545563"" (skosimp*)"" (lemma "nderiv_derivable" ("m" "n!1" "n" "n!1" "f" "f!1" ))"" (assert ) nil nil )) nil ))nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil nth_derivatives nil )"[real -> boolean]" nth_derivatives nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nth_derivatives nil )"posint" nil )"(total_order?[real])" nil )"posint" nil ))nil 3255542603"" (induct "n" )"1" (expand "nderiv" )"1" (expand "nderiv" ) (("1" (propax) nil nil )) nil )) nil )"2" (skosimp*)"2" (expand "nderiv" 1 1)"2" (inst-cp - "deriv(f!1)" )"1" (expand "derivable_n_times?" -3)"1" (flatten -3)"1" (assert )"1" (replace -2 1)"1" (expand "nderiv" 1 2) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "not_one_element" )"2" (expand "not_one_element?" ) (("2" (propax) nil nil ))nil ))nil )"3" (lemma "deriv_domain" ) (("3" (propax) nil nil )) nil ))nil ))nil ))nil )"3" (skolem!)"3" (flatten 1)"3" (lemma "not_one_element" )"3" (expand "not_one_element?" ) (("3" (propax) nil nil ))nil ))nil ))nil ))nil )"4" (lemma "deriv_domain" )"4" (skolem!) (("4" (flatten 1) nil nil )) nil )) nil )"5" (hide 2)"5" (skosimp*)"5" "nderiv_derivable" ("f" "f!1" "n" "n!2" "m" "n!2" ))"5" (assert ) nil nil )) nil ))nil ))nil )"6" (hide 2)"6" (skosimp*)"6" "derivable_n_times_lem" "f" "f!1" "n" "1+n!2" "m" "n!2" ))"6" (assert ) nil nil )) nil ))nil ))nil )"7" (hide 2) (("7" (skosimp*) nil nil )) nil ))nil )nil nth_derivatives nil )nil nth_derivatives nil )"(total_order?[real])" nil )"posint" nil )nil nth_derivatives nil )nil nth_derivatives nil )nil naturalnumbers nil )"[T -> real]" derivatives nil )nil derivatives nil )"[T, T -> boolean]" equalities nil )nil defined_types nil )"bool" deriv_domain_def nil )"bool" deriv_domain_def nil )"bool" derivatives nil )nil nth_derivatives nil )"[T -> real]" nth_derivatives 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]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[real -> boolean]" nth_derivatives nil )nil nth_derivatives nil )"[bool, bool -> bool]" booleans nil )"bool" nth_derivatives nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil ))nil 3255550372"" (lemma "deriv_domain" )"" (replace -1) (("" (skosimp*) nil nil )) nil )) nil )nil nth_derivatives nil )) shostak))nil 3255550372"" (lemma "not_one_element" )"" (replace -1) (("" (skosimp*) nil nil )) nil )) nil )nil nth_derivatives nil )) shostak))nil 3255548066"" (induct "n" )"1" (expand "nderiv" )"1" (expand "derivable_n_times?" )"1" (expand "derivable_n_times?" ) (("1" (propax) nil nil ))nil ))nil ))nil )"2" (skolem 1 ("j" ))"2" (flatten 1)"2" (skolem 1 ("f" ))"2" (split 1)"1" (flatten)"1" (split 1)"1" "derivable_n_times_lem" "f" "f" "n" "j+2" "m" "j+1" ))"1" (assert ) nil nil )) nil )"2" (inst - "deriv(f)" )"1" (expand "derivable_n_times?" -1)"1" (flatten -1)"1" (assert )"1" (flatten -3)"1" (expand "nderiv" 1)"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (lemma "not_one_element" )"2" (expand "not_one_element?" )"2" (propax) nil nil )) nil ))nil )"3" (lemma "deriv_domain" ) (("3" (propax) nil nil ))nil )"4" (expand "derivable_n_times?" -1)"4" (flatten) nil nil )) nil ))nil ))nil ))nil )"2" (flatten)"2" (inst - "deriv(f)" )"1" (flatten -3)"1" (expand "derivable_n_times?" 1)"1" (expand "derivable_n_times?" -1)"1" (flatten -1)"1" (replace -2)"1" (expand "nderiv" -3)"1" (replace -3) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "not_one_element" )"2" (expand "not_one_element?" )"2" (propax) nil nil )) nil ))nil )"3" (lemma "deriv_domain" ) (("3" (propax) nil nil ))nil )"4" (expand "derivable_n_times?" -1)"4" (flatten -1) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (lemma "not_one_element" )"3" (skosimp*)"3" (expand "not_one_element?" ) (("3" (propax) nil nil ))nil ))nil ))nil ))nil )"4" (lemma "deriv_domain" )"4" (replace -1) (("4" (skosimp*) nil nil )) nil )) nil ))nil )"[T -> real]" nth_derivatives nil )"[T -> real]" derivatives nil )nil derivatives nil )nil nth_derivatives nil )nil nth_derivatives nil )"posint" nil )nil nth_derivatives nil )"(total_order?[real])" nil )nil naturalnumbers nil )"[T -> real]" nth_derivatives nil )nil nth_derivatives nil )"bool" derivatives nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )nil defined_types nil )"bool" deriv_domain_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]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[real -> boolean]" nth_derivatives nil )nil nth_derivatives nil )"[bool, bool -> bool]" booleans nil )"bool" nth_derivatives nil )"bool" deriv_domain_def nil )"posint" nil ))quality 100%
¤ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-03-28
