(UNSET-WATERFALL-PARALLELISM)
(ASSIGN SCRIPT-MODE T)
 T
(SET-LD-PROMPT T STATE)
 T
ACL2 !>>(SET-INHIBITED-SUMMARY-TYPES '(TIME STEPS))
 (TIME STEPS)
ACL2 !>>(SET-INHIBIT-OUTPUT-LST '(PROVE PROOF-TREE EVENT))
 (PROVE PROOF-TREE EVENT)
ACL2 !>>(IN-PACKAGE "ACL2")
 "ACL2"
ACL2 !>>(INCLUDE-BOOK "std/testing/must-fail"
                      :DIR :SYSTEM)

Summary
Form:  ( INCLUDE-BOOK "std/testing/must-fail" ...)
Rules: NIL
 "[books]/std/testing/must-fail.lisp"
ACL2 !>>(DEFMACRO
         MF (FORM &KEY (EXPECTED ':SOFT))
         (CONS
          'MUST-FAIL
          (CONS
           FORM
           (CONS ':EXPECTED
                 (CONS EXPECTED
                       '(:WITH-OUTPUT-OFF
                             (PROOF-TREE PROVE EVENT
                                         SUMMARY PROOF-BUILDER HISTORY)))))))

Summary
Form:  ( DEFMACRO MF ...)
Rules: NIL
 MF
ACL2 !>>(SET-COMPILE-FNS T)
 T
ACL2 !>>(DEFUN FIB-LIMIT (N LIMIT)
               (DECLARE (TYPE (INTEGER 0 *) LIMIT)
                        (TYPE INTEGER N))
               (DECLARE (XARGS :MEASURE (NFIX LIMIT)))
               (IF (ZP LIMIT)
                   0
                   (LET ((LIMIT (1- LIMIT)))
                        (IF (OR (= N 0) (= N 1))
                            1
                            (+ (FIB-LIMIT (- N 1) LIMIT)
                               (FIB-LIMIT (- N 2) LIMIT))))))
Subgoal 2
Subgoal 1
Subgoal 1'

Summary
Form:  ( DEFUN FIB-LIMIT ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION NFIX)
        (:DEFINITION O-FINP)
        (:DEFINITION O-P)
        (:DEFINITION O<)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION FIB-LIMIT))
 FIB-LIMIT
ACL2 !>>(MEMOIZE-PARTIAL FIB)

Summary
Form:  ( DEFCHOOSE FIB-LIMIT-CHANGE ...)
Rules: NIL
FIB-LIMIT-CHANGE

Summary
Form:  ( DEFCHOOSE FIB-LIMIT-STABLE ...)
Rules: NIL
FIB-LIMIT-STABLE

Summary
Form:  ( DEFUN FIB ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION FIB-LIMIT)
        (:TYPE-PRESCRIPTION NFIX))
FIB

Summary
Form:  ( TABLE PARTIAL-FUNCTIONS-TABLE ...)
Rules: NIL
PARTIAL-FUNCTIONS-TABLE

Summary
Form:  ( PROGN (DEFCHOOSE FIB-LIMIT-CHANGE ...) ...)
Rules: NIL

Summary
Form:  ( MAKE-EVENT (ER-PROGN ...) ...)
Rules: NIL
PARTIAL-FUNCTIONS-TABLE

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
MEMOIZE-TABLE
FIB

Summary
Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
Rules: NIL
FIB

Summary
Form:  ( PROGN (MAKE-EVENT ...) ...)
Rules: NIL
 FIB
ACL2 !>>(ASSERT-EVENT (EQUAL (FIB 30) (FIB-LIMIT 30 50)))
 :PASSED
ACL2 !>>(ASSERT-EVENT (EQUAL (FIB 100) 573147844013817084101))
 :PASSED
ACL2 !>>(SET-ENFORCE-REDUNDANCY T)
 T
ACL2 !>>(ENCAPSULATE
         NIL
         (DEFCHOOSE FIB-LIMIT-CHANGE (LARGE)
                    (N LIMIT)
                    (AND (NATP LARGE)
                         (<= LIMIT LARGE)
                         (NOT (EQUAL (FIB-LIMIT N LIMIT)
                                     (FIB-LIMIT N LARGE)))))
         (DEFCHOOSE FIB-LIMIT-STABLE (LIMIT)
                    (N)
                    (AND (NATP LIMIT)
                         (EQUAL (FIB-LIMIT N LIMIT)
                                (FIB-LIMIT N (FIB-LIMIT-CHANGE N LIMIT)))))
         (DEFUN FIB (N)
                (DECLARE (TYPE INTEGER N)
                         (XARGS :GUARD T))
                (FIB-LIMIT N (NFIX (FIB-LIMIT-STABLE N))))
         (TABLE
            PARTIAL-FUNCTIONS-TABLE 'FIB-LIMIT
            '((FIB FIB-LIMIT
                   FIB-LIMIT-CHANGE FIB-LIMIT-STABLE
                   (DEFUN FIB (N)
                          (DECLARE (IGNORABLE N))
                          (DECLARE (TYPE INTEGER N))
                          (FLET ((FIB-LIMIT (N LIMIT)
                                            (DECLARE (IGNORE LIMIT))
                                            (FIB N)))
                                (DECLARE (INLINE FIB-LIMIT))
                                (LET ((LIMIT 0))
                                     (DECLARE (IGNORABLE LIMIT))
                                     (IF (OR (= N 0) (= N 1))
                                         1
                                         (+ (FIB-LIMIT (- N 1) LIMIT)
                                            (FIB-LIMIT (- N 2) LIMIT)))))))))
         (MEMOIZE 'FIB :TOTAL 'FIB-LIMIT))

The event ( DEFCHOOSE FIB-LIMIT-CHANGE ...) is redundant.  See :DOC
redundant-events.

Summary
Form:  ( DEFCHOOSE FIB-LIMIT-CHANGE ...)
Rules: NIL
:REDUNDANT

The event ( DEFCHOOSE FIB-LIMIT-STABLE ...) is redundant.  See :DOC
redundant-events.

Summary
Form:  ( DEFCHOOSE FIB-LIMIT-STABLE ...)
Rules: NIL
:REDUNDANT

The event ( DEFUN FIB ...) is redundant.  See :DOC redundant-events.

Summary
Form:  ( DEFUN FIB ...)
Rules: NIL
:REDUNDANT

The event ( TABLE PARTIAL-FUNCTIONS-TABLE ...) is redundant.  See :DOC
redundant-events.

Summary
Form:  ( TABLE PARTIAL-FUNCTIONS-TABLE ...)
Rules: NIL
:REDUNDANT

The event ( TABLE MEMOIZE-TABLE ...) is redundant.  See :DOC redundant-
events.

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
:REDUNDANT
FIB

Summary
Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
Rules: NIL
FIB

ACL2 Observation in ( ENCAPSULATE NIL (DEFCHOOSE FIB-LIMIT-CHANGE ...)
...):  The submitted encapsulate event has created no new ACL2 events,
and thus is leaving the ACL2 logical world unchanged.  See :DOC encapsulate.

Summary
Form:  ( ENCAPSULATE NIL (DEFCHOOSE FIB-LIMIT-CHANGE ...) ...)
Rules: NIL
 :EMPTY-ENCAPSULATE
ACL2 !>>(SET-ENFORCE-REDUNDANCY NIL)
 NIL
ACL2 !>>(DEFUN FIB2-CLOCK (N CLOCK)
               (DECLARE (XARGS :GUARD (NATP CLOCK))
                        (XARGS :GUARD (INTEGERP N)
                               :VERIFY-GUARDS NIL
                               :GUARD-DEBUG T))
               (DECLARE (XARGS :MEASURE (NFIX CLOCK)))
               (IF (ZP CLOCK)
                   0
                   (LET ((CLOCK (1- CLOCK)))
                        (IF (OR (= N 0) (= N 1))
                            1
                            (+ (FIB2-CLOCK (- N 1) CLOCK)
                               (FIB2-CLOCK (- N 2) CLOCK))))))
Subgoal 2
Subgoal 1
Subgoal 1'

Summary
Form:  ( DEFUN FIB2-CLOCK ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION NFIX)
        (:DEFINITION O-FINP)
        (:DEFINITION O-P)
        (:DEFINITION O<)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
 FIB2-CLOCK
ACL2 !>>(VERIFY-GUARDS FIB2-CLOCK)

Summary
Form:  ( VERIFY-GUARDS FIB2-CLOCK)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION FIB2-CLOCK))
 FIB2-CLOCK
ACL2 !>>(MEMOIZE-PARTIAL ((FIB2 FIB2-CLOCK
                                :CHANGE FIB2-CLOCK-CHANGE0
                                :STABLE FIB2-CLOCK-STABLE0
                                :CONDITION '(EQL (MOD N 4) 0)))
                         :CONDITION T)

Summary
Form:  ( DEFCHOOSE FIB2-CLOCK-CHANGE0 ...)
Rules: NIL
FIB2-CLOCK-CHANGE0

Summary
Form:  ( DEFCHOOSE FIB2-CLOCK-STABLE0 ...)
Rules: NIL
FIB2-CLOCK-STABLE0

Summary
Form:  ( DEFUN FIB2 ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:TYPE-PRESCRIPTION FIB2-CLOCK)
        (:TYPE-PRESCRIPTION NFIX))
FIB2

Summary
Form:  ( TABLE PARTIAL-FUNCTIONS-TABLE ...)
Rules: NIL
PARTIAL-FUNCTIONS-TABLE

Summary
Form:  ( PROGN (DEFCHOOSE FIB2-CLOCK-CHANGE0 ...) ...)
Rules: NIL

Summary
Form:  ( MAKE-EVENT (ER-PROGN ...) ...)
Rules: NIL
PARTIAL-FUNCTIONS-TABLE

Summary
Form:  ( DEFUN FIB2-MEMOIZE-CONDITION ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
FIB2-MEMOIZE-CONDITION

Summary
Form:  ( VERIFY-GUARDS FIB2-MEMOIZE-CONDITION)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:EXECUTABLE-COUNTERPART EQL)
        (:EXECUTABLE-COUNTERPART EQLABLEP)
        (:EXECUTABLE-COUNTERPART NOT))
FIB2-MEMOIZE-CONDITION

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
MEMOIZE-TABLE
FIB2

Summary
Form:  ( PROGN (DEFUN FIB2-MEMOIZE-CONDITION ...) ...)
Rules: NIL

Summary
Form:  ( MAKE-EVENT (LET* ...))
Rules: NIL
FIB2

Summary
Form:  ( PROGN (MAKE-EVENT ...) ...)
Rules: NIL
 FIB2
ACL2 !>>(ENCAPSULATE
          NIL (SET-ENFORCE-REDUNDANCY T)
          (DEFCHOOSE FIB2-CLOCK-CHANGE0 (LARGE)
                     (N CLOCK)
                     (AND (NATP LARGE)
                          (<= CLOCK LARGE)
                          (NOT (EQUAL (FIB2-CLOCK N CLOCK)
                                      (FIB2-CLOCK N LARGE)))))
          (DEFCHOOSE
               FIB2-CLOCK-STABLE0 (CLOCK)
               (N)
               (AND (NATP CLOCK)
                    (EQUAL (FIB2-CLOCK N CLOCK)
                           (FIB2-CLOCK N (FIB2-CLOCK-CHANGE0 N CLOCK)))))
          (DEFUN
               FIB2 (N)
               (DECLARE (XARGS :GUARD (LET ((CLOCK 0))
                                           (DECLARE (IGNORABLE CLOCK))
                                           (AND (NATP CLOCK) (INTEGERP N)))))
               (FIB2-CLOCK N (NFIX (FIB2-CLOCK-STABLE0 N)))))
T

The event ( DEFCHOOSE FIB2-CLOCK-CHANGE0 ...) is redundant.  See :DOC
redundant-events.

Summary
Form:  ( DEFCHOOSE FIB2-CLOCK-CHANGE0 ...)
Rules: NIL
:REDUNDANT

The event ( DEFCHOOSE FIB2-CLOCK-STABLE0 ...) is redundant.  See :DOC
redundant-events.

Summary
Form:  ( DEFCHOOSE FIB2-CLOCK-STABLE0 ...)
Rules: NIL
:REDUNDANT

The event ( DEFUN FIB2 ...) is redundant.  See :DOC redundant-events.

Summary
Form:  ( DEFUN FIB2 ...)
Rules: NIL
:REDUNDANT

Summary
Form:  ( ENCAPSULATE NIL (SET-ENFORCE-REDUNDANCY T) ...)
Rules: NIL
 T
ACL2 !>>(ASSERT-EVENT (EQUAL (FIB2 30) (FIB2-CLOCK 30 50)))
 :PASSED
ACL2 !>>(ASSERT-EVENT (EQUAL (FIB2 80) 37889062373143906))
 :PASSED
ACL2 !>>(DEFUN FIB-MV-LIMIT (N LIMIT)
               (DECLARE (TYPE (INTEGER 0 *) LIMIT)
                        (TYPE INTEGER N))
               (DECLARE (XARGS :MEASURE (NFIX LIMIT)
                               :VERIFY-GUARDS NIL))
               (IF (ZP LIMIT)
                   (MV 0 0)
                   (LET ((LIMIT (1- LIMIT)))
                        (IF (OR (= N 0) (= N 1))
                            (MV 1 1)
                            (MV-LET (X1 Y1)
                                    (FIB-MV-LIMIT (- N 1) LIMIT)
                                    (MV-LET (X2 Y2)
                                            (FIB-MV-LIMIT (- N 2) LIMIT)
                                            (MV (+ X1 X2) (+ Y1 Y2))))))))
