diff options
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) |