		Search-engine friendly clone of the ACL2 documentation.

Certificates

Unequivocal-certs-with-authors+round

Properties of certs-with-authors+round when used on unequivocal certificate sets.

The first theorem says that if certificates with certain authors and a certain round are retrieved from a subset of an unequivocal set of certificates, the same certificates are retrieved from the superset. Note the hypothesis that the given authors are all in the certificates at the given round in the subset. That is, a certificates for each author is in the subset at the round. Otherwise, the superset could have additional certificates at the round, with authors not found in the subset at the round. For the proof, we introduce a local lemma for the membership subgoal that arises from the pick-a-point strategy.

The second theorem says that if certificates with certain authors and a certain round are retrieved from both of two mutually unequivocal certificate sets, the same certificates are retrieved from both sets. For the proof, we introduce two local lemmas for the two containment membership subgoals from the pick-a-point strategy. The first hypothesis of the first lemma binds the authors and certs1 variables; the first hypothesis of the second lemma binds the authors and certs2 variables.

Definitions and Theorems

Theorem: certs-with-authors+round-of-unequivocal-superset

(defthm certs-with-authors+round-of-unequivocal-superset
 (implies
  (and
    (certificate-setp certs0)
    (certificate-setp certs)
    (subset certs0 certs)
    (certificate-set-unequivocalp certs)
    (posp round)
    (address-setp authors)
    (subset authors
            (cert-set->author-set (certs-with-round round certs0))))
  (equal (certs-with-authors+round authors round certs)
         (certs-with-authors+round authors round certs0))))

Theorem: certs-with-authors+round-of-unequivocal-sets

(defthm certs-with-authors+round-of-unequivocal-sets
 (implies
  (and
    (certificate-setp certs1)
    (certificate-setp certs2)
    (certificate-sets-unequivocalp certs1 certs2)
    (posp round)
    (address-setp authors)
    (subset authors
            (cert-set->author-set (certs-with-round round certs1)))
    (subset authors
            (cert-set->author-set (certs-with-round round certs2))))
  (equal (certs-with-authors+round authors round certs1)
         (certs-with-authors+round authors round certs2))))