ACL2 Version 2.5.  Level 1.  Cbd "/v/hank/v92/moore/demo/flying-demo/".
Type :help for help.

ACL2 !>(+ 3 4)
7
ACL2 !>(equal (car (cons 1 '(2 3 4))) 1)
T
ACL2 !>(thm (equal (car (cons x y)) x))

By the simple :rewrite rule CAR-CONS we reduce the conjecture to

Goal'
(EQUAL X X).

But we reduce the conjecture to T, by primitive type reasoning.

Q.E.D.

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

Proof succeeded.
ACL2 !>(endp nil)
T
ACL2 !>(endp '(1 2 3 4))
NIL
ACL2 !>(thm (implies (and (not (endp x))
                          (endp (cdr x))
                          (integerp n)
                          (<= 0 n)
                          (rationalp u))
                     (< (* (len x) u) (+ u n 3))))

By the simple :definition ENDP we reduce the conjecture to

Goal'
(IMPLIES (AND (CONSP X)
              (NOT (CONSP (CDR X)))
              (INTEGERP N)
              (<= 0 N)
              (RATIONALP U))
         (< (* (LEN X) U) (+ U N 3))).

This simplifies, using the :definitions FIX and LEN, the :executable-
counterpart of BINARY-+ and the :rewrite rules COMMUTATIVITY-2-OF-+,
COMMUTATIVITY-OF-+ and UNICITY-OF-1, to

Goal''
(IMPLIES (AND (CONSP X)
              (NOT (CONSP (CDR X)))
              (INTEGERP N)
              (<= 0 N)
              (RATIONALP U))
         (< U (+ 3 N U))).

But simplification reduces this to T, using linear arithmetic.

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION FIX)
        (:DEFINITION IMPLIES)
        (:DEFINITION LEN)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:REWRITE COMMUTATIVITY-2-OF-+)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE UNICITY-OF-1))
Warnings:  None
Time:  0.05 seconds (prove: 0.02, print: 0.01, other: 0.02)

Proof succeeded.
ACL2 !>(defun insert (e x)
        (cond ((endp x) (cons e x))
              ((< e (car x)) (cons e x))
              (t (cons (car x) (insert e (cdr x))))))

The admission of INSERT is trivial, using the relation E0-ORD-< (which
is known to be well-founded on the domain recognized by E0-ORDINALP)
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 !>(insert 3 '(1 2 4 5))
(1 2 3 4 5)
ACL2 !>(defun isort (x)
        (if (endp x)
            nil
          (insert (car x)
                  (isort (cdr x)))))

The admission of ISORT is trivial, using the relation E0-ORD-< (which
is known to be well-founded on the domain recognized by E0-ORDINALP)
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 !>(isort '(5 4 6 7 2 1 0 3))
(0 1 2 3 4 5 6 7)
ACL2 !>(defun ordered (x)
        (cond ((endp x) t)
              ((endp (cdr x)) t)
              (t (and (<= (car x) (car (cdr x)))
                      (ordered (cdr x))))))

The admission of ORDERED is trivial, using the relation E0-ORD-< (which
is known to be well-founded on the domain recognized by E0-ORDINALP)
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 !>(ordered '(1 2 3 4))
T
ACL2 !>(ordered '(1 2 3 3 4))
T
ACL2 !>(ordered '(1 3 2 4))
NIL
ACL2 !>(defthm ordered-isort
         (ordered (isort x)))

Name the formula above *1.

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

We will induct according to a scheme suggested by (ISORT X).  If we
let  (:P X) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X)))
              (:P X))
     (IMPLIES (ENDP 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
E0-ORD-< (which is known to be well-founded on the domain recognized
by E0-ORDINALP).  When applied to the goal at hand the above induction
scheme produces the following two nontautological subgoals.

Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
              (ORDERED (ISORT (CDR X))))
         (ORDERED (ISORT X))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (ORDERED (ISORT (CDR X))))
         (ORDERED (ISORT X))).

This simplifies, using the :definition ISORT, to

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

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

Subgoal *1/2'''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (ORDERED (ISORT X2)))
         (ORDERED (INSERT X1 (ISORT X2)))).

This simplifies, using primitive type reasoning, to

Subgoal *1/2'4'
(IMPLIES (ORDERED (ISORT X2))
         (ORDERED (INSERT X1 (ISORT X2)))).

We generalize this conjecture, replacing (ISORT X2) by IT.  This produces

Subgoal *1/2'5'
(IMPLIES (ORDERED IT)
         (ORDERED (INSERT X1 IT))).

Name the formula above *1.1.

Subgoal *1/1
(IMPLIES (ENDP X) (ORDERED (ISORT X))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
         (ORDERED (ISORT X))).

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

So we now return to *1.1, which is

(IMPLIES (ORDERED IT)
         (ORDERED (INSERT X1 IT))).

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

We will induct according to a scheme suggested by (INSERT X1 IT). 
If we let  (:P IT X1) denote *1.1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP IT))
                   (<= (CAR IT) X1)
                   (:P (CDR IT) X1))
              (:P IT X1))
     (IMPLIES (AND (NOT (ENDP IT)) (< X1 (CAR IT)))
              (:P IT X1))
     (IMPLIES (ENDP IT) (:P IT X1))).
This induction is justified by the same argument used to admit INSERT,
namely, the measure (ACL2-COUNT IT) is decreasing according to the
relation E0-ORD-< (which is known to be well-founded on the domain
recognized by E0-ORDINALP).  When applied to the goal at hand the above
induction scheme produces the following four nontautological subgoals.

Subgoal *1.1/4
(IMPLIES (AND (NOT (ENDP IT))
              (<= (CAR IT) X1)
              (ORDERED (INSERT X1 (CDR IT)))
              (ORDERED IT))
         (ORDERED (INSERT X1 IT))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/4'
(IMPLIES (AND (CONSP IT)
              (<= (CAR IT) X1)
              (ORDERED (INSERT X1 (CDR IT)))
              (ORDERED IT))
         (ORDERED (INSERT X1 IT))).

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 and ORDERED, to the following two conjectures.

Subgoal *1.1/4.2
(IMPLIES (AND (CONSP IT)
              (<= (CAR IT) X1)
              (ORDERED (INSERT X1 (CDR IT)))
              (NOT (CONSP (CDR IT))))
         (<= (CAR IT)
             (CAR (INSERT X1 (CDR IT))))).

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

Subgoal *1.1/4.1
(IMPLIES (AND (CONSP IT)
              (<= (CAR IT) X1)
              (ORDERED (INSERT X1 (CDR IT)))
              (<= (CAR IT) (CADR IT))
              (ORDERED (CDR IT)))
         (<= (CAR IT)
             (CAR (INSERT X1 (CDR IT))))).

The destructor terms (CAR IT) and (CDR IT) 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 IT by (CONS IT1 IT2),
generalizing (CAR IT) to IT1 and (CDR IT) to IT2.  (2) Use CAR-CDR-
ELIM, again, to replace IT2 by (CONS IT3 IT4), generalizing (CAR IT2)
to IT3 and (CDR IT2) to IT4.    These steps produce the following two
goals.

Subgoal *1.1/4.1.2
(IMPLIES (AND (NOT (CONSP IT2))
              (CONSP (CONS IT1 IT2))
              (<= IT1 X1)
              (ORDERED (INSERT X1 IT2))
              (<= IT1 (CAR IT2))
              (ORDERED IT2))
         (<= IT1 (CAR (INSERT X1 IT2)))).

But simplification reduces this to T, using the :definitions INSERT
and ORDERED, primitive type reasoning and the :rewrite rules CAR-CONS,
CDR-CONS, DEFAULT-<-1 and DEFAULT-CAR.

Subgoal *1.1/4.1.1
(IMPLIES (AND (CONSP (CONS IT3 IT4))
              (CONSP (LIST* IT1 IT3 IT4))
              (<= IT1 X1)
              (ORDERED (INSERT X1 (CONS IT3 IT4)))
              (<= IT1 IT3)
              (ORDERED (CONS IT3 IT4)))
         (<= IT1 (CAR (INSERT X1 (CONS IT3 IT4))))).

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

Subgoal *1.1/3
(IMPLIES (AND (NOT (ENDP IT))
              (<= (CAR IT) X1)
              (NOT (ORDERED (CDR IT)))
              (ORDERED IT))
         (ORDERED (INSERT X1 IT))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/3'
(IMPLIES (AND (CONSP IT)
              (<= (CAR IT) X1)
              (NOT (ORDERED (CDR IT)))
              (ORDERED IT))
         (ORDERED (INSERT X1 IT))).

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

Subgoal *1.1/3.2
(IMPLIES (AND (CONSP IT)
              (<= (CAR IT) X1)
              (NOT (ORDERED (CDR IT)))
              (NOT (CONSP (CDR IT))))
         (<= (CAR IT)
             (CAR (INSERT X1 (CDR IT))))).

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

Subgoal *1.1/3.1
(IMPLIES (AND (CONSP IT)
              (<= (CAR IT) X1)
              (NOT (ORDERED (CDR IT)))
              (NOT (CONSP (CDR IT))))
         (ORDERED (INSERT X1 (CDR IT)))).

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

Subgoal *1.1/2
(IMPLIES (AND (NOT (ENDP IT))
              (< X1 (CAR IT))
              (ORDERED IT))
         (ORDERED (INSERT X1 IT))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/2'
(IMPLIES (AND (CONSP IT)
              (< X1 (CAR IT))
              (ORDERED IT))
         (ORDERED (INSERT X1 IT))).

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

Subgoal *1.1/2.2
(IMPLIES (AND (CONSP IT)
              (< X1 (CAR IT))
              (NOT (CONSP (CDR IT))))
         (<= X1 (CAR IT))).

But simplification reduces this to T, using linear arithmetic.

Subgoal *1.1/2.1
(IMPLIES (AND (CONSP IT)
              (< X1 (CAR IT))
              (<= (CAR IT) (CADR IT))
              (ORDERED (CDR IT)))
         (<= X1 (CAR IT))).

But simplification reduces this to T, using linear arithmetic.

Subgoal *1.1/1
(IMPLIES (AND (ENDP IT) (ORDERED IT))
         (ORDERED (INSERT X1 IT))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/1'
(IMPLIES (AND (NOT (CONSP IT)) (ORDERED IT))
         (ORDERED (INSERT X1 IT))).

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

That completes the proofs of *1.1 and *1.

Q.E.D.

The storage of ORDERED-ISORT depends upon the :type-prescription rule
ORDERED.

Summary
Form:  ( DEFTHM ORDERED-ISORT ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION INSERT)
        (:DEFINITION ISORT)
        (:DEFINITION NOT)
        (:DEFINITION ORDERED)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART ORDERED)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE DEFAULT-<-1)
        (:REWRITE DEFAULT-CAR)
        (:TYPE-PRESCRIPTION INSERT)
        (:TYPE-PRESCRIPTION ORDERED))
Warnings:  None
Time:  0.37 seconds (prove: 0.23, print: 0.12, other: 0.02)
 ORDERED-ISORT
ACL2 !>(pe 'perm)
   d      2  (INCLUDE-BOOK "isort")
             \
>L            (DEFUN PERM (X Y)
                     (IF (CONSP X)
                         (AND (MEM (CAR X) Y)
                              (PERM (CDR X) (DEL (CAR X) Y)))
                         (NOT (CONSP Y))))
ACL2 !>(perm '(1 2 3 3 4) '(4 3 1 2 3))
T
ACL2 !>(perm '(1 2 3 3 4) '(4 3 1 2 2))
NIL
ACL2 !>(defthm perm-isort
         (perm (isort x) x))

Name the formula above *1.

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

We will induct according to a scheme suggested by (ISORT X).  If we
let  (:P X) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X)))
              (:P X))
     (IMPLIES (ENDP 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
E0-ORD-< (which is known to be well-founded on the domain recognized
by E0-ORDINALP).  When applied to the goal at hand the above induction
scheme produces the following two nontautological subgoals.

Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
              (PERM (ISORT (CDR X)) (CDR X)))
         (PERM (ISORT X) X)).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (PERM (ISORT (CDR X)) (CDR X)))
         (PERM (ISORT X) X)).

This simplifies, using the :definition ISORT, to

Subgoal *1/2''
(IMPLIES (AND (CONSP X)
              (PERM (ISORT (CDR X)) (CDR X)))
         (PERM (INSERT (CAR X) (ISORT (CDR X)))
               X)).

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

Subgoal *1/2'''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (PERM (ISORT X2) X2))
         (PERM (INSERT X1 (ISORT X2))
               (CONS X1 X2))).

This simplifies, using primitive type reasoning, to

Subgoal *1/2'4'
(IMPLIES (PERM (ISORT X2) X2)
         (PERM (INSERT X1 (ISORT X2))
               (CONS X1 X2))).

We generalize this conjecture, replacing (ISORT X2) by IT.  This produces

Subgoal *1/2'5'
(IMPLIES (PERM IT X2)
         (PERM (INSERT X1 IT) (CONS X1 X2))).

This simplifies, using the :congruence rule PERM-IMPLIES-PERM-CONS-
2, to

Subgoal *1/2'6'
(PERM (INSERT X1 IT) (CONS X1 IT)).

Name the formula above *1.1.

Subgoal *1/1
(IMPLIES (ENDP X) (PERM (ISORT X) X)).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
         (PERM (ISORT X) X)).

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

So we now return to *1.1, which is

(PERM (INSERT X1 IT) (CONS X1 IT)).

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

We will induct according to a scheme suggested by (INSERT X1 IT). 
If we let  (:P IT X1) denote *1.1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP IT))
                   (<= (CAR IT) X1)
                   (:P (CDR IT) X1))
              (:P IT X1))
     (IMPLIES (AND (NOT (ENDP IT)) (< X1 (CAR IT)))
              (:P IT X1))
     (IMPLIES (ENDP IT) (:P IT X1))).
This induction is justified by the same argument used to admit INSERT,
namely, the measure (ACL2-COUNT IT) is decreasing according to the
relation E0-ORD-< (which is known to be well-founded on the domain
recognized by E0-ORDINALP).  When applied to the goal at hand the above
induction scheme produces the following three nontautological subgoals.

