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.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 "INSTANCE"
ACL2 !>>
Summary
Form:  ( DEFPKG "COMPUTED-HINTS" ...)
Rules: NIL
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
 "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 444 CONS pages..(8306 writable)..(T=1).GC finished]
[SGC for 1281 CONS pages..(9143 writable)..(T=1).GC finished]
[SGC for 12 STRING pages..(9145 writable)..(T=1).GC finished]
[SGC for 12 STRING pages..(9145 writable)..(T=1).GC finished]
[SGC for 20 CFUN pages..(9178 writable)..(T=1).GC finished]
[SGC for 20 CFUN pages..(9183 writable)..(T=0).GC finished]

Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/primitives.o
start address -T 0x91e9000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/primitives.o
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
[SGC for 25 FIXNUM pages..(10269 writable)..(T=2).GC finished]
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/membership.o
start address -T 0x93f4000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/membership.o
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
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/outer.o
start address -T 0x89e2b80 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/outer.o

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

Summary
Form:  ( DEFUN IN-LIST ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
IN-LIST

Summary
Form:  ( DEFTHM IN-LIST-CONS ...)
Rules: ((:DEFINITION IN-LIST)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
IN-LIST-CONS

Summary
Form:  ( DEFTHM IN-LIST-APPEND ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION IN-LIST)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION BINARY-APPEND)
        (:INDUCTION IN-LIST)
        (:REWRITE IN-LIST-CONS)
        (:TYPE-PRESCRIPTION IN-LIST))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
IN-LIST-APPEND

Summary
Form:  ( DEFTHM LEMMA ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REVAPPEND)
        (:INDUCTION REVAPPEND)
        (:REWRITE IN-LIST-CONS)
        (:TYPE-PRESCRIPTION IN-LIST))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LEMMA

Summary
Form:  ( DEFTHM IN-LIST-REVAPPEND ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION IN-LIST)
        (:DEFINITION NOT)
        (:DEFINITION REVAPPEND)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION IN-LIST)
        (:INDUCTION REVAPPEND)
        (:REWRITE IN-LIST-CONS)
        (:REWRITE LEMMA)
        (:TYPE-PRESCRIPTION IN-LIST))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
IN-LIST-REVAPPEND

Summary
Form:  ( ENCAPSULATE NIL (LOCAL ...) ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
T

Summary
Form:  ( DEFTHM IN-LIST-REVERSE ...)
Rules: ((:DEFINITION IN-LIST)
        (:DEFINITION REVERSE)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE IN-LIST-REVAPPEND)
        (:TYPE-PRESCRIPTION IN-LIST))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
IN-LIST-REVERSE
[SGC for 25 FIXNUM pages..(10304 writable)..(T=2).GC finished]

Summary
Form:  ( DEFTHM IN-LIST-ON-SET ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION HEAD)
        (:DEFINITION IN)
        (:DEFINITION IN-LIST)
        (:DEFINITION NOT)
        (:DEFINITION SETP)
        (:DEFINITION TAIL)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART SETP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION IN)
        (:REWRITE NEVER-IN-EMPTY)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.07 seconds (prove: 0.06, print: 0.00, other: 0.01)
IN-LIST-ON-SET

Summary
Form:  ( DEFUN SPLIT-LIST-OLD ...)
Rules: ((:DEFINITION ACL2-COUNT)
        (:DEFINITION ENDP)
        (:DEFINITION O-FINP)
        (:DEFINITION O<)
        (:ELIM CAR-CDR-ELIM)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION ACL2-COUNT)
        (:TYPE-PRESCRIPTION SPLIT-LIST-OLD))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
SPLIT-LIST-OLD

Summary
Form:  ( DEFTHM SPLIT-LIST-OLD-MEMBERSHIP ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION IN-LIST)
        (:DEFINITION MV-NTH)
        (:DEFINITION NOT)
        (:DEFINITION SPLIT-LIST-OLD)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART MV-NTH)
        (:EXECUTABLE-COUNTERPART SETP)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SPLIT-LIST-OLD)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE IN-LIST-CONS)
        (:REWRITE IN-LIST-ON-SET)
        (:REWRITE NEVER-IN-EMPTY)
        (:TYPE-PRESCRIPTION IN-LIST)
        (:TYPE-PRESCRIPTION SPLIT-LIST-OLD))
Warnings:  None
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
SPLIT-LIST-OLD-MEMBERSHIP

