ACL2 >; In this session log, I have already loaded my patch to ACL2 V42 to
      ; support the dtx stuff.  In the talk, I will interactively execute
      ; each of the following commands.  Following this LD command is the
      ; result of that interaction.

(LD '((defun bit32p (x)
        (and (integerp x)
             (<= 0 x)
             (< x (expt 2 32))))

      (defun bit64p (x)
        (and (integerp x)
             (<= 0 x)
             (< x (expt 2 64))))

      (defdtx bit32p)
      (defdtx bit64p)

      (defdtx (:REC action (:OR 'READ 'WRITE 'BLOCK)))

      (defdtx (:REC line (action bit32p booleanp)))

      (defdtx (:REC lines (:OR nil (line . lines))))

      (thm
       (implies (and (type? action a)
		     (type? bit32p b))
		(type? line (list a b t))))

      (pe 'dtx0)
      (pe 'dtx9)

      (thm
       (implies (and (type? lines lst)
		     (consp lst))
		(type? bit64p (cadr (car lst)))))
                   
      (pe 'dtx10)
      (pe 'dtx19)

      (thm
       (implies (type? line x)
		(true-listp x)))

      (thm
       (implies (and (type? lines x)
		     (type? lines y))
		(type? lines (append x y))))

      (thm (implies (type? action x)
                    (not (type? line x))))

      (thm (implies (type? action x)
                    (symbolp x)))

      (defdtx (:REC (:OR nil (bit64p . *))))

      (defdtx (:REC (:OR nil (bit32p . *))))


      (thm (implies (type? (:REC (:OR (bit32p . *) nil)) x)
                    (type? (:REC (:OR nil (bit64p . *))) x)))

      (defunt add-to-each (n lst)
        ((integerp (:REC (:OR nil (integerp . *))))
         =>
	 (:REC (:OR nil (integerp . *))))
        (cond ((endp lst) nil)
              (t (cons (+ n (car lst))
                       (add-to-each n (cdr lst))))))

      (pcb :x)

      (pe 'DTX62)

      (pe 'DTX60)

      (defdtx integer-listp)

      (pcb! :x))
      :ld-pre-eval-print t)

ACL2 Version 4.2.  Level 2.  Cbd "/Users/moore/work/typer/".
Distributed books directory 
"/Users/moore/work/v4-2/acl2-sources/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 >>(DEFUN BIT32P (X)
              (AND (INTEGERP X)
                   (<= 0 X)
                   (< X (EXPT 2 32))))

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

Summary
Form:  ( DEFUN BIT32P ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 BIT32P
ACL2 >>(DEFUN BIT64P (X)
              (AND (INTEGERP X)
                   (<= 0 X)
                   (< X (EXPT 2 64))))

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

Summary
Form:  ( DEFUN BIT64P ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 BIT64P
ACL2 >>(DEFDTX BIT32P)

Summary
Form:  DEFDTX
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 DTX-DATABASE
ACL2 >>(DEFDTX BIT64P)

Summary
Form:  DEFDTX
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 DTX-DATABASE
ACL2 >>(DEFDTX (:REC ACTION (:OR 'READ 'WRITE 'BLOCK)))

Summary
Form:  DEFDTX
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 DTX-DATABASE
ACL2 >>(DEFDTX (:REC LINE (ACTION BIT32P BOOLEANP)))

Summary
Form:  DEFDTX
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 DTX-DATABASE
ACL2 >>(DEFDTX (:REC LINES (:OR NIL (LINE . LINES))))

Summary
Form:  DEFDTX
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 DTX-DATABASE
ACL2 >>(THM (IMPLIES (AND (TYPE? ACTION A) (TYPE? BIT32P B))
                     (TYPE? LINE (LIST A B T))))

By the simple :definition BIT32P and the :executable-
counterpart of EXPT we reduce the conjecture to

Goal'
(IMPLIES (AND (TYPE? (:REC ACTION (:OR 'BLOCK 'READ 'WRITE))
                     A)
              (INTEGERP B)
              (<= 0 B)
              (< B 4294967296))
         (TYPE? (:REC LINE (ACTION BIT32P BOOLEANP))
                (LIST* A B '(T)))).

But simplification reduces this to T, using the :executable-
counterparts of BOOLEANP, CAR, CDR, CONSP, EQUAL and
EXPT, linear arithmetic, primitive type reasoning, the
:rewrite rules CAR-CONS, CDR-CONS, DTX0 and DTX9 and
the :type-prescription rule ACTION.

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION BIT32P)
        (:EXECUTABLE-COUNTERPART BOOLEANP)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART EXPT)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE DTX0)
        (:REWRITE DTX9)
        (:TYPE-PRESCRIPTION ACTION))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Proof succeeded.
ACL2 >>(PE 'DTX0)
          3  (DEFDTX BIT32P)
             \
>             (DEFTHM
               DTX0
               (IMPLIES (AND (INTEGERP X)
                             (NOT (< X '0))
                             (< X (EXPT '2 '32)))
                        (BIT32P X))
               :RULE-CLASSES ((:REWRITE))
               :HINTS (("Goal" :IN-THEORY (ENABLE BIT32P))))
ACL2 >>(PE 'DTX9)
   d      6  (DEFDTX (:REC LINE #))
             \
>             (DEFTHM
                 DTX9
                 (IMPLIES
                      (AND (CONSP E)
                           (ACTION (CAR E))
                           (CONSP (CDR E))
                           (BIT32P (CAR (CDR E)))
                           (CONSP (CDR (CDR E)))
                           (BOOLEANP (CAR (CDR (CDR E))))
                           (EQUAL (CDR (CDR (CDR E))) 'NIL))
                      (LINE E))
                 :RULE-CLASSES ((:REWRITE))
                 :HINTS (("Goal" :IN-THEORY (ENABLE LINE))))
ACL2 >>(THM (IMPLIES (AND (TYPE? LINES LST) (CONSP LST))
                     (TYPE? BIT64P (CADR (CAR LST)))))

By case analysis we reduce the conjecture to

Goal'
(IMPLIES (AND (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                     LST)
              (CONSP LST))
         (BIT64P (CADAR LST))).

But simplification reduces this to T, using primitive
type reasoning, the :forward-chaining rules DTX10 and
DTX19, the :rewrite rule DTX4 and the :type-prescription
rules BIT32P, LINE and LINES.

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING DTX10)
        (:FORWARD-CHAINING DTX19)
        (:REWRITE DTX4)
        (:TYPE-PRESCRIPTION BIT32P)
        (:TYPE-PRESCRIPTION LINE)
        (:TYPE-PRESCRIPTION LINES))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Proof succeeded.
ACL2 >>(PE 'DTX10)
   d      6  (DEFDTX (:REC LINE #))
             \
>             (DEFTHM
               DTX10
               (IMPLIES
                (LINE E)
                (IF
                 (CONSP E)
                 (IF
                  (ACTION (CAR E))
                  (IF
                   (CONSP (CDR E))
                   (IF
                    (BIT32P (CAR (CDR E)))
                    (IF (CONSP (CDR (CDR E)))
                        (IF (BOOLEANP (CAR (CDR (CDR E))))
                            (EQUAL (CDR (CDR (CDR E))) 'NIL)
                            'NIL)
                        'NIL)
                    'NIL)
                   'NIL)
                  'NIL)
                 'NIL))
               :RULE-CLASSES ((:FORWARD-CHAINING))
               :HINTS (("Goal" :IN-THEORY (ENABLE LINE))))
ACL2 >>(PE 'DTX19)
          7:x(DEFDTX (:REC LINES #))
             \
>             (DEFTHM
               DTX19
               (IMPLIES
                (LINES E)
                (IF
                 (EQUAL E 'NIL)
                 'T
                 (IF
                    (CONSP E)
                    (IF (LINE (CAR E)) (LINES (CDR E)) 'NIL)
                    'NIL)))
               :RULE-CLASSES ((:FORWARD-CHAINING))
               :HINTS (("Goal" :IN-THEORY (ENABLE LINES))))
ACL2 >>(THM (IMPLIES (TYPE? LINE X) (TRUE-LISTP X)))

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

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING DTX10)
        (:TYPE-PRESCRIPTION LINE))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Proof succeeded.
ACL2 >>(THM (IMPLIES (AND (TYPE? LINES X) (TYPE? LINES Y))
                     (TYPE? LINES (APPEND X Y))))

By case analysis we reduce the conjecture to

Goal'
(IMPLIES (AND (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                     X)
              (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                     Y))
         (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                (APPEND X Y))).

Name the formula above *1.

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

We will induct according to a scheme suggested by 
(BINARY-APPEND X Y).  This suggestion was produced using
the :induction rules BINARY-APPEND and LINES.  If we
let (:P X Y) denote *1 above then the induction scheme
we'll use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X) Y))
              (:P X Y))
     (IMPLIES (ENDP X) (:P X Y))).
This induction is justified by the same argument used
to admit BINARY-APPEND.  When applied to the goal at
hand the above induction scheme produces three nontautologica\
l subgoals.

Subgoal *1/3
(IMPLIES (AND (NOT (ENDP X))
              (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                     (APPEND (CDR X) Y))
              (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                     X)
              (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                     Y))
         (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                (APPEND X Y))).

By the simple :definition ENDP we reduce the conjecture
to

Subgoal *1/3'
(IMPLIES (AND (CONSP X)
              (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                     (APPEND (CDR X) Y))
              (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                     X)
              (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                     Y))
         (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                (APPEND X Y))).

But simplification reduces this to T, using the :definitions
BINARY-APPEND and LINES, primitive type reasoning, the
:rewrite rules CAR-CONS, CDR-CONS and DTX18 and the
:type-prescription rules LINE and LINES.

Subgoal *1/2
(IMPLIES
     (AND (NOT (ENDP X))
          (NOT (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                      (CDR X)))
          (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                 X)
          (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                 Y))
     (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
            (APPEND X Y))).

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

Subgoal *1/1
(IMPLIES (AND (ENDP X)
              (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                     X)
              (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                     Y))
         (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                (APPEND X Y))).

By the simple :definition ENDP we reduce the conjecture
to

Subgoal *1/1'
(IMPLIES (AND (NOT (CONSP X))
              (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                     X)
              (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                     Y))
         (TYPE? (:REC LINES (:OR NIL (LINE . LINES)))
                (APPEND X Y))).

But simplification reduces this to T, using the :definitions
BINARY-APPEND and LINES, the :executable-counterpart
of CONSP, primitive type reasoning and the :type-prescription
rule LINES.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION LINES)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING DTX19)
        (:INDUCTION BINARY-APPEND)
        (:INDUCTION LINES)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE DTX18)
        (:TYPE-PRESCRIPTION LINE)
        (:TYPE-PRESCRIPTION LINES))
Time:  0.02 seconds (prove: 0.01, print: 0.01, other: 0.00)

Proof succeeded.
ACL2 >>(THM (IMPLIES (TYPE? ACTION X)
                     (NOT (TYPE? LINE X))))

But we reduce the conjecture to T, by primitive type
reasoning, the :forward-chaining rules DTX10 and DTX5
and the :type-prescription rules ACTION and LINE.

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING DTX10)
        (:FORWARD-CHAINING DTX5)
        (:TYPE-PRESCRIPTION ACTION)
        (:TYPE-PRESCRIPTION LINE))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Proof succeeded.
ACL2 >>(THM (IMPLIES (TYPE? ACTION X) (SYMBOLP X)))

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

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING DTX5)
        (:TYPE-PRESCRIPTION ACTION))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Proof succeeded.
ACL2 >>(DEFDTX (:REC (:OR NIL (BIT64P . *))))

Summary
Form:  DEFDTX
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 DTX-DATABASE
ACL2 >>(DEFDTX (:REC (:OR NIL (BIT32P . *))))

Summary
Form:  DEFDTX
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 DTX-DATABASE
ACL2 >>(THM (IMPLIES (TYPE? (:REC (:OR (BIT32P . *) NIL)) X)
                     (TYPE? (:REC (:OR NIL (BIT64P . *)))
                            X)))

By case analysis we reduce the conjecture to

Goal'
(IMPLIES (TYPE? (:REC (:OR NIL (BIT32P . *))) X)
         (TYPE? (:REC (:OR NIL (BIT64P . *)))
                X)).

But simplification reduces this to T, using the :rewrite
rule DTX41 and the :type-prescription rule 
|(:REC (:OR NIL (BIT32P . *)))|.

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:REWRITE DTX41)
        (:TYPE-PRESCRIPTION
             |(:REC (:OR NIL (BIT32P . *)))|))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Proof succeeded.
ACL2 >>(DEFUNT ADD-TO-EACH (N LST)
               ((INTEGERP (:REC (:OR NIL (INTEGERP . *))))
                => (:REC (:OR NIL (INTEGERP . *))))
               (COND ((ENDP LST) NIL)
                     (T (CONS (+ N (CAR LST))
                              (ADD-TO-EACH N (CDR LST))))))

Summary
Form:  DEFDTX
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Summary
Form:  DEFDTX
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

The admission of ADD-TO-EACH 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 LST).
We observe that the type of ADD-TO-EACH is described
by the theorem (TRUE-LISTP (ADD-TO-EACH N LST)).  We
used primitive type reasoning.

Summary
Form:  ( DEFUN ADD-TO-EACH ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Summary
Form:  DEFDTX
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 DTX-DATABASE
ACL2 >>(PCB :X)
         10:x(DEFUNT ADD-TO-EACH (N LST) ...)
              (DEFTHM DTX44 ...)
              (DEFTHM DTX45 ...)
              (DEFDXT INTEGERP)
 L            (DEFUN |(:REC (:OR NIL (INTEGERP . *)))| (E)
                     ...)
              (IN-THEORY (DISABLE))
              (DEFTHM DTX51 ...)
              (DEFTHM DTX52 ...)
              (DEFTHM DTX60 ...)
              (DEFTHM DTX61 ...)
              (DEFDXT (:REC #))
 L            (DEFUN ADD-TO-EACH (N LST) ...)
              (DEFTHM DTX62 ...)
ACL2 >>(PE 'DTX62)
         10:x(DEFUNT ADD-TO-EACH (N LST) ...)
             \
>             (DEFTHM
               DTX62
               (IMPLIES
                 (AND (TYPE? INTEGERP N)
                      (TYPE? (:REC (:OR NIL (INTEGERP . *)))
                             LST))
                 (TYPE? (:REC (:OR NIL (INTEGERP . *)))
                        (ADD-TO-EACH N LST)))
               :RULE-CLASSES
               ((:REWRITE)
                (:FORWARD-CHAINING
                     :TRIGGER-TERMS ((ADD-TO-EACH N LST)))))
ACL2 >>(PE 'DTX60)
         10:x(DEFUNT ADD-TO-EACH (N LST) ...)
             \
>             (DEFTHM
               DTX60
               (IMPLIES
                    (|(:REC (:OR NIL (BIT64P . *)))| X)
                    (|(:REC (:OR NIL (INTEGERP . *)))| X))
               :RULE-CLASSES ((:REWRITE))
               :HINTS
               (("Goal"
                 :IN-THEORY
                 (ENABLE |(:REC (:OR NIL (INTEGERP . *)))|
                         |(:REC (:OR NIL (BIT64P . *)))|))))
ACL2 >>(DEFDTX INTEGER-LISTP)

Summary
Form:  DEFDTX
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 DTX-DATABASE
ACL2 >>(PCB! :X)
   d     11:x(DEFDTX INTEGER-LISTP)
              (DEFTHM
               DTX63
               (IMPLIES (AND (CONSP L)
                             (INTEGERP (CAR L))
                             (INTEGER-LISTP (CDR L)))
                        (INTEGER-LISTP L))
               :RULE-CLASSES ((:REWRITE))
               :HINTS
               (("Goal" :IN-THEORY (ENABLE INTEGER-LISTP))))
              (DEFTHM
               DTX64
               (IMPLIES (INTEGER-LISTP L)
                        (IF (CONSP L)
                            (IF (INTEGERP (CAR L))
                                (INTEGER-LISTP (CDR L))
                                'NIL)
                            (EQUAL L 'NIL)))
               :RULE-CLASSES ((:FORWARD-CHAINING))
               :HINTS
               (("Goal" :IN-THEORY (ENABLE INTEGER-LISTP))))
              (DEFTHM
               DTX72
               (IMPLIES (|(:REC (:OR NIL (BIT64P . *)))| X)
                        (INTEGER-LISTP X))
               :RULE-CLASSES ((:REWRITE))
               :HINTS
               (("Goal"
                 :IN-THEORY
                 (ENABLE INTEGER-LISTP
                         |(:REC (:OR NIL (BIT64P . *)))|))))
              (DEFTHM
               DTX73
               (IMPLIES (|(:REC (:OR NIL (BIT32P . *)))| X)
                        (INTEGER-LISTP X))
               :RULE-CLASSES ((:REWRITE))
               :HINTS
               (("Goal"
                 :IN-THEORY
                 (ENABLE INTEGER-LISTP
                         |(:REC (:OR NIL (BIT32P . *)))|))))
   D          (DEFTHM
               DTX74
               (IMPLIES
                    (INTEGER-LISTP X)
                    (|(:REC (:OR NIL (INTEGERP . *)))| X))
               :RULE-CLASSES ((:REWRITE))
               :HINTS
               (("Goal"
                  :IN-THEORY
                  (ENABLE
                       INTEGER-LISTP
                       |(:REC (:OR NIL (INTEGERP . *)))|))))
   D          (DEFTHM
               DTX75
               (IMPLIES
                    (|(:REC (:OR NIL (INTEGERP . *)))| X)
                    (INTEGER-LISTP X))
               :RULE-CLASSES ((:REWRITE))
               :HINTS
               (("Goal"
                  :IN-THEORY
                  (ENABLE
                       INTEGER-LISTP
                       |(:REC (:OR NIL (INTEGERP . *)))|))))
              (DEFTHM
                DTX76
                (IFF (|(:REC (:OR NIL (INTEGERP . *)))| X)
                     (INTEGER-LISTP X))
                :RULE-CLASSES ((:REWRITE))
                :HINTS (("Goal" :IN-THEORY '(DTX74 DTX75))))
              (IN-THEORY (DISABLE DTX74 DTX75))
              (DEFTHM
                DTX77
                (IMPLIES (|(:REC (:OR NIL (BIT32P . *)))| X)
                         (INTEGER-LISTP X))
                :RULE-CLASSES ((:REWRITE))
                :HINTS (("Goal" :USE DTX61
                                :IN-THEORY '(DTX76))))
              (DEFTHM
                DTX78
                (IMPLIES (|(:REC (:OR NIL (BIT64P . *)))| X)
                         (INTEGER-LISTP X))
                :RULE-CLASSES ((:REWRITE))
                :HINTS (("Goal" :USE DTX60
                                :IN-THEORY '(DTX76))))
ACL2 >>Bye.
 :EOF
ACL2 >