| products/sources/formale Sprachen/PVS/lebesgue/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: interval_bandb.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(lebesgue_fundamental
(IMP_fundamental_theorem_TCC1 0 (IMP_fundamental_theorem_TCC1-1 nil 3452514920 ("" (assert) nil nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (IMP_fundamental_theorem_TCC2 0 (IMP_fundamental_theorem_TCC2-1 nil 3452514920 ("" (expand "connected?") (("" (skosimp*) (("" (typepred "x!1") (("" (typepred "y!1") (("" (expand "closed") (("" (expand "closed_ball") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals 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) (<= const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (closed? const-decl "bool" topology "topology/") (closed nonempty-type-eq-decl nil topology "topology/") (closed_ball const-decl "closed" real_topology "metric_space/") (closed_interval nonempty-type-eq-decl nil real_topology "metric_space/") (closed const-decl "closed_interval" real_topology "metric_space/") (a formal-const-decl "real" lebesgue_fundamental nil) (< const-decl "bool" reals nil) (b formal-const-decl "{x: real | a < x}" lebesgue_fundamental nil) (connected? const-decl "bool" deriv_domain_def "analysis/")) nil)) (IMP_fundamental_theorem_TCC3 0 (IMP_fundamental_theorem_TCC3-1 nil 3452514920 ("" (expand "not_one_element?") (("" (skosimp) (("" (typepred "x!1") (("" (case "x!1=a") (("1" (inst + "b") (("1" (assert) nil nil) ("2" (hide -2) (("2" (grind) nil nil)) nil)) nil) ("2" (inst + "a") (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (closed_is_measurable application-judgement "measurable_set" lebesgue_def nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals 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) (<= const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (closed? const-decl "bool" topology "topology/") (closed nonempty-type-eq-decl nil topology "topology/") (closed_ball const-decl "closed" real_topology "metric_space/") (closed_interval nonempty-type-eq-decl nil real_topology "metric_space/") (closed const-decl "closed_interval" real_topology "metric_space/") (a formal-const-decl "real" lebesgue_fundamental nil) (< const-decl "bool" reals nil) (b formal-const-decl "{x: real | a < x}" lebesgue_fundamental nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/")) nil)) (IMP_fundamental_theorem_TCC4 0 (IMP_fundamental_theorem_TCC4-1 nil 3452518094 ("" (inst + "a") (("" (grind) nil nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (b formal-const-decl "{x: real | a < x}" lebesgue_fundamental nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" lebesgue_fundamental nil) (closed const-decl "closed_interval" real_topology "metric_space/") (closed_interval nonempty-type-eq-decl nil real_topology "metric_space/") (closed_ball const-decl "closed" real_topology "metric_space/") (closed nonempty-type-eq-decl nil topology "topology/") (closed? const-decl "bool" topology "topology/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (<= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (closed_is_measurable application-judgement "measurable_set" lebesgue_def nil)) nil)) (IMP_restriction_integral_TCC1 0 (IMP_restriction_integral_TCC1-1 nil 3452523885 ("" (skosimp*) (("" (typepred "x!1") (("" (typepred "y!1") (("" (grind) nil nil)) nil)) nil)) nil) ((b formal-const-decl "{x: real | a < x}" lebesgue_fundamental nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" lebesgue_fundamental nil) (closed const-decl "closed_interval" real_topology "metric_space/") (closed_interval nonempty-type-eq-decl nil real_topology "metric_space/") (closed_ball const-decl "closed" real_topology "metric_space/") (closed nonempty-type-eq-decl nil topology "topology/") (closed? const-decl "bool" topology "topology/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (<= const-decl "bool" 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) (number nonempty-type-decl nil numbers nil) (real nonempty-type-from-decl nil reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (closed_is_measurable application-judgement "measurable_set" lebesgue_def nil) (minus_real_is_real application-judgement "real" reals nil)) nil)) (IMP_restriction_integral_TCC2 0 (IMP_restriction_integral_TCC2-1 nil 3452523885 ("" (skosimp) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil)) nil) nil nil)) (IMP_restriction_integral_TCC3 0 (IMP_restriction_integral_TCC3-2 nil 3477731956 ("" (skosimp) (("" (typepred "x!1") (("" (case "x!1=a") (("1" (inst + "b") (("1" (assert) nil nil) ("2" (hide -2) (("2" (grind) nil nil)) nil)) nil) ("2" (inst + "a") (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((b formal-const-decl "{x: real | a < x}" lebesgue_fundamental nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" lebesgue_fundamental nil) (closed const-decl "closed_interval" real_topology "metric_space/") (closed_interval nonempty-type-eq-decl nil real_topology "metric_space/") (closed_ball const-decl "closed" real_topology "metric_space/") (closed nonempty-type-eq-decl nil topology "topology/") (closed? const-decl "bool" topology "topology/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (<= const-decl "bool" 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) (number nonempty-type-decl nil numbers nil) (real nonempty-type-from-decl nil reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (closed_is_measurable application-judgement "measurable_set" lebesgue_def nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil)) nil) (IMP_restriction_integral_TCC3-1 nil 3452523885 ("" (skosimp) (("" (inst + "x!1") nil nil)) nil) ((set type-eq-decl nil sets nil) (setofsets type-eq-decl nil sets nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (closed? const-decl "bool" topology "topology/") (closed nonempty-type-eq-decl nil topology "topology/") (closed_ball const-decl "closed" real_topology "metric_space/") (closed_interval nonempty-type-eq-decl nil real_topology "metric_space/") (closed const-decl "closed_interval" real_topology "metric_space/")) nil)) (IMP_restriction_integral_TCC4 0 (IMP_restriction_integral_TCC4-1 nil 3477673281 ("" (skosimp*) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)) nil)) (IMP_restriction_integral_TCC5 0 (IMP_restriction_integral_TCC5-2 nil 3477731995 ("" (skosimp*) (("" (typepred "x!1") (("" (inst + "x!1") nil nil)) nil)) nil) ((b formal-const-decl "{x: real | a < x}" lebesgue_fundamental nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" lebesgue_fundamental nil) (closed const-decl "closed_interval" real_topology "metric_space/") (closed_interval nonempty-type-eq-decl nil real_topology "metric_space/") (closed_ball const-decl "closed" real_topology "metric_space/") (closed nonempty-type-eq-decl nil topology "topology/") (closed? const-decl "bool" topology "topology/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (<= const-decl "bool" 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) (number nonempty-type-decl nil numbers nil) (real nonempty-type-from-decl nil reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil) (IMP_restriction_integral_TCC5-1 nil 3477673281 ("" (assuming-tcc) nil nil) nil nil)) (F_TCC1 0 (F_TCC1-1 nil 3603447121 ("" (lemma "deriv_domain") (("" (propax) nil nil)) nil) ((deriv_domain formula-decl nil fundamental_theorem "analysis/") (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) (bool nonempty-type-eq-decl nil booleans nil) (<= const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (closed? const-decl "bool" topology "topology/") (closed nonempty-type-eq-decl nil topology "topology/") (closed_ball const-decl "closed" real_topology "metric_space/") (closed_interval nonempty-type-eq-decl nil real_topology "metric_space/") (closed const-decl "closed_interval" real_topology "metric_space/") (a formal-const-decl "real" lebesgue_fundamental nil) (< const-decl "bool" reals nil) (b formal-const-decl "{x: real | a < x}" lebesgue_fundamental nil)) nil)) (fundamental_lebesgue_TCC1 0 (fundamental_lebesgue_TCC1-1 nil 3452514920 ("" (skosimp) (("" (hide -1 -2) (("" (grind) nil nil)) nil)) nil) ((minus_real_is_real application-judgement "real" reals nil) (closed_ball const-decl "closed" real_topology "metric_space/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (closed const-decl "closed_interval" real_topology "metric_space/") (closed_is_measurable application-judgement "measurable_set" lebesgue_def nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (fundamental_lebesgue_TCC2 0 (fundamental_lebesgue_TCC2-1 nil 3452514920 ("" (skosimp) (("" (hide -1 -2) (("" (grind) nil nil)) nil)) nil) ((closed_ball const-decl "closed" real_topology "metric_space/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (closed const-decl "closed_interval" real_topology "metric_space/") (closed_is_measurable application-judgement "measurable_set" lebesgue_def nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (fundamental_lebesgue 0 (fundamental_lebesgue-1 nil 3452515121 ("" (skosimp*) (("" (typepred "F!1") (("" (typepred "f!1") (("" (lemma "continuous_at_is_ae_continuous" ("a" "a" "b" "b" "f" "f!1")) (("" (lemma "bounded_ae_continuous_integrable" ("a" "a" "b" "b" "f" "f!1")) (("" (lemma "continuous_at_is_bounded" ("a" "a" "b" "b" "f" "f!1")) (("" (assert) (("" (assert) (("" (case-replace "(FORALL x: a <= x AND x <= b => continuous_at?(f!1, x))") (("1" (split -4) (("1" (assert) (("1" (hide -5) (("1" (lemma "riemann_integrable_def" ("a" "a" "b" "b" "f" "f!1")) (("1" (assert) (("1" (lemma "fundamental3" ("F" "F!1" "f" "f!1" "a" "a" "b" "b")) (("1" (replace -8) (("1" (replace -7) (("1" (split -1) (("1" (flatten) (("1" (assert) (("1" (hide -1 -2) (("1" (expand "restrict") (("1" (lemma "riemann_lebesgue_integral" ("a" "a" "b" "b" "f" "f!1")) (("1" (assert) (("1" (replace -1 1 rl) (("1" (case-replace "(LAMBDA (s_1: real): f!1(s_1)) = f!1") (("1" (lemma "fundamental3[(closed(a, b))]" ("a" "a" "b" "b" "F" "F!1" "f" "LAMBDA (s_1:(closed(a, b))): f!1(s_1)")) (("1" (replace -10) (("1" (replace -9) (("1" (split) (("1" (flatten) (("1" (lemma "restrict_Integral") (("1" (inst - "a" "b" "f!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -5)) (("2" (expand "continuous?") (("2" (skosimp) (("2" (inst - "x0!1") (("2" (typepred "x0!1") (("2" (split) (("1" (rewrite "metric_continuous_at_def") (("1" (expand "continuous?") (("1" (expand "metric_continuous_at?") (("1" (skosimp) (("1" (inst - "epsilon!1") (("1" (skosimp) (("1" (inst + "delta!1") (("1" (skosimp) (("1" (typepred "x!1") (("1" (inst - "x!1") (("1" (split) (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (expand "restrict") (("2" (assert) (("2" (expand "continuous?") (("2" (skosimp) (("2" (inst - "x0!1") (("2" (typepred "x0!1") (("2" (split -2) (("1" (rewrite "metric_continuous_at_def") (("1" (expand "continuous?") (("1" (expand "metric_continuous_at?") (("1" (skosimp) (("1" (inst - "epsilon!1") (("1" (skosimp) (("1" (inst + "delta!1") (("1" (skosimp) (("1" (inst - "x!1") (("1" (split) (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (skosimp) (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 1)) (("2" (expand "continuous_on?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((deriv_fun type-eq-decl nil derivatives "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (b formal-const-decl "{x: real | a < x}" lebesgue_fundamental nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" lebesgue_fundamental nil) (closed const-decl "closed_interval" real_topology "metric_space/") (closed_interval nonempty-type-eq-decl nil real_topology "metric_space/") (closed_ball const-decl "closed" real_topology "metric_space/") (closed nonempty-type-eq-decl nil topology "topology/") (closed? const-decl "bool" topology "topology/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (<= const-decl "bool" reals 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (continuous_at_is_ae_continuous formula-decl nil ae_continuous_def nil) (continuous_at_is_bounded formula-decl nil riemann_link nil) (x!1 skolem-const-decl "real" lebesgue_fundamental nil) (real_minus_real_is_real application-judgement "real" reals nil) (restrict_Integral formula-decl nil restriction_integral nil) (continuous? const-decl "bool" continuous_functions "analysis/") (continuous? const-decl "bool" continuous_functions "analysis/") (minus_real_is_real application-judgement "real" reals nil) (member const-decl "bool" sets nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (ball_is_metric_open application-judgement "metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" convergence_aux "metric_space/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (metric_continuous_at? const-decl "bool" metric_continuity "metric_space/") (metric_continuous_at_def formula-decl nil metric_continuity "metric_space/") (real_div_nzreal_is_real application-judgement "real" reals nil) (riemann_lebesgue_integral formula-decl nil riemann_link nil) (restrict const-decl "R" restrict nil) (fundamental3 formula-decl nil fundamental_theorem "analysis/") (riemann_integrable_def formula-decl nil riemann_link nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (continuous_at? const-decl "bool" continuity_def "topology/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (closed_is_measurable application-judgement "measurable_set" lebesgue_def nil) (bounded_ae_continuous_integrable formula-decl nil riemann_link nil) (continuous_on? const-decl "bool" continuous_on nil) (continuous_on type-eq-decl nil continuous_on nil)) shostak)) (integration_by_parts_TCC1 0 (integration_by_parts_TCC1-1 nil 3476038809 ("" (skosimp) (("" (hide-all-but 1) (("" (grind) nil nil)) nil)) nil) ((minus_real_is_real application-judgement "real" reals nil) (closed_ball const-decl "closed" real_topology "metric_space/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (closed const-decl "closed_interval" real_topology "metric_space/") (closed_is_measurable application-judgement "measurable_set" lebesgue_def nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (integration_by_parts_TCC2 0 (integration_by_parts_TCC2-1 nil 3476038809 ("" (skosimp) (("" (hide-all-but 1) (("" (grind) nil nil)) nil)) nil) ((closed_ball const-decl "closed" real_topology "metric_space/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (closed const-decl "closed_interval" real_topology "metric_space/") (closed_is_measurable application-judgement "measurable_set" lebesgue_def nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (integration_by_parts 0 (integration_by_parts-1 nil 3476040864 ("" (skosimp) (("" (name "H" "real_fun_ops.*(F!1,G!1)") (("1" (lemma "prod_derivable_fun" ("f1" "F!1" "f2" "G!1")) (("1" (split) (("1" (lemma "deriv_prod_fun" ("ff1" "F!1" "ff2" "G!1")) (("1" (lemma "fundamental_lebesgue" ("F" "H")) (("1" (replace -4) (("1" (replace -2) (("1" (replace -5) (("1" (replace -6) (("1" (hide -4 -5 -6) (("1" (hide -3 -2) (("1" (expand "H" -) (("1" (expand "*" - 3) (("1" (expand "*" - 4) (("1" (expand "restrict" -) (("1" (expand "*" - 1) (("1" (expand "+" - 1) (("1" (assert) (("1" (expand "*" - 1) (("1" (typepred "f!1") (("1" (typepred "g!1") (("1" (lemma "derivable_cont_fun[(closed(a, b))]") (("1" (inst-cp - "F!1") (("1" (inst - "G!1") (("1" (assert) (("1" (name "CE" "lambda (f:[real->real]): lambda x: if x) (("1" (hide -1) (("1" (case "FORALL (f:[real->real]): (forall x: closed(a,b)(x) => continuous_at?(f,x)) => c (("1" (case "FORALL (f:[real->real],x): closed(a, b)(x) => CE(f)(x) = f(x)") (("1" (name-replace "FF" "extend[real, (closed(a, b)), real, 0](F!1)") (("1" (name-replace "GG" "extend[real, (closed(a, b)), real, 0](G!1)") (("1" (inst-cp - "f!1") (("1" (inst-cp - "g!1") (("1" (split) (("1" (split) (("1" (inst-cp - "g!1" "_") (("1" (inst-cp - "f!1" "_") (("1" (hide -6) (("1" (case "continuity_def.continuous?(CE(GG)*CE(f!1))") (("1" (case "continuity_def.continuous?(CE(FF)*CE(g!1))") (("1" (case "continuity_def.continuous?((CE(FF)*CE(g!1)) + (CE(GG)*CE(f!1)))") (("1" (inst -13 "(CE(FF) * CE(g!1)) + (CE(GG) * CE(f!1))") (("1" (split -13) (("1" (flatten) (("1" (lemma "continuous_is_integrable" ("a" "a" "b" "b" "f" "CE(GG) * CE(f!1)")) (("1" (lemma "continuous_is_integrable" ("a" "a" "b" "b" "f" "CE(FF) * CE(g!1)")) (("1" (assert) (("1" (rewrite "indefinite_add" -4) (("1" (expand "integral" (1 -4)) (("1" (expand "integrable?" (1 -1 -2)) (("1" (expand "*") (("1" (hide-all-but (-1 -2 -3 -4 1)) (("1" (expand "phi") (("1" (expand "member") (("1" (case-replace "(LAMBDA (x_1: real): IF closed(a, b)(x_1) THEN 1 ELSE 0 ENDIF * (CE(FF)(x_1) * CE(g!1)(x_1)))=(LAMBDA (x_1: real): IF closed(a, b)(x_1) THEN 1 ELSE 0 ENDIF * (FF(x_1) * g!1(x_1)))") (("1" (replace -2) (("1" (hide -1) (("1" (case-replace "(LAMBDA (x_1: real): IF closed(a, b)(x_1) THEN 1 ELSE 0 ENDIF * (CE(GG)(x_1) * CE(f!1)(x_1)))=(LAMBDA (x_1: real): IF closed(a, b)(x_1) THEN 1 ELSE 0 ENDIF * (GG(x_1) * f!1(x_1)))") (("1" (hide -1) (("1" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.71 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.Bot Zugriff |