Subgoal 2
Subgoal 1
Subgoal 1'

Summary
Form:  ( DEFUN FIB-MV-LIMIT ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION NFIX)
        (:DEFINITION O-FINP)
        (:DEFINITION O-P)
        (:DEFINITION O<)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
 FIB-MV-LIMIT
ACL2 !>>(DEFTHM NATP-FIB-MV-LIMIT-0
                (NATP (CAR (FIB-MV-LIMIT N LIMIT)))
                :RULE-CLASSES :TYPE-PRESCRIPTION)

ACL2 Observation in ( DEFTHM NATP-FIB-MV-LIMIT-0 ...):  Our heuristics
choose (CAR (FIB-MV-LIMIT N LIMIT)) as the :TYPED-TERM.
Subgoal 2
Subgoal 1
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1

Summary
Form:  ( DEFTHM NATP-FIB-MV-LIMIT-0 ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION FIB-MV-LIMIT)
        (:DEFINITION MV-NTH)
        (:DEFINITION NATP)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NATP)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FIB-MV-LIMIT)
        (:REWRITE CAR-CONS)
        (:TYPE-PRESCRIPTION FIB-MV-LIMIT))
 NATP-FIB-MV-LIMIT-0
ACL2 !>>(DEFTHM NATP-FIB-MV-LIMIT-1
                (NATP (MV-NTH 1 (FIB-MV-LIMIT N LIMIT)))
                :RULE-CLASSES :TYPE-PRESCRIPTION)

ACL2 Observation in ( DEFTHM NATP-FIB-MV-LIMIT-1 ...):  Our heuristics
choose (MV-NTH 1 (FIB-MV-LIMIT N LIMIT)) as the :TYPED-TERM.
Subgoal 2
Subgoal 1
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1

Summary
Form:  ( DEFTHM NATP-FIB-MV-LIMIT-1 ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION FIB-MV-LIMIT)
        (:DEFINITION MV-NTH)
        (:DEFINITION NATP)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART MV-NTH)
        (:EXECUTABLE-COUNTERPART NATP)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FIB-MV-LIMIT)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION FIB-MV-LIMIT))
 NATP-FIB-MV-LIMIT-1
ACL2 !>>(VERIFY-GUARDS FIB-MV-LIMIT)
Goal'

Summary
Form:  ( VERIFY-GUARDS FIB-MV-LIMIT)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION MV-NTH)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART ACL2-NUMBERP)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION FIB-MV-LIMIT)
        (:TYPE-PRESCRIPTION NATP-FIB-MV-LIMIT-0)
        (:TYPE-PRESCRIPTION NATP-FIB-MV-LIMIT-1))
 FIB-MV-LIMIT
ACL2 !>>(MEMOIZE-PARTIAL FIB-MV)

Summary
Form:  ( DEFCHOOSE FIB-MV-LIMIT-CHANGE ...)
Rules: NIL
FIB-MV-LIMIT-CHANGE

Summary
Form:  ( DEFCHOOSE FIB-MV-LIMIT-STABLE ...)
Rules: NIL
FIB-MV-LIMIT-STABLE

Summary
Form:  ( DEFUN FIB-MV ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION FIB-MV-LIMIT)
        (:TYPE-PRESCRIPTION NFIX))
FIB-MV

Summary
Form:  ( TABLE PARTIAL-FUNCTIONS-TABLE ...)
Rules: NIL
PARTIAL-FUNCTIONS-TABLE

Summary
Form:  ( PROGN (DEFCHOOSE FIB-MV-LIMIT-CHANGE ...) ...)
Rules: NIL

Summary
Form:  ( MAKE-EVENT (ER-PROGN ...) ...)
Rules: NIL
PARTIAL-FUNCTIONS-TABLE

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
MEMOIZE-TABLE
FIB-MV

Summary
Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
Rules: NIL
FIB-MV

Summary
Form:  ( PROGN (MAKE-EVENT ...) ...)
Rules: NIL
 FIB-MV
ACL2 !>>(ASSERT-EVENT (MV-LET (A B)
                              (FIB-MV 80)
                              (AND (EQUAL A 37889062373143906)
                                   (EQUAL B 37889062373143906))))
 :PASSED
ACL2 !>>(MUTUAL-RECURSION (DEFUN EVENLP-BDD (X BOUND)
                                 (DECLARE (XARGS :GUARD (NATP BOUND)))
                                 (IF (ZP BOUND)
                                     'OUCH
                                     (LET ((BOUND (1- BOUND)))
                                          (IF (CONSP X)
                                              (ODDLP-BDD (CDR X) BOUND)
                                              T))))
                          (DEFUN ODDLP-BDD (X BOUND)
                                 (DECLARE (XARGS :GUARD (NATP BOUND)))
                                 (IF (ZP BOUND)
                                     'OUCH
                                     (LET ((BOUND (1- BOUND)))
                                          (IF (CONSP X)
                                              (EVENLP-BDD (CDR X) BOUND)
                                              NIL)))))

Summary
Form:  ( MUTUAL-RECURSION ( DEFUN EVENLP-BDD ...) ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
 (EVENLP-BDD ODDLP-BDD)
ACL2 !>>(MEMOIZE-PARTIAL ((EVENLP EVENLP-BDD) (ODDLP ODDLP-BDD)))

Summary
Form:  ( DEFCHOOSE EVENLP-BDD-CHANGE ...)
Rules: NIL
EVENLP-BDD-CHANGE

Summary
Form:  ( DEFCHOOSE EVENLP-BDD-STABLE ...)
Rules: NIL
EVENLP-BDD-STABLE

Summary
Form:  ( DEFUN EVENLP ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:EXECUTABLE-COUNTERPART NOT)
        (:TYPE-PRESCRIPTION EVENLP-BDD)
        (:TYPE-PRESCRIPTION NFIX))
EVENLP

Summary
Form:  ( DEFCHOOSE ODDLP-BDD-CHANGE ...)
Rules: NIL
ODDLP-BDD-CHANGE

Summary
Form:  ( DEFCHOOSE ODDLP-BDD-STABLE ...)
Rules: NIL
ODDLP-BDD-STABLE

Summary
Form:  ( DEFUN ODDLP ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:EXECUTABLE-COUNTERPART NOT)
        (:TYPE-PRESCRIPTION NFIX)
        (:TYPE-PRESCRIPTION ODDLP-BDD))
ODDLP

Summary
Form:  ( TABLE PARTIAL-FUNCTIONS-TABLE ...)
Rules: NIL
PARTIAL-FUNCTIONS-TABLE

Summary
Form:  ( PROGN (DEFCHOOSE EVENLP-BDD-CHANGE ...) ...)
Rules: NIL

Summary
Form:  ( MAKE-EVENT (ER-PROGN ...) ...)
Rules: NIL
PARTIAL-FUNCTIONS-TABLE

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
MEMOIZE-TABLE
EVENLP

Summary
Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
Rules: NIL
EVENLP

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
MEMOIZE-TABLE
ODDLP

Summary
Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
Rules: NIL
ODDLP

Summary
Form:  ( PROGN (MAKE-EVENT ...) ...)
Rules: NIL
 ODDLP
ACL2 !>>(SET-ENFORCE-REDUNDANCY T)
 T
ACL2 !>>(ENCAPSULATE
         NIL
         (DEFCHOOSE EVENLP-BDD-CHANGE (LARGE)
                    (X BOUND)
                    (AND (NATP LARGE)
                         (<= BOUND LARGE)
                         (NOT (EQUAL (EVENLP-BDD X BOUND)
                                     (EVENLP-BDD X LARGE)))))
         (DEFCHOOSE EVENLP-BDD-STABLE (BOUND)
                    (X)
                    (AND (NATP BOUND)
                         (EQUAL (EVENLP-BDD X BOUND)
                                (EVENLP-BDD X (EVENLP-BDD-CHANGE X BOUND)))))
         (DEFUN EVENLP (X)
                (DECLARE (XARGS :GUARD (LET ((BOUND 0))
                                            (DECLARE (IGNORABLE BOUND))
                                            (NATP BOUND))))
                (EVENLP-BDD X (NFIX (EVENLP-BDD-STABLE X))))
         (DEFCHOOSE ODDLP-BDD-CHANGE (LARGE)
                    (X BOUND)
                    (AND (NATP LARGE)
                         (<= BOUND LARGE)
                         (NOT (EQUAL (ODDLP-BDD X BOUND)
                                     (ODDLP-BDD X LARGE)))))
         (DEFCHOOSE ODDLP-BDD-STABLE (BOUND)
                    (X)
                    (AND (NATP BOUND)
                         (EQUAL (ODDLP-BDD X BOUND)
                                (ODDLP-BDD X (ODDLP-BDD-CHANGE X BOUND)))))
         (DEFUN ODDLP (X)
                (DECLARE (XARGS :GUARD (LET ((BOUND 0))
                                            (DECLARE (IGNORABLE BOUND))
                                            (NATP BOUND))))
                (ODDLP-BDD X (NFIX (ODDLP-BDD-STABLE X))))
         (TABLE PARTIAL-FUNCTIONS-TABLE 'EVENLP-BDD
                '((EVENLP EVENLP-BDD
                          EVENLP-BDD-CHANGE EVENLP-BDD-STABLE
                          (DEFUN EVENLP (X)
                                 (DECLARE (IGNORABLE X))
                                 (FLET ((EVENLP-BDD (X BOUND)
                                                    (DECLARE (IGNORE BOUND))
                                                    (EVENLP X))
                                        (ODDLP-BDD (X BOUND)
                                                   (DECLARE (IGNORE BOUND))
                                                   (ODDLP X)))
                                       (DECLARE (INLINE EVENLP-BDD))
                                       (LET ((BOUND 0))
                                            (DECLARE (IGNORABLE BOUND))
                                            (IF (CONSP X)
                                                (ODDLP-BDD (CDR X) BOUND)
                                                T)))))
                  (ODDLP ODDLP-BDD
                         ODDLP-BDD-CHANGE ODDLP-BDD-STABLE
                         (DEFUN ODDLP (X)
                                (DECLARE (IGNORABLE X))
                                (FLET ((EVENLP-BDD (X BOUND)
                                                   (DECLARE (IGNORE BOUND))
                                                   (EVENLP X))
                                       (ODDLP-BDD (X BOUND)
                                                  (DECLARE (IGNORE BOUND))
                                                  (ODDLP X)))
                                      (DECLARE (INLINE ODDLP-BDD))
                                      (LET ((BOUND 0))
                                           (DECLARE (IGNORABLE BOUND))
                                           (IF (CONSP X)
                                               (EVENLP-BDD (CDR X) BOUND)
                                               NIL)))))))
         (MEMOIZE 'EVENLP :TOTAL 'EVENLP-BDD)
         (MEMOIZE 'ODDLP :TOTAL 'ODDLP-BDD))

The event ( DEFCHOOSE EVENLP-BDD-CHANGE ...) is redundant.  See :DOC
redundant-events.

Summary
Form:  ( DEFCHOOSE EVENLP-BDD-CHANGE ...)
Rules: NIL
:REDUNDANT

The event ( DEFCHOOSE EVENLP-BDD-STABLE ...) is redundant.  See :DOC
redundant-events.

Summary
Form:  ( DEFCHOOSE EVENLP-BDD-STABLE ...)
Rules: NIL
:REDUNDANT

The event ( DEFUN EVENLP ...) is redundant.  See :DOC redundant-events.

Summary
Form:  ( DEFUN EVENLP ...)
Rules: NIL
:REDUNDANT

The event ( DEFCHOOSE ODDLP-BDD-CHANGE ...) is redundant.  See :DOC
redundant-events.

Summary
Form:  ( DEFCHOOSE ODDLP-BDD-CHANGE ...)
Rules: NIL
:REDUNDANT

The event ( DEFCHOOSE ODDLP-BDD-STABLE ...) is redundant.  See :DOC
redundant-events.

Summary
Form:  ( DEFCHOOSE ODDLP-BDD-STABLE ...)
Rules: NIL
:REDUNDANT

The event ( DEFUN ODDLP ...) is redundant.  See :DOC redundant-events.

Summary
Form:  ( DEFUN ODDLP ...)
Rules: NIL
:REDUNDANT

The event ( TABLE PARTIAL-FUNCTIONS-TABLE ...) is redundant.  See :DOC
redundant-events.

Summary
Form:  ( TABLE PARTIAL-FUNCTIONS-TABLE ...)
Rules: NIL
:REDUNDANT

The event ( TABLE MEMOIZE-TABLE ...) is redundant.  See :DOC redundant-
events.

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
:REDUNDANT
EVENLP

Summary
Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
Rules: NIL
EVENLP

The event ( TABLE MEMOIZE-TABLE ...) is redundant.  See :DOC redundant-
events.

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
:REDUNDANT
ODDLP

Summary
Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
Rules: NIL
ODDLP

ACL2 Observation in ( ENCAPSULATE NIL (DEFCHOOSE EVENLP-BDD-CHANGE
...) ...):  The submitted encapsulate event has created no new ACL2
events, and thus is leaving the ACL2 logical world unchanged.  See
:DOC encapsulate.

Summary
Form:  ( ENCAPSULATE NIL (DEFCHOOSE EVENLP-BDD-CHANGE ...) ...)
Rules: NIL
 :EMPTY-ENCAPSULATE
