ACL2 !>(certify-book "notes-version-1")

CERTIFICATION ATTEMPT FOR 
"/Users/moore/courses/cs389r/spring-06/notes-version-1.lisp"
ACL2 Version 2.9


* Step 1:  Read "/Users/moore/courses/cs389r/spring-06/notes-version-1.lisp"
and compute its check sum.

* Step 2:  There were 329 forms in the file. The check sum is 132297991.
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 >>(DEFMACRO
        THEOREM
        (NAME FORM &KEY
              (RULE-CLASSES ':REWRITE
                            RULE-CLASSES-SUPPLIEDP)
              HINTS)
        (LET
         ((OLD-HINTS HINTS)
          (HINTS
            (COND ((NULL HINTS)
                   '(("Goal" :DO-NOT-INDUCT T)))
                  ((AND (TRUE-LISTP HINTS)
                        (EQUAL (LENGTH HINTS) 1)
                        (EQUAL (CAR (CAR HINTS)) "Goal"))
                   (CONS (CONS '"Goal"
                               (CONS ':DO-NOT-INDUCT
                                     (CONS 'T
                                           (APPEND (CDR (CAR HINTS)) 'NIL))))
                         'NIL))
                  (T NIL))))
         (COND
          ((NULL HINTS)
           (CONS
            'ER
            (CONS
             'SOFT
             (CONS
              (CONS 'QUOTE (CONS 'THEOREM 'NIL))
              (CONS
               '"The :hints value ~x0 is not allowed ~
            by this macro."
               (CONS (CONS 'QUOTE (CONS OLD-HINTS 'NIL))
                     'NIL))))))
          ((AND RULE-CLASSES-SUPPLIEDP
                (EQUAL RULE-CLASSES NIL))
           (CONS
               'DEFTHM
               (CONS NAME
                     (CONS FORM
                           (CONS ':RULE-CLASSES
                                 (CONS 'NIL
                                       (CONS ':HINTS (CONS HINTS 'NIL))))))))
          (T
           (CONS
            'PROGN
            (CONS
               (CONS 'DEFTHM
                     (CONS NAME
                           (CONS FORM
                                 (APPEND (IF RULE-CLASSES-SUPPLIEDP
                                             (CONS ':RULE-CLASSES
                                                   (CONS RULE-CLASSES 'NIL))
                                             NIL)
                                         (CONS ':HINTS (CONS HINTS 'NIL))))))
               (CONS (CONS 'IN-THEORY
                           (CONS (CONS 'DISABLE (CONS NAME 'NIL))
                                 'NIL))
                     (CONS (CONS 'VALUE-TRIPLE
                                 (CONS (CONS 'QUOTE (CONS NAME 'NIL))
                                       'NIL))
                           'NIL))))))))

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


ACL2 >>(DEFUN
            ADD-LABEL-TO-BUCKET
            (LABEL CONST BUCKETS)
            (IF (ENDP BUCKETS)
                (LIST (LIST CONST (LIST LABEL)))
                (IF (EQUAL CONST (CAR (CAR BUCKETS)))
                    (CONS (LIST CONST
                                (APPEND (CADR (CAR BUCKETS))
                                        (LIST LABEL)))
                          (CDR BUCKETS))
                    (CONS (CAR BUCKETS)
                          (ADD-LABEL-TO-BUCKET LABEL CONST (CDR BUCKETS))))))

The admission of ADD-LABEL-TO-BUCKET 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 BUCKETS).  We observe that the type
of ADD-LABEL-TO-BUCKET is described by the theorem 
(CONSP (ADD-LABEL-TO-BUCKET LABEL CONST BUCKETS)).  We used primitive
type reasoning.

Summary
Form:  ( DEFUN ADD-LABEL-TO-BUCKET ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.06 seconds (prove: 0.00, print: 0.02, other: 0.04)
ADD-LABEL-TO-BUCKET


ACL2 >>(DEFUN MAKE-EQUIV-CLASSES (ALIST BUCKETS)
              (IF (ENDP ALIST)
                  BUCKETS
                  (MAKE-EQUIV-CLASSES (CDR ALIST)
                                      (ADD-LABEL-TO-BUCKET (CAAR ALIST)
                                                           (CADR (CAR ALIST))
                                                           BUCKETS))))

The admission of MAKE-EQUIV-CLASSES 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 ALIST).  We observe that the type of
MAKE-EQUIV-CLASSES is described by the theorem 
(OR (CONSP (MAKE-EQUIV-CLASSES ALIST BUCKETS))
    (EQUAL (MAKE-EQUIV-CLASSES ALIST BUCKETS)
           BUCKETS)).
We used the :type-prescription rule ADD-LABEL-TO-BUCKET.

Summary
Form:  ( DEFUN MAKE-EQUIV-CLASSES ...)
Rules: ((:TYPE-PRESCRIPTION ADD-LABEL-TO-BUCKET))
Warnings:  None
Time:  0.04 seconds (prove: 0.00, print: 0.02, other: 0.02)
MAKE-EQUIV-CLASSES


ACL2 >>(THEOREM PROBLEM-2
                (EQUAL (MAKE-EQUIV-CLASSES '((1 (1 2 3))
                                             (2 (NIL NIL NIL))
                                             (3 ((NIL NIL)))
                                             (4 (1 (2 . 3) 4))
                                             (5 (NIL NIL))
                                             (6 (1 (2 . 3) 4))
                                             (7 (HELLOWORLD !))
                                             (8 (1 (2 3) 4))
                                             (9 ((A . T) (B) (C)))
                                             (10 (NIL NIL))
                                             (11 (1 2 3))
                                             (12 (NIL NIL))
                                             (13 (A B C))
                                             (14 (A B C))
                                             (15 (HELLO WORLD !))
                                             (16 ((A . T) (B) (C))))
                                           NIL)
                       '(((1 2 3) (1 11))
                         ((NIL NIL NIL) (2))
                         (((NIL NIL)) (3))
                         ((1 (2 . 3) 4) (4 6))
                         ((NIL NIL) (5 10 12))
                         ((HELLOWORLD !) (7))
                         ((1 (2 3) 4) (8))
                         (((A . T) (B) (C)) (9 16))
                         ((A B C) (13 14))
                         ((HELLO WORLD !) (15))))
                :RULE-CLASSES NIL)

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL and MAKE-EQUIV-CLASSES.

Q.E.D.

Summary
Form:  ( DEFTHM PROBLEM-2 ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART MAKE-EQUIV-CLASSES))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
PROBLEM-2


ACL2 >>(THEOREM PROBLEM-4
                (AND (EQUAL '((1 . 2) 3 . 4)
                            (CONS (CONS '1 '2) (CONS '3 '4)))
                     (EQUAL '(1 2 3)
                            (CONS '1 (CONS '2 (CONS '3 'NIL))))
                     (EQUAL '((1 . T) (2) (3 . T))
                            (CONS (CONS '1 'T)
                                  (CONS (CONS '2 'NIL)
                                        (CONS (CONS '3 'T) 'NIL))))
                     (EQUAL '((A . 1) (B . 2))
                            (CONS (CONS 'A '1)
                                  (CONS (CONS 'B '2) 'NIL))))
                :RULE-CLASSES NIL)

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

But we reduce the conjecture to T, by case analysis.

Q.E.D.

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


ACL2 >>(THEOREM PROBLEM-5
                (AND (EQUAL (CONS (CONS '1 '2)
                                  (CONS (CONS '3 '4) 'NIL))
                            '((1 . 2) (3 . 4)))
                     (EQUAL (CONS '1 (CONS '2 '3))
                            '(1 2 . 3))
                     (EQUAL (CONS 'NIL (CONS (CONS 'NIL 'NIL) 'NIL))
                            '(NIL (NIL)))
                     (EQUAL (IF 'NIL '1 '2) '2)
                     (EQUAL (IF '1 '2 '3) '2)
                     (EQUAL (EQUAL 'NIL (CONS 'NIL 'NIL))
                            'NIL)
                     (EQUAL (EQUAL 'HELLO 'HELLO) 'T)
                     (EQUAL (EQUAL (CONS '1 '2) (CONS '1 'TWO))
                            'NIL))
                :RULE-CLASSES NIL)

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

But we reduce the conjecture to T, by case analysis.

Q.E.D.

Summary
Form:  ( DEFTHM PROBLEM-5 ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
PROBLEM-5


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.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
APP


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.02 seconds (prove: 0.00, print: 0.01, other: 0.01)
REV


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.02 seconds (prove: 0.00, print: 0.01, other: 0.01)
MAPNIL


ACL2 >>(DEFUN SWAP-TREE (X)
              (IF (CONSP X)
                  (CONS (SWAP-TREE (CDR X))
                        (SWAP-TREE (CAR X)))
                  X))

The admission of SWAP-TREE 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 SWAP-TREE.  However, in normalizing the definition we used primitive
type reasoning.

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


ACL2 >>(DEFUN MEM (E X)
              (IF (CONSP X)
                  (IF (EQUAL E (CAR X)) T (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 (EQUAL (MEM E X) T) (EQUAL (MEM E X) NIL)).  

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


ACL2 >>(DEFUN SUB (X Y)
              (IF (CONSP X)
                  (IF (MEM (CAR X) Y) (SUB (CDR X) Y) NIL)
                  T))

The admission of SUB 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 SUB is described by the
theorem (OR (EQUAL (SUB X Y) T) (EQUAL (SUB X Y) NIL)).  

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


ACL2 >>(DEFUN INT (X Y)
              (IF (CONSP X)
                  (IF (MEM (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.02 seconds (prove: 0.00, print: 0.01, other: 0.01)
INT


ACL2 >>(DEFUN TIP (E X)
              (IF (CONSP X)
                  (OR (TIP E (CAR X)) (TIP E (CDR X)))
                  (EQUAL E X)))

The admission of TIP 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 TIP is described by the
theorem (OR (EQUAL (TIP E X) T) (EQUAL (TIP E X) NIL)).  We used primitive
type reasoning.

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


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

The admission of FLATTEN 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 FLATTEN is described by
the theorem (CONSP (FLATTEN X)).  We used primitive type reasoning
and the :type-prescription rule APP.

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


ACL2 >>(DEFUN EVENLEN (X)
              (IF (CONSP X)
                  (IF (CONSP (CDR X))
                      (EVENLEN (CDR (CDR X)))
                      NIL)
                  T))

For the admission of EVENLEN we will use the relation O< (which is
known to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  The non-trivial part of the measure conjecture is

Goal
(IMPLIES (AND (CONSP X) (CONSP (CDR X)))
         (O< (ACL2-COUNT (CDDR X))
             (ACL2-COUNT X))).

This simplifies, using the :definitions O-FINP and O< and the :type-
prescription rule ACL2-COUNT, to

Goal'
(IMPLIES (AND (CONSP X) (CONSP (CDR X)))
         (< (ACL2-COUNT (CDDR X))
            (ACL2-COUNT X))).

The destructor terms (CAR X) and (CDR X) can be eliminated.  Furthermore,
those terms are at the root of a chain of two rounds of destructor
elimination. (1) Use CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X)
by X1 and (CDR X) by X2.  (2) Use CAR-CDR-ELIM, again, to replace X2
by (CONS X3 X4), (CAR X2) by X3 and (CDR X2) by X4.    These steps
produce the following goal.

Goal''
(IMPLIES (AND (CONSP (CONS X3 X4))
              (CONSP (LIST* X1 X3 X4)))
         (< (ACL2-COUNT X4)
            (ACL2-COUNT (LIST* X1 X3 X4)))).

This simplifies, using the :definition ACL2-COUNT, primitive type reasoning
and the :rewrite rules CAR-CONS and CDR-CONS, to

Goal'''
(< (ACL2-COUNT X4)
   (+ 1 (ACL2-COUNT X1)
      1 (ACL2-COUNT X3)
      (ACL2-COUNT X4))).

But simplification reduces this to T, using linear arithmetic and the
:type-prescription rule ACL2-COUNT.

Q.E.D.

That completes the proof of the measure theorem for EVENLEN.  Thus,
we admit this function under the principle of definition. We observe
that the type of EVENLEN is described by the theorem 
(OR (EQUAL (EVENLEN X) T) (EQUAL (EVENLEN X) NIL)).  

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


ACL2 >>(THEOREM PROBLEM-40
                (EQUAL (APP (APP A B) C)
                       (APP A (APP B C)))
                :HINTS (("Goal" :INDUCT (APP A B))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

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 PROBLEM-40 ...)
Rules: ((:DEFINITION APP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION APP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Warnings:  None
Time:  0.04 seconds (prove: 0.01, print: 0.03, other: 0.00)

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


ACL2 >>(THEOREM PROBLEM-41-COUNTEREXAMPLE
                (NOT (EQUAL (APP '(1 2 3 . 4) NIL)
                            '(1 2 3 . 4)))
                :RULE-CLASSES NIL)

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

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

Q.E.D.

Summary
Form:  ( DEFTHM PROBLEM-41-COUNTEREXAMPLE ...)
Rules: ((:EXECUTABLE-COUNTERPART APP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
PROBLEM-41-COUNTEREXAMPLE


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

The admission of PROPER 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 PROPER is described by
the theorem (OR (EQUAL (PROPER X) T) (EQUAL (PROPER X) NIL)).  We used
primitive type reasoning.

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


ACL2 >>(THEOREM PROBLEM-41
                (IMPLIES (PROPER X)
                         (EQUAL (APP X NIL) X))
                :HINTS (("Goal" :INDUCT (APP X NIL))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (APP X 'NIL).  This
suggestion was produced using the :induction rule APP.  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 two nontautological subgoals.

Subgoal *1/2
(IMPLIES (NOT (CONSP X))
         (IMPLIES (PROPER X)
                  (EQUAL (APP X NIL) X))).

By case analysis we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (NOT (CONSP X)) (PROPER X))
         (EQUAL (APP X NIL) X)).

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

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

By case analysis we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP X)
              (IMPLIES (PROPER (CDR X))
                       (EQUAL (APP (CDR X) NIL) (CDR X)))
              (PROPER X))
         (EQUAL (APP X NIL) X)).

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

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM PROBLEM-41 ...)
Rules: ((:DEFINITION APP)
        (:DEFINITION NOT)
        (:DEFINITION PROPER)
        (:EXECUTABLE-COUNTERPART APP)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION APP)
        (:REWRITE CAR-CDR-ELIM))
Warnings:  None
Time:  0.05 seconds (prove: 0.01, print: 0.03, other: 0.01)

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


ACL2 >>(THEOREM PROBLEM-42
                (EQUAL (MAPNIL (APP A B))
                       (APP (MAPNIL A) (MAPNIL B)))
                :HINTS (("Goal" :INDUCT (APP A B))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

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 (MAPNIL (APP A B))
                (APP (MAPNIL A) (MAPNIL B)))).

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

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

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

That completes the proof of *1.

Q.E.D.

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

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


ACL2 >>(THEOREM PROBLEM-43
                (EQUAL (REV (MAPNIL X))
                       (MAPNIL (REV X)))
                :HINTS
                (("Goal" :INDUCT (REV X)
                         :IN-THEORY (ENABLE PROBLEM-42))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

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))
         (EQUAL (REV (MAPNIL X))
                (MAPNIL (REV X)))).

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

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

But simplification reduces this to T, using the :definitions MAPNIL
and REV, the :executable-counterparts of CONS and MAPNIL, primitive
type reasoning, the :rewrite rules CAR-CONS, CDR-CONS and PROBLEM-42
and the :type-prescription rule MAPNIL.

That completes the proof of *1.

Q.E.D.

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

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


ACL2 >>(THEOREM PROBLEM-44-COUNTEREXAMPLE
                (NOT (EQUAL (REV (REV '(1 2 3 . 4)))
                            '(1 2 3 . 4)))
                :RULE-CLASSES NIL)

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

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

Q.E.D.

Summary
Form:  ( DEFTHM PROBLEM-44-COUNTEREXAMPLE ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART REV))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
PROBLEM-44-COUNTEREXAMPLE


ACL2 >>(THEOREM PROBLEM-44C
                (EQUAL (PROPER (APP A B)) (PROPER B))
                :HINTS (("Goal" :INDUCT (APP A B))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

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 (PROPER (APP A B)) (PROPER B))).

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

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

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

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM PROBLEM-44C ...)
Rules: ((:DEFINITION APP)
        (:DEFINITION PROPER)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION APP)
        (:REWRITE CDR-CONS))
Warnings:  None
Time:  0.03 seconds (prove: 0.00, print: 0.03, other: 0.00)

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


ACL2 >>(THEOREM PROBLEM-44B (PROPER (REV X))
                :HINTS
                (("Goal" :INDUCT (REV X)
                         :IN-THEORY (ENABLE PROBLEM-44C))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

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))
         (PROPER (REV X))).

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

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

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

That completes the proof of *1.

Q.E.D.

The storage of PROBLEM-44B depends upon the :type-prescription rule
PROPER.

Summary
Form:  ( DEFTHM PROBLEM-44B ...)
Rules: ((:DEFINITION PROPER)
        (:DEFINITION REV)
        (:EXECUTABLE-COUNTERPART PROPER)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION REV)
        (:REWRITE CDR-CONS)
        (:REWRITE PROBLEM-44C)
        (:TYPE-PRESCRIPTION PROPER))
Warnings:  None
Time:  0.04 seconds (prove: 0.02, print: 0.01, other: 0.01)

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


ACL2 >>(THEOREM PROBLEM-44A
                (EQUAL (REV (APP A B))
                       (APP (REV B) (REV A)))
                :HINTS
                (("Goal" :INDUCT (APP A B)
                         :IN-THEORY
                         (ENABLE PROBLEM-40 PROBLEM-41 PROBLEM-44B))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

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 (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 PROBLEM-41 and
PROBLEM-44B.

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 PROBLEM-
40.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM PROBLEM-44A ...)
Rules: ((:DEFINITION APP)
        (:DEFINITION REV)
        (:ELIM CAR-CDR-ELIM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION APP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE PROBLEM-40)
        (:REWRITE PROBLEM-41)
        (:REWRITE PROBLEM-44B))
Warnings:  None
Time:  0.12 seconds (prove: 0.04, print: 0.07, other: 0.01)

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


ACL2 >>(THEOREM PROBLEM-44
                (IMPLIES (PROPER X)
                         (EQUAL (REV (REV X)) X))
                :HINTS
                (("Goal" :INDUCT (REV X)
                         :IN-THEORY (ENABLE PROBLEM-44A))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

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))
         (IMPLIES (PROPER X)
                  (EQUAL (REV (REV X)) X))).

By case analysis we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (NOT (CONSP X)) (PROPER X))
         (EQUAL (REV (REV X)) X)).

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

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

By case analysis we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP X)
              (IMPLIES (PROPER (CDR X))
                       (EQUAL (REV (REV (CDR X))) (CDR X)))
              (PROPER X))
         (EQUAL (REV (REV X)) X)).

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

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM PROBLEM-44 ...)
Rules: ((:DEFINITION APP)
        (:DEFINITION NOT)
        (:DEFINITION PROPER)
        (:DEFINITION REV)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART REV)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION REV)
        (:REWRITE CAR-CDR-ELIM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE PROBLEM-44A))
Warnings:  None
Time:  0.06 seconds (prove: 0.02, print: 0.03, other: 0.01)

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


ACL2 >>(THEOREM PROBLEM-45
                (EQUAL (SWAP-TREE (SWAP-TREE X)) X)
                :HINTS (("Goal" :INDUCT (SWAP-TREE X))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (SWAP-TREE X).  This
suggestion was produced using the :induction rule SWAP-TREE.  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 SWAP-
TREE, 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 (SWAP-TREE (SWAP-TREE X)) X)).

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

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (EQUAL (SWAP-TREE (SWAP-TREE (CDR X)))
                     (CDR X))
              (EQUAL (SWAP-TREE (SWAP-TREE (CAR X)))
                     (CAR X)))
         (EQUAL (SWAP-TREE (SWAP-TREE X)) X)).

But simplification reduces this to T, using the :definition SWAP-TREE,
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 PROBLEM-45 ...)
Rules: ((:DEFINITION SWAP-TREE)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SWAP-TREE)
        (:REWRITE CAR-CDR-ELIM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Warnings:  None
Time:  0.04 seconds (prove: 0.01, print: 0.02, other: 0.01)

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


ACL2 >>(THEOREM PROBLEM-46
                (EQUAL (MEM E (APP A B))
                       (OR (MEM E A) (MEM E B)))
                :HINTS (("Goal" :INDUCT (MEM E A))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (MEM E A).  This
suggestion was produced using the :induction rule MEM.  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 MEM,
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 (MEM E (APP A B))
                (OR (MEM E A) (MEM E B)))).

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

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

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

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

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

Subgoal *1/1'
(IMPLIES (CONSP A)
         (MEM (CAR A) (APP A B))).

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 (CONSP (CONS A1 A2))
         (MEM A1 (APP (CONS A1 A2) B))).

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

That completes the proof of *1.

Q.E.D.

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

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


ACL2 >>(THEOREM PROBLEM-47A
                (IMPLIES (NOT (MEM E B))
                         (NOT (MEM E (INT A B))))
                :HINTS (("Goal" :INDUCT (INT A B))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (INT A B).  This
suggestion was produced using the :induction rule INT.  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 (MEM (CAR A) B))
                   (:P (CDR A) B E))
              (:P A B E))
     (IMPLIES (AND (CONSP A)
                   (MEM (CAR A) B)
                   (:P (CDR A) B E))
              (:P A B E))).
This induction is justified by the same argument used to admit INT,
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))
         (IMPLIES (NOT (MEM E B))
                  (NOT (MEM E (INT A B))))).

By case analysis we reduce the conjecture to

Subgoal *1/3'
(IMPLIES (AND (NOT (CONSP A)) (NOT (MEM E B)))
         (NOT (MEM E (INT A B)))).

But simplification reduces this to T, using the :definitions INT and
MEM and the :executable-counterpart of CONSP.

Subgoal *1/2
(IMPLIES (AND (CONSP A)
              (NOT (MEM (CAR A) B))
              (IMPLIES (NOT (MEM E B))
                       (NOT (MEM E (INT (CDR A) B)))))
         (IMPLIES (NOT (MEM E B))
                  (NOT (MEM E (INT A B))))).

By case analysis we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP A)
              (NOT (MEM (CAR A) B))
              (IMPLIES (NOT (MEM E B))
                       (NOT (MEM E (INT (CDR A) B))))
              (NOT (MEM E B)))
         (NOT (MEM E (INT A B)))).

But simplification reduces this to T, using the :definitions INT and
NOT and the :executable-counterpart of NOT.

Subgoal *1/1
(IMPLIES (AND (CONSP A)
              (MEM (CAR A) B)
              (IMPLIES (NOT (MEM E B))
                       (NOT (MEM E (INT (CDR A) B)))))
         (IMPLIES (NOT (MEM E B))
                  (NOT (MEM E (INT A B))))).

By case analysis we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP A)
              (MEM (CAR A) B)
              (IMPLIES (NOT (MEM E B))
                       (NOT (MEM E (INT (CDR A) B))))
              (NOT (MEM E B)))
         (NOT (MEM E (INT A B)))).

This simplifies, using the :definitions INT, MEM and NOT, the :executable-
counterpart of NOT, primitive type reasoning, the :rewrite rules CAR-
CONS and CDR-CONS and the :type-prescription rules INT and MEM, to

Subgoal *1/1''
(IMPLIES (AND (CONSP A)
              (MEM (CAR A) B)
              (NOT (MEM E (INT (CDR A) B)))
              (NOT (MEM E B)))
         (NOT (EQUAL E (CAR A)))).

But simplification reduces this to T, using trivial observations.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM PROBLEM-47A ...)
Rules: ((:DEFINITION INT)
        (:DEFINITION MEM)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION INT)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION INT)
        (:TYPE-PRESCRIPTION MEM))
Warnings:  None
Time:  0.08 seconds (prove: 0.03, print: 0.05, other: 0.00)

Summary
Form:  (IN-THEORY (DISABLE ...))
Rules: NIL
Warnings:  None
Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
PROBLEM-47A


ACL2 >>(THEOREM PROBLEM-47
                (EQUAL (MEM E (INT A B))
                       (AND (MEM E A) (MEM E B)))
                :HINTS
                (("Goal" :INDUCT (MEM E A)
                         :IN-THEORY (ENABLE PROBLEM-47A))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (MEM E A).  This
suggestion was produced using the :induction rule MEM.  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 MEM,
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 (MEM E (INT A B))
                (AND (MEM E A) (MEM E B)))).

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

Subgoal *1/2
(IMPLIES (AND (CONSP A)
              (NOT (EQUAL E (CAR A)))
              (EQUAL (MEM E (INT (CDR A) B))
                     (AND (MEM E (CDR A)) (MEM E B))))
         (EQUAL (MEM E (INT A B))
                (AND (MEM E A) (MEM E B)))).

This simplifies, using the :definitions INT and MEM, the :executable-
counterpart of NOT, primitive type reasoning and the :type-prescription
rule MEM, to the following two conjectures.

Subgoal *1/2.2
(IMPLIES (AND (CONSP A)
              (NOT (EQUAL E (CAR A)))
              (MEM E (CDR A))
              (EQUAL (MEM E (INT (CDR A) B))
                     (MEM E B))
              (MEM (CAR A) B))
         (EQUAL (MEM E (CONS (CAR A) (INT (CDR A) B)))
                (MEM E B))).

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

Subgoal *1/2.1
(IMPLIES (AND (CONSP A)
              (NOT (EQUAL E (CAR A)))
              (NOT (MEM E (CDR A)))
              (EQUAL (MEM E (INT (CDR A) B)) NIL)
              (MEM (CAR A) B))
         (NOT (MEM E (CONS (CAR A) (INT (CDR A) B))))).

By case analysis we reduce the conjecture to

Subgoal *1/2.1'
(IMPLIES (AND (CONSP A)
              (NOT (EQUAL E (CAR A)))
              (NOT (MEM E (CDR A)))
              (NOT (MEM E (INT (CDR A) B)))
              (MEM (CAR A) B))
         (NOT (MEM E (CONS (CAR A) (INT (CDR A) B))))).

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

Subgoal *1/1
(IMPLIES (AND (CONSP A) (EQUAL E (CAR A)))
         (EQUAL (MEM E (INT A B))
                (AND (MEM E A) (MEM E B)))).

This simplifies, using the :definition MEM and primitive type reasoning,
to

Subgoal *1/1'
(IMPLIES (CONSP A)
         (EQUAL (MEM (CAR A) (INT A B))
                (MEM (CAR A) B))).

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 (CONSP (CONS A1 A2))
         (EQUAL (MEM A1 (INT (CONS A1 A2) B))
                (MEM A1 B))).

This simplifies, using the :definition INT, primitive type reasoning
and the :rewrite rules CAR-CONS and CDR-CONS, to the following two
conjectures.

Subgoal *1/1.2
(IMPLIES (MEM A1 B)
         (EQUAL (MEM A1 (CONS A1 (INT A2 B)))
                (MEM A1 B))).

But simplification reduces this to T, using the :definition MEM, the
:executable-counterpart of EQUAL, primitive type reasoning, the :rewrite
rule CAR-CONS and the :type-prescription rules INT and MEM.

Subgoal *1/1.1
(IMPLIES (NOT (MEM A1 B))
         (EQUAL (MEM A1 (INT A2 B)) (MEM A1 B))).

But simplification reduces this to T, using the :executable-counterpart
of EQUAL and the :rewrite rule PROBLEM-47A.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM PROBLEM-47 ...)
Rules: ((:DEFINITION INT)
        (:DEFINITION MEM)
        (:DEFINITION NOT)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION MEM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE PROBLEM-47A)
        (:TYPE-PRESCRIPTION INT)
        (:TYPE-PRESCRIPTION MEM))
Warnings:  None
Time:  0.13 seconds (prove: 0.04, print: 0.08, other: 0.01)

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


ACL2 >>(THEOREM PROBLEM-48A
                (IMPLIES (SUB X (CDR Y)) (SUB X Y))
                :HINTS (("Goal" :INDUCT (SUB X Y))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (SUB X Y).  This
suggestion was produced using the :induction rule SUB.  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 (MEM (CAR X) Y)))
              (:P X Y))
     (IMPLIES (AND (CONSP X)
                   (MEM (CAR X) Y)
                   (:P (CDR X) Y))
              (:P X Y))).
This induction is justified by the same argument used to admit SUB,
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 (SUB X (CDR Y)) (SUB X Y))).

By case analysis we reduce the conjecture to

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

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

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

By case analysis we reduce the conjecture to

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

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

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Y)
              (IMPLIES (SUB (CDR X) (CDR Y))
                       (SUB (CDR X) Y)))
         (IMPLIES (SUB X (CDR Y)) (SUB X Y))).

By case analysis we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Y)
              (IMPLIES (SUB (CDR X) (CDR Y))
                       (SUB (CDR X) Y))
              (SUB X (CDR Y)))
         (SUB X Y)).

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

That completes the proof of *1.

Q.E.D.

The storage of PROBLEM-48A depends upon the :type-prescription rule
SUB.

Summary
Form:  ( DEFTHM PROBLEM-48A ...)
Rules: ((:DEFINITION MEM)
        (:DEFINITION NOT)
        (:DEFINITION SUB)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SUB)
        (:REWRITE DEFAULT-CDR)
        (:TYPE-PRESCRIPTION MEM)
        (:TYPE-PRESCRIPTION SUB))
Warnings:  None
Time:  0.05 seconds (prove: 0.01, print: 0.03, other: 0.01)

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


ACL2 >>(THEOREM PROBLEM-48 (SUB X X)
                :HINTS
                (("Goal" :INDUCT (SUB X X)
                         :IN-THEORY (ENABLE PROBLEM-48A))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (SUB X X).  This
suggestion was produced using the :induction rule SUB.  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 (MEM (CAR X) X)))
              (:P X))
     (IMPLIES (AND (CONSP X)
                   (MEM (CAR X) X)
                   (:P (CDR X)))
              (:P X))).
This induction is justified by the same argument used to admit SUB,
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)) (SUB X X)).

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

Subgoal *1/2
(IMPLIES (AND (CONSP X) (NOT (MEM (CAR X) X)))
         (SUB X X)).

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

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) X)
              (SUB (CDR X) (CDR X)))
         (SUB X X)).

But simplification reduces this to T, using the :definitions MEM and
SUB, primitive type reasoning, the :rewrite rule PROBLEM-48A and the
:type-prescription rule SUB.

That completes the proof of *1.

Q.E.D.

The storage of PROBLEM-48 depends upon the :type-prescription rule
SUB.

Summary
Form:  ( DEFTHM PROBLEM-48 ...)
Rules: ((:DEFINITION MEM)
        (:DEFINITION SUB)
        (:EXECUTABLE-COUNTERPART CDR)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SUB)
        (:REWRITE DEFAULT-CDR)
        (:REWRITE PROBLEM-48A)
        (:TYPE-PRESCRIPTION SUB))
Warnings:  None
Time:  0.10 seconds (prove: 0.01, print: 0.08, other: 0.01)

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


ACL2 >>(THEOREM PROBLEM-49A
                (IMPLIES (AND (MEM E A) (SUB A B))
                         (MEM E B))
                :HINTS (("Goal" :INDUCT (SUB A B))))

ACL2 Warning [Free] in ( DEFTHM PROBLEM-49A ...):  The :REWRITE rule
generated from PROBLEM-49A contains the free variable A.  This variable
will be chosen by searching for an instance of (MEM E A) 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.


[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (SUB A B).  This
suggestion was produced using the :induction rule SUB.  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 (MEM (CAR A) B)))
              (:P A B E))
     (IMPLIES (AND (CONSP A)
                   (MEM (CAR A) B)
                   (:P (CDR A) B E))
              (:P A B E))).
This induction is justified by the same argument used to admit SUB,
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))
         (IMPLIES (AND (MEM E A) (SUB A B))
                  (MEM E B))).

By case analysis we reduce the conjecture to

Subgoal *1/3'
(IMPLIES (AND (NOT (CONSP A))
              (MEM E A)
              (SUB A B))
         (MEM E B)).

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

Subgoal *1/2
(IMPLIES (AND (CONSP A) (NOT (MEM (CAR A) B)))
         (IMPLIES (AND (MEM E A) (SUB A B))
                  (MEM E B))).

By case analysis we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP A)
              (NOT (MEM (CAR A) B))
              (MEM E A)
              (SUB A B))
         (MEM E B)).

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

Subgoal *1/1
(IMPLIES (AND (CONSP A)
              (MEM (CAR A) B)
              (IMPLIES (AND (MEM E (CDR A)) (SUB (CDR A) B))
                       (MEM E B)))
         (IMPLIES (AND (MEM E A) (SUB A B))
                  (MEM E B))).

By case analysis we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP A)
              (MEM (CAR A) B)
              (IMPLIES (AND (MEM E (CDR A)) (SUB (CDR A) B))
                       (MEM E B))
              (MEM E A)
              (SUB A B))
         (MEM E B)).

But simplification reduces this to T, using the :definitions MEM and
SUB, primitive type reasoning and the :type-prescription rule MEM.

That completes the proof of *1.

Q.E.D.

The storage of PROBLEM-49A depends upon the :type-prescription rule
MEM.

Summary
Form:  ( DEFTHM PROBLEM-49A ...)
Rules: ((:DEFINITION MEM)
        (:DEFINITION NOT)
        (:DEFINITION SUB)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SUB)
        (:TYPE-PRESCRIPTION MEM))
Warnings:  Free
Time:  0.07 seconds (prove: 0.02, print: 0.04, other: 0.01)

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


ACL2 >>(THEOREM PROBLEM-49
                (IMPLIES (AND (SUB A B) (SUB B C))
                         (SUB A C))
                :HINTS
                (("Goal" :INDUCT (SUB A C)
                         :IN-THEORY
                         (ENABLE PROBLEM-48A PROBLEM-49A))))

ACL2 Warning [Free] in ( DEFTHM PROBLEM-49 ...):  The :REWRITE rule
generated from PROBLEM-49 contains the free variable B.  This variable
will be chosen by searching for an instance of (SUB A B) 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.


[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (SUB A C).  This
suggestion was produced using the :induction rule SUB.  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 (MEM (CAR A) C)))
              (:P A B C))
     (IMPLIES (AND (CONSP A)
                   (MEM (CAR A) C)
                   (:P (CDR A) B C))
              (:P A B C))).
This induction is justified by the same argument used to admit SUB,
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))
         (IMPLIES (AND (SUB A B) (SUB B C))
                  (SUB A C))).

By case analysis we reduce the conjecture to

Subgoal *1/3'
(IMPLIES (AND (NOT (CONSP A))
              (SUB A B)
              (SUB B C))
         (SUB A C)).

But simplification reduces this to T, using the :definition SUB and
the :rewrite rule PROBLEM-48A.

Subgoal *1/2
(IMPLIES (AND (CONSP A) (NOT (MEM (CAR A) C)))
         (IMPLIES (AND (SUB A B) (SUB B C))
                  (SUB A C))).

By case analysis we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP A)
              (NOT (MEM (CAR A) C))
              (SUB A B)
              (SUB B C))
         (SUB A C)).

This simplifies, using the :definition SUB, to

Subgoal *1/2''
(IMPLIES (AND (CONSP A)
              (NOT (MEM (CAR A) C))
              (SUB A B))
         (NOT (SUB B C))).

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/2'''
(IMPLIES (AND (CONSP (CONS A1 A2))
              (NOT (MEM A1 C))
              (SUB (CONS A1 A2) B))
         (NOT (SUB B C))).

This simplifies, using the :definition SUB, primitive type reasoning
and the :rewrite rules CAR-CONS and CDR-CONS, to

Subgoal *1/2'4'
(IMPLIES (AND (NOT (MEM A1 C))
              (MEM A1 B)
              (SUB A2 B))
         (NOT (SUB B C))).

But simplification reduces this to T, using the :rewrite rule PROBLEM-
49A and the :type-prescription rules MEM and SUB.

Subgoal *1/1
(IMPLIES (AND (CONSP A)
              (MEM (CAR A) C)
              (IMPLIES (AND (SUB (CDR A) B) (SUB B C))
                       (SUB (CDR A) C)))
         (IMPLIES (AND (SUB A B) (SUB B C))
                  (SUB A C))).

By case analysis we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP A)
              (MEM (CAR A) C)
              (IMPLIES (AND (SUB (CDR A) B) (SUB B C))
                       (SUB (CDR A) C))
              (SUB A B)
              (SUB B C))
         (SUB A C)).

But simplification reduces this to T, using the :definition SUB, the
:rewrite rule PROBLEM-49A and the :type-prescription rules MEM and
SUB.

That completes the proof of *1.

Q.E.D.

The storage of PROBLEM-49 depends upon the :type-prescription rule
SUB.

Summary
Form:  ( DEFTHM PROBLEM-49 ...)
Rules: ((:DEFINITION NOT)
        (:DEFINITION SUB)
        (:ELIM CAR-CDR-ELIM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SUB)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE PROBLEM-48A)
        (:REWRITE PROBLEM-49A)
        (:TYPE-PRESCRIPTION MEM)
        (:TYPE-PRESCRIPTION SUB))
Warnings:  Free
Time:  0.10 seconds (prove: 0.03, print: 0.06, other: 0.01)

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


ACL2 >>(THEOREM PROBLEM-50A
                (EQUAL (SUB (APP A B) C)
                       (AND (SUB A C) (SUB B C)))
                :HINTS
                (("Goal" :INDUCT (SUB A C)
                         :IN-THEORY
                         (ENABLE PROBLEM-48A PROBLEM-48 PROBLEM-49A))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (SUB A C).  This
suggestion was produced using the :induction rule SUB.  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 (MEM (CAR A) C)))
              (:P A B C))
     (IMPLIES (AND (CONSP A)
                   (MEM (CAR A) C)
                   (:P (CDR A) B C))
              (:P A B C))).
This induction is justified by the same argument used to admit SUB,
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 (SUB (APP A B) C)
                (AND (SUB A C) (SUB B C)))).

But simplification reduces this to T, using the :definitions APP and
SUB, primitive type reasoning and the :rewrite rule PROBLEM-48A.

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

This simplifies, using the :definition SUB and primitive type reasoning,
to

Subgoal *1/2'
(IMPLIES (AND (CONSP A) (NOT (MEM (CAR A) C)))
         (NOT (SUB (APP A B) C))).

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/2''
(IMPLIES (AND (CONSP (CONS A1 A2))
              (NOT (MEM A1 C)))
         (NOT (SUB (APP (CONS A1 A2) B) C))).

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

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

But simplification reduces this to T, using the :definitions APP and
SUB, the :executable-counterpart of EQUAL, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS, PROBLEM-48 and PROBLEM-49A and
the :type-prescription rules MEM and SUB.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM PROBLEM-50A ...)
Rules: ((:DEFINITION APP)
        (:DEFINITION SUB)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SUB)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE PROBLEM-48)
        (:REWRITE PROBLEM-48A)
        (:REWRITE PROBLEM-49A)
        (:TYPE-PRESCRIPTION MEM)
        (:TYPE-PRESCRIPTION SUB))
Warnings:  None
Time:  0.08 seconds (prove: 0.03, print: 0.03, other: 0.02)

Summary
Form:  (IN-THEORY (DISABLE ...))
Rules: NIL
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
PROBLEM-50A


ACL2 >>(THEOREM PROBLEM-50 (SUB (APP A A) A)
                :HINTS
                (("Goal" :IN-THEORY
                         (ENABLE PROBLEM-48 PROBLEM-50A)))
                :RULE-CLASSES NIL)

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

But we reduce the conjecture to T, by the :executable-counterpart of
IF and the simple :rewrite rules PROBLEM-48 and PROBLEM-50A.

Q.E.D.

Summary
Form:  ( DEFTHM PROBLEM-50 ...)
Rules: ((:EXECUTABLE-COUNTERPART IF)
        (:REWRITE PROBLEM-48)
        (:REWRITE PROBLEM-50A))
Warnings:  None
Time:  0.02 seconds (prove: 0.01, print: 0.00, other: 0.01)
PROBLEM-50


ACL2 >>(DEFUN MAPNIL1 (X A)
              (IF (CONSP X)
                  (MAPNIL1 (CDR X) (CONS NIL A))
                  A))

The admission of MAPNIL1 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 MAPNIL1 is described by
the theorem (OR (CONSP (MAPNIL1 X A)) (EQUAL (MAPNIL1 X A) A)).  We
used primitive type reasoning.

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


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

The admission of NILS 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 NILS is described by the
theorem (OR (EQUAL (NILS X) T) (EQUAL (NILS X) NIL)).  We used primitive
type reasoning.

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


ACL2 >>(THEOREM PROBLEM-51A
                (EQUAL (MAPNIL1 A (CONS NIL B))
                       (CONS NIL (MAPNIL1 A B)))
                :HINTS (("Goal" :INDUCT (MAPNIL1 A B))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (MAPNIL1 A B).  This
suggestion was produced using the :induction rule MAPNIL1.  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) (CONS NIL B)))
              (:P A B))).
This induction is justified by the same argument used to admit MAPNIL1,
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).  Note, however, that the unmeasured variable B is being instantiated.
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 (MAPNIL1 A (CONS NIL B))
                (CONS NIL (MAPNIL1 A B)))).

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

Subgoal *1/1
(IMPLIES (AND (CONSP A)
              (EQUAL (MAPNIL1 (CDR A) (LIST* NIL NIL B))
                     (CONS NIL (MAPNIL1 (CDR A) (CONS NIL B)))))
         (EQUAL (MAPNIL1 A (CONS NIL B))
                (CONS NIL (MAPNIL1 A B)))).

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

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM PROBLEM-51A ...)
Rules: ((:DEFINITION MAPNIL1)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION MAPNIL1))
Warnings:  None
Time:  0.03 seconds (prove: 0.00, print: 0.02, other: 0.01)

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


ACL2 >>(THEOREM PROBLEM-51B
                (IMPLIES (NILS X)
                         (EQUAL (MAPNIL1 X NIL) X))
                :HINTS
                (("Goal" :INDUCT (NILS X)
                         :IN-THEORY (ENABLE PROBLEM-51A))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (NILS X).  This suggestion
was produced using the :induction rule NILS.  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) (CAR X)) (:P X))
     (IMPLIES (AND (CONSP X)
                   (NOT (CAR X))
                   (:P (CDR X)))
              (:P X))).
This induction is justified by the same argument used to admit NILS,
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 (NILS X)
                  (EQUAL (MAPNIL1 X NIL) X))).

By case analysis we reduce the conjecture to

Subgoal *1/3'
(IMPLIES (AND (NOT (CONSP X)) (NILS X))
         (EQUAL (MAPNIL1 X NIL) X)).

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

Subgoal *1/2
(IMPLIES (AND (CONSP X) (CAR X))
         (IMPLIES (NILS X)
                  (EQUAL (MAPNIL1 X NIL) X))).

By case analysis we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X) (CAR X) (NILS X))
         (EQUAL (MAPNIL1 X NIL) X)).

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

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (NOT (CAR X))
              (IMPLIES (NILS (CDR X))
                       (EQUAL (MAPNIL1 (CDR X) NIL) (CDR X))))
         (IMPLIES (NILS X)
                  (EQUAL (MAPNIL1 X NIL) X))).

By case analysis we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP X)
              (NOT (CAR X))
              (IMPLIES (NILS (CDR X))
                       (EQUAL (MAPNIL1 (CDR X) NIL) (CDR X)))
              (NILS X))
         (EQUAL (MAPNIL1 X NIL) X)).

This simplifies, using the :definition NILS and the :executable-counterpart
of EQUAL, to

Subgoal *1/1''
(IMPLIES (AND (CONSP X)
              (NOT (CAR X))
              (EQUAL (MAPNIL1 (CDR X) NIL) (CDR X))
              (NILS (CDR X)))
         (EQUAL (MAPNIL1 X NIL) X)).

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

Subgoal *1/1'''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (NOT X1)
              (EQUAL (MAPNIL1 X2 NIL) X2)
              (NILS X2))
         (EQUAL (MAPNIL1 (CONS X1 X2) NIL)
                (CONS X1 X2))).

But simplification reduces this to T, using the :definition MAPNIL1,
the :executable-counterpart of CONS, primitive type reasoning and the
:rewrite rules CDR-CONS and PROBLEM-51A.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM PROBLEM-51B ...)
Rules: ((:DEFINITION MAPNIL1)
        (:DEFINITION NILS)
        (:DEFINITION NOT)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART CONS)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART MAPNIL1)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION NILS)
        (:REWRITE CDR-CONS)
        (:REWRITE PROBLEM-51A))
Warnings:  None
Time:  0.14 seconds (prove: 0.02, print: 0.11, other: 0.01)

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


ACL2 >>(THEOREM PROBLEM-51
                (IMPLIES (AND (NILS A) (NILS B))
                         (EQUAL (MAPNIL1 A B) (MAPNIL1 B A)))
                :HINTS
                (("Goal" :INDUCT (MAPNIL1 A B)
                         :IN-THEORY
                         (ENABLE PROBLEM-51A PROBLEM-51B))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (MAPNIL1 A B).  This
suggestion was produced using the :induction rule MAPNIL1.  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) (CONS NIL B)))
              (:P A B))).
This induction is justified by the same argument used to admit MAPNIL1,
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).  Note, however, that the unmeasured variable B is being instantiated.
When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.

Subgoal *1/2
(IMPLIES (NOT (CONSP A))
         (IMPLIES (AND (NILS A) (NILS B))
                  (EQUAL (MAPNIL1 A B) (MAPNIL1 B A)))).

By case analysis we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (NOT (CONSP A)) (NILS A) (NILS B))
         (EQUAL (MAPNIL1 A B) (MAPNIL1 B A))).

But simplification reduces this to T, using the :definitions MAPNIL1
and NILS, the :executable-counterpart of CONSP, primitive type reasoning,
the :rewrite rule PROBLEM-51B and the :type-prescription rule NILS.

Subgoal *1/1
(IMPLIES (AND (CONSP A)
              (IMPLIES (AND (NILS (CDR A)) (NILS (CONS NIL B)))
                       (EQUAL (MAPNIL1 (CDR A) (CONS NIL B))
                              (MAPNIL1 (CONS NIL B) (CDR A)))))
         (IMPLIES (AND (NILS A) (NILS B))
                  (EQUAL (MAPNIL1 A B) (MAPNIL1 B A)))).

By the simple :rewrite rule PROBLEM-51A we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP A)
              (IMPLIES (AND (NILS (CDR A)) (NILS (CONS NIL B)))
                       (EQUAL (CONS NIL (MAPNIL1 (CDR A) B))
                              (MAPNIL1 (CONS NIL B) (CDR A))))
              (NILS A)
              (NILS B))
         (EQUAL (MAPNIL1 A B) (MAPNIL1 B A))).

This simplifies, using the :definitions MAPNIL1 and NILS, the :executable-
counterpart of EQUAL, primitive type reasoning, the :rewrite rules
CAR-CONS, CDR-CONS, CONS-EQUAL and PROBLEM-51A and the :type-prescription
rule NILS, to

Subgoal *1/1''
(IMPLIES (AND (CONSP A)
              (EQUAL (MAPNIL1 (CDR A) B)
                     (MAPNIL1 B (CDR A)))
              (NOT (CAR A))
              (NILS (CDR A))
              (NILS B))
         (EQUAL (MAPNIL1 (CDR A) (CONS NIL B))
                (MAPNIL1 B A))).

By the simple :rewrite rule PROBLEM-51A we reduce the conjecture to

Subgoal *1/1'''
(IMPLIES (AND (CONSP A)
              (EQUAL (MAPNIL1 (CDR A) B)
                     (MAPNIL1 B (CDR A)))
              (NOT (CAR A))
              (NILS (CDR A))
              (NILS B))
         (EQUAL (CONS NIL (MAPNIL1 (CDR A) B))
                (MAPNIL1 B A))).

This simplifies, using trivial observations, to

Subgoal *1/1'4'
(IMPLIES (AND (CONSP A)
              (EQUAL (MAPNIL1 (CDR A) B)
                     (MAPNIL1 B (CDR A)))
              (NOT (CAR A))
              (NILS (CDR A))
              (NILS B))
         (EQUAL (CONS NIL (MAPNIL1 B (CDR A)))
                (MAPNIL1 B 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'5'
(IMPLIES (AND (CONSP (CONS A1 A2))
              (EQUAL (MAPNIL1 A2 B) (MAPNIL1 B A2))
              (NOT A1)
              (NILS A2)
              (NILS B))
         (EQUAL (CONS NIL (MAPNIL1 B A2))
                (MAPNIL1 B (CONS A1 A2)))).

But simplification reduces this to T, using primitive type reasoning
and the :rewrite rule PROBLEM-51A.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM PROBLEM-51 ...)
Rules: ((:DEFINITION MAPNIL1)
        (:DEFINITION NILS)
        (:DEFINITION NOT)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION MAPNIL1)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE CONS-EQUAL)
        (:REWRITE PROBLEM-51A)
        (:REWRITE PROBLEM-51B)
        (:TYPE-PRESCRIPTION NILS))
Warnings:  None
Time:  0.07 seconds (prove: 0.02, print: 0.04, other: 0.01)

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


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

The admission of RM 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 could deduce no constraints on the type of RM.

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


ACL2 >>(DEFUN PERM (X Y)
              (IF (CONSP X)
                  (AND (MEM (CAR X) Y)
                       (PERM (CDR X) (RM (CAR X) Y)))
                  (NOT (CONSP Y))))

The admission of PERM 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 PERM is described by the
theorem (OR (EQUAL (PERM X Y) T) (EQUAL (PERM X Y) NIL)).  

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


ACL2 >>(THEOREM PROBLEM-53 (PERM X X)
                :HINTS (("Goal" :INDUCT (PERM X X))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (PERM X X).  This
suggestion was produced using the :induction rule PERM.  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 (MEM (CAR X) X)))
              (:P X))
     (IMPLIES (AND (CONSP X)
                   (MEM (CAR X) X)
                   (:P (CDR X)))
              (:P X))).
This induction is justified by the same argument used to admit PERM,
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)) (PERM X X)).

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

Subgoal *1/2
(IMPLIES (AND (CONSP X) (NOT (MEM (CAR X) X)))
         (PERM X X)).

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

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) X)
              (PERM (CDR X) (CDR X)))
         (PERM X X)).

But simplification reduces this to T, using the :definitions MEM, PERM
and RM, primitive type reasoning and the :type-prescription rule PERM.

That completes the proof of *1.

Q.E.D.

The storage of PROBLEM-53 depends upon the :type-prescription rule
PERM.

Summary
Form:  ( DEFTHM PROBLEM-53 ...)
Rules: ((:DEFINITION MEM)
        (:DEFINITION PERM)
        (:DEFINITION RM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION PERM)
        (:TYPE-PRESCRIPTION PERM))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)

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


ACL2 >>(THEOREM PROBLEM-54A
                (IMPLIES (MEM A X)
                         (EQUAL (PERM X (CONS A Y))
                                (PERM (RM A X) Y)))
                :HINTS (("Goal" :INDUCT (PERM X Y))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (PERM X Y).  This
suggestion was produced using the :induction rule PERM.  If we let
 (:P A X Y) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P A X Y))
     (IMPLIES (AND (CONSP X) (NOT (MEM (CAR X) Y)))
              (:P A X Y))
     (IMPLIES (AND (CONSP X)
                   (MEM (CAR X) Y)
                   (:P A (CDR X) (RM (CAR X) Y)))
              (:P A X Y))).
This induction is justified by the same argument used to admit PERM,
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).  Note, however, that the unmeasured variable Y is being instantiated.
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 (MEM A X)
                  (EQUAL (PERM X (CONS A Y))
                         (PERM (RM A X) Y)))).

By case analysis we reduce the conjecture to

Subgoal *1/3'
(IMPLIES (AND (NOT (CONSP X)) (MEM A X))
         (EQUAL (PERM X (CONS A Y))
                (PERM (RM A X) Y))).

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

Subgoal *1/2
(IMPLIES (AND (CONSP X) (NOT (MEM (CAR X) Y)))
         (IMPLIES (MEM A X)
                  (EQUAL (PERM X (CONS A Y))
                         (PERM (RM A X) Y)))).

By case analysis we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (NOT (MEM (CAR X) Y))
              (MEM A X))
         (EQUAL (PERM X (CONS A Y))
                (PERM (RM A X) Y))).

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

