		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-do-merges1

Signature
(vl-lucid-do-merges1 occs) → merged-occs
Arguments: occs — Some sets that all occur in the same always/function/task.
Guard (vl-lucidocclist-p occs).
Returns: merged-occs — Merged together occurrences, if any.
Type (vl-lucidocclist-p merged-occs).

Definitions and Theorems

Function: vl-lucid-do-merges1

(defun vl-lucid-do-merges1 (occs)
  (declare (xargs :guard (vl-lucidocclist-p occs)))
  (let ((__function__ 'vl-lucid-do-merges1))
    (declare (ignorable __function__))
    (b* ((solo (vl-lucid-first-solo-occ occs))
         ((when solo) (list solo))
         ((when (atom occs)) nil))
      (list (vl-lucidocc-fix (car occs))))))

Theorem: vl-lucidocclist-p-of-vl-lucid-do-merges1

(defthm vl-lucidocclist-p-of-vl-lucid-do-merges1
  (b* ((merged-occs (vl-lucid-do-merges1 occs)))
    (vl-lucidocclist-p merged-occs))
  :rule-classes :rewrite)

Theorem: vl-lucid-do-merges1-of-vl-lucidocclist-fix-occs

(defthm vl-lucid-do-merges1-of-vl-lucidocclist-fix-occs
  (equal (vl-lucid-do-merges1 (vl-lucidocclist-fix occs))
         (vl-lucid-do-merges1 occs)))

Theorem: vl-lucid-do-merges1-vl-lucidocclist-equiv-congruence-on-occs

(defthm vl-lucid-do-merges1-vl-lucidocclist-equiv-congruence-on-occs
  (implies (vl-lucidocclist-equiv occs occs-equiv)
           (equal (vl-lucid-do-merges1 occs)
                  (vl-lucid-do-merges1 occs-equiv)))
  :rule-classes :congruence)