		Search-engine friendly clone of the ACL2 documentation.

Node

Node-fix

Fixing function for node structures.

Signature
(node-fix x) → new-x
Arguments: x — Guard (node-p x).
Returns: new-x — Type (node-p new-x).

Definitions and Theorems

Function: node-fix$inline

(defun
     node-fix$inline (x)
     (declare (xargs :guard (node-p x)))
     (let ((__function__ 'node-fix))
          (declare (ignorable __function__))
          (mbe :logic (case (stype x)
                            (:const nil)
                            (:pi '(:pi))
                            (:reg '(:reg))
                            (:and (b* ((fanin0 (lit-fix (cadr x)))
                                       (fanin1 (lit-fix (caddr x))))
                                      (list :and fanin0 fanin1)))
                            (:xor (b* ((fanin0 (lit-fix (cadr x)))
                                       (fanin1 (lit-fix (caddr x))))
                                      (list :xor fanin0 fanin1)))
                            (:po (b* ((fanin (lit-fix (cadr x))))
                                     (list :po fanin)))
                            (:nxst (b* ((fanin (lit-fix (cadr x)))
                                        (reg (nfix (caddr x))))
                                       (list :nxst fanin reg))))
               :exec x)))

Theorem: node-p-of-node-fix

(defthm node-p-of-node-fix
        (b* ((new-x (node-fix$inline x)))
            (node-p new-x))
        :rule-classes :rewrite)

Theorem: node-fix-when-node-p

(defthm node-fix-when-node-p
        (implies (node-p x)
                 (equal (node-fix x) x)))

Function: node-equiv$inline

(defun node-equiv$inline (x acl2::y)
       (declare (xargs :guard (and (node-p x) (node-p acl2::y))))
       (equal (node-fix x) (node-fix acl2::y)))

Theorem: node-equiv-is-an-equivalence

(defthm node-equiv-is-an-equivalence
        (and (booleanp (node-equiv x y))
             (node-equiv x x)
             (implies (node-equiv x y)
                      (node-equiv y x))
             (implies (and (node-equiv x y) (node-equiv y z))
                      (node-equiv x z)))
        :rule-classes (:equivalence))

Theorem: node-equiv-implies-equal-node-fix-1

(defthm node-equiv-implies-equal-node-fix-1
        (implies (node-equiv x x-equiv)
                 (equal (node-fix x) (node-fix x-equiv)))
        :rule-classes (:congruence))

Theorem: node-fix-under-node-equiv

(defthm node-fix-under-node-equiv
        (node-equiv (node-fix x) x)
        :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-node-fix-1-forward-to-node-equiv

(defthm equal-of-node-fix-1-forward-to-node-equiv
        (implies (equal (node-fix x) acl2::y)
                 (node-equiv x acl2::y))
        :rule-classes :forward-chaining)

Theorem: equal-of-node-fix-2-forward-to-node-equiv

(defthm equal-of-node-fix-2-forward-to-node-equiv
        (implies (equal x (node-fix acl2::y))
                 (node-equiv x acl2::y))
        :rule-classes :forward-chaining)

Theorem: node-equiv-of-node-fix-1-forward

(defthm node-equiv-of-node-fix-1-forward
        (implies (node-equiv (node-fix x) acl2::y)
                 (node-equiv x acl2::y))
        :rule-classes :forward-chaining)

Theorem: node-equiv-of-node-fix-2-forward

(defthm node-equiv-of-node-fix-2-forward
        (implies (node-equiv x (node-fix acl2::y))
                 (node-equiv x acl2::y))
        :rule-classes :forward-chaining)

Theorem: stype$inline-of-node-fix-x

(defthm stype$inline-of-node-fix-x
        (equal (stype$inline (node-fix x))
               (stype$inline x)))

Theorem: stype$inline-node-equiv-congruence-on-x

(defthm stype$inline-node-equiv-congruence-on-x
        (implies (node-equiv x x-equiv)
                 (equal (stype$inline x)
                        (stype$inline x-equiv)))
        :rule-classes :congruence)