Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: abstract_min.prf Sprache: Lisp

Original von: PVS^©

(fixed_points
(prefixed_points_closed 0
  (prefixed_points_closed-1 nil 3318609496
   ("" (skosimp :preds? t)
    (("" (expand* "prefixed_point?" "monotone?")
      (("" (inst?) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((prefixed_point? const-decl "bool" fixed_points 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-nonempty-type-decl nil fixed_points nil)
    (pred type-eq-decl nil defined_types nil)
    (complete_lower_semilattice? const-decl "bool" bounded_orders nil)
    (monotone? const-decl "bool" fixed_points nil))
   shostak))
(prefixed_points_lower_bounds 0
  (prefixed_points_lower_bounds-1 nil 3318609521
   ("" (expand "lower_bound?")
    (("" (skosimp* t)
      (("" (inst?)
        ((""
          (expand* "prefixed_point?" "monotone?"
           "complete_lower_semilattice?" "partial_order?" "preorder?"
           "transitive?")
          (("" (flatten)
            (("" (inst - "x!1" "r!1")
              (("" (inst - "f!1(x!1)" "f!1(r!1)" "r!1")
                (("" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((monotone? const-decl "bool" fixed_points nil)
    (complete_lower_semilattice? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-nonempty-type-decl nil fixed_points nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (prefixed_point? const-decl "bool" fixed_points nil)
    (partial_order? const-decl "bool" orders nil)
    (transitive? const-decl "bool" relations nil)
    (preorder? const-decl "bool" orders nil)
    (lower_bound? const-decl "bool" bounded_orders nil))
   shostak))
(least_prefixed_point_is_fixed_point 0
  (least_prefixed_point_is_fixed_point-1 nil 3318609611
   ("" (expand* "greatest_lower_bound?" "fixed_point?")
    (("" (skosimp* t)
      (("" (inst - "f!1(x!1)")
        (("" (rewrite "prefixed_points_lower_bounds")
          (("" (expand "lower_bound?")
            (("" (inst - "f!1(x!1)")
              (("1" (use "antisymmetric") (("1" (assert) nil nil)) nil)
               ("2" (expand* "prefixed_point?" "monotone?")
                (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((monotone? const-decl "bool" fixed_points nil)
    (complete_lower_semilattice? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-nonempty-type-decl nil fixed_points nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (prefixed_points_lower_bounds formula-decl nil fixed_points nil)
    (prefixed_point? const-decl "bool" fixed_points nil)
    (lesseqp!1 skolem-const-decl "(complete_lower_semilattice?[T])"
     fixed_points nil)
    (f!1 skolem-const-decl "(monotone?(lesseqp!1))" fixed_points nil)
    (x!1 skolem-const-decl "T" fixed_points nil)
    (antisymmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (antisymmetric formula-decl nil relations_extra nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (fixed_point? const-decl "bool" fixed_points nil))
   shostak))
(least_fixed_point_le_prefixed_points 0
  (least_fixed_point_le_prefixed_points-1 nil 3318609697
   ("" (skosimp :preds? t)
    (("" (expand "complete_lower_semilattice?")
      (("" (flatten)
        (("" (invoke (inst - "%1") (! 1 2))
          (("" (expand "greatest_bounded_below?")
            (("" (skolem!)
              ((""
                (forward-chain "least_prefixed_point_is_fixed_point")
                (("" (expand* "greatest_lower_bound?" "lfp?" "least?")
                  (("" (flatten)
                    (("" (hide -6 -4)
                      (("" (expand "lower_bound?")
                        (("" (skolem-typepred)
                          (("" (inst?)
                            (("" (inst - "t!1")
                              ((""
                                (expand*
                                 "partial_order?"
                                 "preorder?"
                                 "transitive?")
                                ((""
                                  (flatten)
                                  ((""
                                    (inst - "x!1" "t!1" "r!1")
                                    (("" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((prefixed_point? const-decl "bool" fixed_points nil)
    (set type-eq-decl nil sets nil)
    (lfp? const-decl "bool" fixed_points nil)
    (least? const-decl "bool" minmax_orders nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (fixed_point? const-decl "bool" fixed_points nil)
    (lesseqp!1 skolem-const-decl "(complete_lower_semilattice?[T])"
     fixed_points nil)
    (f!1 skolem-const-decl "(monotone?(lesseqp!1))" fixed_points nil)
    (t!1 skolem-const-decl "T" fixed_points nil)
    (partial_order? const-decl "bool" orders nil)
    (transitive? const-decl "bool" relations nil)
    (preorder? const-decl "bool" orders nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (least_prefixed_point_is_fixed_point formula-decl nil fixed_points
     nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders 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-nonempty-type-decl nil fixed_points nil)
    (pred type-eq-decl nil defined_types nil)
    (complete_lower_semilattice? const-decl "bool" bounded_orders nil)
    (monotone? const-decl "bool" fixed_points nil))
   shostak))
(least_prefixed_point 0
  (least_prefixed_point-1 nil 3318609805
   ("" (skolem-typepred)
    (("" (prop)
      (("1" (expand "greatest_lower_bound?")
        (("1" (rewrite "least_fixed_point_le_prefixed_points")
          (("1" (skosimp)
            (("1" (expand "lower_bound?")
              (("1" (inst?)
                (("1" (expand* "lfp?" "least?")
                  (("1" (flatten)
                    (("1"
                      (expand* "prefixed_point?" "fixed_point?"
                       "complete_lower_semilattice?" "partial_order?"
                       "preorder?" "reflexive?")
                      (("1" (flatten)
                        (("1" (inst - "x!1") (("1" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand* "lfp?" "least?")
        (("2" (rewrite "least_prefixed_point_is_fixed_point")
          (("2" (expand* "greatest_lower_bound?" "lower_bound?")
            (("2" (skosimp :preds? t)
              (("2" (inst?)
                (("2"
                  (expand* "prefixed_point?" "fixed_point?"
                   "complete_lower_semilattice?" "partial_order?"
                   "preorder?" "reflexive?")
                  (("2" (flatten)
                    (("2" (inst -3 "r!1") (("2" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((least_fixed_point_le_prefixed_points formula-decl nil fixed_points
     nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (least? const-decl "bool" minmax_orders nil)
    (lfp? const-decl "bool" fixed_points nil)
    (fixed_point? const-decl "bool" fixed_points nil)
    (partial_order? const-decl "bool" orders nil)
    (reflexive? const-decl "bool" relations nil)
    (preorder? const-decl "bool" orders nil)
    (lesseqp!1 skolem-const-decl "(complete_lower_semilattice?[T])"
     fixed_points nil)
    (f!1 skolem-const-decl "(monotone?(lesseqp!1))" fixed_points nil)
    (x!1 skolem-const-decl "T" fixed_points nil)
    (prefixed_point? const-decl "bool" fixed_points nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (least_prefixed_point_is_fixed_point formula-decl nil fixed_points
     nil)
    (r!1 skolem-const-decl "(fixed_point?(f!1))" fixed_points nil)
    (monotone? const-decl "bool" fixed_points nil)
    (complete_lower_semilattice? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-nonempty-type-decl nil fixed_points nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(least_fixed_point_exists 0
  (least_fixed_point_exists-1 nil 3318609941
   ("" (skolem-typepred)
    (("" (rewrite "nonempty_exists")
      ((""
        (inst + "glb[T](lesseqp!1)(prefixed_point?(lesseqp!1)(f!1))")
        (("1" (rewrite "least_prefixed_point") (("1" (assert) nil nil))
          nil)
         ("2" (expand "complete_lower_semilattice?")
          (("2" (flatten) (("2" (inst?) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((nonempty_exists formula-decl nil sets_lemmas nil)
    (set type-eq-decl nil sets nil)
    (lfp? const-decl "bool" fixed_points nil)
    (least_prefixed_point formula-decl nil fixed_points nil)
    (lesseqp!1 skolem-const-decl "(complete_lower_semilattice?[T])"
     fixed_points nil)
    (f!1 skolem-const-decl "(monotone?(lesseqp!1))" fixed_points nil)
    (prefixed_point? const-decl "bool" fixed_points nil)
    (glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
     bounded_orders nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (monotone? const-decl "bool" fixed_points nil)
    (complete_lower_semilattice? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-nonempty-type-decl nil fixed_points nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(least_fixed_point_unique 0
  (least_fixed_point_unique-1 nil 3318609995
   ("" (expand "unique?")
    (("" (skosimp*)
      (("" (rewrite "least_prefixed_point")
        (("" (rewrite "least_prefixed_point")
          (("" (use "unique_greatest_lower_bound") nil nil)) nil))
        nil))
      nil))
    nil)
   ((unique_greatest_lower_bound formula-decl nil bounded_orders nil)
    (antisymmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (y!1 skolem-const-decl "T" fixed_points nil)
    (lesseqp!1 skolem-const-decl "(complete_lower_semilattice?[T])"
     fixed_points nil)
    (f!1 skolem-const-decl "(monotone?(lesseqp!1))" fixed_points nil)
    (x!1 skolem-const-decl "T" fixed_points nil)
    (set type-eq-decl nil sets nil)
    (prefixed_point? const-decl "bool" fixed_points nil)
    (monotone? const-decl "bool" fixed_points nil)
    (complete_lower_semilattice? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil fixed_points nil)
    (least_prefixed_point formula-decl nil fixed_points nil)
    (unique? const-decl "bool" exists1 nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.25 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.