		Search-engine friendly clone of the ACL2 documentation.

Path

Path-append

Signature
(path-append x y) → new-path
Arguments: x — Guard (path-p x).; y — Guard (path-p y).
Returns: new-path — Type (path-p new-path).

Definitions and Theorems

Function: path-append

(defun path-append (x y)
  (declare (xargs :guard (and (path-p x) (path-p y))))
  (let ((__function__ 'path-append))
    (declare (ignorable __function__))
    (path-case
         x
         :wire (make-path-scope :subpath y
                                :namespace x.name)
         :scope (make-path-scope :subpath (path-append x.subpath y)
                                 :namespace x.namespace))))

Theorem: path-p-of-path-append

(defthm path-p-of-path-append
  (b* ((new-path (path-append x y)))
    (path-p new-path))
  :rule-classes :rewrite)

Theorem: path-append-of-path-fix-x

(defthm path-append-of-path-fix-x
  (equal (path-append (path-fix x) y)
         (path-append x y)))

Theorem: path-append-path-equiv-congruence-on-x

(defthm path-append-path-equiv-congruence-on-x
  (implies (path-equiv x x-equiv)
           (equal (path-append x y)
                  (path-append x-equiv y)))
  :rule-classes :congruence)

Theorem: path-append-of-path-fix-y

(defthm path-append-of-path-fix-y
  (equal (path-append x (path-fix y))
         (path-append x y)))

Theorem: path-append-path-equiv-congruence-on-y

(defthm path-append-path-equiv-congruence-on-y
  (implies (path-equiv y y-equiv)
           (equal (path-append x y)
                  (path-append x y-equiv)))
  :rule-classes :congruence)