		Search-engine friendly clone of the ACL2 documentation.

Balance

Remove-duplicate-lits

Signature
(remove-duplicate-lits x) → new-x
Arguments: x — literal-sorted.
Guard (lit-listp x).
Returns: new-x — Type (lit-listp new-x).

Definitions and Theorems

Function: remove-duplicate-lits

(defun remove-duplicate-lits (x)
  (declare (xargs :guard (lit-listp x)))
  (let ((__function__ 'remove-duplicate-lits))
    (declare (ignorable __function__))
    (if (or (atom x) (atom (cdr x)))
        (lit-list-fix x)
      (if (lit-equiv (car x) (cadr x))
          (remove-duplicate-lits (cdr x))
        (cons-with-hint (lit-fix (car x))
                        (remove-duplicate-lits (cdr x))
                        (lit-list-fix x))))))

Theorem: lit-listp-of-remove-duplicate-lits

(defthm lit-listp-of-remove-duplicate-lits
  (b* ((new-x (remove-duplicate-lits x)))
    (lit-listp new-x))
  :rule-classes :rewrite)

Theorem: remove-duplicate-lits-set-equiv

(defthm remove-duplicate-lits-set-equiv
  (b* ((?new-x (remove-duplicate-lits x)))
    (acl2::set-equiv new-x (lit-list-fix x))))

Theorem: remove-duplicate-lits-of-lit-list-fix-x

(defthm remove-duplicate-lits-of-lit-list-fix-x
  (equal (remove-duplicate-lits (lit-list-fix x))
         (remove-duplicate-lits x)))

Theorem: remove-duplicate-lits-lit-list-equiv-congruence-on-x

(defthm remove-duplicate-lits-lit-list-equiv-congruence-on-x
  (implies (satlink::lit-list-equiv x x-equiv)
           (equal (remove-duplicate-lits x)
                  (remove-duplicate-lits x-equiv)))
  :rule-classes :congruence)