products/sources/formale sprachen/PVS/complex_integration/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: cal_L_inf.prf   Sprache: Lisp

Original von: PVS©
(cal_L_inf
 (mu_TCC1 0
  (mu_TCC1-1 nil 3477288112
   ("" (typepred "S")
    (("" (expand "sigma_algebra?")
      (("" (flatten)
        (("" (expand "subset_algebra_empty?") (("" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((subset_algebra_empty? const-decl "bool" subset_algebra_def
     "measure_integration/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set[T]" countable_setofsets
     "sets_aux/")
    (member const-decl "bool" sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil cal_L_inf nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def
     "measure_integration/")
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
     "measure_integration/")
    (S formal-const-decl "sigma_algebra[T]" cal_L_inf nil))
   nil))
 (cal_L_infty_TCC1 0
  (cal_L_infty_TCC1-1 nil 3477289127
   ("" (expand "cal_L_infty?")
    (("" (expand "essentially_bounded?")
      (("" (rewrite "const_measurable")
        (("" (expand "ae_bounded?")
          (("" (inst + "0")
            (("" (expand "abs")
              (("" (expand "abs")
                (("" (expand "sq_abs")
                  (("" (assert)
                    (("" (expand "ae_le?")
                      (("" (expand "pointwise_ae?")
                        (("" (expand "ae?")
                          (("" (expand "ae_in?")
                            (("" (inst + "emptyset[T]")
                              ((""
                                (skosimp)
                                (("" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((essentially_bounded? const-decl "bool" essentially_bounded nil)
    (ae_bounded? const-decl "bool" complex_measure_theory nil)
    (abs const-decl "[T -> nonneg_real]" complex_fun_ops
         "complex_alt/")
    (sq_abs const-decl "nnreal" complex_types "complex_alt/")
    (ae_le? const-decl "bool" measure_theory "measure_integration/")
    (subset_algebra_fullset name-judgement "(S)" cal_L_inf nil)
    (measurable_fullset name-judgement "measurable_set[T, S]" cal_L_inf
     nil)
    (ae? const-decl "bool" measure_theory "measure_integration/")
    (null_emptyset name-judgement "null_set[T, S, mu]" cal_L_inf nil)
    (subset_algebra_emptyset name-judgement "(S)" cal_L_inf nil)
    (finite_emptyset name-judgement "finite_set[T]" sigma_countable
     "sigma_set/")
    (finite_emptyset name-judgement "finite_set[T]" countable_setofsets
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (emptyset const-decl "set" sets nil)
    (negligible nonempty-type-eq-decl nil measure_theory
     "measure_integration/")
    (negligible_set? const-decl "bool" measure_theory
     "measure_integration/")
    (mu formal-const-decl "measure_type[T, S]" cal_L_inf nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     "measure_integration/")
    (measure? const-decl "bool" generalized_measure_def
     "measure_integration/")
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (set type-eq-decl nil sets nil) (member const-decl "bool" sets nil)
    (ae_in? const-decl "bool" measure_theory "measure_integration/")
    (pointwise_ae? const-decl "bool" measure_theory
     "measure_integration/")
    (sqrt_0 formula-decl nil sqrt "reals/")
    (Re_rew formula-decl nil complex_types "complex_alt/")
    (sq_0 formula-decl nil sq "reals/")
    (Im_rew formula-decl nil complex_types "complex_alt/")
    (abs const-decl "nnreal" polar "complex_alt/")
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (S formal-const-decl "sigma_algebra[T]" cal_L_inf nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
     "measure_integration/")
    (sigma_algebra? const-decl "bool" subset_algebra_def
     "measure_integration/")
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil cal_L_inf nil)
    (complex_ adt-constructor-decl "[[real, real] -> (complex_?)]"
     complex_types "complex_alt/")
    (complex_? adt-recognizer-decl "[complex -> boolean]" complex_types
     "complex_alt/")
    (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)
    (complex type-decl nil complex_types "complex_alt/")
    (const_measurable formula-decl nil complex_measurable nil)
    (cal_L_infty? const-decl "bool" cal_L_inf nil))
   nil))
 (cal_L_infty_is_essentially_bounded 0
  (cal_L_infty_is_essentially_bounded-1 nil 3477386334
   ("" (judgement-tcc) nil nil)
   ((cal_L_infty nonempty-type-eq-decl nil cal_L_inf nil)
    (cal_L_infty? const-decl "bool" cal_L_inf nil)
    (complex type-decl nil complex_types "complex_alt/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (measurable_set? const-decl "bool" measure_space_def
     "measure_integration/")
    (measurable_function? const-decl "bool" measure_space_def
     "measure_integration/")
    (complex_measurable? const-decl "bool" complex_measurable nil)
    (Re const-decl "real" complex_types "complex_alt/")
    (sq const-decl "nonneg_real" sq "reals/")
    (Im const-decl "real" complex_types "complex_alt/")
    (sq_abs const-decl "nnreal" complex_types "complex_alt/")
    (abs const-decl "nnreal" polar "complex_alt/")
    (abs const-decl "[T -> nonneg_real]" complex_fun_ops
         "complex_alt/")
    (member const-decl "bool" sets nil)
    (ae_in? const-decl "bool" measure_theory "measure_integration/")
    (ae? const-decl "bool" measure_theory "measure_integration/")
    (pointwise_ae? const-decl "bool" measure_theory
     "measure_integration/")
    (ae_le? const-decl "bool" measure_theory "measure_integration/")
    (ae_bounded? const-decl "bool" complex_measure_theory nil)
    (mu formal-const-decl "measure_type[T, S]" cal_L_inf nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     "measure_integration/")
    (measure? const-decl "bool" generalized_measure_def
     "measure_integration/")
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (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)
    (S formal-const-decl "sigma_algebra[T]" cal_L_inf nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
     "measure_integration/")
    (sigma_algebra? const-decl "bool" subset_algebra_def
     "measure_integration/")
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil cal_L_inf nil)
    (essentially_bounded? const-decl "bool" essentially_bounded nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (subset_algebra_fullset name-judgement "(S)" cal_L_inf nil)
    (measurable_fullset name-judgement "measurable_set[T, S]" cal_L_inf
     nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
 (scal_cal_L_infty 0
  (scal_cal_L_infty-1 nil 3477289127
   ("" (skosimp)
    (("" (typepred "f!1")
      (("" (expand "cal_L_infty?")
        (("" (expand "essentially_bounded?")
          (("" (flatten)
            (("" (rewrite "scal_complex_measurable")
              (("" (hide -1)
                (("" (expand "ae_bounded?")
                  (("" (skosimp)
                    (("" (inst + "abs(c!1)*K!1")
                      (("" (expand "ae_le?")
                        (("" (expand "pointwise_ae?")
                          (("" (expand "ae?")
                            (("" (expand "fullset")
                              ((""
                                (expand "ae_in?")
                                ((""
                                  (skosimp)
                                  ((""
                                    (inst + "E!1")
                                    ((""
                                      (assert)
                                      ((""
                                        (skosimp)
                                        ((""
                                          (inst - "x!1")
                                          ((""
                                            (assert)
                                            ((""
                                              (expand "abs" 2 1)
                                              ((""
                                                (expand "abs" -1 1)
                                                ((""
                                                  (expand "*" 2)
                                                  ((""
                                                    (hide 1)
                                                    ((""
                                                      (rewrite
                                                       "abs_mult")
                                                      ((""
                                                        (typepred
                                                         "abs(c!1)")
                                                        ((""
                                                          (expand
                                                           ">="
                                                           -1)
                                                          ((""
                                                            (expand
                                                             "<="
                                                             -1)
                                                            ((""
                                                              (split)
                                                              (("1"
                                                                (lemma
                                                                 "both_sides_times_pos_le2"
                                                                 ("pz"
                                                                  "abs(c!1)"
                                                                  "x"
                                                                  "abs(f!1(x!1))"
                                                                  "y"
                                                                  "K!1"))
                                                                (("1"
                                                                  (assert)
                                                                  nil
                                                                  nil)
                                                                 ("2"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (replace
                                                                 -1
                                                                 *
                                                                 rl)
                                                                (("2"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cal_L_infty nonempty-type-eq-decl nil cal_L_inf nil)
    (cal_L_infty? const-decl "bool" cal_L_inf nil)
    (complex type-decl nil complex_types "complex_alt/")
    (T formal-type-decl nil cal_L_inf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (scal_essentially_bounded application-judgement
     "essentially_bounded" cal_L_inf nil))
   nil))
 (add_cal_L_infty 0
  (add_cal_L_infty-1 nil 3477289127
   ("" (skosimp)
    (("" (typepred "f1!1")
      (("" (typepred "f0!1")
        (("" (expand "cal_L_infty?")
          (("" (expand "essentially_bounded?")
            (("" (flatten)
              (("" (rewrite "sum_complex_measurable")
                (("" (hide -1 -3)
                  (("" (expand "ae_bounded?")
                    (("" (skosimp*)
                      (("" (inst + "K!1+K!2")
                        (("" (expand "ae_le?")
                          (("" (expand "pointwise_ae?")
                            (("" (expand "ae?")
                              ((""
                                (expand "fullset")
                                ((""
                                  (expand "ae_in?")
                                  ((""
                                    (skosimp*)
                                    ((""
                                      (inst + "union(E!1,E!2)")
                                      ((""
                                        (skosimp)
                                        ((""
                                          (expand "union")
                                          ((""
                                            (expand "member")
                                            ((""
                                              (flatten)
                                              ((""
                                                (inst - "x!1")
                                                ((""
                                                  (inst - "x!1")
                                                  ((""
                                                    (assert)
                                                    ((""
                                                      (hide 1 2)
                                                      ((""
                                                        (expand "abs")
                                                        ((""
                                                          (expand "+")
                                                          ((""
                                                            (lemma
                                                             "abs_triangle"
                                                             ("z1"
                                                              "f0!1(x!1)"
                                                              "z2"
                                                              "f1!1(x!1)"))
                                                            ((""
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cal_L_infty nonempty-type-eq-decl nil cal_L_inf nil)
    (cal_L_infty? const-decl "bool" cal_L_inf nil)
    (complex type-decl nil complex_types "complex_alt/")
    (T formal-type-decl nil cal_L_inf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (add_essentially_bounded application-judgement
     "essentially_bounded" cal_L_inf nil))
   nil))
 (opp_cal_L_infty 0
  (opp_cal_L_infty-1 nil 3477289127
   ("" (skosimp)
    (("" (expand "cal_L_infty?") (("" (propax) nil nil)) nil)) nil)
   ((opp_essentially_bounded application-judgement
     "essentially_bounded" cal_L_inf nil)
    (cal_L_infty? const-decl "bool" cal_L_inf nil))
   nil))
 (diff_cal_L_infty 0
  (diff_cal_L_infty-1 nil 3477289127
   ("" (skosimp)
    (("" (typepred "f0!1")
      (("" (typepred "f1!1")
        (("" (expand "cal_L_infty?") (("" (propax) nil nil)) nil))
        nil))
      nil))
    nil)
   ((cal_L_infty nonempty-type-eq-decl nil cal_L_inf nil)
    (cal_L_infty? const-decl "bool" cal_L_inf nil)
    (complex type-decl nil complex_types "complex_alt/")
    (T formal-type-decl nil cal_L_inf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (diff_essentially_bounded application-judgement
     "essentially_bounded[T, S, mu]" cal_L_inf nil))
   nil))
 (prod_cal_L_infty 0
  (prod_cal_L_infty-1 nil 3477289127
   ("" (skosimp)
    (("" (typepred "f1!1")
      (("" (typepred "f0!1")
        (("" (expand "cal_L_infty?")
          (("" (expand "essentially_bounded?")
            (("" (flatten)
              (("" (rewrite "prod_complex_measurable")
                (("" (hide -1 -3)
                  (("" (expand "ae_bounded?")
                    (("" (skosimp*)
                      (("" (inst + "K!1*K!2")
                        (("" (expand "ae_le?")
                          (("" (expand "pointwise_ae?")
                            (("" (expand "ae?")
                              ((""
                                (expand "fullset")
                                ((""
                                  (expand "ae_in?")
                                  ((""
                                    (skosimp*)
                                    ((""
                                      (inst + "union(E!1,E!2)")
                                      ((""
                                        (skosimp)
                                        ((""
                                          (inst - "x!1")
                                          ((""
                                            (inst - "x!1")
                                            ((""
                                              (expand "union")
                                              ((""
                                                (expand "member")
                                                ((""
                                                  (flatten)
                                                  ((""
                                                    (assert)
                                                    ((""
                                                      (hide 1 2)
                                                      ((""
                                                        (expand "abs")
                                                        ((""
                                                          (expand "*")
                                                          ((""
                                                            (rewrite
                                                             "abs_mult")
                                                            ((""
                                                              (lemma
                                                               "le_times_le_pos"
                                                               ("nnx"
                                                                "abs(f0!1(x!1))"
                                                                "y"
                                                                "K!1"
                                                                "nnz"
                                                                "abs(f1!1(x!1))"
                                                                "w"
                                                                "K!2"))
                                                              ((""
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cal_L_infty nonempty-type-eq-decl nil cal_L_inf nil)
    (cal_L_infty? const-decl "bool" cal_L_inf nil)
    (complex type-decl nil complex_types "complex_alt/")
    (T formal-type-decl nil cal_L_inf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (prod_essentially_bounded application-judgement
     "essentially_bounded" cal_L_inf nil))
   nil))
 (inf_norm_scal 0
  (inf_norm_scal-1 nil 3477290163
   ("" (skosimp)
    (("" (expand "inf_norm")
      ((""
        (lemma "essential_bound_def1"
         ("f" "c!1*f!1" "K" "abs(c!1) * essential_bound(f!1)"))
        (("" (split -1)
          (("1" (typepred "abs(c!1)")
            (("1" (expand ">=")
              (("1" (expand "<=" -1)
                (("1" (split)
                  (("1"
                    (lemma "essential_bound_def1"
                     ("f" "f!1" "K"
                      "essential_bound(c!1 * f!1)/abs(c!1)"))
                    (("1" (split -1)
                      (("1" (rewrite "div_mult_pos_le2" -1)
                        (("1" (assert) nil nil)) nil)
                       ("2" (hide-all-but (-1 1))
                        (("2"
                          (lemma "essential_bound_def2"
                           ("f" "c!1*f!1"))
                          (("1" (expand "ae_le?")
                            (("1" (expand "pointwise_ae?")
                              (("1"
                                (expand "ae?")
                                (("1"
                                  (expand "fullset")
                                  (("1"
                                    (expand "ae_in?")
                                    (("1"
                                      (skosimp)
                                      (("1"
                                        (inst + "E!1")
                                        (("1"
                                          (skosimp)
                                          (("1"
                                            (expand "member")
                                            (("1"
                                              (inst - "x!1")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (expand "abs" -1)
                                                  (("1"
                                                    (hide 1)
                                                    (("1"
                                                      (expand
                                                       "abs"
                                                       1
                                                       1)
                                                      (("1"
                                                        (expand
                                                         "*"
                                                         -1
                                                         1)
                                                        (("1"
                                                          (rewrite
                                                           "abs_mult")
                                                          (("1"
                                                            (rewrite
                                                             "div_mult_pos_le2"
                                                             +)
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2"
                            (lemma "scal_cal_L_infty"
                             ("c" "c!1" "f" "f!1"))
                            (("2" (expand "cal_L_infty?")
                              (("2" (propax) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2"
                      (typepred
                       "essential_bound[T, S, mu](*[T](c!1, f!1))")
                      (("2" (rewrite "div_mult_pos_ge1" +)
                        (("2" (assert) nil nil)) nil))
                      nil)
                     ("3" (assert) nil nil))
                    nil)
                   ("2" (replace -1 * rl) (("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (lemma "essential_bound_def2" ("f" "f!1"))
              (("1" (expand "ae_le?")
                (("1" (expand "pointwise_ae?")
                  (("1" (expand "ae?")
                    (("1" (expand "fullset")
                      (("1" (expand "ae_in?")
                        (("1" (skosimp)
                          (("1" (inst + "E!1")
                            (("1" (skosimp)
                              (("1"
                                (inst - "x!1")
                                (("1"
                                  (expand "member")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (hide 1)
                                      (("1"
                                        (expand "abs" -)
                                        (("1"
                                          (expand "abs" 1 1)
                                          (("1"
                                            (expand "*" 1 1)
                                            (("1"
                                              (rewrite "abs_mult")
                                              (("1"
                                                (typepred "abs(c!1)")
                                                (("1"
                                                  (expand ">=")
                                                  (("1"
                                                    (expand "<=" -1)
                                                    (("1"
                                                      (split)
                                                      (("1"
                                                        (lemma
                                                         "both_sides_times_pos_le1"
                                                         ("pz"
                                                          "abs(c!1)"
                                                          "x"
                                                          "abs(f!1(x!1))"
                                                          "y"
                                                          "essential_bound(f!1)"))
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil)
                                                         ("2"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (typepred "f!1")
                (("2" (expand "cal_L_infty?") (("2" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((inf_norm const-decl "nnreal" cal_L_inf nil)
    (div_mult_pos_ge1 formula-decl nil real_props 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)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (essential_bound_def2 formula-decl nil essentially_bounded nil)
    (pointwise_ae? const-decl "bool" measure_theory
     "measure_integration/")
    (fullset const-decl "set" sets nil)
    (TRUE const-decl "bool" booleans nil)
    (abs const-decl "[T -> nonneg_real]" complex_fun_ops
         "complex_alt/")
    (abs_mult formula-decl nil polar "complex_alt/")
    (member const-decl "bool" sets nil) (set type-eq-decl nil sets nil)
    (negligible_set? const-decl "bool" measure_theory
     "measure_integration/")
    (negligible nonempty-type-eq-decl nil measure_theory
     "measure_integration/")
    (ae_in? const-decl "bool" measure_theory "measure_integration/")
    (ae? const-decl "bool" measure_theory "measure_integration/")
    (measurable_fullset name-judgement "measurable_set[T, S]" cal_L_inf
     nil)
    (subset_algebra_fullset name-judgement "(S)" cal_L_inf nil)
    (ae_le? const-decl "bool" measure_theory "measure_integration/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (<= const-decl "bool" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (both_sides_times_pos_le1 formula-decl nil real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (scal_cal_L_infty application-judgement "cal_L_infty" cal_L_inf
     nil)
    (essential_bound_def1 formula-decl nil essentially_bounded nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (complex type-decl nil complex_types "complex_alt/")
    (abs const-decl "nnreal" polar "complex_alt/")
    (essentially_bounded? const-decl "bool" essentially_bounded nil)
    (essentially_bounded nonempty-type-eq-decl nil essentially_bounded
     nil)
    (essential_bound const-decl "nnreal" essentially_bounded nil)
    (cal_L_infty? const-decl "bool" cal_L_inf nil)
    (cal_L_infty nonempty-type-eq-decl nil cal_L_inf nil)
    (* const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
    (T formal-type-decl nil cal_L_inf 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
     "measure_integration/")
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
     "measure_integration/")
    (S formal-const-decl "sigma_algebra[T]" cal_L_inf 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
     "measure_integration/")
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     "measure_integration/")
    (mu formal-const-decl "measure_type[T, S]" cal_L_inf nil))
   shostak))
 (inf_norm_add 0
  (inf_norm_add-1 nil 3477386071
   ("" (skosimp)
    (("" (expand "inf_norm")
      ((""
        (lemma "essential_bound_def1"
         ("f" "f0!1+f1!1" "K"
          "essential_bound(f0!1) + essential_bound(f1!1)"))
        (("" (assert)
          (("" (hide 2)
            (("" (lemma "essential_bound_def2" ("f" "f0!1"))
              (("1" (lemma "essential_bound_def2" ("f" "f1!1"))
                (("1" (expand "ae_le?")
                  (("1" (expand "pointwise_ae?")
                    (("1" (expand "ae?")
                      (("1" (expand "fullset")
                        (("1" (expand "ae_in?")
                          (("1" (skosimp*)
                            (("1" (inst + "union(E!1,E!2)")
                              (("1"
                                (skosimp)
                                (("1"
                                  (inst - "x!1")
                                  (("1"
                                    (inst - "x!1")
                                    (("1"
                                      (expand "union")
                                      (("1"
                                        (expand "member")
                                        (("1"
                                          (flatten)
                                          (("1"
                                            (replace 1)
                                            (("1"
                                              (replace 2)
                                              (("1"
                                                (hide 1 2)
                                                (("1"
                                                  (expand "abs")
                                                  (("1"
                                                    (lemma
                                                     "abs_triangle"
                                                     ("z1"
                                                      "f0!1(x!1)"
                                                      "z2"
                                                      "f1!1(x!1)"))
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (expand "+" +)
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (typepred "f1!1")
                  (("2" (expand "cal_L_infty?")
                    (("2" (propax) nil nil)) nil))
                  nil))
                nil)
               ("2" (typepred "f0!1")
                (("2" (expand "cal_L_infty?") (("2" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((inf_norm const-decl "nnreal" cal_L_inf nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (essential_bound_def2 formula-decl nil essentially_bounded nil)
    (ae_le? const-decl "bool" measure_theory "measure_integration/")
    (subset_algebra_fullset name-judgement "(S)" cal_L_inf nil)
    (measurable_fullset name-judgement "measurable_set[T, S]" cal_L_inf
     nil)
    (ae? const-decl "bool" measure_theory "measure_integration/")
    (ae_in? const-decl "bool" measure_theory "measure_integration/")
    (negligible_union application-judgement "negligible[T, S, mu]"
     cal_L_inf nil)
    (union const-decl "set" sets nil)
    (negligible nonempty-type-eq-decl nil measure_theory
     "measure_integration/")
    (negligible_set? const-decl "bool" measure_theory
     "measure_integration/")
    (set type-eq-decl nil sets nil)
    (TRUE const-decl "bool" booleans nil)
    (abs const-decl "[T -> nonneg_real]" complex_fun_ops
         "complex_alt/")
    (abs_triangle formula-decl nil polar "complex_alt/")
    (member const-decl "bool" sets nil)
    (fullset const-decl "set" sets nil)
    (pointwise_ae? const-decl "bool" measure_theory
     "measure_integration/")
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (add_cal_L_infty application-judgement "cal_L_infty" cal_L_inf nil)
    (essential_bound_def1 formula-decl nil essentially_bounded nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (complex type-decl nil complex_types "complex_alt/")
    (essentially_bounded? const-decl "bool" essentially_bounded nil)
    (essentially_bounded nonempty-type-eq-decl nil essentially_bounded
     nil)
    (essential_bound const-decl "nnreal" essentially_bounded nil)
    (cal_L_infty? const-decl "bool" cal_L_inf nil)
    (cal_L_infty nonempty-type-eq-decl nil cal_L_inf nil)
    (+ const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
    (T formal-type-decl nil cal_L_inf 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
     "measure_integration/")
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
     "measure_integration/")
    (S formal-const-decl "sigma_algebra[T]" cal_L_inf 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
     "measure_integration/")
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     "measure_integration/")
    (mu formal-const-decl "measure_type[T, S]" cal_L_inf nil))
   shostak))
 (inf_norm_opp 0
  (inf_norm_opp-1 nil 3477384776
   ("" (skosimp)
    (("" (lemma "essential_bound_opp" ("f" "f!1"))
      (("" (expand "inf_norm") (("" (propax) nil nil)) nil)) nil))
    nil)
   ((mu formal-const-decl "measure_type[T, S]" cal_L_inf nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     "measure_integration/")
    (measure? const-decl "bool" generalized_measure_def
     "measure_integration/")
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (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)
    (S formal-const-decl "sigma_algebra[T]" cal_L_inf nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
     "measure_integration/")
    (sigma_algebra? const-decl "bool" subset_algebra_def
     "measure_integration/")
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil cal_L_inf nil)
    (cal_L_infty nonempty-type-eq-decl nil cal_L_inf nil)
    (cal_L_infty? const-decl "bool" cal_L_inf nil)
    (essentially_bounded nonempty-type-eq-decl nil essentially_bounded
     nil)
    (essentially_bounded? const-decl "bool" essentially_bounded nil)
    (complex type-decl nil complex_types "complex_alt/")
    (essential_bound_opp formula-decl nil essentially_bounded nil)
    (inf_norm const-decl "nnreal" cal_L_inf nil))
   shostak))
 (inf_norm_diff 0
  (inf_norm_diff-1 nil 3477384889
   ("" (skosimp)
    (("" (lemma "essential_bound_diff" ("f0" "f0!1" "f1" "f1!1"))
      (("" (expand "inf_norm") (("" (propax) nil nil)) nil)) nil))
    nil)
   ((mu formal-const-decl "measure_type[T, S]" cal_L_inf nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     "measure_integration/")
    (measure? const-decl "bool" generalized_measure_def
     "measure_integration/")
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (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)
    (S formal-const-decl "sigma_algebra[T]" cal_L_inf nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
     "measure_integration/")
    (sigma_algebra? const-decl "bool" subset_algebra_def
     "measure_integration/")
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil cal_L_inf nil)
    (cal_L_infty nonempty-type-eq-decl nil cal_L_inf nil)
    (cal_L_infty? const-decl "bool" cal_L_inf nil)
    (essentially_bounded nonempty-type-eq-decl nil essentially_bounded
     nil)
    (essentially_bounded? const-decl "bool" essentially_bounded nil)
    (complex type-decl nil complex_types "complex_alt/")
    (essential_bound_diff formula-decl nil essentially_bounded nil)
    (inf_norm const-decl "nnreal" cal_L_inf nil))
   shostak))
 (inf_norm_eq_0 0
  (inf_norm_eq_0-1 nil 3477290216
   ("" (skosimp)
    (("" (typepred "f!1")
      (("" (copy -1)
        (("" (expand "cal_L_infty?" -1)
          (("" (expand "essentially_bounded?")
            (("" (flatten)
              (("" (expand "cal_N?")
                (("" (replace -1)
                  (("" (split)
                    (("1" (flatten)
                      (("1" (expand "inf_norm")
                        (("1"
                          (lemma "essential_bound_def2" ("f" "f!1"))
                          (("1" (replace -2)
                            (("1" (hide-all-but (-1 1))
                              (("1"
                                (expand "ae_le?")
                                (("1"
                                  (expand "ae_0?")
                                  (("1"
                                    (expand "pointwise_ae?")
                                    (("1"
                                      (expand "ae?")
                                      (("1"
                                        (expand "fullset")
                                        (("1"
                                          (expand "ae_in?")
                                          (("1"
                                            (skosimp)
                                            (("1"
                                              (inst + "E!1")
                                              (("1"
                                                (skosimp)
                                                (("1"
                                                  (inst - "x!1")
                                                  (("1"
                                                    (expand "member")
                                                    (("1"
                                                      (replace 1)
                                                      (("1"
                                                        (expand "abs")
                                                        (("1"
                                                          (hide 1)
                                                          (("1"
                                                            (expand
                                                             "<="
                                                             -1)
                                                            (("1"
                                                              (split)
                                                              (("1"
                                                                (assert)
                                                                nil
                                                                nil)
                                                               ("2"
                                                                (rewrite
                                                                 "abs_is_0")
                                                                (("2"
                                                                  (flatten)
                                                                  (("2"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (flatten)
                      (("2" (expand "inf_norm")
                        (("2"
                          (lemma "essential_bound_def1"
                           ("f" "f!1" "K" "0"))
                          (("2" (split)
                            (("1" (assert) nil nil)
                             ("2" (hide-all-but (-1 1))
                              (("2"
                                (expand "ae_0?")
                                (("2"
                                  (expand "ae_le?")
                                  (("2"
                                    (expand "pointwise_ae?")
                                    (("2"
                                      (expand "ae?")
                                      (("2"
                                        (expand "abs")
                                        (("2"
                                          (expand "fullset")
                                          (("2"
                                            (expand "ae_in?")
                                            (("2"
                                              (skosimp)
                                              (("2"
                                                (inst + "E!1")
                                                (("2"
                                                  (skosimp)
                                                  (("2"
                                                    (inst - "x!1")
                                                    (("2"
                                                      (expand "member")
                                                      (("2"
                                                        (replace 1)
                                                        (("2"
                                                          (grind)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cal_L_infty nonempty-type-eq-decl nil cal_L_inf nil)
    (cal_L_infty? const-decl "bool" cal_L_inf nil)
    (complex type-decl nil complex_types "complex_alt/")
    (T formal-type-decl nil cal_L_inf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (essential_bound_def1 formula-decl nil essentially_bounded nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (Re const-decl "real" complex_types "complex_alt/")
    (sq const-decl "nonneg_real" sq "reals/")
    (Im const-decl "real" complex_types "complex_alt/")
    (sq_abs const-decl "nnreal" complex_types "complex_alt/")
    (abs const-decl "nnreal" polar "complex_alt/")
    (= const-decl "bool" complex_types "complex_alt/")
    (sqrt_0 formula-decl nil sqrt "reals/")
    (even_plus_even_is_even application-judgement "even_int" integers
     nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (mu formal-const-decl "measure_type[T, S]" cal_L_inf nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     "measure_integration/")
    (measure? const-decl "bool" generalized_measure_def
     "measure_integration/")
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (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)
    (S formal-const-decl "sigma_algebra[T]" cal_L_inf nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
     "measure_integration/")
    (sigma_algebra? const-decl "bool" subset_algebra_def
     "measure_integration/")
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (essentially_bounded nonempty-type-eq-decl nil essentially_bounded
     nil)
    (essential_bound_def2 formula-decl nil essentially_bounded nil)
    (ae_0? const-decl "bool" complex_measure_theory nil)
    (subset_algebra_fullset name-judgement "(S)" cal_L_inf nil)
    (measurable_fullset name-judgement "measurable_set[T, S]" cal_L_inf
     nil)
    (ae? const-decl "bool" measure_theory "measure_integration/")
    (ae_in? const-decl "bool" measure_theory "measure_integration/")
    (negligible nonempty-type-eq-decl nil measure_theory
     "measure_integration/")
    (negligible_set? const-decl "bool" measure_theory
     "measure_integration/")
    (set type-eq-decl nil sets nil)
    (TRUE const-decl "bool" booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (c_eq1 formula-decl nil complex_types "complex_alt/")
    (Im_rew formula-decl nil complex_types "complex_alt/")
    (Re_rew formula-decl nil complex_types "complex_alt/")
    (c_eq3 formula-decl nil complex_types "complex_alt/")
    (abs_is_0 formula-decl nil polar "complex_alt/")
    (<= const-decl "bool" reals nil)
    (abs const-decl "[T -> nonneg_real]" complex_fun_ops
         "complex_alt/")
    (member const-decl "bool" sets nil)
    (fullset const-decl "set" sets nil)
    (pointwise_ae? const-decl "bool" measure_theory
     "measure_integration/")
    (pointwise_ae? const-decl "bool" complex_measure_theory nil)
    (ae_le? const-decl "bool" measure_theory "measure_integration/")
    (inf_norm const-decl "nnreal" cal_L_inf nil)
    (cal_N? const-decl "bool" complex_measure_theory nil)
    (essentially_bounded? const-decl "bool" essentially_bounded nil))
   shostak))
 (inf_norm_prod 0
  (inf_norm_prod-1 nil 3477386355
   ("" (skosimp)
    (("" (expand "inf_norm")
      ((""
        (lemma "essential_bound_def1"
         ("f" "f0!1 * f1!1" "K"
          "essential_bound(f0!1) * essential_bound(f1!1)"))
        (("" (assert)
          (("" (hide 2)
            (("" (lemma "essential_bound_def2" ("f" "f0!1"))
              (("" (lemma "essential_bound_def2" ("f" "f1!1"))
                (("" (expand "abs")
                  (("" (expand "*" 1)
                    (("" (expand "ae_le?")
                      (("" (expand "pointwise_ae?")
                        (("" (expand "ae?")
                          (("" (expand "fullset")
                            (("" (expand "ae_in?")
                              ((""
                                (skosimp*)
                                ((""
                                  (inst + "union(E!1,E!2)")
                                  ((""
                                    (skosimp)
                                    ((""
                                      (inst - "x!1")
                                      ((""
                                        (inst - "x!1")
                                        ((""
                                          (expand "union")
                                          ((""
                                            (expand "member")
                                            ((""
                                              (flatten)
                                              ((""
                                                (replace 1)
                                                ((""
                                                  (replace 2)
                                                  ((""
                                                    (hide 1 2)
                                                    ((""
                                                      (rewrite
                                                       "abs_mult"
                                                       +)
                                                      ((""
                                                        (lemma
                                                         "le_times_le_pos"
                                                         ("nnx"
                                                          "abs(f0!1(x!1))"
                                                          "nnz"
                                                          "abs(f1!1(x!1))"
                                                          "y"
                                                          "essential_bound(f0!1)"
                                                          "w"
                                                          "essential_bound(f1!1)"))
                                                        ((""
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.48 Sekunden  (vorverarbeitet)  ¤



Bilder
Diashow
Bilder
sprechenden Kalenders

in der Quellcodebibliothek suchen




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