Rules for exec-expr-call-or-asg.
Theorem:
(defthm exec-expr-call-or-asg-when-call (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :call) (not (zp limit)) (equal val?+compst1 (exec-expr-call (expr-call->fun e) (expr-call->args e) compst fenv (1- limit))) (equal val? (mv-nth 0 val?+compst1)) (equal compst1 (mv-nth 1 val?+compst1)) (value-optionp val?)) (equal (exec-expr-call-or-asg e compst fenv limit) compst1)))
Theorem:
(defthm exec-expr-call-or-asg-when-asg (implies (and (syntaxp (quotep e)) (not (equal (expr-kind e) :call)) (not (zp limit)) (compustatep compst)) (equal (exec-expr-call-or-asg e compst fenv limit) (exec-expr-asg e compst fenv (1- limit)))))