|
(restriction_integral
(restrict_Integrable_TCC1 0
(restrict_Integrable_TCC1-1 nil 3432062629
("" (lemma "sub_domain")
(("" (skosimp)
(("" (inst - "a!1") (("" (skosimp) (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((T1 formal-subtype-decl nil restriction_integral nil)
(T1_pred const-decl "[real -> boolean]" restriction_integral 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)
(sub_domain formula-decl nil restriction_integral nil))
nil))
(restrict_Integrable_TCC2 0
(restrict_Integrable_TCC2-1 nil 3432062629
("" (expand "connected?")
(("" (skosimp)
(("" (lemma "connected_domain_T2" ("x" "x!1" "y" "y!1"))
(("" (inst - "z!1") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(connected_domain_T2 formula-decl nil restriction_integral 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)
(T2_pred const-decl "[real -> boolean]" restriction_integral nil)
(T2 formal-subtype-decl nil restriction_integral nil)
(connected? const-decl "bool" deriv_domain_def "analysis/"))
nil))
(restrict_Integrable_TCC3 0
(restrict_Integrable_TCC3-1 nil 3432062629
("" (expand "not_one_element?")
(("" (lemma "not_one_element_T2") (("" (propax) nil nil)) nil))
nil)
((not_one_element_T2 formula-decl nil restriction_integral nil)
(not_one_element? const-decl "bool" deriv_domain_def "analysis/"))
nil))
(restrict_Integrable_TCC4 0
(restrict_Integrable_TCC4-1 nil 3432062629
("" (expand "connected?")
(("" (lemma "connected_domain_T1") (("" (propax) nil nil)) nil))
nil)
((connected_domain_T1 formula-decl nil restriction_integral nil)
(connected? const-decl "bool" deriv_domain_def "analysis/"))
nil))
(restrict_Integrable_TCC5 0
(restrict_Integrable_TCC5-1 nil 3432062629
("" (lemma "not_one_element_T1")
(("" (expand "not_one_element?") (("" (propax) nil nil)) nil)) nil)
((not_one_element? const-decl "bool" deriv_domain_def "analysis/")
(not_one_element_T1 formula-decl nil restriction_integral nil))
nil))
(restrict_Integrable 0
(restrict_Integrable-1 nil 3432063069
("" (auto-rewrite "xis_lem")
((""
(case "FORALL (a, b: T1, f: [T2 -> real]): a
(integrable?[T2](a, b, f) <=>
integrable?[T1](a, b, restrict[T2, T1, real](f)))")
(("1" (skosimp)
(("1" (expand "Integrable?")
(("1" (case-replace "a!1=b!1")
(("1" (assert) nil nil)
("2" (case-replace "a!1)
(("1" (inst - "a!1" "b!1" "f!1") (("1" (assert) nil nil))
nil)
("2" (inst - "b!1" "a!1" "f!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (split)
(("1" (flatten)
(("1" (expand "integrable?")
(("1" (skosimp)
(("1" (inst + "S!1")
(("1" (expand "integral?")
(("1" (skosimp)
(("1" (inst - "epsi!1")
(("1" (skosimp)
(("1" (inst + "delta!1")
(("1"
(skosimp)
(("1"
(inst - "P!1")
(("1"
(split)
(("1"
(skosimp)
(("1"
(inst - "R!1")
(("1"
(typepred "R!1")
(("1"
(hide -2 2)
(("1"
(expand "Riemann_sum?")
(("1"
(skosimp)
(("1"
(inst + "xis!1")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(expand
"Rie_sum")
(("1"
(expand
"finseq_appl")
(("1"
(expand
"restrict")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -1)
(("2"
(split)
(("1"
(skosimp)
(("1"
(typepred
"xis!1(x1!1)")
(("1"
(assert)
(("1"
(lemma
"sub_domain"
("x"
"xis!1(x1!1)"))
(("1"
(skosimp)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred
"xis!1")
(("2"
(expand
"xis?")
(("2"
(expand
"finseq_appl")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "width")
(("2" (propax) nil nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(split)
(("1"
(skosimp)
(("1"
(typepred "P!1`seq(x1!1)")
(("1"
(assert)
(("1"
(lemma
"sub_domain"
("x" "P!1`seq(x1!1)"))
(("1"
(skosimp)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(typepred "P!1")
(("2"
(inst - "ii!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "integrable?")
(("2" (skosimp)
(("2" (inst + "S!1")
(("2" (expand "integral?")
(("2" (skosimp)
(("2" (inst - "epsi!1")
(("2" (skosimp)
(("2" (inst + "delta!1")
(("2"
(skosimp)
(("2"
(inst - "P!1")
(("1"
(split)
(("1"
(skosimp)
(("1"
(inst - "R!1")
(("1"
(hide -1 2)
(("1"
(typepred "R!1")
(("1"
(expand "Riemann_sum?")
(("1"
(skosimp)
(("1"
(inst + "xis!1")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(expand
"Rie_sum")
(("1"
(expand
"restrict")
(("1"
(expand
"finseq_appl")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(split)
(("1"
(skosimp)
(("1"
(typepred
"xis!1(x1!1)")
(("1"
(assert)
(("1"
(lemma
"connected_domain_T1"
("x"
"a!1"
"y"
"b!1"
"z"
"xis!1(x1!1)"))
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(typepred
"xis!1")
(("2"
(expand "xis?")
(("2"
(expand
"finseq_appl")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "width")
(("2" (propax) nil nil))
nil))
nil))
nil)
("2"
(hide 2 -1)
(("2"
(split)
(("1"
(skosimp)
(("1"
(typepred "P!1`seq(x1!1)")
(("1"
(assert)
(("1"
(lemma
"connected_domain_T1"
("x"
"a!1"
"y"
"b!1"
"z"
"P!1`seq(x1!1)"))
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(typepred "P!1")
(("2"
(inst - "ii!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (skosimp*)
(("3" (lemma "sub_domain" ("x" "x!1"))
(("3" (skolem!) (("3" (assert) nil nil)) nil)) nil))
nil))
nil)
("4" (skosimp)
(("4" (lemma "sub_domain" ("x" "b!1"))
(("4" (skolem!) (("4" (assert) nil nil)) nil)) nil))
nil)
("5" (hide 2)
(("5" (skosimp)
(("5" (lemma "sub_domain" ("x" "a!1"))
(("5" (skolem!) (("5" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((restrict const-decl "R" restrict nil)
(integrable? const-decl "bool" integral_def "analysis/")
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T2 formal-subtype-decl nil restriction_integral nil)
(T2_pred const-decl "[real -> boolean]" restriction_integral nil)
(T1 formal-subtype-decl nil restriction_integral nil)
(T1_pred const-decl "[real -> boolean]" restriction_integral 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)
(Integrable? const-decl "bool" integral_def "analysis/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(P!1 skolem-const-decl "partition[T2](a!1, b!1)"
restriction_integral nil)
(xis!1 skolem-const-decl "(xis?(a!1, b!1, P!1))"
restriction_integral nil)
(connected_domain_T1 formula-decl nil restriction_integral nil)
(R!1 skolem-const-decl "(Riemann_sum?(a!1, b!1, P!1, f!1))"
restriction_integral nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(integral? const-decl "bool" integral_def "analysis/")
(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)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(P!1 skolem-const-decl "partition[T1](a!1, b!1)"
restriction_integral nil)
(partition type-eq-decl nil integral_def "analysis/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below type-eq-decl nil naturalnumbers 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/")
(b!1 skolem-const-decl "T1" restriction_integral nil)
(a!1 skolem-const-decl "T1" restriction_integral nil)
(<= const-decl "bool" reals nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(width const-decl "posreal" integral_def "analysis/")
(NOT const-decl "[bool -> bool]" booleans nil)
(xis? const-decl "bool" integral_def "analysis/")
(xis!1 skolem-const-decl "(xis?(a!1, b!1, P!1))"
restriction_integral nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(Rie_sum const-decl "real" integral_def "analysis/")
(real_times_real_is_real application-judgement "real" reals nil)
(sub_domain formula-decl nil restriction_integral nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(R!1 skolem-const-decl
"(Riemann_sum?(a!1, b!1, P!1, restrict[T2, T1, real](f!1)))"
restriction_integral nil)
(f!1 skolem-const-decl "[T2 -> real]" restriction_integral nil)
(Riemann_sum? const-decl "bool" integral_def "analysis/"))
shostak))
(restrict_Integral_TCC1 0
(restrict_Integral_TCC1-1 nil 3432062629
("" (skosimp)
(("" (hide -1)
(("" (typepred "b!1")
(("" (lemma "sub_domain" ("x" "b!1"))
(("" (skosimp) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((sub_domain formula-decl nil restriction_integral nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers 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)
(T1_pred const-decl "[real -> boolean]" restriction_integral nil)
(T1 formal-subtype-decl nil restriction_integral nil))
nil))
(restrict_Integral_TCC2 0
(restrict_Integral_TCC2-1 nil 3432062629
("" (skosimp)
(("" (skosimp)
(("" (lemma "sub_domain" ("x" "x!1"))
(("" (skosimp) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((sub_domain formula-decl nil restriction_integral 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)
(T1_pred const-decl "[real -> boolean]" restriction_integral nil)
(T1 formal-subtype-decl nil restriction_integral nil))
nil))
(restrict_Integral_TCC3 0
(restrict_Integral_TCC3-1 nil 3432189764
("" (skosimp)
(("" (lemma "restrict_Integrable" ("a" "a!1" "b" "b!1" "f" "f!1"))
(("" (assert) nil nil)) nil))
nil)
((T2 formal-subtype-decl nil restriction_integral nil)
(T2_pred const-decl "[real -> boolean]" restriction_integral nil)
(T1 formal-subtype-decl nil restriction_integral nil)
(T1_pred const-decl "[real -> boolean]" restriction_integral 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)
(restrict_Integrable formula-decl nil restriction_integral nil))
nil))
(restrict_Integral 0
(restrict_Integral-1 nil 3432064068
(""
(case "forall a,b,f: a
integral[T2](a, b, f) =
integral[T1](a, b, restrict[T2, T1, real](f))")
(("1" (skosimp)
(("1"
(lemma "restrict_Integrable" ("a" "a!1" "b" "b!1" "f" "f!1"))
(("1" (assert)
(("1" (expand "Integrable?")
(("1" (expand "Integral")
(("1" (case-replace "a!1=b!1")
(("1" (assert)
(("1" (case-replace "a!1)
(("1" (assert)
(("1" (inst - "a!1" "b!1" "f!1")
(("1" (assert) nil nil)) nil))
nil)
("2" (assert)
(("2" (inst - "b!1" "a!1" "f!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp*)
(("2" (typepred "integral[T2](a!1, b!1, f!1)")
(("2"
(typepred
"integral[T1](a!1, b!1, restrict[T2, T1, real](f!1))")
(("1" (expand "integral?")
(("1" (name-replace "LHS" "integral[T2](a!1, b!1, f!1)")
(("1"
(name-replace "RHS"
"integral[T1](a!1, b!1, restrict[T2, T1, real](f!1))")
(("1" (typepred "abs(LHS-RHS)")
(("1" (hide -2 -3)
(("1" (expand ">=" -1)
(("1" (expand "<=" -1)
(("1" (split -1)
(("1" (name "EPS" "abs(LHS-RHS)")
(("1"
(replace -1)
(("1"
(inst - "EPS/2")
(("1"
(inst - "EPS/2")
(("1"
(skosimp*)
(("1"
(name
"DELTA"
"min(delta!1,delta!2)")
(("1"
(name
"N"
"floor((b!1-a!1)/DELTA)+2")
(("1"
(lemma
"width_eq_part[T1]"
("a"
"a!1"
"b"
"b!1"
"N"
"N"))
(("1"
(lemma
"width_eq_part[T2]"
("a"
"a!1"
"b"
"b!1"
"N"
"N"))
(("1"
(assert)
(("1"
(case
"(b!1-a!1)/(N-1))
(("1"
(case
"DELTA <= delta!1 & DELTA<=delta!2")
(("1"
(flatten)
(("1"
(inst
-
"eq_partition[T1](a!1, b!1, N)")
(("1"
(inst
-
"eq_partition[T2](a!1, b!1, N)")
(("1"
(replace
-4)
(("1"
(replace
-5)
(("1"
(assert)
(("1"
(hide
-4
-5)
(("1"
(split
-8)
(("1"
(split
-9)
(("1"
(lemma
"Riemann?_Rie[T2]"
("a"
"a!1"
"b"
"b!1"
"f"
"f!1"))
(("1"
(lemma
"Riemann?_Rie[T1]"
("a"
"a!1"
"b"
"b!1"
"f"
"restrict[T2, T1, real](f!1)"))
(("1"
(assert)
(("1"
(inst
-
"eq_partition[T1](a!1, b!1, N)"
"gen_xis[T1](a!1,b!1,eq_partition[T1](a!1, b!1, N))")
(("1"
(inst
-
"eq_partition[T1](a!1, b!1, N)"
"_")
(("1"
(case
"N>=1")
(("1"
(name
"R1"
"Rie_sum(a!1, b!1, eq_partition[T1](a!1, b!1, N),
gen_xis[T1]
(a!1, b!1, eq_partition[T1](a!1, b!1, N)),
restrict[T2, T1, real](f!1))")
(("1"
(replace
-1)
(("1"
(inst
-6
"R1")
(("1"
(inst
-4
"gen_xis[T1](a!1, b!1, eq_partition[T1](a!1, b!1, N))")
(("1"
(name
"R2"
"Rie_sum[T2](a!1, b!1, eq_partition[T1](a!1, b!1, N),
gen_xis[T1]
(a!1, b!1, eq_partition[T1](a!1, b!1, N)),
f!1)")
(("1"
(replace
-1)
(("1"
(case
"eq_partition[T1](a!1, b!1, N)=eq_partition[T2](a!1, b!1, N)")
(("1"
(inst
-7
"R2")
(("1"
(case-replace
"R1=R2")
(("1"
(hide-all-but
(-8
-9
-15))
(("1"
(grind)
nil
nil))
nil)
("2"
(hide
-3
-5
2
-17
-18
-7
-8
-9
-10
-11
-12
-13
-14
-15)
(("2"
(hide
-2
-4)
(("2"
(expand
"R1")
(("2"
(expand
"R2")
(("2"
(name-replace
"FF"
"gen_xis[T1](a!1, b!1, eq_partition[T1](a!1, b!1, N))")
(("2"
(expand
"Rie_sum")
(("2"
(expand
"finseq_appl")
(("2"
(expand
"restrict")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(expand
"eq_partition")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide
-1
-3
-4
2)
(("2"
(typepred
"gen_xis[T1](a!1, b!1, eq_partition[T1](a!1, b!1, N))")
(("2"
(expand
"xis?")
(("2"
(split)
(("1"
(skosimp)
(("1"
(expand
"finseq_appl")
(("1"
(inst
-
"x1!1")
(("1"
(flatten)
(("1"
(lemma
"parts_order_le[T1]"
("P"
"eq_partition[T1](a!1, b!1, N)"
"a"
"a!1"
"b"
"b!1"))
(("1"
(inst-cp
-
"0"
"x1!1")
(("1"
(assert)
(("1"
(hide
-1
-2
-3
-4)
(("1"
(lemma
"sub_domain"
("x"
"gen_xis[T1](a!1, b!1, eq_partition[T1](a!1, b!1, N))(x1!1)"))
(("1"
(skosimp)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(expand
"finseq_appl")
(("2"
(inst
-
"ii!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(1
-12
-8
-7
-9))
(("2"
(lemma
"posreal_div_posreal_is_posreal"
("px"
"b!1-a!1"
"py"
"DELTA"))
(("2"
(lemma
"nonneg_floor_is_nat")
(("2"
(inst
-
"(b!1 - a!1) / DELTA")
(("1"
(assert)
nil
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
-1
-2
-3
2)
(("2"
(split)
(("1"
(skosimp)
(("1"
(typepred
"eq_partition[T1](a!1, b!1, N)`seq(x1!1)")
(("1"
(assert)
(("1"
(lemma
"sub_domain"
("x"
"eq_partition[T1](a!1, b!1, N)`seq(x1!1)"))
(("1"
(skosimp)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.64 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
