GCL (GNU Common Lisp)  2.6.6 CLtL1    Jan 19 2005 20:24:14
Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
Binary License:  GPL due to GPL'ed components: (BFD UNEXEC)
Modifications of this banner must retain notice of a compatible license
Dedicated to the memory of W. Schelter

Use (help) to get some basic information on how to use GCL.

 ACL2 Version 2.9.3 built August 2, 2005  18:40:53.
 Copyright (C) 2005  University of Texas at Austin
 ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and you
 are welcome to redistribute it under certain conditions.  For details,
 see the GNU General Public License.

 Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*
                      NIL).
 See the documentation topic note-2-9-3 for recent changes.
 Note: We have modified the prompt in some underlying Lisps to further
 distinguish it from the ACL2 prompt.

 NOTE!!  Proof trees are disabled in ACL2.  To enable them in emacs,
 look under the ACL2 source directory in interface/emacs/README.doc; 
 and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2 
 command loop.   Look in the ACL2 documentation under PROOF-TREE.

ACL2 Version 2.9.3.  Level 1.  Cbd 
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>
Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
ACL2>
#<"ACL2" package>

ACL2>
ACL2 Version 2.9.3.  Level 1.  Cbd 
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !> (PROVE PROOF-TREE WARNING OBSERVATION EVENT)
ACL2 !>
Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).

ACL2>
ACL2 Version 2.9.3.  Level 1.  Cbd 
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>
ACL2 Version 2.9.3.  Level 2.  Cbd 
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>>
Summary
Form:  ( DEFPKG "INSTANCE" ...)
Rules: NIL
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
 "INSTANCE"
