← Back to branch summary

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

« back to all changes in this revision

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

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/rtl/rel6/support/support/lextra0.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(include-book "land0")
 
4
(include-book "lior0")
 
5
(include-book "lxor0")
 
6
(local (include-book "lextra-proofs"))
 
7
 
 
8
;theorems mixing two or more of the new logical operators.
 
9
 
 
10
;BOZO really the -1 and -2 names below should be switched?
 
11
 
 
12
(deflabel lextra0-start)
 
13
 
 
14
(defthm lior0-land0-1
 
15
  (equal (lior0 x (land0 y z n) n)
 
16
         (land0 (lior0 x y n) (lior0 x z n) n)))
 
17
 
 
18
(defthm lior0-land0-2
 
19
  (equal (lior0 (land0 y z n) x n)
 
20
         (land0 (lior0 x y n) (lior0 x z n) n)))
 
21
 
 
22
(defthm land0-lior0-1
 
23
  (equal (land0 x (lior0 y z n) n)
 
24
         (lior0 (land0 x y n) (land0 x z n) n)))
 
25
 
 
26
(defthm land0-lior0-2
 
27
  (equal (land0 (lior0 y z n) x n)
 
28
         (lior0 (land0 x y n) (land0 x z n) n)))
 
29
 
 
30
(defthm lior0-land0-lxor0
 
31
  (equal (lior0 (land0 x y n) (lior0 (land0 x z n) (land0 y z n) n) n)
 
32
         (lior0 (land0 x y n) (land0 (lxor0 x y n) z n) n)))
 
33
 
 
34
(defthm lxor0-rewrite
 
35
  (equal (lxor0 x y n)
 
36
         (lior0 (land0 x (lnot y n) n)
 
37
               (land0 y (lnot x n) n)
 
38
               n)))
 
39
 
 
40
(defthm lnot-lxor0
 
41
  (equal (lnot (lxor0 x y n) n)
 
42
         (lxor0 (lnot x n) y n)))
 
43
 
 
44
(defthm lnot-lior0
 
45
  (equal (lnot (lior0 x y n) n)
 
46
         (land0 (lnot x n) (lnot y n) n)))
 
47
 
 
48
(defthm lnot-land0
 
49
  (equal (lnot (land0 x y n) n)
 
50
         (lior0 (lnot x n) (lnot y n) n)))
 
51
 
 
52
(deflabel lextra0-end)
 
53
 
 
54
(in-theory (current-theory 'lextra0-start))