		Search-engine friendly clone of the ACL2 documentation.

Proposals

Prop-set-unequivp

Check if a set of proposals is unequivocal.

That is, check whether the proposals in the set have unique combinations of author and round. We check that any two proposals in the set with the same author and round are in fact the same proposal. This means that the proposals in the set are uniquely identified by their author and round.

The rule prop-set-unequivp-of-insert is useful to prove the preservation of non-equivocation when a set of proposals is extended. Either the added proposal is already in the initial set, or the initial set has no proposal with the added proposal's author and round.

Definitions and Theorems

Theorem: prop-set-unequivp-necc

(defthm prop-set-unequivp-necc
  (implies (not (if (and (in prop1 (proposal-set-fix props))
                         (in prop2 (proposal-set-fix props))
                         (equal (proposal->author prop1)
                                (proposal->author prop2))
                         (equal (proposal->round prop1)
                                (proposal->round prop2)))
                    (if (equal prop1 prop2) t nil)
                  t))
           (not (prop-set-unequivp props))))

Theorem: booleanp-of-prop-set-unequivp

(defthm booleanp-of-prop-set-unequivp
  (b* ((yes/no (prop-set-unequivp props)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: prop-set-unequivp-of-proposal-set-fix-props

(defthm prop-set-unequivp-of-proposal-set-fix-props
  (equal (prop-set-unequivp (proposal-set-fix props))
         (prop-set-unequivp props)))

Theorem: prop-set-unequivp-proposal-set-equiv-congruence-on-props

(defthm prop-set-unequivp-proposal-set-equiv-congruence-on-props
  (implies (proposal-set-equiv props props-equiv)
           (equal (prop-set-unequivp props)
                  (prop-set-unequivp props-equiv)))
  :rule-classes :congruence)

Theorem: prop-set-unequivp-when-subset

(defthm prop-set-unequivp-when-subset
  (implies (and (prop-set-unequivp props)
                (subset (proposal-set-fix props0)
                        (proposal-set-fix props)))
           (prop-set-unequivp props0)))

Theorem: proop-set-unequivp-of-empty

(defthm proop-set-unequivp-of-empty
  (prop-set-unequivp nil))

Theorem: prop-set-unequivp-of-insert

(defthm prop-set-unequivp-of-insert
 (implies
  (and (proposal-setp props)
       (proposalp prop))
  (equal
   (prop-set-unequivp (insert prop props))
   (and (prop-set-unequivp props)
        (or (in prop props)
            (emptyp (props-with-author+round (proposal->author prop)
                                             (proposal->round prop)
                                             props)))))))

Theorem: prop-set-unequivp-of-delete

(defthm prop-set-unequivp-of-delete
  (implies (and (proposal-setp props)
                (prop-set-unequivp props))
           (prop-set-unequivp (delete prop props))))