stirling% v81c
Welcome to Clozure Common Lisp Version 1.12-dev-r16812M-trunk  (DarwinX8664)!

 ACL2 Version 8.1 built January 23, 2019  17:37:11.
 Copyright (C) 2018, Regents of the University of Texas
 ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and you
 are welcome to redistribute it under certain conditions.  For details,
 see the LICENSE file distributed with ACL2.

************************************************************************
*  This is a hacked image of ACL2 on Moore's laptop to explore LOOP$.  *
*  This demo cannot be replayed on any released ACL2 yet.  Maybe ever! *
*  It was used to give the demo of LOOP$ by Moore on 25 Jan 2019.      *
*  The script begins with some setup not shown during the talk.  Find  *
*  ``start demo here'' for the beginning of what the audience saw.     *
************************************************************************

ACL2 Version 8.1.  Level 1.  Cbd "/Users/moore/".
System books directory "/Users/moore/work/acl2/v81c/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>(defmacro ---- (&rest rest)
  (declare (ignore rest))
  '(prog2$ (cw "~%") (value :invisible)))

Summary
Form:  ( DEFMACRO ---- ...)
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 ----
ACL2 !>(ld "/u/moore/text/acl2-work-01/reset-margins-for-demo.lisp")

ACL2 Version 8.1.  Level 2.  Cbd "/u/moore/text/acl2-work-01/".
System books directory "/Users/moore/work/acl2/v81c/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>> "ACL2"
ACL2 !>>
Summary
Form:  ( DEFUN DEMO-PROMPT ...)
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 DEMO-PROMPT
ACL2 !>><state>
ACL2 !>><state>
ACL2 !>> (:WARN! . :OVERWRITE)
ACL2 !>>
TTAG NOTE: Adding ttag :SHORT-MARGINS from the top level loop.
 :SHORT-MARGINS
ACL2 !>>
ACL2 Warning [Redef] in ( DEFCONST *PROOF-FAILURE-STRING* ...):
*PROOF-FAILURE-STRING* redefined.



Summary
Form:  ( DEFCONST *PROOF-FAILURE-STRING* ...)
Rules: NIL
Warnings:  Redef
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 *PROOF-FAILURE-STRING*
ACL2 !>> (:QUERY . :OVERWRITE)
ACL2 !>>
Summary
Form:  ( RESET-PREHISTORY NIL ...)
Rules: NIL
Time:  0.06 seconds (prove: 0.00, print: 0.00, other: 0.06)
 :NEW-PREHISTORY-SET
ACL2 !>>Bye.
 :EOF
ACL2 !>(set-ld-prompt 'demo-prompt state)
 DEMO-PROMPT
!>(include-book "/u/moore/Desktop/new-loop/loop-lemmas")

Summary
Form:  ( INCLUDE-BOOK "/u/moore/Desktop/new-loop/loop-lemmas"
...)
Rules: NIL
Time:  1.16 seconds (prove: 0.00, print: 0.00, other: 1.16)
 "/Users/moore/Desktop/new-loop/loop-lemmas.lisp"
!>(defun$ guard-of-expr (x) (declare (xargs :guard t)) (not (equal x 23)))


ACL2 !>>(DEFUN GUARD-OF-EXPR (X)
               (DECLARE (XARGS :GUARD T))
               (NOT (EQUAL X 23)))

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

Computing the guard conjecture for GUARD-OF-EXPR....

The guard conjecture for GUARD-OF-EXPR is trivial to prove.
GUARD-OF-EXPR is compliant with Common Lisp.

Summary
Form:  ( DEFUN GUARD-OF-EXPR ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
GUARD-OF-EXPR


ACL2 !>>(DEF-WARRANT GUARD-OF-EXPR)

GUARD-OF-EXPR is now warranted, with badge (APPLY$-BADGE T 1 . T).

:WARRANTED

Summary
Form:  ( PROGN (DEFUN GUARD-OF-EXPR ...) ...)
Rules: NIL
Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.02)
Prover steps counted:  686
 :WARRANTED
!>(defun$ expr (x) (declare (xargs :guard (guard-of-expr x))) x)


ACL2 !>>(DEFUN EXPR (X)
               (DECLARE (XARGS :GUARD (GUARD-OF-EXPR X)))
               X)

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

Computing the guard conjecture for EXPR....

The guard conjecture for EXPR is trivial to prove.  EXPR is
compliant with Common Lisp.

Summary
Form:  ( DEFUN EXPR ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
EXPR


ACL2 !>>(DEF-WARRANT EXPR)

EXPR is now warranted, with badge (APPLY$-BADGE T 1 . T).

:WARRANTED

Summary
Form:  ( PROGN (DEFUN EXPR ...) ...)
Rules: NIL
Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.02)
Prover steps counted:  594
 :WARRANTED
!>(defun$ extra-guard-of-expr (x) (declare (xargs :guard t)) (not (equal x 23)))


ACL2 !>>(DEFUN EXTRA-GUARD-OF-EXPR (X)
               (DECLARE (XARGS :GUARD T))
               (NOT (EQUAL X 23)))

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

Computing the guard conjecture for EXTRA-GUARD-OF-EXPR....

The guard conjecture for EXTRA-GUARD-OF-EXPR is trivial to prove.
EXTRA-GUARD-OF-EXPR is compliant with Common Lisp.

Summary
Form:  ( DEFUN EXTRA-GUARD-OF-EXPR ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
EXTRA-GUARD-OF-EXPR


ACL2 !>>(DEF-WARRANT EXTRA-GUARD-OF-EXPR)

EXTRA-GUARD-OF-EXPR is now warranted, with badge 
(APPLY$-BADGE T 1 . T).

:WARRANTED

Summary
Form:  ( PROGN (DEFUN EXTRA-GUARD-OF-EXPR ...) ...)
Rules: NIL
Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.02)
Prover steps counted:  686
 :WARRANTED
!>(defun$ spec (x) (declare (xargs :guard t)) (not (equal x 23)))


ACL2 !>>(DEFUN SPEC (X)
               (DECLARE (XARGS :GUARD T))
               (NOT (EQUAL X 23)))

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

Computing the guard conjecture for SPEC....

The guard conjecture for SPEC is trivial to prove.  SPEC is
compliant with Common Lisp.

Summary
Form:  ( DEFUN SPEC ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SPEC


ACL2 !>>(DEF-WARRANT SPEC)

SPEC is now warranted, with badge (APPLY$-BADGE T 1 . T).

:WARRANTED

Summary
Form:  ( PROGN (DEFUN SPEC ...) ...)
Rules: NIL
Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.02)
Prover steps counted:  686
 :WARRANTED
!>(defun$ guard-of-main (lst) (declare (xargs :guard t)) (not (equal lst nil)))


ACL2 !>>(DEFUN GUARD-OF-MAIN (LST)
               (DECLARE (XARGS :GUARD T))
               (NOT (EQUAL LST NIL)))

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

Computing the guard conjecture for GUARD-OF-MAIN....

The guard conjecture for GUARD-OF-MAIN is trivial to prove.
GUARD-OF-MAIN is compliant with Common Lisp.

Summary
Form:  ( DEFUN GUARD-OF-MAIN ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
GUARD-OF-MAIN


ACL2 !>>(DEF-WARRANT GUARD-OF-MAIN)

GUARD-OF-MAIN is now warranted, with badge (APPLY$-BADGE T 1 . T).

:WARRANTED

Summary
Form:  ( PROGN (DEFUN GUARD-OF-MAIN ...) ...)
Rules: NIL
Time:  0.02 seconds (prove: 0.01, print: 0.00, other: 0.02)
Prover steps counted:  690
 :WARRANTED
!>(----                        This line = max ACL2 length                  ----)

!>(----                        This line = max ACL2 length                  ----)

!>(---- start demo here ----)

!>(---- Recall apply$ and scions (aka mapping functions) ----)

!>(defun$ sum (fn lst)
   (declare (xargs :guard
                   (and (apply$-guard fn '(nil))
                        (true-listp lst))))
   (if (endp lst)
       0
       (+ (fix (apply$ fn (list (car lst))))
          (sum fn (cdr lst)))))


ACL2 !>>(DEFUN SUM (FN LST)
               (DECLARE (XARGS :GUARD (AND (APPLY$-GUARD FN '(NIL))
                                           (TRUE-LISTP LST))))
               (IF (ENDP LST)
                   0
                   (+ (FIX (APPLY$ FN (LIST (CAR LST))))
                      (SUM FN (CDR LST)))))

The admission of SUM is trivial, using the relation O< (which
is known to be well-founded on the domain recognized by O-P)
and the measure (ACL2-COUNT LST).  We observe that the type
of SUM is described by the theorem (ACL2-NUMBERP (SUM FN LST)).
We used primitive type reasoning and the :type-prescription
rule FIX.

Computing the guard conjecture for SUM....

The non-trivial part of the guard conjecture for SUM, given
primitive type reasoning and the :type-prescription rules FIX
and SUM, is

Goal
(IMPLIES (AND (APPLY$-GUARD FN '(NIL))
              (TRUE-LISTP LST)
              (NOT (ENDP LST)))
         (APPLY$-GUARD FN (LIST (CAR LST)))).
Goal'

Q.E.D.

That completes the proof of the guard theorem for SUM.  SUM
is compliant with Common Lisp.

Summary
Form:  ( DEFUN SUM ...)
Rules: ((:DEFINITION APPLY$-GUARD)
        (:DEFINITION APPLY$-LAMBDA-GUARD)
        (:DEFINITION ENDP)
        (:DEFINITION LEN)
        (:DEFINITION LENGTH)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART LENGTH)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART TRUE-LISTP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CDR-CONS)
        (:REWRITE EQUAL-LEN-1)
        (:TYPE-PRESCRIPTION FIX)
        (:TYPE-PRESCRIPTION SUM))
Time:  0.04 seconds (prove: 0.01, print: 0.00, other: 0.03)
Prover steps counted:  216
SUM


ACL2 !>>(DEF-WARRANT SUM)

SUM is now warranted, with badge (APPLY$-BADGE T 2 :FN NIL).

:WARRANTED

Summary
Form:  ( PROGN (DEFUN SUM ...) ...)
Rules: NIL
Time:  0.11 seconds (prove: 0.04, print: 0.00, other: 0.07)
Prover steps counted:  4993
 :WARRANTED
!>(sum (lambda$ (x) (* x x)) '(1 2 3))
14
!>(thm
   (equal (sum fn (append a b))
          (+ (sum fn a)
             (sum fn b))))

*1 (the initial Goal, a key checkpoint) is pushed for proof
by induction.

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

We will induct according to a scheme suggested by (SUM FN A),
but modified to accommodate (APPEND A B).  These suggestions
were produced using the :induction rules BINARY-APPEND and SUM.
If we let (:P A B FN) denote *1 above then the induction scheme
we'll use is
(AND (IMPLIES (AND (NOT (ENDP A)) (:P (CDR A) B FN))
              (:P A B FN))
     (IMPLIES (ENDP A) (:P A B FN))).
This induction is justified by the same argument used to admit
SUM.  When applied to the goal at hand the above induction scheme
produces two nontautological subgoals.
Subgoal *1/2
Subgoal *1/2'

Splitter note (see :DOC splitter) for Subgoal *1/2' (2 subgoals).
  if-intro: ((:DEFINITION FIX) (:DEFINITION SUM))

Subgoal *1/2.2
Subgoal *1/2.1
Subgoal *1/1
Subgoal *1/1'

*1 is COMPLETED!
Thus key checkpoint Goal is COMPLETED!

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION FIX)
        (:DEFINITION NOT)
        (:DEFINITION SUM)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION BINARY-APPEND)
        (:INDUCTION SUM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE UNICITY-OF-0)
        (:TYPE-PRESCRIPTION SUM))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION FIX) (:DEFINITION SUM))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  949

Proof succeeded.
!>(defun nats (n)
   (if (zp n)
       nil
       (cons n (nats (- n 1)))))

The admission of NATS is trivial, using the relation O< (which
is known to be well-founded on the domain recognized by O-P)
and the measure (ACL2-COUNT N).  We observe that the type of
NATS is described by the theorem (TRUE-LISTP (NATS N)).  We
used primitive type reasoning.

Summary
Form:  ( DEFUN NATS ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 NATS
!>(nats 5)
(5 4 3 2 1)
!>(include-book "arithmetic-5/top" :dir :system)

ACL2 Observation in NON-LINEAR-ARITHMETIC:  To turn on non-
linear arithmetic, execute :

(SET-DEFAULT-HINTS
     '((NONLINEARP-DEFAULT-HINT STABLE-UNDER-SIMPLIFICATIONP
                                HIST PSPV)))

or :

(SET-DEFAULT-HINTS
 '((NONLINEARP-DEFAULT-HINT++ ID
                              STABLE-UNDER-SIMPLIFICATIONP HIST NIL)))

See the README for more about non-linear arithmetic and general
information about using this library.

Summary
Form:  ( INCLUDE-BOOK "arithmetic-5/top" ...)
Rules: NIL
Time:  0.91 seconds (prove: 0.00, print: 0.00, other: 0.91)
 "/Users/moore/work/acl2/v81c/books/arithmetic-5/top.lisp"
!>(thm
   (implies (natp n)
            (equal (sum (lambda$ (x) (* x x))
                        (nats n))
                   (/ (* n (+ n 1) (+ (* 2 n) 1)) 6))))
Goal'
Goal''

([ A key checkpoint:

Goal''
(IMPLIES (AND (INTEGERP N)
              (<= 0 N)
              (NOT (EQUAL N 0)))
         (EQUAL (+ (* 1/6 N)
                   (* 1/2 (EXPT N 2))
                   (* 1/3 (EXPT N 3)))
                (SUM (LAMBDA$ (X) (* X X)) (NATS N))))

*1 (Goal'') is pushed for proof by induction.

])

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

We will induct according to a scheme suggested by (NATS N).
This suggestion was produced using the :induction rule NATS.
If we let (:P N) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ZP N)) (:P (+ -1 N)))
              (:P N))
     (IMPLIES (ZP N) (:P N))).
This induction is justified by the same argument used to admit
NATS.  When applied to the goal at hand the above induction
scheme produces five nontautological subgoals.
Subgoal *1/5
Subgoal *1/4
Subgoal *1/3
Subgoal *1/2
Subgoal *1/1

*1 is COMPLETED!
Thus key checkpoint Goal'' is COMPLETED!

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION ASSOC-EQUAL)
        (:DEFINITION EV$-LIST-DEF)
        (:DEFINITION FIX)
        (:DEFINITION NATP)
        (:DEFINITION NATS)
        (:DEFINITION PAIRLIS$)
        (:DEFINITION RETURN-LAST)
        (:DEFINITION SUITABLY-TAMEP-LISTP)
        (:DEFINITION SUM)
        (:DEFINITION SYNP)
        (:DEFINITION TAMEP)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART APPLY$-PRIMP)
        (:EXECUTABLE-COUNTERPART BADGE-PRIM)
        (:EXECUTABLE-COUNTERPART BINARY-*)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONS)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART EXPT)
        (:EXECUTABLE-COUNTERPART INTEGERP)
        (:EXECUTABLE-COUNTERPART NATS)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART PAIRLIS$)
        (:EXECUTABLE-COUNTERPART SUM)
        (:EXECUTABLE-COUNTERPART SYMBOLP)
        (:EXECUTABLE-COUNTERPART UNARY--)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION NATS)
        (:META APPLY$-PRIM-META-FN-CORRECT)
        (:REWRITE |(* (* x y) z)|)
        (:REWRITE |(* -1 x)|)
        (:REWRITE |(* 0 x)|)
        (:REWRITE |(* 1 x)|)
        (:REWRITE |(* a (/ a) b)|)
        (:REWRITE |(* c (* d x))|)
        (:REWRITE |(* x (+ y z))|)
        (:REWRITE |(* x (- y))|)
        (:REWRITE |(* x (expt x n))|)
        (:REWRITE |(* x (if a b c))|)
        (:REWRITE |(* x x)|)
        (:REWRITE |(* y (* x z))|)
        (:REWRITE |(* y x)|)
        (:REWRITE |(+ (* c x) (* d x))|)
        (:REWRITE |(+ (+ x y) z)|)
        (:REWRITE |(+ (- x) (* c x))|)
        (:REWRITE |(+ 0 x)|)
        (:REWRITE |(+ c (+ d x))|)
        (:REWRITE |(+ x (- x))|)
        (:REWRITE |(+ x (if a b c))|)
        (:REWRITE |(+ y (+ x z))|)
        (:REWRITE |(+ y x)|)
        (:REWRITE |(- (* c x))|)
        (:REWRITE |(equal (if a b c) x)|)
        (:REWRITE |(expt (+ x y) 2)|)
        (:REWRITE |(expt (+ x y) 3)|)
        (:REWRITE APPLY$-PRIMITIVE)
        (:REWRITE APPLY$-PRIMP-BADGE)
        (:REWRITE BETA-REDUCTION)
        (:REWRITE BUBBLE-DOWN-*-MATCH-1)
        (:REWRITE BUBBLE-DOWN-+-BUBBLE-DOWN)
        (:REWRITE BUBBLE-DOWN-+-MATCH-3)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE DEFAULT-TIMES-1)
        (:REWRITE DEFAULT-TIMES-2)
        (:REWRITE EV$-OPENER)
        (:REWRITE NORMALIZE-ADDENDS)
        (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS)
        (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL)
        (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL)
        (:REWRITE SIMPLIFY-SUMS-EQUAL)
        (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-INTEGERP-BASE)
        (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NONNEGATIVE-BASE)
        (:TYPE-PRESCRIPTION
             EXPT-TYPE-PRESCRIPTION-NONPOSITIVE-BASE-EVEN-EXPONENT)
        (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-POSITIVE-BASE)
        (:TYPE-PRESCRIPTION NATS)
        (:TYPE-PRESCRIPTION SUM))
Time:  0.15 seconds (prove: 0.15, print: 0.00, other: 0.00)
Prover steps counted:  9032

Proof succeeded.
!>(u)
 L         8:x(DEFUN NATS (N) ...)
!>(---- Common Lisp provides a very flexible LOOP stmt. ----)

!>(value :q)