Subgoal *1.1/3
(IMPLIES (AND (NOT (ENDP IT))
              (<= (CAR IT) X1)
              (PERM (INSERT X1 (CDR IT))
                    (CONS X1 (CDR IT))))
         (PERM (INSERT X1 IT) (CONS X1 IT))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/3'
(IMPLIES (AND (CONSP IT)
              (<= (CAR IT) X1)
              (PERM (INSERT X1 (CDR IT))
                    (CONS X1 (CDR IT))))
         (PERM (INSERT X1 IT) (CONS X1 IT))).

This simplifies, using the :congruence rule PERM-IMPLIES-PERM-CONS-
2, the :definitions DEL, INSERT, MEM and PERM, primitive type reasoning
and the :rewrite rules CAR-CONS and CDR-CONS, to the following four
conjectures.

Subgoal *1.1/3.4
(IMPLIES (AND (CONSP IT)
              (<= (CAR IT) X1)
              (PERM (INSERT X1 (CDR IT))
                    (CONS X1 (CDR IT)))
              (EQUAL (CAR IT) X1))
         (MEM X1 IT)).

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

Subgoal *1.1/3.3
(IMPLIES (AND (CONSP IT)
              (<= (CAR IT) X1)
              (PERM (INSERT X1 (CDR IT))
                    (CONS X1 (CDR IT)))
              (EQUAL (CAR IT) X1))
         (PERM (CDR IT) (DEL X1 IT))).

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

Subgoal *1.1/3.2
(IMPLIES (AND (CONSP IT)
              (<= (CAR IT) X1)
              (PERM (INSERT X1 (CDR IT))
                    (CONS X1 (CDR IT)))
              (NOT (EQUAL (CAR IT) X1)))
         (MEM X1 (CONS X1 (CDR IT)))).

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

Subgoal *1.1/3.1
(IMPLIES (AND (CONSP IT)
              (<= (CAR IT) X1)
              (PERM (INSERT X1 (CDR IT))
                    (CONS X1 (CDR IT)))
              (NOT (EQUAL (CAR IT) X1)))
         (PERM (CDR IT)
               (DEL X1 (CONS X1 (CDR IT))))).

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

Subgoal *1.1/2
(IMPLIES (AND (NOT (ENDP IT)) (< X1 (CAR IT)))
         (PERM (INSERT X1 IT) (CONS X1 IT))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/2'
(IMPLIES (AND (CONSP IT) (< X1 (CAR IT)))
         (PERM (INSERT X1 IT) (CONS X1 IT))).

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

Subgoal *1.1/1
(IMPLIES (ENDP IT)
         (PERM (INSERT X1 IT) (CONS X1 IT))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/1'
(IMPLIES (NOT (CONSP IT))
         (PERM (INSERT X1 IT) (CONS X1 IT))).

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

That completes the proofs of *1.1 and *1.

Q.E.D.

Summary
Form:  ( DEFTHM PERM-ISORT ...)
Rules: ((:CONGRUENCE PERM-IMPLIES-PERM-CONS-2)
        (:DEFINITION DEL)
        (:DEFINITION ENDP)
        (:DEFINITION INSERT)
        (:DEFINITION ISORT)
        (:DEFINITION MEM)
        (:DEFINITION NOT)
        (:DEFINITION PERM)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CDR-ELIM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Warnings:  None
Time:  0.30 seconds (prove: 0.22, print: 0.07, other: 0.01)
 PERM-ISORT
ACL2 !>(defun buggy-insert (e x)
        (cond ((endp x) x)
              ((< e (car x)) (cons e x))
              (t (cons (car x) (buggy-insert e (cdr x))))))

The admission of BUGGY-INSERT is trivial, using the relation E0-ORD-
< (which is known to be well-founded on the domain recognized by E0-
ORDINALP) and the measure (ACL2-COUNT X).  We could deduce no constraints
on the type of BUGGY-INSERT.

Summary
Form:  ( DEFUN BUGGY-INSERT ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 BUGGY-INSERT
ACL2 !>(buggy-insert 3 '(1 2 4 5))
(1 2 3 4 5)
ACL2 !>(buggy-insert 3 '(1 2))
(1 2)
ACL2 !>(defun buggy-isort (x)
        (if (endp x)
            nil
          (buggy-insert (car x)
                        (buggy-isort (cdr x)))))

The admission of BUGGY-ISORT is trivial, using the relation E0-ORD-
< (which is known to be well-founded on the domain recognized by E0-
ORDINALP) and the measure (ACL2-COUNT X).  We could deduce no constraints
on the type of BUGGY-ISORT.

Summary
Form:  ( DEFUN BUGGY-ISORT ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 BUGGY-ISORT
ACL2 !>(defthm ordered-buggy-isort
         (ordered (buggy-isort x)))

Name the formula above *1.

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

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

Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
              (ORDERED (BUGGY-ISORT (CDR X))))
         (ORDERED (BUGGY-ISORT X))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (ORDERED (BUGGY-ISORT (CDR X))))
         (ORDERED (BUGGY-ISORT X))).

This simplifies, using the :definition BUGGY-ISORT, to

Subgoal *1/2''
(IMPLIES (AND (CONSP X)
              (ORDERED (BUGGY-ISORT (CDR X))))
         (ORDERED (BUGGY-INSERT (CAR X)
                                (BUGGY-ISORT (CDR X))))).

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

Subgoal *1/2'''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (ORDERED (BUGGY-ISORT X2)))
         (ORDERED (BUGGY-INSERT X1 (BUGGY-ISORT X2)))).

This simplifies, using primitive type reasoning, to

Subgoal *1/2'4'
(IMPLIES (ORDERED (BUGGY-ISORT X2))
         (ORDERED (BUGGY-INSERT X1 (BUGGY-ISORT X2)))).

We generalize this conjecture, replacing (BUGGY-ISORT X2) by BIT. 
This produces

Subgoal *1/2'5'
(IMPLIES (ORDERED BIT)
         (ORDERED (BUGGY-INSERT X1 BIT))).

Name the formula above *1.1.

Subgoal *1/1
(IMPLIES (ENDP X)
         (ORDERED (BUGGY-ISORT X))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
         (ORDERED (BUGGY-ISORT X))).

But simplification reduces this to T, using the :definition BUGGY-ISORT
and the :executable-counterpart of ORDERED.

So we now return to *1.1, which is

(IMPLIES (ORDERED BIT)
         (ORDERED (BUGGY-INSERT X1 BIT))).

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

We will induct according to a scheme suggested by (BUGGY-INSERT X1 BIT).
If we let  (:P BIT X1) denote *1.1 above then the induction scheme
we'll use is
(AND (IMPLIES (AND (NOT (ENDP BIT))
                   (<= (CAR BIT) X1)
                   (:P (CDR BIT) X1))
              (:P BIT X1))
     (IMPLIES (AND (NOT (ENDP BIT)) (< X1 (CAR BIT)))
              (:P BIT X1))
     (IMPLIES (ENDP BIT) (:P BIT X1))).
This induction is justified by the same argument used to admit BUGGY-
INSERT, namely, the measure (ACL2-COUNT BIT) is decreasing according
to the relation E0-ORD-< (which is known to be well-founded on the
domain recognized by E0-ORDINALP).  When applied to the goal at hand
the above induction scheme produces the following four nontautological
subgoals.

Subgoal *1.1/4
(IMPLIES (AND (NOT (ENDP BIT))
              (<= (CAR BIT) X1)
              (ORDERED (BUGGY-INSERT X1 (CDR BIT)))
              (ORDERED BIT))
         (ORDERED (BUGGY-INSERT X1 BIT))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/4'
(IMPLIES (AND (CONSP BIT)
              (<= (CAR BIT) X1)
              (ORDERED (BUGGY-INSERT X1 (CDR BIT)))
              (ORDERED BIT))
         (ORDERED (BUGGY-INSERT X1 BIT))).

This simplifies, using the :definitions BUGGY-INSERT and ORDERED, primitive
type reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type-
prescription rule ORDERED, to the following two conjectures.

Subgoal *1.1/4.2
(IMPLIES (AND (CONSP BIT)
              (<= (CAR BIT) X1)
              (ORDERED (BUGGY-INSERT X1 (CDR BIT)))
              (NOT (CONSP (CDR BIT)))
              (CONSP (BUGGY-INSERT X1 (CDR BIT))))
         (<= (CAR BIT)
             (CAR (BUGGY-INSERT X1 (CDR BIT))))).

But simplification reduces this to T, using the :definitions BUGGY-
INSERT and ORDERED.

Subgoal *1.1/4.1
(IMPLIES (AND (CONSP BIT)
              (<= (CAR BIT) X1)
              (ORDERED (BUGGY-INSERT X1 (CDR BIT)))
              (<= (CAR BIT) (CADR BIT))
              (ORDERED (CDR BIT))
              (CONSP (BUGGY-INSERT X1 (CDR BIT))))
         (<= (CAR BIT)
             (CAR (BUGGY-INSERT X1 (CDR BIT))))).

The destructor terms (CAR BIT) and (CDR BIT) 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 BIT by (CONS BIT1 BIT2),
generalizing (CAR BIT) to BIT1 and (CDR BIT) to BIT2.  (2) Use CAR-
CDR-ELIM, again, to replace BIT2 by (CONS BIT3 BIT4), generalizing
(CAR BIT2) to BIT3 and (CDR BIT2) to BIT4.    These steps produce the
following two goals.

Subgoal *1.1/4.1.2
(IMPLIES (AND (NOT (CONSP BIT2))
              (CONSP (CONS BIT1 BIT2))
              (<= BIT1 X1)
              (ORDERED (BUGGY-INSERT X1 BIT2))
              (<= BIT1 (CAR BIT2))
              (ORDERED BIT2)
              (CONSP (BUGGY-INSERT X1 BIT2)))
         (<= BIT1 (CAR (BUGGY-INSERT X1 BIT2)))).

But simplification reduces this to T, using the :definitions BUGGY-
INSERT and ORDERED, primitive type reasoning and the :rewrite rules
DEFAULT-<-1 and DEFAULT-CAR.

Subgoal *1.1/4.1.1
(IMPLIES (AND (CONSP (CONS BIT3 BIT4))
              (CONSP (LIST* BIT1 BIT3 BIT4))
              (<= BIT1 X1)
              (ORDERED (BUGGY-INSERT X1 (CONS BIT3 BIT4)))
              (<= BIT1 BIT3)
              (ORDERED (CONS BIT3 BIT4))
              (CONSP (BUGGY-INSERT X1 (CONS BIT3 BIT4))))
         (<= BIT1
             (CAR (BUGGY-INSERT X1 (CONS BIT3 BIT4))))).

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

Subgoal *1.1/3
(IMPLIES (AND (NOT (ENDP BIT))
              (<= (CAR BIT) X1)
              (NOT (ORDERED (CDR BIT)))
              (ORDERED BIT))
         (ORDERED (BUGGY-INSERT X1 BIT))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/3'
(IMPLIES (AND (CONSP BIT)
              (<= (CAR BIT) X1)
              (NOT (ORDERED (CDR BIT)))
              (ORDERED BIT))
         (ORDERED (BUGGY-INSERT X1 BIT))).

This simplifies, using the :definitions BUGGY-INSERT and ORDERED, primitive
type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to the
following two conjectures.

Subgoal *1.1/3.2
(IMPLIES (AND (CONSP BIT)
              (<= (CAR BIT) X1)
              (NOT (ORDERED (CDR BIT)))
              (NOT (CONSP (CDR BIT)))
              (CONSP (BUGGY-INSERT X1 (CDR BIT))))
         (<= (CAR BIT)
             (CAR (BUGGY-INSERT X1 (CDR BIT))))).

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

Subgoal *1.1/3.1
(IMPLIES (AND (CONSP BIT)
              (<= (CAR BIT) X1)
              (NOT (ORDERED (CDR BIT)))
              (NOT (CONSP (CDR BIT)))
              (CONSP (BUGGY-INSERT X1 (CDR BIT))))
         (ORDERED (BUGGY-INSERT X1 (CDR BIT)))).

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

Subgoal *1.1/2
(IMPLIES (AND (NOT (ENDP BIT))
              (< X1 (CAR BIT))
              (ORDERED BIT))
         (ORDERED (BUGGY-INSERT X1 BIT))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/2'
(IMPLIES (AND (CONSP BIT)
              (< X1 (CAR BIT))
              (ORDERED BIT))
         (ORDERED (BUGGY-INSERT X1 BIT))).

This simplifies, using the :definitions BUGGY-INSERT and ORDERED, primitive
type reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type-
prescription rule ORDERED, to the following two conjectures.

Subgoal *1.1/2.2
(IMPLIES (AND (CONSP BIT)
              (< X1 (CAR BIT))
              (NOT (CONSP (CDR BIT))))
         (<= X1 (CAR BIT))).

But simplification reduces this to T, using linear arithmetic.

Subgoal *1.1/2.1
(IMPLIES (AND (CONSP BIT)
              (< X1 (CAR BIT))
              (<= (CAR BIT) (CADR BIT))
              (ORDERED (CDR BIT)))
         (<= X1 (CAR BIT))).

But simplification reduces this to T, using linear arithmetic.

Subgoal *1.1/1
(IMPLIES (AND (ENDP BIT) (ORDERED BIT))
         (ORDERED (BUGGY-INSERT X1 BIT))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/1'
(IMPLIES (AND (NOT (CONSP BIT)) (ORDERED BIT))
         (ORDERED (BUGGY-INSERT X1 BIT))).

But simplification reduces this to T, using the :definitions BUGGY-
INSERT and ORDERED.

That completes the proofs of *1.1 and *1.

Q.E.D.

The storage of ORDERED-BUGGY-ISORT depends upon the :type-prescription
rule ORDERED.

Summary
Form:  ( DEFTHM ORDERED-BUGGY-ISORT ...)
Rules: ((:DEFINITION BUGGY-INSERT)
        (:DEFINITION BUGGY-ISORT)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION ORDERED)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART ORDERED)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE DEFAULT-<-1)
        (:REWRITE DEFAULT-CAR)
        (:TYPE-PRESCRIPTION ORDERED))
Warnings:  None
Time:  0.55 seconds (prove: 0.49, print: 0.04, other: 0.02)
 ORDERED-BUGGY-ISORT
ACL2 !>(defthm perm-buggy-isort
         (perm (buggy-isort x) x))

Name the formula above *1.

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

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

Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
              (PERM (BUGGY-ISORT (CDR X)) (CDR X)))
         (PERM (BUGGY-ISORT X) X)).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (PERM (BUGGY-ISORT (CDR X)) (CDR X)))
         (PERM (BUGGY-ISORT X) X)).

This simplifies, using the :definition BUGGY-ISORT, to

Subgoal *1/2''
(IMPLIES (AND (CONSP X)
              (PERM (BUGGY-ISORT (CDR X)) (CDR X)))
         (PERM (BUGGY-INSERT (CAR X)
                             (BUGGY-ISORT (CDR X)))
               X)).

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

Subgoal *1/2'''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (PERM (BUGGY-ISORT X2) X2))
         (PERM (BUGGY-INSERT X1 (BUGGY-ISORT X2))
               (CONS X1 X2))).

This simplifies, using primitive type reasoning, to

Subgoal *1/2'4'
(IMPLIES (PERM (BUGGY-ISORT X2) X2)
         (PERM (BUGGY-INSERT X1 (BUGGY-ISORT X2))
               (CONS X1 X2))).

We generalize this conjecture, replacing (BUGGY-ISORT X2) by BIT. 
This produces

Subgoal *1/2'5'
(IMPLIES (PERM BIT X2)
         (PERM (BUGGY-INSERT X1 BIT)
               (CONS X1 X2))).

This simplifies, using the :congruence rule PERM-IMPLIES-PERM-CONS-
2, to

Subgoal *1/2'6'
(PERM (BUGGY-INSERT X1 BIT)
      (CONS X1 BIT)).

Name the formula above *1.1.

Subgoal *1/1
(IMPLIES (ENDP X)
         (PERM (BUGGY-ISORT X) X)).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
         (PERM (BUGGY-ISORT X) X)).

But simplification reduces this to T, using the :definitions BUGGY-
ISORT and PERM and the :executable-counterpart of CONSP.

So we now return to *1.1, which is

(PERM (BUGGY-INSERT X1 BIT)
      (CONS X1 BIT)).

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

We will induct according to a scheme suggested by (BUGGY-INSERT X1 BIT).
If we let  (:P BIT X1) denote *1.1 above then the induction scheme
we'll use is
(AND (IMPLIES (AND (NOT (ENDP BIT))
                   (<= (CAR BIT) X1)
                   (:P (CDR BIT) X1))
              (:P BIT X1))
     (IMPLIES (AND (NOT (ENDP BIT)) (< X1 (CAR BIT)))
              (:P BIT X1))
     (IMPLIES (ENDP BIT) (:P BIT X1))).
This induction is justified by the same argument used to admit BUGGY-
INSERT, namely, the measure (ACL2-COUNT BIT) is decreasing according
to the relation E0-ORD-< (which is known to be well-founded on the
domain recognized by E0-ORDINALP).  When applied to the goal at hand
the above induction scheme produces the following three nontautological
subgoals.

Subgoal *1.1/3
(IMPLIES (AND (NOT (ENDP BIT))
              (<= (CAR BIT) X1)
              (PERM (BUGGY-INSERT X1 (CDR BIT))
                    (CONS X1 (CDR BIT))))
         (PERM (BUGGY-INSERT X1 BIT)
               (CONS X1 BIT))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/3'
(IMPLIES (AND (CONSP BIT)
              (<= (CAR BIT) X1)
              (PERM (BUGGY-INSERT X1 (CDR BIT))
                    (CONS X1 (CDR BIT))))
         (PERM (BUGGY-INSERT X1 BIT)
               (CONS X1 BIT))).

This simplifies, using the :definitions BUGGY-INSERT, DEL, MEM and
PERM, the :equivalence rule PERM-IS-AN-EQUIVALENCE, primitive type
reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to the following
two conjectures.

Subgoal *1.1/3.2
(IMPLIES (AND (CONSP BIT)
              (<= (CAR BIT) X1)
              (PERM (BUGGY-INSERT X1 (CDR BIT))
                    (CONS X1 (CDR BIT)))
              (EQUAL (CAR BIT) X1))
         (PERM (BUGGY-INSERT X1 (CDR BIT)) BIT)).

But simplification reduces this to T, using the :rewrite rule CAR-CDR-
ELIM.

Subgoal *1.1/3.1
(IMPLIES (AND (CONSP BIT)
              (<= (CAR BIT) X1)
              (PERM (BUGGY-INSERT X1 (CDR BIT))
                    (CONS X1 (CDR BIT)))
              (NOT (EQUAL (CAR BIT) X1)))
         (PERM (BUGGY-INSERT X1 (CDR BIT))
               (BUGGY-INSERT X1 (CDR BIT)))).

But simplification reduces this to T, using primitive type reasoning.

Subgoal *1.1/2
(IMPLIES (AND (NOT (ENDP BIT)) (< X1 (CAR BIT)))
         (PERM (BUGGY-INSERT X1 BIT)
               (CONS X1 BIT))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/2'
(IMPLIES (AND (CONSP BIT) (< X1 (CAR BIT)))
         (PERM (BUGGY-INSERT X1 BIT)
               (CONS X1 BIT))).

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

Subgoal *1.1/1
(IMPLIES (ENDP BIT)
         (PERM (BUGGY-INSERT X1 BIT)
               (CONS X1 BIT))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/1'
(IMPLIES (NOT (CONSP BIT))
         (PERM (BUGGY-INSERT X1 BIT)
               (CONS X1 BIT))).

This simplifies, using the :definitions BUGGY-INSERT and PERM and primitive
type reasoning, to

Subgoal *1.1/1''
(CONSP BIT).

We suspect that this conjecture is not a theorem.  We might as well
be trying to prove

Subgoal *1.1/1'''
NIL.

Obviously, the proof attempt has failed.

Summary
Form:  ( DEFTHM PERM-BUGGY-ISORT ...)
Rules: ((:CONGRUENCE PERM-IMPLIES-PERM-CONS-2)
        (:DEFINITION BUGGY-INSERT)
        (:DEFINITION BUGGY-ISORT)
        (:DEFINITION DEL)
        (:DEFINITION ENDP)
        (:DEFINITION MEM)
        (:DEFINITION NOT)
        (:DEFINITION PERM)
        (:ELIM CAR-CDR-ELIM)
        (:EQUIVALENCE PERM-IS-AN-EQUIVALENCE)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CDR-ELIM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Warnings:  None
Time:  0.24 seconds (prove: 0.18, print: 0.05, other: 0.01)

******** FAILED ********  See :DOC failure  ******** FAILED ********
ACL2 !>(defthm buggy-isort-is-nil
  (equal (buggy-isort x) nil))

By case analysis we reduce the conjecture to

Goal'
(NOT (BUGGY-ISORT X)).

Name the formula above *1.

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

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

Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
              (NOT (BUGGY-ISORT (CDR X))))
         (NOT (BUGGY-ISORT X))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (NOT (BUGGY-ISORT (CDR X))))
         (NOT (BUGGY-ISORT X))).

But simplification reduces this to T, using the :definitions BUGGY-
INSERT and BUGGY-ISORT and the :executable-counterpart of CONSP.

Subgoal *1/1
(IMPLIES (ENDP X)
         (NOT (BUGGY-ISORT X))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
         (NOT (BUGGY-ISORT X))).

But simplification reduces this to T, using the :definition BUGGY-ISORT.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM BUGGY-ISORT-IS-NIL ...)
Rules: ((:DEFINITION BUGGY-INSERT)
        (:DEFINITION BUGGY-ISORT)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART CONSP))
Warnings:  None
Time:  0.03 seconds (prove: 0.01, print: 0.01, other: 0.01)
 BUGGY-ISORT-IS-NIL
ACL2 !>(defun full-adder (p q c)
        (mv (xor p (xor q c))
            (maj p q c)))

Since FULL-ADDER is non-recursive, its admission is trivial.  We observe
that the type of FULL-ADDER is described by the theorem 
(AND (CONSP (FULL-ADDER P Q C)) (TRUE-LISTP (FULL-ADDER P Q C))). 
We used primitive type reasoning.

(FULL-ADDER * * *) => (MV * *).

Summary
Form:  ( DEFUN FULL-ADDER ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
 FULL-ADDER
ACL2 !>(full-adder t t nil)
(NIL T)
ACL2 !>(full-adder nil nil t)
(T NIL)
ACL2 !>(defun serial-adder (a b c)
        (declare (xargs :measure (+ (acl2-count a) (acl2-count b))))
        (if (and (endp a) (endp b))
            (list c)
          (mv-let (sum cout)
                  (full-adder (car a) (car b) c)
                  (cons sum (serial-adder (cdr a) (cdr b) cout)))))

For the admission of SERIAL-ADDER we will use the relation E0-ORD-<
(which is known to be well-founded on the domain recognized by E0-ORDINALP)
and the measure (+ (ACL2-COUNT A) (ACL2-COUNT B)).  The non-trivial
part of the measure conjecture is

Goal
(AND (E0-ORDINALP (+ (ACL2-COUNT A) (ACL2-COUNT B)))
     (IMPLIES (NOT (AND (ENDP A) (ENDP B)))
              (E0-ORD-< (+ (ACL2-COUNT (CDR A))
                           (ACL2-COUNT (CDR B)))
                        (+ (ACL2-COUNT A) (ACL2-COUNT B))))).

By case analysis we reduce the conjecture to the following two conjectures.

Subgoal 2
(E0-ORDINALP (+ (ACL2-COUNT A) (ACL2-COUNT B))).

But simplification reduces this to T, using the :definition E0-ORDINALP,
primitive type reasoning and the :type-prescription rule ACL2-COUNT.

Subgoal 1
(IMPLIES (NOT (AND (ENDP A) (ENDP B)))
         (E0-ORD-< (+ (ACL2-COUNT (CDR A))
                      (ACL2-COUNT (CDR B)))
                   (+ (ACL2-COUNT A) (ACL2-COUNT B)))).

This simplifies, using the :definitions E0-ORD-< and ENDP, primitive
type reasoning and the :type-prescription rule ACL2-COUNT, to the following
two conjectures.

Subgoal 1.2
(IMPLIES (CONSP A)
         (< (+ (ACL2-COUNT (CDR A))
               (ACL2-COUNT (CDR B)))
            (+ (ACL2-COUNT A) (ACL2-COUNT B)))).

The destructor terms (CAR B) and (CDR B) can be eliminated by using
CAR-CDR-ELIM to replace B by (CONS B1 B2), generalizing (CAR B) to
B1 and (CDR B) to B2.  This produces the following two goals.

Subgoal 1.2.2
(IMPLIES (AND (NOT (CONSP B)) (CONSP A))
         (< (+ (ACL2-COUNT (CDR A))
               (ACL2-COUNT (CDR B)))
            (+ (ACL2-COUNT A) (ACL2-COUNT B)))).

This simplifies, using the :definition FIX, the :executable-counterpart
of ACL2-COUNT, the :rewrite rules COMMUTATIVITY-OF-+, DEFAULT-CDR and
UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to

Subgoal 1.2.2'
(IMPLIES (AND (NOT (CONSP B)) (CONSP A))
         (< (ACL2-COUNT (CDR A))
            (+ (ACL2-COUNT A) (ACL2-COUNT B)))).

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

Subgoal 1.2.2''
(IMPLIES (AND (CONSP (CONS A1 A2))
              (NOT (CONSP B)))
         (< (ACL2-COUNT A2)
            (+ (ACL2-COUNT (CONS A1 A2))
               (ACL2-COUNT B)))).

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

Subgoal 1.2.2'''
(IMPLIES (NOT (CONSP B))
         (< (ACL2-COUNT A2)
            (+ 1 (ACL2-COUNT A1)
               (ACL2-COUNT A2)
               (ACL2-COUNT B)))).

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

Subgoal 1.2.1
(IMPLIES (AND (CONSP (CONS B1 B2)) (CONSP A))
         (< (+ (ACL2-COUNT (CDR A)) (ACL2-COUNT B2))
            (+ (ACL2-COUNT A)
               (ACL2-COUNT (CONS B1 B2))))).

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

Subgoal 1.2.1'
(IMPLIES (CONSP A)
         (< (+ (ACL2-COUNT B2) (ACL2-COUNT (CDR A)))
            (+ 1 (ACL2-COUNT A)
               (ACL2-COUNT B1)
               (ACL2-COUNT B2)))).

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

Subgoal 1.2.1''
(IMPLIES (CONSP (CONS A1 A2))
         (< (+ (ACL2-COUNT B2) (ACL2-COUNT A2))
            (+ 1 (ACL2-COUNT (CONS A1 A2))
               (ACL2-COUNT B1)
               (ACL2-COUNT B2)))).

This simplifies, using the :definitions ACL2-COUNT and SYNTAXP, the
:executable-counterparts of BINARY-+, CAR, CONSP, EQ and IF, primitive
type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-
2-OF-+, COMMUTATIVITY-OF-+ and FOLD-CONSTS-IN-+, to

Subgoal 1.2.1'''
(< (+ (ACL2-COUNT A2) (ACL2-COUNT B2))
   (+ 2 (ACL2-COUNT A1)
      (ACL2-COUNT A2)
      (ACL2-COUNT B1)
      (ACL2-COUNT B2))).

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

Subgoal 1.1
(IMPLIES (CONSP B)
         (< (+ (ACL2-COUNT (CDR A))
               (ACL2-COUNT (CDR B)))
            (+ (ACL2-COUNT A) (ACL2-COUNT B)))).

The destructor terms (CAR B) and (CDR B) can be eliminated by using
CAR-CDR-ELIM to replace B by (CONS B1 B2), generalizing (CAR B) to
B1 and (CDR B) to B2.  This produces the following goal.

Subgoal 1.1'
(IMPLIES (CONSP (CONS B1 B2))
         (< (+ (ACL2-COUNT (CDR A)) (ACL2-COUNT B2))
            (+ (ACL2-COUNT A)
               (ACL2-COUNT (CONS B1 B2))))).

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

Subgoal 1.1''
(< (+ (ACL2-COUNT B2) (ACL2-COUNT (CDR A)))
   (+ 1 (ACL2-COUNT A)
      (ACL2-COUNT B1)
      (ACL2-COUNT B2))).

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

Subgoal 1.1.2
(IMPLIES (NOT (CONSP A))
         (< (+ (ACL2-COUNT B2) (ACL2-COUNT (CDR A)))
            (+ 1 (ACL2-COUNT A)
               (ACL2-COUNT B1)
               (ACL2-COUNT B2)))).

This simplifies, using the :definition FIX, the :executable-counterpart
of ACL2-COUNT, the :rewrite rules COMMUTATIVITY-OF-+, DEFAULT-CDR and
UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to

Subgoal 1.1.2'
(IMPLIES (NOT (CONSP A))
         (< (ACL2-COUNT B2)
            (+ 1 (ACL2-COUNT A)
               (ACL2-COUNT B1)
               (ACL2-COUNT B2)))).

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

Subgoal 1.1.1
(IMPLIES (CONSP (CONS A1 A2))
         (< (+ (ACL2-COUNT B2) (ACL2-COUNT A2))
            (+ 1 (ACL2-COUNT (CONS A1 A2))
               (ACL2-COUNT B1)
               (ACL2-COUNT B2)))).

This simplifies, using the :definitions ACL2-COUNT and SYNTAXP, the
:executable-counterparts of BINARY-+, CAR, CONSP, EQ and IF, primitive
type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-
2-OF-+, COMMUTATIVITY-OF-+ and FOLD-CONSTS-IN-+, to

Subgoal 1.1.1'
(< (+ (ACL2-COUNT A2) (ACL2-COUNT B2))
   (+ 2 (ACL2-COUNT A1)
      (ACL2-COUNT A2)
      (ACL2-COUNT B1)
      (ACL2-COUNT B2))).

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 SERIAL-ADDER. 
Thus, we admit this function under the principle of definition. We
observe that the type of SERIAL-ADDER is described by the theorem 
(AND (CONSP (SERIAL-ADDER A B C)) (TRUE-LISTP (SERIAL-ADDER A B C))).
We used primitive type reasoning.

Summary
Form:  ( DEFUN SERIAL-ADDER ...)
Rules: ((:DEFINITION ACL2-COUNT)
        (:DEFINITION E0-ORD-<)
        (:DEFINITION E0-ORDINALP)
        (:DEFINITION ENDP)
        (:DEFINITION FIX)
        (:DEFINITION SYNTAXP)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART ACL2-COUNT)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQ)
        (:EXECUTABLE-COUNTERPART IF)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE COMMUTATIVITY-2-OF-+)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE DEFAULT-CDR)
        (:REWRITE FOLD-CONSTS-IN-+)
        (:REWRITE UNICITY-OF-0)
        (:TYPE-PRESCRIPTION ACL2-COUNT))
Warnings:  None
Time:  0.64 seconds (prove: 0.58, print: 0.02, other: 0.04)
 SERIAL-ADDER
ACL2 !>(serial-adder '(t t nil)
                     '(t nil t)
                      nil)
(NIL NIL NIL T)
ACL2 !>(serial-adder '(t t nil)
                     '(t nil t)
                     t)
(T NIL NIL T)
ACL2 !>(serial-adder '(t t nil)
                     '()
                     t)
(NIL NIL T NIL)
ACL2 !>(defconst *a*
        '(t nil nil t t t t t nil t t t nil t nil t
          nil t nil t t t t t t t t t t t nil nil
          nil nil nil t t t t t nil t t t nil t nil t
          t t nil t t t t t nil t nil t t nil nil t
          t nil nil t t t t t nil t nil t nil t t t
          nil t nil t t t t t nil t nil t nil t nil nil
          t nil nil t t t t t t t t t t t nil nil
          nil nil nil t t t t t t t t t nil t nil t
          nil nil nil nil t t t t t t nil t nil nil t t))

Summary
Form:  ( DEFCONST *A* ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 *A*
ACL2 !>(defconst *b*
        '(t t t t t t t t t t nil t nil t nil t
          t nil t t t t t t t t t t nil nil nil nil
          nil nil nil t t t t t nil t nil t t t t t
          t nil nil t t t t t t t t t t nil t nil
          t nil t nil t t t t t t t t t nil nil nil
          nil t t t t t t t nil t nil t t t t nil
          t nil t nil t t t t nil t nil t t nil nil t
          nil nil nil t t t t t nil t nil t nil t nil nil
          nil t t t t t t t t t t t nil t nil t))

Summary
Form:  ( DEFCONST *B* ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 *B*
ACL2 !>(serial-adder *a* *b* nil)
(NIL NIL
     NIL T T T T T NIL T NIL T T NIL T NIL
     NIL NIL NIL T T T T T T T T T NIL NIL
     T NIL NIL NIL NIL NIL T T T T T NIL NIL
     T NIL T NIL T T NIL T NIL T T T T NIL T
     NIL T T T T T NIL T T T NIL T T T NIL T
     NIL T NIL NIL NIL NIL T NIL NIL T T T T
     T T NIL T NIL NIL T NIL T NIL T T T NIL
     T T T NIL T NIL T T NIL T T NIL NIL NIL
     NIL T T T T NIL T NIL T T NIL T T NIL
     T T T NIL T T T T T NIL T T T T NIL T)
ACL2 !>(defun n (v)
        (cond ((endp v) 0)
              ((car v) (+ 1 (* 2 (n (cdr v)))))
              (t (* 2 (n (cdr v))))))

The admission of N is trivial, using the relation E0-ORD-< (which is
known to be well-founded on the domain recognized by E0-ORDINALP) and
the measure (ACL2-COUNT V).  We observe that the type of N is described
by the theorem (AND (INTEGERP (N V)) (<= 0 (N V))).  We used primitive
type reasoning.

Summary
Form:  ( DEFUN N ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 N
ACL2 !>(n '(t t nil))
3
ACL2 !>(n *a*)
17765695716094771496618484167493975784730361
ACL2 !>(n *b*)
15331138877664345459150421522004660157524991
ACL2 !>(+ (n *a*) (n *b*))
33096834593759116955768905689498635942255352
ACL2 !>(n (serial-adder *a* *b* nil))
33096834593759116955768905689498635942255352
ACL2 !>(defthm serial-adder-correct
  (equal (n (serial-adder x y c))
         (+ (n x) (n y) (if c 1 0))))

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

Subgoal 2
(IMPLIES C
         (EQUAL (N (SERIAL-ADDER X Y C))
                (+ (N X) (N Y) 1))).

This simplifies, using the :rewrite rules COMMUTATIVITY-2-OF-+ and
COMMUTATIVITY-OF-+, to

Subgoal 2'
(IMPLIES C
         (EQUAL (N (SERIAL-ADDER X Y C))
                (+ 1 (N X) (N Y)))).

Name the formula above *1.

Subgoal 1
(IMPLIES (NOT C)
         (EQUAL (N (SERIAL-ADDER X Y NIL))
                (+ (N X) (N Y) 0))).

This simplifies, using the :definition FIX, the :rewrite rules COMMUTATIVITY-
OF-+ and UNICITY-OF-0 and the :type-prescription rule N, to

Subgoal 1'
(EQUAL (N (SERIAL-ADDER X Y NIL))
       (+ (N X) (N Y))).

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

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

We will induct according to a scheme suggested by (N Y), but modified
to accommodate (N X) and (SERIAL-ADDER X Y C).  If we let  (:P C X Y)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP Y))
                   (NOT (CAR Y))
                   (:P (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))
                       (CDR X)
                       (CDR Y)))
              (:P C X Y))
     (IMPLIES (AND (NOT (ENDP Y))
                   (CAR Y)
                   (:P (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))
                       (CDR X)
                       (CDR Y)))
              (:P C X Y))
     (IMPLIES (ENDP Y) (:P C X Y))).
This induction is justified by the same argument used to admit N, namely,
the measure (ACL2-COUNT Y) is decreasing according to the relation
E0-ORD-< (which is known to be well-founded on the domain recognized
by E0-ORDINALP).  Note, however, that the unmeasured variables C and
X are being instantiated.  When applied to the goal at hand the above
induction scheme produces the following three nontautological subgoals.

Subgoal *1/3
(IMPLIES
     (AND (NOT (ENDP Y))
          (NOT (CAR Y))
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X))
                    (N (CDR Y))
                    (IF (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))
                        1 0))))
     (EQUAL (N (SERIAL-ADDER X Y C))
            (+ (N X) (N Y) (IF C 1 0)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/3'
(IMPLIES
     (AND (CONSP Y)
          (NOT (CAR Y))
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X))
                    (N (CDR Y))
                    (IF (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))
                        1 0))))
     (EQUAL (N (SERIAL-ADDER X Y C))
            (+ (N X) (N Y) (IF C 1 0)))).

This simplifies, using the :definitions FIX, FULL-ADDER, MAJ, MV-NTH,
N, SERIAL-ADDER and XOR, the :executable-counterparts of BINARY-+,
CONS, MV-NTH, XOR and ZP, primitive type reasoning, the :rewrite rules
CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-OF-+ and UNICITY-
OF-0 and the :type-prescription rule N, to the following nine conjectures.

Subgoal *1/3.9
(IMPLIES
     (AND (CONSP Y)
          (NOT (CAR Y))
          (NOT (CAR X))
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y)) 0))
          (CONSP X)
          C)
     (EQUAL (N (CONS T (SERIAL-ADDER (CDR X) (CDR Y) NIL)))
            (+ 1 (* 2 (N (CDR Y)))
               (* 2 (N (CDR X)))))).

This simplifies, using the :definitions FIX and N, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, LEFT-CANCELLATION-
FOR-+ and UNICITY-OF-0 and the :type-prescription rules N and SERIAL-
ADDER, to

Subgoal *1/3.9'
(IMPLIES
     (AND (CONSP Y)
          (NOT (CAR Y))
          (NOT (CAR X))
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y))))
          (CONSP X)
          C)
     (EQUAL (* 2
               (N (SERIAL-ADDER (CDR X) (CDR Y) NIL)))
            (+ (* 2 (N (CDR X)))
               (* 2 (N (CDR Y)))))).

But simplification reduces this to T, using the :definitions FULL-ADDER,
MAJ and XOR, the :executable-counterparts of CONS, MV-NTH and XOR,
primitive type reasoning and the :rewrite rule DISTRIBUTIVITY.

Subgoal *1/3.8
(IMPLIES
     (AND (CONSP Y)
          (NOT (CAR Y))
          (NOT (CAR X))
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y)) 0))
          (NOT (CONSP X))
          C)
     (EQUAL (N (CONS T (SERIAL-ADDER NIL (CDR Y) NIL)))
            (+ 1 (* 2 (N (CDR Y))) 0))).

This simplifies, using the :definitions FIX and N, the :executable-
counterparts of EQUAL and FIX, primitive type reasoning, the :rewrite
rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, LEFT-CANCELLATION-FOR-
*, LEFT-CANCELLATION-FOR-+ and UNICITY-OF-0 and the :type-prescription
rules N and SERIAL-ADDER, to

Subgoal *1/3.8'
(IMPLIES
     (AND (CONSP Y)
          (NOT (CAR Y))
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y))))
          (NOT (CONSP X))
          C)
     (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL))
            (N (CDR Y)))).

But simplification reduces this to T, using the :definitions FIX, FULL-
ADDER, MAJ and XOR, the :executable-counterparts of CONS, MV-NTH, N
and XOR, the :rewrite rules DEFAULT-CAR, DEFAULT-CDR and UNICITY-OF-
0 and the :type-prescription rule N.

Subgoal *1/3.7
(IMPLIES
   (AND (CONSP Y)
        (NOT (CAR Y))
        (NOT (CAR X))
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 0))
        (CONSP X)
        (NOT C))
   (EQUAL (N (CONS NIL (SERIAL-ADDER (CDR X) (CDR Y) NIL)))
          (+ 0 (* 2 (N (CDR Y)))
             (* 2 (N (CDR X)))))).

By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to

Subgoal *1/3.7'
(IMPLIES
   (AND (CONSP Y)
        (NOT (CAR Y))
        (NOT (CAR X))
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 0))
        (CONSP X)
        (NOT C))
   (EQUAL (N (CONS NIL (SERIAL-ADDER (CDR X) (CDR Y) NIL)))
          (FIX (+ (* 2 (N (CDR Y)))
                  (* 2 (N (CDR X))))))).

But simplification reduces this to T, using the :definitions FIX and
N, the :executable-counterparts of FULL-ADDER and MV-NTH, primitive
type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-
OF-+, DISTRIBUTIVITY and UNICITY-OF-0 and the :type-prescription rules
N and SERIAL-ADDER.

Subgoal *1/3.6
(IMPLIES
   (AND (CONSP Y)
        (NOT (CAR Y))
        (NOT (CAR X))
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 0))
        (NOT (CONSP X))
        (NOT C))
   (EQUAL (N (CONS NIL (SERIAL-ADDER NIL (CDR Y) NIL)))
          (+ 0 (* 2 (N (CDR Y))) 0))).

By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to

Subgoal *1/3.6'
(IMPLIES
   (AND (CONSP Y)
        (NOT (CAR Y))
        (NOT (CAR X))
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 0))
        (NOT (CONSP X))
        (NOT C))
   (EQUAL (N (CONS NIL (SERIAL-ADDER NIL (CDR Y) NIL)))
          (FIX (+ (* 2 (N (CDR Y))) 0)))).

This simplifies, using the :definitions FIX and N, the :executable-
counterparts of EQUAL, FIX, FULL-ADDER and MV-NTH, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, DEFAULT-
CAR, DEFAULT-CDR, LEFT-CANCELLATION-FOR-* and UNICITY-OF-0 and the
:type-prescription rules N and SERIAL-ADDER, to

Subgoal *1/3.6''
(IMPLIES (AND (CONSP Y)
              (NOT (CAR Y))
              (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL))
                     (+ (N (CDR X)) (N (CDR Y))))
              (NOT (CONSP X)))
         (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL))
                (N (CDR Y)))).

But simplification reduces this to T, using the :definition FIX, the
:executable-counterpart of N, the :rewrite rules DEFAULT-CDR and UNICITY-
OF-0 and the :type-prescription rule N.

Subgoal *1/3.5
(IMPLIES
     (AND (CONSP Y)
          (NOT (CAR Y))
          (CAR X)
          C
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y)) 1))
          (CONSP X))
     (EQUAL (N (CONS NIL (SERIAL-ADDER (CDR X) (CDR Y) C)))
            (+ 1 (* 2 (N (CDR Y)))
               1 (* 2 (N (CDR X)))))).

This simplifies, using the :definitions N and SYNTAXP, the :executable-
counterparts of BINARY-+, CAR, CONSP, EQ and IF, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-
OF-+ and FOLD-CONSTS-IN-+ and the :type-prescription rule SERIAL-ADDER,
to

Subgoal *1/3.5'
(IMPLIES
     (AND (CONSP Y)
          (NOT (CAR Y))
          (CAR X)
          C
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ 1 (N (CDR X)) (N (CDR Y))))
          (CONSP X))
     (EQUAL (* 2 (N (SERIAL-ADDER (CDR X) (CDR Y) C)))
            (+ 2 (* 2 (N (CDR X)))
               (* 2 (N (CDR Y)))))).

But simplification reduces this to T, using the :definitions FULL-ADDER,
MAJ, MV-NTH and XOR, the :executable-counterparts of BINARY-*, BINARY-
+ and ZP, primitive type reasoning and the :rewrite rules CDR-CONS
and DISTRIBUTIVITY.

Subgoal *1/3.4
(IMPLIES
     (AND (CONSP Y)
          (NOT (CAR Y))
          (CAR X)
          C
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y)) 1))
          (NOT (CONSP X)))
     (EQUAL (N (CONS T (SERIAL-ADDER NIL (CDR Y) NIL)))
            (+ 1 (* 2 (N (CDR Y))) 0))).

But simplification reduces this to T, using trivial observations.

Subgoal *1/3.3
(IMPLIES
   (AND (CONSP Y)
        (NOT (CAR Y))
        (NOT C)
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 0))
        (NOT (CONSP X)))
   (EQUAL (N (SERIAL-ADDER X Y NIL))
          (+ (* 2 (N (CDR Y))) 0))).

This simplifies, using the :definitions FIX, N and SERIAL-ADDER, the
:executable-counterparts of EQUAL, FIX, FULL-ADDER and MV-NTH, primitive
type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-
OF-+, DEFAULT-CAR, DEFAULT-CDR, LEFT-CANCELLATION-FOR-* and UNICITY-
OF-0 and the :type-prescription rules N and SERIAL-ADDER, to

Subgoal *1/3.3'
(IMPLIES (AND (CONSP Y)
              (NOT (CAR Y))
              (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL))
                     (+ (N (CDR X)) (N (CDR Y))))
              (NOT (CONSP X)))
         (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL))
                (N (CDR Y)))).

But simplification reduces this to T, using the :definition FIX, the
:executable-counterpart of N, the :rewrite rules DEFAULT-CDR and UNICITY-
OF-0 and the :type-prescription rule N.

Subgoal *1/3.2
(IMPLIES
   (AND (CONSP Y)
        (NOT (CAR Y))
        (NOT C)
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 0))
        (CONSP X)
        (CAR X))
   (EQUAL (N (SERIAL-ADDER X Y NIL))
          (+ (* 2 (N (CDR Y)))
             1 (* 2 (N (CDR X)))))).

But simplification reduces this to T, using the :definitions FIX, FULL-
ADDER, MAJ, N, SERIAL-ADDER and XOR, the :executable-counterparts of
CONS, MV-NTH and XOR, primitive type reasoning, the :rewrite rules
CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-OF-+, DISTRIBUTIVITY
and UNICITY-OF-0 and the :type-prescription rules N and SERIAL-ADDER.

Subgoal *1/3.1
(IMPLIES
   (AND (CONSP Y)
        (NOT (CAR Y))
        (NOT C)
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 0))
        (CONSP X)
        (NOT (CAR X)))
   (EQUAL (N (SERIAL-ADDER X Y NIL))
          (+ (* 2 (N (CDR Y)))
             (* 2 (N (CDR X)))))).

But simplification reduces this to T, using the :definitions FIX, N
and SERIAL-ADDER, the :executable-counterparts of FULL-ADDER and MV-
NTH, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS,
COMMUTATIVITY-OF-+, DISTRIBUTIVITY and UNICITY-OF-0 and the :type-
prescription rules N and SERIAL-ADDER.

Subgoal *1/2
(IMPLIES
     (AND (NOT (ENDP Y))
          (CAR Y)
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X))
                    (N (CDR Y))
                    (IF (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))
                        1 0))))
     (EQUAL (N (SERIAL-ADDER X Y C))
            (+ (N X) (N Y) (IF C 1 0)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/2'
(IMPLIES
     (AND (CONSP Y)
          (CAR Y)
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X))
                    (N (CDR Y))
                    (IF (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))
                        1 0))))
     (EQUAL (N (SERIAL-ADDER X Y C))
            (+ (N X) (N Y) (IF C 1 0)))).

This simplifies, using the :definitions FULL-ADDER, MAJ, MV-NTH, N,
SERIAL-ADDER, SYNTAXP and XOR, the :executable-counterparts of BINARY-
+, CAR, CONSP, EQ, IF, XOR and ZP, primitive type reasoning and the
:rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-
OF-+ and FOLD-CONSTS-IN-+, to the following nine conjectures.

Subgoal *1/2.9
(IMPLIES
     (AND (CONSP Y)
          (CAR Y)
          (CAR X)
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y)) 1))
          (CONSP X)
          C)
     (EQUAL (N (CONS T
                     (SERIAL-ADDER (CDR X) (CDR Y) (CAR Y))))
            (+ 1 1 (* 2 (N (CDR Y)))
               1 (* 2 (N (CDR X)))))).

This simplifies, using the :definitions N and SYNTAXP, the :executable-
counterparts of BINARY-+, CAR, CONSP, EQ and IF, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-
OF-+ and FOLD-CONSTS-IN-+ and the :type-prescription rule SERIAL-ADDER,
to

Subgoal *1/2.9'
(IMPLIES
     (AND (CONSP Y)
          (CAR Y)
          (CAR X)
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ 1 (N (CDR X)) (N (CDR Y))))
          (CONSP X)
          C)
     (EQUAL (+ 1
               (* 2
                  (N (SERIAL-ADDER (CDR X)
                                   (CDR Y)
                                   (CAR Y)))))
            (+ 3 (* 2 (N (CDR X)))
               (* 2 (N (CDR Y)))))).

But simplification reduces this to T, using the :definitions FULL-ADDER,
MAJ, MV-NTH, SYNTAXP and XOR, the :executable-counterparts of BINARY-
*, BINARY-+, CAR, CONSP, EQ, IF and ZP, primitive type reasoning and
the :rewrite rules CDR-CONS, DISTRIBUTIVITY and FOLD-CONSTS-IN-+.

Subgoal *1/2.8
(IMPLIES
     (AND (CONSP Y)
          (CAR Y)
          (CAR X)
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y)) 1))
          (NOT (CONSP X))
          C)
     (EQUAL (N (CONS NIL (SERIAL-ADDER NIL (CDR Y) C)))
            (+ 1 1 (* 2 (N (CDR Y))) 0))).

But simplification reduces this to T, using trivial observations.

Subgoal *1/2.7
(IMPLIES
   (AND (CONSP Y)
        (CAR Y)
        (CAR X)
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 1))
        (CONSP X)
        (NOT C))
   (EQUAL (N (CONS NIL
                   (SERIAL-ADDER (CDR X) (CDR Y) (CAR Y))))
          (+ 1 0 (* 2 (N (CDR Y)))
             1 (* 2 (N (CDR X)))))).

By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to

Subgoal *1/2.7'
(IMPLIES
   (AND (CONSP Y)
        (CAR Y)
        (CAR X)
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 1))
        (CONSP X)
        (NOT C))
   (EQUAL (N (CONS NIL
                   (SERIAL-ADDER (CDR X) (CDR Y) (CAR Y))))
          (+ 1
             (FIX (+ (* 2 (N (CDR Y)))
                     1 (* 2 (N (CDR X)))))))).

But simplification reduces this to T, using the :definitions FIX, FULL-
ADDER, MAJ, MV-NTH, N, SYNTAXP and XOR, the :executable-counterparts
of BINARY-*, BINARY-+, CAR, CONSP, EQ, IF and ZP, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-
OF-+, DISTRIBUTIVITY and FOLD-CONSTS-IN-+ and the :type-prescription
rules N and SERIAL-ADDER.

Subgoal *1/2.6
(IMPLIES
   (AND (CONSP Y)
        (CAR Y)
        (CAR X)
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 1))
        (NOT (CONSP X))
        (NOT C))
   (EQUAL (N (CONS T (SERIAL-ADDER NIL (CDR Y) NIL)))
          (+ 1 0 (* 2 (N (CDR Y))) 0))).

By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to

Subgoal *1/2.6'
(IMPLIES
   (AND (CONSP Y)
        (CAR Y)
        (CAR X)
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 1))
        (NOT (CONSP X))
        (NOT C))
   (EQUAL (N (CONS T (SERIAL-ADDER NIL (CDR Y) NIL)))
          (+ 1 (FIX (+ (* 2 (N (CDR Y))) 0))))).

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

Subgoal *1/2.5
(IMPLIES
   (AND (CONSP Y)
        (CAR Y)
        (NOT (CAR X))
        (NOT C)
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 0))
        (CONSP X))
   (EQUAL (N (SERIAL-ADDER X Y NIL))
          (+ 1 (* 2 (N (CDR Y)))
             (* 2 (N (CDR X)))))).

But simplification reduces this to T, using the :definitions FIX, FULL-
ADDER, MAJ, N, SERIAL-ADDER and XOR, the :executable-counterparts of
CONS, MV-NTH and XOR, primitive type reasoning, the :rewrite rules
CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, DISTRIBUTIVITY and UNICITY-
OF-0 and the :type-prescription rules N and SERIAL-ADDER.

Subgoal *1/2.4
(IMPLIES
   (AND (CONSP Y)
        (CAR Y)
        (NOT (CAR X))
        (NOT C)
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 0))
        (NOT (CONSP X)))
   (EQUAL (N (SERIAL-ADDER X Y NIL))
          (+ 1 (* 2 (N (CDR Y))) 0))).

This simplifies, using the :definitions FIX, FULL-ADDER, MAJ, N, SERIAL-
ADDER and XOR, the :executable-counterparts of CONS, EQUAL, FIX, MV-
NTH and XOR, primitive type reasoning, the :rewrite rules CAR-CONS,
CDR-CONS, COMMUTATIVITY-OF-+, DEFAULT-CAR, DEFAULT-CDR, LEFT-CANCELLATION-
FOR-*, LEFT-CANCELLATION-FOR-+ and UNICITY-OF-0 and the :type-prescription
rules N and SERIAL-ADDER, to

Subgoal *1/2.4'
(IMPLIES (AND (CONSP Y)
              (CAR Y)
              (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL))
                     (+ (N (CDR X)) (N (CDR Y))))
              (NOT (CONSP X)))
         (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL))
                (N (CDR Y)))).

But simplification reduces this to T, using the :definition FIX, the
:executable-counterpart of N, the :rewrite rules DEFAULT-CDR and UNICITY-
OF-0 and the :type-prescription rule N.

Subgoal *1/2.3
(IMPLIES
     (AND (CONSP Y)
          (CAR Y)
          C
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y)) 1))
          (NOT (CONSP X)))
     (EQUAL (N (CONS NIL (SERIAL-ADDER NIL (CDR Y) C)))
            (+ 2 (* 2 (N (CDR Y))) 0))).

This simplifies, using the :definitions FIX and N, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-
OF-+ and UNICITY-OF-0 and the :type-prescription rules N and SERIAL-
ADDER, to

Subgoal *1/2.3'
(IMPLIES
     (AND (CONSP Y)
          (CAR Y)
          C
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ 1 (N (CDR X)) (N (CDR Y))))
          (NOT (CONSP X)))
     (EQUAL (* 2 (N (SERIAL-ADDER NIL (CDR Y) C)))
            (+ 2 (* 2 (N (CDR Y)))))).

But simplification reduces this to T, using the :definitions FIX, FULL-
ADDER, MAJ, MV-NTH and XOR, the :executable-counterparts of BINARY-
*, BINARY-+, N, XOR and ZP, primitive type reasoning, the :rewrite
rules CDR-CONS, DEFAULT-CAR, DEFAULT-CDR, DISTRIBUTIVITY and UNICITY-
OF-0 and the :type-prescription rule N.

Subgoal *1/2.2
(IMPLIES
     (AND (CONSP Y)
          (CAR Y)
          C
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y)) 1))
          (CONSP X)
          (CAR X))
     (EQUAL (N (CONS T
                     (SERIAL-ADDER (CDR X) (CDR Y) (CAR Y))))
            (+ 2 (* 2 (N (CDR Y)))
               1 (* 2 (N (CDR X)))))).

This simplifies, using the :definitions N and SYNTAXP, the :executable-
counterparts of BINARY-+, CAR, CONSP, EQ and IF, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-
OF-+ and FOLD-CONSTS-IN-+ and the :type-prescription rule SERIAL-ADDER,
to

Subgoal *1/2.2'
(IMPLIES
     (AND (CONSP Y)
          (CAR Y)
          C
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ 1 (N (CDR X)) (N (CDR Y))))
          (CONSP X)
          (CAR X))
     (EQUAL (+ 1
               (* 2
                  (N (SERIAL-ADDER (CDR X)
                                   (CDR Y)
                                   (CAR Y)))))
            (+ 3 (* 2 (N (CDR X)))
               (* 2 (N (CDR Y)))))).

But simplification reduces this to T, using the :definitions FULL-ADDER,
MAJ, MV-NTH, SYNTAXP and XOR, the :executable-counterparts of BINARY-
*, BINARY-+, CAR, CONSP, EQ, IF and ZP, primitive type reasoning and
the :rewrite rules CDR-CONS, DISTRIBUTIVITY and FOLD-CONSTS-IN-+.

Subgoal *1/2.1
(IMPLIES
     (AND (CONSP Y)
          (CAR Y)
          C
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y)) 1))
          (CONSP X)
          (NOT (CAR X)))
     (EQUAL (N (CONS NIL (SERIAL-ADDER (CDR X) (CDR Y) C)))
            (+ 2 (* 2 (N (CDR Y)))
               (* 2 (N (CDR X)))))).

This simplifies, using the :definition N, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+ and COMMUTATIVITY-
OF-+ and the :type-prescription rule SERIAL-ADDER, to

Subgoal *1/2.1'
(IMPLIES
     (AND (CONSP Y)
          (CAR Y)
          C
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ 1 (N (CDR X)) (N (CDR Y))))
          (CONSP X)
          (NOT (CAR X)))
     (EQUAL (* 2 (N (SERIAL-ADDER (CDR X) (CDR Y) C)))
            (+ 2 (* 2 (N (CDR X)))
               (* 2 (N (CDR Y)))))).

But simplification reduces this to T, using the :definitions FULL-ADDER,
MAJ, MV-NTH and XOR, the :executable-counterparts of BINARY-*, BINARY-
+, XOR and ZP, primitive type reasoning and the :rewrite rules CDR-
CONS and DISTRIBUTIVITY.

Subgoal *1/1
(IMPLIES (ENDP Y)
         (EQUAL (N (SERIAL-ADDER X Y C))
                (+ (N X) (N Y) (IF C 1 0)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP Y))
         (EQUAL (N (SERIAL-ADDER X Y C))
                (+ (N X) (N Y) (IF C 1 0)))).

This simplifies, using the :definitions FIX, FULL-ADDER, MAJ, MV-NTH,
N, SERIAL-ADDER and XOR, the :executable-counterparts of BINARY-+,
CONS, EQUAL, N and ZP, primitive type reasoning and the :rewrite rules
CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, DEFAULT-CAR, DEFAULT-CDR and
UNICITY-OF-0, to the following five conjectures.

Subgoal *1/1.5
(IMPLIES (AND (NOT (CONSP Y)) (NOT (CONSP X)) C)
         (EQUAL (N (LIST C)) (+ 1 0))).

By the :executable-counterpart of BINARY-+ we reduce the conjecture
to

Subgoal *1/1.5'
(IMPLIES (AND (NOT (CONSP Y)) (NOT (CONSP X)) C)
         (EQUAL (N (LIST C)) 1)).

But simplification reduces this to T, using the :definition N, the
:executable-counterparts of BINARY-*, BINARY-+, EQUAL and N, primitive
type reasoning and the :rewrite rules CAR-CONS and CDR-CONS.

Subgoal *1/1.4
(IMPLIES (AND (NOT (CONSP Y))
              (CONSP X)
              C (CAR X))
         (EQUAL (N (CONS (XOR (CAR X) T)
                         (SERIAL-ADDER (CDR X) NIL C)))
                (+ 1 1 (* 2 (N (CDR X)))))).

This simplifies, using the :definitions N, SYNTAXP and XOR, the :executable-
counterparts of BINARY-+, CAR, CONSP, EQ and IF, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS and FOLD-CONSTS-IN-+ and the
:type-prescription rule SERIAL-ADDER, to

Subgoal *1/1.4'
(IMPLIES (AND (NOT (CONSP Y))
              (CONSP X)
              C (CAR X))
         (EQUAL (* 2 (N (SERIAL-ADDER (CDR X) NIL C)))
                (+ 2 (* 2 (N (CDR X)))))).

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

Subgoal *1/1.4''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (NOT (CONSP Y))
              C X1)
         (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C)))
                (+ 2 (* 2 (N X2))))).

This simplifies, using primitive type reasoning, to

Subgoal *1/1.4'''
(IMPLIES (AND (NOT (CONSP Y)) C X1)
         (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C)))
                (+ 2 (* 2 (N X2))))).

This simplifies, using trivial observations, to

Subgoal *1/1.4'4'
(IMPLIES (AND (NOT (CONSP Y)) C)
         (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C)))
                (+ 2 (* 2 (N X2))))).

