		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabpaths-append

Concatenate two reversed elabtraversals to get a reversed traversal that (when followed reversed) to the same place as following y reversed, then x reversed.

Signature
(vl-elabpaths-append x y) → xy
Arguments: x — Guard (vl-elabtraversal-p x).; y — Guard (vl-elabtraversal-p y).
Returns: xy — Type (vl-elabtraversal-p xy).

Definitions and Theorems

Function: vl-elabpaths-append

(defun vl-elabpaths-append (x y)
  (declare (xargs :guard (and (vl-elabtraversal-p x)
                              (vl-elabtraversal-p y))))
  (let ((__function__ 'vl-elabpaths-append))
    (declare (ignorable __function__))
    (cond ((atom x) (vl-elabtraversal-fix y))
          ((vl-elabinstruction-case (car x) :root)
           (cons (vl-elabinstruction-fix (car x))
                 (vl-elabtraversal-fix y)))
          (t (cons (vl-elabinstruction-fix (car x))
                   (vl-elabpaths-append (cdr x) y))))))

Theorem: vl-elabtraversal-p-of-vl-elabpaths-append

(defthm vl-elabtraversal-p-of-vl-elabpaths-append
  (b* ((xy (vl-elabpaths-append x y)))
    (vl-elabtraversal-p xy))
  :rule-classes :rewrite)

Theorem: vl-elabpaths-append-of-vl-elabtraversal-fix-x

(defthm vl-elabpaths-append-of-vl-elabtraversal-fix-x
  (equal (vl-elabpaths-append (vl-elabtraversal-fix x)
                              y)
         (vl-elabpaths-append x y)))

Theorem: vl-elabpaths-append-vl-elabtraversal-equiv-congruence-on-x

(defthm vl-elabpaths-append-vl-elabtraversal-equiv-congruence-on-x
  (implies (vl-elabtraversal-equiv x x-equiv)
           (equal (vl-elabpaths-append x y)
                  (vl-elabpaths-append x-equiv y)))
  :rule-classes :congruence)

Theorem: vl-elabpaths-append-of-vl-elabtraversal-fix-y

(defthm vl-elabpaths-append-of-vl-elabtraversal-fix-y
  (equal (vl-elabpaths-append x (vl-elabtraversal-fix y))
         (vl-elabpaths-append x y)))

Theorem: vl-elabpaths-append-vl-elabtraversal-equiv-congruence-on-y

(defthm vl-elabpaths-append-vl-elabtraversal-equiv-congruence-on-y
  (implies (vl-elabtraversal-equiv y y-equiv)
           (equal (vl-elabpaths-append x y)
                  (vl-elabpaths-append x y-equiv)))
  :rule-classes :congruence)