		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabtraversals-remove-common-prefix

Signature
(vl-elabtraversals-remove-common-prefix x y) → (mv x-suffix y-suffix)
Arguments: x — Guard (vl-elabtraversal-p x).; y — Guard (vl-elabtraversal-p y).
Returns: x-suffix — Type (vl-elabtraversal-p x-suffix).; y-suffix — Type (vl-elabtraversal-p y-suffix).

Definitions and Theorems

Function: vl-elabtraversals-remove-common-prefix

(defun vl-elabtraversals-remove-common-prefix (x y)
  (declare (xargs :guard (and (vl-elabtraversal-p x)
                              (vl-elabtraversal-p y))))
  (let ((__function__ 'vl-elabtraversals-remove-common-prefix))
    (declare (ignorable __function__))
    (if (or (atom x)
            (atom y)
            (vl-elabinstruction-case (car x)
                                     :push-anon)
            (vl-elabinstruction-case (car y)
                                     :push-anon)
            (not (vl-elabinstruction-equiv (car x)
                                           (car y))))
        (mv (vl-elabtraversal-fix x)
            (vl-elabtraversal-fix y))
      (vl-elabtraversals-remove-common-prefix (cdr x)
                                              (cdr y)))))

Theorem: vl-elabtraversal-p-of-vl-elabtraversals-remove-common-prefix.x-suffix

(defthm
 vl-elabtraversal-p-of-vl-elabtraversals-remove-common-prefix.x-suffix
 (b* (((mv ?x-suffix ?y-suffix)
       (vl-elabtraversals-remove-common-prefix x y)))
   (vl-elabtraversal-p x-suffix))
 :rule-classes :rewrite)

Theorem: vl-elabtraversal-p-of-vl-elabtraversals-remove-common-prefix.y-suffix

(defthm
 vl-elabtraversal-p-of-vl-elabtraversals-remove-common-prefix.y-suffix
 (b* (((mv ?x-suffix ?y-suffix)
       (vl-elabtraversals-remove-common-prefix x y)))
   (vl-elabtraversal-p y-suffix))
 :rule-classes :rewrite)

Theorem: vl-elabtraversals-remove-common-prefix-of-vl-elabtraversal-fix-x

(defthm
   vl-elabtraversals-remove-common-prefix-of-vl-elabtraversal-fix-x
 (equal
    (vl-elabtraversals-remove-common-prefix (vl-elabtraversal-fix x)
                                            y)
    (vl-elabtraversals-remove-common-prefix x y)))

Theorem: vl-elabtraversals-remove-common-prefix-vl-elabtraversal-equiv-congruence-on-x

(defthm
 vl-elabtraversals-remove-common-prefix-vl-elabtraversal-equiv-congruence-on-x
 (implies
      (vl-elabtraversal-equiv x x-equiv)
      (equal (vl-elabtraversals-remove-common-prefix x y)
             (vl-elabtraversals-remove-common-prefix x-equiv y)))
 :rule-classes :congruence)

Theorem: vl-elabtraversals-remove-common-prefix-of-vl-elabtraversal-fix-y

(defthm
   vl-elabtraversals-remove-common-prefix-of-vl-elabtraversal-fix-y
  (equal (vl-elabtraversals-remove-common-prefix
              x (vl-elabtraversal-fix y))
         (vl-elabtraversals-remove-common-prefix x y)))

Theorem: vl-elabtraversals-remove-common-prefix-vl-elabtraversal-equiv-congruence-on-y

(defthm
 vl-elabtraversals-remove-common-prefix-vl-elabtraversal-equiv-congruence-on-y
 (implies
      (vl-elabtraversal-equiv y y-equiv)
      (equal (vl-elabtraversals-remove-common-prefix x y)
             (vl-elabtraversals-remove-common-prefix x y-equiv)))
 :rule-classes :congruence)