Adding N+1 bit signeds with a carry bit creates an N+1 bit signed.

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-signed-byte-p-of-+.

**Theorem: **

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