		Search-engine friendly clone of the ACL2 documentation.

System-certificates

System-certs-when-init

Initially, there are no certificates in the system.

All DAGs are initially empty, and the network is initially empty.

Definitions and Theorems

Theorem: validators-certs-when-init

(defthm validators-certs-when-init
  (implies (and (system-initp systate)
                (subset vals (correct-addresses systate)))
           (equal (validators-certs vals systate)
                  nil)))

Theorem: system-certs-when-init

(defthm system-certs-when-init
  (implies (system-initp systate)
           (equal (system-certs systate) nil)))