Impressum fundamental_theorem.prf
Sprache: Lisp
(fundamental_theoremnil 3472399705"" (lemma "connected_domain" )"" (lemma "connected_deriv_domain[T]" )"" (lemma not_one_element) (("" (assert ) nil nil )) nil )) nil ))nil )nil fundamental_theorem nil )"[real -> boolean]" fundamental_theorem 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 fundamental_theorem nil )nil fundamental_theorem nil ))nil )nil 3471610571"" (skosimp*)"" (lemma "connected_domain" )"" (lemma "connected_deriv_domain[T]" )"1" (replace -2) (("1" (inst?) nil nil )) nil )"2" (lemma not_one_element) (("2" (propax) nil nil )) nil ))nil ))nil ))nil )nil shostak))nil 3610702394"" (lemma "connected_domain" ) (("" (propax) nil nil )) nil )nil fundamental_theorem nil )) nil ))nil 3610702394"" (lemma "not_one_element" ) (("" (propax) nil nil )) nil )nil fundamental_theorem nil )) nil ))nil 3257699428"" (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" (propax) nil nil )) nil ))nil ))nil )nil fundamental_theorem nil )"[real -> boolean]" fundamental_theorem 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 fundamental_theorem nil )nil fundamental_theorem nil ))nil 3610702232"" (skosimp*)"" (lemma "deriv_domain" ) (("" (propax) nil nil )) nil )) nil )nil fundamental_theorem nil )) nil ))nil 3257787730"" (skosimp*)"" (rewrite "derivative_fun_alt" )"" (skosimp*)"" (expand "convergence" )"" (expand "convergence" )"" (prop)"1" (hide -2)"1" (expand "continuous?" )"1" (inst?)"1" (rewrite continuity_def)"1" (expand "convergence" )"1" (expand "convergence" )"1" (flatten)"1" (hide -2)"1" "1" expand "adh" )"1" "1" "not_one_element" )"1" expand "not_one_element?" )"1" "x!1" )"1" "1" case "x!1 <= y!1" )"1" "min(y!1,x!1+e!1/2)" )"1" (grind) nil nil )"2" expand "min" )"2" "1" "connected_domain" )"1" expand "connected?" )"1" "x!1" "y!1" "x!1 + e!1 / 2" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "max(y!1,x!1-e!1/2)" )"1" (grind) nil nil )"2" expand "max" )"2" "1" "connected_domain" )"1" expand "connected?" )"1" "y!1" "x!1" "x!1 - e!1 / 2" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "continuous?" )"2" (inst -1 "x!1" )"2" (rewrite continuity_def)"2" (expand "convergence" )"2" (expand "convergence" )"2" (flatten)"2" (inst -2 "epsilon!1/2" )"2" "2" case "FORALL (x, x0: T): x /= x0 IMPLIES Integrable?[T](x0, x, (LAMBDA (t: T): f!1(t) - f!1(x0)))" )"1" "delta!1" )"1" "1" case "(FORALL (x,x0: T): x /= x0 IMPLIES abs((F!1(x) - F!1(x0))/(x-x0) - f!1(x0)) = abs(Integral(x0,x,(LAMBDA (t: T): f!1(t) - f!1(x0)))/(x-x0)))" )"1" "1" assert )"1" replace -1)"1" "1" "1" rewrite "abs_div" )"1" "abs(x!2 - x!1)" )"1" "x!2" )"1" assert )"1" "Integral_bounded[T]" )"1" "1" assert )"1" "epsilon!1/2" )"1" "1" assert )nil nil )"2" "2" "2" assert )nil nil ))nil ))nil )"3" "3" "3" "3" "x!3" )"3" assert )"3" "3" "3" expand "fullset" )"3" "x!3" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "not_one_element" )"2" nil nil ))nil )"3" "connected_domain" )"3" nil nil ))nil ))nil ))nil ))nil )"2" "not_one_element" )"2" nil nil ))nil )"3" "connected_domain" )"3" nil nil ))nil )"4" "4" "4" "4" assert )nil nil ))nil ))nil ))nil )"5" "not_one_element" )"5" nil nil ))nil )"6" "connected_domain" )"6" nil nil ))nil )"7" "7" "7" "7" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" assert )"2" "not_one_element" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" "connected_domain" )"3" nil nil ))nil )"4" "4" "4" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "x!3" )"2" "x0!1" )"2" replace -1)"2" "2" replace -1)"2" "2" "Integral_split[T]" )"1" "x0!1" "a!1" "x!3" "f!1" )"1" "1" "1" "Integral(x0!1, a!1, f!1) = -Integral(a!1,x0!1, f!1)" )"1" assert )"1" replace "1" "1" "Integral(x0!1, x!3, (LAMBDA (t: T): f!1(t) - f!1(x0!1))) = Integral(x0!1, x!3, f!1) - Integral(x0!1, x!3, (LAMBDA (t: T): f!1(x0!1)))" )"1" "1" "Integral_const_fun[T]" )"1" "1" "MTT" "(x!3 - x0!1)" )"1" expand "const_fun" )"1" "1" "1" replace "1" assert )"1" "1" "II" "Integral(x0!1, x!3, f!1)" )"1" "1" "(II - f!1(x0!1) * MTT) / MTT = II/MTT - f!1(x0!1) " )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "Integral_diff[T]" )"2" "2" assert )"2" "2" "Integral_const_fun[T]" )"2" expand "const_fun" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "Integral_const_fun[T]" )"3" expand "const_fun" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"4" "4" "4" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "Integral_rev[T]" )"2" "2" assert )"2" "2" "2" "continuous_Integrable?[T]" )"2" "2" "1" nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "continuous_Integrable?[T]" )"2" "2" "1" nil nil )"2" "2" "2" "continuous_Integrable?[T]" )"2" "2" assert )"2" "2" "continuous_Integrable?[T]" )"2" "2" assert )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "continuous_Integrable?[T]" )"3" "3" assert )"3" "3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "not_one_element" )"2" nil nil ))nil )"3" "connected_domain" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (propax) nil nil )"4" "4" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "2" "Integral_diff[T]" )"1" "1" assert )"1" "1" "1" "continuous_Integrable?[T]" )"1" "1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "continuous_Integrable?[T]" )"2" "2" assert )"2" "2" assert )"2" "2" "const_continuous[T]" )"2" expand "const_fun" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "not_one_element" )"2" (propax) nil nil ))nil )"3" "connected_domain" )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "not_one_element" )"3" (skosimp*) nil nil ))nil )"4" "4" "connected_domain" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" deriv_domain_def nil )"bool" deriv_domain_def nil )"bool" integral_def nil )nil integral nil )nil integral nil )nil integral nil )"[T -> real]" real_fun_ops "reals/" )nil integral nil )nil integral nil )nil intervals_real "reals/" )nil integral nil )"real" integral_def nil )nil integral_def nil )nil continuous_functions nil ))nil )nil 3257698051"" (skosimp*)"" (rewrite "derivative_fun_alt" )"" (skosimp*)"" (expand "convergence" )"" (expand "convergence" )"" (prop)"1" (hide -1 -2)"1" (lemma "open" )"1" (inst?)"1" (skosimp*)"1" (expand "adh" )"1" (skosimp*)"1" (inst -1 "x!1 + delta!1/2" )"1" (split -1)"1" case "delta!1/2 < e!1" )"1" "x!1 + delta!1/2" )"1" expand "fullset" )"1" (grind) nil nil ))nil )"2" (assert ) nil nil ))nil )"2" "x!1+e!1/2" )"1" expand "fullset" )"1" expand "abs" )"1" (assert ) nil nil ))nil ))nil )"2" "connected_domain" )"2" "x!1" "x!1+delta!1/2" "x!1 + e!1/2" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "continuous?" )"2" (inst -1 "x!1" )"2" (expand "continuous?" )"2" (expand "convergence" )"2" (expand "convergence" )"2" (flatten)"2" (inst -2 "epsilon!1/2" )"2" "2" case "FORALL (x, x0: T): x /= x0 IMPLIES Integrable?[T](x0, x, (LAMBDA (t: T): f!1(t) - f!1(x0)))" )"1" "delta!1" )"1" "1" case "(FORALL (x,x0: T): x /= x0 IMPLIES abs((F!1(x) - F!1(x0))/(x-x0) - f!1(x0)) = abs(Integral(x0,x,(LAMBDA (t: T): f!1(t) - f!1(x0)))/(x-x0)))" )"1" "1" assert )"1" replace -1)"1" "1" "1" rewrite "abs_div" )"1" "abs(x!2 - x!1)" )"1" "x!2" )"1" assert )"1" "Integral_bounded[T]" )"1" "1" assert )"1" "epsilon!1/2" )"1" "1" assert )"1" "RX" "abs(Integral(x!1, x!2, LAMBDA (t: T): f!1(t) - f!1(x!1)))" )"1" "1" "abs(x!2 - x!1)" )"1" "abs(x!2 - x!1)" )"1" "ABS" "abs(x!2 - x!1)" )"1" "real_props" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil )"3" "3" "3" "3" "x!3" )"3" assert )"3" "3" "3" expand "fullset" )"3" "x!3" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" "2" rewrite "not_one_element" )nil nil ))nil ))nil ))nil ))nil )"3" "connected_domain" )"3" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil )"3" "3" "3" assert )"3" "3" "3" rewrite "not_one_element" )nil nil ))nil ))nil ))nil ))nil ))nil )"4" "connected_domain" )"4" nil nil ))nil )"5" "5" "5" "5" assert )nil nil ))nil ))nil ))nil )"6" "6" nil nil ))nil )"7" "7" rewrite "not_one_element" )nil nil ))nil )"8" "connected_domain" )"8" nil nil ))nil )"9" "9" "9" "9" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "not_one_element" )nil nil ))nil )"3" "connected_domain" )"3" nil nil ))nil )"4" "4" "4" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "x!3" )"2" "x0!1" )"2" replace -1)"2" "2" replace -1)"2" "2" "Integral_split[T]" )"1" "x0!1" "a!1" "x!3" "f!1" )"1" "1" "1" "Integral(x0!1, a!1, f!1) = -Integral(a!1,x0!1, f!1)" )"1" assert )"1" replace "1" "1" "Integral(x0!1, x!3, (LAMBDA (t: T): f!1(t) - f!1(x0!1))) = Integral(x0!1, x!3, f!1) - Integral(x0!1, x!3, (LAMBDA (t: T): f!1(x0!1)))" )"1" "1" "Integral_const_fun[T]" )"1" "1" "MTT" "(x!3 - x0!1)" )"1" expand "const_fun" )"1" "1" "1" replace "1" assert )"1" "1" "II" "Integral(x0!1, x!3, f!1)" )"1" "1" "(II - f!1(x0!1) * MTT) / MTT = II/MTT - f!1(x0!1) " )"1" "1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "Integral_diff[T]" )"2" "2" assert )"2" "2" "Integral_const_fun[T]" )"2" expand "const_fun" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "Integral_const_fun[T]" )"3" expand "const_fun" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"4" "4" "4" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "Integral_rev[T]" )"2" "2" assert )"2" "2" "2" "continuous_Integrable?[T]" )"2" "2" "1" nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "continuous_Integrable?[T]" )"3" "3" "1" nil nil )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "4" "continuous_Integrable?[T]" )"4" "4" assert )"4" "4" "4" "4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "continuous_Integrable?[T]" )"2" "2" assert )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "continuous_Integrable?[T]" )"3" "3" assert )"3" "3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "not_one_element" )nil nil ))nil ))nil )"3" "connected_domain" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (propax) nil nil )"4" "4" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "2" "Integral_diff[T]" )"1" "1" assert )"1" "1" "1" "continuous_Integrable?[T]" )"1" "1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "continuous_Integrable?[T]" )"2" "2" assert )"2" "2" assert )"2" "2" "const_continuous[T]" )"2" expand "const_fun" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "not_one_element" )nil nil ))nil )"3" "connected_domain" )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "not_one_element" )nil nil ))nil )"4" "4" "4" "connected_domain" )"4" "4" "y!1" )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" integral_def nil )nil integral nil )nil integral nil )nil integral nil )"[T -> real]" real_fun_ops "reals/" )nil integral nil )nil integral nil )nil integral nil )"real" integral_def nil )nil integral_def nil )nil continuous_functions nil ))nil ))nil 3610702232"" (skosimp*)"" (lemma "deriv_domain" ) (("" (propax) nil nil )) nil )) nil )nil fundamental_theorem nil )) nil ))nil 3257699451"" (skosimp*)"" (lemma "fundamental" )"" (name "xa" "choose({x: T | true})" )"1" (case "FORALL (x: T): Integrable?[T](xa, x, f!1)" )"1" (inst + "(LAMBDA (x: T): Integral(xa,x,f!1))" )"1" "(LAMBDA (x: T): Integral(xa,x,f!1))" "xa" "f!1" )"1" (assert ) nil nil )"2" (skosimp*)"2" (lemma "not_one_element" ) (("2" (inst?) nil nil ))nil ))nil )"3" (skosimp*)"3" (lemma "connected_domain" )"3" (inst?)"3" (inst?) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"2" (lemma "not_one_element" )"2" (lemma "not_one_element" )"2" (skosimp*) nil nil )) nil ))nil )"3" (lemma "connected_domain" ) (("3" (skosimp*) nil nil ))nil ))nil )"2" (skosimp*)"2" (rewrite "continuous_Integrable?[T]" )"1" (skosimp*)"1" (expand "continuous?" -2)"1" (hide -1 -2 2 3 4)"1" (expand "continuous?" -)"1" (inst?) 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 )"3" (skosimp*) (("3" (rewrite "not_one_element" ) nil nil ))nil )"4" (lemma "connected_domain" ) (("4" (skosimp*) nil nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (inst - "epsilon({x: T | TRUE})" )"2" (expand "member" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil fundamental_theorem nil )"bool" sets nil )"bool" sets nil )nil defined_types nil )"T" epsilons nil )"bool" integral_def nil )"bool" deriv_domain_def nil )"bool" deriv_domain_def nil )nil fundamental_theorem nil )nil fundamental_theorem nil )nil integral_def nil )"real" integral_def nil )"[T -> real]" fundamental_theorem nil )"({x: T | TRUE})" fundamental_theorem nil )nil integral nil )"bool" continuous_functions 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 numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" fundamental_theorem nil )nil fundamental_theorem nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" sets nil )"(p)" sets nil )"bool" booleans nil ))nil )nil 3257692741"" (skosimp*)"" (lemma "fundamental[T]" )"1" (name "xa" "choose({x: T | true})" )"1" (case "FORALL (x: T): Integrable?[T](xa, x, f!1)" )"1" (inst + "(LAMBDA (x: T): Integral(xa,x,f!1))" )"1" "(LAMBDA (x: T): Integral(xa,x,f!1))" "xa" "f!1" )"1" (assert ) nil nil )"2" (skosimp*)"2" (lemma "not_one_element" ) (("2" (inst?) nil nil ))nil ))nil )"3" (lemma "connected_domain" ) (("3" (propax) nil nil ))nil ))nil )"2" (lemma "not_one_element" ) (("2" (propax) nil nil ))nil )"3" (lemma "connected_domain" ) (("3" (propax) nil nil ))nil ))nil )"2" (skosimp*)"2" (rewrite "continuous_Integrable?[T]" )"2" (skosimp*)"2" (expand "continuous?" -2)"2" (hide -1 -2 2 3 4)"2" (expand "continuous?" -)"2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (inst - "epsilon({x: T | TRUE})" ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp*)"2" (lemma "open" ) (("2" (inst?) nil nil )) nil )) nil ))nil )"3" (lemma "not_one_element" ) (("3" (propax) nil nil )) nil )"4" (lemma "connected_domain" ) (("4" (propax) nil nil )) nil ))nil ))nil )nil integral nil )"real" integral_def nil )nil integral_def nil )"bool" integral_def nil ))nil ))nil 3610702232"" (lemma "deriv_domain" ) (("" (propax) nil nil )) nil )nil fundamental_theorem nil )) nil ))nil 3257692741"" (skosimp*)"" (lemma "continuous_Integrable?[T]" )"1" (inst?)"1" (split -1)"1" (assert )"1" (hide -1)"1" (case "FORALL (x): Integrable?[T](a!1, x, f!1)" )"1" case "derivable?[T](LAMBDA x: Integral[T](a!1, x, f!1))" )"1" case "derivable?[T](LAMBDA x: Integral[T](a!1, x, f!1) - F!1(x))" )"1" case "FORALL (xx: T): deriv((LAMBDA x: Integral(a!1, x, f!1) -F!1(x)),xx) = 0" )"1" (lemma "null_derivative[T]" )"1" (inst?)"1" (assert )"1" (replace -2)"1" assert )"1" "1" case "EXISTS (c:real): (LAMBDA x: Integral(a!1, x, f!1)) = F!1+const_fun(c)" )"1" "1" expand "+ " )"1" case "(LAMBDA x: Integral(a!1, x, f!1))(a!1) = (LAMBDA (x: T): const_fun(c!1)(x) + F!1(x))(a!1)" )"1" "1" assert )"1" expand "Integral" -1)"1" expand "const_fun" )"1" "1" case "(LAMBDA x: Integral(a!1, x, f!1))(b!1) = (LAMBDA (x: T): const_fun(c!1)(x) + F!1(x))(b!1)" )"1" "1" assert )"1" expand "const_fun" )"1" assert )nil nil ))nil ))nil ))nil )"2" replace -1)"2" nil nil ))nil )"3" "3" "not_one_element" )"3" nil nil ))nil ))nil )"4" "connected_domain" )"4" nil nil ))nil )"5" "5" "5" "5" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" (propax) nil nil ))nil )"3" "3" "3" assert )"3" "not_one_element" )"3" assert )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"4" "connected_domain" )"4" (skosimp*) nil nil ))nil )"5" "5" "5" "5" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "const_fun" )"2" "- F!1(a!1)" )"2" expand "+ " )"2" "1" expand "constant?" )"1" "a!1" "x!1" )"1" assert )"1" expand "Integral" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "not_one_element" )"2" (propax) nil nil ))nil )"3" "connected_domain" )"3" (propax) nil nil ))nil ))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 ))nil )"2" (lemma "deriv_domain" )"2" (propax) nil nil )) nil ))nil )"2" (skosimp*)"2" (lemma "deriv_diff_fun" )"2" (expand "-" )"2" "(LAMBDA x: Integral(a!1, x, f!1))" "F!1" )"1" assert )"1" case "deriv((LAMBDA x: Integral(a!1, x, f!1) - F!1(x)))(xx!1) = 0" )"1" expand "deriv" -1)"1" (propax) nil nil ))nil )"2" "2" replace -1)"2" assert )"2" "2" "2" "fundamental" )"2" "(LAMBDA x: Integral(a!1, x, f!1))" "a!1" "f!1" )"1" (assert ) nil nil )"2" "not_one_element" )"2" nil nil ))nil )"3" "connected_domain" )"3" nil nil ))nil )"4" "4" "4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "not_one_element" )"2" (propax) nil nil ))nil )"3" "connected_domain" )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (expand "derivable?" -1)"3" (inst?) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (lemma "derivable_diff" )"2" (expand "-" )"2" "(LAMBDA x: Integral[T](a!1, x, f!1))" "F!1" )"1" (lemma "not_one_element" )"1" (propax) nil nil )) nil )"2" (lemma "connected_domain" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "fundamental" )"2" "(LAMBDA x: Integral(a!1, x, f!1))" "a!1" "f!1" )"1" (assert ) nil nil )"2" (lemma "not_one_element" )"2" (propax) nil nil )) nil )"3" (lemma "connected_domain" )"3" (propax) nil nil )) nil ))nil ))nil ))nil )"3" (propax) nil nil ))nil )"2" (lemma "continuous_Integrable?[T]" )"2" (skosimp*)"2" (inst?)"2" (assert )"2" (skosimp*)"2" (expand "continuous?" -3)"2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "not_one_element" )"2" (lemma "connected_domain" )"2" (skosimp*)"2" (hide 2)"2" (hide -1 -2 -3 -4)"2" (expand "continuous?" -1)"2" (inst?) nil 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 ))nil ))nil )nil integral nil )"bool" deriv_domain_def nil )"bool" deriv_domain_def nil )nil intervals_real "reals/" )"real" integral_def nil )nil integral_def nil )"bool" derivatives nil )nil derivatives nil )"real" derivatives_def nil )"bool" derivatives_def nil )nil derivatives nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives nil )"[T -> real]" derivatives nil )"bool" integral_def nil ))nil ))nil 3319993827"" (skosimp*)"" (lemma "derivable_cont[T]" )"" (inst?)"" (assert )"" (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" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil fundamental_theorem nil )"[real -> boolean]" fundamental_theorem nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil derivatives nil )nil fundamental_theorem nil )nil fundamental_theorem 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 )"bool" deriv_domain_def nil )"bool" deriv_domain_def nil )nil integral nil )nil derivatives nil )nil booleans nil )"bool" derivatives nil )"[T -> real]" fundamental_theorem nil ))nil 3393933425"" (skosimp*)"" (lemma "fundamental3" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )nil fundamental_theorem nil )"[T -> real]" derivatives nil )nil derivatives nil )"bool" derivatives nil )nil booleans nil )nil fundamental_theorem nil )"[real -> boolean]" fundamental_theorem nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.107 Sekunden
(vorverarbeitet am 2026-05-05)
¤ *© Formatika GbR, Deutschland
2026-05-26