Summary
Form:  ( DEFTHM SPLIT-LIST-OLD-PART1-TRUELIST ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION MV-NTH)
        (:DEFINITION NOT)
        (:DEFINITION SPLIT-LIST-OLD)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART TRUE-LISTP)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SPLIT-LIST-OLD)
        (:REWRITE CAR-CONS)
        (:TYPE-PRESCRIPTION SPLIT-LIST-OLD))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SPLIT-LIST-OLD-PART1-TRUELIST

Summary
Form:  ( DEFTHM SPLIT-LIST-OLD-PART2-TRUELIST ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION MV-NTH)
        (:DEFINITION NOT)
        (:DEFINITION SPLIT-LIST-OLD)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART MV-NTH)
        (:EXECUTABLE-COUNTERPART TRUE-LISTP)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SPLIT-LIST-OLD)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION SPLIT-LIST-OLD))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
SPLIT-LIST-OLD-PART2-TRUELIST

Summary
Form:  ( DEFTHM SPLIT-LIST-OLD-LENGTH-PART1 ...)
Rules: ((:DEFINITION LEN)
        (:DEFINITION MV-NTH)
        (:DEFINITION NOT)
        (:DEFINITION SPLIT-LIST-OLD)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION SPLIT-LIST-OLD))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SPLIT-LIST-OLD-LENGTH-PART1

Summary
Form:  ( DEFTHM SPLIT-LIST-OLD-LENGTH-PART2 ...)
Rules: ((:DEFINITION LEN)
        (:DEFINITION MV-NTH)
        (:DEFINITION NOT)
        (:DEFINITION SPLIT-LIST-OLD)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION SPLIT-LIST-OLD)
        (:TYPE-PRESCRIPTION SPLIT-LIST-OLD-PART2-TRUELIST))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SPLIT-LIST-OLD-LENGTH-PART2

Summary
Form:  ( DEFTHM SPLIT-LIST-OLD-LENGTH-LESS-PART1 ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION LEN)
        (:DEFINITION MV-NTH)
        (:DEFINITION NOT)
        (:DEFINITION SPLIT-LIST-OLD)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SPLIT-LIST-OLD)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE DEFAULT-CDR)
        (:TYPE-PRESCRIPTION LEN)
        (:TYPE-PRESCRIPTION SPLIT-LIST-OLD))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
SPLIT-LIST-OLD-LENGTH-LESS-PART1

Summary
Form:  ( DEFTHM SPLIT-LIST-OLD-LENGTH-LESS-PART2 ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION LEN)
        (:DEFINITION MV-NTH)
        (:DEFINITION NOT)
        (:DEFINITION SPLIT-LIST-OLD)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART MV-NTH)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SPLIT-LIST-OLD)
        (:REWRITE CDR-CONS)
        (:REWRITE DEFAULT-CDR)
        (:TYPE-PRESCRIPTION LEN)
        (:TYPE-PRESCRIPTION SPLIT-LIST-OLD)
        (:TYPE-PRESCRIPTION SPLIT-LIST-OLD-PART2-TRUELIST))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
SPLIT-LIST-OLD-LENGTH-LESS-PART2

Summary
Form:  ( IN-THEORY (DISABLE ...))
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
1980

Summary
Form:  ( DEFUN SPLIT-LIST ...)
Rules: ((:DEFINITION ACL2-COUNT)
        (:DEFINITION ENDP)
        (:DEFINITION O-FINP)
        (:DEFINITION O<)
        (:ELIM CAR-CDR-ELIM)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION ACL2-COUNT))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
SPLIT-LIST

Summary
Form:  ( DEFTHM LEMMA ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION MV-NTH)
        (:DEFINITION NOT)
        (:DEFINITION REVAPPEND)
        (:DEFINITION SPLIT-LIST)
        (:DEFINITION SPLIT-LIST-OLD)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART MV-NTH)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SPLIT-LIST)
        (:INDUCTION SPLIT-LIST-OLD)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION SPLIT-LIST-OLD)
        (:TYPE-PRESCRIPTION SPLIT-LIST-OLD-PART2-TRUELIST))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
LEMMA

Summary
Form:  ( DEFTHM LEMMA2 ...)
Rules: ((:DEFINITION FIX)
        (:DEFINITION LEN)
        (:DEFINITION REVAPPEND)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION LEN)
        (:INDUCTION REVAPPEND)
        (:REWRITE CDR-CONS)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE UNICITY-OF-0)
        (:TYPE-PRESCRIPTION LEN))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
