Lines Matching defs:member
475 (defthm boolean-p-create-non-member-reduction
485 (defthm create-all-evaluations-for-member-is-boolean
589 ;; Now let us prove that for every member of find-matching-states it is
593 (defthm nth-member-reduction
600 (defthm nth-member-reduction-2
609 (defthm assign-nil-produces-nil-member
615 (defthm assign-t-produces-t-member
630 :in-theory (disable nth-member-reduction)
631 :use ((:instance nth-member-reduction
662 :in-theory (disable nth-member-reduction)
663 :use ((:instance nth-member-reduction
730 (defthm falsifier-not-member-to-evaluation-eq
777 (defthm member-assign-t-reduction
791 (defthm member-assign-nil-reduction
823 (defthm car-of-find-matching-is-member-of-all-evaluations
833 (evaluation-eq-member-p p states vars)))
840 (evaluation-eq-member-p q states vars))
842 :in-theory (disable evaluation-eq evaluation-eq-member-p
858 (evaluation-eq-member-p st (create-all-evaluations vars states)
881 (defthm append-evaluation-eq-member-reduction
882 (implies (evaluation-eq-member-p st states vars)
883 (evaluation-eq-member-p st (set-union init states) vars)))