		Search-engine friendly clone of the ACL2 documentation.

Unequivocal-signed-certificates

Unequivocal-signed-certs-p

Definition of the invariant: the set of certificates signed by each correct validator is unequivocal.

Definitions and Theorems

Theorem: unequivocal-signed-certs-p-necc

(defthm unequivocal-signed-certs-p-necc
 (implies
  (unequivocal-signed-certs-p systate)
  (implies
     (in signer (correct-addresses systate))
     (certificate-set-unequivocalp (signed-certs signer systate)))))

Theorem: booleanp-of-unequivocal-signed-certs-p

(defthm booleanp-of-unequivocal-signed-certs-p
  (b* ((yes/no (unequivocal-signed-certs-p systate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: unequivocal-signed-certs-p-of-system-state-fix-systate

(defthm unequivocal-signed-certs-p-of-system-state-fix-systate
  (equal (unequivocal-signed-certs-p (system-state-fix systate))
         (unequivocal-signed-certs-p systate)))

Theorem: unequivocal-signed-certs-p-system-state-equiv-congruence-on-systate

(defthm
 unequivocal-signed-certs-p-system-state-equiv-congruence-on-systate
 (implies (system-state-equiv systate systate-equiv)
          (equal (unequivocal-signed-certs-p systate)
                 (unequivocal-signed-certs-p systate-equiv)))
 :rule-classes :congruence)