		Search-engine friendly clone of the ACL2 documentation.

List-utilities

List-len-const-theorems

Some theorems about lists whose lengths are (i) equal, (ii) equal or above, or (iii) above constant values.

These theorems are disabled by default. They can be enabled to turn assertions about lengths and constants into assertions about consp and cdr: the expansion terminates because of the syntaxp restriction.

Definitions and Theorems

Theorem: equal-len-const

(defthm equal-len-const
        (implies (syntaxp (quotep c))
                 (equal (equal (len x) c)
                        (if (natp c)
                            (if (equal c 0)
                                (not (consp x))
                                (and (consp x)
                                     (equal (len (cdr x)) (1- c))))
                            nil))))

Theorem: gteq-len-const

(defthm gteq-len-const
        (implies (syntaxp (quotep c))
                 (equal (>= (len x) c)
                        (or (<= (fix c) 0)
                            (and (consp x)
                                 (>= (len (cdr x)) (1- c)))))))

Theorem: gt-len-const

(defthm gt-len-const
        (implies (syntaxp (quotep c))
                 (equal (> (len x) c)
                        (or (< (fix c) 0)
                            (and (consp x)
                                 (> (len (cdr x)) (1- c)))))))