We suspect that the term (NOT (CONSP Y)) is irrelevant to the truth
of this conjecture and throw it out.  We will thus try to prove

Subgoal *1/1.4'5'
(IMPLIES C
         (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C)))
                (+ 2 (* 2 (N X2))))).

Name the formula above *1.1.

Subgoal *1/1.3
(IMPLIES (AND (NOT (CONSP Y))
              (CONSP X)
              (NOT C)
              (CAR X))
         (EQUAL (N (CONS (XOR (CAR X) NIL)
                         (SERIAL-ADDER (CDR X) NIL NIL)))
                (+ 0 1 (* 2 (N (CDR X)))))).

By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to

Subgoal *1/1.3'
(IMPLIES (AND (NOT (CONSP Y))
              (CONSP X)
              (NOT C)
              (CAR X))
         (EQUAL (N (CONS (XOR (CAR X) NIL)
                         (SERIAL-ADDER (CDR X) NIL NIL)))
                (FIX (+ 1 (* 2 (N (CDR X))))))).

This simplifies, using the :definitions FIX, N and XOR, the :executable-
counterparts of EQUAL and FIX, primitive type reasoning, the :rewrite
rules CAR-CONS, CDR-CONS, LEFT-CANCELLATION-FOR-* and LEFT-CANCELLATION-
FOR-+ and the :type-prescription rules N and SERIAL-ADDER, to