LEMMA2

Summary
Form:  ( DEFTHM LEMMA3 ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REVAPPEND)
        (:DEFINITION TRUE-LISTP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION REVAPPEND)
        (:REWRITE CDR-CONS))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LEMMA3

Summary
Form:  ( DEFUN MERGESORT-EXEC ...)
Rules: ((:COMPOUND-RECOGNIZER ACL2::NATP-COMPOUND-RECOGNIZER)
        (:DEFINITION ENDP)
        (:DEFINITION FIX)
        (:DEFINITION LEN)
        (:DEFINITION MV-NTH)
        (:DEFINITION O-FINP)
        (:DEFINITION O-P)
        (:DEFINITION O<)
        (:DEFINITION SPLIT-LIST-OLD)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART O-P)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE LEMMA)
        (:REWRITE LEMMA2)
        (:REWRITE UNICITY-OF-0)
        (:TYPE-PRESCRIPTION LEN)
        (:TYPE-PRESCRIPTION SPLIT-LIST-OLD))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
MERGESORT-EXEC

Summary
Form:  ( DEFTHM MERGESORT-EXEC-SET ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION MERGESORT-EXEC)
        (:DEFINITION MV-NTH)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART SETP)
        (:EXECUTABLE-COUNTERPART ZP)
        (:INDUCTION MERGESORT-EXEC)
        (:REWRITE INSERT-NEVER-EMPTY)
        (:REWRITE LEMMA)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE UNION-SET)
        (:TYPE-PRESCRIPTION SETP-TYPE)
        (:TYPE-PRESCRIPTION SPLIT-LIST-OLD))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
MERGESORT-EXEC-SET

Summary
Form:  ( IN-THEORY (DISABLE ...))
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
1991

Summary
Form:  ( DEFTHM MERGESORT-MEMBERSHIP-2 ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION IN-LIST)
        (:DEFINITION MERGESORT-EXEC)
        (:DEFINITION MV-NTH)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART SETP)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION MERGESORT-EXEC)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE IN-INSERT)
        (:REWRITE IN-LIST-ON-SET)
        (:REWRITE IN-LIST-REVAPPEND)
        (:REWRITE LEMMA)
        (:REWRITE NEVER-IN-EMPTY)
        (:REWRITE UNION-IN)
        (:TYPE-PRESCRIPTION IN-LIST)
        (:TYPE-PRESCRIPTION IN-TYPE)
        (:TYPE-PRESCRIPTION SPLIT-LIST-OLD))
Warnings:  None
Time:  0.11 seconds (prove: 0.11, print: 0.00, other: 0.00)
MERGESORT-MEMBERSHIP-2

Summary
Form:  ( DEFTHM MERGESORT-MEMBERSHIP-1 ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION IN-LIST)
        (:DEFINITION MERGESORT-EXEC)
        (:DEFINITION MV-NTH)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART SETP)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION MERGESORT-EXEC)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE IN-INSERT)
        (:REWRITE IN-LIST-ON-SET)
        (:REWRITE IN-LIST-REVAPPEND)
        (:REWRITE LEMMA)
        (:REWRITE MERGESORT-MEMBERSHIP-2)
        (:REWRITE NEVER-IN-EMPTY)
        (:REWRITE UNION-IN)
        (:TYPE-PRESCRIPTION IN-LIST)
        (:TYPE-PRESCRIPTION IN-TYPE)
        (:TYPE-PRESCRIPTION SPLIT-LIST-OLD))
Warnings:  None
Time:  0.20 seconds (prove: 0.20, print: 0.00, other: 0.00)
MERGESORT-MEMBERSHIP-1