ACL2 !>>(SET-ENFORCE-REDUNDANCY NIL)
 NIL
ACL2 !>>(ASSERT-EVENT (EVENLP '(1 2 3 4 5 6)))
 :PASSED
ACL2 !>>(ASSERT-EVENT (NOT (ODDLP '(1 2 3 4 5 6))))
 :PASSED
ACL2 !>>(DEFMACRO
         XX-WORSE-THAN-BUILTIN-CLOCKED-BODY (CLK)
         (DECLARE (XARGS :GUARD (ATOM CLK)))
         (CONS
          'COND
          (CONS
           (CONS (CONS 'BASIC-XX-WORSE-THAN
                       (CONS 'TERM1
                             (CONS 'TERM2 (CONS CLK 'NIL))))
                 '(T))
           (CONS
            '((PSEUDO-VARIANTP TERM1 TERM2) NIL)
            (CONS
             '((VARIABLEP TERM1) NIL)
             (CONS
                '((FQUOTEP TERM1) NIL)
                (CONS (CONS 'T
                            (CONS (CONS 'XX-WORSE-THAN-LST
                                        (CONS '(FARGS TERM1)
                                              (CONS 'TERM2 (CONS CLK 'NIL))))
                                  'NIL))
                      'NIL)))))))

Summary
Form:  ( DEFMACRO XX-WORSE-THAN-BUILTIN-CLOCKED-BODY ...)
Rules: NIL
 XX-WORSE-THAN-BUILTIN-CLOCKED-BODY
ACL2 !>>(MUTUAL-RECURSION
         (DEFUN XX-WORSE-THAN-BUILTIN-CLOCKED
                (TERM1 TERM2 CLK)
                (DECLARE (TYPE (INTEGER 0 *) CLK)
                         (XARGS :GUARD (AND (PSEUDO-TERMP TERM1)
                                            (PSEUDO-TERMP TERM2))
                                :MEASURE (NFIX CLK)
                                :WELL-FOUNDED-RELATION O<))
                (COND ((ZP CLK) NIL)
                      (T (LET ((CLK (1- CLK)))
                              (XX-WORSE-THAN-BUILTIN-CLOCKED-BODY CLK)))))
         (DEFUN
             XX-WORSE-THAN-OR-EQUAL-BUILTIN-CLOCKED
             (TERM1 TERM2 CLK)
             (DECLARE (TYPE (INTEGER 0 *) CLK)
                      (XARGS :GUARD (AND (PSEUDO-TERMP TERM1)
                                         (PSEUDO-TERMP TERM2))
                             :MEASURE (NFIX CLK)
                             :WELL-FOUNDED-RELATION O<))
             (IF (ZP CLK)
                 NIL
                 (LET ((CLK (1- CLK)))
                      (IF (PSEUDO-VARIANTP TERM1 TERM2)
                          (EQUAL TERM1 TERM2)
                          (XX-WORSE-THAN-BUILTIN-CLOCKED TERM1 TERM2 CLK)))))
         (DEFUN
          BASIC-XX-WORSE-THAN-LST1
          (ARGS1 ARGS2 CLK)
          (DECLARE (TYPE (INTEGER 0 *) CLK)
                   (XARGS :GUARD (AND (PSEUDO-TERM-LISTP ARGS1)
                                      (PSEUDO-TERM-LISTP ARGS2))
                          :MEASURE (NFIX CLK)
                          :WELL-FOUNDED-RELATION O<))
          (COND ((ZP CLK) NIL)
                (T (LET ((CLK (1- CLK)))
                        (COND ((ENDP ARGS1) NIL)
                              ((ENDP ARGS1) NIL)
                              ((OR (AND (OR (VARIABLEP (CAR ARGS1))
                                            (FQUOTEP (CAR ARGS1)))
                                        (NOT (OR (VARIABLEP (CAR ARGS2))
                                                 (FQUOTEP (CAR ARGS2)))))
                                   (XX-WORSE-THAN-BUILTIN-CLOCKED (CAR ARGS2)
                                                                  (CAR ARGS1)
                                                                  CLK))
                               T)
                              (T (BASIC-XX-WORSE-THAN-LST1 (CDR ARGS1)
                                                           (CDR ARGS2)
                                                           CLK)))))))
         (DEFUN
              BASIC-XX-WORSE-THAN-LST2
              (ARGS1 ARGS2 CLK)
              (DECLARE (TYPE (INTEGER 0 *) CLK)
                       (XARGS :GUARD (AND (PSEUDO-TERM-LISTP ARGS1)
                                          (PSEUDO-TERM-LISTP ARGS2))
                              :MEASURE (NFIX CLK)
                              :WELL-FOUNDED-RELATION O<))
              (COND ((ZP CLK) NIL)
                    (T (LET ((CLK (1- CLK)))
                            (COND ((ENDP ARGS1) NIL)
                                  ((XX-WORSE-THAN-BUILTIN-CLOCKED (CAR ARGS1)
                                                                  (CAR ARGS2)
                                                                  CLK)
                                   T)
                                  (T (BASIC-XX-WORSE-THAN-LST2 (CDR ARGS1)
                                                               (CDR ARGS2)
                                                               CLK)))))))
         (DEFUN
          BASIC-XX-WORSE-THAN (TERM1 TERM2 CLK)
          (DECLARE (TYPE (INTEGER 0 *) CLK)
                   (XARGS :GUARD (AND (PSEUDO-TERMP TERM1)
                                      (PSEUDO-TERMP TERM2))
                          :MEASURE (NFIX CLK)
                          :WELL-FOUNDED-RELATION O<))
          (COND
           ((ZP CLK) NIL)
           (T
            (LET
             ((CLK (1- CLK)))
             (COND ((VARIABLEP TERM2)
                    (COND ((EQ TERM1 TERM2) NIL)
                          (T (OCCUR TERM2 TERM1))))
                   ((FQUOTEP TERM2)
                    (COND ((VARIABLEP TERM1) T)
                          ((FQUOTEP TERM1)
                           (> (FN-COUNT-EVG (CADR TERM1))
                              (FN-COUNT-EVG (CADR TERM2))))
                          (T T)))
                   ((VARIABLEP TERM1) NIL)
                   ((FQUOTEP TERM1) NIL)
                   ((COND ((FLAMBDA-APPLICATIONP TERM1)
                           (EQUAL (FFN-SYMB TERM1)
                                  (FFN-SYMB TERM2)))
                          (T (EQ (FFN-SYMB TERM1) (FFN-SYMB TERM2))))
                    (COND ((PSEUDO-VARIANTP TERM1 TERM2) NIL)
                          (T (COND ((BASIC-XX-WORSE-THAN-LST1 (FARGS TERM1)
                                                              (FARGS TERM2)
                                                              CLK)
                                    NIL)
                                   (T (BASIC-XX-WORSE-THAN-LST2 (FARGS TERM1)
                                                                (FARGS TERM2)
                                                                CLK))))))
                   (T NIL))))))
         (DEFUN
          SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL
          (TERM1 TERM2 CLK)
          (DECLARE (TYPE (INTEGER 0 *) CLK)
                   (XARGS :GUARD (AND (PSEUDO-TERMP TERM1)
                                      (PSEUDO-TERMP TERM2))
                          :MEASURE (NFIX CLK)
                          :WELL-FOUNDED-RELATION O<))
          (COND
           ((ZP CLK) NIL)
           (T
            (LET
             ((CLK (1- CLK)))
             (COND
                 ((VARIABLEP TERM1) (EQ TERM1 TERM2))
                 ((IF (PSEUDO-VARIANTP TERM1 TERM2)
                      (EQUAL TERM1 TERM2)
                      (BASIC-XX-WORSE-THAN TERM1 TERM2 CLK))
                  T)
                 ((FQUOTEP TERM1) NIL)
                 (T (SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST (FARGS TERM1)
                                                             TERM2 CLK)))))))
         (DEFUN
          SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST
          (ARGS TERM2 CLK)
          (DECLARE (TYPE (INTEGER 0 *) CLK)
                   (XARGS :GUARD (AND (PSEUDO-TERM-LISTP ARGS)
                                      (PSEUDO-TERMP TERM2))
                          :MEASURE (NFIX CLK)
                          :WELL-FOUNDED-RELATION O<))
          (COND
           ((ZP CLK) NIL)
           (T
            (LET
             ((CLK (1- CLK)))
             (COND
              ((ENDP ARGS) NIL)
              (T
               (OR (SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL (CAR ARGS)
                                                        TERM2 CLK)
                   (SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST (CDR ARGS)
                                                            TERM2 CLK))))))))
         (DEFUN
          XX-WORSE-THAN-LST (ARGS TERM2 CLK)
          (DECLARE (TYPE (INTEGER 0 *) CLK)
                   (XARGS :GUARD (AND (PSEUDO-TERM-LISTP ARGS)
                                      (PSEUDO-TERMP TERM2))
                          :MEASURE (NFIX CLK)
                          :WELL-FOUNDED-RELATION O<))
          (COND
           ((ZP CLK) NIL)
           (T
            (LET ((CLK (1- CLK)))
                 (COND ((ENDP ARGS) NIL)
                       (T (OR (SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL (CAR ARGS)
                                                                   TERM2 CLK)
                              (XX-WORSE-THAN-LST (CDR ARGS)
                                                 TERM2 CLK)))))))))
Subgoal 2
Subgoal 1
Subgoal 1'
Subgoal 7
Subgoal 7'
Subgoal 6
Subgoal 5
Subgoal 5.7
Subgoal 5.6
Subgoal 5.5
Subgoal 5.4
Subgoal 5.3
Subgoal 5.2
Subgoal 5.1
Subgoal 4
Subgoal 4.3
Subgoal 4.2
Subgoal 4.1
Subgoal 3
Subgoal 3.2
Subgoal 3.1
Subgoal 2
Subgoal 2.4
Subgoal 2.3
Subgoal 2.2
Subgoal 2.1
Subgoal 1
Subgoal 1.20
Subgoal 1.19
Subgoal 1.18
Subgoal 1.17
Subgoal 1.16
Subgoal 1.15
Subgoal 1.14
Subgoal 1.13
Subgoal 1.12
Subgoal 1.11
Subgoal 1.10
Subgoal 1.9
Subgoal 1.8
Subgoal 1.7
Subgoal 1.6
Subgoal 1.5
Subgoal 1.4
Subgoal 1.3
Subgoal 1.2
Subgoal 1.1

Summary
Form:  ( MUTUAL-RECURSION ( DEFUN XX-WORSE-THAN-BUILTIN-CLOCKED ...)
...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION ATOM)
        (:DEFINITION ENDP)
        (:DEFINITION EQ)
        (:DEFINITION NFIX)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O-P)
        (:DEFINITION O<)
        (:DEFINITION PSEUDO-TERM-LISTP)
        (:DEFINITION PSEUDO-TERMP)
        (:DEFINITION TRUE-LISTP)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NATP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART PSEUDO-TERM-LISTP)
        (:EXECUTABLE-COUNTERPART PSEUDO-TERMP)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:EXECUTABLE-COUNTERPART UNSIGNED-BYTE-P)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING PSEUDO-TERM-LISTP-FORWARD-TO-TRUE-LISTP)
        (:TYPE-PRESCRIPTION FN-COUNT-EVG-REC-TYPE-PRESCRIPTION)
        (:TYPE-PRESCRIPTION OCCUR)
        (:TYPE-PRESCRIPTION PSEUDO-TERM-LISTP)
        (:TYPE-PRESCRIPTION PSEUDO-TERMP))
 (XX-WORSE-THAN-BUILTIN-CLOCKED XX-WORSE-THAN-OR-EQUAL-BUILTIN-CLOCKED
                                BASIC-XX-WORSE-THAN-LST1
                                BASIC-XX-WORSE-THAN-LST2
                                BASIC-XX-WORSE-THAN
                                SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL
                                SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST
                                XX-WORSE-THAN-LST)
ACL2 !>>(MEMOIZE-PARTIAL
            ((XX-WORSE-THAN* XX-WORSE-THAN-BUILTIN-CLOCKED
                             :CONDITION NIL)
             (XX-WORSE-THAN-OR-EQUAL* XX-WORSE-THAN-OR-EQUAL-BUILTIN-CLOCKED)
             (BASIC-XX-WORSE-THAN-LST1* BASIC-XX-WORSE-THAN-LST1)
             (BASIC-XX-WORSE-THAN-LST2* BASIC-XX-WORSE-THAN-LST2)
             (BASIC-XX-WORSE-THAN* BASIC-XX-WORSE-THAN)
             (SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL*
                  SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL)
             (SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST*
                  SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST)
             (XX-WORSE-THAN-LST* XX-WORSE-THAN-LST)))

Summary
Form:  ( DEFCHOOSE XX-WORSE-THAN-BUILTIN-CLOCKED-CHANGE ...)
Rules: NIL
XX-WORSE-THAN-BUILTIN-CLOCKED-CHANGE

Summary
Form:  ( DEFCHOOSE XX-WORSE-THAN-BUILTIN-CLOCKED-STABLE ...)
Rules: NIL
XX-WORSE-THAN-BUILTIN-CLOCKED-STABLE

Summary
Form:  ( DEFUN XX-WORSE-THAN* ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION NFIX)
        (:TYPE-PRESCRIPTION XX-WORSE-THAN-BUILTIN-CLOCKED))
XX-WORSE-THAN*

Summary
Form:  ( DEFCHOOSE XX-WORSE-THAN-OR-EQUAL-BUILTIN-CLOCKED-CHANGE ...)
Rules: NIL
XX-WORSE-THAN-OR-EQUAL-BUILTIN-CLOCKED-CHANGE

Summary
Form:  ( DEFCHOOSE XX-WORSE-THAN-OR-EQUAL-BUILTIN-CLOCKED-STABLE ...)
Rules: NIL
XX-WORSE-THAN-OR-EQUAL-BUILTIN-CLOCKED-STABLE

Summary
Form:  ( DEFUN XX-WORSE-THAN-OR-EQUAL* ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION NFIX)
        (:TYPE-PRESCRIPTION XX-WORSE-THAN-OR-EQUAL-BUILTIN-CLOCKED))
XX-WORSE-THAN-OR-EQUAL*

Summary
Form:  ( DEFCHOOSE BASIC-XX-WORSE-THAN-LST1-CHANGE ...)
Rules: NIL
BASIC-XX-WORSE-THAN-LST1-CHANGE

Summary
Form:  ( DEFCHOOSE BASIC-XX-WORSE-THAN-LST1-STABLE ...)
Rules: NIL
BASIC-XX-WORSE-THAN-LST1-STABLE

Summary
Form:  ( DEFUN BASIC-XX-WORSE-THAN-LST1* ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION BASIC-XX-WORSE-THAN-LST1)
        (:TYPE-PRESCRIPTION NFIX))
BASIC-XX-WORSE-THAN-LST1*

Summary
Form:  ( DEFCHOOSE BASIC-XX-WORSE-THAN-LST2-CHANGE ...)
Rules: NIL
BASIC-XX-WORSE-THAN-LST2-CHANGE

Summary
Form:  ( DEFCHOOSE BASIC-XX-WORSE-THAN-LST2-STABLE ...)
Rules: NIL
BASIC-XX-WORSE-THAN-LST2-STABLE

Summary
Form:  ( DEFUN BASIC-XX-WORSE-THAN-LST2* ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION BASIC-XX-WORSE-THAN-LST2)
        (:TYPE-PRESCRIPTION NFIX))
BASIC-XX-WORSE-THAN-LST2*

Summary
Form:  ( DEFCHOOSE BASIC-XX-WORSE-THAN-CHANGE ...)
Rules: NIL
BASIC-XX-WORSE-THAN-CHANGE

Summary
Form:  ( DEFCHOOSE BASIC-XX-WORSE-THAN-STABLE ...)
Rules: NIL
BASIC-XX-WORSE-THAN-STABLE

Summary
Form:  ( DEFUN BASIC-XX-WORSE-THAN* ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION BASIC-XX-WORSE-THAN)
        (:TYPE-PRESCRIPTION NFIX))
BASIC-XX-WORSE-THAN*

Summary
Form:  ( DEFCHOOSE SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-CHANGE ...)
Rules: NIL
SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-CHANGE

Summary
Form:  ( DEFCHOOSE SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-STABLE ...)
Rules: NIL
SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-STABLE

Summary
Form:  ( DEFUN SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL* ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION NFIX)
        (:TYPE-PRESCRIPTION SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL))
SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL*

Summary
Form:  ( DEFCHOOSE SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST-CHANGE ...)
Rules: NIL
SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST-CHANGE

Summary
Form:  ( DEFCHOOSE SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST-STABLE ...)
Rules: NIL
SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST-STABLE

Summary
Form:  ( DEFUN SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST* ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION NFIX)
        (:TYPE-PRESCRIPTION SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST))
SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST*

Summary
Form:  ( DEFCHOOSE XX-WORSE-THAN-LST-CHANGE ...)
Rules: NIL
XX-WORSE-THAN-LST-CHANGE

Summary
Form:  ( DEFCHOOSE XX-WORSE-THAN-LST-STABLE ...)
Rules: NIL
XX-WORSE-THAN-LST-STABLE

Summary
Form:  ( DEFUN XX-WORSE-THAN-LST* ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION NFIX)
        (:TYPE-PRESCRIPTION XX-WORSE-THAN-LST))