Subgoal *1/1.3''
(IMPLIES (AND (NOT (CONSP Y)) (CONSP X) (CAR X))
         (EQUAL (N (SERIAL-ADDER (CDR X) NIL NIL))
                (N (CDR X)))).

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

Subgoal *1/1.3'''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (NOT (CONSP Y))
              X1)
         (EQUAL (N (SERIAL-ADDER X2 NIL NIL))
                (N X2))).

This simplifies, using primitive type reasoning, to

Subgoal *1/1.3'4'
(IMPLIES (AND (NOT (CONSP Y)) X1)
         (EQUAL (N (SERIAL-ADDER X2 NIL NIL))
                (N X2))).

This simplifies, using trivial observations, to

Subgoal *1/1.3'5'
(IMPLIES (NOT (CONSP Y))
         (EQUAL (N (SERIAL-ADDER X2 NIL NIL))
                (N X2))).

We suspect that the term (NOT (CONSP Y)) is irrelevant to the truth
of this conjecture and throw it out.  We will thus try to prove

Subgoal *1/1.3'6'
(EQUAL (N (SERIAL-ADDER X2 NIL NIL))
       (N X2)).

Name the formula above *1.2.

Subgoal *1/1.2
(IMPLIES (AND (NOT (CONSP Y))
              (CONSP X)
              C (NOT (CAR X)))
         (EQUAL (N (CONS (XOR (CAR X) T)
                         (SERIAL-ADDER (CDR X) NIL NIL)))
                (+ 1 (* 2 (N (CDR X)))))).

This simplifies, using the :definitions FIX and N, the :executable-
counterparts of EQUAL, FIX and XOR, primitive type reasoning, the :rewrite
rules CAR-CONS, CDR-CONS, LEFT-CANCELLATION-FOR-* and LEFT-CANCELLATION-
FOR-+ and the :type-prescription rules N and SERIAL-ADDER, to

Subgoal *1/1.2'
(IMPLIES (AND (NOT (CONSP Y))
              (CONSP X)
              (NOT (CAR X)))
         (EQUAL (N (SERIAL-ADDER (CDR X) NIL NIL))
                (N (CDR X)))).

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

Subgoal *1/1.2''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (NOT (CONSP Y))
              (NOT X1))
         (EQUAL (N (SERIAL-ADDER X2 NIL NIL))
                (N X2))).

This simplifies, using primitive type reasoning, to

Subgoal *1/1.2'''
(IMPLIES (NOT (CONSP Y))
         (EQUAL (N (SERIAL-ADDER X2 NIL NIL))
                (N X2))).

