• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
        • Syntax-for-tools
        • Atc
        • Language
          • Abstract-syntax
          • Integer-ranges
          • Dynamic-semantics
            • Exec
              • Exec-expr-asg
              • Exec-fun
              • Exec-block-item
              • Exec-expr-call-or-pure
              • Exec-block-item-list
              • Exec-stmt-while
              • Exec-stmt
              • Exec-initer
              • Exec-expr-call-or-asg
              • Exec-expr-call
            • Exec-arrsub
            • Exec-expr-pure
            • Exec-expr-asg
            • Init-value-to-value
            • Exec-memberp
            • Exec-address
            • Apconvert-expr-value
            • Exec-member
            • Exec-unary
            • Init-scope
            • Exec-fun
            • Eval-iconst
            • Exec-block-item
            • Exec-binary-strict-pure
            • Exec-expr-pure-list
            • Eval-binary-strict-pure
            • Exec-expr-call-or-pure
            • Exec-block-item-list
            • Exec-stmt-while
            • Exec-indir
            • Exec-stmt
            • Exec-ident
            • Eval-cast
            • Exec-cast
            • Eval-unary
            • Exec-const
            • Exec-initer
            • Exec-expr-call-or-asg
            • Eval-const
            • Exec-expr-call
          • Static-semantics
          • Grammar
          • Integer-formats
          • Types
          • Portable-ascii-identifiers
          • Values
          • Integer-operations
          • Computation-states
          • Object-designators
          • Implementation-environments
          • Operations
          • Errors
          • Tag-environments
          • Function-environments
          • Character-sets
          • Flexible-array-member-removal
          • Arithmetic-operations
          • Pointer-operations
          • Bytes
          • Keywords
          • Real-operations
          • Array-operations
          • Scalar-operations
          • Structure-operations
        • Representation
        • Transformation-tools
        • Pack
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Dynamic-semantics

Exec

Mutually recursive functions for execution.

Definitions and Theorems

Function: exec-expr-call