Exiting the ACL2 read-eval-print loop.  To re-enter, execute
(LP).
? (loop for x in '(1 2 3) SUM (* x x))
14
? (loop for x in '(1 2 3) COLLECT (* x x))
(1 4 9)
? (loop for x in '(1 2 3) ALWAYS (< x 100))
T
? (loop for x in '(1 2 3) APPEND (list '--> x '<--))
(--> 1 <-- --> 2 <-- --> 3 <--)
? (loop for x ON '(1 2 3) collect x)
((1 2 3) (2 3) (3))
? (loop for x ON '(1 2 3 . 4) collect x)
((1 2 3 . 4) (2 3 . 4) (3 . 4))
? (loop for x FROM 1 TO 10 collect x)
(1 2 3 4 5 6 7 8 9 10)
? (loop for x FROM 1 TO 10 BY 2 collect x)
(1 3 5 7 9)
? (loop for x from 1 to 10
        WHEN (evenp x)
        collect x)
(2 4 6 8 10)
? (loop for x from 1 to 10
        UNTIL (> x 7)
        collect x)
(1 2 3 4 5 6 7)
? (loop for x from 1
        UNTIL (> x 7)
        collect x)
(1 2 3 4 5 6 7)
? (loop for x from 1 to 10
      AS  day in '(mon tue wed thu fri)
      collect (cons day x))
((MON . 1) (TUE . 2) (WED . 3) (THU . 4) (FRI . 5))
? (lp)

ACL2 Version 8.1.  Level 1.  Cbd "/Users/moore/".
System books directory "/Users/moore/work/acl2/v81c/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

!>(----

Semantics of ACL2 LOOP$

(LOOP$ FOR x IN lst sum expr)
==>
(sum$ (LAMBDA$ (x) expr) lst)

----)

!>(---- What about speed? ----)

!>(defconst *m* (nats 1000000))

Summary
Form:  ( DEFCONST *M* ...)
Rules: NIL
Time:  0.15 seconds (prove: 0.00, print: 0.00, other: 0.15)
 *M*
!>:args sum

Function         SUM
Formals:         (FN LST)
Signature:       (SUM * *)
                 => *
Guard:           (AND (APPLY$-GUARD FN '(NIL))
                      (TRUE-LISTP LST))
Guards Verified: T
Defun-Mode:      :logic
Type:            (ACL2-NUMBERP (SUM FN LST))

 SUM
!>:pe apply$-guard
 V     -1145  (DEFUN APPLY$-GUARD (FN ARGS)
                     (DECLARE (XARGS :GUARD T :MODE :LOGIC))
                     (IF (ATOM FN)
                         (TRUE-LISTP ARGS)
                         (APPLY$-LAMBDA-GUARD FN ARGS)))
!>(time$ (sum  (lambda$ (x) (* x x)) *m*))
; (EV-REC *RETURN-LAST-ARG3* ...) took 
; 2.56 seconds realtime, 2.56 seconds runtime
; (144,009,104 bytes allocated).
333333833333500000
!>(---- sum$ is just a faster version of sum. -----)

!>(time$ (sum$ (lambda$ (x) (* x x)) *m*))
; (EV-REC *RETURN-LAST-ARG3* ...) took 
; 1.44 seconds realtime, 1.44 seconds runtime
; (144,000,032 bytes allocated).
333333833333500000
!>(value :q)

Exiting the ACL2 read-eval-print loop.  To re-enter, execute
(LP).
? (time (loop for x in *m* sum (* x x)))
(LOOP FOR X IN *M* SUM (* X X))
took 4,129 microseconds (0.004129 seconds) to run.
During that period, and with 8 available CPU cores,
     4,094 microseconds (0.004094 seconds) were spent in user mode
       136 microseconds (0.000136 seconds) were spent in system mode
333333833333500000
? (time (loop for x of-type integer in *m* sum (* x x)))
(LOOP FOR X OF-TYPE INTEGER IN *M* SUM (* X X))
took 4,051 microseconds (0.004051 seconds) to run.
During that period, and with 8 available CPU cores,
     3,973 microseconds (0.003973 seconds) were spent in user mode
        35 microseconds (0.000035 seconds) were spent in system mode
333333833333500000
? (defun bar nil (loop for x of-type integer in *m* sum (* x x)))
BAR
? (time (bar))
(BAR)
took 4,133 microseconds (0.004133 seconds) to run.
During that period, and with 8 available CPU cores,
     4,087 microseconds (0.004087 seconds) were spent in user mode
        23 microseconds (0.000023 seconds) were spent in system mode
333333833333500000
? (lp)

ACL2 Version 8.1.  Level 1.  Cbd "/Users/moore/".
System books directory "/Users/moore/work/acl2/v81c/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

!>(time$ (loop$ for x in *m* sum (* x x)))
; (EV-REC *RETURN-LAST-ARG3* ...) took 
; 1.37 seconds realtime, 1.37 seconds runtime
; (144,009,296 bytes allocated).
333333833333500000
!>(time$ (loop$ for x of-type integer in *m*
               sum (* x x)))
; (EV-REC *RETURN-LAST-ARG3* ...) took 
; 0.11 seconds realtime, 0.11 seconds runtime
; (16,039,568 bytes allocated).
333333833333500000
!>(defun foo (lst)
         (declare (xargs :guard (integer-listp lst)))
         (loop$ for x of-type integer in lst
                sum (* x x)))

Since FOO is non-recursive, its admission is trivial.  We observe
that the type of FOO is described by the theorem 
(ACL2-NUMBERP (FOO LST)).  We used the :type-prescription rule
SUM$.

Computing the guard conjecture for FOO....

The non-trivial part of the guard conjecture for FOO, given
the :executable-counterpart of APPLY$-GUARD, the :forward-chaining
rules ACL2-NUMBER-LISTP-FORWARD-TO-TRUE-LISTP, 
INTEGER-LISTP-FORWARD-TO-RATIONAL-LISTP and 
RATIONAL-LISTP-FORWARD-TO-ACL2-NUMBER-LISTP and the :type-prescription
rules ACL2-NUMBER-LISTP, INTEGER-LISTP and RATIONAL-LISTP, is

Goal
(AND
 (IMPLIES
    (AND (INTEGER-LISTP LST)
         (< (MEMPOS NEWV LST) (LEN LST)))
    (ACL2-NUMBERP (APPLY$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (* X X))
                          (LIST NEWV))))
 (IMPLIES (AND (INTEGER-LISTP LST)
               (< (MEMPOS NEWV LST) (LEN LST)))
          (INTEGERP NEWV))).
Subgoal 2
Subgoal 1

Q.E.D.

That completes the proof of the guard theorem for FOO.  FOO
is compliant with Common Lisp.

Summary
Form:  ( DEFUN FOO ...)
Rules: ((:DEFINITION ASSOC-EQUAL)
        (:DEFINITION EV$-LIST-DEF)
        (:DEFINITION NOT)
        (:DEFINITION PAIRLIS$)
        (:DEFINITION RETURN-LAST)
        (:DEFINITION SUITABLY-TAMEP-LISTP)
        (:DEFINITION SYNP)
        (:DEFINITION TAMEP)
        (:EXECUTABLE-COUNTERPART APPLY$-GUARD)
        (:EXECUTABLE-COUNTERPART APPLY$-PRIMP)
        (:EXECUTABLE-COUNTERPART BADGE-PRIM)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONS)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART PAIRLIS$)
        (:EXECUTABLE-COUNTERPART SYMBOLP)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING ACL2-NUMBER-LISTP-FORWARD-TO-TRUE-LISTP)
        (:FORWARD-CHAINING INTEGER-LISTP-FORWARD-TO-RATIONAL-LISTP)
        (:FORWARD-CHAINING
             RATIONAL-LISTP-FORWARD-TO-ACL2-NUMBER-LISTP)
        (:META APPLY$-PRIM-META-FN-CORRECT)
        (:REWRITE APPLY$-PRIMITIVE)
        (:REWRITE APPLY$-PRIMP-BADGE)
        (:REWRITE BETA-REDUCTION1)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE EV$-OPENER)
        (:REWRITE INTEGER-LISTP-IMPLIES-ALWAYS$-INTEGERP)
        (:REWRITE PLAIN-UQI-INTEGER-LISTP)
        (:TYPE-PRESCRIPTION ACL2-NUMBER-LISTP)
        (:TYPE-PRESCRIPTION INTEGER-LISTP)
        (:TYPE-PRESCRIPTION LEN)
        (:TYPE-PRESCRIPTION RATIONAL-LISTP)
        (:TYPE-PRESCRIPTION SUM$))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  1798
 FOO
!>(time$ (foo *m*))
; (EV-REC *RETURN-LAST-ARG3* ...) took 
; 0.01 seconds realtime, 0.01 seconds runtime
; (16 bytes allocated).
333333833333500000
!>:pe sum$
   d       1  (INCLUDE-BOOK "/u/moore/Desktop/new-loop/loop-lemmas")
              \
              [Included books, outermost to innermost:
               "/Users/moore/Desktop/new-loop/loop-lemmas.lisp"
              ]
              \
>LV            (DEFUN
                 SUM$ (FN LST)
                 (DECLARE (XARGS :GUARD (AND (APPLY$-GUARD FN '(NIL))
                                             (TRUE-LISTP LST))
                                 :VERIFY-GUARDS NIL))
                 (MBE :LOGIC (IF (ENDP LST)
                                 0
                                 (+ (FIX (APPLY$ FN (LIST (CAR LST))))
                                    (SUM$ FN (CDR LST))))
                      :EXEC (SUM$-AC FN LST 0)))
!>(---- "
       test                       seconds  normed
sum at ACL2 top-level               2.95    507.1
sum$ at ACL2 top-level              1.68    288.8 
loop$ at ACL2 top-level             1.55    266.4
loop$ of-type at ACL2 top-level     0.11     18.9
loop$ of-type in guard verif defun  0.01      1.7
loop in raw Common Lisp             0.005850  1.0
loop of-type in raw Common Lisp     0.005817  1.0

" ----)

!>:q

Exiting the ACL2 read-eval-print loop.  To re-enter, execute
(LP).
? (time (integer-listp *m*))
(INTEGER-LISTP *M*)
took 3,730 microseconds (0.003730 seconds) to run.
During that period, and with 8 available CPU cores,
     3,626 microseconds (0.003626 seconds) were spent in user mode
        65 microseconds (0.000065 seconds) were spent in system mode
T
? (lp)

ACL2 Version 8.1.  Level 1.  Cbd "/Users/moore/".
System books directory "/Users/moore/work/acl2/v81c/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

!>(u)
           9:x(DEFCONST *M* ...)
!>(----

Semantics of ACL2 LOOP$

(LOOP$ FOR x IN lst sum expr)
==>
(sum$ (LAMBDA$ (x) expr) lst)

----)

!>(----

(LOOP$ FOR x ON lst sum expr)
==>
(sum$ (LAMBDA$ (x) expr)
      (TAILS lst))

----)

!>(----

(LOOP$ FOR x IN lst
       WHEN test
       sum expr)
==>
(sum$ (LAMBDA$ (x) expr)
      (when$ (LAMBDA$ (x) test) 
             lst))

----)

!>(----

Note that

 (sum$ fn (when$ p lst))
 (sum$ fn (tails lst))
 etc

copy lst.

This means execution in the ACL2 loop will be slower.

But our focus is on execution in guard verified defuns.

----)

!>(----

Unfortunately the guards proved for

(sum$ (LAMBDA$ (x) (expr x)) lst)

are insufficent to guarantee safe execution of

(LOOP$ FOR x IN lst sum (expr x))!

To explain I will use sum instead of sum$ because
guard verification has been changed to support
sum$.

----)

!>(---- 

To explore the guard conjectures generated
for a loop$ I will define a function named MAIN
and watch what happens.

Guard verification will fail but the point is
to see the guard conjectures!

----)

!>(in-theory (disable apply$-guard (apply$-guard)))

Summary
Form:  ( IN-THEORY (DISABLE ...))
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 (:NUMBER-OF-ENABLED-RUNES 5182)
!>(defun main (lst)
    (declare (xargs :guard (guard-of-main lst)))
;   (loop$ for x in lst sum (expr x))
    (sum (lambda$ (x) (expr x))
         lst))


(AND
  (GUARD-OF-EXPR X)
  (IMPLIES (GUARD-OF-MAIN LST)
           (APPLY$-GUARD '(LAMBDA (X)
                                  (RETURN-LAST 'PROGN
                                               '(LAMBDA$ (X) (EXPR X))
                                               (EXPR X)))
                         '(NIL)))
  (IMPLIES (GUARD-OF-MAIN LST)
           (TRUE-LISTP LST))).
Subgoal 3
Subgoal 3'

([ A key checkpoint:

Subgoal 3'
NIL

A goal of NIL, Subgoal 3', has been generated!  Obviously, the
proof attempt has failed.

])


ACL2 Error in ( DEFUN MAIN ...):  The proof of the guard conjecture
for MAIN has failed.  You may wish to avoid specifying a guard,
or to supply option :VERIFY-GUARDS NIL with the :GUARD.  Otherwise,
you may wish to specify :GUARD-DEBUG T; see :DOC verify-guards.



Summary
Form:  ( DEFUN MAIN ...)
Rules: ((:DEFINITION GUARD-OF-EXPR)
        (:DEFINITION GUARD-OF-MAIN)
        (:DEFINITION NOT)
        (:TYPE-PRESCRIPTION SUM))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  73

---
The key checkpoint goal, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---

*** Key checkpoint at the top level
    before generating a goal of NIL (see :DOC nil-goal): ***

Subgoal 3'
NIL

ACL2 Error in ( DEFUN MAIN ...):  The proof of the guard conjecture
for MAIN has failed; see the discussion above about :VERIFY-GUARDS
and :GUARD-DEBUG.  See :DOC failure.

************    FAILED    ************
!>:pe expr
   d       3  (DEFUN$ EXPR (X) ...)
              \
>V             (DEFUN EXPR (X)
                      (DECLARE (XARGS :GUARD (GUARD-OF-EXPR X)))
                      X)
!>(defun main (lst)
    (declare (xargs :guard (guard-of-main lst)))
;   (loop$ for x of-type (satisfies spec) in lst sum (expr x))
    (sum (lambda$ (x)
                  (declare (type (satisfies spec) x))
                  (expr x))
         lst))
(AND
 (IMPLIES
  (GUARD-OF-MAIN LST)
  (APPLY$-GUARD
   '(LAMBDA (X)
            (DECLARE (TYPE (SATISFIES SPEC) X)
                     (XARGS :GUARD (SPEC X) :SPLIT-TYPES T))
            (RETURN-LAST 'PROGN
                         '(LAMBDA$ (X)
                                   (DECLARE (TYPE (SATISFIES SPEC) X))
                                   (EXPR X))
                         (EXPR X)))
   '(NIL)))
 (IMPLIES (GUARD-OF-MAIN LST)
          (TRUE-LISTP LST))
 (IMPLIES (SPEC X) (GUARD-OF-EXPR X))).
Subgoal 2
Subgoal 2'
Subgoal 2''

([ A key checkpoint:

Subgoal 2''
(APPLY$-GUARD
   '(LAMBDA (X)
            (DECLARE (TYPE (SATISFIES SPEC) X)
                     (XARGS :GUARD (SPEC X) :SPLIT-TYPES T))
            (RETURN-LAST 'PROGN
                         '(LAMBDA$ (X)
                                   (DECLARE (TYPE (SATISFIES SPEC) X))
                                   (EXPR X))
                         (EXPR X)))
   '(NIL))

*1 (Subgoal 2'') is pushed for proof by induction.

])
Subgoal 1
Subgoal 1'

([ A key checkpoint:

Subgoal 1'
(TRUE-LISTP LST)

*2 (Subgoal 1') is pushed for proof by induction.

])

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

We will induct according to a scheme suggested by (TRUE-LISTP LST).
This suggestion was produced using the :induction rule TRUE-LISTP.
If we let (:P LST) denote *2 above then the induction scheme
we'll use is
(AND (IMPLIES (NOT (CONSP LST)) (:P LST))
     (IMPLIES (AND (CONSP LST) (:P (CDR LST)))
              (:P LST))).
This induction is justified by the same argument used to admit
TRUE-LISTP.  When applied to the goal at hand the above induction
scheme produces two nontautological subgoals.
Subgoal *2/2
Subgoal *2/2'
Subgoal *2/2''

([ A key checkpoint while proving *2 (descended from Subgoal
1'):

Subgoal *2/2'
(IMPLIES (NOT (CONSP LST)) (NOT LST))

A goal of NIL, Subgoal *2/2'', has been generated!  Obviously,
the proof attempt has failed.

])


ACL2 Error in ( DEFUN MAIN ...):  The proof of the guard conjecture
for MAIN has failed.  You may wish to avoid specifying a guard,
or to supply option :VERIFY-GUARDS NIL with the :GUARD.  Otherwise,
you may wish to specify :GUARD-DEBUG T; see :DOC verify-guards.



Summary
Form:  ( DEFUN MAIN ...)
Rules: ((:DEFINITION GUARD-OF-EXPR)
        (:DEFINITION GUARD-OF-MAIN)
        (:DEFINITION NOT)
        (:DEFINITION SPEC)
        (:DEFINITION TRUE-LISTP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION TRUE-LISTP)
        (:TYPE-PRESCRIPTION SUM))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  195

---
The key checkpoint goals, below, may help you to debug this
failure.  See :DOC failure and see :DOC set-checkpoint-summary-
limit.
---

*** Key checkpoints at the top level: ***

Subgoal 2''
(APPLY$-GUARD
   '(LAMBDA (X)
            (DECLARE (TYPE (SATISFIES SPEC) X)
                     (XARGS :GUARD (SPEC X) :SPLIT-TYPES T))
            (RETURN-LAST 'PROGN
                         '(LAMBDA$ (X)
                                   (DECLARE (TYPE (SATISFIES SPEC) X))
                                   (EXPR X))
                         (EXPR X)))
   '(NIL))

Subgoal 1'
(TRUE-LISTP LST)

*** Key checkpoint under a top-level induction
    before generating a goal of NIL (see :DOC nil-goal): ***

Subgoal *2/2'
(IMPLIES (NOT (CONSP LST)) (NOT LST))

ACL2 Error in ( DEFUN MAIN ...):  The proof of the guard conjecture
for MAIN has failed; see the discussion above about :VERIFY-GUARDS
and :GUARD-DEBUG.  See :DOC failure.

************    FAILED    ************
!>(----
But the loop in raw Lisp might still be unsafe!

(loop for x of-type (satisfies spec) in lst sum (expr x))

(a) We did not prove every x in lst satisfies spec!

(b) We did not prove that for every x in lst (expr x) is a number!

These are not necessary for sum (or sum$) because apply$ will
do the right thing if guards are violated.

----)

!>(----

Now we put the loop$ into MAIN which means guard verification
will see SUM$ not SUM.

Sum$ is treated specially.

----)

!>(defun main (lst)
    (declare (xargs :guard (guard-of-main lst)))
    (loop$ for x of-type (satisfies spec) in lst
           sum (expr x)))
(AND
 (IMPLIES
  (GUARD-OF-MAIN LST)
  (APPLY$-GUARD
    '(LAMBDA (X)
             (DECLARE (TYPE (SATISFIES SPEC) X)
                      (IGNORABLE X)
                      (XARGS :GUARD (SPEC X) :SPLIT-TYPES T))
             (RETURN-LAST 'PROGN
                          '(LAMBDA$ (X)
                                    (DECLARE (TYPE (SATISFIES SPEC) X)
                                             (IGNORABLE X))
                                    (EXPR X))
                          (EXPR X)))
    '(NIL)))
 (IMPLIES (GUARD-OF-MAIN LST)
          (TRUE-LISTP LST))
 (IMPLIES (AND (GUARD-OF-MAIN LST)
               (< (MEMPOS NEWV LST) (LEN LST))) ; = (member newv lst)
          (SPEC NEWV))
 (IMPLIES
  (AND (GUARD-OF-MAIN LST)
       (< (MEMPOS NEWV LST) (LEN LST)))
  (ACL2-NUMBERP
     (APPLY$ (LAMBDA$ (X)
                      (DECLARE (TYPE (SATISFIES SPEC) X)
                               (IGNORABLE X)
                               (XARGS :GUARD (SPEC X) :SPLIT-TYPES T))
                      (EXPR X))
             (LIST NEWV))))
 (IMPLIES (SPEC X) (GUARD-OF-EXPR X))).
Subgoal 4
Subgoal 4'
Subgoal 4''

([ A key checkpoint:

Subgoal 4''
(APPLY$-GUARD
    '(LAMBDA (X)
             (DECLARE (TYPE (SATISFIES SPEC) X)
                      (IGNORABLE X)
                      (XARGS :GUARD (SPEC X) :SPLIT-TYPES T))
             (RETURN-LAST 'PROGN
                          '(LAMBDA$ (X)
                                    (DECLARE (TYPE (SATISFIES SPEC) X)
                                             (IGNORABLE X))
                                    (EXPR X))
                          (EXPR X)))
    '(NIL))

*1 (Subgoal 4'') is pushed for proof by induction.

])
Subgoal 3
Subgoal 3'

([ A key checkpoint:

Subgoal 3'
(TRUE-LISTP LST)

*2 (Subgoal 3') is pushed for proof by induction.

])
Subgoal 2
Subgoal 2'

([ A key checkpoint:

Subgoal 2'
(IMPLIES LST (<= (LEN LST) (MEMPOS 23 LST)))

*3 (Subgoal 2') is pushed for proof by induction.

])
Subgoal 1

Forcing Round 1 is pending (caused first by Subgoal 1).
Subgoal 1'

([ A key checkpoint:

Subgoal 1'
(IMPLIES (AND LST (< (MEMPOS NEWV LST) (LEN LST)))
         (ACL2-NUMBERP NEWV))

*4 (Subgoal 1') is pushed for proof by induction.

])

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

We will induct according to a scheme suggested by (LEN LST),
but modified to accommodate (MEMPOS NEWV LST).  These suggestions
were produced using the :induction rules LEN and MEMPOS.  If
we let (:P LST NEWV) denote *4 above then the induction scheme
we'll use is
(AND (IMPLIES (NOT (CONSP LST))
              (:P LST NEWV))
     (IMPLIES (AND (CONSP LST) (:P (CDR LST) NEWV))
              (:P LST NEWV))).
This induction is justified by the same argument used to admit
LEN.  When applied to the goal at hand the above induction scheme
produces three nontautological subgoals.
Subgoal *4/3
Subgoal *4/2
Subgoal *4/2'
Subgoal *4/2''
Subgoal *4/2'''
Subgoal *4/2'4'
Subgoal *4/2'5'
Subgoal *4/2'6'

([ A key checkpoint while proving *4 (descended from Subgoal
1'):

Subgoal *4/2''
(IMPLIES (AND (CONSP LST)
              (<= (LEN (CDR LST))
                  (MEMPOS (CAR LST) (CDR LST)))
              LST (< 0 (+ 1 (LEN (CDR LST)))))
         (ACL2-NUMBERP (CAR LST)))

*4.1 (Subgoal *4/2'6') is pushed for proof by induction.

])
Subgoal *4/1

Splitter note (see :DOC splitter) for Subgoal *4/1 (2 subgoals).
  if-intro: ((:DEFINITION MEMPOS))

Subgoal *4/1.2
Subgoal *4/1.2'
Subgoal *4/1.2''
Subgoal *4/1.2'''
Subgoal *4/1.2'4'

([ A key checkpoint while proving *4 (descended from Subgoal
1'):

Subgoal *4/1.2'
(IMPLIES (AND (CONSP LST) (NOT (CDR LST)) LST)
         (ACL2-NUMBERP (CAR LST)))

A goal of NIL, Subgoal *4/1.2'4', has been generated!  Obviously,
the proof attempt has failed.

])


ACL2 Error in ( DEFUN MAIN ...):  The proof of the guard conjecture
for MAIN has failed.  You may wish to avoid specifying a guard,
or to supply option :VERIFY-GUARDS NIL with the :GUARD.  Otherwise,
you may wish to specify :GUARD-DEBUG T; see :DOC verify-guards.



Summary
Form:  ( DEFUN MAIN ...)
Rules: ((:DEFINITION ASSOC-EQUAL)
        (:DEFINITION EV$-LIST-DEF)
        (:DEFINITION EXPR)
        (:DEFINITION GUARD-OF-EXPR)
        (:DEFINITION GUARD-OF-MAIN)
        (:DEFINITION LEN)
        (:DEFINITION MEMPOS)
        (:DEFINITION NOT)
        (:DEFINITION PAIRLIS$)
        (:DEFINITION RETURN-LAST)
        (:DEFINITION SPEC)
        (:DEFINITION SUITABLY-TAMEP-LISTP)
        (:DEFINITION TAMEP)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART APPLY$-PRIMP)
        (:EXECUTABLE-COUNTERPART BADGE-PRIM)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONS)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART FORCE)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART PAIRLIS$)
        (:EXECUTABLE-COUNTERPART SYMBOLP)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION LEN)
        (:INDUCTION MEMPOS)
        (:META APPLY$-PRIM-META-FN-CORRECT)
        (:REWRITE APPLY$-EXPR)
        (:REWRITE APPLY$-PRIMITIVE)
        (:REWRITE APPLY$-PRIMP-BADGE)
        (:REWRITE BETA-REDUCTION1)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE EV$-OPENER)
        (:TYPE-PRESCRIPTION LEN)
        (:TYPE-PRESCRIPTION MEMPOS)
        (:TYPE-PRESCRIPTION SUM$))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION MEMPOS))
Time:  0.06 seconds (prove: 0.05, print: 0.01, other: 0.00)
Prover steps counted:  8910

---
The key checkpoint goals, below, may help you to debug this
failure.  See :DOC failure and see :DOC set-checkpoint-summary-
limit.
---

*** Key checkpoints at the top level: ***

Subgoal 4''
(APPLY$-GUARD
    '(LAMBDA (X)
             (DECLARE (TYPE (SATISFIES SPEC) X)
                      (IGNORABLE X)
                      (XARGS :GUARD (SPEC X) :SPLIT-TYPES T))
             (RETURN-LAST 'PROGN
                          '(LAMBDA$ (X)
                                    (DECLARE (TYPE (SATISFIES SPEC) X)
                                             (IGNORABLE X))
                                    (EXPR X))
                          (EXPR X)))
    '(NIL))

Subgoal 3'
(TRUE-LISTP LST)

Subgoal 2'
(IMPLIES LST (<= (LEN LST) (MEMPOS 23 LST)))

Subgoal 1'
(IMPLIES (AND LST (< (MEMPOS NEWV LST) (LEN LST)))
         (ACL2-NUMBERP NEWV))

*** Key checkpoints under a top-level induction
    before generating a goal of NIL (see :DOC nil-goal): ***

Subgoal *4/2''
(IMPLIES (AND (CONSP LST)
              (<= (LEN (CDR LST))
                  (MEMPOS (CAR LST) (CDR LST)))
              LST (< 0 (+ 1 (LEN (CDR LST)))))
         (ACL2-NUMBERP (CAR LST)))

Subgoal *4/1.2'
(IMPLIES (AND (CONSP LST) (NOT (CDR LST)) LST)
         (ACL2-NUMBERP (CAR LST)))

ACL2 Error in ( DEFUN MAIN ...):  The proof of the guard conjecture
for MAIN has failed; see the discussion above about :VERIFY-GUARDS
and :GUARD-DEBUG.  See :DOC failure.

************    FAILED    ************
!>(mempos 'wed '(mon tue wed thu fri))
2
!>(thm
   (iff (< (mempos newv lst) (len lst))
        (member newv lst)))
Goal'
Subgoal 2

([ A key checkpoint:

Subgoal 2
(IMPLIES (<= (LEN LST) (MEMPOS NEWV LST))
         (NOT (MEMBER-EQUAL NEWV LST)))

*1 (Subgoal 2) is pushed for proof by induction.

])
Subgoal 1

([ A key checkpoint:

Subgoal 1
(IMPLIES (< (MEMPOS NEWV LST) (LEN LST))
         (MEMBER-EQUAL NEWV LST))

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

])

Perhaps we can prove *1 by induction.  Three induction schemes
are suggested by this conjecture.  Subsumption reduces that
number to two.  These merge into one derived induction scheme.

We will induct according to a scheme suggested by (LEN LST),
but modified to accommodate (MEMBER-EQUAL NEWV LST).  These
suggestions were produced using the :induction rules LEN, 
MEMBER-EQUAL and MEMPOS.  If we let (:P LST NEWV) denote *1
above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP LST))
              (:P LST NEWV))
     (IMPLIES (AND (CONSP LST) (:P (CDR LST) NEWV))
              (:P LST NEWV))).
This induction is justified by the same argument used to admit
LEN.  When applied to the goal at hand the above induction scheme
produces two nontautological subgoals.
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'

Splitter note (see :DOC splitter) for Subgoal *1/1' (4 subgoals).
  if-intro: ((:DEFINITION MEMPOS))

Subgoal *1/1.4
Subgoal *1/1.3
Subgoal *1/1.2
Subgoal *1/1.1

*1 is COMPLETED!
Thus key checkpoint Goal is COMPLETED!

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION IFF)
        (:DEFINITION LEN)
        (:DEFINITION MEMBER-EQL-EXEC$GUARD-CHECK)
        (:DEFINITION MEMBER-EQUAL)
        (:DEFINITION MEMPOS)
        (:DEFINITION NOT)
        (:DEFINITION RETURN-LAST)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION LEN)
        (:INDUCTION MEMBER-EQUAL)
        (:INDUCTION MEMPOS)
        (:TYPE-PRESCRIPTION MEMBER-EQUAL))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION MEMPOS))
Time:  0.03 seconds (prove: 0.02, print: 0.00, other: 0.00)
Prover steps counted:  3932

Proof succeeded.
!>(----

Fancy Loops 

(loop$ for x in xlst
       as  y in ylst
       sum (expr x y z))

==>

(sum$+ (lambda$ (locals globals)
         (let ((x (car locals))
               (y (cadr locals))
               (z (car globals)))
           (expr x y z)))
       (list z)
       (as (list xlst ylst)))
----)

!>

ACL2 Error in TRANSLAM:  EXPR takes 1 argument but in the call
(EXPR X Y Z) it is given 3 arguments.  The formal parameters
list for EXPR is (X).

