		Search-engine friendly clone of the ACL2 documentation.

Stv-number-of-phases

Stv-max-phases-in-lines

Signature
(stv-max-phases-in-lines lines) → max-phases
Arguments: lines — Guard (true-list-listp lines).
Returns: max-phases — Type (natp max-phases).

Definitions and Theorems

Function: stv-max-phases-in-lines

(defun stv-max-phases-in-lines (lines)
       (declare (xargs :guard (true-list-listp lines)))
       (let ((__function__ 'stv-max-phases-in-lines))
            (declare (ignorable __function__))
            (if (atom lines)
                0
                (max (length (cdr (car lines)))
                     (stv-max-phases-in-lines (cdr lines))))))

Theorem: natp-of-stv-max-phases-in-lines

(defthm natp-of-stv-max-phases-in-lines
        (b* ((max-phases (stv-max-phases-in-lines lines)))
            (natp max-phases))
        :rule-classes :type-prescription)