(indefinite_integralnil 3472399769"" (lemma "connected_domain" )"" (lemma "connected_deriv_domain[T]" )"" (lemma not_one_element) (("" (assert ) nil nil )) nil )) nil ))nil )nil indefinite_integral nil )"[real -> boolean]" indefinite_integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil deriv_domain_def nil )nil indefinite_integral nil )nil indefinite_integral nil ))nil ))nil 3393924105"" (lemma "connected_domain" ) (("" (propax) nil nil )) nil )nil indefinite_integral nil )) nil ))nil 3393924105"" (lemma "not_one_element" ) (("" (propax) nil nil )) nil )nil indefinite_integral nil )) nil ))nil 3603195717"" (lemma "deriv_domain" ) (("" (propax) nil nil )) nil )nil indefinite_integral nil )) nil ))nil 3603196127"" (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" "xa" "choose({x: T | true})" )"1" "(F!1-G!1)(xa)" )"1" assert )"1" "1" expand "+ " )"1" expand "-" )"1" "x!1" "xa" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" "deriv(G!1 - F!1)(x!1) = 0" )"1" expand "deriv" -1)"1" (propax) nil nil ))nil )"2" "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" "2" expand "-" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" indefinite_integral nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" derivatives nil )nil derivatives nil )"[T, T -> boolean]" equalities nil )"[T -> real]" real_fun_ops "reals/" )"bool" derivatives nil )nil indefinite_integral nil )"[real -> boolean]" indefinite_integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(convergent?)" nil )"continuous_fun" nil )"deriv_fun" derivatives nil )"bool" sets nil )"bool" sets nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"real" reals nil )"bool" booleans nil )"(p)" sets nil )"bool" sets nil )set type-eq-decl nil sets nil )"bool" real_fun_preds "reals/" )nil derivative_props nil )nil derivatives nil )nil derivatives nil ))nil )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" "xa" "choose({x: T | true})" )"1" "(F!1-G!1)(xa)" )"1" assert )"1" "1" expand "+ " )"1" expand "-" )"1" "x!1" "xa" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" "deriv(G!1 - F!1)(x!1) = 0" )"1" expand "deriv" -1)"1" (propax) nil nil ))nil )"2" "2" replace -2)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (lemma "not_one_element" )"2" (lemma "connected_domain" )"2" (inst - x!1 y!1 z!1)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "derivable_diff" )"2" (inst?)"2" (assert )"2" (hide -1)"2" (rewrite "deriv_diff_fun" )"2" (assert )"2" (expand "const_fun" )"2" (replace -2)"2" (replace -4)"2" "2" expand "-" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" derivatives nil )nil derivatives nil )"bool" derivatives nil )"(convergent?)" nil )"[T -> real]" real_fun_ops "reals/" )"bool" real_fun_preds "reals/" )nil derivative_props nil )nil derivatives nil )nil derivatives nil ))nil ))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 )nil indefinite_integral nil )nil booleans nil )"bool" derivatives nil )nil derivatives nil )"[T -> real]" derivatives nil )"bool" indefinite_integral nil )nil indefinite_integral nil )"[real -> boolean]" indefinite_integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3393943252"" (skosimp*)"" (lemma "fundamental2" )"" (inst?)"" (assert )"" (skosimp*)"" (expand "integrable?" )"" (inst?)"" (expand "antiderivative?" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil indefinite_integral nil )"[real -> boolean]" indefinite_integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil fundamental_theorem nil )"bool" indefinite_integral nil )"bool" indefinite_integral nil ))nil ))nil 3393924197"" (lemma "connected_domain" )"" (lemma "not_one_element" )"" (lemma "connected_deriv_domain[T]" )"" (assert )"" "(LAMBDA (f: integrable_fun): choose({F: [T -> real] | AND deriv[T](F) = f}))") "" (assert )"" (skosimp*)"" (expand "nonempty?" )"" (expand "empty?" )"" (assert )"" (typepred "f!1" )"" (expand "integrable?" )"" (skosimp*)"" (expand "antiderivative?" )"" "" "F!1" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil indefinite_integral nil )nil integral_split nil )"bool" sets nil )"bool" indefinite_integral nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )"(p)" sets nil )"bool" sets nil )set type-eq-decl nil sets nil )"[T -> real]" derivatives nil )nil derivatives nil )"[T, T -> boolean]" equalities nil )"bool" derivatives nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil indefinite_integral nil )"bool" indefinite_integral nil )nil booleans nil )nil deriv_domain_def nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" indefinite_integral nil )nil indefinite_integral nil )nil indefinite_integral nil ))nil )nil 3393924105 ("" (existence-tcc) nil nil ) nil nil ))nil 3393926748"" (skosimp*)"" (lemma "antiderivative_lem" )"" (inst?)"" (inst - "f!1" )"" (expand "antiderivative?" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil indefinite_integral nil )"bool" indefinite_integral nil )nil indefinite_integral nil )"[real -> boolean]" indefinite_integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3423992737"" (skosimp*)"" (expand "integrable?" )"" (expand "antiderivative?" ) (("" (inst + "F!1" ) nil nil ))nil ))nil ))nil )"bool" indefinite_integral nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" indefinite_integral nil )nil indefinite_integral nil )"bool" indefinite_integral nil ))nil )nil 3423992362"" (skosimp*)"" (expand "integrable?" )"" (expand "antiderivative?" ) (("" (inst + "F!1" ) nil nil ))nil ))nil ))nil )nil nil ))nil 3423992373 ("" (subtype-tcc) nil nil )nil indefinite_integral nil )"[real -> boolean]" indefinite_integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"set" sets nil )"setof[real]" convergence_functions nil )"real" derivatives_def nil )"bool" convergence_functions nil )"bool" lim_of_functions nil )"bool" lim_of_functions nil )"bool" derivatives_def nil )"bool" derivatives nil )"bool" indefinite_integral nil )"bool" indefinite_integral nil )"real" reals nil )"real" reals nil )"real" reals nil ))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 )nil indefinite_integral nil )nil indefinite_integral nil )"{F: [T -> real] | derivable?(F) AND deriv(F) = f}" nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil indefinite_integral nil )"bool" indefinite_integral nil )nil derivatives nil )"[T -> real]" derivatives nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" indefinite_integral nil )nil indefinite_integral nil )nil booleans nil )"bool" derivatives nil )"[T -> real]" indefinite_integral nil ))nil )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 )"[T -> real]" derivatives nil )nil derivatives nil ))nil ))nil 3393943321"" (skosimp*) (("" (rewrite "cont_fun_integrable?" ) nil nil )) nil )nil indefinite_integral nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" indefinite_integral nil )nil indefinite_integral nil ))nil )nil 3393936480"" (skosimp*) (("" (rewrite "cont_integrable?" ) nil nil )) nil ) nil nil ))nil 3393933020"" (skosimp*)"" (lemma "cont_Integrable?[T]" )"" (inst?)"" (assert )"" (lemma "fundamental3" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil indefinite_integral nil )"[real -> boolean]" indefinite_integral nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil integral nil )nil booleans nil )"bool" indefinite_integral nil )nil indefinite_integral nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" derivatives nil )"[T, T -> boolean]" equalities nil )nil derivatives nil )"[T -> real]" derivatives nil )"{F: [T -> real] | derivable?(F) AND deriv(F) = f}" nil )"real" reals nil )nil fundamental_theorem nil ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
