• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • C
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
        • Transformations
          • Renaming-variables
            • Statements/blocks/cases/fundefs-renamevar
              • Statement-renamevar
              • Statement-list-renamevar
              • Swcase-renamevar
              • Swcase-list-renamevar
              • Fundef-renamevar
              • Block-renamevar
              • Block-option-renamevar
            • Renaming-variables-execution
            • Expressions-renamevar
            • Add-var-to-var-renaming
            • Add-vars-to-var-renaming
            • Renaming-variables-safety
            • Fundef-list-renamevar
            • Expression-option-renamevar
            • Funcall-option-renamevar
            • Path-list-renamevar
            • Var-list-renamevar
            • Var-renamevar
            • Path-renamevar
          • Dead-code-eliminator
          • Renamings
          • Disambiguator
          • Unique-variables
          • Dead-code-eliminator-static-safety
          • No-function-definitions
          • Unique-functions
          • Renaming-functions
          • Dead-code-eliminator-no-loop-initializers
          • Dead-code-eliminator-no-function-definitions
          • No-loop-initializers
          • For-loop-init-rewriter
        • Language
        • Yul-json
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Renaming-variables

Statements/blocks/cases/fundefs-renamevar

Mutually recursive ACL2 functions to check if statements, blocks, cases, and function definitions are related by variable renaming.

Definitions and Theorems

Function: statement-renamevar

