| products/Sources/formale Sprachen/VDM/VDMPP/SortingPP/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: DTControl.vdmrt Sprache: LispOriginal von: PVS© |
|
||||||
|
(nn_integral
(nn_isf_TCC1 0 (nn_isf_TCC1-1 nil 3395153333 ("" (lemma "isf_zero") (("" (assert) (("" (expand "nn_isf?") (("" (propax) nil nil)) nil)) nil)) nil) ((nn_isf? const-decl "bool" nn_integral nil) (isf_zero formula-decl nil isf nil) (T formal-type-decl nil nn_integral nil) (boolean nonempty-type-decl nil booleans 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" nn_integral 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) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types 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) (m formal-const-decl "measure_type" nn_integral nil)) nil)) (increasing_nn_isf_TCC1 0 (increasing_nn_isf_TCC1-1 nil 3395150698 ("" (expand "increasing_nn_isf?") (("" (expand "pointwise_increasing?") (("" (skosimp) (("" (expand "increasing?") (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((pointwise_increasing? const-decl "bool" pointwise_convergence nil) (increasing? const-decl "bool" real_fun_preds "reals/") (increasing_nn_isf? const-decl "bool" nn_integral nil)) nil)) (nn_integrable_zero 0 (nn_integrable_zero-1 nil 3394683734 ("" (expand "nn_integrable?") (("" (inst + "lambda n: lambda x: 0") (("1" (split) (("1" (expand "pointwise_convergence?") (("1" (skosimp) (("1" (expand "convergence?") (("1" (skosimp) (("1" (inst + "0") (("1" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "convergent?") (("2" (inst + "0") (("2" (expand "o ") (("2" (expand "convergence?") (("2" (skosimp) (("2" (inst + "0") (("2" (skosimp) (("2" (lemma "isf_integral_zero") (("2" (replace -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (expand "increasing?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (lemma "isf_zero") (("3" (assert) (("3" (expand "nn_isf?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((nn_isf? const-decl "bool" nn_integral nil) (isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf nil) (m formal-const-decl "measure_type" nn_integral nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (S formal-const-decl "sigma_algebra" nn_integral nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types 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) (T formal-type-decl nil nn_integral nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (increasing_nn_isf? const-decl "bool" nn_integral nil) (sequence type-eq-decl nil sequences nil) (nn_isf nonempty-type-eq-decl nil nn_integral 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) (increasing_nn_isf nonempty-type-eq-decl nil nn_integral nil) (convergent? const-decl "bool" topological_convergence "topology/") (O const-decl "T3" function_props nil) (isf_integral_zero formula-decl nil isf nil) (pointwise_convergence? const-decl "bool" pointwise_convergence nil) (convergence? const-decl "bool" topological_convergence "topology/") (pointwise_increasing? const-decl "bool" pointwise_convergence nil) (increasing? const-decl "bool" real_fun_preds "reals/") (isf_zero formula-decl nil isf nil) (nn_integrable? const-decl "bool" nn_integral nil)) shostak)) (nn_integrable_TCC1 0 (nn_integrable_TCC1-1 nil 3390818142 ("" (rewrite "nn_integrable_zero") nil nil) ((nn_integrable_zero formula-decl nil nn_integral nil)) nil)) (nn_integrable_is_nonneg 0 (nn_integrable_is_nonneg-1 nil 3458999874 ("" (skosimp) (("" (typepred "f!1(x!1)") (("" (propax) nil nil)) nil)) nil) ((nn_integrable nonempty-type-eq-decl nil nn_integral nil) (nn_integrable? const-decl "bool" nn_integral nil) (nnreal type-eq-decl nil real_types nil) (T formal-type-decl nil nn_integral 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)) shostak)) (nn_integrable_is_measurable 0 (nn_integrable_is_measurable-1 nil 3395201393 ("" (skolem + ("f!1")) (("" (typepred "f!1") (("" (expand "nn_integrable?") (("" (skosimp) (("" (lemma "pointwise_measurable" ("u" "u!1" "f" "f!1")) (("" (assert) 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) (nnreal type-eq-decl nil real_types 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) (T formal-type-decl nil nn_integral nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (pointwise_measurable formula-decl nil measure_space 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) (measurable_function? const-decl "bool" measure_space_def nil) (measurable_function nonempty-type-eq-decl nil measure_space_def nil) (sequence type-eq-decl nil sequences 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) (m formal-const-decl "measure_type" nn_integral nil) (isf? const-decl "bool" isf 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) (increasing_nn_isf? const-decl "bool" nn_integral nil) (increasing_nn_isf nonempty-type-eq-decl nil nn_integral 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" nn_integral nil)) nil)) (nn_convergence 0 (nn_convergence-1 nil 3395566466 ("" (skosimp) (("" (name "U1" "lambda (m:nat): lambda n:min(u1!1(n),u2!1(m))") (("" (name "U2" "lambda (m:nat): lambda n:min(u2!1(n),u1!1(m))") (("" (case "forall n: pointwise_convergence?(U2(n), u1!1(n))") (("1" (case "forall n: pointwise_convergence?(U1(n), u2!1(n))") (("1" (hide -3 -4) (("1" (case "forall n: converges_upto?((isf_integral o U2(n)),isf_integral(u1!1(n)))") (("1" (case "forall n: converges_upto?((isf_integral o U1(n)),isf_integral(u2!1(n)))") (("1" (expand "convergent?" -7) (("1" (skosimp) (("1" (lemma "hausdorff_convergence.limit_def" ("v" "isf_integral o u1!1" "l" "l!1")) (("1" (assert) (("1" (replace -1) (("1" (case "convergence?(isf_integral o u2!1, l!1)") (("1" (lemma "hausdorff_convergence.limit_def" ("v" "isf_integral o u2!1" "l" "l!1")) (("1" (assert) (("1" (expand "convergent?") (("1" (inst + "l!1") nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "convergent?") (("2" (inst + "l!1") nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (hide -5 -6) (("2" (case "FORALL (i1, i2: nn_isf): (FORALL x: i1(x) <= i2(x)) IMPLIES isf_integral(i1) <= isf_integral(i2)") (("1" (inst-cp - "lambda x: 0" "_") (("1" (rewrite "isf_integral_zero") (("1" (name-replace "II" "isf_integral") (("1" (case "forall (n,m:nat): (II o U2(n))(m) <= l!1") (("1" (case "forall (n,m:nat): (II o U1(n))(m) = (II o U2(m))(n)") (("1" (case "FORALL n: II(u1!1(n)) <= l!1") (("1" (case "FORALL (n, m: nat): (II o U2(n))(m) <= II(u1!1(n))") (("1" (case "FORALL (n, m: nat): (II o U1(n))(m) <= II(u2!1(n))") (("1" (case "FORALL n: II(u2!1(n)) <= l!1") (("1" (lemma "increasing_bounded_convergence" ("v1" "II o u2!1")) (("1" (split) (("1" (expand "sup") (("1" (typepred "lub(Im(II o u2!1))") (("1" (name-replace "LIMIT" "lub(Im(II o u2!1))") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (inst - "l!1") (("1" (split -2) (("1" (expand "<=" -1) (("1" (split -1) (("1" (expand "Im" -2) (("1" (expand "upper_bound?") (("1" (hide 1) (("1" (rewrite "metric_convergence_def" *) (("1" (expand "metric_converges_to") (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "l!1-LIMIT" "py" "4")) (("1" (name-replace "RR" "(l!1 - LIMIT) / 4") (("1" (inst -17 "RR") (("1" (skosimp) (("1" (expand "ball") (("1" (expand "member") (("1" (expand "o" -17) (("1" (expand "o") (("1" (inst-cp -14 "n!1") (("1" (expand "converges_upto?" -15) (("1" (flatten) (("1" (rewrite "metric_convergence_def" *) (("1" (expand "metric_converges_to") (("1" (inst -15 "RR") (("1" (skosimp) (("1" (expand "ball") (("1" (expand "member") (("1" (hide -14 -17 -18) (("1" (inst -16 "n!1") (("1" (inst -14 "n!2") (("1" (hide -13 -15) (("1" (assert) (("1" (inst -8 "n!1") (("1" (expand "abs" -14) (("1" (assert) (("1" (inst -7 "n!1" "n!2") (("1" (expand "abs" -13) (("1" (assert) (("1" (hide -7 -8) (("1" (inst -7 "n!2" "n!1") (("1" (replace -7 * rl) (("1" (hide -7) (("1" (inst -6 "n!2" "n!1") (("1" (inst - "II(u2!1(n!2))") (("1" (expand "RR") (("1" (hide-all-but (-1 -2 -3 -10 -11 -6)) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "o") (("2" (inst + "n!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -1) (("2" (hide-all-but (-3 1)) (("2" (rewrite "metric_convergence_def" *) (("2" (expand "convergence") (("2" (expand "metric_converges_to") (("2" (skosimp) (("2" (inst - "r!1") (("2" (expand "ball") (("2" (expand "member") (("2" (skosimp) (("2" (inst + "n!1") (("2" (skosimp) (("2" (inst - "i!1") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "o" 1) (("2" (expand "Im" 1) (("2" (expand "upper_bound?" 1) (("2" (skosimp) (("2" (typepred "s!1") (("2" (skolem - ("n!1")) (("2" (replace -1) (("2" (hide -1) (("2" (inst -3 "n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -7)) (("2" (expand "increasing?") (("2" (expand "o ") (("2" (skolem + ("n!1" "m!1")) (("2" (inst - "u2!1(n!1)" "u2!1(m!1)") (("2" (flatten) (("2" (split) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "u2!1") (("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_increasing?") (("2" (inst - "x!1") (("2" (expand "increasing?") (("2" (inst - "n!1" "m!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "o" 1) (("2" (expand "bounded_above?") (("2" (inst + "l!1") nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst -8 "n!1") (("2" (expand "converges_upto?" -8) (("2" (flatten) (("2" (rewrite "metric_convergence_def" *) (("2" (expand "metric_converges_to") (("2" (expand "ball") (("2" (expand "member") (("2" (case "l!1 < II(u2!1(n!1))") (("1" (hide --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.36 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 |
