products/Sources/formale Sprachen/PVS/measure_integration/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: measure_completion_aux.prf   Sprache: Lisp

Original von: PVS©
(measure_completion_aux
 (almost_measurable?_TCC1 0
  (almost_measurable?_TCC1-1 nil 3458543747 ("" (assuming-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil measure_completion_aux 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)
    (sigma_algebra_union? const-decl "bool" subset_algebra_def nil)
    (is_countable const-decl "bool" countability "sets_aux/")
    (subset_algebra_complement? const-decl "bool" subset_algebra_def
     nil)
    (subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
    (member const-decl "bool" sets nil)
    (subset_algebra_complement application-judgement "(S)" measure_def
     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/"))
   nil))
 (empty_almost_measurable 0
  (empty_almost_measurable-1 nil 3423745840
   ("" (skosimp)
    (("" (expand "almost_measurable?")
      (("" (case "negligible_set?[T, S!1, m!1](emptyset[T])")
        (("1" (inst + "emptyset[T]" "emptyset[T]" "emptyset[T]")
          (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil))
            nil)
           ("2" (typepred "S!1")
            (("2" (expand "sigma_algebra?")
              (("2" (expand "subset_algebra_empty?")
                (("2" (expand "member") (("2" (flatten) nil nil)) nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide 2)
          (("2" (typepred "S!1")
            (("2" (typepred "m!1")
              (("2" (expand "measure?")
                (("2" (expand "sigma_algebra?")
                  (("2" (flatten)
                    (("2" (hide -2 -4 -5)
                      (("2" (expand "measure_empty?")
                        (("2" (expand "subset_algebra_empty?")
                          (("2" (expand "member")
                            (("2" (expand "negligible_set?")
                              (("2"
                                (inst + "emptyset[T]")
                                (("2"
                                  (expand "null_set?")
                                  (("2"
                                    (expand "measurable_set?")
                                    (("2"
                                      (expand "mu_fin?")
                                      (("2"
                                        (expand "mu")
                                        (("2"
                                          (replace -1)
                                          (("2"
                                            (assert)
                                            (("2"
                                              (replace -2)
                                              (("2" (grind) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((almost_measurable? const-decl "bool" measure_completion_aux nil)
    (null_set? const-decl "bool" measure_theory nil)
    (mu_fin? const-decl "bool" measure_props nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (subset? const-decl "bool" sets nil)
    (mu const-decl "nnreal" measure_props nil)
    (measurable_set? const-decl "bool" measure_space_def nil)
    (measure_empty? const-decl "bool" generalized_measure_def nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_setofsets
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (S!1 skolem-const-decl "sigma_algebra[T]" measure_completion_aux
     nil)
    (m!1 skolem-const-decl "measure_type[T, S!1]"
     measure_completion_aux nil)
    (negligible nonempty-type-eq-decl nil measure_theory nil)
    (member const-decl "bool" sets nil)
    (finite_union application-judgement "finite_set[T]"
     countable_setofsets "sets_aux/")
    (countable_difference application-judgement "countable_set[T]"
     countable_setofsets "sets_aux/")
    (finite_difference application-judgement "finite_set[T]"
     countable_setofsets "sets_aux/")
    (union const-decl "set" sets nil)
    (difference const-decl "set" sets nil)
    (subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil measure_completion_aux nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets 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)
    (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)
    (negligible_set? const-decl "bool" measure_theory nil)
    (emptyset const-decl "set" sets nil))
   shostak))
 (complement_almost_measurable 0
  (complement_almost_measurable-1 nil 3423745091
   ("" (skolem + ("_" "S!1" "m!1"))
    ((""
      (case "FORALL (X: set[T]):
        almost_measurable?(S!1, m!1)(X) =>
         almost_measurable?(S!1, m!1)(complement(X))")
      (("1" (skosimp)
        (("1" (split)
          (("1" (flatten)
            (("1" (inst - "X!1") (("1" (assert) nil nil)) nil)) nil)
           ("2" (flatten)
            (("2" (inst - "complement(X!1)")
              (("2" (rewrite "complement_complement")
                (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (skosimp)
          (("2" (expand "almost_measurable?")
            (("2" (skosimp)
              (("2" (replace -1)
                (("2" (hide -1)
                  (("2" (rewrite "difference_intersection")
                    (("2" (rewrite "demorgan2")
                      (("2" (rewrite "demorgan1")
                        (("2" (rewrite "complement_complement")
                          (("2" (rewrite "union_commutative")
                            (("2"
                              (rewrite "distribute_union_intersection")
                              (("2"
                                (lemma
                                 "demorgan2"
                                 ("a" "complement(N2!1)" "b" "N1!1"))
                                (("2"
                                  (rewrite "complement_complement")
                                  (("2"
                                    (rewrite
                                     "intersection_commutative")
                                    (("2"
                                      (rewrite
                                       "difference_intersection"
                                       -
                                       :dir
                                       rl)
                                      (("2"
                                        (replace -1 1 rl)
                                        (("2"
                                          (hide -1)
                                          (("2"
                                            (rewrite
                                             "difference_intersection"
                                             +
                                             :dir
                                             rl)
                                            (("2"
                                              (rewrite
                                               "union_commutative")
                                              (("2"
                                                (inst
                                                 +
                                                 "complement(Y!1)"
                                                 "N2!1"
                                                 "difference(N1!1, N2!1)")
                                                nil
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((complement const-decl "set" sets nil)
    (almost_measurable? const-decl "bool" measure_completion_aux 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)
    (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)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil measure_completion_aux nil)
    (complement_complement formula-decl nil sets_lemmas nil)
    (demorgan2 formula-decl nil sets_lemmas nil)
    (distribute_union_intersection formula-decl nil sets_lemmas nil)
    (negligible_union application-judgement "negligible" measure_theory
     nil)
    (subset_algebra_difference application-judgement "(S)" measure_def
     nil)
    (difference const-decl "set" sets nil)
    (negligible_intersection application-judgement "negligible"
     measure_theory nil)
    (intersection_commutative formula-decl nil sets_lemmas nil)
    (union_commutative formula-decl nil sets_lemmas nil)
    (intersection const-decl "set" sets nil)
    (demorgan1 formula-decl nil sets_lemmas nil)
    (subset_algebra_complement application-judgement "(S)" measure_def
     nil)
    (negligible nonempty-type-eq-decl nil measure_theory nil)
    (negligible_set? const-decl "bool" measure_theory nil)
    (union const-decl "set" sets nil)
    (difference_intersection formula-decl nil sets_lemmas nil))
   shostak))
 (Union_almost_measurable 0
  (Union_almost_measurable-1 nil 3423746160
   ("" (skosimp)
    ((""
      (name "SPLIT"
            "lambda (X:(XS!1)): choose({Z:[(S!1),negligible[T,S!1,m!1],negligible[T,S!1,m!1]] | X = difference(union(Z`1,Z`2),Z`3)})")
      (("1"
        (name "F1"
              "lambda X: if XS!1(X) THEN SPLIT(X)`1 else emptyset[T] endif")
        (("1"
          (name "F2"
                "lambda X: if XS!1(X) THEN SPLIT(X)`2 else emptyset[T] endif")
          (("1"
            (name "F3"
                  "lambda X: if XS!1(X) THEN SPLIT(X)`3 else emptyset[T] endif")
            (("1" (hide -4)
              (("1" (lemma "countable_image" ("f" "F1" "S" "XS!1"))
                (("1" (lemma "countable_image" ("f" "F2" "S" "XS!1"))
                  (("1" (lemma "countable_image" ("f" "F3" "S" "XS!1"))
                    (("1" (assert)
                      (("1" (name-replace "NS2" "image(F3)(XS!1)")
                        (("1" (name-replace "NS1" "image(F2)(XS!1)")
                          (("1" (name-replace "YS" "image(F1)(XS!1)")
                            (("1" (hide -4 -5 -6)
                              (("1"
                                (lemma
                                 "negligible_Union[T,S!1,m!1]"
                                 ("Z" "NS2"))
                                (("1"
                                  (lemma
                                   "negligible_Union[T,S!1,m!1]"
                                   ("Z" "NS1"))
                                  (("1"
                                    (assert)
                                    (("1"
                                      (split -1)
                                      (("1"
                                        (split -2)
                                        (("1"
                                          (typepred "S!1")
                                          (("1"
                                            (expand "sigma_algebra?")
                                            (("1"
                                              (flatten)
                                              (("1"
                                                (expand
                                                 "sigma_algebra_union?")
                                                (("1"
                                                  (inst - "YS")
                                                  (("1"
                                                    (assert)
                                                    (("1"
                                                      (split -3)
                                                      (("1"
                                                        (expand
                                                         "almost_measurable?"
                                                         1)
                                                        (("1"
                                                          (case
                                                           "forall (X:(XS!1)): X = difference(union(F1(X), F2(X)), F3(X))")
                                                          (("1"
                                                            (inst
                                                             +
                                                             "Union(YS)"
                                                             "Union(NS1)"
                                                             "difference(union(Union(YS),Union(NS1)),Union(XS!1))")
                                                            (("1"
                                                              (apply-extensionality
                                                               1
                                                               :hide?
                                                               t)
                                                              (("1"
                                                                (expand
                                                                 "union"
                                                                 1)
                                                                (("1"
                                                                  (expand
                                                                   "difference"
                                                                   1)
                                                                  (("1"
                                                                    (expand
                                                                     "member")
                                                                    (("1"
                                                                      (case-replace
                                                                       "Union(XS!1)(x!1)")
                                                                      (("1"
                                                                        (flatten)
                                                                        (("1"
                                                                          (expand
                                                                           "Union")
                                                                          (("1"
                                                                            (skosimp)
                                                                            (("1"
                                                                              (typepred
                                                                               "a!1")
                                                                              (("1"
                                                                                (inst
                                                                                 -
                                                                                 "a!1")
                                                                                (("1"
                                                                                  (replace
                                                                                   -3
                                                                                   -2)
                                                                                  (("1"
                                                                                    (expand
                                                                                     "difference"
                                                                                     -2)
                                                                                    (("1"
                                                                                      (expand
                                                                                       "union"
                                                                                       -2)
                                                                                      (("1"
                                                                                        (expand
                                                                                         "member")
                                                                                        (("1"
                                                                                          (flatten)
                                                                                          (("1"
                                                                                            (split
                                                                                             -2)
                                                                                            (("1"
                                                                                              (inst
                                                                                               2
                                                                                               "F1(a!1)")
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "YS")
                                                                                                (("1"
                                                                                                  (expand
                                                                                                   "image")
                                                                                                  (("1"
                                                                                                    (expand
                                                                                                     "image")
                                                                                                    (("1"
                                                                                                      (inst
                                                                                                       +
                                                                                                       "a!1")
                                                                                                      nil
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil)
                                                                                             ("2"
                                                                                              (inst
                                                                                               3
                                                                                               "F2(a!1)")
                                                                                              (("2"
                                                                                                (expand
                                                                                                 "NS1")
                                                                                                (("2"
                                                                                                  (expand
                                                                                                   "image")
                                                                                                  (("2"
                                                                                                    (expand
                                                                                                     "image")
                                                                                                    (("2"
                                                                                                      (inst
                                                                                                       +
                                                                                                       "a!1")
                                                                                                      nil
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (replace
                                                                         1
                                                                         2)
                                                                        (("2"
                                                                          (assert)
                                                                          (("2"
                                                                            (flatten)
                                                                            (("2"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (lemma
                                                               "negligible_subset[T,S!1,m!1]"
                                                               ("X"
                                                                "difference[T]
               (union[T](Union[T](YS), Union[T](NS1)), Union[T](XS!1))"
                                                                "E"
                                                                "union(Union(NS1),Union(NS2))"))
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (hide
                                                                   2)
                                                                  (("1"
                                                                    (expand
                                                                     "subset?"
                                                                     1)
                                                                    (("1"
                                                                      (expand
                                                                       "union"
                                                                       1)
                                                                      (("1"
                                                                        (expand
                                                                         "member")
                                                                        (("1"
                                                                          (skosimp*)
                                                                          (("1"
                                                                            (expand
                                                                             "difference"
                                                                             -1)
                                                                            (("1"
                                                                              (expand
                                                                               "member")
                                                                              (("1"
                                                                                (flatten)
                                                                                (("1"
                                                                                  (assert)
                                                                                  (("1"
                                                                                    (expand
                                                                                     "Union"
                                                                                     -1)
                                                                                    (("1"
                                                                                      (skosimp)
                                                                                      (("1"
                                                                                        (typepred
                                                                                         "a!1")
                                                                                        (("1"
                                                                                          (expand
                                                                                           "YS"
                                                                                           -1)
                                                                                          (("1"
                                                                                            (expand
                                                                                             "image")
                                                                                            (("1"
                                                                                              (expand
                                                                                               "image")
                                                                                              (("1"
                                                                                                (skosimp)
                                                                                                (("1"
                                                                                                  (typepred
                                                                                                   "x!2")
                                                                                                  (("1"
                                                                                                    (inst
                                                                                                     -
                                                                                                     "x!2")
                                                                                                    (("1"
                                                                                                      (expand
                                                                                                       "Union")
                                                                                                      (("1"
                                                                                                        (inst
                                                                                                         +
                                                                                                         "x!2")
                                                                                                        (("1"
                                                                                                          (replace
                                                                                                           -4
                                                                                                           1)
                                                                                                          (("1"
                                                                                                            (expand
                                                                                                             "difference"
                                                                                                             1)
                                                                                                            (("1"
                                                                                                              (expand
                                                                                                               "member")
                                                                                                              (("1"
                                                                                                                (expand
                                                                                                                 "union"
                                                                                                                 1)
                                                                                                                (("1"
                                                                                                                  (expand
                                                                                                                   "member")
                                                                                                                  (("1"
                                                                                                                    (replace
                                                                                                                     -2)
                                                                                                                    (("1"
                                                                                                                      (assert)
                                                                                                                      (("1"
                                                                                                                        (inst
                                                                                                                         2
                                                                                                                         "F3(x!2)")
                                                                                                                        (("1"
                                                                                                                          (expand
                                                                                                                           "NS2")
                                                                                                                          (("1"
                                                                                                                            (expand
                                                                                                                             "image")
                                                                                                                            (("1"
                                                                                                                              (expand
                                                                                                                               "image")
                                                                                                                              (("1"
                                                                                                                                (inst
                                                                                                                                 +
                                                                                                                                 "x!2")
                                                                                                                                nil
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (rewrite
                                                                 "negligible_union[T, S!1, m!1]"
                                                                 1)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (hide-all-but
                                                             (-9 1))
                                                            (("2"
                                                              (skosimp)
                                                              (("2"
                                                                (typepred
                                                                 "X!1")
                                                                (("2"
                                                                  (expand
                                                                   "F1")
                                                                  (("2"
                                                                    (expand
                                                                     "F2")
                                                                    (("2"
                                                                      (expand
                                                                       "F3")
                                                                      (("2"
                                                                        (name
                                                                         "SP"
                                                                         "SPLIT(X!1)")
                                                                        (("2"
                                                                          (replace
                                                                           -1)
                                                                          (("2"
                                                                            (expand
                                                                             "SPLIT")
                                                                            (("2"
                                                                              (case
                                                                               "nonempty?({Z: [(S!1), negligible[T, S!1, m!1], negligible[T, S!1, m!1]]
                | X!1 = difference(union(Z`1, Z`2), Z`3)})")
                                                                              (("1"
                                                                                (lemma
                                                                                 "choose_member"
                                                                                 ("a"
                                                                                  "{Z:
                   [(S!1), negligible[T, S!1, m!1],
                    negligible[T, S!1, m!1]]
                   | X!1 = difference(union(Z`1, Z`2), Z`3)}"))
                                                                                (("1"
                                                                                  (split
                                                                                   -1)
                                                                                  (("1"
                                                                                    (replace
                                                                                     -3)
                                                                                    (("1"
                                                                                      (expand
                                                                                       "member")
                                                                                      (("1"
                                                                                        (propax)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil)
                                                                                   ("2"
                                                                                    (expand
                                                                                     "nonempty?")
                                                                                    (("2"
                                                                                      (propax)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (hide
                                                                                 -1
                                                                                 2)
                                                                                (("2"
                                                                                  (expand
                                                                                   "nonempty?")
                                                                                  (("2"
                                                                                    (expand
                                                                                     "empty?")
                                                                                    (("2"
                                                                                      (expand
                                                                                       "member")
                                                                                      (("2"
                                                                                        (expand
                                                                                         "every")
                                                                                        (("2"
                                                                                          (inst
                                                                                           -3
                                                                                           "X!1")
                                                                                          (("2"
                                                                                            (expand
                                                                                             "almost_measurable?")
                                                                                            (("2"
                                                                                              (skosimp)
                                                                                              (("2"
                                                                                                (inst
                                                                                                 -
                                                                                                 "(Y!1,N1!1,N2!1)")
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (skosimp)
                                                        (("2"
                                                          (typepred
                                                           "x!1")
                                                          (("2"
                                                            (hide-all-but
                                                             (-1 1))
                                                            (("2"
                                                              (expand
                                                               "YS")
                                                              (("2"
                                                                (expand
                                                                 "image")
                                                                (("2"
                                                                  (expand
                                                                   "image")
                                                                  (("2"
                                                                    (skosimp)
                                                                    (("2"
                                                                      (expand
                                                                       "F1")
                                                                      (("2"
                                                                        (expand
                                                                         "SPLIT")
                                                                        (("2"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide-all-but (-5 1))
                                          (("2"
                                            (expand "every")
                                            (("2"
                                              (skosimp)
                                              (("2"
                                                (typepred "x!1")
                                                (("2"
                                                  (expand "NS2")
                                                  (("2"
                                                    (expand "image")
                                                    (("2"
                                                      (expand "image")
                                                      (("2"
                                                        (skosimp)
                                                        (("2"
                                                          (expand "F3")
                                                          (("2"
                                                            (expand
                                                             "SPLIT")
                                                            (("2"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (hide-all-but (-5 1))
                                        (("2"
                                          (expand "every")
                                          (("2"
                                            (skosimp)
                                            (("2"
                                              (typepred "x!1")
                                              (("2"
                                                (expand "NS1")
                                                (("2"
                                                  (expand "image")
                                                  (("2"
                                                    (expand "image")
                                                    (("2"
                                                      (skosimp)
                                                      (("2"
                                                        (expand "F2")
                                                        (("2"
                                                          (expand
                                                           "SPLIT")
                                                          (("2"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (skosimp)
        (("2" (typepred "X!1")
          (("2" (hide 2 -3)
            (("2" (expand "every")
              (("2" (inst - "X!1")
                (("2" (expand "nonempty?")
                  (("2" (expand "empty?")
                    (("2" (expand "member")
                      (("2" (expand "almost_measurable?")
                        (("2" (skosimp)
                          (("2" (inst - "(Y!1,N1!1,N2!1)") nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((choose const-decl "(p)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (union const-decl "set" sets nil)
    (difference const-decl "set" sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (negligible nonempty-type-eq-decl nil measure_theory nil)
    (negligible_set? const-decl "bool" measure_theory 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)
    (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)
    (set type-eq-decl nil sets 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)
    (T formal-type-decl nil measure_completion_aux nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (negligible_subset formula-decl nil measure_theory nil)
    (x!2 skolem-const-decl "(XS!1)" measure_completion_aux nil)
    (F3 skolem-const-decl "[set[T] -> set[T]]" measure_completion_aux
     nil)
    (NS2 skolem-const-decl "set[set[T]]" measure_completion_aux nil)
    (subset? const-decl "bool" sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (negligible_union judgement-tcc nil measure_theory nil)
    (F2 skolem-const-decl "[set[T] -> set[T]]" measure_completion_aux
     nil)
    (F1 skolem-const-decl "[set[T] -> setof[T]]" measure_completion_aux
     nil)
    (a!1 skolem-const-decl "(XS!1)" measure_completion_aux nil)
    (image const-decl "set[R]" function_image nil)
    (XS!1 skolem-const-decl "setofsets[T]" measure_completion_aux nil)
    (NS1 skolem-const-decl "set[set[T]]" measure_completion_aux nil)
    (m!1 skolem-const-decl "measure_type[T, S!1]"
     measure_completion_aux nil)
    (YS skolem-const-decl "set[setof[T]]" measure_completion_aux nil)
    (Union const-decl "set" sets nil)
    (S!1 skolem-const-decl "sigma_algebra[T]" measure_completion_aux
     nil)
    (choose_member formula-decl nil sets_lemmas nil)
    (every const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (SPLIT skolem-const-decl "[X: (XS!1) ->
   ({Z: [(S!1), negligible[T, S!1, m!1], negligible[T, S!1, m!1]] |
       X = difference(union(Z`1, Z`2), Z`3)})]" measure_completion_aux
     nil)
    (almost_measurable? const-decl "bool" measure_completion_aux nil)
    (member const-decl "bool" sets nil)
    (sigma_algebra_union? const-decl "bool" subset_algebra_def nil)
    (negligible_Union formula-decl nil measure_theory nil)
    (image const-decl "set[R]" function_image nil)
    (countable_image formula-decl nil countable_image "sets_aux/")
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (emptyset const-decl "set" sets nil))
   shostak))
 (completion_TCC1 0
  (completion_TCC1-1 nil 3422591880
   ("" (skosimp)
    (("" (expand "sigma_algebra?")
      (("" (split)
        (("1" (lemma "empty_almost_measurable" ("S" "S!1" "m" "m!1"))
          (("1" (expand "subset_algebra_empty?")
            (("1" (expand "member") (("1" (propax) nil nil)) nil))
            nil))
          nil)
         ("2"
          (lemma "complement_almost_measurable" ("S" "S!1" "m" "m!1"))
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.54 Sekunden  (vorverarbeitet)  ¤



zum Wurzelverzeichnis wechseln
Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen. Man kann per Verzeichnistruktur darin navigieren. Der Code wird farblich markiert angezeigt.
zum Wurzelverzeichnis wechseln
sprechenden Kalenders

Eigene Datei ansehen




Laden

Fehler beim Verzeichnis:


in der Quellcodebibliothek suchen

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff