| products/sources/formale Sprachen/PVS/measure_integration/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: finite_integral.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(finite_integral
(bounded_measurable_is_integrable 0 (bounded_measurable_is_integrable-1 nil 3460348315 ("" (case "forall (h:bounded_measurable): (FORALL (x:T): 0 <= h(x))=>integrable?[T, S, to_measu (("1" (skolem + "h!1") (("1" (inst-cp - "plus(h!1)") (("1" (inst - "minus(h!1)") (("1" (split) (("1" (split) (("1" (rewrite "integrable_pm_def" 1) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "h!1") (("2" (expand "bounded_measurable?") (("2" (flatten) (("2" (expand "bounded?") (("2" (skosimp) (("2" (inst + "c!1") (("2" (skosimp) (("2" (inst - "x!1") (("2" (hide -2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "h!1") (("2" (expand "bounded_measurable?") (("2" (flatten) (("2" (hide -2 2) (("2" (expand "bounded?") (("2" (skosimp) (("2" (inst + "c!1") (("2" (skosimp) (("2" (inst - "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "h!1") (("2" (lemma "nn_integrable_is_integrable[T, S, to_measure(mu)]") (("2" (inst - "h!1") (("2" (split) (("1" (skosimp) (("1" (inst - "x1!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "bounded_measurable?") (("2" (flatten) (("2" (expand "bounded?") (("2" (skosimp) (("2" (lemma "nn_isf_is_nn_integrable[T, S, to_measure(mu)]") (("2" (inst - "*[T](c!1,phi[T,S](fullset[T]))") (("1" (flatten) (("1" (lemma "nn_integrable_le[T, S, to_measure(mu)]" ("f" "*[T](c!1, phi[T, S](fullset[T]))" "g" "h!1")) (("1" (assert) (("1" (skosimp) (("1" (inst -3 "x!1") (("1" (inst -5 "x!1") (("1" (hide-all-but (-3 -5 1)) (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (expand "nn_isf?") (("2" (split) (("1" (expand "isf?") (("1" (expand "mu_fin?") (("1" (expand "to_measure") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "*") (("2" (expand "phi") (("2" (lift-if 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nn_integrable nonempty-type-eq-decl nil nn_integral nil) (nn_integrable? const-decl "bool" nn_integral nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (h!1 skolem-const-decl "bounded_measurable" finite_integral nil) (subset_algebra_fullset name-judgement "(S)" finite_integral nil) (measurable_fullset name-judgement "measurable_set[T, S]" finite_integral nil) (phi_is_simple application-judgement "simple" finite_integral nil) (simple_scal application-judgement "simple" finite_integral nil) (bounded_scal application-judgement "bounded[T]" finite_integral nil) (isf? const-decl "bool" isf nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (c!1 skolem-const-decl "nnreal" finite_integral nil) (set type-eq-decl nil sets 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) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (phi const-decl "nat" measure_space nil) (fullset const-decl "set" sets nil) (isf nonempty-type-eq-decl nil isf nil) (nn_isf? const-decl "bool" nn_integral nil) (nn_isf nonempty-type-eq-decl nil nn_integral nil) (nn_integrable_le formula-decl nil nn_integral nil) (measurable_function? const-decl "bool" measure_space_def nil) (measurable_function nonempty-type-eq-decl nil measure_space_def nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (member const-decl "bool" sets nil) (mu_fin? const-decl "bool" measure_props nil) (nn_isf_is_nn_integrable judgement-tcc nil nn_integral nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nn_integrable_is_integrable judgement-tcc nil integral nil) (minus_measurable application-judgement "measurable_function[T, S]" finite_integral nil) (minus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (integrable_pm_def formula-decl nil integral nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (real_minus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (bounded? const-decl "bool" sup_norm nil) (h!1 skolem-const-decl "bounded_measurable" finite_integral nil) (plus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/") (plus_measurable application-judgement "measurable_function[T, S]" finite_integral nil) (T formal-type-decl nil finite_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) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (S formal-const-decl "sigma_algebra" finite_integral nil) (bounded_measurable? const-decl "bool" measure_space nil) (bounded_measurable nonempty-type-eq-decl nil measure_space nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (finite_measure? const-decl "bool" generalized_measure_def nil) (finite_measure nonempty-type-eq-decl nil generalized_measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (to_measure const-decl "measure_type" generalized_measure_def nil) (mu formal-const-decl "finite_measure" finite_integral nil) (integrable? const-decl "bool" integral nil)) nil))) ¤ Dauer der Verarbeitung: 0.6 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 |
