Impressum 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" ))"2" replace -1)"2" "deriv(f!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" "3" "f!1" )"3" "n!2" "f!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but (-1 1))"3" (skosimp*)"3" (typepred "f!1" )"3" "n!1" "f!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (induct "n" )"1" (expand "derivable_n_times?" )"1" (propax) nil nil )) nil )"2" (skosimp*)"2" (expand "derivable_n_times?" (1 -2))"2" "2" "neg_derivable_fun[real]" "f" "f!1" ))"2" assert )"2" "deriv_neg_fun[real]" "ff" "f!1" ))"2" replace -1)"2" "deriv(f!1)" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T -> real]" derivatives "analysis_ax/" )nil derivatives "analysis_ax/" )"bool" derivatives "analysis_ax/" )nil derivatives "analysis_ax/" )nil derivatives "analysis_ax/" )nil trig_basic nil )"[T -> real]" nth_derivatives "analysis_ax/" )nil nth_derivatives "analysis_ax/" )"bool" nth_derivatives"analysis_ax/" ))nil ))nil 3445346729"" (skosimp*)"" (lemma "nderiv_sin_fun" ("n" "3+2*n!1" ))"" (flatten) nil nil )) nil ))nil )"[numfield, numfield -> numfield]" number_fields 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 reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sincos nil )"odd_int" integers nil )"posint" nil ))nil )nil 3445345573 ("" (subtype-tcc) nil nil ) nil nil ))nil 3445345573 ("" (subtype-tcc) nil nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"boolean" notequal nil ))nil ))nil 3445591283"" (skosimp*)"" "Taylors" ("f" "sin" "n" "2*n!1+2" "aa" "0" "bb" "x!1" ))"1" (lemma "nderiv_sin_fun" ("n" "2*n!1+3" ))"1" (flatten)"1" (replace -1)"1" case "FORALL (n:nat): sigma(0, 2 * n + 2, LAMBDA (nn:nat):IF nn > 2 * n + 2 THEN 0") "1" (inst - "n!1" ) (("1" (assert ) nil nil )) nil )"2" (hide-all-but 1)"2" (expand "sin_series_n" )"2" (induct "n" )"1" (expand "sin_series_term" )"1" (expand "sigma" )"1" (expand "sigma" )"1" (expand "sigma" )"1" (expand "factorial" )"1" expand "factorial" )"1" expand "factorial" )"1" "nderiv_sin_fun" )"1" "1" )"1" "2" )"1" "1" replace -2)"1" replace -4)"1" rewrite "sin_0" )"1" "1" "sin_pi2" )"1" "sin_pi" )"1" replace -1)"1" replace -2)"1" assert )"1" rewrite "expt_x0" "1" assert )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" (expand "sigma" 1)"2" (expand "sigma" 1 1)"2" "sigma_eq[nat]" "low" "0" "high" "j!1" "F" "LAMBDA (i: nat): IF i > 1 + j!1 THEN 0 ELSE sin_series_term(x!1)(i) ENDIF" "G" "LAMBDA (i: nat): IF i > j!1 THEN 0 ELSE sin_series_term(x!1)(i) ENDIF")) "2" (split -1)"1" replace -1)"1" "1" "sigma_eq[nat]" "low" "0" "high" "2+2*j!1" "G" "LAMBDA (nn: nat): IF nn > 2 + 2 * j!1 THEN 0" "F" "LAMBDA (nn: nat): IF nn > 4 + 2 * j!1 THEN 0")) "1" "1" replace -1)"1" replace -2)"1" "1" "nderiv_sin_fun" "n" "3+2*j!1" ))"1" "nderiv_sin_fun" "n" "4+2*j!1" ))"1" "1" replace -2)"1" replace -4)"1" "1" expand "sin_series_term" )"1" "1" "sin_k_pi" "k" "2+j!1" ))"1" "sin_k_pi2" "k" "j!1+1" ))"1" replace "1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "n!2" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "nderiv_sin_fun" "n" "nn!1" ))"2" (flatten) nil nil ))nil ))nil ))nil )"3" "3" "3" "nderiv_sin_fun" "n" "nn!1" ))"3" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp*)"3" (lemma "nderiv_sin_fun" ("n" "nn!1" ))"3" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp*)"3" (lemma "nderiv_sin_fun" ("n" "nn!1" ))"3" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (assert )"2" (expand "connected?" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"[numfield, numfield -> numfield]" number_fields 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 )"real" trig_basic nil )nil taylors "analysis_ax/" )"even_int" integersnil )"posint" nil )"bool" deriv_domain_def "analysis_ax/" )"bool" deriv_domain_def"analysis_ax/" )"real" sincos_def nil )"posnat" factorial "ints/" )nil integers nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )"real" exponentiation nil )"[T -> real]" nth_derivatives "analysis_ax/" )nil nth_derivatives "analysis_ax/" )"bool" nth_derivatives "analysis_ax/" )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic nil )NOT const-decl "[bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"real" reals nil )"posreal" nil )"posreal" nil )"posreal" nil )"nnreal" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )nil trig_basic nil )nil integers nil )nil trig_basic nil )"(strict_total_order?[real])" real_props nil )nil integers nil )"int" integers nil )nil sigma "reals/" )"posint" nil )"posreal" nil )"odd_int" integers nil )nil trig_basic nil )"[numfield -> numfield]" number_fields nil )nil exponentiation nil )nil sigma_nat "reals/" )nil trig_basic nil )"real" reals nil )nil trig_basic nil )"nzreal" exponentiation nil )"int" exponentiation nil )nil naturalnumbers nil )nil defined_types nil )"[nat -> real]" sincos_def nil )"posint" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )nil sincos nil )"odd_int" integersnil ))nil ))nil 3445346756"" (skosimp*)"" (lemma "nderiv_cos_fun" ("n" "2+2*n!1" ))"" (flatten) nil nil )) nil ))nil )"[numfield, numfield -> numfield]" number_fields 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 reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sincos nil )"even_int" integersnil )"posint" nil ))nil )nil 3445345573 ("" (subtype-tcc) nil nil ) nil nil ))nil 3445345573 ("" (subtype-tcc) nil nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"boolean" notequal nil ))nil ))nil 3445346646"" (skosimp*)"" "Taylors" ("f" "cos" "n" "2*n!1+1" "aa" "0" "bb" "x!1" ))"1" (lemma "nderiv_cos_fun" ("n" "2*n!1+2" ))"1" (flatten)"1" (replace -1)"1" case "FORALL (n:nat): sigma(0, 2 * n + 1, LAMBDA (nn:nat):IF nn > 2 * n + 1 THEN 0") "1" (inst - "n!1" ) (("1" (assert ) nil nil )) nil )"2" (hide-all-but 1)"2" (expand "cos_series_n" )"2" (induct "n" )"1" (expand "sigma" )"1" (expand "sigma" )"1" (expand "cos_series_term" )"1" (rewrite "cos_0" )"1" (lemma "nderiv_cos_fun" ("n" "1" ))"1" "1" replace -2)"1" "1" "cos_pi2" )"1" replace -1)"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "sigma" 1)"2" (expand "sigma" 1 1)"2" "sigma_eq[nat]" "low" "0" "high" "1+2*j!1" "G" "LAMBDA (nn: nat): IF nn > 1 + 2 * j!1 THEN 0" " F" " LAMBDA (nn: nat):IF nn > 3 + 2 * j!1 THEN 0")) "1" (split -1)"1" replace -1)"1" replace -2)"1" "1" "sigma_eq[nat]" "low" "0" "high" "j!1" "F" "LAMBDA (i: nat): IF i > j!1 THEN 0 ELSE cos_series_term(x!1)(i) ENDIF" "G" "LAMBDA (i: nat): IF i > 1 + j!1 THEN 0 ELSE cos_series_term(x!1)(i) ENDIF")) "1" "1" replace -1)"1" "1" "1" "nderiv_cos_fun" "n" "3+2*j!1" ))"1" "nderiv_cos_fun" "n" "2+2*j!1" ))"1" "1" replace -2)"1" replace -4)"1" "1" "1" "cos_k_pi" "k" "j!1+1" ))"1" "cos_eq_0" "a" "((2 * (j!1 * pi) + 3 * pi) / 2)" ))"1" "1" "1" "1" replace "1" replace "1" expand "cos_series_term" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "j!1+1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" "2" "nderiv_cos_fun" ("n" "nn!1" ))"2" (flatten) nil nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" "3" "nderiv_cos_fun" ("n" "nn!1" ))"3" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp*)"3" (lemma "nderiv_cos_fun" ("n" "nn!1" ))"3" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp*)"3" (lemma "nderiv_cos_fun" ("n" "nn!1" ))"3" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (assert )"2" (expand "connected?" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"[numfield, numfield -> numfield]" number_fields 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 )"real" trig_basic nil )nil taylors "analysis_ax/" )"odd_int" integers nil )"posint" nil )"bool" deriv_domain_def "analysis_ax/" )"bool" deriv_domain_def"analysis_ax/" )"real" sincos_def nil )"posnat" factorial "ints/" )nil integers nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )"real" exponentiation nil )"[T -> real]" nth_derivatives "analysis_ax/" )nil nth_derivatives "analysis_ax/" )"bool" nth_derivatives "analysis_ax/" )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic nil )NOT const-decl "[bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"real" reals nil )"posreal" nil )"posreal" nil )"posreal" nil )"nnreal" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )nil trig_basic nil )nil integers nil )"odd_int" integers nil )"nzreal" exponentiation nil )"int" exponentiation nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )nil real_types nil )nil real_types nil )nil trig_basic nil )nil sigma "reals/" )nil trig_basic nil )nil sigma_nat "reals/" )nil factorial "ints/" )"posreal" nil )"real" reals nil )nil trig_basic nil )nil naturalnumbers nil )nil defined_types nil )"[nat -> real]" sincos_def nil )"even_int" integersnil )"posint" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )nil sincos nil )"even_int" integersnil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.0.289Bemerkung:
(vorverarbeitet am 2026-04-27)
¤ *Bot Zugriff
2026-05-26
