		Search-engine friendly clone of the ACL2 documentation.

Suffixp

(suffixp x y) determines if the list x occurs at the end of the list y.

For example:

(suffixp '(3 4 5) '(1 2 3 4 5)) == t
(suffixp '(a b c) '(1 2 3 4 5)) == nil

Note that the check is carried out using equal, so the final cdr of the list is considered relevant. That is,

(suffixp '(3 4 5 . 6) '(1 2 3 4 5 . 6)) = t
(suffixp '(3 4 5)     '(1 2 3 4 5 . 6)) = nil

Function: suffixp

(defun suffixp (x y)
  (declare (xargs :guard t))
  (or (equal x y)
      (and (consp y) (suffixp x (cdr y)))))

Theorem: suffixp-of-cons-right

(defthm suffixp-of-cons-right
  (equal (suffixp a (cons c b))
         (or (equal a (cons c b))
             (suffixp a b))))

Theorem: not-suffixp-of-cons-left

(defthm not-suffixp-of-cons-left
  (implies (not (suffixp a b))
           (not (suffixp (cons c a) b))))

Theorem: suffixp-of-self

(defthm suffixp-of-self (suffixp x x))

Theorem: suffixp-transitive

(defthm suffixp-transitive
  (implies (and (suffixp b c) (suffixp a b))
           (suffixp a c)))

Note that the following is disabled by default:

Theorem: suffixp-equals-nthcdr

(defthm suffixp-equals-nthcdr
  (equal (suffixp x y)
         (equal x (nthcdr (- (len y) (len x)) y))))