suffixp

(in-package "ACL2")

(defsection suffixp
  :parents (std/lists)
  :short "@(call suffixp) determines if the list @('x') occurs at the end of
the list @('y')."
  :long "<p>For example:</p>

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

  <p>Note that the check is carried out using @('equal'), so the final cdr
  of the list is considered relevant.  That is,</p>

  @({
      (suffixp '(3 4 5 . 6) '(1 2 3 4 5 . 6)) = t
      (suffixp '(3 4 5)     '(1 2 3 4 5 . 6)) = nil
  })"
  (defund suffixp
    (x y)
    (declare (xargs :guard t))
    (or (equal x y) (and (consp y) (suffixp x (cdr y)))))
  (local (in-theory (enable suffixp)))
  (defthm suffixp-of-cons-right
    (equal (suffixp a (cons c b))
      (or (equal a (cons c b)) (suffixp a b))))
  (defthm not-suffixp-of-cons-left
    (implies (not (suffixp a b)) (not (suffixp (cons c a) b))))
  (defthm suffixp-of-self (suffixp x x))
  (defthm suffixp-transitive
    (implies (and (suffixp b c) (suffixp a b)) (suffixp a c)))
  "<p>Note that the following is disabled by default:</p>"
  (defthmd suffixp-equals-nthcdr
    (equal (suffixp x y)
      (equal x (nthcdr (- (len y) (len x)) y)))))