|
(sincos
(sin_derivable_TCC1 0
(sin_derivable_TCC1-1 nil 3602247635 ("" (assert) nil nil)
((deriv_domain_real formula-decl nil deriv_domain "analysis_ax/"))
nil))
(sin_derivable_TCC2 0
(sin_derivable_TCC2-1 nil 3602247635 ("" (assert) nil nil)
((not_one_element_real formula-decl nil deriv_domain
"analysis_ax/"))
nil))
(sin_derivable 0
(sin_derivable-1 nil 3263379563
("" (skolem 1 ("x"))
(("" (lemma "sin_convergence" ("x" "x"))
((""
(lemma "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)
((not_one_element? const-decl "bool" deriv_domain_def
"analysis_ax/")
(deriv_domain? const-decl "bool" deriv_domain_def "analysis_ax/"))
shostak))
(sin_derivable_fun 0
(sin_derivable_fun-1 nil 3602248246
("" (expand "derivable?")
(("" (lemma "sin_derivable") (("" (propax) nil nil)) nil)) nil)
((sin_derivable formula-decl nil sincos nil)
(derivable? const-decl "bool" derivatives "analysis_ax/"))
shostak))
(deriv_sin_fun_TCC1 0
(deriv_sin_fun_TCC1-1 nil 3263377309
("" (lemma "sin_derivable_fun") (("" (propax) nil nil)) nil)
((sin_derivable_fun formula-decl nil sincos nil)) shostak))
(deriv_sin_fun 0
(deriv_sin_fun-1 nil 3263490807
("" (expand "deriv")
((""
(lemma "extensionality"
("f" "(LAMBDA (x: real): deriv(sin, x))" "g" "cos"))
(("1" (split -1)
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (skosimp*)
(("2"
(lemma "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)
((deriv const-decl "real" derivatives_def "analysis_ax/")
(derivable? const-decl "bool" derivatives_def "analysis_ax/")
(deriv_domain? const-decl "bool" deriv_domain_def "analysis_ax/")
(not_one_element? const-decl "bool" deriv_domain_def
"analysis_ax/")
(deriv const-decl "[T -> real]" derivatives "analysis_ax/"))
shostak))
(cos_derivable 0
(cos_derivable-1 nil 3263378610
("" (skosimp*)
(("" (lemma "cos_convergence" ("x" "x!1"))
((""
(lemma "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)
((not_one_element? const-decl "bool" deriv_domain_def
"analysis_ax/")
(deriv_domain? const-decl "bool" deriv_domain_def "analysis_ax/"))
shostak))
(cos_derivable_fun 0
(cos_derivable_fun-1 nil 3602248261
("" (expand "derivable?")
(("" (lemma "cos_derivable") (("" (propax) nil nil)) nil)) nil)
((cos_derivable formula-decl nil sincos nil)
(derivable? const-decl "bool" derivatives "analysis_ax/"))
shostak))
(deriv_cos_fun_TCC1 0
(deriv_cos_fun_TCC1-1 nil 3263377338
("" (lemma "cos_derivable_fun") (("" (propax) nil nil)) nil)
((cos_derivable_fun formula-decl nil sincos nil)) shostak))
(deriv_cos_fun 0
(deriv_cos_fun-2 nil 3352175440
("" (expand "deriv")
(("" (lemma "cos_convergence")
(("" (lemma "derivative_equivalence1[real]" ("f" "cos"))
(("1"
(lemma "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)
((deriv const-decl "real" derivatives_def "analysis_ax/")
(derivable? const-decl "bool" derivatives_def "analysis_ax/")
(not_one_element? const-decl "bool" deriv_domain_def
"analysis_ax/")
(deriv_domain? const-decl "bool" deriv_domain_def "analysis_ax/")
(deriv const-decl "[T -> real]" derivatives "analysis_ax/"))
nil)
(deriv_cos_fun-1 nil 3263377393
("" (expand "deriv")
(("" (lemma "cos_convergence")
(("" (lemma "derivative_equivalence1" ("f" "cos"))
((""
(lemma "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)
((deriv const-decl "[T -> real]" derivatives "analysis_ax/")
(deriv const-decl "[T -> real]" derivatives "analysis_ax/"))
shostak))
(sin_continuous 0
(sin_continuous-2 nil 3352175475
("" (skosimp*)
(("" (lemma "sin_derivable" ("x" "x0!1"))
(("" (lemma "derivable_continuous[real]" ("f" "sin" "x" "x0!1"))
(("" (assert) nil nil)) nil))
nil))
nil)
((derivable_continuous formula-decl nil derivatives_def
"analysis_ax/")
(sin const-decl "real" trig_basic nil))
nil)
(sin_continuous-1 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))
(cos_continuous 0
(cos_continuous-2 nil 3352175502
("" (skosimp*)
(("" (lemma "cos_derivable" ("x" "x0!1"))
(("" (lemma "derivable_continuous[real]" ("f" "cos" "x" "x0!1"))
(("" (assert) nil nil)) nil))
nil))
nil)
((derivable_continuous formula-decl nil derivatives_def
"analysis_ax/")
(cos const-decl "real" trig_basic nil))
nil)
(cos_continuous-1 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))
(sin_continuous_fun 0
(sin_continuous_fun-1 nil 3602248362
("" (expand "continuous?")
(("" (lemma "sin_continuous") (("" (propax) nil nil)) nil)) nil)
((sin_continuous formula-decl nil sincos nil)
(continuous? const-decl "bool" continuous_functions
"analysis_ax/"))
shostak))
(cos_continuous_fun 0
(cos_continuous_fun-1 nil 3602248393
("" (expand "continuous?")
(("" (lemma "cos_continuous") (("" (propax) nil nil)) nil)) nil)
((cos_continuous formula-decl nil sincos nil)
(continuous? const-decl "bool" continuous_functions
"analysis_ax/"))
shostak))
(nderiv_sin_fun 0
(nderiv_sin_fun-3 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"
(lemma "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"
(lemma "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"
(lemma "extensionality"
("f"
"(LAMBDA (x: real): cos((j!1 * pi / 2) + x))"
"g"
"(LAMBDA (x: real): sin(x + ((j!1 * pi + pi) / 2)))"))
(("3"
(split -1)
(("1"
(replace -1)
(("1"
(case
"FORALL (n:nat,f:nderiv_fun(n)): nderiv(n,-f) = -nderiv(n,f)")
(("1"
(inst - "j!1" "sin")
(("1"
(replace -1)
(("1"
(replace -5)
(("1"
(hide-all-but 1)
(("1"
(expand "-")
(("1"
(lemma
"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"
(split)
(("1"
(propax)
nil
nil)
("2"
(hide 2)
(("2"
(skosimp*)
(("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"
(inst - "j!1")
(("2"
(flatten)
(("2"
(hide-all-but 1)
(("2"
(induct "n")
(("1"
(expand "nderiv")
(("1" (propax) nil nil))
nil)
("2"
(skosimp*)
(("2"
(expand "nderiv" 1)
(("2"
(lemma
"deriv_neg_fun[real]"
("ff" "f!1"))
(("2"
(replace -1)
(("2"
(inst
-
"deriv(f!1)")
nil
nil))
nil))
nil))
nil))
nil)
("3"
(hide 2)
(("3"
(induct "n")
(("1"
(expand
"derivable_n_times?")
(("1"
(propax)
nil
nil))
nil)
("2"
(skosimp*)
(("2"
(expand
"derivable_n_times?"
1)
(("2"
(typepred "f!1")
(("2"
(expand
"derivable_n_times?"
-1)
(("2"
(flatten -1)
(("2"
(lemma
"neg_derivable_fun[real]"
("f"
"f!1"))
(("2"
(assert)
(("2"
(lemma
"deriv_neg_fun[real]"
("ff"
"f!1"))
(("2"
(replace
-1
1)
(("2"
(inst
-
"deriv(f!1)")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide-all-but 1)
(("3"
(induct "n")
(("1"
(skosimp*)
(("1"
(expand
"derivable_n_times?")
(("1" (propax) nil nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(expand
"derivable_n_times?"
1)
(("2"
(lemma
"neg_derivable_fun[real]"
("f" "f!1"))
(("2"
(assert)
(("2"
(typepred "f!1")
(("2"
(expand
"derivable_n_times?"
-1)
(("2"
(flatten)
(("2"
(assert)
(("2"
(lemma
"deriv_neg_fun[real]"
("ff"
"f!1"))
(("2"
(replace
-1)
(("2"
(inst
-
"deriv(f!1)")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(hide-all-but 1)
(("2"
(lemma
"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"
(inst - "j!1" "sin")
(("1" (assert) 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?"
(-2 1))
(("2"
(flatten -2)
(("2"
(lemma
"neg_derivable_fun[real]"
("f" "f!1"))
(("2"
(assert)
(("2"
(inst -2 "deriv(f!1)")
(("2"
(assert)
(("2"
(lemma
"deriv_neg_fun[real]"
("ff" "f!1"))
(("2"
(replace -1 1)
(("2"
(propax)
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)
((derivable_n_times? def-decl "bool" nth_derivatives "analysis_ax/")
(neg_derivable_fun formula-decl nil derivatives "analysis_ax/")
(deriv_neg_fun formula-decl nil derivatives "analysis_ax/")
(derivable? const-decl "bool" derivatives "analysis_ax/")
(deriv_fun type-eq-decl nil derivatives "analysis_ax/")
(deriv const-decl "[T -> real]" derivatives "analysis_ax/")
(neg_sin formula-decl nil trig_basic nil)
(cos_sin formula-decl nil trig_basic nil)
(nderiv_fun type-eq-decl nil nth_derivatives "analysis_ax/")
(nderiv def-decl "[T -> real]" nth_derivatives "analysis_ax/"))
nil)
(nderiv_sin_fun-2 nil 3445346393
(";;; Proof nderiv_sin_fun-3 for formula sincos.nderiv_sin_fun"
(skolem 1 ("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"
(lemma "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"
(lemma "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"
(lemma "extensionality"
("f"
"(LAMBDA (x: real): cos((j!1 * pi / 2) + x))"
"g"
"(LAMBDA (x: real): sin(x + ((j!1 * pi + pi) / 2)))"))
(("3"
(split -1)
(("1"
(replace -1)
(("1"
(case
"FORALL (n:nat,f:nderiv_fun(n)): nderiv(n,-f) = -nderiv(n,f)")
(("1"
(inst - "j!1" "sin")
(("1"
(replace -1)
(("1"
(replace -5)
(("1"
(hide-all-but 1)
(("1"
(expand "-")
(("1"
(lemma
"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"
(split)
(("1" (propax) nil)
("2"
(hide 2)
(("2"
(skosimp*)
(("2"
(rewrite
"cos_sin")
(("2"
(rewrite
"neg_sin")
(("2"
(expand
"pi")
(("2"
(assert)
nil)))))))))))))))))))))))))
("2"
(inst - "j!1")
(("2"
(flatten)
(("2"
(hide-all-but 1)
(("2"
(induct "n")
(("1"
(expand "nderiv")
(("1" (propax) nil)))
("2"
(skosimp*)
(("2"
(expand "nderiv" 1)
(("2"
(lemma
"deriv_neg_fun[real]"
("ff" "f!1"))
(("2"
(replace -1)
(("2"
(inst
-
"deriv(f!1)")
nil)))))))))
("3"
(hide 2)
(("3"
(induct "n")
(("1"
(expand
"derivable_n_times?")
(("1" (propax) nil)))
("2"
(skosimp*)
(("2"
(expand
"derivable_n_times?"
1)
(("2"
(typepred "f!1")
(("2"
(expand
"derivable_n_times?"
-1)
(("2"
(flatten -1)
(("2"
(lemma
"opposite_derivable_fun[real]"
("f"
"f!1"))
(("2"
(assert)
(("2"
(lemma
"deriv_neg_fun[real]"
("ff"
"f!1"))
(("2"
(replace
-1
1)
(("2"
(inst
-
"deriv(f!1)")
nil)))))))))))))))))))))))))))))))
("3"
(hide-all-but 1)
(("3"
(induct "n")
(("1"
(skosimp*)
(("1"
(expand
"derivable_n_times?")
(("1" (propax) nil)))))
("2"
(skosimp*)
(("2"
(expand
"derivable_n_times?"
1)
(("2"
(lemma
"opposite_derivable_fun[real]"
("f" "f!1"))
(("2"
(assert)
(("2"
(typepred "f!1")
(("2"
(expand
"derivable_n_times?"
-1)
(("2"
(flatten)
(("2"
(assert)
(("2"
(lemma
"deriv_neg_fun[real]"
("ff"
"f!1"))
(("2"
(replace
-1)
(("2"
(inst
-
"deriv(f!1)")
nil)))))))))))))))))))))))))))))
("2"
(skosimp*)
(("2"
(hide-all-but 1)
(("2"
(lemma
"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"
(inst - "j!1" "sin")
(("1" (assert) nil)))
("2"
(hide-all-but 1)
(("2"
(induct "n")
(("1"
(expand "derivable_n_times?")
(("1" (propax) nil)))
("2"
(skosimp*)
(("2"
(expand
"derivable_n_times?"
(-2 1))
(("2"
(flatten -2)
(("2"
(lemma
"opposite_derivable_fun[real]"
("f" "f!1"))
(("2"
(assert)
(("2"
(inst -2 "deriv(f!1)")
(("2"
(assert)
(("2"
(lemma
"deriv_neg_fun[real]"
("ff" "f!1"))
(("2"
(replace -1 1)
(("2"
(propax)
nil))))))))))))))))))))))))))))))))))))))))))))))))))
";;; developed with shostak decision procedures")
nil nil)
(nderiv_sin_fun-1 nil 3445346356
(";;; Proof nderiv_sin_fun-3 for formula sincos.nderiv_sin_fun"
(skolem 1 ("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"
(lemma "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"
(lemma "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"
(lemma "extensionality"
("f"
"(LAMBDA (x: real): cos((j!1 * pi / 2) + x))"
"g"
"(LAMBDA (x: real): sin(x + ((j!1 * pi + pi) / 2)))"))
(("3"
(split -1)
(("1"
(replace -1)
(("1"
(case
"FORALL (n:nat,f:nderiv_fun(n)): nderiv(n,-f) = -nderiv(n,f)")
(("1"
(inst - "j!1" "sin")
(("1"
(replace -1)
(("1"
(replace -5)
(("1"
(hide-all-but 1)
(("1"
(expand "-")
(("1"
(lemma
"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"
(split)
(("1" (propax) nil)
("2"
(hide 2)
(("2"
(skosimp*)
(("2"
(rewrite
"cos_sin")
(("2"
(rewrite
"neg_sin")
(("2"
(expand
"pi")
(("2"
(assert)
nil)))))))))))))))))))))))))
("2"
(inst - "j!1")
(("2"
(flatten)
(("2"
(hide-all-but 1)
(("2"
(induct "n")
(("1"
(expand "nderiv")
(("1" (propax) nil)))
("2"
(skosimp*)
(("2"
(expand "nderiv" 1)
(("2"
(lemma
"deriv_opp_fun[real]"
("ff" "f!1"))
(("2"
(replace -1)
(("2"
(inst
-
"deriv(f!1)")
nil)))))))))
("3"
(hide 2)
(("3"
(induct "n")
(("1"
(expand
"derivable_n_times?")
(("1" (propax) nil)))
("2"
(skosimp*)
(("2"
(expand
"derivable_n_times?"
1)
(("2"
(typepred "f!1")
(("2"
(expand
"derivable_n_times?"
-1)
(("2"
(flatten -1)
(("2"
(lemma
"opposite_derivable_fun[real]"
("f"
"f!1"))
(("2"
(assert)
(("2"
(lemma
"deriv_opp_fun[real]"
("ff"
"f!1"))
(("2"
(replace
-1
1)
(("2"
(inst
-
"deriv(f!1)")
nil)))))))))))))))))))))))))))))))
("3"
(hide-all-but 1)
(("3"
(induct "n")
(("1"
(skosimp*)
(("1"
(expand
"derivable_n_times?")
(("1" (propax) nil)))))
("2"
(skosimp*)
(("2"
(expand
"derivable_n_times?"
1)
(("2"
(lemma
"opposite_derivable_fun[real]"
("f" "f!1"))
(("2"
(assert)
(("2"
(typepred "f!1")
(("2"
(expand
"derivable_n_times?"
-1)
(("2"
(flatten)
(("2"
(assert)
(("2"
(lemma
"deriv_opp_fun[real]"
("ff"
"f!1"))
(("2"
(replace
-1)
(("2"
(inst
-
"deriv(f!1)")
nil)))))))))))))))))))))))))))))
("2"
(skosimp*)
(("2"
(hide-all-but 1)
(("2"
(lemma
"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"
(inst - "j!1" "sin")
(("1" (assert) nil)))
("2"
(hide-all-but 1)
(("2"
(induct "n")
(("1"
(expand "derivable_n_times?")
(("1" (propax) nil)))
("2"
(skosimp*)
(("2"
(expand
"derivable_n_times?"
(-2 1))
(("2"
(flatten -2)
(("2"
(lemma
"opposite_derivable_fun[real]"
("f" "f!1"))
(("2"
(assert)
(("2"
(inst -2 "deriv(f!1)")
(("2"
(assert)
(("2"
(lemma
"deriv_opp_fun[real]"
("ff" "f!1"))
(("2"
(replace -1 1)
(("2"
(propax)
nil))))))))))))))))))))))))))))))))))))))))))))))))))
";;; developed with shostak decision procedures")
nil nil))
(nderiv_cos_fun 0
(nderiv_cos_fun-1 nil 3445346583
("" (induct "n")
(("1" (expand "derivable_n_times?") (("1" (propax) nil nil)) nil)
("2" (expand "nderiv")
(("2"
(lemma "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"
(inst - "j!1" "sin")
(("1"
(replace -3)
(("1"
(replace -2)
(("1"
(hide-all-but 1)
(("1"
(expand "-")
(("1"
(lemma
"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"
(split -1)
(("1" (propax) nil nil)
("2"
(hide 2)
(("2"
(skosimp*)
(("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"
(typepred "f!1")
(("2"
(expand "derivable_n_times?" -1)
(("2"
(flatten)
(("2"
(lemma
"neg_derivable_fun[real]"
("f" "f!1"))
(("2"
(assert)
(("2"
(lemma
"deriv_neg_fun[real]"
("ff" "f!1"))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.73 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