Subgoal *1/2''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (NOT (MEM X1 Y))
              (MEM A (CONS X1 X2)))
         (EQUAL (PERM (CONS X1 X2) (CONS A Y))
                (PERM (RM A (CONS X1 X2)) Y))).

This simplifies, using the :definitions MEM, PERM and RM, primitive
type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to

Subgoal *1/2'''
(IMPLIES (AND (NOT (MEM X1 Y))
              (MEM A X2)
              (NOT (EQUAL X1 A)))
         (EQUAL NIL (PERM (CONS X1 (RM A X2)) Y))).

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

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Y)
              (IMPLIES (MEM A (CDR X))
                       (EQUAL (PERM (CDR X) (CONS A (RM (CAR X) Y)))
                              (PERM (RM A (CDR X)) (RM (CAR X) Y)))))
         (IMPLIES (MEM A X)
                  (EQUAL (PERM X (CONS A Y))
                         (PERM (RM A X) Y)))).

By case analysis we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Y)
              (IMPLIES (MEM A (CDR X))
                       (EQUAL (PERM (CDR X) (CONS A (RM (CAR X) Y)))
                              (PERM (RM A (CDR X)) (RM (CAR X) Y))))
              (MEM A X))
         (EQUAL (PERM X (CONS A Y))
                (PERM (RM A X) Y))).

This simplifies, using the :definitions MEM, PERM and RM, primitive
type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to the
following two conjectures.

Subgoal *1/1.2
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Y)
              (EQUAL (PERM (CDR X) (CONS A (RM (CAR X) Y)))
                     (PERM (RM A (CDR X)) (RM (CAR X) Y)))
              (MEM A (CDR X))
              (EQUAL A (CAR X)))
         (EQUAL (PERM X (CONS A Y))
                (PERM (CDR X) Y))).

But simplification reduces this to T, using the :definitions MEM, PERM
and RM, primitive type reasoning and the :rewrite rules CAR-CONS and
CDR-CONS.

Subgoal *1/1.1
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Y)
              (EQUAL (PERM (CDR X) (CONS A (RM (CAR X) Y)))
                     (PERM (RM A (CDR X)) (RM (CAR X) Y)))
              (MEM A (CDR X))
              (NOT (EQUAL A (CAR X))))
         (EQUAL (PERM X (CONS A Y))
                (PERM (CONS (CAR X) (RM A (CDR X)))
                      Y))).

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

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM PROBLEM-54A ...)
Rules: ((:DEFINITION MEM)
        (:DEFINITION NOT)
        (:DEFINITION PERM)
        (:DEFINITION RM)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION PERM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION MEM))
Warnings:  None
Time:  0.12 seconds (prove: 0.07, print: 0.05, other: 0.00)

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


ACL2 >>(THEOREM PROBLEM-54
                (IMPLIES (PERM X Y) (PERM Y X))
                :HINTS
                (("Goal" :INDUCT (PERM X Y)
                         :IN-THEORY (ENABLE PROBLEM-54A))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (PERM X Y).  This
suggestion was produced using the :induction rule PERM.  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 (MEM (CAR X) Y)))
              (:P X Y))
     (IMPLIES (AND (CONSP X)
                   (MEM (CAR X) Y)
                   (:P (CDR X) (RM (CAR X) Y)))
              (:P X Y))).
This induction is justified by the same argument used to admit PERM,
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).  Note, however, that the unmeasured variable Y is being instantiated.
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 (PERM X Y) (PERM Y X))).

By case analysis we reduce the conjecture to

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

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

Subgoal *1/2
(IMPLIES (AND (CONSP X) (NOT (MEM (CAR X) Y)))
         (IMPLIES (PERM X Y) (PERM Y X))).

By case analysis we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (NOT (MEM (CAR X) Y))
              (PERM X Y))
         (PERM Y X)).

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

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Y)
              (IMPLIES (PERM (CDR X) (RM (CAR X) Y))
                       (PERM (RM (CAR X) Y) (CDR X))))
         (IMPLIES (PERM X Y) (PERM Y X))).

By case analysis we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Y)
              (IMPLIES (PERM (CDR X) (RM (CAR X) Y))
                       (PERM (RM (CAR X) Y) (CDR X)))
              (PERM X Y))
         (PERM Y X)).

This simplifies, using the :definition PERM and the :type-prescription
rule MEM, to

Subgoal *1/1''
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Y)
              (PERM (RM (CAR X) Y) (CDR X))
              (PERM (CDR X) (RM (CAR X) Y)))
         (PERM Y X)).

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

Subgoal *1/1'''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (MEM X1 Y)
              (PERM (RM X1 Y) X2)
              (PERM X2 (RM X1 Y)))
         (PERM Y (CONS X1 X2))).

