		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))))