Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: open_sets.prf Sprache: Lisp

Original von: PVS^©

(open_sets
(open_ball?_lem 0
  (open_ball?_lem-1 nil 3258223423
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "open_ball?")
        (("1" (skosimp*)
          (("1" (expand "open_ball")
            (("1" (expand "subset?")
              (("1" (expand "member")
                (("1" (inst + "delta!1") nil nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "open_ball?")
        (("2" (skosimp*)
          (("2" (expand "subset?")
            (("2" (expand "member")
              (("2" (expand "open_ball") (("2" (inst + "r!1") nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((subset? const-decl "bool" sets 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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (member const-decl "bool" sets nil)
    (open_ball const-decl "set[T]" open_sets nil)
    (open_ball? const-decl "bool" open_sets nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(open?_lem 0
  (open?_lem-1 nil 3258223381
   ("" (skosimp*) (("" (expand "open?") (("" (inst?) nil nil)) nil))
    nil)
   ((open? const-decl "bool" open_sets 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)
    (T_pred const-decl "[real -> boolean]" open_sets nil)
    (T formal-subtype-decl nil open_sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (x!1 skolem-const-decl "T" open_sets nil)
    (S!1 skolem-const-decl "set[T]" open_sets nil))
   shostak))
(open_intv_open 0
  (open_intv_open-1 nil 3258299476
   ("" (skosimp*)
    (("" (expand "open?")
      (("" (skosimp*)
        (("" (expand "open_ball?")
          (("" (inst + "min(x!1 -a!1,b!1-x!1)")
            (("1" (skosimp*) (("1" (grind) nil nil)) nil)
             ("2" (grind) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((open? const-decl "bool" open_sets nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (open_ball? const-decl "bool" open_sets nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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) (<= const-decl "bool" reals nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_pred const-decl "[real -> boolean]" open_sets nil)
    (T formal-subtype-decl nil open_sets nil)
    (< const-decl "bool" reals nil)
    (a!1 skolem-const-decl "T" open_sets nil)
    (b!1 skolem-const-decl "T" open_sets nil)
    (x!1 skolem-const-decl "(LAMBDA (x: T): a!1 < x AND x < b!1)"
     open_sets nil)
    (> const-decl "bool" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
(above_intv_open 0
  (above_intv_open-1 nil 3258299818
   ("" (skosimp*)
    (("" (expand "open?")
      (("" (skosimp*)
        (("" (expand "open_ball?")
          (("" (inst + "x!1-a!1")
            (("" (skosimp*) (("" (grind) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((open? const-decl "bool" open_sets nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (open_ball? const-decl "bool" open_sets nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (T formal-subtype-decl nil open_sets nil)
    (T_pred const-decl "[real -> boolean]" open_sets nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals 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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
(below_intv_open 0
  (below_intv_open-1 nil 3258299894
   ("" (skosimp*)
    (("" (expand "open?")
      (("" (skosimp*)
        (("" (expand "open_ball?")
          (("" (inst + "a!1-x!1") (("" (grind) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((open? const-decl "bool" open_sets nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (open_ball? const-decl "bool" open_sets nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (T formal-subtype-decl nil open_sets nil)
    (T_pred const-decl "[real -> boolean]" open_sets nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals 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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(union_open 0
  (union_open-1 nil 3258299981
   ("" (skosimp*)
    (("" (expand "open?")
      (("" (skosimp*)
        (("" (expand "open_ball?")
          (("" (typepred "x!1")
            (("" (expand "union")
              (("" (expand "member")
                (("" (split -2)
                  (("1" (hide -4)
                    (("1" (inst?)
                      (("1" (skosimp*)
                        (("1" (inst + "delta!1")
                          (("1" (skosimp*)
                            (("1" (inst - "y!1")
                              (("1" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide -3)
                    (("2" (inst?)
                      (("2" (skosimp*)
                        (("2" (inst + "delta!1")
                          (("2" (skosimp*)
                            (("2" (inst - "y!1")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((open? const-decl "bool" open_sets nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (open_ball? const-decl "bool" open_sets nil)
    (S1!1 skolem-const-decl "set[T]" open_sets nil)
    (S2!1 skolem-const-decl "set[T]" open_sets nil)
    (x!1 skolem-const-decl "(union(S1!1, S2!1))" open_sets nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (member 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)
    (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)
    (T_pred const-decl "[real -> boolean]" open_sets nil)
    (T formal-subtype-decl nil open_sets nil)
    (set type-eq-decl nil sets nil) (union const-decl "set" sets nil))
   shostak))
(closed_intv_closed 0
  (closed_intv_closed-1 nil 3258299631
   ("" (skosimp*)
    (("" (expand "closed?")
      ((""
        (case-replace "complement(LAMBDA (x): a!1 <= x AND x <= b!1) =
             union(above_intv(b!1),below_intv(a!1))")
        (("1" (hide -1)
          (("1" (lemma "union_open")
            (("1" (inst?)
              (("1" (assert)
                (("1" (hide 2)
                  (("1" (lemma "above_intv_open ")
                    (("1" (inst?)
                      (("1" (assert)
                        (("1" (lemma "below_intv_open ")
                          (("1" (inst?) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide 2)
          (("2" (apply-extensionality 1 :hide? t)
            (("2" (grind) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((closed? const-decl "bool" open_sets nil)
    (member const-decl "bool" sets nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (below_intv_open formula-decl nil open_sets nil)
    (above_intv_open formula-decl nil open_sets nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (union_open formula-decl nil open_sets nil)
    (< const-decl "bool" reals nil) (> const-decl "bool" reals nil)
    (union const-decl "set" sets nil) (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (complement const-decl "set" sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-subtype-decl nil open_sets nil)
    (T_pred const-decl "[real -> boolean]" open_sets 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))
   shostak)))

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