		Search-engine friendly clone of the ACL2 documentation.

Same-associated-certificates

Same-associated-certs-p

Definition of the invariant: any two correct validators in the system have the same set of associated certificates.

Definitions and Theorems

Theorem: same-associated-certs-p-necc

(defthm same-associated-certs-p-necc
  (implies (same-associated-certs-p systate)
           (implies (and (in val1 (correct-addresses systate))
                         (in val2 (correct-addresses systate)))
                    (equal (associated-certs val1 systate)
                           (associated-certs val2 systate)))))

Theorem: booleanp-of-same-associated-certs-p

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

Theorem: same-associated-certs-p-of-system-state-fix-systate

(defthm same-associated-certs-p-of-system-state-fix-systate
  (equal (same-associated-certs-p (system-state-fix systate))
         (same-associated-certs-p systate)))

Theorem: same-associated-certs-p-system-state-equiv-congruence-on-systate

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