Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: real_fun_preds.prf Sprache: Lisp

Original von: PVS^©

(real_fun_preds
(bounded?_lem 0
  (bounded?_lem-3 nil 3297509203
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "bounded?")
        (("1" (flatten)
          (("1" (expand "abs")
            (("1" (expand "bounded_above?")
              (("1" (expand "bounded_below?")
                (("1" (skosimp*)
                  (("1" (inst + "max(abs(a!1),abs(a!2))")
                    (("1" (skosimp*)
                      (("1" (lift-if)
                        (("1" (ground)
                          (("1" (expand "max")
                            (("1" (lift-if)
                              (("1"
                                (inst?)
                                (("1"
                                  (inst?)
                                  (("1" (grind) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (inst?)
                            (("2" (inst?) (("2" (grind) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "bounded?")
        (("2" (skosimp*)
          (("2" (prop)
            (("1" (expand "bounded_above?")
              (("1" (inst + "B!1")
                (("1" (skosimp*)
                  (("1" (inst?) (("1" (grind) nil nil)) nil)) nil))
                nil))
              nil)
             ("2" (expand "bounded_below?")
              (("2" (inst + "-B!1")
                (("2" (skosimp*)
                  (("2" (inst?) (("2" (grind) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((bounded_above? const-decl "bool" real_fun_preds nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (T_pred const-decl "[real -> boolean]" real_fun_preds nil)
    (T formal-subtype-decl nil real_fun_preds nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nnreal 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)
    (nonneg_real_max application-judgement
     "{z: nonneg_real | z >= x AND z >= y}" real_defs nil)
    (bounded_below? const-decl "bool" real_fun_preds nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (bounded? const-decl "bool" real_fun_preds nil))
   nil)
  (bounded?_lem-2 nil 3297509167
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "bounded?")
        (("1" (flatten)
          (("1" (expand "abs")
            (("1" (expand "bounded_above?")
              (("1" (expand "bounded_below?")
                (("1" (skosimp*)
                  (("1" (inst + "max(abs(B!1),abs(a!2))")
                    (("1" (skosimp*)
                      (("1" (lift-if)
                        (("1" (ground)
                          (("1" (expand "max")
                            (("1" (lift-if)
                              (("1"
                                (inst?)
                                (("1"
                                  (inst?)
                                  (("1" (grind) nil)))))))))
                           ("2" (inst?)
                            (("2" (inst?)
                              (("2"
                                (grind)
                                nil)))))))))))))))))))))))))
       ("2" (expand "bounded?")
        (("2" (skosimp*)
          (("2" (prop)
            (("1" (expand "bounded_above?")
              (("1" (inst + "B!1")
                (("1" (skosimp*)
                  (("1" (inst?) (("1" (grind) nil)))))))))
             ("2" (expand "bounded_below?")
              (("2" (inst + "-B!1")
                (("2" (skosimp*)
                  (("2" (inst?) (("2" (grind) nil))))))))))))))))))
    nil)
   nil nil)
  (bounded?_lem-1 nil 3280071776
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "bounded?")
        (("1" (flatten)
          (("1" (expand "abs")
            (("1" (expand "bounded_above?")
              (("1" (expand "bounded_below?")
                (("1" (skosimp*)
                  (("1" (inst + "max(abs(a!1),abs(a!2))")
                    (("1" (skosimp*)
                      (("1" (lift-if)
                        (("1" (ground)
                          (("1" (expand "max")
                            (("1" (lift-if)
                              (("1"
                                (inst?)
                                (("1"
                                  (inst?)
                                  (("1" (grind) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (inst?)
                            (("2" (inst?) (("2" (grind) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "bounded?")
        (("2" (skosimp*)
          (("2" (prop)
            (("1" (expand "bounded_above?")
              (("1" (inst + "a!1")
                (("1" (skosimp*)
                  (("1" (inst?) (("1" (grind) nil nil)) nil)) nil))
                nil))
              nil)
             ("2" (expand "bounded_below?")
              (("2" (inst + "-a!1")
                (("2" (skosimp*)
                  (("2" (inst?) (("2" (grind) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil shostak)))

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