Rules for exec-expr-call-or-pure.
Theorem:
(defthm exec-expr-call-or-pure-when-pure (implies (and (syntaxp (quotep e)) (not (equal (expr-kind e) :call)) (not (zp limit)) (compustatep compst) (equal eval (exec-expr-pure e compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1)) (equal (exec-expr-call-or-pure e compst fenv limit) (mv (expr-value->value eval1) compst))))
Theorem:
(defthm exec-expr-call-or-pure-when-call (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :call) (not (zp limit))) (equal (exec-expr-call-or-pure e compst fenv limit) (exec-expr-call (expr-call->fun e) (expr-call->args e) compst fenv (1- limit)))))