But simplification reduces this to T, using primitive type reasoning,
the :rewrite rule PROBLEM-54A and the :type-prescription rules MEM
and PERM.

That completes the proof of *1.

Q.E.D.

The storage of PROBLEM-54 depends upon the :type-prescription rule
PERM.

Summary
Form:  ( DEFTHM PROBLEM-54 ...)
Rules: ((:DEFINITION NOT)
        (:DEFINITION PERM)
        (:ELIM CAR-CDR-ELIM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION PERM)
        (:REWRITE PROBLEM-54A)
        (:TYPE-PRESCRIPTION MEM)
        (:TYPE-PRESCRIPTION PERM))
Warnings:  None
Time:  0.11 seconds (prove: 0.02, print: 0.08, other: 0.01)

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


ACL2 >>(THEOREM PROBLEM-55A
                (IMPLIES (MEM A (RM B X)) (MEM A X))
                :HINTS (("Goal" :INDUCT (MEM A X))))

ACL2 Warning [Free] in ( DEFTHM PROBLEM-55A ...):  The :REWRITE rule
generated from PROBLEM-55A contains the free variable B.  This variable
will be chosen by searching for an instance of (MEM A (RM B X)) 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.


[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (MEM A X).  This
suggestion was produced using the :induction rule MEM.  If we let  
(:P A B X) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P A B X))
     (IMPLIES (AND (CONSP X)
                   (NOT (EQUAL A (CAR X)))
                   (:P A B (CDR X)))
              (:P A B X))
     (IMPLIES (AND (CONSP X) (EQUAL A (CAR X)))
              (:P A B X))).