!>:translam (lambda$ (locals globals)
		     (let ((x (car locals))
			   (y (cadr locals))
			   (z (car globals)))
		       (list x y z)))

 '(LAMBDA (LOCALS GLOBALS)
          (RETURN-LAST 'PROGN
                       '(LAMBDA$ (LOCALS GLOBALS)
                                 (LET ((X (CAR LOCALS))
                                       (Y (CADR LOCALS))
                                       (Z (CAR GLOBALS)))
                                      (LIST X Y Z)))
                       ((LAMBDA (X Y Z)
                                (CONS X (CONS Y (CONS Z 'NIL))))
                        (CAR LOCALS)
                        (CAR (CDR LOCALS))
                        (CAR GLOBALS))))
!>(----

Fancy Loops 

(loop$ for x in xlst
       as  y in ylst
       sum (expr x y z))

==>

(sum$+ (lambda$ (locals globals)
         (let ((x (car locals))
               (y (cadr locals))
               (z (car globals)))
           (expr x y z)))
       (list z)
       (as (list xlst ylst)))
----)

!>(as (list '(1 2 3 4 5 6 7 8 9 10)
            '(sun mon tue wed thu fri sat)
            '(off on on off on on off)))
((1 SUN OFF)
 (2 MON ON)
 (3 TUE ON)
 (4 WED OFF)
 (5 THU ON)
 (6 FRI ON)
 (7 SAT OFF))
!>(pe 'sum$+)
   d       1  (INCLUDE-BOOK "/u/moore/Desktop/new-loop/loop-lemmas")
              \
              [Included books, outermost to innermost:
               "/Users/moore/Desktop/new-loop/loop-lemmas.lisp"
              ]
              \
>LV            (DEFUN
                SUM$+ (FN GLOBALS LST)
                (DECLARE
                     (XARGS :GUARD (AND (APPLY$-GUARD FN '(NIL NIL))
                                        (TRUE-LISTP GLOBALS)
                                        (TRUE-LIST-LISTP LST))
                            :VERIFY-GUARDS NIL))
                (MBE :LOGIC
                     (IF (ENDP LST)
                         0
                         (+ (FIX (APPLY$ FN (LIST (CAR LST) GLOBALS)))
                            (SUM$+ FN GLOBALS (CDR LST))))
                     :EXEC (SUM$+-AC FN GLOBALS LST 0)))
!>(----

One reason mempos is more helpful than member
is that if newv is in (as (list xlst ylst))
with mempos = k then

(car newv) = (nth k xlst)
(cadr newv) = (nth k ylst)

I.e. (car newv) and (cadr newv) are CORRESPONDING
members of their respective targets not just
members.

----)

!>:pbt 1
   d       1  (INCLUDE-BOOK "/u/moore/Desktop/new-loop/loop-lemmas")
   d       2  (DEFUN$ GUARD-OF-EXPR (X) ...)
   d       3  (DEFUN$ EXPR (X) ...)
   d       4  (DEFUN$ EXTRA-GUARD-OF-EXPR (X) ...)
   d       5  (DEFUN$ SPEC (X) ...)
   d       6  (DEFUN$ GUARD-OF-MAIN (LST) ...)
   d       7  (DEFUN$ SUM (FN LST) ...)
 L         8  (DEFUN NATS (N) ...)
           9  (DEFCONST *M* ...)
          10:x(IN-THEORY (DISABLE APPLY$-GUARD #))
!>:u
           9:x(DEFCONST *M* ...)
!>(defun$ symp (x) (declare (xargs :guard t))
  (if (equal x 23)
      nil
      (symbolp x)))


ACL2 !>>(DEFUN SYMP (X)
               (DECLARE (XARGS :GUARD T))
               (IF (EQUAL X 23) NIL (SYMBOLP X)))

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

Computing the guard conjecture for SYMP....

The guard conjecture for SYMP is trivial to prove.  SYMP is
compliant with Common Lisp.

Summary
Form:  ( DEFUN SYMP ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SYMP


ACL2 !>>(DEF-WARRANT SYMP)

SYMP is now warranted, with badge (APPLY$-BADGE T 1 . T).

:WARRANTED

Summary
Form:  ( PROGN (DEFUN SYMP ...) ...)
Rules: NIL
Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.02)
Prover steps counted:  688
 :WARRANTED
!>(defun$ ssq (x)
  (declare (xargs :guard (symp x)))
  (length (symbol-name x)))


ACL2 !>>(DEFUN SSQ (X)
               (DECLARE (XARGS :GUARD (SYMP X)))
               (LENGTH (SYMBOL-NAME X)))

Since SSQ is non-recursive, its admission is trivial.  We observe
that the type of SSQ is described by the theorem 
(AND (INTEGERP (SSQ X)) (<= 0 (SSQ X))).  We used the :type-
prescription rule LENGTH.

Computing the guard conjecture for SSQ....

The non-trivial part of the guard conjecture for SSQ, given
primitive type reasoning, is

Goal
(IMPLIES (SYMP X) (SYMBOLP X)).

Q.E.D.

That completes the proof of the guard theorem for SSQ.  SSQ
is compliant with Common Lisp.

Summary
Form:  ( DEFUN SSQ ...)
Rules: ((:DEFINITION NOT)
        (:DEFINITION SYMP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION LENGTH))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  19
SSQ


ACL2 !>>(DEF-WARRANT SSQ)

SSQ is now warranted, with badge (APPLY$-BADGE T 1 . T).

:WARRANTED

Summary
Form:  ( PROGN (DEFUN SSQ ...) ...)
Rules: NIL
Time:  0.03 seconds (prove: 0.01, print: 0.00, other: 0.02)
Prover steps counted:  665
 :WARRANTED
!>(defun test (n)

; Best to call this with (<= 10 n) to expect every until/when to have some effect.

  (declare (xargs :guard (natp n)
                  :guard-hints (("Goal" :in-theory (disable as) ; <---- This is important! ***
                                        :do-not-induct t))))
  (list
; SUM
; simple (in/on/from-to-by)
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          sum x)
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          sum (length x))
   (loop$ for x of-type integer from 1 to n sum x)
; ... with until
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          until (equal x 7)
          sum x)
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          until (equal (car x) 7)
          sum (length x))
   (loop$ for x of-type integer
          from 1 to n
          until (equal x 8)
          sum x)
; ... with when
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          when (not (equal x 7))
          sum x)
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          when (not (equal (car x) 7))
          sum (length x))
   (loop$ for x of-type integer
          from 1 to n
          when (not (equal x 7))
          sum x)
; ... with until and when
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          until (equal x 9)
          when (not (equal x 7))
          sum x)
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          until (equal (car x) 9)
          when (not (equal (car x) 7))
          sum (length x))
   (loop$ for x of-type integer
          from 1 to n
          until (equal x 9)
          when (not (equal x 7))
          sum x)

; ALWAYS
; simple (in/on/from-to-by)
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          always (integerp x))
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          always (true-listp x))
   (loop$ for x of-type integer from 1 to n always (integerp x))
; ... with until
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          until (equal x 7)
          always (integerp x))
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          until (equal (car x) 7)
          always (true-listp x))
   (loop$ for x of-type integer
          from 1 to n
          until (equal x 8)
          always (integerp x))
; ... with when -- illegal with always
; ... with until and when -- illegal with always

; COLLECT
; simple (in/on/from-to-by)
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          collect x)
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          collect (length x))
   (loop$ for x of-type integer from 1 to n collect x)
; ... with until
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          until (equal x 7)
          collect x)
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          until (equal (car x) 7)
          collect (length x))
   (loop$ for x of-type integer
          from 1 to n
          until (equal x 8)
          collect x)
; ... with when
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          when (not (equal x 7))
          collect x)
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          when (not (equal (car x) 7))
          collect (length x))
   (loop$ for x of-type integer
          from 1 to n
          when (not (equal x 7))
          collect x)
; ... with until and when
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          until (equal x 9)
          when (not (equal x 7))
          collect x)
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          until (equal (car x) 9)
          when (not (equal (car x) 7))
          collect (length x))
   (loop$ for x of-type integer
          from 1 to n
          until (equal x 9)
          when (not (equal x 7))
          collect x)

; APPEND
; simple (in/on/from-to-by)
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          append (list x))
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          append x)
   (loop$ for x of-type integer from 1 to n append (list x))
; ... with until
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          until (equal x 7)
          append (list x))
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          until (equal (car x) 7)
          append x)
   (loop$ for x of-type integer
          from 1 to n
          until (equal x 8)
          append (list x))
; ... with when
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          when (not (equal x 7))
          append (list x))
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          when (not (equal (car x) 7))
          append x)
   (loop$ for x of-type integer
          from 1 to n
          when (not (equal x 7))
          append (list x))
; ... with until and when
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          until (equal x 9)
          when (not (equal x 7))
          append (list x))
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          until (equal (car x) 9)
          when (not (equal (car x) 7))
          append x)
   (loop$ for x of-type integer
          from 1 to n
          until (equal x 9)
          when (not (equal x 7))
          append (list x))

; -----------------------------------------------------------------
; And now we'll repeat all of that with an AS clause

; SUM
; simple (in/on/from-to-by) 
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          as sym in '(a b c d e f g h i j k l m n o p)
          sum :guard (symbolp sym) (+ x (length (symbol-name sym))))
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          as sym in '(a b c d e f g h i j k l m n o p)
          sum :guard (symbolp sym) (+ (length x) (length (symbol-name sym))))

   (loop$ for x of-type integer from 1 to n
          as sym in '(a b c d e f g h i j k l m n o p)
          sum :guard (symbolp sym) (+ x (length (symbol-name sym))))

; ... with until
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          as sym in '(a b c d e f g h i j k l m n o p)
          until :guard (symp sym) (or (equal x 7) (eq sym '(a b c)))
          sum :guard (symp sym) (+ x (length (symbol-name sym))))

   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          until (equal (car x) 7)
          sum (length x))
   (loop$ for x of-type integer
          from 1 to n
          until (equal x 8)
          sum x)

; ... with when
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          as rattail of-type (and (satisfies rational-listp) (satisfies identity))
             on (make-list n :initial-element 1/2)
          when (and (<= x 6) (<= (car rattail) 7))
          sum (+ x (length rattail)))
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          as rattail of-type (and (satisfies rational-listp) (satisfies identity))
             on (make-list n :initial-element 1/2)
          when (or (<= (length x) 6) (<= (car rattail) 7))
          sum (+ (length x) (car rattail)))
   (loop$ for x of-type integer
          from 1 to n
          as rattail of-type (and (satisfies rational-listp) (satisfies identity))
             on (make-list n :initial-element 1/2)
          when (or (<= x 6) (<= (car rattail) 7))
          sum (+ x (car rattail)))

; ... with until and when
   (loop$ for x of-type integer in (make-list n :initial-element 1)
          as y of-type rational in (make-list n :initial-element 1)
          until (equal x 9)
          when (not (equal y 7))
          sum x)
   (loop$ for x of-type (and (satisfies rational-listp) (satisfies identity))
              on (make-list n :initial-element 1)
          as
          y of-type (and (satisfies rational-listp) (satisfies identity))
             on (make-list n :initial-element 1/3)
          until (equal (car x) 9)
          when (not (equal (car x) 1/3))
          sum (+ (length x) (car y)))
   (loop$ for x of-type integer from 1 to n
          as y of-type rational in (make-list n :initial-element 1)
          until (equal x 9)
          when (not (equal y 7))
          sum x)

; ALWAYS
; simple (in/on/from-to-by) 
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          as sym in '(a b c d e f g h i j k l m n o p)
          always :guard (symbolp sym) (< (+ x (length (symbol-name sym))) 100))
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          as sym in '(a b c d e f g h i j k l m n o p)
          always :guard (symbolp sym) (< (+ (length x) (length (symbol-name sym))) 100))

   (loop$ for x of-type integer from 1 to n
          as sym in '(a b c d e f g h i j k l m n o p)
          always :guard (symbolp sym) (< (+ x (length (symbol-name sym))) 100))

; ... with until
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          as sym in '(a b c d e f g h i j k l m n o p)
          until :guard (symp sym) (or (equal x 7) (eq sym '(a b c)))
          always :guard (symp sym) (< (+ x (length (symbol-name sym))) 100))

   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          until (equal (car x) 7)
          always (< (length x) 100))
   (loop$ for x of-type integer
          from 1 to n
          until (equal x 8)
          always (< x 100))

; ... with when -- illegal with always
; ... with until and when -- illegal with always

; COLLECT
; simple (in/on/from-to-by) 
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          as sym in '(a b c d e f g h i j k l m n o p)
          collect :guard (symbolp sym) (+ x (length (symbol-name sym))))
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          as sym in '(a b c d e f g h i j k l m n o p)
          collect :guard (symbolp sym) (+ (length x) (length (symbol-name sym))))

   (loop$ for x of-type integer from 1 to n
          as sym in '(a b c d e f g h i j k l m n o p)
          collect :guard (symbolp sym) (+ x (length (symbol-name sym))))

; ... with until
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          as sym in '(a b c d e f g h i j k l m n o p)
          until :guard (symp sym) (or (equal x 7) (eq sym '(a b c)))
          collect :guard (symp sym) (+ x (length (symbol-name sym))))

   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          until (equal (car x) 7)
          collect (length x))
   (loop$ for x of-type integer
          from 1 to n
          until (equal x 8)
          collect x)

; ... with when
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          as rattail of-type (and (satisfies rational-listp) (satisfies identity))
             on (make-list n :initial-element 1/2)
          when (and (<= x 6) (<= (car rattail) 7))
          collect (+ x (length rattail)))
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          as rattail of-type (and (satisfies rational-listp) (satisfies identity))
             on (make-list n :initial-element 1/2)
          when (or (<= (length x) 6) (<= (car rattail) 7))
          collect (+ (length x) (car rattail)))
   (loop$ for x of-type integer
          from 1 to n
          as rattail of-type (and (satisfies rational-listp) (satisfies identity))
             on (make-list n :initial-element 1/2)
          when (or (<= x 6) (<= (car rattail) 7))
          collect (+ x (car rattail)))

; ... with until and when
   (loop$ for x of-type integer in (make-list n :initial-element 1)
          as y of-type rational in (make-list n :initial-element 1)
          until (equal x 9)
          when (not (equal y 7))
          collect x)
   (loop$ for x of-type (and (satisfies rational-listp) (satisfies identity))
              on (make-list n :initial-element 1)
          as
          y of-type (and (satisfies rational-listp) (satisfies identity))
             on (make-list n :initial-element 1/3)
          until (equal (car x) 9)
          when (not (equal (car x) 1/3))
          collect (+ (length x) (car y)))
   (loop$ for x of-type integer from 1 to n
          as y of-type rational in (make-list n :initial-element 1)
          until (equal x 9)
          when (not (equal y 7))
          collect x)


; APPEND
; simple (in/on/from-to-by) 
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          as sym in '(a b c d e f g h i j k l m n o p)
          append :guard (symbolp sym) (make-list-ac 3 (+ x (length (symbol-name sym))) nil))
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          as sym in '(a b c d e f g h i j k l m n o p)
          append :guard (symbolp sym) (make-list-ac 3 (+ (length x) (length (symbol-name sym))) nil))

   (loop$ for x of-type integer from 1 to n
          as sym in '(a b c d e f g h i j k l m n o p)
          append :guard (symbolp sym) (make-list-ac 3 (+ x (length (symbol-name sym))) nil))

; ... with until
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          as sym in '(a b c d e f g h i j k l m n o p)
          until :guard (symp sym) (or (equal x 7) (eq sym '(a b c)))
          append :guard (symp sym) (make-list-ac 3 (+ x (length (symbol-name sym))) nil))

   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          until (equal (car x) 7)
          append x)
   (loop$ for x of-type integer
          from 1 to n
          until (equal x 8)
          append (list x))

; ... with when
   (loop$ for x of-type integer
          in (make-list n :initial-element 1)
          as rattail of-type (and (satisfies rational-listp) (satisfies identity))
             on (make-list n :initial-element 1/2)
          when (and (<= x 6) (<= (car rattail) 7))
          append (cons x rattail))
   (loop$ for x of-type (satisfies true-listp)
          on (make-list n :initial-element 1)
          as rattail of-type (and (satisfies rational-listp) (satisfies identity))
             on (make-list n :initial-element 1/2)
          when (or (<= (length x) 6) (<= (car rattail) 7))
          append (append x rattail))
   (loop$ for x of-type integer
          from 1 to n
          as rattail of-type (and (satisfies rational-listp) (satisfies identity))
             on (make-list n :initial-element 1/2)
          when (or (<= x 6) (<= (car rattail) 7))
          append (cons x rattail))

; ... with until and when
   (loop$ for x of-type integer in (make-list n :initial-element 1)
          as y of-type rational in (make-list n :initial-element 1)
          until (equal x 9)
          when (not (equal y 7))
          append (list x))
   (loop$ for x of-type (and (satisfies rational-listp) (satisfies identity))
              on (make-list n :initial-element 1)
          as
          y of-type (and (satisfies rational-listp) (satisfies identity))
             on (make-list n :initial-element 1/3)
          until (equal (car x) 9)
          when (not (equal (car x) 1/3))
          append (append x y))
   (loop$ for x of-type integer from 1 to n
          as y of-type rational in (make-list n :initial-element 1)
          until (equal x 9)
          when (not (equal y 7))
          append (list x y))

; And finally, a global variable

   (loop$ for x of-type integer from 1 to n
          as y of-type rational in (make-list n :initial-element 1)
          until (equal x 9)
          when (not (equal y 7))
          append :guard (rationalp n) (list x y (+ 1 n)))

   ))

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

Computing the guard conjecture for TEST....

The non-trivial part of the guard conjecture for TEST, given
the :compound-recognizer rule NATP-COMPOUND-RECOGNIZER, the
:executable-counterparts of APPLY$-GUARD, CONS, EQUAL, LEN and
TRUE-LISTP, primitive type reasoning and the :type-prescription
rules FROM-TO-BY, LENGTH, TAILS, UNTIL$ and WHEN$, is

