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
69
70
71
72
73
|
(in-package "ACL2")
;Necessary definitions:
(defund fl (x)
(declare (xargs :guard (real/rationalp x)))
(floor x 1))
(local (include-book "fl")) ; yuck?
(defun or-dist-induct (y n)
(if (and (integerp n) (>= n 0))
(if (= n 0)
y
(or-dist-induct (fl (/ y 2)) (1- n)))
()))
(defun log-induct (i j)
(if (and (integerp i) (>= i 0)
(integerp j) (>= j 0))
(if (or (= i 0) (= j 0))
()
(log-induct (fl (/ i 2)) (fl (/ j 2))))
()))
(DEFUN logand-three-args-induct (I J K)
(declare (xargs :measure (ACL2-COUNT (abs i))
:hints (("Goal" :in-theory (enable abs)))))
(IF (AND (INTEGERP I)
(INTEGERP J)
(INTEGERP K)
)
(IF (OR (= I 0) (= J 0) (= K 0)
(= I -1) (= J -1) (= K -1))
NIL
(logand-three-args-induct
(FL (/ I 2))
(FL (/ J 2))
(FL (/ K 2))))
NIL))
(DEFUN LOG-INDUCT-allows-negatives (i j)
(IF (AND (INTEGERP i)
(INTEGERP j)
)
(IF (OR (= i 0) (= j 0) (= i -1) (= j -1))
NIL
(LOG-INDUCT-allows-negatives (FL (/ i 2)) (FL (/ j 2))))
NIL))
(defun op-dist-induct (i j n)
(if (and (integerp n) (>= n 0))
(if (= n 0)
(list i j)
(op-dist-induct (fl (/ i 2)) (fl (/ j 2)) (1- n)))
()))
#|
(defun op-dist-induct-negative (i j n)
(if (and (integerp n) (<= n 0))
(if (= n 0)
(list i j)
(op-dist-induct-negative (fl (/ i 2)) (fl (/ j 2)) (1+ n)))
()))
|#
;move?
(defun natp-induct (k)
(if (zp k)
t
(natp-induct (1- k))))
|
