diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2021-08-13 17:11:51 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2021-08-13 17:11:51 +0900 |
| commit | ce65b8aea1fafda8ce5fd2eff1150db3e919de53 (patch) | |
| tree | 1b7a17cadf798934442622e4d846f0373125fbe0 /pigenhole.lisp | |
| parent | b420ce87ceae55123e1780a7eddec7eea5388ab7 (diff) | |
pigenhole: Remove sum-map-count/list-induction.
Diffstat (limited to 'pigenhole.lisp')
| -rw-r--r-- | pigenhole.lisp | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/pigenhole.lisp b/pigenhole.lisp index 0536656..c2fb779 100644 --- a/pigenhole.lisp +++ b/pigenhole.lisp @@ -37,11 +37,6 @@ (equal (len (map-count/list x s)) (len s))) -(defun sum-map-count/list-induction (x s) - (if (endp s) - x - (sum-map-count/list-induction (remove (car s) x) (cdr s)))) - (defthm len-remove (equal (len (remove e x)) (- (len x) (count/list e x)))) @@ -55,7 +50,7 @@ (subsetp x s)) (equal (sum (map-count/list x s)) (len x))) - :hints (("Goal" :induct (sum-map-count/list-induction x s)))) + :hints (("Goal" :induct (map-count/list x s)))) (defthm not-no-duplicatesp-count/list (implies (< 1 (count/list e x)) @@ -70,7 +65,7 @@ (subsetp x s) (member-if-over-1 (map-count/list x s))) (not (no-duplicatesp x))) - :hints (("Goal" :induct (sum-map-count/list-induction x s)))) + :hints (("Goal" :induct (map-count/list x s)))) (defthm pigeonhole-for-list (implies (and (no-duplicatesp s) |