This induction is justified by the same argument used to admit MEM,
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 (MEM A (RM B X)) (MEM A X))).

By case analysis we reduce the conjecture to

Subgoal *1/3'
(IMPLIES (AND (NOT (CONSP X)) (MEM A (RM B X)))
         (MEM A X)).

But simplification reduces this to T, using the :definitions MEM and
RM.

Subgoal *1/2
(IMPLIES (AND (CONSP X)
              (NOT (EQUAL A (CAR X)))
              (IMPLIES (MEM A (RM B (CDR X)))
                       (MEM A (CDR X))))
         (IMPLIES (MEM A (RM B X)) (MEM A X))).

By case analysis we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (NOT (EQUAL A (CAR X)))
              (IMPLIES (MEM A (RM B (CDR X)))
                       (MEM A (CDR X)))
              (MEM A (RM B X)))
         (MEM A X)).

This simplifies, using the :definitions MEM and RM, primitive type
reasoning and the :type-prescription rule MEM, to

Subgoal *1/2''
(IMPLIES (AND (CONSP X)
              (NOT (EQUAL A (CAR X)))
              (NOT (MEM A (RM B (CDR X))))
              (NOT (EQUAL B (CAR X)))
              (MEM A (CONS (CAR X) (RM B (CDR X)))))
         (MEM A (CDR X))).

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

