diff options
| -rw-r--r-- | pigeonhole.lisp | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/pigeonhole.lisp b/pigeonhole.lisp index bda4cfc..4be756b 100644 --- a/pigeonhole.lisp +++ b/pigeonhole.lisp @@ -54,24 +54,28 @@ (defthm not-no-duplicatesp-list-count (implies (< 1 (list-count e x)) - (not (no-duplicatesp x)))) + (not (no-duplicatesp x))) + :rule-classes ((:rewrite :match-free :all))) (defthm not-no-duplicatesp-remove (implies (not (no-duplicatesp (remove e x))) - (not (no-duplicatesp x)))) + (not (no-duplicatesp x))) + :rule-classes ((:rewrite :match-free :all))) (defthm member-if-over-1-map-list-count-is-duplicated (implies (and (no-duplicatesp s) (subsetp x s) (member-if-over-1 (map-list-count x s))) (not (no-duplicatesp x))) - :hints (("Goal" :induct (map-list-count x s)))) + :hints (("Goal" :induct (map-list-count x s))) + :rule-classes ((:rewrite :match-free :all))) (defthm pigeonhole-for-list (implies (and (no-duplicatesp s) (subsetp x s) (< (len s) (len x))) - (not (no-duplicatesp x)))) + (not (no-duplicatesp x))) + :rule-classes ((:rewrite :match-free :all))) (in-theory (disable pigeonhole-for-list)) (defthm blood-types-are-duplicates @@ -126,11 +130,13 @@ (no-duplicatesp (nats-below n))) (defthm duplicates-nats - (implies (and (posp n) + (implies (and (integerp n) + (<= 0 n) (subsetp x (nats-below n)) (< n m) (<= m (len x))) (not (no-duplicatesp x))) + :rule-classes ((:rewrite :match-free :all)) :hints (("Goal" :use (:instance pigeonhole-for-list (s (nats-below n)) (x x))))) |