products/Sources/formale Sprachen/Cobol/Test-Suite/SQL P/dml100-186/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: antlr4.xml   Sprache: Lisp

Original von: PVS©
(fubini_tonelli
 (fubini_tonelli_1 0
  (fubini_tonelli_1-1 nil 3453187626
   ("" (skosimp)
    (("" (lemma "fubini_tonelli_scaf1" ("h" "h!1"))
      (("" (replace 1 -1) (("" (propax) nil nil)) nil)) nil))
    nil)
   ((nu formal-const-decl "sigma_finite_measure[T2, S2]" fubini_tonelli
     nil)
    (mu formal-const-decl "sigma_finite_measure[T1, S1]" fubini_tonelli
     nil)
    (sigma_finite_measure nonempty-type-eq-decl nil measure_def nil)
    (sigma_finite_measure? const-decl "bool" 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)
    (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)
    (S2 formal-const-decl "sigma_algebra[T2]" fubini_tonelli nil)
    (S1 formal-const-decl "sigma_algebra[T1]" fubini_tonelli 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)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil fubini_tonelli nil)
    (T1 formal-type-decl nil fubini_tonelli nil)
    (nn_measurable nonempty-type-eq-decl nil measure_space nil)
    (nn_measurable? const-decl "bool" measure_space nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (fubini_tonelli_scaf1 formula-decl nil fubini_tonelli_scaf nil))
   shostak))
 (fubini_tonelli_2 0
  (fubini_tonelli_2-1 nil 3459562328
   ("" (skosimp)
    (("" (lemma "fubini_tonelli_scaf2" ("h" "h!1"))
      (("" (replace 1 -1) (("" (propax) nil nil)) nil)) nil))
    nil)
   ((nu formal-const-decl "sigma_finite_measure[T2, S2]" fubini_tonelli
     nil)
    (mu formal-const-decl "sigma_finite_measure[T1, S1]" fubini_tonelli
     nil)
    (sigma_finite_measure nonempty-type-eq-decl nil measure_def nil)
    (sigma_finite_measure? const-decl "bool" 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)
    (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)
    (S2 formal-const-decl "sigma_algebra[T2]" fubini_tonelli nil)
    (S1 formal-const-decl "sigma_algebra[T1]" fubini_tonelli 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)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil fubini_tonelli nil)
    (T1 formal-type-decl nil fubini_tonelli nil)
    (nn_measurable nonempty-type-eq-decl nil measure_space nil)
    (nn_measurable? const-decl "bool" measure_space nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (fubini_tonelli_scaf2 formula-decl nil fubini_tonelli_scaf nil))
   shostak))
 (fubini_tonelli_3_TCC1 0
  (fubini_tonelli_3_TCC1-1 nil 3431151472
   ("" (skosimp)
    (("" (typepred "g!1")
      (("" (lemma "fubini_tonelli_1" ("h" "g!1"))
        (("1" (assert)
          (("1"
            (lemma
             "nn_integrable_is_integrable[[T1, T2], sigma_times(S1, S2), m_times(mu, nu)]")
            (("1" (inst - "g!1") nil nil)) nil))
          nil)
         ("2" (expand "nn_measurable?")
          (("2" (split)
            (("1"
              (use "nn_integrable_is_measurable[[T1, T2], sigma_times(S1, S2), m_times(mu, nu)]")
              nil nil)
             ("2" (skosimp) (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nn_integrable nonempty-type-eq-decl nil nn_integral nil)
    (nn_integrable? const-decl "bool" nn_integral nil)
    (nu formal-const-decl "sigma_finite_measure[T2, S2]" fubini_tonelli
     nil)
    (mu formal-const-decl "sigma_finite_measure[T1, S1]" fubini_tonelli
     nil)
    (m_times const-decl
     "sigma_finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_measure nil)
    (sigma_finite_measure nonempty-type-eq-decl nil measure_def nil)
    (sigma_finite_measure? const-decl "bool" measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (S2 formal-const-decl "sigma_algebra[T2]" fubini_tonelli nil)
    (S1 formal-const-decl "sigma_algebra[T1]" fubini_tonelli nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     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)
    (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)
    (T2 formal-type-decl nil fubini_tonelli nil)
    (T1 formal-type-decl nil fubini_tonelli nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nn_integrable_is_measurable judgement-tcc nil nn_integral nil)
    (nn_integrable_is_integrable judgement-tcc nil integral nil)
    (fubini_tonelli_1 formula-decl nil fubini_tonelli nil)
    (nn_measurable? const-decl "bool" measure_space nil)
    (nn_measurable nonempty-type-eq-decl nil measure_space nil))
   nil))
 (fubini_tonelli_3 0
  (fubini_tonelli_3-1 nil 3459216640
   ("" (skosimp)
    (("" (typepred "g!1")
      ((""
        (lemma
         "nn_integrable_is_measurable[[T1,T2],sigma_times(S1,S2),m_times(mu,nu)]")
        (("" (inst - "g!1")
          (("" (lemma "fubini_tonelli_scaf1" ("h" "g!1"))
            (("1" (flatten)
              (("1" (split -3)
                (("1" (propax) nil nil)
                 ("2"
                  (lemma
                   "nn_integrable_is_integrable[[T1, T2], sigma_times(S1, S2), m_times(mu, nu)]")
                  (("2" (inst - "g!1") nil nil)) nil))
                nil))
              nil)
             ("2" (expand "nn_measurable?")
              (("2" (assert)
                (("2" (skosimp)
                  (("2" (typepred "g!1(x!1)") (("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nn_integrable nonempty-type-eq-decl nil nn_integral nil)
    (nn_integrable? const-decl "bool" nn_integral nil)
    (nu formal-const-decl "sigma_finite_measure[T2, S2]" fubini_tonelli
     nil)
    (mu formal-const-decl "sigma_finite_measure[T1, S1]" fubini_tonelli
     nil)
    (m_times const-decl
     "sigma_finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_measure nil)
    (sigma_finite_measure nonempty-type-eq-decl nil measure_def nil)
    (sigma_finite_measure? const-decl "bool" measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (S2 formal-const-decl "sigma_algebra[T2]" fubini_tonelli nil)
    (S1 formal-const-decl "sigma_algebra[T1]" fubini_tonelli nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     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)
    (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)
    (T2 formal-type-decl nil fubini_tonelli nil)
    (T1 formal-type-decl nil fubini_tonelli nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nn_integrable_is_integrable judgement-tcc nil integral nil)
    (fubini_tonelli_scaf1 formula-decl nil fubini_tonelli_scaf nil)
    (nn_measurable? const-decl "bool" measure_space nil)
    (nn_measurable nonempty-type-eq-decl nil measure_space nil)
    (nn_integrable_is_measurable judgement-tcc nil nn_integral nil))
   shostak))
 (fubini_tonelli_4_TCC1 0
  (fubini_tonelli_4_TCC1-1 nil 3431151472
   ("" (skosimp)
    (("" (typepred "g!1")
      (("" (lemma "fubini_tonelli_2" ("h" "g!1"))
        (("1" (assert)
          (("1"
            (lemma
             "nn_integrable_is_integrable[[T1, T2], sigma_times(S1, S2), m_times(mu, nu)]")
            (("1" (inst - "g!1") nil nil)) nil))
          nil)
         ("2" (expand "nn_measurable?")
          (("2"
            (use "nn_integrable_is_measurable[[T1, T2], sigma_times(S1, S2), m_times(mu, nu)]")
            (("2" (assert)
              (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nn_integrable nonempty-type-eq-decl nil nn_integral nil)
    (nn_integrable? const-decl "bool" nn_integral nil)
    (nu formal-const-decl "sigma_finite_measure[T2, S2]" fubini_tonelli
     nil)
    (mu formal-const-decl "sigma_finite_measure[T1, S1]" fubini_tonelli
     nil)
    (m_times const-decl
     "sigma_finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_measure nil)
    (sigma_finite_measure nonempty-type-eq-decl nil measure_def nil)
    (sigma_finite_measure? const-decl "bool" measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (S2 formal-const-decl "sigma_algebra[T2]" fubini_tonelli nil)
    (S1 formal-const-decl "sigma_algebra[T1]" fubini_tonelli nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     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)
    (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)
    (T2 formal-type-decl nil fubini_tonelli nil)
    (T1 formal-type-decl nil fubini_tonelli nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nn_integrable_is_measurable judgement-tcc nil nn_integral nil)
    (nn_integrable_is_integrable judgement-tcc nil integral nil)
    (fubini_tonelli_2 formula-decl nil fubini_tonelli nil)
    (nn_measurable? const-decl "bool" measure_space nil)
    (nn_measurable nonempty-type-eq-decl nil measure_space nil))
   nil))
 (fubini_tonelli_4 0
  (fubini_tonelli_4-1 nil 3459746299
   ("" (skosimp)
    (("" (typepred "g!1")
      ((""
        (lemma
         "nn_integrable_is_measurable[[T1, T2], sigma_times(S1, S2), m_times(mu, nu)]")
        (("" (inst - "g!1")
          (("" (lemma "fubini_tonelli_scaf2" ("h" "g!1"))
            (("1" (flatten)
              (("1" (split -3)
                (("1" (propax) nil nil)
                 ("2"
                  (lemma
                   "nn_integrable_is_integrable[[T1, T2], sigma_times(S1, S2), m_times(mu, nu)]")
                  (("2" (inst - "g!1") nil nil)) nil))
                nil))
              nil)
             ("2" (expand "nn_measurable?")
              (("2" (assert)
                (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nn_integrable nonempty-type-eq-decl nil nn_integral nil)
    (nn_integrable? const-decl "bool" nn_integral nil)
    (nu formal-const-decl "sigma_finite_measure[T2, S2]" fubini_tonelli
     nil)
    (mu formal-const-decl "sigma_finite_measure[T1, S1]" fubini_tonelli
     nil)
    (m_times const-decl
     "sigma_finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_measure nil)
    (sigma_finite_measure nonempty-type-eq-decl nil measure_def nil)
    (sigma_finite_measure? const-decl "bool" measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (S2 formal-const-decl "sigma_algebra[T2]" fubini_tonelli nil)
    (S1 formal-const-decl "sigma_algebra[T1]" fubini_tonelli nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     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)
    (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)
    (T2 formal-type-decl nil fubini_tonelli nil)
    (T1 formal-type-decl nil fubini_tonelli nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nn_integrable_is_integrable judgement-tcc nil integral nil)
    (fubini_tonelli_scaf2 formula-decl nil fubini_tonelli_scaf nil)
    (nn_measurable? const-decl "bool" measure_space nil)
    (nn_measurable nonempty-type-eq-decl nil measure_space nil)
    (nn_integrable_is_measurable judgement-tcc nil nn_integral nil))
   shostak)))


¤ Dauer der Verarbeitung: 0.5 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff