~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/rtl/rel6/support/support/lop1.lisp

• browse files at revision 7
• compare with another revision
• download diff
• download tarball
• view history from revision 7

Show diffs side-by-side

added

removed

books/rtl/rel6/support/support/lop1.lisp

 

1

(in-package "ACL2")

 

2

 

 

3

(local (include-book "lop1-proofs"))

 

4

(include-book "merge") ;BOZO drop

 

5

 

 

6

(defund lop (a b d k)

 

7

  (let ((c (- (bitn a (1- k)) (bitn b (1- k)))))

 

8

    (if (and (integerp k) (>= k 0))

 

9

        (if (= k 0)

 

10

            0

 

11

          (if (= d 0)

 

12

              (lop a b c (1- k))

 

13

            (if (= d (- c))

 

14

                (lop a b (- c) (1- k))

 

15

              k)))

 

16

      0)))

 

17

 

 

18

(defthm LOP-MOD

 

19

  (implies (and (integerp a)

 

20

                (>= a 0)

 

21

                (integerp b)

 

22

                (>= b 0)

 

23

                (integerp d)

 

24

                (integerp j)

 

25

                (>= j 0)

 

26

                (integerp k)

 

27

                (>= k j))

 

28

           (= (lop a b d j)

 

29

              (lop (mod a (expt 2 k)) (mod b (expt 2 k)) d j)))

 

30

  :rule-classes ())

 

31

 

 

32

(defthm LOP-BNDS

 

33

  (implies (and (integerp a)

 

34

                (integerp b)

 

35

                (integerp n)

 

36

                (>= a 0)

 

37

                (>= b 0)

 

38

                (>= n 0)

 

39

                (not (= a b))

 

40

                (< a (expt 2 n))

 

41

                (< b (expt 2 n)))

 

42

           (or (= (lop a b 0 n) (expo (- a b)))

 

43

               (= (lop a b 0 n) (1+ (expo (- a b))))))

 

44

  :rule-classes ())

 

45

 

• Older »

Loggerhead is a web-based interface for Breezy
Version: 2.0.1