sumlist

(in-package "ACL2")

(defun sumlist
  (x)
  (if (consp x)
    (+ (car x) (sumlist (cdr x)))
    0))

(defthm rationalp-sumlist
  (implies (rational-listp x) (rationalp (sumlist x))))

(defthm sumlist-append
  (equal (sumlist (append x y)) (+ (sumlist x) (sumlist y))))