Goal
(AND
 (IMPLIES
      (NATP N)
      (TRUE-LIST-LISTP (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                                 (TAILS (MAKE-LIST-AC N 1/2 NIL))))))
 (IMPLIES (NATP N)
          (TRUE-LIST-LISTP (LIST (FROM-TO-BY 1 N 1)
                                 (MAKE-LIST-AC N 1 NIL))))
 (IMPLIES
  (NATP N)
  (TRUE-LIST-LISTP
     (UNTIL$+
          (LAMBDA$ (LOCALS GLOBALS)
                   (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                               (EQUAL (LEN LOCALS) 2)
                                               (TRUE-LISTP GLOBALS)
                                               (EQUAL (LEN GLOBALS) 0)
                                               (INTEGERP (CAR LOCALS))
                                               (SYMP (CADR LOCALS)))
                                   :SPLIT-TYPES T)
                            (IGNORE GLOBALS))
                   (LET ((X (CAR LOCALS)) (SYM (CADR LOCALS)))
                        (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (OR (EQUAL X 7) (EQ SYM '(A B C))))))
          NIL
          (AS (CONS (MAKE-LIST-AC N 1 NIL)
                    '((A B C D E F G H I J K L M N O P)))))))
 (IMPLIES
  (NATP N)
  (TRUE-LIST-LISTP
   (WHEN$+
    (LAMBDA$
     (LOCALS GLOBALS)
     (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                 (EQUAL (LEN LOCALS) 2)
                                 (TRUE-LISTP GLOBALS)
                                 (EQUAL (LEN GLOBALS) 0)
                                 (INTEGERP (CAR LOCALS))
                                 (RATIONAL-LISTP (CADR LOCALS))
                                 (IDENTITY (CADR LOCALS)))
                     :SPLIT-TYPES T)
              (IGNORE GLOBALS))
     (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                         '(INTEGERP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (AND (<= X 6) (<= (CAR RATTAIL) 7)))))
    NIL
    (AS (LIST (MAKE-LIST-AC N 1 NIL)
              (TAILS (MAKE-LIST-AC N 1/2 NIL)))))))
 (IMPLIES (NATP N)
          (TRUE-LIST-LISTP (LIST (MAKE-LIST-AC N 1 NIL)
                                 (MAKE-LIST-AC N 1 NIL))))
 (IMPLIES (NATP N)
          (TRUE-LISTP (MAKE-LIST-AC N 1 NIL)))
 (IMPLIES
      (NATP N)
      (TRUE-LIST-LISTP (AS (LIST (MAKE-LIST-AC N 1 NIL)
                                 (TAILS (MAKE-LIST-AC N 1/2 NIL))))))
 (IMPLIES
   (NATP N)
   (TRUE-LIST-LISTP (AS (CONS (FROM-TO-BY 1 N 1)
                              '((A B C D E F G H I J K L M N O P))))))
 (IMPLIES
  (NATP N)
  (TRUE-LIST-LISTP
   (WHEN$+
    (LAMBDA$
     (LOCALS GLOBALS)
     (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                 (EQUAL (LEN LOCALS) 2)
                                 (TRUE-LISTP GLOBALS)
                                 (EQUAL (LEN GLOBALS) 0)
                                 (TRUE-LISTP (CAR LOCALS))
                                 (RATIONAL-LISTP (CADR LOCALS))
                                 (IDENTITY (CADR LOCALS)))
                     :SPLIT-TYPES T)
              (IGNORE GLOBALS))
     (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (TRUE-LISTP X)
                                         '(TRUE-LISTP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (OR (<= (LENGTH X) 6)
                 (<= (CAR RATTAIL) 7)))))
    NIL
    (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
              (TAILS (MAKE-LIST-AC N 1/2 NIL)))))))
 (IMPLIES
   (NATP N)
   (TRUE-LIST-LISTP (AS (CONS (MAKE-LIST-AC N 1 NIL)
                              '((A B C D E F G H I J K L M N O P))))))
 (IMPLIES (NATP N)
          (TRUE-LIST-LISTP (LIST (FROM-TO-BY 1 N 1)
                                 (TAILS (MAKE-LIST-AC N 1/2 NIL)))))
 (IMPLIES
   (NATP N)
   (TRUE-LIST-LISTP (AS (CONS (TAILS (MAKE-LIST-AC N 1 NIL))
                              '((A B C D E F G H I J K L M N O P))))))
 (IMPLIES (NATP N)
          (TRUE-LIST-LISTP (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                                 (TAILS (MAKE-LIST-AC N 1/3 NIL)))))
 (IMPLIES (NATP N)
          (TRUE-LIST-LISTP (LIST (MAKE-LIST-AC N 1 NIL)
                                 (TAILS (MAKE-LIST-AC N 1/2 NIL)))))
 (IMPLIES
  (NATP N)
  (TRUE-LIST-LISTP
   (UNTIL$+
    (LAMBDA$
     (LOCALS GLOBALS)
     (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                 (EQUAL (LEN LOCALS) 2)
                                 (TRUE-LISTP GLOBALS)
                                 (EQUAL (LEN GLOBALS) 0)
                                 (AND (RATIONAL-LISTP (CAR LOCALS))
                                      (IDENTITY (CAR LOCALS)))
                                 (RATIONAL-LISTP (CADR LOCALS))
                                 (IDENTITY (CADR LOCALS)))
                     :SPLIT-TYPES T)
              (IGNORE GLOBALS))
     (LET
      ((X (CAR LOCALS)) (Y (CADR LOCALS)))
      (PROG2$
        (PROG2$
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP X) (IDENTITY X))
                                 '(IF (RATIONAL-LISTP X)
                                      (IDENTITY X)
                                      'NIL))
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                                 '(IF (RATIONAL-LISTP Y)
                                      (IDENTITY Y)
                                      'NIL)))
        (EQUAL (CAR X) 9))))
    NIL
    (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
              (TAILS (MAKE-LIST-AC N 1/3 NIL)))))))
 (IMPLIES
  (NATP N)
  (TRUE-LIST-LISTP
   (WHEN$+
    (LAMBDA$
     (LOCALS GLOBALS)
     (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                 (EQUAL (LEN LOCALS) 2)
                                 (TRUE-LISTP GLOBALS)
                                 (EQUAL (LEN GLOBALS) 0)
                                 (INTEGERP (CAR LOCALS))
                                 (RATIONAL-LISTP (CADR LOCALS))
                                 (IDENTITY (CADR LOCALS)))
                     :SPLIT-TYPES T)
              (IGNORE GLOBALS))
     (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                         '(INTEGERP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (OR (<= X 6) (<= (CAR RATTAIL) 7)))))
    NIL
    (AS (LIST (FROM-TO-BY 1 N 1)
              (TAILS (MAKE-LIST-AC N 1/2 NIL)))))))
 (IMPLIES
      (NATP N)
      (TRUE-LIST-LISTP (CONS (FROM-TO-BY 1 N 1)
                             '((A B C D E F G H I J K L M N O P)))))
 (IMPLIES (NATP N)
          (TRUE-LIST-LISTP (AS (LIST (FROM-TO-BY 1 N 1)
                                     (MAKE-LIST-AC N 1 NIL)))))
 (IMPLIES
  (NATP N)
  (TRUE-LIST-LISTP
   (WHEN$+
    (LAMBDA$ (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (NOT (EQUAL Y 7)))))
    NIL
    (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (MAKE-LIST-AC N 1 NIL)
                  (MAKE-LIST-AC N 1 NIL)))))))
 (IMPLIES (NATP N)
          (TRUE-LIST-LISTP (AS (LIST (MAKE-LIST-AC N 1 NIL)
                                     (MAKE-LIST-AC N 1 NIL)))))
 (IMPLIES
      (NATP N)
      (TRUE-LIST-LISTP (CONS (MAKE-LIST-AC N 1 NIL)
                             '((A B C D E F G H I J K L M N O P)))))
 (IMPLIES (NATP N)
          (TRUE-LISTP (MAKE-LIST-AC N 1/2 NIL)))
 (IMPLIES
      (NATP N)
      (TRUE-LIST-LISTP (CONS (TAILS (MAKE-LIST-AC N 1 NIL))
                             '((A B C D E F G H I J K L M N O P)))))
 (IMPLIES
  (NATP N)
  (TRUE-LIST-LISTP
   (WHEN$+
    (LAMBDA$ (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (NOT (EQUAL Y 7)))))
    NIL
    (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (FROM-TO-BY 1 N 1)
                  (MAKE-LIST-AC N 1 NIL)))))))
 (IMPLIES (NATP N)
          (TRUE-LISTP (MAKE-LIST-AC N 1/3 NIL)))
 (IMPLIES
  (NATP N)
  (TRUE-LIST-LISTP
   (WHEN$+
    (LAMBDA$
     (LOCALS GLOBALS)
     (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                 (EQUAL (LEN LOCALS) 2)
                                 (TRUE-LISTP GLOBALS)
                                 (EQUAL (LEN GLOBALS) 0)
                                 (AND (RATIONAL-LISTP (CAR LOCALS))
                                      (IDENTITY (CAR LOCALS)))
                                 (RATIONAL-LISTP (CADR LOCALS))
                                 (IDENTITY (CADR LOCALS)))
                     :SPLIT-TYPES T)
              (IGNORE GLOBALS))
     (LET
      ((X (CAR LOCALS)) (Y (CADR LOCALS)))
      (PROG2$
        (PROG2$
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP X) (IDENTITY X))
                                 '(IF (RATIONAL-LISTP X)
                                      (IDENTITY X)
                                      'NIL))
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                                 '(IF (RATIONAL-LISTP Y)
                                      (IDENTITY Y)
                                      'NIL)))
        (NOT (EQUAL (CAR X) 1/3)))))
    NIL
    (UNTIL$+
     (LAMBDA$
      (LOCALS GLOBALS)
      (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                  (EQUAL (LEN LOCALS) 2)
                                  (TRUE-LISTP GLOBALS)
                                  (EQUAL (LEN GLOBALS) 0)
                                  (AND (RATIONAL-LISTP (CAR LOCALS))
                                       (IDENTITY (CAR LOCALS)))
                                  (RATIONAL-LISTP (CADR LOCALS))
                                  (IDENTITY (CADR LOCALS)))
                      :SPLIT-TYPES T)
               (IGNORE GLOBALS))
      (LET
       ((X (CAR LOCALS)) (Y (CADR LOCALS)))
       (PROG2$
        (PROG2$
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP X) (IDENTITY X))
                                 '(IF (RATIONAL-LISTP X)
                                      (IDENTITY X)
                                      'NIL))
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                                 '(IF (RATIONAL-LISTP Y)
                                      (IDENTITY Y)
                                      'NIL)))
        (EQUAL (CAR X) 9))))
     NIL
     (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
               (TAILS (MAKE-LIST-AC N 1/3 NIL))))))))
 (IMPLIES
  (NATP N)
  (TRUE-LIST-LISTP
   (UNTIL$+
    (LAMBDA$ (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
    NIL
    (AS (LIST (FROM-TO-BY 1 N 1)
              (MAKE-LIST-AC N 1 NIL))))))
 (IMPLIES (NATP N)
          (TRUE-LIST-LISTP (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                                 (TAILS (MAKE-LIST-AC N 1/2 NIL)))))
 (IMPLIES
  (NATP N)
  (TRUE-LIST-LISTP
   (UNTIL$+
    (LAMBDA$ (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
    NIL
    (AS (LIST (MAKE-LIST-AC N 1 NIL)
              (MAKE-LIST-AC N 1 NIL))))))
 (IMPLIES
      (NATP N)
      (TRUE-LIST-LISTP (AS (LIST (FROM-TO-BY 1 N 1)
                                 (TAILS (MAKE-LIST-AC N 1/2 NIL))))))
 (IMPLIES
      (NATP N)
      (TRUE-LIST-LISTP (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                                 (TAILS (MAKE-LIST-AC N 1/3 NIL))))))
 (IMPLIES
    (AND (NATP N)
         (< (MEMPOS NEWV (MAKE-LIST-AC N 1 NIL))
            (LEN (MAKE-LIST-AC N 1 NIL))))
    (ACL2-NUMBERP (APPLY$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   X)
                          (LIST NEWV))))
 (IMPLIES
      (AND (NATP N)
           (< (MEMPOS NEWV (MAKE-LIST-AC N 1 NIL))
              (LEN (MAKE-LIST-AC N 1 NIL))))
      (TRUE-LISTP (APPLY$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (LIST X))
                          (LIST NEWV))))
 (IMPLIES (AND (NATP N)
               (< (MEMPOS NEWV (MAKE-LIST-AC N 1 NIL))
                  (LEN (MAKE-LIST-AC N 1 NIL))))
          (INTEGERP NEWV))
 (IMPLIES
  (AND (NATP N)
       (< (MEMPOS NEWV
                  (UNTIL$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (EQUAL X 8))
                          (FROM-TO-BY 1 N 1)))
          (LEN (UNTIL$ (LAMBDA$ (X)
                                (DECLARE (TYPE INTEGER X)
                                         (IGNORABLE X)
                                         (XARGS :GUARD (INTEGERP X)
                                                :SPLIT-TYPES T))
                                (EQUAL X 8))
                       (FROM-TO-BY 1 N 1)))))
  (TRUE-LISTP (APPLY$ (LAMBDA$ (X)
                               (DECLARE (TYPE INTEGER X)
                                        (IGNORABLE X)
                                        (XARGS :GUARD (INTEGERP X)
                                               :SPLIT-TYPES T))
                               (LIST X))
                      (LIST NEWV))))
 (IMPLIES
  (AND (NATP N)
       (< (MEMPOS NEWV
                  (UNTIL$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (EQUAL X 8))
                          (FROM-TO-BY 1 N 1)))
          (LEN (UNTIL$ (LAMBDA$ (X)
                                (DECLARE (TYPE INTEGER X)
                                         (IGNORABLE X)
                                         (XARGS :GUARD (INTEGERP X)
                                                :SPLIT-TYPES T))
                                (EQUAL X 8))
                       (FROM-TO-BY 1 N 1)))))
  (ACL2-NUMBERP (APPLY$ (LAMBDA$ (X)
                                 (DECLARE (TYPE INTEGER X)
                                          (IGNORABLE X)
                                          (XARGS :GUARD (INTEGERP X)
                                                 :SPLIT-TYPES T))
                                 X)
                        (LIST NEWV))))
 (IMPLIES
  (AND (NATP N)
       (< (MEMPOS NEWV
                  (UNTIL$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (EQUAL X 8))
                          (FROM-TO-BY 1 N 1)))
          (LEN (UNTIL$ (LAMBDA$ (X)
                                (DECLARE (TYPE INTEGER X)
                                         (IGNORABLE X)
                                         (XARGS :GUARD (INTEGERP X)
                                                :SPLIT-TYPES T))
                                (EQUAL X 8))
                       (FROM-TO-BY 1 N 1)))))
  (INTEGERP NEWV))
 (IMPLIES
  (AND (NATP N)
       (< (MEMPOS NEWV
                  (AS (CONS (TAILS (MAKE-LIST-AC N 1 NIL))
                            '((A B C D E F G H I J K L M N O P)))))
          (LEN (AS (CONS (TAILS (MAKE-LIST-AC N 1 NIL))
                         '((A B C D E F G H I J K L M N O P)))))))
  (ACL2-NUMBERP
   (APPLY$
        (LAMBDA$ (LOCALS GLOBALS)
                 (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                             (EQUAL (LEN LOCALS) 2)
                                             (TRUE-LISTP GLOBALS)
                                             (EQUAL (LEN GLOBALS) 0)
                                             (TRUE-LISTP (CAR LOCALS))
                                             (SYMBOLP (CADR LOCALS)))
                                 :SPLIT-TYPES T)
                          (IGNORE GLOBALS))
                 (LET ((X (CAR LOCALS)) (SYM (CADR LOCALS)))
                      (PROG2$ (CHECK-DCL-GUARDIAN (TRUE-LISTP X)
                                                  '(TRUE-LISTP X))
                              (+ (LENGTH X)
                                 (LENGTH (SYMBOL-NAME SYM))))))
        (CONS NEWV '(NIL)))))
 (IMPLIES
  (AND (NATP N)
       (< (MEMPOS NEWV
                  (AS (CONS (TAILS (MAKE-LIST-AC N 1 NIL))
                            '((A B C D E F G H I J K L M N O P)))))
          (LEN (AS (CONS (TAILS (MAKE-LIST-AC N 1 NIL))
                         '((A B C D E F G H I J K L M N O P)))))))
  (TRUE-LISTP
   (APPLY$
    (LAMBDA$ (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (TRUE-LISTP (CAR LOCALS))
                                         (SYMBOLP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (SYM (CADR LOCALS)))
                  (PROG2$ (CHECK-DCL-GUARDIAN (TRUE-LISTP X)
                                              '(TRUE-LISTP X))
                          (MAKE-LIST-AC 3
                                        (+ (LENGTH X)
                                           (LENGTH (SYMBOL-NAME SYM)))
                                        NIL))))
    (CONS NEWV '(NIL)))))
 (IMPLIES
     (AND (NATP N)
          (< (MEMPOS NEWV
                     (AS (CONS (TAILS (MAKE-LIST-AC N 1 NIL))
                               '((A B C D E F G H I J K L M N O P)))))
             (LEN (AS (CONS (TAILS (MAKE-LIST-AC N 1 NIL))
                            '((A B C D E F G H I J K L M N O P)))))))
     (AND (TRUE-LISTP NEWV)
          (EQUAL (LEN NEWV) 2)
          (TRUE-LISTP (CAR NEWV))
          (SYMBOLP (CADR NEWV))))
 (IMPLIES
      (AND (NATP N)
           (< (MEMPOS NEWV
                      (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                                (TAILS (MAKE-LIST-AC N 1/3 NIL)))))
              (LEN (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                             (TAILS (MAKE-LIST-AC N 1/3 NIL)))))))
      (AND (TRUE-LISTP NEWV)
           (EQUAL (LEN NEWV) 2)
           (AND (RATIONAL-LISTP (CAR NEWV))
                (IDENTITY (CAR NEWV)))
           (RATIONAL-LISTP (CADR NEWV))
           (IDENTITY (CADR NEWV))))
 (IMPLIES
   (AND (NATP N)
        (< (MEMPOS NEWV
                   (WHEN$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (NOT (EQUAL X 7)))
                          (MAKE-LIST-AC N 1 NIL)))
           (LEN (WHEN$ (LAMBDA$ (X)
                                (DECLARE (TYPE INTEGER X)
                                         (IGNORABLE X)
                                         (XARGS :GUARD (INTEGERP X)
                                                :SPLIT-TYPES T))
                                (NOT (EQUAL X 7)))
                       (MAKE-LIST-AC N 1 NIL)))))
   (TRUE-LISTP (APPLY$ (LAMBDA$ (X)
                                (DECLARE (TYPE INTEGER X)
                                         (IGNORABLE X)
                                         (XARGS :GUARD (INTEGERP X)
                                                :SPLIT-TYPES T))
                                (LIST X))
                       (LIST NEWV))))
 (IMPLIES
   (AND (NATP N)
        (< (MEMPOS NEWV
                   (WHEN$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (NOT (EQUAL X 7)))
                          (MAKE-LIST-AC N 1 NIL)))
           (LEN (WHEN$ (LAMBDA$ (X)
                                (DECLARE (TYPE INTEGER X)
                                         (IGNORABLE X)
                                         (XARGS :GUARD (INTEGERP X)
                                                :SPLIT-TYPES T))
                                (NOT (EQUAL X 7)))
                       (MAKE-LIST-AC N 1 NIL)))))
   (ACL2-NUMBERP (APPLY$ (LAMBDA$ (X)
                                  (DECLARE (TYPE INTEGER X)
                                           (IGNORABLE X)
                                           (XARGS :GUARD (INTEGERP X)
                                                  :SPLIT-TYPES T))
                                  X)
                         (LIST NEWV))))
 (IMPLIES
   (AND (NATP N)
        (< (MEMPOS NEWV
                   (WHEN$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (NOT (EQUAL X 7)))
                          (MAKE-LIST-AC N 1 NIL)))
           (LEN (WHEN$ (LAMBDA$ (X)
                                (DECLARE (TYPE INTEGER X)
                                         (IGNORABLE X)
                                         (XARGS :GUARD (INTEGERP X)
                                                :SPLIT-TYPES T))
                                (NOT (EQUAL X 7)))
                       (MAKE-LIST-AC N 1 NIL)))))
   (INTEGERP NEWV))
 (IMPLIES
      (AND (NATP N)
           (< (MEMPOS NEWV
                      (AS (LIST (FROM-TO-BY 1 N 1)
                                (TAILS (MAKE-LIST-AC N 1/2 NIL)))))
              (LEN (AS (LIST (FROM-TO-BY 1 N 1)
                             (TAILS (MAKE-LIST-AC N 1/2 NIL)))))))
      (AND (TRUE-LISTP NEWV)
           (EQUAL (LEN NEWV) 2)
           (INTEGERP (CAR NEWV))
           (RATIONAL-LISTP (CADR NEWV))
           (IDENTITY (CADR NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
      NEWV
      (WHEN$ (LAMBDA$ (X)
                      (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                               (IGNORABLE X)
                               (XARGS :GUARD (TRUE-LISTP X)
                                      :SPLIT-TYPES T))
                      (NOT (EQUAL (CAR X) 7)))
             (UNTIL$ (LAMBDA$ (X)
                              (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                       (IGNORABLE X)
                                       (XARGS :GUARD (TRUE-LISTP X)
                                              :SPLIT-TYPES T))
                              (EQUAL (CAR X) 9))
                     (TAILS (MAKE-LIST-AC N 1 NIL)))))
    (LEN
      (WHEN$ (LAMBDA$ (X)
                      (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                               (IGNORABLE X)
                               (XARGS :GUARD (TRUE-LISTP X)
                                      :SPLIT-TYPES T))
                      (NOT (EQUAL (CAR X) 7)))
             (UNTIL$ (LAMBDA$ (X)
                              (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                       (IGNORABLE X)
                                       (XARGS :GUARD (TRUE-LISTP X)
                                              :SPLIT-TYPES T))
                              (EQUAL (CAR X) 9))
                     (TAILS (MAKE-LIST-AC N 1 NIL)))))))
  (ACL2-NUMBERP
       (APPLY$ (LAMBDA$ (X)
                        (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                 (IGNORABLE X)
                                 (XARGS :GUARD (TRUE-LISTP X)
                                        :SPLIT-TYPES T))
                        (LENGTH X))
               (LIST NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
      NEWV
      (WHEN$ (LAMBDA$ (X)
                      (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                               (IGNORABLE X)
                               (XARGS :GUARD (TRUE-LISTP X)
                                      :SPLIT-TYPES T))
                      (NOT (EQUAL (CAR X) 7)))
             (UNTIL$ (LAMBDA$ (X)
                              (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                       (IGNORABLE X)
                                       (XARGS :GUARD (TRUE-LISTP X)
                                              :SPLIT-TYPES T))
                              (EQUAL (CAR X) 9))
                     (TAILS (MAKE-LIST-AC N 1 NIL)))))
    (LEN
      (WHEN$ (LAMBDA$ (X)
                      (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                               (IGNORABLE X)
                               (XARGS :GUARD (TRUE-LISTP X)
                                      :SPLIT-TYPES T))
                      (NOT (EQUAL (CAR X) 7)))
             (UNTIL$ (LAMBDA$ (X)
                              (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                       (IGNORABLE X)
                                       (XARGS :GUARD (TRUE-LISTP X)
                                              :SPLIT-TYPES T))
                              (EQUAL (CAR X) 9))
                     (TAILS (MAKE-LIST-AC N 1 NIL)))))))
  (TRUE-LISTP NEWV))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
      NEWV
      (WHEN$ (LAMBDA$ (X)
                      (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                               (IGNORABLE X)
                               (XARGS :GUARD (TRUE-LISTP X)
                                      :SPLIT-TYPES T))
                      (NOT (EQUAL (CAR X) 7)))
             (UNTIL$ (LAMBDA$ (X)
                              (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                       (IGNORABLE X)
                                       (XARGS :GUARD (TRUE-LISTP X)
                                              :SPLIT-TYPES T))
                              (EQUAL (CAR X) 9))
                     (TAILS (MAKE-LIST-AC N 1 NIL)))))
    (LEN
      (WHEN$ (LAMBDA$ (X)
                      (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                               (IGNORABLE X)
                               (XARGS :GUARD (TRUE-LISTP X)
                                      :SPLIT-TYPES T))
                      (NOT (EQUAL (CAR X) 7)))
             (UNTIL$ (LAMBDA$ (X)
                              (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                       (IGNORABLE X)
                                       (XARGS :GUARD (TRUE-LISTP X)
                                              :SPLIT-TYPES T))
                              (EQUAL (CAR X) 9))
                     (TAILS (MAKE-LIST-AC N 1 NIL)))))))
  (TRUE-LISTP
       (APPLY$ (LAMBDA$ (X)
                        (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                 (IGNORABLE X)
                                 (XARGS :GUARD (TRUE-LISTP X)
                                        :SPLIT-TYPES T))
                        X)
               (LIST NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (WHEN$+
      (LAMBDA$
           (LOCALS GLOBALS)
           (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                       (EQUAL (LEN LOCALS) 2)
                                       (TRUE-LISTP GLOBALS)
                                       (EQUAL (LEN GLOBALS) 0)
                                       (INTEGERP (CAR LOCALS))
                                       (RATIONALP (CADR LOCALS)))
                           :SPLIT-TYPES T)
                    (IGNORE GLOBALS))
           (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                    '(RATIONALP Y)))
                        (NOT (EQUAL Y 7)))))
      NIL
      (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (MAKE-LIST-AC N 1 NIL)
                  (MAKE-LIST-AC N 1 NIL))))))
    (LEN
     (WHEN$+
      (LAMBDA$
           (LOCALS GLOBALS)
           (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                       (EQUAL (LEN LOCALS) 2)
                                       (TRUE-LISTP GLOBALS)
                                       (EQUAL (LEN GLOBALS) 0)
                                       (INTEGERP (CAR LOCALS))
                                       (RATIONALP (CADR LOCALS)))
                           :SPLIT-TYPES T)
                    (IGNORE GLOBALS))
           (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                    '(RATIONALP Y)))
                        (NOT (EQUAL Y 7)))))
      NIL
      (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (MAKE-LIST-AC N 1 NIL)
                  (MAKE-LIST-AC N 1 NIL))))))))
  (ACL2-NUMBERP
   (APPLY$
    (LAMBDA$ (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          X)))
    (CONS NEWV '(NIL)))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (WHEN$+
      (LAMBDA$
           (LOCALS GLOBALS)
           (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                       (EQUAL (LEN LOCALS) 2)
                                       (TRUE-LISTP GLOBALS)
                                       (EQUAL (LEN GLOBALS) 0)
                                       (INTEGERP (CAR LOCALS))
                                       (RATIONALP (CADR LOCALS)))
                           :SPLIT-TYPES T)
                    (IGNORE GLOBALS))
           (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                    '(RATIONALP Y)))
                        (NOT (EQUAL Y 7)))))
      NIL
      (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (MAKE-LIST-AC N 1 NIL)
                  (MAKE-LIST-AC N 1 NIL))))))
    (LEN
     (WHEN$+
      (LAMBDA$
           (LOCALS GLOBALS)
           (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                       (EQUAL (LEN LOCALS) 2)
                                       (TRUE-LISTP GLOBALS)
                                       (EQUAL (LEN GLOBALS) 0)
                                       (INTEGERP (CAR LOCALS))
                                       (RATIONALP (CADR LOCALS)))
                           :SPLIT-TYPES T)
                    (IGNORE GLOBALS))
           (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                    '(RATIONALP Y)))
                        (NOT (EQUAL Y 7)))))
      NIL
      (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (MAKE-LIST-AC N 1 NIL)
                  (MAKE-LIST-AC N 1 NIL))))))))
  (AND (TRUE-LISTP NEWV)
       (EQUAL (LEN NEWV) 2)
       (INTEGERP (CAR NEWV))
       (RATIONALP (CADR NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (WHEN$+
      (LAMBDA$
           (LOCALS GLOBALS)
           (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                       (EQUAL (LEN LOCALS) 2)
                                       (TRUE-LISTP GLOBALS)
                                       (EQUAL (LEN GLOBALS) 0)
                                       (INTEGERP (CAR LOCALS))
                                       (RATIONALP (CADR LOCALS)))
                           :SPLIT-TYPES T)
                    (IGNORE GLOBALS))
           (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                    '(RATIONALP Y)))
                        (NOT (EQUAL Y 7)))))
      NIL
      (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (MAKE-LIST-AC N 1 NIL)
                  (MAKE-LIST-AC N 1 NIL))))))
    (LEN
     (WHEN$+
      (LAMBDA$
           (LOCALS GLOBALS)
           (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                       (EQUAL (LEN LOCALS) 2)
                                       (TRUE-LISTP GLOBALS)
                                       (EQUAL (LEN GLOBALS) 0)
                                       (INTEGERP (CAR LOCALS))
                                       (RATIONALP (CADR LOCALS)))
                           :SPLIT-TYPES T)
                    (IGNORE GLOBALS))
           (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                    '(RATIONALP Y)))
                        (NOT (EQUAL Y 7)))))
      NIL
      (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (MAKE-LIST-AC N 1 NIL)
                  (MAKE-LIST-AC N 1 NIL))))))))
  (TRUE-LISTP
   (APPLY$
    (LAMBDA$ (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (LIST X))))
    (CONS NEWV '(NIL)))))
 (IMPLIES
  (AND
   (NATP N)
   (< (MEMPOS
           NEWV
           (WHEN$ (LAMBDA$ (X)
                           (DECLARE (TYPE INTEGER X)
                                    (IGNORABLE X)
                                    (XARGS :GUARD (INTEGERP X)
                                           :SPLIT-TYPES T))
                           (NOT (EQUAL X 7)))
                  (UNTIL$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (EQUAL X 9))
                          (MAKE-LIST-AC N 1 NIL))))
      (LEN (WHEN$ (LAMBDA$ (X)
                           (DECLARE (TYPE INTEGER X)
                                    (IGNORABLE X)
                                    (XARGS :GUARD (INTEGERP X)
                                           :SPLIT-TYPES T))
                           (NOT (EQUAL X 7)))
                  (UNTIL$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (EQUAL X 9))
                          (MAKE-LIST-AC N 1 NIL))))))
  (TRUE-LISTP (APPLY$ (LAMBDA$ (X)
                               (DECLARE (TYPE INTEGER X)
                                        (IGNORABLE X)
                                        (XARGS :GUARD (INTEGERP X)
                                               :SPLIT-TYPES T))
                               (LIST X))
                      (LIST NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (< (MEMPOS
           NEWV
           (WHEN$ (LAMBDA$ (X)
                           (DECLARE (TYPE INTEGER X)
                                    (IGNORABLE X)
                                    (XARGS :GUARD (INTEGERP X)
                                           :SPLIT-TYPES T))
                           (NOT (EQUAL X 7)))
                  (UNTIL$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (EQUAL X 9))
                          (MAKE-LIST-AC N 1 NIL))))
      (LEN (WHEN$ (LAMBDA$ (X)
                           (DECLARE (TYPE INTEGER X)
                                    (IGNORABLE X)
                                    (XARGS :GUARD (INTEGERP X)
                                           :SPLIT-TYPES T))
                           (NOT (EQUAL X 7)))
                  (UNTIL$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (EQUAL X 9))
                          (MAKE-LIST-AC N 1 NIL))))))
  (ACL2-NUMBERP (APPLY$ (LAMBDA$ (X)
                                 (DECLARE (TYPE INTEGER X)
                                          (IGNORABLE X)
                                          (XARGS :GUARD (INTEGERP X)
                                                 :SPLIT-TYPES T))
                                 X)
                        (LIST NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (< (MEMPOS
           NEWV
           (WHEN$ (LAMBDA$ (X)
                           (DECLARE (TYPE INTEGER X)
                                    (IGNORABLE X)
                                    (XARGS :GUARD (INTEGERP X)
                                           :SPLIT-TYPES T))
                           (NOT (EQUAL X 7)))
                  (UNTIL$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (EQUAL X 9))
                          (MAKE-LIST-AC N 1 NIL))))
      (LEN (WHEN$ (LAMBDA$ (X)
                           (DECLARE (TYPE INTEGER X)
                                    (IGNORABLE X)
                                    (XARGS :GUARD (INTEGERP X)
                                           :SPLIT-TYPES T))
                           (NOT (EQUAL X 7)))
                  (UNTIL$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (EQUAL X 9))
                          (MAKE-LIST-AC N 1 NIL))))))
  (INTEGERP NEWV))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (MAKE-LIST-AC N 1 NIL)
                  (MAKE-LIST-AC N 1 NIL)))))
    (LEN
     (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (MAKE-LIST-AC N 1 NIL)
                  (MAKE-LIST-AC N 1 NIL)))))))
  (AND (TRUE-LISTP NEWV)
       (EQUAL (LEN NEWV) 2)
       (INTEGERP (CAR NEWV))
       (RATIONALP (CADR NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (AND (RATIONAL-LISTP (CAR LOCALS))
                                        (IDENTITY (CAR LOCALS)))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS)) (Y (CADR LOCALS)))
        (PROG2$
         (PROG2$
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP X) (IDENTITY X))
                                 '(IF (RATIONAL-LISTP X)
                                      (IDENTITY X)
                                      'NIL))
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                                 '(IF (RATIONAL-LISTP Y)
                                      (IDENTITY Y)
                                      'NIL)))
         (NOT (EQUAL (CAR X) 1/3)))))
      NIL
      (UNTIL$+
       (LAMBDA$
        (LOCALS GLOBALS)
        (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                    (EQUAL (LEN LOCALS) 2)
                                    (TRUE-LISTP GLOBALS)
                                    (EQUAL (LEN GLOBALS) 0)
                                    (AND (RATIONAL-LISTP (CAR LOCALS))
                                         (IDENTITY (CAR LOCALS)))
                                    (RATIONAL-LISTP (CADR LOCALS))
                                    (IDENTITY (CADR LOCALS)))
                        :SPLIT-TYPES T)
                 (IGNORE GLOBALS))
        (LET
         ((X (CAR LOCALS)) (Y (CADR LOCALS)))
         (PROG2$
          (PROG2$
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP X) (IDENTITY X))
                                 '(IF (RATIONAL-LISTP X)
                                      (IDENTITY X)
                                      'NIL))
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                                 '(IF (RATIONAL-LISTP Y)
                                      (IDENTITY Y)
                                      'NIL)))
          (EQUAL (CAR X) 9))))
       NIL
       (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                 (TAILS (MAKE-LIST-AC N 1/3 NIL)))))))
    (LEN
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (AND (RATIONAL-LISTP (CAR LOCALS))
                                        (IDENTITY (CAR LOCALS)))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS)) (Y (CADR LOCALS)))
        (PROG2$
         (PROG2$
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP X) (IDENTITY X))
                                 '(IF (RATIONAL-LISTP X)
                                      (IDENTITY X)
                                      'NIL))
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                                 '(IF (RATIONAL-LISTP Y)
                                      (IDENTITY Y)
                                      'NIL)))
         (NOT (EQUAL (CAR X) 1/3)))))
      NIL
      (UNTIL$+
       (LAMBDA$
        (LOCALS GLOBALS)
        (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                    (EQUAL (LEN LOCALS) 2)
                                    (TRUE-LISTP GLOBALS)
                                    (EQUAL (LEN GLOBALS) 0)
                                    (AND (RATIONAL-LISTP (CAR LOCALS))
                                         (IDENTITY (CAR LOCALS)))
                                    (RATIONAL-LISTP (CADR LOCALS))
                                    (IDENTITY (CADR LOCALS)))
                        :SPLIT-TYPES T)
                 (IGNORE GLOBALS))
        (LET
         ((X (CAR LOCALS)) (Y (CADR LOCALS)))
         (PROG2$
          (PROG2$
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP X) (IDENTITY X))
                                 '(IF (RATIONAL-LISTP X)
                                      (IDENTITY X)
                                      'NIL))
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                                 '(IF (RATIONAL-LISTP Y)
                                      (IDENTITY Y)
                                      'NIL)))
          (EQUAL (CAR X) 9))))
       NIL
       (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                 (TAILS (MAKE-LIST-AC N 1/3 NIL)))))))))
  (AND (TRUE-LISTP NEWV)
       (EQUAL (LEN NEWV) 2)
       (AND (RATIONAL-LISTP (CAR NEWV))
            (IDENTITY (CAR NEWV)))
       (RATIONAL-LISTP (CADR NEWV))
       (IDENTITY (CADR NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (AND (RATIONAL-LISTP (CAR LOCALS))
                                        (IDENTITY (CAR LOCALS)))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS)) (Y (CADR LOCALS)))
        (PROG2$
         (PROG2$
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP X) (IDENTITY X))
                                 '(IF (RATIONAL-LISTP X)
                                      (IDENTITY X)
                                      'NIL))
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                                 '(IF (RATIONAL-LISTP Y)
                                      (IDENTITY Y)
                                      'NIL)))
         (NOT (EQUAL (CAR X) 1/3)))))
      NIL
      (UNTIL$+
       (LAMBDA$
        (LOCALS GLOBALS)
        (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                    (EQUAL (LEN LOCALS) 2)
                                    (TRUE-LISTP GLOBALS)
                                    (EQUAL (LEN GLOBALS) 0)
                                    (AND (RATIONAL-LISTP (CAR LOCALS))
                                         (IDENTITY (CAR LOCALS)))
                                    (RATIONAL-LISTP (CADR LOCALS))
                                    (IDENTITY (CADR LOCALS)))
                        :SPLIT-TYPES T)
                 (IGNORE GLOBALS))
        (LET
         ((X (CAR LOCALS)) (Y (CADR LOCALS)))
         (PROG2$
          (PROG2$
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP X) (IDENTITY X))
                                 '(IF (RATIONAL-LISTP X)
                                      (IDENTITY X)
                                      'NIL))
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                                 '(IF (RATIONAL-LISTP Y)
                                      (IDENTITY Y)
                                      'NIL)))
          (EQUAL (CAR X) 9))))
       NIL
       (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                 (TAILS (MAKE-LIST-AC N 1/3 NIL)))))))
    (LEN
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (AND (RATIONAL-LISTP (CAR LOCALS))
                                        (IDENTITY (CAR LOCALS)))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS)) (Y (CADR LOCALS)))
        (PROG2$
         (PROG2$
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP X) (IDENTITY X))
                                 '(IF (RATIONAL-LISTP X)
                                      (IDENTITY X)
                                      'NIL))
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                                 '(IF (RATIONAL-LISTP Y)
                                      (IDENTITY Y)
                                      'NIL)))
         (NOT (EQUAL (CAR X) 1/3)))))
      NIL
      (UNTIL$+
       (LAMBDA$
        (LOCALS GLOBALS)
        (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                    (EQUAL (LEN LOCALS) 2)
                                    (TRUE-LISTP GLOBALS)
                                    (EQUAL (LEN GLOBALS) 0)
                                    (AND (RATIONAL-LISTP (CAR LOCALS))
                                         (IDENTITY (CAR LOCALS)))
                                    (RATIONAL-LISTP (CADR LOCALS))
                                    (IDENTITY (CADR LOCALS)))
                        :SPLIT-TYPES T)
                 (IGNORE GLOBALS))
        (LET
         ((X (CAR LOCALS)) (Y (CADR LOCALS)))
         (PROG2$
          (PROG2$
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP X) (IDENTITY X))
                                 '(IF (RATIONAL-LISTP X)
                                      (IDENTITY X)
                                      'NIL))
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                                 '(IF (RATIONAL-LISTP Y)
                                      (IDENTITY Y)
                                      'NIL)))
          (EQUAL (CAR X) 9))))
       NIL
       (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                 (TAILS (MAKE-LIST-AC N 1/3 NIL)))))))))
  (ACL2-NUMBERP
   (APPLY$
    (LAMBDA$
     (LOCALS GLOBALS)
     (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                 (EQUAL (LEN LOCALS) 2)
                                 (TRUE-LISTP GLOBALS)
                                 (EQUAL (LEN GLOBALS) 0)
                                 (AND (RATIONAL-LISTP (CAR LOCALS))
                                      (IDENTITY (CAR LOCALS)))
                                 (RATIONAL-LISTP (CADR LOCALS))
                                 (IDENTITY (CADR LOCALS)))
                     :SPLIT-TYPES T)
              (IGNORE GLOBALS))
     (LET
      ((X (CAR LOCALS)) (Y (CADR LOCALS)))
      (PROG2$
        (PROG2$
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP X) (IDENTITY X))
                                 '(IF (RATIONAL-LISTP X)
                                      (IDENTITY X)
                                      'NIL))
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                                 '(IF (RATIONAL-LISTP Y)
                                      (IDENTITY Y)
                                      'NIL)))
        (+ (LENGTH X) (CAR Y)))))
    (CONS NEWV '(NIL)))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (AND (RATIONAL-LISTP (CAR LOCALS))
                                        (IDENTITY (CAR LOCALS)))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS)) (Y (CADR LOCALS)))
        (PROG2$
         (PROG2$
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP X) (IDENTITY X))
                                 '(IF (RATIONAL-LISTP X)
                                      (IDENTITY X)
                                      'NIL))
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                                 '(IF (RATIONAL-LISTP Y)
                                      (IDENTITY Y)
                                      'NIL)))
         (NOT (EQUAL (CAR X) 1/3)))))
      NIL
      (UNTIL$+
       (LAMBDA$
        (LOCALS GLOBALS)
        (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                    (EQUAL (LEN LOCALS) 2)
                                    (TRUE-LISTP GLOBALS)
                                    (EQUAL (LEN GLOBALS) 0)
                                    (AND (RATIONAL-LISTP (CAR LOCALS))
                                         (IDENTITY (CAR LOCALS)))
                                    (RATIONAL-LISTP (CADR LOCALS))
                                    (IDENTITY (CADR LOCALS)))
                        :SPLIT-TYPES T)
                 (IGNORE GLOBALS))
        (LET
         ((X (CAR LOCALS)) (Y (CADR LOCALS)))
         (PROG2$
          (PROG2$
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP X) (IDENTITY X))
                                 '(IF (RATIONAL-LISTP X)
                                      (IDENTITY X)
                                      'NIL))
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                                 '(IF (RATIONAL-LISTP Y)
                                      (IDENTITY Y)
                                      'NIL)))
          (EQUAL (CAR X) 9))))
       NIL
       (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                 (TAILS (MAKE-LIST-AC N 1/3 NIL)))))))
    (LEN
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (AND (RATIONAL-LISTP (CAR LOCALS))
                                        (IDENTITY (CAR LOCALS)))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS)) (Y (CADR LOCALS)))
        (PROG2$
         (PROG2$
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP X) (IDENTITY X))
                                 '(IF (RATIONAL-LISTP X)
                                      (IDENTITY X)
                                      'NIL))
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                                 '(IF (RATIONAL-LISTP Y)
                                      (IDENTITY Y)
                                      'NIL)))
         (NOT (EQUAL (CAR X) 1/3)))))
      NIL
      (UNTIL$+
       (LAMBDA$
        (LOCALS GLOBALS)
        (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                    (EQUAL (LEN LOCALS) 2)
                                    (TRUE-LISTP GLOBALS)
                                    (EQUAL (LEN GLOBALS) 0)
                                    (AND (RATIONAL-LISTP (CAR LOCALS))
                                         (IDENTITY (CAR LOCALS)))
                                    (RATIONAL-LISTP (CADR LOCALS))
                                    (IDENTITY (CADR LOCALS)))
                        :SPLIT-TYPES T)
                 (IGNORE GLOBALS))
        (LET
         ((X (CAR LOCALS)) (Y (CADR LOCALS)))
         (PROG2$
          (PROG2$
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP X) (IDENTITY X))
                                 '(IF (RATIONAL-LISTP X)
                                      (IDENTITY X)
                                      'NIL))
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                                 '(IF (RATIONAL-LISTP Y)
                                      (IDENTITY Y)
                                      'NIL)))
          (EQUAL (CAR X) 9))))
       NIL
       (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                 (TAILS (MAKE-LIST-AC N 1/3 NIL)))))))))
  (TRUE-LISTP
   (APPLY$
    (LAMBDA$
     (LOCALS GLOBALS)
     (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                 (EQUAL (LEN LOCALS) 2)
                                 (TRUE-LISTP GLOBALS)
                                 (EQUAL (LEN GLOBALS) 0)
                                 (AND (RATIONAL-LISTP (CAR LOCALS))
                                      (IDENTITY (CAR LOCALS)))
                                 (RATIONAL-LISTP (CADR LOCALS))
                                 (IDENTITY (CADR LOCALS)))
                     :SPLIT-TYPES T)
              (IGNORE GLOBALS))
     (LET
      ((X (CAR LOCALS)) (Y (CADR LOCALS)))
      (PROG2$
        (PROG2$
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP X) (IDENTITY X))
                                 '(IF (RATIONAL-LISTP X)
                                      (IDENTITY X)
                                      'NIL))
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                                 '(IF (RATIONAL-LISTP Y)
                                      (IDENTITY Y)
                                      'NIL)))
        (APPEND X Y))))
    (CONS NEWV '(NIL)))))
 (IMPLIES
   (AND (NATP N)
        (< (MEMPOS NEWV
                   (WHEN$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (NOT (EQUAL X 7)))
                          (FROM-TO-BY 1 N 1)))
           (LEN (WHEN$ (LAMBDA$ (X)
                                (DECLARE (TYPE INTEGER X)
                                         (IGNORABLE X)
                                         (XARGS :GUARD (INTEGERP X)
                                                :SPLIT-TYPES T))
                                (NOT (EQUAL X 7)))
                       (FROM-TO-BY 1 N 1)))))
   (TRUE-LISTP (APPLY$ (LAMBDA$ (X)
                                (DECLARE (TYPE INTEGER X)
                                         (IGNORABLE X)
                                         (XARGS :GUARD (INTEGERP X)
                                                :SPLIT-TYPES T))
                                (LIST X))
                       (LIST NEWV))))
 (IMPLIES
   (AND (NATP N)
        (< (MEMPOS NEWV
                   (WHEN$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (NOT (EQUAL X 7)))
                          (FROM-TO-BY 1 N 1)))
           (LEN (WHEN$ (LAMBDA$ (X)
                                (DECLARE (TYPE INTEGER X)
                                         (IGNORABLE X)
                                         (XARGS :GUARD (INTEGERP X)
                                                :SPLIT-TYPES T))
                                (NOT (EQUAL X 7)))
                       (FROM-TO-BY 1 N 1)))))
   (ACL2-NUMBERP (APPLY$ (LAMBDA$ (X)
                                  (DECLARE (TYPE INTEGER X)
                                           (IGNORABLE X)
                                           (XARGS :GUARD (INTEGERP X)
                                                  :SPLIT-TYPES T))
                                  X)
                         (LIST NEWV))))
 (IMPLIES
   (AND (NATP N)
        (< (MEMPOS NEWV
                   (WHEN$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (NOT (EQUAL X 7)))
                          (FROM-TO-BY 1 N 1)))
           (LEN (WHEN$ (LAMBDA$ (X)
                                (DECLARE (TYPE INTEGER X)
                                         (IGNORABLE X)
                                         (XARGS :GUARD (INTEGERP X)
                                                :SPLIT-TYPES T))
                                (NOT (EQUAL X 7)))
                       (FROM-TO-BY 1 N 1)))))
   (INTEGERP NEWV))
 (IMPLIES
  (AND (NATP N)
       (< (MEMPOS NEWV
                  (AS (CONS (FROM-TO-BY 1 N 1)
                            '((A B C D E F G H I J K L M N O P)))))
          (LEN (AS (CONS (FROM-TO-BY 1 N 1)
                         '((A B C D E F G H I J K L M N O P)))))))
  (TRUE-LISTP
   (APPLY$
    (LAMBDA$
         (LOCALS GLOBALS)
         (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                     (EQUAL (LEN LOCALS) 2)
                                     (TRUE-LISTP GLOBALS)
                                     (EQUAL (LEN GLOBALS) 0)
                                     (INTEGERP (CAR LOCALS))
                                     (SYMBOLP (CADR LOCALS)))
                         :SPLIT-TYPES T)
                  (IGNORE GLOBALS))
         (LET ((X (CAR LOCALS)) (SYM (CADR LOCALS)))
              (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                          '(INTEGERP X))
                      (MAKE-LIST-AC 3 (+ X (LENGTH (SYMBOL-NAME SYM)))
                                    NIL))))
    (CONS NEWV '(NIL)))))
 (IMPLIES
  (AND (NATP N)
       (< (MEMPOS NEWV
                  (AS (CONS (FROM-TO-BY 1 N 1)
                            '((A B C D E F G H I J K L M N O P)))))
          (LEN (AS (CONS (FROM-TO-BY 1 N 1)
                         '((A B C D E F G H I J K L M N O P)))))))
  (ACL2-NUMBERP
    (APPLY$
         (LAMBDA$ (LOCALS GLOBALS)
                  (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                              (EQUAL (LEN LOCALS) 2)
                                              (TRUE-LISTP GLOBALS)
                                              (EQUAL (LEN GLOBALS) 0)
                                              (INTEGERP (CAR LOCALS))
                                              (SYMBOLP (CADR LOCALS)))
                                  :SPLIT-TYPES T)
                           (IGNORE GLOBALS))
                  (LET ((X (CAR LOCALS)) (SYM (CADR LOCALS)))
                       (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                   '(INTEGERP X))
                               (+ X (LENGTH (SYMBOL-NAME SYM))))))
         (CONS NEWV '(NIL)))))
 (IMPLIES
     (AND (NATP N)
          (< (MEMPOS NEWV
                     (AS (CONS (FROM-TO-BY 1 N 1)
                               '((A B C D E F G H I J K L M N O P)))))
             (LEN (AS (CONS (FROM-TO-BY 1 N 1)
                            '((A B C D E F G H I J K L M N O P)))))))
     (AND (TRUE-LISTP NEWV)
          (EQUAL (LEN NEWV) 2)
          (INTEGERP (CAR NEWV))
          (SYMBOLP (CADR NEWV))))
 (IMPLIES
      (AND (NATP N)
           (< (MEMPOS NEWV (FROM-TO-BY 1 N 1))
              (LEN (FROM-TO-BY 1 N 1))))
      (TRUE-LISTP (APPLY$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (LIST X))
                          (LIST NEWV))))
 (IMPLIES
    (AND (NATP N)
         (< (MEMPOS NEWV (FROM-TO-BY 1 N 1))
            (LEN (FROM-TO-BY 1 N 1))))
    (ACL2-NUMBERP (APPLY$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   X)
                          (LIST NEWV))))
 (IMPLIES (AND (NATP N)
               (< (MEMPOS NEWV (FROM-TO-BY 1 N 1))
                  (LEN (FROM-TO-BY 1 N 1))))
          (INTEGERP NEWV))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (TRUE-LISTP (CAR LOCALS))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (TRUE-LISTP X)
                                         '(TRUE-LISTP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (OR (<= (LENGTH X) 6)
                 (<= (CAR RATTAIL) 7)))))
      NIL
      (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                (TAILS (MAKE-LIST-AC N 1/2 NIL))))))
    (LEN
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (TRUE-LISTP (CAR LOCALS))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (TRUE-LISTP X)
                                         '(TRUE-LISTP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (OR (<= (LENGTH X) 6)
                 (<= (CAR RATTAIL) 7)))))
      NIL
      (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                (TAILS (MAKE-LIST-AC N 1/2 NIL))))))))
  (TRUE-LISTP
   (APPLY$
    (LAMBDA$
     (LOCALS GLOBALS)
     (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                 (EQUAL (LEN LOCALS) 2)
                                 (TRUE-LISTP GLOBALS)
                                 (EQUAL (LEN GLOBALS) 0)
                                 (TRUE-LISTP (CAR LOCALS))
                                 (RATIONAL-LISTP (CADR LOCALS))
                                 (IDENTITY (CADR LOCALS)))
                     :SPLIT-TYPES T)
              (IGNORE GLOBALS))
     (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (TRUE-LISTP X)
                                         '(TRUE-LISTP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (APPEND X RATTAIL))))
    (CONS NEWV '(NIL)))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (TRUE-LISTP (CAR LOCALS))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (TRUE-LISTP X)
                                         '(TRUE-LISTP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (OR (<= (LENGTH X) 6)
                 (<= (CAR RATTAIL) 7)))))
      NIL
      (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                (TAILS (MAKE-LIST-AC N 1/2 NIL))))))
    (LEN
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (TRUE-LISTP (CAR LOCALS))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (TRUE-LISTP X)
                                         '(TRUE-LISTP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (OR (<= (LENGTH X) 6)
                 (<= (CAR RATTAIL) 7)))))
      NIL
      (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                (TAILS (MAKE-LIST-AC N 1/2 NIL))))))))
  (ACL2-NUMBERP
   (APPLY$
    (LAMBDA$
     (LOCALS GLOBALS)
     (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                 (EQUAL (LEN LOCALS) 2)
                                 (TRUE-LISTP GLOBALS)
                                 (EQUAL (LEN GLOBALS) 0)
                                 (TRUE-LISTP (CAR LOCALS))
                                 (RATIONAL-LISTP (CADR LOCALS))
                                 (IDENTITY (CADR LOCALS)))
                     :SPLIT-TYPES T)
              (IGNORE GLOBALS))
     (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (TRUE-LISTP X)
                                         '(TRUE-LISTP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (+ (LENGTH X) (CAR RATTAIL)))))
    (CONS NEWV '(NIL)))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (TRUE-LISTP (CAR LOCALS))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (TRUE-LISTP X)
                                         '(TRUE-LISTP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (OR (<= (LENGTH X) 6)
                 (<= (CAR RATTAIL) 7)))))
      NIL
      (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                (TAILS (MAKE-LIST-AC N 1/2 NIL))))))
    (LEN
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (TRUE-LISTP (CAR LOCALS))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (TRUE-LISTP X)
                                         '(TRUE-LISTP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (OR (<= (LENGTH X) 6)
                 (<= (CAR RATTAIL) 7)))))
      NIL
      (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                (TAILS (MAKE-LIST-AC N 1/2 NIL))))))))
  (AND (TRUE-LISTP NEWV)
       (EQUAL (LEN NEWV) 2)
       (TRUE-LISTP (CAR NEWV))
       (RATIONAL-LISTP (CADR NEWV))
       (IDENTITY (CADR NEWV))))
 (IMPLIES
  (AND (NATP N)
       (< (MEMPOS NEWV
                  (AS (CONS (MAKE-LIST-AC N 1 NIL)
                            '((A B C D E F G H I J K L M N O P)))))
          (LEN (AS (CONS (MAKE-LIST-AC N 1 NIL)
                         '((A B C D E F G H I J K L M N O P)))))))
  (TRUE-LISTP
   (APPLY$
    (LAMBDA$
         (LOCALS GLOBALS)
         (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                     (EQUAL (LEN LOCALS) 2)
                                     (TRUE-LISTP GLOBALS)
                                     (EQUAL (LEN GLOBALS) 0)
                                     (INTEGERP (CAR LOCALS))
                                     (SYMBOLP (CADR LOCALS)))
                         :SPLIT-TYPES T)
                  (IGNORE GLOBALS))
         (LET ((X (CAR LOCALS)) (SYM (CADR LOCALS)))
              (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                          '(INTEGERP X))
                      (MAKE-LIST-AC 3 (+ X (LENGTH (SYMBOL-NAME SYM)))
                                    NIL))))
    (CONS NEWV '(NIL)))))
 (IMPLIES
     (AND (NATP N)
          (< (MEMPOS NEWV
                     (AS (CONS (MAKE-LIST-AC N 1 NIL)
                               '((A B C D E F G H I J K L M N O P)))))
             (LEN (AS (CONS (MAKE-LIST-AC N 1 NIL)
                            '((A B C D E F G H I J K L M N O P)))))))
     (AND (TRUE-LISTP NEWV)
          (EQUAL (LEN NEWV) 2)
          (INTEGERP (CAR NEWV))
          (SYMBOLP (CADR NEWV))))
 (IMPLIES
     (AND (NATP N)
          (< (MEMPOS NEWV
                     (AS (CONS (MAKE-LIST-AC N 1 NIL)
                               '((A B C D E F G H I J K L M N O P)))))
             (LEN (AS (CONS (MAKE-LIST-AC N 1 NIL)
                            '((A B C D E F G H I J K L M N O P)))))))
     (AND (TRUE-LISTP NEWV)
          (EQUAL (LEN NEWV) 2)
          (INTEGERP (CAR NEWV))
          (SYMP (CADR NEWV))))
 (IMPLIES
  (AND (NATP N)
       (< (MEMPOS NEWV
                  (AS (CONS (MAKE-LIST-AC N 1 NIL)
                            '((A B C D E F G H I J K L M N O P)))))
          (LEN (AS (CONS (MAKE-LIST-AC N 1 NIL)
                         '((A B C D E F G H I J K L M N O P)))))))
  (ACL2-NUMBERP
    (APPLY$
         (LAMBDA$ (LOCALS GLOBALS)
                  (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                              (EQUAL (LEN LOCALS) 2)
                                              (TRUE-LISTP GLOBALS)
                                              (EQUAL (LEN GLOBALS) 0)
                                              (INTEGERP (CAR LOCALS))
                                              (SYMBOLP (CADR LOCALS)))
                                  :SPLIT-TYPES T)
                           (IGNORE GLOBALS))
                  (LET ((X (CAR LOCALS)) (SYM (CADR LOCALS)))
                       (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                   '(INTEGERP X))
                               (+ X (LENGTH (SYMBOL-NAME SYM))))))
         (CONS NEWV '(NIL)))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (FROM-TO-BY 1 N 1)
                  (MAKE-LIST-AC N 1 NIL)))))
    (LEN
     (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (FROM-TO-BY 1 N 1)
                  (MAKE-LIST-AC N 1 NIL)))))))
  (AND (TRUE-LISTP NEWV)
       (EQUAL (LEN NEWV) 2)
       (INTEGERP (CAR NEWV))
       (RATIONALP (CADR NEWV))))
 (IMPLIES
  (AND (NATP N)
       (< (MEMPOS NEWV
                  (UNTIL$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (EQUAL X 9))
                          (FROM-TO-BY 1 N 1)))
          (LEN (UNTIL$ (LAMBDA$ (X)
                                (DECLARE (TYPE INTEGER X)
                                         (IGNORABLE X)
                                         (XARGS :GUARD (INTEGERP X)
                                                :SPLIT-TYPES T))
                                (EQUAL X 9))
                       (FROM-TO-BY 1 N 1)))))
  (INTEGERP NEWV))
 (IMPLIES
  (AND
   (NATP N)
   (<
     (MEMPOS NEWV
             (UNTIL$ (LAMBDA$ (X)
                              (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                       (IGNORABLE X)
                                       (XARGS :GUARD (TRUE-LISTP X)
                                              :SPLIT-TYPES T))
                              (EQUAL (CAR X) 7))
                     (TAILS (MAKE-LIST-AC N 1 NIL))))
     (LEN (UNTIL$ (LAMBDA$ (X)
                           (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                    (IGNORABLE X)
                                    (XARGS :GUARD (TRUE-LISTP X)
                                           :SPLIT-TYPES T))
                           (EQUAL (CAR X) 7))
                  (TAILS (MAKE-LIST-AC N 1 NIL))))))
  (TRUE-LISTP NEWV))
 (IMPLIES
  (AND
   (NATP N)
   (<
     (MEMPOS NEWV
             (UNTIL$ (LAMBDA$ (X)
                              (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                       (IGNORABLE X)
                                       (XARGS :GUARD (TRUE-LISTP X)
                                              :SPLIT-TYPES T))
                              (EQUAL (CAR X) 7))
                     (TAILS (MAKE-LIST-AC N 1 NIL))))
     (LEN (UNTIL$ (LAMBDA$ (X)
                           (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                    (IGNORABLE X)
                                    (XARGS :GUARD (TRUE-LISTP X)
                                           :SPLIT-TYPES T))
                           (EQUAL (CAR X) 7))
                  (TAILS (MAKE-LIST-AC N 1 NIL))))))
  (TRUE-LISTP
       (APPLY$ (LAMBDA$ (X)
                        (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                 (IGNORABLE X)
                                 (XARGS :GUARD (TRUE-LISTP X)
                                        :SPLIT-TYPES T))
                        X)
               (LIST NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (<
     (MEMPOS NEWV
             (UNTIL$ (LAMBDA$ (X)
                              (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                       (IGNORABLE X)
                                       (XARGS :GUARD (TRUE-LISTP X)
                                              :SPLIT-TYPES T))
                              (EQUAL (CAR X) 7))
                     (TAILS (MAKE-LIST-AC N 1 NIL))))
     (LEN (UNTIL$ (LAMBDA$ (X)
                           (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                    (IGNORABLE X)
                                    (XARGS :GUARD (TRUE-LISTP X)
                                           :SPLIT-TYPES T))
                           (EQUAL (CAR X) 7))
                  (TAILS (MAKE-LIST-AC N 1 NIL))))))
  (ACL2-NUMBERP
       (APPLY$ (LAMBDA$ (X)
                        (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                 (IGNORABLE X)
                                 (XARGS :GUARD (TRUE-LISTP X)
                                        :SPLIT-TYPES T))
                        (LENGTH X))
               (LIST NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (UNTIL$+
          (LAMBDA$ (LOCALS GLOBALS)
                   (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                               (EQUAL (LEN LOCALS) 2)
                                               (TRUE-LISTP GLOBALS)
                                               (EQUAL (LEN GLOBALS) 0)
                                               (INTEGERP (CAR LOCALS))
                                               (SYMP (CADR LOCALS)))
                                   :SPLIT-TYPES T)
                            (IGNORE GLOBALS))
                   (LET ((X (CAR LOCALS)) (SYM (CADR LOCALS)))
                        (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (OR (EQUAL X 7) (EQ SYM '(A B C))))))
          NIL
          (AS (CONS (MAKE-LIST-AC N 1 NIL)
                    '((A B C D E F G H I J K L M N O P))))))
    (LEN
     (UNTIL$+
          (LAMBDA$ (LOCALS GLOBALS)
                   (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                               (EQUAL (LEN LOCALS) 2)
                                               (TRUE-LISTP GLOBALS)
                                               (EQUAL (LEN GLOBALS) 0)
                                               (INTEGERP (CAR LOCALS))
                                               (SYMP (CADR LOCALS)))
                                   :SPLIT-TYPES T)
                            (IGNORE GLOBALS))
                   (LET ((X (CAR LOCALS)) (SYM (CADR LOCALS)))
                        (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (OR (EQUAL X 7) (EQ SYM '(A B C))))))
          NIL
          (AS (CONS (MAKE-LIST-AC N 1 NIL)
                    '((A B C D E F G H I J K L M N O P))))))))
  (ACL2-NUMBERP
     (APPLY$
          (LAMBDA$ (LOCALS GLOBALS)
                   (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                               (EQUAL (LEN LOCALS) 2)
                                               (TRUE-LISTP GLOBALS)
                                               (EQUAL (LEN GLOBALS) 0)
                                               (INTEGERP (CAR LOCALS))
                                               (SYMP (CADR LOCALS)))
                                   :SPLIT-TYPES T)
                            (IGNORE GLOBALS))
                   (LET ((X (CAR LOCALS)) (SYM (CADR LOCALS)))
                        (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (+ X (LENGTH (SYMBOL-NAME SYM))))))
          (CONS NEWV '(NIL)))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (UNTIL$+
          (LAMBDA$ (LOCALS GLOBALS)
                   (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                               (EQUAL (LEN LOCALS) 2)
                                               (TRUE-LISTP GLOBALS)
                                               (EQUAL (LEN GLOBALS) 0)
                                               (INTEGERP (CAR LOCALS))
                                               (SYMP (CADR LOCALS)))
                                   :SPLIT-TYPES T)
                            (IGNORE GLOBALS))
                   (LET ((X (CAR LOCALS)) (SYM (CADR LOCALS)))
                        (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (OR (EQUAL X 7) (EQ SYM '(A B C))))))
          NIL
          (AS (CONS (MAKE-LIST-AC N 1 NIL)
                    '((A B C D E F G H I J K L M N O P))))))
    (LEN
     (UNTIL$+
          (LAMBDA$ (LOCALS GLOBALS)
                   (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                               (EQUAL (LEN LOCALS) 2)
                                               (TRUE-LISTP GLOBALS)
                                               (EQUAL (LEN GLOBALS) 0)
                                               (INTEGERP (CAR LOCALS))
                                               (SYMP (CADR LOCALS)))
                                   :SPLIT-TYPES T)
                            (IGNORE GLOBALS))
                   (LET ((X (CAR LOCALS)) (SYM (CADR LOCALS)))
                        (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (OR (EQUAL X 7) (EQ SYM '(A B C))))))
          NIL
          (AS (CONS (MAKE-LIST-AC N 1 NIL)
                    '((A B C D E F G H I J K L M N O P))))))))
  (TRUE-LISTP
   (APPLY$
    (LAMBDA$
         (LOCALS GLOBALS)
         (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                     (EQUAL (LEN LOCALS) 2)
                                     (TRUE-LISTP GLOBALS)
                                     (EQUAL (LEN GLOBALS) 0)
                                     (INTEGERP (CAR LOCALS))
                                     (SYMP (CADR LOCALS)))
                         :SPLIT-TYPES T)
                  (IGNORE GLOBALS))
         (LET ((X (CAR LOCALS)) (SYM (CADR LOCALS)))
              (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                          '(INTEGERP X))
                      (MAKE-LIST-AC 3 (+ X (LENGTH (SYMBOL-NAME SYM)))
                                    NIL))))
    (CONS NEWV '(NIL)))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (UNTIL$+
          (LAMBDA$ (LOCALS GLOBALS)
                   (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                               (EQUAL (LEN LOCALS) 2)
                                               (TRUE-LISTP GLOBALS)
                                               (EQUAL (LEN GLOBALS) 0)
                                               (INTEGERP (CAR LOCALS))
                                               (SYMP (CADR LOCALS)))
                                   :SPLIT-TYPES T)
                            (IGNORE GLOBALS))
                   (LET ((X (CAR LOCALS)) (SYM (CADR LOCALS)))
                        (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (OR (EQUAL X 7) (EQ SYM '(A B C))))))
          NIL
          (AS (CONS (MAKE-LIST-AC N 1 NIL)
                    '((A B C D E F G H I J K L M N O P))))))
    (LEN
     (UNTIL$+
          (LAMBDA$ (LOCALS GLOBALS)
                   (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                               (EQUAL (LEN LOCALS) 2)
                                               (TRUE-LISTP GLOBALS)
                                               (EQUAL (LEN GLOBALS) 0)
                                               (INTEGERP (CAR LOCALS))
                                               (SYMP (CADR LOCALS)))
                                   :SPLIT-TYPES T)
                            (IGNORE GLOBALS))
                   (LET ((X (CAR LOCALS)) (SYM (CADR LOCALS)))
                        (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (OR (EQUAL X 7) (EQ SYM '(A B C))))))
          NIL
          (AS (CONS (MAKE-LIST-AC N 1 NIL)
                    '((A B C D E F G H I J K L M N O P))))))))
  (AND (TRUE-LISTP NEWV)
       (EQUAL (LEN NEWV) 2)
       (INTEGERP (CAR NEWV))
       (SYMP (CADR NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (UNTIL$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (AND (RATIONAL-LISTP (CAR LOCALS))
                                        (IDENTITY (CAR LOCALS)))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS)) (Y (CADR LOCALS)))
        (PROG2$
         (PROG2$
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP X) (IDENTITY X))
                                 '(IF (RATIONAL-LISTP X)
                                      (IDENTITY X)
                                      'NIL))
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                                 '(IF (RATIONAL-LISTP Y)
                                      (IDENTITY Y)
                                      'NIL)))
         (EQUAL (CAR X) 9))))
      NIL
      (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                (TAILS (MAKE-LIST-AC N 1/3 NIL))))))
    (LEN
     (UNTIL$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (AND (RATIONAL-LISTP (CAR LOCALS))
                                        (IDENTITY (CAR LOCALS)))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS)) (Y (CADR LOCALS)))
        (PROG2$
         (PROG2$
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP X) (IDENTITY X))
                                 '(IF (RATIONAL-LISTP X)
                                      (IDENTITY X)
                                      'NIL))
             (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                                 '(IF (RATIONAL-LISTP Y)
                                      (IDENTITY Y)
                                      'NIL)))
         (EQUAL (CAR X) 9))))
      NIL
      (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                (TAILS (MAKE-LIST-AC N 1/3 NIL))))))))
  (AND (TRUE-LISTP NEWV)
       (EQUAL (LEN NEWV) 2)
       (AND (RATIONAL-LISTP (CAR NEWV))
            (IDENTITY (CAR NEWV)))
       (RATIONAL-LISTP (CADR NEWV))
       (IDENTITY (CADR NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (< (MEMPOS NEWV
              (WHEN$ (LAMBDA$ (X)
                              (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                       (IGNORABLE X)
                                       (XARGS :GUARD (TRUE-LISTP X)
                                              :SPLIT-TYPES T))
                              (NOT (EQUAL (CAR X) 7)))
                     (TAILS (MAKE-LIST-AC N 1 NIL))))
      (LEN (WHEN$ (LAMBDA$ (X)
                           (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                    (IGNORABLE X)
                                    (XARGS :GUARD (TRUE-LISTP X)
                                           :SPLIT-TYPES T))
                           (NOT (EQUAL (CAR X) 7)))
                  (TAILS (MAKE-LIST-AC N 1 NIL))))))
  (TRUE-LISTP
       (APPLY$ (LAMBDA$ (X)
                        (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                 (IGNORABLE X)
                                 (XARGS :GUARD (TRUE-LISTP X)
                                        :SPLIT-TYPES T))
                        X)
               (LIST NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (< (MEMPOS NEWV
              (WHEN$ (LAMBDA$ (X)
                              (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                       (IGNORABLE X)
                                       (XARGS :GUARD (TRUE-LISTP X)
                                              :SPLIT-TYPES T))
                              (NOT (EQUAL (CAR X) 7)))
                     (TAILS (MAKE-LIST-AC N 1 NIL))))
      (LEN (WHEN$ (LAMBDA$ (X)
                           (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                    (IGNORABLE X)
                                    (XARGS :GUARD (TRUE-LISTP X)
                                           :SPLIT-TYPES T))
                           (NOT (EQUAL (CAR X) 7)))
                  (TAILS (MAKE-LIST-AC N 1 NIL))))))
  (TRUE-LISTP NEWV))
 (IMPLIES
  (AND
   (NATP N)
   (< (MEMPOS NEWV
              (WHEN$ (LAMBDA$ (X)
                              (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                       (IGNORABLE X)
                                       (XARGS :GUARD (TRUE-LISTP X)
                                              :SPLIT-TYPES T))
                              (NOT (EQUAL (CAR X) 7)))
                     (TAILS (MAKE-LIST-AC N 1 NIL))))
      (LEN (WHEN$ (LAMBDA$ (X)
                           (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                    (IGNORABLE X)
                                    (XARGS :GUARD (TRUE-LISTP X)
                                           :SPLIT-TYPES T))
                           (NOT (EQUAL (CAR X) 7)))
                  (TAILS (MAKE-LIST-AC N 1 NIL))))))
  (ACL2-NUMBERP
       (APPLY$ (LAMBDA$ (X)
                        (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                 (IGNORABLE X)
                                 (XARGS :GUARD (TRUE-LISTP X)
                                        :SPLIT-TYPES T))
                        (LENGTH X))
               (LIST NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (INTEGERP (CAR LOCALS))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                         '(INTEGERP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (OR (<= X 6) (<= (CAR RATTAIL) 7)))))
      NIL
      (AS (LIST (FROM-TO-BY 1 N 1)
                (TAILS (MAKE-LIST-AC N 1/2 NIL))))))
    (LEN
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (INTEGERP (CAR LOCALS))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                         '(INTEGERP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (OR (<= X 6) (<= (CAR RATTAIL) 7)))))
      NIL
      (AS (LIST (FROM-TO-BY 1 N 1)
                (TAILS (MAKE-LIST-AC N 1/2 NIL))))))))
  (AND (TRUE-LISTP NEWV)
       (EQUAL (LEN NEWV) 2)
       (INTEGERP (CAR NEWV))
       (RATIONAL-LISTP (CADR NEWV))
       (IDENTITY (CADR NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (INTEGERP (CAR LOCALS))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                         '(INTEGERP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (OR (<= X 6) (<= (CAR RATTAIL) 7)))))
      NIL
      (AS (LIST (FROM-TO-BY 1 N 1)
                (TAILS (MAKE-LIST-AC N 1/2 NIL))))))
    (LEN
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (INTEGERP (CAR LOCALS))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                         '(INTEGERP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (OR (<= X 6) (<= (CAR RATTAIL) 7)))))
      NIL
      (AS (LIST (FROM-TO-BY 1 N 1)
                (TAILS (MAKE-LIST-AC N 1/2 NIL))))))))
  (TRUE-LISTP
   (APPLY$
    (LAMBDA$
     (LOCALS GLOBALS)
     (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                 (EQUAL (LEN LOCALS) 2)
                                 (TRUE-LISTP GLOBALS)
                                 (EQUAL (LEN GLOBALS) 0)
                                 (INTEGERP (CAR LOCALS))
                                 (RATIONAL-LISTP (CADR LOCALS))
                                 (IDENTITY (CADR LOCALS)))
                     :SPLIT-TYPES T)
              (IGNORE GLOBALS))
     (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                         '(INTEGERP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (CONS X RATTAIL))))
    (CONS NEWV '(NIL)))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (INTEGERP (CAR LOCALS))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                         '(INTEGERP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (OR (<= X 6) (<= (CAR RATTAIL) 7)))))
      NIL
      (AS (LIST (FROM-TO-BY 1 N 1)
                (TAILS (MAKE-LIST-AC N 1/2 NIL))))))
    (LEN
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (INTEGERP (CAR LOCALS))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                         '(INTEGERP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (OR (<= X 6) (<= (CAR RATTAIL) 7)))))
      NIL
      (AS (LIST (FROM-TO-BY 1 N 1)
                (TAILS (MAKE-LIST-AC N 1/2 NIL))))))))
  (ACL2-NUMBERP
   (APPLY$
    (LAMBDA$
     (LOCALS GLOBALS)
     (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                 (EQUAL (LEN LOCALS) 2)
                                 (TRUE-LISTP GLOBALS)
                                 (EQUAL (LEN GLOBALS) 0)
                                 (INTEGERP (CAR LOCALS))
                                 (RATIONAL-LISTP (CADR LOCALS))
                                 (IDENTITY (CADR LOCALS)))
                     :SPLIT-TYPES T)
              (IGNORE GLOBALS))
     (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                         '(INTEGERP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (+ X (CAR RATTAIL)))))
    (CONS NEWV '(NIL)))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (WHEN$+
      (LAMBDA$
           (LOCALS GLOBALS)
           (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                       (EQUAL (LEN LOCALS) 2)
                                       (TRUE-LISTP GLOBALS)
                                       (EQUAL (LEN GLOBALS) 0)
                                       (INTEGERP (CAR LOCALS))
                                       (RATIONALP (CADR LOCALS)))
                           :SPLIT-TYPES T)
                    (IGNORE GLOBALS))
           (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                    '(RATIONALP Y)))
                        (NOT (EQUAL Y 7)))))
      NIL
      (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (FROM-TO-BY 1 N 1)
                  (MAKE-LIST-AC N 1 NIL))))))
    (LEN
     (WHEN$+
      (LAMBDA$
           (LOCALS GLOBALS)
           (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                       (EQUAL (LEN LOCALS) 2)
                                       (TRUE-LISTP GLOBALS)
                                       (EQUAL (LEN GLOBALS) 0)
                                       (INTEGERP (CAR LOCALS))
                                       (RATIONALP (CADR LOCALS)))
                           :SPLIT-TYPES T)
                    (IGNORE GLOBALS))
           (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                    '(RATIONALP Y)))
                        (NOT (EQUAL Y 7)))))
      NIL
      (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (FROM-TO-BY 1 N 1)
                  (MAKE-LIST-AC N 1 NIL))))))))
  (ACL2-NUMBERP
   (APPLY$
    (LAMBDA$ (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          X)))
    (CONS NEWV '(NIL)))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (WHEN$+
      (LAMBDA$
           (LOCALS GLOBALS)
           (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                       (EQUAL (LEN LOCALS) 2)
                                       (TRUE-LISTP GLOBALS)
                                       (EQUAL (LEN GLOBALS) 0)
                                       (INTEGERP (CAR LOCALS))
                                       (RATIONALP (CADR LOCALS)))
                           :SPLIT-TYPES T)
                    (IGNORE GLOBALS))
           (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                    '(RATIONALP Y)))
                        (NOT (EQUAL Y 7)))))
      NIL
      (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (FROM-TO-BY 1 N 1)
                  (MAKE-LIST-AC N 1 NIL))))))
    (LEN
     (WHEN$+
      (LAMBDA$
           (LOCALS GLOBALS)
           (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                       (EQUAL (LEN LOCALS) 2)
                                       (TRUE-LISTP GLOBALS)
                                       (EQUAL (LEN GLOBALS) 0)
                                       (INTEGERP (CAR LOCALS))
                                       (RATIONALP (CADR LOCALS)))
                           :SPLIT-TYPES T)
                    (IGNORE GLOBALS))
           (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                    '(RATIONALP Y)))
                        (NOT (EQUAL Y 7)))))
      NIL
      (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (FROM-TO-BY 1 N 1)
                  (MAKE-LIST-AC N 1 NIL))))))))
  (AND (TRUE-LISTP NEWV)
       (EQUAL (LEN NEWV) 2)
       (INTEGERP (CAR NEWV))
       (RATIONALP (CADR NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (WHEN$+
      (LAMBDA$
           (LOCALS GLOBALS)
           (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                       (EQUAL (LEN LOCALS) 2)
                                       (TRUE-LISTP GLOBALS)
                                       (EQUAL (LEN GLOBALS) 0)
                                       (INTEGERP (CAR LOCALS))
                                       (RATIONALP (CADR LOCALS)))
                           :SPLIT-TYPES T)
                    (IGNORE GLOBALS))
           (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                    '(RATIONALP Y)))
                        (NOT (EQUAL Y 7)))))
      NIL
      (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (FROM-TO-BY 1 N 1)
                  (MAKE-LIST-AC N 1 NIL))))))
    (LEN
     (WHEN$+
      (LAMBDA$
           (LOCALS GLOBALS)
           (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                       (EQUAL (LEN LOCALS) 2)
                                       (TRUE-LISTP GLOBALS)
                                       (EQUAL (LEN GLOBALS) 0)
                                       (INTEGERP (CAR LOCALS))
                                       (RATIONALP (CADR LOCALS)))
                           :SPLIT-TYPES T)
                    (IGNORE GLOBALS))
           (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                    '(RATIONALP Y)))
                        (NOT (EQUAL Y 7)))))
      NIL
      (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (FROM-TO-BY 1 N 1)
                  (MAKE-LIST-AC N 1 NIL))))))))
  (AND (TRUE-LISTP NEWV)
       (EQUAL (LEN NEWV) 2)
       (TRUE-LISTP (LIST N))
       (EQUAL (LEN (LIST N)) 1)
       (INTEGERP (CAR NEWV))
       (RATIONALP (CADR NEWV))
       (RATIONALP (CAR (LIST N)))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (WHEN$+
      (LAMBDA$
           (LOCALS GLOBALS)
           (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                       (EQUAL (LEN LOCALS) 2)
                                       (TRUE-LISTP GLOBALS)
                                       (EQUAL (LEN GLOBALS) 0)
                                       (INTEGERP (CAR LOCALS))
                                       (RATIONALP (CADR LOCALS)))
                           :SPLIT-TYPES T)
                    (IGNORE GLOBALS))
           (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                    '(RATIONALP Y)))
                        (NOT (EQUAL Y 7)))))
      NIL
      (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (FROM-TO-BY 1 N 1)
                  (MAKE-LIST-AC N 1 NIL))))))
    (LEN
     (WHEN$+
      (LAMBDA$
           (LOCALS GLOBALS)
           (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                       (EQUAL (LEN LOCALS) 2)
                                       (TRUE-LISTP GLOBALS)
                                       (EQUAL (LEN GLOBALS) 0)
                                       (INTEGERP (CAR LOCALS))
                                       (RATIONALP (CADR LOCALS)))
                           :SPLIT-TYPES T)
                    (IGNORE GLOBALS))
           (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                    '(RATIONALP Y)))
                        (NOT (EQUAL Y 7)))))
      NIL
      (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (FROM-TO-BY 1 N 1)
                  (MAKE-LIST-AC N 1 NIL))))))))
  (TRUE-LISTP
   (APPLY$
    (LAMBDA$ (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (LIST X Y))))
    (CONS NEWV '(NIL)))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (WHEN$+
      (LAMBDA$
           (LOCALS GLOBALS)
           (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                       (EQUAL (LEN LOCALS) 2)
                                       (TRUE-LISTP GLOBALS)
                                       (EQUAL (LEN GLOBALS) 0)
                                       (INTEGERP (CAR LOCALS))
                                       (RATIONALP (CADR LOCALS)))
                           :SPLIT-TYPES T)
                    (IGNORE GLOBALS))
           (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                    '(RATIONALP Y)))
                        (NOT (EQUAL Y 7)))))
      NIL
      (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (FROM-TO-BY 1 N 1)
                  (MAKE-LIST-AC N 1 NIL))))))
    (LEN
     (WHEN$+
      (LAMBDA$
           (LOCALS GLOBALS)
           (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                       (EQUAL (LEN LOCALS) 2)
                                       (TRUE-LISTP GLOBALS)
                                       (EQUAL (LEN GLOBALS) 0)
                                       (INTEGERP (CAR LOCALS))
                                       (RATIONALP (CADR LOCALS)))
                           :SPLIT-TYPES T)
                    (IGNORE GLOBALS))
           (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                    '(INTEGERP X))
                                (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                    '(RATIONALP Y)))
                        (NOT (EQUAL Y 7)))))
      NIL
      (UNTIL$+
        (LAMBDA$
             (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 0)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS)))
                             :SPLIT-TYPES T)
                      (IGNORE GLOBALS))
             (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (EQUAL X 9))))
        NIL
        (AS (LIST (FROM-TO-BY 1 N 1)
                  (MAKE-LIST-AC N 1 NIL))))))))
  (TRUE-LISTP
   (APPLY$
    (LAMBDA$ (LOCALS GLOBALS)
             (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                         (EQUAL (LEN LOCALS) 2)
                                         (TRUE-LISTP GLOBALS)
                                         (EQUAL (LEN GLOBALS) 1)
                                         (INTEGERP (CAR LOCALS))
                                         (RATIONALP (CADR LOCALS))
                                         (RATIONALP (CAR GLOBALS)))
                             :SPLIT-TYPES T))
             (LET ((X (CAR LOCALS))
                   (Y (CADR LOCALS))
                   (N (CAR GLOBALS)))
                  (PROG2$ (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                                      '(INTEGERP X))
                                  (CHECK-DCL-GUARDIAN (RATIONALP Y)
                                                      '(RATIONALP Y)))
                          (LIST X Y (+ 1 N)))))
    (LIST NEWV (LIST N)))))
 (IMPLIES (AND (NATP N)
               (< (MEMPOS NEWV
                          (AS (LIST (FROM-TO-BY 1 N 1)
                                    (MAKE-LIST-AC N 1 NIL))))
                  (LEN (AS (LIST (FROM-TO-BY 1 N 1)
                                 (MAKE-LIST-AC N 1 NIL))))))
          (AND (TRUE-LISTP NEWV)
               (EQUAL (LEN NEWV) 2)
               (INTEGERP (CAR NEWV))
               (RATIONALP (CADR NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (INTEGERP (CAR LOCALS))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                         '(INTEGERP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (AND (<= X 6) (<= (CAR RATTAIL) 7)))))
      NIL
      (AS (LIST (MAKE-LIST-AC N 1 NIL)
                (TAILS (MAKE-LIST-AC N 1/2 NIL))))))
    (LEN
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (INTEGERP (CAR LOCALS))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                         '(INTEGERP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (AND (<= X 6) (<= (CAR RATTAIL) 7)))))
      NIL
      (AS (LIST (MAKE-LIST-AC N 1 NIL)
                (TAILS (MAKE-LIST-AC N 1/2 NIL))))))))
  (TRUE-LISTP
   (APPLY$
    (LAMBDA$
     (LOCALS GLOBALS)
     (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                 (EQUAL (LEN LOCALS) 2)
                                 (TRUE-LISTP GLOBALS)
                                 (EQUAL (LEN GLOBALS) 0)
                                 (INTEGERP (CAR LOCALS))
                                 (RATIONAL-LISTP (CADR LOCALS))
                                 (IDENTITY (CADR LOCALS)))
                     :SPLIT-TYPES T)
              (IGNORE GLOBALS))
     (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                         '(INTEGERP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (CONS X RATTAIL))))
    (CONS NEWV '(NIL)))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (INTEGERP (CAR LOCALS))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                         '(INTEGERP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (AND (<= X 6) (<= (CAR RATTAIL) 7)))))
      NIL
      (AS (LIST (MAKE-LIST-AC N 1 NIL)
                (TAILS (MAKE-LIST-AC N 1/2 NIL))))))
    (LEN
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (INTEGERP (CAR LOCALS))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                         '(INTEGERP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (AND (<= X 6) (<= (CAR RATTAIL) 7)))))
      NIL
      (AS (LIST (MAKE-LIST-AC N 1 NIL)
                (TAILS (MAKE-LIST-AC N 1/2 NIL))))))))
  (AND (TRUE-LISTP NEWV)
       (EQUAL (LEN NEWV) 2)
       (INTEGERP (CAR NEWV))
       (RATIONAL-LISTP (CADR NEWV))
       (IDENTITY (CADR NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (<
    (MEMPOS
     NEWV
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (INTEGERP (CAR LOCALS))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                         '(INTEGERP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (AND (<= X 6) (<= (CAR RATTAIL) 7)))))
      NIL
      (AS (LIST (MAKE-LIST-AC N 1 NIL)
                (TAILS (MAKE-LIST-AC N 1/2 NIL))))))
    (LEN
     (WHEN$+
      (LAMBDA$
       (LOCALS GLOBALS)
       (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                   (EQUAL (LEN LOCALS) 2)
                                   (TRUE-LISTP GLOBALS)
                                   (EQUAL (LEN GLOBALS) 0)
                                   (INTEGERP (CAR LOCALS))
                                   (RATIONAL-LISTP (CADR LOCALS))
                                   (IDENTITY (CADR LOCALS)))
                       :SPLIT-TYPES T)
                (IGNORE GLOBALS))
       (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                         '(INTEGERP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (AND (<= X 6) (<= (CAR RATTAIL) 7)))))
      NIL
      (AS (LIST (MAKE-LIST-AC N 1 NIL)
                (TAILS (MAKE-LIST-AC N 1/2 NIL))))))))
  (ACL2-NUMBERP
   (APPLY$
    (LAMBDA$
     (LOCALS GLOBALS)
     (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOCALS)
                                 (EQUAL (LEN LOCALS) 2)
                                 (TRUE-LISTP GLOBALS)
                                 (EQUAL (LEN GLOBALS) 0)
                                 (INTEGERP (CAR LOCALS))
                                 (RATIONAL-LISTP (CADR LOCALS))
                                 (IDENTITY (CADR LOCALS)))
                     :SPLIT-TYPES T)
              (IGNORE GLOBALS))
     (LET
        ((X (CAR LOCALS))
         (RATTAIL (CADR LOCALS)))
        (PROG2$
             (PROG2$ (CHECK-DCL-GUARDIAN (INTEGERP X)
                                         '(INTEGERP X))
                     (CHECK-DCL-GUARDIAN (AND (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL))
                                         '(IF (RATIONAL-LISTP RATTAIL)
                                              (IDENTITY RATTAIL)
                                              'NIL)))
             (+ X (LENGTH RATTAIL)))))
    (CONS NEWV '(NIL)))))
 (IMPLIES
  (AND (NATP N)
       (< (MEMPOS NEWV
                  (UNTIL$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (EQUAL X 9))
                          (MAKE-LIST-AC N 1 NIL)))
          (LEN (UNTIL$ (LAMBDA$ (X)
                                (DECLARE (TYPE INTEGER X)
                                         (IGNORABLE X)
                                         (XARGS :GUARD (INTEGERP X)
                                                :SPLIT-TYPES T))
                                (EQUAL X 9))
                       (MAKE-LIST-AC N 1 NIL)))))
  (INTEGERP NEWV))
 (IMPLIES (AND (NATP N)
               (< (MEMPOS NEWV
                          (AS (LIST (MAKE-LIST-AC N 1 NIL)
                                    (MAKE-LIST-AC N 1 NIL))))
                  (LEN (AS (LIST (MAKE-LIST-AC N 1 NIL)
                                 (MAKE-LIST-AC N 1 NIL))))))
          (AND (TRUE-LISTP NEWV)
               (EQUAL (LEN NEWV) 2)
               (INTEGERP (CAR NEWV))
               (RATIONALP (CADR NEWV))))
 (IMPLIES
  (AND (NATP N)
       (< (MEMPOS NEWV
                  (UNTIL$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (EQUAL X 7))
                          (MAKE-LIST-AC N 1 NIL)))
          (LEN (UNTIL$ (LAMBDA$ (X)
                                (DECLARE (TYPE INTEGER X)
                                         (IGNORABLE X)
                                         (XARGS :GUARD (INTEGERP X)
                                                :SPLIT-TYPES T))
                                (EQUAL X 7))
                       (MAKE-LIST-AC N 1 NIL)))))
  (TRUE-LISTP (APPLY$ (LAMBDA$ (X)
                               (DECLARE (TYPE INTEGER X)
                                        (IGNORABLE X)
                                        (XARGS :GUARD (INTEGERP X)
                                               :SPLIT-TYPES T))
                               (LIST X))
                      (LIST NEWV))))
 (IMPLIES
  (AND (NATP N)
       (< (MEMPOS NEWV
                  (UNTIL$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (EQUAL X 7))
                          (MAKE-LIST-AC N 1 NIL)))
          (LEN (UNTIL$ (LAMBDA$ (X)
                                (DECLARE (TYPE INTEGER X)
                                         (IGNORABLE X)
                                         (XARGS :GUARD (INTEGERP X)
                                                :SPLIT-TYPES T))
                                (EQUAL X 7))
                       (MAKE-LIST-AC N 1 NIL)))))
  (INTEGERP NEWV))
 (IMPLIES
  (AND (NATP N)
       (< (MEMPOS NEWV
                  (UNTIL$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (EQUAL X 7))
                          (MAKE-LIST-AC N 1 NIL)))
          (LEN (UNTIL$ (LAMBDA$ (X)
                                (DECLARE (TYPE INTEGER X)
                                         (IGNORABLE X)
                                         (XARGS :GUARD (INTEGERP X)
                                                :SPLIT-TYPES T))
                                (EQUAL X 7))
                       (MAKE-LIST-AC N 1 NIL)))))
  (ACL2-NUMBERP (APPLY$ (LAMBDA$ (X)
                                 (DECLARE (TYPE INTEGER X)
                                          (IGNORABLE X)
                                          (XARGS :GUARD (INTEGERP X)
                                                 :SPLIT-TYPES T))
                                 X)
                        (LIST NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (< (MEMPOS
           NEWV
           (WHEN$ (LAMBDA$ (X)
                           (DECLARE (TYPE INTEGER X)
                                    (IGNORABLE X)
                                    (XARGS :GUARD (INTEGERP X)
                                           :SPLIT-TYPES T))
                           (NOT (EQUAL X 7)))
                  (UNTIL$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (EQUAL X 9))
                          (FROM-TO-BY 1 N 1))))
      (LEN (WHEN$ (LAMBDA$ (X)
                           (DECLARE (TYPE INTEGER X)
                                    (IGNORABLE X)
                                    (XARGS :GUARD (INTEGERP X)
                                           :SPLIT-TYPES T))
                           (NOT (EQUAL X 7)))
                  (UNTIL$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (EQUAL X 9))
                          (FROM-TO-BY 1 N 1))))))
  (TRUE-LISTP (APPLY$ (LAMBDA$ (X)
                               (DECLARE (TYPE INTEGER X)
                                        (IGNORABLE X)
                                        (XARGS :GUARD (INTEGERP X)
                                               :SPLIT-TYPES T))
                               (LIST X))
                      (LIST NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (< (MEMPOS
           NEWV
           (WHEN$ (LAMBDA$ (X)
                           (DECLARE (TYPE INTEGER X)
                                    (IGNORABLE X)
                                    (XARGS :GUARD (INTEGERP X)
                                           :SPLIT-TYPES T))
                           (NOT (EQUAL X 7)))
                  (UNTIL$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (EQUAL X 9))
                          (FROM-TO-BY 1 N 1))))
      (LEN (WHEN$ (LAMBDA$ (X)
                           (DECLARE (TYPE INTEGER X)
                                    (IGNORABLE X)
                                    (XARGS :GUARD (INTEGERP X)
                                           :SPLIT-TYPES T))
                           (NOT (EQUAL X 7)))
                  (UNTIL$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (EQUAL X 9))
                          (FROM-TO-BY 1 N 1))))))
  (ACL2-NUMBERP (APPLY$ (LAMBDA$ (X)
                                 (DECLARE (TYPE INTEGER X)
                                          (IGNORABLE X)
                                          (XARGS :GUARD (INTEGERP X)
                                                 :SPLIT-TYPES T))
                                 X)
                        (LIST NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (< (MEMPOS
           NEWV
           (WHEN$ (LAMBDA$ (X)
                           (DECLARE (TYPE INTEGER X)
                                    (IGNORABLE X)
                                    (XARGS :GUARD (INTEGERP X)
                                           :SPLIT-TYPES T))
                           (NOT (EQUAL X 7)))
                  (UNTIL$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (EQUAL X 9))
                          (FROM-TO-BY 1 N 1))))
      (LEN (WHEN$ (LAMBDA$ (X)
                           (DECLARE (TYPE INTEGER X)
                                    (IGNORABLE X)
                                    (XARGS :GUARD (INTEGERP X)
                                           :SPLIT-TYPES T))
                           (NOT (EQUAL X 7)))
                  (UNTIL$ (LAMBDA$ (X)
                                   (DECLARE (TYPE INTEGER X)
                                            (IGNORABLE X)
                                            (XARGS :GUARD (INTEGERP X)
                                                   :SPLIT-TYPES T))
                                   (EQUAL X 9))
                          (FROM-TO-BY 1 N 1))))))
  (INTEGERP NEWV))
 (IMPLIES
      (AND (NATP N)
           (< (MEMPOS NEWV (TAILS (MAKE-LIST-AC N 1 NIL)))
              (LEN (TAILS (MAKE-LIST-AC N 1 NIL)))))
      (ACL2-NUMBERP
           (APPLY$ (LAMBDA$ (X)
                            (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                     (IGNORABLE X)
                                     (XARGS :GUARD (TRUE-LISTP X)
                                            :SPLIT-TYPES T))
                            (LENGTH X))
                   (LIST NEWV))))
 (IMPLIES
      (AND (NATP N)
           (< (MEMPOS NEWV (TAILS (MAKE-LIST-AC N 1 NIL)))
              (LEN (TAILS (MAKE-LIST-AC N 1 NIL)))))
      (TRUE-LISTP
           (APPLY$ (LAMBDA$ (X)
                            (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                     (IGNORABLE X)
                                     (XARGS :GUARD (TRUE-LISTP X)
                                            :SPLIT-TYPES T))
                            X)
                   (LIST NEWV))))
 (IMPLIES (AND (NATP N)
               (< (MEMPOS NEWV (TAILS (MAKE-LIST-AC N 1 NIL)))
                  (LEN (TAILS (MAKE-LIST-AC N 1 NIL)))))
          (TRUE-LISTP NEWV))
 (IMPLIES
      (AND (NATP N)
           (< (MEMPOS NEWV
                      (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                                (TAILS (MAKE-LIST-AC N 1/2 NIL)))))
              (LEN (AS (LIST (TAILS (MAKE-LIST-AC N 1 NIL))
                             (TAILS (MAKE-LIST-AC N 1/2 NIL)))))))
      (AND (TRUE-LISTP NEWV)
           (EQUAL (LEN NEWV) 2)
           (TRUE-LISTP (CAR NEWV))
           (RATIONAL-LISTP (CADR NEWV))
           (IDENTITY (CADR NEWV))))
 (IMPLIES
  (AND
   (NATP N)
   (<
     (MEMPOS NEWV
             (UNTIL$ (LAMBDA$ (X)
                              (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                       (IGNORABLE X)
                                       (XARGS :GUARD (TRUE-LISTP X)
                                              :SPLIT-TYPES T))
                              (EQUAL (CAR X) 9))
                     (TAILS (MAKE-LIST-AC N 1 NIL))))
     (LEN (UNTIL$ (LAMBDA$ (X)
                           (DECLARE (TYPE (SATISFIES TRUE-LISTP) X)
                                    (IGNORABLE X)
                                    (XARGS :GUARD (TRUE-LISTP X)
                                           :SPLIT-TYPES T))
                           (EQUAL (CAR X) 9))
                  (TAILS (MAKE-LIST-AC N 1 NIL))))))
  (TRUE-LISTP NEWV))
 (IMPLIES
      (AND (NATP N)
           (< (MEMPOS NEWV
                      (AS (LIST (MAKE-LIST-AC N 1 NIL)
                                (TAILS (MAKE-LIST-AC N 1/2 NIL)))))
              (LEN (AS (LIST (MAKE-LIST-AC N 1 NIL)
                             (TAILS (MAKE-LIST-AC N 1/2 NIL)))))))
      (AND (TRUE-LISTP NEWV)
           (EQUAL (LEN NEWV) 2)
           (INTEGERP (CAR NEWV))
           (RATIONAL-LISTP (CADR NEWV))
           (IDENTITY (CADR NEWV))))
 (IMPLIES (AND (TRUE-LISTP LOCALS)
               (EQUAL (LEN LOCALS) 2)
               (TRUE-LISTP GLOBALS)
               (EQUAL (LEN GLOBALS) 0)
               (INTEGERP (CAR LOCALS))
               (SYMP (CADR LOCALS)))
          (LET ((X (CAR LOCALS)) (SYM (CADR LOCALS)))
               (AND (INTEGERP X)
                    (SYMBOLP SYM)
                    (OR (TRUE-LISTP (SYMBOL-NAME SYM))
                        (STRINGP (SYMBOL-NAME SYM)))
                    (ACL2-NUMBERP X)
                    (ACL2-NUMBERP (LENGTH (SYMBOL-NAME SYM)))
                    (RATIONALP (+ X (LENGTH (SYMBOL-NAME SYM)))))))
 (IMPLIES (AND (TRUE-LISTP LOCALS)
               (EQUAL (LEN LOCALS) 2)
               (TRUE-LISTP GLOBALS)
               (EQUAL (LEN GLOBALS) 0)
               (INTEGERP (CAR LOCALS))
               (SYMP (CADR LOCALS)))
          (LET ((X (CAR LOCALS)) (SYM (CADR LOCALS)))
               (AND (INTEGERP X)
                    (OR (EQUAL X 7) (SYMBOLP SYM)))))
 (IMPLIES (AND (TRUE-LISTP LOCALS)
               (EQUAL (LEN LOCALS) 2)
               (TRUE-LISTP GLOBALS)
               (EQUAL (LEN GLOBALS) 0)
               (INTEGERP (CAR LOCALS))
               (SYMP (CADR LOCALS)))
          (LET ((X (CAR LOCALS)) (SYM (CADR LOCALS)))
               (AND (INTEGERP X)
                    (SYMBOLP SYM)
                    (OR (TRUE-LISTP (SYMBOL-NAME SYM))
                        (STRINGP (SYMBOL-NAME SYM)))
                    (ACL2-NUMBERP X)
                    (ACL2-NUMBERP (LENGTH (SYMBOL-NAME SYM))))))
 (IMPLIES (AND (TRUE-LISTP LOCALS)
               (EQUAL (LEN LOCALS) 2)
               (TRUE-LISTP GLOBALS)
               (EQUAL (LEN GLOBALS) 0)
               (INTEGERP (CAR LOCALS))
               (RATIONAL-LISTP (CADR LOCALS))
               (IDENTITY (CADR LOCALS)))
          (LET ((X (CAR LOCALS))
                (RATTAIL (CADR LOCALS)))
               (AND (INTEGERP X)
                    (AND (RATIONAL-LISTP RATTAIL)
                         (IDENTITY RATTAIL))
                    (OR (TRUE-LISTP RATTAIL)
                        (STRINGP RATTAIL))
                    (ACL2-NUMBERP X)
                    (ACL2-NUMBERP (LENGTH RATTAIL)))))
 (IMPLIES (AND (TRUE-LISTP LOCALS)
               (EQUAL (LEN LOCALS) 2)
               (TRUE-LISTP GLOBALS)
               (EQUAL (LEN GLOBALS) 0)
               (INTEGERP (CAR LOCALS))
               (RATIONAL-LISTP (CADR LOCALS))
               (IDENTITY (CADR LOCALS)))
          (LET ((X (CAR LOCALS))
                (RATTAIL (CADR LOCALS)))
               (AND (INTEGERP X)
                    (AND (RATIONAL-LISTP RATTAIL)
                         (IDENTITY RATTAIL))
                    (RATIONALP X)
                    (OR (< 6 X) (RATIONALP X))
                    (OR (<= X 6)
                        (CONSP RATTAIL)
                        (EQUAL RATTAIL NIL))
                    (OR (<= X 6)
                        (RATIONALP (CAR RATTAIL))))))
 (IMPLIES (AND (TRUE-LISTP LOCALS)
               (EQUAL (LEN LOCALS) 2)
               (TRUE-LISTP GLOBALS)
               (EQUAL (LEN GLOBALS) 0)
               (INTEGERP (CAR LOCALS))
               (RATIONAL-LISTP (CADR LOCALS))
               (IDENTITY (CADR LOCALS)))
          (LET ((X (CAR LOCALS))
                (RATTAIL (CADR LOCALS)))
               (AND (INTEGERP X)
                    (AND (RATIONAL-LISTP RATTAIL)
                         (IDENTITY RATTAIL))
                    (OR (CONSP RATTAIL) (EQUAL RATTAIL NIL))
                    (ACL2-NUMBERP X)
                    (ACL2-NUMBERP (CAR RATTAIL)))))
 (IMPLIES (AND (TRUE-LISTP LOCALS)
               (EQUAL (LEN LOCALS) 2)
               (TRUE-LISTP GLOBALS)
               (EQUAL (LEN GLOBALS) 0)
               (INTEGERP (CAR LOCALS))
               (RATIONAL-LISTP (CADR LOCALS))
               (IDENTITY (CADR LOCALS)))
          (LET ((X (CAR LOCALS))
                (RATTAIL (CADR LOCALS)))
               (AND (INTEGERP X)
                    (AND (RATIONAL-LISTP RATTAIL)
                         (IDENTITY RATTAIL))
                    (RATIONALP X)
                    (OR (< 6 X)
                        (CONSP RATTAIL)
                        (EQUAL RATTAIL NIL))
                    (OR (< 6 X)
                        (RATIONALP (CAR RATTAIL))))))
 (IMPLIES (AND (TRUE-LISTP LOCALS)
               (EQUAL (LEN LOCALS) 2)
               (TRUE-LISTP GLOBALS)
               (EQUAL (LEN GLOBALS) 0)
               (TRUE-LISTP (CAR LOCALS))
               (RATIONAL-LISTP (CADR LOCALS))
               (IDENTITY (CADR LOCALS)))
          (LET ((X (CAR LOCALS))
                (RATTAIL (CADR LOCALS)))
               (AND (TRUE-LISTP X)
                    (AND (RATIONAL-LISTP RATTAIL)
                         (IDENTITY RATTAIL))
                    (OR (TRUE-LISTP X) (STRINGP X))
                    (RATIONALP (LENGTH X))
                    (OR (< 6 (LENGTH X))
                        (TRUE-LISTP X)
                        (STRINGP X))
                    (OR (< 6 (LENGTH X))
                        (RATIONALP (LENGTH X)))
                    (OR (<= (LENGTH X) 6)
                        (CONSP RATTAIL)
                        (EQUAL RATTAIL NIL))
                    (OR (<= (LENGTH X) 6)
                        (RATIONALP (CAR RATTAIL))))))
 (IMPLIES (AND (TRUE-LISTP LOCALS)
               (EQUAL (LEN LOCALS) 2)
               (TRUE-LISTP GLOBALS)
               (EQUAL (LEN GLOBALS) 0)
               (TRUE-LISTP (CAR LOCALS))
               (RATIONAL-LISTP (CADR LOCALS))
               (IDENTITY (CADR LOCALS)))
          (LET ((X (CAR LOCALS))
                (RATTAIL (CADR LOCALS)))
               (AND (TRUE-LISTP X)
                    (AND (RATIONAL-LISTP RATTAIL)
                         (IDENTITY RATTAIL))
                    (OR (TRUE-LISTP X) (STRINGP X))
                    (OR (CONSP RATTAIL) (EQUAL RATTAIL NIL))
                    (ACL2-NUMBERP (LENGTH X))
                    (ACL2-NUMBERP (CAR RATTAIL)))))
 (IMPLIES (AND (TRUE-LISTP LOCALS)
               (EQUAL (LEN LOCALS) 2)
               (TRUE-LISTP GLOBALS)
               (EQUAL (LEN GLOBALS) 0)
               (RATIONAL-LISTP (CAR LOCALS))
               (IDENTITY (CAR LOCALS))
               (RATIONAL-LISTP (CADR LOCALS))
               (IDENTITY (CADR LOCALS)))
          (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
               (AND (AND (RATIONAL-LISTP X) (IDENTITY X))
                    (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                    (OR (TRUE-LISTP X) (STRINGP X))
                    (OR (CONSP Y) (EQUAL Y NIL))
                    (ACL2-NUMBERP (LENGTH X))
                    (ACL2-NUMBERP (CAR Y)))))
 (IMPLIES (AND (TRUE-LISTP LOCALS)
               (EQUAL (LEN LOCALS) 2)
               (TRUE-LISTP GLOBALS)
               (EQUAL (LEN GLOBALS) 0)
               (RATIONAL-LISTP (CAR LOCALS))
               (IDENTITY (CAR LOCALS))
               (RATIONAL-LISTP (CADR LOCALS))
               (IDENTITY (CADR LOCALS)))
          (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
               (AND (AND (RATIONAL-LISTP X) (IDENTITY X))
                    (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                    (TRUE-LISTP X))))
 (IMPLIES (AND (TRUE-LISTP LOCALS)
               (EQUAL (LEN LOCALS) 2)
               (TRUE-LISTP GLOBALS)
               (EQUAL (LEN GLOBALS) 0)
               (RATIONAL-LISTP (CAR LOCALS))
               (IDENTITY (CAR LOCALS))
               (RATIONAL-LISTP (CADR LOCALS))
               (IDENTITY (CADR LOCALS)))
          (LET ((X (CAR LOCALS)) (Y (CADR LOCALS)))
               (AND (AND (RATIONAL-LISTP X) (IDENTITY X))
                    (AND (RATIONAL-LISTP Y) (IDENTITY Y))
                    (OR (CONSP X) (EQUAL X NIL)))))).
Subgoal 116
Subgoal 115
Subgoal 114
Subgoal 113
Subgoal 112
Subgoal 111
Subgoal 110
Subgoal 109
Subgoal 108
Subgoal 107
Subgoal 106
Subgoal 105
Subgoal 104
Subgoal 103
Subgoal 102
Subgoal 101
Subgoal 100
Subgoal 99
Subgoal 98
Subgoal 97
Subgoal 96
Subgoal 95
Subgoal 94
Subgoal 93
Subgoal 92
Subgoal 91
Subgoal 90
Subgoal 89
Subgoal 88
Subgoal 87
Subgoal 86
Subgoal 85
Subgoal 84
Subgoal 84'
Subgoal 83
Subgoal 82
Subgoal 81
Subgoal 80
Subgoal 80.2
Subgoal 80.1
Subgoal 79
Subgoal 79.4
Subgoal 79.3
Subgoal 79.2
Subgoal 79.1
Subgoal 78
Subgoal 77
Subgoal 76
Subgoal 75

Splitter note (see :DOC splitter) for Subgoal 75 (6 subgoals).
  if-intro: ((:DEFINITION FROM-TO-BY))

Subgoal 75.6
Subgoal 75.5
Subgoal 75.4
Subgoal 75.3
Subgoal 75.2
Subgoal 75.1
Subgoal 74
Subgoal 73
Subgoal 72
Subgoal 72'
Subgoal 71
Subgoal 71'
Subgoal 70

Splitter note (see :DOC splitter) for Subgoal 70 (5 subgoals).
  if-intro: ((:DEFINITION EV$-LIST-DEF)
             (:DEFINITION LEN)
             (:DEFINITION NOT)
             (:DEFINITION TRUE-LISTP)
             (:META APPLY$-PRIM-META-FN-CORRECT)
             (:REWRITE MEMPOS-UNTIL$+))

Subgoal 70.5
Subgoal 70.4
Subgoal 70.4.3
Subgoal 70.4.2
Subgoal 70.4.1
Subgoal 70.4.1'
Subgoal 70.3
Subgoal 70.2
Subgoal 70.1
Subgoal 70.1.3
Subgoal 70.1.2
Subgoal 70.1.1
Subgoal 69
Subgoal 68
Subgoal 67
Subgoal 67'
Subgoal 66
Subgoal 65

Splitter note (see :DOC splitter) for Subgoal 65 (5 subgoals).
  if-intro: ((:DEFINITION LEN)
             (:DEFINITION TRUE-LISTP)
             (:REWRITE MEMPOS-UNTIL$+))

Subgoal 65.5
Subgoal 65.4
Subgoal 65.4.2
Subgoal 65.4.1
Subgoal 65.3
Subgoal 65.2
Subgoal 65.1
Subgoal 65.1.2
Subgoal 65.1.1
Subgoal 64

Splitter note (see :DOC splitter) for Subgoal 64 (7 subgoals).
  if-intro: ((:DEFINITION EV$-LIST-DEF)
             (:DEFINITION LEN)
             (:DEFINITION NOT)
             (:DEFINITION TRUE-LISTP)
             (:META APPLY$-PRIM-META-FN-CORRECT)
             (:REWRITE MEMPOS-UNTIL$+))

Subgoal 64.7
Subgoal 64.6
Subgoal 64.5
Subgoal 64.4
Subgoal 64.4.3
Subgoal 64.4.2
Subgoal 64.4.1
Subgoal 64.3
Subgoal 64.2
Subgoal 64.2.3
Subgoal 64.2.2
Subgoal 64.2.1
Subgoal 64.1
Subgoal 63
Subgoal 62
Subgoal 62'
Subgoal 61
Subgoal 60
Subgoal 59
Subgoal 58
Subgoal 57
Subgoal 56

Splitter note (see :DOC splitter) for Subgoal 56 (4 subgoals).
  if-intro: ((:DEFINITION FROM-TO-BY))

Subgoal 56.4
Subgoal 56.3
Subgoal 56.2
Subgoal 56.1
Subgoal 55
Subgoal 54
Subgoal 53
Subgoal 52

Splitter note (see :DOC splitter) for Subgoal 52 (3 subgoals).
  if-intro: ((:DEFINITION EV$-LIST-DEF)
             (:DEFINITION LENGTH)
             (:DEFINITION NOT)
             (:META APPLY$-PRIM-META-FN-CORRECT)
             (:REWRITE EV$-OPENER))

Subgoal 52.3
Subgoal 52.2
Subgoal 52.1
Subgoal 51
Subgoal 50

Splitter note (see :DOC splitter) for Subgoal 50 (7 subgoals).
  if-intro: ((:DEFINITION EV$-LIST-DEF)
             (:DEFINITION LENGTH)
             (:DEFINITION NOT)
             (:META APPLY$-PRIM-META-FN-CORRECT)
             (:REWRITE EV$-OPENER))

Subgoal 50.7
Subgoal 50.6
Subgoal 50.5
Subgoal 50.4
Subgoal 50.3
Subgoal 50.2
Subgoal 50.1
Subgoal 49
Subgoal 48
Subgoal 48.2
Subgoal 48.1
Subgoal 47

Splitter note (see :DOC splitter) for Subgoal 47 (3 subgoals).
  if-intro: ((:DEFINITION SYMP))

Subgoal 47.3
Subgoal 47.2
Subgoal 47.1
Subgoal 46
Subgoal 45

Splitter note (see :DOC splitter) for Subgoal 45 (10 subgoals).
  if-intro: ((:DEFINITION FROM-TO-BY)
             (:DEFINITION LEN)
             (:DEFINITION TRUE-LISTP)
             (:REWRITE MEMPOS-UNTIL$+))

Subgoal 45.10
Subgoal 45.9
Subgoal 45.8
Subgoal 45.7
Subgoal 45.6
Subgoal 45.5
Subgoal 45.4
Subgoal 45.4.2
Subgoal 45.4.1
Subgoal 45.3
Subgoal 45.2
Subgoal 45.1
Subgoal 45.1.2
Subgoal 45.1.1
Subgoal 44
Subgoal 43
Subgoal 42
Subgoal 42'
Subgoal 41
Subgoal 40
Subgoal 39
Subgoal 38

Splitter note (see :DOC splitter) for Subgoal 38 (6 subgoals).
  if-intro: ((:DEFINITION LEN)
             (:DEFINITION SYMP)
             (:DEFINITION TRUE-LISTP)
             (:REWRITE MEMPOS-UNTIL$+))

Subgoal 38.6
Subgoal 38.5
Subgoal 38.5.2
Subgoal 38.5.1
Subgoal 38.4
Subgoal 38.3
Subgoal 38.2
Subgoal 38.2.2
Subgoal 38.2.1
Subgoal 38.1
Subgoal 37

Splitter note (see :DOC splitter) for Subgoal 37 (7 subgoals).
  if-intro: ((:DEFINITION LEN)
             (:DEFINITION TRUE-LISTP)
             (:REWRITE MEMPOS-UNTIL$+))

Subgoal 37.7
Subgoal 37.6
Subgoal 37.5
Subgoal 37.4
Subgoal 37.4.2
Subgoal 37.4.1
Subgoal 37.3
Subgoal 37.2
Subgoal 37.2.2
Subgoal 37.2.1
Subgoal 37.1
Subgoal 36
Subgoal 35
Subgoal 34
Subgoal 33

Splitter note (see :DOC splitter) for Subgoal 33 (12 subgoals).
  if-intro: ((:DEFINITION EV$-LIST-DEF)
             (:DEFINITION FROM-TO-BY)
             (:DEFINITION NOT)
             (:META APPLY$-PRIM-META-FN-CORRECT)
             (:REWRITE EV$-OPENER))

Subgoal 33.12
Subgoal 33.11
Subgoal 33.10
Subgoal 33.9
Subgoal 33.8
Subgoal 33.7
Subgoal 33.6
Subgoal 33.5
Subgoal 33.4
Subgoal 33.3
Subgoal 33.2
Subgoal 33.1
Subgoal 32

Splitter note (see :DOC splitter) for Subgoal 32 (2 subgoals).
  if-intro: ((:DEFINITION EV$-LIST-DEF)
             (:DEFINITION NOT)
             (:META APPLY$-PRIM-META-FN-CORRECT)
             (:REWRITE EV$-OPENER))

Subgoal 32.2
Subgoal 32.1
Subgoal 31
Subgoal 30
Subgoal 30'
Subgoal 29

Splitter note (see :DOC splitter) for Subgoal 29 (10 subgoals).
  if-intro: ((:DEFINITION EV$-LIST-DEF)
             (:DEFINITION FROM-TO-BY)
             (:DEFINITION LEN)
             (:DEFINITION NOT)
             (:DEFINITION TRUE-LISTP)
             (:META APPLY$-PRIM-META-FN-CORRECT)
             (:REWRITE MEMPOS-UNTIL$+))

Subgoal 29.10
Subgoal 29.9
Subgoal 29.8
Subgoal 29.7
Subgoal 29.6
Subgoal 29.5
Subgoal 29.4
Subgoal 29.4.3
Subgoal 29.4.2
Subgoal 29.4.1
Subgoal 29.4.1'
Subgoal 29.3
Subgoal 29.2
Subgoal 29.1
Subgoal 29.1.3
Subgoal 29.1.2
Subgoal 29.1.1
Subgoal 28

Splitter note (see :DOC splitter) for Subgoal 28 (10 subgoals).
  if-intro: ((:DEFINITION EV$-LIST-DEF)
             (:DEFINITION FROM-TO-BY)
             (:DEFINITION LEN)
             (:DEFINITION NOT)
             (:DEFINITION TRUE-LISTP)
             (:META APPLY$-PRIM-META-FN-CORRECT)
             (:REWRITE MEMPOS-UNTIL$+))

Subgoal 28.10
Subgoal 28.9
Subgoal 28.8
Subgoal 28.7
Subgoal 28.6
Subgoal 28.5
Subgoal 28.4
Subgoal 28.4.3
Subgoal 28.4.2
Subgoal 28.4.1
Subgoal 28.4.1'
Subgoal 28.3
Subgoal 28.2
Subgoal 28.1
Subgoal 28.1.3
Subgoal 28.1.2
Subgoal 28.1.1
Subgoal 27
Subgoal 26
Subgoal 25

Splitter note (see :DOC splitter) for Subgoal 25 (4 subgoals).
  if-intro: ((:DEFINITION FROM-TO-BY))

Subgoal 25.4
Subgoal 25.3
Subgoal 25.2
Subgoal 25.1
Subgoal 24
Subgoal 24'
Subgoal 23

Splitter note (see :DOC splitter) for Subgoal 23 (3 subgoals).
  if-intro: ((:DEFINITION EV$-LIST-DEF)
             (:DEFINITION NOT)
             (:META APPLY$-PRIM-META-FN-CORRECT)
             (:REWRITE EV$-OPENER))

Subgoal 23.3
Subgoal 23.2
Subgoal 23.1
Subgoal 22
Subgoal 21
Subgoal 20
Subgoal 20.2
Subgoal 20.1
Subgoal 19
Subgoal 18
Subgoal 17
Subgoal 17'
Subgoal 16
Subgoal 15
Subgoal 15'
Subgoal 14
Subgoal 13
Subgoal 12
Subgoal 11
Subgoal 10
Subgoal 10.3
Subgoal 10.2
Subgoal 10.1
Subgoal 9
Subgoal 8
Subgoal 8.3
Subgoal 8.2
Subgoal 8.1
Subgoal 7
Subgoal 7'
Subgoal 6
Subgoal 6'
Subgoal 5
Subgoal 5'
Subgoal 4
Subgoal 4'
Subgoal 3
Subgoal 3'
Subgoal 2
Subgoal 2'
Subgoal 1

Q.E.D.

That completes the proof of the guard theorem for TEST.  TEST
is compliant with Common Lisp.

Summary
Form:  ( DEFUN TEST ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:DEFINITION ASSOC-EQUAL)
        (:DEFINITION BINARY-APPEND)
        (:DEFINITION CHECK-DCL-GUARDIAN)
        (:DEFINITION EV$-LIST-DEF)
        (:DEFINITION FROM-TO-BY)
        (:DEFINITION IDENTITY)
        (:DEFINITION INTEGER-LISTP)
        (:DEFINITION LEN)
        (:DEFINITION LENGTH)
        (:DEFINITION NATP)
        (:DEFINITION NOT)
        (:DEFINITION PAIRLIS$)
        (:DEFINITION RATIONAL-LISTP)
        (:DEFINITION RETURN-LAST)
        (:DEFINITION SUITABLY-TAMEP-LISTP)
        (:DEFINITION SYMP)
        (:DEFINITION SYNP)
        (:DEFINITION TAMEP)
        (:DEFINITION TRUE-LIST-LISTP)
        (:DEFINITION TRUE-LISTP)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART ACL2-NUMBER-LISTP)
        (:EXECUTABLE-COUNTERPART ALWAYS$)
        (:EXECUTABLE-COUNTERPART APPLY$-GUARD)
        (:EXECUTABLE-COUNTERPART APPLY$-PRIMP)
        (:EXECUTABLE-COUNTERPART AS)
        (:EXECUTABLE-COUNTERPART BADGE-PRIM)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONS)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART INTEGER-LISTP)
        (:EXECUTABLE-COUNTERPART INTEGERP)
        (:EXECUTABLE-COUNTERPART LAMBDA-OBJECT-BODY)
        (:EXECUTABLE-COUNTERPART LAMBDA-OBJECT-FORMALS)
        (:EXECUTABLE-COUNTERPART LAMBDA-OBJECT-SHAPEP)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART LENGTH)
        (:EXECUTABLE-COUNTERPART MAKE-LIST-AC)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART PAIRLIS$)
        (:EXECUTABLE-COUNTERPART RATIONAL-LISTP)
        (:EXECUTABLE-COUNTERPART RATIONALP)
        (:EXECUTABLE-COUNTERPART SYMBOL-LISTP)
        (:EXECUTABLE-COUNTERPART SYMBOLP)
        (:EXECUTABLE-COUNTERPART TAILS)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:EXECUTABLE-COUNTERPART TRUE-LIST-LISTP)
        (:EXECUTABLE-COUNTERPART TRUE-LISTP)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING ACL2-NUMBER-LISTP-FORWARD-TO-TRUE-LISTP)
        (:FORWARD-CHAINING
             RATIONAL-LISTP-FORWARD-TO-ACL2-NUMBER-LISTP)
        (:LINEAR LEN-AS-CAR)
        (:LINEAR LEN-UNTIL$)
        (:LINEAR LEN-UNTIL$+)
        (:META APPLY$-PRIM-META-FN-CORRECT)
        (:REWRITE ACL2-NUMBER-LISTP-FROM-TO-BY)
        (:REWRITE ACL2-NUMBER-LISTP-IMPLIES-ACL2-NUMBERP)
        (:REWRITE ACL2-NUMBER-LISTP-IMPLIES-ALWAYS$-ACL2-NUMBERP)
        (:REWRITE ACL2-NUMBER-LISTP-MAKE-LIST)
        (:REWRITE ALWAYS-RATIONAL-LISTP-TAILS)
        (:REWRITE APPLY$-PRIMITIVE)
        (:REWRITE APPLY$-PRIMP-BADGE)
        (:REWRITE BETA-REDUCTION)
        (:REWRITE BETA-REDUCTION1)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE EQUAL-LEN-0)
        (:REWRITE EV$-OPENER)
        (:REWRITE FANCY-UQI-ACL2-NUMBER-1)
        (:REWRITE FANCY-UQI-IDENTITY-1)
        (:REWRITE FANCY-UQI-IDENTITY-2)
        (:REWRITE FANCY-UQI-INTEGER-1)
        (:REWRITE FANCY-UQI-RATIONAL-2)
        (:REWRITE FANCY-UQI-RATIONAL-LISTP-1)
        (:REWRITE FANCY-UQI-RATIONAL-LISTP-2)
        (:REWRITE FANCY-UQI-SYMBOL-2)
        (:REWRITE FANCY-UQI-TRUE-LIST-1)
        (:REWRITE FANCY-UQI-TRUE-LIST-2)
        (:REWRITE FOLD-CONSTS-IN-+)
        (:REWRITE INTEGER-LISTP-FROM-TO-BY)
        (:REWRITE INTEGER-LISTP-IMPLIES-ALWAYS$-INTEGERP)
        (:REWRITE INTEGER-LISTP-MAKE-LIST)
        (:REWRITE LEN-MEMPOS-AS)
        (:REWRITE MEMPOS-UNTIL$)
        (:REWRITE MEMPOS-UNTIL$+)
        (:REWRITE MEMPOS-WHEN$)
        (:REWRITE MEMPOS-WHEN$+)
        (:REWRITE NO-ELEMENT-TAILS-EMPTY)
        (:REWRITE PLAIN-UQI-ACL2-NUMBER-LISTP)
        (:REWRITE PLAIN-UQI-INTEGER-LISTP)
        (:REWRITE PLAIN-UQI-TRUE-LIST-LISTP)
        (:REWRITE RATIONAL-LISTP-MAKE-LIST)
        (:REWRITE STRUCTURE-OF-AS-ELEMENTS-BRIDGE)
        (:REWRITE TRUE-LIST-LISTP-AS)
        (:REWRITE TRUE-LIST-LISTP-IMPLIES-ALWAYS$-TRUE-LISTP)
        (:REWRITE TRUE-LIST-LISTP-IMPLIES-TRUE-LISTP)
        (:REWRITE TRUE-LIST-LISTP-TAILS)
        (:REWRITE TRUE-LIST-LISTP-UNTIL$+)
        (:REWRITE TRUE-LIST-LISTP-WHEN$+)
        (:REWRITE TRUE-LISTP-APPEND-REWRITE)
        (:REWRITE TRUE-LISTP-MAKE-LIST)
        (:TYPE-PRESCRIPTION ACL2-NUMBER-LISTP)
        (:TYPE-PRESCRIPTION FROM-TO-BY)
        (:TYPE-PRESCRIPTION LEN)
        (:TYPE-PRESCRIPTION LENGTH)
        (:TYPE-PRESCRIPTION MEMPOS)
        (:TYPE-PRESCRIPTION RATIONAL-LISTP)
        (:TYPE-PRESCRIPTION TAILS)
        (:TYPE-PRESCRIPTION UNTIL$)
        (:TYPE-PRESCRIPTION WHEN$))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION EV$-LIST-DEF)
             (:DEFINITION FROM-TO-BY)
             (:DEFINITION LEN)
             (:DEFINITION LENGTH)
             (:DEFINITION NOT)
             (:DEFINITION SYMP)
             (:DEFINITION TRUE-LISTP)
             (:META APPLY$-PRIM-META-FN-CORRECT)
             (:REWRITE EV$-OPENER)
             (:REWRITE MEMPOS-UNTIL$+))
