		Search-engine friendly clone of the ACL2 documentation.

Committed-anchor-sequences

Committed-anchors-when-init

Initially, a validator has no committed anchors.

Definitions and Theorems

Theorem: committed-anchors-when-init

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