blob: 18679233111bbdd85f2b6eaeb5000350e18cff8a (
plain)
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
|
(defun cons-all (e x)
(declare (xargs :guard (true-listp x)))
(if (endp x)
nil
(cons (cons e (car x))
(cons-all e (cdr x)))))
(defun combinations (x n)
(declare (xargs :guard (and (true-listp x)
(natp n))))
(cond
((zp n) (list nil))
((endp x) nil)
(t
(append (cons-all (car x)
(combinations (cdr x) (- n 1)))
(combinations (cdr x) n)))))
(defun comb (n k)
(cond
((zp k) 1)
((zp n) 0)
(t (+ (comb (- n 1) k)
(comb (- n 1) (- k 1))))))
(defthm len-combinations
(equal (len (combinations x n))
(comb (len x) n)))
|
