• 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
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
        • Builtin-defaxioms/defthms
          • Builtin-defthms
          • Builtin-defaxioms
          • Builtin-defaxioms/defthms-by-rule-classes
            • Builtin-defaxioms/defthms-without-rule-classes
            • Builtin-defaxioms/defthms-of-class-type-prescription
            • Builtin-defaxioms/defthms-of-class-rewrite
            • Builtin-defaxioms/defthms-of-class-forward-chaining
            • Builtin-defaxioms/defthms-of-class-definition
            • Builtin-defaxioms/defthms-of-class-congruence
            • Builtin-defaxioms/defthms-of-class-linear
            • Builtin-defaxioms/defthms-of-class-compound-recognizer
            • Builtin-defaxioms/defthms-of-class-tau-system
            • Builtin-defaxioms/defthms-of-class-equivalence
            • Builtin-defaxioms/defthms-of-class-elim
            • Builtin-defaxioms/defthms-of-class-well-founded-relation
            • Builtin-defaxioms/defthms-of-class-type-set-inverter
            • Builtin-defaxioms/defthms-of-class-rewrite-quoted-constant
            • Builtin-defaxioms/defthms-of-class-refinement
            • Builtin-defaxioms/defthms-of-class-generalize
            • Builtin-defaxioms/defthms-of-class-clause-processor
            • Builtin-defaxioms/defthms-of-class-built-in-clause
            • Builtin-defaxioms/defthms-of-class-meta
            • Builtin-defaxioms/defthms-of-class-induction
          • Builtin-defaxioms/defthms-by-types/functions
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Builtin-defaxioms/defthms-by-rule-classes

Builtin-defaxioms/defthms-of-class-congruence

Built-in axioms and theorems of the :congruence rule class.

Theorem: fn-equal-implies-equal-do$-4

