|
(fundamental_theorem
(deriv_domain 0
(deriv_domain-2 nil 3472399705
("" (lemma "connected_domain")
(("" (lemma "connected_deriv_domain[T]")
(("" (lemma not_one_element) (("" (assert) nil nil)) nil)) nil))
nil)
((T formal-nonempty-subtype-decl nil fundamental_theorem nil)
(T_pred const-decl "[real -> boolean]" fundamental_theorem nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(connected_deriv_domain formula-decl nil deriv_domain_def nil)
(not_one_element formula-decl nil fundamental_theorem nil)
(connected_domain formula-decl nil fundamental_theorem nil))
nil)
(deriv_domain-1 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))
(IMP_derivative_props_TCC1 0
(IMP_derivative_props_TCC1-1 nil 3610702394
("" (lemma "connected_domain") (("" (propax) nil nil)) nil)
((connected_domain formula-decl nil fundamental_theorem nil)) nil))
(IMP_derivative_props_TCC2 0
(IMP_derivative_props_TCC2-1 nil 3610702394
("" (lemma "not_one_element") (("" (propax) nil nil)) nil)
((not_one_element formula-decl nil fundamental_theorem nil)) nil))
(fundamental_TCC1 0
(fundamental_TCC1-1 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)
((T formal-nonempty-subtype-decl nil fundamental_theorem nil)
(T_pred const-decl "[real -> boolean]" fundamental_theorem nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(continuous_Integrable? formula-decl nil integral nil)
(connected? const-decl "bool" deriv_domain_def nil)
(not_one_element? const-decl "bool" deriv_domain_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(continuous? const-decl "bool" continuous_functions nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(Closed_interval type-eq-decl nil intervals_real "reals/")
(not_one_element formula-decl nil fundamental_theorem nil)
(connected_domain formula-decl nil fundamental_theorem nil))
shostak))
(fundamental_TCC2 0
(fundamental_TCC2-1 nil 3610702232
("" (skosimp*)
(("" (lemma "deriv_domain") (("" (propax) nil nil)) nil)) nil)
((deriv_domain formula-decl nil fundamental_theorem nil)) nil))
(fundamental 0
(fundamental-2 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"
(hide -1)
(("1"
(expand "adh")
(("1"
(skosimp*)
(("1"
(lemma "not_one_element")
(("1"
(expand "not_one_element?")
(("1"
(inst -1 "x!1")
(("1"
(skosimp*)
(("1"
(case "x!1 <= y!1")
(("1"
(inst
+
"min(y!1,x!1+e!1/2)")
(("1" (grind) nil nil)
("2"
(expand "min")
(("2"
(ground)
(("1"
(lemma
"connected_domain")
(("1"
(expand
"connected?")
(("1"
(inst
-1
"x!1"
"y!1"
"x!1 + e!1 / 2")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(lift-if)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(inst
+
"max(y!1,x!1-e!1/2)")
(("1" (grind) nil nil)
("2"
(expand "max")
(("2"
(ground)
(("1"
(lemma
"connected_domain")
(("1"
(expand
"connected?")
(("1"
(inst
-1
"y!1"
"x!1"
"x!1 - e!1 / 2")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(lift-if)
(("2"
(ground)
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"
(skosimp*)
(("2"
(case
"FORALL (x, x0: T): x /= x0 IMPLIES Integrable?[T](x0, x, (LAMBDA (t: T): f!1(t) - f!1(x0)))")
(("1"
(inst + "delta!1")
(("1"
(skosimp*)
(("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"
(inst?)
(("1"
(assert)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(hide -1)
(("1"
(rewrite "abs_div")
(("1"
(mult-by
1
"abs(x!2 - x!1)")
(("1"
(inst -4 "x!2")
(("1"
(assert)
(("1"
(lemma
"Integral_bounded[T]")
(("1"
(inst?)
(("1"
(assert)
(("1"
(inst
-1
"epsilon!1/2")
(("1"
(split
-1)
(("1"
(assert)
nil
nil)
("2"
(reveal
-6)
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil)
("3"
(skosimp*)
(("3"
(reveal
-3)
(("3"
(hide
2)
(("3"
(inst
-1
"x!3")
(("3"
(assert)
(("3"
(hide
-3
-4
2)
(("3"
(hide
-3)
(("3"
(expand
"fullset")
(("3"
(typepred
"x!3")
(("3"
(grind)
nil
nil))
nil))
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))
nil)
("2"
(lemma
"not_one_element")
(("2"
(propax)
nil
nil))
nil)
("3"
(lemma
"connected_domain")
(("3"
(propax)
nil
nil))
nil)
("4"
(hide-all-but
1)
(("4"
(reveal -8)
(("4"
(inst?)
(("4"
(assert)
nil
nil))
nil))
nil))
nil)
("5"
(lemma
"not_one_element")
(("5"
(propax)
nil
nil))
nil)
("6"
(lemma
"connected_domain")
(("6"
(propax)
nil
nil))
nil)
("7"
(hide-all-but
1)
(("7"
(reveal -7)
(("7"
(inst?)
(("7"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(reveal -6)
(("2"
(inst?)
(("2"
(assert)
(("2"
(lemma
"not_one_element")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(lemma
"connected_domain")
(("3"
(propax)
nil
nil))
nil)
("4"
(hide-all-but 1)
(("4"
(reveal -6)
(("4"
(inst?)
(("4"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(skosimp*)
(("2"
(hide -1 -2 -3 -4 -5)
(("2"
(inst-cp -1 "x!3")
(("2"
(inst -1 "x0!1")
(("2"
(replace -1)
(("2"
(hide -1)
(("2"
(replace -1)
(("2"
(hide -1)
(("2"
(lemma
"Integral_split[T]")
(("1"
(inst
-1
"x0!1"
"a!1"
"x!3"
"f!1")
(("1"
(split
-1)
(("1"
(flatten)
(("1"
(case-replace
"Integral(x0!1, a!1, f!1) = -Integral(a!1,x0!1, f!1)")
(("1"
(assert)
(("1"
(replace
-3)
(("1"
(hide
-3)
(("1"
(case-replace
"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"
(hide
-1
-2
-3)
(("1"
(lemma
"Integral_const_fun[T]")
(("1"
(inst?)
(("1"
(name-replace
"MTT"
"(x!3 - x0!1)")
(("1"
(expand
"const_fun")
(("1"
(inst?)
(("1"
(flatten)
(("1"
(replace
-2)
(("1"
(assert)
(("1"
(hide
-1
-2)
(("1"
(name-replace
"II"
"Integral(x0!1, x!3, f!1)")
(("1"
(reveal
-5)
(("1"
(case-replace
"(II - f!1(x0!1) * MTT) / MTT = II/MTT - f!1(x0!1) ")
(("1"
(hide
3)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(hide-all-but
1)
(("2"
(lemma
"Integral_diff[T]")
(("2"
(inst?)
(("2"
(assert)
(("2"
(hide
2)
(("2"
(lemma
"Integral_const_fun[T]")
(("2"
(expand
"const_fun")
(("2"
(inst?)
(("2"
(flatten)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide-all-but
1)
(("3"
(lemma
"Integral_const_fun[T]")
(("3"
(expand
"const_fun")
(("3"
(inst?)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("4"
(hide-all-but
1)
(("4"
(reveal
-8)
(("4"
(inst?)
(("4"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(lemma
"Integral_rev[T]")
(("2"
(inst?)
(("2"
(assert)
(("2"
(hide
2)
(("2"
(reveal
-14)
(("2"
(lemma
"continuous_Integrable?[T]")
(("2"
(inst?)
(("2"
(split
-1)
(("1"
(propax)
nil
nil)
("2"
(skosimp*)
(("2"
(inst?)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
3)
(("2"
(hide-all-but
1)
(("2"
(lemma
"continuous_Integrable?[T]")
(("2"
(inst?)
(("2"
(split
-1)
(("1"
(propax)
nil
nil)
("2"
(hide
2)
(("2"
(skosimp*)
(("2"
(lemma
"continuous_Integrable?[T]")
(("2"
(inst?)
(("2"
(assert)
(("2"
(inst?)
(("2"
(lemma
"continuous_Integrable?[T]")
(("2"
(inst?)
(("2"
(assert)
(("2"
(reveal
-12)
(("2"
(reveal
-13)
(("2"
(inst?)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide
3)
(("3"
(lemma
"continuous_Integrable?[T]")
(("3"
(inst?)
(("3"
(assert)
(("3"
(skosimp*)
(("3"
(reveal
-12)
(("3"
(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))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (propax) nil nil)
("4"
(skosimp*)
(("4" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(skosimp*)
(("2"
(hide -1 -2 -3)
(("2"
(reveal -5)
(("2"
(lemma "Integral_diff[T]")
(("1"
(inst?)
(("1"
(assert)
(("1"
(hide 3)
(("1"
(prop)
(("1"
(lemma
"continuous_Integrable?[T]")
(("1"
(inst?)
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(inst?)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"continuous_Integrable?[T]")
(("2"
(inst?)
(("2"
(assert)
(("2"
(skosimp*)
(("2"
(assert)
(("2"
(hide-all-but
1)
(("2"
(lemma
"const_continuous[T]")
(("2"
(expand
"const_fun")
(("2"
(inst?)
nil
nil))
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))
nil))
nil))
nil)
("3"
(lemma "not_one_element")
(("3" (skosimp*) nil nil))
nil)
("4"
(skosimp*)
(("4"
(lemma "connected_domain")
(("4" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((connected? const-decl "bool" deriv_domain_def nil)
(not_one_element? const-decl "bool" deriv_domain_def nil)
(Integrable? const-decl "bool" integral_def nil)
(continuous_Integrable? formula-decl nil integral nil)
(Integral_rev formula-decl nil integral nil)
(Integral_diff formula-decl nil integral nil)
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(Integral_const_fun formula-decl nil integral nil)
(Integral_split formula-decl nil integral nil)
(Closed_interval type-eq-decl nil intervals_real "reals/")
(Integral_bounded formula-decl nil integral nil)
(Integral const-decl "real" integral_def nil)
(Integrable_funs type-eq-decl nil integral_def nil)
(const_continuous formula-decl nil continuous_functions nil))
nil)
(fundamental-1 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"
(inst + "x!1 + delta!1/2")
(("1"
(expand "fullset")
(("1" (grind) nil nil))
nil)
("2" (assert) nil nil))
nil)
("2"
(inst + "x!1+e!1/2")
(("1"
(expand "fullset")
(("1"
(expand "abs")
(("1" (assert) nil nil))
nil))
nil)
("2"
(lemma "connected_domain")
(("2"
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.107Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
