Check if all the structure declarations in a list have formal dynamic semantics.
(structdecl-list-formalp structdecls) → yes/no
Function:
(defun structdecl-list-formalp (structdecls) (declare (xargs :guard (structdecl-listp structdecls))) (declare (xargs :guard (structdecl-list-unambp structdecls))) (let ((__function__ 'structdecl-list-formalp)) (declare (ignorable __function__)) (or (endp structdecls) (and (structdecl-formalp (car structdecls)) (structdecl-list-formalp (cdr structdecls))))))
Theorem:
(defthm booleanp-of-structdecl-list-formalp (b* ((yes/no (structdecl-list-formalp structdecls))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm structdecl-list-formalp-of-structdecl-list-fix-structdecls (equal (structdecl-list-formalp (structdecl-list-fix structdecls)) (structdecl-list-formalp structdecls)))
Theorem:
(defthm structdecl-list-formalp-structdecl-list-equiv-congruence-on-structdecls (implies (structdecl-list-equiv structdecls structdecls-equiv) (equal (structdecl-list-formalp structdecls) (structdecl-list-formalp structdecls-equiv))) :rule-classes :congruence)