Impressum sets_lemmas_aux.prf   Sprache: unbekannt

(sets_lemmas_aux
 (union_complement 0
  (union_complement-1 nil 3313990217
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "complement")
        (("" (expand "union")
          (("" (expand "fullset")
            (("" (flatten)
              (("" (expand "member") (("" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil sets_lemmas_aux nil)
    (boolean nonempty-type-decl nil booleans nil)
    (fullset const-decl "set" sets nil)
    (complement const-decl "set" sets nil)
    (union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (member const-decl "bool" sets nil))
   shostak))
 (intersection_complement 0
  (intersection_complement-1 nil 3313990250
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T formal-type-decl nil sets_lemmas_aux nil)
    (boolean nonempty-type-decl nil booleans nil)
    (emptyset const-decl "set" sets nil)
    (complement const-decl "set" sets nil)
    (intersection const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (member const-decl "bool" sets nil))
   shostak))
 (disjoint_complement 0
  (disjoint_complement-1 nil 3322194982
   ("" (skosimp)
    (("" (lemma "intersection_complement" ("a" "a!1"))
      (("" (expand "disjoint?")
        (("" (rewrite "emptyset_is_empty?") nil nil)) nil))
      nil))
    nil)
   ((set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil sets_lemmas_aux nil)
    (intersection_complement formula-decl nil sets_lemmas_aux nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (intersection const-decl "set" sets nil)
    (complement const-decl "set" sets nil)
    (disjoint? const-decl "bool" sets nil))
   shostak))
 (disjoint_commutative 0
  (disjoint_commutative-1 nil 3314018116
   ("" (expand "disjoint?")
    (("" (skosimp) (("" (rewrite "intersection_commutative") nil nil))
      nil))
    nil)
   ((T formal-type-decl nil sets_lemmas_aux nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (intersection_commutative formula-decl nil sets_lemmas nil)
    (disjoint? const-decl "bool" sets nil))
   shostak))
 (disjoint_empty 0
  (disjoint_empty-1 nil 3314018543
   ("" (skosimp)
    (("" (expand "disjoint?")
      (("" (expand "intersection")
        (("" (expand "empty?")
          (("" (skosimp*)
            (("" (expand "member")
              (("" (expand "emptyset") (("" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_intersection1 application-judgement "finite_set"
     finite_sets nil)
    (disjoint? const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (emptyset const-decl "set" sets nil)
    (intersection const-decl "set" sets nil))
   shostak))
 (powerset_fullset 0
  (powerset_fullset-1 nil 3321769783
   ("" (skosimp)
    (("" (lemma "subset_powerset" ("a" "a!1" "b" "a!1"))
      (("" (rewrite "subset_reflexive") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((T formal-type-decl nil sets_lemmas_aux nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (subset_powerset formula-decl nil sets_lemmas nil)
    (nonempty_powerset application-judgement "(nonempty?[set[T]])"
     sets_lemmas_aux nil)
    (subset_reflexive formula-decl nil sets_lemmas nil))
   shostak))
 (union_diff_inter 0
  (union_diff_inter-1 nil 3321854850
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "difference")
        (("" (expand "intersection")
          (("" (expand "union")
            (("" (expand "member")
              (("" (case-replace "a!1(x!1)")
                (("1" (flatten) nil nil) ("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil sets_lemmas_aux nil)
    (boolean nonempty-type-decl nil booleans nil)
    (intersection const-decl "set" sets nil)
    (difference const-decl "set" sets nil)
    (union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (member const-decl "bool" sets nil))
   shostak))
 (disjoint_diff_inter 0
  (disjoint_diff_inter-1 nil 3321854884
   ("" (skosimp)
    (("" (expand "disjoint?")
      (("" (expand "intersection")
        (("" (expand "difference")
          (("" (expand "empty?")
            (("" (expand "member") (("" (skosimp*) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((disjoint? const-decl "bool" sets nil)
    (difference const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil))
   shostak))
 (disjoint_member 0
  (disjoint_member-1 nil 3321935681
   ("" (expand "disjoint?")
    (("" (expand "intersection")
      (("" (expand "empty?")
        (("" (expand "member")
          (("" (skosimp*)
            (("" (inst - "x!1") (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((intersection const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (T formal-type-decl nil sets_lemmas_aux nil)
    (empty? const-decl "bool" sets nil)
    (disjoint? const-decl "bool" sets nil))
   shostak)))