ACL2 !>>
Summary
Form:  ( DEFPKG "COMPUTED-HINTS" ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 "COMPUTED-HINTS"
ACL2 !>>[SGC for 444 CONS pages..(8302 writable)..(T=1).GC finished]

Summary
Form:  ( DEFPKG "SETS" ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 "SETS"
ACL2 !>>Bye.
 :EOF
ACL2 !>[SGC for 12 STRING pages..(8304 writable)..(T=0).GC finished]
2
[SGC for 12 STRING pages..(8307 writable)..(T=0).GC finished]
[SGC for 444 CONS pages..(8307 writable)..(T=1).GC finished]
[SGC for 444 CONS pages..(8308 writable)..(T=1).GC finished]
[SGC for 20 CFUN pages..(8609 writable)..(T=1).GC finished]
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.o
start address -T 0x9e95000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.o
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.o
start address -T 0x89e1000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.o

Summary
Form:  ( INCLUDE-BOOK "computed-hints" ...)
Rules: NIL
Warnings:  None
Time:  0.15 seconds (prove: 0.00, print: 0.00, other: 0.15)
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.lisp"
[SGC for 20 CFUN pages..(8720 writable)..(T=1).GC finished]
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/primitives.o
start address -T 0x91e9a90 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/primitives.o

Summary
Form:  ( INCLUDE-BOOK "primitives" ...)
Rules: NIL
Warnings:  None
Time:  0.09 seconds (prove: 0.00, print: 0.00, other: 0.09)
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/primitives.lisp"
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/membership.o
start address -T 0x9b24000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/membership.o

Summary
Form:  ( INCLUDE-BOOK "membership" ...)
Rules: NIL
Warnings:  None
Time:  0.09 seconds (prove: 0.00, print: 0.00, other: 0.09)
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/membership.lisp"
[SGC for 25 FIXNUM pages..(10339 writable)..(T=2).GC finished]
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/fast.o
start address -T 0x89e2300 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/fast.o

Summary
Form:  ( INCLUDE-BOOK "fast" ...)
Rules: NIL
Warnings:  None
Time:  0.06 seconds (prove: 0.00, print: 0.00, other: 0.06)
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/fast.lisp"
[SGC for 25 FIXNUM pages..(10342 writable)..(T=1).GC finished]
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/outer.o
start address -T 0x91e9000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/outer.o

Summary
Form:  ( INCLUDE-BOOK "outer" ...)
Rules: NIL
Warnings:  None
Time:  0.10 seconds (prove: 0.00, print: 0.00, other: 0.10)
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/outer.lisp"
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/sort.o
start address -T 0x91e9750 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/sort.o

Summary
Form:  ( INCLUDE-BOOK "sort" ...)
Rules: NIL
Warnings:  None
Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/sort.lisp"

Summary
Form:  ( DEFUN << ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:DEFUND <<)

Summary
Form:  ( DEFUN SETP ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:DEFUND SETP)

Summary
Form:  ( DEFTHM SETP-TYPE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFUN EMPTY ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:DEFUND EMPTY)

Summary
Form:  ( DEFTHM EMPTY-TYPE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFUN SFIX ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:DEFUND SFIX)

Summary
Form:  ( DEFUN HEAD ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:DEFUND HEAD)

Summary
Form:  ( DEFUN TAIL ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:DEFUND TAIL)

Summary
Form:  ( DEFUN INSERT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:DEFUND INSERT)

Summary
Form:  ( DEFUN IN ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM IN-TYPE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFUN FAST-SUBSET ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:DEFUND FAST-SUBSET)

Summary
Form:  ( DEFUN SUBSET ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM SUBSET-TYPE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFUN FAST-MEASURE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:DEFUND FAST-MEASURE)

Summary
Form:  ( DEFUN FAST-UNION ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFUN FAST-INTERSECT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFUN FAST-DIFFERENCE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFUN DELETE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFUN UNION ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFUN INTERSECT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFUN DIFFERENCE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFUN CARDINALITY ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFUN SPLIT-LIST ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:DEFUND SPLIT-LIST)

Summary
Form:  ( DEFUN IN-LIST ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFUN MERGESORT-EXEC ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFUN MERGESORT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( ENCAPSULATE (((PREDICATE * ...) ...) ...) ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFUN ALL ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( ENCAPSULATE (((ALL-HYPS ...) ...) ...) ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM ALL-BY-MEMBERSHIP ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:DEFTHMD ALL-BY-MEMBERSHIP)

Summary
Form:  ( DEFUN SUBSET-TRIGGER ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:DEFUND SUBSET-TRIGGER)

Summary
Form:  ( DEFTHM PICK-A-POINT-SUBSET-STRATEGY ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( ENCAPSULATE NIL (DEFUN PICK-A-POINT-SUBSET-HINT ...) ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DOUBLE-CONTAINMENT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM SETS-ARE-TRUE-LISTS ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM TAIL-COUNT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM HEAD-COUNT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM TAIL-COUNT-BUILT-IN ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM HEAD-COUNT-BUILT-IN ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INSERT-INSERT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM SFIX-PRODUCES-SET ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM TAIL-PRODUCES-SET ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INSERT-PRODUCES-SET ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INSERT-NEVER-EMPTY ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM TAIL-PRESERVES-EMPTY ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM NONEMPTY-MEANS-SET ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM SFIX-SET-IDENTITY ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM EMPTY-SFIX-CANCEL ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM HEAD-SFIX-CANCEL ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM TAIL-SFIX-CANCEL ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INSERT-HEAD-TAIL ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM REPEATED-INSERT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INSERT-SFIX-CANCEL ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM HEAD-INSERT-EMPTY ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM TAIL-INSERT-EMPTY ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM NOT-IN-SELF ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM IN-SFIX-CANCEL ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM NEVER-IN-EMPTY ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM IN-SET ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM IN-TAIL ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM IN-TAIL-OR-HEAD ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM IN-HEAD ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM HEAD-UNIQUE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INSERT-IDENTITY ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM IN-INSERT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM SUBSET-TRANSITIVE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM SUBSET-INSERT-X ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM SUBSET-SFIX-CANCEL-X ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM SUBSET-SFIX-CANCEL-Y ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM SUBSET-IN ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM SUBSET-IN-2 ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM EMPTY-SUBSET ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM EMPTY-SUBSET-2 ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM SUBSET-REFLEXIVE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM SUBSET-INSERT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM SUBSET-TAIL ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM WEAK-INSERT-INDUCTION-HELPER-1 ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM WEAK-INSERT-INDUCTION-HELPER-2 ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM WEAK-INSERT-INDUCTION-HELPER-3 ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFUN WEAK-INSERT-INDUCTION ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM USE-WEAK-INSERT-INDUCTION ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DELETE-DELETE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DELETE-SET ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DELETE-PRESERVES-EMPTY ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DELETE-IN ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DELETE-SFIX-CANCEL ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DELETE-NONMEMBER-CANCEL ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM REPEATED-DELETE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DELETE-INSERT-CANCEL ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INSERT-DELETE-CANCEL ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM SUBSET-DELETE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM UNION-SYMMETRIC ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM UNION-COMMUTATIVE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM UNION-INSERT-X ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM UNION-INSERT-Y ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM UNION-DELETE-X ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM UNION-DELETE-Y ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM UNION-SET ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM UNION-SFIX-CANCEL-X ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM UNION-SFIX-CANCEL-Y ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM UNION-EMPTY-X ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM UNION-EMPTY-Y ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM UNION-EMPTY ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM UNION-IN ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM UNION-SUBSET-X ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM UNION-SUBSET-Y ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM UNION-SELF ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM UNION-ASSOCIATIVE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM UNION-OUTER-CANCEL ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-SYMMETRIC ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-INSERT-X ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-INSERT-Y ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-DELETE-X ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-DELETE-Y ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-SET ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-SFIX-CANCEL-X ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-SFIX-CANCEL-Y ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-EMPTY-X ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-EMPTY-Y ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-IN ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-SUBSET-X ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-SUBSET-Y ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-SELF ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-ASSOCIATIVE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM UNION-OVER-INTERSECT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:DEFTHMD UNION-OVER-INTERSECT)

Summary
Form:  ( DEFTHM INTERSECT-OVER-UNION ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-COMMUTATIVE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-OUTER-CANCEL ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DIFFERENCE-SET ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DIFFERENCE-SFIX-X ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DIFFERENCE-SFIX-Y ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DIFFERENCE-EMPTY-X ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DIFFERENCE-EMPTY-Y ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DIFFERENCE-IN ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DIFFERENCE-SUBSET-X ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM SUBSET-DIFFERENCE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DIFFERENCE-OVER-UNION ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DIFFERENCE-OVER-INTERSECT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DIFFERENCE-INSERT-X ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DIFFERENCE-INSERT-Y ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DIFFERENCE-DELETE-X ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DIFFERENCE-DELETE-Y ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DIFFERENCE-PRESERVES-SUBSET ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM CARDINALITY-TYPE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM CARDINALITY-ZERO-EMPTY ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM CARDINALITY-SFIX-CANCEL ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INSERT-CARDINALITY ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM DELETE-CARDINALITY ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM SUBSET-CARDINALITY ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM EQUAL-CARDINALITY-SUBSET-IS-EQUALITY ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
[SGC for 2996 CONS pages..(11722 writable)..(T=2).GC finished]
(:DEFTHMD EQUAL-CARDINALITY-SUBSET-IS-EQUALITY)

Summary
Form:  ( DEFTHM INTERSECT-CARDINALITY-X ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-CARDINALITY-Y ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM EXPAND-CARDINALITY-OF-UNION ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM EXPAND-CARDINALITY-OF-DIFFERENCE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-CARDINALITY-SUBSET ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-CARDINALITY-NON-SUBSET ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-CARDINALITY-SUBSET-2 ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM INTERSECT-CARDINALITY-NON-SUBSET-2 ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM IN-LIST-CONS ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM IN-LIST-APPEND ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM IN-LIST-REVAPPEND ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM IN-LIST-REVERSE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM IN-LIST-ON-SET ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM MERGESORT-SET ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM IN-MERGESORT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( DEFTHM MERGESORT-SET-IDENTITY ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT

Summary
Form:  ( TABLE ACL2::ACL2-DEFAULTS-TABLE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ACL2::ACL2-DEFAULTS-TABLE
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.o
start address -T 0x9ea5000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.o
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.o
start address -T 0x9ea7160 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.o

Summary
Form:  ( INCLUDE-BOOK "sets" ...)
Rules: NIL
Warnings:  None
Time:  0.29 seconds (prove: 0.00, print: 0.00, other: 0.29)
Compiling /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/sets.lisp.
[SGC for 12 SYMBOL pages..(12778 writable)..(T=3).GC finished]
End of Pass 1.  

;; Note: Tail-recursive call of SETP was replaced by iteration.
;; Note: Tail-recursive call of IN was replaced by iteration.
;; Note: Tail-recursive call of FAST-SUBSET was replaced by iteration.
;; Note: Tail-recursive call of FAST-SUBSET was replaced by iteration.
;; Note: Tail-recursive call of FAST-UNION was replaced by iteration.
;; Note: Tail-recursive call of FAST-UNION was replaced by iteration.
;; Note: Tail-recursive call of FAST-UNION was replaced by iteration.
;; Note: Tail-recursive call of FAST-INTERSECT was replaced by iteration.
;; Note: Tail-recursive call of FAST-INTERSECT was replaced by iteration.
;; Note: Tail-recursive call of FAST-INTERSECT was replaced by iteration.
;; Note: Tail-recursive call of FAST-DIFFERENCE was replaced by iteration.
;; Note: Tail-recursive call of FAST-DIFFERENCE was replaced by iteration.
;; Note: Tail-recursive call of FAST-DIFFERENCE was replaced by iteration.
;; Note: Tail-recursive call of SPLIT-LIST was replaced by iteration.
;; Note: Tail-recursive call of IN-LIST was replaced by iteration.
;; Note: Tail-recursive call of ALL was replaced by iteration.
End of Pass 2.  
OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
Finished compiling /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/sets.o.

"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/sets.o" 

Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/sets.o
start address -T 0x9665000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/sets.o

Summary
Form:  (CERTIFY-BOOK "sets" ...)
Rules: NIL
Warnings:  None
Time:  0.36 seconds (prove: 0.00, print: 0.00, other: 0.36)
 "/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/sets.lisp"
ACL2 !>
Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).

ACL2>