		Search-engine friendly clone of the ACL2 documentation.

Blocks

Blocks-last-round

Last round in a list of blocks, or 0 if there are no blocks.

Signature
(blocks-last-round blocks) → last
Arguments: blocks — Guard (block-listp blocks).
Returns: last — Type (natp last).

If blocks-ordered-even-p holds, block rounds are in strictly increading order from right to left. This function then returns the latest, i.e. highest, round. If there are no blocks, we totalize this function to return 0. However, we do not require blocks-ordered-even-p in the guard.

Definitions and Theorems

Function: blocks-last-round

(defun blocks-last-round (blocks)
  (declare (xargs :guard (block-listp blocks)))
  (let ((__function__ 'blocks-last-round))
    (declare (ignorable __function__))
    (if (consp blocks)
        (block->round (car blocks))
      0)))

Theorem: natp-of-blocks-last-round

(defthm natp-of-blocks-last-round
  (b* ((last (blocks-last-round blocks)))
    (natp last))
  :rule-classes :rewrite)

Theorem: evenp-of-blocks-last-round

(defthm evenp-of-blocks-last-round
  (implies (blocks-ordered-even-p blocks)
           (evenp (blocks-last-round blocks))))

Theorem: oldest-of-prefix-gt-newest-of-suffix-when-blocks-ordered-even-p

(defthm
    oldest-of-prefix-gt-newest-of-suffix-when-blocks-ordered-even-p
  (implies (and (blocks-ordered-even-p (append blocks1 blocks2))
                (consp blocks1))
           (> (block->round (car (last blocks1)))
              (blocks-last-round blocks2))))

Theorem: blocks-last-round-of-block-list-fix-blocks

(defthm blocks-last-round-of-block-list-fix-blocks
  (equal (blocks-last-round (block-list-fix blocks))
         (blocks-last-round blocks)))

Theorem: blocks-last-round-block-list-equiv-congruence-on-blocks

(defthm blocks-last-round-block-list-equiv-congruence-on-blocks
  (implies (block-list-equiv blocks blocks-equiv)
           (equal (blocks-last-round blocks)
                  (blocks-last-round blocks-equiv)))
  :rule-classes :congruence)