From d1cf027f4247f01a3d4781ec7f751c67da96e923 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Fri, 13 Aug 2021 23:33:52 +0900
Subject: pigeonhole: Rename from count/list to list-count.

---
 pigeonhole.lisp | 34 +++++++++++++++++-----------------
 1 file changed, 17 insertions(+), 17 deletions(-)

diff --git a/pigeonhole.lisp b/pigeonhole.lisp
index c2fb779..69fe8ab 100644
--- a/pigeonhole.lisp
+++ b/pigeonhole.lisp
@@ -13,10 +13,10 @@
   (implies (< (len x) (sum x))
            (member-if-over-1 x)))
 
-(defun count/list (e x)
+(defun list-count (e x)
   (cond ((endp x) 0)
-        ((equal e (car x)) (1+ (count/list e (cdr x))))
-        (t (count/list e (cdr x)))))
+        ((equal e (car x)) (1+ (list-count e (cdr x))))
+        (t (list-count e (cdr x)))))
 
 (defthm member-remove
   (implies (not (equal x y))
@@ -27,45 +27,45 @@
   (implies (no-duplicatesp x)
            (no-duplicatesp (remove e x))))
 
-(defun map-count/list (x s)
+(defun map-list-count (x s)
   (if (endp s)
       nil
-      (cons (count/list (car s) x)
-            (map-count/list (remove (car s) x) (cdr s)))))
+      (cons (list-count (car s) x)
+            (map-list-count (remove (car s) x) (cdr s)))))
 
-(defthm len-map-count/list
-  (equal (len (map-count/list x s))
+(defthm len-map-list-count
+  (equal (len (map-list-count x s))
          (len s)))
 
 (defthm len-remove
   (equal (len (remove e x))
-         (- (len x) (count/list e x))))
+         (- (len x) (list-count e x))))
 
 (defthm not-subsetp-remove
   (implies (not (subsetp (remove e x) y))
            (not (subsetp x (cons e y)))))
 
-(defthm sum-map-count/list
+(defthm sum-map-list-count
   (implies (and (no-duplicatesp s)
                 (subsetp x s))
-           (equal (sum (map-count/list x s))
+           (equal (sum (map-list-count x s))
                   (len x)))
-  :hints (("Goal" :induct (map-count/list x s))))
+  :hints (("Goal" :induct (map-list-count x s))))
 
-(defthm not-no-duplicatesp-count/list
-  (implies (< 1 (count/list e x))
+(defthm not-no-duplicatesp-list-count
+  (implies (< 1 (list-count 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
+(defthm member-if-over-1-map-list-count-is-duplicated
   (implies (and (no-duplicatesp s)
                 (subsetp x s)
-                (member-if-over-1 (map-count/list x s)))
+                (member-if-over-1 (map-list-count x s)))
            (not (no-duplicatesp x)))
-  :hints (("Goal" :induct (map-count/list x s))))
+  :hints (("Goal" :induct (map-list-count x s))))
 
 (defthm pigeonhole-for-list
   (implies (and (no-duplicatesp s)
-- 
cgit v1.2.3