		Search-engine friendly clone of the ACL2 documentation.

Last-anchor-def-and-init

Last-anchor-when-init

Initially, a validator has no last committed anchor.

Definitions and Theorems

Theorem: last-anchor-when-init

(defthm last-anchor-when-init
  (implies (and (system-initp systate)
                (in val (correct-addresses systate)))
           (equal (last-anchor (get-validator-state val systate))
                  nil)))