Summary
Form:  ( DEFTHM MERGESORT-MEMBERSHIP ...)
Rules: ((:DEFINITION IFF)
        (:REWRITE MERGESORT-MEMBERSHIP-1)
        (:REWRITE MERGESORT-MEMBERSHIP-2)
        (:TYPE-PRESCRIPTION IN-LIST)
        (:TYPE-PRESCRIPTION IN-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
MERGESORT-MEMBERSHIP

Summary
Form:  ( VERIFY-GUARDS MERGESORT-EXEC ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION MV-NTH)
        (:DEFINITION NOT)
        (:DEFINITION TRUE-LISTP)
        (:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART SETP)
        (:EXECUTABLE-COUNTERPART TRUE-LISTP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE LEMMA)
        (:REWRITE LEMMA3)
        (:REWRITE MERGESORT-EXEC-SET))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
MERGESORT-EXEC

Summary
Form:  ( DEFUN MERGESORT ...)
Rules: ((:TYPE-PRESCRIPTION INSERT))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MERGESORT

Summary
Form:  ( DEFTHM MERGESORT-SET ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION MERGESORT)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART SETP)
        (:INDUCTION MERGESORT)
        (:REWRITE INSERT-NEVER-EMPTY)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
MERGESORT-SET

Summary
Form:  ( DEFTHM IN-MERGESORT ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION IN-LIST)
        (:DEFINITION MERGESORT)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION IN-LIST)
        (:INDUCTION MERGESORT)
        (:REWRITE IN-INSERT)
        (:REWRITE MERGESORT-MEMBERSHIP)
        (:REWRITE MERGESORT-MEMBERSHIP-1)
        (:REWRITE NEVER-IN-EMPTY)
        (:TYPE-PRESCRIPTION IN-LIST)
        (:TYPE-PRESCRIPTION IN-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
IN-MERGESORT

We suspect this conjecture sould be proven by functional instantiation
of ALL-BY-MEMBERSHIP.  This suspicion is caused by PICK-A-POINT-SUBSET-
STRATEGY, so if this is not what you want to do, then you should disable
PICK-A-POINT-SUBSET-STRATEGY.  Accordingly, we suggest the following
hint: 

("Subgoal 2'"
    (:USE ((:FUNCTIONAL-INSTANCE
                ALL-BY-MEMBERSHIP
                (ALL-HYPS (LAMBDA NIL
                                  (AND (CONSP X) (TRUE-LISTP (CDR X)))))
                (ALL-SET (LAMBDA NIL (MERGESORT (CDR X))))
                (ALL (LAMBDA (COMPUTED-HINTS::?X)
                             (SUBSET COMPUTED-HINTS::?X (MERGESORT-EXEC X))))
                (PREDICATE (LAMBDA (COMPUTED-HINTS::?X)
                                   (IN COMPUTED-HINTS::?X
                                       (MERGESORT-EXEC X))))))
          :EXPAND ((SUBSET-TRIGGER (MERGESORT (CDR X))
                                   (MERGESORT-EXEC X)))))

[SGC for 3622 CONS pages..(11973 writable)..(T=2).GC finished]

We suspect this conjecture sould be proven by functional instantiation
of ALL-BY-MEMBERSHIP.  This suspicion is caused by PICK-A-POINT-SUBSET-
STRATEGY, so if this is not what you want to do, then you should disable
PICK-A-POINT-SUBSET-STRATEGY.  Accordingly, we suggest the following
hint: 

("Subgoal 1'"
     (:USE ((:FUNCTIONAL-INSTANCE
                 ALL-BY-MEMBERSHIP
                 (ALL-HYPS (LAMBDA NIL
                                   (AND (CONSP X) (TRUE-LISTP (CDR X)))))
                 (ALL-SET (LAMBDA NIL (MERGESORT-EXEC X)))
                 (ALL (LAMBDA (COMPUTED-HINTS::?X)
                              (SUBSET COMPUTED-HINTS::?X
                                      (INSERT (CAR X) (MERGESORT (CDR X))))))
                 (PREDICATE (LAMBDA (COMPUTED-HINTS::?X)
                                    (IN COMPUTED-HINTS::?X
                                        (INSERT (CAR X)
                                                (MERGESORT (CDR X))))))))
           :EXPAND ((SUBSET-TRIGGER (MERGESORT-EXEC X)
                                    (INSERT (CAR X) (MERGESORT (CDR X)))))))


Summary
Form:  ( VERIFY-GUARDS MERGESORT)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION IN-LIST)
        (:DEFINITION NOT)
        (:DEFINITION SUBSET)
        (:DEFINITION SUBSET-TRIGGER)
        (:DEFINITION SYNP)
        (:DEFINITION TRUE-LISTP)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART ENDP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART INSERT)
        (:EXECUTABLE-COUNTERPART MERGESORT)
        (:EXECUTABLE-COUNTERPART MERGESORT-EXEC)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE DOUBLE-CONTAINMENT)
        (:REWRITE IN-INSERT)
        (:REWRITE IN-MERGESORT)
        (:REWRITE INSERT-NEVER-EMPTY)
        (:REWRITE MERGESORT-EXEC-SET)
        (:REWRITE MERGESORT-MEMBERSHIP)
        (:REWRITE MERGESORT-MEMBERSHIP-1)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE PICK-A-POINT-SUBSET-STRATEGY)
        (:REWRITE SUBSET-INSERT-X)
        (:TYPE-PRESCRIPTION IN-LIST)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.22 seconds (prove: 0.22, print: 0.00, other: 0.00)
