		Search-engine friendly clone of the ACL2 documentation.

Network

Aignet-outputs

Signature
(aignet-outputs aignet) → outputs
Arguments: aignet — Guard (node-listp aignet).
Returns: outputs — Type (node-listp outputs).

Definitions and Theorems

Function: aignet-outputs

(defun aignet-outputs (aignet)
  (declare (xargs :guard (node-listp aignet)))
  (let ((__function__ 'aignet-outputs))
    (declare (ignorable __function__))
    (aignet-outputs-aux (stype-count :po aignet)
                        aignet)))

Theorem: node-listp-of-aignet-outputs

(defthm node-listp-of-aignet-outputs
  (b* ((outputs (aignet-outputs aignet)))
    (node-listp outputs))
  :rule-classes :rewrite)

Theorem: fanin-count-of-aignet-outputs

(defthm fanin-count-of-aignet-outputs
  (b* ((?outputs (aignet-outputs aignet)))
    (equal (fanin-count outputs) 0)))

Theorem: lookup-id-of-aignet-outputs

(defthm lookup-id-of-aignet-outputs
  (b* ((?outputs (aignet-outputs aignet)))
    (equal (lookup-id k outputs) nil)))

Theorem: stype-count-of-aignet-outputs

(defthm stype-count-of-aignet-outputs
  (b* ((?outputs (aignet-outputs aignet)))
    (equal (stype-count stype outputs)
           (if (equal (stype-fix stype) :po)
               (stype-count :po aignet)
             0))))

Theorem: aignet-outputs-of-node-list-fix-aignet

(defthm aignet-outputs-of-node-list-fix-aignet
  (equal (aignet-outputs (node-list-fix aignet))
         (aignet-outputs aignet)))

Theorem: aignet-outputs-node-list-equiv-congruence-on-aignet

(defthm aignet-outputs-node-list-equiv-congruence-on-aignet
  (implies (node-list-equiv aignet aignet-equiv)
           (equal (aignet-outputs aignet)
                  (aignet-outputs aignet-equiv)))
  :rule-classes :congruence)

Theorem: lookup-stype-of-aignet-outputs

(defthm lookup-stype-of-aignet-outputs
  (b* ((?outputs (aignet-outputs aignet)))
    (equal (lookup-stype k stype outputs)
           (if (and (equal (stype-fix stype) :po)
                    (< (nfix k) (stype-count :po aignet)))
               (aignet-outputs (lookup-stype k :po aignet))
             nil))))

Theorem: lookup-reg->nxst-of-append-aignet-outputs

(defthm lookup-reg->nxst-of-append-aignet-outputs
  (b* ((?outputs (aignet-outputs aignet)))
    (equal (lookup-reg->nxst k (append outputs rest))
           (lookup-reg->nxst k rest))))

Theorem: car-of-aignet-outputs

(defthm car-of-aignet-outputs
 (b* ((?outputs (aignet-outputs aignet)))
  (implies
    (posp (stype-count :po aignet))
    (equal
         (car outputs)
         (po-node (fanin 0
                         (lookup-stype (1- (stype-count :po aignet))
                                       :po aignet)))))))

Theorem: consp-of-aignet-outputs

(defthm consp-of-aignet-outputs
  (b* ((?outputs (aignet-outputs aignet)))
    (equal (consp outputs)
           (posp (stype-count :po aignet)))))

Theorem: aignet-outputs-of-append-aignet-outputs

(defthm aignet-outputs-of-append-aignet-outputs
 (b* nil
   (implies (and (equal (stype-count :po rest) 0)
                 (<= (fanin-count x) (fanin-count rest)))
            (equal (aignet-outputs (append (aignet-outputs x) rest))
                   (aignet-outputs x)))))

Theorem: aignet-outputs-of-append-non-outputs

(defthm aignet-outputs-of-append-non-outputs
  (implies (equal (stype-count :po first) 0)
           (equal (aignet-outputs (append first x))
                  (aignet-outputs x))))

Theorem: aignet-outputs-of-cons

(defthm aignet-outputs-of-cons
  (equal (aignet-outputs (cons node x))
         (if (equal (stype node) :po)
             (cons (po-node (aignet-lit-fix (po-node->fanin node)
                                            x))
                   (aignet-outputs x))
           (aignet-outputs x))))