ACL2 !> (defun app (x y) (if (endp x) y (cons (car x) (app (cdr x) y))))

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

Summary
Form:  ( DEFUN APP ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 APP
ACL2 !> (defun rev (x) (if (endp x) '() (app (rev (cdr x)) (list (car x)))))

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

Summary
Form:  ( DEFUN REV ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION APP))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 REV
ACL2 !> (thm (implies (true-listp x) (equal (rev (rev x)) x)))
Name the formula above *1.

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

We will induct according to a scheme suggested by (REV X).  This suggestion
was produced using the :induction rules REV and TRUE-LISTP.  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 REV.
When applied to the goal at hand the above induction scheme produces
three nontautological subgoals.

Subgoal *1/3
(IMPLIES (AND (NOT (ENDP X))
              (EQUAL (REV (REV (CDR X))) (CDR X))
              (TRUE-LISTP X))
         (EQUAL (REV (REV X)) X)).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/3'
(IMPLIES (AND (CONSP X)
              (EQUAL (REV (REV (CDR X))) (CDR X))
              (TRUE-LISTP X))
         (EQUAL (REV (REV X)) X)).

This simplifies, using the :definitions REV and TRUE-LISTP, to

Subgoal *1/3''
(IMPLIES (AND (CONSP X)
              (EQUAL (REV (REV (CDR X))) (CDR X))
              (TRUE-LISTP (CDR X)))
         (EQUAL (REV (APP (REV (CDR X)) (LIST (CAR 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), (CAR X) by X1 and (CDR X)
by X2.  This produces the following goal.

Subgoal *1/3'''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (EQUAL (REV (REV X2)) X2)
              (TRUE-LISTP X2))
         (EQUAL (REV (APP (REV X2) (LIST X1)))
                (CONS X1 X2))).

This simplifies, using primitive type reasoning, to

Subgoal *1/3'4'
(IMPLIES (AND (EQUAL (REV (REV X2)) X2)
              (TRUE-LISTP X2))
         (EQUAL (REV (APP (REV X2) (LIST X1)))
                (CONS X1 X2))).

We now use the first hypothesis by cross-fertilizing (REV (REV X2))
for X2 and throwing away the hypothesis.  This produces

Subgoal *1/3'5'
(IMPLIES (TRUE-LISTP X2)
         (EQUAL (REV (APP (REV X2) (LIST X1)))
                (CONS X1 (REV (REV X2))))).

We generalize this conjecture, replacing (REV X2) by RV.  This produces

Subgoal *1/3'6'
(IMPLIES (TRUE-LISTP X2)
         (EQUAL (REV (APP RV (LIST X1)))
                (CONS X1 (REV RV)))).

We suspect that the term (TRUE-LISTP X2) is irrelevant to the truth
of this conjecture and throw it out.  We will thus try to prove

Subgoal *1/3'7'
(EQUAL (REV (APP RV (LIST X1)))
       (CONS X1 (REV RV))).

Name the formula above *1.1.

Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
              (NOT (TRUE-LISTP (CDR X)))
              (TRUE-LISTP X))
         (EQUAL (REV (REV X)) X)).

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

Subgoal *1/1
(IMPLIES (AND (ENDP X) (TRUE-LISTP X))
         (EQUAL (REV (REV X)) X)).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (NOT (CONSP X)) (TRUE-LISTP X))
         (EQUAL (REV (REV X)) X)).

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

So we now return to *1.1, which is

(EQUAL (REV (APP RV (LIST X1)))
       (CONS X1 (REV RV))).

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

We will induct according to a scheme suggested by (REV RV).  This suggestion
was produced using the :induction rules APP and REV.  If we let (:P RV X1)
denote *1.1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP RV)) (:P (CDR RV) X1))
              (:P RV X1))
     (IMPLIES (ENDP RV) (:P RV X1))).
This induction is justified by the same argument used to admit REV.
When applied to the goal at hand the above induction scheme produces
two nontautological subgoals.

Subgoal *1.1/2
(IMPLIES (AND (NOT (ENDP RV))
              (EQUAL (REV (APP (CDR RV) (LIST X1)))
                     (CONS X1 (REV (CDR RV)))))
         (EQUAL (REV (APP RV (LIST X1)))
                (CONS X1 (REV RV)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/2'
(IMPLIES (AND (CONSP RV)
              (EQUAL (REV (APP (CDR RV) (LIST X1)))
                     (CONS X1 (REV (CDR RV)))))
         (EQUAL (REV (APP RV (LIST X1)))
                (CONS X1 (REV RV)))).

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

Subgoal *1.1/1
(IMPLIES (ENDP RV)
         (EQUAL (REV (APP RV (LIST X1)))
                (CONS X1 (REV RV)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/1'
(IMPLIES (NOT (CONSP RV))
         (EQUAL (REV (APP RV (LIST X1)))
                (CONS X1 (REV RV)))).

But simplification reduces this to T, using the :definitions APP and
REV, the :executable-counterparts of CONSP and REV, 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:  ( THM ...)
Rules: ((:DEFINITION APP)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REV)
        (:DEFINITION TRUE-LISTP)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART REV)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION APP)
        (:INDUCTION REV)
        (:INDUCTION TRUE-LISTP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Warnings:  None
Time:  0.07 seconds (prove: 0.04, print: 0.03, other: 0.00)

Proof succeeded.