From ce65b8aea1fafda8ce5fd2eff1150db3e919de53 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Fri, 13 Aug 2021 17:11:51 +0900 Subject: pigenhole: Remove sum-map-count/list-induction. --- pigenhole.lisp | 9 ++------- 1 file 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) -- cgit v1.2.3