Constraints induced by parse-bit.
Theorem: constraints-from-parse-bit
(defthm constraints-from-parse-bit (implies (not (mv-nth 0 (parse-bit input))) (member-equal (car input) (chars=>nats '(#\0 #\1)))) :rule-classes nil)