Subgoal *1/1
(IMPLIES (AND (CONSP X) (EQUAL A (CAR X)))
         (IMPLIES (MEM A (RM B X)) (MEM A X))).

By case analysis we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP X)
              (EQUAL A (CAR X))
              (MEM A (RM B X)))
         (MEM A X)).

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

That completes the proof of *1.

Q.E.D.

The storage of PROBLEM-55A depends upon the :type-prescription rule
MEM.

Summary
Form:  ( DEFTHM PROBLEM-55A ...)
Rules: ((:DEFINITION MEM)
        (:DEFINITION NOT)
        (:DEFINITION RM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION MEM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION MEM))
Warnings:  Free
Time:  0.06 seconds (prove: 0.03, print: 0.02, other: 0.01)

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


ACL2 >>(THEOREM PROBLEM-55B
                (IMPLIES (AND (PERM X Y) (MEM A X))
                         (MEM A Y))
                :HINTS
                (("Goal" :INDUCT (PERM X Y)
                         :IN-THEORY (ENABLE PROBLEM-55A))))

ACL2 Warning [Free] in ( DEFTHM PROBLEM-55B ...):  The :REWRITE rule
generated from PROBLEM-55B contains the free variable X.  This variable
will be chosen by searching for an instance of (PERM 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.


[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (PERM X Y).  This
suggestion was produced using the :induction rule PERM.  If we let
 (:P A X Y) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P A X Y))
     (IMPLIES (AND (CONSP X) (NOT (MEM (CAR X) Y)))
              (:P A X Y))
     (IMPLIES (AND (CONSP X)
                   (MEM (CAR X) Y)
                   (:P A (CDR X) (RM (CAR X) Y)))
              (:P A X Y))).
