GCL (GNU Common Lisp)  2.6.5 CLtL1    Oct 17 2004 12:48:32
Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
Binary License:  GPL due to GPL'ed components: (READLINE 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 built December 9, 2004  12:40:52.
 Copyright (C) 2004  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 for recent changes.

 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.
Loading /export/v/filer2/moore/acl2-init.lsp
Finished loading /export/v/filer2/moore/acl2-init.lsp

ACL2 Version 2.9.  Level 1.  Cbd 
"/export/v/filer3/v0q005/text/marktoberdorf-04/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>(certify-book "how-to-prove-thms")

CERTIFICATION ATTEMPT FOR 
"/export/v/filer3/v0q005/text/marktoberdorf-04/how-to-prove-thms.lisp"
ACL2 Version 2.9


* Step 1:  Read 
"/export/v/filer3/v0q005/text/marktoberdorf-04/how-to-prove-thms.lisp"
and compute its check sum.

* Step 2:  There were 115 forms in the file. The check sum is 190369092.
We now attempt to establish that each form, whether local or non-local,
is indeed an admissible embedded event form in the context of the previously
admitted ones.  Note that proof-tree output is inhibited during this
check; see :DOC proof-tree.


ACL2 >>(DEFUN DUP (X)
              (IF (CONSP X)
                  (CONS (CAR X)
                        (CONS (CAR X) (DUP (CDR X))))
                  NIL))

The admission of DUP is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  We observe that the type of DUP is described by the
theorem (TRUE-LISTP (DUP X)).  We used primitive type reasoning.

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


