		Search-engine friendly clone of the ACL2 documentation.

Proposals

Prop-set-none-author-p

Check if none of the proposals in a set have a given author.

Definitions and Theorems

Theorem: prop-set-none-author-p-necc

(defthm prop-set-none-author-p-necc
  (implies (prop-set-none-author-p author props)
           (implies (in prop (proposal-set-fix props))
                    (not (equal (proposal->author prop)
                                (address-fix author))))))

Theorem: booleanp-of-prop-set-none-author-p

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

Theorem: prop-set-none-author-p-of-address-fix-author

(defthm prop-set-none-author-p-of-address-fix-author
  (equal (prop-set-none-author-p (address-fix author)
                                 props)
         (prop-set-none-author-p author props)))

Theorem: prop-set-none-author-p-address-equiv-congruence-on-author

(defthm prop-set-none-author-p-address-equiv-congruence-on-author
  (implies (address-equiv author author-equiv)
           (equal (prop-set-none-author-p author props)
                  (prop-set-none-author-p author-equiv props)))
  :rule-classes :congruence)

Theorem: prop-set-none-author-p-of-proposal-set-fix-props

(defthm prop-set-none-author-p-of-proposal-set-fix-props
  (equal (prop-set-none-author-p author (proposal-set-fix props))
         (prop-set-none-author-p author props)))

Theorem: prop-set-none-author-p-proposal-set-equiv-congruence-on-props

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