This induction is justified by the same argument used to admit PERM,
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).  Note, however, that the unmeasured variable Y is being instantiated.
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 (AND (PERM X Y) (MEM A X))
                  (MEM A Y))).

By case analysis we reduce the conjecture to

Subgoal *1/3'
(IMPLIES (AND (NOT (CONSP X))
              (PERM X Y)
              (MEM A X))
         (MEM A Y)).

But simplification reduces this to T, using the :definitions MEM and
PERM.

Subgoal *1/2
(IMPLIES (AND (CONSP X) (NOT (MEM (CAR X) Y)))
         (IMPLIES (AND (PERM X Y) (MEM A X))
                  (MEM A Y))).

By case analysis we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (NOT (MEM (CAR X) Y))
              (PERM X Y)
              (MEM A X))
         (MEM A Y)).

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

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Y)
              (IMPLIES (AND (PERM (CDR X) (RM (CAR X) Y))
                            (MEM A (CDR X)))
                       (MEM A (RM (CAR X) Y))))
         (IMPLIES (AND (PERM X Y) (MEM A X))
                  (MEM A Y))).

By case analysis we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Y)
              (IMPLIES (AND (PERM (CDR X) (RM (CAR X) Y))
                            (MEM A (CDR X)))
                       (MEM A (RM (CAR X) Y)))
              (PERM X Y)
              (MEM A X))
         (MEM A Y)).

This simplifies, using the :definitions MEM and PERM, primitive type
reasoning, the :rewrite rule PROBLEM-55A and the :type-prescription
rule MEM, to

Subgoal *1/1''
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Y)
              (NOT (MEM A (CDR X)))
              (PERM (CDR X) (RM (CAR X) Y))
              (EQUAL A (CAR X)))
         (MEM A Y)).

But simplification reduces this to T, using trivial observations.

That completes the proof of *1.

Q.E.D.

The storage of PROBLEM-55B depends upon the :type-prescription rule
MEM.

Summary
Form:  ( DEFTHM PROBLEM-55B ...)
Rules: ((:DEFINITION MEM)
        (:DEFINITION NOT)
        (:DEFINITION PERM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION PERM)
        (:REWRITE PROBLEM-55A)
        (:TYPE-PRESCRIPTION MEM))
Warnings:  Free
Time:  0.15 seconds (prove: 0.01, print: 0.13, other: 0.01)

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


ACL2 >>(THEOREM PROBLEM-55C
                (EQUAL (RM A (RM B X)) (RM B (RM A X)))
                :HINTS (("Goal" :INDUCT (RM A X))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (RM A X).  This suggestion
was produced using the :induction rule RM.  If we let  (:P A B X) denote
*1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P A B X))
     (IMPLIES (AND (CONSP X)
                   (NOT (EQUAL A (CAR X)))
                   (:P A B (CDR X)))
              (:P A B X))
     (IMPLIES (AND (CONSP X) (EQUAL A (CAR X)))
              (:P A B X))).
This induction is justified by the same argument used to admit RM,
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 (RM A (RM B X))
                (RM B (RM A X)))).

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

Subgoal *1/2
(IMPLIES (AND (CONSP X)
              (NOT (EQUAL A (CAR X)))
              (EQUAL (RM A (RM B (CDR X)))
                     (RM B (RM A (CDR X)))))
         (EQUAL (RM A (RM B X))
                (RM B (RM A X)))).

This simplifies, using the :definition RM, primitive type reasoning
and the :rewrite rules CAR-CONS and CDR-CONS, to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (NOT (EQUAL A (CAR X)))
              (EQUAL (RM A (RM B (CDR X)))
                     (RM B (RM A (CDR X))))
              (NOT (EQUAL B (CAR X))))
         (EQUAL (RM A (CONS (CAR X) (RM B (CDR X))))
                (CONS (CAR X) (RM A (RM B (CDR X)))))).

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

Subgoal *1/1
(IMPLIES (AND (CONSP X) (EQUAL A (CAR X)))
         (EQUAL (RM A (RM B X))
                (RM B (RM A X)))).

This simplifies, using the :definition RM and primitive type reasoning,
to

