;=================================================================
; 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)