Quelle sincos.prf
Sprache: Lisp
(sincosnil 3602247635 ("" (assert ) nil nil )nil deriv_domain "analysis_ax/" ))nil ))nil 3602247635 ("" (assert ) nil nil )nil deriv_domain"analysis_ax/" ))nil ))nil 3263379563"" (skolem 1 ("x" ))"" (lemma "sin_convergence" ("x" "x" ))"" "derivative_equivalence1[real]" "f" "sin" "x" "x" "D" "cos(x)" ))"1" (assert ) nil nil )"2" (skosimp*)"2" (inst + "x!1+1" ) (("2" (assert ) nil nil )) nil )) nil )"3" (lemma deriv_domain_real) (("3" (propax) nil nil )) nil ))nil ))nil ))nil )"bool" deriv_domain_def"analysis_ax/" )"bool" deriv_domain_def "analysis_ax/" ))nil 3602248246"" (expand "derivable?" )"" (lemma "sin_derivable" ) (("" (propax) nil nil )) nil )) nil )nil sincos nil )"bool" derivatives "analysis_ax/" ))nil 3263377309"" (lemma "sin_derivable_fun" ) (("" (propax) nil nil )) nil )nil sincos nil )) shostak))nil 3263490807"" (expand "deriv" )"" "extensionality" "f" "(LAMBDA (x: real): deriv(sin, x))" "g" "cos" ))"1" (split -1)"1" (propax) nil nil )"2" (hide 2)"2" (skosimp*)"2" "derivative_equivalence1[real]" "f" "sin" "x" "x!1" "D" "cos(x!1)" ))"1" (lemma "sin_convergence" ("x" "x!1" ))"1" (assert ) nil nil )) nil )"2" (lemma "sin_derivable" )"2" (skosimp*)"2" (inst + "x!2+1" ) (("2" (assert ) nil nil )) nil ))nil ))nil )"3" (lemma deriv_domain_real) (("3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "sin_derivable" ) (("2" (propax) nil nil )) nil ))nil ))nil )"real" derivatives_def "analysis_ax/" )"bool" derivatives_def "analysis_ax/" )"bool" deriv_domain_def "analysis_ax/" )"bool" deriv_domain_def"analysis_ax/" )"[T -> real]" derivatives "analysis_ax/" ))nil 3263378610"" (skosimp*)"" (lemma "cos_convergence" ("x" "x!1" ))"" "derivative_equivalence1[real]" "f" "cos" "x" "x!1" "D" "-sin(x!1)" ))"1" (assert ) nil nil )"2" (skosimp*)"2" (inst + "x!2+1" ) (("2" (assert ) nil nil )) nil )) nil )"3" (lemma deriv_domain_real) (("3" (propax) nil nil )) nil ))nil ))nil ))nil )"bool" deriv_domain_def"analysis_ax/" )"bool" deriv_domain_def "analysis_ax/" ))nil 3602248261"" (expand "derivable?" )"" (lemma "cos_derivable" ) (("" (propax) nil nil )) nil )) nil )nil sincos nil )"bool" derivatives "analysis_ax/" ))nil 3263377338"" (lemma "cos_derivable_fun" ) (("" (propax) nil nil )) nil )nil sincos nil )) shostak))nil 3352175440"" (expand "deriv" )"" (lemma "cos_convergence" )"" (lemma "derivative_equivalence1[real]" ("f" "cos" ))"1" "extensionality" "f" "(LAMBDA (x: real): deriv(cos, x))" "g" "-sin" ))"1" (split -1)"1" (propax) nil nil )"2" (hide 2)"2" (skosimp*)"2" (expand "-" )"2" (inst - "x!1" )"2" (inst - "-sin(x!1)" "x!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (inst - "x!1" )"2" (inst - "-sin(x!1)" "x!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst + "x!1+1" ) (("2" (assert ) nil nil )) nil )) nil )"3" (lemma deriv_domain_real) (("3" (propax) nil nil )) nil ))nil ))nil ))nil )"real" derivatives_def "analysis_ax/" )"bool" derivatives_def "analysis_ax/" )"bool" deriv_domain_def"analysis_ax/" )"bool" deriv_domain_def "analysis_ax/" )"[T -> real]" derivatives "analysis_ax/" ))nil )nil 3263377393"" (expand "deriv" )"" (lemma "cos_convergence" )"" (lemma "derivative_equivalence1" ("f" "cos" ))"" "extensionality" "f" "(LAMBDA (x: real): deriv(cos, x))" "g" "-sin" ))"1" (split -1)"1" (propax) nil nil )"2" (hide 2)"2" (skosimp*)"2" (expand "-" )"2" (inst - "x!1" )"2" (inst - "-sin(x!1)" "x!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (inst - "x!1" )"2" (inst - "-sin(x!1)" "x!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T -> real]" derivatives "analysis_ax/" )"[T -> real]" derivatives "analysis_ax/" ))nil 3352175475"" (skosimp*)"" (lemma "sin_derivable" ("x" "x0!1" ))"" (lemma "derivable_continuous[real]" ("f" "sin" "x" "x0!1" ))"" (assert ) nil nil )) nil ))nil ))nil )nil derivatives_def"analysis_ax/" )"real" trig_basic nil ))nil )nil 3266853726"" (skosimp*)"" (lemma "sin_derivable" ("x" "x0!1" ))"" (lemma "derivable_continuous" ("f" "sin" "x" "x0!1" ))"" (assert ) nil nil )) nil ))nil ))nil )nil shostak))nil 3352175502"" (skosimp*)"" (lemma "cos_derivable" ("x" "x0!1" ))"" (lemma "derivable_continuous[real]" ("f" "cos" "x" "x0!1" ))"" (assert ) nil nil )) nil ))nil ))nil )nil derivatives_def"analysis_ax/" )"real" trig_basic nil ))nil )nil 3266853851"" (skosimp*)"" (lemma "cos_derivable" ("x" "x0!1" ))"" (lemma "derivable_continuous" ("f" "cos" "x" "x0!1" ))"" (assert ) nil nil )) nil ))nil ))nil )nil shostak))nil 3602248362"" (expand "continuous?" )"" (lemma "sin_continuous" ) (("" (propax) nil nil )) nil )) nil )nil sincos nil )"bool" continuous_functions"analysis_ax/" ))nil 3602248393"" (expand "continuous?" )"" (lemma "cos_continuous" ) (("" (propax) nil nil )) nil )) nil )nil sincos nil )"bool" continuous_functions"analysis_ax/" ))nil 3445346452"" (skolem 1 ("n" ))"" case "FORALL (n:nat): derivable_n_times?(sin, n) AND derivable_n_times?(cos,n)" )"1" case "FORALL (n:nat): nderiv(n, sin) = (LAMBDA (x: real): sin((n * pi / 2) + x)) AND nderiv(n,cos) = LAMBDA (x:real): cos((n*pi/2)+x)" )"1" (inst - "n" )"1" (inst - "n" )"1" (flatten) (("1" (assert ) nil nil )) nil )) nil ))nil )"2" (hide 2)"2" (copy -1)"2" (induct "n" 1)"1" (expand "nderiv" )"1" "extensionality" "f" "sin" "g" "(LAMBDA (x: real): sin(x + (0 * pi / 2)))" ))"1" (split -1)"1" (propax) nil nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (expand "nderiv" )"2" "extensionality" "f" "cos" "g" "(LAMBDA (x: real): cos(x + (0 * pi / 2)))" ))"2" (split -1)"1" (propax) nil nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (skosimp*)"3" (expand "nderiv" 1)"3" (lemma "deriv_sin_fun" )"3" (replace -1)"3" (replace -3)"3" (lemma "deriv_cos_fun" )"3" (replace -1)"3" "extensionality" "f" "(LAMBDA (x: real): cos((j!1 * pi / 2) + x))" "g" "(LAMBDA (x: real): sin(x + ((j!1 * pi + pi) / 2)))" ))"3" "1" replace -1)"1" case "FORALL (n:nat,f:nderiv_fun(n)): nderiv(n,-f) = -nderiv(n,f)" )"1" "j!1" "sin" )"1" replace -1)"1" replace -5)"1" "1" expand "-" )"1" "extensionality" "f" "(LAMBDA (x_1: real): -sin(x_1 + (j!1 * pi / 2)))" "g" "(LAMBDA (x: real): cos(x + ((j!1 * pi + pi) / 2)))" ))"1" "1" nil nil )"2" "2" "2" rewrite "cos_sin" )"2" rewrite "neg_sin" )"2" expand "pi" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "j!1" )"2" "2" "2" "n" )"1" expand "nderiv" )"1" (propax) nil nil ))nil )"2" "2" expand "nderiv" 1)"2" "deriv_neg_fun[real]" "ff" "f!1" ))"2" replace -1)"2" "deriv(f!1)" )nil nil ))nil ))nil ))nil ))nil )"3" "3" "n" )"1" expand "derivable_n_times?" )"1" nil nil ))nil )"2" "2" expand "derivable_n_times?" "2" "f!1" )"2" expand "derivable_n_times?" "2" "2" "neg_derivable_fun[real]" "f" "f!1" ))"2" assert )"2" "deriv_neg_fun[real]" "ff" "f!1" ))"2" replace "2" "deriv(f!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "n" )"1" "1" expand "derivable_n_times?" )"1" (propax) nil nil ))nil ))nil )"2" "2" expand "derivable_n_times?" "2" "neg_derivable_fun[real]" "f" "f!1" ))"2" assert )"2" "f!1" )"2" expand "derivable_n_times?" "2" "2" assert )"2" "deriv_neg_fun[real]" "ff" "f!1" ))"2" replace "2" "deriv(f!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "cos_sin" "a" "(j!1 * pi / 2) + x!1" ))"2" expand "pi" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (skosimp*)"4" (inst - "n!2" ) (("4" (flatten) nil nil )) nil ))nil )"5" (skosimp*)"5" (inst - "n!2" ) (("5" (flatten) nil nil )) nil ))nil )"6" (skosimp*)"6" (inst - "n!2" ) (("6" (flatten) nil nil )) nil ))nil )"7" (skosimp*)"7" (inst - "n!2" ) (("7" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (inst - "n!1" ) (("3" (flatten -2) nil nil )) nil )) nil )"4" (skosimp*)"4" (inst - "n!1" ) (("4" (flatten) nil nil )) nil )) nil ))nil )"2" (hide 2)"2" (induct "n" )"1" (expand "derivable_n_times?" ) (("1" (propax) nil nil ))nil )"2" (expand "derivable_n_times?" ) (("2" (propax) nil nil ))nil )"3" (skosimp*)"3" (expand "derivable_n_times?" 1)"3" (lemma "sin_derivable_fun" )"3" (lemma "cos_derivable_fun" )"3" (lemma "deriv_sin_fun" )"3" (lemma "deriv_cos_fun" )"3" (replace -1)"3" (replace -2)"3" (assert )"3" case "FORALL (n:nat,f:[real->real]): derivable_n_times?(f,n) => derivable_n_times?(-f,n)" )"1" "j!1" "sin" )"1" (assert ) nil nil ))nil )"2" "2" "n" )"1" expand "derivable_n_times?" )"1" (propax) nil nil ))nil )"2" "2" expand "derivable_n_times?" "2" "2" "neg_derivable_fun[real]" "f" "f!1" ))"2" assert )"2" "deriv(f!1)" )"2" assert )"2" "deriv_neg_fun[real]" "ff" "f!1" ))"2" replace -1 1)"2" 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 )"bool" nth_derivatives "analysis_ax/" )nil derivatives "analysis_ax/" )nil derivatives "analysis_ax/" )"bool" derivatives "analysis_ax/" )nil derivatives "analysis_ax/" )"[T -> real]" derivatives "analysis_ax/" )nil trig_basic nil )nil trig_basic nil )nil nth_derivatives "analysis_ax/" )"[T -> real]" nth_derivatives "analysis_ax/" ))nil )nil 3445346393";;; Proof nderiv_sin_fun-3 for formula sincos.nderiv_sin_fun" "n" ))";;; Proof nderiv_sin_fun-3 for formula sincos.nderiv_sin_fun" case "FORALL (n:nat): derivable_n_times?(sin, n) AND derivable_n_times?(cos,n)" )"1" case "FORALL (n:nat): nderiv(n, sin) = (LAMBDA (x: real): sin((n * pi / 2) + x)) AND nderiv(n,cos) = LAMBDA (x:real): cos((n*pi/2)+x)" )"1" (inst - "n" )"1" (inst - "n" ) (("1" (flatten) (("1" (assert ) nil )))))))"2" (hide 2)"2" (copy -1)"2" (induct "n" 1)"1" (expand "nderiv" )"1" "extensionality" "f" "sin" "g" "(LAMBDA (x: real): sin(x + (0 * pi / 2)))" ))"1" (split -1)"1" (propax) nil )"2" (skosimp*) (("2" (assert ) nil )))))))))"2" (expand "nderiv" )"2" "extensionality" "f" "cos" "g" "(LAMBDA (x: real): cos(x + (0 * pi / 2)))" ))"2" (split -1)"1" (propax) nil )"2" (skosimp*) (("2" (assert ) nil )))))))))"3" (skosimp*)"3" (expand "nderiv" 1)"3" (lemma "deriv_sin_fun" )"3" (replace -1)"3" (replace -3)"3" (lemma "deriv_cos_fun" )"3" (replace -1)"3" "extensionality" "f" "(LAMBDA (x: real): cos((j!1 * pi / 2) + x))" "g" "(LAMBDA (x: real): sin(x + ((j!1 * pi + pi) / 2)))" ))"3" "1" replace -1)"1" case "FORALL (n:nat,f:nderiv_fun(n)): nderiv(n,-f) = -nderiv(n,f)" )"1" "j!1" "sin" )"1" replace -1)"1" replace -5)"1" "1" expand "-" )"1" "extensionality" "f" "(LAMBDA (x_1: real): -sin(x_1 + (j!1 * pi / 2)))" "g" "(LAMBDA (x: real): cos(x + ((j!1 * pi + pi) / 2)))" ))"1" "1" (propax) nil )"2" "2" "2" rewrite "cos_sin" )"2" rewrite "neg_sin" )"2" expand "pi" )"2" assert )nil )))))))))))))))))))))))))"2" "j!1" )"2" "2" "2" "n" )"1" expand "nderiv" )"1" (propax) nil )))"2" "2" expand "nderiv" 1)"2" "deriv_neg_fun[real]" "ff" "f!1" ))"2" replace -1)"2" "deriv(f!1)" )nil )))))))))"3" "3" "n" )"1" expand "derivable_n_times?" )"1" (propax) nil )))"2" "2" expand "derivable_n_times?" "2" "f!1" )"2" expand "derivable_n_times?" "2" "2" "opposite_derivable_fun[real]" "f" "f!1" ))"2" assert )"2" "deriv_neg_fun[real]" "ff" "f!1" ))"2" replace "2" "deriv(f!1)" )nil )))))))))))))))))))))))))))))))"3" "3" "n" )"1" "1" expand "derivable_n_times?" )"1" (propax) nil )))))"2" "2" expand "derivable_n_times?" "2" "opposite_derivable_fun[real]" "f" "f!1" ))"2" assert )"2" "f!1" )"2" expand "derivable_n_times?" "2" "2" assert )"2" "deriv_neg_fun[real]" "ff" "f!1" ))"2" replace "2" "deriv(f!1)" )nil )))))))))))))))))))))))))))))"2" "2" "2" "cos_sin" "a" "(j!1 * pi / 2) + x!1" ))"2" expand "pi" )"2" assert )nil )))))))))))))))))))))))))))"4" (skosimp*)"4" (inst - "n!2" ) (("4" (flatten) nil )))))"5" (skosimp*)"5" (inst - "n!2" ) (("5" (flatten) nil )))))"6" (skosimp*)"6" (inst - "n!2" ) (("6" (flatten) nil )))))"7" (skosimp*)"7" (inst - "n!2" ) (("7" (flatten) nil )))))))))))"3" (skosimp*)"3" (inst - "n!1" ) (("3" (flatten -2) nil )))))"4" (skosimp*)"4" (inst - "n!1" ) (("4" (flatten) nil )))))))"2" (hide 2)"2" (induct "n" )"1" (expand "derivable_n_times?" ) (("1" (propax) nil )))"2" (expand "derivable_n_times?" ) (("2" (propax) nil )))"3" (skosimp*)"3" (expand "derivable_n_times?" 1)"3" (lemma "sin_derivable_fun" )"3" (lemma "cos_derivable_fun" )"3" (lemma "deriv_sin_fun" )"3" (lemma "deriv_cos_fun" )"3" (replace -1)"3" (replace -2)"3" (assert )"3" case "FORALL (n:nat,f:[real->real]): derivable_n_times?(f,n) => derivable_n_times?(-f,n)" )"1" "j!1" "sin" )"1" (assert ) nil )))"2" "2" "n" )"1" expand "derivable_n_times?" )"1" (propax) nil )))"2" "2" expand "derivable_n_times?" "2" "2" "opposite_derivable_fun[real]" "f" "f!1" ))"2" assert )"2" "deriv(f!1)" )"2" assert )"2" "deriv_neg_fun[real]" "ff" "f!1" ))"2" replace -1 1)"2" nil ))))))))))))))))))))))))))))))))))))))))))))))))))";;; developed with shostak decision procedures") nil nil )nil 3445346356";;; Proof nderiv_sin_fun-3 for formula sincos.nderiv_sin_fun" "n" ))";;; Proof nderiv_sin_fun-3 for formula sincos.nderiv_sin_fun" case "FORALL (n:nat): derivable_n_times?(sin, n) AND derivable_n_times?(cos,n)" )"1" case "FORALL (n:nat): nderiv(n, sin) = (LAMBDA (x: real): sin((n * pi / 2) + x)) AND nderiv(n,cos) = LAMBDA (x:real): cos((n*pi/2)+x)" )"1" (inst - "n" )"1" (inst - "n" ) (("1" (flatten) (("1" (assert ) nil )))))))"2" (hide 2)"2" (copy -1)"2" (induct "n" 1)"1" (expand "nderiv" )"1" "extensionality" "f" "sin" "g" "(LAMBDA (x: real): sin(x + (0 * pi / 2)))" ))"1" (split -1)"1" (propax) nil )"2" (skosimp*) (("2" (assert ) nil )))))))))"2" (expand "nderiv" )"2" "extensionality" "f" "cos" "g" "(LAMBDA (x: real): cos(x + (0 * pi / 2)))" ))"2" (split -1)"1" (propax) nil )"2" (skosimp*) (("2" (assert ) nil )))))))))"3" (skosimp*)"3" (expand "nderiv" 1)"3" (lemma "deriv_sin_fun" )"3" (replace -1)"3" (replace -3)"3" (lemma "deriv_cos_fun" )"3" (replace -1)"3" "extensionality" "f" "(LAMBDA (x: real): cos((j!1 * pi / 2) + x))" "g" "(LAMBDA (x: real): sin(x + ((j!1 * pi + pi) / 2)))" ))"3" "1" replace -1)"1" case "FORALL (n:nat,f:nderiv_fun(n)): nderiv(n,-f) = -nderiv(n,f)" )"1" "j!1" "sin" )"1" replace -1)"1" replace -5)"1" "1" expand "-" )"1" "extensionality" "f" "(LAMBDA (x_1: real): -sin(x_1 + (j!1 * pi / 2)))" "g" "(LAMBDA (x: real): cos(x + ((j!1 * pi + pi) / 2)))" ))"1" "1" (propax) nil )"2" "2" "2" rewrite "cos_sin" )"2" rewrite "neg_sin" )"2" expand "pi" )"2" assert )nil )))))))))))))))))))))))))"2" "j!1" )"2" "2" "2" "n" )"1" expand "nderiv" )"1" (propax) nil )))"2" "2" expand "nderiv" 1)"2" "deriv_opp_fun[real]" "ff" "f!1" ))"2" replace -1)"2" "deriv(f!1)" )nil )))))))))"3" "3" "n" )"1" expand "derivable_n_times?" )"1" (propax) nil )))"2" "2" expand "derivable_n_times?" "2" "f!1" )"2" expand "derivable_n_times?" "2" "2" "opposite_derivable_fun[real]" "f" "f!1" ))"2" assert )"2" "deriv_opp_fun[real]" "ff" "f!1" ))"2" replace "2" "deriv(f!1)" )nil )))))))))))))))))))))))))))))))"3" "3" "n" )"1" "1" expand "derivable_n_times?" )"1" (propax) nil )))))"2" "2" expand "derivable_n_times?" "2" "opposite_derivable_fun[real]" "f" "f!1" ))"2" assert )"2" "f!1" )"2" expand "derivable_n_times?" "2" "2" assert )"2" "deriv_opp_fun[real]" "ff" "f!1" ))"2" replace "2" "deriv(f!1)" )nil )))))))))))))))))))))))))))))"2" "2" "2" "cos_sin" "a" "(j!1 * pi / 2) + x!1" ))"2" expand "pi" )"2" assert )nil )))))))))))))))))))))))))))"4" (skosimp*)"4" (inst - "n!2" ) (("4" (flatten) nil )))))"5" (skosimp*)"5" (inst - "n!2" ) (("5" (flatten) nil )))))"6" (skosimp*)"6" (inst - "n!2" ) (("6" (flatten) nil )))))"7" (skosimp*)"7" (inst - "n!2" ) (("7" (flatten) nil )))))))))))"3" (skosimp*)"3" (inst - "n!1" ) (("3" (flatten -2) nil )))))"4" (skosimp*)"4" (inst - "n!1" ) (("4" (flatten) nil )))))))"2" (hide 2)"2" (induct "n" )"1" (expand "derivable_n_times?" ) (("1" (propax) nil )))"2" (expand "derivable_n_times?" ) (("2" (propax) nil )))"3" (skosimp*)"3" (expand "derivable_n_times?" 1)"3" (lemma "sin_derivable_fun" )"3" (lemma "cos_derivable_fun" )"3" (lemma "deriv_sin_fun" )"3" (lemma "deriv_cos_fun" )"3" (replace -1)"3" (replace -2)"3" (assert )"3" case "FORALL (n:nat,f:[real->real]): derivable_n_times?(f,n) => derivable_n_times?(-f,n)" )"1" "j!1" "sin" )"1" (assert ) nil )))"2" "2" "n" )"1" expand "derivable_n_times?" )"1" (propax) nil )))"2" "2" expand "derivable_n_times?" "2" "2" "opposite_derivable_fun[real]" "f" "f!1" ))"2" assert )"2" "deriv(f!1)" )"2" assert )"2" "deriv_opp_fun[real]" "ff" "f!1" ))"2" replace -1 1)"2" nil ))))))))))))))))))))))))))))))))))))))))))))))))))";;; developed with shostak decision procedures") nil nil ))nil 3445346583"" (induct "n" )"1" (expand "derivable_n_times?" ) (("1" (propax) nil nil )) nil )"2" (expand "nderiv" )"2" "extensionality" "f" "cos" "g" "(LAMBDA (x: real): cos(x + (0 * pi / 2)))" ))"2" (split -1)"1" (propax) nil nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (skosimp*)"3" (expand "derivable_n_times?" 1)"3" (lemma "cos_derivable_fun" )"3" (replace -1)"3" (lemma "deriv_cos_fun" )"3" (replace -1)"3" (expand "nderiv" 1)"3" (replace -1)"3" case "FORALL (n:nat,f:[real->real]): derivable_n_times?(f,n) => derivable_n_times?(-f,n)" )"1" case "FORALL (n: nat, f: nderiv_fun(n)): nderiv(n, -f) = -nderiv(n, f)" )"1" (inst -2 "j!1" "sin" )"1" (lemma "nderiv_sin_fun" ("n" "j!1" ))"1" (flatten -1)"1" assert )"1" "j!1" "sin" )"1" replace -3)"1" replace -2)"1" "1" expand "-" )"1" "extensionality" "f" "(LAMBDA (x_1: real): -sin(x_1 + (j!1 * pi / 2)))" "g" "(LAMBDA (x: real): cos(x + ((j!1 * pi + pi) / 2)))" ))"1" "1" (propax) nil nil )"2" "2" "2" rewrite "sin_cos" )"2" expand "pi" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (induct "n" )"1" (expand "nderiv" )"1" (propax) nil nil )) nil )"2" (skosimp*)"2" expand "nderiv" 1)"2" "f!1" )"2" expand "derivable_n_times?" -1)"2" "2" "neg_derivable_fun[real]" "f" "f!1" ))"2" assert )"2" "deriv_neg_fun[real]" "ff" "f!1" ))quality 100%
¤ Dauer der Verarbeitung: 0.46 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-03-28
