Adding N-bit unsigneds 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-+-with-cin.

**Theorem: **

(defthm basic-unsigned-byte-p-of-+ (implies (and (unsigned-byte-p n a) (unsigned-byte-p n b)) (unsigned-byte-p (+ 1 n) (+ a b))))