aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMasaya Tojo <masaya@tojo.tokyo>2021-08-13 23:33:52 +0900
committerMasaya Tojo <masaya@tojo.tokyo>2021-08-13 23:33:52 +0900
commitd1cf027f4247f01a3d4781ec7f751c67da96e923 (patch)
treefa0d20276e6f01b0ce49e3ed357ec084a6db974a
parent22e1d6c1abc5c7c825364658deab9969190586a6 (diff)
pigeonhole: Rename from count/list to list-count.
-rw-r--r--pigeonhole.lisp34
1 files 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)