		Search-engine friendly clone of the ACL2 documentation.

Network

Aignet-outputs-aux

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

Definitions and Theorems

Function: aignet-outputs-aux

(defun aignet-outputs-aux (n aignet)
  (declare (xargs :guard (and (natp n) (node-listp aignet))))
  (declare (xargs :guard (<= n (stype-count :po aignet))))
  (let ((__function__ 'aignet-outputs-aux))
    (declare (ignorable __function__))
    (if (zp n)
        nil
      (cons (po-node (fanin 0 (lookup-stype (1- n) :po aignet)))
            (aignet-outputs-aux (1- n) aignet)))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: aignet-outputs-aux-of-lookup-po

(defthm aignet-outputs-aux-of-lookup-po
 (b* nil
  (implies (and (<= (nfix n) (+ 1 (nfix k)))
                (< (nfix k) (stype-count :po aignet)))
           (equal (aignet-outputs-aux n (lookup-stype k :po aignet))
                  (aignet-outputs-aux n aignet)))))

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

(defthm lookup-stype-of-aignet-outputs-aux
  (b* ((?outputs (aignet-outputs-aux n aignet)))
    (implies
         (<= (nfix n) (stype-count :po aignet))
         (equal (lookup-stype k stype outputs)
                (if (and (equal (stype-fix stype) :po)
                         (< (nfix k) (nfix n)))
                    (aignet-outputs-aux (+ 1 (nfix k))
                                        (lookup-stype k :po aignet))
                  nil)))))

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

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

Theorem: car-of-aignet-outputs-aux

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

Theorem: consp-of-aignet-outputs-aux

(defthm consp-of-aignet-outputs-aux
  (b* ((?outputs (aignet-outputs-aux n aignet)))
    (equal (consp outputs) (posp n))))

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

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

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

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

Theorem: aignet-outputs-aux-of-cons

(defthm aignet-outputs-aux-of-cons
  (implies (<= (nfix n) (stype-count :po x))
           (equal (aignet-outputs-aux n (cons node x))
                  (aignet-outputs-aux n x))))