Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/orders/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: main.pas 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)))