We suspect that the term (NOT (CONSP Y)) is irrelevant to the truth
of this conjecture and throw it out.  We will thus try to prove

Subgoal *1/1.2'4'
(EQUAL (N (SERIAL-ADDER X2 NIL NIL))
       (N X2)).

Name the formula above *1.3.

Subgoal *1/1.1
(IMPLIES (AND (NOT (CONSP Y))
              (CONSP X)
              (NOT C)
              (NOT (CAR X)))
         (EQUAL (N (CONS (XOR (CAR X) NIL)
                         (SERIAL-ADDER (CDR X) NIL NIL)))
                (+ 0 (* 2 (N (CDR X)))))).

By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to

Subgoal *1/1.1'
(IMPLIES (AND (NOT (CONSP Y))
              (CONSP X)
              (NOT C)
              (NOT (CAR X)))
         (EQUAL (N (CONS (XOR (CAR X) NIL)
                         (SERIAL-ADDER (CDR X) NIL NIL)))
                (FIX (* 2 (N (CDR X)))))).

This simplifies, using the :definitions FIX and N, the :executable-
counterparts of EQUAL, FIX and XOR, primitive type reasoning, the :rewrite
rules CAR-CONS, CDR-CONS and LEFT-CANCELLATION-FOR-* and the :type-
prescription rules N and SERIAL-ADDER, to

