		Search-engine friendly clone of the ACL2 documentation.

Html-encode-push

Repeated-revappend

Signature
(repeated-revappend n x y) → *
Arguments: n — Guard (natp n).

Definitions and Theorems

Function: repeated-revappend

(defun repeated-revappend (n x y)
  (declare (xargs :guard (natp n)))
  (let ((acl2::__function__ 'repeated-revappend))
    (declare (ignorable acl2::__function__))
    (if (zp n)
        y
      (repeated-revappend (- n 1)
                          x
                          (acl2::revappend-without-guard x y)))))

Theorem: character-listp-of-repeated-revappend

(defthm character-listp-of-repeated-revappend
  (implies (and (character-listp x)
                (character-listp y))
           (character-listp (repeated-revappend n x y))))

Theorem: repeated-revappend-of-nfix-n

(defthm repeated-revappend-of-nfix-n
  (equal (repeated-revappend (nfix n) x y)
         (repeated-revappend n x y)))

Theorem: repeated-revappend-nat-equiv-congruence-on-n

(defthm repeated-revappend-nat-equiv-congruence-on-n
  (implies (acl2::nat-equiv n n-equiv)
           (equal (repeated-revappend n x y)
                  (repeated-revappend n-equiv x y)))
  :rule-classes :congruence)