Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: bounded_reals.prf Sprache: Lisp

Original von: PVS^©

(bounded_reals
(sup_exists 0
  (sup_exists-1 nil 3506273121
   ("" (skosimp*)
    (("" (lemma "real_complete2")
      (("" (inst?)
        (("" (typepred "Su!1")
          (("" (expand "above_bounded")
            (("" (skosimp*)
              (("" (prop) (("" (inst 1 "n!1") nil))))))))))))))
    nil)
   ((T formal-subtype-decl nil bounded_reals nil)
    (T_pred const-decl "[real -> boolean]" bounded_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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_complete2 formula-decl nil reals_complete_more nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (sup_set type-eq-decl nil bounded_reals nil)
    (above_bounded const-decl "bool" bounded_reals nil)
    (setof type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil))
   nil))
(sup_TCC1 0
  (sup_TCC1-1 nil 3506273121
   (""
    (inst 1 "(LAMBDA (s: sup_set): choose({x: real
                      | least_upper_bound(<=)(x, s)}))")
    (("" (skosimp*)
      (("" (lemma "sup_exists")
        (("" (inst?)
          (("" (skosimp*)
            (("" (grind :exclude "least_upper_bound") nil))))))))))
    nil)
   ((empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (sup_exists formula-decl nil bounded_reals nil)
    (choose const-decl "(p)" sets nil) (<= const-decl "bool" reals nil)
    (least_upper_bound const-decl "bool" bound_defs nil)
    (pred type-eq-decl nil defined_types nil)
    (sup_set type-eq-decl nil bounded_reals nil)
    (above_bounded const-decl "bool" bounded_reals nil)
    (setof type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-subtype-decl nil bounded_reals nil)
    (T_pred const-decl "[real -> boolean]" bounded_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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(sup_def 0
  (sup_def-1 nil 3506273121
   ("" (skosimp*)
    (("" (typepred "sup(Su!1)")
      (("" (prop)
        (("1" (assert) nil)
         ("2" (expand "least_upper_bound")
          (("2" (flatten)
            (("2" (inst -4 "x!1")
              (("2" (inst -2 "sup(Su!1)")
                (("2" (assert) nil))))))))))))))
    nil)
   ((sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals
     nil)
    (sup_set type-eq-decl nil bounded_reals nil)
    (above_bounded const-decl "bool" bounded_reals nil)
    (setof type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil) (<= const-decl "bool" reals nil)
    (least_upper_bound const-decl "bool" bound_defs nil)
    (T formal-subtype-decl nil bounded_reals nil)
    (T_pred const-decl "[real -> boolean]" bounded_reals nil)
    (pred type-eq-decl nil defined_types 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(max_TCC1 0
  (max_TCC1-1 nil 3506273121 ("" (subtype-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)
    (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]" bounded_reals nil)
    (T formal-subtype-decl nil bounded_reals nil)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (setof type-eq-decl nil defined_types nil)
    (above_bounded const-decl "bool" bounded_reals nil)
    (sup_set type-eq-decl nil bounded_reals nil)
    (in_set const-decl "bool" bounded_reals nil)
    (pred type-eq-decl nil defined_types nil)
    (least_upper_bound const-decl "bool" bound_defs nil)
    (<= const-decl "bool" reals nil)
    (sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals
     nil)
    (max_set type-eq-decl nil bounded_reals nil)
    (upper_bound const-decl "bool" bound_defs nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil))
   nil))
(max_def 0
  (max_def-1 nil 3506273121
   ("" (skolem-typepred)
    (("" (expand "max")
      (("" (typepred "sup(W!1)")
        (("" (prop)
          (("1" (grind :exclude "upper_bound") nil)
           ("2" (grind :exclude "upper_bound")
            (("2" (expand "upper_bound" -5)
              (("2" (inst -5 "t!1")
                (("2" (grind :exclude "upper_bound") nil))))))))))))))
    nil)
   ((max const-decl "T" bounded_reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (maximum? const-decl "bool" bounded_reals nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (upper_bound const-decl "bool" bound_defs nil)
    (max_set type-eq-decl nil bounded_reals nil)
    (sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals
     nil)
    (<= const-decl "bool" reals nil)
    (least_upper_bound const-decl "bool" bound_defs nil)
    (pred type-eq-decl nil defined_types nil)
    (in_set const-decl "bool" bounded_reals nil)
    (sup_set type-eq-decl nil bounded_reals nil)
    (above_bounded const-decl "bool" bounded_reals nil)
    (setof type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (T formal-subtype-decl nil bounded_reals nil)
    (T_pred const-decl "[real -> boolean]" bounded_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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(inf_exists 0
  (inf_exists-1 nil 3506273121
   ("" (skosimp*)
    (("" (lemma "real_lower_complete2")
      (("" (inst?)
        (("" (typepred "Sl!1")
          (("" (expand "below_bounded")
            (("" (skosimp*)
              (("" (prop) (("" (inst 1 "n!1") nil))))))))))))))
    nil)
   ((T formal-subtype-decl nil bounded_reals nil)
    (T_pred const-decl "[real -> boolean]" bounded_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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_lower_complete2 formula-decl nil reals_complete_more nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (inf_set type-eq-decl nil bounded_reals nil)
    (below_bounded const-decl "bool" bounded_reals nil)
    (setof type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil))
   nil))
(inf_TCC1 0
  (inf_TCC1-1 nil 3506273121
   (""
    (inst 1 "(LAMBDA Sl: choose({x: real
                      | greatest_lower_bound(<=)(x, Sl)}))")
    (("" (skosimp*)
      (("" (lemma "inf_exists")
        (("" (inst?)
          (("" (grind :exclude "greatest_lower_bound") nil))))))))
    nil)
   ((member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (inf_exists formula-decl nil bounded_reals nil)
    (choose const-decl "(p)" sets nil) (<= const-decl "bool" reals nil)
    (greatest_lower_bound const-decl "bool" bound_defs nil)
    (pred type-eq-decl nil defined_types nil)
    (inf_set type-eq-decl nil bounded_reals nil)
    (below_bounded const-decl "bool" bounded_reals nil)
    (setof type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-subtype-decl nil bounded_reals nil)
    (T_pred const-decl "[real -> boolean]" bounded_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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(inf_def 0
  (inf_def-1 nil 3506273121
   ("" (skosimp*)
    (("" (typepred "inf(Sl!1)")
      (("" (prop)
        (("1" (assert) nil)
         ("2" (expand "greatest_lower_bound")
          (("2" (flatten)
            (("2" (inst -4 "x!1")
              (("2" (inst -2 "inf(Sl!1)")
                (("2" (assert) nil))))))))))))))
    nil)
   ((inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}"
     bounded_reals nil)
    (inf_set type-eq-decl nil bounded_reals nil)
    (below_bounded const-decl "bool" bounded_reals nil)
    (setof type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil) (<= const-decl "bool" reals nil)
    (greatest_lower_bound const-decl "bool" bound_defs nil)
    (T formal-subtype-decl nil bounded_reals nil)
    (T_pred const-decl "[real -> boolean]" bounded_reals nil)
    (pred type-eq-decl nil defined_types 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(min_TCC1 0
  (min_TCC1-1 nil 3506273121 ("" (subtype-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)
    (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]" bounded_reals nil)
    (T formal-subtype-decl nil bounded_reals nil)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (setof type-eq-decl nil defined_types nil)
    (below_bounded const-decl "bool" bounded_reals nil)
    (inf_set type-eq-decl nil bounded_reals nil)
    (ext const-decl "set[real]" bounded_reals nil)
    (pred type-eq-decl nil defined_types nil)
    (greatest_lower_bound const-decl "bool" bound_defs nil)
    (<= const-decl "bool" reals nil)
    (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}"
     bounded_reals nil)
    (min_set type-eq-decl nil bounded_reals nil)
    (lower_bound const-decl "bool" bound_defs nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil))
   nil))
(min_def 0
  (min_def-1 nil 3506273121
   ("" (skolem-typepred)
    (("" (expand "min")
      (("" (typepred "inf(X!1)")
        (("" (prop)
          (("1" (grind :exclude "lower_bound") nil)
           ("2" (grind :exclude "lower_bound")
            (("2" (expand "lower_bound" -5)
              (("2" (inst -5 "t!1") (("2" (assert) nil))))))))))))))
    nil)
   ((min const-decl "T" bounded_reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minimum? const-decl "bool" bounded_reals nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (lower_bound const-decl "bool" bound_defs nil)
    (min_set type-eq-decl nil bounded_reals nil)
    (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}"
     bounded_reals nil)
    (<= const-decl "bool" reals nil)
    (greatest_lower_bound const-decl "bool" bound_defs nil)
    (pred type-eq-decl nil defined_types nil)
    (ext const-decl "set[real]" bounded_reals nil)
    (inf_set type-eq-decl nil bounded_reals nil)
    (below_bounded const-decl "bool" bounded_reals nil)
    (setof type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (T formal-subtype-decl nil bounded_reals nil)
    (T_pred const-decl "[real -> boolean]" bounded_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)
    (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.5 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.