		Search-engine friendly clone of the ACL2 documentation.

Format-strings

Format-string-containers-aux

Signature
(format-string-containers-aux elements) → n
Arguments: elements — Guard (char/container-listp elements).
Returns: n — Type (natp n).

Definitions and Theorems

Function: format-string-containers-aux

(defun format-string-containers-aux (elements)
  (declare (xargs :guard (char/container-listp elements)))
  (let ((__function__ 'format-string-containers-aux))
    (declare (ignorable __function__))
    (b* (((when (endp elements)) 0)
         (element (car elements))
         (n1 (char/container-case element
                                  :char 0
                                  :container 1))
         (n2 (format-string-containers-aux (cdr elements))))
      (+ n1 n2))))

Theorem: natp-of-format-string-containers-aux

(defthm natp-of-format-string-containers-aux
  (b* ((n (format-string-containers-aux elements)))
    (natp n))
  :rule-classes :rewrite)

Theorem: format-string-containers-aux-of-char/container-list-fix-elements

(defthm
   format-string-containers-aux-of-char/container-list-fix-elements
 (equal
   (format-string-containers-aux (char/container-list-fix elements))
   (format-string-containers-aux elements)))

Theorem: format-string-containers-aux-char/container-list-equiv-congruence-on-elements

(defthm
 format-string-containers-aux-char/container-list-equiv-congruence-on-elements
 (implies (char/container-list-equiv elements elements-equiv)
          (equal (format-string-containers-aux elements)
                 (format-string-containers-aux elements-equiv)))
 :rule-classes :congruence)