L-99: Fix P16 problem.

1 files changed, 21 insertions, 27 deletions

diff --git a/L-99.lisp b/L-99.lisp
index 820e741..3c8dc71 100644
--- a/L-99.lisp
+++ b/L-99.lisp
@@ -431,37 +431,18 @@
                   (* n (len x)))))
 
 ;; P16 (**) Drop every N'th element from a list.
-(defun drop (x n)
+(defun drop-1 (x n i)
   (cond
     ((endp x) nil)
-    ((zp (1- n)) (cdr x))
+    ((zp (- i 1))
+     (drop-1 (cdr x) n n))
     (t (cons (car x)
-             (drop (cdr x) (1- n))))))
-
-(defthm len-drop
-  (implies (and (posp i)
-                (<= i (len x)))
-           (equal (len (drop x i))
-                  (- (len x) 1))))
-
-(defun count/list (e x)
-  (cond ((endp x) 0)
-        ((equal (car x) e) (+ 1 (count/list e (cdr x))))
-        (t (count/list e (cdr x)))))
-
-(defthm count-to-count/list
- (implies (consp x)
-          (equal (count e x) (count/list e x))))
-
-(defthm posp-len-implies-consp
-  (implies (posp (len x))
-           (consp x)))
+             (drop-1 (cdr x)
+                     n
+                     (1- i))))))
 
-(defthm not-member-element-at-drop-implies-only-one
-  (implies (and (posp i)
-                (<= i (len x))
-                (not (member (element-at x i) (drop x i))))
-           (equal (count (element-at x i) x) 1)))
+(defmacro drop (x n)
+  `(drop-1 ,x ,n ,n))
 
 ;; P17 (*) Split a list into two parts; the length of the first part is given.
 (defun split-1 (x n acc)
@@ -578,6 +559,19 @@
     (t (cons (car x)
              (remove-at (cdr x) (1- n))))))
 
+(defun count/list (e x)
+  (cond ((endp x) 0)
+        ((equal (car x) e) (+ 1 (count/list e (cdr x))))
+        (t (count/list e (cdr x)))))
+
+(defthm count-to-count/list
+ (implies (consp x)
+          (equal (count e x) (count/list e x))))
+
+(defthm posp-len-implies-consp
+  (implies (posp (len x))
+           (consp x)))
+
 (defthm len-remove-at
   (implies (and (posp i)
                 (<= i (len x)))