| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/lebesgue/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 88 kB |
|
SSL restriction_integral.prfInteraktion undPortierbarkeitLisp |
|||||||||||||||
|
(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<b=> (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<b!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<b&integrable?[T2](a, b, f) & integrable?[T1](a,b,restrict[T2,T1,real](f))=> 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<b!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)<DELTA") (("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 "eq_partition[T1](a!1, b!1, N)") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "not_one_element_T1") (("2" (hide-all-but (1 -12 -8 -9)) (("2" (lemma "posreal_div_posreal_is_posreal" ("px" "b!1-a!1" "py" "DELTA")) (("2" (lemma "nonneg_floor_is_nat" ("x" "(b!1 - a!1) / DELTA")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-5 1)) (("2" (grind) nil nil)) nil)) nil) ("2" (hide-all-but (-3 -4 -9 1)) (("2" (lemma "posreal_div_posreal_is_posreal" ("px" "b!1-a!1" "py" "DELTA")) (("2" (typepred "floor((b!1 - a!1) / DELTA)") (("2" (rewrite "div_mult_pos_lt1" 1) (("2" (rewrite "div_mult_pos_lt1" -2) (("2" (rewrite "div_mult_pos_le2" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "floor((b!1 - a!1) / DELTA)") (("2" (lemma "posreal_div_posreal_is_posreal" ("px" "b!1-a!1" "py" "DELTA")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "abs") (("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "not_one_element_T1") (("2" (skosimp) (("2" (lemma "sub_domain" ("x" "x!1")) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (lemma "not_one_element_T1") (("3" (skosimp) (("3" (lemma "sub_domain" ("x" "x!1")) (("3" (skolem!) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (lemma "connected_domain_T1") (("4" (lemma "sub_domain" ("x" "b!1")) (("4" (skolem!) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("5" (skosimp) (("5" (hide-all-but 1) (("5" (lemma "sub_domain" ("x" "a!1")) (("5" (skosimp) (("5" (assert) nil nil)) nil)) nil)) nil)) nil) ("6" (skosimp) (("6" (lemma "sub_domain" ("x" "b!1")) (("6" (skosimp) (("6" (assert) (("6" (skosimp*) (("6" (lemma "sub_domain" ("x" "x!1")) (("6" (skolem!) (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("7" (skosimp) (("7" (lemma "sub_domain" ("x" "a!1")) (("7" (skosimp) (("7" (assert) (("7" (lemma "sub_domain" ("x" "b!1")) (("7" (skolem!) (("7" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("8" (skosimp) (("8" (lemma "not_one_element_T1") (("8" (lemma "sub_domain" ("x" "a!1")) (("8" (skolem!) (("8" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((connected_domain_T1 formula-decl nil restriction_integral nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_minus_real_is_real application-judgement "real" reals nil) (<= const-decl "bool" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (> const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (a!1 skolem-const-decl "T1" restriction_integral nil) (b!1 skolem-const-decl "T1" restriction_integral nil) (f!1 skolem-const-decl "[T2 -> real]" restriction_integral nil) (LHS skolem-const-decl "{S: real | integral?(a!1, b!1, f!1, S)}" restriction_integral nil) (RHS skolem-const-decl "{S: real | integral?(a!1, b!1, restrict[T2, T1, real](f!1), S)}" restriction_integral nil) (EPS skolem-const-decl "{n: nonneg_real | n >= LHS - RHS AND n >= -(LHS - RHS)}" restriction_integral nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (integer nonempty-type-from-decl nil integers nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (int nonempty-type-eq-decl nil integers nil) (N skolem-const-decl "int" restriction_integral nil) (gen_xis const-decl "(xis?(a, b, P))" integral_def "analysis/") (xis? const-decl "bool" integral_def "analysis/") (R2 skolem-const-decl "real" restriction_integral nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sub_domain formula-decl nil restriction_integral nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (parts_order_le formula-decl nil integral_def "analysis/") (R1 skolem-const-decl "real" restriction_integral nil) (Riemann_sum? const-decl "bool" integral_def "analysis/") (Rie_sum const-decl "real" integral_def "analysis/") (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (delta!1 skolem-const-decl "posreal" restriction_integral nil) (delta!2 skolem-const-decl "posreal" restriction_integral nil) (DELTA skolem-const-decl "{z: posreal | z <= delta!1 AND z <= delta!2}" restriction_integral nil) (nonneg_floor_is_nat judgement-tcc nil floor_ceil nil) (not_one_element_T1 formula-decl nil restriction_integral nil) (Riemann?_Rie formula-decl nil integral_def "analysis/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil naturalnumbers nil) (partition type-eq-decl nil integral_def "analysis/") (eq_partition const-decl "partition(a, b)" integral_def "analysis/") (div_mult_pos_lt1 formula-decl nil real_props nil) (div_mult_pos_le2 formula-decl nil real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (above nonempty-type-eq-decl nil integers nil) (width_eq_part formula-decl nil integral_def "analysis/") (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (posreal_min application-judgement "{z: posreal | z <= x AND z <= y}" real_defs nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (Integral const-decl "real" integral_def "analysis/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (Integrable? const-decl "bool" integral_def "analysis/") (restrict_Integrable 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) (T2_pred const-decl "[real -> boolean]" restriction_integral nil) (T2 formal-subtype-decl nil restriction_integral nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (integrable? const-decl "bool" integral_def "analysis/") (restrict const-decl "R" restrict nil) (= const-decl "[T, T -> boolean]" equalities nil) (integral? const-decl "bool" integral_def "analysis/") (integral const-decl "{S: real | integral?(a, b, ff, S)}" integral_def "analysis/")) shostak)) (extend_Integrable 0 (extend_Integrable-1 nil 3432190262 ("" (auto-rewrite "xis_lem") (("" (skosimp) (("" (lemma "restrict_Integrable" ("a" "a!1" "b" "b!1" "f" "extend[T2, T1, real, c!1](g!1)")) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "restrict[T2, T1, real](extend[T2, T1, real, c!1](g!1))=g!1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("1" (expand "extend") (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp) (("2" (lemma "sub_domain" ("x" "x!1")) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (lemma "sub_domain" ("x" "x!1")) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((= const-decl "[T, T -> boolean]" equalities nil) (restrict const-decl "R" restrict nil) (sub_domain formula-decl nil restriction_integral nil) (restrict_Integrable 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) (T2_pred const-decl "[real -> boolean]" restriction_integral nil) (T2 formal-subtype-decl nil restriction_integral nil) (extend const-decl "R" extend nil)) shostak)) (extend_Integral_TCC1 0 (extend_Integral_TCC1-1 nil 3432189764 ("" (skosimp) (("" (lemma "sub_domain" ("x" "b!1")) (("" (skosimp) (("" (assert) 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)) (extend_Integral_TCC2 0 (extend_Integral_TCC2-1 nil 3432189764 ("" (skosimp*) (("" (lemma "sub_domain" ("x" "x!1")) (("" (skosimp) (("" (assert) 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)) (extend_Integral_TCC3 0 (extend_Integral_TCC3-1 nil 3432189764 ("" (skosimp) (("" (lemma "extend_Integrable" ("a" "a!1" "b" "b!1" "g" "g!1" "c" "c!1")) (("" (assert) 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) (extend_Integrable formula-decl nil restriction_integral nil)) nil)) (extend_Integral 0 (extend_Integral-1 nil 3432190639 ("" (skosimp) (("" (lemma "extend_Integrable" ("a" "a!1" "b" "b!1" "c" "c!1" "g" "g!1")) (("" (assert) (("" (lemma "restrict_Integral" ("a" "a!1" "b" "b!1" "f" "extend[T2, T1, real, c!1](g!1)")) (("1" (assert) (("1" (case-replace "restrict[T2, T1, real](extend[T2, T1, real, c!1](g!1))=g!1") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("1" (grind) nil nil) ("2" (skosimp) (("2" (lemma "sub_domain" ("x" "x!1")) (("2" (skolem!) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (lemma "sub_domain" ("x" "x!1")) (("2" (skolem!) (("2" (assert) nil nil)) nil)) 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) (extend_Integrable formula-decl nil restriction_integral nil) (extend const-decl "R" extend nil) (T2 formal-subtype-decl nil restriction_integral nil) (T2_pred const-decl "[real -> boolean]" restriction_integral nil) (restrict_Integral formula-decl nil restriction_integral nil) (= const-decl "[T, T -> boolean]" equalities nil) (restrict const-decl "R" restrict nil) (sub_domain formula-decl nil restriction_integral nil)) shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.52Angebot (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-26) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26