Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: monotone_classes.pvs Sprache: Lisp

Original von: PVS^©

(measure_equality
(measure_eq_isf? 0
  (measure_eq_isf?-1 nil 3459229994
   (""
    (case "FORALL (f: [T -> real], mu, nu: measure_type[T, S]):
        (FORALL E: x_eq(mu(E), nu(E))) & isf?[T, S, mu](f) => isf?[T, S, nu](f)")
    (("1" (skosimp)
      (("1" (inst-cp - "f!1" "mu!1" "nu!1")
        (("1" (inst - "f!1" "nu!1" "mu!1")
          (("1" (replace -3)
            (("1" (split 1)
              (("1" (propax) nil nil)
               ("2" (flatten)
                (("2" (assert)
                  (("2" (hide-all-but (-3 2))
                    (("2" (skosimp)
                      (("2" (inst - "E!1")
                        (("2" (expand "x_eq")
                          (("2" (flatten)
                            (("2" (assert)
                              (("2"
                                (flatten)
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (hide 2)
      (("2" (skolem + ("_" "mu!1" "nu!1"))
        (("2" (case-replace "(FORALL E: x_eq(mu!1(E), nu!1(E)))")
          (("1"
            (case "forall (f:isf[T, S, mu!1]): isf?[T, S, nu!1](f)")
            (("1" (skosimp) (("1" (inst - "f!1") nil nil)) nil)
             ("2" (hide 2)
              (("2" (skosimp)
                (("2" (typepred "f!1")
                  (("2"
                    (lemma "isf_induction[T, S, mu!1]"
                     ("P" "isf?[T, S, nu!1]"))
                    (("2" (expand "restrict")
                      (("2" (inst - "f!1")
                        (("2" (assert)
                          (("2" (hide 2)
                            (("2" (rewrite "isf_zero[T,S,nu!1]")
                              (("2"
                                (skosimp)
                                (("2"
                                  (typepred "E!1")
                                  (("2"
                                    (inst - "E!1")
                                    (("1"
                                      (rewrite "isf_add[T,S,nu!1]" 1)
                                      (("1"
                                        (hide 2)
                                        (("1"
                                          (rewrite
                                           "isf_scal[T,S,nu!1]"
                                           1)
                                          (("1"
                                            (hide 2)
                                            (("1"
                                              (rewrite
                                               "isf_phi[T,S,nu!1]"
                                               1)
                                              (("1"
                                                (hide 2)
                                                (("1"
                                                  (expand "mu_fin?")
                                                  (("1"
                                                    (expand "x_eq")
                                                    (("1"
                                                      (flatten)
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (expand "measurable_set?")
                                      (("2" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (assert)
            (("2" (replace 1 2)
              (("2" (hide 1) (("2" (skosimp) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((NOT const-decl "[bool -> bool]" booleans nil)
    (isf_zero formula-decl nil isf nil) (set type-eq-decl nil sets nil)
    (measurable_set? const-decl "bool" measure_space_def nil)
    (measurable_set nonempty-type-eq-decl nil measure_space_def nil)
    (mu_fin? const-decl "bool" measure_props nil)
    (isf_phi application-judgement "isf" integral nil)
    (phi const-decl "nat" measure_space nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (isf_add judgement-tcc nil isf nil)
    (isf_scal judgement-tcc nil isf nil)
    (isf_phi judgement-tcc nil isf nil)
    (E!1 skolem-const-decl "(mu_fin?)" measure_equality nil)
    (restrict const-decl "R" restrict nil)
    (pred type-eq-decl nil defined_types nil)
    (isf_induction formula-decl nil isf nil)
    (f!1 skolem-const-decl "[T -> real]" measure_equality nil)
    (mu!1 skolem-const-decl "measure_type[T, S]" measure_equality nil)
    (isf nonempty-type-eq-decl nil isf nil)
    (T formal-type-decl nil measure_equality nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S formal-const-decl "sigma_algebra" measure_equality nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (measure? const-decl "bool" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (x_eq const-decl "bool" extended_nnreal "extended_nnreal/")
    (isf? const-decl "bool" isf nil))
   shostak))
(measure_eq_isf_TCC1 0
  (measure_eq_isf_TCC1-1 nil 3459230996
   ("" (skosimp)
    (("" (assert)
      ((""
        (lemma "measure_eq_isf?" ("mu" "mu!1" "nu" "nu!1" "f" "f!1"))
        (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((measure_eq_isf? formula-decl nil measure_equality nil)
    (T formal-type-decl nil measure_equality nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S formal-const-decl "sigma_algebra" measure_equality nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (measure? const-decl "bool" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil))
   nil))
(measure_eq_isf_TCC2 0
  (measure_eq_isf_TCC2-1 nil 3459230996
   ("" (skosimp)
    (("" (assert)
      ((""
        (lemma "measure_eq_isf?" ("mu" "mu!1" "nu" "nu!1" "f" "f!1"))
        (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((measure_eq_isf? formula-decl nil measure_equality nil)
    (T formal-type-decl nil measure_equality nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S formal-const-decl "sigma_algebra" measure_equality nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (measure? const-decl "bool" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil))
   nil))
(measure_eq_isf 0
  (measure_eq_isf-1 nil 3459230997
   ("" (skolem + ("_" "mu!1" "nu!1"))
    (("" (case-replace "FORALL E: x_eq(mu!1(E), nu!1(E))")
      (("1"
        (case "forall (f:isf[T, S, mu!1]): isf_integral[T, S, mu!1](f) = isf_integral[T, S, nu!1](f)")
        (("1" (skosimp)
          (("1" (split -3)
            (("1" (inst - "f!1") nil nil)
             ("2"
              (lemma "measure_eq_isf?"
               ("mu" "mu!1" "nu" "nu!1" "f" "f!1"))
              (("2" (assert)
                (("2" (split)
                  (("1" (inst - "f!1") nil nil) ("2" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide 2)
          (("2" (skosimp)
            (("2"
              (lemma "isf_induction[T,S,mu!1]"
               ("P"
                "lambda (f:isf[T, S, mu!1]): isf_integral[T, S, mu!1](f) = isf_integral[T, S, nu!1](f)"))
              (("2" (inst - "f!1")
                (("2" (assert)
                  (("2" (hide 2)
                    (("2" (rewrite "isf_integral_zero[T, S, mu!1]")
                      (("2" (rewrite "isf_integral_zero[T, S, nu!1]")
                        (("2" (skosimp)
                          (("2"
                            (rewrite "isf_integral_add[T, S, nu!1]")
                            (("1"
                              (rewrite "isf_integral_add[T, S, mu!1]")
                              (("1"
                                (replace -1)
                                (("1"
                                  (assert)
                                  (("1"
                                    (hide -1)
                                    (("1"
                                      (rewrite
                                       "isf_integral_scal[T, S, mu!1]")
                                      (("1"
                                        (rewrite
                                         "isf_integral_scal[T, S, nu!1]")
                                        (("1"
                                          (rewrite
                                           "isf_integral_phi[T,S,mu!1]")
                                          (("1"
                                            (rewrite
                                             "isf_integral_phi[T,S,nu!1]")
                                            (("1"
                                              (inst - "E!1")
                                              (("1"
                                                (expand "x_eq")
                                                (("1"
                                                  (expand "mu")
                                                  (("1"
                                                    (flatten)
                                                    (("1"
                                                      (typepred "E!1")
                                                      (("1"
                                                        (expand
                                                         "mu_fin?")
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (typepred "E!1")
                                              (("2"
                                                (expand "mu_fin?")
                                                (("2"
                                                  (inst - "E!1")
                                                  (("2"
                                                    (expand "x_eq")
                                                    (("2"
                                                      (flatten)
                                                      (("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (rewrite
                                           "isf_phi[T, S, nu!1]")
                                          (("2"
                                            (typepred "E!1")
                                            (("2"
                                              (expand "mu_fin?")
                                              (("2"
                                                (inst - "E!1")
                                                (("2"
                                                  (expand "x_eq")
                                                  (("2"
                                                    (flatten)
                                                    (("2"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (rewrite "isf_scal[T, S, mu!1]")
                                nil
                                nil))
                              nil)
                             ("2" (rewrite "isf_scal[T, S, nu!1]")
                              (("2"
                                (rewrite "isf_phi[T, S, nu!1]")
                                (("2"
                                  (typepred "E!1")
                                  (("2"
                                    (expand "mu_fin?")
                                    (("2"
                                      (inst - "E!1")
                                      (("2"
                                        (expand "x_eq")
                                        (("2"
                                          (flatten)
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("3" (skosimp)
          (("3"
            (lemma "measure_eq_isf?"
             ("mu" "mu!1" "nu" "nu!1" "f" "f!1"))
            (("3" (assert) nil nil)) nil))
          nil))
        nil)
       ("2" (replace 1 2)
        (("2" (hide 1) (("2" (skosimp) nil nil)) nil)) nil))
      nil))
    nil)
   ((T formal-type-decl nil measure_equality nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S formal-const-decl "sigma_algebra" measure_equality 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/")
    (x_eq const-decl "bool" extended_nnreal "extended_nnreal/")
    (measure? const-decl "bool" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (pred type-eq-decl nil defined_types nil)
    (isf_induction formula-decl nil isf nil)
    (isf_integral_zero formula-decl nil isf nil)
    (isf_integral_scal formula-decl nil isf nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (isf_phi judgement-tcc nil isf nil)
    (isf_integral_phi formula-decl nil isf nil)
    (mu const-decl "nnreal" measure_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (isf_scal judgement-tcc nil isf nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (mu_fin? const-decl "bool" measure_props nil)
    (measurable_set nonempty-type-eq-decl nil measure_space_def nil)
    (measurable_set? const-decl "bool" measure_space_def nil)
    (phi const-decl "nat" measure_space nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (set type-eq-decl nil sets nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (isf_integral_add formula-decl nil isf nil)
    (isf_phi application-judgement "isf" integral nil)
    (measure_eq_isf? formula-decl nil measure_equality nil)
    (isf? const-decl "bool" isf nil)
    (isf nonempty-type-eq-decl nil isf nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (isf_integral const-decl "real" isf nil))
   shostak))
(measure_eq_nn_integrable? 0
  (measure_eq_nn_integrable?-1 nil 3459232122
   (""
    (case "FORALL (g: [T -> nnreal], mu, nu: measure_type[T, S]):
        (FORALL E: x_eq(mu(E), nu(E)))&nn_integrable?[T, S, mu](g) => nn_integrable?[T, S, nu](g)")
    (("1" (skosimp)
      (("1" (split 1)
        (("1" (flatten)
          (("1" (inst - "g!1" "mu!1" "nu!1") (("1" (assert) nil nil))
            nil))
          nil)
         ("2" (flatten)
          (("2" (inst - "g!1" "nu!1" "mu!1")
            (("2" (assert)
              (("2" (hide-all-but (-2 2))
                (("2" (skosimp)
                  (("2" (inst - "E!1")
                    (("2" (expand "x_eq")
                      (("2" (flatten)
                        (("2" (assert)
                          (("2" (flatten) (("2" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (hide 2)
      (("2" (skosimp)
        (("2" (expand "nn_integrable?")
          (("2" (skosimp)
            (("2" (inst + "u!1")
              (("1" (assert)
                (("1" (expand "o ")
                  (("1"
                    (case-replace
                     "(LAMBDA (n: nat): isf_integral[T,S,mu!1](u!1(n)))=LAMBDA (n: nat): isf_integral[T,S,nu!1](u!1(n))")
                    (("1" (apply-extensionality :hide? t)
                      (("1" (hide -3 2 -2)
                        (("1" (typepred "u!1(x!1)")
                          (("1"
                            (lemma "measure_eq_isf"
                             ("mu" "mu!1" "nu" "nu!1" "f" "u!1(x!1)"))
                            (("1" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (skosimp)
                        (("2" (typepred "u!1(n!1)")
                          (("2"
                            (lemma "measure_eq_isf?"
                             ("nu" "nu!1" "mu" "mu!1" "f" "u!1(n!1)"))
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("2" (skosimp)
                      (("2"
                        (lemma "measure_eq_isf?"
                         ("nu" "nu!1" "mu" "mu!1" "f" "u!1(n!1)"))
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (typepred "u!1")
                (("2" (expand "increasing_nn_isf?")
                  (("2" (assert)
                    (("2" (skolem + "n!1")
                      (("2" (typepred "u!1(n!1)")
                        (("2" (expand "nn_isf?")
                          (("2" (assert)
                            (("2" (split)
                              (("1"
                                (lemma
                                 "measure_eq_isf?"
                                 ("mu"
                                  "mu!1"
                                  "nu"
                                  "nu!1"
                                  "f"
                                  "u!1(n!1)"))
                                (("1" (assert) nil nil))
                                nil)
                               ("2" (propax) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((u!1 skolem-const-decl "increasing_nn_isf[T, S, mu!1]"
     measure_equality nil)
    (increasing_nn_isf nonempty-type-eq-decl nil nn_integral nil)
    (increasing_nn_isf? const-decl "bool" nn_integral nil)
    (sequence type-eq-decl nil sequences nil)
    (nn_isf nonempty-type-eq-decl nil nn_integral nil)
    (nn_isf? const-decl "bool" nn_integral nil)
    (isf nonempty-type-eq-decl nil isf nil)
    (mu!1 skolem-const-decl "measure_type[T, S]" measure_equality nil)
    (isf? const-decl "bool" isf nil)
    (nu!1 skolem-const-decl "measure_type[T, S]" measure_equality nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (O const-decl "T3" function_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (measure_eq_isf formula-decl nil measure_equality nil)
    (measure_eq_isf? formula-decl nil measure_equality nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (isf_integral const-decl "real" isf nil)
    (T formal-type-decl nil measure_equality nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S formal-const-decl "sigma_algebra" measure_equality nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (measure? const-decl "bool" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (x_eq const-decl "bool" extended_nnreal "extended_nnreal/")
    (nn_integrable? const-decl "bool" nn_integral nil))
   shostak))
(measure_eq_nn_integral_TCC1 0
  (measure_eq_nn_integral_TCC1-1 nil 3459232044
   ("" (skosimp)
    (("" (split)
      (("1" (propax) nil nil)
       ("2"
        (lemma "measure_eq_nn_integrable?"
         ("mu" "mu!1" "nu" "nu!1" "g" "g!1"))
        (("2" (assert) nil nil)) nil))
      nil))
    nil)
   ((measure_eq_nn_integrable? formula-decl nil measure_equality nil)
    (T formal-type-decl nil measure_equality nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S formal-const-decl "sigma_algebra" measure_equality nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (measure? const-decl "bool" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil))
   nil))
(measure_eq_nn_integral_TCC2 0
  (measure_eq_nn_integral_TCC2-1 nil 3459232044
   ("" (skosimp)
    (("" (assert)
      ((""
        (lemma "measure_eq_nn_integrable?"
         ("mu" "mu!1" "nu" "nu!1" "g" "g!1"))
        (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((measure_eq_nn_integrable? formula-decl nil measure_equality nil)
    (T formal-type-decl nil measure_equality nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S formal-const-decl "sigma_algebra" measure_equality nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (measure? const-decl "bool" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil))
   nil))
(measure_eq_nn_integral 0
  (measure_eq_nn_integral-1 nil 3459232639
   (""
    (case "FORALL (g: [T -> nnreal], mu, nu: measure_type[T, S]):
        (FORALL E: x_eq(mu(E), nu(E))) AND
         nn_integrable?[T, S, mu](g)
         => (nn_integral[T, S, mu](g) = nn_integral[T, S, nu](g))")
    (("1" (skosimp)
      (("1" (split -3)
        (("1" (inst - "g!1" "mu!1" "nu!1") (("1" (assert) nil nil))
          nil)
         ("2"
          (lemma "measure_eq_nn_integrable?"
           ("mu" "mu!1" "nu" "nu!1" "g" "g!1"))
          (("2" (assert)
            (("2" (replace -4 -1)
              (("2" (inst - "g!1" "mu!1" "nu!1")
                (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (hide 2)
      (("2" (skosimp)
        (("2"
          (lemma "measure_eq_nn_integrable?"
           ("mu" "mu!1" "nu" "nu!1" "g" "g!1"))
          (("2" (assert)
            (("2" (split)
              (("1" (lemma "nn_integral_def[T,S,nu!1]" ("f" "g!1"))
                (("1" (lemma "nn_integral_def[T,S,mu!1]" ("f" "g!1"))
                  (("1" (skosimp*)
                    (("1"
                      (name-replace "LHS"
                       "nn_integral[T, S, mu!1](g!1)")
                      (("1"
                        (name-replace "RHS"
                         "nn_integral[T, S, nu!1](g!1)")
                        (("1"
                          (lemma "nn_convergence[T,S,mu!1]"
                           ("u1" "u!1" "u2" "u!2" "f" "g!1"))
                          (("1" (replace -2)
                            (("1" (replace -4)
                              (("1"
                                (split -1)
                                (("1"
                                  (flatten)
                                  (("1"
                                    (case-replace
                                     "isf_integral[T, S, nu!1] o u!2 = isf_integral[T, S, mu!1] o u!2")
                                    (("1"
                                      (hide -1)
                                      (("1"
                                        (lemma
                                         "hausdorff_convergence.limit_def"
                                         ("v"
                                          "isf_integral[T, S, mu!1] o u!2"
                                          "l"
                                          "RHS"))
                                        (("1"
                                          (assert)
                                          (("1"
                                            (replace -1)
                                            (("1"
                                              (lemma
                                               "hausdorff_convergence.limit_def"
                                               ("v"
                                                "isf_integral[T, S, mu!1] o u!1"
                                                "l"
                                                "LHS"))
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (apply-extensionality :hide? t)
                                      (("2"
                                        (hide 2)
                                        (("2"
                                          (expand "o ")
                                          (("2"
                                            (lemma
                                             "measure_eq_isf?"
                                             ("mu"
                                              "mu!1"
                                              "nu"
                                              "nu!1"
                                              "f"
                                              "u!2(x!1)"))
                                            (("2"
                                              (assert)
                                              (("2"
                                                (split)
                                                (("1"
                                                  (lemma
                                                   "measure_eq_isf"
                                                   ("mu"
                                                    "mu!1"
                                                    "nu"
                                                    "nu!1"
                                                    "f"
                                                    "u!2(x!1)"))
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (expand "convergent?")
                                  (("2" (inst + "LHS") nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (hide-all-but (-6 1))
                            (("2" (typepred "u!2")
                              (("2"
                                (expand "increasing_nn_isf?")
                                (("2"
                                  (replace -1)
                                  (("2"
                                    (skosimp)
                                    (("2"
                                      (typepred "u!2(x1!1)")
                                      (("2"
                                        (expand "nn_isf?")
                                        (("2"
                                          (replace -2)
                                          (("2"
                                            (lemma
                                             "measure_eq_isf?"
                                             ("mu"
                                              "mu!1"
                                              "nu"
                                              "nu!1"
                                              "f"
                                              "u!2(x1!1)"))
                                            (("2" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (propax) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (hide 2)
      (("3" (skosimp)
        (("3"
          (lemma "measure_eq_nn_integrable?"
           ("nu" "nu!1" "mu" "mu!1" "g" "g!1"))
          (("3" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((increasing_nn_isf nonempty-type-eq-decl nil nn_integral nil)
    (increasing_nn_isf? const-decl "bool" nn_integral nil)
    (sequence type-eq-decl nil sequences nil)
    (nn_isf nonempty-type-eq-decl nil nn_integral nil)
    (nn_isf? const-decl "bool" nn_integral nil)
    (isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (nn_convergence formula-decl nil nn_integral nil)
    (measure_eq_isf formula-decl nil measure_equality nil)
    (measure_eq_isf? formula-decl nil measure_equality nil)
    (limit_def formula-decl nil hausdorff_convergence "topology/")
    (convergent? const-decl "bool" topological_convergence "topology/")
    (convergent type-eq-decl nil topological_convergence "topology/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (metric_induced_topology const-decl "setofsets[T]" metric_space_def
     "metric_space/")
    (O const-decl "T3" function_props nil)
    (isf_integral const-decl "real" isf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (nn_integral_def formula-decl nil nn_integral nil)
    (measure_eq_nn_integrable? formula-decl nil measure_equality nil)
    (T formal-type-decl nil measure_equality nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S formal-const-decl "sigma_algebra" measure_equality nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (measure? const-decl "bool" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (x_eq const-decl "bool" extended_nnreal "extended_nnreal/")
    (nn_integrable? const-decl "bool" nn_integral nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nn_integrable nonempty-type-eq-decl nil nn_integral nil)
    (nn_integral const-decl "nnreal" nn_integral nil))
   shostak))
(measure_eq_integrable? 0
  (measure_eq_integrable?-1 nil 3459234013
   ("" (skosimp)
    (("" (rewrite "integrable_pm_def[T, S, mu!1]")
      (("" (rewrite "integrable_pm_def[T, S, nu!1]")
        ((""
          (lemma "measure_eq_nn_integrable?"
           ("nu" "nu!1" "mu" "mu!1" "g" "plus(f!1)"))
          ((""
            (lemma "measure_eq_nn_integrable?"
             ("nu" "nu!1" "mu" "mu!1" "g" "minus(f!1)"))
            (("" (replace -3)
              (("" (assert)
                (("" (split 1)
                  (("1" (flatten)
                    (("1" (assert)
                      (("1"
                        (lemma
                         "nn_integrable_is_nn_integrable[T, S, mu!1]"
                         ("f" "plus(f!1)"))
                        (("1" (split -1)
                          (("1" (assert)
                            (("1"
                              (lemma
                               "nn_integrable_is_nn_integrable[T, S, mu!1]"
                               ("f" "minus(f!1)"))
                              (("1"
                                (split)
                                (("1"
                                  (assert)
                                  (("1"
                                    (hide-all-but (-5 -7 1))
                                    (("1"
                                      (lemma
                                       "nn_integrable_is_integrable[T,S,nu!1]")
                                      (("1"
                                        (inst-cp - "minus(f!1)")
                                        (("1"
                                          (inst - "plus(f!1)")
                                          (("1" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide-all-but 1)
                                  (("2" (grind) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (hide-all-but 1)
                            (("2" (grind) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (flatten)
                    (("2"
                      (lemma
                       "nn_integrable_is_nn_integrable[T, S, nu!1]"
                       ("f" "minus(f!1)"))
                      (("1"
                        (lemma
                         "nn_integrable_is_nn_integrable[T, S, nu!1]"
                         ("f" "plus(f!1)"))
                        (("1" (split)
                          (("1" (split)
                            (("1" (assert)
                              (("1"
                                (lemma
                                 "nn_integrable_is_integrable[T,S,mu!1]")
                                (("1"
                                  (inst-cp - "minus(f!1)")
                                  (("1"
                                    (inst - "plus(f!1)")
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide-all-but 1)
                              (("2" (grind) nil nil)) nil))
                            nil)
                           ("2" (hide-all-but 1)
                            (("2" (grind) nil nil)) nil))
                          nil)
                         ("2" (propax) nil nil))
                        nil)
                       ("2" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((integrable_pm_def formula-decl nil integral nil)
    (T formal-type-decl nil measure_equality nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S formal-const-decl "sigma_algebra" measure_equality nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (measure? const-decl "bool" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (plus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
    (measure_eq_nn_integrable? formula-decl nil measure_equality nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nn_integrable_is_integrable judgement-tcc nil integral nil)
    (nn_integrable? const-decl "bool" nn_integral nil)
    (nn_integrable nonempty-type-eq-decl nil nn_integral nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nn_integrable_is_nn_integrable formula-decl nil integral nil)
    (integrable? const-decl "bool" integral nil)
    (integrable nonempty-type-eq-decl nil integral nil)
    (minus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/"))
   shostak))
(measure_eq_integral_TCC1 0
  (measure_eq_integral_TCC1-1 nil 3459233920
   ("" (skosimp)
    ((""
      (lemma "measure_eq_integrable?"
       ("nu" "nu!1" "mu" "mu!1" "f" "f!1"))
      (("" (assert)
        (("" (split) (("1" (propax) nil nil) ("2" (propax) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (S formal-const-decl "sigma_algebra" measure_equality nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (T formal-type-decl nil measure_equality nil)
    (measure_eq_integrable? formula-decl nil measure_equality nil))
   nil))
(measure_eq_integral_TCC2 0
  (measure_eq_integral_TCC2-1 nil 3459233920
   ("" (skosimp)
    ((""
      (lemma "measure_eq_integrable?"
       ("nu" "nu!1" "mu" "mu!1" "f" "f!1"))
      (("" (assert)
        (("" (split) (("1" (propax) nil nil) ("2" (propax) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (S formal-const-decl "sigma_algebra" measure_equality nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (T formal-type-decl nil measure_equality nil)
    (measure_eq_integrable? formula-decl nil measure_equality nil))
   nil))
(measure_eq_integral 0
  (measure_eq_integral-1 nil 3459234384
   (""
    (case "FORALL (f: [T -> real], mu, nu: measure_type[T, S]):
        (FORALL E: x_eq(mu(E), nu(E))) AND integrable?[T, S, mu](f)
         => (integral[T, S, mu](f) = integral[T, S, nu](f))")
    (("1" (skosimp)
      (("1" (split -3)
        (("1" (inst - "f!1" "mu!1" "nu!1") (("1" (assert) nil nil))
          nil)
         ("2"
          (lemma "measure_eq_integrable?"
           ("mu" "mu!1" "nu" "nu!1" "f" "f!1"))
          (("2" (assert)
            (("2" (split -1)
              (("1" (inst - "f!1" "mu!1" "nu!1")
                (("1" (assert) nil nil)) nil)
               ("2" (propax) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (hide 2)
      (("2" (skosimp)
        (("2" (rewrite "integral_pm[T, S, mu!1]")
          (("2" (rewrite "integral_pm[T, S, nu!1]")
            (("2"
              (lemma "measure_eq_integrable?"
               ("mu" "mu!1" "nu" "nu!1" "f" "f!1"))
              (("2" (assert)
                (("2" (replace -2)
                  (("2" (rewrite "integrable_pm_def[T, S, nu!1]")
                    (("2" (rewrite "integrable_pm_def[T, S, mu!1]")
                      (("2" (flatten)
                        (("2"
                          (lemma
                           "nn_integrable_is_nn_integrable[T,S,mu!1]")
                          (("2" (inst-cp - "plus(f!1)")
                            (("2" (inst - "minus(f!1)")
                              (("2"
                                (lemma
                                 "nn_integrable_is_nn_integrable[T,S,nu!1]")
                                (("2"
                                  (inst-cp - "plus(f!1)")
                                  (("2"
                                    (inst - "minus(f!1)")
                                    (("2"
                                      (case-replace
                                       "FORALL (x: T): minus(f!1)(x) >= 0")
                                      (("1"
                                        (case-replace
                                         "FORALL (x: T): plus(f!1)(x) >= 0")
                                        (("1"
                                          (rewrite
                                           "integral_nn[T,S,mu!1]")
                                          (("1"
                                            (rewrite
                                             "integral_nn[T,S,mu!1]")
                                            (("1"
                                              (rewrite
                                               "integral_nn[T,S,nu!1]")
                                              (("1"
                                                (rewrite
                                                 "integral_nn[T,S,nu!1]")
                                                (("1"
                                                  (lemma
                                                   "measure_eq_nn_integral"
                                                   ("mu"
                                                    "mu!1"
                                                    "nu"
                                                    "nu!1"
                                                    "g"
                                                    "plus(f!1)"))
                                                  (("1"
                                                    (lemma
                                                     "measure_eq_nn_integral"
                                                     ("mu"
                                                      "mu!1"
                                                      "nu"
                                                      "nu!1"
                                                      "g"
                                                      "minus(f!1)"))
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (replace -11)
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide-all-but 1)
                                          (("2" (grind) nil nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (hide-all-but 1)
                                        (("2" (grind) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (hide 2)
      (("3" (skosimp)
        (("3"
          (lemma "measure_eq_integrable?"
           ("mu" "mu!1" "nu" "nu!1" "f" "f!1"))
          (("3" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((integral_pm formula-decl nil integral nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nn_integrable_is_nn_integrable formula-decl nil integral nil)
    (minus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (nn_integrable nonempty-type-eq-decl nil nn_integral nil)
    (nn_integrable? const-decl "bool" nn_integral nil)
    (integral_nn formula-decl nil integral nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (measure_eq_nn_integral formula-decl nil measure_equality nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (plus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
    (integrable_pm_def formula-decl nil integral nil)
    (measure_eq_integrable? formula-decl nil measure_equality nil)
    (T formal-type-decl nil measure_equality nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S formal-const-decl "sigma_algebra" measure_equality nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (measure? const-decl "bool" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (x_eq const-decl "bool" extended_nnreal "extended_nnreal/")
    (integrable? const-decl "bool" integral nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (integrable nonempty-type-eq-decl nil integral nil)
    (integral const-decl "real" integral nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.49 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.