Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: p_integrable.prf Sprache: Lisp

Original von: PVS^©

(p_integrable
(mu_TCC1 0
  (mu_TCC1-1 nil 3477417010
   ("" (typepred "S")
    (("" (expand "sigma_algebra?")
      (("" (expand "subset_algebra_empty?")
        (("" (flatten) (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((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)
    (subset_algebra_empty? const-decl "bool" subset_algebra_def
     "measure_integration/")
    (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 p_integrable 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]" p_integrable nil))
   nil))
(scal_p_integrable 0
  (scal_p_integrable-1 nil 3477417010
   ("" (skosimp)
    (("" (typepred "f!1")
      (("" (expand "p_integrable?")
        (("" (flatten)
          (("" (rewrite "scal_complex_measurable")
            (("" (hide -1)
              ((""
                (lemma "integral.integrable_scal"
                 ("c" "abs(c!1)^p" "f" "abs(f!1)^p"))
                (("1"
                  (case-replace
                   "(*[T](abs(c!1) ^ p, abs(f!1) ^ p))=(abs(*[T](c!1, f!1)) ^ p)")
                  (("1" (apply-extensionality :hide? t)
                    (("1" (hide-all-but 1)
                      (("1" (expand "*" 1 1)
                        (("1" (expand "^" 1 2)
                          (("1" (expand "abs" 1 2)
                            (("1" (expand "^" 1 3)
                              (("1"
                                (expand "abs" 1 3)
                                (("1"
                                  (expand "*" 1 2)
                                  (("1"
                                    (rewrite "abs_mult")
                                    (("1"
                                      (lemma
                                       "mult_real_expt"
                                       ("x"
                                        "abs(c!1)"
                                        "y"
                                        "abs(f!1(x!1))"
                                        "a"
                                        "p"))
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (propax) nil nil) ("3" (assert) nil nil)
                 ("4" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((p_integrable nonempty-type-eq-decl nil p_integrable_def nil)
    (p_integrable? const-decl "bool" p_integrable_def nil)
    (p formal-const-decl "{a: real | a >= 1}" p_integrable nil)
    (mu formal-const-decl "measure_type[T, S]" p_integrable 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]" p_integrable 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)
    (complex type-decl nil complex_types "complex_alt/")
    (T formal-type-decl nil p_integrable nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (* const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (mult_real_expt formula-decl nil real_expt "power/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (abs_mult formula-decl nil polar "complex_alt/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (integrable_scal judgement-tcc nil integral "measure_integration/")
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (> const-decl "bool" reals nil)
    (^ const-decl "nnreal" real_expt "power/")
    (abs const-decl "nnreal" polar "complex_alt/")
    (integrable? const-decl "bool" integral "measure_integration/")
    (integrable nonempty-type-eq-decl nil integral
     "measure_integration/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (^ const-decl "[T -> nnreal]" real_fun_power "power/")
    (abs const-decl "[T -> nonneg_real]" complex_fun_ops
         "complex_alt/")
    (Im_fun_mul2 formula-decl nil complex_fun_ops "complex_alt/")
    (Re_fun_mul2 formula-decl nil complex_fun_ops "complex_alt/")
    (complex_measurable nonempty-type-eq-decl nil complex_measurable
     nil)
    (complex_measurable? const-decl "bool" complex_measurable nil)
    (scal_complex_measurable judgement-tcc nil complex_measurable nil)
    (Im const-decl "[T -> real]" complex_fun_ops "complex_alt/")
    (Re const-decl "[T -> real]" complex_fun_ops "complex_alt/")
    (measurable_function? const-decl "bool" measure_space_def
     "measure_integration/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (complex_measurable_def formula-decl nil complex_measurable nil))
   nil))
(sum_p_integrable 0
  (sum_p_integrable-1 nil 3477417965
   ("" (skosimp)
    (("" (typepred "f1!1")
      (("" (typepred "f0!1")
        (("" (lemma "minkowski_scaf" ("f" "f0!1" "g" "f1!1"))
          (("" (flatten) nil nil)) nil))
        nil))
      nil))
    nil)
   ((p_integrable nonempty-type-eq-decl nil p_integrable_def nil)
    (p_integrable? const-decl "bool" p_integrable_def nil)
    (p formal-const-decl "{a: real | a >= 1}" p_integrable nil)
    (mu formal-const-decl "measure_type[T, S]" p_integrable 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]" p_integrable 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)
    (complex type-decl nil complex_types "complex_alt/")
    (T formal-type-decl nil p_integrable nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (minkowski_scaf formula-decl nil minkowski_scaf nil))
   nil))
(opp_p_integrable 0
  (opp_p_integrable-1 nil 3477417010
   ("" (skosimp)
    (("" (typepred "f!1")
      (("" (expand "p_integrable?")
        (("" (flatten)
          (("" (rewrite "opp_complex_measurable")
            (("" (assert)
              (("" (case-replace "abs(-f!1)=abs(f!1)")
                (("" (apply-extensionality :hide? t)
                  (("" (hide-all-but 1)
                    (("" (expand "abs")
                      (("" (expand "-")
                        (("" (expand "abs")
                          (("" (expand "sq_abs")
                            (("" (assert)
                              ((""
                                (expand "sq")
                                (("" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((p_integrable nonempty-type-eq-decl nil p_integrable_def nil)
    (p_integrable? const-decl "bool" p_integrable_def nil)
    (p formal-const-decl "{a: real | a >= 1}" p_integrable nil)
    (mu formal-const-decl "measure_type[T, S]" p_integrable 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]" p_integrable 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)
    (complex type-decl nil complex_types "complex_alt/")
    (T formal-type-decl nil p_integrable nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (complex_abs_neg formula-decl nil complex_fun_ops "complex_alt/")
    (Im_fun_neg1 formula-decl nil complex_fun_ops "complex_alt/")
    (Re_fun_neg1 formula-decl nil complex_fun_ops "complex_alt/")
    (complex_measurable nonempty-type-eq-decl nil complex_measurable
     nil)
    (complex_measurable? const-decl "bool" complex_measurable nil)
    (opp_complex_measurable judgement-tcc nil complex_measurable nil)
    (Im const-decl "[T -> real]" complex_fun_ops "complex_alt/")
    (Re const-decl "[T -> real]" complex_fun_ops "complex_alt/")
    (measurable_function? const-decl "bool" measure_space_def
     "measure_integration/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (complex_measurable_def formula-decl nil complex_measurable nil))
   nil))
(diff_p_integrable 0
  (diff_p_integrable-1 nil 3477417010
   ("" (skosimp)
    (("" (lemma "opp_p_integrable" ("f" "f1!1"))
      (("" (lemma "sum_p_integrable" ("f0" "f0!1" "f1" "-f1!1"))
        (("" (case-replace "(+[T])(f0!1, -f1!1)=(-[T])(f0!1, f1!1)")
          (("1" (hide-all-but 1)
            (("1" (typepred "f0!1")
              (("1" (typepred "f1!1")
                (("1" (lemma "opp_p_integrable" ("f" "f1!1"))
                  (("1"
                    (lemma "sum_p_integrable"
                     ("f0" "f0!1" "f1" "-f1!1"))
                    (("1" (hide -2 -3 -4)
                      (("1" (expand "+")
                        (("1" (expand "-")
                          (("1" (expand "p_integrable?")
                            (("1" (flatten)
                              (("1"
                                (expand "complex_measurable?")
                                (("1"
                                  (flatten)
                                  (("1"
                                    (assert)
                                    (("1"
                                      (expand "Re")
                                      (("1"
                                        (expand "Im")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (hide -1 -2)
                                            (("1"
                                              (expand "abs")
                                              (("1"
                                                (expand "abs")
                                                (("1"
                                                  (expand "sq_abs")
                                                  (("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" (hide-all-but 1)
            (("2" (expand "+")
              (("2" (expand "-")
                (("2" (expand "=")
                  (("2" (split)
                    (("1" (apply-extensionality :hide? t) nil nil)
                     ("2" (apply-extensionality :hide? t) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((p_integrable nonempty-type-eq-decl nil p_integrable_def nil)
    (p_integrable? const-decl "bool" p_integrable_def nil)
    (p formal-const-decl "{a: real | a >= 1}" p_integrable nil)
    (mu formal-const-decl "measure_type[T, S]" p_integrable 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]" p_integrable 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)
    (complex type-decl nil complex_types "complex_alt/")
    (T formal-type-decl nil p_integrable nil)
    (opp_p_integrable judgement-tcc nil p_integrable nil)
    (- const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
    (+ const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
    (= const-decl "bool" complex_fun_ops "complex_alt/")
    (sum_p_integrable application-judgement "p_integrable" p_integrable
     nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (Re const-decl "[T -> real]" complex_fun_ops "complex_alt/")
    (minus_real_is_real application-judgement "real" reals nil)
    (Re_neg1 formula-decl nil complex_types "complex_alt/")
    (Re_add1 formula-decl nil complex_types "complex_alt/")
    (Im_neg1 formula-decl nil complex_types "complex_alt/")
    (Im_add1 formula-decl nil complex_types "complex_alt/")
    (Re_sub1 formula-decl nil complex_types "complex_alt/")
    (Im_sub1 formula-decl nil complex_types "complex_alt/")
    (abs const-decl "[T -> nonneg_real]" complex_fun_ops
         "complex_alt/")
    (sq_abs const-decl "nnreal" complex_types "complex_alt/")
    (abs const-decl "nnreal" polar "complex_alt/")
    (Im const-decl "[T -> real]" complex_fun_ops "complex_alt/")
    (complex_measurable? const-decl "bool" complex_measurable nil)
    (Im_fun_rew formula-decl nil complex_fun_ops "complex_alt/")
    (- const-decl "complex" complex_types "complex_alt/")
    (- const-decl "complex" complex_types "complex_alt/")
    (+ const-decl "complex" complex_types "complex_alt/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (Re_fun_rew formula-decl nil complex_fun_ops "complex_alt/")
    (opp_p_integrable application-judgement "p_integrable" p_integrable
     nil)
    (sum_p_integrable judgement-tcc nil p_integrable nil)
    (- const-decl "[T -> complex]" complex_fun_ops "complex_alt/"))
   nil))
(norm_scal 0
  (norm_scal-1 nil 3477454646
   ("" (skosimp)
    (("" (expand "norm")
      ((""
        (case-replace "(abs(c!1 * f!1) ^ p)=abs(c!1)^p * abs(f!1)^p")
        (("1" (hide -1)
          (("1" (rewrite "integral.integral_scal")
            (("1"
              (name-replace "INT" "integral.integral(abs(f!1) ^ p)")
              (("1" (rewrite "mult_real_expt")
                (("1"
                  (lemma "real_expt_times"
                   ("x" "abs(c!1)" "a" "p" "b" "1/p"))
                  (("1" (replace -1 1 rl)
                    (("1" (rewrite "div_cancel1")
                      (("1" (rewrite "real_expt_x1") nil nil)) nil))
                    nil))
                  nil)
                 ("2" (flatten)
                  (("2"
                    (lemma "posreal_div_posreal_is_posreal"
                     ("px" "1" "py" "p"))
                    (("2" (assert) nil nil)) nil))
                  nil)
                 ("3" (expand "INT")
                  (("3" (hide 2)
                    (("3"
                      (lemma "integral_nonneg" ("f" "abs(f!1) ^ p"))
                      (("3" (split)
                        (("1" (propax) nil nil)
                         ("2" (hide 2)
                          (("2" (skosimp)
                            (("2" (expand "^")
                              (("2"
                                (expand "abs")
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide 2)
          (("2" (apply-extensionality :hide? t)
            (("1" (expand "^" 1 1)
              (("1" (expand "^" 1 3)
                (("1" (expand "*" 1)
                  (("1" (expand "abs" 1 1)
                    (("1" (rewrite "abs_mult")
                      (("1" (expand "abs" 1 4)
                        (("1" (rewrite "mult_real_expt") nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (skolem + "x!1")
              (("2" (expand "*")
                (("2" (expand "^" 1 2)
                  (("2" (expand "abs" 1 2)
                    (("2" (rewrite "mult_real_expt" + :dir rl)
                      (("2"
                        (lemma "abs_mult" ("z1" "c!1" "z2" "f!1(x!1)"))
                        (("2" (replace -1 1 rl)
                          (("2" (hide -1) (("2" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("3" (assert) nil nil) ("4" (assert) nil nil))
        nil))
      nil))
    nil)
   ((norm const-decl "nnreal" p_integrable_def nil)
    (abs_mult formula-decl nil polar "complex_alt/")
    (c!1 skolem-const-decl "complex" p_integrable nil)
    (f!1 skolem-const-decl "p_integrable[T, S, mu, p]" p_integrable
     nil)
    (integral const-decl "real" integral "measure_integration/")
    (INT skolem-const-decl "real" p_integrable nil)
    (integral_nonneg formula-decl nil integral "measure_integration/")
    (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil)
    (real_expt_times formula-decl nil real_expt "power/")
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_cancel1 formula-decl nil real_props nil)
    (real_expt_x1 formula-decl nil real_expt "power/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (mult_real_expt formula-decl nil real_expt "power/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (integral_scal formula-decl nil integral "measure_integration/")
    (integrable? const-decl "bool" integral "measure_integration/")
    (integrable nonempty-type-eq-decl nil integral
     "measure_integration/")
    (abs const-decl "nnreal" polar "complex_alt/")
    (^ const-decl "nnreal" real_expt "power/")
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (p_integrable nonempty-type-eq-decl nil p_integrable_def nil)
    (p_integrable? const-decl "bool" p_integrable_def nil)
    (p formal-const-decl "{a: real | a >= 1}" p_integrable nil)
    (mu formal-const-decl "measure_type[T, S]" p_integrable 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/")
    (S formal-const-decl "sigma_algebra[T]" p_integrable 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)
    (* const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
    (abs const-decl "[T -> nonneg_real]" complex_fun_ops
         "complex_alt/")
    (complex type-decl nil complex_types "complex_alt/")
    (^ const-decl "[T -> nnreal]" real_fun_power "power/")
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (T formal-type-decl nil p_integrable nil)
    (scal_p_integrable application-judgement "p_integrable"
     p_integrable nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
(norm_add 0
  (norm_add-1 nil 3477590515
   ("" (skosimp)
    (("" (lemma "minkowski_scaf" ("f" "f0!1" "g" "f1!1"))
      (("" (flatten) nil nil)) nil))
    nil)
   ((p formal-const-decl "{a: real | a >= 1}" p_integrable nil)
    (mu formal-const-decl "measure_type[T, S]" p_integrable 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]" p_integrable 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 p_integrable nil)
    (p_integrable nonempty-type-eq-decl nil p_integrable_def nil)
    (p_integrable? const-decl "bool" p_integrable_def nil)
    (complex type-decl nil complex_types "complex_alt/")
    (minkowski_scaf formula-decl nil minkowski_scaf nil))
   shostak))
(norm_opp 0
  (norm_opp-1 nil 3477455430
   ("" (skosimp)
    (("" (expand "norm")
      (("" (assert)
        (("" (case-replace "abs(-f!1)=abs(f!1)")
          (("" (hide 2)
            (("" (apply-extensionality :hide? t) (("" (grind) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((norm const-decl "nnreal" p_integrable_def nil)
    (opp_p_integrable application-judgement "p_integrable" p_integrable
     nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (complex_abs_neg formula-decl nil complex_fun_ops "complex_alt/"))
   shostak))
(norm_diff 0
  (norm_diff-1 nil 3477455509
   ("" (skosimp)
    (("" (lemma "norm_add" ("f0" "f0!1" "f1" "-f1!1"))
      (("" (rewrite "norm_opp")
        (("" (name-replace "RHS" "norm(f0!1) + norm(f1!1)")
          (("" (expand "norm")
            (("" (expand "abs")
              (("" (expand "+ ")
                (("" (expand "-")
                  (("" (assert)
                    (("" (expand "-")
                      (("" (expand "abs")
                        ((""
                          (expand "+
")
                          (("" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((- const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
    (p_integrable nonempty-type-eq-decl nil p_integrable_def nil)
    (p_integrable? const-decl "bool" p_integrable_def nil)
    (p formal-const-decl "{a: real | a >= 1}" p_integrable nil)
    (mu formal-const-decl "measure_type[T, S]" p_integrable 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]" p_integrable 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)
    (complex type-decl nil complex_types "complex_alt/")
    (T formal-type-decl nil p_integrable nil)
    (norm_add formula-decl nil p_integrable nil)
    (opp_p_integrable application-judgement "p_integrable" p_integrable
     nil)
    (norm const-decl "nnreal" p_integrable_def nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (abs const-decl "[T -> nonneg_real]" complex_fun_ops
         "complex_alt/")
    (- const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
    (- const-decl "complex" complex_types "complex_alt/")
    (- const-decl "complex" complex_types "complex_alt/")
    (+ const-decl "complex" complex_types "complex_alt/")
    (minus_real_is_real application-judgement "real" reals nil)
    (Im_rew formula-decl nil complex_types "complex_alt/")
    (Re_rew formula-decl nil complex_types "complex_alt/")
    (abs const-decl "nnreal" polar "complex_alt/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (+ const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
    (norm_opp formula-decl nil p_integrable nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des 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.