Filtering...

element-list

books/std/osets/element-list

Included Books

top abstract list-fix
other
(in-package "ACL2")
include-book
(include-book "top")
include-book
(include-book "std/lists/abstract" :dir :system)
include-book
(include-book "std/lists/list-fix" :dir :system)
other
(def-listp-rule element-list-p-of-sfix
  (iff (element-list-p (sfix x))
    (or (element-list-p x) (not (setp x))))
  :hints (("Goal" :in-theory (enable emptyp sfix)))
  :tags (:osets))
other
(def-listp-rule element-list-p-of-insert
  (iff (element-list-p (insert a x))
    (and (element-list-p (sfix x)) (element-p a)))
  :hints (("Goal" :in-theory (e/d (insert tail head emptyp setp)
       (iff))
     :induct (len x)))
  :tags (:osets))
other
(def-listp-rule element-list-p-of-delete
  (implies (element-list-p x) (element-list-p (delete k x)))
  :hints (("Goal" :in-theory (enable delete head tail emptyp)))
  :tags (:osets))
other
(def-listp-rule element-list-p-of-mergesort
  (iff (element-list-p (mergesort x))
    (element-list-p (list-fix x)))
  :hints (("Goal" :in-theory (enable mergesort)))
  :tags (:osets))
other
(def-listp-rule element-list-p-of-union
  (iff (element-list-p (union x y))
    (and (element-list-p (sfix x))
      (element-list-p (sfix y))))
  :hints (("Goal" :in-theory (enable union head tail emptyp setp)
     :induct (len x)))
  :tags (:osets))
other
(def-listp-rule element-list-p-of-intersect-1
  (implies (element-list-p x)
    (element-list-p (intersect x y)))
  :hints (("Goal" :in-theory (enable intersect
       head
       tail
       emptyp
       setp)))
  :tags (:osets))
local
(local (defthm element-p-when-in-element-list-p
    (implies (and (in a x) (element-list-p x))
      (element-p a))
    :hints (("Goal" :in-theory (enable in head tail emptyp)))))
other
(def-listp-rule element-list-p-of-intersect-2
  (implies (element-list-p y)
    (element-list-p (intersect x y)))
  :hints (("Goal" :in-theory (enable intersect
       head
       tail
       emptyp
       setp)))
  :tags (:osets))
other
(def-listp-rule element-list-p-of-difference
  (implies (element-list-p x)
    (element-list-p (difference x y)))
  :hints (("Goal" :in-theory (enable difference
       head
       tail
       emptyp
       setp)))
  :tags (:osets))