Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: bounded_sets.prf Sprache: Lisp

Original von: PVS^©

(bounded_sets
(least_bounded_above_is_bounded_above 0
  (least_bounded_above_is_bounded_above-1 nil 3315154466
   ("" (skolem-typepred)
    ((""
      (expand* "least_bounded_above?" "bounded_above?"
       "least_upper_bound?")
      (("" (skosimp) (("" (inst? +) nil nil)) nil)) nil))
    nil)
   ((bounded_above? const-decl "bool" bounded_orders nil)
    (least_upper_bound? const-decl "bool" bounded_orders nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(greatest_bounded_below_is_bounded_below 0
  (greatest_bounded_below_is_bounded_below-1 nil 3315154466
   ("" (skolem-typepred)
    ((""
      (expand* "greatest_bounded_below?" "bounded_below?"
       "greatest_lower_bound?")
      (("" (skosimp) (("" (inst? +) nil nil)) nil)) nil))
    nil)
   ((bounded_below? const-decl "bool" bounded_orders nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(bounded_is_bounded_above 0
  (bounded_is_bounded_above-1 nil 3315154466
   ("" (judgement-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)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (bounded? const-decl "bool" bounded_orders nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded_below? const-decl "bool" bounded_orders nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (T formal-type-decl nil bounded_sets nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (bounded_above? const-decl "bool" bounded_orders nil))
   nil))
(bounded_is_bounded_below 0
  (bounded_is_bounded_below-1 nil 3315154466
   ("" (judgement-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)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (bounded? const-decl "bool" bounded_orders nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded_above? const-decl "bool" bounded_orders nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (T formal-type-decl nil bounded_sets nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (bounded_below? const-decl "bool" bounded_orders nil))
   nil))
(tightly_bounded_is_bounded 0
  (tightly_bounded_is_bounded-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (expand* "tightly_bounded?" "bounded?")
      (("" (rewrite "least_bounded_above_is_bounded_above")
        (("" (rewrite "greatest_bounded_below_is_bounded_below") nil
          nil))
        nil))
      nil))
    nil)
   ((bounded? const-decl "bool" bounded_orders nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (greatest_bounded_below_is_bounded_below judgement-tcc nil
     bounded_sets nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (least_bounded_above_is_bounded_above judgement-tcc nil
     bounded_sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (tightly_bounded? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(tightly_bounded_above 0
  (tightly_bounded_above-1 nil 3315154466 ("" (judgement-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)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (tightly_bounded? const-decl "bool" bounded_orders nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (T formal-type-decl nil bounded_sets nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (least_upper_bound? const-decl "bool" bounded_orders nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil))
   nil))
(tightly_bounded_below 0
  (tightly_bounded_below-1 nil 3315154466 ("" (judgement-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)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (tightly_bounded? const-decl "bool" bounded_orders nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (least_upper_bound? const-decl "bool" bounded_orders nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (T formal-type-decl nil bounded_sets nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil))
   nil))
(intersection1_preserves_bounded_above 0
  (intersection1_preserves_bounded_above-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (expand* "bounded_above?" "upper_bound?")
      (("" (skolem!)
        (("" (inst? +)
          (("" (skolem-typepred)
            (("" (expand* "intersection" "member")
              (("" (flatten) (("" (inst?) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((upper_bound? const-decl "bool" bounded_orders nil)
    (member const-decl "bool" sets nil)
    (Su!1 skolem-const-decl
     "(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_sets nil)
    (S!1 skolem-const-decl "set[T]" bounded_sets nil)
    (r!1 skolem-const-decl "(intersection[T](Su!1, S!1))" bounded_sets
     nil)
    (intersection const-decl "set" sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded_above? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(intersection2_preserves_bounded_above 0
  (intersection2_preserves_bounded_above-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (expand* "bounded_above?" "upper_bound?")
      (("" (skolem!)
        (("" (inst? +)
          (("" (skolem-typepred)
            (("" (expand* "intersection" "member")
              (("" (flatten) (("" (inst?) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((upper_bound? const-decl "bool" bounded_orders nil)
    (member const-decl "bool" sets nil)
    (Su!1 skolem-const-decl
     "(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_sets nil)
    (S!1 skolem-const-decl "set[T]" bounded_sets nil)
    (r!1 skolem-const-decl "(intersection[T](S!1, Su!1))" bounded_sets
     nil)
    (intersection const-decl "set" sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded_above? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(difference_preserves_bounded_above 0
  (difference_preserves_bounded_above-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (rewrite "difference_intersection")
      (("" (rewrite "intersection1_preserves_bounded_above") nil nil))
      nil))
    nil)
   ((difference_intersection formula-decl nil sets_lemmas nil)
    (intersection1_preserves_bounded_above application-judgement
     "(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_sets nil)
    (intersection1_preserves_bounded_above judgement-tcc nil
     bounded_sets nil)
    (complement const-decl "set" sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded_above? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(remove_preserves_bounded_above 0
  (remove_preserves_bounded_above-1 nil 3315154466
   ("" (skolem!)
    (("" (rewrite "remove_as_difference")
      (("" (rewrite "difference_preserves_bounded_above") nil nil))
      nil))
    nil)
   ((remove_as_difference formula-decl nil sets_lemmas nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (bounded_above? const-decl "bool" bounded_orders nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" bounded_sets nil)
    (difference_preserves_bounded_above application-judgement
     "(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (difference_preserves_bounded_above judgement-tcc nil bounded_sets
     nil))
   nil))
(intersection1_preserves_bounded_below 0
  (intersection1_preserves_bounded_below-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (expand* "bounded_below?" "lower_bound?")
      (("" (skolem!)
        (("" (inst? +)
          (("" (skolem-typepred)
            (("" (expand* "intersection" "member")
              (("" (flatten) (("" (inst?) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lower_bound? const-decl "bool" bounded_orders nil)
    (member const-decl "bool" sets nil)
    (Sl!1 skolem-const-decl
     "(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_sets nil)
    (S!1 skolem-const-decl "set[T]" bounded_sets nil)
    (r!1 skolem-const-decl "(intersection[T](Sl!1, S!1))" bounded_sets
     nil)
    (intersection const-decl "set" sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded_below? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(intersection2_preserves_bounded_below 0
  (intersection2_preserves_bounded_below-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (expand* "bounded_below?" "lower_bound?")
      (("" (skolem!)
        (("" (inst? +)
          (("" (skolem-typepred)
            (("" (expand* "intersection" "member")
              (("" (flatten) (("" (inst?) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lower_bound? const-decl "bool" bounded_orders nil)
    (member const-decl "bool" sets nil)
    (Sl!1 skolem-const-decl
     "(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_sets nil)
    (S!1 skolem-const-decl "set[T]" bounded_sets nil)
    (r!1 skolem-const-decl "(intersection[T](S!1, Sl!1))" bounded_sets
     nil)
    (intersection const-decl "set" sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded_below? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(difference_preserves_bounded_below 0
  (difference_preserves_bounded_below-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (rewrite "difference_intersection")
      (("" (rewrite "intersection1_preserves_bounded_below") nil nil))
      nil))
    nil)
   ((difference_intersection formula-decl nil sets_lemmas nil)
    (intersection1_preserves_bounded_below application-judgement
     "(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_sets nil)
    (intersection1_preserves_bounded_below judgement-tcc nil
     bounded_sets nil)
    (complement const-decl "set" sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded_below? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(remove_preserves_bounded_below 0
  (remove_preserves_bounded_below-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (rewrite "remove_as_difference")
      (("" (rewrite "difference_preserves_bounded_below") nil nil))
      nil))
    nil)
   ((remove_as_difference formula-decl nil sets_lemmas nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" bounded_sets nil)
    (difference_preserves_bounded_below application-judgement
     "(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_sets nil)
    (difference_preserves_bounded_below judgement-tcc nil bounded_sets
     nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded_below? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(intersection1_preserves_bounded 0
  (intersection1_preserves_bounded-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (expand "bounded?") (("" (ground) nil nil)) nil)) nil)
   ((intersection1_preserves_bounded_above application-judgement
     "(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_sets nil)
    (intersection1_preserves_bounded_below application-judgement
     "(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(intersection2_preserves_bounded 0
  (intersection2_preserves_bounded-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (expand "bounded?") (("" (ground) nil nil)) nil)) nil)
   ((intersection2_preserves_bounded_above application-judgement
     "(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_sets nil)
    (intersection2_preserves_bounded_below application-judgement
     "(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(difference_preserves_bounded 0
  (difference_preserves_bounded-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (expand "bounded?") (("" (ground) nil nil)) nil)) nil)
   ((difference_preserves_bounded_above application-judgement
     "(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_sets nil)
    (difference_preserves_bounded_below application-judgement
     "(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(remove_preserves_bounded 0
  (remove_preserves_bounded-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (expand "bounded?") (("" (ground) nil nil)) nil)) nil)
   ((remove_preserves_bounded_above application-judgement
     "(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_sets nil)
    (remove_preserves_bounded_below application-judgement
     "(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil)))

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