File: lop1.lisp

package info (click to toggle)
acl2 6.5-2
  • links: PTS
  • area: main
  • in suites: jessie, jessie-kfreebsd
  • size: 108,856 kB
  • ctags: 110,136
  • sloc: lisp: 1,492,565; xml: 7,958; perl: 3,682; sh: 2,103; cpp: 1,477; makefile: 1,470; ruby: 453; ansic: 358; csh: 125; java: 24; haskell: 17
file content (47 lines) | stat: -rw-r--r-- 1,140 bytes parent folder | download | duplicates (12) 
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
 
(in-package "ACL2")

(local (include-book "lop1-proofs"))
(include-book "merge") ;BOZO drop

(defund C (k a b)
  (- (bitn a k) (bitn b k)))

(defund PHI (a b d k)
  (if (and (integerp k) (>= k 0))
      (if (= k 0)
	  0
	(if (= d 0)
	    (phi a b (c (1- k) a b) (1- k))
	  (if (= d (- (c (1- k) a b)))
	      (phi a b (- (c (1- k) a b)) (1- k))
	    k)))
    0))

(defthm PHI-MOD
  (implies (and (integerp a)
                (>= a 0)
                (integerp b)
                (>= b 0)
                (integerp d)
                (integerp j)
                (>= j 0)
                (integerp k)
                (>= k j))
           (= (phi a b d j)
              (phi (mod a (expt 2 k)) (mod b (expt 2 k)) d j)))
  :rule-classes ())

(defthm LOP-THM-0
  (implies (and (integerp a)
                (integerp b)
                (integerp n)
                (>= a 0)
                (>= b 0)
                (>= n 0)
                (not (= a b))
                (< a (expt 2 n))
                (< b (expt 2 n)))
           (or (= (phi a b 0 n) (expo (- a b)))
               (= (phi a b 0 n) (1+ (expo (- a b))))))
  :rule-classes ())