		Search-engine friendly clone of the ACL2 documentation.

Network

Aignet-idp

Check whether a node ID is in bounds for this network.

Signature
(aignet-idp id aignet) → *
Arguments: id — Guard (natp id).; aignet — Guard (node-listp aignet).

Definitions and Theorems

Function: aignet-idp

(defun aignet-idp (id aignet)
  (declare (xargs :guard (and (natp id) (node-listp aignet))))
  (let ((__function__ 'aignet-idp))
    (declare (ignorable __function__))
    (<= (lnfix id) (fanin-count aignet))))

Theorem: aignet-idp-of-nfix-id

(defthm aignet-idp-of-nfix-id
  (equal (aignet-idp (nfix id) aignet)
         (aignet-idp id aignet)))

Theorem: aignet-idp-nat-equiv-congruence-on-id

(defthm aignet-idp-nat-equiv-congruence-on-id
  (implies (nat-equiv id id-equiv)
           (equal (aignet-idp id aignet)
                  (aignet-idp id-equiv aignet)))
  :rule-classes :congruence)

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

(defthm aignet-idp-of-node-list-fix-aignet
  (equal (aignet-idp id (node-list-fix aignet))
         (aignet-idp id aignet)))

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

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

Theorem: bound-when-aignet-idp

(defthm bound-when-aignet-idp
  (implies (aignet-idp id aignet)
           (<= (nfix id) (fanin-count aignet))))

Theorem: aignet-idp-in-extension

(defthm aignet-idp-in-extension
  (implies (and (aignet-extension-p aignet2 aignet)
                (aignet-idp id aignet))
           (aignet-idp id aignet2)))

Theorem: lookup-id-implies-aignet-idp

(defthm lookup-id-implies-aignet-idp
  (implies (consp (lookup-id id aignet))
           (aignet-idp id aignet)))

Theorem: aignet-idp-of-fanin-count-of-extension

(defthm aignet-idp-of-fanin-count-of-extension
  (implies (aignet-extension-p aignet prev)
           (aignet-idp (fanin-count prev) aignet)))

Theorem: aignet-idp-of-0

(defthm aignet-idp-of-0
  (aignet-idp 0 aignet))

Theorem: aignet-extension-simplify-lookup-id

(defthm aignet-extension-simplify-lookup-id
  (implies (and (aignet-extension-binding)
                (aignet-idp id orig))
           (equal (lookup-id id new)
                  (lookup-id id orig))))

Theorem: aignet-extension-simplify-aignet-idp

(defthm aignet-extension-simplify-aignet-idp
  (implies (and (aignet-extension-binding)
                (aignet-idp id orig))
           (aignet-idp id new)))