From 5ff4399cdea98a6805568db18581ef176f2aa816 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Sun, 1 Aug 2021 01:14:47 +0900 Subject: L-99: Solve P20 problem. --- L-99.lisp | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) 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))) -- cgit v1.2.3