L-99: Solve P20 problem.

1 files changed, 20 insertions, 0 deletions

diff --git a/L-99.lisp b/L-99.lisp
index ff9e1c6..820e741 100644
--- a/L-99.lisp
+++ b/L-99.lisp
@@ -569,3 +569,23 @@
                 (natp n)
                 (< n (len x)))
            (subsetp x (rotate x n))))
+
+;; P20 (*) Remove the K'th element from a list.
+(defun remove-at (x n)
+  (cond
+    ((endp x) nil)
+    ((zp (1- n)) (cdr x))
+    (t (cons (car x)
+             (remove-at (cdr x) (1- n))))))
+
+(defthm len-remove-at
+  (implies (and (posp i)
+                (<= i (len x)))
+           (equal (len (remove-at x i))
+                  (- (len x) 1))))
+
+(defthm not-member-element-at-remove-at-implies-only-one
+  (implies (and (posp i)
+                (<= i (len x))
+                (not (member (element-at x i) (remove-at x i))))
+           (equal (count (element-at x i) x) 1)))