1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
(in-package "ACL2")
(defthm len-nthcdr-le-len-lst--thm
(<= (len (nthcdr x lst)) (len lst)))
(defthm nthcdr-of-len-lst--thm
(implies (and (true-listp lst) (natp xx) (>= xx (len lst)))
(= (nthcdr xx lst) nil)))
(local (include-book "arithmetic/top-with-meta" :dir :system))
(defthm nthcdr-cdr--thm
(implies (and (integerp xx) (>= xx 0) (true-listp lst))
(= (nthcdr xx (cdr lst)) (nthcdr (1+ xx) lst))))
(defthm cdr-nthcdr--thm
(implies (and (integerp xx) (>= xx 0) (true-listp lst))
(= (cdr (nthcdr xx lst)) (nthcdr (1+ xx) lst))))
(defthmd cdr-nthcdr-minus-1--thm
(implies (and (integerp xx) (> xx 0) (true-listp lst))
(= (nthcdr xx lst) (cdr (nthcdr (1- xx) lst)) )))
(defthm nthcdr-len-minus-2--thm
(implies (and (true-listp lst) (> (len lst) 1))
(= (nthcdr (- (len lst) 2) lst)
(list (nth (- (len lst) 2) lst)
(nth (- (len lst) 1) lst)))))
(defthm nthcdr-member-nth--thm
(implies (and (true-listp lst) (natp xx) (< xx (len lst)))
(member-equal (nth xx lst) (nthcdr xx lst))))
(defthm nthcdr-member-nth-1--thm
(implies (and (true-listp lst) (natp xx)
(< (1+ xx) (len lst)))
(member-equal (nth (1+ xx) lst) (nthcdr xx lst))))
(defthm nthcdr-len-minus-1--thm
(implies (and (consp x) (true-listp x))
(= (nthcdr (1- (len x)) x)
(list (nth (1- (len x)) x)))))
(defthm nthcdr-preserves-true-listp--thm
(implies (and (true-listp lst) (natp x))
(true-listp (nthcdr x lst))))
(defthm nthcdr-ge-len-nil--thm
(implies (and (true-listp x) (natp q) (>= q (len x)))
(= (nthcdr q x) nil)))
(defthm nthcdr-lt-len-not-nil--thm
(implies (and (true-listp x) (not (endp x)) (natp q) (< q (len x)))
(not (= (nthcdr q x) nil))))
(defthm len-nthcdr-minus-1-gt-len-nthcdr--thm
(implies (and (true-listp x) (not (endp x)) (natp q) (> q 0) (< q (len x)))
(> (len (nthcdr (1- q) x)) (len (nthcdr q x)))))
(defthm nth-ge-len-nil--thm
(implies (and (true-listp x) (natp q) (>= q (len x)))
(= (nth q x) nil)))
(defthm nthcdr-update-nth--thm
(implies (and (true-listp lst) (natp ix) (< ix (len lst))
(natp iy) (< ix iy))
(= (nthcdr iy (update-nth ix z lst))
(nthcdr iy lst))))
|