XX-WORSE-THAN-LST*

Summary
Form:  ( TABLE PARTIAL-FUNCTIONS-TABLE ...)
Rules: NIL
PARTIAL-FUNCTIONS-TABLE

Summary
Form:  ( PROGN (DEFCHOOSE XX-WORSE-THAN-BUILTIN-CLOCKED-CHANGE ...)
...)
Rules: NIL

Summary
Form:  ( MAKE-EVENT (ER-PROGN ...) ...)
Rules: NIL
PARTIAL-FUNCTIONS-TABLE

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
MEMOIZE-TABLE
XX-WORSE-THAN*

Summary
Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
Rules: NIL
XX-WORSE-THAN*

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
MEMOIZE-TABLE
XX-WORSE-THAN-OR-EQUAL*

Summary
Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
Rules: NIL
XX-WORSE-THAN-OR-EQUAL*

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
MEMOIZE-TABLE
BASIC-XX-WORSE-THAN-LST1*

Summary
Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
Rules: NIL
BASIC-XX-WORSE-THAN-LST1*

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
MEMOIZE-TABLE
BASIC-XX-WORSE-THAN-LST2*

Summary
Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
Rules: NIL
BASIC-XX-WORSE-THAN-LST2*

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
MEMOIZE-TABLE
BASIC-XX-WORSE-THAN*

Summary
Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
Rules: NIL
BASIC-XX-WORSE-THAN*

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
MEMOIZE-TABLE
SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL*

Summary
Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
Rules: NIL
SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL*

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
MEMOIZE-TABLE
SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST*

Summary
Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
Rules: NIL
SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST*

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
MEMOIZE-TABLE
XX-WORSE-THAN-LST*

Summary
Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
Rules: NIL
XX-WORSE-THAN-LST*

Summary
Form:  ( PROGN (MAKE-EVENT ...) ...)
Rules: NIL
 XX-WORSE-THAN-LST*
ACL2 !>>(ASSERT-EVENT (EQUAL (XX-WORSE-THAN* '(MEM (CAR (DEL A X)) X)
                                             '(MEM (CAR (DEL A X)) Y))
                             NIL))
 :PASSED
ACL2 !>>(ASSERT-EVENT (EQUAL (XX-WORSE-THAN-OR-EQUAL* '(MEM (CAR Z) X)
                                                      '(PERM Z Y))
                             NIL))
 :PASSED
ACL2 !>>(ASSERT-EVENT
             (EQUAL (XX-WORSE-THAN-OR-EQUAL* '(PERM (DEL (CAR Z) X) (CDR Z))
                                             '(PERM Z X))
                    T))
 :PASSED
ACL2 !>>(U)
 V        23:x(MUTUAL-RECURSION
                   (DEFUN XX-WORSE-THAN-BUILTIN-CLOCKED
                          (TERM1 TERM2 CLK)
                          ...)
                   (DEFUN XX-WORSE-THAN-OR-EQUAL-BUILTIN-CLOCKED
                          (TERM1 TERM2 CLK)
                          ...)
                   (DEFUN BASIC-XX-WORSE-THAN-LST1
                          (ARGS1 ARGS2 CLK)
                          ...)
                   (DEFUN BASIC-XX-WORSE-THAN-LST2
                          (ARGS1 ARGS2 CLK)
                          ...)
                   (DEFUN BASIC-XX-WORSE-THAN (TERM1 TERM2 CLK)
                          ...)
                   (DEFUN SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL
                          (TERM1 TERM2 CLK)
                          ...)
                   (DEFUN SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST
                          (ARGS TERM2 CLK)
                          ...)
                   (DEFUN XX-WORSE-THAN-LST (ARGS TERM2 CLK)
                          ...))
ACL2 !>>(WITH-OUTPUT
         :OFF
         :ALL
         (MEMOIZE-PARTIAL
            ((XX-WORSE-THAN* XX-WORSE-THAN-BUILTIN-CLOCKED
                             :RECURSIVE NIL)
             (XX-WORSE-THAN-OR-EQUAL* XX-WORSE-THAN-OR-EQUAL-BUILTIN-CLOCKED)
             (BASIC-XX-WORSE-THAN-LST1* BASIC-XX-WORSE-THAN-LST1)
             (BASIC-XX-WORSE-THAN-LST2* BASIC-XX-WORSE-THAN-LST2)
             (BASIC-XX-WORSE-THAN* BASIC-XX-WORSE-THAN)
             (SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL*
                  SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL)
             (SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST*
                  SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST)
             (XX-WORSE-THAN-LST* XX-WORSE-THAN-LST))))
 XX-WORSE-THAN-LST*
ACL2 !>>(MF (ASSERT-EVENT (EQUAL (XX-WORSE-THAN* '(MEM (CAR (DEL A X)) X)
                                                 '(MEM (CAR (DEL A X)) Y))
                                 NIL)))


ACL2 Error in ASSERT-EVENT:  ACL2 cannot ev the call of non-executable
function XX-WORSE-THAN-BUILTIN-CLOCKED-STABLE on argument list:

((MEM (CAR (DEL A X)) X) (MEM (CAR (DEL A X)) Y))

To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.


Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(U)
 V        23:x(MUTUAL-RECURSION
                   (DEFUN XX-WORSE-THAN-BUILTIN-CLOCKED
                          (TERM1 TERM2 CLK)
                          ...)
                   (DEFUN XX-WORSE-THAN-OR-EQUAL-BUILTIN-CLOCKED
                          (TERM1 TERM2 CLK)
                          ...)
                   (DEFUN BASIC-XX-WORSE-THAN-LST1
                          (ARGS1 ARGS2 CLK)
                          ...)
                   (DEFUN BASIC-XX-WORSE-THAN-LST2
                          (ARGS1 ARGS2 CLK)
                          ...)
                   (DEFUN BASIC-XX-WORSE-THAN (TERM1 TERM2 CLK)
                          ...)
                   (DEFUN SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL
                          (TERM1 TERM2 CLK)
                          ...)
                   (DEFUN SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST
                          (ARGS TERM2 CLK)
                          ...)
                   (DEFUN XX-WORSE-THAN-LST (ARGS TERM2 CLK)
                          ...))
ACL2 !>>(WITH-OUTPUT
         :OFF
         :ALL
         (MEMOIZE-PARTIAL
            ((XX-WORSE-THAN* XX-WORSE-THAN-BUILTIN-CLOCKED)
             (XX-WORSE-THAN-OR-EQUAL* XX-WORSE-THAN-OR-EQUAL-BUILTIN-CLOCKED)
             (BASIC-XX-WORSE-THAN-LST1* BASIC-XX-WORSE-THAN-LST1)
             (BASIC-XX-WORSE-THAN-LST2* BASIC-XX-WORSE-THAN-LST2)
             (BASIC-XX-WORSE-THAN* BASIC-XX-WORSE-THAN)
             (SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL*
                  SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL)
             (SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST*
                  SOME-SUBTERM-XX-WORSE-THAN-OR-EQUAL-LST)
             (XX-WORSE-THAN-LST* XX-WORSE-THAN-LST))
            :CONDITION NIL))
 XX-WORSE-THAN-LST*
ACL2 !>>(ASSERT-EVENT (EQUAL (XX-WORSE-THAN* '(MEM (CAR (DEL A X)) X)
                                             '(MEM (CAR (DEL A X)) Y))
                             NIL))
 :PASSED
ACL2 !>>(ASSERT-EVENT (EQUAL (XX-WORSE-THAN-OR-EQUAL* '(MEM (CAR Z) X)
                                                      '(PERM Z Y))
                             NIL))
 :PASSED
ACL2 !>>(ASSERT-EVENT
             (EQUAL (XX-WORSE-THAN-OR-EQUAL* '(PERM (DEL (CAR Z) X) (CDR Z))
                                             '(PERM Z X))
                    T))
 :PASSED
ACL2 !>>(DEFUN BAD{WRONG-FORM}-LIMIT (N LIMIT)
               (DECLARE (TYPE (INTEGER 0 *) LIMIT)
                        (TYPE (INTEGER 0 *) N)
                        (XARGS :VERIFY-GUARDS NIL))
               (IF (ZP LIMIT)
                   0
                   (LET ((LIMIT (1+ LIMIT)))
                        (IF (OR (ZP N) (= N 1))
                            1
                            (+ (BAD{WRONG-FORM}-LIMIT (- N 1) LIMIT)
                               (BAD{WRONG-FORM}-LIMIT (- N 2)
                                                      LIMIT))))))
Subgoal 2
Subgoal 2.2
Subgoal 2.1
Subgoal 1
Subgoal 1'

Summary
Form:  ( DEFUN BAD{WRONG-FORM}-LIMIT ...)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION ACL2-COUNT)
        (:DEFINITION INTEGER-ABS)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O<)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:EXECUTABLE-COUNTERPART UNARY--)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE DISTRIBUTIVITY-OF-MINUS-OVER-+))
 BAD{WRONG-FORM}-LIMIT
ACL2 !>>(MF (MEMOIZE-PARTIAL BAD{WRONG-FORM}))


ACL2 Error in MEMOIZE-PARTIAL:  The function BAD{WRONG-FORM}-LIMIT
is not guard-verified.  See :DOC memoize-partial.


Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(VERIFY-GUARDS BAD{WRONG-FORM}-LIMIT)
Goal'
Goal''

Summary
Form:  ( VERIFY-GUARDS BAD{WRONG-FORM}-LIMIT)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART INTEGERP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION BAD{WRONG-FORM}-LIMIT))
 BAD{WRONG-FORM}-LIMIT
