• 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-fix

    (aignet-output-range-map-fix x) is an ACL2::fty alist fixing function that follows the fix-keys strategy.

    Signature
    (aignet-output-range-map-fix x) → fty::newx
    Arguments
    x — Guard (aignet-output-range-map-p x).
    Returns
    fty::newx — Type (aignet-output-range-map-p fty::newx).

    Note that in the execution this is just an inline identity function.

    Definitions and Theorems

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

    (defun aignet-output-range-map-fix$inline (x)
      (declare (xargs :guard (aignet-output-range-map-p x)))
      (let ((__function__ 'aignet-output-range-map-fix))
        (declare (ignorable __function__))
        (mbe :logic
             (if (atom x)
                 nil
               (if (consp (car x))
                   (cons (cons (acl2::symbol-fix (caar x))
                               (nfix (cdar x)))
                         (aignet-output-range-map-fix (cdr x)))
                 (aignet-output-range-map-fix (cdr x))))
             :exec x)))

    Theorem: aignet-output-range-map-p-of-aignet-output-range-map-fix

    (defthm aignet-output-range-map-p-of-aignet-output-range-map-fix
      (b* ((fty::newx (aignet-output-range-map-fix$inline x)))
        (aignet-output-range-map-p fty::newx))
      :rule-classes :rewrite)

    Theorem: aignet-output-range-map-fix-when-aignet-output-range-map-p

    (defthm aignet-output-range-map-fix-when-aignet-output-range-map-p
      (implies (aignet-output-range-map-p x)
               (equal (aignet-output-range-map-fix x)
                      x)))

    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)

    Theorem: cons-of-symbol-fix-k-under-aignet-output-range-map-equiv

    (defthm cons-of-symbol-fix-k-under-aignet-output-range-map-equiv
      (aignet-output-range-map-equiv
           (cons (cons (acl2::symbol-fix acl2::k)
                       acl2::v)
                 x)
           (cons (cons acl2::k acl2::v) x)))

    Theorem: cons-symbol-equiv-congruence-on-k-under-aignet-output-range-map-equiv

    (defthm
     cons-symbol-equiv-congruence-on-k-under-aignet-output-range-map-equiv
     (implies
        (acl2::symbol-equiv acl2::k k-equiv)
        (aignet-output-range-map-equiv (cons (cons acl2::k acl2::v) x)
                                       (cons (cons k-equiv acl2::v) x)))
     :rule-classes :congruence)

    Theorem: cons-of-nfix-v-under-aignet-output-range-map-equiv

    (defthm cons-of-nfix-v-under-aignet-output-range-map-equiv
      (aignet-output-range-map-equiv
           (cons (cons acl2::k (nfix acl2::v)) x)
           (cons (cons acl2::k acl2::v) x)))

    Theorem: cons-nat-equiv-congruence-on-v-under-aignet-output-range-map-equiv

    (defthm
     cons-nat-equiv-congruence-on-v-under-aignet-output-range-map-equiv
     (implies
        (nat-equiv acl2::v v-equiv)
        (aignet-output-range-map-equiv (cons (cons acl2::k acl2::v) x)
                                       (cons (cons acl2::k v-equiv) x)))
     :rule-classes :congruence)

    Theorem: cons-of-aignet-output-range-map-fix-y-under-aignet-output-range-map-equiv

    (defthm
     cons-of-aignet-output-range-map-fix-y-under-aignet-output-range-map-equiv
     (aignet-output-range-map-equiv
          (cons x (aignet-output-range-map-fix acl2::y))
          (cons x acl2::y)))

    Theorem: cons-aignet-output-range-map-equiv-congruence-on-y-under-aignet-output-range-map-equiv

    (defthm
     cons-aignet-output-range-map-equiv-congruence-on-y-under-aignet-output-range-map-equiv
     (implies (aignet-output-range-map-equiv acl2::y y-equiv)
              (aignet-output-range-map-equiv (cons x acl2::y)
                                             (cons x y-equiv)))
     :rule-classes :congruence)

    Theorem: aignet-output-range-map-fix-of-acons

    (defthm aignet-output-range-map-fix-of-acons
      (equal
           (aignet-output-range-map-fix (cons (cons acl2::a acl2::b) x))
           (cons (cons (acl2::symbol-fix acl2::a)
                       (nfix acl2::b))
                 (aignet-output-range-map-fix x))))

    Theorem: aignet-output-range-map-fix-of-append

    (defthm aignet-output-range-map-fix-of-append
      (equal (aignet-output-range-map-fix (append std::a std::b))
             (append (aignet-output-range-map-fix std::a)
                     (aignet-output-range-map-fix std::b))))

    Theorem: consp-car-of-aignet-output-range-map-fix

    (defthm consp-car-of-aignet-output-range-map-fix
      (equal (consp (car (aignet-output-range-map-fix x)))
             (consp (aignet-output-range-map-fix x))))