		Search-engine friendly clone of the ACL2 documentation.

Unequivocal-signed-certificates

Unequivocal-signed-certs-p-of-events-next

Preservation of the invariant by multiple transitions.

Definitions and Theorems

Theorem: unequivocal-signed-certs-p-of-events-next

(defthm unequivocal-signed-certs-p-of-events-next
  (implies
       (and (events-possiblep events systate)
            (signer-records-p systate)
            (no-self-endorsed-p systate)
            (unequivocal-signed-certs-p systate))
       (unequivocal-signed-certs-p (events-next events systate))))