ACL2 !>>(MF (MEMOIZE-PARTIAL BAD{WRONG-FORM}))


ACL2 Error in MEMOIZE-PARTIAL:  
The (untranslated) body of function BAD{WRONG-FORM}-LIMIT is not of
the appropriate form.
See :DOC memoize-partial.



Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(DEFUN BAD{USES-LIMIT}-LIMIT (N LIMIT)
               (DECLARE (TYPE (INTEGER 0 *) LIMIT)
                        (TYPE INTEGER N))
               (DECLARE (XARGS :MEASURE (NFIX LIMIT)))
               (IF (ZP LIMIT)
                   0
                   (LET ((LIMIT (1- LIMIT)))
                        (IF (OR (= N 0) (= N 1))
                            1
                            (+ (BAD{USES-LIMIT}-LIMIT (+ LIMIT (- N 1))
                                                      LIMIT)
                               (BAD{USES-LIMIT}-LIMIT (- N 2)
                                                      LIMIT))))))
Subgoal 2
Subgoal 1
Subgoal 1'

Summary
Form:  ( DEFUN BAD{USES-LIMIT}-LIMIT ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION NFIX)
        (:DEFINITION O-FINP)
        (:DEFINITION O-P)
        (:DEFINITION O<)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION BAD{USES-LIMIT}-LIMIT))
 BAD{USES-LIMIT}-LIMIT
ACL2 !>>(MF (MEMOIZE-PARTIAL BAD{USES-LIMIT}))


