|
(indefinite_integral
(deriv_domain 0
(deriv_domain-1 nil 3472399769
("" (lemma "connected_domain")
(("" (lemma "connected_deriv_domain[T]")
(("" (lemma not_one_element) (("" (assert) nil nil)) nil)) nil))
nil)
((T formal-nonempty-subtype-decl nil indefinite_integral nil)
(T_pred const-decl "[real -> boolean]" indefinite_integral 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)
(connected_deriv_domain formula-decl nil deriv_domain_def nil)
(not_one_element formula-decl nil indefinite_integral nil)
(connected_domain formula-decl nil indefinite_integral nil))
nil))
(IMP_integral_TCC1 0
(IMP_integral_TCC1-1 nil 3393924105
("" (lemma "connected_domain") (("" (propax) nil nil)) nil)
((connected_domain formula-decl nil indefinite_integral nil)) nil))
(IMP_integral_TCC2 0
(IMP_integral_TCC2-1 nil 3393924105
("" (lemma "not_one_element") (("" (propax) nil nil)) nil)
((not_one_element formula-decl nil indefinite_integral nil)) nil))
(antiderivative?_TCC1 0
(antiderivative?_TCC1-1 nil 3610702294
("" (lemma "deriv_domain") (("" (propax) nil nil)) nil)
((deriv_domain formula-decl nil indefinite_integral nil)) nil))
(antiderivative_lem 0
(antiderivative_lem-1 nil 3393924909
("" (skosimp*)
(("" (expand "antiderivative?")
(("" (flatten)
((""
(case "derivable?(G!1-F!1) AND deriv(G!1-F!1) = const_fun(0)")
(("1" (flatten)
(("1" (expand "const_fun")
(("1" (lemma "null_derivative[T]")
(("1" (inst -1 "G!1-F!1")
(("1" (assert)
(("1" (flatten)
(("1" (hide -1)
(("1" (split -1)
(("1" (expand "constant?")
(("1" (hide-all-but (-1 1))
(("1"
(name "xa" "choose({x: T | true})")
(("1"
(inst + "(F!1-G!1)(xa)")
(("1"
(assert)
(("1"
(apply-extensionality 1 :hide? t)
(("1"
(expand "+ ")
(("1"
(expand "-")
(("1"
(inst - "x!1" "xa")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2"
(case-replace
"deriv(G!1 - F!1)(x!1) = 0")
(("1"
(expand "deriv" -1)
(("1" (propax) nil nil))
nil)
("2"
(hide 2 3)
(("2"
(replace -2)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "derivable_diff[T]")
(("2" (inst?)
(("2" (assert)
(("2" (hide -1)
(("2" (rewrite "deriv_diff_fun[T]")
(("2" (assert)
(("2" (expand "const_fun")
(("2" (replace -2)
(("2" (replace -4)
(("2"
(apply-extensionality 1 :hide? t)
(("2"
(expand "-")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((antiderivative? const-decl "bool" indefinite_integral nil)
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(deriv const-decl "[T -> real]" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(derivable? const-decl "bool" derivatives nil)
(T formal-nonempty-subtype-decl nil indefinite_integral nil)
(T_pred const-decl "[real -> boolean]" indefinite_integral 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)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(derivable_const application-judgement "deriv_fun" derivatives nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(TRUE const-decl "bool" booleans nil)
(choose const-decl "(p)" sets nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(constant? const-decl "bool" real_fun_preds "reals/")
(null_derivative formula-decl nil derivative_props nil)
(derivable_diff judgement-tcc nil derivatives nil)
(deriv_diff_fun formula-decl nil derivatives nil))
nil))
(derivs_eq 0
(derivs_eq-1 nil 3393930788
("" (skosimp*)
(("" (lemma "antiderivative_lem")
(("" (inst?)
(("" (inst -1 "deriv(F!1)")
(("" (assert)
(("" (split -1)
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (expand "antiderivative?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((antiderivative_lem formula-decl nil indefinite_integral nil)
(bool nonempty-type-eq-decl nil booleans nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil)
(deriv const-decl "[T -> real]" derivatives nil)
(antiderivative? const-decl "bool" indefinite_integral nil)
(T formal-nonempty-subtype-decl nil indefinite_integral nil)
(T_pred const-decl "[real -> boolean]" indefinite_integral 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))
nil))
(cont_fun_integrable? 0
(cont_fun_integrable?-1 nil 3393943252
("" (skosimp*)
(("" (lemma "fundamental2")
(("" (inst?)
(("" (assert)
(("" (skosimp*)
(("" (expand "integrable?")
(("" (inst?)
(("" (expand "antiderivative?") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-nonempty-subtype-decl nil indefinite_integral nil)
(T_pred const-decl "[real -> boolean]" indefinite_integral 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)
(fundamental2 formula-decl nil fundamental_theorem nil)
(integrable? const-decl "bool" indefinite_integral nil)
(antiderivative? const-decl "bool" indefinite_integral nil))
nil))
(integral_TCC1 0
(integral_TCC1-2 nil 3393924197
("" (lemma "connected_domain")
(("" (lemma "not_one_element")
(("" (lemma "connected_deriv_domain[T]")
(("" (assert)
((""
(inst +
"(LAMBDA (f: integrable_fun): choose({F: [T -> real] |
derivable?[T](F) AND deriv[T](F) = f}))")
(("" (assert)
(("" (skosimp*)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (assert)
(("" (typepred "f!1")
(("" (expand "integrable?")
(("" (skosimp*)
(("" (expand "antiderivative?")
((""
(flatten)
((""
(inst - "F!1")
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((not_one_element formula-decl nil indefinite_integral nil)
(member const-decl "bool" sets nil)
(antiderivative? const-decl "bool" indefinite_integral nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(empty? const-decl "bool" sets nil)
(choose const-decl "(p)" sets nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(deriv const-decl "[T -> real]" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(derivable? const-decl "bool" derivatives nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(integrable_fun type-eq-decl nil indefinite_integral nil)
(integrable? const-decl "bool" indefinite_integral nil)
(bool nonempty-type-eq-decl nil booleans nil)
(connected_deriv_domain formula-decl nil deriv_domain_def 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]" indefinite_integral nil)
(T formal-nonempty-subtype-decl nil indefinite_integral nil)
(connected_domain formula-decl nil indefinite_integral nil))
nil)
(integral_TCC1-1 nil 3393924105 ("" (existence-tcc) nil nil) nil
nil))
(integral_lem 0
(integral_lem-1 nil 3393926748
("" (skosimp*)
(("" (lemma "antiderivative_lem")
(("" (inst?)
(("" (inst - "f!1")
(("" (expand "antiderivative?") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((antiderivative_lem formula-decl nil indefinite_integral nil)
(antiderivative? const-decl "bool" indefinite_integral nil)
(T formal-nonempty-subtype-decl nil indefinite_integral nil)
(T_pred const-decl "[real -> boolean]" indefinite_integral 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))
shostak))
(deriv_integ 0
(deriv_integ-2 nil 3423992737
("" (skosimp*)
(("" (expand "integrable?")
(("" (expand "antiderivative?") (("" (inst + "F!1") nil nil))
nil))
nil))
nil)
((integrable? const-decl "bool" indefinite_integral 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]" indefinite_integral nil)
(T formal-nonempty-subtype-decl nil indefinite_integral nil)
(antiderivative? const-decl "bool" indefinite_integral nil))
nil)
(deriv_integ-1 nil 3423992362
("" (skosimp*)
(("" (expand "integrable?")
(("" (expand "antiderivative?") (("" (inst + "F!1") nil nil))
nil))
nil))
nil)
nil nil))
(indef_integral_thm_TCC1 0
(indef_integral_thm_TCC1-1 nil 3423992373 ("" (subtype-tcc) nil 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]" indefinite_integral nil)
(T formal-nonempty-subtype-decl nil indefinite_integral nil)
(derivable? const-decl "bool" derivatives nil)
(antiderivative? const-decl "bool" indefinite_integral nil)
(integrable? const-decl "bool" indefinite_integral nil)
(real_plus_real_is_real application-judgement "real" reals nil))
shostak))
(indef_integral_thm 0
(indef_integral_thm-2 nil 3423992748
("" (skosimp*)
(("" (lemma "integral_lem[T]")
(("" (inst - "integral(deriv(F!1))" "F!1" "deriv(F!1)")
(("1" (assert)
(("1" (split -1)
(("1" (propax) nil nil)
("2" (rewrite "deriv_integ") nil nil))
nil))
nil)
("2" (rewrite "deriv_integ") nil nil))
nil))
nil))
nil)
((integral_lem formula-decl nil indefinite_integral nil)
(deriv_integ formula-decl nil indefinite_integral nil)
(integral const-decl
"{F: [T -> real] | derivable?(F) AND deriv(F) = f}"
indefinite_integral nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(integrable_fun type-eq-decl nil indefinite_integral nil)
(integrable? const-decl "bool" indefinite_integral nil)
(deriv_fun type-eq-decl nil derivatives nil)
(deriv const-decl "[T -> real]" derivatives 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]" indefinite_integral nil)
(T formal-nonempty-subtype-decl nil indefinite_integral nil)
(bool nonempty-type-eq-decl nil booleans nil)
(derivable? const-decl "bool" derivatives nil)
(F!1 skolem-const-decl "[T -> real]" indefinite_integral nil))
nil)
(indef_integral_thm-1 nil 3423992321
("" (skosimp*)
(("" (lemma "integral_lem[T]")
(("" (inst - "integral(deriv(F!1))" "F!1" "deriv(F!1)")
(("1" (assert)
(("1" (split -1)
(("1" (propax) nil nil)
("2" (rewrite "deriv_integ") nil nil))
nil))
nil)
("2" (rewrite "deriv_integ") nil nil))
nil))
nil))
nil)
((deriv const-decl "[T -> real]" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil))
nil))
(fundamental_indef_TCC1 0
(fundamental_indef_TCC1-2 nil 3393943321
("" (skosimp*) (("" (rewrite "cont_fun_integrable?") nil nil)) nil)
((cont_fun_integrable? formula-decl nil indefinite_integral 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]" indefinite_integral nil)
(T formal-nonempty-subtype-decl nil indefinite_integral nil))
nil)
(fundamental_indef_TCC1-1 nil 3393936480
("" (skosimp*) (("" (rewrite "cont_integrable?") nil nil)) nil) nil
nil))
(fundamental_indef 0
(fundamental_indef-1 nil 3393933020
("" (skosimp*)
(("" (lemma "cont_Integrable?[T]")
(("" (inst?)
(("" (assert)
(("" (lemma "fundamental3")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((T formal-nonempty-subtype-decl nil indefinite_integral nil)
(T_pred const-decl "[real -> boolean]" indefinite_integral 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)
(cont_Integrable? formula-decl nil integral nil)
(bool nonempty-type-eq-decl nil booleans nil)
(integrable? const-decl "bool" indefinite_integral nil)
(integrable_fun type-eq-decl nil indefinite_integral nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(derivable? const-decl "bool" derivatives nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(deriv_fun type-eq-decl nil derivatives nil)
(deriv const-decl "[T -> real]" derivatives nil)
(integral const-decl
"{F: [T -> real] | derivable?(F) AND deriv(F) = f}"
indefinite_integral nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(fundamental3 formula-decl nil fundamental_theorem nil))
nil)))
¤ Dauer der Verarbeitung: 0.61 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
