~/acl2/devel/books/misc$ acl2
Welcome to Clozure Common Lisp Version 1.9-dev-r15422M-trunk  (DarwinX8664)!

 ACL2 Version 6.1 built March 25, 2013  21:11:46.
 Copyright (C) 2013, 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.

 WARNING: Do not redistribute.  This is NOT an ACL2 release; it is,
 rather, an svn distribution, $Revision: 938 $.
 The authors of ACL2 consider svn distributions to be experimental.

 Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*).
 See the documentation topic note-6-1 for recent changes.
 Note: We have modified the prompt in some underlying Lisps to further
 distinguish it from the ACL2 prompt.

ACL2 Version 6.1.  Level 1.  Cbd "/Users/kaufmann/acl2/devel/books/misc/".
System books directory "/Users/kaufmann/acl2/devel/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>(defstobj counters
	 (NodeCnt     :type integer :initially 0)
	 (TipCnt      :type integer :initially 0)
	 (IntTipsSeen :type t       :initially nil))

Summary
Form:  ( DEFSTOBJ COUNTERS ...)
Rules: NIL
Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
 COUNTERS
ACL2 !>counters
<counters>
ACL2 !>:q

Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
? [RAW LISP] *the-live-counters*
#( #(0)  #(0) NIL)
? [RAW LISP] (LP)

ACL2 Version 6.1.  Level 1.  Cbd "/Users/kaufmann/acl2/devel/books/misc/".
System books directory "/Users/kaufmann/acl2/devel/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>(NodeCnt counters)
0
ACL2 !>(thm (equal (create-counters)
		   '(0 0 nil)))

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION CREATE-COUNTERS)
        (:EXECUTABLE-COUNTERPART EQUAL))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  4

Proof succeeded.
ACL2 !>(update-NodeCnt 3 counters)
<counters>
ACL2 !>(NodeCnt counters)
3
ACL2 !>(defun show-counters (counters)

       ; Convert to ordinary object --
       ; note :stobjs declaration:

       ; Note output:
       ; (SHOW-COUNTERS COUNTERS) => *.

	 (declare (xargs :stobjs (counters)))
	 (list (NodeCnt counters)
	       (TipCnt counters)
	       (IntTipsSeen counters)))

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

(SHOW-COUNTERS COUNTERS) => *.

Computing the guard conjecture for SHOW-COUNTERS....

The guard conjecture for SHOW-COUNTERS is trivial to prove.  SHOW-COUNTERS
is compliant with Common Lisp.

Summary
Form:  ( DEFUN SHOW-COUNTERS ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 SHOW-COUNTERS
ACL2 !>(show-counters counters)
(3 0 NIL)
ACL2 !>(defun reset-counters (counters)
	 (declare (xargs :stobjs (counters)))

       ; Note that let binds only one stobj at a time.

	 (let ((counters (update-NodeCnt 0 counters)))
	   (let ((counters (update-TipCnt 0 counters)))
	     (update-IntTipsSeen nil counters))))

Since RESET-COUNTERS is non-recursive, its admission is trivial.  We
observe that the type of RESET-COUNTERS is described by the theorem
(CONSP (RESET-COUNTERS COUNTERS)).  We used the :type-prescription
rule UPDATE-INTTIPSSEEN.

(RESET-COUNTERS COUNTERS) => COUNTERS.

Computing the guard conjecture for RESET-COUNTERS....

The guard conjecture for RESET-COUNTERS is trivial to prove.  RESET-COUNTERS
is compliant with Common Lisp.

Summary
Form:  ( DEFUN RESET-COUNTERS ...)
Rules: ((:TYPE-PRESCRIPTION UPDATE-INTTIPSSEEN))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 RESET-COUNTERS
ACL2 !>(defun reset-counters2 (counters)
	 (declare (xargs :stobjs counters))

       ; This is also OK, by how let* macroexpands
       ; to a sequence of let forms.

	 (let* ((counters (update-NodeCnt 0 counters))
		(counters (update-TipCnt 0 counters))
		(counters (update-IntTipsSeen nil counters)))
	   counters))

Since RESET-COUNTERS2 is non-recursive, its admission is trivial. 
We observe that the type of RESET-COUNTERS2 is described by the theorem
(CONSP (RESET-COUNTERS2 COUNTERS)).  We used the :type-prescription
rule UPDATE-INTTIPSSEEN.

(RESET-COUNTERS2 COUNTERS) => COUNTERS.

Computing the guard conjecture for RESET-COUNTERS2....

The guard conjecture for RESET-COUNTERS2 is trivial to prove.  
RESET-COUNTERS2 is compliant with Common Lisp.

Summary
Form:  ( DEFUN RESET-COUNTERS2 ...)
Rules: ((:TYPE-PRESCRIPTION UPDATE-INTTIPSSEEN))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
 RESET-COUNTERS2
ACL2 !>(thm ; a check
	(equal (reset-counters counters)
	       (reset-counters2 counters)))

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION RESET-COUNTERS)
        (:DEFINITION RESET-COUNTERS2)
        (:DEFINITION UPDATE-INTTIPSSEEN)
        (:DEFINITION UPDATE-NODECNT)
        (:DEFINITION UPDATE-NTH)
        (:DEFINITION UPDATE-TIPCNT)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  264

Proof succeeded.
ACL2 !>(thm ; a check
	(equal (reset-counters counters)
	       (create-counters)))
Goal'
Goal''
Subgoal 4
Subgoal 3
Subgoal 2
Subgoal 1
Subgoal 1'

([ A key checkpoint:

Goal''
(NOT (CDDDR COUNTERS))

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.)

])

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

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION CREATE-COUNTERS)
        (:DEFINITION RESET-COUNTERS)
        (:DEFINITION UPDATE-INTTIPSSEEN)
        (:DEFINITION UPDATE-NODECNT)
        (:DEFINITION UPDATE-NTH)
        (:DEFINITION UPDATE-TIPCNT)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE CONS-EQUAL))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  426

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

*** Key checkpoint before reverting to proof by induction: ***

Goal''
(NOT (CDDDR COUNTERS))

ACL2 Error in ( THM ...):  See :DOC failure.

******** FAILED ********
ACL2 !>(thm
	(implies (countersp counters)
		 (equal (reset-counters counters)
			(create-counters))))
Goal'
Goal''
Goal'''
Goal'4'
Goal'5'

([ A key checkpoint:

Goal'''
(IMPLIES (AND (CONSP (CDR COUNTERS))
              (CONSP (CDDR COUNTERS))
              (TRUE-LISTP (CDDDR COUNTERS))
              (EQUAL (+ 1 1 1 (LEN (CDDDR COUNTERS)))
                     3)
              (CONSP COUNTERS)
              (INTEGERP (CAR COUNTERS))
              (INTEGERP (NTH *TIPCNT* COUNTERS)))
         (NOT (CDDDR COUNTERS)))

Normally we would attempt to prove Goal'5' 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.)

])

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

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION COUNTERSP)
        (:DEFINITION CREATE-COUNTERS)
        (:DEFINITION LEN)
        (:DEFINITION LENGTH)
        (:DEFINITION NODECNTP)
        (:DEFINITION NTH)
        (:DEFINITION RESET-COUNTERS)
        (:DEFINITION TIPCNTP)
        (:DEFINITION TRUE-LISTP)
        (:DEFINITION UPDATE-INTTIPSSEEN)
        (:DEFINITION UPDATE-NODECNT)
        (:DEFINITION UPDATE-NTH)
        (:DEFINITION UPDATE-TIPCNT)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE CONS-EQUAL)
        (:REWRITE NTH-0-CONS)
        (:REWRITE NTH-ADD1))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  1185

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

*** Key checkpoint before reverting to proof by induction: ***

Goal'''
(IMPLIES (AND (CONSP (CDR COUNTERS))
              (CONSP (CDDR COUNTERS))
              (TRUE-LISTP (CDDDR COUNTERS))
              (EQUAL (+ 1 1 1 (LEN (CDDDR COUNTERS)))
                     3)
              (CONSP COUNTERS)
              (INTEGERP (CAR COUNTERS))
              (INTEGERP (NTH *TIPCNT* COUNTERS)))
         (NOT (CDDDR COUNTERS)))

ACL2 Error in ( THM ...):  See :DOC failure.

******** FAILED ********
ACL2 !>(include-book "arithmetic/top" :dir :system)

Summary
Form:  ( INCLUDE-BOOK "arithmetic/top" ...)
Rules: NIL
Time:  0.21 seconds (prove: 0.00, print: 0.00, other: 0.21)
 "/Users/kaufmann/acl2/devel/books/arithmetic/top.lisp"
ACL2 !>(thm
	(implies (countersp counters)
		 (equal (reset-counters counters)
			(create-counters))))
Goal'
Goal''
Goal'''
Goal'4'
Goal'5'
Goal'6'

([ A key checkpoint:

Goal'4'
(IMPLIES (AND (CONSP (CDR COUNTERS))
              (CONSP (CDDR COUNTERS))
              (TRUE-LISTP (CDDDR COUNTERS))
              (EQUAL (LEN (CDDDR COUNTERS)) 0)
              (CONSP COUNTERS)
              (INTEGERP (CAR COUNTERS))
              (INTEGERP (CADR COUNTERS)))
         (NOT (CDDDR COUNTERS)))

Normally we would attempt to prove Goal'6' 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.)

])

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

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION COUNTERSP)
        (:DEFINITION CREATE-COUNTERS)
        (:DEFINITION LEN)
        (:DEFINITION LENGTH)
        (:DEFINITION NODECNTP)
        (:DEFINITION NTH)
        (:DEFINITION RESET-COUNTERS)
        (:DEFINITION SYNP)
        (:DEFINITION TIPCNTP)
        (:DEFINITION TRUE-LISTP)
        (:DEFINITION UPDATE-INTTIPSSEEN)
        (:DEFINITION UPDATE-NODECNT)
        (:DEFINITION UPDATE-NTH)
        (:DEFINITION UPDATE-TIPCNT)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART ACL2-NUMBERP)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART UNARY--)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE CONS-EQUAL)
        (:REWRITE EQUAL-CONSTANT-+)
        (:REWRITE FOLD-CONSTS-IN-+)
        (:TYPE-PRESCRIPTION LEN))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  1284

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

*** Key checkpoint before reverting to proof by induction: ***

Goal'4'
(IMPLIES (AND (CONSP (CDR COUNTERS))
              (CONSP (CDDR COUNTERS))
              (TRUE-LISTP (CDDDR COUNTERS))
              (EQUAL (LEN (CDDDR COUNTERS)) 0)
              (CONSP COUNTERS)
              (INTEGERP (CAR COUNTERS))
              (INTEGERP (CADR COUNTERS)))
         (NOT (CDDDR COUNTERS)))

ACL2 Error in ( THM ...):  See :DOC failure.

******** FAILED ********
ACL2 !>(create-counters)


ACL2 Error in TOP-LEVEL:  It is illegal to call CREATE-COUNTERS in
this context because it is a stobj creator.  Stobj creators cannot
be called directly except in theorems.  If you did not explicitly call
a stobj creator, then this error is probably due to an attempt to evaluate
a with-local-stobj form directly in the top-level loop.  Such forms
are only allowed in the bodies of functions and in theorems.  Also
see :DOC with-local-stobj.  Note:  this error occurred in the context
(CREATE-COUNTERS).

ACL2 !>Bye.
~/acl2/devel/books/misc$ acl2
Welcome to Clozure Common Lisp Version 1.9-dev-r15422M-trunk  (DarwinX8664)!

 ACL2 Version 6.1 built March 25, 2013  21:11:46.
 Copyright (C) 2013, 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.

 WARNING: Do not redistribute.  This is NOT an ACL2 release; it is,
 rather, an svn distribution, $Revision: 938 $.
 The authors of ACL2 consider svn distributions to be experimental.

 Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*).
 See the documentation topic note-6-1 for recent changes.
 Note: We have modified the prompt in some underlying Lisps to further
 distinguish it from the ACL2 prompt.

ACL2 Version 6.1.  Level 1.  Cbd "/Users/kaufmann/acl2/devel/books/misc/".
System books directory "/Users/kaufmann/acl2/devel/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>(include-book "eval") ; defines must-fail

Summary
Form:  ( INCLUDE-BOOK "eval" ...)
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 "/Users/kaufmann/acl2/devel/books/misc/eval.lisp"
ACL2 !>(defstobj sub1 sub1-fld1)

Summary
Form:  ( DEFSTOBJ SUB1 ...)
Rules: NIL
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
 SUB1
ACL2 !>(defstobj top1 (top1-fld :type sub1))

Summary
Form:  ( DEFSTOBJ TOP1 ...)
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 TOP1
ACL2 !>(must-fail
	(defun f (top1)
	  (declare (xargs :stobjs top1))
	  (top1-fld top1)))


ACL2 Error in ( DEFUN F ...):  It is illegal to call TOP1-FLD because
it is a stobj updater or accessor for a field of stobj type.  For a
way to generate such a call, see :DOC stobj-let.  Note:  this error
occurred in the context (TOP1-FLD TOP1).


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

ACL2 Error in ( DEFUN F ...):  See :DOC failure.

******** FAILED ********

Summary
Form:  ( MAKE-EVENT (STATE-GLOBAL-LET* ...) ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 T
ACL2 !>(must-fail
	(defun f (sub1 top1)
	  (declare (xargs :stobjs (sub1 top1)))
	  (update-top1-fld sub1 top1)))


ACL2 Error in ( DEFUN F ...):  It is illegal to call UPDATE-TOP1-FLD
because it is a stobj updater or accessor for a field of stobj type.
For a way to generate such a call, see :DOC stobj-let.  Note:  this
error occurred in the context (UPDATE-TOP1-FLD SUB1 TOP1).


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

ACL2 Error in ( DEFUN F ...):  See :DOC failure.

******** FAILED ********

Summary
Form:  ( MAKE-EVENT (STATE-GLOBAL-LET* ...) ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 T
ACL2 !>:trans1 (stobj-let
		((sub1 (top1-fld top1)))  ; bindings
		(sub1)                    ; producer variables
		(update-sub1-fld1 x sub1) ; producer
		top1)                     ; consumer
 (LET ((SUB1 (TOP1-FLD TOP1)))
      (DECLARE (IGNORABLE SUB1))
      (LET ((SUB1 (CHECK-VARS-NOT-FREE (TOP1)
                                       (UPDATE-SUB1-FLD1 X SUB1))))
           (LET* ((TOP1 (UPDATE-TOP1-FLD SUB1 TOP1)))
                 (CHECK-VARS-NOT-FREE (SUB1) TOP1))))
ACL2 !>(defun top1-fld.update-fld1 (x top1)
	 (declare (xargs :stobjs top1))
	 (stobj-let
	  ((sub1 (top1-fld top1)))
	  (sub1)
	  (update-sub1-fld1 x sub1)
	  top1))

Since TOP1-FLD.UPDATE-FLD1 is non-recursive, its admission is trivial.
We observe that the type of TOP1-FLD.UPDATE-FLD1 is described by the
theorem (CONSP (TOP1-FLD.UPDATE-FLD1 X TOP1)).  We used the :type-
prescription rule UPDATE-TOP1-FLD.

(TOP1-FLD.UPDATE-FLD1 * TOP1) => TOP1.

Computing the guard conjecture for TOP1-FLD.UPDATE-FLD1....

The non-trivial part of the guard conjecture for TOP1-FLD.UPDATE-FLD1
is

Goal
(IMPLIES (TOP1P TOP1)
         (LET* ((SUB1 (TOP1-FLD TOP1))
                (SUB1 (UPDATE-SUB1-FLD1 X SUB1)))
               (SUB1P SUB1))).
Goal'
Goal''

Q.E.D.

That completes the proof of the guard theorem for TOP1-FLD.UPDATE-FLD1.
TOP1-FLD.UPDATE-FLD1 is compliant with Common Lisp.

Summary
Form:  ( DEFUN TOP1-FLD.UPDATE-FLD1 ...)
Rules: ((:DEFINITION LEN)
        (:DEFINITION LENGTH)
        (:DEFINITION NOT)
        (:DEFINITION NTH)
        (:DEFINITION SUB1P)
        (:DEFINITION TOP1-FLD)
        (:DEFINITION TOP1-FLDP)
        (:DEFINITION TOP1P)
        (:DEFINITION TRUE-LISTP)
        (:DEFINITION UPDATE-NTH)
        (:DEFINITION UPDATE-SUB1-FLD1)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART LENGTH)
        (:EXECUTABLE-COUNTERPART NTH)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION UPDATE-TOP1-FLD))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.01)