ACL2 Error in ( TABLE PARTIAL-FUNCTIONS-TABLE ...):  Illegal partial-
functions-table key and value (see :DOC memoize-partial):
key = BAD{USES-LIMIT}-LIMIT
value  = ((BAD{USES-LIMIT} BAD{USES-LIMIT}-LIMIT
                           BAD{USES-LIMIT}-LIMIT-CHANGE
                           BAD{USES-LIMIT}-LIMIT-STABLE
                           (DEFUN BAD{USES-LIMIT} (N)
                                  (DECLARE (IGNORABLE N))
                                  (DECLARE (TYPE INTEGER N))
                                  (FLET (#) (DECLARE #) (LET # # #)))))
Reason:
The limit variable LIMIT fails to occur free exactly where expected
in the body of the definition of function BAD{USES-LIMIT}-LIMIT (essentially,
as the last argument of each recursive call).

(See :DOC set-iprint to be able to see elided values in this message.)


ACL2 Error [Failure] in ( TABLE PARTIAL-FUNCTIONS-TABLE ...):  See
:DOC failure.

Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(DEFN BAD{ONE-FORMAL}-LIMIT (LIMIT)
              (DECLARE (XARGS :GUARD (NATP LIMIT)))
              (IF (ZP LIMIT)
                  LIMIT
                  (LET ((LIMIT (1- LIMIT)))
                       (BAD{ONE-FORMAL}-LIMIT LIMIT))))

Summary
Form:  ( DEFUN BAD{ONE-FORMAL}-LIMIT ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
 BAD{ONE-FORMAL}-LIMIT
ACL2 !>>(MF (MEMOIZE-PARTIAL BAD{ONE-FORMAL}))


ACL2 Error in ( TABLE PARTIAL-FUNCTIONS-TABLE ...):  Illegal partial-
functions-table key and value (see :DOC memoize-partial):
key = BAD{ONE-FORMAL}-LIMIT
value  = ((BAD{ONE-FORMAL} BAD{ONE-FORMAL}-LIMIT
                           BAD{ONE-FORMAL}-LIMIT-CHANGE
                           BAD{ONE-FORMAL}-LIMIT-STABLE
                           (DEFUN BAD{ONE-FORMAL}
                                  NIL (DECLARE (IGNORABLE))
                                  (FLET (#) (DECLARE #) (LET # # #)))))
Reason:
The key is a guard-verified function symbol but it needs at least two
formal parameters.

(See :DOC set-iprint to be able to see elided values in this message.)


ACL2 Error [Failure] in ( TABLE PARTIAL-FUNCTIONS-TABLE ...):  See
:DOC failure.

Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(MUTUAL-RECURSION
             (DEFUN EVENLP{DIFFERENT-LIMIT-VARS}-BDD
                    (X BOUND)
                    (DECLARE (XARGS :GUARD (NATP BOUND)))
                    (IF (ZP BOUND)
                        'OUCH
                        (LET ((BOUND (1- BOUND)))
                             (IF (CONSP X)
                                 (ODDLP{DIFFERENT-LIMIT-VARS}-BDD (CDR X)
                                                                  BOUND)
                                 T))))
             (DEFUN ODDLP{DIFFERENT-LIMIT-VARS}-BDD
                    (X BOUND2)
                    (DECLARE (XARGS :GUARD (NATP BOUND2)))
                    (IF (ZP BOUND2)
                        'OUCH
                        (LET ((BOUND2 (1- BOUND2)))
                             (IF (CONSP X)
                                 (EVENLP{DIFFERENT-LIMIT-VARS}-BDD (CDR X)
                                                                   BOUND2)
                                 NIL)))))

Summary
Form:  ( MUTUAL-RECURSION ( DEFUN EVENLP{DIFFERENT-LIMIT-VARS}-BDD
...) ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
 (EVENLP{DIFFERENT-LIMIT-VARS}-BDD ODDLP{DIFFERENT-LIMIT-VARS}-BDD)
ACL2 !>>(MF
         (MEMOIZE-PARTIAL
            ((EVENLP{DIFFERENT-LIMIT-VARS} EVENLP{DIFFERENT-LIMIT-VARS}-BDD)
             (ODDLP{DIFFERENT-LIMIT-VARS} ODDLP{DIFFERENT-LIMIT-VARS}-BDD))))


ACL2 Error in ( TABLE PARTIAL-FUNCTIONS-TABLE ...):  Illegal partial-
functions-table key and value (see :DOC memoize-partial):
key = EVENLP{DIFFERENT-LIMIT-VARS}-BDD
value  = ((EVENLP{DIFFERENT-LIMIT-VARS}
               EVENLP{DIFFERENT-LIMIT-VARS}-BDD
               EVENLP{DIFFERENT-LIMIT-VARS}-BDD-CHANGE
               EVENLP{DIFFERENT-LIMIT-VARS}-BDD-STABLE
               (DEFUN EVENLP{DIFFERENT-LIMIT-VARS} (X)
                      (DECLARE (IGNORABLE X))
                      (FLET (# #) (DECLARE #) (LET # # #))))
          (ODDLP{DIFFERENT-LIMIT-VARS}
               ODDLP{DIFFERENT-LIMIT-VARS}-BDD
               ODDLP{DIFFERENT-LIMIT-VARS}-BDD-CHANGE
               ODDLP{DIFFERENT-LIMIT-VARS}-BDD-STABLE
               (DEFUN ODDLP{DIFFERENT-LIMIT-VARS} (X)
                      (DECLARE (IGNORABLE X))
                      (FLET (# #) (DECLARE #) (LET # # #)))))
Reason:
The formal parameter lists for function symbols 
EVENLP{DIFFERENT-LIMIT-VARS}-BDD and ODDLP{DIFFERENT-LIMIT-VARS}-BDD
have different final elements (of BOUND and BOUND2, respectively).

(See :DOC set-iprint to be able to see elided values in this message.)


ACL2 Error [Failure] in ( TABLE PARTIAL-FUNCTIONS-TABLE ...):  See
:DOC failure.

Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(DEFMACRO MY-IF (X Y Z)
                  (CONS 'IF
                        (CONS X (CONS Y (CONS Z 'NIL)))))

Summary
Form:  ( DEFMACRO MY-IF ...)
Rules: NIL
 MY-IF
ACL2 !>>(DEFUN BAD{WRONG-IF}-LIMIT (N LIMIT)
               (DECLARE (TYPE (INTEGER 0 *) LIMIT)
                        (TYPE (INTEGER 0 *) N))
               (MY-IF (ZP LIMIT)
                      0
                      (LET ((LIMIT (1- LIMIT)))
                           (IF (OR (ZP N) (= N 1))
                               1
                               (+ (BAD{WRONG-IF}-LIMIT (- N 1) LIMIT)
                                  (BAD{WRONG-IF}-LIMIT (- N 2) LIMIT))))))
Subgoal 2
Subgoal 2.2
Subgoal 2.1
Subgoal 1
Subgoal 1'
Goal'
Goal''

Summary
Form:  ( DEFUN BAD{WRONG-IF}-LIMIT ...)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION ACL2-COUNT)
        (:DEFINITION INTEGER-ABS)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O<)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART INTEGERP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:EXECUTABLE-COUNTERPART UNARY--)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE DISTRIBUTIVITY-OF-MINUS-OVER-+)
        (:TYPE-PRESCRIPTION BAD{WRONG-IF}-LIMIT))
 BAD{WRONG-IF}-LIMIT
ACL2 !>>(MF (MEMOIZE-PARTIAL BAD{WRONG-IF}))


ACL2 Error in MEMOIZE-PARTIAL:  
The (untranslated) body of function BAD{WRONG-IF}-LIMIT is not of the
appropriate form.
See :DOC memoize-partial.



Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(DEFUN BAD{WRONG-ZP}-LIMIT (N LIMIT)
               (DECLARE (TYPE (INTEGER 0 *) LIMIT)
                        (TYPE (INTEGER 0 *) N))
               (IF (NOT (POSP LIMIT))
                   0
                   (LET ((LIMIT (1- LIMIT)))
                        (IF (OR (ZP N) (= N 1))
                            1
                            (+ (BAD{WRONG-ZP}-LIMIT (- N 1) LIMIT)
                               (BAD{WRONG-ZP}-LIMIT (- N 2) LIMIT))))))
Subgoal 2
Subgoal 2.2
Subgoal 2.1
Subgoal 1
Subgoal 1'
Goal'
Goal''

Summary
Form:  ( DEFUN BAD{WRONG-ZP}-LIMIT ...)
Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION ACL2-COUNT)
        (:DEFINITION INTEGER-ABS)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O<)
        (:DEFINITION POSP)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART INTEGERP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:EXECUTABLE-COUNTERPART UNARY--)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE DISTRIBUTIVITY-OF-MINUS-OVER-+)
        (:TYPE-PRESCRIPTION BAD{WRONG-ZP}-LIMIT))
 BAD{WRONG-ZP}-LIMIT
ACL2 !>>(MF (MEMOIZE-PARTIAL BAD{WRONG-ZP}))


ACL2 Error in MEMOIZE-PARTIAL:  
The (untranslated) body of function BAD{WRONG-ZP}-LIMIT is not of the
appropriate form.
See :DOC memoize-partial.



Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(MF (MEMOIZE-PARTIAL MY-UNDEF))


ACL2 Error in MEMOIZE-PARTIAL:  You must define MY-UNDEF-LIMIT before
submitting your memoize-partial form.  See :DOC memoize-partial.


Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(DEFUN BAD{NON-REC}-LIMIT (X LIMIT)
               (DECLARE (TYPE (INTEGER 0 *) LIMIT))
               (IF (ZP LIMIT)
                   0
                   (LET ((LIMIT (1- LIMIT)))
                        (CONS X LIMIT))))

Summary
Form:  ( DEFUN BAD{NON-REC}-LIMIT ...)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
 BAD{NON-REC}-LIMIT
ACL2 !>>(MF (MEMOIZE-PARTIAL BAD{NON-REC}))


ACL2 Error in ( TABLE PARTIAL-FUNCTIONS-TABLE ...):  Illegal partial-
functions-table key and value (see :DOC memoize-partial):
key = BAD{NON-REC}-LIMIT
value  = ((BAD{NON-REC} BAD{NON-REC}-LIMIT
                        BAD{NON-REC}-LIMIT-CHANGE
                        BAD{NON-REC}-LIMIT-STABLE
                        (DEFUN BAD{NON-REC} (X)
                               (DECLARE (IGNORABLE X))
                               (FLET (#) (DECLARE #) (LET # # #)))))
Reason:
The key is a non-recursive function symbol.

(See :DOC set-iprint to be able to see elided values in this message.)


ACL2 Error [Failure] in ( TABLE PARTIAL-FUNCTIONS-TABLE ...):  See
:DOC failure.

Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(UNMEMOIZE 'EVENLP)
 EVENLP
ACL2 !>>(UNMEMOIZE 'ODDLP)
 ODDLP
ACL2 !>>(MF (MEMOIZE-PARTIAL ((EVENLP EVENLP-BDD))))


ACL2 Error in ( TABLE PARTIAL-FUNCTIONS-TABLE ...):  Illegal partial-
functions-table key and value (see :DOC memoize-partial):
key = EVENLP-BDD
value  = ((EVENLP EVENLP-BDD
                  EVENLP-BDD-CHANGE EVENLP-BDD-STABLE
                  (DEFUN EVENLP (X)
                         (DECLARE (IGNORABLE X))
                         (FLET (#) (DECLARE #) (LET # # #)))))
Reason:
The strip-cadrs of the proposed value is not the list of function symbols,
in order, defined by mutual-recursion with the key.  That expected
list of functions is (EVENLP-BDD ODDLP-BDD).

(See :DOC set-iprint to be able to see elided values in this message.)


ACL2 Error [Failure] in ( TABLE PARTIAL-FUNCTIONS-TABLE ...):  See
:DOC failure.

Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(MF (MEMOIZE-PARTIAL ((ODDLP ODDLP-BDD))))


ACL2 Error in ( TABLE PARTIAL-FUNCTIONS-TABLE ...):  Illegal partial-
functions-table key and value (see :DOC memoize-partial):
key = ODDLP-BDD
value  = ((ODDLP ODDLP-BDD
                 ODDLP-BDD-CHANGE ODDLP-BDD-STABLE
                 (DEFUN ODDLP (X)
                        (DECLARE (IGNORABLE X))
                        (FLET (#) (DECLARE #) (LET # # #)))))
Reason:
The strip-cadrs of the proposed value is not the list of function symbols,
in order, defined by mutual-recursion with the key.  That expected
list of functions is (EVENLP-BDD ODDLP-BDD).

(See :DOC set-iprint to be able to see elided values in this message.)


ACL2 Error [Failure] in ( TABLE PARTIAL-FUNCTIONS-TABLE ...):  See
:DOC failure.

Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(MF (MEMOIZE-PARTIAL ((ODDLP ODDLP-BDD)
                              (EVENLP EVENLP-BDD))))


ACL2 Error in ( TABLE PARTIAL-FUNCTIONS-TABLE ...):  Illegal partial-
functions-table key and value (see :DOC memoize-partial):
key = ODDLP-BDD
value  = ((ODDLP ODDLP-BDD
                 ODDLP-BDD-CHANGE ODDLP-BDD-STABLE
                 (DEFUN ODDLP (X)
                        (DECLARE (IGNORABLE X))
                        (FLET (# #) (DECLARE #) (LET # # #))))
          (EVENLP EVENLP-BDD
                  EVENLP-BDD-CHANGE EVENLP-BDD-STABLE
                  (DEFUN EVENLP (X)
                         (DECLARE (IGNORABLE X))
                         (FLET (# #) (DECLARE #) (LET # # #)))))
Reason:
The strip-cadrs of the proposed value is not the list of function symbols,
in order, defined by mutual-recursion with the key.  That expected
list of functions is (EVENLP-BDD ODDLP-BDD).

(See :DOC set-iprint to be able to see elided values in this message.)


ACL2 Error [Failure] in ( TABLE PARTIAL-FUNCTIONS-TABLE ...):  See
:DOC failure.

Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(MUTUAL-RECURSION (DEFUN EVENLP2-BDD (X BOUND)
                                 (DECLARE (XARGS :GUARD (NATP BOUND)))
                                 (IF (ZP BOUND)
                                     'OUCH
                                     (LET ((BOUND (1- BOUND)))
                                          (IF (CONSP X)
                                              (ODDLP2-BDD (CDR X) BOUND)
                                              T))))
                          (DEFUN ODDLP2-BDD (X BOUND)
                                 (DECLARE (XARGS :GUARD (NATP BOUND)))
                                 (IF (ZP BOUND)
                                     'OUCH
                                     (LET ((BOUND (1- BOUND)))
                                          (IF (CONSP X)
                                              (EVENLP2-BDD (CDR X) BOUND)
                                              NIL)))))

Summary
Form:  ( MUTUAL-RECURSION ( DEFUN EVENLP2-BDD ...) ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
 (EVENLP2-BDD ODDLP2-BDD)
ACL2 !>>(MF
         (ENCAPSULATE
          NIL
          (DEFCHOOSE EVENLP2-BDD-CHANGE (LARGE)
                     (X BOUND)
                     (AND (NATP LARGE)
                          (<= BOUND LARGE)
                          (NOT (EQUAL (EVENLP2-BDD X BOUND)
                                      (EVENLP2-BDD X LARGE)))))
          (DEFCHOOSE
               EVENLP2-BDD-STABLE (BOUND)
               (X)
               (AND (NATP BOUND)
                    (EQUAL (EVENLP2-BDD X BOUND)
                           (EVENLP2-BDD X (EVENLP2-BDD-CHANGE X BOUND)))))
          (DEFUN EVENLP2 (X)
                 (DECLARE (XARGS :GUARD (LET ((BOUND 0))
                                             (DECLARE (IGNORABLE BOUND))
                                             (NATP BOUND))))
                 (EVENLP2-BDD X (NFIX (EVENLP2-BDD-STABLE X))))
          (DEFCHOOSE ODDLP2-BDD-CHANGE (LARGE)
                     (X BOUND)
                     (AND (NATP LARGE)
                          (<= BOUND LARGE)
                          (NOT (EQUAL (ODDLP2-BDD X BOUND)
                                      (ODDLP2-BDD X LARGE)))))
          (DEFCHOOSE
               ODDLP2-BDD-STABLE (BOUND)
               (X)
               (AND (NATP BOUND)
                    (EQUAL (ODDLP2-BDD X BOUND)
                           (ODDLP2-BDD X (ODDLP2-BDD-CHANGE X BOUND)))))
          (TABLE
               PARTIAL-FUNCTIONS-TABLE 'EVENLP2-BDD
               '((EVENLP2 EVENLP2-BDD
                          EVENLP2-BDD-CHANGE EVENLP2-BDD-STABLE
                          (DEFUN EVENLP2 (X)
                                 (DECLARE (IGNORABLE X))
                                 (FLET ((EVENLP2-BDD (X BOUND)
                                                     (DECLARE (IGNORE BOUND))
                                                     (EVENLP2 X))
                                        (ODDLP2-BDD (X BOUND)
                                                    (DECLARE (IGNORE BOUND))
                                                    (ODDLP2 X)))
                                       (DECLARE (INLINE EVENLP2-BDD))
                                       (LET ((BOUND 0))
                                            (DECLARE (IGNORABLE BOUND))
                                            (IF (CONSP X)
                                                (ODDLP2-BDD (CDR X) BOUND)
                                                T)))))
                 (ODDLP2 ODDLP2-BDD
                         ODDLP2-BDD-CHANGE ODDLP2-BDD-STABLE
                         (DEFUN ODDLP2 (X)
                                (DECLARE (IGNORABLE X))
                                (FLET ((EVENLP2-BDD (X BOUND)
                                                    (DECLARE (IGNORE BOUND))
                                                    (EVENLP2 X))
                                       (ODDLP2-BDD (X BOUND)
                                                   (DECLARE (IGNORE BOUND))
                                                   (ODDLP2 X)))
                                      (DECLARE (INLINE ODDLP2-BDD))
                                      (LET ((BOUND 0))
                                           (DECLARE (IGNORABLE BOUND))
                                           (IF (CONSP X)
                                               (EVENLP2-BDD (CDR X) BOUND)
                                               NIL)))))))
          (MEMOIZE 'EVENLP2 :TOTAL 'EVENLP2-BDD)
          (MEMOIZE 'ODDLP2 :TOTAL 'ODDLP2-BDD)))


ACL2 Error in ( TABLE PARTIAL-FUNCTIONS-TABLE ...):  Illegal partial-
functions-table key and value (see :DOC memoize-partial):
key = EVENLP2-BDD
value  = ((EVENLP2 EVENLP2-BDD
                   EVENLP2-BDD-CHANGE EVENLP2-BDD-STABLE
                   (DEFUN EVENLP2 (X)
                          (DECLARE (IGNORABLE X))
                          (FLET (# #) (DECLARE #) (LET # # #))))
          (ODDLP2 ODDLP2-BDD
                  ODDLP2-BDD-CHANGE ODDLP2-BDD-STABLE
                  (DEFUN ODDLP2 (X)
                         (DECLARE (IGNORABLE X))
                         (FLET (# #) (DECLARE #) (LET # # #)))))
Reason:
The following event is missing:

(DEFUN ODDLP2 (X)
       (DECLARE (XARGS :GUARD (LET ((BOUND 0))
                                   (DECLARE (IGNORABLE BOUND))
                                   (NATP BOUND))))
       (ODDLP2-BDD X (NFIX (ODDLP2-BDD-STABLE X))))


(See :DOC set-iprint to be able to see elided values in this message.)


ACL2 Error [Failure] in ( TABLE PARTIAL-FUNCTIONS-TABLE ...):  See
:DOC failure.

ACL2 Warning in ( ENCAPSULATE NIL (DEFCHOOSE EVENLP2-BDD-CHANGE ...)
...):  The attempted ENCAPSULATE has failed while trying to establish
the admissibility of one of the (local or non-local) forms in the body
of the ENCAPSULATE.


Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(MF
         (ENCAPSULATE
          NIL
          (DEFCHOOSE EVENLP2-BDD-CHANGE (LARGE)
                     (X BOUND)
                     (AND (NATP LARGE)
                          (<= BOUND LARGE)
                          (NOT (EQUAL (EVENLP2-BDD X BOUND)
                                      (EVENLP2-BDD X LARGE)))))
          (DEFCHOOSE
               EVENLP2-BDD-STABLE (BOUND)
               (X)
               (AND (NATP BOUND)
                    (EQUAL (EVENLP2-BDD X BOUND)
                           (EVENLP2-BDD X (EVENLP2-BDD-CHANGE X BOUND)))))
          (DEFUN EVENLP2 (X)
                 (DECLARE (XARGS :GUARD (LET ((BOUND 0))
                                             (DECLARE (IGNORABLE BOUND))
                                             (NATP BOUND))))
                 X)
          (DEFCHOOSE ODDLP2-BDD-CHANGE (LARGE)
                     (X BOUND)
                     (AND (NATP LARGE)
                          (<= BOUND LARGE)
                          (NOT (EQUAL (ODDLP2-BDD X BOUND)
                                      (ODDLP2-BDD X LARGE)))))
          (DEFCHOOSE
               ODDLP2-BDD-STABLE (BOUND)
               (X)
               (AND (NATP BOUND)
                    (EQUAL (ODDLP2-BDD X BOUND)
                           (ODDLP2-BDD X (ODDLP2-BDD-CHANGE X BOUND)))))
          (TABLE
               PARTIAL-FUNCTIONS-TABLE 'EVENLP2-BDD
               '((EVENLP2 EVENLP2-BDD
                          EVENLP2-BDD-CHANGE EVENLP2-BDD-STABLE
                          (DEFUN EVENLP2 (X)
                                 (DECLARE (IGNORABLE X))
                                 (FLET ((EVENLP2-BDD (X BOUND)
                                                     (DECLARE (IGNORE BOUND))
                                                     (EVENLP2 X))
                                        (ODDLP2-BDD (X BOUND)
                                                    (DECLARE (IGNORE BOUND))
                                                    (ODDLP2 X)))
                                       (DECLARE (INLINE EVENLP2-BDD))
                                       (LET ((BOUND 0))
                                            (DECLARE (IGNORABLE BOUND))
                                            (IF (CONSP X)
                                                (ODDLP2-BDD (CDR X) BOUND)
                                                T)))))
                 (ODDLP2 ODDLP2-BDD
                         ODDLP2-BDD-CHANGE ODDLP2-BDD-STABLE
                         (DEFUN ODDLP2 (X)
                                (DECLARE (IGNORABLE X))
                                (FLET ((EVENLP2-BDD (X BOUND)
                                                    (DECLARE (IGNORE BOUND))
                                                    (EVENLP2 X))
                                       (ODDLP2-BDD (X BOUND)
                                                   (DECLARE (IGNORE BOUND))
                                                   (ODDLP2 X)))
                                      (DECLARE (INLINE ODDLP2-BDD))
                                      (LET ((BOUND 0))
                                           (DECLARE (IGNORABLE BOUND))
                                           (IF (CONSP X)
                                               (EVENLP2-BDD (CDR X) BOUND)
                                               NIL)))))))))


ACL2 Error in ( TABLE PARTIAL-FUNCTIONS-TABLE ...):  Illegal partial-
functions-table key and value (see :DOC memoize-partial):
key = EVENLP2-BDD
value  = ((EVENLP2 EVENLP2-BDD
                   EVENLP2-BDD-CHANGE EVENLP2-BDD-STABLE
                   (DEFUN EVENLP2 (X)
                          (DECLARE (IGNORABLE X))
                          (FLET (# #) (DECLARE #) (LET # # #))))
          (ODDLP2 ODDLP2-BDD
                  ODDLP2-BDD-CHANGE ODDLP2-BDD-STABLE
                  (DEFUN ODDLP2 (X)
                         (DECLARE (IGNORABLE X))
                         (FLET (# #) (DECLARE #) (LET # # #)))))
Reason:
The following events are missing:

(DEFUN EVENLP2 (X)
       (DECLARE (XARGS :GUARD (LET ((BOUND 0))
                                   (DECLARE (IGNORABLE BOUND))
                                   (NATP BOUND))))
       (EVENLP2-BDD X (NFIX (EVENLP2-BDD-STABLE X))))

(DEFUN ODDLP2 (X)
       (DECLARE (XARGS :GUARD (LET ((BOUND 0))
                                   (DECLARE (IGNORABLE BOUND))
                                   (NATP BOUND))))
       (ODDLP2-BDD X (NFIX (ODDLP2-BDD-STABLE X))))


(See :DOC set-iprint to be able to see elided values in this message.)


ACL2 Error [Failure] in ( TABLE PARTIAL-FUNCTIONS-TABLE ...):  See
:DOC failure.

ACL2 Warning in ( ENCAPSULATE NIL (DEFCHOOSE EVENLP2-BDD-CHANGE ...)
...):  The attempted ENCAPSULATE has failed while trying to establish
the admissibility of one of the (local or non-local) forms in the body
of the ENCAPSULATE.


Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(MF (MEMOIZE-PARTIAL ((FIB2-NEW FIB2-CLOCK
                                        :CHANGE FIB2-CLOCK-CHANGE0-NEW
                                        :CHANGE FIB2-CLOCK-CHANGE0-NEW2
                                        :STABLE FIB2-CLOCK-STABLE0-NEW
                                        :CONDITION '(EQL (MOD N 4) 0)))
                             :CONDITION T)
            :EXPECTED :HARD)


HARD ACL2 ERROR in MEMOIZE-PARTIAL:  Ill-formed argument for memoize-
partial: The keyword :CHANGE appears more than once for the tuple associated
with FIB2-NEW.  See :DOC memoize-partial.



ACL2 Error in HARD-ERROR-TO-SOFT-ERROR:  In the attempt to macroexpand
the form 
(MEMOIZE-PARTIAL ((FIB2-NEW FIB2-CLOCK
                            :CHANGE FIB2-CLOCK-CHANGE0-NEW
                            :CHANGE FIB2-CLOCK-CHANGE0-NEW2
                            :STABLE ...))
                 :CONDITION T),
evaluation of the macro body caused the error below.

Evaluation aborted.  To debug see :DOC print-gv, see :DOC trace, and
see :DOC wet.
(See :DOC set-iprint to be able to see elided values in this message.)


Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(MEMOIZE-PARTIAL ((FIB2-NEW FIB2-CLOCK
                                    :CHANGE FIB2-CLOCK-CHANGE0-NEW
                                    :STABLE FIB2-CLOCK-STABLE0-NEW
                                    :CONDITION '(EQL (MOD N 4) 0)))
                         :CONDITION T)

Summary
Form:  ( DEFCHOOSE FIB2-CLOCK-CHANGE0-NEW ...)
Rules: NIL
FIB2-CLOCK-CHANGE0-NEW

Summary
Form:  ( DEFCHOOSE FIB2-CLOCK-STABLE0-NEW ...)
Rules: NIL
FIB2-CLOCK-STABLE0-NEW

Summary
Form:  ( DEFUN FIB2-NEW ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:TYPE-PRESCRIPTION FIB2-CLOCK)
        (:TYPE-PRESCRIPTION NFIX))
FIB2-NEW

Summary
Form:  ( TABLE PARTIAL-FUNCTIONS-TABLE ...)
Rules: NIL
PARTIAL-FUNCTIONS-TABLE

Summary
Form:  ( PROGN (DEFCHOOSE FIB2-CLOCK-CHANGE0-NEW ...) ...)
Rules: NIL

Summary
Form:  ( MAKE-EVENT (ER-PROGN ...) ...)
Rules: NIL
PARTIAL-FUNCTIONS-TABLE

Summary
Form:  ( DEFUN FIB2-NEW-MEMOIZE-CONDITION ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
FIB2-NEW-MEMOIZE-CONDITION

Summary
Form:  ( VERIFY-GUARDS FIB2-NEW-MEMOIZE-CONDITION)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:EXECUTABLE-COUNTERPART EQL)
        (:EXECUTABLE-COUNTERPART EQLABLEP)
        (:EXECUTABLE-COUNTERPART NOT))
FIB2-NEW-MEMOIZE-CONDITION

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
MEMOIZE-TABLE
FIB2-NEW

Summary
Form:  ( PROGN (DEFUN FIB2-NEW-MEMOIZE-CONDITION ...) ...)
Rules: NIL

Summary
Form:  ( MAKE-EVENT (LET* ...))
Rules: NIL
FIB2-NEW

Summary
Form:  ( PROGN (MAKE-EVENT ...) ...)
Rules: NIL
 FIB2-NEW
ACL2 !>>(ASSERT-EVENT (EQUAL (FIB2-NEW 30)
                             (FIB2-CLOCK 30 50)))
 :PASSED
ACL2 !>>(ASSERT-EVENT (EQUAL (FIB2-NEW 80) 37889062373143906))
 :PASSED
ACL2 !>>(MF (MEMOIZE-PARTIAL ((FIB2-NEW FIB2-CLOCK
                                        :CHANGE FIB2-CLOCK-CHANGE0-NEW
                                        :STABLE FIB2-CLOCK-STABLE0-NEW
                                        :CONDITION '(EQL (MOD N 4) 0))
                              . BAD-CDR)
                             :CONDITION T)
            :EXPECTED :HARD)


HARD ACL2 ERROR in MEMOIZE-PARTIAL:  Ill-formed argument for memoize-
partial: Not a null-terminated list.  See :DOC memoize-partial.



ACL2 Error in HARD-ERROR-TO-SOFT-ERROR:  In the attempt to macroexpand
the form 
(MEMOIZE-PARTIAL ((FIB2-NEW FIB2-CLOCK
                            :CHANGE FIB2-CLOCK-CHANGE0-NEW
                            :STABLE FIB2-CLOCK-STABLE0-NEW
                            :CONDITION ...)
                  . BAD-CDR)
                 :CONDITION T),
evaluation of the macro body caused the error below.

Evaluation aborted.  To debug see :DOC print-gv, see :DOC trace, and
see :DOC wet.
(See :DOC set-iprint to be able to see elided values in this message.)


Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(MF (MEMOIZE-PARTIAL ((FIB2-NEW FIB2-CLOCK JUNK-THAT-DOES-NOT-BELONG
                                        :CHANGE FIB2-CLOCK-CHANGE0-NEW
                                        :STABLE FIB2-CLOCK-STABLE0-NEW
                                        :CONDITION '(EQL (MOD N 4) 0)))
                             :CONDITION T)
            :EXPECTED :HARD)


HARD ACL2 ERROR in MEMOIZE-PARTIAL:  Ill-formed argument for memoize-
partial: The tuple associated with FIB2-NEW is not of the form (fn
fn-limit :kwd1 val1 ... :kwdn valn).  See :DOC memoize-partial.



ACL2 Error in HARD-ERROR-TO-SOFT-ERROR:  In the attempt to macroexpand
the form 
(MEMOIZE-PARTIAL ((FIB2-NEW FIB2-CLOCK JUNK-THAT-DOES-NOT-BELONG
                            :CHANGE FIB2-CLOCK-CHANGE0-NEW
                            :STABLE FIB2-CLOCK-STABLE0-NEW ...))
                 :CONDITION T),
evaluation of the macro body caused the error below.

Evaluation aborted.  To debug see :DOC print-gv, see :DOC trace, and
see :DOC wet.
(See :DOC set-iprint to be able to see elided values in this message.)


Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(MF
           (MEMOIZE-PARTIAL ((FIB2-NEW FIB2-CLOCK
                                       :CHANGE FIB2-CLOCK-CHANGE0-NEW :STABLE
                                       FIB2-CLOCK-STABLE0-NEW :CONDITION))
                            :CONDITION T)
           :EXPECTED :HARD)


HARD ACL2 ERROR in MEMOIZE-PARTIAL:  Ill-formed argument for memoize-
partial: The tuple associated with FIB2-NEW is not of the form (fn
fn-limit :kwd1 val1 ... :kwdn valn).  See :DOC memoize-partial.



ACL2 Error in HARD-ERROR-TO-SOFT-ERROR:  In the attempt to macroexpand
the form 
(MEMOIZE-PARTIAL ((FIB2-NEW FIB2-CLOCK
                            :CHANGE FIB2-CLOCK-CHANGE0-NEW :STABLE
                            FIB2-CLOCK-STABLE0-NEW :CONDITION))
                 :CONDITION T),
evaluation of the macro body caused the error below.

Evaluation aborted.  To debug see :DOC print-gv, see :DOC trace, and
see :DOC wet.


Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(MF (MEMOIZE-PARTIAL 'FIB)
            :EXPECTED :HARD)


HARD ACL2 ERROR in MEMOIZE-PARTIAL:  The argument for memoize-partial
should not be quoted.  Perhaps you intended that argument to be FIB.
See :DOC memoize-partial.



ACL2 Error in HARD-ERROR-TO-SOFT-ERROR:  In the attempt to macroexpand
the form (MEMOIZE-PARTIAL 'FIB), evaluation of the macro body caused
the error below.

Evaluation aborted.  To debug see :DOC print-gv, see :DOC trace, and
see :DOC wet.


Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(MF (MEMOIZE-PARTIAL ((FIB2-NEW FIB2-CLOCK
                                        :CHANGE FIB2-CLOCK-CHANGE0-NEW
                                        :STABLE FIB2-CLOCK-STABLE0-NEW
                                        :CONDITION T))
                             :CONDITION)
            :EXPECTED :HARD)


HARD ACL2 ERROR in MEMOIZE-PARTIAL:  The arguments to MEMOIZE-PARTIAL
after the first argument should be an alternating list of keywords
and values (keyword first), which will be passed to MEMOIZE.  The call
(MEMOIZE-PARTIAL ((FIB2-NEW FIB2-CLOCK
                            :CHANGE FIB2-CLOCK-CHANGE0-NEW
                            :STABLE FIB2-CLOCK-STABLE0-NEW
                            :CONDITION ...))
                 :CONDITION)
is thus illegal.  See :DOC memoize-partial.
(See :DOC set-iprint to be able to see elided values in this message.)



ACL2 Error in HARD-ERROR-TO-SOFT-ERROR:  In the attempt to macroexpand
the form 
(MEMOIZE-PARTIAL ((FIB2-NEW FIB2-CLOCK
                            :CHANGE FIB2-CLOCK-CHANGE0-NEW
                            :STABLE FIB2-CLOCK-STABLE0-NEW
                            :CONDITION ...))
                 :CONDITION),
evaluation of the macro body caused the error below.

Evaluation aborted.  To debug see :DOC print-gv, see :DOC trace, and
see :DOC wet.
(See :DOC set-iprint to be able to see elided values in this message.)


Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(DEFSTOBJ ST FLD)

Summary
Form:  ( DEFSTOBJ ST ...)
Rules: NIL
 ST
ACL2 !>>(DEFUN FIB-ST-LIMIT (N ST LIMIT)
               (DECLARE (TYPE (INTEGER 0 *) LIMIT)
                        (TYPE INTEGER N))
               (DECLARE (XARGS :MEASURE (NFIX LIMIT)
                               :STOBJS ST))
               (IF (ZP LIMIT)
                   (PROG2$ (ER HARD? 'FIB-ST-LIMIT
                               "Hit the limit: n=~x0 (fld st)=~x1."
                               N (FLD ST))
                           0)
                   (LET ((LIMIT (1- LIMIT)))
                        (IF (OR (= N 0) (= N 1))
                            1
                            (+ (FIB-ST-LIMIT (- N 1) ST LIMIT)
                               (FIB-ST-LIMIT (- N 2) ST LIMIT))))))
Subgoal 2
Subgoal 1
Subgoal 1'

Summary
Form:  ( DEFUN FIB-ST-LIMIT ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION NFIX)
        (:DEFINITION O-FINP)
        (:DEFINITION O-P)
        (:DEFINITION O<)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION FIB-ST-LIMIT))
 FIB-ST-LIMIT
ACL2 !>>(MEMOIZE-PARTIAL FIB-ST)

Summary
Form:  ( DEFCHOOSE FIB-ST-LIMIT-CHANGE ...)
Rules: NIL
FIB-ST-LIMIT-CHANGE

Summary
Form:  ( DEFCHOOSE FIB-ST-LIMIT-STABLE ...)
Rules: NIL
FIB-ST-LIMIT-STABLE

Summary
Form:  ( DEFUN FIB-ST ...)
Rules: ((:TYPE-PRESCRIPTION FIB-ST-LIMIT))
FIB-ST

Summary
Form:  ( TABLE PARTIAL-FUNCTIONS-TABLE ...)
Rules: NIL
PARTIAL-FUNCTIONS-TABLE

Summary
Form:  ( PROGN (DEFCHOOSE FIB-ST-LIMIT-CHANGE ...) ...)
Rules: NIL

Summary
Form:  ( MAKE-EVENT (ER-PROGN ...) ...)
Rules: NIL
PARTIAL-FUNCTIONS-TABLE

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
MEMOIZE-TABLE
FIB-ST

Summary
Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
Rules: NIL
FIB-ST

Summary
Form:  ( PROGN (MAKE-EVENT ...) ...)
Rules: NIL
 FIB-ST
ACL2 !>>(ASSERT-EVENT (EQUAL (FIB-ST 100 ST)
                             573147844013817084101))
 :PASSED
ACL2 !>>(DEFUN
             FIB-ST-OUT-LIMIT (N ST LIMIT)
             (DECLARE (TYPE (INTEGER 0 *) LIMIT)
                      (TYPE INTEGER N))
             (DECLARE (XARGS :MEASURE (NFIX LIMIT)
                             :STOBJS ST
                             :VERIFY-GUARDS NIL))
             (IF (ZP LIMIT)
                 (MV 0 ST)
                 (LET ((LIMIT (1- LIMIT)))
                      (IF (OR (= N 0) (= N 1))
                          (MV 1 ST)
                          (MV-LET (X1 ST)
                                  (FIB-ST-OUT-LIMIT (- N 1) ST LIMIT)
                                  (MV-LET (X2 ST)
                                          (FIB-ST-OUT-LIMIT (- N 2) ST LIMIT)
                                          (MV (+ X1 X2) ST)))))))
Subgoal 2
Subgoal 1
Subgoal 1'

Summary
Form:  ( DEFUN FIB-ST-OUT-LIMIT ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION NFIX)
        (:DEFINITION O-FINP)
        (:DEFINITION O-P)
        (:DEFINITION O<)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
 FIB-ST-OUT-LIMIT
ACL2 !>>(DEFTHM NATP-FIB-ST-OUT-LIMIT-0
                (NATP (CAR (FIB-ST-OUT-LIMIT N LIMIT ST)))
                :RULE-CLASSES :TYPE-PRESCRIPTION)

ACL2 Observation in ( DEFTHM NATP-FIB-ST-OUT-LIMIT-0 ...):  Our heuristics
choose (CAR (FIB-ST-OUT-LIMIT N LIMIT ST)) as the :TYPED-TERM.
Subgoal 2
Subgoal 1
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1

Summary
Form:  ( DEFTHM NATP-FIB-ST-OUT-LIMIT-0 ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION FIB-ST-OUT-LIMIT)
        (:DEFINITION MV-NTH)
        (:DEFINITION NATP)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NATP)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FIB-ST-OUT-LIMIT)
        (:REWRITE CAR-CONS)
        (:TYPE-PRESCRIPTION FIB-ST-OUT-LIMIT))
 NATP-FIB-ST-OUT-LIMIT-0
ACL2 !>>(VERIFY-GUARDS FIB-ST-OUT-LIMIT)
Goal'

Summary
Form:  ( VERIFY-GUARDS FIB-ST-OUT-LIMIT)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION LENGTH)
        (:DEFINITION MV-NTH)
        (:DEFINITION NOT)
        (:DEFINITION STP)
        (:EXECUTABLE-COUNTERPART ACL2-NUMBERP)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION FIB-ST-OUT-LIMIT)
        (:TYPE-PRESCRIPTION NATP-FIB-ST-OUT-LIMIT-0))
 FIB-ST-OUT-LIMIT
ACL2 !>>(MF (MEMOIZE-PARTIAL FIB-ST-OUT))


ACL2 Error in MEMOIZE-PARTIAL:  
The stobj ST is returned by FIB-ST-OUT-LIMIT, which is illegal for
memoization.
See :DOC memoize-partial.



Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(DEFUN
           FIB-STATE-LIMIT (N STATE LIMIT)
           (DECLARE (TYPE (INTEGER 0 *) LIMIT)
                    (TYPE INTEGER N))
           (DECLARE (XARGS :MEASURE (NFIX LIMIT)
                           :STOBJS STATE
                           :VERIFY-GUARDS NIL))
           (IF (ZP LIMIT)
               (MV 0 STATE)
               (LET ((LIMIT (1- LIMIT)))
                    (IF (OR (= N 0) (= N 1))
                        (MV 1 STATE)
                        (MV-LET (X1 STATE)
                                (FIB-STATE-LIMIT (- N 1) STATE LIMIT)
                                (MV-LET (X2 STATE)
                                        (FIB-STATE-LIMIT (- N 2) STATE LIMIT)
                                        (MV (+ X1 X2) STATE)))))))
Subgoal 2
Subgoal 1
Subgoal 1'

Summary
Form:  ( DEFUN FIB-STATE-LIMIT ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION NFIX)
        (:DEFINITION O-FINP)
        (:DEFINITION O-P)
        (:DEFINITION O<)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
 FIB-STATE-LIMIT
ACL2 !>>(DEFTHM NATP-FIB-STATE-LIMIT-0
                (NATP (CAR (FIB-STATE-LIMIT N LIMIT STATE)))
                :RULE-CLASSES :TYPE-PRESCRIPTION)

ACL2 Observation in ( DEFTHM NATP-FIB-STATE-LIMIT-0 ...):  Our heuristics
choose (CAR (FIB-STATE-LIMIT N LIMIT STATE)) as the :TYPED-TERM.
Subgoal 2
Subgoal 1
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1

Summary
Form:  ( DEFTHM NATP-FIB-STATE-LIMIT-0 ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION FIB-STATE-LIMIT)
        (:DEFINITION MV-NTH)
        (:DEFINITION NATP)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NATP)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FIB-STATE-LIMIT)
        (:REWRITE CAR-CONS)
        (:TYPE-PRESCRIPTION FIB-STATE-LIMIT))
 NATP-FIB-STATE-LIMIT-0
ACL2 !>>(VERIFY-GUARDS FIB-STATE-LIMIT)
Goal'

Summary
Form:  ( VERIFY-GUARDS FIB-STATE-LIMIT)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION MV-NTH)
        (:DEFINITION NOT)
        (:DEFINITION STATE-P)
        (:EXECUTABLE-COUNTERPART ACL2-NUMBERP)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION FIB-STATE-LIMIT)
        (:TYPE-PRESCRIPTION NATP-FIB-STATE-LIMIT-0))
 FIB-STATE-LIMIT
ACL2 !>>(MF (MEMOIZE-PARTIAL FIB-STATE))


ACL2 Error in MEMOIZE-PARTIAL:  
STATE is among the formals of FIB-STATE-LIMIT, which is illegal for
memoization.
See :DOC memoize-partial.



Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
 T
ACL2 !>>(SET-COMPILE-FNS NIL)
 NIL
ACL2 !>>(DEFUN
         COLLATZ-LIMIT (N LIMIT)
         (DECLARE (XARGS :GUARD (AND (NATP N) (NATP LIMIT))
                         :MEASURE (ACL2-COUNT LIMIT)))
         (IF
          (ZP LIMIT)
          (PROG2$ (ER HARD? 'COLLATZ-LIMIT
                      "Limit exceeded!")
                  0)
          (LET ((LIMIT (1- LIMIT)))
               (IF (INT= N 1)
                   0
                   (1+ (COLLATZ-LIMIT (IF (EVENP N) (FLOOR N 2) (1+ (* 3 N)))
                                      LIMIT))))))

Summary
Form:  ( DEFUN COLLATZ-LIMIT ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION EQL)
        (:DEFINITION EVENP)
        (:DEFINITION FLOOR)
        (:DEFINITION NATP)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EQL)
        (:EXECUTABLE-COUNTERPART EQLABLEP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:EXECUTABLE-COUNTERPART UNARY-/)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
 COLLATZ-LIMIT
ACL2 !>>(MEMOIZE-PARTIAL COLLATZ)

Summary
Form:  ( DEFCHOOSE COLLATZ-LIMIT-CHANGE ...)
Rules: NIL
COLLATZ-LIMIT-CHANGE

Summary
Form:  ( DEFCHOOSE COLLATZ-LIMIT-STABLE ...)
Rules: NIL
COLLATZ-LIMIT-STABLE

Summary
Form:  ( DEFUN COLLATZ ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:TYPE-PRESCRIPTION COLLATZ-LIMIT)
        (:TYPE-PRESCRIPTION NATP)
        (:TYPE-PRESCRIPTION NFIX))
COLLATZ

Summary
Form:  ( TABLE PARTIAL-FUNCTIONS-TABLE ...)
Rules: NIL
PARTIAL-FUNCTIONS-TABLE

Summary
Form:  ( PROGN (DEFCHOOSE COLLATZ-LIMIT-CHANGE ...) ...)
Rules: NIL

Summary
Form:  ( MAKE-EVENT (ER-PROGN ...) ...)
Rules: NIL
PARTIAL-FUNCTIONS-TABLE

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
MEMOIZE-TABLE
COLLATZ

Summary
Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
Rules: NIL
COLLATZ

Summary
Form:  ( PROGN (MAKE-EVENT ...) ...)
Rules: NIL
 COLLATZ
ACL2 !>>(SET-ENFORCE-REDUNDANCY T)
 T
ACL2 !>>(ENCAPSULATE
         NIL
         (DEFCHOOSE COLLATZ-LIMIT-CHANGE (LARGE)
                    (N LIMIT)
                    (AND (NATP LARGE)
                         (<= LIMIT LARGE)
                         (NOT (EQUAL (COLLATZ-LIMIT N LIMIT)
                                     (COLLATZ-LIMIT N LARGE)))))
         (DEFCHOOSE
              COLLATZ-LIMIT-STABLE (LIMIT)
              (N)
              (AND (NATP LIMIT)
                   (EQUAL (COLLATZ-LIMIT N LIMIT)
                          (COLLATZ-LIMIT N (COLLATZ-LIMIT-CHANGE N LIMIT)))))
         (DEFUN COLLATZ (N)
                (DECLARE (XARGS :GUARD (LET ((LIMIT 0))
                                            (DECLARE (IGNORABLE LIMIT))
                                            (AND (NATP N) (NATP LIMIT)))))
                (COLLATZ-LIMIT N (NFIX (COLLATZ-LIMIT-STABLE N))))
         (TABLE
          PARTIAL-FUNCTIONS-TABLE 'COLLATZ-LIMIT
          '((COLLATZ
             COLLATZ-LIMIT COLLATZ-LIMIT-CHANGE
             COLLATZ-LIMIT-STABLE
             (DEFUN
              COLLATZ (N)
              (DECLARE (IGNORABLE N))
              (FLET
               ((COLLATZ-LIMIT (N LIMIT)
                               (DECLARE (IGNORE LIMIT))
                               (COLLATZ N)))
               (DECLARE (INLINE COLLATZ-LIMIT))
               (LET
                ((LIMIT 0))
                (DECLARE (IGNORABLE LIMIT))
                (IF
                   (INT= N 1)
                   0
                   (1+ (COLLATZ-LIMIT (IF (EVENP N) (FLOOR N 2) (1+ (* 3 N)))
                                      LIMIT)))))))))
         (MEMOIZE 'COLLATZ
                  :TOTAL 'COLLATZ-LIMIT))

The event ( DEFCHOOSE COLLATZ-LIMIT-CHANGE ...) is redundant.  See
:DOC redundant-events.

Summary
Form:  ( DEFCHOOSE COLLATZ-LIMIT-CHANGE ...)
Rules: NIL
:REDUNDANT

The event ( DEFCHOOSE COLLATZ-LIMIT-STABLE ...) is redundant.  See
:DOC redundant-events.

Summary
Form:  ( DEFCHOOSE COLLATZ-LIMIT-STABLE ...)
Rules: NIL
:REDUNDANT

The event ( DEFUN COLLATZ ...) is redundant.  See :DOC redundant-events.

Summary
Form:  ( DEFUN COLLATZ ...)
Rules: NIL
:REDUNDANT

The event ( TABLE PARTIAL-FUNCTIONS-TABLE ...) is redundant.  See :DOC
redundant-events.

Summary
Form:  ( TABLE PARTIAL-FUNCTIONS-TABLE ...)
Rules: NIL
:REDUNDANT

The event ( TABLE MEMOIZE-TABLE ...) is redundant.  See :DOC redundant-
events.

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
:REDUNDANT
COLLATZ

Summary
Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
Rules: NIL
COLLATZ

ACL2 Observation in ( ENCAPSULATE NIL (DEFCHOOSE COLLATZ-LIMIT-CHANGE
...) ...):  The submitted encapsulate event has created no new ACL2
events, and thus is leaving the ACL2 logical world unchanged.  See
:DOC encapsulate.

Summary
Form:  ( ENCAPSULATE NIL (DEFCHOOSE COLLATZ-LIMIT-CHANGE ...) ...)
Rules: NIL
 :EMPTY-ENCAPSULATE
ACL2 !>>(SET-ENFORCE-REDUNDANCY NIL)
 NIL
ACL2 !>>(DEFUN COLLATZ-SUM-REC (N ACC)
               (DECLARE (XARGS :GUARD (AND (NATP N) (NATP ACC))))
               (IF (ZP N)
                   ACC
                   (COLLATZ-SUM-REC (1- N)
                                    (+ (COLLATZ N) ACC))))

Summary
Form:  ( DEFUN COLLATZ-SUM-REC ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:EXECUTABLE-COUNTERPART NATP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION COLLATZ))
 COLLATZ-SUM-REC
ACL2 !>>(DEFUN COLLATZ-SUM (N)
               (COLLATZ-SUM-REC N 0))

Summary
Form:  ( DEFUN COLLATZ-SUM ...)
Rules: ((:TYPE-PRESCRIPTION COLLATZ-SUM-REC))
 COLLATZ-SUM
ACL2 !>>(DEFUN
             COLLATZ-LIMIT-SUM-REC (N ACC LIMIT)
             (DECLARE (XARGS :GUARD (AND (NATP N) (NATP ACC) (NATP LIMIT))))
             (IF (ZP N)
                 ACC
                 (COLLATZ-LIMIT-SUM-REC (1- N)
                                        (+ (COLLATZ-LIMIT N LIMIT) ACC)
                                        LIMIT)))

Summary
Form:  ( DEFUN COLLATZ-LIMIT-SUM-REC ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION COLLATZ-LIMIT))
 COLLATZ-LIMIT-SUM-REC
ACL2 !>>(DEFUN COLLATZ-LIMIT-SUM (N)
               (COLLATZ-LIMIT-SUM-REC N 0 (1- (EXPT 2 60))))

Summary
Form:  ( DEFUN COLLATZ-LIMIT-SUM ...)
Rules: ((:TYPE-PRESCRIPTION COLLATZ-LIMIT-SUM-REC))
 COLLATZ-LIMIT-SUM
ACL2 !>>(WITH-OUTPUT :OFF
                     :ALL (PROGN (COMP T) (VALUE-TRIPLE NIL)))
 NIL
ACL2 !>>(ASSERT-EVENT (EQUAL (COLLATZ-SUM (EXPT 10 6))
                             131434424))
 :PASSED
ACL2 !>>(ASSERT-EVENT (EQUAL (COLLATZ-LIMIT-SUM (EXPT 10 6))
                             (COLLATZ-SUM (EXPT 10 6))))
 :PASSED
ACL2 !>>Bye.