(defthm fn-equal-implies-equal-do$-4
  (implies (fn-equal finally-fn finally-fn-equiv)
           (equal (do$ measure-fn
                       alist do-fn finally-fn values dolia)
                  (do$ measure-fn alist
                       do-fn finally-fn-equiv values dolia)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-do$-3

(defthm fn-equal-implies-equal-do$-3
  (implies (fn-equal do-fn do-fn-equiv)
           (equal (do$ measure-fn
                       alist do-fn finally-fn values dolia)
                  (do$ measure-fn alist
                       do-fn-equiv finally-fn values dolia)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-do$-1

(defthm fn-equal-implies-equal-do$-1
  (implies (fn-equal measure-fn measure-fn-equiv)
           (equal (do$ measure-fn
                       alist do-fn finally-fn values dolia)
                  (do$ measure-fn-equiv
                       alist do-fn finally-fn values dolia)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-append$+-1

(defthm fn-equal-implies-equal-append$+-1
  (implies (fn-equal fn fn-equiv)
           (equal (append$+ fn globals lst)
                  (append$+ fn-equiv globals lst)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-append$+-ac-1

(defthm fn-equal-implies-equal-append$+-ac-1
  (implies (fn-equal fn fn-equiv)
           (equal (append$+-ac fn globals lst ac)
                  (append$+-ac fn-equiv globals lst ac)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-append$-1

(defthm fn-equal-implies-equal-append$-1
  (implies (fn-equal fn fn-equiv)
           (equal (append$ fn lst)
                  (append$ fn-equiv lst)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-append$-ac-1

(defthm fn-equal-implies-equal-append$-ac-1
  (implies (fn-equal fn fn-equiv)
           (equal (append$-ac fn lst ac)
                  (append$-ac fn-equiv lst ac)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-collect$+-1

(defthm fn-equal-implies-equal-collect$+-1
  (implies (fn-equal fn fn-equiv)
           (equal (collect$+ fn globals lst)
                  (collect$+ fn-equiv globals lst)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-collect$+-ac-1

(defthm fn-equal-implies-equal-collect$+-ac-1
  (implies (fn-equal fn fn-equiv)
           (equal (collect$+-ac fn globals lst ac)
                  (collect$+-ac fn-equiv globals lst ac)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-collect$-1

(defthm fn-equal-implies-equal-collect$-1
  (implies (fn-equal fn fn-equiv)
           (equal (collect$ fn lst)
                  (collect$ fn-equiv lst)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-collect$-ac-1

(defthm fn-equal-implies-equal-collect$-ac-1
  (implies (fn-equal fn fn-equiv)
           (equal (collect$-ac fn lst ac)
                  (collect$-ac fn-equiv lst ac)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-thereis$+-1

(defthm fn-equal-implies-equal-thereis$+-1
  (implies (fn-equal fn fn-equiv)
           (equal (thereis$+ fn globals lst)
                  (thereis$+ fn-equiv globals lst)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-thereis$-1

(defthm fn-equal-implies-equal-thereis$-1
  (implies (fn-equal fn fn-equiv)
           (equal (thereis$ fn lst)
                  (thereis$ fn-equiv lst)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-always$+-1

(defthm fn-equal-implies-equal-always$+-1
  (implies (fn-equal fn fn-equiv)
           (equal (always$+ fn globals lst)
                  (always$+ fn-equiv globals lst)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-always$-1

(defthm fn-equal-implies-equal-always$-1
  (implies (fn-equal fn fn-equiv)
           (equal (always$ fn lst)
                  (always$ fn-equiv lst)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-sum$+-1

(defthm fn-equal-implies-equal-sum$+-1
  (implies (fn-equal fn fn-equiv)
           (equal (sum$+ fn globals lst)
                  (sum$+ fn-equiv globals lst)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-sum$+-ac-1

(defthm fn-equal-implies-equal-sum$+-ac-1
  (implies (fn-equal fn fn-equiv)
           (equal (sum$+-ac fn globals lst ac)
                  (sum$+-ac fn-equiv globals lst ac)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-sum$-1

(defthm fn-equal-implies-equal-sum$-1
  (implies (fn-equal fn fn-equiv)
           (equal (sum$ fn lst)
                  (sum$ fn-equiv lst)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-sum$-ac-1

(defthm fn-equal-implies-equal-sum$-ac-1
  (implies (fn-equal fn fn-equiv)
           (equal (sum$-ac fn lst ac)
                  (sum$-ac fn-equiv lst ac)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-when$+-1

(defthm fn-equal-implies-equal-when$+-1
  (implies (fn-equal fn fn-equiv)
           (equal (when$+ fn globals lst)
                  (when$+ fn-equiv globals lst)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-when$+-ac-1

(defthm fn-equal-implies-equal-when$+-ac-1
  (implies (fn-equal fn fn-equiv)
           (equal (when$+-ac fn globals lst ac)
                  (when$+-ac fn-equiv globals lst ac)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-when$-1

(defthm fn-equal-implies-equal-when$-1
  (implies (fn-equal fn fn-equiv)
           (equal (when$ fn lst)
                  (when$ fn-equiv lst)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-when$-ac-1

(defthm fn-equal-implies-equal-when$-ac-1
  (implies (fn-equal fn fn-equiv)
           (equal (when$-ac fn lst ac)
                  (when$-ac fn-equiv lst ac)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-until$+-1

(defthm fn-equal-implies-equal-until$+-1
  (implies (fn-equal fn fn-equiv)
           (equal (until$+ fn globals lst)
                  (until$+ fn-equiv globals lst)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-until$+-ac-1

(defthm fn-equal-implies-equal-until$+-ac-1
  (implies (fn-equal fn fn-equiv)
           (equal (until$+-ac fn globals lst ac)
                  (until$+-ac fn-equiv globals lst ac)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-until$-1

(defthm fn-equal-implies-equal-until$-1
  (implies (fn-equal fn fn-equiv)
           (equal (until$ fn lst)
                  (until$ fn-equiv lst)))
  :rule-classes (:congruence))

Theorem: fn-equal-implies-equal-until$-ac-1

(defthm fn-equal-implies-equal-until$-ac-1
  (implies (fn-equal fn fn-equiv)
           (equal (until$-ac fn lst ac)
                  (until$-ac fn-equiv lst ac)))
  :rule-classes (:congruence))

Theorem: iff-implies-equal-not

(defthm iff-implies-equal-not
  (implies (iff x x-equiv)
           (equal (not x) (not x-equiv)))
  :rule-classes (:congruence))

Theorem: iff-implies-equal-implies-2

(defthm iff-implies-equal-implies-2
  (implies (iff y y-equiv)
           (equal (implies x y)
                  (implies x y-equiv)))
  :rule-classes (:congruence))

Theorem: iff-implies-equal-implies-1

(defthm iff-implies-equal-implies-1
  (implies (iff x x-equiv)
           (equal (implies x y)
                  (implies x-equiv y)))
  :rule-classes (:congruence))