Subgoal *1/1'
(IMPLIES (CONSP X)
         (EQUAL (RM (CAR X) (RM B X))
                (RM B (CDR X)))).

This simplifies, using the :definition RM, to the following two conjectures.

Subgoal *1/1.2
(IMPLIES (AND (CONSP X) (EQUAL B (CAR X)))
         (EQUAL (RM (CAR X) (CDR X))
                (RM B (CDR X)))).

But simplification reduces this to T, using trivial observations.

Subgoal *1/1.1
(IMPLIES (AND (CONSP X) (NOT (EQUAL B (CAR X))))
         (EQUAL (RM (CAR X)
                    (CONS (CAR X) (RM B (CDR X))))
                (RM B (CDR X)))).

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

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM PROBLEM-55C ...)
Rules: ((:DEFINITION RM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION RM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Warnings:  None
Time:  0.07 seconds (prove: 0.02, print: 0.05, other: 0.00)

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


ACL2 >>(THEOREM PROBLEM-55D
                (IMPLIES (AND (NOT (EQUAL E D)) (MEM E X))
                         (MEM E (RM D X)))
                :HINTS
                (("Goal" :INDUCT (RM D X)
                         :IN-THEORY
                         (ENABLE PROBLEM-48 PROBLEM-49A))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (RM D X).  This suggestion
was produced using the :induction rule RM.  If we let  (:P D E X) denote
*1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P D E X))
     (IMPLIES (AND (CONSP X)
                   (NOT (EQUAL D (CAR X)))
                   (:P D E (CDR X)))
              (:P D E X))
     (IMPLIES (AND (CONSP X) (EQUAL D (CAR X)))
              (:P D E X))).
This induction is justified by the same argument used to admit RM,
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 (AND (NOT (EQUAL E D)) (MEM E X))
                  (MEM E (RM D X)))).

By case analysis we reduce the conjecture to

Subgoal *1/3'
(IMPLIES (AND (NOT (CONSP X))
              (NOT (EQUAL E D))
              (MEM E X))
         (MEM E (RM D X))).

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

Subgoal *1/2
(IMPLIES (AND (CONSP X)
              (NOT (EQUAL D (CAR X)))
              (IMPLIES (AND (NOT (EQUAL E D)) (MEM E (CDR X)))
                       (MEM E (RM D (CDR X)))))
         (IMPLIES (AND (NOT (EQUAL E D)) (MEM E X))
                  (MEM E (RM D X)))).

By case analysis we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (NOT (EQUAL D (CAR X)))
              (IMPLIES (AND (NOT (EQUAL E D)) (MEM E (CDR X)))
                       (MEM E (RM D (CDR X))))
              (NOT (EQUAL E D))
              (MEM E X))
         (MEM E (RM D X))).

But simplification reduces this to T, using the :definitions MEM and
RM, the :executable-counterpart of NOT, primitive type reasoning, the
:rewrite rules CAR-CONS, CDR-CONS, PROBLEM-48 and PROBLEM-49A and the
:type-prescription rule MEM.

Subgoal *1/1
(IMPLIES (AND (CONSP X) (EQUAL D (CAR X)))
         (IMPLIES (AND (NOT (EQUAL E D)) (MEM E X))
                  (MEM E (RM D X)))).

By case analysis we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP X)
              (EQUAL D (CAR X))
              (NOT (EQUAL E D))
              (MEM E X))
         (MEM E (RM D X))).

This simplifies, using the :definition RM and primitive type reasoning,
to

Subgoal *1/1''
(IMPLIES (AND (CONSP X)
              (NOT (EQUAL E (CAR X)))
              (MEM E X))
         (MEM E (CDR X))).

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

That completes the proof of *1.

Q.E.D.

The storage of PROBLEM-55D depends upon the :type-prescription rule
MEM.

Summary
Form:  ( DEFTHM PROBLEM-55D ...)
Rules: ((:DEFINITION MEM)
        (:DEFINITION NOT)
        (:DEFINITION RM)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION RM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE PROBLEM-48)
        (:REWRITE PROBLEM-49A)
        (:TYPE-PRESCRIPTION MEM))
Warnings:  None
Time:  0.13 seconds (prove: 0.01, print: 0.10, other: 0.02)

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


ACL2 >>(THEOREM PROBLEM-55E
                (IMPLIES (PERM X Y)
                         (PERM (RM A X) (RM A Y)))
                :HINTS
                (("Goal" :INDUCT (PERM X Y)
                         :IN-THEORY
                         (ENABLE PROBLEM-54A
                                 PROBLEM-54 PROBLEM-55C PROBLEM-55D))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (PERM X Y).  This
suggestion was produced using the :induction rule PERM.  If we let
 (:P A X Y) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P A X Y))
     (IMPLIES (AND (CONSP X) (NOT (MEM (CAR X) Y)))
              (:P A X Y))
     (IMPLIES (AND (CONSP X)
                   (MEM (CAR X) Y)
                   (:P A (CDR X) (RM (CAR X) Y)))
              (:P A X Y))).
This induction is justified by the same argument used to admit PERM,
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).  Note, however, that the unmeasured variable Y is being instantiated.
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 (PERM X Y)
                  (PERM (RM A X) (RM A Y)))).

By case analysis we reduce the conjecture to

Subgoal *1/3'
(IMPLIES (AND (NOT (CONSP X)) (PERM X Y))
         (PERM (RM A X) (RM A Y))).

But simplification reduces this to T, using the :definitions PERM and
RM and the :rewrite rule PROBLEM-54.

Subgoal *1/2
(IMPLIES (AND (CONSP X) (NOT (MEM (CAR X) Y)))
         (IMPLIES (PERM X Y)
                  (PERM (RM A X) (RM A Y)))).

By case analysis we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (NOT (MEM (CAR X) Y))
              (PERM X Y))
         (PERM (RM A X) (RM A Y))).

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

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Y)
              (IMPLIES (PERM (CDR X) (RM (CAR X) Y))
                       (PERM (RM A (CDR X))
                             (RM A (RM (CAR X) Y)))))
         (IMPLIES (PERM X Y)
                  (PERM (RM A X) (RM A Y)))).

By case analysis we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Y)
              (IMPLIES (PERM (CDR X) (RM (CAR X) Y))
                       (PERM (RM A (CDR X))
                             (RM A (RM (CAR X) Y))))
              (PERM X Y))
         (PERM (RM A X) (RM A Y))).

This simplifies, using the :definitions PERM and RM and the :type-
prescription rule MEM, to the following two conjectures.

Subgoal *1/1.2
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Y)
              (PERM (RM A (CDR X))
                    (RM A (RM (CAR X) Y)))
              (PERM (CDR X) (RM (CAR X) Y))
              (EQUAL A (CAR X)))
         (PERM (CDR X) (RM A Y))).

But simplification reduces this to T, using trivial observations.

Subgoal *1/1.1
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Y)
              (PERM (RM A (CDR X))
                    (RM A (RM (CAR X) Y)))
              (PERM (CDR X) (RM (CAR X) Y))
              (NOT (EQUAL A (CAR X))))
         (PERM (CONS (CAR X) (RM A (CDR X)))
               (RM A Y))).

But simplification reduces this to T, using primitive type reasoning,
the :rewrite rules PROBLEM-54, PROBLEM-54A, PROBLEM-55C and PROBLEM-
55D and the :type-prescription rules MEM and PERM.

That completes the proof of *1.

Q.E.D.

The storage of PROBLEM-55E depends upon the :type-prescription rule
PERM.

Summary
Form:  ( DEFTHM PROBLEM-55E ...)
Rules: ((:DEFINITION NOT)
        (:DEFINITION PERM)
        (:DEFINITION RM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION PERM)
        (:REWRITE PROBLEM-54)
        (:REWRITE PROBLEM-54A)
        (:REWRITE PROBLEM-55C)
        (:REWRITE PROBLEM-55D)
        (:TYPE-PRESCRIPTION MEM)
        (:TYPE-PRESCRIPTION PERM))
Warnings:  None
Time:  0.20 seconds (prove: 0.04, print: 0.15, other: 0.01)

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


ACL2 >>(THEOREM PROBLEM-55
                (IMPLIES (AND (PERM X Y) (PERM Y Z))
                         (PERM X Z))
                :HINTS
                (("Goal" :INDUCT (LIST (PERM X Y) (PERM X Z))
                         :IN-THEORY
                         (ENABLE PROBLEM-54 PROBLEM-55B PROBLEM-55E))))

ACL2 Warning [Free] in ( DEFTHM PROBLEM-55 ...):  The :REWRITE rule
generated from PROBLEM-55 contains the free variable Y.  This variable
will be chosen by searching for an instance of (PERM 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.


[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  Two induction schemes are suggested
by the induction hint.  These merge into one derived induction scheme.

We will induct according to a scheme suggested by (PERM X Z), but modified
to accommodate (PERM X Y).  These suggestions were produced using the
:induction rule PERM.  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 (MEM (CAR X) Z)))
              (:P X Y Z))
     (IMPLIES (AND (CONSP X)
                   (MEM (CAR X) Z)
                   (:P (CDR X)
                       (RM (CAR X) Y)
                       (RM (CAR X) Z)))
              (:P X Y Z))).
This induction is justified by the same argument used to admit PERM,
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).  Note, however, that the unmeasured variables Y and Z are being
instantiated.  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 (AND (PERM X Y) (PERM Y Z))
                  (PERM X Z))).

By case analysis we reduce the conjecture to

Subgoal *1/3'
(IMPLIES (AND (NOT (CONSP X))
              (PERM X Y)
              (PERM Y Z))
         (PERM X Z)).

But simplification reduces this to T, using the :definition PERM and
the :rewrite rule PROBLEM-54.

Subgoal *1/2
(IMPLIES (AND (CONSP X) (NOT (MEM (CAR X) Z)))
         (IMPLIES (AND (PERM X Y) (PERM Y Z))
                  (PERM X Z))).

By case analysis we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (NOT (MEM (CAR X) Z))
              (PERM X Y)
              (PERM Y Z))
         (PERM X Z)).

This simplifies, using the :definition PERM, the :rewrite rule PROBLEM-
55B and the :type-prescription rules MEM and PERM, to

Subgoal *1/2''
(IMPLIES (AND (CONSP X)
              (NOT (MEM (CAR X) Z))
              (MEM (CAR X) Y)
              (PERM (CDR X) (RM (CAR X) Y))
              (PERM Y Z))
         (PERM (CDR X) (RM (CAR X) Z))).

But simplification reduces this to T, using the :rewrite rule PROBLEM-
55B and the :type-prescription rules MEM and PERM.

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Z)
              (IMPLIES (AND (PERM (CDR X) (RM (CAR X) Y))
                            (PERM (RM (CAR X) Y) (RM (CAR X) Z)))
                       (PERM (CDR X) (RM (CAR X) Z))))
         (IMPLIES (AND (PERM X Y) (PERM Y Z))
                  (PERM X Z))).

By case analysis we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Z)
              (IMPLIES (AND (PERM (CDR X) (RM (CAR X) Y))
                            (PERM (RM (CAR X) Y) (RM (CAR X) Z)))
                       (PERM (CDR X) (RM (CAR X) Z)))
              (PERM X Y)
              (PERM Y Z))
         (PERM X Z)).

