Rules for exec-expr-pure-list.
Theorem:
(defthm exec-expr-pure-list-of-nil (equal (exec-expr-pure-list nil compst) nil))
Theorem:
(defthm exec-expr-pure-list-when-consp (implies (and (syntaxp (quotep es)) (consp es) (equal eval (exec-expr-pure (car es) compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (equal vals (exec-expr-pure-list (cdr es) compst)) (value-listp vals)) (equal (exec-expr-pure-list es compst) (cons val vals))))