		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-execution-rules

Atc-exec-block-item-rules

Rules for exec-block-item.

Definitions and Theorems

Theorem: exec-block-item-when-declon

(defthm exec-block-item-when-declon
  (implies
       (and (syntaxp (quotep item))
            (equal (block-item-kind item) :declon)
            (equal declon (block-item-declon->get item))
            (not (zp limit))
            (equal compst1
                   (exec-obj-declon declon compst fenv (1- limit)))
            (compustatep compst1))
       (equal (exec-block-item item compst fenv limit)
              (mv (stmt-value-none) compst1))))

Theorem: exec-block-item-when-stmt

(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)))))