		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-execution-rules

Atc-exec-obj-declon-rules

Rules for exec-block-item.

Definitions and Theorems

Theorem: exec-obj-declon-open

(defthm exec-obj-declon-open
  (implies
       (and (syntaxp (quotep declon))
            (not (zp limit))
            (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-obj-declon declon compst fenv limit)
              compst2)))