(defun exec-expr-call (fun args compst fenv limit)
  (declare (xargs :guard (and (identp fun)
                              (expr-listp args)
                              (compustatep compst)
                              (fun-envp fenv)
                              (natp limit))))
  (let ((__function__ 'exec-expr-call))
    (declare (ignorable __function__))
    (b* (((when (zp limit))
          (mv (error :limit)
              (compustate-fix compst)))
         (vals (exec-expr-pure-list args compst))
         ((when (errorp vals))
          (mv vals (compustate-fix compst))))
      (exec-fun fun vals compst fenv (1- limit)))))

Function: exec-expr-call-or-pure

(defun exec-expr-call-or-pure (e compst fenv limit)
  (declare (xargs :guard (and (exprp e)
                              (compustatep compst)
                              (fun-envp fenv)
                              (natp limit))))
  (let ((__function__ 'exec-expr-call-or-pure))
    (declare (ignorable __function__))
    (b* (((when (zp limit))
          (mv (error :limit)
              (compustate-fix compst)))
         (e (expr-fix e)))
      (if (expr-case e :call)
          (exec-expr-call (expr-call->fun e)
                          (expr-call->args e)
                          compst fenv (1- limit))
        (b* ((eval (exec-expr-pure e compst))
             ((when (errorp eval))
              (mv eval (compustate-fix compst)))
             (eval (apconvert-expr-value eval))
             ((when (errorp eval))
              (mv eval (compustate-fix compst))))
          (mv (expr-value->value eval)
              (compustate-fix compst)))))))

Function: exec-expr-asg

(defun exec-expr-asg (e compst fenv limit)
  (declare (xargs :guard (and (exprp e)
                              (compustatep compst)
                              (fun-envp fenv)
                              (natp limit))))
  (let ((__function__ 'exec-expr-asg))
    (declare (ignorable __function__))
    (b* (((when (zp limit)) (error :limit))
         ((unless (expr-case e :binary))
          (error (list :expr-asg-not-binary (expr-fix e))))
         (op (expr-binary->op e))
         (left (expr-binary->arg1 e))
         (right (expr-binary->arg2 e))
         ((unless (binop-case op :asg))
          (error (list :expr-asg-not-asg op)))
         ((mv val? compst)
          (if (expr-case left :ident)
              (exec-expr-call-or-pure right compst fenv (1- limit))
            (b* ((eval (exec-expr-pure right compst))
                 ((when (errorp eval)) (mv eval compst))
                 (eval (apconvert-expr-value eval))
                 ((when (errorp eval)) (mv eval compst)))
              (mv (expr-value->value eval) compst))))
         ((when (errorp val?)) val?)
         ((when (not val?))
          (error (list :asg-void-expr right)))
         (val val?)
         (eval (exec-expr-pure left compst))
         ((when (errorp eval)) eval)
         (objdes (expr-value->object eval))
         ((unless objdes)
          (error (list :not-lvalue left))))
      (write-object objdes val compst))))

Function: exec-expr-call-or-asg

(defun exec-expr-call-or-asg (e compst fenv limit)
  (declare (xargs :guard (and (exprp e)
                              (compustatep compst)
                              (fun-envp fenv)
                              (natp limit))))
  (let ((__function__ 'exec-expr-call-or-asg))
    (declare (ignorable __function__))
    (b* (((when (zp limit)) (error :limit)))
      (if (expr-case e :call)
          (b* (((mv result compst)
                (exec-expr-call (expr-call->fun e)
                                (expr-call->args e)
                                compst fenv (1- limit)))
               ((when (errorp result)) result))
            compst)
        (exec-expr-asg e compst fenv (1- limit))))))

Function: exec-fun

(defun exec-fun (fun args compst fenv limit)
  (declare (xargs :guard (and (identp fun)
                              (value-listp args)
                              (compustatep compst)
                              (fun-envp fenv)
                              (natp limit))))
  (let ((__function__ 'exec-fun))
    (declare (ignorable __function__))
    (b* (((when (zp limit))
          (mv (error :limit)
              (compustate-fix compst)))
         (info (fun-env-lookup fun fenv))
         ((when (not info))
          (mv (error (list :function-undefined (ident-fix fun)))
              (compustate-fix compst)))
         ((fun-info info) info)
         (scope (init-scope info.params args))
         ((when (errorp scope))
          (mv scope (compustate-fix compst)))
         (frame (make-frame :function fun
                            :scopes (list scope)))
         (compst (push-frame frame compst))
         ((mv val? compst)
          (exec-block-item-list info.body compst fenv (1- limit)))
         (compst (pop-frame compst))
         ((when (errorp val?)) (mv val? compst))
         ((unless (equal (type-of-value-option val?)
                         (tyname-to-type info.result)))
          (mv (error (list :return-value-mistype
                           :required info.result
                           :supplied (type-of-value-option val?)))
              compst)))
      (mv val? compst))))

Function: exec-stmt

(defun exec-stmt (s compst fenv limit)
 (declare (xargs :guard (and (stmtp s)
                             (compustatep compst)
                             (fun-envp fenv)
                             (natp limit))))
 (declare (xargs :guard (> (compustate-frames-number compst)
                           0)))
 (let ((__function__ 'exec-stmt))
  (declare (ignorable __function__))
  (b* (((when (zp limit))
        (mv (error :limit)
            (compustate-fix compst)))
       (s (stmt-fix s)))
   (stmt-case
     s :labeled
     (mv (error (list :exec-stmt s))
         (compustate-fix compst))
     :compound
     (b* ((compst (enter-scope compst))
          ((mv value? compst)
           (exec-block-item-list s.items compst fenv (1- limit))))
       (mv value? (exit-scope compst)))
     :expr
     (b* ((compst/error
               (exec-expr-call-or-asg s.get compst fenv (1- limit)))
          ((when (errorp compst/error))
           (mv compst/error (compustate-fix compst))))
       (mv nil compst/error))
     :null
     (mv (error (list :exec-stmt s))
         (compustate-fix compst))
     :if
     (b* ((test (exec-expr-pure s.test compst))
          ((when (errorp test))
           (mv test (compustate-fix compst)))
          (test (apconvert-expr-value test))
          ((when (errorp test))
           (mv test (compustate-fix compst)))
          (test (expr-value->value test))
          (test (test-value test))
          ((when (errorp test))
           (mv test (compustate-fix compst))))
       (if test (exec-stmt s.then compst fenv (1- limit))
         (mv nil (compustate-fix compst))))
     :ifelse
     (b* ((test (exec-expr-pure s.test compst))
          ((when (errorp test))
           (mv test (compustate-fix compst)))
          (test (apconvert-expr-value test))
          ((when (errorp test))
           (mv test (compustate-fix compst)))
          (test (expr-value->value test))
          (test (test-value test))
          ((when (errorp test))
           (mv test (compustate-fix compst))))
       (if test (exec-stmt s.then compst fenv (1- limit))
         (exec-stmt s.else compst fenv (1- limit))))
     :switch
     (mv (error (list :exec-stmt s))
         (compustate-fix compst))
     :while
     (exec-stmt-while s.test s.body compst fenv (1- limit))
     :dowhile
     (mv (error (list :exec-stmt s))
         (compustate-fix compst))
     :for
     (mv (error (list :exec-stmt s))
         (compustate-fix compst))
     :goto
     (mv (error (list :exec-stmt s))
         (compustate-fix compst))
     :continue
     (mv (error (list :exec-stmt s))
         (compustate-fix compst))
     :break
     (mv (error (list :exec-stmt s))
         (compustate-fix compst))
     :return
     (if
      (exprp s.value)
      (b* (((mv val? compst)
            (exec-expr-call-or-pure s.value compst fenv (1- limit)))
           ((when (errorp val?)) (mv val? compst))
           ((when (not val?))
            (mv (error (list :return-void-expr s.value))
                compst)))
        (mv val? compst))
      (mv nil (compustate-fix compst)))))))

Function: exec-stmt-while

(defun exec-stmt-while (test body compst fenv limit)
  (declare (xargs :guard (and (exprp test)
                              (stmtp body)
                              (compustatep compst)
                              (fun-envp fenv)
                              (natp limit))))
  (declare (xargs :guard (> (compustate-frames-number compst)
                            0)))
  (let ((__function__ 'exec-stmt-while))
    (declare (ignorable __function__))
    (b* (((when (zp limit))
          (mv (error :limit)
              (compustate-fix compst)))
         (test-eval (exec-expr-pure test compst))
         ((when (errorp test-eval))
          (mv test-eval (compustate-fix compst)))
         (test-eval (apconvert-expr-value test-eval))
         ((when (errorp test-eval))
          (mv test-eval (compustate-fix compst)))
         (test-val (expr-value->value test-eval))
         (continuep (test-value test-val))
         ((when (errorp continuep))
          (mv continuep (compustate-fix compst)))
         ((when (not continuep))
          (mv nil (compustate-fix compst)))
         ((mv val? compst)
          (exec-stmt body compst fenv (1- limit)))
         ((when (errorp val?)) (mv val? compst))
         ((when (valuep val?)) (mv val? compst)))
      (exec-stmt-while test body compst fenv (1- limit)))))

Function: exec-initer

(defun exec-initer (initer compst fenv limit)
 (declare (xargs :guard (and (initerp initer)
                             (compustatep compst)
                             (fun-envp fenv)
                             (natp limit))))
 (declare (xargs :guard (> (compustate-frames-number compst)
                           0)))
 (let ((__function__ 'exec-initer))
  (declare (ignorable __function__))
  (b* (((when (zp limit))
        (mv (error :limit)
            (compustate-fix compst))))
   (initer-case
     initer :single
     (b*
       (((mv val compst)
         (exec-expr-call-or-pure initer.get compst fenv (1- limit)))
        ((when (errorp val)) (mv val compst))
        ((when (not val))
         (mv (error (list :void-initializer (initer-fix initer)))
             compst))
        (ival (init-value-single val)))
       (mv ival compst))
     :list
     (b* ((vals (exec-expr-pure-list initer.get compst))
          ((when (errorp vals))
           (mv vals (compustate-fix compst)))
          (ival (init-value-list vals)))
       (mv ival (compustate-fix compst)))))))

Function: exec-block-item

(defun exec-block-item (item compst fenv limit)
 (declare (xargs :guard (and (block-itemp item)
                             (compustatep compst)
                             (fun-envp fenv)
                             (natp limit))))
 (declare
   (xargs :guard (and (> (compustate-frames-number compst) 0)
                      (> (compustate-top-frame-scopes-number compst)
                         0))))
 (let ((__function__ 'exec-block-item))
   (declare (ignorable __function__))
   (b* (((when (zp limit))
         (mv (error :limit)
             (compustate-fix compst))))
     (block-item-case
          item :declon
          (b* (((mv var scspec tyname init?)
                (obj-declon-to-ident+scspec+tyname+init item.get))
               ((unless (scspecseq-case scspec :none))
                (mv (error :unsupported-storage-class-specifier)
                    (compustate-fix compst)))
               (type (tyname-to-type tyname))
               ((when (type-case type :array))
                (mv (error :unsupported-local-array)
                    (compustate-fix compst)))
               ((when (not init?))
                (mv (error :unsupported-no-initializer)
                    (compustate-fix compst)))
               (init init?)
               ((mv ival compst)
                (exec-initer init compst fenv (1- limit)))
               ((when (errorp ival)) (mv ival compst))
               (val (init-value-to-value type ival))
               ((when (errorp val)) (mv val compst))
               (new-compst (create-var var val compst))
               ((when (errorp new-compst))
                (mv new-compst compst)))
            (mv nil new-compst))
          :stmt (exec-stmt item.get compst fenv (1- limit))))))

Function: exec-block-item-list

(defun exec-block-item-list (items compst fenv limit)
 (declare (xargs :guard (and (block-item-listp items)
                             (compustatep compst)
                             (fun-envp fenv)
                             (natp limit))))
 (declare
   (xargs :guard (and (> (compustate-frames-number compst) 0)
                      (> (compustate-top-frame-scopes-number compst)
                         0))))
 (let ((__function__ 'exec-block-item-list))
   (declare (ignorable __function__))
   (b* (((when (zp limit))
         (mv (error :limit)
             (compustate-fix compst)))
        ((when (endp items))
         (mv nil (compustate-fix compst)))
        ((mv val? compst)
         (exec-block-item (car items)
                          compst fenv (1- limit)))
        ((when (errorp val?)) (mv val? compst))
        ((when (valuep val?)) (mv val? compst)))
     (exec-block-item-list (cdr items)
                           compst fenv (1- limit)))))

Theorem: return-type-of-exec-expr-call.result

(defthm return-type-of-exec-expr-call.result
  (b* (((mv ?result ?new-compst)
        (exec-expr-call fun args compst fenv limit)))
    (value-option-resultp result))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-expr-call.new-compst

(defthm return-type-of-exec-expr-call.new-compst
  (b* (((mv ?result ?new-compst)
        (exec-expr-call fun args compst fenv limit)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-expr-call-or-pure.result

(defthm return-type-of-exec-expr-call-or-pure.result
  (b* (((mv ?result ?new-compst)
        (exec-expr-call-or-pure e compst fenv limit)))
    (value-option-resultp result))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-expr-call-or-pure.new-compst

(defthm return-type-of-exec-expr-call-or-pure.new-compst
  (b* (((mv ?result ?new-compst)
        (exec-expr-call-or-pure e compst fenv limit)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-expr-asg.new-compst

(defthm return-type-of-exec-expr-asg.new-compst
  (b* ((?new-compst (exec-expr-asg e compst fenv limit)))
    (compustate-resultp new-compst))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-expr-call-or-asg.new-compst

(defthm return-type-of-exec-expr-call-or-asg.new-compst
  (b* ((?new-compst (exec-expr-call-or-asg e compst fenv limit)))
    (compustate-resultp new-compst))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-fun.result

(defthm return-type-of-exec-fun.result
  (b* (((mv ?result ?new-compst)
        (exec-fun fun args compst fenv limit)))
    (value-option-resultp result))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-fun.new-compst

(defthm return-type-of-exec-fun.new-compst
  (b* (((mv ?result ?new-compst)
        (exec-fun fun args compst fenv limit)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-stmt.result

(defthm return-type-of-exec-stmt.result
  (b* (((mv ?result ?new-compst)
        (exec-stmt s compst fenv limit)))
    (value-option-resultp result))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-stmt.new-compst

(defthm return-type-of-exec-stmt.new-compst
  (b* (((mv ?result ?new-compst)
        (exec-stmt s compst fenv limit)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-stmt-while.result

(defthm return-type-of-exec-stmt-while.result
  (b* (((mv ?result ?new-compst)
        (exec-stmt-while test body compst fenv limit)))
    (value-option-resultp result))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-stmt-while.new-compst

(defthm return-type-of-exec-stmt-while.new-compst
  (b* (((mv ?result ?new-compst)
        (exec-stmt-while test body compst fenv limit)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-initer.result

(defthm return-type-of-exec-initer.result
  (b* (((mv ?result ?new-compst)
        (exec-initer initer compst fenv limit)))
    (init-value-resultp result))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-initer.new-compst

(defthm return-type-of-exec-initer.new-compst
  (b* (((mv ?result ?new-compst)
        (exec-initer initer compst fenv limit)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-block-item.result

(defthm return-type-of-exec-block-item.result
  (b* (((mv ?result ?new-compst)
        (exec-block-item item compst fenv limit)))
    (value-option-resultp result))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-block-item.new-compst

(defthm return-type-of-exec-block-item.new-compst
  (b* (((mv ?result ?new-compst)
        (exec-block-item item compst fenv limit)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-block-item-list.result

(defthm return-type-of-exec-block-item-list.result
  (b* (((mv ?result ?new-compst)
        (exec-block-item-list items compst fenv limit)))
    (value-option-resultp result))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-block-item-list.new-compst

(defthm return-type-of-exec-block-item-list.new-compst
  (b* (((mv ?result ?new-compst)
        (exec-block-item-list items compst fenv limit)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: compustate-frames-number-of-exec-expr-call

(defthm compustate-frames-number-of-exec-expr-call
  (b* (((mv ?result ?new-compst)
        (exec-expr-call fun args compst fenv limit)))
    (equal (compustate-frames-number new-compst)
           (compustate-frames-number compst))))

Theorem: compustate-frames-number-of-exec-expr-call-or-pure

(defthm compustate-frames-number-of-exec-expr-call-or-pure
  (b* (((mv ?result ?new-compst)
        (exec-expr-call-or-pure e compst fenv limit)))
    (equal (compustate-frames-number new-compst)
           (compustate-frames-number compst))))

Theorem: compustate-frames-number-of-exec-expr-asg

(defthm compustate-frames-number-of-exec-expr-asg
  (b* ((?new-compst (exec-expr-asg e compst fenv limit)))
    (implies (compustatep new-compst)
             (equal (compustate-frames-number new-compst)
                    (compustate-frames-number compst)))))

Theorem: compustate-frames-number-of-exec-expr-call-or-asg

(defthm compustate-frames-number-of-exec-expr-call-or-asg
  (b* ((?new-compst (exec-expr-call-or-asg e compst fenv limit)))
    (implies (compustatep new-compst)
             (equal (compustate-frames-number new-compst)
                    (compustate-frames-number compst)))))

Theorem: compustate-frames-number-of-exec-fun

(defthm compustate-frames-number-of-exec-fun
  (b* (((mv ?result ?new-compst)
        (exec-fun fun args compst fenv limit)))
    (equal (compustate-frames-number new-compst)
           (compustate-frames-number compst))))

Theorem: compustate-frames-number-of-exec-stmt

(defthm compustate-frames-number-of-exec-stmt
  (implies (> (compustate-frames-number compst) 0)
           (b* (((mv ?result ?new-compst)
                 (exec-stmt s compst fenv limit)))
             (equal (compustate-frames-number new-compst)
                    (compustate-frames-number compst)))))

Theorem: compustate-frames-number-of-exec-stmt-while

(defthm compustate-frames-number-of-exec-stmt-while
  (implies (> (compustate-frames-number compst) 0)
           (b* (((mv ?result ?new-compst)
                 (exec-stmt-while test body compst fenv limit)))
             (equal (compustate-frames-number new-compst)
                    (compustate-frames-number compst)))))

Theorem: compustate-frames-number-of-exec-initer

(defthm compustate-frames-number-of-exec-initer
  (implies (> (compustate-frames-number compst) 0)
           (b* (((mv ?result ?new-compst)
                 (exec-initer initer compst fenv limit)))
             (equal (compustate-frames-number new-compst)
                    (compustate-frames-number compst)))))

Theorem: compustate-frames-number-of-exec-block-item

(defthm compustate-frames-number-of-exec-block-item
  (implies (> (compustate-frames-number compst) 0)
           (b* (((mv ?result ?new-compst)
                 (exec-block-item item compst fenv limit)))
             (equal (compustate-frames-number new-compst)
                    (compustate-frames-number compst)))))

Theorem: compustate-frames-number-of-exec-block-item-list

(defthm compustate-frames-number-of-exec-block-item-list
  (implies (> (compustate-frames-number compst) 0)
           (b* (((mv ?result ?new-compst)
                 (exec-block-item-list items compst fenv limit)))
             (equal (compustate-frames-number new-compst)
                    (compustate-frames-number compst)))))

Theorem: compustate-scopes-numbers-of-exec-expr-call

(defthm compustate-scopes-numbers-of-exec-expr-call
  (b* (((mv ?result ?new-compst)
        (exec-expr-call fun args compst fenv limit)))
    (equal (compustate-scopes-numbers new-compst)
           (compustate-scopes-numbers compst))))

Theorem: compustate-scopes-numbers-of-exec-expr-call-or-pure

(defthm compustate-scopes-numbers-of-exec-expr-call-or-pure
  (b* (((mv ?result ?new-compst)
        (exec-expr-call-or-pure e compst fenv limit)))
    (equal (compustate-scopes-numbers new-compst)
           (compustate-scopes-numbers compst))))

Theorem: compustate-scopes-numbers-of-exec-expr-asg

(defthm compustate-scopes-numbers-of-exec-expr-asg
  (b* ((?new-compst (exec-expr-asg e compst fenv limit)))
    (implies (compustatep new-compst)
             (equal (compustate-scopes-numbers new-compst)
                    (compustate-scopes-numbers compst)))))

Theorem: compustate-scopes-numbers-of-exec-expr-call-or-asg

(defthm compustate-scopes-numbers-of-exec-expr-call-or-asg
  (b* ((?new-compst (exec-expr-call-or-asg e compst fenv limit)))
    (implies (compustatep new-compst)
             (equal (compustate-scopes-numbers new-compst)
                    (compustate-scopes-numbers compst)))))

Theorem: compustate-scopes-numbers-of-exec-fun

(defthm compustate-scopes-numbers-of-exec-fun
  (b* (((mv ?result ?new-compst)
        (exec-fun fun args compst fenv limit)))
    (equal (compustate-scopes-numbers new-compst)
           (compustate-scopes-numbers compst)))
  :rule-classes nil)

Theorem: compustate-scopes-numbers-of-exec-stmt

(defthm compustate-scopes-numbers-of-exec-stmt
  (implies (> (compustate-frames-number compst) 0)
           (b* (((mv ?result ?new-compst)
                 (exec-stmt s compst fenv limit)))
             (equal (compustate-scopes-numbers new-compst)
                    (compustate-scopes-numbers compst)))))

Theorem: compustate-scopes-numbers-of-exec-stmt-while

(defthm compustate-scopes-numbers-of-exec-stmt-while
  (implies (> (compustate-frames-number compst) 0)
           (b* (((mv ?result ?new-compst)
                 (exec-stmt-while test body compst fenv limit)))
             (equal (compustate-scopes-numbers new-compst)
                    (compustate-scopes-numbers compst)))))

Theorem: compustate-scopes-numbers-of-exec-initer

(defthm compustate-scopes-numbers-of-exec-initer
  (implies (and (> (compustate-frames-number compst) 0)
                (> (compustate-top-frame-scopes-number compst)
                   0))
           (b* (((mv ?result ?new-compst)
                 (exec-initer initer compst fenv limit)))
             (equal (compustate-scopes-numbers new-compst)
                    (compustate-scopes-numbers compst)))))

Theorem: compustate-scopes-numbers-of-exec-block-item

(defthm compustate-scopes-numbers-of-exec-block-item
  (implies (and (> (compustate-frames-number compst) 0)
                (> (compustate-top-frame-scopes-number compst)
                   0))
           (b* (((mv ?result ?new-compst)
                 (exec-block-item item compst fenv limit)))
             (equal (compustate-scopes-numbers new-compst)
                    (compustate-scopes-numbers compst)))))

Theorem: compustate-scopes-numbers-of-exec-block-item-list

(defthm compustate-scopes-numbers-of-exec-block-item-list
  (implies (and (> (compustate-frames-number compst) 0)
                (> (compustate-top-frame-scopes-number compst)
                   0))
           (b* (((mv ?result ?new-compst)
                 (exec-block-item-list items compst fenv limit)))
             (equal (compustate-scopes-numbers new-compst)
                    (compustate-scopes-numbers compst)))))

Theorem: exec-expr-call-of-ident-fix-fun

(defthm exec-expr-call-of-ident-fix-fun
  (equal (exec-expr-call (ident-fix fun)
                         args compst fenv limit)
         (exec-expr-call fun args compst fenv limit)))

Theorem: exec-expr-call-of-expr-list-fix-args

(defthm exec-expr-call-of-expr-list-fix-args
  (equal (exec-expr-call fun (expr-list-fix args)
                         compst fenv limit)
         (exec-expr-call fun args compst fenv limit)))

Theorem: exec-expr-call-of-compustate-fix-compst

(defthm exec-expr-call-of-compustate-fix-compst
  (equal (exec-expr-call fun args (compustate-fix compst)
                         fenv limit)
         (exec-expr-call fun args compst fenv limit)))

Theorem: exec-expr-call-of-fun-env-fix-fenv

(defthm exec-expr-call-of-fun-env-fix-fenv
  (equal (exec-expr-call fun args compst (fun-env-fix fenv)
                         limit)
         (exec-expr-call fun args compst fenv limit)))

Theorem: exec-expr-call-of-nfix-limit

(defthm exec-expr-call-of-nfix-limit
  (equal (exec-expr-call fun args compst fenv (nfix limit))
         (exec-expr-call fun args compst fenv limit)))

Theorem: exec-expr-call-or-pure-of-expr-fix-e

(defthm exec-expr-call-or-pure-of-expr-fix-e
  (equal (exec-expr-call-or-pure (expr-fix e)
                                 compst fenv limit)
         (exec-expr-call-or-pure e compst fenv limit)))

Theorem: exec-expr-call-or-pure-of-compustate-fix-compst

(defthm exec-expr-call-or-pure-of-compustate-fix-compst
  (equal (exec-expr-call-or-pure e (compustate-fix compst)
                                 fenv limit)
         (exec-expr-call-or-pure e compst fenv limit)))

Theorem: exec-expr-call-or-pure-of-fun-env-fix-fenv

(defthm exec-expr-call-or-pure-of-fun-env-fix-fenv
  (equal (exec-expr-call-or-pure e compst (fun-env-fix fenv)
                                 limit)
         (exec-expr-call-or-pure e compst fenv limit)))

Theorem: exec-expr-call-or-pure-of-nfix-limit

(defthm exec-expr-call-or-pure-of-nfix-limit
  (equal (exec-expr-call-or-pure e compst fenv (nfix limit))
         (exec-expr-call-or-pure e compst fenv limit)))

Theorem: exec-expr-asg-of-expr-fix-e

(defthm exec-expr-asg-of-expr-fix-e
  (equal (exec-expr-asg (expr-fix e)
                        compst fenv limit)
         (exec-expr-asg e compst fenv limit)))

Theorem: exec-expr-asg-of-compustate-fix-compst

(defthm exec-expr-asg-of-compustate-fix-compst
  (equal (exec-expr-asg e (compustate-fix compst)
                        fenv limit)
         (exec-expr-asg e compst fenv limit)))

Theorem: exec-expr-asg-of-fun-env-fix-fenv

(defthm exec-expr-asg-of-fun-env-fix-fenv
  (equal (exec-expr-asg e compst (fun-env-fix fenv)
                        limit)
         (exec-expr-asg e compst fenv limit)))

Theorem: exec-expr-asg-of-nfix-limit

(defthm exec-expr-asg-of-nfix-limit
  (equal (exec-expr-asg e compst fenv (nfix limit))
         (exec-expr-asg e compst fenv limit)))

Theorem: exec-expr-call-or-asg-of-expr-fix-e

(defthm exec-expr-call-or-asg-of-expr-fix-e
  (equal (exec-expr-call-or-asg (expr-fix e)
                                compst fenv limit)
         (exec-expr-call-or-asg e compst fenv limit)))

Theorem: exec-expr-call-or-asg-of-compustate-fix-compst

(defthm exec-expr-call-or-asg-of-compustate-fix-compst
  (equal (exec-expr-call-or-asg e (compustate-fix compst)
                                fenv limit)
         (exec-expr-call-or-asg e compst fenv limit)))

Theorem: exec-expr-call-or-asg-of-fun-env-fix-fenv

(defthm exec-expr-call-or-asg-of-fun-env-fix-fenv
  (equal (exec-expr-call-or-asg e compst (fun-env-fix fenv)
                                limit)
         (exec-expr-call-or-asg e compst fenv limit)))

Theorem: exec-expr-call-or-asg-of-nfix-limit

(defthm exec-expr-call-or-asg-of-nfix-limit
  (equal (exec-expr-call-or-asg e compst fenv (nfix limit))
         (exec-expr-call-or-asg e compst fenv limit)))

Theorem: exec-fun-of-ident-fix-fun

(defthm exec-fun-of-ident-fix-fun
  (equal (exec-fun (ident-fix fun)
                   args compst fenv limit)
         (exec-fun fun args compst fenv limit)))

Theorem: exec-fun-of-value-list-fix-args

(defthm exec-fun-of-value-list-fix-args
  (equal (exec-fun fun (value-list-fix args)
                   compst fenv limit)
         (exec-fun fun args compst fenv limit)))

Theorem: exec-fun-of-compustate-fix-compst

(defthm exec-fun-of-compustate-fix-compst
  (equal (exec-fun fun args (compustate-fix compst)
                   fenv limit)
         (exec-fun fun args compst fenv limit)))

Theorem: exec-fun-of-fun-env-fix-fenv

(defthm exec-fun-of-fun-env-fix-fenv
  (equal (exec-fun fun args compst (fun-env-fix fenv)
                   limit)
         (exec-fun fun args compst fenv limit)))

Theorem: exec-fun-of-nfix-limit

(defthm exec-fun-of-nfix-limit
  (equal (exec-fun fun args compst fenv (nfix limit))
         (exec-fun fun args compst fenv limit)))

Theorem: exec-stmt-of-stmt-fix-s

(defthm exec-stmt-of-stmt-fix-s
  (equal (exec-stmt (stmt-fix s)
                    compst fenv limit)
         (exec-stmt s compst fenv limit)))

Theorem: exec-stmt-of-compustate-fix-compst

(defthm exec-stmt-of-compustate-fix-compst
  (equal (exec-stmt s (compustate-fix compst)
                    fenv limit)
         (exec-stmt s compst fenv limit)))

Theorem: exec-stmt-of-fun-env-fix-fenv

(defthm exec-stmt-of-fun-env-fix-fenv
  (equal (exec-stmt s compst (fun-env-fix fenv)
                    limit)
         (exec-stmt s compst fenv limit)))

Theorem: exec-stmt-of-nfix-limit

(defthm exec-stmt-of-nfix-limit
  (equal (exec-stmt s compst fenv (nfix limit))
         (exec-stmt s compst fenv limit)))

Theorem: exec-stmt-while-of-expr-fix-test

(defthm exec-stmt-while-of-expr-fix-test
  (equal (exec-stmt-while (expr-fix test)
                          body compst fenv limit)
         (exec-stmt-while test body compst fenv limit)))

Theorem: exec-stmt-while-of-stmt-fix-body

(defthm exec-stmt-while-of-stmt-fix-body
  (equal (exec-stmt-while test (stmt-fix body)
                          compst fenv limit)
         (exec-stmt-while test body compst fenv limit)))

Theorem: exec-stmt-while-of-compustate-fix-compst

(defthm exec-stmt-while-of-compustate-fix-compst
  (equal (exec-stmt-while test body (compustate-fix compst)
                          fenv limit)
         (exec-stmt-while test body compst fenv limit)))

Theorem: exec-stmt-while-of-fun-env-fix-fenv

(defthm exec-stmt-while-of-fun-env-fix-fenv
  (equal (exec-stmt-while test body compst (fun-env-fix fenv)
                          limit)
         (exec-stmt-while test body compst fenv limit)))

Theorem: exec-stmt-while-of-nfix-limit

(defthm exec-stmt-while-of-nfix-limit
  (equal (exec-stmt-while test body compst fenv (nfix limit))
         (exec-stmt-while test body compst fenv limit)))

Theorem: exec-initer-of-initer-fix-initer

(defthm exec-initer-of-initer-fix-initer
  (equal (exec-initer (initer-fix initer)
                      compst fenv limit)
         (exec-initer initer compst fenv limit)))

Theorem: exec-initer-of-compustate-fix-compst

(defthm exec-initer-of-compustate-fix-compst
  (equal (exec-initer initer (compustate-fix compst)
                      fenv limit)
         (exec-initer initer compst fenv limit)))

Theorem: exec-initer-of-fun-env-fix-fenv

(defthm exec-initer-of-fun-env-fix-fenv
  (equal (exec-initer initer compst (fun-env-fix fenv)
                      limit)
         (exec-initer initer compst fenv limit)))

Theorem: exec-initer-of-nfix-limit

(defthm exec-initer-of-nfix-limit
  (equal (exec-initer initer compst fenv (nfix limit))
         (exec-initer initer compst fenv limit)))

Theorem: exec-block-item-of-block-item-fix-item

(defthm exec-block-item-of-block-item-fix-item
  (equal (exec-block-item (block-item-fix item)
                          compst fenv limit)
         (exec-block-item item compst fenv limit)))

Theorem: exec-block-item-of-compustate-fix-compst

(defthm exec-block-item-of-compustate-fix-compst
  (equal (exec-block-item item (compustate-fix compst)
                          fenv limit)
         (exec-block-item item compst fenv limit)))

Theorem: exec-block-item-of-fun-env-fix-fenv

(defthm exec-block-item-of-fun-env-fix-fenv
  (equal (exec-block-item item compst (fun-env-fix fenv)
                          limit)
         (exec-block-item item compst fenv limit)))

Theorem: exec-block-item-of-nfix-limit

(defthm exec-block-item-of-nfix-limit
  (equal (exec-block-item item compst fenv (nfix limit))
         (exec-block-item item compst fenv limit)))

Theorem: exec-block-item-list-of-block-item-list-fix-items

(defthm exec-block-item-list-of-block-item-list-fix-items
  (equal (exec-block-item-list (block-item-list-fix items)
                               compst fenv limit)
         (exec-block-item-list items compst fenv limit)))

Theorem: exec-block-item-list-of-compustate-fix-compst

(defthm exec-block-item-list-of-compustate-fix-compst
  (equal (exec-block-item-list items (compustate-fix compst)
                               fenv limit)
         (exec-block-item-list items compst fenv limit)))

Theorem: exec-block-item-list-of-fun-env-fix-fenv

(defthm exec-block-item-list-of-fun-env-fix-fenv
  (equal (exec-block-item-list items compst (fun-env-fix fenv)
                               limit)
         (exec-block-item-list items compst fenv limit)))

Theorem: exec-block-item-list-of-nfix-limit

(defthm exec-block-item-list-of-nfix-limit
  (equal (exec-block-item-list items compst fenv (nfix limit))
         (exec-block-item-list items compst fenv limit)))

Theorem: exec-expr-call-ident-equiv-congruence-on-fun

(defthm exec-expr-call-ident-equiv-congruence-on-fun
 (implies (ident-equiv fun fun-equiv)
          (equal (exec-expr-call fun args compst fenv limit)
                 (exec-expr-call fun-equiv args compst fenv limit)))
 :rule-classes :congruence)

Theorem: exec-expr-call-expr-list-equiv-congruence-on-args

(defthm exec-expr-call-expr-list-equiv-congruence-on-args
 (implies (expr-list-equiv args args-equiv)
          (equal (exec-expr-call fun args compst fenv limit)
                 (exec-expr-call fun args-equiv compst fenv limit)))
 :rule-classes :congruence)

Theorem: exec-expr-call-compustate-equiv-congruence-on-compst

(defthm exec-expr-call-compustate-equiv-congruence-on-compst
 (implies (compustate-equiv compst compst-equiv)
          (equal (exec-expr-call fun args compst fenv limit)
                 (exec-expr-call fun args compst-equiv fenv limit)))
 :rule-classes :congruence)

Theorem: exec-expr-call-fun-env-equiv-congruence-on-fenv

(defthm exec-expr-call-fun-env-equiv-congruence-on-fenv
 (implies (fun-env-equiv fenv fenv-equiv)
          (equal (exec-expr-call fun args compst fenv limit)
                 (exec-expr-call fun args compst fenv-equiv limit)))
 :rule-classes :congruence)

Theorem: exec-expr-call-nat-equiv-congruence-on-limit

(defthm exec-expr-call-nat-equiv-congruence-on-limit
 (implies (acl2::nat-equiv limit limit-equiv)
          (equal (exec-expr-call fun args compst fenv limit)
                 (exec-expr-call fun args compst fenv limit-equiv)))
 :rule-classes :congruence)

Theorem: exec-expr-call-or-pure-expr-equiv-congruence-on-e

(defthm exec-expr-call-or-pure-expr-equiv-congruence-on-e
  (implies
       (expr-equiv e e-equiv)
       (equal (exec-expr-call-or-pure e compst fenv limit)
              (exec-expr-call-or-pure e-equiv compst fenv limit)))
  :rule-classes :congruence)

Theorem: exec-expr-call-or-pure-compustate-equiv-congruence-on-compst

(defthm exec-expr-call-or-pure-compustate-equiv-congruence-on-compst
  (implies
       (compustate-equiv compst compst-equiv)
       (equal (exec-expr-call-or-pure e compst fenv limit)
              (exec-expr-call-or-pure e compst-equiv fenv limit)))
  :rule-classes :congruence)

Theorem: exec-expr-call-or-pure-fun-env-equiv-congruence-on-fenv

(defthm exec-expr-call-or-pure-fun-env-equiv-congruence-on-fenv
  (implies
       (fun-env-equiv fenv fenv-equiv)
       (equal (exec-expr-call-or-pure e compst fenv limit)
              (exec-expr-call-or-pure e compst fenv-equiv limit)))
  :rule-classes :congruence)

Theorem: exec-expr-call-or-pure-nat-equiv-congruence-on-limit

(defthm exec-expr-call-or-pure-nat-equiv-congruence-on-limit
  (implies
       (acl2::nat-equiv limit limit-equiv)
       (equal (exec-expr-call-or-pure e compst fenv limit)
              (exec-expr-call-or-pure e compst fenv limit-equiv)))
  :rule-classes :congruence)

Theorem: exec-expr-asg-expr-equiv-congruence-on-e

(defthm exec-expr-asg-expr-equiv-congruence-on-e
  (implies (expr-equiv e e-equiv)
           (equal (exec-expr-asg e compst fenv limit)
                  (exec-expr-asg e-equiv compst fenv limit)))
  :rule-classes :congruence)

Theorem: exec-expr-asg-compustate-equiv-congruence-on-compst

(defthm exec-expr-asg-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (exec-expr-asg e compst fenv limit)
                  (exec-expr-asg e compst-equiv fenv limit)))
  :rule-classes :congruence)

Theorem: exec-expr-asg-fun-env-equiv-congruence-on-fenv

(defthm exec-expr-asg-fun-env-equiv-congruence-on-fenv
  (implies (fun-env-equiv fenv fenv-equiv)
           (equal (exec-expr-asg e compst fenv limit)
                  (exec-expr-asg e compst fenv-equiv limit)))
  :rule-classes :congruence)

Theorem: exec-expr-asg-nat-equiv-congruence-on-limit

(defthm exec-expr-asg-nat-equiv-congruence-on-limit
  (implies (acl2::nat-equiv limit limit-equiv)
           (equal (exec-expr-asg e compst fenv limit)
                  (exec-expr-asg e compst fenv limit-equiv)))
  :rule-classes :congruence)

Theorem: exec-expr-call-or-asg-expr-equiv-congruence-on-e

(defthm exec-expr-call-or-asg-expr-equiv-congruence-on-e
 (implies (expr-equiv e e-equiv)
          (equal (exec-expr-call-or-asg e compst fenv limit)
                 (exec-expr-call-or-asg e-equiv compst fenv limit)))
 :rule-classes :congruence)

Theorem: exec-expr-call-or-asg-compustate-equiv-congruence-on-compst

(defthm exec-expr-call-or-asg-compustate-equiv-congruence-on-compst
 (implies (compustate-equiv compst compst-equiv)
          (equal (exec-expr-call-or-asg e compst fenv limit)
                 (exec-expr-call-or-asg e compst-equiv fenv limit)))
 :rule-classes :congruence)

Theorem: exec-expr-call-or-asg-fun-env-equiv-congruence-on-fenv

(defthm exec-expr-call-or-asg-fun-env-equiv-congruence-on-fenv
 (implies (fun-env-equiv fenv fenv-equiv)
          (equal (exec-expr-call-or-asg e compst fenv limit)
                 (exec-expr-call-or-asg e compst fenv-equiv limit)))
 :rule-classes :congruence)

Theorem: exec-expr-call-or-asg-nat-equiv-congruence-on-limit

(defthm exec-expr-call-or-asg-nat-equiv-congruence-on-limit
 (implies (acl2::nat-equiv limit limit-equiv)
          (equal (exec-expr-call-or-asg e compst fenv limit)
                 (exec-expr-call-or-asg e compst fenv limit-equiv)))
 :rule-classes :congruence)

Theorem: exec-fun-ident-equiv-congruence-on-fun

(defthm exec-fun-ident-equiv-congruence-on-fun
  (implies (ident-equiv fun fun-equiv)
           (equal (exec-fun fun args compst fenv limit)
                  (exec-fun fun-equiv args compst fenv limit)))
  :rule-classes :congruence)

Theorem: exec-fun-value-list-equiv-congruence-on-args

(defthm exec-fun-value-list-equiv-congruence-on-args
  (implies (value-list-equiv args args-equiv)
           (equal (exec-fun fun args compst fenv limit)
                  (exec-fun fun args-equiv compst fenv limit)))
  :rule-classes :congruence)

Theorem: exec-fun-compustate-equiv-congruence-on-compst

(defthm exec-fun-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (exec-fun fun args compst fenv limit)
                  (exec-fun fun args compst-equiv fenv limit)))
  :rule-classes :congruence)

Theorem: exec-fun-fun-env-equiv-congruence-on-fenv

(defthm exec-fun-fun-env-equiv-congruence-on-fenv
  (implies (fun-env-equiv fenv fenv-equiv)
           (equal (exec-fun fun args compst fenv limit)
                  (exec-fun fun args compst fenv-equiv limit)))
  :rule-classes :congruence)

Theorem: exec-fun-nat-equiv-congruence-on-limit

(defthm exec-fun-nat-equiv-congruence-on-limit
  (implies (acl2::nat-equiv limit limit-equiv)
           (equal (exec-fun fun args compst fenv limit)
                  (exec-fun fun args compst fenv limit-equiv)))
  :rule-classes :congruence)

Theorem: exec-stmt-stmt-equiv-congruence-on-s

(defthm exec-stmt-stmt-equiv-congruence-on-s
  (implies (stmt-equiv s s-equiv)
           (equal (exec-stmt s compst fenv limit)
                  (exec-stmt s-equiv compst fenv limit)))
  :rule-classes :congruence)

Theorem: exec-stmt-compustate-equiv-congruence-on-compst

(defthm exec-stmt-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (exec-stmt s compst fenv limit)
                  (exec-stmt s compst-equiv fenv limit)))
  :rule-classes :congruence)

Theorem: exec-stmt-fun-env-equiv-congruence-on-fenv

(defthm exec-stmt-fun-env-equiv-congruence-on-fenv
  (implies (fun-env-equiv fenv fenv-equiv)
           (equal (exec-stmt s compst fenv limit)
                  (exec-stmt s compst fenv-equiv limit)))
  :rule-classes :congruence)

Theorem: exec-stmt-nat-equiv-congruence-on-limit

(defthm exec-stmt-nat-equiv-congruence-on-limit
  (implies (acl2::nat-equiv limit limit-equiv)
           (equal (exec-stmt s compst fenv limit)
                  (exec-stmt s compst fenv limit-equiv)))
  :rule-classes :congruence)

Theorem: exec-stmt-while-expr-equiv-congruence-on-test

(defthm exec-stmt-while-expr-equiv-congruence-on-test
  (implies
       (expr-equiv test test-equiv)
       (equal (exec-stmt-while test body compst fenv limit)
              (exec-stmt-while test-equiv body compst fenv limit)))
  :rule-classes :congruence)

Theorem: exec-stmt-while-stmt-equiv-congruence-on-body

(defthm exec-stmt-while-stmt-equiv-congruence-on-body
  (implies
       (stmt-equiv body body-equiv)
       (equal (exec-stmt-while test body compst fenv limit)
              (exec-stmt-while test body-equiv compst fenv limit)))
  :rule-classes :congruence)

Theorem: exec-stmt-while-compustate-equiv-congruence-on-compst

(defthm exec-stmt-while-compustate-equiv-congruence-on-compst
  (implies
       (compustate-equiv compst compst-equiv)
       (equal (exec-stmt-while test body compst fenv limit)
              (exec-stmt-while test body compst-equiv fenv limit)))
  :rule-classes :congruence)

Theorem: exec-stmt-while-fun-env-equiv-congruence-on-fenv

(defthm exec-stmt-while-fun-env-equiv-congruence-on-fenv
  (implies
       (fun-env-equiv fenv fenv-equiv)
       (equal (exec-stmt-while test body compst fenv limit)
              (exec-stmt-while test body compst fenv-equiv limit)))
  :rule-classes :congruence)

Theorem: exec-stmt-while-nat-equiv-congruence-on-limit

(defthm exec-stmt-while-nat-equiv-congruence-on-limit
  (implies
       (acl2::nat-equiv limit limit-equiv)
       (equal (exec-stmt-while test body compst fenv limit)
              (exec-stmt-while test body compst fenv limit-equiv)))
  :rule-classes :congruence)

Theorem: exec-initer-initer-equiv-congruence-on-initer

(defthm exec-initer-initer-equiv-congruence-on-initer
  (implies (initer-equiv initer initer-equiv)
           (equal (exec-initer initer compst fenv limit)
                  (exec-initer initer-equiv compst fenv limit)))
  :rule-classes :congruence)

Theorem: exec-initer-compustate-equiv-congruence-on-compst

(defthm exec-initer-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (exec-initer initer compst fenv limit)
                  (exec-initer initer compst-equiv fenv limit)))
  :rule-classes :congruence)

Theorem: exec-initer-fun-env-equiv-congruence-on-fenv

(defthm exec-initer-fun-env-equiv-congruence-on-fenv
  (implies (fun-env-equiv fenv fenv-equiv)
           (equal (exec-initer initer compst fenv limit)
                  (exec-initer initer compst fenv-equiv limit)))
  :rule-classes :congruence)

Theorem: exec-initer-nat-equiv-congruence-on-limit

(defthm exec-initer-nat-equiv-congruence-on-limit
  (implies (acl2::nat-equiv limit limit-equiv)
           (equal (exec-initer initer compst fenv limit)
                  (exec-initer initer compst fenv limit-equiv)))
  :rule-classes :congruence)

Theorem: exec-block-item-block-item-equiv-congruence-on-item

(defthm exec-block-item-block-item-equiv-congruence-on-item
  (implies (block-item-equiv item item-equiv)
           (equal (exec-block-item item compst fenv limit)
                  (exec-block-item item-equiv compst fenv limit)))
  :rule-classes :congruence)

Theorem: exec-block-item-compustate-equiv-congruence-on-compst

(defthm exec-block-item-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (exec-block-item item compst fenv limit)
                  (exec-block-item item compst-equiv fenv limit)))
  :rule-classes :congruence)

Theorem: exec-block-item-fun-env-equiv-congruence-on-fenv

(defthm exec-block-item-fun-env-equiv-congruence-on-fenv
  (implies (fun-env-equiv fenv fenv-equiv)
           (equal (exec-block-item item compst fenv limit)
                  (exec-block-item item compst fenv-equiv limit)))
  :rule-classes :congruence)

Theorem: exec-block-item-nat-equiv-congruence-on-limit

(defthm exec-block-item-nat-equiv-congruence-on-limit
  (implies (acl2::nat-equiv limit limit-equiv)
           (equal (exec-block-item item compst fenv limit)
                  (exec-block-item item compst fenv limit-equiv)))
  :rule-classes :congruence)

Theorem: exec-block-item-list-block-item-list-equiv-congruence-on-items

(defthm
     exec-block-item-list-block-item-list-equiv-congruence-on-items
  (implies
       (block-item-list-equiv items items-equiv)
       (equal (exec-block-item-list items compst fenv limit)
              (exec-block-item-list items-equiv compst fenv limit)))
  :rule-classes :congruence)

Theorem: exec-block-item-list-compustate-equiv-congruence-on-compst

(defthm exec-block-item-list-compustate-equiv-congruence-on-compst
  (implies
       (compustate-equiv compst compst-equiv)
       (equal (exec-block-item-list items compst fenv limit)
              (exec-block-item-list items compst-equiv fenv limit)))
  :rule-classes :congruence)

Theorem: exec-block-item-list-fun-env-equiv-congruence-on-fenv

(defthm exec-block-item-list-fun-env-equiv-congruence-on-fenv
  (implies
       (fun-env-equiv fenv fenv-equiv)
       (equal (exec-block-item-list items compst fenv limit)
              (exec-block-item-list items compst fenv-equiv limit)))
  :rule-classes :congruence)

Theorem: exec-block-item-list-nat-equiv-congruence-on-limit

(defthm exec-block-item-list-nat-equiv-congruence-on-limit
  (implies
       (acl2::nat-equiv limit limit-equiv)
       (equal (exec-block-item-list items compst fenv limit)
              (exec-block-item-list items compst fenv limit-equiv)))
  :rule-classes :congruence)

Subtopics

Exec-expr-asg

Execute an assignment expression.

Exec-fun

Execute a function on argument values.

Exec-block-item

Execute a block item.

Exec-expr-call-or-pure

Execute a function call or a pure expression.

Exec-block-item-list

Execute a list of block items.

Exec-stmt-while

Execute a while statement.

Exec-stmt

Execute a statement.

Exec-initer

Execute an initializer.

Exec-expr-call-or-asg

Execute a function call or assignment expression.

Exec-expr-call

Execution a function call.