Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: outer_measure.prf Sprache: Lisp

Original von: PVS^©

(outer_measure
(IMP_ast_def_TCC1 0
  (IMP_ast_def_TCC1-1 nil 3458456184
   ("" (typepred "A")
    (("" (expand "subset_algebra?")
      (("" (flatten)
        (("" (expand "subset_algebra_empty?")
          (("" (expand "nonempty?")
            (("" (expand "member")
              (("" (expand "empty?")
                (("" (inst - "emptyset[T]")
                  (("" (expand "member") (("" (propax) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
    (member const-decl "bool" sets nil)
    (emptyset const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (subset_algebra_emptyset name-judgement "(S)" outer_measure nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil outer_measure nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (subset_algebra? const-decl "bool" subset_algebra_def nil)
    (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (A formal-const-decl "subset_algebra" outer_measure nil))
   nil))
(IMP_ast_def_TCC2 0
  (IMP_ast_def_TCC2-1 nil 3458456184
   ("" (typepred "A")
    (("" (expand "subset_algebra?")
      (("" (flatten)
        (("" (expand "subset_algebra_empty?")
          (("" (assert)
            (("" (expand "member") (("" (propax) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (subset_algebra_emptyset name-judgement "(S)" outer_measure 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 outer_measure nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (subset_algebra? const-decl "bool" subset_algebra_def nil)
    (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (A formal-const-decl "subset_algebra" outer_measure nil))
   nil))
(IMP_ast_def_TCC3 0
  (IMP_ast_def_TCC3-1 nil 3458456184
   ("" (lemma "subset_algebra_fullset") (("" (propax) nil nil)) nil)
   ((subset_algebra_fullset judgement-tcc nil subset_algebra nil)
    (T formal-type-decl nil outer_measure 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)
    (subset_algebra? const-decl "bool" subset_algebra_def nil)
    (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (A formal-const-decl "subset_algebra" outer_measure nil))
   nil))
(IMP_ast_def_TCC4 0
  (IMP_ast_def_TCC4-1 nil 3458456184
   ("" (skosimp)
    (("" (lemma "subset_algebra_intersection")
      (("" (inst - "a!1" "b!1") nil nil)) nil))
    nil)
   ((A formal-const-decl "subset_algebra" outer_measure nil)
    (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (subset_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 outer_measure nil)
    (subset_algebra_intersection judgement-tcc nil subset_algebra nil)
    (set type-eq-decl nil sets nil))
   nil))
(IMP_ast_def_TCC5 0
  (IMP_ast_def_TCC5-1 nil 3458456184
   ("" (skosimp)
    (("" (lemma "subset_algebra_difference" ("x" "a!1" "y" "b!1"))
      (("" (expand "finite_disjoint_union?")
        ((""
          (inst +
           "lambda (i:nat): if i=0 then difference[T](a!1, b!1) else emptyset endif"
           "1")
          (("" (split)
            (("1" (grind) nil nil)
             ("2" (apply-extensionality :hide? t)
              (("2" (expand "IUnion")
                (("2" (expand "emptyset")
                  (("2" (case-replace "difference[T](a!1, b!1)(x!1)")
                    (("1" (inst + "0") nil nil) ("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil)
             ("3" (skosimp)
              (("3" (case-replace "i!1=0")
                (("1" (expand "member") (("1" (propax) nil nil)) nil)
                 ("2" (assert) (("2" (grind) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((A formal-const-decl "subset_algebra" outer_measure nil)
    (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (subset_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 outer_measure nil)
    (set type-eq-decl nil sets nil)
    (subset_algebra_difference judgement-tcc nil subset_algebra nil)
    (subset_algebra_difference application-judgement "(A)"
     outer_measure 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (sequence type-eq-decl nil sequences nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (difference const-decl "set" sets nil)
    (emptyset const-decl "set" sets nil)
    (subset_algebra_emptyset name-judgement "(S)" outer_measure nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (subset_algebra_intersection application-judgement "(S)"
     outer_measure nil)
    (/= const-decl "boolean" notequal nil)
    (member const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (empty? const-decl "bool" sets nil)
    (disjoint? const-decl "bool" sets nil)
    (disjoint? const-decl "bool" indexed_sets_aux "sets_aux/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (finite_disjoint_union? const-decl "bool" subset_algebra_def nil))
   nil)))

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