		Search-engine friendly clone of the ACL2 documentation.

Network

Aignet-nxsts-aux

Signature
(aignet-nxsts-aux n aignet) → nxsts
Arguments: n — Guard (natp n).; aignet — Guard (node-listp aignet).
Returns: nxsts — Type (node-listp nxsts).

Definitions and Theorems

Function: aignet-nxsts-aux

(defun aignet-nxsts-aux (n aignet)
  (declare (xargs :guard (and (natp n) (node-listp aignet))))
  (declare (xargs :guard (<= n (stype-count :reg aignet))))
  (let ((__function__ 'aignet-nxsts-aux))
    (declare (ignorable __function__))
    (if (zp n)
        nil
      (cons (nxst-node (lookup-reg->nxst (1- n) aignet)
                       (1- n))
            (aignet-nxsts-aux (1- n) aignet)))))

Theorem: node-listp-of-aignet-nxsts-aux

(defthm node-listp-of-aignet-nxsts-aux
  (b* ((nxsts (aignet-nxsts-aux n aignet)))
    (node-listp nxsts))
  :rule-classes :rewrite)

Theorem: fanin-count-of-aignet-nxsts-aux

(defthm fanin-count-of-aignet-nxsts-aux
  (b* ((?nxsts (aignet-nxsts-aux n aignet)))
    (equal (fanin-count nxsts) 0)))

Theorem: lookup-id-of-aignet-nxsts-aux

(defthm lookup-id-of-aignet-nxsts-aux
  (b* ((?nxsts (aignet-nxsts-aux n aignet)))
    (equal (lookup-id k nxsts) nil)))

Theorem: stype-count-of-aignet-nxsts-aux

(defthm stype-count-of-aignet-nxsts-aux
  (b* ((?nxsts (aignet-nxsts-aux n aignet)))
    (equal (stype-count stype nxsts)
           (if (equal (stype-fix stype) :nxst)
               (nfix n)
             0))))

Theorem: aignet-nxsts-aux-of-nfix-n

(defthm aignet-nxsts-aux-of-nfix-n
  (equal (aignet-nxsts-aux (nfix n) aignet)
         (aignet-nxsts-aux n aignet)))

Theorem: aignet-nxsts-aux-nat-equiv-congruence-on-n

(defthm aignet-nxsts-aux-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (aignet-nxsts-aux n aignet)
                  (aignet-nxsts-aux n-equiv aignet)))
  :rule-classes :congruence)

Theorem: aignet-nxsts-aux-of-node-list-fix-aignet

(defthm aignet-nxsts-aux-of-node-list-fix-aignet
  (equal (aignet-nxsts-aux n (node-list-fix aignet))
         (aignet-nxsts-aux n aignet)))

Theorem: aignet-nxsts-aux-node-list-equiv-congruence-on-aignet

(defthm aignet-nxsts-aux-node-list-equiv-congruence-on-aignet
  (implies (node-list-equiv aignet aignet-equiv)
           (equal (aignet-nxsts-aux n aignet)
                  (aignet-nxsts-aux n aignet-equiv)))
  :rule-classes :congruence)

Theorem: lookup-stype-of-aignet-nxsts-aux

(defthm lookup-stype-of-aignet-nxsts-aux
  (b* ((?nxsts (aignet-nxsts-aux n aignet)))
    (implies (not (equal (stype-fix stype) :nxst))
             (equal (lookup-stype k stype nxsts)
                    nil))))

Theorem: lookup-reg->nxst-of-aignet-nxsts-aux

(defthm lookup-reg->nxst-of-aignet-nxsts-aux
  (b* ((?nxsts (aignet-nxsts-aux n aignet)))
    (implies (<= (fanin-count aignet)
                 (fanin-count rest))
             (equal (lookup-reg->nxst k (append nxsts rest))
                    (if (and (< (nfix k) (nfix n))
                             (< (nfix k) (stype-count :reg rest)))
                        (lookup-reg->nxst k aignet)
                      (lookup-reg->nxst k rest))))))

Theorem: aignet-nxsts-aux-of-append-aignet-nxsts-aux

(defthm aignet-nxsts-aux-of-append-aignet-nxsts-aux
 (implies
    (and (<= (nfix n) (stype-count :reg rest))
         (<= (fanin-count x) (fanin-count rest))
         (<= (nfix n) (nfix m)))
    (equal (aignet-nxsts-aux n (append (aignet-nxsts-aux m x) rest))
           (aignet-nxsts-aux n x))))

Theorem: aignet-nxsts-aux-of-cons

(defthm aignet-nxsts-aux-of-cons
 (implies
  (<= (nfix n) (stype-count :reg x))
  (equal
    (aignet-nxsts-aux n (cons node x))
    (if
      (and (equal (stype node) :nxst)
           (< (nxst-node->reg node) (nfix n)))
      (update-nth (- (nfix n) (+ 1 (nxst-node->reg node)))
                  (nxst-node (aignet-lit-fix (nxst-node->fanin node)
                                             x)
                             (nxst-node->reg node))
                  (aignet-nxsts-aux n x))
      (aignet-nxsts-aux n x)))))