;================================================================= ; Demo 1 ;================================================================= ACL2 >(defun app (x y) (if (endp x) y (cons (car x) (app (cdr x) y)))) The admission of APP is trivial, using the relation E0- ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP) and the measure (ACL2-COUNT X). We observe that the type of APP is described by the theorem (OR (CONSP (APP X Y)) (EQUAL (APP X Y) Y)). We used primitive type reasoning. Summary Form: ( DEFUN APP ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) APP ACL2 >(app '(1 2 3) '(4 5 6)) (1 2 3 4 5 6) ACL2 >(defthm app-is-associative (equal (app (app a b) c) (app a (app 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 (APP A B). If we let (:P A B C) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP A)) (:P (CDR A) B C)) (:P A B C)) (IMPLIES (ENDP A) (:P A B C))). This induction is justified by the same argument used to admit APP, namely, the measure (ACL2-COUNT A) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). When applied to the goal at hand the above induction scheme produces the following two nontautological subgoals. Subgoal *1/2 (IMPLIES (AND (NOT (ENDP A)) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (APP A B) C) (APP A (APP B C)))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (APP A B) C) (APP A (APP B C)))). But simplification reduces this to T, using the :definition APP, primitive type reasoning and the :rewrite rules CAR- CONS and CDR-CONS. Subgoal *1/1 (IMPLIES (ENDP A) (EQUAL (APP (APP A B) C) (APP A (APP B C)))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/1' (IMPLIES (NOT (CONSP A)) (EQUAL (APP (APP A B) C) (APP A (APP B C)))). But simplification reduces this to T, using the :definition APP and primitive type reasoning. That completes the proof of *1. Q.E.D. Summary Form: ( DEFTHM APP-IS-ASSOCIATIVE ...) Rules: ((:DEFINITION APP) (:DEFINITION ENDP) (:DEFINITION NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) APP-IS-ASSOCIATIVE ACL2 >(defun insert (e x) (cond ((endp x) (cons e x)) ((<= e (car x)) (cons e x)) (t (cons (car x) (insert e (cdr x)))))) The admission of INSERT is trivial, using the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP) and the measure (ACL2-COUNT X). We observe that the type of INSERT is described by the theorem (CONSP (INSERT E X)). We used primitive type reasoning. Summary Form: ( DEFUN INSERT ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) INSERT ACL2 >(insert 3 '(1 2 4 5)) (1 2 3 4 5) ACL2 >(insert 3 '(1 2 3 4 5)) (1 2 3 3 4 5) ACL2 >(defun isort (x) (cond ((endp x) nil) (t (insert (car x) (isort (cdr x)))))) The admission of ISORT is trivial, using the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP) and the measure (ACL2-COUNT X). We observe that the type of ISORT is described by the theorem (OR (CONSP (ISORT X)) (EQUAL (ISORT X) NIL)). We used the :type-prescription rule INSERT. Summary Form: ( DEFUN ISORT ...) Rules: ((:TYPE-PRESCRIPTION INSERT)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ISORT ACL2 >(isort '(5 4 3 1 2)) (1 2 3 4 5) ACL2 >(defun ordered (x) (cond ((endp x) t) ((endp (cdr x)) t) (t (and (<= (car x) (car (cdr x))) (ordered (cdr x)))))) The admission of ORDERED is trivial, using the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP) and the measure (ACL2-COUNT X). We observe that the type of ORDERED is described by the theorem (OR (EQUAL (ORDERED X) T) (EQUAL (ORDERED X) NIL)). Summary Form: ( DEFUN ORDERED ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00) ORDERED ACL2 >(defthm isort-is-correct (and (ordered (isort x)) (perm (isort x) x))) By case analysis we reduce the conjecture to the following two conjectures. Subgoal 2 (ORDERED (ISORT X)). Name the formula above *1. Subgoal 1 (PERM (ISORT X) X). Normally we would attempt to prove this formula by induction. However, we prefer in this instance to focus on the original input conjecture rather than this simplified special case. We therefore abandon our previous work on this conjecture and reassign the name *1 to the original conjecture. (See :DOC otf-flg.) Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. Subsumption reduces that number to one. We will induct according to a scheme suggested by (ISORT X). If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit ISORT, namely, the measure (ACL2-COUNT X) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0- ORDINALP). When applied to the goal at hand the above induction scheme produces the following two nontautological subgoals. Subgoal *1/2 (IMPLIES (AND (NOT (ENDP X)) (AND (ORDERED (ISORT (CDR X))) (PERM (ISORT (CDR X)) (CDR X)))) (AND (ORDERED (ISORT X)) (PERM (ISORT X) X))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (CONSP X) (ORDERED (ISORT (CDR X))) (PERM (ISORT (CDR X)) (CDR X))) (AND (ORDERED (ISORT X)) (PERM (ISORT X) X))). This simplifies, using the :definition ISORT, to the following two conjectures. Subgoal *1/2.2 (IMPLIES (AND (CONSP X) (ORDERED (ISORT (CDR X))) (PERM (ISORT (CDR X)) (CDR X))) (ORDERED (INSERT (CAR X) (ISORT (CDR X))))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X) by X2. This produces the following goal. Subgoal *1/2.2' (IMPLIES (AND (CONSP (CONS X1 X2)) (ORDERED (ISORT X2)) (PERM (ISORT X2) X2)) (ORDERED (INSERT X1 (ISORT X2)))). This simplifies, using primitive type reasoning, to Subgoal *1/2.2'' (IMPLIES (AND (ORDERED (ISORT X2)) (PERM (ISORT X2) X2)) (ORDERED (INSERT X1 (ISORT X2)))). We generalize this conjecture, replacing (ISORT X2) by IT. This produces Subgoal *1/2.2''' (IMPLIES (AND (ORDERED IT) (PERM IT X2)) (ORDERED (INSERT X1 IT))). This simplifies, using trivial observations, to Subgoal *1/2.2'4' (IMPLIES (ORDERED IT) (ORDERED (INSERT X1 IT))). Name the formula above *1.1. Subgoal *1/2.1 (IMPLIES (AND (CONSP X) (ORDERED (ISORT (CDR X))) (PERM (ISORT (CDR X)) (CDR X))) (PERM (INSERT (CAR X) (ISORT (CDR X))) X)). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X) by X2. This produces the following goal. Subgoal *1/2.1' (IMPLIES (AND (CONSP (CONS X1 X2)) (ORDERED (ISORT X2)) (PERM (ISORT X2) X2)) (PERM (INSERT X1 (ISORT X2)) (CONS X1 X2))). This simplifies, using primitive type reasoning, to Subgoal *1/2.1'' (IMPLIES (AND (ORDERED (ISORT X2)) (PERM (ISORT X2) X2)) (PERM (INSERT X1 (ISORT X2)) (CONS X1 X2))). We generalize this conjecture, replacing (ISORT X2) by IT. This produces Subgoal *1/2.1''' (IMPLIES (AND (ORDERED IT) (PERM IT X2)) (PERM (INSERT X1 IT) (CONS X1 X2))). This simplifies, using the :congruence rule PERM-IMPLIES- PERM-CONS-2, to Subgoal *1/2.1'4' (IMPLIES (ORDERED IT) (PERM (INSERT X1 IT) (CONS X1 IT))). Name the formula above *1.2. Subgoal *1/1 (IMPLIES (ENDP X) (AND (ORDERED (ISORT X)) (PERM (ISORT X) X))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/1' (IMPLIES (NOT (CONSP X)) (AND (ORDERED (ISORT X)) (PERM (ISORT X) X))). But simplification reduces this to T, using the :definitions ISORT and PERM and the :executable-counterparts of CONSP and ORDERED. So we now return to *1.2, which is (IMPLIES (ORDERED IT) (PERM (INSERT X1 IT) (CONS X1 IT))). Perhaps we can prove *1.2 by induction. Two induction schemes are suggested by this conjecture. These merge into one derived induction scheme. We will induct according to a scheme suggested by (INSERT X1 IT). If we let (:P IT X1) denote *1.2 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP IT)) (< (CAR IT) X1) (:P (CDR IT) X1)) (:P IT X1)) (IMPLIES (AND (NOT (ENDP IT)) (<= X1 (CAR IT))) (:P IT X1)) (IMPLIES (ENDP IT) (:P IT X1))). This induction is justified by the same argument used to admit INSERT, namely, the measure (ACL2-COUNT IT) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0- ORDINALP). When applied to the goal at hand the above induction scheme produces the following four nontautological subgoals. Subgoal *1.2/4 (IMPLIES (AND (NOT (ENDP IT)) (< (CAR IT) X1) (PERM (INSERT X1 (CDR IT)) (CONS X1 (CDR IT))) (ORDERED IT)) (PERM (INSERT X1 IT) (CONS X1 IT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.2/4' (IMPLIES (AND (CONSP IT) (< (CAR IT) X1) (PERM (INSERT X1 (CDR IT)) (CONS X1 (CDR IT))) (ORDERED IT)) (PERM (INSERT X1 IT) (CONS X1 IT))). This simplifies, using the :congruence rule PERM-IMPLIES- PERM-CONS-2, the :definitions DEL, INSERT, MEM, ORDERED and PERM, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to the following eight conjectures. Subgoal *1.2/4.8 (IMPLIES (AND (CONSP IT) (< (CAR IT) X1) (PERM (INSERT X1 (CDR IT)) (CONS X1 (CDR IT))) (NOT (CONSP (CDR IT))) (EQUAL (CAR IT) X1)) (MEM X1 IT)). But simplification reduces this to T, using linear arithmetic. Subgoal *1.2/4.7 (IMPLIES (AND (CONSP IT) (< (CAR IT) X1) (PERM (INSERT X1 (CDR IT)) (CONS X1 (CDR IT))) (NOT (CONSP (CDR IT))) (EQUAL (CAR IT) X1)) (NOT (CONSP (DEL X1 IT)))). But simplification reduces this to T, using linear arithmetic. Subgoal *1.2/4.6 (IMPLIES (AND (CONSP IT) (< (CAR IT) X1) (PERM (INSERT X1 (CDR IT)) (CONS X1 (CDR IT))) (NOT (CONSP (CDR IT))) (NOT (EQUAL (CAR IT) X1))) (MEM X1 (CONS X1 (CDR IT)))). But simplification reduces this to T, using the :definition MEM, primitive type reasoning and the :rewrite rule CAR- CONS. Subgoal *1.2/4.5 (IMPLIES (AND (CONSP IT) (< (CAR IT) X1) (PERM (INSERT X1 (CDR IT)) (CONS X1 (CDR IT))) (NOT (CONSP (CDR IT))) (NOT (EQUAL (CAR IT) X1))) (NOT (CONSP (DEL X1 (CONS X1 (CDR IT)))))). But simplification reduces this to T, using the :definition DEL, primitive type reasoning and the :rewrite rules CAR- CONS and CDR-CONS. Subgoal *1.2/4.4 (IMPLIES (AND (CONSP IT) (< (CAR IT) X1) (PERM (INSERT X1 (CDR IT)) (CONS X1 (CDR IT))) (<= (CAR IT) (CADR IT)) (ORDERED (CDR IT)) (EQUAL (CAR IT) X1)) (MEM X1 IT)). But simplification reduces this to T, using linear arithmetic. Subgoal *1.2/4.3 (IMPLIES (AND (CONSP IT) (< (CAR IT) X1) (PERM (INSERT X1 (CDR IT)) (CONS X1 (CDR IT))) (<= (CAR IT) (CADR IT)) (ORDERED (CDR IT)) (EQUAL (CAR IT) X1)) (PERM (CDR IT) (DEL X1 IT))). But simplification reduces this to T, using linear arithmetic. Subgoal *1.2/4.2 (IMPLIES (AND (CONSP IT) (< (CAR IT) X1) (PERM (INSERT X1 (CDR IT)) (CONS X1 (CDR IT))) (<= (CAR IT) (CADR IT)) (ORDERED (CDR IT)) (NOT (EQUAL (CAR IT) X1))) (MEM X1 (CONS X1 (CDR IT)))). But simplification reduces this to T, using the :definition MEM, primitive type reasoning and the :rewrite rule CAR- CONS. Subgoal *1.2/4.1 (IMPLIES (AND (CONSP IT) (< (CAR IT) X1) (PERM (INSERT X1 (CDR IT)) (CONS X1 (CDR IT))) (<= (CAR IT) (CADR IT)) (ORDERED (CDR IT)) (NOT (EQUAL (CAR IT) X1))) (PERM (CDR IT) (DEL X1 (CONS X1 (CDR IT))))). But simplification reduces this to T, using the :definitions DEL, MEM and PERM, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. Subgoal *1.2/3 (IMPLIES (AND (NOT (ENDP IT)) (< (CAR IT) X1) (NOT (ORDERED (CDR IT))) (ORDERED IT)) (PERM (INSERT X1 IT) (CONS X1 IT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.2/3' (IMPLIES (AND (CONSP IT) (< (CAR IT) X1) (NOT (ORDERED (CDR IT))) (ORDERED IT)) (PERM (INSERT X1 IT) (CONS X1 IT))). This simplifies, using the :definitions DEL, INSERT, MEM, ORDERED and PERM, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to the following two conjectures. Subgoal *1.2/3.2 (IMPLIES (AND (CONSP IT) (< (CAR IT) X1) (NOT (ORDERED (CDR IT))) (NOT (CONSP (CDR IT))) (EQUAL (CAR IT) X1)) (PERM (INSERT X1 (CDR IT)) IT)). But simplification reduces this to T, using linear arithmetic. Subgoal *1.2/3.1 (IMPLIES (AND (CONSP IT) (< (CAR IT) X1) (NOT (ORDERED (CDR IT))) (NOT (CONSP (CDR IT))) (NOT (EQUAL (CAR IT) X1))) (PERM (INSERT X1 (CDR IT)) (CONS X1 (CDR IT)))). But simplification reduces this to T, using the :definition ORDERED. Subgoal *1.2/2 (IMPLIES (AND (NOT (ENDP IT)) (<= X1 (CAR IT)) (ORDERED IT)) (PERM (INSERT X1 IT) (CONS X1 IT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.2/2' (IMPLIES (AND (CONSP IT) (<= X1 (CAR IT)) (ORDERED IT)) (PERM (INSERT X1 IT) (CONS X1 IT))). But simplification reduces this to T, using the :definitions DEL, INSERT, MEM, ORDERED and PERM, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. Subgoal *1.2/1 (IMPLIES (AND (ENDP IT) (ORDERED IT)) (PERM (INSERT X1 IT) (CONS X1 IT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.2/1' (IMPLIES (AND (NOT (CONSP IT)) (ORDERED IT)) (PERM (INSERT X1 IT) (CONS X1 IT))). But simplification reduces this to T, using the :definitions DEL, INSERT, MEM, ORDERED and PERM, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. That completes the proof of *1.2. We therefore turn our attention to *1.1, which is (IMPLIES (ORDERED IT) (ORDERED (INSERT X1 IT))). Perhaps we can prove *1.1 by induction. Two induction schemes are suggested by this conjecture. These merge into one derived induction scheme. We will induct according to a scheme suggested by (INSERT X1 IT). If we let (:P IT X1) denote *1.1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP IT)) (< (CAR IT) X1) (:P (CDR IT) X1)) (:P IT X1)) (IMPLIES (AND (NOT (ENDP IT)) (<= X1 (CAR IT))) (:P IT X1)) (IMPLIES (ENDP IT) (:P IT X1))). This induction is justified by the same argument used to admit INSERT, namely, the measure (ACL2-COUNT IT) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0- ORDINALP). When applied to the goal at hand the above induction scheme produces the following four nontautological subgoals. Subgoal *1.1/4 (IMPLIES (AND (NOT (ENDP IT)) (< (CAR IT) X1) (ORDERED (INSERT X1 (CDR IT))) (ORDERED IT)) (ORDERED (INSERT X1 IT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/4' (IMPLIES (AND (CONSP IT) (< (CAR IT) X1) (ORDERED (INSERT X1 (CDR IT))) (ORDERED IT)) (ORDERED (INSERT X1 IT))). This simplifies, using the :definitions INSERT and ORDERED, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription rules INSERT and ORDERED, to the following two conjectures. Subgoal *1.1/4.2 (IMPLIES (AND (CONSP IT) (< (CAR IT) X1) (ORDERED (INSERT X1 (CDR IT))) (NOT (CONSP (CDR IT)))) (<= (CAR IT) (CAR (INSERT X1 (CDR IT))))). This simplifies, using the :definitions INSERT and ORDERED, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to Subgoal *1.1/4.2' (IMPLIES (AND (CONSP IT) (< (CAR IT) X1) (NOT (CONSP (CDR IT)))) (<= (CAR IT) X1)). But simplification reduces this to T, using linear arithmetic. Subgoal *1.1/4.1 (IMPLIES (AND (CONSP IT) (< (CAR IT) X1) (ORDERED (INSERT X1 (CDR IT))) (<= (CAR IT) (CADR IT)) (ORDERED (CDR IT))) (<= (CAR IT) (CAR (INSERT X1 (CDR IT))))). The destructor terms (CAR IT) and (CDR IT) can be eliminated. Furthermore, those terms are at the root of a chain of two rounds of destructor elimination. (1) Use CAR-CDR- ELIM to replace IT by (CONS IT1 IT2), (CAR IT) by IT1 and (CDR IT) by IT2. (2) Use CAR-CDR-ELIM, again, to replace IT2 by (CONS IT3 IT4), (CAR IT2) by IT3 and (CDR IT2) by IT4. These steps produce the following two goals. Subgoal *1.1/4.1.2 (IMPLIES (AND (NOT (CONSP IT2)) (CONSP (CONS IT1 IT2)) (< IT1 X1) (ORDERED (INSERT X1 IT2)) (<= IT1 (CAR IT2)) (ORDERED IT2)) (<= IT1 (CAR (INSERT X1 IT2)))). This simplifies, using the :definitions INSERT and ORDERED, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, DEFAULT-<-1 and DEFAULT-CAR, to Subgoal *1.1/4.1.2' (IMPLIES (AND (NOT (CONSP IT2)) (< IT1 X1) (<= IT1 0)) (<= IT1 X1)). But simplification reduces this to T, using linear arithmetic. Subgoal *1.1/4.1.1 (IMPLIES (AND (CONSP (CONS IT3 IT4)) (CONSP (LIST* IT1 IT3 IT4)) (< IT1 X1) (ORDERED (INSERT X1 (CONS IT3 IT4))) (<= IT1 IT3) (ORDERED (CONS IT3 IT4))) (<= IT1 (CAR (INSERT X1 (CONS IT3 IT4))))). This simplifies, using the :definitions INSERT and ORDERED, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to the following two conjectures. Subgoal *1.1/4.1.1.2 (IMPLIES (AND (< IT1 X1) (<= X1 IT3) (ORDERED (LIST* X1 IT3 IT4)) (<= IT1 IT3) (NOT (CONSP IT4))) (<= IT1 X1)). But simplification reduces this to T, using linear arithmetic. Subgoal *1.1/4.1.1.1 (IMPLIES (AND (< IT1 X1) (<= X1 IT3) (ORDERED (LIST* X1 IT3 IT4)) (<= IT1 IT3) (<= IT3 (CAR IT4)) (ORDERED IT4)) (<= IT1 X1)). But simplification reduces this to T, using linear arithmetic. Subgoal *1.1/3 (IMPLIES (AND (NOT (ENDP IT)) (< (CAR IT) X1) (NOT (ORDERED (CDR IT))) (ORDERED IT)) (ORDERED (INSERT X1 IT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/3' (IMPLIES (AND (CONSP IT) (< (CAR IT) X1) (NOT (ORDERED (CDR IT))) (ORDERED IT)) (ORDERED (INSERT X1 IT))). This simplifies, using the :definitions INSERT and ORDERED, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription rule INSERT, to the following two conjectures. Subgoal *1.1/3.2 (IMPLIES (AND (CONSP IT) (< (CAR IT) X1) (NOT (ORDERED (CDR IT))) (NOT (CONSP (CDR IT)))) (<= (CAR IT) (CAR (INSERT X1 (CDR IT))))). But simplification reduces this to T, using the :definition ORDERED. Subgoal *1.1/3.1 (IMPLIES (AND (CONSP IT) (< (CAR IT) X1) (NOT (ORDERED (CDR IT))) (NOT (CONSP (CDR IT)))) (ORDERED (INSERT X1 (CDR IT)))). But simplification reduces this to T, using the :definition ORDERED. Subgoal *1.1/2 (IMPLIES (AND (NOT (ENDP IT)) (<= X1 (CAR IT)) (ORDERED IT)) (ORDERED (INSERT X1 IT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/2' (IMPLIES (AND (CONSP IT) (<= X1 (CAR IT)) (ORDERED IT)) (ORDERED (INSERT X1 IT))). But simplification reduces this to T, using the :definitions INSERT and ORDERED, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription rule ORDERED. Subgoal *1.1/1 (IMPLIES (AND (ENDP IT) (ORDERED IT)) (ORDERED (INSERT X1 IT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/1' (IMPLIES (AND (NOT (CONSP IT)) (ORDERED IT)) (ORDERED (INSERT X1 IT))). But simplification reduces this to T, using the :definitions INSERT and ORDERED, primitive type reasoning and the :rewrite rule CDR-CONS. That completes the proofs of *1.1 and *1. Q.E.D. The storage of ISORT-IS-CORRECT depends upon the :type- prescription rule ORDERED. Summary Form: ( DEFTHM ISORT-IS-CORRECT ...) Rules: ((:CONGRUENCE PERM-IMPLIES-PERM-CONS-2) (:DEFINITION DEL) (:DEFINITION ENDP) (:DEFINITION INSERT) (:DEFINITION ISORT) (:DEFINITION MEM) (:DEFINITION NOT) (:DEFINITION ORDERED) (:DEFINITION PERM) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART ORDERED) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE DEFAULT-<-1) (:REWRITE DEFAULT-CAR) (:TYPE-PRESCRIPTION INSERT) (:TYPE-PRESCRIPTION ORDERED)) Warnings: None Time: 0.22 seconds (prove: 0.17, print: 0.04, other: 0.01) ISORT-IS-CORRECT ACL2 >(quote (end of Demo 1)) (END OF DEMO 1) ;================================================================= ; Demo 2 ;================================================================= hailes% cat Demo.java class Demo { public static int fact(int n){ if (n>0) {return n*fact(n-1);} else return 1; } public static void main(String[] args){ int n = Integer.parseInt(args[0], 10); System.out.println(fact(n)); return; } } hailes% javac Demo.java hailes% javap -c Demo Compiled from Demo.java synchronized class Demo extends java.lang.Object /* ACC_SUPER bit set */ { public static int fact(int); public static void main(java.lang.String[]); Demo(); } Method int fact(int) 0 iload_0 1 ifle 13 4 iload_0 5 iload_0 6 iconst_1 7 isub 8 invokestatic #7 11 imul 12 ireturn 13 iconst_1 14 ireturn Method void main(java.lang.String[]) 0 aload_0 1 iconst_0 2 aaload 3 bipush 10 5 invokestatic #9 8 istore_1 9 getstatic #8 12 iload_1 13 invokestatic #7 16 invokevirtual #10 19 return Method Demo() 0 aload_0 1 invokespecial #6 4 return hailes% java Demo 5 120 hailes% java Demo 10 3628800 hailes% java Demo 15 2004310016 hailes% java Demo 20 -2102132736 hailes% java Demo 34 0 ;================================================================= ; Demo 3 ;================================================================= ACL2 >(in-package "M5") "M5" M5 >(lookup-method "fact" "Demo" (class-table *demo-state*)) ("fact" (INT) NIL (ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN)) M5 >(pe 'run) d 1 (INCLUDE-BOOK "/u/moore/m5/tolquhon/jvm-fact-setup") \ >L d (DEFUN RUN (SCHED S) (IF (ENDP SCHED) S (RUN (CDR SCHED) (STEP (CAR SCHED) S)))) M5 >(pe 'step) d 1 (INCLUDE-BOOK "/u/moore/m5/tolquhon/jvm-fact-setup") \ >L d (DEFUN STEP (TH S) (IF (EQUAL (STATUS TH S) 'SCHEDULED) (DO-INST (NEXT-INST TH S) TH S) S)) M5 >(pe 'do-inst) d 1 (INCLUDE-BOOK "/u/moore/m5/tolquhon/jvm-fact-setup") \ >L (DEFUN DO-INST (INST TH S) (CASE (OP-CODE INST) (AALOAD (EXECUTE-AALOAD INST TH S)) (AASTORE (EXECUTE-AASTORE INST TH S)) (ACONST_NULL (EXECUTE-ACONST_NULL INST TH S)) (ALOAD (EXECUTE-ALOAD INST TH S)) (ALOAD_0 (EXECUTE-ALOAD_X INST TH S 0)) (ALOAD_1 (EXECUTE-ALOAD_X INST TH S 1)) (ALOAD_2 (EXECUTE-ALOAD_X INST TH S 2)) (ALOAD_3 (EXECUTE-ALOAD_X INST TH S 3)) (ANEWARRAY (EXECUTE-ANEWARRAY INST TH S)) (ARETURN (EXECUTE-ARETURN INST TH S)) (ARRAYLENGTH (EXECUTE-ARRAYLENGTH INST TH S)) (ASTORE (EXECUTE-ASTORE INST TH S)) (ASTORE_0 (EXECUTE-ASTORE_X INST TH S 0)) (ASTORE_1 (EXECUTE-ASTORE_X INST TH S 1)) (ASTORE_2 (EXECUTE-ASTORE_X INST TH S 2)) (ASTORE_3 (EXECUTE-ASTORE_X INST TH S 3)) (BALOAD (EXECUTE-BALOAD INST TH S)) (BASTORE (EXECUTE-BASTORE INST TH S)) (BIPUSH (EXECUTE-BIPUSH INST TH S)) (CALOAD (EXECUTE-CALOAD INST TH S)) (CASTORE (EXECUTE-CASTORE INST TH S)) (DUP (EXECUTE-DUP INST TH S)) (DUP_X1 (EXECUTE-DUP_X1 INST TH S)) (DUP_X2 (EXECUTE-DUP_X2 INST TH S)) (DUP2 (EXECUTE-DUP2 INST TH S)) (DUP2_X1 (EXECUTE-DUP2_X1 INST TH S)) (DUP2_X2 (EXECUTE-DUP2_X2 INST TH S)) (GETFIELD (EXECUTE-GETFIELD INST TH S)) (GETSTATIC (EXECUTE-GETSTATIC INST TH S)) (GOTO (EXECUTE-GOTO INST TH S)) (GOTO_W (EXECUTE-GOTO_W INST TH S)) (I2B (EXECUTE-I2B INST TH S)) (I2C (EXECUTE-I2C INST TH S)) (I2L (EXECUTE-I2L INST TH S)) (I2S (EXECUTE-I2S INST TH S)) (IADD (EXECUTE-IADD INST TH S)) (IALOAD (EXECUTE-IALOAD INST TH S)) (IAND (EXECUTE-IAND INST TH S)) (IASTORE (EXECUTE-IASTORE INST TH S)) (ICONST_M1 (EXECUTE-ICONST_X INST TH S -1)) (ICONST_0 (EXECUTE-ICONST_X INST TH S 0)) (ICONST_1 (EXECUTE-ICONST_X INST TH S 1)) (ICONST_2 (EXECUTE-ICONST_X INST TH S 2)) (ICONST_3 (EXECUTE-ICONST_X INST TH S 3)) (ICONST_4 (EXECUTE-ICONST_X INST TH S 4)) (ICONST_5 (EXECUTE-ICONST_X INST TH S 5)) (IDIV (EXECUTE-IDIV INST TH S)) (IF_ACMPEQ (EXECUTE-IF_ACMPEQ INST TH S)) (IF_ACMPNE (EXECUTE-IF_ACMPNE INST TH S)) (IF_ICMPEQ (EXECUTE-IF_ICMPEQ INST TH S)) (IF_ICMPGE (EXECUTE-IF_ICMPGE INST TH S)) (IF_ICMPGT (EXECUTE-IF_ICMPGT INST TH S)) (IF_ICMPLE (EXECUTE-IF_ICMPLE INST TH S)) (IF_ICMPLT (EXECUTE-IF_ICMPLT INST TH S)) (IF_ICMPNE (EXECUTE-IF_ICMPNE INST TH S)) (IFEQ (EXECUTE-IFEQ INST TH S)) (IFGE (EXECUTE-IFGE INST TH S)) (IFGT (EXECUTE-IFGT INST TH S)) (IFLE (EXECUTE-IFLE INST TH S)) (IFLT (EXECUTE-IFLT INST TH S)) (IFNE (EXECUTE-IFNE INST TH S)) (IFNONNULL (EXECUTE-IFNONNULL INST TH S)) (IFNULL (EXECUTE-IFNULL INST TH S)) (IINC (EXECUTE-IINC INST TH S)) (ILOAD (EXECUTE-ILOAD INST TH S)) (ILOAD_0 (EXECUTE-ILOAD_X INST TH S 0)) (ILOAD_1 (EXECUTE-ILOAD_X INST TH S 1)) (ILOAD_2 (EXECUTE-ILOAD_X INST TH S 2)) (ILOAD_3 (EXECUTE-ILOAD_X INST TH S 3)) (IMUL (EXECUTE-IMUL INST TH S)) (INEG (EXECUTE-INEG INST TH S)) (INSTANCEOF (EXECUTE-INSTANCEOF INST TH S)) (INVOKESPECIAL (EXECUTE-INVOKESPECIAL INST TH S)) (INVOKESTATIC (EXECUTE-INVOKESTATIC INST TH S)) (INVOKEVIRTUAL (EXECUTE-INVOKEVIRTUAL INST TH S)) (IOR (EXECUTE-IOR INST TH S)) (IREM (EXECUTE-IREM INST TH S)) (IRETURN (EXECUTE-IRETURN INST TH S)) (ISHL (EXECUTE-ISHL INST TH S)) (ISHR (EXECUTE-ISHR INST TH S)) (ISTORE (EXECUTE-ISTORE INST TH S)) (ISTORE_0 (EXECUTE-ISTORE_X INST TH S 0)) (ISTORE_1 (EXECUTE-ISTORE_X INST TH S 1)) (ISTORE_2 (EXECUTE-ISTORE_X INST TH S 2)) (ISTORE_3 (EXECUTE-ISTORE_X INST TH S 3)) (ISUB (EXECUTE-ISUB INST TH S)) (IUSHR (EXECUTE-IUSHR INST TH S)) (IXOR (EXECUTE-IXOR INST TH S)) (JSR (EXECUTE-JSR INST TH S)) (JSR_W (EXECUTE-JSR_W INST TH S)) (L2I (EXECUTE-L2I INST TH S)) (LADD (EXECUTE-LADD INST TH S)) (LALOAD (EXECUTE-LALOAD INST TH S)) (LAND (EXECUTE-LAND INST TH S)) (LASTORE (EXECUTE-LASTORE INST TH S)) (LCMP (EXECUTE-LCMP INST TH S)) (LCONST_0 (EXECUTE-LCONST_X INST TH S 0)) (LCONST_1 (EXECUTE-LCONST_X INST TH S 1)) (LDC (EXECUTE-LDC INST TH S)) (LDC_W (EXECUTE-LDC INST TH S)) (LDC2_W (EXECUTE-LDC2_W INST TH S)) (LDIV (EXECUTE-LDIV INST TH S)) (LLOAD (EXECUTE-LLOAD INST TH S)) (LLOAD_0 (EXECUTE-LLOAD_X INST TH S 0)) (LLOAD_1 (EXECUTE-LLOAD_X INST TH S 1)) (LLOAD_2 (EXECUTE-LLOAD_X INST TH S 2)) (LLOAD_3 (EXECUTE-LLOAD_X INST TH S 3)) (LMUL (EXECUTE-LMUL INST TH S)) (LNEG (EXECUTE-LNEG INST TH S)) (LOR (EXECUTE-LOR INST TH S)) (LREM (EXECUTE-LREM INST TH S)) (LRETURN (EXECUTE-LRETURN INST TH S)) (LSHL (EXECUTE-LSHL INST TH S)) (LSHR (EXECUTE-LSHR INST TH S)) (LSTORE (EXECUTE-LSTORE INST TH S)) (LSTORE_0 (EXECUTE-LSTORE_X INST TH S 0)) (LSTORE_1 (EXECUTE-LSTORE_X INST TH S 1)) (LSTORE_2 (EXECUTE-LSTORE_X INST TH S 2)) (LSTORE_3 (EXECUTE-LSTORE_X INST TH S 3)) (LSUB (EXECUTE-LSUB INST TH S)) (LUSHR (EXECUTE-LUSHR INST TH S)) (LXOR (EXECUTE-LXOR INST TH S)) (MONITORENTER (EXECUTE-MONITORENTER INST TH S)) (MONITOREXIT (EXECUTE-MONITOREXIT INST TH S)) (MULTIANEWARRAY (EXECUTE-MULTIANEWARRAY INST TH S)) (NEW (EXECUTE-NEW INST TH S)) (NEWARRAY (EXECUTE-NEWARRAY INST TH S)) (NOP (EXECUTE-NOP INST TH S)) (POP (EXECUTE-POP INST TH S)) (POP2 (EXECUTE-POP2 INST TH S)) (PUTFIELD (EXECUTE-PUTFIELD INST TH S)) (PUTSTATIC (EXECUTE-PUTSTATIC INST TH S)) (RET (EXECUTE-RET INST TH S)) (RETURN (EXECUTE-RETURN INST TH S)) (SALOAD (EXECUTE-SALOAD INST TH S)) (SASTORE (EXECUTE-SASTORE INST TH S)) (SIPUSH (EXECUTE-SIPUSH INST TH S)) (SWAP (EXECUTE-SWAP INST TH S)) (HALT S) (OTHERWISE S))) M5 >(pe 'execute-iload) d 1 (INCLUDE-BOOK "/u/moore/m5/tolquhon/jvm-fact-setup") \ >L (DEFUN EXECUTE-ILOAD (INST TH S) (MODIFY TH S :PC (+ (INST-LENGTH INST) (PC (TOP-FRAME TH S))) :STACK (PUSH (NTH (ARG1 INST) (LOCALS (TOP-FRAME TH S))) (STACK (TOP-FRAME TH S))))) M5 >(pe 'execute-invokevirtual) d 1 (INCLUDE-BOOK "/u/moore/m5/tolquhon/jvm-fact-setup") \ >L (DEFUN EXECUTE-INVOKEVIRTUAL (INST TH S) (LET* ((METHOD-NAME (ARG2 INST)) (NFORMALS (ARG3 INST)) (OBJ-REF (TOP (POPN NFORMALS (STACK (TOP-FRAME TH S))))) (INSTANCE (DEREF OBJ-REF (HEAP S))) (OBJ-CLASS-NAME (CLASS-NAME-OF-REF OBJ-REF (HEAP S))) (CLOSEST-METHOD (LOOKUP-METHOD METHOD-NAME OBJ-CLASS-NAME (CLASS-TABLE S))) (PROG (METHOD-PROGRAM CLOSEST-METHOD)) (S1 (MODIFY TH S :PC (+ (INST-LENGTH INST) (PC (TOP-FRAME TH S))) :STACK (POPN (+ NFORMALS 1) (STACK (TOP-FRAME TH S))))) (TTHREAD (RREFTOTHREAD OBJ-REF (THREAD-TABLE S)))) (COND ((METHOD-ISNATIVE? CLOSEST-METHOD) (COND ((EQUAL METHOD-NAME "start") (MODIFY TTHREAD S1 :STATUS 'SCHEDULED)) ((EQUAL METHOD-NAME "stop") (MODIFY TTHREAD S1 :STATUS 'UNSCHEDULED)) (T S))) ((AND (METHOD-SYNC CLOSEST-METHOD) (OBJECTLOCKABLE? INSTANCE TH)) (MODIFY TH S1 :CALL-STACK (PUSH (MAKE-FRAME 0 (REVERSE (BIND-FORMALS (+ NFORMALS 1) (STACK (TOP-FRAME TH S)))) NIL PROG 'LOCKED (ARG1 INST)) (CALL-STACK TH S1)) :HEAP (LOCK-OBJECT TH OBJ-REF (HEAP S)))) ((METHOD-SYNC CLOSEST-METHOD) S) (T (MODIFY TH S1 :CALL-STACK (PUSH (MAKE-FRAME 0 (REVERSE (BIND-FORMALS (+ NFORMALS 1) (STACK (TOP-FRAME TH S)))) NIL PROG 'UNLOCKED (ARG1 INST)) (CALL-STACK TH S1))))))) M5 >(pe 'acl2-Demo) L 2 (DEFUN ACL2-DEMO (N) (TOP (STACK (TOP-FRAME 0 (RUN (FACT-SCHED 0 N) (MODIFY 0 *DEMO-STATE* :PC 0 :STACK (PUSH N NIL) :PROGRAM '((INVOKESTATIC "Demo" "fact" 1)))))))) M5 >(acl2-Demo 5) 120 M5 >(! 5) 120 M5 >(acl2-Demo 10) 3628800 M5 >(! 10) 3628800 M5 >(acl2-Demo 15) 2004310016 M5 >(! 15) 1307674368000 M5 >(int-fix (! 15)) 2004310016 M5 >(acl2-Demo 20) -2102132736 M5 >(! 20) 2432902008176640000 M5 >(int-fix (! 20)) -2102132736 M5 >(acl2-Demo 34) 0 M5 >(acl2-Demo 100) 0 M5 >(! 100) 93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000 M5 >(quote (end of Demo 3)) (END OF DEMO 3) ;================================================================= ; Demo 4 ;================================================================= M5 > (pe 'poised-to-invoke-fact) d 1 (INCLUDE-BOOK "/u/moore/m5/tolquhon/jvm-fact-setup") \ (DEFUN POISED-TO-INVOKE-FACT (TH S N) (AND (EQUAL (STATUS TH S) 'SCHEDULED) (EQUAL (NEXT-INST TH S) '(INVOKESTATIC "Demo" "fact" 1)) (EQUAL N (TOP (STACK (TOP-FRAME TH S)))) (INTP N) (EQUAL (LOOKUP-METHOD "fact" "Demo" (CLASS-TABLE S)) *FACT-DEF*))) M5 >(defthm fact-is-correct (implies (poised-to-invoke-fact th s n) (equal (run (fact-sched th n) s) (modify th s :pc (+ 3 (pc (top-frame th s))) :stack (push (int-fix (! n)) (pop (stack (top-frame th s))))))) :hints (("Goal" :induct (induction-hint th s n)))) [Note: A hint was supplied for our processing of the goal above. Thanks!] Name the formula above *1. We have been told to use induction. One induction scheme is suggested by the induction hint. We will induct according to a scheme suggested by (INDUCTION-HINT TH S N). If we let (:P N S TH) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ZP N)) (:P (+ -1 N) (MAKE-STATE (BIND TH (MAKE-THREAD (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP-FRAME TH S)))) (PUSH (+ -1 (TOP (STACK (TOP-FRAME TH S)))) (PUSH (TOP (STACK (TOP-FRAME TH S))) NIL)) (METHOD-PROGRAM '("fact" (INT) NIL (ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN))) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CALL-STACK TH S)))) (LOCALS (TOP (CALL-STACK TH S))) (POP (STACK (TOP (CALL-STACK TH S)))) (PROGRAM (TOP (CALL-STACK TH S))) (SYNC-FLG (TOP (CALL-STACK TH S))) (CUR-CLASS (TOP (CALL-STACK TH S)))) (POP (CALL-STACK TH S)))) 'SCHEDULED (RREF TH S)) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S)) TH)) (:P N S TH)) (IMPLIES (ZP N) (:P N S TH))). This induction is justified by the same argument used to admit INDUCTION-HINT, namely, the measure (ACL2-COUNT N) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). Note, however, that the unmeasured variable S is being instantiated. When applied to the goal at hand the above induction scheme produces the following two nontautological subgoals. Subgoal *1/2 (IMPLIES (AND (NOT (ZP N)) (IMPLIES (POISED-TO-INVOKE-FACT TH (MAKE-STATE (BIND TH (MAKE-THREAD (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP-FRAME TH S)))) (PUSH (+ -1 (TOP (STACK (TOP-FRAME TH S)))) (PUSH (TOP (STACK (TOP-FRAME TH S))) NIL)) (METHOD-PROGRAM '("fact" (INT) NIL (ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN))) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CALL-STACK TH S)))) (LOCALS (TOP (CALL-STACK TH S))) (POP (STACK (TOP (CALL-STACK TH S)))) (PROGRAM (TOP (CALL-STACK TH S))) (SYNC-FLG (TOP (CALL-STACK TH S))) (CUR-CLASS (TOP (CALL-STACK TH S)))) (POP (CALL-STACK TH S)))) 'SCHEDULED (RREF TH S)) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S)) (+ -1 N)) (EQUAL (RUN (FACT-SCHED TH (+ -1 N)) (MAKE-STATE (BIND TH (MAKE-THREAD (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP-FRAME TH S)))) (PUSH (+ -1 (TOP (STACK (TOP-FRAME TH S)))) (PUSH (TOP (STACK (TOP-FRAME TH S))) NIL)) (METHOD-PROGRAM '("fact" (INT) NIL (ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN))) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CALL-STACK TH S)))) (LOCALS (TOP (CALL-STACK TH S))) (POP (STACK (TOP (CALL-STACK TH S)))) (PROGRAM (TOP (CALL-STACK TH S))) (SYNC-FLG (TOP (CALL-STACK TH S))) (CUR-CLASS (TOP (CALL-STACK TH S)))) (POP (CALL-STACK TH S)))) 'SCHEDULED (RREF TH S)) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S))) (MAKE-STATE (BIND TH (MAKE-THREAD (PUSH (MAKE-FRAME (+ 3 (PC (TOP-FRAME TH (MAKE-STATE (BIND TH (MAKE-THREAD (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP-FRAME TH S)))) (PUSH (+ -1 (TOP (STACK (TOP-FRAME TH S)))) (PUSH (TOP (STACK (TOP-FRAME TH S))) NIL)) (METHOD-PROGRAM '("fact" (INT) NIL (ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN))) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CALL-STACK TH S)))) (LOCALS (TOP (CALL-STACK TH S))) (POP (STACK (TOP (CALL-STACK TH S)))) (PROGRAM (TOP (CALL-STACK TH S))) (SYNC-FLG (TOP (CALL-STACK TH S))) (CUR-CLASS (TOP (CALL-STACK TH S)))) (POP (CALL-STACK TH S)))) 'SCHEDULED (RREF TH S)) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S))))) (LOCALS (TOP-FRAME TH (MAKE-STATE (BIND TH (MAKE-THREAD (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP-FRAME TH S)))) (PUSH (+ -1 (TOP (STACK (TOP-FRAME TH S)))) (PUSH (TOP (STACK (TOP-FRAME TH S))) NIL)) (METHOD-PROGRAM '("fact" (INT) NIL (ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN))) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CALL-STACK TH S)))) (LOCALS (TOP (CALL-STACK TH S))) (POP (STACK (TOP (CALL-STACK TH S)))) (PROGRAM (TOP (CALL-STACK TH S))) (SYNC-FLG (TOP (CALL-STACK TH S))) (CUR-CLASS (TOP (CALL-STACK TH S)))) (POP (CALL-STACK TH S)))) 'SCHEDULED (RREF TH S)) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S)))) (PUSH (INT-FIX (! (+ -1 N))) (POP (STACK (TOP-FRAME TH (MAKE-STATE (BIND TH (MAKE-THREAD (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP-FRAME TH S)))) (PUSH (+ -1 (TOP (STACK (TOP-FRAME TH S)))) (PUSH (TOP (STACK (TOP-FRAME TH S))) NIL)) (METHOD-PROGRAM '("fact" (INT) NIL (ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN))) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CALL-STACK TH S)))) (LOCALS (TOP (CALL-STACK TH S))) (POP (STACK (TOP (CALL-STACK TH S)))) (PROGRAM (TOP (CALL-STACK TH S))) (SYNC-FLG (TOP (CALL-STACK TH S))) (CUR-CLASS (TOP (CALL-STACK TH S)))) (POP (CALL-STACK TH S)))) 'SCHEDULED (RREF TH S)) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S)))))) (PROGRAM (TOP-FRAME TH (MAKE-STATE (BIND TH (MAKE-THREAD (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP-FRAME TH S)))) (PUSH (+ -1 (TOP (STACK (TOP-FRAME TH S)))) (PUSH (TOP (STACK (TOP-FRAME TH S))) NIL)) (METHOD-PROGRAM '("fact" (INT) NIL (ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN))) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CALL-STACK TH S)))) (LOCALS (TOP (CALL-STACK TH S))) (POP (STACK (TOP (CALL-STACK TH S)))) (PROGRAM (TOP (CALL-STACK TH S))) (SYNC-FLG (TOP (CALL-STACK TH S))) (CUR-CLASS (TOP (CALL-STACK TH S)))) (POP (CALL-STACK TH S)))) 'SCHEDULED (RREF TH S)) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S)))) (SYNC-FLG (TOP-FRAME TH (MAKE-STATE (BIND TH (MAKE-THREAD (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP-FRAME TH S)))) (PUSH (+ -1 (TOP (STACK (TOP-FRAME TH S)))) (PUSH (TOP (STACK (TOP-FRAME TH S))) NIL)) (METHOD-PROGRAM '("fact" (INT) NIL (ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN))) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CALL-STACK TH S)))) (LOCALS (TOP (CALL-STACK TH S))) (POP (STACK (TOP (CALL-STACK TH S)))) (PROGRAM (TOP (CALL-STACK TH S))) (SYNC-FLG (TOP (CALL-STACK TH S))) (CUR-CLASS (TOP (CALL-STACK TH S)))) (POP (CALL-STACK TH S)))) 'SCHEDULED (RREF TH S)) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S)))) (CUR-CLASS (TOP-FRAME TH (MAKE-STATE (BIND TH (MAKE-THREAD (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP-FRAME TH S)))) (PUSH (+ -1 (TOP (STACK (TOP-FRAME TH S)))) (PUSH (TOP (STACK (TOP-FRAME TH S))) NIL)) (METHOD-PROGRAM '("fact" (INT) NIL (ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN))) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CALL-STACK TH S)))) (LOCALS (TOP (CALL-STACK TH S))) (POP (STACK (TOP (CALL-STACK TH S)))) (PROGRAM (TOP (CALL-STACK TH S))) (SYNC-FLG (TOP (CALL-STACK TH S))) (CUR-CLASS (TOP (CALL-STACK TH S)))) (POP (CALL-STACK TH S)))) 'SCHEDULED (RREF TH S)) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S))))) (POP (CALL-STACK TH (MAKE-STATE (BIND TH (MAKE-THREAD (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP-FRAME TH S)))) (PUSH (+ -1 (TOP (STACK (TOP-FRAME TH S)))) (PUSH (TOP (STACK (TOP-FRAME TH S))) NIL)) (METHOD-PROGRAM '("fact" (INT) NIL (ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN))) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CALL-STACK TH S)))) (LOCALS (TOP (CALL-STACK TH S))) (POP (STACK (TOP (CALL-STACK TH S)))) (PROGRAM (TOP (CALL-STACK TH S))) (SYNC-FLG (TOP (CALL-STACK TH S))) (CUR-CLASS (TOP (CALL-STACK TH S)))) (POP (CALL-STACK TH S)))) 'SCHEDULED (RREF TH S)) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S))))) (STATUS TH (MAKE-STATE (BIND TH (MAKE-THREAD (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP-FRAME TH S)))) (PUSH (+ -1 (TOP (STACK (TOP-FRAME TH S)))) (PUSH (TOP (STACK (TOP-FRAME TH S))) NIL)) (METHOD-PROGRAM '("fact" (INT) NIL (ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN))) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CALL-STACK TH S)))) (LOCALS (TOP (CALL-STACK TH S))) (POP (STACK (TOP (CALL-STACK TH S)))) (PROGRAM (TOP (CALL-STACK TH S))) (SYNC-FLG (TOP (CALL-STACK TH S))) (CUR-CLASS (TOP (CALL-STACK TH S)))) (POP (CALL-STACK TH S)))) 'SCHEDULED (RREF TH S)) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S))) (RREF TH (MAKE-STATE (BIND TH (MAKE-THREAD (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP-FRAME TH S)))) (PUSH (+ -1 (TOP (STACK (TOP-FRAME TH S)))) (PUSH (TOP (STACK (TOP-FRAME TH S))) NIL)) (METHOD-PROGRAM '("fact" (INT) NIL (ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN))) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CALL-STACK TH S)))) (LOCALS (TOP (CALL-STACK TH S))) (POP (STACK (TOP (CALL-STACK TH S)))) (PROGRAM (TOP (CALL-STACK TH S))) (SYNC-FLG (TOP (CALL-STACK TH S))) (CUR-CLASS (TOP (CALL-STACK TH S)))) (POP (CALL-STACK TH S)))) 'SCHEDULED (RREF TH S)) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S)))) (THREAD-TABLE (MAKE-STATE (BIND TH (MAKE-THREAD (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP-FRAME TH S)))) (PUSH (+ -1 (TOP (STACK (TOP-FRAME TH S)))) (PUSH (TOP (STACK (TOP-FRAME TH S))) NIL)) (METHOD-PROGRAM '("fact" (INT) NIL (ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN))) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CALL-STACK TH S)))) (LOCALS (TOP (CALL-STACK TH S))) (POP (STACK (TOP (CALL-STACK TH S)))) (PROGRAM (TOP (CALL-STACK TH S))) (SYNC-FLG (TOP (CALL-STACK TH S))) (CUR-CLASS (TOP (CALL-STACK TH S)))) (POP (CALL-STACK TH S)))) 'SCHEDULED (RREF TH S)) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S)))) (HEAP (MAKE-STATE (BIND TH (MAKE-THREAD (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP-FRAME TH S)))) (PUSH (+ -1 (TOP (STACK (TOP-FRAME TH S)))) (PUSH (TOP (STACK (TOP-FRAME TH S))) NIL)) (METHOD-PROGRAM '("fact" (INT) NIL (ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN))) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CALL-STACK TH S)))) (LOCALS (TOP (CALL-STACK TH S))) (POP (STACK (TOP (CALL-STACK TH S)))) (PROGRAM (TOP (CALL-STACK TH S))) (SYNC-FLG (TOP (CALL-STACK TH S))) (CUR-CLASS (TOP (CALL-STACK TH S)))) (POP (CALL-STACK TH S)))) 'SCHEDULED (RREF TH S)) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S))) (CLASS-TABLE (MAKE-STATE (BIND TH (MAKE-THREAD (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP-FRAME TH S)))) (PUSH (+ -1 (TOP (STACK (TOP-FRAME TH S)))) (PUSH (TOP (STACK (TOP-FRAME TH S))) NIL)) (METHOD-PROGRAM '("fact" (INT) NIL (ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN))) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CALL-STACK TH S)))) (LOCALS (TOP (CALL-STACK TH S))) (POP (STACK (TOP (CALL-STACK TH S)))) (PROGRAM (TOP (CALL-STACK TH S))) (SYNC-FLG (TOP (CALL-STACK TH S))) (CUR-CLASS (TOP (CALL-STACK TH S)))) (POP (CALL-STACK TH S)))) 'SCHEDULED (RREF TH S)) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S))))))) (IMPLIES (POISED-TO-INVOKE-FACT TH S N) (EQUAL (RUN (FACT-SCHED TH N) S) (MAKE-STATE (BIND TH (MAKE-THREAD (PUSH (MAKE-FRAME (+ 3 (PC (TOP-FRAME TH S))) (LOCALS (TOP-FRAME TH S)) (PUSH (INT-FIX (! N)) (POP (STACK (TOP-FRAME TH S)))) (PROGRAM (TOP-FRAME TH S)) (SYNC-FLG (TOP-FRAME TH S)) (CUR-CLASS (TOP-FRAME TH S))) (POP (CALL-STACK TH S))) (STATUS TH S) (RREF TH S)) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S))))). By the simple :definitions BINDING, CALL-STACK, MAKE-THREAD, POISED-TO-INVOKE-FACT, RREF, STATUS and TOP-FRAME, the :executable-counterpart of METHOD-PROGRAM and the simple :rewrite rules BIND-BIND, NTH-OPENER and STATES we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (NOT (ZP N)) (IMPLIES (POISED-TO-INVOKE-FACT TH (MAKE-STATE (BIND TH (LIST (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (+ -1 (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) NIL)) '((ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN)) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (LOCALS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (POP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (PROGRAM (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (SYNC-FLG (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (CUR-CLASS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) 'SCHEDULED (NTH 2 (CDR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S)) (+ -1 N)) (EQUAL (RUN (FACT-SCHED TH (+ -1 N)) (MAKE-STATE (BIND TH (LIST (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (+ -1 (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) NIL)) '((ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN)) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (LOCALS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (POP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (PROGRAM (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (SYNC-FLG (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (CUR-CLASS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) 'SCHEDULED (NTH 2 (CDR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S))) (MAKE-STATE (BIND TH (LIST (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CADR (ASSOC-EQUAL TH (BIND TH (LIST (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (+ -1 (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) NIL)) '((ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN)) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (LOCALS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (POP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (PROGRAM (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (SYNC-FLG (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (CUR-CLASS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) 'SCHEDULED (NTH 2 (CDR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (THREAD-TABLE S))))))) (LOCALS (TOP (CADR (ASSOC-EQUAL TH (BIND TH (LIST (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (+ -1 (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) NIL)) '((ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN)) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (LOCALS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (POP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (PROGRAM (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (SYNC-FLG (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (CUR-CLASS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) 'SCHEDULED (NTH 2 (CDR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (THREAD-TABLE S)))))) (PUSH (INT-FIX (! (+ -1 N))) (POP (STACK (TOP (CADR (ASSOC-EQUAL TH (BIND TH (LIST (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (+ -1 (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) NIL)) '((ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN)) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (LOCALS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (POP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (PROGRAM (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (SYNC-FLG (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (CUR-CLASS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) 'SCHEDULED (NTH 2 (CDR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (THREAD-TABLE S)))))))) (PROGRAM (TOP (CADR (ASSOC-EQUAL TH (BIND TH (LIST (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (+ -1 (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) NIL)) '((ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN)) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (LOCALS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (POP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (PROGRAM (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (SYNC-FLG (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (CUR-CLASS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) 'SCHEDULED (NTH 2 (CDR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (THREAD-TABLE S)))))) (SYNC-FLG (TOP (CADR (ASSOC-EQUAL TH (BIND TH (LIST (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (+ -1 (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) NIL)) '((ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN)) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (LOCALS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (POP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (PROGRAM (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (SYNC-FLG (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (CUR-CLASS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) 'SCHEDULED (NTH 2 (CDR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (THREAD-TABLE S)))))) (CUR-CLASS (TOP (CADR (ASSOC-EQUAL TH (BIND TH (LIST (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (+ -1 (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) NIL)) '((ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN)) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (LOCALS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (POP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (PROGRAM (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (SYNC-FLG (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (CUR-CLASS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) 'SCHEDULED (NTH 2 (CDR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (THREAD-TABLE S))))))) (POP (CADR (ASSOC-EQUAL TH (BIND TH (LIST (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (+ -1 (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) NIL)) '((ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN)) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (LOCALS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (POP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (PROGRAM (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (SYNC-FLG (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (CUR-CLASS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) 'SCHEDULED (NTH 2 (CDR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (THREAD-TABLE S)))))) (NTH 1 (CDR (ASSOC-EQUAL TH (BIND TH (LIST (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (+ -1 (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) NIL)) '((ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN)) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (LOCALS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (POP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (PROGRAM (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (SYNC-FLG (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (CUR-CLASS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) 'SCHEDULED (NTH 2 (CDR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (THREAD-TABLE S))))) (NTH 2 (CDR (ASSOC-EQUAL TH (BIND TH (LIST (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (+ -1 (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PUSH (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) NIL)) '((ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN)) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (LOCALS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (POP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (PROGRAM (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (SYNC-FLG (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (CUR-CLASS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) 'SCHEDULED (NTH 2 (CDR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (THREAD-TABLE S)))))) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S)))) (EQUAL (NTH 1 (CDR (ASSOC-EQUAL TH (THREAD-TABLE S)))) 'SCHEDULED) (EQUAL (NEXT-INST TH S) '(INVOKESTATIC "Demo" "fact" 1)) (EQUAL N (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (INTP N) (EQUAL (LOOKUP-METHOD "fact" "Demo" (CLASS-TABLE S)) '("fact" (INT) NIL (ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN)))) (EQUAL (RUN (FACT-SCHED TH N) S) (MAKE-STATE (BIND TH (LIST (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (LOCALS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (PUSH (INT-FIX (! N)) (POP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PROGRAM (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (SYNC-FLG (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (CUR-CLASS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (NTH 1 (CDR (ASSOC-EQUAL TH (THREAD-TABLE S)))) (NTH 2 (CDR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S)))). But simplification reduces this to T, using the :compound- recognizer rule ACL2::ZP-COMPOUND-RECOGNIZER, the :definitions !, BINARY-APPEND, BIND-FORMALS, BINDING, BOUND?, CALL- STACK, CLASS-DECL-HEAPREF, CLASS-DECL-METHODS, CLASS-DECL- SUPERCLASSES, DEREF, DO-INST, EXECUTE-ICONST_X, EXECUTE- IFLE, EXECUTE-ILOAD_X, EXECUTE-IMUL, EXECUTE-INVOKESTATIC, EXECUTE-IRETURN, EXECUTE-ISUB, FACT-SCHED, LOOKUP-METHOD, LOOKUP-METHOD-IN-SUPERCLASSES, MAKE-THREAD, NEXT-INST, NOT, POISED-TO-INVOKE-FACT, POPN, REPEAT, REVERSE, RREF, STATUS, SYNP and TOP-FRAME, the :executable-counterparts of ARG1, ARG2, ARG3, BINARY-+, CONSP, EQUAL, INDEX-INTO- PROGRAM, INST-LENGTH, METHOD-PROGRAM, METHOD-SYNC, NOT, OP-CODE, REVERSE, UNARY-- and ZP, primitive type reasoning, the :forward-chaining rule INT-LEMMA0, the :rewrite rules ASSOC-EQUAL-BIND, BIND-BIND, BIND-FORMALS-OPENER, CAR- CONS, CDR-CONS, COMMUTATIVITY-OF-+, FRAMES, INT-LEMMA3, INT-LEMMA4A, INT-LEMMA6, NTH-OPENER, POPN-OPENER, REPEAT- OPENER, RUN-APPEND, RUN-OPENER, STACKS, STATES, STEP-OPENER and ACL2::ZP-OPEN and the :type-prescription rules !, INTEGERP-FACTORIAL and INTP. Subgoal *1/1 (IMPLIES (ZP N) (IMPLIES (POISED-TO-INVOKE-FACT TH S N) (EQUAL (RUN (FACT-SCHED TH N) S) (MAKE-STATE (BIND TH (MAKE-THREAD (PUSH (MAKE-FRAME (+ 3 (PC (TOP-FRAME TH S))) (LOCALS (TOP-FRAME TH S)) (PUSH (INT-FIX (! N)) (POP (STACK (TOP-FRAME TH S)))) (PROGRAM (TOP-FRAME TH S)) (SYNC-FLG (TOP-FRAME TH S)) (CUR-CLASS (TOP-FRAME TH S))) (POP (CALL-STACK TH S))) (STATUS TH S) (RREF TH S)) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S))))). By the simple :definitions BINDING, CALL-STACK, MAKE-THREAD, POISED-TO-INVOKE-FACT, RREF, STATUS and TOP-FRAME and the simple :rewrite rule NTH-OPENER we reduce the conjecture to Subgoal *1/1' (IMPLIES (AND (ZP N) (EQUAL (NTH 1 (CDR (ASSOC-EQUAL TH (THREAD-TABLE S)))) 'SCHEDULED) (EQUAL (NEXT-INST TH S) '(INVOKESTATIC "Demo" "fact" 1)) (EQUAL N (TOP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (INTP N) (EQUAL (LOOKUP-METHOD "fact" "Demo" (CLASS-TABLE S)) '("fact" (INT) NIL (ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN)))) (EQUAL (RUN (FACT-SCHED TH N) S) (MAKE-STATE (BIND TH (LIST (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (LOCALS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (PUSH (INT-FIX (! N)) (POP (STACK (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))) (PROGRAM (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (SYNC-FLG (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (CUR-CLASS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))) (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (NTH 1 (CDR (ASSOC-EQUAL TH (THREAD-TABLE S)))) (NTH 2 (CDR (ASSOC-EQUAL TH (THREAD-TABLE S))))) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S)))). But simplification reduces this to T, using the :compound- recognizer rule ACL2::ZP-COMPOUND-RECOGNIZER, the :definitions !, BINARY-APPEND, BIND-FORMALS, BINDING, BOUND?, CALL- STACK, CLASS-DECL-HEAPREF, CLASS-DECL-METHODS, CLASS-DECL- SUPERCLASSES, DEREF, DO-INST, EXECUTE-ICONST_X, EXECUTE- IFLE, EXECUTE-ILOAD_X, EXECUTE-INVOKESTATIC, EXECUTE-IRETURN, FACT-SCHED, LOOKUP-METHOD, LOOKUP-METHOD-IN-SUPERCLASSES, MAKE-THREAD, NEXT-INST, NOT, POPN, REPEAT, REVERSE, RREF, STATUS, SYNP and TOP-FRAME, the :executable-counterparts of ARG1, ARG2, ARG3, BINARY-+, CONSP, EQUAL, INDEX-INTO- PROGRAM, INST-LENGTH, INT-FIX, METHOD-PROGRAM, METHOD- SYNC, NOT, OP-CODE, PUSH, REVERSE, TOP and ZP, primitive type reasoning, the :forward-chaining rule INT-LEMMA0, the :rewrite rules ASSOC-EQUAL-BIND, BIND-BIND, BIND-FORMALS- OPENER, CAR-CONS, CDR-CONS, FRAMES, NTH-OPENER, POPN-OPENER, REPEAT-OPENER, RUN-OPENER, STACKS, STATES, STEP-OPENER and ACL2::ZP-OPEN and the :type-prescription rule INTP. That completes the proof of *1. Q.E.D. Summary Form: ( DEFTHM FACT-IS-CORRECT ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION !) (:DEFINITION BINARY-APPEND) (:DEFINITION BIND-FORMALS) (:DEFINITION BINDING) (:DEFINITION BOUND?) (:DEFINITION CALL-STACK) (:DEFINITION CLASS-DECL-HEAPREF) (:DEFINITION CLASS-DECL-METHODS) (:DEFINITION CLASS-DECL-SUPERCLASSES) (:DEFINITION DEREF) (:DEFINITION DO-INST) (:DEFINITION EXECUTE-ICONST_X) (:DEFINITION EXECUTE-IFLE) (:DEFINITION EXECUTE-ILOAD_X) (:DEFINITION EXECUTE-IMUL) (:DEFINITION EXECUTE-INVOKESTATIC) (:DEFINITION EXECUTE-IRETURN) (:DEFINITION EXECUTE-ISUB) (:DEFINITION FACT-SCHED) (:DEFINITION LOOKUP-METHOD) (:DEFINITION LOOKUP-METHOD-IN-SUPERCLASSES) (:DEFINITION MAKE-THREAD) (:DEFINITION NEXT-INST) (:DEFINITION NOT) (:DEFINITION POISED-TO-INVOKE-FACT) (:DEFINITION POPN) (:DEFINITION REPEAT) (:DEFINITION REVERSE) (:DEFINITION RREF) (:DEFINITION STATUS) (:DEFINITION SYNP) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART ARG1) (:EXECUTABLE-COUNTERPART ARG2) (:EXECUTABLE-COUNTERPART ARG3) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INDEX-INTO-PROGRAM) (:EXECUTABLE-COUNTERPART INST-LENGTH) (:EXECUTABLE-COUNTERPART INT-FIX) (:EXECUTABLE-COUNTERPART METHOD-PROGRAM) (:EXECUTABLE-COUNTERPART METHOD-SYNC) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART OP-CODE) (:EXECUTABLE-COUNTERPART PUSH) (:EXECUTABLE-COUNTERPART REVERSE) (:EXECUTABLE-COUNTERPART TOP) (:EXECUTABLE-COUNTERPART UNARY--) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:REWRITE ASSOC-EQUAL-BIND) (:REWRITE BIND-BIND) (:REWRITE BIND-FORMALS-OPENER) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE FRAMES) (:REWRITE INT-LEMMA3) (:REWRITE INT-LEMMA4A) (:REWRITE INT-LEMMA6) (:REWRITE NTH-OPENER) (:REWRITE POPN-OPENER) (:REWRITE REPEAT-OPENER) (:REWRITE RUN-APPEND) (:REWRITE RUN-OPENER) (:REWRITE STACKS) (:REWRITE STATES) (:REWRITE STEP-OPENER) (:REWRITE ACL2::ZP-OPEN) (:TYPE-PRESCRIPTION !) (:TYPE-PRESCRIPTION INTEGERP-FACTORIAL) (:TYPE-PRESCRIPTION INTP)) Warnings: None Time: 2.44 seconds (prove: 2.34, print: 0.09, other: 0.01) FACT-IS-CORRECT M5 >(defthm acl2-Demo-main (implies (intp n) (equal (acl2-Demo n) (int-fix (! n))))) ACL2 Warning [Non-rec] in ( DEFTHM ACL2-DEMO-MAIN ...): The :REWRITE rule generated from ACL2-DEMO-MAIN will be triggered only by terms containing the non-recursive function symbol ACL2-DEMO. Unless this function is disabled, ACL2- DEMO-MAIN is unlikely ever to be used. But simplification reduces this to T, using the :definitions ACL2-DEMO, ASSOC-EQUAL, BIND, BINDING, CALL-STACK, MAKE- THREAD, NEXT-INST, POISED-TO-INVOKE-FACT, RREF, STATUS and TOP-FRAME, the :executable-counterparts of BINARY- +, CALL-STACK, CAR, CDR, CLASS-TABLE, CONS, CONSP, CUR- CLASS, EQUAL, HEAP, INDEX-INTO-PROGRAM, LOCALS, LOOKUP- METHOD, NTH, POP, RREF, STATUS, SYNC-FLG, THREAD-TABLE and TOP-FRAME, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, FACT-IS-CORRECT, FRAMES, NTH- OPENER, STACKS and STATES and the :type-prescription rule INTP. Q.E.D. Summary Form: ( DEFTHM ACL2-DEMO-MAIN ...) Rules: ((:DEFINITION ACL2-DEMO) (:DEFINITION ASSOC-EQUAL) (:DEFINITION BIND) (:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION MAKE-THREAD) (:DEFINITION NEXT-INST) (:DEFINITION POISED-TO-INVOKE-FACT) (:DEFINITION RREF) (:DEFINITION STATUS) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CALL-STACK) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CLASS-TABLE) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART CUR-CLASS) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART HEAP) (:EXECUTABLE-COUNTERPART INDEX-INTO-PROGRAM) (:EXECUTABLE-COUNTERPART LOCALS) (:EXECUTABLE-COUNTERPART LOOKUP-METHOD) (:EXECUTABLE-COUNTERPART NTH) (:EXECUTABLE-COUNTERPART POP) (:EXECUTABLE-COUNTERPART RREF) (:EXECUTABLE-COUNTERPART STATUS) (:EXECUTABLE-COUNTERPART SYNC-FLG) (:EXECUTABLE-COUNTERPART THREAD-TABLE) (:EXECUTABLE-COUNTERPART TOP-FRAME) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE FACT-IS-CORRECT) (:REWRITE FRAMES) (:REWRITE NTH-OPENER) (:REWRITE STACKS) (:REWRITE STATES) (:TYPE-PRESCRIPTION INTP)) Warnings: Non-rec Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00) ACL2-DEMO-MAIN M5 >(quote (end of Demo 4)) (END OF DEMO 4)