		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)