• Top
    • Documentation
    • Books
    • Boolean-reasoning
      • Ipasir
      • Aignet
        • Base-api
        • Aignet-construction
        • Representation
        • Aignet-copy-init
        • Aignet-simplify-with-tracking
        • Aignet-simplify-marked-with-tracking
        • Aignet-cnf
        • Aignet-simplify-marked
        • Aignet-complete-copy
        • Aignet-transforms
          • Aignet-output-ranges
            • Aignet-output-range-map
              • Aignet-output-range-map-p
              • Aignet-output-range-map-fix
              • Aignet-output-range-map-equiv
            • Aignet-comb-transforms
            • Aignet-m-assumption-n-output-transforms
            • Aignet-n-output-comb-transforms
          • Aignet-eval
          • Semantics
          • Aignet-read-aiger
          • Aignet-write-aiger
          • Aignet-abc-interface
          • Utilities
        • Aig
        • Satlink
        • Truth
        • Ubdds
        • Bdd
        • Faig
        • Bed
        • 4v
      • Projects
      • Debugging
      • Std
      • Community
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Aignet-output-range-map

    Aignet-output-range-map-equiv

    Basic equivalence relation for aignet-output-range-map structures.

    Definitions and Theorems

    Function: aignet-output-range-map-equiv$inline

    (defun aignet-output-range-map-equiv$inline (x acl2::y)
      (declare (xargs :guard (and (aignet-output-range-map-p x)
                                  (aignet-output-range-map-p acl2::y))))
      (equal (aignet-output-range-map-fix x)
             (aignet-output-range-map-fix acl2::y)))

    Theorem: aignet-output-range-map-equiv-is-an-equivalence

    (defthm aignet-output-range-map-equiv-is-an-equivalence
      (and (booleanp (aignet-output-range-map-equiv x y))
           (aignet-output-range-map-equiv x x)
           (implies (aignet-output-range-map-equiv x y)
                    (aignet-output-range-map-equiv y x))
           (implies (and (aignet-output-range-map-equiv x y)
                         (aignet-output-range-map-equiv y z))
                    (aignet-output-range-map-equiv x z)))
      :rule-classes (:equivalence))

    Theorem: aignet-output-range-map-equiv-implies-equal-aignet-output-range-map-fix-1

    (defthm
     aignet-output-range-map-equiv-implies-equal-aignet-output-range-map-fix-1
     (implies (aignet-output-range-map-equiv x x-equiv)
              (equal (aignet-output-range-map-fix x)
                     (aignet-output-range-map-fix x-equiv)))
     :rule-classes (:congruence))

    Theorem: aignet-output-range-map-fix-under-aignet-output-range-map-equiv

    (defthm
        aignet-output-range-map-fix-under-aignet-output-range-map-equiv
      (aignet-output-range-map-equiv (aignet-output-range-map-fix x)
                                     x)
      :rule-classes (:rewrite :rewrite-quoted-constant))

    Theorem: equal-of-aignet-output-range-map-fix-1-forward-to-aignet-output-range-map-equiv

    (defthm
     equal-of-aignet-output-range-map-fix-1-forward-to-aignet-output-range-map-equiv
     (implies (equal (aignet-output-range-map-fix x)
                     acl2::y)
              (aignet-output-range-map-equiv x acl2::y))
     :rule-classes :forward-chaining)

    Theorem: equal-of-aignet-output-range-map-fix-2-forward-to-aignet-output-range-map-equiv

    (defthm
     equal-of-aignet-output-range-map-fix-2-forward-to-aignet-output-range-map-equiv
     (implies (equal x (aignet-output-range-map-fix acl2::y))
              (aignet-output-range-map-equiv x acl2::y))
     :rule-classes :forward-chaining)

    Theorem: aignet-output-range-map-equiv-of-aignet-output-range-map-fix-1-forward

    (defthm
     aignet-output-range-map-equiv-of-aignet-output-range-map-fix-1-forward
     (implies
          (aignet-output-range-map-equiv (aignet-output-range-map-fix x)
                                         acl2::y)
          (aignet-output-range-map-equiv x acl2::y))
     :rule-classes :forward-chaining)

    Theorem: aignet-output-range-map-equiv-of-aignet-output-range-map-fix-2-forward

    (defthm
     aignet-output-range-map-equiv-of-aignet-output-range-map-fix-2-forward
     (implies (aignet-output-range-map-equiv
                   x (aignet-output-range-map-fix acl2::y))
              (aignet-output-range-map-equiv x acl2::y))
     :rule-classes :forward-chaining)