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