• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Riscv
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
      • Transformations
        • Renaming-variables
          • Statements/blocks/cases/fundefs-renamevar
          • Renaming-variables-execution
            • Restrict-vars-when-renamevar
            • Function-environments-when-renaming-variables
            • Exec-when-renamevar
            • Exec-when-renamevar-restrict-vars-lemmas
            • Lstate-match-renamevarp
            • Soutcome-result-renamevarp
            • Lstate-renamevarp
            • Reserr-limitp-theorems
            • Eoutcome-result-renamevarp
            • Eoutcome-renamevarp
            • Soutcome-renamevarp
            • Cstate-renamevarp-with-larger-renaming
            • Cstate-renamevarp
            • Funinfo-renamevarp
            • Funscope-renamevarp
            • Funenv-renamevarp
            • Path/paths-renamevar-theorems
            • Init-local-when-renamevar
            • Write-var/vars-value/values-when-renamevar
            • Add-var/vars-value/values-when-renamevar
            • Read-var/vars-value/values-when-renamevar
            • Vars-of-cstate-after-exec
          • 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
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Axe
    • Bigmems
    • Builtins
    • Execloader
    • Aleo
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Proof-automation
  • Community
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Renaming-variables-execution

Eoutcome-result-renamevarp

Variable renaming relation over expression outcome results.

Signature

(eoutcome-result-renamevarp old new ren) → yes/no

Arguments

old — Guard (eoutcome-resultp old).

new — Guard (eoutcome-resultp new).

ren — Guard (renamingp ren).

Returns

yes/no — Type (booleanp yes/no).

Either they are both (possibly different) errors, or they are related expression outcomes.

Definitions and Theorems

Function: eoutcome-result-renamevarp

(defun eoutcome-result-renamevarp (old new ren)
  (declare (xargs :guard (and (eoutcome-resultp old)
                              (eoutcome-resultp new)
                              (renamingp ren))))
  (let ((__function__ 'eoutcome-result-renamevarp))
    (declare (ignorable __function__))
    (b* ((old (eoutcome-result-fix old))
         (new (eoutcome-result-fix new)))
      (or (and (reserrp old) (reserrp new))
          (and (not (reserrp old))
               (not (reserrp new))
               (eoutcome-renamevarp old new ren))))))

Theorem: booleanp-of-eoutcome-result-renamevarp

(defthm booleanp-of-eoutcome-result-renamevarp
  (b* ((yes/no (eoutcome-result-renamevarp old new ren)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: eoutcome-result-renamevarp-of-eoutcome-result-fix-old

(defthm eoutcome-result-renamevarp-of-eoutcome-result-fix-old
  (equal (eoutcome-result-renamevarp (eoutcome-result-fix old)
                                     new ren)
         (eoutcome-result-renamevarp old new ren)))

Theorem: eoutcome-result-renamevarp-eoutcome-result-equiv-congruence-on-old

(defthm
 eoutcome-result-renamevarp-eoutcome-result-equiv-congruence-on-old
 (implies (eoutcome-result-equiv old old-equiv)
          (equal (eoutcome-result-renamevarp old new ren)
                 (eoutcome-result-renamevarp old-equiv new ren)))
 :rule-classes :congruence)

Theorem: eoutcome-result-renamevarp-of-eoutcome-result-fix-new

(defthm eoutcome-result-renamevarp-of-eoutcome-result-fix-new
  (equal (eoutcome-result-renamevarp old (eoutcome-result-fix new)
                                     ren)
         (eoutcome-result-renamevarp old new ren)))

Theorem: eoutcome-result-renamevarp-eoutcome-result-equiv-congruence-on-new

(defthm
 eoutcome-result-renamevarp-eoutcome-result-equiv-congruence-on-new
 (implies (eoutcome-result-equiv new new-equiv)
          (equal (eoutcome-result-renamevarp old new ren)
                 (eoutcome-result-renamevarp old new-equiv ren)))
 :rule-classes :congruence)

Theorem: eoutcome-result-renamevarp-of-renaming-fix-ren

(defthm eoutcome-result-renamevarp-of-renaming-fix-ren
  (equal (eoutcome-result-renamevarp old new (renaming-fix ren))
         (eoutcome-result-renamevarp old new ren)))

Theorem: eoutcome-result-renamevarp-renaming-equiv-congruence-on-ren

(defthm eoutcome-result-renamevarp-renaming-equiv-congruence-on-ren
  (implies (renaming-equiv ren ren-equiv)
           (equal (eoutcome-result-renamevarp old new ren)
                  (eoutcome-result-renamevarp old new ren-equiv)))
  :rule-classes :congruence)