blob: 8c62e9d9da0cab31184ab75c56d91f1c9cd25b1e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
(in-package "ACL2")
(defun remove-nth (i x)
(declare (xargs :guard (and (natp i)
(true-listp x))))
(cond ((endp x) nil)
((zp i) (cdr x))
(t
(cons (car x)
(remove-nth (1- i) (cdr x))))))
(defthm len-remove-nth
(implies (and (consp x)
(< i (len x)))
(equal (len (remove-nth i x))
(- (len x) 1))))
(defthm true-listp-remove-nth
(implies (true-listp x)
(true-listp (remove-nth i x))))
|
