ACL2 Version 2.9. Level 4. Cbd "/u/moore/m6/currentwork/src/M6/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ; [Prior the demo, I loaded Hanbing Liu's M6 model of the JVM ; the Manolios and Moore defpun book, the macro definition of ; defspec (which allows us to use the inductive assertion method ; as described in the talk), and some lemmas about 32-bit int ; arithmetic.] ; Demo 1: The classic theorem proved by the Boyer-Moore system ; back in 1972. m6 >(defun ap (x y) (if (consp x) (cons (car x) (ap (cdr x) y)) y)) The admission of AP is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). We observe that the type of AP is described by the theorem (OR (CONSP (AP X Y)) (EQUAL (AP X Y) Y)). We used primitive type reasoning. Summary Form: ( DEFUN AP ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.01, other: 0.02) AP m6 >(ap '(1 2 3 4 5) '(6 7 8 9 10)) (1 2 3 4 5 6 7 8 9 10) m6 >(thm (equal (ap (ap a b) c) (ap a (ap b c)))) Name the formula above *1. Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. Subsumption reduces that number to two. However, one of these is flawed and so we are left with one viable candidate. We will induct according to a scheme suggested by (AP A B). This suggestion was produced using the :induction rule AP. If we let (:P A B C) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP A)) (:P A B C)) (IMPLIES (AND (CONSP A) (:P (CDR A) B C)) (:P A B C))). This induction is justified by the same argument used to admit AP, namely, the measure (ACL2-COUNT A) is decreasing according to the relation O< (which is known to be well-founded on the domain recognized by O-P). When applied to the goal at hand the above induction scheme produces the following two nontautological subgoals. Subgoal *1/2 (IMPLIES (NOT (CONSP A)) (EQUAL (AP (AP A B) C) (AP A (AP B C)))). But simplification reduces this to T, using the :definition AP and primitive type reasoning. Subgoal *1/1 (IMPLIES (AND (CONSP A) (EQUAL (AP (AP (CDR A) B) C) (AP (CDR A) (AP B C)))) (EQUAL (AP (AP A B) C) (AP A (AP B C)))). But simplification reduces this to T, using the :definition AP, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. That completes the proof of *1. Q.E.D. Summary Form: ( THM ...) Rules: ((:DEFINITION AP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION AP) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS)) Warnings: None Time: 0.06 seconds (prove: 0.02, print: 0.04, other: 0.00) Proof succeeded. m6t T m6 >(quote (end of Demo 1)) (END OF DEMO 1) m6 >(show *pi-empty-state*) (STATE ; a very large ACL2 object representing an empty JVM state in which ; the class "Demo" and many classes of the Sun CLDC API can be ; loaded. I'll delete the display of this object, except for the ; part showing "Demo": ; ... (CLASS "Demo" "java.lang.Object" (JVM::CONSTANT_POOL) (FIELDS) (METHODS (METHOD "pi" (PARAMETERS INT) (RETURNTYPE INT) (ACCESSFLAGS *CLASS* *PUBLIC* *STATIC*) (CODE (MAX_STACK 2) (JVM::MAX_LOCALS 2) (CODE_LENGTH 19) (PARSEDCODE (0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (IRETURN)) (ENDOFCODE 19)) (EXCEPTIONS) (STACKMAP))) (METHOD "main" (PARAMETERS (ARRAY (CLASS "java.lang.String"))) (RETURNTYPE VOID) (ACCESSFLAGS *CLASS* *PUBLIC* *STATIC*) (CODE (MAX_STACK 2) (JVM::MAX_LOCALS 2) (CODE_LENGTH 20) (PARSEDCODE (0 (ALOAD_0)) (1 (ICONST_0)) (2 (AALOAD)) (3 (BIPUSH 10)) (5 (INVOKESTATIC (METHODCP "parseInt" "java.lang.Integer" ((CLASS "java.lang.String") INT) INT))) (8 (ISTORE_1)) (9 (GETSTATIC (JVM::FIELDCP "out" "java.lang.System" (CLASS "java.io.PrintStream")))) (12 (ILOAD_1)) (13 (INVOKESTATIC (METHODCP "pi" "Demo" (INT) INT))) (16 (INVOKEVIRTUAL (METHODCP "println" "java.io.PrintStream" (INT) VOID))) (19 (RETURN)) (ENDOFCODE 20)) (EXCEPTIONS) (STACKMAP))) (METHOD "" (PARAMETERS) (RETURNTYPE VOID) (ACCESSFLAGS *CLASS*) (CODE (MAX_STACK 1) (JVM::MAX_LOCALS 1) (CODE_LENGTH 5) (PARSEDCODE (0 (ALOAD_0)) (1 (INVOKESPECIAL (METHODCP "" "java.lang.Object" NIL VOID))) (4 (RETURN)) (ENDOFCODE 5)) (EXCEPTIONS) (STACKMAP)))) (INTERFACES) (ACCESSFLAGS *CLASS* *SUPER* *SYNCHRONIZED*)) ; ... ) m6 >(all-class-names (instance-class-table *pi-empty-state*)) NIL m6 >(all-class-names (external-class-table *pi-empty-state*)) ("java.lang.ArithmeticException" "java.lang.RuntimeException" "java.lang.Exception" "java.lang.Throwable" "java.lang.Object" "java.lang.String" "java.lang.Class" "java.lang.InterruptedException" "java.lang.StringBuffer" "java.lang.ClassNotFoundException" "java.lang.InstantiationException" "java.lang.IllegalAccessException" "java.lang.ArrayStoreException" "java.lang.ArrayIndexOutOfBoundsException" "java.lang.Boolean" "java.lang.IndexOutOfBoundsException" "java.lang.Byte" "java.lang.NumberFormatException" "java.lang.IllegalArgumentException" "java.lang.Character" "java.lang.ClassCastException" "java.lang.Error" "java.lang.IllegalMonitorStateException" "java.lang.IllegalThreadStateException" "java.lang.Integer" "java.lang.Long" "java.lang.Math" "java.lang.NegativeArraySizeException" "java.lang.Runnable" "java.lang.NullPointerException" "java.lang.OutOfMemoryError" "java.lang.VirtualMachineError" "java.lang.Runtime" "java.lang.SecurityException" "java.lang.Short" "java.lang.StringIndexOutOfBoundsException" "java.lang.System" "java.lang.Thread" "java.io.UnsupportedEncodingException" "java.io.IOException" "java.io.InputStream" "java.io.PrintStream" "java.io.OutputStream" "java.io.OutputStreamWriter" "java.io.Writer" "java.io.Reader" "java.io.DataInputStream" "java.io.DataInput" "java.io.DataOutputStream" "java.io.DataOutput" "java.io.ByteArrayInputStream" "java.io.ByteArrayOutputStream" "java.io.EOFException" "java.io.InputStreamReader" "java.io.UTFDataFormatException" "java.io.InterruptedIOException" "java.util.Calendar" "java.util.TimeZone" "java.util.Date" "java.util.EmptyStackException" "java.util.Enumeration" "java.util.Hashtable$HashtableEnumerator" "java.util.Hashtable" "java.util.HashtableEntry" "java.util.NoSuchElementException" "java.util.Random" "java.util.Stack" "java.util.Vector" "java.util.VectorEnumerator" "javax.microedition.io.Connector" "javax.microedition.io.Connection" "javax.microedition.io.ConnectionNotFoundException" "javax.microedition.io.InputConnection" "javax.microedition.io.OutputConnection" "javax.microedition.io.ContentConnection" "javax.microedition.io.StreamConnection" "javax.microedition.io.Datagram" "javax.microedition.io.DatagramConnection" "javax.microedition.io.StreamConnectionNotifier" "com.sun.cldc.i18n.uclc.DefaultCaseConverter" "com.sun.cldc.i18n.Helper" "com.sun.cldc.i18n.StreamReader" "com.sun.cldc.i18n.StreamWriter" "com.sun.cldc.io.ConnectionBaseInterface" "com.sun.cldc.io.GeneralBase" "com.sun.cldc.util.TimeZoneImplementation" "Apprentice" "Container" "Job" "Main6" "Main5" "Main4" "Main3" "Main2" "First" "FirstX" "Second" "Fact" "FactHelper" "FactJob" "Main" "ExceptionTest" "Demo") m6 >(pe 'execute-ILOAD_0) d 1 (INCLUDE-BOOK "/u/moore/m6/currentwork/src/M6/m6-start-jvm") \ [Included books, outermost to innermost: "/u/moore/m6/currentwork/src/M6/m6-start-jvm.lisp" "/u/moore/m6/currentwork/src/M6/m6-interpreter.lisp" "/u/moore/m6/currentwork/src/M6/m6-bytecode.lisp" "/u/moore/m6/currentwork/src/M6/m6-type-value.lisp" "/u/moore/m6/currentwork/src/M6/m6-static-initializer.lisp" "/u/moore/m6/currentwork/src/M6/m6-linker.lisp" ] \ >L (DEFUN EXECUTE-ILOAD_0 (INST S) (ADVANCE-PC (PUSHSTACK (LP 0) S))) m6 >(pe 'execute-IADD) d 1 (INCLUDE-BOOK "/u/moore/m6/currentwork/src/M6/m6-start-jvm") \ [Included books, outermost to innermost: "/u/moore/m6/currentwork/src/M6/m6-start-jvm.lisp" "/u/moore/m6/currentwork/src/M6/m6-interpreter.lisp" "/u/moore/m6/currentwork/src/M6/m6-bytecode.lisp" "/u/moore/m6/currentwork/src/M6/m6-type-value.lisp" "/u/moore/m6/currentwork/src/M6/m6-static-initializer.lisp" "/u/moore/m6/currentwork/src/M6/m6-linker.lisp" ] \ >L (DEFUN EXECUTE-IADD (INST S) (LET ((V1 (TOPSTACK S)) (V2 (SECONDSTACK S))) (ADVANCE-PC (PUSHSTACK (INT-FIX (+ V1 V2)) (POPSTACK (POPSTACK S)))))) m6 >(pe 'execute-INVOKEVIRTUAL) d 1 (INCLUDE-BOOK "/u/moore/m6/currentwork/src/M6/m6-start-jvm") \ [Included books, outermost to innermost: "/u/moore/m6/currentwork/src/M6/m6-start-jvm.lisp" "/u/moore/m6/currentwork/src/M6/m6-interpreter.lisp" "/u/moore/m6/currentwork/src/M6/m6-bytecode.lisp" "/u/moore/m6/currentwork/src/M6/m6-type-value.lisp" "/u/moore/m6/currentwork/src/M6/m6-static-initializer.lisp" "/u/moore/m6/currentwork/src/M6/m6-linker.lisp" ] \ >L (DEFUN EXECUTE-INVOKEVIRTUAL (INST S) (LET* ((METHODCP (ARG INST)) (METHOD-PTR (METHODCP-TO-METHOD-PTR METHODCP))) (MV-LET (METHOD-REP NEW-S) (RESOLVEMETHODREFERENCE METHOD-PTR NIL S) (IF (PENDING-EXCEPTION S) (RAISE-EXCEPTION (PENDING-EXCEPTION S) S) (LET ((THIS-REF (TOPSTACK (POPSTACKN (METHOD-ARGS-COUNT METHOD-REP) NEW-S)))) (IF (CHECK-NULL THIS-REF) (RAISE-EXCEPTION "java.lang.NullPointerException" S) (IF METHOD-REP (LET* ((DYNAMICCLASS (OBJ-TYPE (BINDING THIS-REF (HEAP S)))) (NEW-METHOD-PTR (MAKE-METHOD-PTR DYNAMICCLASS (METHOD-PTR-METHODNAME METHOD-PTR) (METHOD-PTR-ARGS-TYPE METHOD-PTR) (METHOD-PTR-RETURNTYPE METHOD-PTR))) (CLOSEST-METHOD (LOOKUPMETHOD NEW-METHOD-PTR NEW-S))) (IF CLOSEST-METHOD (CALL_VIRTUAL_METHOD THIS-REF CLOSEST-METHOD NEW-S) (FATALSLOTERROR METHODCP NEW-S))) (FATALSLOTERROR METHODCP NEW-S)))))))) m6 >(pe 'simple-run) d 1 (INCLUDE-BOOK "/u/moore/m6/currentwork/src/M6/m6-start-jvm") \ [Included books, outermost to innermost: "/u/moore/m6/currentwork/src/M6/m6-start-jvm.lisp" "/u/moore/m6/currentwork/src/M6/m6-interpreter.lisp" ] \ >L d (DEFUN SIMPLE-RUN (S N) (IF (ZP N) S (SIMPLE-RUN (M6STEP S) (- N 1)))) m6 >(pe 'm6step) d 1 (INCLUDE-BOOK "/u/moore/m6/currentwork/src/M6/m6-start-jvm") \ [Included books, outermost to innermost: "/u/moore/m6/currentwork/src/M6/m6-start-jvm.lisp" "/u/moore/m6/currentwork/src/M6/m6-interpreter.lisp" ] \ >L d (DEFUN M6STEP (S) (LET* ((INST (NEXT-INST S)) (OP (INST-OPCODE INST))) (IF (NO-FATAL-ERROR? S) (PROG2$ (DEBUG-PRINT "thread ~p0 executing inst ~p1~%Current pc ~p2~%" (CURRENT-THREAD S) INST (PC S)) (IF (EQUAL OP 'INVALID-OP-CODE) (FATALERROR "impossible: opcode invalid" S) (CASE OP (NOP (EXECUTE-NOP INST S)) (ICONST_M1 (EXECUTE-ICONST_M1 INST S)) (ICONST_0 (EXECUTE-ICONST_0 INST S)) (ICONST_1 (EXECUTE-ICONST_1 INST S)) (ICONST_2 (EXECUTE-ICONST_2 INST S)) (ICONST_3 (EXECUTE-ICONST_3 INST S)) (ICONST_4 (EXECUTE-ICONST_4 INST S)) (ICONST_5 (EXECUTE-ICONST_5 INST S)) (LCONST_0 (EXECUTE-LCONST_0 INST S)) (LCONST_1 (EXECUTE-LCONST_1 INST S)) (ACONST_NULL (EXECUTE-ACONST_NULL INST S)) (BIPUSH (EXECUTE-BIPUSH INST S)) (SIPUSH (EXECUTE-SIPUSH INST S)) (LDC (EXECUTE-LDC INST S)) (ILOAD (EXECUTE-ILOAD INST S)) (LLOAD (EXECUTE-LLOAD INST S)) (ALOAD (EXECUTE-ALOAD INST S)) (ILOAD_0 (EXECUTE-ILOAD_0 INST S)) (ILOAD_1 (EXECUTE-ILOAD_1 INST S)) (ILOAD_2 (EXECUTE-ILOAD_2 INST S)) (ILOAD_3 (EXECUTE-ILOAD_3 INST S)) (ALOAD_0 (EXECUTE-ALOAD_0 INST S)) (ALOAD_1 (EXECUTE-ALOAD_1 INST S)) (ALOAD_2 (EXECUTE-ALOAD_2 INST S)) (ALOAD_3 (EXECUTE-ALOAD_3 INST S)) (IALOAD (EXECUTE-IALOAD INST S)) (LALOAD (EXECUTE-LALOAD INST S)) (AALOAD (EXECUTE-AALOAD INST S)) (BALOAD (EXECUTE-BALOAD INST S)) (ISTORE (EXECUTE-ISTORE INST S)) (LSTORE (EXECUTE-LSTORE INST S)) (ASTORE (EXECUTE-ASTORE INST S)) (ISTORE_0 (EXECUTE-ISTORE_0 INST S)) (ISTORE_1 (EXECUTE-ISTORE_1 INST S)) (ISTORE_2 (EXECUTE-ISTORE_2 INST S)) (ISTORE_3 (EXECUTE-ISTORE_3 INST S)) (LSTORE_0 (EXECUTE-LSTORE_0 INST S)) (LSTORE_1 (EXECUTE-LSTORE_1 INST S)) (LSTORE_2 (EXECUTE-LSTORE_2 INST S)) (LSTORE_3 (EXECUTE-LSTORE_3 INST S)) (ASTORE_0 (EXECUTE-ASTORE_0 INST S)) (ASTORE_1 (EXECUTE-ASTORE_1 INST S)) (ASTORE_2 (EXECUTE-ASTORE_2 INST S)) (ASTORE_3 (EXECUTE-ASTORE_3 INST S)) (IASTORE (EXECUTE-IASTORE INST S)) (LASTORE (EXECUTE-LASTORE INST S)) (AASTORE (EXECUTE-AASTORE INST S)) (BASTORE (EXECUTE-BASTORE INST S)) (CALOAD (EXECUTE-CALOAD INST S)) (CASTORE (EXECUTE-CASTORE INST S)) (SASTORE (EXECUTE-SASTORE INST S)) (POP (EXECUTE-POP INST S)) (POP2 (EXECUTE-POP2 INST S)) (DUP (EXECUTE-DUP INST S)) (DUP_X1 (EXECUTE-DUP_X1 INST S)) (DUP_X2 (EXECUTE-DUP_X2 INST S)) (DUP2 (EXECUTE-DUP2 INST S)) (DUP2_X1 (EXECUTE-DUP2_X1 INST S)) (DUP2_X2 (EXECUTE-DUP2_X2 INST S)) (SWAP (EXECUTE-SWAP INST S)) (IADD (EXECUTE-IADD INST S)) (ISUB (EXECUTE-ISUB INST S)) (IMUL (EXECUTE-IMUL INST S)) (IDIV (EXECUTE-IDIV INST S)) (IREM (EXECUTE-IREM INST S)) (INEG (EXECUTE-INEG INST S)) (IINC (EXECUTE-IINC INST S)) (NEWARRAY (EXECUTE-NEWARRAY INST S)) (ARRAYLENGTH (EXECUTE-ARRAYLENGTH INST S)) (MONITORENTER (EXECUTE-MONITORENTER INST S)) (MONITOREXIT (EXECUTE-MONITOREXIT INST S)) (CHECKCAST (EXECUTE-CHECKCAST INST S)) (CUSTOMCODE (EXECUTE-CUSTOMCODE INST S)) (ISTORE_1 (EXECUTE-ISTORE_1 INST S)) (ISTORE_2 (EXECUTE-ISTORE_2 INST S)) (IADD (EXECUTE-IADD INST S)) (NEW (EXECUTE-NEW INST S)) (LDC (EXECUTE-LDC INST S)) (INVOKESPECIAL (EXECUTE-INVOKESPECIAL INST S)) (INVOKESTATIC (EXECUTE-INVOKESTATIC INST S)) (INVOKEVIRTUAL (EXECUTE-INVOKEVIRTUAL INST S)) (INVOKEINTERFACE (EXECUTE-INVOKEINTERFACE INST S)) (ASTORE_3 (EXECUTE-ASTORE_3 INST S)) (ALOAD_0 (EXECUTE-ALOAD_0 INST S)) (PUTFIELD (EXECUTE-PUTFIELD INST S)) (GETFIELD (EXECUTE-GETFIELD INST S)) (GETSTATIC (EXECUTE-GETSTATIC INST S)) (PUTSTATIC (EXECUTE-PUTSTATIC INST S)) (CASTORE (EXECUTE-CASTORE INST S)) (PUTSTATIC (EXECUTE-PUTSTATIC INST S)) (IFNULL (EXECUTE-IFNULL INST S)) (IFNONNULL (EXECUTE-IFNONNULL INST S)) (IFEQ (EXECUTE-IFEQ INST S)) (IFNE (EXECUTE-IFNE INST S)) (IFLT (EXECUTE-IFLT INST S)) (IFGE (EXECUTE-IFGE INST S)) (IFGT (EXECUTE-IFGT INST S)) (IFLE (EXECUTE-IFLE INST S)) (IF_ICMPEQ (EXECUTE-IF_ICMPEQ INST S)) (IF_ICMPNE (EXECUTE-IF_ICMPNE INST S)) (IF_ICMPLT (EXECUTE-IF_ICMPLT INST S)) (IF_ICMPGE (EXECUTE-IF_ICMPGE INST S)) (IF_ICMPGT (EXECUTE-IF_ICMPGT INST S)) (IF_ICMPLE (EXECUTE-IF_ICMPLE INST S)) (GOTO (EXECUTE-GOTO INST S)) (IRETURN (EXECUTE-RETURN INST S 1)) (RETURN (EXECUTE-RETURN INST S 0)) (ARETURN (EXECUTE-RETURN INST S 1)) (ATHROW (EXECUTE-ATHROW INST S)) (JSR (EXECUTE-JSR INST S)) (RET (EXECUTE-RET INST S)) (T S)))) S))) m6 >(jvm-Demo "246") output from the stream at heap ref 91 is "123" output from the stream at heap ref 91 is "newline" ((CLASSES-LOADED "com.sun.cldc.i18n.uclc.DefaultCaseConverter" "java.io.PrintStream" "java.io.OutputStream" "java.lang.Character" "java.lang.Integer") (OUTPUT-STREAM . "123 ")) m6 >(jvm-Demo "245") (TIMEOUT AFTER 5000 STEPS) m6 >(defconst *program-pi* ; public static int half(int n){ ; int a = 0; ; while (n!=0){a=a+1;n=n-2;}; ; return a; ; } '(( 0 (iconst_0)) ( 1 (istore_1)) ( 2 (goto 13)) ( 5 (iload_1)) ( 6 (iconst_1)) ( 7 (iadd)) ( 8 (istore_1)) ( 9 (iload_0)) (10 (iconst_2)) (11 (isub)) (12 (istore_0)) (13 (iload_0)) (14 (ifne 5)) (17 (iload_1)) (18 (halt)))) Summary Form: ( DEFCONST *PROGRAM-PI* ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *PROGRAM-PI* m6 >(defun n (s) (local-at 0 s)) Since N is non-recursive, its admission is trivial. We could deduce no constraints on the type of N. Summary Form: ( DEFUN N ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) N m6 >(defun a (s) (local-at 1 s)) Since A is non-recursive, its admission is trivial. We could deduce no constraints on the type of A. Summary Form: ( DEFUN A ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) A m6 >(defspec pi *program-pi* (n0) 0 18 (; Pre-Condition: (0 (and (equal (n s) n0) (intp n0) (<= 0 n0))) ; Loop Invariant: (13 (and (intp n0) (<= 0 n0) (intp (n s)) (if (and (<= 0 (n s)) (intp (a s)) (evenp (n s))) (equal (int-fix (+ (a s) (/ (n s) 2))) (/ n0 2)) (not (evenp (n s)))) (iff (evenp n0) (evenp (n s))))) ; Post-condition: (18 (and (evenp n0) (equal (topstack s) (/ n0 2)))))) To verify that the eight encapsulated events correctly extend the current theory we will evaluate them. The theory thus constructed is only ephemeral. Encapsulated Events: m6 >>(SET-IGNORE-OK T) T m6 >>(SET-IRRELEVANT-FORMALS-OK T) T m6 >>(LOCAL (DEFUN |PI-INV-arity-1-test| (ACL2::X) (LET ((N0 (CAR ACL2::X)) (S (CAR (CDR ACL2::X)))) (MEMBER (PC S) '(0 13 18))))) Since |PI-INV-arity-1-test| is non-recursive, its admission is trivial. We observe that the type of |PI-INV-arity-1-test| is described by the theorem (OR (CONSP (|PI-INV-arity-1-test| ACL2::X)) (EQUAL (|PI-INV-arity-1-test| ACL2::X) NIL)). We used the :type-prescription rule MEMBER. ;Compiler warnings : ; Unused lexical variable \m6::N0, in ACL2_*1*_\m6::|PI-INV-arity-1-test| inside ACL2_*1*_\m6::|PI-INV-arity-1-test|. ;Compiler warnings : ; Unused lexical variable \m6::N0, in \m6::|PI-INV-arity-1-test|. Summary Form: ( DEFUN |PI-INV-arity-1-test| ...) Rules: ((:TYPE-PRESCRIPTION MEMBER)) Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.01, other: 0.01) |PI-INV-arity-1-test| m6 >>(LOCAL (DEFUN |PI-INV-arity-1-base| (ACL2::X) (LET ((N0 (CAR ACL2::X)) (S (CAR (CDR ACL2::X)))) (AND (PROGRAM-IS *PROGRAM-PI* S) (CASE (PC S) (0 (AND (EQUAL (N S) N0) (INTP N0) (<= 0 N0))) (13 (AND (INTP N0) (<= 0 N0) (INTP (N S)) (IF (AND (<= 0 (N S)) (INTP (A S)) (EVENP (N S))) (EQUAL (INT-FIX (+ (A S) (/ (N S) 2))) (/ N0 2)) (NOT (EVENP (N S)))) (IFF (EVENP N0) (EVENP (N S))))) (18 (AND (EVENP N0) (EQUAL (TOPSTACK S) (/ N0 2))))))))) Since |PI-INV-arity-1-base| is non-recursive, its admission is trivial. We observe that the type of |PI-INV-arity-1-base| is described by the theorem (OR (EQUAL (|PI-INV-arity-1-base| ACL2::X) T) (EQUAL (|PI-INV-arity-1-base| ACL2::X) NIL)). We used primitive type reasoning and the :type- prescription rules EVENP and IFF. Summary Form: ( DEFUN |PI-INV-arity-1-base| ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION EVENP) (:TYPE-PRESCRIPTION IFF)) Warnings: None Time: 0.04 seconds (prove: 0.00, print: 0.01, other: 0.03) |PI-INV-arity-1-base| m6 >>(LOCAL (DEFUN |PI-INV-arity-1-step| (ACL2::X) (LET ((N0 (CAR ACL2::X)) (S (CAR (CDR ACL2::X)))) (LIST N0 (M6STEP S))))) Since |PI-INV-arity-1-step| is non-recursive, its admission is trivial. We observe that the type of |PI-INV-arity-1-step| is described by the theorem (AND (CONSP (|PI-INV-arity-1-step| ACL2::X)) (TRUE-LISTP (|PI-INV-arity-1-step| ACL2::X))). We used primitive type reasoning. Summary Form: ( DEFUN |PI-INV-arity-1-step| ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.01) |PI-INV-arity-1-step| m6 >>(LOCAL (ENCAPSULATE ((|PI-INV-arity-1| (ACL2::X) T)) (LOCAL (IN-THEORY (DISABLE |PI-INV-arity-1-test| |PI-INV-arity-1-base| |PI-INV-arity-1-step|))) (LOCAL (DEFUN |PI-INV-arity-1-stn| (ACL2::X ACL2::N) (IF (ZP ACL2::N) ACL2::X (|PI-INV-arity-1-stn| (|PI-INV-arity-1-step| ACL2::X) (1- ACL2::N))))) (LOCAL (DEFCHOOSE |PI-INV-arity-1-fch| (ACL2::N) (ACL2::X) (|PI-INV-arity-1-test| (|PI-INV-arity-1-stn| ACL2::X ACL2::N)))) (LOCAL (DEFUN |PI-INV-arity-1-fn| (ACL2::X ACL2::N) (DECLARE (XARGS :MEASURE (NFIX ACL2::N))) (IF (OR (ZP ACL2::N) (|PI-INV-arity-1-test| ACL2::X)) (|PI-INV-arity-1-base| ACL2::X) (|PI-INV-arity-1-fn| (|PI-INV-arity-1-step| ACL2::X) (1- ACL2::N))))) (LOCAL (DEFUN |PI-INV-arity-1| (ACL2::X) (IF (|PI-INV-arity-1-test| (|PI-INV-arity-1-stn| ACL2::X (|PI-INV-arity-1-fch| ACL2::X))) (|PI-INV-arity-1-fn| ACL2::X (|PI-INV-arity-1-fch| ACL2::X)) NIL))) (LOCAL (IN-THEORY '(|PI-INV-arity-1| |PI-INV-arity-1-test| |PI-INV-arity-1-base| |PI-INV-arity-1-step| |PI-INV-arity-1-stn| |PI-INV-arity-1-fn| (:TYPE-PRESCRIPTION |PI-INV-arity-1-fn|)))) (DEFTHM |PI-INV-arity-1-DEF| (EQUAL (|PI-INV-arity-1| ACL2::X) (IF (|PI-INV-arity-1-test| ACL2::X) (|PI-INV-arity-1-base| ACL2::X) (|PI-INV-arity-1| (|PI-INV-arity-1-step| ACL2::X)))) :HINTS (("Goal" :USE (:FUNCTIONAL-INSTANCE ACL2::GENERIC-TAIL-RECURSIVE-F (ACL2::F |PI-INV-arity-1|) (ACL2::TEST |PI-INV-arity-1-test|) (ACL2::BASE |PI-INV-arity-1-base|) (ACL2::ST |PI-INV-arity-1-step|) (ACL2::STN |PI-INV-arity-1-stn|) (ACL2::FCH |PI-INV-arity-1-fch|) (ACL2::FN |PI-INV-arity-1-fn|))) ("Subgoal 2" :USE |PI-INV-arity-1-fch|)) :RULE-CLASSES NIL))) To verify that the seven encapsulated events correctly extend the current theory we will evaluate them. The theory thus constructed is only ephemeral. Encapsulated Events: m6 >>(LOCAL (IN-THEORY (DISABLE |PI-INV-arity-1-test| |PI-INV-arity-1-base| |PI-INV-arity-1-step|))) Summary Form: (IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.05 seconds (prove: 0.00, print: 0.00, other: 0.05) 6498 m6 >>(LOCAL (DEFUN |PI-INV-arity-1-stn| (ACL2::X ACL2::N) (IF (ZP ACL2::N) ACL2::X (|PI-INV-arity-1-stn| (|PI-INV-arity-1-step| ACL2::X) (1- ACL2::N))))) The admission of |PI-INV-arity-1-stn| is trivial, using the relation O< (which is known to be well- founded on the domain recognized by O-P) and the measure (ACL2-COUNT ACL2::N). We observe that the type of |PI-INV-arity-1-stn| is described by the theorem (OR (AND (CONSP (|PI-INV-arity-1-stn| ACL2::X ACL2::N)) (TRUE-LISTP (|PI-INV-arity-1-stn| ACL2::X ACL2::N))) (EQUAL (|PI-INV-arity-1-stn| ACL2::X ACL2::N) ACL2::X)). We used the :type-prescription rule |PI-INV-arity- 1-step|. Summary Form: ( DEFUN |PI-INV-arity-1-stn| ...) Rules: ((:TYPE-PRESCRIPTION |PI-INV-arity-1-step|)) Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.01, other: 0.01) |PI-INV-arity-1-stn| m6 >>(LOCAL (DEFCHOOSE |PI-INV-arity-1-fch| (ACL2::N) (ACL2::X) (|PI-INV-arity-1-test| (|PI-INV-arity-1-stn| ACL2::X ACL2::N)))) Summary Form: ( DEFCHOOSE |PI-INV-arity-1-fch| ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) |PI-INV-arity-1-fch| m6 >>(LOCAL (DEFUN |PI-INV-arity-1-fn| (ACL2::X ACL2::N) (DECLARE (XARGS :MEASURE (NFIX ACL2::N))) (IF (OR (ZP ACL2::N) (|PI-INV-arity-1-test| ACL2::X)) (|PI-INV-arity-1-base| ACL2::X) (|PI-INV-arity-1-fn| (|PI-INV-arity-1-step| ACL2::X) (1- ACL2::N))))) For the admission of |PI-INV-arity-1-fn| we will use the relation O< (which is known to be well- founded on the domain recognized by O-P) and the measure (NFIX ACL2::N). The non-trivial part of the measure conjecture is Goal (AND (O-P (NFIX ACL2::N)) (IMPLIES (NOT (OR (ZP ACL2::N) (|PI-INV-arity-1-test| ACL2::X))) (O< (NFIX (+ -1 ACL2::N)) (NFIX ACL2::N)))). By case analysis we reduce the conjecture to the following two conjectures. Subgoal 2 (O-P (NFIX ACL2::N)). But simplification reduces this to T, using the :definitions NATP, NFIX, O-FINP and O-P, the :executable- counterpart of < and the :rewrite rule ACL2::|(< (if x y z) w)|. Subgoal 1 (IMPLIES (NOT (OR (ZP ACL2::N) (|PI-INV-arity-1-test| ACL2::X))) (O< (NFIX (+ -1 ACL2::N)) (NFIX ACL2::N))). But simplification reduces this to T, using the :definitions FIX, NFIX, O-FINP, O< and ZP, the :executable-counterparts of < and BINARY-+, primitive type reasoning, the :meta rules ACL2::CANCEL-ADDENDS- <-THM and ACL2::PREFER-POSITIVE-ADDENDS-<-THM and the :rewrite rules ACL2::|(+ 0 x)|, ACL2::COLLECT- PLUS-1B, ACL2::COLLECT-PLUS-1C and ACL2::UN-HIDE- PLUS. Q.E.D. That completes the proof of the measure theorem for |PI-INV-arity-1-fn|. Thus, we admit this function under the principle of definition. We observe that the type of |PI-INV-arity-1-fn| is described by the theorem (OR (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) T) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). We used the :compound-recognizer rule ACL2::ZP- COMPOUND-RECOGNIZER and the :type-prescription rule |PI-INV-arity-1-base|. Summary Form: ( DEFUN |PI-INV-arity-1-fn| ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION FIX) (:DEFINITION NATP) (:DEFINITION NFIX) (:DEFINITION O-FINP) (:DEFINITION O-P) (:DEFINITION O<) (:DEFINITION ZP) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART BINARY-+) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:META ACL2::CANCEL-ADDENDS-<-THM) (:META ACL2::PREFER-POSITIVE-ADDENDS-<-THM) (:REWRITE ACL2::|(+ 0 x)|) (:REWRITE ACL2::|(< (if x y z) w)|) (:REWRITE ACL2::COLLECT-PLUS-1B) (:REWRITE ACL2::COLLECT-PLUS-1C) (:REWRITE ACL2::UN-HIDE-PLUS) (:TYPE-PRESCRIPTION |PI-INV-arity-1-base|)) Warnings: None Time: 0.07 seconds (prove: 0.00, print: 0.06, other: 0.01) |PI-INV-arity-1-fn| m6 >>(LOCAL (DEFUN |PI-INV-arity-1| (ACL2::X) (IF (|PI-INV-arity-1-test| (|PI-INV-arity-1-stn| ACL2::X (|PI-INV-arity-1-fch| ACL2::X))) (|PI-INV-arity-1-fn| ACL2::X (|PI-INV-arity-1-fch| ACL2::X)) NIL))) Since |PI-INV-arity-1| is non-recursive, its admission is trivial. We observe that the type of |PI-INV- arity-1| is described by the theorem (OR (EQUAL (|PI-INV-arity-1| ACL2::X) T) (EQUAL (|PI-INV-arity-1| ACL2::X) NIL)). We used the :type-prescription rule |PI-INV-arity- 1-fn|. Summary Form: ( DEFUN |PI-INV-arity-1| ...) Rules: ((:TYPE-PRESCRIPTION |PI-INV-arity-1-fn|)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.01) |PI-INV-arity-1| m6 >>(LOCAL (IN-THEORY '(|PI-INV-arity-1| |PI-INV-arity-1-test| |PI-INV-arity-1-base| |PI-INV-arity-1-step| |PI-INV-arity-1-stn| |PI-INV-arity-1-fn| (:TYPE-PRESCRIPTION |PI-INV-arity-1-fn|)))) ACL2 Warning [Theory] in (IN-THEORY (QUOTE ...)): The value of the theory expression '(|PI-INV-arity-1| |PI-INV-arity-1-test| |PI-INV-arity-1-base| |PI-INV-arity-1-step| |PI-INV-arity-1-stn| |PI-INV-arity-1-fn| (:TYPE-PRESCRIPTION |PI-INV-arity-1-fn|)) does not include the :DEFINITION rules for MV-NTH, IFF, NOT, IMPLIES, EQ, ATOM, EQL, =, /=, NULL, ENDP, ZEROP, SYNP, PLUSP, MINUSP, LISTP, PROG2$, ACL2::MUST-BE-EQUAL, FORCE or CASE-SPLIT. But these functions are among a set of primitive functions whose definitions are built into the ACL2 system in various places. This set consists of the functions MV-NTH, IFF, NOT, IMPLIES, EQ, ATOM, EQL, =, /=, NULL, ENDP, ZEROP, SYNP, PLUSP, MINUSP, LISTP, PROG2$, ACL2::MUST-BE-EQUAL, FORCE and CASE-SPLIT. While excluding them from the current theory will prevent certain expansions it will not prevent others. Good luck! ACL2 Warning [Theory] in (IN-THEORY (QUOTE ...)): The value of the theory expression '(|PI-INV-arity-1| |PI-INV-arity-1-test| |PI-INV-arity-1-base| |PI-INV-arity-1-step| |PI-INV-arity-1-stn| |PI-INV-arity-1-fn| (:TYPE-PRESCRIPTION |PI-INV-arity-1-fn|)) does not include the :EXECUTABLE-COUNTERPART rules for ACL2-NUMBERP, BINARY-*, BINARY-+, UNARY--, UNARY-/, <, CAR, CDR, CHAR-CODE, CHARACTERP, CODE- CHAR, COMPLEX, COMPLEX-RATIONALP, COERCE, CONS, CONSP, DENOMINATOR, EQUAL, IF, IMAGPART, INTEGERP, INTERN-IN-PACKAGE-OF-SYMBOL, NUMERATOR, ACL2::- PKG-WITNESS, RATIONALP, REALPART, STRINGP, SYMBOL- NAME, SYMBOL-PACKAGE-NAME, SYMBOLP or NOT. But these functions are among a set of primitive functions whose executable counterparts are built into the ACL2 system. This set consists of the functions ACL2-NUMBERP, BINARY-*, BINARY-+, UNARY--, UNARY- /, <, CAR, CDR, CHAR-CODE, CHARACTERP, CODE-CHAR, COMPLEX, COMPLEX-RATIONALP, COERCE, CONS, CONSP, DENOMINATOR, EQUAL, IF, IMAGPART, INTEGERP, INTERN- IN-PACKAGE-OF-SYMBOL, NUMERATOR, ACL2::PKG-WITNESS, RATIONALP, REALPART, STRINGP, SYMBOL-NAME, SYMBOL- PACKAGE-NAME, SYMBOLP and NOT. While excluding them from the current theory may prevent certain expansions it will not prevent others. Good luck! ACL2 Warning [Disable] in (IN-THEORY (QUOTE ...)): Forcing has transitioned from enabled to disabled. See :DOC force. Summary Form: (IN-THEORY (QUOTE ...)) Rules: NIL Warnings: Disable and Theory Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04) 9 m6 >>(DEFTHM |PI-INV-arity-1-DEF| (EQUAL (|PI-INV-arity-1| ACL2::X) (IF (|PI-INV-arity-1-test| ACL2::X) (|PI-INV-arity-1-base| ACL2::X) (|PI-INV-arity-1| (|PI-INV-arity-1-step| ACL2::X)))) :HINTS (("Goal" :USE (:FUNCTIONAL-INSTANCE ACL2::GENERIC-TAIL-RECURSIVE-F (ACL2::F |PI-INV-arity-1|) (ACL2::TEST |PI-INV-arity-1-test|) (ACL2::BASE |PI-INV-arity-1-base|) (ACL2::ST |PI-INV-arity-1-step|) (ACL2::STN |PI-INV-arity-1-stn|) (ACL2::FCH |PI-INV-arity-1-fch|) (ACL2::FN |PI-INV-arity-1-fn|))) ("Subgoal 2" :USE |PI-INV-arity-1-fch|)) :RULE-CLASSES NIL) [Note: A hint was supplied for our processing of the goal above. Thanks!] We now augment the goal above by adding the hypothesis indicated by the :USE hint. This produces a proposition\ al tautology. The hypothesis can be derived from ACL2::GENERIC-TAIL-RECURSIVE-F via functional instantiat\ ion, provided we can establish the four constraints generated. Subgoal 4 (EQUAL (|PI-INV-arity-1| ACL2::X) (AND (|PI-INV-arity-1-test| (|PI-INV-arity-1-stn| ACL2::X (|PI-INV-arity-1-fch| ACL2::X))) (|PI-INV-arity-1-fn| ACL2::X (|PI-INV-arity-1-fch| ACL2::X)))). But simplification reduces this to T, using the :definitions |PI-INV-arity-1| and |PI-INV-arity- 1-test| and primitive type reasoning. Subgoal 3 (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) (IF (OR (ZP ACL2::N) (|PI-INV-arity-1-test| ACL2::X)) (|PI-INV-arity-1-base| ACL2::X) (|PI-INV-arity-1-fn| (|PI-INV-arity-1-step| ACL2::X) (+ -1 ACL2::N)))). This simplifies, using the :definitions |PI-INV- arity-1-base|, |PI-INV-arity-1-step| and |PI-INV- arity-1-test|, to the following 33 conjectures. Subgoal 3.33 (IMPLIES (AND (NOT (ZP ACL2::N)) (NOT (MEMBER (PC (CADR ACL2::X)) '(0 13 18)))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) (|PI-INV-arity-1-fn| (LIST (CAR ACL2::X) (M6STEP (CADR ACL2::X))) (+ -1 ACL2::N)))). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-fn|, |PI-INV-arity- 1-step| and |PI-INV-arity-1-test| and primitive type reasoning. Subgoal 3.32 (IMPLIES (AND (ZP ACL2::N) (NOT (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) (CADR ACL2::X)))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base| and |PI-INV- arity-1-fn| and primitive type reasoning. Subgoal 3.31 (IMPLIES (AND (ZP ACL2::N) (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) (CADR ACL2::X)) (EQUAL (PC (CADR ACL2::X)) 18) (EVENP (CAR ACL2::X))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) (EQUAL (TOPSTACK (CADR ACL2::X)) (* (CAR ACL2::X) 1/2)))). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base| and |PI-INV- arity-1-fn| and primitive type reasoning. Subgoal 3.30 (IMPLIES (AND (ZP ACL2::N) (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) (CADR ACL2::X)) (EQUAL (PC (CADR ACL2::X)) 13) (INTP (CAR ACL2::X)) (<= 0 (CAR ACL2::X)) (INTP (N (CADR ACL2::X))) (NOT (EVENP (N (CADR ACL2::X))))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) (IFF (EVENP (CAR ACL2::X)) NIL))). By the :executable-counterpart of IF we reduce the conjecture to Subgoal 3.30' (IMPLIES (AND (ZP ACL2::N) (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) (CADR ACL2::X)) (EQUAL (PC (CADR ACL2::X)) 13) (INTP (CAR ACL2::X)) (<= 0 (CAR ACL2::X)) (INTP (N (CADR ACL2::X))) (NOT (EVENP (N (CADR ACL2::X))))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) (AND (NOT (EVENP (CAR ACL2::X))) T))). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base| and |PI-INV- arity-1-fn| and primitive type reasoning. Subgoal 3.29 (IMPLIES (AND (ZP ACL2::N) (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) (CADR ACL2::X)) (EQUAL (PC (CADR ACL2::X)) 13) (INTP (CAR ACL2::X)) (<= 0 (CAR ACL2::X)) (INTP (N (CADR ACL2::X))) (<= 0 (N (CADR ACL2::X))) (INTP (A (CADR ACL2::X))) (EVENP (N (CADR ACL2::X))) (EQUAL (INT-FIX (+ (A (CADR ACL2::X)) (* (N (CADR ACL2::X)) 1/2))) (* (CAR ACL2::X) 1/2))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) (IFF (EVENP (CAR ACL2::X)) T))). By the :executable-counterpart of IF we reduce the conjecture to Subgoal 3.29' (IMPLIES (AND (ZP ACL2::N) (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) (CADR ACL2::X)) (EQUAL (PC (CADR ACL2::X)) 13) (INTP (CAR ACL2::X)) (<= 0 (CAR ACL2::X)) (INTP (N (CADR ACL2::X))) (<= 0 (N (CADR ACL2::X))) (INTP (A (CADR ACL2::X))) (EVENP (N (CADR ACL2::X))) (EQUAL (INT-FIX (+ (A (CADR ACL2::X)) (* (N (CADR ACL2::X)) 1/2))) (* (CAR ACL2::X) 1/2))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) (AND (EVENP (CAR ACL2::X)) T))). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base| and |PI-INV- arity-1-fn| and primitive type reasoning. Subgoal 3.28 (IMPLIES (AND (ZP ACL2::N) (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) (CADR ACL2::X)) (EQUAL (PC (CADR ACL2::X)) 0) (EQUAL (N (CADR ACL2::X)) (CAR ACL2::X)) (INTP (CAR ACL2::X)) (<= 0 (CAR ACL2::X))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) T)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base| and |PI-INV- arity-1-fn| and primitive type reasoning. Subgoal 3.27 (IMPLIES (AND (ZP ACL2::N) (EQUAL (PC (CADR ACL2::X)) 13) (< (CAR ACL2::X) 0)) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base| and |PI-INV- arity-1-fn| and primitive type reasoning. Subgoal 3.26 (IMPLIES (AND (ZP ACL2::N) (EQUAL (PC (CADR ACL2::X)) 13) (NOT (INTP (CAR ACL2::X)))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base| and |PI-INV- arity-1-fn| and primitive type reasoning. Subgoal 3.25 (IMPLIES (AND (ZP ACL2::N) (NOT (EQUAL (PC (CADR ACL2::X)) 0)) (NOT (EQUAL (PC (CADR ACL2::X)) 13)) (NOT (EVENP (CAR ACL2::X)))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base| and |PI-INV- arity-1-fn| and primitive type reasoning. Subgoal 3.24 (IMPLIES (AND (ZP ACL2::N) (EQUAL (PC (CADR ACL2::X)) 13) (NOT (INTP (N (CADR ACL2::X))))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base| and |PI-INV- arity-1-fn| and primitive type reasoning. Subgoal 3.23 (IMPLIES (AND (ZP ACL2::N) (NOT (EQUAL (PC (CADR ACL2::X)) 0)) (NOT (EQUAL (PC (CADR ACL2::X)) 13)) (NOT (EQUAL (PC (CADR ACL2::X)) 18))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base| and |PI-INV- arity-1-fn| and primitive type reasoning. Subgoal 3.22 (IMPLIES (AND (ZP ACL2::N) (EQUAL (PC (CADR ACL2::X)) 13) (EVENP (N (CADR ACL2::X))) (NOT (EQUAL (INT-FIX (+ (A (CADR ACL2::X)) (* (N (CADR ACL2::X)) 1/2))) (* (CAR ACL2::X) 1/2)))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base| and |PI-INV- arity-1-fn| and primitive type reasoning. Subgoal 3.21 (IMPLIES (AND (ZP ACL2::N) (EQUAL (PC (CADR ACL2::X)) 13) (NOT (INTP (A (CADR ACL2::X)))) (EVENP (N (CADR ACL2::X)))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base| and |PI-INV- arity-1-fn| and primitive type reasoning. Subgoal 3.20 (IMPLIES (AND (ZP ACL2::N) (EQUAL (PC (CADR ACL2::X)) 13) (< (N (CADR ACL2::X)) 0) (EVENP (N (CADR ACL2::X)))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base| and |PI-INV- arity-1-fn| and primitive type reasoning. Subgoal 3.19 (IMPLIES (AND (ZP ACL2::N) (EQUAL (PC (CADR ACL2::X)) 0) (NOT (EQUAL (N (CADR ACL2::X)) (CAR ACL2::X)))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base| and |PI-INV- arity-1-fn| and primitive type reasoning. Subgoal 3.18 (IMPLIES (AND (ZP ACL2::N) (EQUAL (PC (CADR ACL2::X)) 0) (< (CAR ACL2::X) 0)) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base| and |PI-INV- arity-1-fn| and primitive type reasoning. Subgoal 3.17 (IMPLIES (AND (ZP ACL2::N) (EQUAL (PC (CADR ACL2::X)) 0) (NOT (INTP (CAR ACL2::X)))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base| and |PI-INV- arity-1-fn| and primitive type reasoning. Subgoal 3.16 (IMPLIES (AND (MEMBER (PC (CADR ACL2::X)) '(0 13 18)) (NOT (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) (CADR ACL2::X)))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base|, |PI-INV-arity- 1-fn| and |PI-INV-arity-1-test| and primitive type reasoning. Subgoal 3.15 (IMPLIES (AND (MEMBER 0 '(0 13 18)) (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) (CADR ACL2::X)) (EQUAL (PC (CADR ACL2::X)) 0) (EQUAL (N (CADR ACL2::X)) (CAR ACL2::X)) (INTP (CAR ACL2::X)) (<= 0 (CAR ACL2::X))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) T)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base|, |PI-INV-arity- 1-fn| and |PI-INV-arity-1-test| and primitive type reasoning. Subgoal 3.14 (IMPLIES (AND (MEMBER 18 '(0 13 18)) (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) (CADR ACL2::X)) (EQUAL (PC (CADR ACL2::X)) 18) (EVENP (CAR ACL2::X))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) (EQUAL (TOPSTACK (CADR ACL2::X)) (* (CAR ACL2::X) 1/2)))). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base|, |PI-INV-arity- 1-fn| and |PI-INV-arity-1-test| and primitive type reasoning. Subgoal 3.13 (IMPLIES (AND (MEMBER 13 '(0 13 18)) (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) (CADR ACL2::X)) (EQUAL (PC (CADR ACL2::X)) 13) (INTP (CAR ACL2::X)) (<= 0 (CAR ACL2::X)) (INTP (N (CADR ACL2::X))) (NOT (EVENP (N (CADR ACL2::X))))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) (IFF (EVENP (CAR ACL2::X)) NIL))). By the :executable-counterpart of IF we reduce the conjecture to Subgoal 3.13' (IMPLIES (AND (MEMBER 13 '(0 13 18)) (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) (CADR ACL2::X)) (EQUAL (PC (CADR ACL2::X)) 13) (INTP (CAR ACL2::X)) (<= 0 (CAR ACL2::X)) (INTP (N (CADR ACL2::X))) (NOT (EVENP (N (CADR ACL2::X))))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) (AND (NOT (EVENP (CAR ACL2::X))) T))). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base|, |PI-INV-arity- 1-fn| and |PI-INV-arity-1-test| and primitive type reasoning. Subgoal 3.12 (IMPLIES (AND (MEMBER 13 '(0 13 18)) (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) (CADR ACL2::X)) (EQUAL (PC (CADR ACL2::X)) 13) (INTP (CAR ACL2::X)) (<= 0 (CAR ACL2::X)) (INTP (N (CADR ACL2::X))) (<= 0 (N (CADR ACL2::X))) (INTP (A (CADR ACL2::X))) (EVENP (N (CADR ACL2::X))) (EQUAL (INT-FIX (+ (A (CADR ACL2::X)) (* (N (CADR ACL2::X)) 1/2))) (* (CAR ACL2::X) 1/2))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) (IFF (EVENP (CAR ACL2::X)) T))). By the :executable-counterpart of IF we reduce the conjecture to Subgoal 3.12' (IMPLIES (AND (MEMBER 13 '(0 13 18)) (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) (CADR ACL2::X)) (EQUAL (PC (CADR ACL2::X)) 13) (INTP (CAR ACL2::X)) (<= 0 (CAR ACL2::X)) (INTP (N (CADR ACL2::X))) (<= 0 (N (CADR ACL2::X))) (INTP (A (CADR ACL2::X))) (EVENP (N (CADR ACL2::X))) (EQUAL (INT-FIX (+ (A (CADR ACL2::X)) (* (N (CADR ACL2::X)) 1/2))) (* (CAR ACL2::X) 1/2))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) (AND (EVENP (CAR ACL2::X)) T))). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base|, |PI-INV-arity- 1-fn| and |PI-INV-arity-1-test| and primitive type reasoning. Subgoal 3.11 (IMPLIES (AND (MEMBER 0 '(0 13 18)) (EQUAL (PC (CADR ACL2::X)) 0) (NOT (INTP (CAR ACL2::X)))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base|, |PI-INV-arity- 1-fn| and |PI-INV-arity-1-test| and primitive type reasoning. Subgoal 3.10 (IMPLIES (AND (MEMBER 0 '(0 13 18)) (EQUAL (PC (CADR ACL2::X)) 0) (NOT (EQUAL (N (CADR ACL2::X)) (CAR ACL2::X)))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base|, |PI-INV-arity- 1-fn| and |PI-INV-arity-1-test| and primitive type reasoning. Subgoal 3.9 (IMPLIES (AND (MEMBER 0 '(0 13 18)) (EQUAL (PC (CADR ACL2::X)) 0) (< (CAR ACL2::X) 0)) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base|, |PI-INV-arity- 1-fn| and |PI-INV-arity-1-test| and primitive type reasoning. Subgoal 3.8 (IMPLIES (AND (MEMBER (PC (CADR ACL2::X)) '(0 13 18)) (NOT (EQUAL (PC (CADR ACL2::X)) 0)) (NOT (EQUAL (PC (CADR ACL2::X)) 13)) (NOT (EVENP (CAR ACL2::X)))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base|, |PI-INV-arity- 1-fn| and |PI-INV-arity-1-test| and primitive type reasoning. Subgoal 3.7 (IMPLIES (AND (MEMBER 13 '(0 13 18)) (EQUAL (PC (CADR ACL2::X)) 13) (NOT (INTP (N (CADR ACL2::X))))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base|, |PI-INV-arity- 1-fn| and |PI-INV-arity-1-test| and primitive type reasoning. Subgoal 3.6 (IMPLIES (AND (MEMBER (PC (CADR ACL2::X)) '(0 13 18)) (NOT (EQUAL (PC (CADR ACL2::X)) 0)) (NOT (EQUAL (PC (CADR ACL2::X)) 13)) (NOT (EQUAL (PC (CADR ACL2::X)) 18))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base|, |PI-INV-arity- 1-fn| and |PI-INV-arity-1-test| and primitive type reasoning. Subgoal 3.5 (IMPLIES (AND (MEMBER 13 '(0 13 18)) (EQUAL (PC (CADR ACL2::X)) 13) (NOT (INTP (A (CADR ACL2::X)))) (EVENP (N (CADR ACL2::X)))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base|, |PI-INV-arity- 1-fn| and |PI-INV-arity-1-test| and primitive type reasoning. Subgoal 3.4 (IMPLIES (AND (MEMBER 13 '(0 13 18)) (EQUAL (PC (CADR ACL2::X)) 13) (EVENP (N (CADR ACL2::X))) (NOT (EQUAL (INT-FIX (+ (A (CADR ACL2::X)) (* (N (CADR ACL2::X)) 1/2))) (* (CAR ACL2::X) 1/2)))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base|, |PI-INV-arity- 1-fn| and |PI-INV-arity-1-test| and primitive type reasoning. Subgoal 3.3 (IMPLIES (AND (MEMBER 13 '(0 13 18)) (EQUAL (PC (CADR ACL2::X)) 13) (< (N (CADR ACL2::X)) 0) (EVENP (N (CADR ACL2::X)))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base|, |PI-INV-arity- 1-fn| and |PI-INV-arity-1-test| and primitive type reasoning. Subgoal 3.2 (IMPLIES (AND (MEMBER 13 '(0 13 18)) (EQUAL (PC (CADR ACL2::X)) 13) (< (CAR ACL2::X) 0)) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base|, |PI-INV-arity- 1-fn| and |PI-INV-arity-1-test| and primitive type reasoning. Subgoal 3.1 (IMPLIES (AND (MEMBER 13 '(0 13 18)) (EQUAL (PC (CADR ACL2::X)) 13) (NOT (INTP (CAR ACL2::X)))) (EQUAL (|PI-INV-arity-1-fn| ACL2::X ACL2::N) NIL)). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-base|, |PI-INV-arity- 1-fn| and |PI-INV-arity-1-test| and primitive type reasoning. [Note: A hint was supplied for our processing of the goal below. Thanks!] Subgoal 2 (IMPLIES (|PI-INV-arity-1-test| (|PI-INV-arity-1-stn| ACL2::X ACL2::N)) (|PI-INV-arity-1-test| (|PI-INV-arity-1-stn| ACL2::X (|PI-INV-arity-1-fch| ACL2::X)))). We now augment the goal above by adding the hypothesis indicated by the :USE hint. The hypothesis can be obtained from |PI-INV-arity-1-fch|. The augmented goal is shown below. Subgoal 2' (IMPLIES (AND (IMPLIES (|PI-INV-arity-1-test| (|PI-INV-arity-1-stn| ACL2::X ACL2::N)) (LET ((ACL2::N (|PI-INV-arity-1-fch| ACL2::X))) (|PI-INV-arity-1-test| (|PI-INV-arity-1-stn| ACL2::X ACL2::N)))) (|PI-INV-arity-1-test| (|PI-INV-arity-1-stn| ACL2::X ACL2::N))) (|PI-INV-arity-1-test| (|PI-INV-arity-1-stn| ACL2::X (|PI-INV-arity-1-fch| ACL2::X)))). By case analysis we reduce the conjecture to Subgoal 2'' (IMPLIES (AND (IMPLIES (|PI-INV-arity-1-test| (|PI-INV-arity-1-stn| ACL2::X ACL2::N)) (|PI-INV-arity-1-test| (|PI-INV-arity-1-stn| ACL2::X (|PI-INV-arity-1-fch| ACL2::X)))) (|PI-INV-arity-1-test| (|PI-INV-arity-1-stn| ACL2::X ACL2::N))) (|PI-INV-arity-1-test| (|PI-INV-arity-1-stn| ACL2::X (|PI-INV-arity-1-fch| ACL2::X)))). But we reduce the conjecture to T, by case analysis. Subgoal 1 (EQUAL (|PI-INV-arity-1-stn| ACL2::X ACL2::N) (IF (ZP ACL2::N) ACL2::X (|PI-INV-arity-1-stn| (|PI-INV-arity-1-step| ACL2::X) (+ -1 ACL2::N)))). This simplifies, using the :definition |PI-INV- arity-1-step|, to the following two conjectures. Subgoal 1.2 (IMPLIES (ZP ACL2::N) (EQUAL (|PI-INV-arity-1-stn| ACL2::X ACL2::N) ACL2::X)). But simplification reduces this to T, using the :definition |PI-INV-arity-1-stn| and primitive type reasoning. Subgoal 1.1 (IMPLIES (NOT (ZP ACL2::N)) (EQUAL (|PI-INV-arity-1-stn| ACL2::X ACL2::N) (|PI-INV-arity-1-stn| (LIST (CAR ACL2::X) (M6STEP (CADR ACL2::X))) (+ -1 ACL2::N)))). But simplification reduces this to T, using the :definitions |PI-INV-arity-1-step| and |PI-INV- arity-1-stn| and primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM |PI-INV-arity-1-DEF| ...) Rules: ((:DEFINITION IFF) (:DEFINITION |PI-INV-arity-1|) (:DEFINITION |PI-INV-arity-1-base|) (:DEFINITION |PI-INV-arity-1-fn|) (:DEFINITION |PI-INV-arity-1-step|) (:DEFINITION |PI-INV-arity-1-stn|) (:DEFINITION |PI-INV-arity-1-test|) (:EXECUTABLE-COUNTERPART IF) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.63 seconds (prove: 0.12, print: 0.51, other: 0.00) |PI-INV-arity-1-DEF| End of Encapsulated Events. Having verified that the encapsulated events validate the signatures of the ENCAPSULATE event, we discard the ephemeral theory and extend the original theory as directed by the signatures and the non-LOCAL events. The following constraint is associated with the function |PI-INV-arity-1|: (EQUAL (|PI-INV-arity-1| ACL2::X) (IF (|PI-INV-arity-1-test| ACL2::X) (|PI-INV-arity-1-base| ACL2::X) (|PI-INV-arity-1| (|PI-INV-arity-1-step| ACL2::X)))) Summary Form: ( ENCAPSULATE ((|PI-INV-arity-1| ...) ...) ...) Rules: NIL Warnings: Disable and Theory Time: 0.85 seconds (prove: 0.13, print: 0.58, other: 0.14) T m6 >>(LOCAL (DEFUN PI-INV (N0 S) (|PI-INV-arity-1| (LIST N0 S)))) Since PI-INV is non-recursive, its admission is trivial. We could deduce no constraints on the type of PI-INV. Summary Form: ( DEFUN PI-INV ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) PI-INV m6 >>(DEFTHM PI-INV-DEF (EQUAL (PI-INV N0 S) (IF (MEMBER (PC S) '(0 13 18)) (AND (PROGRAM-IS *PROGRAM-PI* S) (CASE (PC S) (0 (AND (EQUAL (N S) N0) (INTP N0) (<= 0 N0))) (13 (AND (INTP N0) (<= 0 N0) (INTP (N S)) (IF (AND (<= 0 (N S)) (INTP (A S)) (EVENP (N S))) (EQUAL (INT-FIX (+ (A S) (/ (N S) 2))) (/ N0 2)) (NOT (EVENP (N S)))) (IFF (EVENP N0) (EVENP (N S))))) (18 (AND (EVENP N0) (EQUAL (TOPSTACK S) (/ N0 2)))))) (PI-INV N0 (M6STEP S)))) :HINTS (("Goal" :USE (:INSTANCE |PI-INV-arity-1-DEF| (ACL2::X (LIST N0 S))))) :RULE-CLASSES :DEFINITION) ACL2 Warning [Non-rec] in ( DEFTHM PI-INV-DEF ...): The :DEFINITION rule generated from PI-INV-DEF will be triggered only by terms containing the non-recursive function symbol PI-INV. Unless this function is disabled, PI-INV-DEF is unlikely ever to be used. ACL2 Warning [Subsume] in ( DEFTHM PI-INV-DEF ...): The newly proposed :DEFINITION rule PI-INV-DEF probably subsumes the previously added :REWRITE rule PI-INV, in the sense that PI-INV-DEF will now probably be applied whenever the old rule would have been. ACL2 Warning [Subsume] in ( DEFTHM PI-INV-DEF ...): The previously added rule PI-INV subsumes the newly proposed :DEFINITION rule PI-INV-DEF, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. [Note: A hint was supplied for our processing of the goal above. Thanks!] We now augment the goal above by adding the hypothesis indicated by the :USE hint. The hypothesis can be derived from |PI-INV-arity-1-DEF| via instantiation. The augmented goal is shown below. Goal' (IMPLIES (EQUAL (|PI-INV-arity-1| (LIST N0 S)) (IF (|PI-INV-arity-1-test| (LIST N0 S)) (|PI-INV-arity-1-base| (LIST N0 S)) (|PI-INV-arity-1| (|PI-INV-arity-1-step| (LIST N0 S))))) (EQUAL (PI-INV N0 S) (IF (MEMBER (PC S) '(0 13 18)) (AND (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) S) (LET ((ACL2::CASE-DO-NOT-USE-ELSEWHERE (PC S))) (CASE ACL2::CASE-DO-NOT-USE-ELSEWHERE (0 (AND (EQUAL (N S) N0) (INTP N0) (<= 0 N0))) (13 (AND (INTP N0) (<= 0 N0) (INTP (N S)) (IF (AND (<= 0 (N S)) (INTP (A S)) (EVENP (N S))) (EQUAL (INT-FIX (+ (A S) (* (N S) 1/2))) (* N0 1/2)) (NOT (EVENP (N S)))) (IFF (EVENP N0) (EVENP (N S))))) (18 (AND (EVENP N0) (EQUAL (TOPSTACK S) (* N0 1/2)))) (OTHERWISE NIL)))) (PI-INV N0 (M6STEP S))))). By the simple :definitions A, EQL, LOCAL-AT, N and PI-INV we reduce the conjecture to Goal'' (IMPLIES (EQUAL (|PI-INV-arity-1| (LIST N0 S)) (IF (|PI-INV-arity-1-test| (LIST N0 S)) (|PI-INV-arity-1-base| (LIST N0 S)) (|PI-INV-arity-1| (|PI-INV-arity-1-step| (LIST N0 S))))) (EQUAL (|PI-INV-arity-1| (LIST N0 S)) (IF (MEMBER (PC S) '(0 13 18)) (AND (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) S) (LET ((ACL2::CASE-DO-NOT-USE-ELSEWHERE (PC S))) (CASE ACL2::CASE-DO-NOT-USE-ELSEWHERE (0 (AND (EQUAL (NTH 0 (LOCALS (CURRENT-FRAME S))) N0) (INTP N0) (<= 0 N0))) (13 (AND (INTP N0) (<= 0 N0) (INTP (NTH 0 (LOCALS (CURRENT-FRAME S)))) (IF (AND (<= 0 (NTH 0 (LOCALS (CURRENT-FRAME S)))) (INTP (NTH 1 (LOCALS (CURRENT-FRAME S)))) (EVENP (NTH 0 (LOCALS (CURRENT-FRAME S))))) (EQUAL (INT-FIX (+ (NTH 1 (LOCALS (CURRENT-FRAME S))) (* (NTH 0 (LOCALS (CURRENT-FRAME S))) 1/2))) (* N0 1/2)) (NOT (EVENP (NTH 0 (LOCALS (CURRENT-FRAME S)))))) (COND ((EVENP N0) (AND (EVENP (NTH 0 (LOCALS (CURRENT-FRAME S)))) T)) ((EVENP (NTH 0 (LOCALS (CURRENT-FRAME S)))) NIL) (T T)))) (18 (AND (EVENP N0) (EQUAL (TOPSTACK S) (* N0 1/2)))) (OTHERWISE NIL)))) (|PI-INV-arity-1| (LIST N0 (M6STEP S)))))). But simplification reduces this to T, using the :compound-recognizer rule INTP-IMPLIES-INTEGERP, the :definitions A, FIX, IFF, LOCAL-AT, MEMBER, N, NOT, NTH, |PI-INV-arity-1-base|, |PI-INV-arity- 1-step|, |PI-INV-arity-1-test| and PROGRAM-IS, the :executable-counterparts of <, BINARY-*, CAR, CDR, CONSP, EQUAL, INTP, MEMBER, NOT and ZP, primitive type reasoning, the :rewrite rules ACL2::|(* (if x y z) w)|, ACL2::|(* y x)|, ACL2::|(+ w (if x y z))|, ACL2::|(+ x 0)|, ACL2::|(< (if x y z) w)|, ACL2::|(equal (if x y z) w)|, CAR-CONS, CDR-CONS and WFF-THREAD-TABLE-REGULAR-IMPLIES-WFF-THREAD- TABLE and the :type-prescription rules EVENP, INTP, UNIQUE-ID-THREAD-TABLE, WFF-CALL-FRAME-REGULAR, WFF-STATE-REGULAR and WFF-THREAD-TABLE-REGULAR. Q.E.D. Summary Form: ( DEFTHM PI-INV-DEF ...) Rules: ((:COMPOUND-RECOGNIZER INTP-IMPLIES-INTEGERP) (:DEFINITION A) (:DEFINITION EQL) (:DEFINITION FIX) (:DEFINITION IFF) (:DEFINITION LOCAL-AT) (:DEFINITION MEMBER) (:DEFINITION N) (:DEFINITION NOT) (:DEFINITION NTH) (:DEFINITION PI-INV) (:DEFINITION |PI-INV-arity-1-base|) (:DEFINITION |PI-INV-arity-1-step|) (:DEFINITION |PI-INV-arity-1-test|) (:DEFINITION PROGRAM-IS) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INTP) (:EXECUTABLE-COUNTERPART MEMBER) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE ACL2::|(* (if x y z) w)|) (:REWRITE ACL2::|(* y x)|) (:REWRITE ACL2::|(+ w (if x y z))|) (:REWRITE ACL2::|(+ x 0)|) (:REWRITE ACL2::|(< (if x y z) w)|) (:REWRITE ACL2::|(equal (if x y z) w)|) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE WFF-THREAD-TABLE-REGULAR-IMPLIES-WFF-THREAD-TABLE) (:TYPE-PRESCRIPTION EVENP) (:TYPE-PRESCRIPTION INTP) (:TYPE-PRESCRIPTION UNIQUE-ID-THREAD-TABLE) (:TYPE-PRESCRIPTION WFF-CALL-FRAME-REGULAR) (:TYPE-PRESCRIPTION WFF-STATE-REGULAR) (:TYPE-PRESCRIPTION WFF-THREAD-TABLE-REGULAR)) Warnings: Subsume and Non-rec Time: 0.69 seconds (prove: 0.54, print: 0.14, other: 0.02) PI-INV-DEF m6 >>(TABLE ACL2::ACL2-DEFAULTS-TABLE NIL '((:INCLUDE-BOOK-DIR-ALIST (:SYSTEM . "/v/filer3/v0q004/acl2/v2-9/acl2-sources/books/")) (:DEFUN-MODE . :LOGIC) (:CASE-SPLIT-LIMITATIONS 500 100) (:NU-REWRITER-MODE)) :CLEAR) Summary Form: ( TABLE ACL2::ACL2-DEFAULTS-TABLE ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2::ACL2-DEFAULTS-TABLE End of Encapsulated Events. Having verified that the encapsulated events validate the signatures of the ENCAPSULATE event, we discard the ephemeral theory and extend the original theory as directed by the signatures and the non-LOCAL events. The following constraint is associated with the function PI-INV: (EQUAL (PI-INV N0 S) (IF (MEMBER (PC S) '(0 13 18)) (AND (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) S) (LET ((ACL2::CASE-DO-NOT-USE-ELSEWHERE (PC S))) (CASE ACL2::CASE-DO-NOT-USE-ELSEWHERE (0 (AND (EQUAL (N S) N0) (INTP N0) (<= 0 N0))) (13 (AND (INTP N0) (<= 0 N0) (INTP (N S)) (IF (AND (<= 0 (N S)) (INTP (A S)) (EVENP (N S))) (EQUAL (INT-FIX (+ (A S) (* (N S) 1/2))) (* N0 1/2)) (NOT (EVENP (N S)))) (IFF (EVENP N0) (EVENP (N S))))) (18 (AND (EVENP N0) (EQUAL (TOPSTACK S) (* N0 1/2)))) (OTHERWISE NIL)))) (PI-INV N0 (M6STEP S)))) Summary Form: ( ENCAPSULATE ((PI-INV ...) ...) ...) Rules: NIL Warnings: Subsume, Non-rec, Disable and Theory Time: 1.68 seconds (prove: 0.67, print: 0.74, other: 0.27) By the :executable-counterpart of SYNP we reduce the conjecture to Goal' (IMPLIES (AND (EQUAL PC (PC S)) (NOT (MEMBER PC '(0 13 18)))) (EQUAL (PI-INV N0 S) (PI-INV N0 (M6STEP S)))). But simplification reduces this to T, using the :definitions MEMBER and PI-INV-DEF, the :executable- counterparts of CAR, CDR and CONSP and primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM PI-INV-OPENER ...) Rules: ((:DEFINITION MEMBER) (:DEFINITION NOT) (:DEFINITION PI-INV-DEF) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.58 seconds (prove: 0.57, print: 0.01, other: 0.00) This simplifies, using the :compound-recognizer rule INTP-IMPLIES-INTEGERP, the :definitions A, EQL, EXECUTE-ICONST_0, EXECUTE-ILOAD_0, FIX, FMT- TO-COMMENT-WINDOW, IFF, INST-BY-OFFSET, LOCAL-AT, MEMBER, N, NEXT-INST, NOT, NTH, PAIRLIS2, PI-INV- DEF, PROG2$ and PROGRAM-IS, the :executable-counterparts of <, BINARY-*, BINARY-+, CAR, CDR, CONS, CONSP, EQL, EQUAL, INST-BY-OFFSET1, INST-OPCODE, INST- SIZE, INTP, MEMBER, NOT, PAIRLIS2 and ZP, primitive type reasoning, the :rewrite rules ACL2::|(* (if x y z) w)|, ACL2::|(* y x)|, ACL2::|(+ w (if x y z))|, ACL2::|(+ x 0)|, ACL2::|(< (if x y z) w)|, ACL2::|(equal (if x y z) w)|, CAR-CONS, CDR-CONS, DO-INST-OPENER, PC-PUSHSTACK and WFF-THREAD-TABLE- REGULAR-IMPLIES-WFF-THREAD-TABLE and the :type- prescription rules EVENP, UNIQUE-ID-THREAD-TABLE, WFF-CALL-FRAME-REGULAR, WFF-STATE-REGULAR and WFF- THREAD-TABLE-REGULAR, to the following six conjectures. Subgoal 6 (IMPLIES (AND (EQUAL (PC S) 0) (CURRENT-THREAD-EXISTS? S) (WFF-STATE-REGULAR S) (WFF-THREAD-TABLE (THREAD-TABLE S)) (UNIQUE-ID-THREAD-TABLE (THREAD-TABLE S)) (WFF-CALL-FRAME-REGULAR (CURRENT-FRAME S)) (WFF-THREAD-TABLE-REGULAR (THREAD-TABLE S)) (EQUAL (CODE-INSTRS (METHOD-CODE (DEREF-METHOD (CURRENT-METHOD-PTR S) (INSTANCE-CLASS-TABLE S)))) '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT)))) (CONSP (LOCALS (CURRENT-FRAME S))) (EQUAL (CAR (LOCALS (CURRENT-FRAME S))) N0) (INTP N0) (<= 0 N0) (NO-FATAL-ERROR? S)) (PI-INV N0 (STATE-SET-PC 1 (PUSHSTACK 0 S)))). But simplification reduces this to T, using the :compound-recognizer rule INTP-IMPLIES-INTEGERP, the :definitions A, EXECUTE-GOTO, EXECUTE-ISTORE_- 1, FIX, FMT-TO-COMMENT-WINDOW, IFF, INST-BY-OFFSET, LOCAL-AT, N, NEXT-INST, NTH, PAIRLIS2, PI-INV-DEF, PROG2$, PROGRAM-IS and SYNP, the :executable-counterpart\ s of ARG, BINARY-+, CAR, CDR, CONS, CONSP, EQL, EQUAL, INST-BY-OFFSET1, INST-OPCODE, INST-SIZE, INTP, MEMBER, NFIX, NOT, PAIRLIS2 and ZP, primitive type reasoning, the :forward-chaining rule INT- LEMMA0, the :rewrite rules ACL2::|(* y x)|, ACL2::- |(+ 0 x)|, CAR-CONS, CDR-CONS, CURRENT-FRAME-STATE- SET, CURRENT-METHOD-PTR-POPSTACK, CURRENT-METHOD- PTR-PUSHSTACK, CURRENT-METHOD-PTR-STATE-SET-LOCAL- AT, CURRENT-METHOD-PTR-STATE-SET-PC, CURRENT-THREAD- EXISTS-PREVSERVED-BY-PUSHSTACK, CURRENT-THREAD- EXISTS-PREVSERVED-BY-SET-LOCAL, CURRENT-THREAD- EXISTS?-POPSTACK, CURRENT-THREAD-EXISTS?-STATE- SET-PC, DO-INST-OPENER, INSTANCE-CLASS-TABLE-POPSTACK, INSTANCE-CLASS-TABLE-STATE-SET-LOCAL-AT, INT-LEMMA6, INTP-HALF-N, LOCAL-AT-ACCESSOR-1, LOCAL-AT-ACCESSOR- 2, NO-FATAL-ERROR-POPSTACK, NO-FATAL-ERROR-STATE- SET-PC, NO-FATAL-ERROR?-STATE-SET, PC-STATE-SET- PC, PI-INV-OPENER, PUSHSTACK-NO-CHANGE-INSTANCE- CLASS-TABLE, JVM::STATE-ACCESSOR-SET-PC, STATE- SET-PC-STATE-SET-PC, THREAD-PRIMITIVES-STATE-SET- PC, TOPSTACK-OF-PUSHSTACK, TOPSTACK-STATE-SET-PC, UNIQUE-ID-THREAD-TABLE-POPSTACK, UNIQUE-ID-THREAD- TABLE-PUSHSTACK, UNIQUE-ID-THREAD-TABLE-STATE-SET- LOCAL, WFF-CALL-FRAME-CURRENT-FRAME-PREVSERVED- BY-POPSTACK, WFF-CALL-FRAME-CURRENT-FRAME-PREVSERVED- BY-PUSHSTACK, WFF-CALL-FRAME-CURRENT-FRAME-PREVSERVED- BY-STATE-SET-LOCAL-AT, WFF-STATE-REGULAR-POPSTACK, WFF-STATE-REGULAR-PUSHSTACK, WFF-STATE-REGULAR- STATE-SET-LOCAL, WFF-STATE-REGULAR-STATE-SET-PC, WFF-THREAD-TABLE-REGULAR-IMPLIES-WFF-THREAD-TABLE, WFF-THREAD-TABLE-REGULAR-POPSTACK, WFF-THREAD-TABLE- REGULAR-PUSHSTACK and WFF-THREAD-TABLE-REGULAR- STATE-SET-LOCAL-AT and the :type-prescription rules EVENP, NO-FATAL-ERROR?, UNIQUE-ID-THREAD-TABLE, WFF-CALL-FRAME-REGULAR, WFF-STATE-REGULAR and WFF- THREAD-TABLE-REGULAR. Subgoal 5 (IMPLIES (AND (EQUAL (PC S) 0) (CURRENT-THREAD-EXISTS? S) (WFF-STATE-REGULAR S) (WFF-THREAD-TABLE (THREAD-TABLE S)) (UNIQUE-ID-THREAD-TABLE (THREAD-TABLE S)) (WFF-CALL-FRAME-REGULAR (CURRENT-FRAME S)) (WFF-THREAD-TABLE-REGULAR (THREAD-TABLE S)) (EQUAL (CODE-INSTRS (METHOD-CODE (DEREF-METHOD (CURRENT-METHOD-PTR S) (INSTANCE-CLASS-TABLE S)))) '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT)))) (CONSP (LOCALS (CURRENT-FRAME S))) (EQUAL (CAR (LOCALS (CURRENT-FRAME S))) N0) (INTP N0) (<= 0 N0) (NOT (NO-FATAL-ERROR? S))) (PI-INV N0 S)). But simplification reduces this to T, using the :compound-recognizer rule INTP-IMPLIES-INTEGERP, the :definitions LOCAL-AT, N, NTH, PI-INV-DEF and PROGRAM-IS, the :executable-counterparts of EQL, EQUAL, MEMBER, NOT and ZP, primitive type reasoning, the :forward-chaining rule INT-LEMMA0, the :rewrite rule WFF-THREAD-TABLE-REGULAR-IMPLIES-WFF-THREAD- TABLE and the :type-prescription rules UNIQUE-ID- THREAD-TABLE, WFF-CALL-FRAME-REGULAR, WFF-STATE- REGULAR and WFF-THREAD-TABLE-REGULAR. Subgoal 4 (IMPLIES (AND (EQUAL (PC S) 13) (CURRENT-THREAD-EXISTS? S) (WFF-STATE-REGULAR S) (WFF-THREAD-TABLE (THREAD-TABLE S)) (UNIQUE-ID-THREAD-TABLE (THREAD-TABLE S)) (WFF-CALL-FRAME-REGULAR (CURRENT-FRAME S)) (WFF-THREAD-TABLE-REGULAR (THREAD-TABLE S)) (EQUAL (CODE-INSTRS (METHOD-CODE (DEREF-METHOD (CURRENT-METHOD-PTR S) (INSTANCE-CLASS-TABLE S)))) '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT)))) (INTP N0) (<= 0 N0) (CONSP (LOCALS (CURRENT-FRAME S))) (INTP (CAR (LOCALS (CURRENT-FRAME S)))) (<= 0 (CAR (LOCALS (CURRENT-FRAME S)))) (INTP (NTH 1 (LOCALS (CURRENT-FRAME S)))) (EVENP (CAR (LOCALS (CURRENT-FRAME S)))) (EQUAL (INT-FIX (+ (NTH 1 (LOCALS (CURRENT-FRAME S))) (* 1/2 (CAR (LOCALS (CURRENT-FRAME S)))))) (* 1/2 N0)) (EVENP N0) (NO-FATAL-ERROR? S)) (PI-INV N0 (STATE-SET-PC 14 (PUSHSTACK (CAR (LOCALS (CURRENT-FRAME S))) S)))). This simplifies, using the :definitions EXECUTE- IFNE, FMT-TO-COMMENT-WINDOW, INST-BY-OFFSET, NEXT- INST, PAIRLIS2, PROG2$ and SYNP, the :executable- counterparts of <, ARG, BINARY-*, BINARY-+, CAR, CDR, CONS, CONSP, EQL, EQUAL, EVENP, INST-BY-OFFSET1, INST-OPCODE, INST-SIZE, INTP, MEMBER, NOT and PAIRLIS2, primitive type reasoning, the :rewrite rules CAR- CONS, CDR-CONS, CURRENT-METHOD-PTR-PUSHSTACK, CURRENT- METHOD-PTR-STATE-SET-PC, DO-INST-OPENER, NO-FATAL- ERROR-STATE-SET-PC, NO-FATAL-ERROR?-STATE-SET, PC-STATE-SET-PC, PI-INV-OPENER, POPSTACK-PUSHSTACK- IS, PUSHSTACK-NO-CHANGE-INSTANCE-CLASS-TABLE, JVM::- STATE-ACCESSOR-SET-PC, STATE-SET-PC-STATE-SET-PC, THREAD-PRIMITIVES-STATE-SET-PC, TOPSTACK-OF-PUSHSTACK, TOPSTACK-STATE-SET-PC and WFF-THREAD-TABLE-REGULAR- IMPLIES-WFF-THREAD-TABLE and the :type-prescription rules NO-FATAL-ERROR?, UNIQUE-ID-THREAD-TABLE, WFF-CALL-FRAME-REGULAR, WFF-STATE-REGULAR and WFF- THREAD-TABLE-REGULAR, to the following two conjectures. Subgoal 4.2 (IMPLIES (AND (EQUAL (PC S) 13) (CURRENT-THREAD-EXISTS? S) (WFF-STATE-REGULAR S) (UNIQUE-ID-THREAD-TABLE (THREAD-TABLE S)) (WFF-CALL-FRAME-REGULAR (CURRENT-FRAME S)) (WFF-THREAD-TABLE-REGULAR (THREAD-TABLE S)) (EQUAL (CODE-INSTRS (METHOD-CODE (DEREF-METHOD (CURRENT-METHOD-PTR S) (INSTANCE-CLASS-TABLE S)))) '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT)))) (INTP N0) (<= 0 N0) (CONSP (LOCALS (CURRENT-FRAME S))) (INTP (NTH 1 (LOCALS (CURRENT-FRAME S)))) (EQUAL (INT-FIX (+ (NTH 1 (LOCALS (CURRENT-FRAME S))) 0)) (* 1/2 N0)) (EVENP N0) (NO-FATAL-ERROR? S) (EQUAL (CAR (LOCALS (CURRENT-FRAME S))) 0)) (PI-INV N0 (STATE-SET-PC 17 S))). By the simple :rewrite rule ACL2::|(+ x 0)| we reduce the conjecture to Subgoal 4.2' (IMPLIES (AND (EQUAL (PC S) 13) (CURRENT-THREAD-EXISTS? S) (WFF-STATE-REGULAR S) (UNIQUE-ID-THREAD-TABLE (THREAD-TABLE S)) (WFF-CALL-FRAME-REGULAR (CURRENT-FRAME S)) (WFF-THREAD-TABLE-REGULAR (THREAD-TABLE S)) (EQUAL (CODE-INSTRS (METHOD-CODE (DEREF-METHOD (CURRENT-METHOD-PTR S) (INSTANCE-CLASS-TABLE S)))) '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT)))) (INTP N0) (<= 0 N0) (CONSP (LOCALS (CURRENT-FRAME S))) (INTP (NTH 1 (LOCALS (CURRENT-FRAME S)))) (EQUAL (INT-FIX (FIX (NTH 1 (LOCALS (CURRENT-FRAME S))))) (* 1/2 N0)) (EVENP N0) (NO-FATAL-ERROR? S) (EQUAL (CAR (LOCALS (CURRENT-FRAME S))) 0)) (PI-INV N0 (STATE-SET-PC 17 S))). But simplification reduces this to T, using the :compound-recognizer rule INTP-IMPLIES-INTEGERP, the :definitions EXECUTE-ILOAD_1, FIX, FMT-TO-COMMENT- WINDOW, INST-BY-OFFSET, LOCAL-AT, NEXT-INST, PAIRLIS2, PI-INV-DEF, PROG2$, PROGRAM-IS and SYNP, the :executable- counterparts of BINARY-+, CAR, CDR, CONS, CONSP, EQL, EQUAL, INST-BY-OFFSET1, INST-OPCODE, INST- SIZE, MEMBER and PAIRLIS2, primitive type reasoning, the :forward-chaining rule INT-LEMMA0, the :rewrite rules ACL2::|(* y x)|, CAR-CONS, CDR-CONS, CURRENT- FRAME-STATE-SET, CURRENT-METHOD-PTR-PUSHSTACK, CURRENT-METHOD-PTR-STATE-SET-PC, CURRENT-THREAD- EXISTS-PREVSERVED-BY-PUSHSTACK, CURRENT-THREAD- EXISTS?-STATE-SET-PC, DO-INST-OPENER, INT-LEMMA6, LOCAL-AT-ACCESSOR-1, NO-FATAL-ERROR-STATE-SET-PC, PC-STATE-SET-PC, PI-INV-OPENER, PUSHSTACK-NO-CHANGE- INSTANCE-CLASS-TABLE, JVM::STATE-ACCESSOR-SET-PC, STATE-SET-PC-STATE-SET-PC, THREAD-PRIMITIVES-STATE- SET-PC, TOPSTACK-OF-PUSHSTACK, TOPSTACK-STATE-SET- PC, UNIQUE-ID-THREAD-TABLE-PUSHSTACK, WFF-CALL- FRAME-CURRENT-FRAME-PREVSERVED-BY-PUSHSTACK, WFF- STATE-REGULAR-PUSHSTACK, WFF-STATE-REGULAR-STATE- SET-PC, WFF-THREAD-TABLE-REGULAR-IMPLIES-WFF-THREAD- TABLE and WFF-THREAD-TABLE-REGULAR-PUSHSTACK and the :type-prescription rules EVENP, NO-FATAL-ERROR?, UNIQUE-ID-THREAD-TABLE, WFF-CALL-FRAME-REGULAR, WFF-STATE-REGULAR and WFF-THREAD-TABLE-REGULAR. Subgoal 4.1 (IMPLIES (AND (EQUAL (PC S) 13) (CURRENT-THREAD-EXISTS? S) (WFF-STATE-REGULAR S) (UNIQUE-ID-THREAD-TABLE (THREAD-TABLE S)) (WFF-CALL-FRAME-REGULAR (CURRENT-FRAME S)) (WFF-THREAD-TABLE-REGULAR (THREAD-TABLE S)) (EQUAL (CODE-INSTRS (METHOD-CODE (DEREF-METHOD (CURRENT-METHOD-PTR S) (INSTANCE-CLASS-TABLE S)))) '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT)))) (INTP N0) (<= 0 N0) (CONSP (LOCALS (CURRENT-FRAME S))) (INTP (CAR (LOCALS (CURRENT-FRAME S)))) (<= 0 (CAR (LOCALS (CURRENT-FRAME S)))) (INTP (NTH 1 (LOCALS (CURRENT-FRAME S)))) (EVENP (CAR (LOCALS (CURRENT-FRAME S)))) (EQUAL (INT-FIX (+ (NTH 1 (LOCALS (CURRENT-FRAME S))) (* 1/2 (CAR (LOCALS (CURRENT-FRAME S)))))) (* 1/2 N0)) (EVENP N0) (NO-FATAL-ERROR? S) (NOT (EQUAL (CAR (LOCALS (CURRENT-FRAME S))) 0))) (PI-INV N0 (STATE-SET-PC 5 S))). This simplifies, using the :compound-recognizer rule INTP-IMPLIES-INTEGERP, the :definitions A, EXECUTE-IADD, EXECUTE-ICONST_1, EXECUTE-ICONST_- 2, EXECUTE-ILOAD_0, EXECUTE-ILOAD_1, EXECUTE-ISTORE_- 0, EXECUTE-ISTORE_1, EXECUTE-ISUB, FIX, FMT-TO- COMMENT-WINDOW, INST-BY-OFFSET, LOCAL-AT, N, NEXT- INST, NOT, NTH, PAIRLIS2, PI-INV-DEF, PROG2$, PROGRAM- IS, SECONDSTACK and SYNP, the :executable-counterparts of BINARY-*, BINARY-+, CAR, CDR, CONS, CONSP, EQL, EQUAL, IFF, INST-BY-OFFSET1, INST-OPCODE, INST- SIZE, MEMBER, NFIX, NOT, PAIRLIS2, UNARY-- and ZP, primitive type reasoning, the :forward-chaining rule INT-LEMMA0, the :meta rule ACL2::PREFER-POSITIVE- ADDENDS-<-THM, the :rewrite rules ACL2::|(* (+ x y) z)|, ACL2::|(* y x)|, ACL2::|(+ 0 x)|, ACL2::- |(+ c (+ d x))|, ACL2::|(+ y (+ x z))|, ACL2::- |(+ y x)|, CAR-CONS, CDR-CONS, ACL2::COLLECT-PLUS- 1B, CURRENT-FRAME-STATE-SET, CURRENT-METHOD-PTR- POPSTACK, CURRENT-METHOD-PTR-PUSHSTACK, CURRENT- METHOD-PTR-STATE-SET-LOCAL-AT, CURRENT-METHOD-PTR- STATE-SET-PC, CURRENT-THREAD-EXISTS-PREVSERVED- BY-PUSHSTACK, CURRENT-THREAD-EXISTS-PREVSERVED- BY-SET-LOCAL, CURRENT-THREAD-EXISTS?-POPSTACK, CURRENT-THREAD-EXISTS?-STATE-SET-PC, DO-INST-OPENER, INSTANCE-CLASS-TABLE-POPSTACK, INSTANCE-CLASS-TABLE- STATE-SET-LOCAL-AT, INT-EVENP-INV-B, INT-LEMMA0, INT-LEMMA1, INT-LEMMA2A, INT-LEMMA2B, INT-LEMMA5A1, INTP-HALF-N, LOCAL-AT-ACCESSOR-1, LOCAL-AT-ACCESSOR- 2, NO-FATAL-ERROR-POPSTACK, NO-FATAL-ERROR-STATE- SET-PC, NO-FATAL-ERROR?-STATE-SET, PC-STATE-SET- PC, PI-INV-OPENER, POPSTACK-PUSHSTACK-IS, PUSHSTACK- NO-CHANGE-INSTANCE-CLASS-TABLE, JVM::STATE-ACCESSOR- SET-PC, STATE-SET-PC-STATE-SET-PC, THREAD-PRIMITIVES- STATE-SET-PC, TOPSTACK-OF-PUSHSTACK, TOPSTACK-STATE- SET-PC, ACL2::UN-HIDE-PLUS, UNIQUE-ID-THREAD-TABLE- POPSTACK, UNIQUE-ID-THREAD-TABLE-PUSHSTACK, UNIQUE- ID-THREAD-TABLE-STATE-SET-LOCAL, WFF-CALL-FRAME- CURRENT-FRAME-PREVSERVED-BY-POPSTACK, WFF-CALL- FRAME-CURRENT-FRAME-PREVSERVED-BY-PUSHSTACK, WFF- CALL-FRAME-CURRENT-FRAME-PREVSERVED-BY-STATE-SET- LOCAL-AT, WFF-STATE-REGULAR-POPSTACK, WFF-STATE- REGULAR-PUSHSTACK, WFF-STATE-REGULAR-STATE-SET- LOCAL, WFF-STATE-REGULAR-STATE-SET-PC, WFF-THREAD- TABLE-REGULAR-IMPLIES-WFF-THREAD-TABLE, WFF-THREAD- TABLE-REGULAR-POPSTACK, WFF-THREAD-TABLE-REGULAR- PUSHSTACK and WFF-THREAD-TABLE-REGULAR-STATE-SET- LOCAL-AT and the :type-prescription rules EVENP, NO-FATAL-ERROR?, UNIQUE-ID-THREAD-TABLE, WFF-CALL- FRAME-REGULAR, WFF-STATE-REGULAR and WFF-THREAD- TABLE-REGULAR, to Subgoal 4.1' (IMPLIES (AND (EQUAL (PC S) 13) (CURRENT-THREAD-EXISTS? S) (WFF-STATE-REGULAR S) (UNIQUE-ID-THREAD-TABLE (THREAD-TABLE S)) (WFF-CALL-FRAME-REGULAR (CURRENT-FRAME S)) (WFF-THREAD-TABLE-REGULAR (THREAD-TABLE S)) (EQUAL (CODE-INSTRS (METHOD-CODE (DEREF-METHOD (CURRENT-METHOD-PTR S) (INSTANCE-CLASS-TABLE S)))) '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT)))) (INTP N0) (<= 0 N0) (CONSP (LOCALS (CURRENT-FRAME S))) (INTP (CAR (LOCALS (CURRENT-FRAME S)))) (<= 0 (CAR (LOCALS (CURRENT-FRAME S)))) (INTP (NTH 1 (LOCALS (CURRENT-FRAME S)))) (EVENP (CAR (LOCALS (CURRENT-FRAME S)))) (EQUAL (INT-FIX (+ (NTH 1 (LOCALS (CURRENT-FRAME S))) (* 1/2 (CAR (LOCALS (CURRENT-FRAME S)))))) (* 1/2 N0)) (EVENP N0) (NO-FATAL-ERROR? S) (NOT (EQUAL (CAR (LOCALS (CURRENT-FRAME S))) 0))) (<= 2 (CAR (LOCALS (CURRENT-FRAME S))))). But simplification reduces this to T, using the :compound-recognizer rule INTP-IMPLIES-INTEGERP, the :executable-counterparts of <, BINARY-*, EQUAL, EVENP, INTP and NOT and linear arithmetic. Subgoal 3 (IMPLIES (AND (EQUAL (PC S) 13) (CURRENT-THREAD-EXISTS? S) (WFF-STATE-REGULAR S) (WFF-THREAD-TABLE (THREAD-TABLE S)) (UNIQUE-ID-THREAD-TABLE (THREAD-TABLE S)) (WFF-CALL-FRAME-REGULAR (CURRENT-FRAME S)) (WFF-THREAD-TABLE-REGULAR (THREAD-TABLE S)) (EQUAL (CODE-INSTRS (METHOD-CODE (DEREF-METHOD (CURRENT-METHOD-PTR S) (INSTANCE-CLASS-TABLE S)))) '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT)))) (INTP N0) (<= 0 N0) (CONSP (LOCALS (CURRENT-FRAME S))) (INTP (CAR (LOCALS (CURRENT-FRAME S)))) (<= 0 (CAR (LOCALS (CURRENT-FRAME S)))) (INTP (NTH 1 (LOCALS (CURRENT-FRAME S)))) (EVENP (CAR (LOCALS (CURRENT-FRAME S)))) (EQUAL (INT-FIX (+ (NTH 1 (LOCALS (CURRENT-FRAME S))) (* 1/2 (CAR (LOCALS (CURRENT-FRAME S)))))) (* 1/2 N0)) (EVENP N0) (NOT (NO-FATAL-ERROR? S))) (PI-INV N0 S)). But simplification reduces this to T, using the :compound-recognizer rule INTP-IMPLIES-INTEGERP, the :definitions A, LOCAL-AT, N, NTH, PI-INV-DEF and PROGRAM-IS, the :executable-counterparts of EQL, EQUAL, IFF, MEMBER, NOT and ZP, primitive type reasoning, the :forward-chaining rule INT- LEMMA0, the :rewrite rules ACL2::|(* y x)| and WFF-THREAD-TABLE-REGULAR-IMPLIES-WFF-THREAD-TABLE and the :type-prescription rules EVENP, UNIQUE- ID-THREAD-TABLE, WFF-CALL-FRAME-REGULAR, WFF-STATE- REGULAR and WFF-THREAD-TABLE-REGULAR. Subgoal 2 (IMPLIES (AND (EQUAL (PC S) 13) (CURRENT-THREAD-EXISTS? S) (WFF-STATE-REGULAR S) (WFF-THREAD-TABLE (THREAD-TABLE S)) (UNIQUE-ID-THREAD-TABLE (THREAD-TABLE S)) (WFF-CALL-FRAME-REGULAR (CURRENT-FRAME S)) (WFF-THREAD-TABLE-REGULAR (THREAD-TABLE S)) (EQUAL (CODE-INSTRS (METHOD-CODE (DEREF-METHOD (CURRENT-METHOD-PTR S) (INSTANCE-CLASS-TABLE S)))) '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT)))) (INTP N0) (<= 0 N0) (CONSP (LOCALS (CURRENT-FRAME S))) (INTP (CAR (LOCALS (CURRENT-FRAME S)))) (NOT (EVENP (CAR (LOCALS (CURRENT-FRAME S))))) (NOT (EVENP N0)) (NO-FATAL-ERROR? S)) (PI-INV N0 (STATE-SET-PC 14 (PUSHSTACK (CAR (LOCALS (CURRENT-FRAME S))) S)))). This simplifies, using the :definitions EXECUTE- IFNE, FMT-TO-COMMENT-WINDOW, INST-BY-OFFSET, NEXT- INST, PAIRLIS2, PROG2$ and SYNP, the :executable- counterparts of ARG, BINARY-+, CAR, CDR, CONS, CONSP, EQL, EQUAL, EVENP, INST-BY-OFFSET1, INST- OPCODE, INST-SIZE, INTP, MEMBER, NOT and PAIRLIS2, primitive type reasoning, the :rewrite rules CAR- CONS, CDR-CONS, CURRENT-METHOD-PTR-PUSHSTACK, CURRENT- METHOD-PTR-STATE-SET-PC, DO-INST-OPENER, NO-FATAL- ERROR-STATE-SET-PC, NO-FATAL-ERROR?-STATE-SET, PC-STATE-SET-PC, PI-INV-OPENER, POPSTACK-PUSHSTACK- IS, PUSHSTACK-NO-CHANGE-INSTANCE-CLASS-TABLE, JVM::- STATE-ACCESSOR-SET-PC, STATE-SET-PC-STATE-SET-PC, THREAD-PRIMITIVES-STATE-SET-PC, TOPSTACK-OF-PUSHSTACK, TOPSTACK-STATE-SET-PC and WFF-THREAD-TABLE-REGULAR- IMPLIES-WFF-THREAD-TABLE and the :type-prescription rules NO-FATAL-ERROR?, UNIQUE-ID-THREAD-TABLE, WFF-CALL-FRAME-REGULAR, WFF-STATE-REGULAR and WFF- THREAD-TABLE-REGULAR, to Subgoal 2' (IMPLIES (AND (EQUAL (PC S) 13) (CURRENT-THREAD-EXISTS? S) (WFF-STATE-REGULAR S) (UNIQUE-ID-THREAD-TABLE (THREAD-TABLE S)) (WFF-CALL-FRAME-REGULAR (CURRENT-FRAME S)) (WFF-THREAD-TABLE-REGULAR (THREAD-TABLE S)) (EQUAL (CODE-INSTRS (METHOD-CODE (DEREF-METHOD (CURRENT-METHOD-PTR S) (INSTANCE-CLASS-TABLE S)))) '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT)))) (INTP N0) (<= 0 N0) (CONSP (LOCALS (CURRENT-FRAME S))) (INTP (CAR (LOCALS (CURRENT-FRAME S)))) (NOT (EVENP (CAR (LOCALS (CURRENT-FRAME S))))) (NOT (EVENP N0)) (NO-FATAL-ERROR? S) (NOT (EQUAL (CAR (LOCALS (CURRENT-FRAME S))) 0))) (PI-INV N0 (STATE-SET-PC 5 S))). But simplification reduces this to T, using the :compound-recognizer rule INTP-IMPLIES-INTEGERP, the :definitions A, EXECUTE-IADD, EXECUTE-ICONST_- 1, EXECUTE-ICONST_2, EXECUTE-ILOAD_0, EXECUTE-ILOAD_- 1, EXECUTE-ISTORE_0, EXECUTE-ISTORE_1, EXECUTE- ISUB, FMT-TO-COMMENT-WINDOW, INST-BY-OFFSET, LOCAL- AT, N, NEXT-INST, NOT, NTH, PAIRLIS2, PI-INV-DEF, PROG2$, PROGRAM-IS, SECONDSTACK and SYNP, the :executabl\ e-counterparts of BINARY-+, CAR, CDR, CONS, CONSP, EQL, EQUAL, IFF, INST-BY-OFFSET1, INST-OPCODE, INST-SIZE, MEMBER, NFIX, NOT, PAIRLIS2, UNARY-- and ZP, primitive type reasoning, the :forward- chaining rule INT-LEMMA0, the :rewrite rules ACL2::- |(+ y x)|, CAR-CONS, CDR-CONS, CURRENT-FRAME-STATE- SET, CURRENT-METHOD-PTR-POPSTACK, CURRENT-METHOD- PTR-PUSHSTACK, CURRENT-METHOD-PTR-STATE-SET-LOCAL- AT, CURRENT-METHOD-PTR-STATE-SET-PC, CURRENT-THREAD- EXISTS-PREVSERVED-BY-PUSHSTACK, CURRENT-THREAD- EXISTS-PREVSERVED-BY-SET-LOCAL, CURRENT-THREAD- EXISTS?-POPSTACK, CURRENT-THREAD-EXISTS?-STATE- SET-PC, DO-INST-OPENER, INSTANCE-CLASS-TABLE-POPSTACK, INSTANCE-CLASS-TABLE-STATE-SET-LOCAL-AT, INT-EVENP- INV-A, INT-LEMMA1, LOCAL-AT-ACCESSOR-1, LOCAL-AT- ACCESSOR-2, NO-FATAL-ERROR-POPSTACK, NO-FATAL-ERROR- STATE-SET-PC, NO-FATAL-ERROR?-STATE-SET, PC-STATE- SET-PC, PI-INV-OPENER, POPSTACK-PUSHSTACK-IS, PUSHSTACK- NO-CHANGE-INSTANCE-CLASS-TABLE, JVM::STATE-ACCESSOR- SET-PC, STATE-SET-PC-STATE-SET-PC, THREAD-PRIMITIVES- STATE-SET-PC, TOPSTACK-OF-PUSHSTACK, TOPSTACK-STATE- SET-PC, UNIQUE-ID-THREAD-TABLE-POPSTACK, UNIQUE- ID-THREAD-TABLE-PUSHSTACK, UNIQUE-ID-THREAD-TABLE- STATE-SET-LOCAL, WFF-CALL-FRAME-CURRENT-FRAME-PREVSERVED\ -BY-POPSTACK, WFF-CALL-FRAME-CURRENT-FRAME-PREVSERVED- BY-PUSHSTACK, WFF-CALL-FRAME-CURRENT-FRAME-PREVSERVED- BY-STATE-SET-LOCAL-AT, WFF-STATE-REGULAR-POPSTACK, WFF-STATE-REGULAR-PUSHSTACK, WFF-STATE-REGULAR- STATE-SET-LOCAL, WFF-STATE-REGULAR-STATE-SET-PC, WFF-THREAD-TABLE-REGULAR-IMPLIES-WFF-THREAD-TABLE, WFF-THREAD-TABLE-REGULAR-POPSTACK, WFF-THREAD-TABLE- REGULAR-PUSHSTACK and WFF-THREAD-TABLE-REGULAR- STATE-SET-LOCAL-AT and the :type-prescription rules NO-FATAL-ERROR?, UNIQUE-ID-THREAD-TABLE, WFF-CALL- FRAME-REGULAR, WFF-STATE-REGULAR and WFF-THREAD- TABLE-REGULAR. Subgoal 1 (IMPLIES (AND (EQUAL (PC S) 13) (CURRENT-THREAD-EXISTS? S) (WFF-STATE-REGULAR S) (WFF-THREAD-TABLE (THREAD-TABLE S)) (UNIQUE-ID-THREAD-TABLE (THREAD-TABLE S)) (WFF-CALL-FRAME-REGULAR (CURRENT-FRAME S)) (WFF-THREAD-TABLE-REGULAR (THREAD-TABLE S)) (EQUAL (CODE-INSTRS (METHOD-CODE (DEREF-METHOD (CURRENT-METHOD-PTR S) (INSTANCE-CLASS-TABLE S)))) '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT)))) (INTP N0) (<= 0 N0) (CONSP (LOCALS (CURRENT-FRAME S))) (INTP (CAR (LOCALS (CURRENT-FRAME S)))) (NOT (EVENP (CAR (LOCALS (CURRENT-FRAME S))))) (NOT (EVENP N0)) (NOT (NO-FATAL-ERROR? S))) (PI-INV N0 S)). But simplification reduces this to T, using the :compound-recognizer rule INTP-IMPLIES-INTEGERP, the :definitions A, LOCAL-AT, N, NOT, NTH, PI-INV- DEF and PROGRAM-IS, the :executable-counterparts of EQL, EQUAL, IFF, MEMBER, NOT and ZP, the :forward- chaining rule INT-LEMMA0, the :rewrite rule WFF- THREAD-TABLE-REGULAR-IMPLIES-WFF-THREAD-TABLE and the :type-prescription rules UNIQUE-ID-THREAD-TABLE, WFF-CALL-FRAME-REGULAR, WFF-STATE-REGULAR and WFF- THREAD-TABLE-REGULAR. Q.E.D. Summary Form: ( DEFTHM PI-INV-STEP ...) Rules: ((:COMPOUND-RECOGNIZER INTP-IMPLIES-INTEGERP) (:DEFINITION A) (:DEFINITION EQL) (:DEFINITION EXECUTE-GOTO) (:DEFINITION EXECUTE-IADD) (:DEFINITION EXECUTE-ICONST_0) (:DEFINITION EXECUTE-ICONST_1) (:DEFINITION EXECUTE-ICONST_2) (:DEFINITION EXECUTE-IFNE) (:DEFINITION EXECUTE-ILOAD_0) (:DEFINITION EXECUTE-ILOAD_1) (:DEFINITION EXECUTE-ISTORE_0) (:DEFINITION EXECUTE-ISTORE_1) (:DEFINITION EXECUTE-ISUB) (:DEFINITION FIX) (:DEFINITION FMT-TO-COMMENT-WINDOW) (:DEFINITION IFF) (:DEFINITION INST-BY-OFFSET) (:DEFINITION LOCAL-AT) (:DEFINITION MEMBER) (:DEFINITION N) (:DEFINITION NEXT-INST) (:DEFINITION NOT) (:DEFINITION NTH) (:DEFINITION PAIRLIS2) (:DEFINITION PI-INV-DEF) (:DEFINITION PROG2$) (:DEFINITION PROGRAM-IS) (:DEFINITION SECONDSTACK) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART ARG) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQL) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART EVENP) (:EXECUTABLE-COUNTERPART IFF) (:EXECUTABLE-COUNTERPART INST-BY-OFFSET1) (:EXECUTABLE-COUNTERPART INST-OPCODE) (:EXECUTABLE-COUNTERPART INST-SIZE) (:EXECUTABLE-COUNTERPART INTP) (:EXECUTABLE-COUNTERPART MEMBER) (:EXECUTABLE-COUNTERPART NFIX) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART PAIRLIS2) (:EXECUTABLE-COUNTERPART UNARY--) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:META ACL2::PREFER-POSITIVE-ADDENDS-<-THM) (:REWRITE ACL2::|(* (+ x y) z)|) (:REWRITE ACL2::|(* (if x y z) w)|) (:REWRITE ACL2::|(* y x)|) (:REWRITE ACL2::|(+ 0 x)|) (:REWRITE ACL2::|(+ c (+ d x))|) (:REWRITE ACL2::|(+ w (if x y z))|) (:REWRITE ACL2::|(+ x 0)|) (:REWRITE ACL2::|(+ y (+ x z))|) (:REWRITE ACL2::|(+ y x)|) (:REWRITE ACL2::|(< (if x y z) w)|) (:REWRITE ACL2::|(equal (if x y z) w)|) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE ACL2::COLLECT-PLUS-1B) (:REWRITE CURRENT-FRAME-STATE-SET) (:REWRITE CURRENT-METHOD-PTR-POPSTACK) (:REWRITE CURRENT-METHOD-PTR-PUSHSTACK) (:REWRITE CURRENT-METHOD-PTR-STATE-SET-LOCAL-AT) (:REWRITE CURRENT-METHOD-PTR-STATE-SET-PC) (:REWRITE CURRENT-THREAD-EXISTS-PREVSERVED-BY-PUSHSTACK) (:REWRITE CURRENT-THREAD-EXISTS-PREVSERVED-BY-SET-LOCAL) (:REWRITE CURRENT-THREAD-EXISTS?-POPSTACK) (:REWRITE CURRENT-THREAD-EXISTS?-STATE-SET-PC) (:REWRITE DO-INST-OPENER) (:REWRITE INSTANCE-CLASS-TABLE-POPSTACK) (:REWRITE INSTANCE-CLASS-TABLE-STATE-SET-LOCAL-AT) (:REWRITE INT-EVENP-INV-A) (:REWRITE INT-EVENP-INV-B) (:REWRITE INT-LEMMA0) (:REWRITE INT-LEMMA1) (:REWRITE INT-LEMMA2A) (:REWRITE INT-LEMMA2B) (:REWRITE INT-LEMMA5A1) (:REWRITE INT-LEMMA6) (:REWRITE INTP-HALF-N) (:REWRITE LOCAL-AT-ACCESSOR-1) (:REWRITE LOCAL-AT-ACCESSOR-2) (:REWRITE NO-FATAL-ERROR-POPSTACK) (:REWRITE NO-FATAL-ERROR-STATE-SET-PC) (:REWRITE NO-FATAL-ERROR?-STATE-SET) (:REWRITE PC-PUSHSTACK) (:REWRITE PC-STATE-SET-PC) (:REWRITE PI-INV-OPENER) (:REWRITE POPSTACK-PUSHSTACK-IS) (:REWRITE PUSHSTACK-NO-CHANGE-INSTANCE-CLASS-TABLE) (:REWRITE JVM::STATE-ACCESSOR-SET-PC) (:REWRITE STATE-SET-PC-STATE-SET-PC) (:REWRITE THREAD-PRIMITIVES-STATE-SET-PC) (:REWRITE TOPSTACK-OF-PUSHSTACK) (:REWRITE TOPSTACK-STATE-SET-PC) (:REWRITE ACL2::UN-HIDE-PLUS) (:REWRITE UNIQUE-ID-THREAD-TABLE-POPSTACK) (:REWRITE UNIQUE-ID-THREAD-TABLE-PUSHSTACK) (:REWRITE UNIQUE-ID-THREAD-TABLE-STATE-SET-LOCAL) (:REWRITE WFF-CALL-FRAME-CURRENT-FRAME-PREVSERVED-BY-POPSTACK) (:REWRITE WFF-CALL-FRAME-CURRENT-FRAME-PREVSERVED-BY-PUSHSTACK) (:REWRITE WFF-CALL-FRAME-CURRENT-FRAME-PREVSERVED-BY-STATE-SET-LOCAL-AT) (:REWRITE WFF-STATE-REGULAR-POPSTACK) (:REWRITE WFF-STATE-REGULAR-PUSHSTACK) (:REWRITE WFF-STATE-REGULAR-STATE-SET-LOCAL) (:REWRITE WFF-STATE-REGULAR-STATE-SET-PC) (:REWRITE WFF-THREAD-TABLE-REGULAR-IMPLIES-WFF-THREAD-TABLE) (:REWRITE WFF-THREAD-TABLE-REGULAR-POPSTACK) (:REWRITE WFF-THREAD-TABLE-REGULAR-PUSHSTACK) (:REWRITE WFF-THREAD-TABLE-REGULAR-STATE-SET-LOCAL-AT) (:TYPE-PRESCRIPTION EVENP) (:TYPE-PRESCRIPTION NO-FATAL-ERROR?) (:TYPE-PRESCRIPTION UNIQUE-ID-THREAD-TABLE) (:TYPE-PRESCRIPTION WFF-CALL-FRAME-REGULAR) (:TYPE-PRESCRIPTION WFF-STATE-REGULAR) (:TYPE-PRESCRIPTION WFF-THREAD-TABLE-REGULAR)) Warnings: None Time: 2.89 seconds (prove: 2.46, print: 0.43, other: 0.00) [Note: A hint was supplied for our processing of the goal above. Thanks!] Name the formula above *1. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (SIMPLE-RUN S K). This suggestion was produced using the :induction rule SIMPLE-RUN. If we let (:P K N0 S) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ZP K)) (:P (+ -1 K) N0 (M6STEP S))) (:P K N0 S)) (IMPLIES (ZP K) (:P K N0 S))). This induction is justified by the same argument used to admit SIMPLE-RUN, namely, the measure (ACL2-COUNT K) is decreasing according to the relation O< (which is known to be well-founded on the domain recognized by O-P). Note, however, that the unmeasured variable S is being instantiated. When applied to the goal at hand the above induction scheme produces the following three nontautological subgoals. Subgoal *1/3 (IMPLIES (AND (NOT (ZP K)) (PI-INV N0 (SIMPLE-RUN (M6STEP S) (+ -1 K))) (PI-INV N0 S)) (PI-INV N0 (SIMPLE-RUN S K))). By the simple :definition ZP we reduce the conjecture to Subgoal *1/3' (IMPLIES (AND (INTEGERP K) (< 0 K) (PI-INV N0 (SIMPLE-RUN (M6STEP S) (+ -1 K))) (PI-INV N0 S)) (PI-INV N0 (SIMPLE-RUN S K))). But simplification reduces this to T, using the :compound-recognizer rule ACL2::ZP-COMPOUND-RECOGNIZER and the :definition SIMPLE-RUN. Subgoal *1/2 (IMPLIES (AND (NOT (ZP K)) (NOT (PI-INV N0 (M6STEP S))) (PI-INV N0 S)) (PI-INV N0 (SIMPLE-RUN S K))). By the simple :definition ZP we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (INTEGERP K) (< 0 K) (NOT (PI-INV N0 (M6STEP S))) (PI-INV N0 S)) (PI-INV N0 (SIMPLE-RUN S K))). But simplification reduces this to T, using the :rewrite rule PI-INV-STEP. Subgoal *1/1 (IMPLIES (AND (ZP K) (PI-INV N0 S)) (PI-INV N0 (SIMPLE-RUN S K))). But simplification reduces this to T, using the :compound-recognizer rule ACL2::ZP-COMPOUND-RECOGNIZER and the :definitions SIMPLE-RUN and ZP. That completes the proof of *1. Q.E.D. Summary Form: ( DEFTHM PI-INV-RUN ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION NOT) (:DEFINITION SIMPLE-RUN) (:DEFINITION ZP) (:INDUCTION SIMPLE-RUN) (:REWRITE PI-INV-STEP)) Warnings: None Time: 0.14 seconds (prove: 0.06, print: 0.03, other: 0.05) [Note: A hint was supplied for our processing of the goal above. Thanks!] We now augment the goal above by adding the hypothesis indicated by the :USE hint. The hypothesis can be derived from PI-INV-RUN via instantiation. The augmented goal is shown below. Goal' (IMPLIES (IMPLIES (PI-INV N0 S0) (PI-INV N0 (SIMPLE-RUN S0 K))) (LET ((SK (SIMPLE-RUN S0 K))) (IMPLIES (AND (LET ((S S0)) (AND (EQUAL (N S) N0) (INTP N0) (<= 0 N0))) (EQUAL (PC S0) 0) (EQUAL (LOCALS (CURRENT-FRAME S0)) (CONS N0 ANY)) (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) S0) (EQUAL (PC SK) 18)) (LET ((S SK)) (AND (EVENP N0) (EQUAL (TOPSTACK S) (* N0 1/2))))))). By the simple :definitions LOCAL-AT, N and PROGRAM- IS we reduce the conjecture to Goal'' (IMPLIES (AND (IMPLIES (PI-INV N0 S0) (PI-INV N0 (SIMPLE-RUN S0 K))) (EQUAL (NTH 0 (LOCALS (CURRENT-FRAME S0))) N0) (INTP N0) (<= 0 N0) (EQUAL (PC S0) 0) (EQUAL (LOCALS (CURRENT-FRAME S0)) (CONS N0 ANY)) (CURRENT-THREAD-EXISTS? S0) (WFF-STATE-REGULAR S0) (WFF-THREAD-TABLE (THREAD-TABLE S0)) (UNIQUE-ID-THREAD-TABLE (THREAD-TABLE S0)) (WFF-CALL-FRAME-REGULAR (CURRENT-FRAME S0)) (WFF-THREAD-TABLE-REGULAR (THREAD-TABLE S0)) (EQUAL (CODE-INSTRS (METHOD-CODE (DEREF-METHOD (CURRENT-METHOD-PTR S0) (INSTANCE-CLASS-TABLE S0)))) '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT)))) (EQUAL (PC (SIMPLE-RUN S0 K)) 18)) (LET ((S (SIMPLE-RUN S0 K))) (AND (EVENP N0) (EQUAL (TOPSTACK S) (* N0 1/2))))). But simplification reduces this to T, using the :definitions LOCAL-AT, N, NOT, NTH, PI-INV-DEF and PROGRAM-IS, the :executable-counterparts of EQL, EQUAL, MEMBER and ZP, primitive type reasoning, the :rewrite rules ACL2::|(* y x)| and WFF-THREAD- TABLE-REGULAR-IMPLIES-WFF-THREAD-TABLE and the :type-prescription rules EVENP, UNIQUE-ID-THREAD- TABLE, WFF-CALL-FRAME-REGULAR, WFF-STATE-REGULAR and WFF-THREAD-TABLE-REGULAR. Q.E.D. Summary Form: ( DEFTHM PARTIAL-CORRECTNESS-OF-PROGRAM- PI ...) Rules: ((:DEFINITION LOCAL-AT) (:DEFINITION N) (:DEFINITION NOT) (:DEFINITION NTH) (:DEFINITION PI-INV-DEF) (:DEFINITION PROGRAM-IS) (:EXECUTABLE-COUNTERPART EQL) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART MEMBER) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE ACL2::|(* y x)|) (:REWRITE WFF-THREAD-TABLE-REGULAR-IMPLIES-WFF-THREAD-TABLE) (:TYPE-PRESCRIPTION EVENP) (:TYPE-PRESCRIPTION UNIQUE-ID-THREAD-TABLE) (:TYPE-PRESCRIPTION WFF-CALL-FRAME-REGULAR) (:TYPE-PRESCRIPTION WFF-STATE-REGULAR) (:TYPE-PRESCRIPTION WFF-THREAD-TABLE-REGULAR)) Warnings: None Time: 0.12 seconds (prove: 0.08, print: 0.03, other: 0.00) PARTIAL-CORRECTNESS-OF-PROGRAM-PI m6 >(defthm correctness-restated (implies (and (intp (n s0)) (<= 0 (n s0)) (equal (pc s0) 0) (program-is *program-pi* s0) (equal sk (simple-run s0 k)) (equal (pc sk) 18)) (and (evenp (n s0)) (equal (topstack sk) (/ (n s0) 2)))) :rule-classes nil :hints (("Goal" :use (:instance PARTIAL-CORRECTNESS-OF-PROGRAM-PI (n0 (n s0)) (any (cdr (locals (current-frame s0)))))))) [Note: A hint was supplied for our processing of the goal above. Thanks!] We now augment the goal above by adding the hypothesis indicated by the :USE hint. The hypothesis can be derived from PARTIAL-CORRECTNESS-OF-PROGRAM- PI via instantiation. The augmented goal is shown below. Goal' (IMPLIES (LET ((SK (SIMPLE-RUN S0 K)) (ANY (CDR (LOCALS (CURRENT-FRAME S0)))) (N0 (N S0))) (IMPLIES (AND (LET ((S S0)) (AND (EQUAL (N S) N0) (INTP N0) (<= 0 N0))) (EQUAL (PC S0) 0) (EQUAL (LOCALS (CURRENT-FRAME S0)) (CONS N0 ANY)) (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) S0) (EQUAL (PC SK) 18)) (LET ((S SK)) (AND (EVENP N0) (EQUAL (TOPSTACK S) (* N0 1/2)))))) (IMPLIES (AND (INTP (N S0)) (<= 0 (N S0)) (EQUAL (PC S0) 0) (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) S0) (EQUAL SK (SIMPLE-RUN S0 K)) (EQUAL (PC SK) 18)) (AND (EVENP (N S0)) (EQUAL (TOPSTACK SK) (* (N S0) 1/2))))). By the simple :definitions LOCAL-AT, N and PROGRAM- IS we reduce the conjecture to Goal'' (IMPLIES (AND (LET ((SK (SIMPLE-RUN S0 K)) (ANY (CDR (LOCALS (CURRENT-FRAME S0)))) (N0 (NTH 0 (LOCALS (CURRENT-FRAME S0))))) (IMPLIES (AND (LET ((S S0)) (AND (EQUAL (NTH 0 (LOCALS (CURRENT-FRAME S))) N0) (INTP N0) (<= 0 N0))) (EQUAL (PC S0) 0) (EQUAL (LOCALS (CURRENT-FRAME S0)) (CONS N0 ANY)) (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) S0) (EQUAL (PC SK) 18)) (LET ((S SK)) (AND (EVENP N0) (EQUAL (TOPSTACK S) (* N0 1/2)))))) (INTP (NTH 0 (LOCALS (CURRENT-FRAME S0)))) (<= 0 (NTH 0 (LOCALS (CURRENT-FRAME S0)))) (EQUAL (PC S0) 0) (CURRENT-THREAD-EXISTS? S0) (WFF-STATE-REGULAR S0) (WFF-THREAD-TABLE (THREAD-TABLE S0)) (UNIQUE-ID-THREAD-TABLE (THREAD-TABLE S0)) (WFF-CALL-FRAME-REGULAR (CURRENT-FRAME S0)) (WFF-THREAD-TABLE-REGULAR (THREAD-TABLE S0)) (EQUAL (CODE-INSTRS (METHOD-CODE (DEREF-METHOD (CURRENT-METHOD-PTR S0) (INSTANCE-CLASS-TABLE S0)))) '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT)))) (EQUAL SK (SIMPLE-RUN S0 K)) (EQUAL (PC SK) 18)) (AND (EVENP (NTH 0 (LOCALS (CURRENT-FRAME S0)))) (EQUAL (TOPSTACK SK) (* (NTH 0 (LOCALS (CURRENT-FRAME S0))) 1/2)))). This simplifies, using the :definition NTH, the :executable-counterparts of INTP and ZP, the :rewrite rules ACL2::|(* y x)| and WFF-THREAD-TABLE-REGULAR- IMPLIES-WFF-THREAD-TABLE and the :type-prescription rule WFF-THREAD-TABLE-REGULAR, to the following two conjectures. Subgoal 2 (IMPLIES (AND (CONSP (LOCALS (CURRENT-FRAME S0))) (LET ((SK (SIMPLE-RUN S0 K)) (ANY (CDR (LOCALS (CURRENT-FRAME S0)))) (N0 (CAR (LOCALS (CURRENT-FRAME S0))))) (IMPLIES (AND (LET ((S S0)) (AND (EQUAL (NTH 0 (LOCALS (CURRENT-FRAME S))) N0) (INTP N0) (<= 0 N0))) (EQUAL (PC S0) 0) (EQUAL (LOCALS (CURRENT-FRAME S0)) (CONS N0 ANY)) (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) S0) (EQUAL (PC SK) 18)) (LET ((S SK)) (AND (EVENP N0) (EQUAL (TOPSTACK S) (* N0 1/2)))))) (INTP (CAR (LOCALS (CURRENT-FRAME S0)))) (<= 0 (CAR (LOCALS (CURRENT-FRAME S0)))) (EQUAL (PC S0) 0) (CURRENT-THREAD-EXISTS? S0) (WFF-STATE-REGULAR S0) (UNIQUE-ID-THREAD-TABLE (THREAD-TABLE S0)) (WFF-CALL-FRAME-REGULAR (CURRENT-FRAME S0)) (WFF-THREAD-TABLE-REGULAR (THREAD-TABLE S0)) (EQUAL (CODE-INSTRS (METHOD-CODE (DEREF-METHOD (CURRENT-METHOD-PTR S0) (INSTANCE-CLASS-TABLE S0)))) '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT)))) (EQUAL (PC (SIMPLE-RUN S0 K)) 18)) (EVENP (CAR (LOCALS (CURRENT-FRAME S0))))). But simplification reduces this to T, using the :compound-recognizer rule INTP-IMPLIES-INTEGERP, the :definitions NTH and PROGRAM-IS, the :executable- counterparts of EQUAL, NOT and ZP, primitive type reasoning, the :forward-chaining rule INT-LEMMA0, the :rewrite rules CAR-CDR-ELIM and WFF-THREAD- TABLE-REGULAR-IMPLIES-WFF-THREAD-TABLE and the :type-prescription rules UNIQUE-ID-THREAD-TABLE, WFF-CALL-FRAME-REGULAR, WFF-STATE-REGULAR and WFF- THREAD-TABLE-REGULAR. Subgoal 1 (IMPLIES (AND (CONSP (LOCALS (CURRENT-FRAME S0))) (LET ((SK (SIMPLE-RUN S0 K)) (ANY (CDR (LOCALS (CURRENT-FRAME S0)))) (N0 (CAR (LOCALS (CURRENT-FRAME S0))))) (IMPLIES (AND (LET ((S S0)) (AND (EQUAL (NTH 0 (LOCALS (CURRENT-FRAME S))) N0) (INTP N0) (<= 0 N0))) (EQUAL (PC S0) 0) (EQUAL (LOCALS (CURRENT-FRAME S0)) (CONS N0 ANY)) (PROGRAM-IS '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT))) S0) (EQUAL (PC SK) 18)) (LET ((S SK)) (AND (EVENP N0) (EQUAL (TOPSTACK S) (* N0 1/2)))))) (INTP (CAR (LOCALS (CURRENT-FRAME S0)))) (<= 0 (CAR (LOCALS (CURRENT-FRAME S0)))) (EQUAL (PC S0) 0) (CURRENT-THREAD-EXISTS? S0) (WFF-STATE-REGULAR S0) (UNIQUE-ID-THREAD-TABLE (THREAD-TABLE S0)) (WFF-CALL-FRAME-REGULAR (CURRENT-FRAME S0)) (WFF-THREAD-TABLE-REGULAR (THREAD-TABLE S0)) (EQUAL (CODE-INSTRS (METHOD-CODE (DEREF-METHOD (CURRENT-METHOD-PTR S0) (INSTANCE-CLASS-TABLE S0)))) '((0 (ICONST_0)) (1 (ISTORE_1)) (2 (GOTO 13)) (5 (ILOAD_1)) (6 (ICONST_1)) (7 (IADD)) (8 (ISTORE_1)) (9 (ILOAD_0)) (10 (ICONST_2)) (11 (ISUB)) (12 (ISTORE_0)) (13 (ILOAD_0)) (14 (IFNE 5)) (17 (ILOAD_1)) (18 (HALT)))) (EQUAL (PC (SIMPLE-RUN S0 K)) 18)) (EQUAL (TOPSTACK (SIMPLE-RUN S0 K)) (* 1/2 (CAR (LOCALS (CURRENT-FRAME S0)))))). But simplification reduces this to T, using the :compound-recognizer rule INTP-IMPLIES-INTEGERP, the :definitions NTH and PROGRAM-IS, the :executable- counterparts of EQUAL, NOT and ZP, primitive type reasoning, the :forward-chaining rule INT-LEMMA0, the :rewrite rules ACL2::|(* y x)|, CAR-CDR-ELIM and WFF-THREAD-TABLE-REGULAR-IMPLIES-WFF-THREAD- TABLE and the :type-prescription rules UNIQUE-ID- THREAD-TABLE, WFF-CALL-FRAME-REGULAR, WFF-STATE- REGULAR and WFF-THREAD-TABLE-REGULAR. Q.E.D. Summary Form: ( DEFTHM CORRECTNESS-RESTATED ...) Rules: ((:COMPOUND-RECOGNIZER INTP-IMPLIES-INTEGERP) (:DEFINITION LOCAL-AT) (:DEFINITION N) (:DEFINITION NOT) (:DEFINITION NTH) (:DEFINITION PROGRAM-IS) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INTP) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:REWRITE ACL2::|(* y x)|) (:REWRITE CAR-CDR-ELIM) (:REWRITE WFF-THREAD-TABLE-REGULAR-IMPLIES-WFF-THREAD-TABLE) (:TYPE-PRESCRIPTION UNIQUE-ID-THREAD-TABLE) (:TYPE-PRESCRIPTION WFF-CALL-FRAME-REGULAR) (:TYPE-PRESCRIPTION WFF-STATE-REGULAR) (:TYPE-PRESCRIPTION WFF-THREAD-TABLE-REGULAR)) Warnings: None Time: 0.29 seconds (prove: 0.11, print: 0.18, other: 0.00) CORRECTNESS-RESTATED m6 >