Subgoal *1/1.1''
(IMPLIES (AND (NOT (CONSP Y))
              (CONSP X)
              (NOT (CAR X)))
         (EQUAL (N (SERIAL-ADDER (CDR X) NIL NIL))
                (N (CDR X)))).

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

Subgoal *1/1.1'''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (NOT (CONSP Y))
              (NOT X1))
         (EQUAL (N (SERIAL-ADDER X2 NIL NIL))
                (N X2))).

This simplifies, using primitive type reasoning, to

Subgoal *1/1.1'4'
(IMPLIES (NOT (CONSP Y))
         (EQUAL (N (SERIAL-ADDER X2 NIL NIL))
                (N X2))).

We suspect that the term (NOT (CONSP Y)) is irrelevant to the truth
of this conjecture and throw it out.  We will thus try to prove

Subgoal *1/1.1'5'
(EQUAL (N (SERIAL-ADDER X2 NIL NIL))
       (N X2)).

Name the formula above *1.4.


But this formula is subsumed by *1.3, which we'll try to prove later.
We therefore regard *1.4 as proved (pending the proof of the more general
*1.3).

We next consider *1.3, which is

(EQUAL (N (SERIAL-ADDER X2 NIL NIL))
       (N X2)).

But this formula is subsumed by *1.2, which we'll try to prove later.
We therefore regard *1.3 as proved (pending the proof of the more general
*1.2).

We next consider *1.2, which is

(EQUAL (N (SERIAL-ADDER X2 NIL NIL))
       (N X2)).

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

We will induct according to a scheme suggested by (N X2).  If we let
 (:P X2) denote *1.2 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X2))
                   (NOT (CAR X2))
                   (:P (CDR X2)))
              (:P X2))
     (IMPLIES (AND (NOT (ENDP X2))
                   (CAR X2)
                   (:P (CDR X2)))
              (:P X2))
     (IMPLIES (ENDP X2) (:P X2))).
This induction is justified by the same argument used to admit N, namely,
the measure (ACL2-COUNT X2) is decreasing according to the relation
E0-ORD-< (which is known to be well-founded on the domain recognized
by E0-ORDINALP).  When applied to the goal at hand the above induction
scheme produces the following three nontautological subgoals.

Subgoal *1.2/3
(IMPLIES (AND (NOT (ENDP X2))
              (NOT (CAR X2))
              (EQUAL (N (SERIAL-ADDER (CDR X2) NIL NIL))
                     (N (CDR X2))))
         (EQUAL (N (SERIAL-ADDER X2 NIL NIL))
                (N X2))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.2/3'
(IMPLIES (AND (CONSP X2)
              (NOT (CAR X2))
              (EQUAL (N (SERIAL-ADDER (CDR X2) NIL NIL))
                     (N (CDR X2))))
         (EQUAL (N (SERIAL-ADDER X2 NIL NIL))
                (N X2))).

But simplification reduces this to T, using the :definitions N and
SERIAL-ADDER, the :executable-counterparts of CAR, CDR, FULL-ADDER
and MV-NTH, primitive type reasoning, the :rewrite rules CAR-CONS and
CDR-CONS and the :type-prescription rule SERIAL-ADDER.

Subgoal *1.2/2
(IMPLIES (AND (NOT (ENDP X2))
              (CAR X2)
              (EQUAL (N (SERIAL-ADDER (CDR X2) NIL NIL))
                     (N (CDR X2))))
         (EQUAL (N (SERIAL-ADDER X2 NIL NIL))
                (N X2))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.2/2'
(IMPLIES (AND (CONSP X2)
              (CAR X2)
              (EQUAL (N (SERIAL-ADDER (CDR X2) NIL NIL))
                     (N (CDR X2))))
         (EQUAL (N (SERIAL-ADDER X2 NIL NIL))
                (N X2))).

But simplification reduces this to T, using the :definitions FULL-ADDER,
MAJ, N, SERIAL-ADDER and XOR, the :executable-counterparts of CAR,
CDR, CONS, MV-NTH and XOR, primitive type reasoning, the :rewrite rules
CAR-CONS and CDR-CONS and the :type-prescription rule SERIAL-ADDER.

Subgoal *1.2/1
(IMPLIES (ENDP X2)
         (EQUAL (N (SERIAL-ADDER X2 NIL NIL))
                (N X2))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.2/1'
(IMPLIES (NOT (CONSP X2))
         (EQUAL (N (SERIAL-ADDER X2 NIL NIL))
                (N X2))).

But simplification reduces this to T, using the :definitions N and
SERIAL-ADDER and the :executable-counterparts of CONS, CONSP, EQUAL
and N.

That completes the proof of *1.2.

We therefore turn our attention to *1.1, which is

(IMPLIES C
         (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C)))
                (+ 2 (* 2 (N X2))))).

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

We will induct according to a scheme suggested by (N X2).  If we let
 (:P C X2) denote *1.1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X2))
                   (NOT (CAR X2))
                   (:P C (CDR X2)))
              (:P C X2))
     (IMPLIES (AND (NOT (ENDP X2))
                   (CAR X2)
                   (:P C (CDR X2)))
              (:P C X2))
     (IMPLIES (ENDP X2) (:P C X2))).
This induction is justified by the same argument used to admit N, namely,
the measure (ACL2-COUNT X2) is decreasing according to the relation
E0-ORD-< (which is known to be well-founded on the domain recognized
by E0-ORDINALP).  When applied to the goal at hand the above induction
scheme produces the following three nontautological subgoals.

Subgoal *1.1/3
(IMPLIES (AND (NOT (ENDP X2))
              (NOT (CAR X2))
              (EQUAL (* 2 (N (SERIAL-ADDER (CDR X2) NIL C)))
                     (+ 2 (* 2 (N (CDR X2)))))
              C)
         (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C)))
                (+ 2 (* 2 (N X2))))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/3'
(IMPLIES (AND (CONSP X2)
              (NOT (CAR X2))
              (EQUAL (* 2 (N (SERIAL-ADDER (CDR X2) NIL C)))
                     (+ 2 (* 2 (N (CDR X2)))))
              C)
         (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C)))
                (+ 2 (* 2 (N X2))))).

This simplifies, using the :definitions FIX, FULL-ADDER, MAJ, N, SERIAL-
ADDER, SYNTAXP and XOR, the :executable-counterparts of BINARY-*, CAR,
CDR, CONS, CONSP, EQ, EQUAL, FIX, IF, MV-NTH and XOR, primitive type
reasoning, the :rewrite rules CAR-CONS, CDR-CONS, DISTRIBUTIVITY, FOLD-
CONSTS-IN-*, LEFT-CANCELLATION-FOR-* and LEFT-CANCELLATION-FOR-+ and
the :type-prescription rules N and SERIAL-ADDER, to

Subgoal *1.1/3''
(IMPLIES (AND (CONSP X2)
              (NOT (CAR X2))
              (EQUAL (* 2 (N (SERIAL-ADDER (CDR X2) NIL C)))
                     (+ 2 (* 2 (N (CDR X2)))))
              C)
         (EQUAL (N (SERIAL-ADDER (CDR X2) NIL NIL))
                (N (CDR X2)))).

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

Subgoal *1.1/3'''
(IMPLIES (AND (CONSP (CONS X3 X4))
              (NOT X3)
              (EQUAL (* 2 (N (SERIAL-ADDER X4 NIL C)))
                     (+ 2 (* 2 (N X4))))
              C)
         (EQUAL (N (SERIAL-ADDER X4 NIL NIL))
                (N X4))).

This simplifies, using primitive type reasoning, to

Subgoal *1.1/3'4'
(IMPLIES (AND (EQUAL (* 2 (N (SERIAL-ADDER X4 NIL C)))
                     (+ 2 (* 2 (N X4))))
              C)
         (EQUAL (N (SERIAL-ADDER X4 NIL NIL))
                (N X4))).

We generalize this conjecture, replacing (N X4) by I and restricting
the type of the new variable I to be that of the term it replaces,
as established by N.  This produces

Subgoal *1.1/3'5'
(IMPLIES (AND (INTEGERP I)
              (<= 0 I)
              (EQUAL (* 2 (N (SERIAL-ADDER X4 NIL C)))
                     (+ 2 (* 2 I)))
              C)
         (EQUAL (N (SERIAL-ADDER X4 NIL NIL))
                I)).

Name the formula above *1.1.1.

Subgoal *1.1/2
(IMPLIES (AND (NOT (ENDP X2))
              (CAR X2)
              (EQUAL (* 2 (N (SERIAL-ADDER (CDR X2) NIL C)))
                     (+ 2 (* 2 (N (CDR X2)))))
              C)
         (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C)))
                (+ 2 (* 2 (N X2))))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/2'
(IMPLIES (AND (CONSP X2)
              (CAR X2)
              (EQUAL (* 2 (N (SERIAL-ADDER (CDR X2) NIL C)))
                     (+ 2 (* 2 (N (CDR X2)))))
              C)
         (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C)))
                (+ 2 (* 2 (N X2))))).

But simplification reduces this to T, using the :definitions FULL-ADDER,
MAJ, MV-NTH, N, SERIAL-ADDER, SYNTAXP and XOR, the :executable-counterparts
of BINARY-*, BINARY-+, CAR, CDR, CONSP, EQ, IF and ZP, primitive type
reasoning, the :rewrite rules CAR-CONS, CDR-CONS, DISTRIBUTIVITY, FOLD-
CONSTS-IN-* and FOLD-CONSTS-IN-+ and the :type-prescription rule SERIAL-
ADDER.

Subgoal *1.1/1
(IMPLIES (AND (ENDP X2) C)
         (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C)))
                (+ 2 (* 2 (N X2))))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/1'
(IMPLIES (AND (NOT (CONSP X2)) C)
         (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C)))
                (+ 2 (* 2 (N X2))))).

But simplification reduces this to T, using the :definitions N and
SERIAL-ADDER, the :executable-counterparts of BINARY-*, BINARY-+, CONSP,
EQUAL and N, primitive type reasoning and the :rewrite rules CAR-CONS
and CDR-CONS.

So we now return to *1.1.1, which is

(IMPLIES (AND (INTEGERP I)
              (<= 0 I)
              (EQUAL (* 2 (N (SERIAL-ADDER X4 NIL C)))
                     (+ 2 (* 2 I)))
              C)
         (EQUAL (N (SERIAL-ADDER X4 NIL NIL))
                I)).

No induction schemes are suggested by *1.1.1.  Consequently, the proof
attempt has failed.

Summary
Form:  ( DEFTHM SERIAL-ADDER-CORRECT ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION FIX)
        (:DEFINITION FULL-ADDER)
        (:DEFINITION MAJ)
        (:DEFINITION MV-NTH)
        (:DEFINITION N)
        (:DEFINITION NOT)
        (:DEFINITION SERIAL-ADDER)
        (:DEFINITION SYNTAXP)
        (:DEFINITION XOR)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART BINARY-*)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONS)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQ)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART FIX)
        (:EXECUTABLE-COUNTERPART FULL-ADDER)
        (:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART MV-NTH)
        (:EXECUTABLE-COUNTERPART N)
        (:EXECUTABLE-COUNTERPART XOR)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE COMMUTATIVITY-2-OF-+)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE DEFAULT-CAR)
        (:REWRITE DEFAULT-CDR)
        (:REWRITE DISTRIBUTIVITY)
        (:REWRITE FOLD-CONSTS-IN-*)
        (:REWRITE FOLD-CONSTS-IN-+)
        (:REWRITE LEFT-CANCELLATION-FOR-*)
        (:REWRITE LEFT-CANCELLATION-FOR-+)
        (:REWRITE UNICITY-OF-0)
        (:TYPE-PRESCRIPTION N)
        (:TYPE-PRESCRIPTION SERIAL-ADDER))
Warnings:  None
Time:  2.64 seconds (prove: 2.16, print: 0.47, other: 0.01)

******** FAILED ********  See :DOC failure  ******** FAILED ********
ACL2 !>(defthm serial-adder-special-case
  (and (equal (n (serial-adder x nil t)) (+ 1 (n x)))
       (equal (n (serial-adder x nil nil)) (n x))))

By case analysis we reduce the conjecture to the following two conjectures.

