fundamental_theorem.prf
Interaktion und
(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 3603195158"" (lemma "connected_domain" ) (("" (propax) nil nil )) nil )nil fundamental_theorem nil )) nil ))nil 3603195158"" (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 3603195158"" (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 )nil derivative_props 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]" fundamental_theorem nil )nil fundamental_theorem nil )"bool" lim_of_functions nil )"bool" continuous_functions nil )nil continuous_functions nil )"setof[real]" convergence_functions nil )nil fundamental_theorem nil )nil booleans nil )"bool" reals nil )nil fundamental_theorem nil )"bool" deriv_domain_def nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"set" sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"T" fundamental_theorem nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" fundamental_theorem nil )"T" fundamental_theorem nil )NOT const-decl "[bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"posreal" nil )"real" reals nil )"nzreal" nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" deriv_domain_def nil )"[bool, bool -> bool]" booleans 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 )"odd_int" integers nil )nil extra_real_propsnil )"[T -> real]" fundamental_theorem nil )"{yy: T | yy /= x!1}" fundamental_theoremnil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"nnreal" nil )"real" reals nil )nil real_props nil )"real" reals nil )nil intervals_real "reals/" )nil integral nil )nil real_props nil )nil reals nil )"(total_order?[real])" nil )"real" integral_def nil )nil integral_def nil )"[numfield -> numfield]" number_fields nil )nil continuous_functions nil )"bool" convergence_functions nil )"real" reals nil )"real" reals 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 )"setof[real]" convergence_functions 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 )"bool" convergence_functions nil ))nil ))nil 3603195158"" (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 3603195158"" (lemma "deriv_domain" ) (("" (propax) nil nil )) nil )nil fundamental_theorem nil )) nil ))nil 3603195620"" (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" 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 ))nil )"2" (skosimp*)"2" (lemma "deriv_diff_fun[T]" )"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" (expand "derivable?" -1)"3" (inst?)"3" (lemma "deriv_domain" )"3" (propax) nil nil )) nil ))nil ))nil )"4" (skosimp*)"4" (expand "derivable?" -1)"4" (inst?) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (lemma "derivable_diff[T]" )"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 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 )nil intervals_real "reals/" )"bool" reals nil ) (<= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" continuous_functions nil )"real" integral_def nil )nil integral_def nil )"bool" derivatives nil )nil derivatives nil )"real" derivatives_def nil )"bool" derivatives_def nil )"[T, T -> boolean]" equalities nil )"bool" deriv_domain_def nil )"T" fundamental_theorem nil )"[T -> real]" fundamental_theorem nil )"[T -> real]" fundamental_theorem nil )nil derivatives nil )"bool" real_fun_preds "reals/" )"real" reals nil )"[numfield -> numfield]" number_fields nil )"real" reals nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[bool, bool -> bool]" booleans nil )nil fundamental_theorem nil )nil fundamental_theorem nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"(convergent?)" nil )"deriv_fun" derivatives nil )nil derivative_props nil )nil derivatives nil )"[T -> real]" derivatives nil )nil fundamental_theorem nil )"[T -> real]" real_fun_ops "reals/" )nil fundamental_theorem nil )"real" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" integral_def 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 )"bool" real_fun_preds "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"(convergent?)" nil )nil derivative_props nil )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
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.158Bemerkung:
(vorverarbeitet am 2026-04-26)
¤ *Bot Zugriff
2026-05-26
