(vcd-index->codechars x) → chars
Function:
(defun vcd-index->codechars (x) (declare (xargs :guard (natp x))) (let ((__function__ 'vcd-index->codechars)) (declare (ignorable __function__)) (b* ((first (code-char (+ 33 (mod (lnfix x) 94)))) (rest (floor (lnfix x) 94)) ((when (zp rest)) (list first))) (cons first (vcd-index->codechars rest)))))
Theorem:
(defthm character-listp-of-vcd-index->codechars (b* ((chars (vcd-index->codechars x))) (character-listp chars)) :rule-classes :rewrite)
Theorem:
(defthm vcd-index->codechars-of-nfix-x (equal (vcd-index->codechars (nfix x)) (vcd-index->codechars x)))
Theorem:
(defthm vcd-index->codechars-nat-equiv-congruence-on-x (implies (nat-equiv x x-equiv) (equal (vcd-index->codechars x) (vcd-index->codechars x-equiv))) :rule-classes :congruence)