(integral_chg_varnil 3472399896"" (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_chg_var 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_chg_var nil )nil integral_chg_var nil )nil integral_chg_var nil )"bool" deriv_domain_def nil )"real" reals nil ))nil ))nil 3472399927"" (expand "deriv_domain?" )"" (skosimp*)"" (lemma "con_dom_U" )"" (lemma "connected_deriv_domain[U]" )"" (lemma not_one_U)"" (assert )"" (expand "deriv_domain?" ) (("" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integral_chg_var nil )"[real -> boolean]" integral_chg_var 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 real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil integral_chg_var nil )nil integral_chg_var nil )"bool" deriv_domain_def nil )"real" reals nil ))nil ))nil 3313937110"" (skosimp*)"" (lemma "con_dom_U" )"" (lemma "deriv_domain_U" ) (("" (propax) nil nil )) nil )) nil ))nil )nil integral_chg_var nil )nil integral_chg_var nil ))nil ))nil 3313937110"" (lemma "not_one_U" )"" (expand "not_one_element?" ) (("" (skosimp*) nil nil )) nil ))nil )"bool" deriv_domain_def nil )nil integral_chg_var nil ))nil ))nil 3471608937"" (skosimp*)"" (hide -1 -2 -3 -4)"" (lemma "con_dom_U" )"" (inst - x!1 y!1 z!1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil integral_chg_var nil )) nil ))nil 3313937160"" (skosimp*)"" (lemma "cont_fun_Integrable?[U]" )"1" (inst?)"1" (assert )"1" "(LAMBDA (u: U): f!1(phi!1(u)) * deriv[U](phi!1)(u)) = ") "1" (hide -1)"1" (lemma "composition_cont_fun[U,T]" )"1" (inst - "phi!1" "f!1" )"1" (assert )"1" (lemma "derivable_cont_fun[U]" )"1" (inst - "phi!1" )"1" (assert )"1" (lemma "prod_fun_continuous[U]" )"1" (inst?) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "o " )"2" (assert )"2" (expand "*" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "not_one_U" ) (("2" (propax) nil nil )) nil )"3" (lemma "con_dom_U" )"3" (expand "connected?" ) (("3" (propax) nil nil )) nil ))nil ))nil ))nil )nil integral_chg_var nil )"[real -> boolean]" integral_chg_var 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 derivatives nil )nil continuous_functions nil )"bool" continuous_functions nil )nil continuous_functions nil )nil composition_continuous nil )"T3" function_props nil )"[T -> real]" real_fun_ops "reals/" )"[T, T -> boolean]" equalities nil )"[T -> real]" derivatives nil )nil derivatives nil )"bool" derivatives nil )nil integral_chg_var nil )"[real -> boolean]" integral_chg_var nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" reals nil )nil integral_chg_var nil )nil integral_chg_var nil ))nil ))nil 3319990294"" (lemma "deriv_domain_U" ) (("" (propax) nil nil )) nil )nil integral_chg_var nil )) nil ))nil 3319990294"" (skosimp*)"" (lemma "not_one_U" )"" (expand "not_one_element?" ) (("" (inst?) nil nil )) nil ))nil ))nil )nil integral_chg_var nil )) nil ))"" 3319993700"" (skosimp*)"" (lemma "continuous_Integrable?[T]" )"1" (inst?)"1" (assert )"1" (skosimp*)"1" (expand "continuous?" -1) (("1" (inst?) nil nil ))nil ))nil ))nil ))nil )"2" (lemma "not_one_element" ) (("2" (propax) nil nil )) nil )"3" (lemma "connected_domain" )"3" (expand "connected?" ) (("3" (propax) nil nil )) nil ))nil ))nil ))nil )nil integral_chg_var nil )"[real -> boolean]" integral_chg_var 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 )"bool" continuous_functions 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/" )nil integral_chg_var nil )"[real -> boolean]" integral_chg_var nil )nil integral_chg_var nil )nil integral_chg_var nil ))nil 3319990294 ("" (subtype-tcc) nil nil ) nil nil ))nil 3319990294"" (lemma "connected_domain" ) (("" (skosimp*) nil nil )) nil )nil integral_chg_var nil )) nil ))nil 3319990294"" (lemma "not_one_element" ) (("" (skosimp*) nil nil )) nil )nil integral_chg_var nil )) nil ))nil 3319998251"" (skosimp*)"" (lemma "int_chg_var_prep" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )nil integral_chg_var nil )"real" reals nil )nil integral_chg_var nil )"[real -> boolean]" integral_chg_var nil )nil integral_chg_var nil )"[real -> boolean]" integral_chg_var 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 3319990294"" (skosimp*)"" (lemma "continuous_Integrable?[U]" )"1" (inst?)"1" (assert )"1" (skosimp*) (("1" (postpone) nil nil )) nil )) nil ))nil )"2" (postpone) nil nil ) ("3" (postpone) nil nil ))nil ))nil )nil nil ))nil 3471608937"" (skosimp*)"" (lemma "con_dom_U" )"" (inst - x!1 y!1 z!1) (("" (assert ) nil nil )) nil )) nil ))nil )nil integral_chg_var nil )) nil ))nil 3319990307"" (skosimp*)"" (lemma "fundamental[T]" )"1" "(LAMBDA (y: T): Integral(phi!1(a!1),y,f!1))" "phi!1(a!1)" "f!1" )"1" (name "FF" "(LAMBDA (y: T): Integral(phi!1(a!1),y,f!1))" )"1" (replace -1)"1" (assert )"1" (flatten)"1" (name "GG" "FF o phi!1" )"1" case "(LAMBDA (x:U): Integral(phi!1(a!1), phi!1(x), f!1)) = GG" )"1" (lemma "composition_derivable_fun[U,T]" )"1" (inst - "phi!1" "FF" )"1" (assert )"1" (replace -3)"1" (lemma "deriv_comp_fun[U,T]" )"1" "phi!1" "FF" )"1" replace -4)"1" replace -7)"1" "Integral(phi!1(a!1), phi!1(b!1), f!1) = GG(b!1)" )"1" "fundamental3[U]" )"1" "GG" "a!1" "b!1" "(f!1 o phi!1) * deriv(phi!1)" )"1" assert )"1" "1" "1" "(LAMBDA (u: U): f!1(phi!1(u)) * deriv(phi!1)(u)) = (f!1 o phi!1) * deriv(phi!1)" )"1" replace -3)"1" "GG(a!1) = 0" )"1" assert )nil nil )"2" "2" replace "2" assert )"2" rewrite "Integral_a_to_a[T]" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "o " )"2" assert )"2" expand "*" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "int_chg_var_prep" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "con_dom_U" )"2" (propax) nil nil ))nil ))nil )"2" "2" replace -3 + rl)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "not_one_element" )"2" (lemma "not_one_U" )"2" (lemma "deriv_domain_T" )"2" (propax) nil nil )) nil ))nil ))nil )"3" (lemma "con_dom_U" )"3" (lemma not_one_U)"3" (propax) nil nil )) nil ))nil )"4" (lemma "deriv_domain_U" )"4" (propax) nil nil )) nil ))nil )"2" (hide 2)"2" (replace -1 + rl)"2" (hide -1)"2" (replace -1 + rl)"2" (hide -1)"2" expand "o " )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp*)"3" (lemma "cont_fun_Integrable?[T]" )"3" (inst?) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" (lemma "connected_domain" )"2" (expand "connected?" )"2" (skosimp*)"2" (lemma "cont_fun_Integrable?[T]" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "not_one_element" ) (("2" (propax) nil nil )) nil )"3" (lemma "connected_domain" ) (("3" (propax) nil nil )) nil )"4" (hide 2)"4" (skosimp*)"4" (lemma "cont_fun_Integrable?[T]" )"4" (inst?) (("4" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"2" (lemma "not_one_element" ) (("2" (propax) nil nil )) nil )"3" (lemma "connected_domain" ) (("3" (propax) nil nil )) nil ))nil ))nil )nil integral_chg_var nil )"[real -> boolean]" integral_chg_var 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" deriv_domain_def nil )"bool" deriv_domain_def nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"T3" function_props nil )nil integral nil )nil chain_rule nil )"bool" deriv_domain_def nil )nil chain_rule nil )nil integral_chg_var nil )"[T -> real]" derivatives nil )nil derivatives nil )"[T -> real]" real_fun_ops "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" reals nil )nil integral nil )nil integral_chg_var nil )nil fundamental_theorem nil )"bool" derivatives nil )nil integral_chg_var nil )nil integral_chg_var nil )nil integral_chg_var nil )nil integral_chg_var nil )nil integral_chg_var nil )"real" integral_def nil )nil integral_def nil )"bool" integral_def nil )"[real -> boolean]" integral_chg_var nil )nil integral_chg_var nil )"[U -> T]" integral_chg_var nil )"U" integral_chg_var nil )"[T -> real]" integral_chg_var nil ))nil ))nil 3319990512"" (skosimp*)"" (lemma "continuous_Integrable?[T]" )"1" (inst - "phi!1(a!1)" "phi!1(b!1)" "f!1" )"1" (assert )"1" (expand "Integrable?" )"1" (skosimp*)"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_chg_var nil )"[real -> boolean]" integral_chg_var 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 )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 )"bool" integral_def nil )nil integral_chg_var nil )"[real -> boolean]" integral_chg_var nil )nil integral_chg_var nil )nil integral_chg_var nil ))nil ))nil 3319998518"" (skosimp*)"" (lemma "int_chg_var_prep" )"" (inst?)"" (assert )"" (inst - "a!1" "b!1" )"" (flatten)"" (expand "Integrable?" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integral_chg_var nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"bool" integral_def nil )nil integral_chg_var nil )"[real -> boolean]" integral_chg_var nil )nil integral_chg_var nil )"[real -> boolean]" integral_chg_var 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 3319990512 ("" (subtype-tcc) nil nil ) nil nil ))nil 3313940293"" (skosimp*)"" (lemma "Int_chg_var" )"" (inst?)"" (inst - "b!1" "_" )"" (inst?)"" (assert )"" (expand "Integral" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integral_chg_var nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" integral_def nil )nil integral_chg_var nil )"[real -> boolean]" integral_chg_var nil )nil integral_chg_var nil )"[real -> boolean]" integral_chg_var nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))quality 100%
¤ Dauer der Verarbeitung: 0.7 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
