Rules for exec-block-item.
Theorem:
(defthm exec-block-item-when-declon (implies (and (syntaxp (quotep item)) (equal (block-item-kind item) :declon) (not (zp limit)) (equal declon (block-item-declon->get item)) (equal var+scspec+tyname+init (obj-declon-to-ident+scspec+tyname+init declon)) (equal var (mv-nth 0 var+scspec+tyname+init)) (equal scspec (mv-nth 1 var+scspec+tyname+init)) (equal tyname (mv-nth 2 var+scspec+tyname+init)) (equal init (mv-nth 3 var+scspec+tyname+init)) (scspecseq-case scspec :none) init (equal type (tyname-to-type tyname)) (not (type-case type :array)) (equal ival+compst1 (exec-initer init compst fenv (1- limit))) (equal ival (mv-nth 0 ival+compst1)) (equal compst1 (mv-nth 1 ival+compst1)) (init-valuep ival) (equal val (init-value-to-value type ival)) (valuep val) (equal compst2 (create-var var val compst1)) (compustatep compst2)) (equal (exec-block-item item compst fenv limit) (mv nil compst2))))
Theorem:
(defthm exec-block-item-when-stmt (implies (and (syntaxp (quotep item)) (equal (block-item-kind item) :stmt) (not (zp limit))) (equal (exec-block-item item compst fenv limit) (exec-stmt (block-item-stmt->get item) compst fenv (1- limit)))))