Time:  13.72 seconds (prove: 13.05, print: 0.23, other: 0.45)
Prover steps counted:  7337383
 TEST
!>:pe TRUE-LIST-LISTP-UNTIL$+
   d       1  (INCLUDE-BOOK "/u/moore/Desktop/new-loop/loop-lemmas")
              \
              [Included books, outermost to innermost:
               "/Users/moore/Desktop/new-loop/loop-lemmas.lisp"
              ]
              \
>              (DEFTHM
                 TRUE-LIST-LISTP-UNTIL$+
                 (IMPLIES (TRUE-LIST-LISTP LST)
                          (TRUE-LIST-LISTP (UNTIL$+ FN GLOBALS LST))))
!>(----

Future Work

* Apply$ only works on logic mode functions so 
  it is an error if a program mode function appears
  in a loop$ body (or when or until) expression.

* Apply$ does not work on state- or stobj-using
  functions but there is nothing we can do about that!

* This is not allowed
  (defun foo (x)
    (if (atom x)
        (list x)
        (loop$ for y in x append (foo y))))

----)

!>(----

Future Work (continued)

* Some features of loop that can be formalized have not 
  been formalized yet e.g.

  (loop for i from 10 downto 1 maximize expr)

* Speed up execution at the top-level of the ACL2 loop!

----)

!>(---- The End ----)