Logically simple definition that is similar to nat-to-bin-chars.
(basic-nat-to-bin-chars n) → chars
This almost computes
Function:
(defun basic-nat-to-bin-chars (n) (declare (xargs :guard (natp n))) (let ((acl2::__function__ 'basic-nat-to-bin-chars)) (declare (ignorable acl2::__function__)) (if (zp n) nil (cons (if (eql (the bit (logand n 1)) 1) #\1 #\0) (basic-nat-to-bin-chars (ash n -1))))))
Theorem:
(defthm bin-digit-char-list*p-of-basic-nat-to-bin-chars (b* ((chars (basic-nat-to-bin-chars n))) (bin-digit-char-list*p chars)) :rule-classes :rewrite)
Theorem:
(defthm basic-nat-to-bin-chars-when-zp (implies (zp n) (equal (basic-nat-to-bin-chars n) nil)))
Theorem:
(defthm true-listp-of-basic-nat-to-bin-chars (true-listp (basic-nat-to-bin-chars n)) :rule-classes :type-prescription)
Theorem:
(defthm character-listp-of-basic-nat-to-bin-chars (character-listp (basic-nat-to-bin-chars n)))
Theorem:
(defthm basic-nat-to-bin-chars-under-iff (iff (basic-nat-to-bin-chars n) (not (zp n))))
Theorem:
(defthm consp-of-basic-nat-to-bin-chars (equal (consp (basic-nat-to-bin-chars n)) (if (basic-nat-to-bin-chars n) t nil)))
Theorem:
(defthm basic-nat-to-bin-chars-one-to-one (equal (equal (basic-nat-to-bin-chars n) (basic-nat-to-bin-chars m)) (equal (nfix n) (nfix m))))