Quelle  card_power_set.prf   Sprache: Lisp

(card_power_set
 (card_power 0
  (card_power-1 nil 3316968399
   ("" (skolem!)
    (("" (rewrite "card_lt_surj")
      (("" (split)
        (("1" (inst + "emptyset[T]") (("1" (grind) nil nil)) nil)
         ("2" (skolem!)
          (("2" (expand "surjective?")
            (("2" (inst - "{t: T | S!1(t) AND NOT f!1(t)(t)}")
              (("1" (skolem!)
                (("1" (decompose-equality)
                  (("1" (inst - "x!1")
                    (("1" (iff) (("1" (ground) nil nil)) nil)) nil))
                  nil))
                nil)
               ("2" (grind) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((card_lt_surj formula-decl nil card_comp_set_props nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (powerset const-decl "setofsets" sets nil)
    (T formal-type-decl nil card_power_set nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (f!1 skolem-const-decl "[(S!1) -> (powerset(S!1))]" card_power_set
     nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (surjective? const-decl "bool" functions nil)
    (nonempty_powerset application-judgement "(nonempty?[set[T]])"
     sets_lemmas nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (emptyset const-decl "set" sets nil)
    (S!1 skolem-const-decl "set[T]" card_power_set nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil))
   shostak)))