But simplification reduces this to T, using the :definition PERM, the
:rewrite rules PROBLEM-55B and PROBLEM-55E and the :type-prescription
rules MEM and PERM.

That completes the proof of *1.

Q.E.D.

The storage of PROBLEM-55 depends upon the :type-prescription rule
PERM.

Summary
Form:  ( DEFTHM PROBLEM-55 ...)
Rules: ((:DEFINITION NOT)
        (:DEFINITION PERM)
        (:INDUCTION PERM)
        (:REWRITE PROBLEM-54)
        (:REWRITE PROBLEM-55B)
        (:REWRITE PROBLEM-55E)
        (:TYPE-PRESCRIPTION MEM)
        (:TYPE-PRESCRIPTION PERM))
Warnings:  Free
Time:  0.12 seconds (prove: 0.02, print: 0.06, other: 0.04)

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


ACL2 >>(DEFUN <<= (X Y) (LEXORDER X Y))

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

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


ACL2 >>(THEOREM <<=-NON-STRICT-TOTAL-ORDER
                (AND (<<= X X)
                     (IMPLIES (AND (<<= X Y) (<<= Y X))
                              (EQUAL X Y))
                     (IMPLIES (AND (<<= X Y) (<<= Y Z))
                              (<<= X Z))
                     (OR (<<= X Y) (<<= Y X)))
                :RULE-CLASSES NIL)

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

By the simple :definition <<= and the simple :rewrite rule LEXORDER-
REFLEXIVE we reduce the conjecture to the following three conjectures.

Subgoal 3
(IMPLIES (AND (LEXORDER X Y) (LEXORDER Y X))
         (EQUAL X Y)).

But we reduce the conjecture to T, by primitive type reasoning, the
:forward-chaining rule LEXORDER-ANTI-SYMMETRIC and the :type-prescription
rule LEXORDER.

Subgoal 2
(IMPLIES (AND (LEXORDER X Y) (LEXORDER Y Z))
         (LEXORDER X Z)).

But simplification reduces this to T, using the :rewrite rule LEXORDER-
TRANSITIVE and the :type-prescription rule LEXORDER.

Subgoal 1
(OR (LEXORDER X Y) (LEXORDER Y X)).

But we reduce the conjecture to T, by primitive type reasoning, the
:forward-chaining rule LEXORDER-TOTAL and the :type-prescription rule
LEXORDER.

Q.E.D.

Summary
Form:  ( DEFTHM <<=-NON-STRICT-TOTAL-ORDER ...)
Rules: ((:DEFINITION <<=)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING LEXORDER-ANTI-SYMMETRIC)
        (:FORWARD-CHAINING LEXORDER-TOTAL)
        (:REWRITE LEXORDER-REFLEXIVE)
        (:REWRITE LEXORDER-TRANSITIVE)
        (:TYPE-PRESCRIPTION LEXORDER))
Warnings:  None
Time:  0.04 seconds (prove: 0.01, print: 0.03, other: 0.00)
<<=-NON-STRICT-TOTAL-ORDER


ACL2 >>(DEFUN ORDERED (X)
              (IF (CONSP X)
                  (IF (CONSP (CDR X))
                      (AND (<<= (CAR X) (CADR X))
                           (ORDERED (CDR X)))
                      T)
                  T))

The admission of ORDERED 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 ORDERED is described by
the theorem (OR (EQUAL (ORDERED X) T) (EQUAL (ORDERED X) NIL)).  

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


ACL2 >>(DEFUN INSERT (E X)
              (IF (CONSP X)
                  (IF (<<= E (CAR X))
                      (CONS E X)
                      (CONS (CAR X) (INSERT E (CDR X))))
                  (CONS E NIL)))

The admission of INSERT 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 INSERT is described by
the theorem (CONSP (INSERT E X)).  We used primitive type reasoning.

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


ACL2 >>(DEFUN ISORT (X)
              (IF (CONSP X)
                  (INSERT (CAR X) (ISORT (CDR X)))
                  NIL))

The admission of ISORT 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 ISORT is described by
the theorem (OR (CONSP (ISORT X)) (EQUAL (ISORT X) NIL)).  We used
the :type-prescription rule INSERT.

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


ACL2 >>(THEOREM PROBLEM-58A
                (IMPLIES (ORDERED X)
                         (ORDERED (INSERT E X)))
                :HINTS (("Goal" :INDUCT (INSERT E X))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (INSERT E X).  This
suggestion was produced using the :induction rule INSERT.  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 (<<= E (CAR X)))
                   (:P E (CDR X)))
              (:P E X))
     (IMPLIES (AND (CONSP X) (<<= E (CAR X)))
              (:P E X))).
This induction is justified by the same argument used to admit INSERT,
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 (ORDERED X)
                  (ORDERED (INSERT E X)))).

By case analysis we reduce the conjecture to

Subgoal *1/3'
(IMPLIES (AND (NOT (CONSP X)) (ORDERED X))
         (ORDERED (INSERT E X))).

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

Subgoal *1/2
(IMPLIES (AND (CONSP X)
              (NOT (<<= E (CAR X)))
              (IMPLIES (ORDERED (CDR X))
                       (ORDERED (INSERT E (CDR X)))))
         (IMPLIES (ORDERED X)
                  (ORDERED (INSERT E X)))).

By the simple :definition <<= we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (NOT (LEXORDER E (CAR X)))
              (IMPLIES (ORDERED (CDR X))
                       (ORDERED (INSERT E (CDR X))))
              (ORDERED X))
         (ORDERED (INSERT E X))).

This simplifies, using the :definitions <<=, INSERT and ORDERED, primitive
type reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type-
prescription rules INSERT, LEXORDER and ORDERED, to the following four
conjectures.

Subgoal *1/2.4
(IMPLIES (AND (CONSP X)
              (NOT (LEXORDER E (CAR X)))
              (NOT (ORDERED (CDR X)))
              (NOT (CONSP (CDR X))))
         (LEXORDER (CAR X)
                   (CAR (INSERT E (CDR X))))).

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

Subgoal *1/2.3
(IMPLIES (AND (CONSP X)
              (NOT (LEXORDER E (CAR X)))
              (NOT (ORDERED (CDR X)))
              (NOT (CONSP (CDR X))))
         (ORDERED (INSERT E (CDR X)))).

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

Subgoal *1/2.2
(IMPLIES (AND (CONSP X)
              (NOT (LEXORDER E (CAR X)))
              (ORDERED (INSERT E (CDR X)))
              (NOT (CONSP (CDR X))))
         (LEXORDER (CAR X)
                   (CAR (INSERT E (CDR X))))).

But simplification reduces this to T, using the :definitions INSERT
and ORDERED, the :executable-counterpart of CONSP, primitive type reasoning,
the :forward-chaining rule LEXORDER-TOTAL, the :rewrite rules CAR-CONS,
CDR-CONS, LEXORDER-REFLEXIVE and LEXORDER-TRANSITIVE and the :type-
prescription rule LEXORDER.

Subgoal *1/2.1
(IMPLIES (AND (CONSP X)
              (NOT (LEXORDER E (CAR X)))
              (ORDERED (INSERT E (CDR X)))
              (LEXORDER (CAR X) (CADR X))
              (ORDERED (CDR X)))
         (LEXORDER (CAR X)
                   (CAR (INSERT E (CDR X))))).

The destructor terms (CAR X) and (CDR X) can be eliminated.  Furthermore,
those terms are at the root of a chain of two rounds of destructor
elimination. (1) Use CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X)
by X1 and (CDR X) by X2.  (2) Use CAR-CDR-ELIM, again, to replace X2
by (CONS X3 X4), (CAR X2) by X3 and (CDR X2) by X4.    These steps
produce the following two goals.

Subgoal *1/2.1.2
(IMPLIES (AND (NOT (CONSP X2))
              (CONSP (CONS X1 X2))
              (NOT (LEXORDER E X1))
              (ORDERED (INSERT E X2))
              (LEXORDER X1 (CAR X2))
              (ORDERED X2))
         (LEXORDER X1 (CAR (INSERT E X2)))).

But simplification reduces this to T, using the :definitions INSERT
and ORDERED, the :executable-counterpart of CONSP, primitive type reasoning,
the :forward-chaining rule LEXORDER-TOTAL, the :rewrite rules CAR-CONS,
CDR-CONS, DEFAULT-CAR, LEXORDER-REFLEXIVE and LEXORDER-TRANSITIVE and
the :type-prescription rule LEXORDER.

Subgoal *1/2.1.1
(IMPLIES (AND (CONSP (CONS X3 X4))
              (CONSP (LIST* X1 X3 X4))
              (NOT (LEXORDER E X1))
              (ORDERED (INSERT E (CONS X3 X4)))
              (LEXORDER X1 X3)
              (ORDERED (CONS X3 X4)))
         (LEXORDER X1 (CAR (INSERT E (CONS X3 X4))))).

But simplification reduces this to T, using the :definitions <<=, INSERT
and ORDERED, primitive type reasoning, the :forward-chaining rule LEXORDER-
TOTAL, the :rewrite rules CAR-CONS, CDR-CONS, LEXORDER-REFLEXIVE and
LEXORDER-TRANSITIVE and the :type-prescription rule LEXORDER.

Subgoal *1/1
(IMPLIES (AND (CONSP X) (<<= E (CAR X)))
         (IMPLIES (ORDERED X)
                  (ORDERED (INSERT E X)))).

By the simple :definition <<= we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (CONSP X)
              (LEXORDER E (CAR X))
              (ORDERED X))
         (ORDERED (INSERT E X))).

But simplification reduces this to T, using the :definitions <<=, INSERT
and ORDERED, primitive type reasoning, the :rewrite rules CAR-CONS,
CDR-CONS, LEXORDER-REFLEXIVE and LEXORDER-TRANSITIVE and the :type-
prescription rules LEXORDER and ORDERED.

That completes the proof of *1.

Q.E.D.

The storage of PROBLEM-58A depends upon the :type-prescription rule
ORDERED.

Summary
Form:  ( DEFTHM PROBLEM-58A ...)
Rules: ((:DEFINITION <<=)
        (:DEFINITION INSERT)
        (:DEFINITION NOT)
        (:DEFINITION ORDERED)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING LEXORDER-TOTAL)
        (:INDUCTION INSERT)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE DEFAULT-CAR)
        (:REWRITE LEXORDER-REFLEXIVE)
        (:REWRITE LEXORDER-TRANSITIVE)
        (:TYPE-PRESCRIPTION INSERT)
        (:TYPE-PRESCRIPTION LEXORDER)
        (:TYPE-PRESCRIPTION ORDERED))
Warnings:  None
Time:  0.10 seconds (prove: 0.02, print: 0.07, other: 0.01)

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


ACL2 >>(THEOREM PROBLEM-58 (ORDERED (ISORT X))
                :HINTS
                (("Goal" :INDUCT (ISORT X)
                         :IN-THEORY (ENABLE PROBLEM-58A))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (ISORT X).  This
suggestion was produced using the :induction rule ISORT.  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 ISORT,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on th