Quelle  kuratowski.prf   Sprache: Lisp

(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)))