		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Desiniter-list-formalp

Check if all the initializers with optional designations in a list have formal dynamic semantics.

Signature
(desiniter-list-formalp desiniters) → yes/no
Arguments: desiniters — Guard (desiniter-listp desiniters).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: desiniter-list-formalp

(defun desiniter-list-formalp (desiniters)
  (declare (xargs :guard (desiniter-listp desiniters)))
  (declare (xargs :guard (desiniter-list-unambp desiniters)))
  (let ((__function__ 'desiniter-list-formalp))
    (declare (ignorable __function__))
    (or (endp desiniters)
        (and (desiniter-formalp (car desiniters))
             (desiniter-list-formalp (cdr desiniters))))))

Theorem: booleanp-of-desiniter-list-formalp

(defthm booleanp-of-desiniter-list-formalp
  (b* ((yes/no (desiniter-list-formalp desiniters)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: desiniter-list-formalp-of-desiniter-list-fix-desiniters

(defthm desiniter-list-formalp-of-desiniter-list-fix-desiniters
  (equal (desiniter-list-formalp (desiniter-list-fix desiniters))
         (desiniter-list-formalp desiniters)))

Theorem: desiniter-list-formalp-desiniter-list-equiv-congruence-on-desiniters

(defthm
 desiniter-list-formalp-desiniter-list-equiv-congruence-on-desiniters
 (implies (desiniter-list-equiv desiniters desiniters-equiv)
          (equal (desiniter-list-formalp desiniters)
                 (desiniter-list-formalp desiniters-equiv)))
 :rule-classes :congruence)