		Search-engine friendly clone of the ACL2 documentation.

Parametrize

Copy-lits-compose

Signature
(copy-lits-compose start count aignet litarr copy copy2) → new-copy2
Arguments: start — Guard (natp start).; count — Guard (natp count).

Definitions and Theorems

Function: copy-lits-compose

(defun copy-lits-compose (start count aignet litarr copy copy2)
  (declare (xargs :stobjs (aignet litarr copy copy2)))
  (declare (xargs :guard (and (natp start) (natp count))))
  (declare
       (xargs :guard (and (<= (+ start count)
                              (lits-length litarr))
                          (<= (num-fanins aignet)
                              (lits-length copy))
                          (<= (+ start count) (lits-length copy2))
                          (aignet-copies-in-bounds litarr aignet))))
  (let ((__function__ 'copy-lits-compose))
    (declare (ignorable __function__))
    (b* (((when (zp count)) copy2)
         (lit (get-lit start litarr))
         (copy2 (set-lit start (lit-copy lit copy)
                         copy2)))
      (copy-lits-compose (1+ (lnfix start))
                         (1- count)
                         aignet litarr copy copy2))))

Theorem: len-of-copy-lits-compose

(defthm len-of-copy-lits-compose
  (b*
    ((?new-copy2
          (copy-lits-compose start count aignet litarr copy copy2)))
    (implies (<= (+ (nfix start) (nfix count))
                 (len copy2))
             (equal (len new-copy2) (len copy2)))))

Theorem: nth-of-copy-lits-compose

(defthm nth-of-copy-lits-compose
  (b*
    ((?new-copy2
          (copy-lits-compose start count aignet litarr copy copy2)))
    (equal (nth-lit n new-copy2)
           (if (and (<= (nfix start) (nfix n))
                    (< (nfix n)
                       (+ (nfix start) (nfix count))))
               (lit-copy (nth-lit n litarr) copy)
             (nth-lit n copy2)))))

Theorem: aignet-elim-copy-lits-compose

(defthm aignet-elim-copy-lits-compose
 (b*
   ((?new-copy2
         (copy-lits-compose start count aignet litarr copy copy2)))
  (implies
    (syntaxp (not (equal aignet ''nil)))
    (equal new-copy2
           (let ((aignet nil))
             (copy-lits-compose start
                                count aignet litarr copy copy2))))))

Theorem: aignet-lit-listp-of-copy-lits-compose

(defthm aignet-lit-listp-of-copy-lits-compose
  (b*
    ((?new-copy2
          (copy-lits-compose start count aignet litarr copy copy2)))
    (implies (and (aignet-copies-in-bounds copy aignet2)
                  (aignet-lit-listp copy2 aignet2))
             (aignet-lit-listp new-copy2 aignet2))))

Theorem: copy-lits-compose-of-nfix-start

(defthm copy-lits-compose-of-nfix-start
  (equal (copy-lits-compose (nfix start)
                            count aignet litarr copy copy2)
         (copy-lits-compose start count aignet litarr copy copy2)))

Theorem: copy-lits-compose-nat-equiv-congruence-on-start

(defthm copy-lits-compose-nat-equiv-congruence-on-start
 (implies
     (nat-equiv start start-equiv)
     (equal (copy-lits-compose start count aignet litarr copy copy2)
            (copy-lits-compose start-equiv
                               count aignet litarr copy copy2)))
 :rule-classes :congruence)

Theorem: copy-lits-compose-of-nfix-count

(defthm copy-lits-compose-of-nfix-count
  (equal (copy-lits-compose start (nfix count)
                            aignet litarr copy copy2)
         (copy-lits-compose start count aignet litarr copy copy2)))

Theorem: copy-lits-compose-nat-equiv-congruence-on-count

(defthm copy-lits-compose-nat-equiv-congruence-on-count
 (implies
   (nat-equiv count count-equiv)
   (equal (copy-lits-compose start count aignet litarr copy copy2)
          (copy-lits-compose start
                             count-equiv aignet litarr copy copy2)))
 :rule-classes :congruence)

Theorem: copy-lits-compose-of-node-list-fix-aignet

(defthm copy-lits-compose-of-node-list-fix-aignet
  (equal (copy-lits-compose start count (node-list-fix aignet)
                            litarr copy copy2)
         (copy-lits-compose start count aignet litarr copy copy2)))

Theorem: copy-lits-compose-node-list-equiv-congruence-on-aignet

(defthm copy-lits-compose-node-list-equiv-congruence-on-aignet
 (implies
   (node-list-equiv aignet aignet-equiv)
   (equal (copy-lits-compose start count aignet litarr copy copy2)
          (copy-lits-compose start
                             count aignet-equiv litarr copy copy2)))
 :rule-classes :congruence)