ACL2 >>(DEFTHM DUP-EXAMPLES
               (AND (EQUAL (DUP '(1 2 3)) '(1 1 2 2 3 3))
                    (EQUAL (DUP '(HELLO)) '(HELLO HELLO))
                    (EQUAL (DUP '(A B C . D))
                           '(A A B B C C)))
               :RULE-CLASSES NIL)

But we reduce the conjecture to T, by the :executable-counterparts
of DUP, EQUAL and IF.

Q.E.D.

Summary
Form:  ( DEFTHM DUP-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART DUP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART IF))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
DUP-EXAMPLES


ACL2 >>(DEFUN APP (X Y)
              (IF (CONSP X)
                  (CONS (CAR X) (APP (CDR X) Y))
                  Y))

The admission of APP is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  We observe that the type of APP is described by the
theorem (OR (CONSP (APP X Y)) (EQUAL (APP X Y) Y)).  We used primitive
type reasoning.

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


ACL2 >>(DEFTHM APP-EXAMPLES
               (AND (EQUAL (APP '(1 2 3) '(4 5 6))
                           '(1 2 3 4 5 6))
                    (EQUAL (APP '(3 2 1) '(0)) '(3 2 1 0))
                    (EQUAL (APP '(A B C . D) '(E F))
                           '(A B C E F)))
               :RULE-CLASSES NIL)

But we reduce the conjecture to T, by the :executable-counterparts
of APP, EQUAL and IF.

Q.E.D.

Summary
Form:  ( DEFTHM APP-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART APP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART IF))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
APP-EXAMPLES


ACL2 >>(DEFUN MEMP (E X)
              (IF (CONSP X)
                  (IF (EQUAL E (CAR X))
                      T (MEMP E (CDR X)))
                  NIL))

The admission of MEMP is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  We observe that the type of MEMP is described by the
theorem (OR (EQUAL (MEMP E X) T) (EQUAL (MEMP E X) NIL)).  

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


ACL2 >>(DEFTHM MEMP-EXAMPLES
               (AND (MEMP 1 '(0 1 2 3))
                    (NOT (MEMP 5 '(0 1 2 3)))
                    (NOT (MEMP 2 '((0) (1) (2))))
                    (MEMP '(2) '((0) (1) (2)))
                    (NOT (MEMP 2 '(0 1 . 2))))
               :RULE-CLASSES NIL)

But we reduce the conjecture to T, by the :executable-counterparts
of IF and MEMP.

Q.E.D.

Summary
Form:  ( DEFTHM MEMP-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART MEMP)
        (:EXECUTABLE-COUNTERPART NOT))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MEMP-EXAMPLES


ACL2 >>(DEFUN REV (X)
              (IF (CONSP X)
                  (APP (REV (CDR X)) (CONS (CAR X) NIL))
                  NIL))

The admission of REV is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  We observe that the type of REV is described by the
theorem (OR (CONSP (REV X)) (EQUAL (REV X) NIL)).  We used primitive
type reasoning and the :type-prescription rule APP.

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


ACL2 >>(DEFTHM REV-EXAMPLES
               (AND (EQUAL (REV '(1 2 3)) '(3 2 1))
                    (EQUAL (REV '(OK)) '(OK))
                    (EQUAL (REV '(1 2 3 . END)) '(3 2 1)))
               :RULE-CLASSES NIL)

But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL, IF and REV.

Q.E.D.

Summary
Form:  ( DEFTHM REV-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART REV))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
REV-EXAMPLES


ACL2 >>(DEFUN REV1 (X A)
              (IF (CONSP X)
                  (REV1 (CDR X) (CONS (CAR X) A))
                  A))

The admission of REV1 is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  We observe that the type of REV1 is described by the
theorem (OR (CONSP (REV1 X A)) (EQUAL (REV1 X A) A)).  We used primitive
type reasoning.

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


ACL2 >>(DEFTHM REV1-EXAMPLES
               (AND (EQUAL (REV1 '(1 2 3) NIL) '(3 2 1))
                    (EQUAL (REV1 '(OK) NIL) '(OK))
                    (EQUAL (REV1 '(1 2 3 . END) NIL)
                           '(3 2 1))
                    (EQUAL (REV1 '(A B C) '(1 2 3))
                           '(C B A 1 2 3)))
               :RULE-CLASSES NIL)

But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL, IF and REV1.

Q.E.D.

Summary
Form:  ( DEFTHM REV1-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART REV1))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
REV1-EXAMPLES


ACL2 >>(DEFUN PROPERP (X)
              (IF (CONSP X)
                  (PROPERP (CDR X))
                  (EQUAL X NIL)))

The admission of PROPERP is trivial, using the relation O< (which is
known to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  We observe that the type of PROPERP is described by
the theorem (OR (EQUAL (PROPERP X) T) (EQUAL (PROPERP X) NIL)).  We
used primitive type reasoning.

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


ACL2 >>(DEFTHM PROPERP-EXAMPLES
               (AND (PROPERP '(1 2 3))
                    (NOT (PROPERP '(1 2 3 . END)))
                    (PROPERP '((A . 1) (B . 2) (C . 3)))
                    (PROPERP NIL)
                    (NOT (PROPERP 7)))
               :RULE-CLASSES NIL)
[SGC for 19 STRING pages..(8001 writable)..(T=2).GC finished]

But we reduce the conjecture to T, by the :executable-counterparts
of IF and PROPERP.

Q.E.D.

Summary
Form:  ( DEFTHM PROPERP-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART PROPERP))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
PROPERP-EXAMPLES


ACL2 >>(DEFUN MAPNIL (X)
              (IF (CONSP X)
                  (CONS NIL (MAPNIL (CDR X)))
                  NIL))

The admission of MAPNIL is trivial, using the relation O< (which is
known to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  We observe that the type of MAPNIL is described by
the theorem (TRUE-LISTP (MAPNIL X)).  We used primitive type reasoning.

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


ACL2 >>(DEFTHM MAPNIL-EXAMPLES
               (AND (EQUAL (MAPNIL '(1 2 3)) '(NIL NIL NIL))
                    (EQUAL (MAPNIL '(HELLO)) '(NIL)))
               :RULE-CLASSES NIL)

But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL, IF and MAPNIL.

Q.E.D.

Summary
Form:  ( DEFTHM MAPNIL-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART MAPNIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MAPNIL-EXAMPLES


ACL2 >>(DEFUN SWAPTREE (X)
              (IF (CONSP X)
                  (CONS (SWAPTREE (CDR X))
                        (SWAPTREE (CAR X)))
                  X))

The admission of SWAPTREE is trivial, using the relation O< (which
is known to be well-founded on the domain recognized by O-P) and the
measure (ACL2-COUNT X).  We could deduce no constraints on the type
of SWAPTREE.  However, in normalizing the definition we used primitive
type reasoning.

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


ACL2 >>(DEFTHM SWAPTREE-EXAMPLES
               (AND (EQUAL (SWAPTREE '((A . B) C . D))
                           '((D . C) B . A))
                    (EQUAL (SWAPTREE '(A B C D))
                           '((((NIL . D) . C) . B) . A)))
               :RULE-CLASSES NIL)

But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL, IF and SWAPTREE.

Q.E.D.

Summary
Form:  ( DEFTHM SWAPTREE-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART SWAPTREE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SWAPTREE-EXAMPLES


ACL2 >>(DEFUN ZIPLISTS (X Y)
              (IF (CONSP X)
                  (CONS (CONS (CAR X) (CAR Y))
                        (ZIPLISTS (CDR X) (CDR Y)))
                  NIL))

The admission of ZIPLISTS is trivial, using the relation O< (which
is known to be well-founded on the domain recognized by O-P) and the
measure (ACL2-COUNT X).  We observe that the type of ZIPLISTS is described
by the theorem (TRUE-LISTP (ZIPLISTS X Y)).  We used primitive type
reasoning.

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


ACL2 >>(DEFTHM ZIPLISTS-EXAMPLES
               (AND (EQUAL (ZIPLISTS '(A B C) '(1 2 3 4))
                           '((A . 1) (B . 2) (C . 3)))
                    (EQUAL (ZIPLISTS '(A B C) '(1 2))
                           '((A . 1) (B . 2) (C))))
               :RULE-CLASSES NIL)

But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL, IF and ZIPLISTS.

Q.E.D.

Summary
Form:  ( DEFTHM ZIPLISTS-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART ZIPLISTS))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ZIPLISTS-EXAMPLES


ACL2 >>(DEFUN LOOKUP (X A)
              (IF (CONSP A)
                  (IF (EQUAL X (CAR (CAR A)))
                      (CDR (CAR A))
                      (LOOKUP X (CDR A)))
                  NIL))

The admission of LOOKUP is trivial, using the relation O< (which is
known to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT A).  We could deduce no constraints on the type of LOOKUP.

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


ACL2 >>(DEFTHM LOOKUP-EXAMPLES
               (AND (EQUAL (LOOKUP 'B
                                   '((A . 1) (B . 2) (C . 3) (A . 4)))
                           2)
                    (EQUAL (LOOKUP 'A
                                   '((A . 1) (B . 2) (C . 3) (A . 4)))
                           1)
                    (EQUAL (LOOKUP 'X
                                   '((A . 1) (B . 2) (C . 3) (A . 4)))
                           NIL)
                    (EQUAL (LOOKUP 'J '((I . 1) (J) (K . 123)))
                           NIL))
               :RULE-CLASSES NIL)

But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL, IF and LOOKUP.

Q.E.D.

Summary
Form:  ( DEFTHM LOOKUP-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART LOOKUP))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LOOKUP-EXAMPLES


ACL2 >>(DEFUN FOUNDP (X A)
              (IF (CONSP A)
                  (IF (EQUAL X (CAR (CAR A)))
                      T (FOUNDP X (CDR A)))
                  NIL))

The admission of FOUNDP is trivial, using the relation O< (which is
known to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT A).  We observe that the type of FOUNDP is described by
the theorem (OR (EQUAL (FOUNDP X A) T) (EQUAL (FOUNDP X A) NIL)). 

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


ACL2 >>(DEFTHM FOUNDP-EXAMPLES
               (AND (EQUAL (FOUNDP 'B
                                   '((A . 1) (B . 2) (C . 3) (A . 4)))
                           T)
                    (EQUAL (FOUNDP 'A
                                   '((A . 1) (B . 2) (C . 3) (A . 4)))
                           T)
                    (EQUAL (FOUNDP 'X
                                   '((A . 1) (B . 2) (C . 3) (A . 4)))
                           NIL)
                    (EQUAL (FOUNDP 'J '((I . 1) (J) (K . 123)))
                           T))
               :RULE-CLASSES NIL)

But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL, FOUNDP and IF.

Q.E.D.

Summary
Form:  ( DEFTHM FOUNDP-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART FOUNDP)
        (:EXECUTABLE-COUNTERPART IF))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FOUNDP-EXAMPLES


ACL2 >>(DEFUN SUBP (X Y)
              (IF (CONSP X)
                  (IF (MEMP (CAR X) Y)
                      (SUBP (CDR X) Y)
                      NIL)
                  T))

The admission of SUBP is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  We observe that the type of SUBP is described by the
theorem (OR (EQUAL (SUBP X Y) T) (EQUAL (SUBP X Y) NIL)).  

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


ACL2 >>(DEFTHM SUBP-EXAMPLES
               (AND (SUBP '(A B B A) '(A B))
                    (SUBP '(A B C) '(E D C B A))
                    (NOT (SUBP '(A B) '(A C A D A F))))
               :RULE-CLASSES NIL)

But we reduce the conjecture to T, by the :executable-counterparts
of IF and SUBP.

Q.E.D.
[SGC for 19 STRING pages..(8003 writable)..(T=1).GC finished]

Summary
Form:  ( DEFTHM SUBP-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART SUBP))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
SUBP-EXAMPLES


ACL2 >>(DEFUN INT (X Y)
              (IF (CONSP X)
                  (IF (MEMP (CAR X) Y)
                      (CONS (CAR X) (INT (CDR X) Y))
                      (INT (CDR X) Y))
                  NIL))

The admission of INT is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  We observe that the type of INT is described by the
theorem (TRUE-LISTP (INT X Y)).  We used primitive type reasoning.

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


ACL2 >>(DEFTHM INT-EXAMPLES
               (AND (EQUAL (INT '(A B C) '(A B A D)) '(A B))
                    (EQUAL (INT '(A B C) '(X Y Z)) NIL)
                    (EQUAL (INT '(A A B B) '(A B C))
                           '(A A B B)))
               :RULE-CLASSES NIL)

But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL, IF and INT.

Q.E.D.

Summary
Form:  ( DEFTHM INT-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART INT))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
INT-EXAMPLES


ACL2 >>(DEFUN MEM (E X)
              (IF (CONSP X)
                  (IF (EQUAL E (CAR X)) X (MEM E (CDR X)))
                  NIL))

The admission of MEM is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  We observe that the type of MEM is described by the
theorem (OR (CONSP (MEM E X)) (EQUAL (MEM E X) NIL)).  

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


ACL2 >>(DEFUN LONESOMEP (E LST)
              (IF (MEM E LST)
                  (NOT (MEM E (CDR (MEM E LST))))
                  NIL))

Since LONESOMEP is non-recursive, its admission is trivial.  We observe
that the type of LONESOMEP is described by the theorem 
(OR (EQUAL (LONESOMEP E LST) T) (EQUAL (LONESOMEP E LST) NIL)).  

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


ACL2 >>(DEFUN COLLECT-LONESOMEP (A B)
              (IF (CONSP A)
                  (IF (LONESOMEP (CAR A) B)
                      (CONS (CAR A)
                            (COLLECT-LONESOMEP (CDR A) B))
                      (COLLECT-LONESOMEP (CDR A) B))
                  NIL))

The admission of COLLECT-LONESOMEP is trivial, using the relation O<
(which is known to be well-founded on the domain recognized by O-P)
and the measure (ACL2-COUNT A).  We observe that the type of COLLECT-
LONESOMEP is described by the theorem (TRUE-LISTP (COLLECT-LONESOMEP A B)).
We used primitive type reasoning.

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


ACL2 >>(DEFUN LEAVES (X)
              (IF (CONSP X)
                  (APP (LEAVES (CAR X)) (LEAVES (CDR X)))
                  (CONS X NIL)))

The admission of LEAVES is trivial, using the relation O< (which is
known to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  We observe that the type of LEAVES is described by
the theorem (CONSP (LEAVES X)).  We used primitive type reasoning and
the :type-prescription rule APP.

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


ACL2 >>(DEFUN LONESOMES (X)
              (COLLECT-LONESOMEP (LEAVES X)
                                 (LEAVES X)))

Since LONESOMES is non-recursive, its admission is trivial.  We observe
that the type of LONESOMES is described by the theorem 
(TRUE-LISTP (LONESOMES X)).  We used the :type-prescription rule COLLECT-
LONESOMEP.

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


ACL2 >>(DEFTHM LONESOMES-EXAMPLES
               (AND (EQUAL (LONESOMES '((A . B) C . A))
                           '(B C))
                    (EQUAL (LONESOMES '((A . A) . A)) NIL)
                    (EQUAL (LONESOMES '(((A . B) B . C) (X . Y) C . X))
                           '(A Y)))
               :RULE-CLASSES NIL)

But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL, IF and LONESOMES.

Q.E.D.

Summary
Form:  ( DEFTHM LONESOMES-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART LONESOMES))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LONESOMES-EXAMPLES


ACL2 >>(DEFUN TREECOPY (X)
              (IF (CONSP X)
                  (CONS (TREECOPY (CAR X))
                        (TREECOPY (CDR X)))
                  X))

The admission of TREECOPY is trivial, using the relation O< (which
is known to be well-founded on the domain recognized by O-P) and the
measure (ACL2-COUNT X).  We could deduce no constraints on the type
of TREECOPY.  However, in normalizing the definition we used primitive
type reasoning.

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


ACL2 >>(DEFTHM TREECOPY-IS-ID (EQUAL (TREECOPY X) X))

Name the formula above *1.

Perhaps we can prove *1 by induction.  One induction scheme is suggested
by this conjecture.  

We will induct according to a scheme suggested by (TREECOPY X).  This
suggestion was produced using the :induction rule TREECOPY.  If we
let  (:P X) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P X))
     (IMPLIES (AND (CONSP X)
                   (:P (CAR X))
                   (:P (CDR X)))
              (:P X))).
This induction is justified by the same argument used to admit TREECOPY,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.

Subgoal *1/2
(IMPLIES (NOT (CONSP X))
         (EQUAL (TREECOPY X) X)).

But simplification reduces this to T, using the :definition TREECOPY
and primitive type reasoning.

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (EQUAL (TREECOPY (CAR X)) (CAR X))
              (EQUAL (TREECOPY (CDR X)) (CDR X)))
         (EQUAL (TREECOPY X) X)).

But simplification reduces this to T, using the :definition TREECOPY,
primitive type reasoning and the :rewrite rule CAR-CDR-ELIM.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM TREECOPY-IS-ID ...)
Rules: ((:DEFINITION TREECOPY)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION TREECOPY)
        (:REWRITE CAR-CDR-ELIM))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TREECOPY-IS-ID


ACL2 >>(DEFTHM ASSOCIATIVITY-OF-APP
               (EQUAL (APP (APP A B) C)
                      (APP A (APP B C))))

Name the formula above *1.

Perhaps we can prove *1 by induction.  Three induction schemes are
suggested by this conjecture.  Subsumption reduces that number to two.
However, one of these is flawed and so we are left with one viable
candidate.  

We will induct according to a scheme suggested by (APP A B).  This
suggestion was produced using the :induction rule APP.  If we let  
(:P A B C) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A B C))
     (IMPLIES (AND (CONSP A) (:P (CDR A) B C))
              (:P A B C))).
This induction is justified by the same argument used to admit APP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.

Subgoal *1/2
(IMPLIES (NOT (CONSP A))
         (EQUAL (APP (APP A B) C)
                (APP A (APP B C)))).

But simplification reduces this to T, using the :definition APP and
primitive type reasoning.

Subgoal *1/1
(IMPLIES (AND (CONSP A)
              (EQUAL (APP (APP (CDR A) B) C)
                     (APP (CDR A) (APP B C))))
         (EQUAL (APP (APP A B) C)
                (APP A (APP B C)))).

But simplification reduces this to T, using the :definition APP, primitive
type reasoning and the :rewrite rules CAR-CONS and CDR-CONS.

That completes the proof of *1.

Q.E.D.

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


ACL2 >>(DEFTHM DUP-APP
               (EQUAL (DUP (APP A B))
                      (APP (DUP A) (DUP B))))

Name the formula above *1.

Perhaps we can prove *1 by induction.  Three induction schemes are
suggested by this conjecture.  Subsumption reduces that number to two.
However, one of these is flawed and so we are left with one viable
candidate.  

We will induct according to a scheme suggested by (APP A B).  This
suggestion was produced using the :induction rules APP and DUP.  If
we let  (:P A B) denote *1 above then the induction scheme we'll use
is
(AND (IMPLIES (NOT (CONSP A)) (:P A B))
     (IMPLIES (AND (CONSP A) (:P (CDR A) B))
              (:P A B))).
This induction is justified by the same argument used to admit APP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.

Subgoal *1/2
(IMPLIES (NOT (CONSP A))
         (EQUAL (DUP (APP A B))
                (APP (DUP A) (DUP B)))).

But simplification reduces this to T, using the :definitions APP and
DUP, the :executable-counterpart of CONSP and primitive type reasoning.

Subgoal *1/1
(IMPLIES (AND (CONSP A)
              (EQUAL (DUP (APP (CDR A) B))
                     (APP (DUP (CDR A)) (DUP B))))
         (EQUAL (DUP (APP A B))
                (APP (DUP A) (DUP B)))).

But simplification reduces this to T, using the :definitions APP and
DUP, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-
CONS and the :type-prescription rule DUP.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM DUP-APP ...)
Rules: ((:DEFINITION APP)
        (:DEFINITION DUP)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION APP)
        (:INDUCTION DUP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION DUP))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
DUP-APP


ACL2 >>(DEFTHM DUP-MAPNIL
               (EQUAL (DUP (MAPNIL A))
                      (MAPNIL (DUP A))))

Name the formula above *1.

Perhaps we can prove *1 by induction.  Two induction schemes are suggested
by this conjecture.  Subsumption reduces that number to one.  

We will induct according to a scheme suggested by (DUP A).  This suggestion
was produced using the :induction rules DUP and MAPNIL.  If we let
 (:P A) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A))
     (IMPLIES (AND (CONSP A) (:P (CDR A)))
              (:P A))).
This induction is justified by the same argument used to admit DUP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.

Subgoal *1/2
(IMPLIES (NOT (CONSP A))
         (EQUAL (DUP (MAPNIL A))
                (MAPNIL (DUP A)))).

But simplification reduces this to T, using the :definitions DUP and
MAPNIL and the :executable-counterparts of DUP, EQUAL and MAPNIL.

Subgoal *1/1
(IMPLIES (AND (CONSP A)
              (EQUAL (DUP (MAPNIL (CDR A)))
                     (MAPNIL (DUP (CDR A)))))
         (EQUAL (DUP (MAPNIL A))
                (MAPNIL (DUP A)))).

But simplification reduces this to T, using the :definitions DUP and
MAPNIL, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-
CONS and the :type-prescription rules DUP and MAPNIL.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM DUP-MAPNIL ...)
Rules: ((:DEFINITION DUP)
        (:DEFINITION MAPNIL)
        (:EXECUTABLE-COUNTERPART DUP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART MAPNIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION DUP)
        (:INDUCTION MAPNIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION DUP)
        (:TYPE-PRESCRIPTION MAPNIL))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
DUP-MAPNIL


ACL2 >>(DEFTHM PROPERP-APP-NIL (PROPERP (APP A NIL)))

Name the formula above *1.

Perhaps we can prove *1 by induction.  One induction scheme is suggested
by this conjecture.  

We will induct according to a scheme suggested by (APP A 'NIL).  This
suggestion was produced using the :induction rule APP.  If we let  (:P A)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A))
     (IMPLIES (AND (CONSP A) (:P (CDR A)))
              (:P A))).
This induction is justified by the same argument used to admit APP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.

Subgoal *1/2
(IMPLIES (NOT (CONSP A))
         (PROPERP (APP A NIL))).

But simplification reduces this to T, using the :definition APP and
the :executable-counterpart of PROPERP.

Subgoal *1/1
(IMPLIES (AND (CONSP A)
              (PROPERP (APP (CDR A) NIL)))
         (PROPERP (APP A NIL))).

But simplification reduces this to T, using the :definitions APP and
PROPERP, primitive type reasoning, the :rewrite rule CDR-CONS and the
:type-prescription rule PROPERP.

That completes the proof of *1.

Q.E.D.

The storage of PROPERP-APP-NIL depends upon the :type-prescription
rule PROPERP.

Summary
Form:  ( DEFTHM PROPERP-APP-NIL ...)
Rules: ((:DEFINITION APP)
        (:DEFINITION PROPERP)
        (:EXECUTABLE-COUNTERPART PROPERP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION APP)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION PROPERP))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
PROPERP-APP-NIL


ACL2 >>(DEFTHM SWAPTREE-SWAPTREE
               (EQUAL (SWAPTREE (SWAPTREE X)) X))

Name the formula above *1.

Perhaps we can prove *1 by induction.  One induction scheme is suggested
by this conjecture.  

We will induct according to a scheme suggested by (SWAPTREE X).  This
suggestion was produced using the :induction rule SWAPTREE.  If we
let  (:P X) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P X))
     (IMPLIES (AND (CONSP X)
                   (:P (CDR X))
                   (:P (CAR X)))
              (:P X))).
This induction is justified by the same argument used to admit SWAPTREE,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.

Subgoal *1/2
(IMPLIES (NOT (CONSP X))
         (EQUAL (SWAPTREE (SWAPTREE X)) X)).

But simplification reduces this to T, using the :definition SWAPTREE
and primitive type reasoning.
[SGC for 21 CFUN pages..(8013 writable)..(T=1).GC finished]

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (EQUAL (SWAPTREE (SWAPTREE (CDR X)))
                     (CDR X))
              (EQUAL (SWAPTREE (SWAPTREE (CAR X)))
                     (CAR X)))
         (EQUAL (SWAPTREE (SWAPTREE X)) X)).

But simplification reduces this to T, using the :definition SWAPTREE,
primitive type reasoning and the :rewrite rules CAR-CDR-ELIM, CAR-CONS
and CDR-CONS.

That completes the proof of *1.

Q.E.D.

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


ACL2 >>(DEFTHM MEMP-APP
               (EQUAL (MEMP E (APP A B))
                      (OR (MEMP E A) (MEMP E B))))

This simplifies, using the :type-prescription rule MEMP, to the following
two conjectures.

Subgoal 2
(IMPLIES (MEMP E A)
         (EQUAL (MEMP E (APP A B)) T)).

This simplifies, using primitive type reasoning and the :type-prescription
rule MEMP, to

Subgoal 2'
(IMPLIES (MEMP E A) (MEMP E (APP A B))).

Name the formula above *1.

Subgoal 1
(IMPLIES (NOT (MEMP E A))
         (EQUAL (MEMP E (APP A B)) (MEMP E B))).

Normally we would attempt to prove this formula by induction.  However,
we prefer in this instance to focus on the original input conjecture
rather than this simplified special case.  We therefore abandon our
previous work on this conjecture and reassign the name *1 to the original
conjecture.  (See :DOC otf-flg.)

Perhaps we can prove *1 by induction.  Four induction schemes are suggested
by this conjecture.  Subsumption reduces that number to three.  These
merge into two derived induction schemes.  However, one of these is
flawed and so we are left with one viable candidate.  

We will induct according to a scheme suggested by (MEMP E A), but modified
to accommodate (APP A B).  These suggestions were produced using the
:induction rules APP and MEMP.  If we let  (:P A B E) denote *1 above
then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A B E))
     (IMPLIES (AND (CONSP A)
                   (NOT (EQUAL E (CAR A)))
                   (:P (CDR A) B E))
              (:P A B E))
     (IMPLIES (AND (CONSP A) (EQUAL E (CAR A)))
              (:P A B E))).
This induction is justified by the same argument used to admit MEMP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following three nontautological subgoals.

Subgoal *1/3
(IMPLIES (NOT (CONSP A))
         (EQUAL (MEMP E (APP A B))
                (OR (MEMP E A) (MEMP E B)))).

But simplification reduces this to T, using the :definitions APP and
MEMP and primitive type reasoning.

Subgoal *1/2
(IMPLIES (AND (CONSP A)
              (NOT (EQUAL E (CAR A)))
              (EQUAL (MEMP E (APP (CDR A) B))
                     (OR (MEMP E (CDR A)) (MEMP E B))))
         (EQUAL (MEMP E (APP A B))
                (OR (MEMP E A) (MEMP E B)))).

But simplification reduces this to T, using the :definitions APP and
MEMP, the :executable-counterpart of EQUAL, primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rule MEMP.

Subgoal *1/1
(IMPLIES (AND (CONSP A) (EQUAL E (CAR A)))
         (EQUAL (MEMP E (APP A B))
                (OR (MEMP E A) (MEMP E B)))).

But simplification reduces this to T, using the :definitions APP and
MEMP, the :executable-counterpart of EQUAL, primitive type reasoning
and the :rewrite rule CAR-CONS.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM MEMP-APP ...)
Rules: ((:DEFINITION APP)
        (:DEFINITION MEMP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION APP)
        (:INDUCTION MEMP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION MEMP))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MEMP-APP


ACL2 >>(DEFTHM PROBLEM-6-1
               (EQUAL (MEMP E (APP A A)) (MEMP E A))
               :RULE-CLASSES NIL)

But simplification reduces this to T, using primitive type reasoning,
the :rewrite rule MEMP-APP and the :type-prescription rule MEMP.

Q.E.D.

Summary
Form:  ( DEFTHM PROBLEM-6-1 ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE MEMP-APP)
        (:TYPE-PRESCRIPTION MEMP))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
PROBLEM-6-1


ACL2 >>(DEFTHM PROPERP-APP
               (EQUAL (PROPERP (APP A B)) (PROPERP B)))

ACL2 Warning [Subsume] in ( DEFTHM PROPERP-APP ...):  The newly proposed
:REWRITE rule PROPERP-APP probably subsumes the previously added :REWRITE
rule PROPERP-APP-NIL, in the sense that PROPERP-APP will now probably
be applied whenever the old rule would have been.


Name the formula above *1.

Perhaps we can prove *1 by induction.  Two induction schemes are suggested
by this conjecture.  However, one of these is flawed and so we are
left with one viable candidate.  

We will induct according to a scheme suggested by (APP A B).  This
suggestion was produced using the :induction rule APP.  If we let  (:P A B)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A B))
     (IMPLIES (AND (CONSP A) (:P (CDR A) B))
              (:P A B))).
This induction is justified by the same argument used to admit APP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.

Subgoal *1/2
(IMPLIES (NOT (CONSP A))
         (EQUAL (PROPERP (APP A B))
                (PROPERP B))).

But simplification reduces this to T, using the :definition APP and
primitive type reasoning.

Subgoal *1/1
(IMPLIES (AND (CONSP A)
              (EQUAL (PROPERP (APP (CDR A) B))
                     (PROPERP B)))
         (EQUAL (PROPERP (APP A B))
                (PROPERP B))).

But simplification reduces this to T, using the :definitions APP and
PROPERP, primitive type reasoning and the :rewrite rule CDR-CONS.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM PROPERP-APP ...)
Rules: ((:DEFINITION APP)
        (:DEFINITION PROPERP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION APP)
        (:REWRITE CDR-CONS))
Warnings:  Subsume
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
PROPERP-APP


ACL2 >>(DEFTHM PROPERP-REV (PROPERP (REV X)))

Name the formula above *1.

Perhaps we can prove *1 by induction.  One induction scheme is suggested
by this conjecture.  

We will induct according to a scheme suggested by (REV X).  This suggestion
was produced using the :induction rule REV.  If we let  (:P X) denote
*1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P X))
     (IMPLIES (AND (CONSP X) (:P (CDR X)))
              (:P X))).
This induction is justified by the same argument used to admit REV,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.

Subgoal *1/2
(IMPLIES (NOT (CONSP X))
         (PROPERP (REV X))).

But simplification reduces this to T, using the :definition REV and
the :executable-counterpart of PROPERP.

Subgoal *1/1
(IMPLIES (AND (CONSP X) (PROPERP (REV (CDR X))))
         (PROPERP (REV X))).

But simplification reduces this to T, using the :definitions PROPERP
and REV, the :executable-counterpart of PROPERP, primitive type reasoning
and the :rewrite rules CDR-CONS and PROPERP-APP.

That completes the proof of *1.

Q.E.D.

The storage of PROPERP-REV depends upon the :type-prescription rule
PROPERP.

Summary
Form:  ( DEFTHM PROPERP-REV ...)
Rules: ((:DEFINITION PROPERP)
        (:DEFINITION REV)
        (:EXECUTABLE-COUNTERPART PROPERP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION REV)
        (:REWRITE CDR-CONS)
        (:REWRITE PROPERP-APP)
        (:TYPE-PRESCRIPTION PROPERP))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
PROPERP-REV


ACL2 >>(DEFTHM APP-RIGHT-IDENTITY
               (IMPLIES (PROPERP X)
                        (EQUAL (APP X NIL) X)))

Name the formula above *1.

Perhaps we can prove *1 by induction.  Two induction schemes are suggested
by this conjecture.  Subsumption reduces that number to one.  

We will induct according to a scheme suggested by (APP X 'NIL).  This
suggestion was produced using the :induction rules APP and PROPERP.
If we let  (:P X) denote *1 above then the induction scheme we'll use
is
(AND (IMPLIES (NOT (CONSP X)) (:P X))
     (IMPLIES (AND (CONSP X) (:P (CDR X)))
              (:P X))).
This induction is justified by the same argument used to admit APP,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following three nontautological subgoals.

Subgoal *1/3
(IMPLIES (AND (NOT (CONSP X)) (PROPERP X))
         (EQUAL (APP X NIL) X)).

But simplification reduces this to T, using the :definition PROPERP,
the :executable-counterparts of APP, CONSP and EQUAL and primitive
type reasoning.

Subgoal *1/2
(IMPLIES (AND (CONSP X)
              (EQUAL (APP (CDR X) NIL) (CDR X))
              (PROPERP X))
         (EQUAL (APP X NIL) X)).

But simplification reduces this to T, using the :definitions APP and
PROPERP, primitive type reasoning and the :rewrite rule CAR-CDR-ELIM.

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (NOT (PROPERP (CDR X)))
              (PROPERP X))
         (EQUAL (APP X NIL) X)).

But simplification reduces this to T, using the :definition PROPERP.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM APP-RIGHT-IDENTITY ...)
Rules: ((:DEFINITION APP)
        (:DEFINITION PROPERP)
        (:EXECUTABLE-COUNTERPART APP)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION APP)
        (:INDUCTION PROPERP)
        (:REWRITE CAR-CDR-ELIM))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
APP-RIGHT-IDENTITY


ACL2 >>(DEFTHM REV-APP
               (EQUAL (REV (APP A B))
                      (APP (REV B) (REV A))))

Name the formula above *1.

Perhaps we can prove *1 by induction.  Three induction schemes are
suggested by this conjecture.  Subsumption reduces that number to two.
However, one of these is flawed and so we are left with one viable
candidate.  

We will induct according to a scheme suggested by (APP A B).  This
suggestion was produced using the :induction rules APP and REV.  If
we let  (:P A B) denote *1 above then the induction scheme we'll use
is
(AND (IMPLIES (NOT (CONSP A)) (:P A B))
     (IMPLIES (AND (CONSP A) (:P (CDR A) B))
              (:P A B))).
This induction is justified by the same argument used to admit APP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.

Subgoal *1/2
(IMPLIES (NOT (CONSP A))
         (EQUAL (REV (APP A B))
                (APP (REV B) (REV A)))).

But simplification reduces this to T, using the :definitions APP and
REV, primitive type reasoning and the :rewrite rules APP-RIGHT-IDENTITY
and PROPERP-REV.

Subgoal *1/1
(IMPLIES (AND (CONSP A)
              (EQUAL (REV (APP (CDR A) B))
                     (APP (REV B) (REV (CDR A)))))
         (EQUAL (REV (APP A B))
                (APP (REV B) (REV A)))).

This simplifies, using the :definitions APP and REV, primitive type
reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to

Subgoal *1/1'
(IMPLIES (AND (CONSP A)
              (EQUAL (REV (APP (CDR A) B))
                     (APP (REV B) (REV (CDR A)))))
         (EQUAL (APP (REV (APP (CDR A) B))
                     (LIST (CAR A)))
                (APP (REV B)
                     (APP (REV (CDR A)) (LIST (CAR A)))))).

The destructor terms (CAR A) and (CDR A) can be eliminated by using
CAR-CDR-ELIM to replace A by (CONS A1 A2), (CAR A) by A1 and (CDR A)
by A2.  This produces the following goal.

Subgoal *1/1''
(IMPLIES (AND (CONSP (CONS A1 A2))
              (EQUAL (REV (APP A2 B))
                     (APP (REV B) (REV A2))))
         (EQUAL (APP (REV (APP A2 B)) (LIST A1))
                (APP (REV B)
                     (APP (REV A2) (LIST A1))))).

This simplifies, using primitive type reasoning, to

Subgoal *1/1'''
(IMPLIES (EQUAL (REV (APP A2 B))
                (APP (REV B) (REV A2)))
         (EQUAL (APP (REV (APP A2 B)) (LIST A1))
                (APP (REV B)
                     (APP (REV A2) (LIST A1))))).

We now use the hypothesis by substituting (APP (REV B) (REV A2)) for
(REV (APP A2 B)) and throwing away the hypothesis.  This produces

Subgoal *1/1'4'
(EQUAL (APP (APP (REV B) (REV A2)) (LIST A1))
       (APP (REV B) (APP (REV A2) (LIST A1)))).

But we reduce the conjecture to T, by the simple :rewrite rule ASSOCIATIVITY-
OF-APP.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM REV-APP ...)
Rules: ((:DEFINITION APP)
        (:DEFINITION REV)
        (:ELIM CAR-CDR-ELIM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION APP)
        (:INDUCTION REV)
        (:REWRITE APP-RIGHT-IDENTITY)
        (:REWRITE ASSOCIATIVITY-OF-APP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE PROPERP-REV))
Warnings:  None
Time:  0.02 seconds (prove: 0.01, print: 0.01, other: 0.00)
REV-APP


ACL2 >>(DEFTHM REV-REV
               (IMPLIES (PROPERP Z)
                        (EQUAL (REV (REV Z)) Z)))

Name the formula above *1.

Perhaps we can prove *1 by induction.  Two induction schemes are suggested
by this conjecture.  Subsumption reduces that number to one.  

We will induct according to a scheme suggested by (REV Z).  This suggestion
was produced using the :induction rules PROPERP and REV.  If we let
 (:P Z) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP Z)) (:P Z))
     (IMPLIES (AND (CONSP Z) (:P (CDR Z)))
              (:P Z))).
This induction is justified by the same argument used to admit REV,
namely, the measure (ACL2-COUNT Z) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following three nontautological subgoals.

Subgoal *1/3
(IMPLIES (AND (NOT (CONSP Z)) (PROPERP Z))
         (EQUAL (REV (REV Z)) Z)).

But simplification reduces this to T, using the :definition PROPERP,
the :executable-counterparts of CONSP, EQUAL and REV and primitive
type reasoning.

Subgoal *1/2
(IMPLIES (AND (CONSP Z)
              (EQUAL (REV (REV (CDR Z))) (CDR Z))
              (PROPERP Z))
         (EQUAL (REV (REV Z)) Z)).

But simplification reduces this to T, using the :definitions APP, PROPERP
and REV, the :executable-counterparts of CONSP and REV, primitive type
reasoning and the :rewrite rules CAR-CDR-ELIM, CAR-CONS, CDR-CONS and
REV-APP.

Subgoal *1/1
(IMPLIES (AND (CONSP Z)
              (NOT (PROPERP (CDR Z)))
              (PROPERP Z))
         (EQUAL (REV (REV Z)) Z)).

But simplification reduces this to T, using the :definition PROPERP.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM REV-REV ...)
Rules: ((:DEFINITION APP)
        (:DEFINITION PROPERP)
        (:DEFINITION REV)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART REV)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION PROPERP)
        (:INDUCTION REV)
        (:REWRITE CAR-CDR-ELIM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE REV-APP))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
REV-REV


ACL2 >>(DEFTHM TRIPLE-REV
               (EQUAL (REV (REV (REV A))) (REV A)))

But simplification reduces this to T, using primitive type reasoning
and the :rewrite rules PROPERP-REV and REV-REV.

Q.E.D.

Summary
Form:  ( DEFTHM TRIPLE-REV ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE PROPERP-REV)
        (:REWRITE REV-REV))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TRIPLE-REV


ACL2 >>(DEFTHM MEMP-REV
               (EQUAL (MEMP E (REV X)) (MEMP E X)))

Name the formula above *1.

Perhaps we can prove *1 by induction.  Two induction schemes are suggested
by this conjecture.  Subsumption reduces that number to one.  

We will induct according to a scheme suggested by (MEMP E X).  This
suggestion was produced using the :induction rules MEMP and REV.  If
we let  (:P E X) denote *1 above then the induction scheme we'll use
is
(AND (IMPLIES (NOT (CONSP X)) (:P E X))
     (IMPLIES (AND (CONSP X)
                   (NOT (EQUAL E (CAR X)))
                   (:P E (CDR X)))
              (:P E X))
     (IMPLIES (AND (CONSP X) (EQUAL E (CAR X)))
              (:P E X))).
This induction is justified by the same argument used to admit MEMP,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following three nontautological subgoals.

Subgoal *1/3
(IMPLIES (NOT (CONSP X))
         (EQUAL (MEMP E (REV X)) (MEMP E X))).

But simplification reduces this to T, using the :definitions MEMP and
REV and the :executable-counterparts of CONSP and EQUAL.

Subgoal *1/2
(IMPLIES (AND (CONSP X)
              (NOT (EQUAL E (CAR X)))
              (EQUAL (MEMP E (REV (CDR X)))
                     (MEMP E (CDR X))))
         (EQUAL (MEMP E (REV X)) (MEMP E X))).

But simplification reduces this to T, using the :definitions MEMP and
REV, the :executable-counterpart of CONSP, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS and MEMP-APP and the :type-prescription
rule MEMP.

Subgoal *1/1
(IMPLIES (AND (CONSP X) (EQUAL E (CAR X)))
         (EQUAL (MEMP E (REV X)) (MEMP E X))).

But simplification reduces this to T, using the :definitions MEMP and
REV, the :executable-counterpart of EQUAL, primitive type reasoning,
the :rewrite rules CAR-CONS and MEMP-APP and the :type-prescription
rule MEMP.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM MEMP-REV ...)
Rules: ((:DEFINITION MEMP)
        (:DEFINITION REV)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION MEMP)
        (:INDUCTION REV)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE MEMP-APP)
        (:TYPE-PRESCRIPTION MEMP))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MEMP-REV


ACL2 >>(DEFTHM MEMP-DUP
               (EQUAL (MEMP E (DUP X)) (MEMP E X)))

Name the formula above *1.

Perhaps we can prove *1 by induction.  Two induction schemes are suggested
by this conjecture.  Subsumption reduces that number to one.  

We will induct according to a scheme suggested by (MEMP E X).  This
suggestion was produced using the :induction rules DUP and MEMP.  If
we let  (:P E X) denote *1 above then the induction scheme we'll use
is
(AND (IMPLIES (NOT (CONSP X)) (:P E X))
     (IMPLIES (AND (CONSP X)
                   (NOT (EQUAL E (CAR X)))
                   (:P E (CDR X)))
              (:P E X))
     (IMPLIES (AND (CONSP X) (EQUAL E (CAR X)))
              (:P E X))).
This induction is justified by the same argument used to admit MEMP,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following three nontautological subgoals.

Subgoal *1/3
(IMPLIES (NOT (CONSP X))
         (EQUAL (MEMP E (DUP X)) (MEMP E X))).

But simplification reduces this to T, using the :definitions DUP and
MEMP and the :executable-counterparts of CONSP and EQUAL.

Subgoal *1/2
(IMPLIES (AND (CONSP X)
              (NOT (EQUAL E (CAR X)))
              (EQUAL (MEMP E (DUP (CDR X)))
                     (MEMP E (CDR X))))
         (EQUAL (MEMP E (DUP X)) (MEMP E X))).

But simplification reduces this to T, using the :definitions DUP and
MEMP, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-
CONS and the :type-prescription rule DUP.

Subgoal *1/1
(IMPLIES (AND (CONSP X) (EQUAL E (CAR X)))
         (EQUAL (MEMP E (DUP X)) (MEMP E X))).

But simplification reduces this to T, using the :definitions DUP and
MEMP, the :executable-counterpart of EQUAL, primitive type reasoning,
the :rewrite rule CAR-CONS and the :type-prescription rule DUP.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM MEMP-DUP ...)
Rules: ((:DEFINITION DUP)
        (:DEFINITION MEMP)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION DUP)
        (:INDUCTION MEMP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION DUP))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
MEMP-DUP


ACL2 >>(DEFTHM COMPLICATED-MEMP-THEOREM
               (IMPLIES (MEMP E C)
                        (MEMP E (REV (DUP (DUP C)))))
               :RULE-CLASSES NIL)

But we reduce the conjecture to T, by the simple :rewrite rules MEMP-
DUP and MEMP-REV.

Q.E.D.

Summary
Form:  ( DEFTHM COMPLICATED-MEMP-THEOREM ...)
Rules: ((:REWRITE MEMP-DUP)
        (:REWRITE MEMP-REV))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
COMPLICATED-MEMP-THEOREM


ACL2 >>(DEFUN LEAVES (X)
              (IF (CONSP X)
                  (APP (LEAVES (CAR X)) (LEAVES (CDR X)))
                  (CONS X NIL)))

This event is redundant.  See :DOC redundant-events.

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


ACL2 >>(DEFTHM LEAVES-SWAPTREE
               (EQUAL (LEAVES (SWAPTREE X))
                      (REV (LEAVES X))))

Name the formula above *1.

Perhaps we can prove *1 by induction.  Two induction schemes are suggested
by this conjecture.  Subsumption reduces that number to one.  

We will induct according to a scheme suggested by (LEAVES X).  This
suggestion was produced using the :induction rules LEAVES and SWAPTREE.
If we let  (:P X) denote *1 above then the induction scheme we'll use
is
(AND (IMPLIES (NOT (CONSP X)) (:P X))
     (IMPLIES (AND (CONSP X)
                   (:P (CAR X))
                   (:P (CDR X)))
              (:P X))).
This induction is justified by the same argument used to admit LEAVES,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.

Subgoal *1/2
(IMPLIES (NOT (CONSP X))
         (EQUAL (LEAVES (SWAPTREE X))
                (REV (LEAVES X)))).

But simplification reduces this to T, using the :definitions APP, LEAVES,
REV and SWAPTREE, the :executable-counterparts of CONSP and REV, primitive
type reasoning and the :rewrite rules CAR-CONS and CDR-CONS.

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (EQUAL (LEAVES (SWAPTREE (CAR X)))
                     (REV (LEAVES (CAR X))))
              (EQUAL (LEAVES (SWAPTREE (CDR X)))
                     (REV (LEAVES (CDR X)))))
         (EQUAL (LEAVES (SWAPTREE X))
                (REV (LEAVES X)))).

But simplification reduces this to T, using the :definitions LEAVES
and SWAPTREE, primitive type reasoning and the :rewrite rules CAR-CONS,
CDR-CONS and REV-APP.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM LEAVES-SWAPTREE ...)
Rules: ((:DEFINITION APP)
        (:DEFINITION LEAVES)
        (:DEFINITION REV)
        (:DEFINITION SWAPTREE)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART REV)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION LEAVES)
        (:INDUCTION SWAPTREE)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE REV-APP))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LEAVES-SWAPTREE


ACL2 >>(DEFTHM SUBP-CDR
               (IMPLIES (SUBP X (CDR Y)) (SUBP X Y)))

The destructor terms (CAR Y) and (CDR Y) can be eliminated by using
CAR-CDR-ELIM to replace Y by (CONS Y1 Y2), (CAR Y) by Y1 and (CDR Y)
by Y2.  This produces the following two goals.

Subgoal 2
(IMPLIES (AND (NOT (CONSP Y)) (SUBP X (CDR Y)))
         (SUBP X Y)).

But simplification reduces this to T, using the :definitions MEMP and
SUBP, the :executable-counterpart of CONSP and the :rewrite rule DEFAULT-
CDR.

Subgoal 1
(IMPLIES (AND (CONSP (CONS Y1 Y2)) (SUBP X Y2))
         (SUBP X (CONS Y1 Y2))).

This simplifies, using primitive type reasoning, to

Subgoal 1'
(IMPLIES (SUBP X Y2)
         (SUBP X (CONS Y1 Y2))).

Normally we would attempt to prove this formula by induction.  However,
we prefer in this instance to focus on the original input conjecture
rather than this simplified special case.  We therefore abandon our
previous work on this conjecture and reassign the name *1 to the original
conjecture.  (See :DOC otf-flg.)

Perhaps we can prove *1 by induction.  Two induction schemes are suggested
by this conjecture.  These merge into one derived induction scheme.

We will induct according to a scheme suggested by (SUBP X Y).  This
suggestion was produced using the :induction rule SUBP.  If we let
 (:P X Y) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P X Y))
     (IMPLIES (AND (CONSP X) (NOT (MEMP (CAR X) Y)))
              (:P X Y))
     (IMPLIES (AND (CONSP X)
                   (MEMP (CAR X) Y)
                   (:P (CDR X) Y))
              (:P X Y))).
This induction is justified by the same argument used to admit SUBP,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following three nontautological subgoals.

Subgoal *1/3
(IMPLIES (NOT (CONSP X))
         (IMPLIES (SUBP X (CDR Y)) (SUBP X Y))).

By case analysis we reduce the conjecture to

Subgoal *1/3'
(IMPLIES (AND (NOT (CONSP X)) (SUBP X (CDR Y)))
         (SUBP X Y)).

But simplification reduces this to T, using the :definition SUBP.

Subgoal *1/2
(IMPLIES (AND (CONSP X) (NOT (MEMP (CAR X) Y)))
         (IMPLIES (SUBP X (CDR Y)) (SUBP X Y))).

By case analysis we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (NOT (MEMP (CAR X) Y))
              (SUBP X (CDR Y)))
         (SUBP X Y)).

But simplification reduces this to T, using the :definitions MEMP and
SUBP, the :executable-counterpart of CONSP and the :rewrite rule DEFAULT-
CDR.

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (MEMP (CAR X) Y)
              (IMPLIES (SUBP (CDR X) (CDR Y))
                       (SUBP (CDR X) Y)))
         (IMPLIES (SUBP X (CDR Y)) (SUBP X Y))).

By case analysis we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP X)
              (MEMP (CAR X) Y)
              (IMPLIES (SUBP (CDR X) (CDR Y))
                       (SUBP (CDR X) Y))
              (SUBP X (CDR Y)))
         (SUBP X Y)).

But simplification reduces this to T, using the :definitions MEMP and
SUBP, primitive type reasoning and the :type-prescription rules MEMP
and SUBP.

That completes the proof of *1.

Q.E.D.

The storage of SUBP-CDR depends upon the :type-prescription rule SUBP.

Summary
Form:  ( DEFTHM SUBP-CDR ...)
Rules: ((:DEFINITION MEMP)
        (:DEFINITION NOT)
        (:DEFINITION SUBP)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SUBP)
        (:REWRITE DEFAULT-CDR)
        (:TYPE-PRESCRIPTION MEMP)
        (:TYPE-PRESCRIPTION SUBP))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
SUBP-CDR


ACL2 >>(DEFTHM SUBP-REFLEXIVE (SUBP X X))

Name the formula above *1.

Perhaps we can prove *1 by induction.  One induction scheme is suggested
by this conjecture.  

We will induct according to a scheme suggested by (SUBP X X).  This
suggestion was produced using the :induction rule SUBP.  If we let
 (:P X) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P X))
     (IMPLIES (AND (CONSP X) (NOT (MEMP (CAR X) X)))
              (:P X))
     (IMPLIES (AND (CONSP X)
                   (MEMP (CAR X) X)
                   (:P (CDR X)))
              (:P X))).
This induction is justified by the same argument used to admit SUBP,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following three nontautological subgoals.

Subgoal *1/3
(IMPLIES (NOT (CONSP X)) (SUBP X X)).

But simplification reduces this to T, using the :definition SUBP, the
:executable-counterpart of CDR and the :rewrite rules DEFAULT-CDR and
SUBP-CDR.

Subgoal *1/2
(IMPLIES (AND (CONSP X) (NOT (MEMP (CAR X) X)))
         (SUBP X X)).

But simplification reduces this to T, using the :definition MEMP and
primitive type reasoning.

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (MEMP (CAR X) X)
              (SUBP (CDR X) (CDR X)))
         (SUBP X X)).

But simplification reduces this to T, using the :definitions MEMP and
SUBP, primitive type reasoning, the :rewrite rule SUBP-CDR and the
:type-prescription rule SUBP.

That completes the proof of *1.

Q.E.D.

The storage of SUBP-REFLEXIVE depends upon the :type-prescription rule
SUBP.

Summary
Form:  ( DEFTHM SUBP-REFLEXIVE ...)
Rules: ((:DEFINITION MEMP)
        (:DEFINITION SUBP)
        (:EXECUTABLE-COUNTERPART CDR)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SUBP)
        (:REWRITE DEFAULT-CDR)
        (:REWRITE SUBP-CDR)
        (:TYPE-PRESCRIPTION SUBP))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
SUBP-REFLEXIVE


ACL2 >>(DEFTHM SUBP-INT
               (IMPLIES (AND (PROPERP X) (SUBP X Y))
                        (EQUAL (INT X Y) X)))
[SGC for 439 CONS pages..(8013 writable)..(T=1).GC finished]

Name the formula above *1.

Perhaps we can prove *1 by induction.  Three induction schemes are
suggested by this conjecture.  Subsumption reduces that number to one.

We will induct according to a scheme suggested by (INT X Y).  This
suggestion was produced using the :induction rules INT, PROPERP and
SUBP.  If we let  (:P X Y) denote *1 above then the induction scheme
we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P X Y))
     (IMPLIES (AND (CONSP X)
                   (NOT (MEMP (CAR X) Y))
                   (:P (CDR X) Y))
              (:P X Y))
     (IMPLIES (AND (CONSP X)
                   (MEMP (CAR X) Y)
                   (:P (CDR X) Y))
              (:P X Y))).
This induction is justified by the same argument used to admit INT,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following seven nontautological subgoals.

Subgoal *1/7
(IMPLIES (AND (NOT (CONSP X))
              (PROPERP X)
              (SUBP X Y))
         (EQUAL (INT X Y) X)).

But simplification reduces this to T, using the :definitions INT, PROPERP
and SUBP, the :executable-counterparts of CONSP and EQUAL, primitive
type reasoning and the :rewrite rule SUBP-CDR.

Subgoal *1/6
(IMPLIES (AND (CONSP X)
              (NOT (MEMP (CAR X) Y))
              (EQUAL (INT (CDR X) Y) (CDR X))
              (PROPERP X)
              (SUBP X Y))
         (EQUAL (INT X Y) X)).

But simplification reduces this to T, using the :definitions PROPERP
and SUBP.

Subgoal *1/5
(IMPLIES (AND (CONSP X)
              (NOT (MEMP (CAR X) Y))
              (NOT (SUBP (CDR X) Y))
              (PROPERP X)
              (SUBP X Y))
         (EQUAL (INT X Y) X)).

But simplification reduces this to T, using the :definitions PROPERP
and SUBP.

Subgoal *1/4
(IMPLIES (AND (CONSP X)
              (NOT (MEMP (CAR X) Y))
              (NOT (PROPERP (CDR X)))
              (PROPERP X)
              (SUBP X Y))
         (EQUAL (INT X Y) X)).

But simplification reduces this to T, using the :definition PROPERP.

Subgoal *1/3
(IMPLIES (AND (CONSP X)
              (MEMP (CAR X) Y)
              (EQUAL (INT (CDR X) Y) (CDR X))
              (PROPERP X)
              (SUBP X Y))
         (EQUAL (INT X Y) X)).

But simplification reduces this to T, using the :definitions INT, PROPERP
and SUBP, primitive type reasoning, the :rewrite rule CAR-CDR-ELIM
and the :type-prescription rule MEMP.

Subgoal *1/2
(IMPLIES (AND (CONSP X)
              (MEMP (CAR X) Y)
              (NOT (SUBP (CDR X) Y))
              (PROPERP X)
              (SUBP X Y))
         (EQUAL (INT X Y) X)).

But simplification reduces this to T, using the :definitions PROPERP
and SUBP and the :type-prescription rule MEMP.

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (MEMP (CAR X) Y)
              (NOT (PROPERP (CDR X)))
              (PROPERP X)
              (SUBP X Y))
         (EQUAL (INT X Y) X)).

But simplification reduces this to T, using the :definition PROPERP.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM SUBP-INT ...)
Rules: ((:DEFINITION INT)
        (:DEFINITION PROPERP)
        (:DEFINITION SUBP)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION INT)
        (:INDUCTION PROPERP)
        (:INDUCTION SUBP)
        (:REWRITE CAR-CDR-ELIM)
        (:REWRITE SUBP-CDR)
        (:TYPE-PRESCRIPTION MEMP))
Warnings:  None
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
SUBP-INT


ACL2 >>(DEFTHM INT-X-X
               (IMPLIES (PROPERP X)
                        (EQUAL (INT X X) X)))

But simplification reduces this to T, using primitive type reasoning,
the :rewrite rules SUBP-INT and SUBP-REFLEXIVE and the :type-prescription
rule PROPERP.

Q.E.D.

Summary
Form:  ( DEFTHM INT-X-X ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE SUBP-INT)
        (:REWRITE SUBP-REFLEXIVE)
        (:TYPE-PRESCRIPTION PROPERP))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
INT-X-X


ACL2 >>(DEFTHM MEMP-SUBP
               (IMPLIES (AND (SUBP Y Z) (MEMP E Y))
                        (MEMP E Z)))

ACL2 Warning [Free] in ( DEFTHM MEMP-SUBP ...):  The :REWRITE rule
generated from MEMP-SUBP contains the free variable Y.  This variable
will be chosen by searching for an instance of (SUBP Y Z) among the
hypotheses of the conjecture being rewritten.  This is generally a
severe restriction on the applicability of the :REWRITE rule.  See
:DOC free-variables.


Name the formula above *1.

Perhaps we can prove *1 by induction.  Three induction schemes are
suggested by this conjecture.  These merge into two derived induction
schemes.  However, one of these is flawed and so we are left with one
viable candidate.  

We will induct according to a scheme suggested by (MEMP E Y), but modified
to accommodate (SUBP Y Z).  These suggestions were produced using the
:induction rules MEMP and SUBP.  If we let  (:P E Y Z) denote *1 above
then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP Y)) (:P E Y Z))
     (IMPLIES (AND (CONSP Y)
                   (NOT (EQUAL E (CAR Y)))
                   (:P E (CDR Y) Z))
              (:P E Y Z))
     (IMPLIES (AND (CONSP Y) (EQUAL E (CAR Y)))
              (:P E Y Z))).
This induction is justified by the same argument used to admit MEMP,
namely, the measure (ACL2-COUNT Y) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following four nontautological subgoals.

Subgoal *1/4
(IMPLIES (AND (NOT (CONSP Y))
              (SUBP Y Z)
              (MEMP E Y))
         (MEMP E Z)).

But simplification reduces this to T, using the :definitions MEMP and
SUBP and the :rewrite rule SUBP-CDR.

Subgoal *1/3
(IMPLIES (AND (CONSP Y)
              (NOT (EQUAL E (CAR Y)))
              (NOT (MEMP E (CDR Y)))
              (SUBP Y Z)
              (MEMP E Y))
         (MEMP E Z)).

But simplification reduces this to T, using the :definitions MEMP and
SUBP and primitive type reasoning.

Subgoal *1/2
(IMPLIES (AND (CONSP Y)
              (NOT (EQUAL E (CAR Y)))
              (NOT (SUBP (CDR Y) Z))
              (SUBP Y Z)
              (MEMP E Y))
         (MEMP E Z)).

But simplification reduces this to T, using the :definition SUBP.

Subgoal *1/1
(IMPLIES (AND (CONSP Y)
              (EQUAL E (CAR Y))
              (SUBP Y Z)
              (MEMP E Y))
         (MEMP E Z)).

But simplification reduces this to T, using the :definition SUBP.

That completes the proof of *1.

Q.E.D.

The storage of MEMP-SUBP depends upon the :type-prescription rule MEMP.

Summary
Form:  ( DEFTHM MEMP-SUBP ...)
Rules: ((:DEFINITION MEMP)
        (:DEFINITION SUBP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION MEMP)
        (:INDUCTION SUBP)
        (:REWRITE SUBP-CDR)
        (:TYPE-PRESCRIPTION MEMP))
Warnings:  Free
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
MEMP-SUBP


ACL2 >>(DEFTHM SUBP-TRANSITIVE
               (IMPLIES (AND (SUBP X Y) (SUBP Y Z))
                        (SUBP X Z)))

ACL2 Warning [Free] in ( DEFTHM SUBP-TRANSITIVE ...):  The :REWRITE
rule generated from SUBP-TRANSITIVE contains the free variable Y. 
This variable will be chosen by searching for an instance of (SUBP X Y)
among the hypotheses of the conjecture being rewritten.  This is generally
a severe restriction on the applicability of the :REWRITE rule.  See
:DOC free-variables.


Name the formula above *1.

Perhaps we can prove *1 by induction.  Three induction schemes are
suggested by this conjecture.  These merge into two derived induction
schemes.  However, one of these is flawed and so we are left with one
viable candidate.  

We will induct according to a scheme suggested by (SUBP X Z), but modified
to accommodate (SUBP X Y).  These suggestions were produced using the
:induction rule SUBP.  If we let  (:P X Y Z) denote *1 above then the
induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P X Y Z))
     (IMPLIES (AND (CONSP X) (NOT (MEMP (CAR X) Z)))
              (:P X Y Z))
     (IMPLIES (AND (CONSP X)
                   (MEMP (CAR X) Z)
                   (:P (CDR X) Y Z))
              (:P X Y Z))).
This induction is justified by the same argument used to admit SUBP,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following four nontautological subgoals.

Subgoal *1/4
(IMPLIES (AND (NOT (CONSP X))
              (SUBP X Y)
              (SUBP Y Z))
         (SUBP X Z)).

But simplification reduces this to T, using the :definition SUBP and
the :rewrite rule SUBP-CDR.

Subgoal *1/3
(IMPLIES (AND (CONSP X)
              (NOT (MEMP (CAR X) Z))
              (SUBP X Y)
              (SUBP Y Z))
         (SUBP X Z)).

This simplifies, using the :definition SUBP, the :rewrite rule MEMP-
SUBP and the :type-prescription rules MEMP and SUBP, to

Subgoal *1/3'
(IMPLIES (AND (CONSP X)
              (NOT (MEMP (CAR X) Z))
              (MEMP (CAR X) Y)
              (SUBP (CDR X) Y)
              (SUBP Y Z))
         (SUBP (CDR X) Z)).

But simplification reduces this to T, using the :rewrite rule MEMP-
SUBP and the :type-prescription rules MEMP and SUBP.

Subgoal *1/2
(IMPLIES (AND (CONSP X)
              (MEMP (CAR X) Z)
              (SUBP (CDR X) Z)
              (SUBP X Y)
              (SUBP Y Z))
         (SUBP X Z)).

But simplification reduces this to T, using the :definition SUBP, the
:rewrite rule MEMP-SUBP and the :type-prescription rules MEMP and SUBP.

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (MEMP (CAR X) Z)
              (NOT (SUBP (CDR X) Y))
              (SUBP X Y)
              (SUBP Y Z))
         (SUBP X Z)).

But simplification reduces this to T, using the :definition SUBP.

That completes the proof of *1.

Q.E.D.

The storage of SUBP-TRANSITIVE depends upon the :type-prescription
rule SUBP.

Summary
Form:  ( DEFTHM SUBP-TRANSITIVE ...)
Rules: ((:DEFINITION SUBP)
        (:INDUCTION SUBP)
        (:REWRITE MEMP-SUBP)
        (:REWRITE SUBP-CDR)
        (:TYPE-PRESCRIPTION MEMP)
        (:TYPE-PRESCRIPTION SUBP))
Warnings:  Free
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
SUBP-TRANSITIVE


ACL2 >>(DEFTHM SUBP-APP-1
               (EQUAL (SUBP (APP A B) C)
                      (AND (SUBP A C) (SUBP B C))))

This simplifies, using trivial observations, to the following two conjectures.

Subgoal 2
(IMPLIES (SUBP A C)
         (EQUAL (SUBP (APP A B) C) (SUBP B C))).

Name the formula above *1.

Subgoal 1
(IMPLIES (NOT (SUBP A C))
         (EQUAL (SUBP (APP A B) C) NIL)).

This simplifies, using primitive type reasoning, to

Subgoal 1'
(IMPLIES (NOT (SUBP A C))
         (NOT (SUBP (APP A B) C))).

Normally we would attempt to prove this formula by induction.  However,
we prefer in this instance to focus on the original input conjecture
rather than this simplified special case.  We therefore abandon our
previous work on this conjecture and reassign the name *1 to the original
conjecture.  (See :DOC otf-flg.)

Perhaps we can prove *1 by induction.  Three induction schemes are
suggested by this conjecture.  These merge into two derived induction
schemes.  However, one of these is flawed and so we are left with one
viable candidate.  

We will induct according to a scheme suggested by (SUBP A C), but modified
to accommodate (APP A B).  These suggestions were produced using the
:induction rules APP and SUBP.  If we let  (:P A B C) denote *1 above
then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A B C))
     (IMPLIES (AND (CONSP A) (NOT (MEMP (CAR A) C)))
              (:P A B C))
     (IMPLIES (AND (CONSP A)
                   (MEMP (CAR A) C)
                   (:P (CDR A) B C))
              (:P A B C))).
This induction is justified by the same argument used to admit SUBP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following three nontautological subgoals.

Subgoal *1/3
(IMPLIES (NOT (CONSP A))
         (EQUAL (SUBP (APP A B) C)
                (AND (SUBP A C) (SUBP B C)))).

But simplification reduces this to T, using the :definitions APP and
SUBP, primitive type reasoning and the :rewrite rule SUBP-CDR.

Subgoal *1/2
(IMPLIES (AND (CONSP A) (NOT (MEMP (CAR A) C)))
         (EQUAL (SUBP (APP A B) C)
                (AND (SUBP A C) (SUBP B C)))).

But simplification reduces this to T, using the :definitions APP and
SUBP, the :executable-counterpart of EQUAL, primitive type reasoning
and the :rewrite rule CAR-CONS.

Subgoal *1/1
(IMPLIES (AND (CONSP A)
              (MEMP (CAR A) C)
              (EQUAL (SUBP (APP (CDR A) B) C)
                     (AND (SUBP (CDR A) C) (SUBP B C))))
         (EQUAL (SUBP (APP A B) C)
                (AND (SUBP A C) (SUBP B C)))).

But simplification reduces this to T, using the :definitions APP and
SUBP, the :executable-counterpart of EQUAL, primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rules MEMP and SUBP.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM SUBP-APP-1 ...)
Rules: ((:DEFINITION APP)
        (:DEFINITION SUBP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION APP)
        (:INDUCTION SUBP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE SUBP-CDR)
        (:TYPE-PRESCRIPTION MEMP)
        (:TYPE-PRESCRIPTION SUBP))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
SUBP-APP-1


ACL2 >>(DEFTHM SUBP-APP-A-A (SUBP (APP A A) A))

ACL2 Warning [Subsume] in ( DEFTHM SUBP-APP-A-A ...):  The previously
added rule SUBP-APP-1 subsumes the newly proposed :REWRITE rule SUBP-
APP-A-A, in the sense that the old rule rewrites a more general target.
Because the new rule will be tried first, it may nonetheless find application.


But we reduce the conjecture to T, by the :executable-counterpart of
IF and the simple :rewrite rules SUBP-APP-1 and SUBP-REFLEXIVE.

Q.E.D.

The storage of SUBP-APP-A-A depends upon the :type-prescription rule
SUBP.

Summary
Form:  ( DEFTHM SUBP-APP-A-A ...)
Rules: ((:EXECUTABLE-COUNTERPART IF)
        (:REWRITE SUBP-APP-1)
        (:REWRITE SUBP-REFLEXIVE)
        (:TYPE-PRESCRIPTION SUBP))
Warnings:  Subsume
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SUBP-APP-A-A


ACL2 >>(DEFUN SETEQP (X Y)
              (AND (SUBP X Y) (SUBP Y X)))

Since SETEQP is non-recursive, its admission is trivial.  We observe
that the type of SETEQP is described by the theorem 
(OR (EQUAL (SETEQP X Y) T) (EQUAL (SETEQP X Y) NIL)).  We used the
:type-prescription rule SUBP.

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


ACL2 >>(DEFTHM SUBP-APP-2
               (IMPLIES (SUBP A B) (SUBP A (APP B C))))

Name the formula above *1.

Perhaps we can prove *1 by induction.  Three induction schemes are
suggested by this conjecture.  These merge into two derived induction
schemes.  However, one of these is flawed and so we are left with one
viable candidate.  

We will induct according to a scheme suggested by (SUBP A (APP B C)),
but modified to accommodate (SUBP A B).  These suggestions were produced
using the :induction rule SUBP.  If we let  (:P A B C) denote *1 above
then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A B C))
     (IMPLIES (AND (CONSP A)
                   (NOT (MEMP (CAR A) (APP B C))))
              (:P A B C))
     (IMPLIES (AND (CONSP A)
                   (MEMP (CAR A) (APP B C))
                   (:P (CDR A) B C))
              (:P A B C))).
This induction is justified by the same argument used to admit SUBP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following four nontautological subgoals.

Subgoal *1/4
(IMPLIES (AND (NOT (CONSP A)) (SUBP A B))
         (SUBP A (APP B C))).

But simplification reduces this to T, using the :definition SUBP and
the :rewrite rule SUBP-CDR.

Subgoal *1/3
(IMPLIES (AND (CONSP A)
              (NOT (MEMP (CAR A) (APP B C)))
              (SUBP A B))
         (SUBP A (APP B C))).

But simplification reduces this to T, using the :definition MEMP, primitive
type reasoning, the :rewrite rules MEMP-APP and MEMP-SUBP and the :type-
prescription rule SUBP.

Subgoal *1/2
(IMPLIES (AND (CONSP A)
              (MEMP (CAR A) (APP B C))
              (SUBP (CDR A) (APP B C))
              (SUBP A B))
         (SUBP A (APP B C))).

But simplification reduces this to T, using the :definitions MEMP and
SUBP, primitive type reasoning, the :rewrite rules MEMP-APP and MEMP-
SUBP and the :type-prescription rules MEMP and SUBP.

Subgoal *1/1
(IMPLIES (AND (CONSP A)
              (MEMP (CAR A) (APP B C))
              (NOT (SUBP (CDR A) B))
              (SUBP A B))
         (SUBP A (APP B C))).

But simplification reduces this to T, using the :definitions MEMP and
SUBP, primitive type reasoning, the :rewrite rules MEMP-APP and MEMP-
SUBP and the :type-prescription rule SUBP.

That completes the proof of *1.

Q.E.D.

The storage of SUBP-APP-2 depends upon the :type-prescription rule
SUBP.

Summary
Form:  ( DEFTHM SUBP-APP-2 ...)
Rules: ((:DEFINITION MEMP)
        (:DEFINITION SUBP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SUBP)
        (:REWRITE MEMP-APP)
        (:REWRITE MEMP-SUBP)
        (:REWRITE SUBP-CDR)
        (:TYPE-PRESCRIPTION MEMP)
        (:TYPE-PRESCRIPTION SUBP))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
SUBP-APP-2


ACL2 >>(DEFTHM SETEQ-REV (SETEQP (REV A) A))

ACL2 Warning [Non-rec] in ( DEFTHM SETEQ-REV ...):  The :REWRITE rule
generated from SETEQ-REV will be triggered only by terms containing
the non-recursive function symbol SETEQP.  Unless this function is
disabled, SETEQ-REV is unlikely ever to be used.


By the simple :definition SETEQP we reduce the conjecture to the following
two conjectures.

Subgoal 2
(SUBP (REV A) A).

Name the formula above *1.

Subgoal 1
(SUBP A (REV A)).

Normally we would attempt to prove this formula by induction.  However,
we prefer in this instance to focus on the original input conjecture
rather than this simplified special case.  We therefore abandon our
previous work on this conjecture and reassign the name *1 to the original
conjecture.  (See :DOC otf-flg.)

Perhaps we can prove *1 by induction.  One induction scheme is suggested
by this conjecture.  

We will induct according to a scheme suggested by (REV A).  This suggestion
was produced using the :induction rule REV.  If we let  (:P A) denote
*1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A))
     (IMPLIES (AND (CONSP A) (:P (CDR A)))
              (:P A))).
This induction is justified by the same argument used to admit REV,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.

Subgoal *1/2
(IMPLIES (NOT (CONSP A))
         (SETEQP (REV A) A)).

But simplification reduces this to T, using the :definitions REV, SETEQP
and SUBP, the :executable-counterparts of CDR and SUBP and the :rewrite
rules DEFAULT-CDR and SUBP-CDR.

Subgoal *1/1
(IMPLIES (AND (CONSP A)
              (SETEQP (REV (CDR A)) (CDR A)))
         (SETEQP (REV A) A)).

By the simple :definition SETEQP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP A)
              (SUBP (REV (CDR A)) (CDR A))
              (SUBP (CDR A) (REV (CDR A))))
         (SETEQP (REV A) A)).
[SGC for 439 CONS pages..(8014 writable)..(T=1).GC finished]

But simplification reduces this to T, using the :definitions MEMP,
REV, SETEQP and SUBP, the :executable-counterpart of CONSP, primitive
type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, MEMP-APP, MEMP-
REV, SUBP-APP-1, SUBP-APP-2 and SUBP-CDR and the :type-prescription
rule SUBP.

That completes the proof of *1.

Q.E.D.

The storage of SETEQ-REV depends upon the :type-prescription rule SETEQP.

Summary
Form:  ( DEFTHM SETEQ-REV ...)
Rules: ((:DEFINITION MEMP)
        (:DEFINITION NOT)
        (:DEFINITION REV)
        (:DEFINITION SETEQP)
        (:DEFINITION SUBP)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART SUBP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION REV)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE DEFAULT-CDR)
        (:REWRITE MEMP-APP)
        (:REWRITE MEMP-REV)
        (:REWRITE SUBP-APP-1)
        (:REWRITE SUBP-APP-2)
        (:REWRITE SUBP-CDR)
        (:TYPE-PRESCRIPTION SETEQP)
        (:TYPE-PRESCRIPTION SUBP))
Warnings:  Non-rec
Time:  0.02 seconds (prove: 0.01, print: 0.01, other: 0.00)
SETEQ-REV


ACL2 >>(DEFTHM SUBP-APP-3
               (IMPLIES (SUBP A C) (SUBP A (APP B C))))

Name the formula above *1.

Perhaps we can prove *1 by induction.  Three induction schemes are
suggested by this conjecture.  These merge into two derived induction
schemes.  One of these has a score higher than the other.  

We will induct according to a scheme suggested by (SUBP A (APP B C)),
but modified to accommodate (SUBP A C).  These suggestions were produced
using the :induction rule SUBP.  If we let  (:P A B C) denote *1 above
then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A B C))
     (IMPLIES (AND (CONSP A)
                   (NOT (MEMP (CAR A) (APP B C))))
              (:P A B C))
     (IMPLIES (AND (CONSP A)
                   (MEMP (CAR A) (APP B C))
                   (:P (CDR A) B C))
              (:P A B C))).
This induction is justified by the same argument used to admit SUBP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following four nontautological subgoals.

Subgoal *1/4
(IMPLIES (AND (NOT (CONSP A)) (SUBP A C))
         (SUBP A (APP B C))).

But simplification reduces this to T, using the :definition SUBP and
the :rewrite rules SUBP-APP-2 and SUBP-CDR.

Subgoal *1/3
(IMPLIES (AND (CONSP A)
              (NOT (MEMP (CAR A) (APP B C)))
              (SUBP A C))
         (SUBP A (APP B C))).

But simplification reduces this to T, using the :definition MEMP, primitive
type reasoning, the :rewrite rules MEMP-APP and MEMP-SUBP and the :type-
prescription rule SUBP.

Subgoal *1/2
(IMPLIES (AND (CONSP A)
              (MEMP (CAR A) (APP B C))
              (SUBP (CDR A) (APP B C))
              (SUBP A C))
         (SUBP A (APP B C))).

But simplification reduces this to T, using the :definitions MEMP and
SUBP, primitive type reasoning, the :rewrite rules MEMP-APP and MEMP-
SUBP and the :type-prescription rules MEMP and SUBP.

Subgoal *1/1
(IMPLIES (AND (CONSP A)
              (MEMP (CAR A) (APP B C))
              (NOT (SUBP (CDR A) C))
              (SUBP A C))
         (SUBP A (APP B C))).

But simplification reduces this to T, using the :definitions MEMP and
SUBP, primitive type reasoning, the :rewrite rules MEMP-APP and MEMP-
SUBP and the :type-prescription rule SUBP.

That completes the proof of *1.

Q.E.D.

The storage of SUBP-APP-3 depends upon the :type-prescription rule
SUBP.

Summary
Form:  ( DEFTHM SUBP-APP-3 ...)
Rules: ((:DEFINITION MEMP)
        (:DEFINITION SUBP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SUBP)
        (:REWRITE MEMP-APP)
        (:REWRITE MEMP-SUBP)
        (:REWRITE SUBP-APP-2)
        (:REWRITE SUBP-CDR)
        (:TYPE-PRESCRIPTION MEMP)
        (:TYPE-PRESCRIPTION SUBP))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
SUBP-APP-3


ACL2 >>(DEFTHM APP-COMMUTATIVE
               (SETEQP (APP A B) (APP B A)))

ACL2 Warning [Non-rec] in ( DEFTHM APP-COMMUTATIVE ...):  The :REWRITE
rule generated from APP-COMMUTATIVE will be triggered only by terms
containing the non-recursive function symbol SETEQP.  Unless this function
is disabled, APP-COMMUTATIVE is unlikely ever to be used.


By the simple :definition SETEQP and the simple :rewrite rule SUBP-
APP-1 we reduce the conjecture to the following four conjectures.

Subgoal 4
(SUBP A (APP B A)).

But simplification reduces this to T, using the :rewrite rules SUBP-
APP-3 and SUBP-REFLEXIVE.

Subgoal 3
(SUBP B (APP B A)).

But simplification reduces this to T, using the :rewrite rules SUBP-
APP-2 and SUBP-REFLEXIVE.

Subgoal 2
(SUBP B (APP A B)).

But simplification reduces this to T, using the :rewrite rules SUBP-
APP-3 and SUBP-REFLEXIVE.

Subgoal 1
(SUBP A (APP A B)).

But simplification reduces this to T, using the :rewrite rules SUBP-
APP-2 and SUBP-REFLEXIVE.

Q.E.D.

The storage of APP-COMMUTATIVE depends upon the :type-prescription
rule SETEQP.

Summary
Form:  ( DEFTHM APP-COMMUTATIVE ...)
Rules: ((:DEFINITION SETEQP)
        (:REWRITE SUBP-APP-1)
        (:REWRITE SUBP-APP-2)
        (:REWRITE SUBP-APP-3)
        (:REWRITE SUBP-REFLEXIVE)
        (:TYPE-PRESCRIPTION SETEQP))
Warnings:  Non-rec
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
APP-COMMUTATIVE


ACL2 >>(DEFUN LIST-OF-ATOMSP (X)
              (IF (CONSP X)
                  (AND (NOT (CONSP (CAR X)))
                       (LIST-OF-ATOMSP (CDR X)))
                  T))

The admission of LIST-OF-ATOMSP is trivial, using the relation O< (which
is known to be well-founded on the domain recognized by O-P) and the
measure (ACL2-COUNT X).  We observe that the type of LIST-OF-ATOMSP
is described by the theorem 
(OR (EQUAL (LIST-OF-ATOMSP X) T) (EQUAL (LIST-OF-ATOMSP X) NIL)). 

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


ACL2 >>(DEFTHM LIST-OF-ATOMSP-APP
               (EQUAL (LIST-OF-ATOMSP (APP A B))
                      (AND (LIST-OF-ATOMSP A)
                           (LIST-OF-ATOMSP B))))

This simplifies, using trivial observations, to the following two conjectures.

Subgoal 2
(IMPLIES (LIST-OF-ATOMSP A)
         (EQUAL (LIST-OF-ATOMSP (APP A B))
                (LIST-OF-ATOMSP B))).

Name the formula above *1.

Subgoal 1
(IMPLIES (NOT (LIST-OF-ATOMSP A))
         (EQUAL (LIST-OF-ATOMSP (APP A B)) NIL)).

This simplifies, using primitive type reasoning, to

Subgoal 1'
(IMPLIES (NOT (LIST-OF-ATOMSP A))
         (NOT (LIST-OF-ATOMSP (APP A B)))).

Normally we would attempt to prove this formula by induction.  However,
we prefer in this instance to focus on the original input conjecture
rather than this simplified special case.  We therefore abandon our
previous work on this conjecture and reassign the name *1 to the original
conjecture.  (See :DOC otf-flg.)

Perhaps we can prove *1 by induction.  Three induction schemes are
suggested by this conjecture.  These merge into two derived induction
schemes.  However, one of these is flawed and so we are left with one
viable candidate.  

We will induct according to a scheme suggested by (LIST-OF-ATOMSP A),
but modified to accommodate (APP A B).  These suggestions were produced
using the :induction rules APP and LIST-OF-ATOMSP.  If we let  (:P A B)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A B))
     (IMPLIES (AND (CONSP A) (CONSP (CAR A)))
              (:P A B))
     (IMPLIES (AND (CONSP A)
                   (NOT (CONSP (CAR A)))
                   (:P (CDR A) B))
              (:P A B))).
This induction is justified by the same argument used to admit LIST-
OF-ATOMSP, namely, the measure (ACL2-COUNT A) is decreasing according
to the relation O< (which is known to be well-founded on the domain
recognized by O-P).  When applied to the goal at hand the above induction
scheme produces the following three nontautological subgoals.

Subgoal *1/3
(IMPLIES (NOT (CONSP A))
         (EQUAL (LIST-OF-ATOMSP (APP A B))
                (AND (LIST-OF-ATOMSP A)
                     (LIST-OF-ATOMSP B)))).

But simplification reduces this to T, using the :definitions APP and
LIST-OF-ATOMSP and primitive type reasoning.

Subgoal *1/2
(IMPLIES (AND (CONSP A) (CONSP (CAR A)))
         (EQUAL (LIST-OF-ATOMSP (APP A B))
                (AND (LIST-OF-ATOMSP A)
                     (LIST-OF-ATOMSP B)))).

But simplification reduces this to T, using the :definitions APP and
LIST-OF-ATOMSP, the :executable-counterpart of EQUAL, primitive type
reasoning and the :rewrite rule CAR-CONS.

Subgoal *1/1
(IMPLIES (AND (CONSP A)
              (NOT (CONSP (CAR A)))
              (EQUAL (LIST-OF-ATOMSP (APP (CDR A) B))
                     (AND (LIST-OF-ATOMSP (CDR A))
                          (LIST-OF-ATOMSP B))))
         (EQUAL (LIST-OF-ATOMSP (APP A B))
                (AND (LIST-OF-ATOMSP A)
                     (LIST-OF-ATOMSP B)))).

But simplification reduces this to T, using the :definitions APP and
LIST-OF-ATOMSP, the :executable-counterpart of EQUAL, primitive type
reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type-
prescription rule LIST-OF-ATOMSP.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM LIST-OF-ATOMSP-APP ...)
Rules: ((:DEFINITION APP)
        (:DEFINITION LIST-OF-ATOMSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION APP)
        (:INDUCTION LIST-OF-ATOMSP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION LIST-OF-ATOMSP))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LIST-OF-ATOMSP-APP


ACL2 >>(DEFTHM LIST-OF-ATOMSP-LEAVES
               (LIST-OF-ATOMSP (LEAVES X)))

Name the formula above *1.

Perhaps we can prove *1 by induction.  One induction scheme is suggested
by this conjecture.  

We will induct according to a scheme suggested by (LEAVES X).  This
suggestion was produced using the :induction rule LEAVES.  If we let
 (:P X) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P X))
     (IMPLIES (AND (CONSP X)
                   (:P (CAR X))
                   (:P (CDR X)))
              (:P X))).
This induction is justified by the same argument used to admit LEAVES,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.

Subgoal *1/2
(IMPLIES (NOT (CONSP X))
         (LIST-OF-ATOMSP (LEAVES X))).

But simplification reduces this to T, using the :definitions LEAVES
and LIST-OF-ATOMSP, the :executable-counterpart of LIST-OF-ATOMSP,
primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS.

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (LIST-OF-ATOMSP (LEAVES (CAR X)))
              (LIST-OF-ATOMSP (LEAVES (CDR X))))
         (LIST-OF-ATOMSP (LEAVES X))).

But simplification reduces this to T, using the :definition LEAVES,
the :rewrite rule LIST-OF-ATOMSP-APP and the :type-prescription rule
LIST-OF-ATOMSP.

That completes the proof of *1.

Q.E.D.

The storage of LIST-OF-ATOMSP-LEAVES depends upon the :type-prescription
rule LIST-OF-ATOMSP.

Summary
Form:  ( DEFTHM LIST-OF-ATOMSP-LEAVES ...)
Rules: ((:DEFINITION LEAVES)
        (:DEFINITION LIST-OF-ATOMSP)
        (:EXECUTABLE-COUNTERPART LIST-OF-ATOMSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION LEAVES)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE LIST-OF-ATOMSP-APP)
        (:TYPE-PRESCRIPTION LIST-OF-ATOMSP))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LIST-OF-ATOMSP-LEAVES


ACL2 >>(DEFTHM LEAVES-OF-LIST-OF-ATOMS
               (IMPLIES (AND (PROPERP X) (LIST-OF-ATOMSP X))
                        (EQUAL (LEAVES X) (APP X '(NIL)))))

Name the formula above *1.

Perhaps we can prove *1 by induction.  Four induction schemes are suggested
by this conjecture.  Subsumption reduces that number to two.  These
merge into one derived induction scheme.  

We will induct according to a scheme suggested by (LEAVES X).  This
suggestion was produced using the :induction rules APP, LEAVES, LIST-
OF-ATOMSP and PROPERP.  If we let  (:P X) denote *1 above then the
induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P X))
     (IMPLIES (AND (CONSP X)
                   (:P (CAR X))
                   (:P (CDR X)))
              (:P X))).
This induction is justified by the same argument used to admit LEAVES,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following ten nontautological subgoals.

Subgoal *1/10
(IMPLIES (AND (NOT (CONSP X))
              (PROPERP X)
              (LIST-OF-ATOMSP X))
         (EQUAL (LEAVES X) (APP X '(NIL)))).

But simplification reduces this to T, using the :definition PROPERP,
the :executable-counterparts of APP, CONSP, EQUAL, LEAVES, LIST-OF-
ATOMSP and NOT and primitive type reasoning.

Subgoal *1/9
(IMPLIES (AND (CONSP X)
              (EQUAL (LEAVES (CAR X))
                     (APP (CAR X) '(NIL)))
              (EQUAL (LEAVES (CDR X))
                     (APP (CDR X) '(NIL)))
              (PROPERP X)
              (LIST-OF-ATOMSP X))
         (EQUAL (LEAVES X) (APP X '(NIL)))).

This simplifies, using the :definitions APP, LEAVES, LIST-OF-ATOMSP
and PROPERP and primitive type reasoning, to

Subgoal *1/9'
(IMPLIES (AND (CONSP X)
              (EQUAL (LEAVES (CAR X))
                     (APP (CAR X) '(NIL)))
              (EQUAL (LEAVES (CDR X))
                     (APP (CDR X) '(NIL)))
              (PROPERP (CDR X))
              (NOT (CONSP (CAR X)))
              (LIST-OF-ATOMSP (CDR X)))
         (EQUAL (APP (LEAVES (CAR X)) (LEAVES (CDR X)))
                (CONS (CAR X) (LEAVES (CDR X))))).

But simplification reduces this to T, using the :definitions APP and
LEAVES, the :executable-counterparts of CAR, CDR, CONSP, EQUAL and
LEAVES, primitive type reasoning and the :rewrite rule CONS-EQUAL.

Subgoal *1/8
(IMPLIES (AND (CONSP X)
              (NOT (LIST-OF-ATOMSP (CAR X)))
              (EQUAL (LEAVES (CDR X))
                     (APP (CDR X) '(NIL)))
              (PROPERP X)
              (LIST-OF-ATOMSP X))
         (EQUAL (LEAVES X) (APP X '(NIL)))).

This simplifies, using the :definitions APP, LEAVES, LIST-OF-ATOMSP
and PROPERP and primitive type reasoning, to

Subgoal *1/8'
(IMPLIES (AND (CONSP X)
              (NOT (LIST-OF-ATOMSP (CAR X)))
              (EQUAL (LEAVES (CDR X))
                     (APP (CDR X) '(NIL)))
              (PROPERP (CDR X))
              (NOT (CONSP (CAR X)))
              (LIST-OF-ATOMSP (CDR X)))
         (EQUAL (APP (LEAVES (CAR X)) (LEAVES (CDR X)))
                (CONS (CAR X) (LEAVES (CDR X))))).

But simplification reduces this to T, using the :definition LIST-OF-
ATOMSP.

Subgoal *1/7
(IMPLIES (AND (CONSP X)
              (NOT (PROPERP (CAR X)))
              (EQUAL (LEAVES (CDR X))
                     (APP (CDR X) '(NIL)))
              (PROPERP X)
              (LIST-OF-ATOMSP X))
         (EQUAL (LEAVES X) (APP X '(NIL)))).

This simplifies, using the :definitions APP, LEAVES, LIST-OF-ATOMSP
and PROPERP and primitive type reasoning, to

Subgoal *1/7'
(IMPLIES (AND (CONSP X)
              (NOT (PROPERP (CAR X)))
              (EQUAL (LEAVES (CDR X))
                     (APP (CDR X) '(NIL)))
              (PROPERP (CDR X))
              (NOT (CONSP (CAR X)))
              (LIST-OF-ATOMSP (CDR X)))
         (EQUAL (APP (LEAVES (CAR X)) (LEAVES (CDR X)))
                (CONS (CAR X) (LEAVES (CDR X))))).

But simplification reduces this to T, using the :definitions APP, LEAVES
and PROPERP, the :executable-counterpart of CONSP, primitive type reasoning
and the :rewrite rules CAR-CONS and CDR-CONS.

Subgoal *1/6
(IMPLIES (AND (CONSP X)
              (EQUAL (LEAVES (CAR X))
                     (APP (CAR X) '(NIL)))
              (NOT (LIST-OF-ATOMSP (CDR X)))
              (PROPERP X)
              (LIST-OF-ATOMSP X))
         (EQUAL (LEAVES X) (APP X '(NIL)))).

But simplification reduces this to T, using the :definitions LIST-OF-
ATOMSP and PROPERP.

Subgoal *1/5
(IMPLIES (AND (CONSP X)
              (NOT (LIST-OF-ATOMSP (CAR X)))
              (NOT (LIST-OF-ATOMSP (CDR X)))
              (PROPERP X)
              (LIST-OF-ATOMSP X))
         (EQUAL (LEAVES X) (APP X '(NIL)))).

But simplification reduces this to T, using the :definitions LIST-OF-
ATOMSP and PROPERP.

Subgoal *1/4
(IMPLIES (AND (CONSP X)
              (NOT (PROPERP (CAR X)))
              (NOT (LIST-OF-ATOMSP (CDR X)))
              (PROPERP X)
              (LIST-OF-ATOMSP X))
         (EQUAL (LEAVES X) (APP X '(NIL)))).

But simplification reduces this to T, using the :definitions LIST-OF-
ATOMSP and PROPERP.

Subgoal *1/3
(IMPLIES (AND (CONSP X)
              (EQUAL (LEAVES (CAR X))
                     (APP (CAR X) '(NIL)))
              (NOT (PROPERP (CDR X)))
              (PROPERP X)
              (LIST-OF-ATOMSP X))
         (EQUAL (LEAVES X) (APP X '(NIL)))).

But simplification reduces this to T, using the :definition PROPERP.

Subgoal *1/2
(IMPLIES (AND (CONSP X)
              (NOT (LIST-OF-ATOMSP (CAR X)))
              (NOT (PROPERP (CDR X)))
              (PROPERP X)
              (LIST-OF-ATOMSP X))
         (EQUAL (LEAVES X) (APP X '(NIL)))).

But simplification reduces this to T, using the :definition PROPERP.

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (NOT (PROPERP (CAR X)))
              (NOT (PROPERP (CDR X)))
              (PROPERP X)
              (LIST-OF-ATOMSP X))
         (EQUAL (LEAVES X) (APP X '(NIL)))).

But simplification reduces this to T, using the :definition PROPERP.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM LEAVES-OF-LIST-OF-ATOMS ...)
Rules: ((:DEFINITION APP)
        (:DEFINITION LEAVES)
        (:DEFINITION LIST-OF-ATOMSP)
        (:DEFINITION PROPERP)
        (:EXECUTABLE-COUNTERPART APP)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART LEAVES)
        (:EXECUTABLE-COUNTERPART LIST-OF-ATOMSP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION APP)
        (:INDUCTION LEAVES)
        (:INDUCTION LIST-OF-ATOMSP)
        (:INDUCTION PROPERP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE CONS-EQUAL))
Warnings:  None
Time:  0.03 seconds (prove: 0.01, print: 0.01, other: 0.01)
LEAVES-OF-LIST-OF-ATOMS


ACL2 >>(DEFTHM PROPERP-LEAVES (PROPERP (LEAVES X)))

Name the formula above *1.

Perhaps we can prove *1 by induction.  One induction scheme is suggested
by this conjecture.  

We will induct according to a scheme suggested by (LEAVES X).  This
suggestion was produced using the :induction rule LEAVES.  If we let
 (:P X) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P X))
     (IMPLIES (AND (CONSP X)
                   (:P (CAR X))
                   (:P (CDR X)))
              (:P X))).
This induction is justified by the same argument used to admit LEAVES,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.

Subgoal *1/2
(IMPLIES (NOT (CONSP X))
         (PROPERP (LEAVES X))).

But simplification reduces this to T, using the :definitions LEAVES
and PROPERP, the :executable-counterpart of PROPERP, primitive type
reasoning and the :rewrite rule CDR-CONS.

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (PROPERP (LEAVES (CAR X)))
              (PROPERP (LEAVES (CDR X))))
         (PROPERP (LEAVES X))).

But simplification reduces this to T, using the :definition LEAVES,
the :rewrite rule PROPERP-APP and the :type-prescription rule PROPERP.

That completes the proof of *1.

Q.E.D.

The storage of PROPERP-LEAVES depends upon the :type-prescription rule
PROPERP.

Summary
Form:  ( DEFTHM PROPERP-LEAVES ...)
Rules: ((:DEFINITION LEAVES)
        (:DEFINITION PROPERP)
        (:EXECUTABLE-COUNTERPART PROPERP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION LEAVES)
        (:REWRITE CDR-CONS)
        (:REWRITE PROPERP-APP)
        (:TYPE-PRESCRIPTION PROPERP))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
PROPERP-LEAVES


ACL2 >>(DEFTHM LEAVES-LEAVES
               (EQUAL (LEAVES (LEAVES X))
                      (APP (LEAVES X) '(NIL))))

But simplification reduces this to T, using primitive type reasoning
and the :rewrite rules LEAVES-OF-LIST-OF-ATOMS, LIST-OF-ATOMSP-LEAVES
and PROPERP-LEAVES.

Q.E.D.

Summary
Form:  ( DEFTHM LEAVES-LEAVES ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE LEAVES-OF-LIST-OF-ATOMS)
        (:REWRITE LIST-OF-ATOMSP-LEAVES)
        (:REWRITE PROPERP-LEAVES))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LEAVES-LEAVES


ACL2 >>(DEFTHM LEMMA8-10A
               (IMPLIES (NOT (MEM E LEAVES))
                        (NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))))

Name the formula above *1.

Perhaps we can prove *1 by induction.  Two induction schemes are suggested
by this conjecture.  However, one of these is flawed and so we are
left with one viable candidate.  

We will induct according to a scheme suggested by 
(COLLECT-LONESOMEP LST LEAVES).  This suggestion was produced using
the :induction rule COLLECT-LONESOMEP.  If we let  (:P E LEAVES LST)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP LST))
              (:P E LEAVES LST))
     (IMPLIES (AND (CONSP LST)
                   (NOT (LONESOMEP (CAR LST) LEAVES))
                   (:P E LEAVES (CDR LST)))
              (:P E LEAVES LST))
     (IMPLIES (AND (CONSP LST)
                   (LONESOMEP (CAR LST) LEAVES)
                   (:P E LEAVES (CDR LST)))
              (:P E LEAVES LST))).
This induction is justified by the same argument used to admit COLLECT-
LONESOMEP, namely, the measure (ACL2-COUNT LST) is decreasing according
to the relation O< (which is known to be well-founded on the domain
recognized by O-P).  When applied to the goal at hand the above induction
scheme produces the following three nontautological subgoals.

Subgoal *1/3
(IMPLIES (AND (NOT (CONSP LST))
              (NOT (MEM E LEAVES)))
         (NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))).

But simplification reduces this to T, using the :definitions COLLECT-
LONESOMEP and MEMP and the :executable-counterpart of CONSP.

Subgoal *1/2
(IMPLIES (AND (CONSP LST)
              (NOT (LONESOMEP (CAR LST) LEAVES))
              (NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
              (NOT (MEM E LEAVES)))
         (NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))).

But simplification reduces this to T, using the :definitions COLLECT-
LONESOMEP and LONESOMEP and the :type-prescription rule MEM.

Subgoal *1/1
(IMPLIES (AND (CONSP LST)
              (LONESOMEP (CAR LST) LEAVES)
              (NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
              (NOT (MEM E LEAVES)))
         (NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))).

By the simple :definition LONESOMEP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP LST)
              (MEM (CAR LST) LEAVES)
              (NOT (MEM (CAR LST)
                        (CDR (MEM (CAR LST) LEAVES))))
              (NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
              (NOT (MEM E LEAVES)))
         (NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))).

This simplifies, using the :definitions COLLECT-LONESOMEP, LONESOMEP
and MEMP, primitive type reasoning, the :rewrite rules CAR-CONS and
CDR-CONS and the :type-prescription rules COLLECT-LONESOMEP and MEM,
to

Subgoal *1/1''
(IMPLIES (AND (CONSP LST)
              (MEM (CAR LST) LEAVES)
              (NOT (MEM (CAR LST)
                        (CDR (MEM (CAR LST) LEAVES))))
              (NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
              (NOT (MEM E LEAVES)))
         (NOT (EQUAL E (CAR LST)))).

But simplification reduces this to T, using trivial observations.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM LEMMA8-10A ...)
Rules: ((:DEFINITION COLLECT-LONESOMEP)
        (:DEFINITION LONESOMEP)
        (:DEFINITION MEMP)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION COLLECT-LONESOMEP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION COLLECT-LONESOMEP)
        (:TYPE-PRESCRIPTION MEM))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
LEMMA8-10A


ACL2 >>(DEFTHM LEMMA8-10B
               (IMPLIES (MEM E (CDR (MEM E LEAVES)))
                        (NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))))

Name the formula above *1.

Perhaps we can prove *1 by induction.  Two induction schemes are suggested
by this conjecture.  However, one of these is flawed and so we are
left with one viable candidate.  

We will induct according to a scheme suggested by 
(COLLECT-LONESOMEP LST LEAVES).  This suggestion was produced using
the :induction rule COLLECT-LONESOMEP.  If we let  (:P E LEAVES LST)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP LST))
              (:P E LEAVES LST))
     (IMPLIES (AND (CONSP LST)
                   (NOT (LONESOMEP (CAR LST) LEAVES))
                   (:P E LEAVES (CDR LST)))
              (:P E LEAVES LST))
     (IMPLIES (AND (CONSP LST)
                   (LONESOMEP (CAR LST) LEAVES)
                   (:P E LEAVES (CDR LST)))
              (:P E LEAVES LST))).
This induction is justified by the same argument used to admit COLLECT-
LONESOMEP, namely, the measure (ACL2-COUNT LST) is decreasing according
to the relation O< (which is known to be well-founded on the domain
recognized by O-P).  When applied to the goal at hand the above induction
scheme produces the following three nontautological subgoals.

Subgoal *1/3
(IMPLIES (AND (NOT (CONSP LST))
              (MEM E (CDR (MEM E LEAVES))))
         (NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))).
[SGC for 439 CONS pages..(8014 writable)..(T=1).GC finished]

But simplification reduces this to T, using the :definitions COLLECT-
LONESOMEP and MEMP and the :executable-counterpart of CONSP.

Subgoal *1/2
(IMPLIES (AND (CONSP LST)
              (NOT (LONESOMEP (CAR LST) LEAVES))
              (NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
              (MEM E (CDR (MEM E LEAVES))))
         (NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))).

But simplification reduces this to T, using the :definitions COLLECT-
LONESOMEP and LONESOMEP and the :type-prescription rule MEM.

Subgoal *1/1
(IMPLIES (AND (CONSP LST)
              (LONESOMEP (CAR LST) LEAVES)
              (NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
              (MEM E (CDR (MEM E LEAVES))))
         (NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))).

By the simple :definition LONESOMEP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP LST)
              (MEM (CAR LST) LEAVES)
              (NOT (MEM (CAR LST)
                        (CDR (MEM (CAR LST) LEAVES))))
              (NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
              (MEM E (CDR (MEM E LEAVES))))
         (NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))).

This simplifies, using the :definitions COLLECT-LONESOMEP, LONESOMEP
and MEMP, primitive type reasoning, the :rewrite rules CAR-CONS and
CDR-CONS and the :type-prescription rules COLLECT-LONESOMEP and MEM,
to

Subgoal *1/1''
(IMPLIES (AND (CONSP LST)
              (MEM (CAR LST) LEAVES)
              (NOT (MEM (CAR LST)
                        (CDR (MEM (CAR LST) LEAVES))))
              (NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
              (MEM E (CDR (MEM E LEAVES))))
         (NOT (EQUAL E (CAR LST)))).

But simplification reduces this to T, using trivial observations.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM LEMMA8-10B ...)
Rules: ((:DEFINITION COLLECT-LONESOMEP)
        (:DEFINITION LONESOMEP)
        (:DEFINITION MEMP)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION COLLECT-LONESOMEP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION COLLECT-LONESOMEP)
        (:TYPE-PRESCRIPTION MEM))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
LEMMA8-10B


ACL2 >>(DEFTHM MEMP-COLLECT-LONESOMEP
               (IFF (MEMP E (COLLECT-LONESOMEP LST LEAVES))
                    (AND (MEMP E LST)
                         (LONESOMEP E LEAVES))))

ACL2 Warning [Subsume] in ( DEFTHM MEMP-COLLECT-LONESOMEP ...):  The
newly proposed :REWRITE rule MEMP-COLLECT-LONESOMEP probably subsumes
the previously added :REWRITE rules LEMMA8-10B and LEMMA8-10A, in the
sense that MEMP-COLLECT-LONESOMEP will now probably be applied whenever
the old rules would have been.


By case analysis we reduce the conjecture to

Goal'
(COND ((MEMP E (COLLECT-LONESOMEP LST LEAVES))
       (AND (MEMP E LST) (LONESOMEP E LEAVES)))
      ((AND (MEMP E LST) (LONESOMEP E LEAVES))
       NIL)
      (T T)).

This simplifies, using the :definition LONESOMEP, to the following
four conjectures.

Subgoal 4
(IMPLIES (AND (NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))
              (MEMP E LST)
              (MEM E LEAVES))
         (MEM E (CDR (MEM E LEAVES)))).

Name the formula above *1.

Subgoal 3
(IMPLIES (MEMP E (COLLECT-LONESOMEP LST LEAVES))
         (MEM E LEAVES)).

But simplification reduces this to T, using the :rewrite rule LEMMA8-
10A.

Subgoal 2
(IMPLIES (MEMP E (COLLECT-LONESOMEP LST LEAVES))
         (MEMP E LST)).

Normally we would attempt to prove this formula by induction.  However,
we prefer in this instance to focus on the original input conjecture
rather than this simplified special case.  We therefore abandon our
previous work on this conjecture and reassign the name *1 to the original
conjecture.  (See :DOC otf-flg.)

Perhaps we can prove *1 by induction.  Two induction schemes are suggested
by this conjecture.  These merge into one derived induction scheme.

We will induct according to a scheme suggested by (MEMP E LST), but
modified to accommodate (COLLECT-LONESOMEP LST LEAVES).  These suggestions
were produced using the :induction rules COLLECT-LONESOMEP and MEMP.
If we let  (:P E LEAVES LST) denote *1 above then the induction scheme
we'll use is
(AND (IMPLIES (NOT (CONSP LST))
              (:P E LEAVES LST))
     (IMPLIES (AND (CONSP LST)
                   (NOT (EQUAL E (CAR LST)))
                   (:P E LEAVES (CDR LST)))
              (:P E LEAVES LST))
     (IMPLIES (AND (CONSP LST) (EQUAL E (CAR LST)))
              (:P E LEAVES LST))).
This induction is justified by the same argument used to admit MEMP,
namely, the measure (ACL2-COUNT LST) is decreasing according to the
relation O< (which is known to be well-founded on the domain recognized
by O-P).  When applied to the goal at hand the above induction scheme
produces the following three nontautological subgoals.

Subgoal *1/3
(IMPLIES (NOT (CONSP LST))
         (IFF (MEMP E (COLLECT-LONESOMEP LST LEAVES))
              (AND (MEMP E LST)
                   (LONESOMEP E LEAVES)))).

By case analysis we reduce the conjecture to

Subgoal *1/3'
(IMPLIES (NOT (CONSP LST))
         (COND ((MEMP E (COLLECT-LONESOMEP LST LEAVES))
                (AND (MEMP E LST) (LONESOMEP E LEAVES)))
               ((AND (MEMP E LST) (LONESOMEP E LEAVES))
                NIL)
               (T T))).

But simplification reduces this to T, using the :definitions COLLECT-
LONESOMEP and MEMP and the :executable-counterpart of CONSP.

Subgoal *1/2
(IMPLIES (AND (CONSP LST)
              (NOT (EQUAL E (CAR LST)))
              (IFF (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES))
                   (AND (MEMP E (CDR LST))
                        (LONESOMEP E LEAVES))))
         (IFF (MEMP E (COLLECT-LONESOMEP LST LEAVES))
              (AND (MEMP E LST)
                   (LONESOMEP E LEAVES)))).

By case analysis we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP LST)
              (NOT (EQUAL E (CAR LST)))
              (COND ((MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES))
                     (AND (MEMP E (CDR LST))
                          (LONESOMEP E LEAVES)))
                    ((AND (MEMP E (CDR LST))
                          (LONESOMEP E LEAVES))
                     NIL)
                    (T T)))
         (COND ((MEMP E (COLLECT-LONESOMEP LST LEAVES))
                (AND (MEMP E LST) (LONESOMEP E LEAVES)))
               ((AND (MEMP E LST) (LONESOMEP E LEAVES))
                NIL)
               (T T))).

This simplifies, using the :definitions COLLECT-LONESOMEP, LONESOMEP
and MEMP, primitive type reasoning and the :type-prescription rules
MEM and MEMP, to the following four conjectures.

Subgoal *1/2.4
(IMPLIES (AND (CONSP LST)
              (NOT (EQUAL E (CAR LST)))
              (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES))
              (MEMP E (CDR LST))
              (MEM E LEAVES)
              (NOT (MEM E (CDR (MEM E LEAVES))))
              (MEM (CAR LST) LEAVES)
              (NOT (MEM (CAR LST)
                        (CDR (MEM (CAR LST) LEAVES)))))
         (MEMP E
               (CONS (CAR LST)
                     (COLLECT-LONESOMEP (CDR LST) LEAVES)))).

But simplification reduces this to T, using the :definition MEMP, primitive
type reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type-
prescription rules COLLECT-LONESOMEP and MEMP.

Subgoal *1/2.3
(IMPLIES (AND (CONSP LST)
              (NOT (EQUAL E (CAR LST)))
              (NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
              (NOT (MEM E LEAVES))
              (MEM (CAR LST) LEAVES)
              (NOT (MEM (CAR LST)
                        (CDR (MEM (CAR LST) LEAVES)))))
         (NOT (MEMP E
                    (CONS (CAR LST)
                          (COLLECT-LONESOMEP (CDR LST)
                                             LEAVES))))).

But simplification reduces this to T, using the :definition MEMP, primitive
type reasoning, the :rewrite rules CAR-CONS, CDR-CONS and LEMMA8-10A
and the :type-prescription rule COLLECT-LONESOMEP.

Subgoal *1/2.2
(IMPLIES (AND (CONSP LST)
              (NOT (EQUAL E (CAR LST)))
              (NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
              (NOT (MEMP E (CDR LST)))
              (MEM (CAR LST) LEAVES)
              (NOT (MEM (CAR LST)
                        (CDR (MEM (CAR LST) LEAVES)))))
         (NOT (MEMP E
                    (CONS (CAR LST)
                          (COLLECT-LONESOMEP (CDR LST)
                                             LEAVES))))).

But simplification reduces this to T, using the :definition MEMP, primitive
type reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type-
prescription rule COLLECT-LONESOMEP.

Subgoal *1/2.1
(IMPLIES (AND (CONSP LST)
              (NOT (EQUAL E (CAR LST)))
              (NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
              (MEM E (CDR (MEM E LEAVES)))
              (MEM (CAR LST) LEAVES)
              (NOT (MEM (CAR LST)
                        (CDR (MEM (CAR LST) LEAVES)))))
         (NOT (MEMP E
                    (CONS (CAR LST)
                          (COLLECT-LONESOMEP (CDR LST)
                                             LEAVES))))).

But simplification reduces this to T, using the :definition MEMP, primitive
type reasoning, the :rewrite rules CAR-CONS, CDR-CONS and LEMMA8-10B
and the :type-prescription rules COLLECT-LONESOMEP and MEM.

Subgoal *1/1
(IMPLIES (AND (CONSP LST) (EQUAL E (CAR LST)))
         (IFF (MEMP E (COLLECT-LONESOMEP LST LEAVES))
              (AND (MEMP E LST)
                   (LONESOMEP E LEAVES)))).

By case analysis we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP LST) (EQUAL E (CAR LST)))
         (COND ((MEMP E (COLLECT-LONESOMEP LST LEAVES))
                (AND (MEMP E LST) (LONESOMEP E LEAVES)))
               ((AND (MEMP E LST) (LONESOMEP E LEAVES))
                NIL)
               (T T))).

This simplifies, using the :definitions COLLECT-LONESOMEP, LONESOMEP
and MEMP and primitive type reasoning, to the following three conjectures.

Subgoal *1/1.3
(IMPLIES (AND (CONSP LST)
              (NOT (MEM (CAR LST) LEAVES)))
         (NOT (MEMP (CAR LST)
                    (COLLECT-LONESOMEP (CDR LST) LEAVES)))).

But simplification reduces this to T, using the :rewrite rule LEMMA8-
10A.

Subgoal *1/1.2
(IMPLIES (AND (CONSP LST)
              (MEM (CAR LST) LEAVES)
              (NOT (MEM (CAR LST)
                        (CDR (MEM (CAR LST) LEAVES)))))
         (MEMP (CAR LST)
               (CONS (CAR LST)
                     (COLLECT-LONESOMEP (CDR LST) LEAVES)))).

But simplification reduces this to T, using the :definition MEMP, primitive
type reasoning, the :rewrite rule CAR-CONS and the :type-prescription
rule COLLECT-LONESOMEP.

Subgoal *1/1.1
(IMPLIES (AND (CONSP LST)
              (MEM (CAR LST)
                   (CDR (MEM (CAR LST) LEAVES))))
         (NOT (MEMP (CAR LST)
                    (COLLECT-LONESOMEP (CDR LST) LEAVES)))).

But simplification reduces this to T, using the :rewrite rule LEMMA8-
10B and the :type-prescription rule MEM.

That completes the proof of *1.

Q.E.D.

The storage of MEMP-COLLECT-LONESOMEP depends upon the :type-prescription
rules LONESOMEP and MEMP.

Summary
Form:  ( DEFTHM MEMP-COLLECT-LONESOMEP ...)
Rules: ((:DEFINITION COLLECT-LONESOMEP)
        (:DEFINITION IFF)
        (:DEFINITION LONESOMEP)
        (:DEFINITION MEMP)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION COLLECT-LONESOMEP)
        (:INDUCTION MEMP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE LEMMA8-10A)
        (:REWRITE LEMMA8-10B)
        (:TYPE-PRESCRIPTION COLLECT-LONESOMEP)
        (:TYPE-PRESCRIPTION LONESOMEP)
        (:TYPE-PRESCRIPTION MEM)
        (:TYPE-PRESCRIPTION MEMP))
Warnings:  Subsume
Time:  0.04 seconds (prove: 0.03, print: 0.01, other: 0.00)
MEMP-COLLECT-LONESOMEP


ACL2 >>(DEFTHM MEMP-LONESOMES
               (IFF (MEMP E (LONESOMES X))
                    (AND (MEMP E (LEAVES X))
                         (LONESOMEP E (LEAVES X)))))

ACL2 Warning [Non-rec] in ( DEFTHM MEMP-LONESOMES ...):  The :REWRITE
rule generated from MEMP-LONESOMES will be triggered only by terms
containing the non-recursive function symbol LONESOMES.  Unless this
function is disabled, MEMP-LONESOMES is unlikely ever to be used.


By case analysis we reduce the conjecture to

Goal'
(COND ((MEMP E (LONESOMES X))
       (AND (MEMP E (LEAVES X))
            (LONESOMEP E (LEAVES X))))
      ((AND (MEMP E (LEAVES X))
            (LONESOMEP E (LEAVES X)))
       NIL)
      (T T)).

But simplification reduces this to T, using the :definitions LONESOMEP
and LONESOMES, the :rewrite rule MEMP-COLLECT-LONESOMEP and the :type-
prescription rules MEM and MEMP.

Q.E.D.

The storage of MEMP-LONESOMES depends upon the :type-prescription rules
LONESOMEP and MEMP.

Summary
Form:  ( DEFTHM MEMP-LONESOMES ...)
Rules: ((:DEFINITION IFF)
        (:DEFINITION LONESOMEP)
        (:DEFINITION LONESOMES)
        (:REWRITE MEMP-COLLECT-LONESOMEP)
        (:TYPE-PRESCRIPTION LONESOMEP)
        (:TYPE-PRESCRIPTION MEM)
        (:TYPE-PRESCRIPTION MEMP))
Warnings:  Non-rec
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MEMP-LONESOMES


ACL2 >>(DEFUN NUMP (X)
              (IF (CONSP X)
                  (AND (EQUAL (CAR X) NIL) (NUMP (CDR X)))
                  (EQUAL X NIL)))

The admission of NUMP is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  We observe that the type of NUMP is described by the
theorem (OR (EQUAL (NUMP X) T) (EQUAL (NUMP X) NIL)).  We used primitive
type reasoning.

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


ACL2 >>(DEFUN ADD (X Y)
              (IF (CONSP X)
                  (CONS NIL (ADD (CDR X) Y))
                  (MAPNIL Y)))

The admission of ADD is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  We observe that the type of ADD is described by the
theorem (TRUE-LISTP (ADD X Y)).  We used primitive type reasoning and
the :type-prescription rule MAPNIL.

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


ACL2 >>(DEFUN MULT (X Y)
              (IF (CONSP X)
                  (ADD Y (MULT (CDR X) Y))
                  NIL))

The admission of MULT is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  We observe that the type of MULT is described by the
theorem (TRUE-LISTP (MULT X Y)).  We used the :type-prescription rule
ADD.

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


ACL2 >>(DEFUN RAISE (X Y)
              (IF (CONSP Y)
                  (MULT X (RAISE X (CDR Y)))
                  '(NIL)))

The admission of RAISE is trivial, using the relation O< (which is
known to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT Y).  We observe that the type of RAISE is described by
the theorem (TRUE-LISTP (RAISE X Y)).  We used the :type-prescription
rule MULT.

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


ACL2 >>(DEFTHM NUMP-MAPNIL (NUMP (MAPNIL X)))

Name the formula above *1.

Perhaps we can prove *1 by induction.  One induction scheme is suggested
by this conjecture.  

We will induct according to a scheme suggested by (MAPNIL X).  This
suggestion was produced using the :induction rule MAPNIL.  If we let
 (:P X) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P X))
     (IMPLIES (AND (CONSP X) (:P (CDR X)))
              (:P X))).
This induction is justified by the same argument used to admit MAPNIL,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.

Subgoal *1/2
(IMPLIES (NOT (CONSP X))
         (NUMP (MAPNIL X))).

But simplification reduces this to T, using the :definition MAPNIL
and the :executable-counterpart of NUMP.

Subgoal *1/1
(IMPLIES (AND (CONSP X) (NUMP (MAPNIL (CDR X))))
         (NUMP (MAPNIL X))).

But simplification reduces this to T, using the :definitions MAPNIL
and NUMP, the :executable-counterpart of EQUAL, primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rules MAPNIL and NUMP.

That completes the proof of *1.

Q.E.D.

The storage of NUMP-MAPNIL depends upon the :type-prescription rule
NUMP.
[SGC for 4 SYMBOL pages..(8015 writable)..(T=1).GC finished]

Summary
Form:  ( DEFTHM NUMP-MAPNIL ...)
Rules: ((:DEFINITION MAPNIL)
        (:DEFINITION NUMP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NUMP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION MAPNIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION MAPNIL)
        (:TYPE-PRESCRIPTION NUMP))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
NUMP-MAPNIL


ACL2 >>(DEFTHM NUMP-ADD (NUMP (ADD X Y)))

Name the formula above *1.

Perhaps we can prove *1 by induction.  One induction scheme is suggested
by this conjecture.  

We will induct according to a scheme suggested by (ADD X Y).  This
suggestion was produced using the :induction rule ADD.  If we let  (:P X Y)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P X Y))
     (IMPLIES (AND (CONSP X) (:P (CDR X) Y))
              (:P X Y))).
This induction is justified by the same argument used to admit ADD,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.

Subgoal *1/2
(IMPLIES (NOT (CONSP X))
         (NUMP (ADD X Y))).

But simplification reduces this to T, using the :definition ADD and
the :rewrite rule NUMP-MAPNIL.

Subgoal *1/1
(IMPLIES (AND (CONSP X) (NUMP (ADD (CDR X) Y)))
         (NUMP (ADD X Y))).

But simplification reduces this to T, using the :definitions ADD and
NUMP, the :executable-counterpart of EQUAL, primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rules ADD and NUMP.

That completes the proof of *1.

Q.E