(defun statement-renamevar (old new ren)
 (declare (xargs :guard (and (statementp old)
                             (statementp new)
                             (renamingp ren))))
 (let ((__function__ 'statement-renamevar))
   (declare (ignorable __function__))
   (statement-case
        old :block
        (b* (((unless (statement-case new :block))
              (reserrf (list :mismatch (statement-fix old)
                             (statement-fix new))))
             ((statement-block new) new)
             ((okf &)
              (block-renamevar old.get new.get ren)))
          (renaming-fix ren))
        :variable-single
        (b* (((unless (statement-case new :variable-single))
              (reserrf (list :mismatch (statement-fix old)
                             (statement-fix new))))
             ((statement-variable-single new) new)
             ((okf &)
              (expression-option-renamevar old.init new.init ren)))
          (add-var-to-var-renaming old.name new.name ren))
        :variable-multi
        (b* (((unless (statement-case new :variable-multi))
              (reserrf (list :mismatch (statement-fix old)
                             (statement-fix new))))
             ((statement-variable-multi new) new)
             ((okf &)
              (funcall-option-renamevar old.init new.init ren)))
          (add-vars-to-var-renaming old.names new.names ren))
        :assign-single
        (b* (((unless (statement-case new :assign-single))
              (reserrf (list :mismatch (statement-fix old)
                             (statement-fix new))))
             ((statement-assign-single new) new)
             ((okf &)
              (path-renamevar old.target new.target ren))
             ((okf &)
              (expression-renamevar old.value new.value ren)))
          (renaming-fix ren))
        :assign-multi
        (b* (((unless (statement-case new :assign-multi))
              (reserrf (list :mismatch (statement-fix old)
                             (statement-fix new))))
             ((statement-assign-multi new) new)
             ((okf &)
              (path-list-renamevar old.targets new.targets ren))
             ((okf &)
              (funcall-renamevar old.value new.value ren)))
          (renaming-fix ren))
        :funcall
        (b* (((unless (statement-case new :funcall))
              (reserrf (list :mismatch (statement-fix old)
                             (statement-fix new))))
             ((statement-funcall new) new)
             ((okf &)
              (funcall-renamevar old.get new.get ren)))
          (renaming-fix ren))
        :if
        (b* (((unless (statement-case new :if))
              (reserrf (list :mismatch (statement-fix old)
                             (statement-fix new))))
             ((statement-if new) new)
             ((okf &)
              (expression-renamevar old.test new.test ren))
             ((okf &)
              (block-renamevar old.body new.body ren)))
          (renaming-fix ren))
        :for
        (b* (((unless (statement-case new :for))
              (reserrf (list :mismatch (statement-fix old)
                             (statement-fix new))))
             ((statement-for new) new)
             (old-stmts (block->statements old.init))
             (new-stmts (block->statements new.init))
             ((okf ren1)
              (statement-list-renamevar old-stmts new-stmts ren))
             ((okf &)
              (expression-renamevar old.test new.test ren1))
             ((okf &)
              (block-renamevar old.update new.update ren1))
             ((okf &)
              (block-renamevar old.body new.body ren1)))
          (renaming-fix ren))
        :switch
        (b* (((unless (statement-case new :switch))
              (reserrf (list :mismatch (statement-fix old)
                             (statement-fix new))))
             ((statement-switch new) new)
             ((okf &)
              (expression-renamevar old.target new.target ren))
             ((okf &)
              (swcase-list-renamevar old.cases new.cases ren))
             ((okf &)
              (block-option-renamevar old.default new.default ren)))
          (renaming-fix ren))
        :leave
        (b* (((unless (statement-case new :leave))
              (reserrf (list :mismatch (statement-fix old)
                             (statement-fix new)))))
          (renaming-fix ren))
        :break
        (b* (((unless (statement-case new :break))
              (reserrf (list :mismatch (statement-fix old)
                             (statement-fix new)))))
          (renaming-fix ren))
        :continue
        (b* (((unless (statement-case new :continue))
              (reserrf (list :mismatch (statement-fix old)
                             (statement-fix new)))))
          (renaming-fix ren))
        :fundef
        (b* (((unless (statement-case new :fundef))
              (reserrf (list :mismatch (statement-fix old)
                             (statement-fix new))))
             ((statement-fundef new) new)
             ((okf &)
              (fundef-renamevar old.get new.get)))
          (renaming-fix ren)))))

Function: statement-list-renamevar

(defun statement-list-renamevar (old new ren)
 (declare (xargs :guard (and (statement-listp old)
                             (statement-listp new)
                             (renamingp ren))))
 (let ((__function__ 'statement-list-renamevar))
   (declare (ignorable __function__))
   (b*
    (((when (endp old))
      (if (endp new)
          (renaming-fix ren)
        (reserrf
             (list :mismatch-extra-new (statement-list-fix new)))))
     ((when (endp new))
      (reserrf (list :mismatch-extra-old (statement-list-fix old))))
     ((okf ren)
      (statement-renamevar (car old)
                           (car new)
                           ren)))
    (statement-list-renamevar (cdr old)
                              (cdr new)
                              ren))))

Function: block-renamevar

(defun block-renamevar (old new ren)
  (declare (xargs :guard (and (blockp old)
                              (blockp new)
                              (renamingp ren))))
  (let ((__function__ 'block-renamevar))
    (declare (ignorable __function__))
    (b* ((old-stmts (block->statements old))
         (new-stmts (block->statements new))
         ((okf &)
          (statement-list-renamevar old-stmts new-stmts ren)))
      nil)))

Function: block-option-renamevar

(defun block-option-renamevar (old new ren)
 (declare (xargs :guard (and (block-optionp old)
                             (block-optionp new)
                             (renamingp ren))))
 (let ((__function__ 'block-option-renamevar))
  (declare (ignorable __function__))
  (block-option-case
    old :none
    (if (block-option-case new :none)
        nil
      (reserrf (list :mismatch (block-option-fix old)
                     (block-option-fix new))))
    :some (block-option-case
               new
               :none (reserrf (list :mismatch (block-option-fix old)
                                    (block-option-fix new)))
               :some (block-renamevar (block-option-some->val old)
                                      (block-option-some->val new)
                                      ren)))))

Function: swcase-renamevar

(defun swcase-renamevar (old new ren)
  (declare (xargs :guard (and (swcasep old)
                              (swcasep new)
                              (renamingp ren))))
  (let ((__function__ 'swcase-renamevar))
    (declare (ignorable __function__))
    (b* (((unless (equal (swcase->value old)
                         (swcase->value new)))
          (reserrf (list :mismatch-case-value (swcase->value old)
                         (swcase->value new)))))
      (block-renamevar (swcase->body old)
                       (swcase->body new)
                       ren))))

Function: swcase-list-renamevar

(defun swcase-list-renamevar (old new ren)
 (declare (xargs :guard (and (swcase-listp old)
                             (swcase-listp new)
                             (renamingp ren))))
 (let ((__function__ 'swcase-list-renamevar))
   (declare (ignorable __function__))
   (b*
    (((when (endp old))
      (if (endp new)
          nil
        (reserrf (list :mismatch-extra-new (swcase-list-fix new)))))
     ((when (endp new))
      (reserrf (list :mismatch-extra-old (swcase-list-fix old))))
     ((okf &)
      (swcase-renamevar (car old)
                        (car new)
                        ren)))
    (swcase-list-renamevar (cdr old)
                           (cdr new)
                           ren))))

Function: fundef-renamevar

(defun fundef-renamevar (old new)
  (declare (xargs :guard (and (fundefp old) (fundefp new))))
  (let ((__function__ 'fundef-renamevar))
    (declare (ignorable __function__))
    (b* (((unless (equal (fundef->name old)
                         (fundef->name new)))
          (reserrf (list :mismatch-function-name
                         (fundef->name old)
                         (fundef->name new))))
         ((okf ren)
          (add-vars-to-var-renaming (fundef->inputs old)
                                    (fundef->inputs new)
                                    (renaming nil)))
         ((okf ren)
          (add-vars-to-var-renaming (fundef->outputs old)
                                    (fundef->outputs new)
                                    ren)))
      (block-renamevar (fundef->body old)
                       (fundef->body new)
                       ren))))

Theorem: return-type-of-statement-renamevar.new-ren

(defthm return-type-of-statement-renamevar.new-ren
  (b* ((?new-ren (statement-renamevar old new ren)))
    (renaming-resultp new-ren))
  :rule-classes :rewrite)

Theorem: return-type-of-statement-list-renamevar.new-ren

(defthm return-type-of-statement-list-renamevar.new-ren
  (b* ((?new-ren (statement-list-renamevar old new ren)))
    (renaming-resultp new-ren))
  :rule-classes :rewrite)

Theorem: return-type-of-block-renamevar._

(defthm return-type-of-block-renamevar._
  (b* ((?_ (block-renamevar old new ren)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: return-type-of-block-option-renamevar._

(defthm return-type-of-block-option-renamevar._
  (b* ((?_ (block-option-renamevar old new ren)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: return-type-of-swcase-renamevar._

(defthm return-type-of-swcase-renamevar._
  (b* ((?_ (swcase-renamevar old new ren)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: return-type-of-swcase-list-renamevar._

(defthm return-type-of-swcase-list-renamevar._
  (b* ((?_ (swcase-list-renamevar old new ren)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: return-type-of-fundef-renamevar._

(defthm return-type-of-fundef-renamevar._
  (b* ((?_ (fundef-renamevar old new)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: statement-renamevar-of-statement-fix-old

(defthm statement-renamevar-of-statement-fix-old
  (equal (statement-renamevar (statement-fix old)
                              new ren)
         (statement-renamevar old new ren)))

Theorem: statement-renamevar-of-statement-fix-new

(defthm statement-renamevar-of-statement-fix-new
  (equal (statement-renamevar old (statement-fix new)
                              ren)
         (statement-renamevar old new ren)))

Theorem: statement-renamevar-of-renaming-fix-ren

(defthm statement-renamevar-of-renaming-fix-ren
  (equal (statement-renamevar old new (renaming-fix ren))
         (statement-renamevar old new ren)))

Theorem: statement-list-renamevar-of-statement-list-fix-old

(defthm statement-list-renamevar-of-statement-list-fix-old
  (equal (statement-list-renamevar (statement-list-fix old)
                                   new ren)
         (statement-list-renamevar old new ren)))

Theorem: statement-list-renamevar-of-statement-list-fix-new

(defthm statement-list-renamevar-of-statement-list-fix-new
  (equal (statement-list-renamevar old (statement-list-fix new)
                                   ren)
         (statement-list-renamevar old new ren)))

Theorem: statement-list-renamevar-of-renaming-fix-ren

(defthm statement-list-renamevar-of-renaming-fix-ren
  (equal (statement-list-renamevar old new (renaming-fix ren))
         (statement-list-renamevar old new ren)))

Theorem: block-renamevar-of-block-fix-old

(defthm block-renamevar-of-block-fix-old
  (equal (block-renamevar (block-fix old)
                          new ren)
         (block-renamevar old new ren)))

Theorem: block-renamevar-of-block-fix-new

(defthm block-renamevar-of-block-fix-new
  (equal (block-renamevar old (block-fix new)
                          ren)
         (block-renamevar old new ren)))

Theorem: block-renamevar-of-renaming-fix-ren

(defthm block-renamevar-of-renaming-fix-ren
  (equal (block-renamevar old new (renaming-fix ren))
         (block-renamevar old new ren)))

Theorem: block-option-renamevar-of-block-option-fix-old

(defthm block-option-renamevar-of-block-option-fix-old
  (equal (block-option-renamevar (block-option-fix old)
                                 new ren)
         (block-option-renamevar old new ren)))

Theorem: block-option-renamevar-of-block-option-fix-new

(defthm block-option-renamevar-of-block-option-fix-new
  (equal (block-option-renamevar old (block-option-fix new)
                                 ren)
         (block-option-renamevar old new ren)))

Theorem: block-option-renamevar-of-renaming-fix-ren

(defthm block-option-renamevar-of-renaming-fix-ren
  (equal (block-option-renamevar old new (renaming-fix ren))
         (block-option-renamevar old new ren)))

Theorem: swcase-renamevar-of-swcase-fix-old

(defthm swcase-renamevar-of-swcase-fix-old
  (equal (swcase-renamevar (swcase-fix old)
                           new ren)
         (swcase-renamevar old new ren)))

Theorem: swcase-renamevar-of-swcase-fix-new

(defthm swcase-renamevar-of-swcase-fix-new
  (equal (swcase-renamevar old (swcase-fix new)
                           ren)
         (swcase-renamevar old new ren)))

Theorem: swcase-renamevar-of-renaming-fix-ren

(defthm swcase-renamevar-of-renaming-fix-ren
  (equal (swcase-renamevar old new (renaming-fix ren))
         (swcase-renamevar old new ren)))

Theorem: swcase-list-renamevar-of-swcase-list-fix-old

(defthm swcase-list-renamevar-of-swcase-list-fix-old
  (equal (swcase-list-renamevar (swcase-list-fix old)
                                new ren)
         (swcase-list-renamevar old new ren)))

Theorem: swcase-list-renamevar-of-swcase-list-fix-new

(defthm swcase-list-renamevar-of-swcase-list-fix-new
  (equal (swcase-list-renamevar old (swcase-list-fix new)
                                ren)
         (swcase-list-renamevar old new ren)))

Theorem: swcase-list-renamevar-of-renaming-fix-ren

(defthm swcase-list-renamevar-of-renaming-fix-ren
  (equal (swcase-list-renamevar old new (renaming-fix ren))
         (swcase-list-renamevar old new ren)))

Theorem: fundef-renamevar-of-fundef-fix-old

(defthm fundef-renamevar-of-fundef-fix-old
  (equal (fundef-renamevar (fundef-fix old) new)
         (fundef-renamevar old new)))

Theorem: fundef-renamevar-of-fundef-fix-new

(defthm fundef-renamevar-of-fundef-fix-new
  (equal (fundef-renamevar old (fundef-fix new))
         (fundef-renamevar old new)))

Theorem: statement-renamevar-statement-equiv-congruence-on-old

(defthm statement-renamevar-statement-equiv-congruence-on-old
  (implies (statement-equiv old old-equiv)
           (equal (statement-renamevar old new ren)
                  (statement-renamevar old-equiv new ren)))
  :rule-classes :congruence)

Theorem: statement-renamevar-statement-equiv-congruence-on-new

(defthm statement-renamevar-statement-equiv-congruence-on-new
  (implies (statement-equiv new new-equiv)
           (equal (statement-renamevar old new ren)
                  (statement-renamevar old new-equiv ren)))
  :rule-classes :congruence)

Theorem: statement-renamevar-renaming-equiv-congruence-on-ren

(defthm statement-renamevar-renaming-equiv-congruence-on-ren
  (implies (renaming-equiv ren ren-equiv)
           (equal (statement-renamevar old new ren)
                  (statement-renamevar old new ren-equiv)))
  :rule-classes :congruence)

Theorem: statement-list-renamevar-statement-list-equiv-congruence-on-old

(defthm
    statement-list-renamevar-statement-list-equiv-congruence-on-old
  (implies (statement-list-equiv old old-equiv)
           (equal (statement-list-renamevar old new ren)
                  (statement-list-renamevar old-equiv new ren)))
  :rule-classes :congruence)

Theorem: statement-list-renamevar-statement-list-equiv-congruence-on-new

(defthm
    statement-list-renamevar-statement-list-equiv-congruence-on-new
  (implies (statement-list-equiv new new-equiv)
           (equal (statement-list-renamevar old new ren)
                  (statement-list-renamevar old new-equiv ren)))
  :rule-classes :congruence)

Theorem: statement-list-renamevar-renaming-equiv-congruence-on-ren

(defthm statement-list-renamevar-renaming-equiv-congruence-on-ren
  (implies (renaming-equiv ren ren-equiv)
           (equal (statement-list-renamevar old new ren)
                  (statement-list-renamevar old new ren-equiv)))
  :rule-classes :congruence)

Theorem: block-renamevar-block-equiv-congruence-on-old

(defthm block-renamevar-block-equiv-congruence-on-old
  (implies (block-equiv old old-equiv)
           (equal (block-renamevar old new ren)
                  (block-renamevar old-equiv new ren)))
  :rule-classes :congruence)

Theorem: block-renamevar-block-equiv-congruence-on-new

(defthm block-renamevar-block-equiv-congruence-on-new
  (implies (block-equiv new new-equiv)
           (equal (block-renamevar old new ren)
                  (block-renamevar old new-equiv ren)))
  :rule-classes :congruence)

Theorem: block-renamevar-renaming-equiv-congruence-on-ren

(defthm block-renamevar-renaming-equiv-congruence-on-ren
  (implies (renaming-equiv ren ren-equiv)
           (equal (block-renamevar old new ren)
                  (block-renamevar old new ren-equiv)))
  :rule-classes :congruence)

Theorem: block-option-renamevar-block-option-equiv-congruence-on-old

(defthm block-option-renamevar-block-option-equiv-congruence-on-old
  (implies (block-option-equiv old old-equiv)
           (equal (block-option-renamevar old new ren)
                  (block-option-renamevar old-equiv new ren)))
  :rule-classes :congruence)

Theorem: block-option-renamevar-block-option-equiv-congruence-on-new

(defthm block-option-renamevar-block-option-equiv-congruence-on-new
  (implies (block-option-equiv new new-equiv)
           (equal (block-option-renamevar old new ren)
                  (block-option-renamevar old new-equiv ren)))
  :rule-classes :congruence)

Theorem: block-option-renamevar-renaming-equiv-congruence-on-ren

(defthm block-option-renamevar-renaming-equiv-congruence-on-ren
  (implies (renaming-equiv ren ren-equiv)
           (equal (block-option-renamevar old new ren)
                  (block-option-renamevar old new ren-equiv)))
  :rule-classes :congruence)

Theorem: swcase-renamevar-swcase-equiv-congruence-on-old

(defthm swcase-renamevar-swcase-equiv-congruence-on-old
  (implies (swcase-equiv old old-equiv)
           (equal (swcase-renamevar old new ren)
                  (swcase-renamevar old-equiv new ren)))
  :rule-classes :congruence)

Theorem: swcase-renamevar-swcase-equiv-congruence-on-new

(defthm swcase-renamevar-swcase-equiv-congruence-on-new
  (implies (swcase-equiv new new-equiv)
           (equal (swcase-renamevar old new ren)
                  (swcase-renamevar old new-equiv ren)))
  :rule-classes :congruence)

Theorem: swcase-renamevar-renaming-equiv-congruence-on-ren

(defthm swcase-renamevar-renaming-equiv-congruence-on-ren
  (implies (renaming-equiv ren ren-equiv)
           (equal (swcase-renamevar old new ren)
                  (swcase-renamevar old new ren-equiv)))
  :rule-classes :congruence)

Theorem: swcase-list-renamevar-swcase-list-equiv-congruence-on-old

(defthm swcase-list-renamevar-swcase-list-equiv-congruence-on-old
  (implies (swcase-list-equiv old old-equiv)
           (equal (swcase-list-renamevar old new ren)
                  (swcase-list-renamevar old-equiv new ren)))
  :rule-classes :congruence)

Theorem: swcase-list-renamevar-swcase-list-equiv-congruence-on-new

(defthm swcase-list-renamevar-swcase-list-equiv-congruence-on-new
  (implies (swcase-list-equiv new new-equiv)
           (equal (swcase-list-renamevar old new ren)
                  (swcase-list-renamevar old new-equiv ren)))
  :rule-classes :congruence)

Theorem: swcase-list-renamevar-renaming-equiv-congruence-on-ren

(defthm swcase-list-renamevar-renaming-equiv-congruence-on-ren
  (implies (renaming-equiv ren ren-equiv)
           (equal (swcase-list-renamevar old new ren)
                  (swcase-list-renamevar old new ren-equiv)))
  :rule-classes :congruence)

Theorem: fundef-renamevar-fundef-equiv-congruence-on-old

(defthm fundef-renamevar-fundef-equiv-congruence-on-old
  (implies (fundef-equiv old old-equiv)
           (equal (fundef-renamevar old new)
                  (fundef-renamevar old-equiv new)))
  :rule-classes :congruence)

Theorem: fundef-renamevar-fundef-equiv-congruence-on-new

(defthm fundef-renamevar-fundef-equiv-congruence-on-new
  (implies (fundef-equiv new new-equiv)
           (equal (fundef-renamevar old new)
                  (fundef-renamevar old new-equiv)))
  :rule-classes :congruence)

Theorem: same-len-when-expression-list-renamevar

(defthm same-len-when-expression-list-renamevar
  (implies (not (reserrp (expression-list-renamevar old new ren)))
           (equal (len old) (len new))))

Theorem: expression-list-renamevar-of-append-error

(defthm expression-list-renamevar-of-append-error
 (implies
  (equal (len old) (len new))
  (equal (reserrp (expression-list-renamevar (append old old1)
                                             (append new new1)
                                             ren))
         (or (reserrp (expression-list-renamevar old new ren))
             (reserrp (expression-list-renamevar old1 new1 ren))))))

Theorem: expression-list-renamevar-of-rev-error

(defthm expression-list-renamevar-of-rev-error
  (implies
       (equal (len old) (len new))
       (equal (reserrp (expression-list-renamevar (rev old)
                                                  (rev new)
                                                  ren))
              (reserrp (expression-list-renamevar old new ren)))))

Theorem: expression-list-renamevar-of-rev-not-error

(defthm expression-list-renamevar-of-rev-not-error
  (implies (not (reserrp (expression-list-renamevar old new ren)))
           (not (reserrp (expression-list-renamevar (rev old)
                                                    (rev new)
                                                    ren)))))

Theorem: same-statement-kind-when-statement-renamevar

(defthm same-statement-kind-when-statement-renamevar
  (implies (not (reserrp (statement-renamevar old new ren)))
           (equal (statement-kind new)
                  (statement-kind old))))

Theorem: block-option-renamevar-of-nil-1-forward

(defthm block-option-renamevar-of-nil-1-forward
  (implies (not (reserrp (block-option-renamevar nil block ren)))
           (equal block nil))
  :rule-classes
  ((:forward-chaining
        :trigger-terms
        ((reserrp (block-option-renamevar nil block ren))))))

Theorem: block-option-renamevar-of-nil-2-forward

(defthm block-option-renamevar-of-nil-2-forward
  (implies (not (reserrp (block-option-renamevar block nil ren)))
           (equal block nil))
  :rule-classes
  ((:forward-chaining
        :trigger-terms
        ((reserrp (block-option-renamevar block nil ren))))))

Theorem: block-option-renamevar-when-nonnil

(defthm block-option-renamevar-when-nonnil
  (implies (and x y)
           (equal (block-option-renamevar x y ren)
                  (block-renamevar x y ren))))

Theorem: same-swcase->value-when-swcase-renamevar

(defthm same-swcase->value-when-swcase-renamevar
  (implies (not (reserrp (swcase-renamevar old new ren)))
           (equal (swcase->value new)
                  (swcase->value old))))

Theorem: reserrp-of-swcase-renamevar

(defthm reserrp-of-swcase-renamevar
  (equal (reserrp (swcase-renamevar x y ren))
         (or (not (equal (swcase->value x)
                         (swcase->value y)))
             (reserrp (block-renamevar (swcase->body x)
                                       (swcase->body y)
                                       ren)))))

Theorem: same-swcase-list->value-list-when-swcase-list-renamevar

(defthm same-swcase-list->value-list-when-swcase-list-renamevar
  (implies (not (reserrp (swcase-list-renamevar old new ren)))
           (equal (swcase-list->value-list new)
                  (swcase-list->value-list old))))

Theorem: same-fundef->name-when-fundef-renamevar

(defthm same-fundef->name-when-fundef-renamevar
  (implies (not (reserrp (fundef-renamevar old new)))
           (equal (fundef->name new)
                  (fundef->name old))))

Theorem: subsetp-equal-of-statement-renamevar

(defthm subsetp-equal-of-statement-renamevar
  (b* ((ren1 (statement-renamevar old new ren)))
    (implies (not (reserrp ren1))
             (subsetp-equal (renaming->list ren)
                            (renaming->list ren1)))))

Theorem: subsetp-equal-of-statement-list-renamevar

(defthm subsetp-equal-of-statement-list-renamevar
  (b* ((ren1 (statement-list-renamevar old new ren)))
    (implies (not (reserrp ren1))
             (subsetp-equal (renaming->list ren)
                            (renaming->list ren1)))))

Theorem: subsetp-equal-of-block-renamevar

(defthm subsetp-equal-of-block-renamevar
  t
  :rule-classes nil)

Theorem: subsetp-equal-of-block-option-renamevar

(defthm subsetp-equal-of-block-option-renamevar
  t
  :rule-classes nil)

Theorem: subsetp-equal-of-swcase-renamevar

(defthm subsetp-equal-of-swcase-renamevar
  t
  :rule-classes nil)

Theorem: subsetp-equal-of-swcase-list-renamevar

(defthm subsetp-equal-of-swcase-list-renamevar
  t
  :rule-classes nil)

Theorem: subsetp-equal-of-fundef-renamevar

(defthm subsetp-equal-of-fundef-renamevar
  t
  :rule-classes nil)

Subtopics

Statement-renamevar

Check if two statements are related by variable renaming.

Statement-list-renamevar

Check if two lists of statements are related by variable renaming.

Swcase-renamevar

Check if two switch cases are related by variable renaming.

Swcase-list-renamevar

Check if two lists of switch cases are related by variable renaming.

Fundef-renamevar

Check if two function definitions are related by variable renaming.

Block-renamevar

Check if two blocks are related by variable renaming.

Block-option-renamevar

Check if two optional blocks are related by variable renaming.