pigeonhole: Rename pigenhole from to pigeonhole.

1 files changed, 0 insertions, 74 deletions

diff --git a/pigenhole.lisp b/pigenhole.lisp
deleted file mode 100644
index c2fb779..0000000
--- a/pigenhole.lisp
+++ /dev/null
@@ -1,74 +0,0 @@
-(defun member-if-over-1 (x)
-  (cond ((endp x) nil)
-        ((< 1 (car x)) x)
-        (t (member-if-over-1 (cdr x)))))
-
-(defun sum (x)
-  (if (endp x)
-      0
-      (+ (car x)
-         (sum (cdr x)))))
-
-(defthm pigeonhole
-  (implies (< (len x) (sum x))
-           (member-if-over-1 x)))
-
-(defun count/list (e x)
-  (cond ((endp x) 0)
-        ((equal e (car x)) (1+ (count/list e (cdr x))))
-        (t (count/list e (cdr x)))))
-
-(defthm member-remove
-  (implies (not (equal x y))
-           (iff (member x (remove y z))
-                (member x z))))
-
-(defthm no-duplicatesp-remove
-  (implies (no-duplicatesp x)
-           (no-duplicatesp (remove e x))))
-
-(defun map-count/list (x s)
-  (if (endp s)
-      nil
-      (cons (count/list (car s) x)
-            (map-count/list (remove (car s) x) (cdr s)))))
-
-(defthm len-map-count/list
-  (equal (len (map-count/list x s))
-         (len s)))
-
-(defthm len-remove
-  (equal (len (remove e x))
-         (- (len x) (count/list e x))))
-
-(defthm not-subsetp-remove
-  (implies (not (subsetp (remove e x) y))
-           (not (subsetp x (cons e y)))))
-
-(defthm sum-map-count/list
-  (implies (and (no-duplicatesp s)
-                (subsetp x s))
-           (equal (sum (map-count/list x s))
-                  (len x)))
-  :hints (("Goal" :induct (map-count/list x s))))
-
-(defthm not-no-duplicatesp-count/list
-  (implies (< 1 (count/list e x))
-           (not (no-duplicatesp x))))
-
-(defthm not-no-duplicatesp-remove
-  (implies (not (no-duplicatesp (remove e x)))
-           (not (no-duplicatesp x))))
-
-(defthm member-if-over-1-map-count/list-is-duplicated
-  (implies (and (no-duplicatesp s)
-                (subsetp x s)
-                (member-if-over-1 (map-count/list x s)))
-           (not (no-duplicatesp x)))
-  :hints (("Goal" :induct (map-count/list x s))))
-
-(defthm pigeonhole-for-list
-  (implies (and (no-duplicatesp s)
-                (subsetp x s)
-                (< (len s) (len x)))
-           (not (no-duplicatesp x))))