Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: util.pvs Sprache: Lisp

Original von: PVS^©

(kuratowski
(kuratowski 0
  (kuratowski-1 nil 3315007192
   ("" (typepred "<=")
    (("" (lemma "zorn")
      (("" (split)
        (("1" (skolem-typepred)
          (("1" (inst + "t!1")
            (("1"
              (expand* "fullset" "maximal?" "maximal_chain?"
               "strict_subset?" "chain_incl" "member")
              nil nil))
            nil))
          nil)
         ("2" (skolem!)
          (("2" (inst + "chain_union(ch!1)")
            (("2"
              (expand* "bounded_above?" "upper_bound?" "chain_incl"
               "subset?" "member")
              (("2" (inst + "chain_union(ch!1)")
                (("2" (skosimp*)
                  (("2" (expand* "chain_union" "Union")
                    (("2" (inst + "r!1")
                      (("2" (expand "extend") (("2" (propax) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((chain_incl const-decl "bool" chain_chain nil)
    (subchain nonempty-type-eq-decl nil chain_chain nil)
    (chain? const-decl "bool" chain nil)
    (set type-eq-decl nil sets nil) (zorn formula-decl nil zorn nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (bounded_above? const-decl "bool" bounded_orders nil)
    (extend const-decl "R" extend nil)
    (FALSE const-decl "bool" booleans nil)
    (ch!1 skolem-const-decl "chain[subchain, chain_incl]" kuratowski
     nil)
    (r!1 skolem-const-decl "(ch!1)" kuratowski nil)
    (Union const-decl "set" sets nil)
    (chain_union const-decl "subchain" chain_chain nil)
    (chain_chain nonempty-type-eq-decl nil chain_chain nil)
    (fullset const-decl "set" sets nil)
    (maximal? const-decl "bool" minmax_orders nil)
    (maximal_chain? const-decl "bool" chain nil)
    (strict_subset? const-decl "bool" sets nil)
    (chain nonempty-type-eq-decl nil chain 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-type-decl nil kuratowski nil)
    (pred type-eq-decl nil defined_types nil)
    (partial_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(partial_order?[T])" kuratowski nil))
   shostak)))

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