|
(integral_sincos
(IMP_deriv_sincos_TCC1 0
(IMP_deriv_sincos_TCC1-1 nil 3476447258
("" (lemma "connected_deriv_domain[T]") (("" (assert) nil nil)) nil)
((connected_domain formula-decl nil integral_sincos nil)
(connected_deriv_domain formula-decl nil deriv_domain_def
"analysis_ax/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" integral_sincos nil)
(T formal-nonempty-subtype-decl nil integral_sincos nil))
nil))
(IMP_deriv_sincos_TCC2 0
(IMP_deriv_sincos_TCC2-1 nil 3476447258 ("" (assert) nil nil)
((not_one_element formula-decl nil integral_sincos nil)) nil))
(sin_Integrable 0
(sin_Integrable-1 nil 3476447279
("" (skosimp*)
(("" (lemma "sin_derivable[T]")
(("" (inst?)
(("" (lemma "derivable_Integrable?")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((T formal-nonempty-subtype-decl nil integral_sincos nil)
(T_pred const-decl "[real -> boolean]" integral_sincos nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sin_derivable formula-decl nil deriv_sincos nil)
(derivable_Integrable? formula-decl nil fundamental_theorem
"analysis_ax/")
(sin_range application-judgement "trig_range" trig_basic nil)
(sin const-decl "real" trig_basic nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(cos_Integrable 0
(cos_Integrable-2 nil 3479113925
("" (skosimp*)
(("" (lemma "cos_derivable[T]")
(("" (inst?)
(("" (assert)
(("" (lemma "derivable_Integrable?")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((T formal-nonempty-subtype-decl nil integral_sincos nil)
(T_pred const-decl "[real -> boolean]" integral_sincos nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(cos_derivable formula-decl nil deriv_sincos nil)
(cos_range application-judgement "trig_range" trig_basic nil)
(real_times_real_is_real application-judgement "real" reals nil)
(cos const-decl "real" trig_basic nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(derivable_Integrable? formula-decl nil fundamental_theorem
"analysis_ax/"))
nil)
(cos_Integrable-1 nil 3476446588
("" (skosimp*)
(("" (lemma "cos_derivable")
(("" (inst?)
(("" (assert)
(("" (lemma "derivable_Integrable?")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((cos_derivable formula-decl nil deriv_sincos nil)
(derivable_Integrable? formula-decl nil fundamental_theorem
"analysis_ax/"))
shostak))
(Integral_sin_TCC1 0
(Integral_sin_TCC1-1 nil 3476447258
("" (skosimp*)
(("" (lemma sin_Integrable) (("" (inst?) nil nil)) nil)) nil)
((sin_Integrable formula-decl nil integral_sincos nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" integral_sincos nil)
(T formal-nonempty-subtype-decl nil integral_sincos nil))
nil))
(Integral_sin 0
(Integral_sin-1 nil 3476447372
("" (skosimp*)
(("" (lemma "fundamental3")
(("" (inst?)
((""
(inst - "(LAMBDA (x: T): -k!1 / alpha!1* cos(alpha!1 * x))")
(("" (assert)
(("" (lemma "cos_derivable[T]")
(("" (inst - "alpha!1" "-k!1/alpha!1")
(("" (assert)
(("" (lemma "deriv_cos[T]")
(("" (inst - "alpha!1" "-k!1/alpha!1")
(("" (assert)
(("" (hide-all-but 1)
(("" (lemma "sin_continuous[T]")
(("" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-nonempty-subtype-decl nil integral_sincos nil)
(T_pred const-decl "[real -> boolean]" integral_sincos nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(fundamental3 formula-decl nil fundamental_theorem "analysis_ax/")
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(cos const-decl "real" trig_basic nil)
(cos_derivable formula-decl nil deriv_sincos nil)
(sin_continuous formula-decl nil deriv_sincos nil)
(deriv_cos formula-decl nil deriv_sincos nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" trig_basic nil)
(sin_range application-judgement "trig_range" trig_basic nil)
(sin const-decl "real" trig_basic nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(Integral_cos_TCC1 0
(Integral_cos_TCC1-1 nil 3476447258
("" (skosimp*)
(("" (lemma cos_Integrable) (("" (inst?) nil nil)) nil)) nil)
((cos_Integrable formula-decl nil integral_sincos nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" integral_sincos nil)
(T formal-nonempty-subtype-decl nil integral_sincos nil))
nil))
(Integral_cos 0
(Integral_cos-2 nil 3479114004
("" (skosimp*)
(("" (lemma "fundamental3")
(("" (inst?)
((""
(inst - "(LAMBDA (x: T): k!1 / alpha!1* sin(alpha!1 * x))")
(("" (assert)
(("" (lemma "sin_derivable[T]")
(("" (inst - "alpha!1" "k!1/alpha!1")
(("" (assert)
(("" (lemma "deriv_sin[T]")
(("" (inst - "alpha!1" "k!1/alpha!1")
(("" (assert)
(("" (hide-all-but 1)
(("" (lemma "cos_continuous[T]")
(("" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-nonempty-subtype-decl nil integral_sincos nil)
(T_pred const-decl "[real -> boolean]" integral_sincos nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(fundamental3 formula-decl nil fundamental_theorem "analysis_ax/")
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(sin const-decl "real" trig_basic nil)
(sin_derivable formula-decl nil deriv_sincos nil)
(cos_continuous formula-decl nil deriv_sincos nil)
(deriv_sin formula-decl nil deriv_sincos nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" trig_basic nil)
(cos_range application-judgement "trig_range" trig_basic nil)
(cos const-decl "real" trig_basic nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil)
(Integral_cos-1 nil 3476449527
("" (skosimp*)
(("" (lemma "fundamental3")
(("" (inst?)
((""
(inst - "(LAMBDA (x: T): k!1 / alpha!1* sin(alpha!1 * x))")
(("" (assert)
(("" (lemma "sin_derivable")
(("" (inst - "alpha!1" "k!1/alpha!1")
(("" (assert)
(("" (lemma "deriv_sin")
(("" (inst - "alpha!1" "k!1/alpha!1")
(("" (assert)
(("" (hide-all-but 1)
(("" (lemma "cos_continuous")
(("" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((fundamental3 formula-decl nil fundamental_theorem "analysis_ax/")
(sin_derivable formula-decl nil deriv_sincos nil)
(cos_continuous formula-decl nil deriv_sincos nil)
(deriv_sin formula-decl nil deriv_sincos nil))
nil)))
¤ Dauer der Verarbeitung: 0.17 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.
|
