diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2021-08-14 11:39:40 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2021-08-14 11:39:40 +0900 |
| commit | 4ada0d21de63a954c17d0b9ee4002be7fb7e22ab (patch) | |
| tree | 32e33de39d8e71950397ef1ef59e6e338e8d73de /pigeonhole.lisp | |
| parent | 58930a5cb5e011da1ef50a793b48e2ec4856491f (diff) | |
pigeonhole: Remove warnings.
Diffstat (limited to 'pigeonhole.lisp')
| -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))))) |