Subgoal 2
(EQUAL (N (SERIAL-ADDER X NIL T))
       (+ 1 (N X))).

Name the formula above *1.

Subgoal 1
(EQUAL (N (SERIAL-ADDER X NIL NIL))
       (N X)).

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

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

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

Subgoal *1/3
(IMPLIES (AND (NOT (ENDP X))
              (NOT (CAR X))
              (AND (EQUAL (N (SERIAL-ADDER (CDR X) NIL T))
                          (+ 1 (N (CDR X))))
                   (EQUAL (N (SERIAL-ADDER (CDR X) NIL NIL))
                          (N (CDR X)))))
         (AND (EQUAL (N (SERIAL-ADDER X NIL T))
                     (+ 1 (N X)))
              (EQUAL (N (SERIAL-ADDER X NIL NIL))
                     (N X)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/3'
(IMPLIES (AND (CONSP X)
              (NOT (CAR X))
              (EQUAL (N (SERIAL-ADDER (CDR X) NIL T))
                     (+ 1 (N (CDR X))))
              (EQUAL (N (SERIAL-ADDER (CDR X) NIL NIL))
                     (N (CDR X))))
         (AND (EQUAL (N (SERIAL-ADDER X NIL T))
                     (+ 1 (N X)))
              (EQUAL (N (SERIAL-ADDER X NIL NIL))
                     (N X)))).

But simplification reduces this to T, using the :definitions N and
SERIAL-ADDER, the :executable-counterparts of CAR, CDR, FULL-ADDER
and MV-NTH, primitive type reasoning, the :rewrite rules CAR-CONS and
CDR-CONS and the :type-prescription rule SERIAL-ADDER.

Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
              (CAR X)
              (AND (EQUAL (N (SERIAL-ADDER (CDR X) NIL T))
                          (+ 1 (N (CDR X))))
                   (EQUAL (N (SERIAL-ADDER (CDR X) NIL NIL))
                          (N (CDR X)))))
         (AND (EQUAL (N (SERIAL-ADDER X NIL T))
                     (+ 1 (N X)))
              (EQUAL (N (SERIAL-ADDER X NIL NIL))
                     (N X)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (CAR X)
              (EQUAL (N (SERIAL-ADDER (CDR X) NIL T))
                     (+ 1 (N (CDR X))))
              (EQUAL (N (SERIAL-ADDER (CDR X) NIL NIL))
                     (N (CDR X))))
         (AND (EQUAL (N (SERIAL-ADDER X NIL T))
                     (+ 1 (N X)))
              (EQUAL (N (SERIAL-ADDER X NIL NIL))
                     (N X)))).

But simplification reduces this to T, using the :definitions FULL-ADDER,
MAJ, N, SERIAL-ADDER, SYNTAXP and XOR, the :executable-counterparts
of BINARY-*, BINARY-+, CAR, CDR, CONS, CONSP, EQ, IF, MV-NTH and XOR,
primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, DISTRIBUTIVIT\
Y and FOLD-CONSTS-IN-+ and the :type-prescription rule SERIAL-ADDER.

Subgoal *1/1
(IMPLIES (ENDP X)
         (AND (EQUAL (N (SERIAL-ADDER X NIL T))
                     (+ 1 (N X)))
              (EQUAL (N (SERIAL-ADDER X NIL NIL))
                     (N X)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
         (AND (EQUAL (N (SERIAL-ADDER X NIL T))
                     (+ 1 (N X)))
              (EQUAL (N (SERIAL-ADDER X NIL NIL))
                     (N X)))).

But simplification reduces this to T, using the :definitions N and
SERIAL-ADDER and the :executable-counterparts of BINARY-+, CONS, CONSP,
EQUAL and N.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM SERIAL-ADDER-SPECIAL-CASE ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION FULL-ADDER)
        (:DEFINITION MAJ)
        (:DEFINITION N)
        (:DEFINITION NOT)
        (:DEFINITION SERIAL-ADDER)
        (:DEFINITION SYNTAXP)
        (:DEFINITION XOR)
        (:EXECUTABLE-COUNTERPART BINARY-*)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONS)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQ)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART FULL-ADDER)
        (:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART MV-NTH)
        (:EXECUTABLE-COUNTERPART N)
        (:EXECUTABLE-COUNTERPART XOR)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE DISTRIBUTIVITY)
        (:REWRITE FOLD-CONSTS-IN-+)
        (:TYPE-PRESCRIPTION SERIAL-ADDER))
Warnings:  None
Time:  0.37 seconds (prove: 0.32, print: 0.04, other: 0.01)
 SERIAL-ADDER-SPECIAL-CASE
ACL2 !>(defthm serial-adder-correct
  (equal (n (serial-adder x y c))
         (+ (n x) (n y) (if c 1 0))))

ACL2 Warning [Subsume] in ( DEFTHM SERIAL-ADDER-CORRECT ...):  The
newly proposed :REWRITE rule SERIAL-ADDER-CORRECT probably subsumes
the previously added :REWRITE rules SERIAL-ADDER-SPECIAL-CASE and SERIAL-
ADDER-SPECIAL-CASE, in the sense that SERIAL-ADDER-CORRECT will now
probably be applied whenever the old rules would have been.


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

Subgoal 2
(IMPLIES C
         (EQUAL (N (SERIAL-ADDER X Y C))
                (+ (N X) (N Y) 1))).

This simplifies, using the :rewrite rules COMMUTATIVITY-2-OF-+ and
COMMUTATIVITY-OF-+, to

Subgoal 2'
(IMPLIES C
         (EQUAL (N (SERIAL-ADDER X Y C))
                (+ 1 (N X) (N Y)))).

Name the formula above *1.

Subgoal 1
(IMPLIES (NOT C)
         (EQUAL (N (SERIAL-ADDER X Y NIL))
                (+ (N X) (N Y) 0))).

This simplifies, using the :definition FIX, the :rewrite rules COMMUTATIVITY-
OF-+ and UNICITY-OF-0 and the :type-prescription rule N, to

Subgoal 1'
(EQUAL (N (SERIAL-ADDER X Y NIL))
       (+ (N X) (N Y))).

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

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

We will induct according to a scheme suggested by (N Y), but modified
to accommodate (N X) and (SERIAL-ADDER X Y C).  If we let  (:P C X Y)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP Y))
                   (NOT (CAR Y))
                   (:P (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))
                       (CDR X)
                       (CDR Y)))
              (:P C X Y))
     (IMPLIES (AND (NOT (ENDP Y))
                   (CAR Y)
                   (:P (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))
                       (CDR X)
                       (CDR Y)))
              (:P C X Y))
     (IMPLIES (ENDP Y) (:P C X Y))).
This induction is justified by the same argument used to admit N, namely,
the measure (ACL2-COUNT Y) is decreasing according to the relation
E0-ORD-< (which is known to be well-founded on the domain recognized
by E0-ORDINALP).  Note, however, that the unmeasured variables C and
X are being instantiated.  When applied to the goal at hand the above
induction scheme produces the following three nontautological subgoals.

Subgoal *1/3
(IMPLIES
     (AND (NOT (ENDP Y))
          (NOT (CAR Y))
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X))
                    (N (CDR Y))
                    (IF (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))
                        1 0))))
     (EQUAL (N (SERIAL-ADDER X Y C))
            (+ (N X) (N Y) (IF C 1 0)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/3'
(IMPLIES
     (AND (CONSP Y)
          (NOT (CAR Y))
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X))
                    (N (CDR Y))
                    (IF (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))
                        1 0))))
     (EQUAL (N (SERIAL-ADDER X Y C))
            (+ (N X) (N Y) (IF C 1 0)))).

This simplifies, using the :definitions FIX, FULL-ADDER, MAJ, MV-NTH,
N, SERIAL-ADDER and XOR, the :executable-counterparts of BINARY-+,
CONS, MV-NTH, XOR and ZP, primitive type reasoning, the :rewrite rules
CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-OF-+ and UNICITY-
OF-0 and the :type-prescription rule N, to the following nine conjectures.

Subgoal *1/3.9
(IMPLIES
     (AND (CONSP Y)
          (NOT (CAR Y))
          (NOT (CAR X))
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y)) 0))
          (CONSP X)
          C)
     (EQUAL (N (CONS T (SERIAL-ADDER (CDR X) (CDR Y) NIL)))
            (+ 1 (* 2 (N (CDR Y)))
               (* 2 (N (CDR X)))))).

This simplifies, using the :definitions FIX and N, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, LEFT-CANCELLATION-
FOR-+ and UNICITY-OF-0 and the :type-prescription rules N and SERIAL-
ADDER, to

Subgoal *1/3.9'
(IMPLIES
     (AND (CONSP Y)
          (NOT (CAR Y))
          (NOT (CAR X))
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y))))
          (CONSP X)
          C)
     (EQUAL (* 2
               (N (SERIAL-ADDER (CDR X) (CDR Y) NIL)))
            (+ (* 2 (N (CDR X)))
               (* 2 (N (CDR Y)))))).

But simplification reduces this to T, using the :definitions FULL-ADDER,
MAJ and XOR, the :executable-counterparts of CONS, MV-NTH and XOR,
primitive type reasoning and the :rewrite rule DISTRIBUTIVITY.

Subgoal *1/3.8
(IMPLIES
     (AND (CONSP Y)
          (NOT (CAR Y))
          (NOT (CAR X))
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y)) 0))
          (NOT (CONSP X))
          C)
     (EQUAL (N (CONS T (SERIAL-ADDER NIL (CDR Y) NIL)))
            (+ 1 (* 2 (N (CDR Y))) 0))).

This simplifies, using the :definitions FIX and N, the :executable-
counterparts of EQUAL and FIX, primitive type reasoning, the :rewrite
rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, LEFT-CANCELLATION-FOR-
*, LEFT-CANCELLATION-FOR-+ and UNICITY-OF-0 and the :type-prescription
rules N and SERIAL-ADDER, to

Subgoal *1/3.8'
(IMPLIES
     (AND (CONSP Y)
          (NOT (CAR Y))
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y))))
          (NOT (CONSP X))
          C)
     (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL))
            (N (CDR Y)))).

But simplification reduces this to T, using the :definitions FIX, FULL-
ADDER, MAJ and XOR, the :executable-counterparts of CONS, MV-NTH, N
and XOR, the :rewrite rules DEFAULT-CAR, DEFAULT-CDR and UNICITY-OF-
0 and the :type-prescription rule N.

Subgoal *1/3.7
(IMPLIES
   (AND (CONSP Y)
        (NOT (CAR Y))
        (NOT (CAR X))
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 0))
        (CONSP X)
        (NOT C))
   (EQUAL (N (CONS NIL (SERIAL-ADDER (CDR X) (CDR Y) NIL)))
          (+ 0 (* 2 (N (CDR Y)))
             (* 2 (N (CDR X)))))).

By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to

Subgoal *1/3.7'
(IMPLIES
   (AND (CONSP Y)
        (NOT (CAR Y))
        (NOT (CAR X))
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 0))
        (CONSP X)
        (NOT C))
   (EQUAL (N (CONS NIL (SERIAL-ADDER (CDR X) (CDR Y) NIL)))
          (FIX (+ (* 2 (N (CDR Y)))
                  (* 2 (N (CDR X))))))).

But simplification reduces this to T, using the :definitions FIX and
N, the :executable-counterparts of FULL-ADDER and MV-NTH, primitive
type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-
OF-+, DISTRIBUTIVITY and UNICITY-OF-0 and the :type-prescription rules
N and SERIAL-ADDER.

Subgoal *1/3.6
(IMPLIES
   (AND (CONSP Y)
        (NOT (CAR Y))
        (NOT (CAR X))
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 0))
        (NOT (CONSP X))
        (NOT C))
   (EQUAL (N (CONS NIL (SERIAL-ADDER NIL (CDR Y) NIL)))
          (+ 0 (* 2 (N (CDR Y))) 0))).

By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to

Subgoal *1/3.6'
(IMPLIES
   (AND (CONSP Y)
        (NOT (CAR Y))
        (NOT (CAR X))
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 0))
        (NOT (CONSP X))
        (NOT C))
   (EQUAL (N (CONS NIL (SERIAL-ADDER NIL (CDR Y) NIL)))
          (FIX (+ (* 2 (N (CDR Y))) 0)))).

This simplifies, using the :definitions FIX and N, the :executable-
counterparts of EQUAL, FIX, FULL-ADDER and MV-NTH, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, DEFAULT-
CAR, DEFAULT-CDR, LEFT-CANCELLATION-FOR-* and UNICITY-OF-0 and the
:type-prescription rules N and SERIAL-ADDER, to

Subgoal *1/3.6''
(IMPLIES (AND (CONSP Y)
              (NOT (CAR Y))
              (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL))
                     (+ (N (CDR X)) (N (CDR Y))))
              (NOT (CONSP X)))
         (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL))
                (N (CDR Y)))).

But simplification reduces this to T, using the :definition FIX, the
:executable-counterpart of N, the :rewrite rules DEFAULT-CDR and UNICITY-
OF-0 and the :type-prescription rule N.

Subgoal *1/3.5
(IMPLIES
     (AND (CONSP Y)
          (NOT (CAR Y))
          (CAR X)
          C
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y)) 1))
          (CONSP X))
     (EQUAL (N (CONS NIL (SERIAL-ADDER (CDR X) (CDR Y) C)))
            (+ 1 (* 2 (N (CDR Y)))
               1 (* 2 (N (CDR X)))))).

This simplifies, using the :definitions N and SYNTAXP, the :executable-
counterparts of BINARY-+, CAR, CONSP, EQ and IF, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-
OF-+ and FOLD-CONSTS-IN-+ and the :type-prescription rule SERIAL-ADDER,
to

Subgoal *1/3.5'
(IMPLIES
     (AND (CONSP Y)
          (NOT (CAR Y))
          (CAR X)
          C
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ 1 (N (CDR X)) (N (CDR Y))))
          (CONSP X))
     (EQUAL (* 2 (N (SERIAL-ADDER (CDR X) (CDR Y) C)))
            (+ 2 (* 2 (N (CDR X)))
               (* 2 (N (CDR Y)))))).

But simplification reduces this to T, using the :definitions FULL-ADDER,
MAJ, MV-NTH and XOR, the :executable-counterparts of BINARY-*, BINARY-
+ and ZP, primitive type reasoning and the :rewrite rules CDR-CONS
and DISTRIBUTIVITY.

Subgoal *1/3.4
(IMPLIES
     (AND (CONSP Y)
          (NOT (CAR Y))
          (CAR X)
          C
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y)) 1))
          (NOT (CONSP X)))
     (EQUAL (N (CONS T (SERIAL-ADDER NIL (CDR Y) NIL)))
            (+ 1 (* 2 (N (CDR Y))) 0))).

But simplification reduces this to T, using trivial observations.

Subgoal *1/3.3
(IMPLIES
   (AND (CONSP Y)
        (NOT (CAR Y))
        (NOT C)
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 0))
        (NOT (CONSP X)))
   (EQUAL (N (SERIAL-ADDER X Y NIL))
          (+ (* 2 (N (CDR Y))) 0))).

This simplifies, using the :definitions FIX, N and SERIAL-ADDER, the
:executable-counterparts of EQUAL, FIX, FULL-ADDER and MV-NTH, primitive
type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-
OF-+, DEFAULT-CAR, DEFAULT-CDR, LEFT-CANCELLATION-FOR-* and UNICITY-
OF-0 and the :type-prescription rules N and SERIAL-ADDER, to

