(integral_mean_valuenil 3472400278"" (expand "deriv_domain?" )"" (skosimp*)"" (lemma "connected_domain" )"" (expand "connected?" )"" (lemma "connected_deriv_domain[T]" )"" (expand "connected?" )"" (expand "not_one_element?" )"" (expand "deriv_domain?" )"" (replace -2)"" (lemma not_one_element)"" (expand "not_one_element?" )"" (replace -1)"" (hide -1) (("" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" deriv_domain_def nil )nil integral_mean_value nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" deriv_domain_def 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]" integral_mean_value nil )nil integral_mean_value nil )nil integral_mean_value nil )"bool" deriv_domain_def nil )"real" reals nil ))nil ))nil 3376221540"" (lemma "connected_domain" ) (("" (propax) nil nil )) nil )nil integral_mean_value nil )) nil ))nil 3376221540"" (lemma "not_one_element" ) (("" (propax) nil nil )) nil )nil integral_mean_value nil )) nil ))nil 3376221540"" (skosimp*)"" (lemma "continuous_Integrable?[T]" )"1" (inst?)"1" (split -1)"1" (propax) nil nil )"2" (hide 2)"2" (skosimp*)"2" (expand "continuous?" -1) (("2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "not_one_element" ) (("2" (propax) nil nil )) nil ))nil )"3" (lemma "connected_domain" )"3" (expand "connected?" ) (("3" (propax) nil nil )) nil ))nil ))nil ))nil )nil integral_mean_value nil )"[real -> boolean]" integral_mean_value 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 )"bool" deriv_domain_def nil )"bool" deriv_domain_def nil )nil booleans nil )nil intervals_real "reals/" )"bool" reals nil ) (<= const-decl "bool" reals nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" continuous_functions nil )nil integral_mean_value nil )nil integral_mean_value nil ))nil ))nil 3376221553"" (skosimp*)"" (lemma "fundamental2" )"" (inst?)"" (assert )"" (skosimp*)"" (lemma "mean_value[T]" )"" (inst?)"" (assert )"" (inst - "F!1" )"" (assert )"" (skosimp*)"" "deriv(F!1, c!1) = f!1(c!1)" )"1" (inst + "c!1" )"1" (assert )"1" "fundamental3" )"1" "1" "F!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (hide 2)"2" (expand "deriv" -5)"2" replace -5 + rl)"2" (assert ) nil nil ))nil ))nil ))nil )"3" (lemma "not_one_element" )"3" (propax) nil nil )) nil )"4" (lemma "deriv_domain" )"4" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integral_mean_value nil )"[real -> boolean]" integral_mean_value 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 )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil derivative_props nil )"bool" deriv_domain_def nil )"bool" deriv_domain_def nil )"real" derivatives_def nil )"bool" derivatives_def nil )nil booleans nil )"[T, T -> boolean]" equalities nil )nil fundamental_theorem nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil intervals_real "reals/" )"T" integral_mean_value nil )"T" integral_mean_value nil )"T" integral_mean_value nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"[T -> real]" derivatives nil )nil integral_mean_value nil )nil integral_mean_value nil )"real" reals nil ))nil 3376222786"" (skosimp*)"" (lemma "continuous_Integrable?[T]" )"1" (inst?)"1" (assert )"1" (skosimp*)"1" (inst?)"1" (expand "continuous?" -3) (("1" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (lemma "not_one_element" ) (("2" (propax) nil nil )) nil ))nil )"3" (lemma "connected_domain" )"3" (expand "connected?" ) (("3" (propax) nil nil )) nil ))nil ))nil ))nil )nil integral_mean_value nil )"[real -> boolean]" integral_mean_value 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 )"bool" deriv_domain_def nil )"bool" deriv_domain_def nil )nil booleans nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil intervals_real "reals/" )"bool" continuous_functions nil )nil integral_mean_value nil )nil integral_mean_value nil ))nil ))nil 3376222764"" (skosimp*)"" (lemma "mean_value_integral" )"" (inst?)"" (assert )"" (skosimp*)"" (replace -1)"" (factor -5)"" (mult-cases -5)"" (inst?)"1" (assert ) nil nil )"2" (assert )"2" (typepred "c!1" )"2" (assert ) (("2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integral_mean_value nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )nil intervals_real "reals/" )"Open_interval[T](a!1, b!1)" nil )"T" integral_mean_value nil )"T" integral_mean_value nil )"(total_order?[real])" nil )nil intervals_real "reals/" )"bool" reals nil ) (<= const-decl "bool" reals nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"real" reals nil )nil integral_mean_value nil )"[real -> boolean]" integral_mean_value nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil )))quality 95%
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
