|
(integral_diff_doms
(int_diff_dom_TCC1 0
(int_diff_dom_TCC1-1 nil 3319997019
("" (skosimp*)
(("" (lemma "connected_domain")
(("" (inst - "x!1" "y!1" "z!1") (("" (assert) nil nil)) nil))
nil))
nil)
((connected_domain formula-decl nil integral_diff_doms nil)) nil))
(int_diff_dom_TCC2 0
(int_diff_dom_TCC2-1 nil 3319997019
("" (lemma "not_one_element") (("" (skosimp*) nil nil)) nil)
((not_one_element formula-decl nil integral_diff_doms nil)) nil))
(int_diff_dom_TCC3 0
(int_diff_dom_TCC3-1 nil 3319997019
("" (lemma "con_dom_U") (("" (skosimp*) nil nil)) nil)
((con_dom_U formula-decl nil integral_diff_doms nil)) nil))
(int_diff_dom_TCC4 0
(int_diff_dom_TCC4-1 nil 3319997019
("" (lemma "not_one_U ") (("" (skosimp*) nil nil)) nil)
((not_one_U formula-decl nil integral_diff_doms nil)) nil))
(int_diff_dom_TCC5 0
(int_diff_dom_TCC5-1 nil 3319997019
("" (lemma "connected_domain")
(("" (expand "connected?")
(("" (skosimp*)
(("" (inst - "a!1" "b!1" "x!1") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((connected? const-decl "bool" deriv_domain_def nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" integral_diff_doms nil)
(T formal-nonempty-subtype-decl nil integral_diff_doms nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(connected_domain formula-decl nil integral_diff_doms nil))
nil))
(int_diff_dom_TCC6 0
(int_diff_dom_TCC6-1 nil 3319997019
("" (lemma "con_dom_U")
(("" (expand "connected?")
(("" (skosimp*)
(("" (inst - "a!1" "b!1" "x!1") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((connected? const-decl "bool" deriv_domain_def nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(U_pred const-decl "[real -> boolean]" integral_diff_doms nil)
(U formal-nonempty-subtype-decl nil integral_diff_doms nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(con_dom_U formula-decl nil integral_diff_doms nil))
nil))
(int_diff_dom 0
(int_diff_dom-2 nil 3477655792
("" (skosimp*)
(("" (expand "integrable?")
(("" (skosimp*)
(("" (lemma "integral_def[T]")
(("1" (inst?)
(("1" (assert)
(("1" (hide 2)
(("1" (case-replace "integral(a!1, b!1, g!1) = S!2")
(("1" (expand "integral?")
(("1" (hide -1)
(("1" (skosimp*)
(("1" (inst -7 "epsi!1")
(("1" (skosimp*)
(("1" (inst + "delta!1")
(("1"
(skosimp*)
(("1"
(typepred "P!1")
(("1"
(inst -12 "P!1")
(("1"
(assert)
(("1"
(split -12)
(("1"
(inst -1 "R!1")
(("1"
(assert)
(("1"
(typepred "R!1")
(("1"
(hide 2)
(("1"
(expand
"Riemann_sum?")
(("1"
(skosimp*)
(("1"
(inst + "xis!1")
(("1"
(assert)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(expand
"Rie_sum")
(("1"
(assert)
(("1"
(rewrite
"sigma_restrict_eq")
(("1"
(rewrite
"sigma_restrict_eq")
(("1"
(hide
2)
(("1"
(expand
"restrict")
(("1"
(hide
2)
(("1"
(apply-extensionality
1
:hide?
t)
(("1"
(hide
-4
-11)
(("1"
(inst?)
(("1"
(assert)
(("1"
(expand
"finseq_appl")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(hide
-11
-12)
(("2"
(typepred
"xis!1")
(("2"
(expand
"xis?")
(("2"
(assert)
(("2"
(inst
-
"i!1")
(("2"
(flatten)
(("2"
(assert)
(("2"
(lemma
"con_dom_U")
(("2"
(expand
"connected?")
(("2"
(inst
-
"a!1"
"b!1"
"xis!1(i!1)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(skosimp*)
(("3"
(assert)
(("3"
(typepred
"P!1`seq(x1!1)")
(("3"
(lemma
"con_dom_U")
(("3"
(expand
"connected?")
(("3"
(inst
-
"a!1"
"b!1"
"P!1`seq(x1!1)")
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
-11
-12
2)
(("2"
(skosimp*)
(("2"
(lemma
"con_dom_U")
(("2"
(expand
"connected?")
(("2"
(inst
-
"a!1"
"b!1"
"xis!1(n!1)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide
2)
(("3"
(skosimp*)
(("3"
(assert)
(("3"
(assert)
(("3"
(hide
2)
(("3"
(lemma
"con_dom_U")
(("3"
(expand
"connected?")
(("3"
(inst
-
"a!1"
"b!1"
"P!1`seq(x1!1)")
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4"
(hide
2
3)
(("4"
(skosimp*)
(("4"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(hide
-11
-12
2)
(("2"
(skosimp*)
(("2"
(lemma
"con_dom_U")
(("2"
(assert)
(("2"
(expand
"connected?")
(("2"
(inst
-
"a!1"
"b!1"
"xis!1(n!1)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide
2)
(("3"
(skosimp*)
(("3"
(assert)
(("3"
(lemma
"con_dom_U")
(("3"
(expand
"connected?")
(("3"
(inst
-
"a!1"
"b!1"
"P!1`seq(x1!1)")
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4"
(skosimp*)
(("4"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(prop)
(("1"
(skosimp*)
(("1"
(assert)
(("1"
(lemma
"con_dom_U")
(("1"
(expand
"connected?")
(("1"
(inst
-
"a!1"
"b!1"
"xis!1(x1!1)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred
"xis!1")
(("2"
(assert)
(("2"
(expand
"xis?")
(("2"
(assert)
(("2"
(skosimp*)
(("2"
(expand
"finseq_appl")
(("2"
(inst?)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "width")
(("2" (propax) nil nil))
nil))
nil))
nil)
("2"
(prop)
(("2"
(skosimp*)
(("2"
(lemma "parts_order[T]")
(("2"
(inst
-
"a!1"
"b!1"
"P!1"
"0"
"x1!1")
(("2"
(assert)
(("2"
(case-replace
"x1!1 = 0")
(("1" (assert) nil nil)
("2"
(assert)
(("2"
(lemma "con_dom_U")
(("2"
(expand
"connected?")
(("2"
(inst
-
"a!1"
"b!1"
"P!1`seq(x1!1)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "integral_def[U]")
(("1" (inst?) (("1" (assert) nil nil)) nil)
("2" (lemma "not_one_U")
(("2" (propax) nil nil)) nil)
("3" (lemma "con_dom_U")
(("3" (propax) nil nil)) nil))
nil))
nil)
("3" (lemma "not_one_U") (("3" (propax) nil nil))
nil)
("4" (lemma "con_dom_U") (("4" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element")
(("2" (lemma "connected_domain")
(("2" (lemma "not_one_U") (("2" (propax) nil nil))
nil))
nil))
nil)
("3" (lemma "con_dom_U") (("3" (propax) nil nil)) nil))
nil)
("2" (lemma "connected_domain")
(("2" (lemma "not_one_element") (("2" (propax) nil nil))
nil))
nil)
("3" (lemma "connected_domain") (("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
((integrable? const-decl "bool" integral_def nil)
(T formal-nonempty-subtype-decl nil integral_diff_doms nil)
(T_pred const-decl "[real -> boolean]" integral_diff_doms 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)
(integral_def formula-decl nil integral_def 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)
(not_one_element formula-decl nil integral_diff_doms nil)
(connected_domain formula-decl nil integral_diff_doms nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(partition type-eq-decl nil integral_def nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(parts_order formula-decl nil integral_def nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(width const-decl "posreal" integral_def nil)
(Riemann_sum? const-decl "bool" integral_def nil)
(g!1 skolem-const-decl "[U -> real]" integral_diff_doms nil)
(f!1 skolem-const-decl "[T -> real]" integral_diff_doms nil)
(R!1 skolem-const-decl "(Riemann_sum?(a!1, b!1, P!1, f!1))"
integral_diff_doms nil)
(xis? const-decl "bool" integral_def nil)
(xis!1 skolem-const-decl "(xis?(a!1, b!1, P!1))" integral_diff_doms
nil)
(real_times_real_is_real application-judgement "real" reals nil)
(Rie_sum const-decl "real" integral_def nil)
(integer nonempty-type-from-decl nil integers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(T_low type-eq-decl nil sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sigma_restrict_eq formula-decl nil sigma "reals/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(con_dom_U formula-decl nil integral_diff_doms nil)
(restrict const-decl "[T -> real]" sigma "reals/")
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_diff_doms
nil)
(b!1 skolem-const-decl "real" integral_diff_doms nil)
(a!1 skolem-const-decl "real" integral_diff_doms nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(not_one_U formula-decl nil integral_diff_doms nil)
(integral const-decl "{S: real | integral?(a, b, ff, S)}"
integral_def nil)
(integral? const-decl "bool" integral_def nil)
(< const-decl "bool" reals nil)
(U_pred const-decl "[real -> boolean]" integral_diff_doms nil)
(U formal-nonempty-subtype-decl nil integral_diff_doms nil))
nil)
(int_diff_dom-1 nil 3321116320
("" (skosimp*)
(("" (expand "integrable?")
(("" (skosimp*)
(("" (lemma "integral_def[T]")
(("1" (inst?)
(("1" (assert)
(("1" (hide 2)
(("1" (case-replace "integral(a!1, b!1, g!1) = S!2")
(("1" (expand "integral?")
(("1" (hide -1)
(("1" (skosimp*)
(("1" (inst -7 "epsi!1")
(("1" (skosimp*)
(("1" (inst + "delta!1")
(("1"
(skosimp*)
(("1"
(typepred "P!1")
(("1"
(inst -12 "P!1")
(("1"
(assert)
(("1"
(split -12)
(("1"
(inst -1 "R!1")
(("1"
(assert)
(("1"
(typepred "R!1")
(("1"
(hide 2)
(("1"
(expand
"Riemann_sum?")
(("1"
(skosimp*)
(("1"
(inst + "xis!1")
(("1"
(assert)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(expand
"Rie_sum")
(("1"
(assert)
(("1"
(rewrite
"sigma_restrict_eq")
(("1"
(hide
2)
(("1"
(expand
"restrict")
(("1"
(apply-extensionality
1
:hide?
t)
(("1"
(hide
-4
-11)
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(hide
-11
-12)
(("2"
(typepred
"xis!1")
(("2"
(expand
"xis?")
(("2"
(assert)
(("2"
(inst
-
"i!1")
(("2"
(flatten)
(("2"
(assert)
(("2"
(lemma
"con_dom_U")
(("2"
(inst
-
"a!1"
"b!1"
"xis!1(i!1)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
-11
-12
2)
(("2"
(skosimp*)
(("2"
(lemma
"con_dom_U")
(("2"
(inst
-
"a!1"
"b!1"
"xis!1(n!1)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("3"
(hide
2)
(("3"
(skosimp*)
(("3"
(assert)
nil
nil))
nil))
nil)
("4"
(skosimp*)
(("4"
(assert)
nil
nil))
nil)
("5"
(skosimp*)
(("5"
(assert)
nil
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(prop)
(("1"
(skosimp*)
(("1"
(assert)
(("1"
(lemma
"con_dom_U")
(("1"
(inst
-
"a!1"
"b!1"
"xis!1(x1!1)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(typepred
"xis!1")
(("2"
(expand
"xis?")
(("2"
(assert)
(("2"
(inst?)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "width")
(("2" (propax) nil nil))
nil))
nil))
nil)
("2"
(prop)
(("2"
(skosimp*)
(("2"
(lemma "parts_order[T]")
(("2"
(inst
-
"a!1"
"b!1"
"P!1"
"0"
"x1!1")
(("2"
(assert)
(("2"
(case-replace
"x1!1 = 0")
(("1" (assert) nil nil)
("2"
(assert)
(("2"
(lemma "con_dom_U")
(("2"
(inst
-
"a!1"
"b!1"
"P!1`seq(x1!1)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "integral_def[U]")
(("1" (inst?) (("1" (assert) nil nil)) nil)
("2" (lemma "not_one_U")
(("2" (propax) nil nil)) nil)
("3" (lemma "con_dom_U")
(("3" (propax) nil nil)) nil))
nil))
nil)
("3" (lemma "not_one_U") (("3" (propax) nil nil))
nil)
("4" (lemma "con_dom_U") (("4" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element")
(("2" (lemma "connected_domain")
(("2" (lemma "not_one_U") (("2" (propax) nil nil))
nil))
nil))
nil)
("3" (lemma "con_dom_U") (("3" (propax) nil nil)) nil))
nil)
("2" (lemma "connected_domain")
(("2" (lemma "not_one_element") (("2" (propax) nil nil))
nil))
nil)
("3" (lemma "connected_domain") (("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
((integral? const-decl "bool" integral_def nil)
(integral const-decl "{S: real | integral?(a, b, ff, S)}"
integral_def nil)
(restrict const-decl "[T -> real]" sigma "reals/")
(sigma_restrict_eq formula-decl nil sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(Rie_sum const-decl "real" integral_def nil)
(xis? const-decl "bool" integral_def nil)
(Riemann_sum? const-decl "bool" integral_def nil)
(width const-decl "posreal" integral_def nil)
(parts_order formula-decl nil integral_def nil)
(partition type-eq-decl nil integral_def nil)
(integral_def formula-decl nil integral_def nil)
(integrable? const-decl "bool" integral_def nil))
shostak))
(Int_diff_dom_TCC1 0
(Int_diff_dom_TCC1-1 nil 3320059104
("" (skosimp*)
(("" (lemma "connected_domain")
(("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((connected_domain formula-decl nil integral_diff_doms nil)) nil))
(Int_diff_dom_TCC2 0
(Int_diff_dom_TCC2-1 nil 3320059104
("" (lemma "not_one_element") (("" (skosimp*) nil nil)) nil)
((not_one_element formula-decl nil integral_diff_doms nil)) nil))
(Int_diff_dom_TCC3 0
(Int_diff_dom_TCC3-1 nil 3320059104
("" (lemma "con_dom_U") (("" (skosimp*) nil nil)) nil)
((con_dom_U formula-decl nil integral_diff_doms nil)) nil))
(Int_diff_dom_TCC4 0
(Int_diff_dom_TCC4-1 nil 3320059104
("" (lemma "not_one_U") (("" (skosimp*) nil nil)) nil)
((not_one_U formula-decl nil integral_diff_doms nil)) nil))
(Int_diff_dom_TCC5 0
(Int_diff_dom_TCC5-1 nil 3320059104
("" (skosimp*)
(("" (typepred "x!1")
(("" (ground)
(("1" (lemma "connected_domain")
(("1" (expand "connected?")
(("1" (inst - "a!1" "b!1" "x!1") (("1" (assert) nil nil))
nil))
nil))
nil)
("2" (lemma "connected_domain")
(("2" (expand "connected?")
(("2" (inst - "b!1" "a!1" "x!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Closed_interval type-eq-decl nil intervals_real "reals/")
(< const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.120Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
