Adding N-bit unsigneds with a carry bit creates an N+1 bit unsigned.

ACL2's fancy unification stuff means this works fine in the common case that you're dealing with quoted constants for N and N+1. See also basic-unsigned-byte-p-of-+.

**Theorem: **

(defthm basic-unsigned-byte-p-of-+-with-cin (implies (and (bitp cin) (unsigned-byte-p n a) (unsigned-byte-p n b)) (unsigned-byte-p (+ 1 n) (+ cin a b))) :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (bitp cin) (unsigned-byte-p n a) (unsigned-byte-p n b)) (unsigned-byte-p (+ 1 n) (+ a b cin))))))