MERGESORT

We suspect this conjecture sould be proven by functional instantiation
of ALL-BY-MEMBERSHIP.  This suspicion is caused by PICK-A-POINT-SUBSET-
STRATEGY, so if this is not what you want to do, then you should disable
PICK-A-POINT-SUBSET-STRATEGY.  Accordingly, we suggest the following
hint: 

("Subgoal 2'"
 (:USE
      ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP
                             (ALL-HYPS (LAMBDA NIL (SETP X)))
                             (ALL-SET (LAMBDA NIL (MERGESORT X)))
                             (ALL (LAMBDA (COMPUTED-HINTS::?X)
                                          (SUBSET COMPUTED-HINTS::?X X)))
                             (PREDICATE (LAMBDA (COMPUTED-HINTS::?X)
                                                (IN COMPUTED-HINTS::?X X)))))
      :EXPAND ((SUBSET-TRIGGER (MERGESORT X) X))))


We suspect this conjecture sould be proven by functional instantiation
of ALL-BY-MEMBERSHIP.  This suspicion is caused by PICK-A-POINT-SUBSET-
STRATEGY, so if this is not what you want to do, then you should disable
PICK-A-POINT-SUBSET-STRATEGY.  Accordingly, we suggest the following
hint: 

("Subgoal 1'"
     (:USE ((:FUNCTIONAL-INSTANCE
                 ALL-BY-MEMBERSHIP
                 (ALL-HYPS (LAMBDA NIL (SETP X)))
                 (ALL-SET (LAMBDA NIL X))
                 (ALL (LAMBDA (COMPUTED-HINTS::?X)
                              (SUBSET COMPUTED-HINTS::?X (MERGESORT X))))
                 (PREDICATE (LAMBDA (COMPUTED-HINTS::?X)
                                    (IN COMPUTED-HINTS::?X (MERGESORT X))))))
           :EXPAND ((SUBSET-TRIGGER X (MERGESORT X)))))


Summary
Form:  ( DEFTHM MERGESORT-SET-IDENTITY ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION HEAD)
        (:DEFINITION IN)
        (:DEFINITION SETP)
        (:DEFINITION SUBSET)
        (:DEFINITION SUBSET-TRIGGER)
        (:DEFINITION SYNP)
        (:DEFINITION TAIL)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE DOUBLE-CONTAINMENT)
        (:REWRITE EMPTY-SUBSET)
        (:REWRITE IN-LIST-ON-SET)
        (:REWRITE IN-MERGESORT)
        (:REWRITE IN-SET)
        (:REWRITE MERGESORT-MEMBERSHIP)
        (:REWRITE MERGESORT-MEMBERSHIP-1)
        (:REWRITE MERGESORT-SET)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE PICK-A-POINT-SUBSET-STRATEGY)
        (:REWRITE SFIX-SET-IDENTITY)
        (:REWRITE SUBSET-IN)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION IN-LIST)
        (:TYPE-PRESCRIPTION IN-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.25 seconds (prove: 0.24, print: 0.00, other: 0.01)
MERGESORT-SET-IDENTITY

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
[SGC for 3622 CONS pages..(11974 writable)..(T=3).GC finished]
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/primitives.o
start address -T 0x93f4a70 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/primitives.o
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
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/membership.o
start address -T 0x9945000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/membership.o
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/fast.o
start address -T 0x94582c0 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/fast.o
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/outer.o
start address -T 0x9b24320 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/outer.o

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

;; Note: Tail-recursive call of IN-LIST was replaced by iteration.
;; Note: Tail-recursive call of SPLIT-LIST was replaced by iteration.
End of Pass 2.  
[SGC for 12 SYMBOL pages..(12576 writable)..(T=3).GC finished]
OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
Finished compiling /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/sort.o.

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

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

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

ACL2>