Prover steps counted:  424
 TOP1-FLD.UPDATE-FLD1
ACL2 !>:trans1 (local-test
		; Here we 
		:defs
		((defun f1 (x top1)
		   (declare (xargs :stobjs top1))
		   (stobj-let
		    ((sub1 (top1-fld top1)))
		    (val)
		    (sub1-fld1 sub1)
		    (equal val x))))
		:run
		(top1-fld.update-fld1 17 top1)
		:check
		(f1 17 top1))


ACL2 Error in TOP-LEVEL:  TRANS1 may only be applied to a non-atom
form that begins with a symbol with a 'macro-body property.

ACL2 !>(defmacro local-test (&key defs run check)

; This is a convenient macro for our testing: evaluate defs (using progn rather
; than er-progn, so that we don't get a translate error in the make-event
; form), run a form, and then check that the check is true.

  `(make-event
    (progn
     ,@defs
     (make-event
      (er-progn (trans-eval ',run 'top state t)
                (assert-event ,check :on-skip-proofs t)
                (value '(value-triple '(value-triple :success))))))))

Summary
Form:  ( DEFMACRO LOCAL-TEST ...)
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 LOCAL-TEST
ACL2 !>:trans1 (local-test
		; Here we 
		:defs
		((defun f1 (x top1)
		   (declare (xargs :stobjs top1))
		   (stobj-let
		    ((sub1 (top1-fld top1)))
		    (val)
		    (sub1-fld1 sub1)
		    (equal val x))))
		:run
		(top1-fld.update-fld1 17 top1)
		:check
		(f1 17 top1))
 (MAKE-EVENT
  (PROGN
   (DEFUN F1 (X TOP1)
          (DECLARE (XARGS :STOBJS TOP1))
          (STOBJ-LET ((SUB1 (TOP1-FLD TOP1)))
                     (VAL)
                     (SUB1-FLD1 SUB1)
                     (EQUAL VAL X)))
   (MAKE-EVENT (ER-PROGN (TRANS-EVAL '(TOP1-FLD.UPDATE-FLD1 17 TOP1)
                                     'TOP
                                     STATE T)
                         (ASSERT-EVENT (F1 17 TOP1)
                                       :ON-SKIP-PROOFS T)
                         (VALUE '(VALUE-TRIPLE '(VALUE-TRIPLE :SUCCESS)))))))
ACL2 !>(local-test
; Here we 
 :defs
 ((defun f1 (x top1)
    (declare (xargs :stobjs top1))
    (stobj-let
     ((sub1 (top1-fld top1)))
     (val)
     (sub1-fld1 sub1)
     (equal val x))))
 :run
 (top1-fld.update-fld1 17 top1)
 :check
 (f1 17 top1))

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

(F1 * TOP1) => *.

Computing the guard conjecture for F1....

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

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

Summary
Form:  ( MAKE-EVENT (ER-PROGN ...))
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

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

Summary
Form:  ( MAKE-EVENT (PROGN ...))
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 :SUCCESS
ACL2 !>(defstobj sub1a sub1a-fld1 :congruent-to sub1)

Summary
Form:  ( DEFSTOBJ SUB1A ...)
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 SUB1A
ACL2 !>(defun new-top1-fld.update-fld1 (x top1)
; Note that use of a congruent stobj: sub1a in place of sub1.
  (declare (xargs :stobjs top1))
  (stobj-let
   ((sub1a (top1-fld top1)))
   (sub1a)
   (update-sub1-fld1 x sub1a)
   top1))

Since NEW-TOP1-FLD.UPDATE-FLD1 is non-recursive, its admission is trivial.
We observe that the type of NEW-TOP1-FLD.UPDATE-FLD1 is described by
the theorem (CONSP (NEW-TOP1-FLD.UPDATE-FLD1 X TOP1)).  We used the
:type-prescription rule UPDATE-TOP1-FLD.

(NEW-TOP1-FLD.UPDATE-FLD1 * TOP1) => TOP1.

Computing the guard conjecture for NEW-TOP1-FLD.UPDATE-FLD1....

The non-trivial part of the guard conjecture for NEW-TOP1-FLD.UPDATE-FLD1
is

Goal
(IMPLIES (TOP1P TOP1)
         (LET* ((SUB1A (TOP1-FLD TOP1))
                (SUB1A (UPDATE-SUB1-FLD1 X SUB1A)))
               (SUB1P SUB1A))).
Goal'
Goal''

Q.E.D.

That completes the proof of the guard theorem for NEW-TOP1-FLD.UPDATE-FLD1.
NEW-TOP1-FLD.UPDATE-FLD1 is compliant with Common Lisp.

Summary
Form:  ( DEFUN NEW-TOP1-FLD.UPDATE-FLD1 ...)
Rules: ((:DEFINITION LEN)
        (:DEFINITION LENGTH)
        (:DEFINITION NOT)
        (:DEFINITION NTH)
        (:DEFINITION SUB1P)
        (:DEFINITION TOP1-FLD)
        (:DEFINITION TOP1-FLDP)
        (:DEFINITION TOP1P)
        (:DEFINITION TRUE-LISTP)
        (:DEFINITION UPDATE-NTH)
        (:DEFINITION UPDATE-SUB1-FLD1)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART LENGTH)
        (:EXECUTABLE-COUNTERPART NTH)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION UPDATE-TOP1-FLD))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  424
 NEW-TOP1-FLD.UPDATE-FLD1
ACL2 !>(defstobj top2
; This stobj has two fields of the same type, which is fine.
  (top2-fld1 :type sub1)
  (top2-fld2 :type sub1))

Summary
Form:  ( DEFSTOBJ TOP2 ...)
Rules: NIL
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
 TOP2
ACL2 !>(defun top2.test1 (top2)
; In order to bind two stobjs to fields of the same type, we use a congruent
; stobj, binding sub1 and sub1a.
  (declare (xargs :stobjs top2))
  (stobj-let ((sub1 (top2-fld1 top2))
              (sub1a (top2-fld2 top2)))
             (sub1 sub1a)
             (let* ((sub1 (update-sub1-fld1 3 sub1))
                    (sub1a (update-sub1-fld1 4 sub1a)))
               (mv sub1 sub1a))
             top2))

Since TOP2.TEST1 is non-recursive, its admission is trivial.  We observe
that the type of TOP2.TEST1 is described by the theorem 
(CONSP (TOP2.TEST1 TOP2)).  We used the :type-prescription rule 
UPDATE-TOP2-FLD2.

(TOP2.TEST1 TOP2) => TOP2.

Computing the guard conjecture for TOP2.TEST1....

The non-trivial part of the guard conjecture for TOP2.TEST1 is

Goal
(IMPLIES (TOP2P TOP2)
         (LET ((SUB1 (TOP2-FLD1 TOP2))
               (SUB1A (TOP2-FLD2 TOP2)))
              (LET ((MV (LET* ((SUB1 (UPDATE-SUB1-FLD1 3 SUB1))
                               (SUB1A (UPDATE-SUB1-FLD1 4 SUB1A)))
                              (LIST SUB1 SUB1A))))
                   (LET ((SUB1 (MV-NTH 0 MV))
                         (SUB1A (MV-NTH 1 MV)))
                        (AND (SUB1P SUB1)
                             (LET NIL (SUB1P SUB1A))))))).
Goal'

Splitter note (see :DOC splitter) for Goal' (2 subgoals).
  if-intro: ((:DEFINITION NTH))

Subgoal 2
Subgoal 1

Q.E.D.

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

Summary
Form:  ( DEFUN TOP2.TEST1 ...)
Rules: ((:DEFINITION LEN)
        (:DEFINITION LENGTH)
        (:DEFINITION MV-NTH)
        (:DEFINITION NOT)
        (:DEFINITION NTH)
        (:DEFINITION SUB1P)
        (:DEFINITION TOP2-FLD1)
        (:DEFINITION TOP2-FLD1P)
        (:DEFINITION TOP2-FLD2)
        (:DEFINITION TOP2-FLD2P)
        (:DEFINITION TOP2P)
        (:DEFINITION TRUE-LISTP)
        (:DEFINITION UPDATE-NTH)
        (:DEFINITION UPDATE-SUB1-FLD1)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART LENGTH)
        (:EXECUTABLE-COUNTERPART NTH)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION UPDATE-TOP2-FLD2))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION NTH))
Time:  0.02 seconds (prove: 0.01, print: 0.00, other: 0.01)
Prover steps counted:  1044
 TOP2.TEST1
ACL2 !>(must-fail
; Error: This is just like top2.test1 above, except that this time the
; stobj-let bindings fail to include sub1a.
 (defun top2.test1-bad (top2)
   (declare (xargs :stobjs top2))
   (stobj-let ((sub1 (top2-fld1 top2)))
              (sub1 sub1a)
              (let* ((sub1 (update-sub1-fld1 3 sub1))
                     (sub1a (update-sub1-fld1 4 sub1a)))
                (mv sub1 sub1a))
              top2)))


ACL2 Error in ( DEFUN TOP2.TEST1-BAD ...):  It is illegal to invoke
UPDATE-SUB1-FLD1 here because of a signature mismatch.  This function
call returns a result of shape SUB1 where a result of shape * is required.
Note:  this error occurred in the context (UPDATE-SUB1-FLD1 4 SUB1A).


Summary
Form:  ( DEFUN TOP2.TEST1-BAD ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

ACL2 Error in ( DEFUN TOP2.TEST1-BAD ...):  See :DOC failure.

******** FAILED ********

Summary
Form:  ( MAKE-EVENT (STATE-GLOBAL-LET* ...) ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 T
ACL2 !>(must-fail
; Error: Same as top1-fld.update-fld1 and new-top1-fld.update-fld1, except that
; we operate on sub2 where we should be operating on sub1 or sub1a.  (Note that
; unlike sub1a, sub2 is not congruent to sub1.)
 (defun newer-top1-fld.update-fld1 (x top1)
  (declare (xargs :stobjs top1))
  (stobj-let
   ((sub2 (top1-fld top1)))
   (sub2)
   (update-sub1-fld1 x sub2)
   top1)))


ACL2 Error in ( DEFUN NEWER-TOP1-FLD.UPDATE-FLD1 ...):  The stobj-
let bound variable SUB2 is not the name of a known single-threaded
object in the current ACL2 world.  The form 
(STOBJ-LET ((SUB2 (TOP1-FLD TOP1))) (SUB2) (UPDATE-SUB1-FLD1 X SUB2) TOP1)
is thus illegal.  See :DOC stobj-let.


Summary
Form:  ( DEFUN NEWER-TOP1-FLD.UPDATE-FLD1 ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

ACL2 Error in ( DEFUN NEWER-TOP1-FLD.UPDATE-FLD1 ...):  See :DOC failure.

******** FAILED ********

Summary
Form:  ( MAKE-EVENT (STATE-GLOBAL-LET* ...) ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 T
ACL2 !>(defstobj sub2 sub2-fld1)

Summary
Form:  ( DEFSTOBJ SUB2 ...)
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 SUB2
ACL2 !>(must-fail
; Error: Same as top1-fld.update-fld1 and new-top1-fld.update-fld1, except that
; we operate on sub2 where we should be operating on sub1 or sub1a.  (Note that
; unlike sub1a, sub2 is not congruent to sub1.)
 (defun newer-top1-fld.update-fld1 (x top1)
  (declare (xargs :stobjs top1))
  (stobj-let
   ((sub2 (top1-fld top1)))
   (sub2)
   (update-sub1-fld1 x sub2)
   top1)))


ACL2 Error in ( DEFUN NEWER-TOP1-FLD.UPDATE-FLD1 ...):  The stobj-
let bound variable SUB2 is not the same as, or even congruent to, the
output SUB1 of accessor TOP1-FLD (of stobj TOP1).  The form 
(STOBJ-LET ((SUB2 (TOP1-FLD TOP1))) (SUB2) (UPDATE-SUB1-FLD1 X SUB2) TOP1)
is thus illegal.  See :DOC stobj-let.


Summary
Form:  ( DEFUN NEWER-TOP1-FLD.UPDATE-FLD1 ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

ACL2 Error in ( DEFUN NEWER-TOP1-FLD.UPDATE-FLD1 ...):  See :DOC failure.

******** FAILED ********

Summary
Form:  ( MAKE-EVENT (STATE-GLOBAL-LET* ...) ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 T
ACL2 !>(defstobj top3 (top3-fld :type (array sub1 (10))))

Summary
Form:  ( DEFSTOBJ TOP3 ...)
Rules: NIL
Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
 TOP3
ACL2 !>(defconst *i1* 1)

Summary
Form:  ( DEFCONST *I1* ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 *I1*
ACL2 !>(defconst *i1* 1)

The event ( DEFCONST *I1* ...) is redundant.  See :DOC redundant-events.

Summary
Form:  ( DEFCONST *I1* ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 :REDUNDANT
ACL2 !>(defconst *i2* 2)

Summary
Form:  ( DEFCONST *I2* ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 *I2*
ACL2 !>(local-test
; This is just a simple test of array update in a stobj field of a stobj.
; It uses constants just to make this a bit more interesting.
 :defs
 ((defun f1 (top3)
    (declare (xargs :stobjs top3))
    (stobj-let ((sub1 (top3-fldi *i1* top3))
                (sub1a (top3-fldi *i2* top3)))
               (sub1 sub1a)
               (let* ((sub1 (update-sub1-fld1 'x sub1))
                      (sub1a (update-sub1-fld1 'y sub1a)))
                 (mv sub1 sub1a))
               top3))
  (defun f2 (top3)
    (declare (xargs :stobjs top3))
    (stobj-let ((sub1 (top3-fldi *i1* top3))
                (sub1a (top3-fldi *i2* top3)))
               (val1 val2)
               (mv (sub1-fld1 sub1) (sub1-fld1 sub1a))
               (and (eq val1 'x)
                    (eq val2 'y)))))
 :run
 (f1 top3)
 :check
 (f2 top3))

Since F1 is non-recursive, its admission is trivial.  We observe that
the type of F1 is described by the theorem (CONSP (F1 TOP3)).  We used
the :type-prescription rule UPDATE-TOP3-FLDI.

(F1 TOP3) => TOP3.

Computing the guard conjecture for F1....

The non-trivial part of the guard conjecture for F1, given the :executable-
counterparts of CHK-NO-DUPLICATESP and CONS, is

Goal
(AND
    (IMPLIES (TOP3P TOP3)
             (< 1 (TOP3-FLD-LENGTH TOP3)))
    (IMPLIES (TOP3P TOP3)
             (LET ((SUB1 (TOP3-FLDI 1 TOP3))
                   (SUB1A (TOP3-FLDI 2 TOP3)))
                  (LET ((MV (LET* ((SUB1 (UPDATE-SUB1-FLD1 'X SUB1))
                                   (SUB1A (UPDATE-SUB1-FLD1 'Y SUB1A)))
                                  (LIST SUB1 SUB1A))))
                       (LET ((SUB1 (MV-NTH 0 MV))
                             (SUB1A (MV-NTH 1 MV)))
                            (AND (< 1 (TOP3-FLD-LENGTH TOP3))
                                 (SUB1P SUB1)
                                 (LET ((TOP3 (UPDATE-TOP3-FLDI 1 SUB1 TOP3)))
                                      (AND (< 2 (TOP3-FLD-LENGTH TOP3))
                                           (SUB1P SUB1A))))))))
    (IMPLIES (TOP3P TOP3)
             (< 2 (TOP3-FLD-LENGTH TOP3)))).
Goal'

Splitter note (see :DOC splitter) for Goal' (4 subgoals).
  if-intro: ((:DEFINITION NTH) (:DEFINITION SUB1P))

Subgoal 4
Subgoal 4'
Subgoal 4''

([ A key checkpoint:

Subgoal 4
(IMPLIES (AND (TRUE-LISTP TOP3)
              (EQUAL (LEN TOP3) 1)
              (CONSP TOP3)
              (TOP3-FLDP (CAR TOP3))
              (EQUAL (LEN (CAR TOP3)) 10))
         (TRUE-LISTP (CDR (NTH 1 (CAR TOP3)))))

*1 (Subgoal 4'') is pushed for proof by induction:
(IMPLIES (AND (TRUE-LISTP TOP5)
              (TRUE-LISTP (CONS TOP4 TOP5))
              (EQUAL (+ 1 (LEN TOP5)) 1)
              (TOP3-FLDP TOP4)
              (EQUAL (LEN TOP4) 10))
         (TRUE-LISTP (CDR (NTH 1 TOP4)))).

])
Subgoal 3
Subgoal 3'
Subgoal 3''

([ A key checkpoint:

Subgoal 3
(IMPLIES (AND (TRUE-LISTP TOP3)
              (EQUAL (LEN TOP3) 1)
              (CONSP TOP3)
              (TOP3-FLDP (CAR TOP3))
              (EQUAL (LEN (CAR TOP3)) 10))
         (TRUE-LISTP (CDR (NTH 2 (CAR TOP3)))))

*2 (Subgoal 3'') is pushed for proof by induction:
(IMPLIES (AND (TRUE-LISTP TOP5)
              (TRUE-LISTP (CONS TOP4 TOP5))
              (EQUAL (+ 1 (LEN TOP5)) 1)
              (TOP3-FLDP TOP4)
              (EQUAL (LEN TOP4) 10))
         (TRUE-LISTP (CDR (NTH 2 TOP4)))).

])
Subgoal 2
Subgoal 2'
Subgoal 2''

([ A key checkpoint:

Subgoal 2
(IMPLIES (AND (TRUE-LISTP TOP3)
              (EQUAL (LEN TOP3) 1)
              (CONSP TOP3)
              (TOP3-FLDP (CAR TOP3))
              (EQUAL (LEN (CAR TOP3)) 10))
         (EQUAL (+ 1 (LEN (CDR (NTH 1 (CAR TOP3)))))
                1))

*3 (Subgoal 2'') is pushed for proof by induction:
(IMPLIES (AND (TRUE-LISTP TOP5)
              (TRUE-LISTP (CONS TOP4 TOP5))
              (EQUAL (+ 1 (LEN TOP5)) 1)
              (TOP3-FLDP TOP4)
              (EQUAL (LEN TOP4) 10))
         (EQUAL (+ 1 (LEN (CDR (NTH 1 TOP4))))
                1)).

])
Subgoal 1
Subgoal 1'
Subgoal 1''

([ A key checkpoint:

Subgoal 1
(IMPLIES (AND (TRUE-LISTP TOP3)
              (EQUAL (LEN TOP3) 1)
              (CONSP TOP3)
              (TOP3-FLDP (CAR TOP3))
              (EQUAL (LEN (CAR TOP3)) 10))
         (EQUAL (+ 1 (LEN (CDR (NTH 2 (CAR TOP3)))))
                1))

*4 (Subgoal 1'') is pushed for proof by induction:
(IMPLIES (AND (TRUE-LISTP TOP5)
              (TRUE-LISTP (CONS TOP4 TOP5))
              (EQUAL (+ 1 (LEN TOP5)) 1)
              (TOP3-FLDP TOP4)
              (EQUAL (LEN TOP4) 10))
         (EQUAL (+ 1 (LEN (CDR (NTH 2 TOP4))))
                1)).

])

Perhaps we can prove *4 by induction.  Four induction schemes are suggested
by this conjecture.  Subsumption reduces that number to three.  These
merge into two derived induction schemes.  We will choose arbitrarily
among these.  

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

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

Subgoal *4/4''
(IMPLIES (AND (TOP3-FLDP TOP4)
              (EQUAL (LEN TOP4) 10))
         (EQUAL (+ 1 (LEN (CDR (NTH 2 TOP4))))
                1))

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

])
Subgoal *4/3
Subgoal *4/3'
Subgoal *4/2
Subgoal *4/1

So we now return to *4.1, which is

(IMPLIES (AND (TOP3-FLDP TOP4)
              (EQUAL (LEN TOP4) 10))
         (EQUAL (+ 1 (LEN (CDR (NTH 2 TOP4))))
                1)).
Subgoal *4.1/4
Subgoal *4.1/3
Subgoal *4.1/3'
Subgoal *4.1/3''
Subgoal *4.1/3'''

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

*4.1.2 (Subgoal *4.1/2'5') is pushed for proof by induction.
Subgoal *4.1/1

So we now return to *4.1.2, which is

(IMPLIES (AND (INTEGERP I)
              (<= 0 I)
              (NOT (EQUAL I 10))
              (TRUE-LISTP TOP5)
              (EQUAL (LEN TOP5) 1)
              (TOP3-FLDP TOP6)
              (EQUAL (+ 1 I) 10))
         (EQUAL (+ 1 (LEN (CDR (NTH 1 TOP6))))
                1)).
Subgoal *4.1.2/3
Subgoal *4.1.2/2
Subgoal *4.1.2/2'
Subgoal *4.1.2/2''
Subgoal *4.1.2/2'''
Subgoal *4.1.2/2'4'

*4.1.2.1 (Subgoal *4.1.2/2'4') is pushed for proof by induction.
Subgoal *4.1.2/1

So we now return to *4.1.2.1, which is

(IMPLIES (AND (EQUAL (LEN TOP8) 0)
              (INTEGERP I)
              (<= 0 I)
              (NOT (EQUAL I 10))
              (TRUE-LISTP TOP8)
              (TOP3-FLDP TOP6)
              (EQUAL (+ 1 I) 10))
         (EQUAL (+ 1 (LEN (CDR (NTH 1 TOP6))))
                1)).
Subgoal *4.1.2.1/3
Subgoal *4.1.2.1/3'
Subgoal *4.1.2.1/3''

*4.1.2.1.1 (Subgoal *4.1.2.1/3'') is pushed for proof by induction.
Subgoal *4.1.2.1/2
Subgoal *4.1.2.1/1

So we now return to *4.1.2.1.1, which is

(IMPLIES (AND (INTEGERP I)
              (<= 0 I)
              (NOT (EQUAL I 10))
              (TOP3-FLDP TOP6)
              (EQUAL (+ 1 I) 10))
         (EQUAL (+ 1 (LEN (CDR (NTH 1 TOP6))))
                1)).
Subgoal *4.1.2.1.1/4
Subgoal *4.1.2.1.1/4'
Subgoal *4.1.2.1.1/3
Subgoal *4.1.2.1.1/3'

Splitter note (see :DOC splitter) for Subgoal *4.1.2.1.1/3' (2 subgoals).
  if-intro: ((:DEFINITION NTH))

Subgoal *4.1.2.1.1/3.2
Subgoal *4.1.2.1.1/3.2.2
Subgoal *4.1.2.1.1/3.2.1
Subgoal *4.1.2.1.1/3.1
Subgoal *4.1.2.1.1/2
Subgoal *4.1.2.1.1/2'
Subgoal *4.1.2.1.1/1
Subgoal *4.1.2.1.1/1'

*4.1.2.1.1, *4.1.2.1 and *4.1.2 are COMPLETED!

We therefore turn our attention to *4.1.1, which is

(IMPLIES (AND (EQUAL (+ 1 (LEN (CDR (NTH 2 TOP6)))) 1)
              (TRUE-LISTP TOP5)
              (EQUAL (LEN TOP5) 1)
              (TOP3-FLDP TOP6)
              (EQUAL (+ 1 (LEN TOP6)) 10))
         (EQUAL (+ 1 (LEN (CDR (NTH 1 TOP6))))
                1)).
Subgoal *4.1.1/3
Subgoal *4.1.1/2
Subgoal *4.1.1/2'
Subgoal *4.1.1/2''
Subgoal *4.1.1/2'''
Subgoal *4.1.1/2'4'

*4.1.1.1 (Subgoal *4.1.1/2'4') is pushed for proof by induction.
Subgoal *4.1.1/1

So we now return to *4.1.1.1, which is

(IMPLIES (AND (EQUAL (LEN TOP8) 0)
              (EQUAL (+ 1 (LEN (CDR (NTH 2 TOP6)))) 1)
              (TRUE-LISTP TOP8)
              (TOP3-FLDP TOP6)
              (EQUAL (+ 1 (LEN TOP6)) 10))
         (EQUAL (+ 1 (LEN (CDR (NTH 1 TOP6))))
                1)).
Subgoal *4.1.1.1/3
Subgoal *4.1.1.1/3'
Subgoal *4.1.1.1/3''

*4.1.1.1.1 (Subgoal *4.1.1.1/3'') is pushed for proof by induction.
Subgoal *4.1.1.1/2
Subgoal *4.1.1.1/1

So we now return to *4.1.1.1.1, which is

(IMPLIES (AND (EQUAL (+ 1 (LEN (CDR (NTH 2 TOP6)))) 1)
              (TOP3-FLDP TOP6)
              (EQUAL (+ 1 (LEN TOP6)) 10))
         (EQUAL (+ 1 (LEN (CDR (NTH 1 TOP6))))
                1)).
Subgoal *4.1.1.1.1/5
Subgoal *4.1.1.1.1/4
Subgoal *4.1.1.1.1/4'
Subgoal *4.1.1.1.1/4''

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

Subgoal *4.1.1.1.1/4.2

*4.1.1.1.1.1 (Subgoal *4.1.1.1.1/4.2) is pushed for proof by induction.
Subgoal *4.1.1.1.1/4.1
Subgoal *4.1.1.1.1/3
Subgoal *4.1.1.1.1/3'
Subgoal *4.1.1.1.1/3''

Splitter note (see :DOC splitter) for Subgoal *4.1.1.1.1/3'' (2 subgoals).
  if-intro: ((:DEFINITION NTH))

Subgoal *4.1.1.1.1/3.2
Subgoal *4.1.1.1.1/3.2'
Subgoal *4.1.1.1.1/3.2''
Subgoal *4.1.1.1.1/3.2'''

*4.1.1.1.1.2 (Subgoal *4.1.1.1.1/3.2''') is pushed for proof by induction.
Subgoal *4.1.1.1.1/3.1
Subgoal *4.1.1.1.1/2
Subgoal *4.1.1.1.1/1
Subgoal *4.1.1.1.1/1'
Subgoal *4.1.1.1.1/1''

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

Subgoal *4.1.1.1.1/1.2

*4.1.1.1.1.3 (Subgoal *4.1.1.1.1/1.2) is pushed for proof by induction.
Subgoal *4.1.1.1.1/1.1

So we now return to *4.1.1.1.1.3, which is

(IMPLIES (AND (NOT (EQUAL (+ 1 (LEN (CDR (NTH 2 TOP8))))
                          1))
              (EQUAL (+ 1 (LEN (CDR (NTH 1 TOP8)))) 1)
              (TRUE-LISTP TOP7)
              (EQUAL (LEN TOP7) 1)
              (TOP3-FLDP TOP8)
              (EQUAL (+ 1 1 (LEN TOP8)) 10)
              (CONSP TOP8))
         (EQUAL (+ 1 (LEN (CDAR TOP8))) 1)).

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

We next consider *4.1.1.1.1.2, which is

(IMPLIES (AND (INTEGERP J)
              (< 0 J)
              (INTEGERP I)
              (<= 0 I)
              (NOT (EQUAL J 10))
              (EQUAL (+ 1 (LEN (CDR (NTH 1 TOP8)))) 1)
              (TRUE-LISTP TOP7)
              (EQUAL (LEN TOP7) 1)
              (TOP3-FLDP TOP8)
              (EQUAL (+ 1 J) 10)
              (CONSP TOP8))
         (EQUAL (+ 1 (LEN (CDAR TOP8))) 1)).
Subgoal *4.1.1.1.1.2/3
Subgoal *4.1.1.1.1.2/2
Subgoal *4.1.1.1.1.2/2'
Subgoal *4.1.1.1.1.2/2''
Subgoal *4.1.1.1.1.2/2.2
Subgoal *4.1.1.1.1.2/2.1
Subgoal *4.1.1.1.1.2/1

*4.1.1.1.1.2 is COMPLETED!

We therefore turn our attention to *4.1.1.1.1.1, which is

(IMPLIES (AND (EQUAL (+ 1 (LEN (CDR (NTH 1 TOP8)))) 1)
              (TRUE-LISTP TOP7)
              (EQUAL (LEN TOP7) 1)
              (TOP3-FLDP TOP8)
              (EQUAL (+ 1 1 (LEN TOP8)) 10)
              (CONSP TOP8))
         (EQUAL (+ 1 (LEN (CDAR TOP8))) 1)).
Subgoal *4.1.1.1.1.1/3
Subgoal *4.1.1.1.1.1/2
Subgoal *4.1.1.1.1.1/2'
Subgoal *4.1.1.1.1.1/2''
Subgoal *4.1.1.1.1.1/2.2
Subgoal *4.1.1.1.1.1/2.1
Subgoal *4.1.1.1.1.1/1

*4.1.1.1.1.1, *4.1.1.1.1, *4.1.1.1, *4.1.1, *4.1 and *4 are COMPLETED!
Thus key checkpoints Subgoal *4/4'' and Subgoal 1 are COMPLETED!

Perhaps we can prove *3 by induction.  Four induction schemes are suggested
by this conjecture.  Subsumption reduces that number to three.  These
merge into two derived induction schemes.  We will choose arbitrarily
among these.  

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

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

Subgoal *3/4''
(IMPLIES (AND (TOP3-FLDP TOP4)
              (EQUAL (LEN TOP4) 10))
         (EQUAL (+ 1 (LEN (CDR (NTH 1 TOP4))))
                1))

*3.1 (Subgoal *3/4'') is pushed for proof by induction.

])
Subgoal *3/3
Subgoal *3/3'
Subgoal *3/2
Subgoal *3/1

So we now return to *3.1, which is

(IMPLIES (AND (TOP3-FLDP TOP4)
              (EQUAL (LEN TOP4) 10))
         (EQUAL (+ 1 (LEN (CDR (NTH 1 TOP4))))
                1)).
Subgoal *3.1/4
Subgoal *3.1/3
Subgoal *3.1/3'
Subgoal *3.1/3''

Splitter note (see :DOC splitter) for Subgoal *3.1/3'' (2 subgoals).
  if-intro: ((:DEFINITION NTH))

Subgoal *3.1/3.2

*3.1.1 (Subgoal *3.1/3.2) is pushed for proof by induction.
Subgoal *3.1/3.1
Subgoal *3.1/2
Subgoal *3.1/2'
Subgoal *3.1/2''

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

Subgoal *3.1/2.2
Subgoal *3.1/2.2'
Subgoal *3.1/2.2''

*3.1.2 (Subgoal *3.1/2.2'') is pushed for proof by induction.
Subgoal *3.1/2.1
Subgoal *3.1/1

So we now return to *3.1.2, which is

(IMPLIES (AND (INTEGERP I)
              (<= 0 I)
              (NOT (EQUAL I 10))
              (TRUE-LISTP TOP5)
              (EQUAL (LEN TOP5) 1)
              (TOP3-FLDP TOP6)
              (EQUAL (+ 1 I) 10)
              (CONSP TOP6))
         (EQUAL (+ 1 (LEN (CDAR TOP6))) 1)).
Subgoal *3.1.2/3
Subgoal *3.1.2/2
Subgoal *3.1.2/2'
Subgoal *3.1.2/2''
Subgoal *3.1.2/2.2
Subgoal *3.1.2/2.1
Subgoal *3.1.2/1

*3.1.2 is COMPLETED!

We therefore turn our attention to *3.1.1, which is

(IMPLIES (AND (EQUAL (+ 1 (LEN (CDR (NTH 1 TOP6)))) 1)
              (TRUE-LISTP TOP5)
              (EQUAL (LEN TOP5) 1)
              (TOP3-FLDP TOP6)
              (EQUAL (+ 1 (LEN TOP6)) 10)
              (CONSP TOP6))
         (EQUAL (+ 1 (LEN (CDAR TOP6))) 1)).
Subgoal *3.1.1/3
Subgoal *3.1.1/2
Subgoal *3.1.1/2'
Subgoal *3.1.1/2''
Subgoal *3.1.1/2.2
Subgoal *3.1.1/2.1
Subgoal *3.1.1/1

*3.1.1, *3.1 and *3 are COMPLETED!
Thus key checkpoints Subgoal *3/4'' and Subgoal 2 are COMPLETED!

Perhaps we can prove *2 by induction.  Four induction schemes are suggested
by this conjecture.  Subsumption reduces that number to three.  These
merge into two derived induction schemes.  We will choose arbitrarily
among these.  

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

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

Subgoal *2/4''
(IMPLIES (AND (TOP3-FLDP TOP4)
              (EQUAL (LEN TOP4) 10))
         (TRUE-LISTP (CDR (NTH 2 TOP4))))

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

])
Subgoal *2/3
Subgoal *2/3'
Subgoal *2/2
Subgoal *2/1

So we now return to *2.1, which is

(IMPLIES (AND (TOP3-FLDP TOP4)
              (EQUAL (LEN TOP4) 10))
         (TRUE-LISTP (CDR (NTH 2 TOP4)))).
Subgoal *2.1/4
Subgoal *2.1/3
Subgoal *2.1/3'
Subgoal *2.1/3''
Subgoal *2.1/3'''
Subgoal *2.1/3'4'

*2.1.1 (Subgoal *2.1/3'4') is pushed for proof by induction.
Subgoal *2.1/2
Subgoal *2.1/2'
Subgoal *2.1/2''
Subgoal *2.1/2'''
Subgoal *2.1/2'4'
Subgoal *2.1/2'5'
Subgoal *2.1/2'6'

*2.1.2 (Subgoal *2.1/2'6') is pushed for proof by induction.
Subgoal *2.1/1

So we now return to *2.1.2, which is

(IMPLIES (AND (INTEGERP I)
              (<= 0 I)
              (NOT (EQUAL I 10))
              (TRUE-LISTP TOP5)
              (EQUAL (LEN TOP5) 1)
              (TOP3-FLDP TOP6)
              (EQUAL (+ 1 I) 10))
         (TRUE-LISTP (CDR (NTH 1 TOP6)))).
Subgoal *2.1.2/3
Subgoal *2.1.2/2
Subgoal *2.1.2/2'
Subgoal *2.1.2/2''
Subgoal *2.1.2/2'''
Subgoal *2.1.2/2'4'

*2.1.2.1 (Subgoal *2.1.2/2'4') is pushed for proof by induction.
Subgoal *2.1.2/1

So we now return to *2.1.2.1, which is

(IMPLIES (AND (EQUAL (LEN TOP8) 0)
              (INTEGERP I)
              (<= 0 I)
              (NOT (EQUAL I 10))
              (TRUE-LISTP TOP8)
              (TOP3-FLDP TOP6)
              (EQUAL (+ 1 I) 10))
         (TRUE-LISTP (CDR (NTH 1 TOP6)))).
Subgoal *2.1.2.1/3
Subgoal *2.1.2.1/3'
Subgoal *2.1.2.1/3''

*2.1.2.1.1 (Subgoal *2.1.2.1/3'') is pushed for proof by induction.
Subgoal *2.1.2.1/2
Subgoal *2.1.2.1/1

So we now return to *2.1.2.1.1, which is

(IMPLIES (AND (INTEGERP I)
              (<= 0 I)
              (NOT (EQUAL I 10))
              (TOP3-FLDP TOP6)
              (EQUAL (+ 1 I) 10))
         (TRUE-LISTP (CDR (NTH 1 TOP6)))).
Subgoal *2.1.2.1.1/4
Subgoal *2.1.2.1.1/4'
Subgoal *2.1.2.1.1/3
Subgoal *2.1.2.1.1/3'

Splitter note (see :DOC splitter) for Subgoal *2.1.2.1.1/3' (2 subgoals).
  if-intro: ((:DEFINITION NTH))

Subgoal *2.1.2.1.1/3.2
Subgoal *2.1.2.1.1/3.1
Subgoal *2.1.2.1.1/2
Subgoal *2.1.2.1.1/2'
Subgoal *2.1.2.1.1/1
Subgoal *2.1.2.1.1/1'

*2.1.2.1.1, *2.1.2.1 and *2.1.2 are COMPLETED!

We therefore turn our attention to *2.1.1, which is

(IMPLIES (AND (TRUE-LISTP (CDR (NTH 2 TOP6)))
              (TRUE-LISTP TOP5)
              (EQUAL (LEN TOP5) 1)
              (TOP3-FLDP TOP6)
              (EQUAL (+ 1 (LEN TOP6)) 10))
         (TRUE-LISTP (CDR (NTH 1 TOP6)))).
Subgoal *2.1.1/3
Subgoal *2.1.1/2
Subgoal *2.1.1/2'
Subgoal *2.1.1/2''
Subgoal *2.1.1/2'''
Subgoal *2.1.1/2'4'

*2.1.1.1 (Subgoal *2.1.1/2'4') is pushed for proof by induction.
Subgoal *2.1.1/1

So we now return to *2.1.1.1, which is

(IMPLIES (AND (EQUAL (LEN TOP8) 0)
              (TRUE-LISTP (CDR (NTH 2 TOP6)))
              (TRUE-LISTP TOP8)
              (TOP3-FLDP TOP6)
              (EQUAL (+ 1 (LEN TOP6)) 10))
         (TRUE-LISTP (CDR (NTH 1 TOP6)))).
Subgoal *2.1.1.1/3
Subgoal *2.1.1.1/3'
Subgoal *2.1.1.1/3''

*2.1.1.1.1 (Subgoal *2.1.1.1/3'') is pushed for proof by induction.
Subgoal *2.1.1.1/2
Subgoal *2.1.1.1/1

So we now return to *2.1.1.1.1, which is

(IMPLIES (AND (TRUE-LISTP (CDR (NTH 2 TOP6)))
              (TOP3-FLDP TOP6)
              (EQUAL (+ 1 (LEN TOP6)) 10))
         (TRUE-LISTP (CDR (NTH 1 TOP6)))).
Subgoal *2.1.1.1.1/5
Subgoal *2.1.1.1.1/4
Subgoal *2.1.1.1.1/4'
Subgoal *2.1.1.1.1/4''

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

Subgoal *2.1.1.1.1/4.2
Subgoal *2.1.1.1.1/4.1
Subgoal *2.1.1.1.1/3
Subgoal *2.1.1.1.1/3'
Subgoal *2.1.1.1.1/3''

Splitter note (see :DOC splitter) for Subgoal *2.1.1.1.1/3'' (2 subgoals).
  if-intro: ((:DEFINITION NTH))

Subgoal *2.1.1.1.1/3.2
Subgoal *2.1.1.1.1/3.1
Subgoal *2.1.1.1.1/2
Subgoal *2.1.1.1.1/1
Subgoal *2.1.1.1.1/1'
Subgoal *2.1.1.1.1/1''

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

Subgoal *2.1.1.1.1/1.2
Subgoal *2.1.1.1.1/1.1

*2.1.1.1.1, *2.1.1.1, *2.1.1, *2.1 and *2 are COMPLETED!
Thus key checkpoints Subgoal *2/4'' and Subgoal 3 are COMPLETED!

Perhaps we can prove *1 by induction.  Four induction schemes are suggested
by this conjecture.  Subsumption reduces that number to three.  These
merge into two derived induction schemes.  We will choose arbitrarily
among these.  

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

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

Subgoal *1/4''
(IMPLIES (AND (TOP3-FLDP TOP4)
              (EQUAL (LEN TOP4) 10))
         (TRUE-LISTP (CDR (NTH 1 TOP4))))

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

])
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/1

So we now return to *1.1, which is

(IMPLIES (AND (TOP3-FLDP TOP4)
              (EQUAL (LEN TOP4) 10))
         (TRUE-LISTP (CDR (NTH 1 TOP4)))).
Subgoal *1.1/4
Subgoal *1.1/3
Subgoal *1.1/3'
Subgoal *1.1/3''

Splitter note (see :DOC splitter) for Subgoal *1.1/3'' (2 subgoals).
  if-intro: ((:DEFINITION NTH))

Subgoal *1.1/3.2
Subgoal *1.1/3.1
Subgoal *1.1/2
Subgoal *1.1/2'
Subgoal *1.1/2''

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

Subgoal *1.1/2.2
Subgoal *1.1/2.1
Subgoal *1.1/1

*1.1 and *1 are COMPLETED!
Thus key checkpoints Subgoal *1/4'' and Subgoal 4 are COMPLETED!

Q.E.D.

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

Summary
Form:  ( DEFUN F1 ...)
Rules: ((:DEFINITION ATOM)
        (:DEFINITION LEN)
        (:DEFINITION LENGTH)
        (:DEFINITION MV-NTH)
        (:DEFINITION NOT)
        (:DEFINITION NTH)
        (:DEFINITION SUB1P)
        (:DEFINITION TOP3-FLD-LENGTH)
        (:DEFINITION TOP3-FLDI)
        (:DEFINITION TOP3-FLDP)
        (:DEFINITION TOP3P)
        (:DEFINITION TRUE-LISTP)
        (:DEFINITION UPDATE-NTH)
        (:DEFINITION UPDATE-SUB1-FLD1)
        (:DEFINITION UPDATE-TOP3-FLDI)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CHK-NO-DUPLICATESP)
        (:EXECUTABLE-COUNTERPART CONS)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART LENGTH)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART NTH)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:EXECUTABLE-COUNTERPART TRUE-LISTP)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION LEN)
        (:INDUCTION TOP3-FLDP)
        (:INDUCTION TRUE-LISTP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE NTH-ADD1)
        (:TYPE-PRESCRIPTION LEN)
        (:TYPE-PRESCRIPTION UPDATE-TOP3-FLDI))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION NTH) (:DEFINITION SUB1P))
Time:  0.35 seconds (prove: 0.29, print: 0.05, other: 0.00)
Prover steps counted:  45595

Since F2 is non-recursive, its admission is trivial.  We observe that
the type of F2 is described by the theorem 
(OR (EQUAL (F2 TOP3) T) (EQUAL (F2 TOP3) NIL)).  We used primitive
type reasoning.

(F2 TOP3) => *.

Computing the guard conjecture for F2....

The non-trivial part of the guard conjecture for F2, given the :executable-
counterparts of CHK-NO-DUPLICATESP and CONS, is

Goal
(AND (IMPLIES (TOP3P TOP3)
              (< 1 (TOP3-FLD-LENGTH TOP3)))
     (IMPLIES (TOP3P TOP3)
              (< 2 (TOP3-FLD-LENGTH TOP3)))).

Q.E.D.

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

Summary
Form:  ( DEFUN F2 ...)
Rules: ((:DEFINITION TOP3-FLD-LENGTH)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART CHK-NO-DUPLICATESP)
        (:EXECUTABLE-COUNTERPART CONS)
        (:EXECUTABLE-COUNTERPART IF)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
Prover steps counted:  22

Summary
Form:  ( MAKE-EVENT (ER-PROGN ...))
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Summary
Form:  ( PROGN (DEFUN F1 ...) ...)
Rules: NIL
Time:  0.36 seconds (prove: 0.29, print: 0.05, other: 0.02)
Prover steps counted:  45617

Summary
Form:  ( MAKE-EVENT (PROGN ...))
Rules: NIL
Time:  0.36 seconds (prove: 0.29, print: 0.05, other: 0.02)
Prover steps counted:  45617
 :SUCCESS
ACL2 !>(must-fail
; The producer updates a stobj field, but the parent stobj is not returned.
 (defun foo (top3)
   (declare (xargs :stobjs top3))
   (stobj-let ((sub1 (top3-fldi 5 top3)))
              (sub1)
              (update-sub1-fld1 'x sub1) ; producer
              (top3p top3))))


ACL2 Error in ( DEFUN FOO ...):  A STOBJ-LET form has been encountered
that specifies (with its list of producer variables) a call of stobj
updater UPDATE-TOP3-FLDI of TOP3.  It is therefore a requirement that
TOP3 be among the outputs of the STOBJ-LET, but it is not.  The STOBJ-
LET returns no single-threaded objects.  See :DOC stobj-let.  Note:
this error occurred in the context 
(STOBJ-LET ((SUB1 (TOP3-FLDI 5 TOP3)))
           (SUB1)
           (UPDATE-SUB1-FLD1 'X SUB1)
           (TOP3P TOP3)).



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

ACL2 Error in ( DEFUN FOO ...):  See :DOC failure.

******** FAILED ********

Summary
Form:  ( MAKE-EVENT (STATE-GLOBAL-LET* ...) ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 T
ACL2 !>(must-fail
; Don't allow the same index to occur twice.  Otherwise we get the problem
; shown in a comment just below.
 (defun foo (top3)
   (declare (xargs :stobjs top3))
   (stobj-let ((sub1 (top3-fldi (* 2 6) top3))
               (sub1a (top3-fldi 5 top3)))
              (sub1 sub1a)
              (let* ((sub1a (update-sub1-fld1 'x sub1a))
                     (sub1 (update-sub1-fld1 'y sub1)))
                (mv sub1 sub1a))
              top3)))


ACL2 Error in ( DEFUN FOO ...):  Illegal binding for stobj-let, 
(SUB1 (TOP3-FLDI (* 2 6) TOP3)).  The form 
(STOBJ-LET ((SUB1 (TOP3-FLDI (* 2 6) TOP3))
            (SUB1A (TOP3-FLDI 5 TOP3)))
           (SUB1 SUB1A)
           (LET* ((SUB1A (UPDATE-SUB1-FLD1 # SUB1A))
                  (SUB1 (UPDATE-SUB1-FLD1 # SUB1)))
                 (MV SUB1 SUB1A))
           TOP3)
is thus illegal.  See :DOC stobj-let.
(See :DOC set-iprint to be able to see elided values in this message.)


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

ACL2 Error in ( DEFUN FOO ...):  See :DOC failure.

******** FAILED ********

Summary
Form:  ( MAKE-EVENT (STATE-GLOBAL-LET* ...) ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 T
ACL2 !>(must-fail
; Don't allow the same index to occur twice.  Otherwise we get the problem
; shown in a comment just below.
 (defun foo (top3)
   (declare (xargs :stobjs top3))
   (stobj-let ((sub1 (top3-fldi (* 2 2) top3))
               (sub1a (top3-fldi 5 top3)))
              (sub1 sub1a)
              (let* ((sub1a (update-sub1-fld1 'x sub1a))
                     (sub1 (update-sub1-fld1 'y sub1)))
                (mv sub1 sub1a))
              top3)))


ACL2 Error in ( DEFUN FOO ...):  Illegal binding for stobj-let, 
(SUB1 (TOP3-FLDI (* 2 2) TOP3)).  The form 
(STOBJ-LET ((SUB1 (TOP3-FLDI (* 2 2) TOP3))
            (SUB1A (TOP3-FLDI 5 TOP3)))
           (SUB1 SUB1A)
           (LET* ((SUB1A (UPDATE-SUB1-FLD1 # SUB1A))
                  (SUB1 (UPDATE-SUB1-FLD1 # SUB1)))
                 (MV SUB1 SUB1A))
           TOP3)
is thus illegal.  See :DOC stobj-let.
(See :DOC set-iprint to be able to see elided values in this message.)


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

ACL2 Error in ( DEFUN FOO ...):  See :DOC failure.

******** FAILED ********

Summary
Form:  ( MAKE-EVENT (STATE-GLOBAL-LET* ...) ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 T
ACL2 !>(must-fail
; Don't allow the same index to occur twice.  Otherwise we get the problem
; shown in a comment just below.
 (defun foo (top3)
   (declare (xargs :stobjs top3))
   (stobj-let ((sub1 (top3-fldi 5 top3))
               (sub1a (top3-fldi 5 top3)))
              (sub1 sub1a)
              (let* ((sub1a (update-sub1-fld1 'x sub1a))
                     (sub1 (update-sub1-fld1 'y sub1)))
                (mv sub1 sub1a))
              top3)))

Since FOO is non-recursive, its admission is trivial.  We observe that
the type of FOO is described by the theorem (CONSP (FOO TOP3)).  We
used the :type-prescription rule UPDATE-TOP3-FLDI.

(FOO TOP3) => TOP3.

Computing the guard conjecture for FOO....

The non-trivial part of the guard conjecture for FOO, given the :executable-
counterparts of CONS, EQLABLE-LISTP, NO-DUPLICATESP-EQL-EXEC, 
NO-DUPLICATESP-EQUAL and RETURN-LAST, is

Goal
(AND
    (IMPLIES (TOP3P TOP3) NIL)
    (IMPLIES (TOP3P TOP3)
             (LET ((SUB1 (TOP3-FLDI 5 TOP3))
                   (SUB1A (TOP3-FLDI 5 TOP3)))
                  (LET ((MV (LET* ((SUB1A (UPDATE-SUB1-FLD1 'X SUB1A))
                                   (SUB1 (UPDATE-SUB1-FLD1 'Y SUB1)))
                                  (LIST SUB1 SUB1A))))
                       (LET ((SUB1 (MV-NTH 0 MV))
                             (SUB1A (MV-NTH 1 MV)))
                            (AND (< 5 (TOP3-FLD-LENGTH TOP3))
                                 (SUB1P SUB1)
                                 (LET ((TOP3 (UPDATE-TOP3-FLDI 5 SUB1 TOP3)))
                                      (AND (< 5 (TOP3-FLD-LENGTH TOP3))
                                           (SUB1P SUB1A))))))))
    (IMPLIES (TOP3P TOP3)
             (< 5 (TOP3-FLD-LENGTH TOP3)))).
Subgoal 2
Subgoal 2'
Subgoal 2''
Subgoal 2'''

([ A key checkpoint:

Subgoal 2'
(IMPLIES (AND (TRUE-LISTP TOP3)
              (EQUAL (LEN TOP3) 1)
              (CONSP TOP3)
              (TOP3-FLDP (CAR TOP3)))
         (NOT (EQUAL (LEN (CAR TOP3)) 10)))

*1 (Subgoal 2''') is pushed for proof by induction:
(IMPLIES (AND (TRUE-LISTP TOP5)
              (TRUE-LISTP (CONS TOP4 TOP5))
              (EQUAL (+ 1 (LEN TOP5)) 1)
              (TOP3-FLDP TOP4))
         (NOT (EQUAL (LEN TOP4) 10))).

])
Subgoal 1

Splitter note (see :DOC splitter) for Subgoal 1 (2 subgoals).
  if-intro: ((:DEFINITION NTH) (:DEFINITION SUB1P))

Subgoal 1.2
Subgoal 1.2'
Subgoal 1.2''

([ A key checkpoint:

Subgoal 1.2
(IMPLIES (AND (TRUE-LISTP TOP3)
              (EQUAL (LEN TOP3) 1)
              (CONSP TOP3)
              (TOP3-FLDP (CAR TOP3))
              (EQUAL (LEN (CAR TOP3)) 10))
         (TRUE-LISTP (CDR (NTH 5 (CAR TOP3)))))

*2 (Subgoal 1.2'') is pushed for proof by induction:
(IMPLIES (AND (TRUE-LISTP TOP5)
              (TRUE-LISTP (CONS TOP4 TOP5))
              (EQUAL (+ 1 (LEN TOP5)) 1)
              (TOP3-FLDP TOP4)
              (EQUAL (LEN TOP4) 10))
         (TRUE-LISTP (CDR (NTH 5 TOP4)))).

])
Subgoal 1.1
Subgoal 1.1'
Subgoal 1.1''

([ A key checkpoint:

Subgoal 1.1
(IMPLIES (AND (TRUE-LISTP TOP3)
              (EQUAL (LEN TOP3) 1)
              (CONSP TOP3)
              (TOP3-FLDP (CAR TOP3))
              (EQUAL (LEN (CAR TOP3)) 10))
         (EQUAL (+ 1 (LEN (CDR (NTH 5 (CAR TOP3)))))
                1))

*3 (Subgoal 1.1'') is pushed for proof by induction:
(IMPLIES (AND (TRUE-LISTP TOP5)
              (TRUE-LISTP (CONS TOP4 TOP5))
              (EQUAL (+ 1 (LEN TOP5)) 1)
              (TOP3-FLDP TOP4)
              (EQUAL (LEN TOP4) 10))
         (EQUAL (+ 1 (LEN (CDR (NTH 5 TOP4))))
                1)).

])

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

Subgoal 1.1 COMPLETED!

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

Subgoal 1.2 COMPLETED!

Perhaps we can prove *1 by induction.  Four induction schemes are suggested
by this conjecture.  Subsumption reduces that number to three.  These
merge into two derived induction schemes.  We will choose arbitrarily
among these.  

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

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

Subgoal *1/4''
(IMPLIES (TOP3-FLDP TOP4)
         (NOT (EQUAL (LEN TOP4) 10)))

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

])
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/1

So we now return to *1.1, which is

(IMPLIES (TOP3-FLDP TOP4)
         (NOT (EQUAL (LEN TOP4) 10))).
Subgoal *1.1/3
Subgoal *1.1/2
Subgoal *1.1/2'
Subgoal *1.1/2''
Subgoal *1.1/2'''
Subgoal *1.1/2'4'
Subgoal *1.1/2'5'
Subgoal *1.1/2'6'

*1.1.1 (Subgoal *1.1/2'6') is pushed for proof by induction.
Subgoal *1.1/1

So we now return to *1.1.1, which is

(IMPLIES (AND (INTEGERP I)
              (<= 0 I)
              (NOT (EQUAL I 10))
              (TRUE-LISTP TOP5)
              (EQUAL (LEN TOP5) 1))
         (NOT (EQUAL (+ 1 I) 10))).
Subgoal *1.1.1/3
Subgoal *1.1.1/2
Subgoal *1.1.1/2'
Subgoal *1.1.1/2''
Subgoal *1.1.1/2'''
Subgoal *1.1.1/2'4'

*1.1.1.1 (Subgoal *1.1.1/2'4') is pushed for proof by induction.
Subgoal *1.1.1/1

So we now return to *1.1.1.1, which is

(IMPLIES (AND (EQUAL (LEN TOP7) 0)
              (INTEGERP I)
              (<= 0 I)
              (NOT (EQUAL I 10))
              (TRUE-LISTP TOP7))
         (NOT (EQUAL (+ 1 I) 10))).
Subgoal *1.1.1.1/3
Subgoal *1.1.1.1/3'
Subgoal *1.1.1.1/3''

*1.1.1.1.1 (Subgoal *1.1.1.1/3'') is pushed for proof by induction.
Subgoal *1.1.1.1/2
Subgoal *1.1.1.1/1

So we now return to *1.1.1.1.1, which is

(IMPLIES (AND (INTEGERP I)
              (<= 0 I)
              (NOT (EQUAL I 10)))
         (NOT (EQUAL (+ 1 I) 10))).

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


ACL2 Error in ( DEFUN FOO ...):  The proof of the guard conjecture
for FOO 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 FOO ...)
Rules: ((:DEFINITION LEN)
        (:DEFINITION LENGTH)
        (:DEFINITION MV-NTH)
        (:DEFINITION NOT)
        (:DEFINITION NTH)
        (:DEFINITION SUB1P)
        (:DEFINITION TOP3-FLD-LENGTH)
        (:DEFINITION TOP3-FLDI)
        (:DEFINITION TOP3-FLDP)
        (:DEFINITION TOP3P)
        (:DEFINITION TRUE-LISTP)
        (:DEFINITION UPDATE-NTH)
        (:DEFINITION UPDATE-SUB1-FLD1)
        (:DEFINITION UPDATE-TOP3-FLDI)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART NTH)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:EXECUTABLE-COUNTERPART TRUE-LISTP)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION LEN)
        (:INDUCTION TOP3-FLDP)
        (:INDUCTION TRUE-LISTP)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION LEN)
        (:TYPE-PRESCRIPTION UPDATE-TOP3-FLDI))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION NTH) (:DEFINITION SUB1P))
Time:  0.06 seconds (prove: 0.04, print: 0.02, other: 0.00)
Prover steps counted:  5469

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

*** Key checkpoint at the top level: ***

Subgoal 2'
(IMPLIES (AND (TRUE-LISTP TOP3)
              (EQUAL (LEN TOP3) 1)
              (CONSP TOP3)
              (TOP3-FLDP (CAR TOP3)))
         (NOT (EQUAL (LEN (CAR TOP3)) 10)))

*** Key checkpoint under a top-level induction ***

Subgoal *1/4''
(IMPLIES (TOP3-FLDP TOP4)
         (NOT (EQUAL (LEN TOP4) 10)))

ACL2 Error in ( DEFUN FOO ...):  See :DOC failure.

******** FAILED ********

Summary
Form:  ( MAKE-EVENT (STATE-GLOBAL-LET* ...) ...)
Rules: NIL
Time:  0.06 seconds (prove: 0.04, print: 0.02, other: 0.01)
Prover steps counted:  5469

Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
Time:  0.06 seconds (prove: 0.04, print: 0.02, other: 0.01)
Prover steps counted:  5469
 T
ACL2 !>(must-fail
; Don't allow the same index to occur twice.  Otherwise we get the problem
; shown in a comment just below.
 (defun foo (top3)
   (declare (xargs :stobjs top3))
   (stobj-let ((sub1 (top3-fldi 5 top3))
               (sub1a (top3-fldi 5 top3)))
              (sub1 sub1a)
              (let* ((sub1a (update-sub1-fld1 'x sub1a))
                     (sub1 (update-sub1-fld1 'y sub1)))
                (mv sub1 sub1a))
              top3)))

Since FOO is non-recursive, its admission is trivial.  We observe that
the type of FOO is described by the theorem (CONSP (FOO TOP3)).  We
used the :type-prescription rule UPDATE-TOP3-FLDI.

(FOO TOP3) => TOP3.

Computing the guard conjecture for FOO....

The non-trivial part of the guard conjecture for FOO, given the :executable-
counterparts of CONS, EQLABLE-LISTP, NO-DUPLICATESP-EQL-EXEC, 
NO-DUPLICATESP-EQUAL and RETURN-LAST, is

Goal
(AND
    (IMPLIES (TOP3P TOP3) NIL)
    (IMPLIES (TOP3P TOP3)
             (LET ((SUB1 (TOP3-FLDI 5 TOP3))
                   (SUB1A (TOP3-FLDI 5 TOP3)))
                  (LET ((MV (LET* ((SUB1A (UPDATE-SUB1-FLD1 'X SUB1A))
                                   (SUB1 (UPDATE-SUB1-FLD1 'Y SUB1)))
                                  (LIST SUB1 SUB1A))))
                       (LET ((SUB1 (MV-NTH 0 MV))
                             (SUB1A (MV-NTH 1 MV)))
                            (AND (< 5 (TOP3-FLD-LENGTH TOP3))
                                 (SUB1P SUB1)
                                 (LET ((TOP3 (UPDATE-TOP3-FLDI 5 SUB1 TOP3)))
                                      (AND (< 5 (TOP3-FLD-LENGTH TOP3))
                                           (SUB1P SUB1A))))))))
    (IMPLIES (TOP3P TOP3)
             (< 5 (TOP3-FLD-LENGTH TOP3)))).
Subgoal 2
Subgoal 2'
Subgoal 2''
Subgoal 2'''

([ A key checkpoint:

Subgoal 2'
(IMPLIES (AND (TRUE-LISTP TOP3)
              (EQUAL (LEN TOP3) 1)
              (CONSP TOP3)
              (TOP3-FLDP (CAR TOP3)))
         (NOT (EQUAL (LEN (CAR TOP3)) 10)))

*1 (Subgoal 2''') is pushed for proof by induction:
(IMPLIES (AND (TRUE-LISTP TOP5)
              (TRUE-LISTP (CONS TOP4 TOP5))
              (EQUAL (+ 1 (LEN TOP5)) 1)
              (TOP3-FLDP TOP4))
         (NOT (EQUAL (LEN TOP4) 10))).

])
Subgoal 1

Splitter note (see :DOC splitter) for Subgoal 1 (2 subgoals).
  if-intro: ((:DEFINITION NTH) (:DEFINITION SUB1P))

Subgoal 1.2
Subgoal 1.2'
Subgoal 1.2''

([ A key checkpoint:

Subgoal 1.2
(IMPLIES (AND (TRUE-LISTP TOP3)
              (EQUAL (LEN TOP3) 1)
              (CONSP TOP3)
              (TOP3-FLDP (CAR TOP3))
              (EQUAL (LEN (CAR TOP3)) 10))
         (TRUE-LISTP (CDR (NTH 5 (CAR TOP3)))))

*2 (Subgoal 1.2'') is pushed for proof by induction:
(IMPLIES (AND (TRUE-LISTP TOP5)
              (TRUE-LISTP (CONS TOP4 TOP5))
              (EQUAL (+ 1 (LEN TOP5)) 1)
              (TOP3-FLDP TOP4)
              (EQUAL (LEN TOP4) 10))
         (TRUE-LISTP (CDR (NTH 5 TOP4)))).

])
Subgoal 1.1
Subgoal 1.1'
Subgoal 1.1''

([ A key checkpoint:

Subgoal 1.1
(IMPLIES (AND (TRUE-LISTP TOP3)
              (EQUAL (LEN TOP3) 1)
              (CONSP TOP3)
              (TOP3-FLDP (CAR TOP3))
              (EQUAL (LEN (CAR TOP3)) 10))
         (EQUAL (+ 1 (LEN (CDR (NTH 5 (CAR TOP3)))))
                1))

*3 (Subgoal 1.1'') is pushed for proof by induction:
(IMPLIES (AND (TRUE-LISTP TOP5)
              (TRUE-LISTP (CONS TOP4 TOP5))
              (EQUAL (+ 1 (LEN TOP5)) 1)
              (TOP3-FLDP TOP4)
              (EQUAL (LEN TOP4) 10))
         (EQUAL (+ 1 (LEN (CDR (NTH 5 TOP4))))
                1)).

])

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

Subgoal 1.1 COMPLETED!

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

Subgoal 1.2 COMPLETED!

Perhaps we can prove *1 by induction.  Four induction schemes are suggested
by this conjecture.  Subsumption reduces that number to three.  These
merge into two derived induction schemes.  We will choose arbitrarily
among these.  

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

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

Subgoal *1/4''
(IMPLIES (TOP3-FLDP TOP4)
         (NOT (EQUAL (LEN TOP4) 10)))

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

])
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/1

So we now return to *1.1, which is

(IMPLIES (TOP3-FLDP TOP4)
         (NOT (EQUAL (LEN TOP4) 10))).
Subgoal *1.1/3
Subgoal *1.1/2
Subgoal *1.1/2'
Subgoal *1.1/2''
Subgoal *1.1/2'''
Subgoal *1.1/2'4'
Subgoal *1.1/2'5'
Subgoal *1.1/2'6'

*1.1.1 (Subgoal *1.1/2'6') is pushed for proof by induction.
Subgoal *1.1/1

So we now return to *1.1.1, which is

(IMPLIES (AND (INTEGERP I)
              (<= 0 I)
              (NOT (EQUAL I 10))
              (TRUE-LISTP TOP5)
              (EQUAL (LEN TOP5) 1))
         (NOT (EQUAL (+ 1 I) 10))).
Subgoal *1.1.1/3
Subgoal *1.1.1/2
Subgoal *1.1.1/2'
Subgoal *1.1.1/2''
Subgoal *1.1.1/2'''
Subgoal *1.1.1/2'4'

*1.1.1.1 (Subgoal *1.1.1/2'4') is pushed for proof by induction.
Subgoal *1.1.1/1

So we now return to *1.1.1.1, which is

(IMPLIES (AND (EQUAL (LEN TOP7) 0)
              (INTEGERP I)
              (<= 0 I)
              (NOT (EQUAL I 10))
              (TRUE-LISTP TOP7))
         (NOT (EQUAL (+ 1 I) 10))).
Subgoal *1.1.1.1/3
Subgoal *1.1.1.1/3'
Subgoal *1.1.1.1/3''

*1.1.1.1.1 (Subgoal *1.1.1.1/3'') is pushed for proof by induction.
Subgoal *1.1.1.1/2
Subgoal *1.1.1.1/1

So we now return to *1.1.1.1.1, which is

(IMPLIES (AND (INTEGERP I)
              (<= 0 I)
              (NOT (EQUAL I 10)))
         (NOT (EQUAL (+ 1 I) 10))).

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


ACL2 Error in ( DEFUN FOO ...):  The proof of the guard conjecture
for FOO 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 FOO ...)
Rules: ((:DEFINITION LEN)
        (:DEFINITION LENGTH)
        (:DEFINITION MV-NTH)
        (:DEFINITION NOT)
        (:DEFINITION NTH)
        (:DEFINITION SUB1P)
        (:DEFINITION TOP3-FLD-LENGTH)
        (:DEFINITION TOP3-FLDI)
        (:DEFINITION TOP3-FLDP)
        (:DEFINITION TOP3P)
        (:DEFINITION TRUE-LISTP)
        (:DEFINITION UPDATE-NTH)
        (:DEFINITION UPDATE-SUB1-FLD1)
        (:DEFINITION UPDATE-TOP3-FLDI)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART NTH)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:EXECUTABLE-COUNTERPART TRUE-LISTP)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION LEN)
        (:INDUCTION TOP3-FLDP)
        (:INDUCTION TRUE-LISTP)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION LEN)
        (:TYPE-PRESCRIPTION UPDATE-TOP3-FLDI))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION NTH) (:DEFINITION SUB1P))
Time:  0.06 seconds (prove: 0.04, print: 0.01, other: 0.00)
Prover steps counted:  5469

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

*** Key checkpoint at the top level: ***

Subgoal 2'
(IMPLIES (AND (TRUE-LISTP TOP3)
              (EQUAL (LEN TOP3) 1)
              (CONSP TOP3)
              (TOP3-FLDP (CAR TOP3)))
         (NOT (EQUAL (LEN (CAR TOP3)) 10)))

*** Key checkpoint under a top-level induction ***

Subgoal *1/4''
(IMPLIES (TOP3-FLDP TOP4)
         (NOT (EQUAL (LEN TOP4) 10)))

ACL2 Error in ( DEFUN FOO ...):  See :DOC failure.

******** FAILED ********

Summary
Form:  ( MAKE-EVENT (STATE-GLOBAL-LET* ...) ...)
Rules: NIL
Time:  0.06 seconds (prove: 0.04, print: 0.01, other: 0.01)
Prover steps counted:  5469

Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
Time:  0.07 seconds (prove: 0.04, print: 0.01, other: 0.01)
Prover steps counted:  5469
 T
ACL2 !>;; Ready to execute ACL2-LOAD -- hit <RETURN> when ready
(acl2::ld "/Users/kaufmann/acl2/devel/books/misc/temp-emacs-file.lsp" :LD-PRE-EVAL-PRINT acl2::t :ld-error-action :return)

ACL2 Version 6.1.  Level 2.  Cbd "/Users/kaufmann/acl2/devel/books/misc/".
System books directory "/Users/kaufmann/acl2/devel/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>>(DEFTHM SUB1P-UPDATE-SUB1-FLD1-LEMMA
                (IMPLIES (SUB1P SUB1)
                         (SUB1P (UPDATE-SUB1-FLD1 ANY SUB1))))

ACL2 Warning [Non-rec] in ( DEFTHM SUB1P-UPDATE-SUB1-FLD1-LEMMA ...):
A :REWRITE rule generated from SUB1P-UPDATE-SUB1-FLD1-LEMMA will be
triggered only by terms containing the non-recursive function symbols
SUB1P and UPDATE-SUB1-FLD1.  Unless these functions are disabled, this
rule is unlikely ever to be used.

Goal'
Goal''

Q.E.D.

The storage of SUB1P-UPDATE-SUB1-FLD1-LEMMA depends upon the :type-
prescription rule SUB1P.

Summary
Form:  ( DEFTHM SUB1P-UPDATE-SUB1-FLD1-LEMMA ...)
Rules: ((:DEFINITION LEN)
        (:DEFINITION LENGTH)
        (:DEFINITION SUB1P)
        (:DEFINITION TRUE-LISTP)
        (:DEFINITION UPDATE-NTH)
        (:DEFINITION UPDATE-SUB1-FLD1)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION SUB1P))
Warnings:  Non-rec
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  219
 SUB1P-UPDATE-SUB1-FLD1-LEMMA
ACL2 !>>(DEFTHM SUB1P-NTH
                (IMPLIES (AND (TOP3-FLDP X)
                              (NATP INDEX)
                              (< INDEX (LEN X)))
                         (SUB1P (NTH INDEX X))))

ACL2 Warning [Non-rec] in ( DEFTHM SUB1P-NTH ...):  A :REWRITE rule
generated from SUB1P-NTH will be triggered only by terms containing
the non-recursive function symbol SUB1P.  Unless this function is disabled,
this rule is unlikely ever to be used.

Goal'

Splitter note (see :DOC splitter) for Goal' (2 subgoals).
  if-intro: ((:DEFINITION SUB1P))

Subgoal 2

([ A key checkpoint:

Subgoal 2
(IMPLIES (AND (TOP3-FLDP X)
              (INTEGERP INDEX)
              (<= 0 INDEX)
              (< INDEX (LEN X)))
         (TRUE-LISTP (NTH INDEX X)))

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

])
Subgoal 1

([ A key checkpoint:

Subgoal 1
(IMPLIES (AND (TOP3-FLDP X)
              (INTEGERP INDEX)
              (<= 0 INDEX)
              (< INDEX (LEN X)))
         (EQUAL (LEN (NTH INDEX X)) 1))

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.  These merge into one derived induction
scheme.  

We will induct according to a scheme suggested by (NTH INDEX X).  This
suggestion was produced using the :induction rules LEN, NTH and TOP3-FLDP.
If we let (:P INDEX X) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP X))
                   (NOT (ZP INDEX))
                   (:P (+ -1 INDEX) (CDR X)))
              (:P INDEX X))
     (IMPLIES (AND (NOT (ENDP X)) (ZP INDEX))
              (:P INDEX X))
     (IMPLIES (ENDP X) (:P INDEX X))).
This induction is justified by the same argument used to admit NTH.
Note, however, that the unmeasured variable X is being instantiated.
When applied to the goal at hand the above induction scheme produces
three nontautological subgoals.
Subgoal *1/3
Subgoal *1/3'

Splitter note (see :DOC splitter) for Subgoal *1/3' (2 subgoals).
  if-intro: ((:DEFINITION SUB1P)
             (:DEFINITION TOP3-FLDP))

Subgoal *1/3.2
Subgoal *1/3.1
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/2''
Subgoal *1/1
Subgoal *1/1'

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

Q.E.D.

The storage of SUB1P-NTH depends upon the :type-prescription rule SUB1P.

Summary
Form:  ( DEFTHM SUB1P-NTH ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION ENDP)
        (:DEFINITION LEN)
        (:DEFINITION LENGTH)
        (:DEFINITION NATP)
        (:DEFINITION NOT)
        (:DEFINITION NTH)
        (:DEFINITION SUB1P)
        (:DEFINITION TOP3-FLDP)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART INTEGERP)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION LEN)
        (:INDUCTION NTH)
        (:INDUCTION TOP3-FLDP)
        (:TYPE-PRESCRIPTION SUB1P))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION SUB1P)
             (:DEFINITION TOP3-FLDP))
Warnings:  Non-rec
Time:  0.02 seconds (prove: 0.01, print: 0.01, other: 0.00)
Prover steps counted:  1630
 SUB1P-NTH
ACL2 !>>(IN-THEORY (DISABLE SUB1P UPDATE-SUB1-FLD1))

Summary
Form:  ( IN-THEORY (DISABLE ...))
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 3102
ACL2 !>>(DEFTHM SUB1P-TOP3-FLDI
                (IMPLIES (AND (TOP3P TOP3)
                              (NATP INDEX)
                              (< INDEX 10))
                         (SUB1P (TOP3-FLDI INDEX TOP3))))

ACL2 Warning [Non-rec] in ( DEFTHM SUB1P-TOP3-FLDI ...):  A :REWRITE
rule generated from SUB1P-TOP3-FLDI will be triggered only by terms
containing the non-recursive function symbol TOP3-FLDI.  Unless this
function is disabled, this rule is unlikely ever to be used.


Q.E.D.

The storage of SUB1P-TOP3-FLDI depends upon the :type-prescription
rule SUB1P.

Summary
Form:  ( DEFTHM SUB1P-TOP3-FLDI ...)
Rules: ((:DEFINITION NATP)
        (:DEFINITION TOP3-FLDI)
        (:DEFINITION TOP3P)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:TYPE-PRESCRIPTION SUB1P))
Warnings:  Non-rec
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  57
 SUB1P-TOP3-FLDI
ACL2 !>>(DEFTHM
             SUB1P-UPDATE-SUB1-FLD1
             (IMPLIES (AND (TOP3P TOP3)
                           (NATP INDEX)
                           (< INDEX 10))
                      (SUB1P (UPDATE-SUB1-FLD1 ANY (TOP3-FLDI INDEX TOP3)))))

ACL2 Warning [Non-rec] in ( DEFTHM SUB1P-UPDATE-SUB1-FLD1 ...):  A
:REWRITE rule generated from SUB1P-UPDATE-SUB1-FLD1 will be triggered
only by terms containing the non-recursive function symbol TOP3-FLDI.
Unless this function is disabled, this rule is unlikely ever to be
used.


Q.E.D.

The storage of SUB1P-UPDATE-SUB1-FLD1 depends upon the :type-prescription
rule SUB1P.

Summary
Form:  ( DEFTHM SUB1P-UPDATE-SUB1-FLD1 ...)
Rules: ((:DEFINITION NATP)
        (:DEFINITION TOP3-FLDI)
        (:DEFINITION TOP3P)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:TYPE-PRESCRIPTION SUB1P))
Warnings:  Non-rec
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  59
 SUB1P-UPDATE-SUB1-FLD1
ACL2 !>>Bye.
 :EOF
ACL2 !>(defun top3.fldi.update-sub1-fld1/i1/i2 (i1 v1 i2 v2 top3)
; Here we update an stobj array field of a stobj, at two distinct indices.
  (declare (type (integer 0 9) i1 i2)
           (xargs :stobjs top3
                  :guard (not (eql i1 i2))))
  (stobj-let ((sub1 (top3-fldi i1 top3))
              (sub1a (top3-fldi i2 top3)))
             (sub1 sub1a)
             (let* ((sub1a (update-sub1-fld1 v2 sub1a))
                    (sub1 (update-sub1-fld1 v1 sub1)))
               (mv sub1 sub1a))
             top3))

Since TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 is non-recursive, its admission
is trivial.  We observe that the type of TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2
is described by the theorem 
(CONSP (TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 I1 V1 I2 V2 TOP3)).  We used
the :type-prescription rule UPDATE-TOP3-FLDI.

(TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 * * * * TOP3) => TOP3.

Computing the guard conjecture for TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2....

The non-trivial part of the guard conjecture for 
TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2, given the :compound-recognizer rule
EQLABLEP-RECOG, is

Goal
(AND
   (IMPLIES (AND (NOT (EQUAL I1 I2))
                 (TOP3P TOP3)
                 (<= I2 9)
                 (<= 0 I2)
                 (INTEGERP I2)
                 (<= I1 9)
                 (<= 0 I1)
                 (INTEGERP I1))
            (< I2 (TOP3-FLD-LENGTH TOP3)))
   (IMPLIES (AND (NOT (EQUAL I1 I2))
                 (TOP3P TOP3)
                 (<= I2 9)
                 (<= 0 I2)
                 (INTEGERP I2)
                 (<= I1 9)
                 (<= 0 I1)
                 (INTEGERP I1))
            (LET ((X (LIST I1 I2)))
                 (MBE1 (NO-DUPLICATESP-EQL-EXEC X)
                       (NO-DUPLICATESP-EQUAL X))))
   (IMPLIES (AND (NOT (EQUAL I1 I2))
                 (TOP3P TOP3)
                 (<= I2 9)
                 (<= 0 I2)
                 (INTEGERP I2)
                 (<= I1 9)
                 (<= 0 I1)
                 (INTEGERP I1))
            (EQLABLE-LISTP (LIST I1 I2)))
   (IMPLIES (AND (NOT (EQUAL I1 I2))
                 (TOP3P TOP3)
                 (<= I2 9)
                 (<= 0 I2)
                 (INTEGERP I2)
                 (<= I1 9)
                 (<= 0 I1)
                 (INTEGERP I1))
            (LET ((SUB1 (TOP3-FLDI I1 TOP3))
                  (SUB1A (TOP3-FLDI I2 TOP3)))
                 (LET ((MV (LET* ((SUB1A (UPDATE-SUB1-FLD1 V2 SUB1A))
                                  (SUB1 (UPDATE-SUB1-FLD1 V1 SUB1)))
                                 (LIST SUB1 SUB1A))))
                      (LET ((SUB1 (MV-NTH 0 MV))
                            (SUB1A (MV-NTH 1 MV)))
                           (AND (INTEGERP I1)
                                (< I1 (TOP3-FLD-LENGTH TOP3))
                                (<= 0 I1)
                                (SUB1P SUB1)
                                (LET ((TOP3 (UPDATE-TOP3-FLDI I1 SUB1 TOP3)))
                                     (AND (INTEGERP I2)
                                          (< I2 (TOP3-FLD-LENGTH TOP3))
                                          (<= 0 I2)
                                          (SUB1P SUB1A))))))))
   (IMPLIES (AND (NOT (EQUAL I1 I2))
                 (TOP3P TOP3)
                 (<= I2 9)
                 (<= 0 I2)
                 (INTEGERP I2)
                 (<= I1 9)
                 (<= 0 I1)
                 (INTEGERP I1))
            (< I1 (TOP3-FLD-LENGTH TOP3)))).
Subgoal 3
Subgoal 2
Subgoal 1

Q.E.D.

That completes the proof of the guard theorem for 
TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2.  TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2
is compliant with Common Lisp.

Summary
Form:  ( DEFUN TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 ...)
Rules: ((:COMPOUND-RECOGNIZER EQLABLEP-RECOG)
        (:DEFINITION EQLABLE-LISTP)
        (:DEFINITION LENGTH)
        (:DEFINITION MEMBER-EQUAL)
        (:DEFINITION MV-NTH)
        (:DEFINITION NO-DUPLICATESP-EQUAL)
        (:DEFINITION NOT)
        (:DEFINITION NTH)
        (:DEFINITION RETURN-LAST)
        (:DEFINITION TOP3-FLD-LENGTH)
        (:DEFINITION TOP3-FLDI)
        (:DEFINITION TOP3P)
        (:DEFINITION UPDATE-NTH-ARRAY)
        (:DEFINITION UPDATE-TOP3-FLDI)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQLABLE-LISTP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART NO-DUPLICATESP-EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART NTH)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE SUB1P-NTH)
        (:REWRITE SUB1P-UPDATE-SUB1-FLD1-LEMMA)
        (:TYPE-PRESCRIPTION TOP3-FLDP)
        (:TYPE-PRESCRIPTION UPDATE-TOP3-FLDI))
Time:  0.02 seconds (prove: 0.01, print: 0.00, other: 0.01)
Prover steps counted:  1558
 TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2
ACL2 !>:u
         18:x(DEFTHM SUB1P-UPDATE-SUB1-FLD1 ...)
ACL2 !>(defun top3.fldi.update-sub1-fld1/i1/i2 (i1 v1 i2 v2 top3)
; Here we update an stobj array field of a stobj, at two distinct indices.
  (declare (type (integer 0 9) i1 i2)
           (xargs :stobjs top3
                  :guard t))
  (stobj-let ((sub1 (top3-fldi i1 top3))
              (sub1a (top3-fldi i2 top3)))
             (sub1 sub1a)
             (let* ((sub1a (update-sub1-fld1 v2 sub1a))
                    (sub1 (update-sub1-fld1 v1 sub1)))
               (mv sub1 sub1a))
             top3))

Since TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 is non-recursive, its admission
is trivial.  We observe that the type of TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2
is described by the theorem 
(CONSP (TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 I1 V1 I2 V2 TOP3)).  We used
the :type-prescription rule UPDATE-TOP3-FLDI.

(TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 * * * * TOP3) => TOP3.

Computing the guard conjecture for TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2....

The non-trivial part of the guard conjecture for 
TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 is

Goal
(AND
   (IMPLIES (AND (TOP3P TOP3)
                 (<= I2 9)
                 (<= 0 I2)
                 (INTEGERP I2)
                 (<= I1 9)
                 (<= 0 I1)
                 (INTEGERP I1))
            (EQLABLE-LISTP (LIST I1 I2)))
   (IMPLIES (AND (TOP3P TOP3)
                 (<= I2 9)
                 (<= 0 I2)
                 (INTEGERP I2)
                 (<= I1 9)
                 (<= 0 I1)
                 (INTEGERP I1))
            (LET ((SUB1 (TOP3-FLDI I1 TOP3))
                  (SUB1A (TOP3-FLDI I2 TOP3)))
                 (LET ((MV (LET* ((SUB1A (UPDATE-SUB1-FLD1 V2 SUB1A))
                                  (SUB1 (UPDATE-SUB1-FLD1 V1 SUB1)))
                                 (LIST SUB1 SUB1A))))
                      (LET ((SUB1 (MV-NTH 0 MV))
                            (SUB1A (MV-NTH 1 MV)))
                           (AND (INTEGERP I1)
                                (< I1 (TOP3-FLD-LENGTH TOP3))
                                (<= 0 I1)
                                (SUB1P SUB1)
                                (LET ((TOP3 (UPDATE-TOP3-FLDI I1 SUB1 TOP3)))
                                     (AND (INTEGERP I2)
                                          (< I2 (TOP3-FLD-LENGTH TOP3))
                                          (<= 0 I2)
                                          (SUB1P SUB1A))))))))
   (IMPLIES (AND (TOP3P TOP3)
                 (<= I2 9)
                 (<= 0 I2)
                 (INTEGERP I2)
                 (<= I1 9)
                 (<= 0 I1)
                 (INTEGERP I1))
            (< I1 (TOP3-FLD-LENGTH TOP3)))
   (IMPLIES (AND (TOP3P TOP3)
                 (<= I2 9)
                 (<= 0 I2)
                 (INTEGERP I2)
                 (<= I1 9)
                 (<= 0 I1)
                 (INTEGERP I1))
            (LET ((X (LIST I1 I2)))
                 (MBE1 (NO-DUPLICATESP-EQL-EXEC X)
                       (NO-DUPLICATESP-EQUAL X))))
   (IMPLIES (AND (TOP3P TOP3)
                 (<= I2 9)
                 (<= 0 I2)
                 (INTEGERP I2)
                 (<= I1 9)
                 (<= 0 I1)
                 (INTEGERP I1))
            (< I2 (TOP3-FLD-LENGTH TOP3)))).
Subgoal 3
Subgoal 2
Subgoal 1
Subgoal 1'
Subgoal 1''
Subgoal 1'''
Subgoal 1'4'

([ A key checkpoint:

Subgoal 1''
(IMPLIES (AND (TRUE-LISTP TOP3)
              (EQUAL (LEN TOP3) 1)
              (CONSP TOP3)
              (TOP3-FLDP (CAR TOP3))
              (EQUAL (LEN (CAR TOP3)) 10)
              (<= I1 9)
              (<= 0 I1)
              (INTEGERP I1))
         (NOT (LIST I1)))

*1 (Subgoal 1'4') is pushed for proof by induction:
(IMPLIES (AND (TRUE-LISTP TOP5)
              (TRUE-LISTP (CONS TOP4 TOP5))
              (EQUAL (+ 1 (LEN TOP5)) 1)
              (TOP3-FLDP TOP4)
              (EQUAL (LEN TOP4) 10)
              (<= I1 9)
              (<= 0 I1)
              (INTEGERP I1))
         (NOT (LIST I1))).

])

Perhaps we can prove *1 by induction.  Four induction schemes are suggested
by this conjecture.  Subsumption reduces that number to three.  These
merge into two derived induction schemes.  We will choose arbitrarily
among these.  

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

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

Subgoal *1/4''
(IMPLIES (AND (TOP3-FLDP TOP4)
              (EQUAL (LEN TOP4) 10)
              (<= I1 9)
              (<= 0 I1)
              (INTEGERP I1))
         (NOT (LIST I1)))

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

])
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/1

So we now return to *1.1, which is

(IMPLIES (AND (TOP3-FLDP TOP4)
              (EQUAL (LEN TOP4) 10)
              (<= I1 9)
              (<= 0 I1)
              (INTEGERP I1))
         (NOT (LIST I1))).
Subgoal *1.1/3
Subgoal *1.1/2
Subgoal *1.1/2'
Subgoal *1.1/2''
Subgoal *1.1/2'''
Subgoal *1.1/2'4'
Subgoal *1.1/2'5'
Subgoal *1.1/2'6'

*1.1.1 (Subgoal *1.1/2'6') is pushed for proof by induction.
Subgoal *1.1/1

So we now return to *1.1.1, which is

(IMPLIES (AND (INTEGERP I)
              (<= 0 I)
              (NOT (EQUAL I 10))
              (EQUAL (+ 1 I) 10)
              (<= I1 9)
              (<= 0 I1)
              (INTEGERP I1))
         (NOT (LIST I1))).

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


ACL2 Error in ( DEFUN TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 ...):  The proof
of the guard conjecture for TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 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 TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 ...)
Rules: ((:COMPOUND-RECOGNIZER EQLABLEP-RECOG)
        (:DEFINITION EQLABLE-LISTP)
        (:DEFINITION LEN)
        (:DEFINITION LENGTH)
        (:DEFINITION MEMBER-EQUAL)
        (:DEFINITION MV-NTH)
        (:DEFINITION NO-DUPLICATESP-EQUAL)
        (:DEFINITION NOT)
        (:DEFINITION NTH)
        (:DEFINITION RETURN-LAST)
        (:DEFINITION TOP3-FLD-LENGTH)
        (:DEFINITION TOP3-FLDI)
        (:DEFINITION TOP3-FLDP)
        (:DEFINITION TOP3P)
        (:DEFINITION TRUE-LISTP)
        (:DEFINITION UPDATE-NTH-ARRAY)
        (:DEFINITION UPDATE-TOP3-FLDI)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQLABLE-LISTP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART NO-DUPLICATESP-EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART NTH)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:EXECUTABLE-COUNTERPART TRUE-LISTP)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION LEN)
        (:INDUCTION TOP3-FLDP)
        (:INDUCTION TRUE-LISTP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE SUB1P-NTH)
        (:REWRITE SUB1P-UPDATE-SUB1-FLD1-LEMMA)
        (:TYPE-PRESCRIPTION LEN)
        (:TYPE-PRESCRIPTION TOP3-FLDP)
        (:TYPE-PRESCRIPTION UPDATE-TOP3-FLDI))
Time:  0.03 seconds (prove: 0.02, print: 0.01, other: 0.00)
Prover steps counted:  4182

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

*** Key checkpoint at the top level: ***

Subgoal 1''
(IMPLIES (AND (TRUE-LISTP TOP3)
              (EQUAL (LEN TOP3) 1)
              (CONSP TOP3)
              (TOP3-FLDP (CAR TOP3))
              (EQUAL (LEN (CAR TOP3)) 10)
              (<= I1 9)
              (<= 0 I1)
              (INTEGERP I1))
         (NOT (LIST I1)))

*** Key checkpoint under a top-level induction ***

Subgoal *1/4''
(IMPLIES (AND (TOP3-FLDP TOP4)
              (EQUAL (LEN TOP4) 10)
              (<= I1 9)
              (<= 0 I1)
              (INTEGERP I1))
         (NOT (LIST I1)))

ACL2 Error in ( DEFUN TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 ...):  See :DOC
failure.

******** FAILED ********
ACL2 !>(defun top3.fldi.update-sub1-fld1/i1/i2 (i1 v1 i2 v2 top3)
	 ; Here we update an stobj array field of a stobj, at two distinct indices.
	 (declare (type (integer 0 9) i1 i2)
		  (xargs :stobjs top3
			  :guard t))
	 (if (equal i1 i2)
	     top3
	   (stobj-let ((sub1 (top3-fldi i1 top3))
		       (sub1a (top3-fldi i2 top3)))
		      (sub1 sub1a)
		      (let* ((sub1a (update-sub1-fld1 v2 sub1a))
			     (sub1 (update-sub1-fld1 v1 sub1)))
			(mv sub1 sub1a))
		      top3)))

Since TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 is non-recursive, its admission
is trivial.  We observe that the type of TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2
is described by the theorem 
(OR (CONSP (TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 I1 V1 I2 V2 TOP3))
    (EQUAL (TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 I1 V1 I2 V2 TOP3)
           TOP3)).
We used the :type-prescription rule UPDATE-TOP3-FLDI.

(TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 * * * * TOP3) => TOP3.

Computing the guard conjecture for TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2....

The non-trivial part of the guard conjecture for 
TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 is

Goal
(AND
   (IMPLIES (AND (TOP3P TOP3)
                 (<= I2 9)
                 (<= 0 I2)
                 (INTEGERP I2)
                 (<= I1 9)
                 (<= 0 I1)
                 (INTEGERP I1)
                 (NOT (EQUAL I1 I2)))
            (EQLABLE-LISTP (LIST I1 I2)))
   (IMPLIES (AND (TOP3P TOP3)
                 (<= I2 9)
                 (<= 0 I2)
                 (INTEGERP I2)
                 (<= I1 9)
                 (<= 0 I1)
                 (INTEGERP I1)
                 (NOT (EQUAL I1 I2)))
            (LET ((SUB1 (TOP3-FLDI I1 TOP3))
                  (SUB1A (TOP3-FLDI I2 TOP3)))
                 (LET ((MV (LET* ((SUB1A (UPDATE-SUB1-FLD1 V2 SUB1A))
                                  (SUB1 (UPDATE-SUB1-FLD1 V1 SUB1)))
                                 (LIST SUB1 SUB1A))))
                      (LET ((SUB1 (MV-NTH 0 MV))
                            (SUB1A (MV-NTH 1 MV)))
                           (AND (INTEGERP I1)
                                (< I1 (TOP3-FLD-LENGTH TOP3))
                                (<= 0 I1)
                                (SUB1P SUB1)
                                (LET ((TOP3 (UPDATE-TOP3-FLDI I1 SUB1 TOP3)))
                                     (AND (INTEGERP I2)
                                          (< I2 (TOP3-FLD-LENGTH TOP3))
                                          (<= 0 I2)
                                          (SUB1P SUB1A))))))))
   (IMPLIES (AND (TOP3P TOP3)
                 (<= I2 9)
                 (<= 0 I2)
                 (INTEGERP I2)
                 (<= I1 9)
                 (<= 0 I1)
                 (INTEGERP I1)
                 (NOT (EQUAL I1 I2)))
            (< I1 (TOP3-FLD-LENGTH TOP3)))
   (IMPLIES (AND (TOP3P TOP3)
                 (<= I2 9)
                 (<= 0 I2)
                 (INTEGERP I2)
                 (<= I1 9)
                 (<= 0 I1)
                 (INTEGERP I1)
                 (NOT (EQUAL I1 I2)))
            (LET ((X (LIST I1 I2)))
                 (MBE1 (NO-DUPLICATESP-EQL-EXEC X)
                       (NO-DUPLICATESP-EQUAL X))))
   (IMPLIES (AND (TOP3P TOP3)
                 (<= I2 9)
                 (<= 0 I2)
                 (INTEGERP I2)
                 (<= I1 9)
                 (<= 0 I1)
                 (INTEGERP I1)
                 (NOT (EQUAL I1 I2)))
            (< I2 (TOP3-FLD-LENGTH TOP3)))).
Subgoal 3
Subgoal 2
Subgoal 1

Q.E.D.

That completes the proof of the guard theorem for 
TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2.  TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2
is compliant with Common Lisp.

Summary
Form:  ( DEFUN TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2 ...)
Rules: ((:COMPOUND-RECOGNIZER EQLABLEP-RECOG)
        (:DEFINITION EQLABLE-LISTP)
        (:DEFINITION LENGTH)
        (:DEFINITION MEMBER-EQUAL)
        (:DEFINITION MV-NTH)
        (:DEFINITION NO-DUPLICATESP-EQUAL)
        (:DEFINITION NOT)
        (:DEFINITION NTH)
        (:DEFINITION RETURN-LAST)
        (:DEFINITION TOP3-FLD-LENGTH)
        (:DEFINITION TOP3-FLDI)
        (:DEFINITION TOP3P)
        (:DEFINITION UPDATE-NTH-ARRAY)
        (:DEFINITION UPDATE-TOP3-FLDI)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQLABLE-LISTP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART NO-DUPLICATESP-EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART NTH)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE SUB1P-NTH)
        (:REWRITE SUB1P-UPDATE-SUB1-FLD1-LEMMA)
        (:TYPE-PRESCRIPTION TOP3-FLDP)
        (:TYPE-PRESCRIPTION UPDATE-TOP3-FLDI))
Time:  0.02 seconds (prove: 0.01, print: 0.00, other: 0.01)
Prover steps counted:  1558
 TOP3.FLDI.UPDATE-SUB1-FLD1/I1/I2
ACL2 !>(defun stobj-er-test-aux (x sub1)
  (declare (xargs :stobjs sub1 :guard (consp x)))
  (mv (car x) sub1))

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

(STOBJ-ER-TEST-AUX * SUB1) => (MV * SUB1).

Computing the guard conjecture for STOBJ-ER-TEST-AUX....

The guard conjecture for STOBJ-ER-TEST-AUX is trivial to prove.  
STOBJ-ER-TEST-AUX is compliant with Common Lisp.

Summary
Form:  ( DEFUN STOBJ-ER-TEST-AUX ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 STOBJ-ER-TEST-AUX
ACL2 !>(defun stobj-er-test (x top1)
  (declare (xargs :stobjs top1 :verify-guards nil))
  (stobj-let
   ((sub1 (top1-fld top1)))
   (val sub1)
   (stobj-er-test-aux x sub1)
   top1))

Since STOBJ-ER-TEST is non-recursive, its admission is trivial.  We
observe that the type of STOBJ-ER-TEST is described by the theorem
(CONSP (STOBJ-ER-TEST X TOP1)).  We used the :type-prescription rule
UPDATE-TOP1-FLD.

(STOBJ-ER-TEST * TOP1) => TOP1.

Summary
Form:  ( DEFUN STOBJ-ER-TEST ...)
Rules: ((:TYPE-PRESCRIPTION UPDATE-TOP1-FLD))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 STOBJ-ER-TEST
ACL2 !>(local-test
; No guard violation, so this succeeds:
 :defs
 ((defun f1 (top1)
    (declare (xargs :stobjs top1 :verify-guards nil))
    (stobj-er-test '(4 5) top1)))
 :run
 (f1 top1)
 :check
 t)

Since F1 is non-recursive, its admission is trivial.  We observe that
the type of F1 is described by the theorem (CONSP (F1 TOP1)).  We used
the :type-prescription rule STOBJ-ER-TEST.

(F1 TOP1) => TOP1.

Summary
Form:  ( DEFUN F1 ...)
Rules: ((:TYPE-PRESCRIPTION STOBJ-ER-TEST))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)

Summary
Form:  ( MAKE-EVENT (ER-PROGN ...))
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

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

Summary
Form:  ( MAKE-EVENT (PROGN ...))
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 :SUCCESS
ACL2 !>(must-fail
; And now the error message:
 (local-test
  :defs
  ((defun f1 (top1)
     (declare (xargs :stobjs top1 :verify-guards nil))
     (stobj-er-test '3 top1)))
  :run
  (with-guard-checking t (f1 top1))
  :check
  t))

Since F1 is non-recursive, its admission is trivial.  We observe that
the type of F1 is described by the theorem (CONSP (F1 TOP1)).  We used
the :type-prescription rule STOBJ-ER-TEST.

(F1 TOP1) => TOP1.

Summary
Form:  ( DEFUN F1 ...)
Rules: ((:TYPE-PRESCRIPTION STOBJ-ER-TEST))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)


ACL2 Error in TOP:  The guard for the function call 
(STOBJ-ER-TEST-AUX X SUB1), which is (AND (SUB1P SUB1) (CONSP X)),
is violated by the arguments in the call 
(STOBJ-ER-TEST-AUX 3 |<some-stobj>|).
See :DOC set-guard-checking for information about suppressing this
check with (set-guard-checking :none), as recommended for new users.
To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.



ACL2 Error in ( MAKE-EVENT (ER-PROGN ...)):  Error in MAKE-EVENT from
expansion of:
  (ER-PROGN (TRANS-EVAL '(WITH-GUARD-CHECKING T (F1 TOP1))
                        'TOP
                        STATE T)
            (ASSERT-EVENT T :ON-SKIP-PROOFS T)
            (VALUE '(VALUE-TRIPLE '#)))
(See :DOC set-iprint to be able to see elided values in this message.)


Summary
Form:  ( MAKE-EVENT (ER-PROGN ...))
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

ACL2 Error in ( MAKE-EVENT (ER-PROGN ...)):  See :DOC failure.

******** FAILED ********


ACL2 Error in ( PROGN (DEFUN F1 ...) ...):  PROGN failed!


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

ACL2 Error in ( PROGN (DEFUN F1 ...) ...):  See :DOC failure.

******** FAILED ********


ACL2 Error in ( MAKE-EVENT (PROGN ...)):  Error in MAKE-EVENT from
expansion of:
  (PROGN (DEFUN F1 (TOP1)
                (DECLARE (XARGS :STOBJS TOP1 :VERIFY-GUARDS NIL))
                (STOBJ-ER-TEST '3 TOP1))
         (MAKE-EVENT (ER-PROGN (TRANS-EVAL '# 'TOP STATE T)
                               (ASSERT-EVENT T :ON-SKIP-PROOFS T)
                               (VALUE '#))))
(See :DOC set-iprint to be able to see elided values in this message.)


Summary
Form:  ( MAKE-EVENT (PROGN ...))
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)

ACL2 Error in ( MAKE-EVENT (PROGN ...)):  See :DOC failure.

******** FAILED ********

Summary
Form:  ( MAKE-EVENT (STATE-GLOBAL-LET* ...) ...)
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)

Summary
Form:  ( MAKE-EVENT (QUOTE ...) ...)
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 T
ACL2 !>(trace$ update-sub1-fld1)
 ((UPDATE-SUB1-FLD1))
ACL2 !>(top1-fld.update-fld1 17 top1)
1> (UPDATE-SUB1-FLD1 17 |<sub1>{instance}|)
<1 (UPDATE-SUB1-FLD1 |<sub1>{instance}|)
<top1>
ACL2 !>(sub1p 17)
NIL
ACL2 !>(sub1p sub2)


ACL2 Error in TOP-LEVEL:  The form SUB2 is being used, as an argument
to a call of SUB1P, where the single-threaded object SUB1 is required.
Note that the variable SUB1 is required, not merely a term that returns
such a single-threaded object, so you may need to bind SUB1 with LET;
see :DOC stobj.  Note:  this error occurred in the context (SUB1P SUB2).
Observe that while it is permitted to apply SUB1P to an ordinary object,
this stobj recognizer must not be applied to the wrong stobj.

ACL2 !>(sub1p sub1a)
T
ACL2 !>(thm (equal (sub1p a) (sub1ap a)))

Splitter note (see :DOC splitter) for Goal (2 subgoals).
  if-intro: ((:DEFINITION SUB1AP))

Subgoal 2
Subgoal 2.2
Subgoal 2.2'

([ A key checkpoint:

Subgoal 2.2'
(IMPLIES (AND (TRUE-LISTP A) (EQUAL (LEN A) 1))
         (SUB1P A))

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

])
Subgoal 2.1

([ A key checkpoint:

Subgoal 2.1
(IMPLIES (AND (TRUE-LISTP A)
              (NOT (EQUAL (LEN A) 1)))
         (NOT (SUB1P A)))

Normally we would attempt to prove Subgoal 2.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.)

])

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

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION LENGTH)
        (:DEFINITION SUB1AP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION SUB1P))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION SUB1AP))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  293

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

*** Key checkpoints before reverting to proof by induction: ***

Subgoal 2.2'
(IMPLIES (AND (TRUE-LISTP A) (EQUAL (LEN A) 1))
         (SUB1P A))

Subgoal 2.1
(IMPLIES (AND (TRUE-LISTP A)
              (NOT (EQUAL (LEN A) 1)))
         (NOT (SUB1P A)))

ACL2 Error in ( THM ...):  See :DOC failure.

******** FAILED ********
ACL2 !>(include-book "arithmetic/top" :dir :system)

Summary
Form:  ( INCLUDE-BOOK "arithmetic/top" ...)
Rules: NIL
Time:  0.16 seconds (prove: 0.00, print: 0.00, other: 0.16)
 "/Users/kaufmann/acl2/devel/books/arithmetic/top.lisp"
ACL2 !>(thm (equal (sub1p a) (sub1ap a)))

Splitter note (see :DOC splitter) for Goal (2 subgoals).
  if-intro: ((:DEFINITION SUB1AP))

Subgoal 2
Subgoal 2.2
Subgoal 2.2'

([ A key checkpoint:

Subgoal 2.2'
(IMPLIES (AND (TRUE-LISTP A) (EQUAL (LEN A) 1))
         (SUB1P A))

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

])
Subgoal 2.1

([ A key checkpoint:

Subgoal 2.1
(IMPLIES (AND (TRUE-LISTP A)
              (NOT (EQUAL (LEN A) 1)))
         (NOT (SUB1P A)))

Normally we would attempt to prove Subgoal 2.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.)

])

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

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION LENGTH)
        (:DEFINITION SUB1AP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION SUB1P))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION SUB1AP))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  293

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

*** Key checkpoints before reverting to proof by induction: ***

Subgoal 2.2'
(IMPLIES (AND (TRUE-LISTP A) (EQUAL (LEN A) 1))
         (SUB1P A))

Subgoal 2.1
(IMPLIES (AND (TRUE-LISTP A)
              (NOT (EQUAL (LEN A) 1)))
         (NOT (SUB1P A)))

ACL2 Error in ( THM ...):  See :DOC failure.

******** FAILED ********
ACL2 !>:pe sub1a
   d      6  (DEFSTOBJ SUB1A SUB1A-FLD1
                       :CONGRUENT-TO SUB1)
ACL2 !>(disabledp 'sub1ap)
NIL
ACL2 !>(disabledp 'sub1p)
((:DEFINITION SUB1P))
ACL2 !>(in-theory (enable sub1p))

Summary
Form:  ( IN-THEORY (ENABLE ...))
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 3280
ACL2 !>(thm (equal (sub1p a) (sub1ap a)))

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION LENGTH)
        (:DEFINITION SUB1AP)
        (:DEFINITION SUB1P)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  72

Proof succeeded.
ACL2 !>