Subgoal *1/3.3'
(IMPLIES (AND (CONSP Y)
              (NOT (CAR Y))
              (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL))
                     (+ (N (CDR X)) (N (CDR Y))))
              (NOT (CONSP X)))
         (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL))
                (N (CDR Y)))).

But simplification reduces this to T, using the :definition FIX, the
:executable-counterpart of N, the :rewrite rules DEFAULT-CDR and UNICITY-
OF-0 and the :type-prescription rule N.

Subgoal *1/3.2
(IMPLIES
   (AND (CONSP Y)
        (NOT (CAR Y))
        (NOT C)
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 0))
        (CONSP X)
        (CAR X))
   (EQUAL (N (SERIAL-ADDER X Y NIL))
          (+ (* 2 (N (CDR Y)))
             1 (* 2 (N (CDR X)))))).

But simplification reduces this to T, using the :definitions FIX, FULL-
ADDER, MAJ, N, SERIAL-ADDER and XOR, the :executable-counterparts of
CONS, MV-NTH and XOR, primitive type reasoning, the :rewrite rules
CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-OF-+, DISTRIBUTIVITY
and UNICITY-OF-0 and the :type-prescription rules N and SERIAL-ADDER.

Subgoal *1/3.1
(IMPLIES
   (AND (CONSP Y)
        (NOT (CAR Y))
        (NOT C)
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 0))
        (CONSP X)
        (NOT (CAR X)))
   (EQUAL (N (SERIAL-ADDER X Y NIL))
          (+ (* 2 (N (CDR Y)))
             (* 2 (N (CDR X)))))).

But simplification reduces this to T, using the :definitions FIX, N
and SERIAL-ADDER, the :executable-counterparts of FULL-ADDER and MV-
NTH, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS,
COMMUTATIVITY-OF-+, DISTRIBUTIVITY and UNICITY-OF-0 and the :type-
prescription rules N and SERIAL-ADDER.

Subgoal *1/2
(IMPLIES
     (AND (NOT (ENDP Y))
          (CAR Y)
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X))
                    (N (CDR Y))
                    (IF (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))
                        1 0))))
     (EQUAL (N (SERIAL-ADDER X Y C))
            (+ (N X) (N Y) (IF C 1 0)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/2'
(IMPLIES
     (AND (CONSP Y)
          (CAR Y)
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X))
                    (N (CDR Y))
                    (IF (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))
                        1 0))))
     (EQUAL (N (SERIAL-ADDER X Y C))
            (+ (N X) (N Y) (IF C 1 0)))).

This simplifies, using the :definitions FULL-ADDER, MAJ, MV-NTH, N,
SERIAL-ADDER, SYNTAXP and XOR, the :executable-counterparts of BINARY-
+, CAR, CONSP, EQ, IF, XOR and ZP, primitive type reasoning and the
:rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-
OF-+ and FOLD-CONSTS-IN-+, to the following nine conjectures.

Subgoal *1/2.9
(IMPLIES
     (AND (CONSP Y)
          (CAR Y)
          (CAR X)
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y)) 1))
          (CONSP X)
          C)
     (EQUAL (N (CONS T
                     (SERIAL-ADDER (CDR X) (CDR Y) (CAR Y))))
            (+ 1 1 (* 2 (N (CDR Y)))
               1 (* 2 (N (CDR X)))))).

This simplifies, using the :definitions N and SYNTAXP, the :executable-
counterparts of BINARY-+, CAR, CONSP, EQ and IF, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-
OF-+ and FOLD-CONSTS-IN-+ and the :type-prescription rule SERIAL-ADDER,
to

Subgoal *1/2.9'
(IMPLIES
     (AND (CONSP Y)
          (CAR Y)
          (CAR X)
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ 1 (N (CDR X)) (N (CDR Y))))
          (CONSP X)
          C)
     (EQUAL (+ 1
               (* 2
                  (N (SERIAL-ADDER (CDR X)
                                   (CDR Y)
                                   (CAR Y)))))
            (+ 3 (* 2 (N (CDR X)))
               (* 2 (N (CDR Y)))))).

But simplification reduces this to T, using the :definitions FULL-ADDER,
MAJ, MV-NTH, SYNTAXP and XOR, the :executable-counterparts of BINARY-
*, BINARY-+, CAR, CONSP, EQ, IF and ZP, primitive type reasoning and
the :rewrite rules CDR-CONS, DISTRIBUTIVITY and FOLD-CONSTS-IN-+.

Subgoal *1/2.8
(IMPLIES
     (AND (CONSP Y)
          (CAR Y)
          (CAR X)
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y)) 1))
          (NOT (CONSP X))
          C)
     (EQUAL (N (CONS NIL (SERIAL-ADDER NIL (CDR Y) C)))
            (+ 1 1 (* 2 (N (CDR Y))) 0))).

But simplification reduces this to T, using trivial observations.

Subgoal *1/2.7
(IMPLIES
   (AND (CONSP Y)
        (CAR Y)
        (CAR X)
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 1))
        (CONSP X)
        (NOT C))
   (EQUAL (N (CONS NIL
                   (SERIAL-ADDER (CDR X) (CDR Y) (CAR Y))))
          (+ 1 0 (* 2 (N (CDR Y)))
             1 (* 2 (N (CDR X)))))).

By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to

Subgoal *1/2.7'
(IMPLIES
   (AND (CONSP Y)
        (CAR Y)
        (CAR X)
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 1))
        (CONSP X)
        (NOT C))
   (EQUAL (N (CONS NIL
                   (SERIAL-ADDER (CDR X) (CDR Y) (CAR Y))))
          (+ 1
             (FIX (+ (* 2 (N (CDR Y)))
                     1 (* 2 (N (CDR X)))))))).

But simplification reduces this to T, using the :definitions FIX, FULL-
ADDER, MAJ, MV-NTH, N, SYNTAXP and XOR, the :executable-counterparts
of BINARY-*, BINARY-+, CAR, CONSP, EQ, IF and ZP, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-
OF-+, DISTRIBUTIVITY and FOLD-CONSTS-IN-+ and the :type-prescription
rules N and SERIAL-ADDER.

Subgoal *1/2.6
(IMPLIES
   (AND (CONSP Y)
        (CAR Y)
        (CAR X)
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 1))
        (NOT (CONSP X))
        (NOT C))
   (EQUAL (N (CONS T (SERIAL-ADDER NIL (CDR Y) NIL)))
          (+ 1 0 (* 2 (N (CDR Y))) 0))).

By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to

Subgoal *1/2.6'
(IMPLIES
   (AND (CONSP Y)
        (CAR Y)
        (CAR X)
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 1))
        (NOT (CONSP X))
        (NOT C))
   (EQUAL (N (CONS T (SERIAL-ADDER NIL (CDR Y) NIL)))
          (+ 1 (FIX (+ (* 2 (N (CDR Y))) 0))))).

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

Subgoal *1/2.5
(IMPLIES
   (AND (CONSP Y)
        (CAR Y)
        (NOT (CAR X))
        (NOT C)
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 0))
        (CONSP X))
   (EQUAL (N (SERIAL-ADDER X Y NIL))
          (+ 1 (* 2 (N (CDR Y)))
             (* 2 (N (CDR X)))))).

But simplification reduces this to T, using the :definitions FIX, FULL-
ADDER, MAJ, N, SERIAL-ADDER and XOR, the :executable-counterparts of
CONS, MV-NTH and XOR, primitive type reasoning, the :rewrite rules
CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, DISTRIBUTIVITY and UNICITY-
OF-0 and the :type-prescription rules N and SERIAL-ADDER.

Subgoal *1/2.4
(IMPLIES
   (AND (CONSP Y)
        (CAR Y)
        (NOT (CAR X))
        (NOT C)
        (EQUAL (N (SERIAL-ADDER (CDR X)
                                (CDR Y)
                                (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL))))
               (+ (N (CDR X)) (N (CDR Y)) 0))
        (NOT (CONSP X)))
   (EQUAL (N (SERIAL-ADDER X Y NIL))
          (+ 1 (* 2 (N (CDR Y))) 0))).

This simplifies, using the :definitions FIX, FULL-ADDER, MAJ, N, SERIAL-
ADDER and XOR, the :executable-counterparts of CONS, EQUAL, FIX, MV-
NTH and XOR, primitive type reasoning, the :rewrite rules CAR-CONS,
CDR-CONS, COMMUTATIVITY-OF-+, DEFAULT-CAR, DEFAULT-CDR, LEFT-CANCELLATION-
FOR-*, LEFT-CANCELLATION-FOR-+ and UNICITY-OF-0 and the :type-prescription
rules N and SERIAL-ADDER, to

Subgoal *1/2.4'
(IMPLIES (AND (CONSP Y)
              (CAR Y)
              (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL))
                     (+ (N (CDR X)) (N (CDR Y))))
              (NOT (CONSP X)))
         (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL))
                (N (CDR Y)))).

But simplification reduces this to T, using the :definition FIX, the
:executable-counterpart of N, the :rewrite rules DEFAULT-CDR and UNICITY-
OF-0 and the :type-prescription rule N.

Subgoal *1/2.3
(IMPLIES
     (AND (CONSP Y)
          (CAR Y)
          C
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y)) 1))
          (NOT (CONSP X)))
     (EQUAL (N (CONS NIL (SERIAL-ADDER NIL (CDR Y) C)))
            (+ 2 (* 2 (N (CDR Y))) 0))).

This simplifies, using the :definitions FIX and N, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-
OF-+ and UNICITY-OF-0 and the :type-prescription rules N and SERIAL-
ADDER, to

Subgoal *1/2.3'
(IMPLIES
     (AND (CONSP Y)
          (CAR Y)
          C
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ 1 (N (CDR X)) (N (CDR Y))))
          (NOT (CONSP X)))
     (EQUAL (* 2 (N (SERIAL-ADDER NIL (CDR Y) C)))
            (+ 2 (* 2 (N (CDR Y)))))).

But simplification reduces this to T, using the :definitions FIX, FULL-
ADDER, MAJ, MV-NTH and XOR, the :executable-counterparts of BINARY-
*, BINARY-+, N, XOR and ZP, primitive type reasoning, the :rewrite
rules CDR-CONS, DEFAULT-CAR, DEFAULT-CDR, DISTRIBUTIVITY and UNICITY-
OF-0 and the :type-prescription rule N.

Subgoal *1/2.2
(IMPLIES
     (AND (CONSP Y)
          (CAR Y)
          C
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y)) 1))
          (CONSP X)
          (CAR X))
     (EQUAL (N (CONS T
                     (SERIAL-ADDER (CDR X) (CDR Y) (CAR Y))))
            (+ 2 (* 2 (N (CDR Y)))
               1 (* 2 (N (CDR X)))))).

This simplifies, using the :definitions N and SYNTAXP, the :executable-
counterparts of BINARY-+, CAR, CONSP, EQ and IF, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-
OF-+ and FOLD-CONSTS-IN-+ and the :type-prescription rule SERIAL-ADDER,
to

Subgoal *1/2.2'
(IMPLIES
     (AND (CONSP Y)
          (CAR Y)
          C
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ 1 (N (CDR X)) (N (CDR Y))))
          (CONSP X)
          (CAR X))
     (EQUAL (+ 1
               (* 2
                  (N (SERIAL-ADDER (CDR X)
                                   (CDR Y)
                                   (CAR Y)))))
            (+ 3 (* 2 (N (CDR X)))
               (* 2 (N (CDR Y)))))).

But simplification reduces this to T, using the :definitions FULL-ADDER,
MAJ, MV-NTH, SYNTAXP and XOR, the :executable-counterparts of BINARY-
*, BINARY-+, CAR, CONSP, EQ, IF and ZP, primitive type reasoning and
the :rewrite rules CDR-CONS, DISTRIBUTIVITY and FOLD-CONSTS-IN-+.

Subgoal *1/2.1
(IMPLIES
     (AND (CONSP Y)
          (CAR Y)
          C
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ (N (CDR X)) (N (CDR Y)) 1))
          (CONSP X)
          (NOT (CAR X)))
     (EQUAL (N (CONS NIL (SERIAL-ADDER (CDR X) (CDR Y) C)))
            (+ 2 (* 2 (N (CDR Y)))
               (* 2 (N (CDR X)))))).

This simplifies, using the :definition N, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+ and COMMUTATIVITY-
OF-+ and the :type-prescription rule SERIAL-ADDER, to

Subgoal *1/2.1'
(IMPLIES
     (AND (CONSP Y)
          (CAR Y)
          C
          (EQUAL (N (SERIAL-ADDER (CDR X)
                                  (CDR Y)
                                  (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C))))
                 (+ 1 (N (CDR X)) (N (CDR Y))))
          (CONSP X)
          (NOT (CAR X)))
     (EQUAL (* 2 (N (SERIAL-ADDER (CDR X) (CDR Y) C)))
            (+ 2 (* 2 (N (CDR X)))
               (* 2 (N (CDR Y)))))).

But simplification reduces this to T, using the :definitions FULL-ADDER,
MAJ, MV-NTH and XOR, the :executable-counterparts of BINARY-*, BINARY-
+, XOR and ZP, primitive type reasoning and the :rewrite rules CDR-
CONS and DISTRIBUTIVITY.

Subgoal *1/1
(IMPLIES (ENDP Y)
         (EQUAL (N (SERIAL-ADDER X Y C))
                (+ (N X) (N Y) (IF C 1 0)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP Y))
         (EQUAL (N (SERIAL-ADDER X Y C))
                (+ (N X) (N Y) (IF C 1 0)))).

This simplifies, using the :definitions FIX, FULL-ADDER, MAJ, MV-NTH,
N, SERIAL-ADDER and XOR, the :executable-counterparts of BINARY-+,
CONS, EQUAL, N and ZP, primitive type reasoning and the :rewrite rules
CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, DEFAULT-CAR, DEFAULT-CDR and
UNICITY-OF-0, to the following five conjectures.

Subgoal *1/1.5
(IMPLIES (AND (NOT (CONSP Y)) (NOT (CONSP X)) C)
         (EQUAL (N (LIST C)) (+ 1 0))).

By the :executable-counterpart of BINARY-+ we reduce the conjecture
to

Subgoal *1/1.5'
(IMPLIES (AND (NOT (CONSP Y)) (NOT (CONSP X)) C)
         (EQUAL (N (LIST C)) 1)).

But simplification reduces this to T, using the :definition N, the
:executable-counterparts of BINARY-*, BINARY-+, EQUAL and N, primitive
type reasoning and the :rewrite rules CAR-CONS and CDR-CONS.

Subgoal *1/1.4
(IMPLIES (AND (NOT (CONSP Y))
              (CONSP X)
              C (CAR X))
         (EQUAL (N (CONS (XOR (CAR X) T)
                         (SERIAL-ADDER (CDR X) NIL C)))
                (+ 1 1 (* 2 (N (CDR X)))))).

This simplifies, using the :definitions N, SYNTAXP and XOR, the :executable-
counterparts of BINARY-+, CAR, CONSP, EQ and IF, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS and FOLD-CONSTS-IN-+ and the
:type-prescription rule SERIAL-ADDER, to

Subgoal *1/1.4'
(IMPLIES (AND (NOT (CONSP Y))
              (CONSP X)
              C (CA