(BOOT-STRAP NQTHM)
[ 0.0 0.1 0.0 ]
GROUND-ZERO
(PROVE-LEMMA APPEND-ASSOCIATIVITY
(REWRITE)
(EQUAL (APPEND (APPEND X Y) Z)
(APPEND X (APPEND Y Z))))
Call the conjecture *1.
Perhaps we can prove it by induction. Three inductions are suggested by
terms in the conjecture. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (AND (LISTP X) (p (CDR X) Y Z))
(p X Y Z))
(IMPLIES (NOT (LISTP X)) (p X Y Z))).
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT X) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme leads to two
new goals:
Case 2. (IMPLIES (AND (LISTP X)
(EQUAL (APPEND (APPEND (CDR X) Y) Z)
(APPEND (CDR X) (APPEND Y Z))))
(EQUAL (APPEND (APPEND X Y) Z)
(APPEND X (APPEND Y Z)))),
which simplifies, applying the lemmas CDR-CONS and CAR-CONS, and opening up
the definition of APPEND, to:
T.
Case 1. (IMPLIES (NOT (LISTP X))
(EQUAL (APPEND (APPEND X Y) Z)
(APPEND X (APPEND Y Z)))),
which simplifies, unfolding the function APPEND, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
APPEND-ASSOCIATIVITY
(DEFN LENGTH
(LST)
(IF (LISTP LST)
(ADD1 (LENGTH (CDR LST)))
0))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT LST) decreases according to the well-founded relation LESSP in each
recursive call. Hence, LENGTH is accepted under the principle of definition.
From the definition we can conclude that (NUMBERP (LENGTH LST)) is a theorem.
[ 0.0 0.0 0.0 ]
LENGTH
(ADD-SHELL MAKE-OP NIL OP?
((OP-TYPE (NONE-OF) ZERO)
(TID (ONE-OF NUMBERP) ZERO)))
[ 0.0 0.0 0.0 ]
MAKE-OP
(ADD-SHELL MAKE-OBJ NIL OBJ?
((LOCK-TID (ONE-OF NUMBERP FALSEP)
ZERO)
(WAITERS (NONE-OF) ZERO)))
[ 0.0 0.0 0.0 ]
MAKE-OBJ
(PROVE-LEMMA LENGTH-APPEND
(REWRITE)
(EQUAL (LENGTH (APPEND X Y))
(PLUS (LENGTH X) (LENGTH Y))))
Call the conjecture *1.
Perhaps we can prove it by induction. Three inductions are suggested by
terms in the conjecture. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (AND (LISTP X) (p (CDR X) Y))
(p X Y))
(IMPLIES (NOT (LISTP X)) (p X Y))).
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT X) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme leads to two
new goals:
Case 2. (IMPLIES (AND (LISTP X)
(EQUAL (LENGTH (APPEND (CDR X) Y))
(PLUS (LENGTH (CDR X)) (LENGTH Y))))
(EQUAL (LENGTH (APPEND X Y))
(PLUS (LENGTH X) (LENGTH Y)))),
which simplifies, applying the lemmas CDR-CONS and SUB1-ADD1, and opening up
the definitions of APPEND, LENGTH, and PLUS, to:
T.
Case 1. (IMPLIES (NOT (LISTP X))
(EQUAL (LENGTH (APPEND X Y))
(PLUS (LENGTH X) (LENGTH Y)))),
which simplifies, unfolding the functions APPEND, LENGTH, EQUAL, and PLUS,
to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
LENGTH-APPEND
(DEFN SERVER
(TRANQ X)
(LET ((CURRENT (CAR TRANQ)))
(COND ((NLISTP TRANQ) NIL)
((AND (EQUAL (OP-TYPE CURRENT) 'WRITE)
(EQUAL (TID CURRENT) (LOCK-TID X)))
(CONS CURRENT
(SERVER (APPEND (WAITERS X) (CDR TRANQ))
(MAKE-OBJ F NIL))))
((FALSEP (LOCK-TID X))
(IF (EQUAL (OP-TYPE CURRENT) 'READ)
(CONS CURRENT
(SERVER (CDR TRANQ)
(MAKE-OBJ (TID CURRENT) (WAITERS X))))
(CONS CURRENT
(SERVER (CDR TRANQ) X))))
(T (SERVER (CDR TRANQ)
(MAKE-OBJ (LOCK-TID X)
(APPEND (WAITERS X)
(LIST CURRENT)))))))
((ORD-LESSP (CONS (ADD1 (PLUS (LENGTH (WAITERS X))
(LENGTH TRANQ)))
(LENGTH TRANQ)))))
Linear arithmetic, the lemmas CAR-CONS, CDR-CONS, SUB1-ADD1, ADD1-EQUAL,
LENGTH-APPEND, and WAITERS-MAKE-OBJ, and the definitions of ORDINALP, LESSP,
ORD-LESSP, LENGTH, WAITERS, AND, NLISTP, EQUAL, and ADD1 can be used to prove
that the measure:
(CONS (ADD1 (PLUS (LENGTH (WAITERS X))
(LENGTH TRANQ)))
(LENGTH TRANQ))
decreases according to the well-founded relation ORD-LESSP in each recursive
call. Hence, SERVER is accepted under the definitional principle. Note that:
(OR (LITATOM (SERVER TRANQ X))
(LISTP (SERVER TRANQ X)))
is a theorem.
[ 0.0 0.1 0.0 ]
SERVER
(DEFN FIND-WRITE
(TID TRANQ)
(IF (LISTP TRANQ)
(OR (AND (OP? (CAR TRANQ))
(EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL TID (TID (CAR TRANQ))))
(FIND-WRITE TID (CDR TRANQ)))
F))
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT TRANQ) decreases according to the well-founded relation LESSP
in each recursive call. Hence, FIND-WRITE is accepted under the principle of
definition. Note that:
(OR (FALSEP (FIND-WRITE TID TRANQ))
(TRUEP (FIND-WRITE TID TRANQ)))
is a theorem.
[ 0.0 0.0 0.0 ]
FIND-WRITE
(DEFN REMOVE-WRITE
(TID TRANQ)
(IF (LISTP TRANQ)
(IF (AND (OP? (CAR TRANQ))
(EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL TID (TID (CAR TRANQ))))
(CDR TRANQ)
(CONS (CAR TRANQ)
(REMOVE-WRITE TID (CDR TRANQ))))
NIL))
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT TRANQ) decreases according to the well-founded relation LESSP
in each recursive call. Hence, REMOVE-WRITE is accepted under the principle
of definition.
[ 0.0 0.0 0.0 ]
REMOVE-WRITE
(PROVE-LEMMA GOOD-TRANQ-HELPER
(REWRITE)
(NOT (LESSP (LENGTH TRANQ)
(LENGTH (REMOVE-WRITE TID TRANQ)))))
WARNING: Note that the proposed lemma GOOD-TRANQ-HELPER is to be stored as
zero type prescription rules, zero compound recognizer rules, one linear rule,
and zero replacement rules.
Give the conjecture the name *1.
Let us appeal to the induction principle. Two inductions are suggested
by terms in the conjecture. However, they merge into one likely candidate
induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP TRANQ)
(AND (OP? (CAR TRANQ))
(EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL TID (TID (CAR TRANQ)))))
(p TRANQ TID))
(IMPLIES (AND (LISTP TRANQ)
(NOT (AND (OP? (CAR TRANQ))
(EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL TID (TID (CAR TRANQ)))))
(p (CDR TRANQ) TID))
(p TRANQ TID))
(IMPLIES (NOT (LISTP TRANQ))
(p TRANQ TID))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT TRANQ) decreases according to the well-founded relation LESSP in each
induction step of the scheme. The above induction scheme generates three new
conjectures:
Case 3. (IMPLIES (AND (LISTP TRANQ)
(AND (OP? (CAR TRANQ))
(EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL TID (TID (CAR TRANQ)))))
(NOT (LESSP (LENGTH TRANQ)
(LENGTH (REMOVE-WRITE TID TRANQ))))),
which simplifies, applying SUB1-ADD1, and opening up AND, LENGTH,
REMOVE-WRITE, EQUAL, and LESSP, to:
(IMPLIES (AND (LISTP TRANQ)
(OP? (CAR TRANQ))
(EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL TID (TID (CAR TRANQ)))
(NOT (EQUAL (LENGTH (CDR TRANQ)) 0)))
(NOT (LESSP (LENGTH (CDR TRANQ))
(SUB1 (LENGTH (CDR TRANQ)))))),
which again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (LISTP TRANQ)
(NOT (AND (OP? (CAR TRANQ))
(EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL TID (TID (CAR TRANQ)))))
(NOT (LESSP (LENGTH (CDR TRANQ))
(LENGTH (REMOVE-WRITE TID (CDR TRANQ))))))
(NOT (LESSP (LENGTH TRANQ)
(LENGTH (REMOVE-WRITE TID TRANQ))))),
which simplifies, applying the lemmas CDR-CONS and SUB1-ADD1, and opening up
AND, LENGTH, REMOVE-WRITE, and LESSP, to:
T.
Case 1. (IMPLIES (NOT (LISTP TRANQ))
(NOT (LESSP (LENGTH TRANQ)
(LENGTH (REMOVE-WRITE TID TRANQ))))),
which simplifies, opening up LENGTH, REMOVE-WRITE, and LESSP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
GOOD-TRANQ-HELPER
(DEFN GOOD-TRANQ
(TRANQ)
(IF (LISTP TRANQ)
(AND (OP? (CAR TRANQ))
(IF (EQUAL (OP-TYPE (CAR TRANQ)) 'READ)
(AND (FIND-WRITE (TID (CAR TRANQ))
(CDR TRANQ))
(GOOD-TRANQ (REMOVE-WRITE (TID (CAR TRANQ))
(CDR TRANQ))))
(GOOD-TRANQ (CDR TRANQ))))
T)
((LESSP (LENGTH TRANQ))))
Linear arithmetic, the lemmas SUB1-ADD1 and GOOD-TRANQ-HELPER, and the
definitions of LESSP and LENGTH establish that the measure (LENGTH TRANQ)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, GOOD-TRANQ is accepted under the principle of definition. From the
definition we can conclude that:
(OR (FALSEP (GOOD-TRANQ TRANQ))
(TRUEP (GOOD-TRANQ TRANQ)))
is a theorem.
[ 0.0 0.0 0.0 ]
GOOD-TRANQ
(DEFN GOOD-TRACE
(TRACE TID)
(IF (LISTP TRACE)
(AND (OP? (CAR TRACE))
(IF TID
(CASE (OP-TYPE (CAR TRACE))
(READ F)
(WRITE (AND (EQUAL (TID (CAR TRACE)) TID)
(GOOD-TRACE (CDR TRACE) F)))
(OTHERWISE (GOOD-TRACE (CDR TRACE) TID)))
(CASE (OP-TYPE (CAR TRACE))
(READ (GOOD-TRACE (CDR TRACE)
(TID (CAR TRACE))))
(OTHERWISE (GOOD-TRACE (CDR TRACE) F)))))
(IF TID F T)))
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT TRACE) decreases according to the well-founded relation LESSP in each
recursive call. Hence, GOOD-TRACE is accepted under the definitional
principle. Note that:
(OR (FALSEP (GOOD-TRACE TRACE TID))
(TRUEP (GOOD-TRACE TRACE TID)))
is a theorem.
[ 0.0 0.0 0.0 ]
GOOD-TRACE
(DEFN GOOD-TRANQ-TID
(X Y TID)
(IF TID
(AND (FIND-WRITE TID Y)
(GOOD-TRANQ (APPEND X (REMOVE-WRITE TID Y))))
(AND (EQUAL X NIL) (GOOD-TRANQ Y))))
Observe that:
(OR (FALSEP (GOOD-TRANQ-TID X Y TID))
(TRUEP (GOOD-TRANQ-TID X Y TID)))
is a theorem.
[ 0.0 0.0 0.0 ]
GOOD-TRANQ-TID
(PROVE-LEMMA SERVER-SAFETY-MAIN-LEMMA NIL
(IMPLIES (AND (OBJ? X)
(GOOD-TRANQ-TID (WAITERS X)
TRANQ
(LOCK-TID X)))
(GOOD-TRACE (SERVER TRANQ X)
(LOCK-TID X))))
This simplifies, opening up the function GOOD-TRANQ-TID, to two new goals:
Case 2. (IMPLIES (AND (OBJ? X)
(NOT (LOCK-TID X))
(EQUAL (WAITERS X) NIL)
(GOOD-TRANQ TRANQ))
(GOOD-TRACE (SERVER TRANQ X) F)).
Applying the lemma LOCK-TID-WAITERS-ELIM, replace X by (MAKE-OBJ Z V) to
eliminate (LOCK-TID X) and (WAITERS X). This produces:
(IMPLIES (AND (NOT Z)
(EQUAL V NIL)
(GOOD-TRANQ TRANQ))
(GOOD-TRACE (SERVER TRANQ (MAKE-OBJ Z V))
F)),
which further simplifies, trivially, to:
(IMPLIES (GOOD-TRANQ TRANQ)
(GOOD-TRACE (SERVER TRANQ (MAKE-OBJ F NIL))
F)),
which we would normally push and work on later by induction. But if we must
use induction to prove the input conjecture, we prefer to induct on the
original formulation of the problem. Thus we will disregard all that we
have previously done, give the name *1 to the original input, and work on it.
So now let us return to:
(IMPLIES (AND (OBJ? X)
(GOOD-TRANQ-TID (WAITERS X)
TRANQ
(LOCK-TID X)))
(GOOD-TRACE (SERVER TRANQ X)
(LOCK-TID X))),
named *1. Let us appeal to the induction principle. There is only one
suggested induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP TRANQ) (p TRANQ X))
(IMPLIES (AND (NOT (NLISTP TRANQ))
(AND (EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL (TID (CAR TRANQ))
(LOCK-TID X)))
(p (APPEND (WAITERS X) (CDR TRANQ))
(MAKE-OBJ F NIL)))
(p TRANQ X))
(IMPLIES (AND (NOT (NLISTP TRANQ))
(NOT (AND (EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL (TID (CAR TRANQ))
(LOCK-TID X))))
(FALSEP (LOCK-TID X))
(EQUAL (OP-TYPE (CAR TRANQ)) 'READ)
(p (CDR TRANQ)
(MAKE-OBJ (TID (CAR TRANQ))
(WAITERS X))))
(p TRANQ X))
(IMPLIES (AND (NOT (NLISTP TRANQ))
(NOT (AND (EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL (TID (CAR TRANQ))
(LOCK-TID X))))
(FALSEP (LOCK-TID X))
(NOT (EQUAL (OP-TYPE (CAR TRANQ)) 'READ))
(p (CDR TRANQ) X))
(p TRANQ X))
(IMPLIES (AND (NOT (NLISTP TRANQ))
(NOT (AND (EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL (TID (CAR TRANQ))
(LOCK-TID X))))
(NOT (FALSEP (LOCK-TID X)))
(p (CDR TRANQ)
(MAKE-OBJ (LOCK-TID X)
(APPEND (WAITERS X)
(LIST (CAR TRANQ))))))
(p TRANQ X))).
Linear arithmetic, the lemmas CAR-CONS, CDR-CONS, SUB1-ADD1, ADD1-EQUAL,
LENGTH-APPEND, and WAITERS-MAKE-OBJ, and the definitions of ORDINALP, LESSP,
ORD-LESSP, LENGTH, WAITERS, AND, NLISTP, EQUAL, and ADD1 inform us that the
measure:
(CONS (ADD1 (PLUS (LENGTH (WAITERS X))
(LENGTH TRANQ)))
(LENGTH TRANQ))
decreases according to the well-founded relation ORD-LESSP in each induction
step of the scheme. The above induction scheme leads to nine new conjectures:
Case 9. (IMPLIES (AND (NLISTP TRANQ)
(OBJ? X)
(GOOD-TRANQ-TID (WAITERS X)
TRANQ
(LOCK-TID X)))
(GOOD-TRACE (SERVER TRANQ X)
(LOCK-TID X))),
which simplifies, unfolding NLISTP, GOOD-TRANQ, FIND-WRITE, GOOD-TRANQ-TID,
SERVER, and GOOD-TRACE, to:
T.
Case 8. (IMPLIES (AND (NOT (NLISTP TRANQ))
(AND (EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL (TID (CAR TRANQ))
(LOCK-TID X)))
(NOT (GOOD-TRANQ-TID (WAITERS (MAKE-OBJ F NIL))
(APPEND (WAITERS X) (CDR TRANQ))
(LOCK-TID (MAKE-OBJ F NIL))))
(OBJ? X)
(GOOD-TRANQ-TID (WAITERS X)
TRANQ
(LOCK-TID X)))
(GOOD-TRACE (SERVER TRANQ X)
(LOCK-TID X))),
which simplifies, rewriting with the lemma OP-TYPE-NOP?, and opening up the
definitions of NLISTP, AND, WAITERS, LOCK-TID, EQUAL, GOOD-TRANQ-TID,
REMOVE-WRITE, FIND-WRITE, and SERVER, to:
(IMPLIES (AND (LISTP TRANQ)
(EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL (TID (CAR TRANQ)) (LOCK-TID X))
(NOT (GOOD-TRANQ (APPEND (WAITERS X) (CDR TRANQ))))
(OBJ? X)
(NOT (OP? (CAR TRANQ)))
(FIND-WRITE (LOCK-TID X) (CDR TRANQ))
(GOOD-TRANQ (APPEND (WAITERS X)
(CONS (CAR TRANQ)
(REMOVE-WRITE (LOCK-TID X)
(CDR TRANQ))))))
(GOOD-TRACE (SERVER (CDR TRANQ)
(MAKE-OBJ (LOCK-TID X)
(APPEND (WAITERS X)
(LIST (CAR TRANQ)))))
(LOCK-TID X))).
But this again simplifies, applying OP-TYPE-NOP?, and expanding the function
EQUAL, to:
T.
Case 7. (IMPLIES (AND (NOT (NLISTP TRANQ))
(AND (EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL (TID (CAR TRANQ))
(LOCK-TID X)))
(GOOD-TRACE (SERVER (APPEND (WAITERS X) (CDR TRANQ))
(MAKE-OBJ F NIL))
(LOCK-TID (MAKE-OBJ F NIL)))
(OBJ? X)
(GOOD-TRANQ-TID (WAITERS X)
TRANQ
(LOCK-TID X)))
(GOOD-TRACE (SERVER TRANQ X)
(LOCK-TID X))).
This simplifies, applying CDR-CONS, CAR-CONS, and OP-TYPE-NOP?, and
expanding the definitions of NLISTP, AND, LOCK-TID, REMOVE-WRITE, FIND-WRITE,
EQUAL, GOOD-TRANQ-TID, SERVER, and GOOD-TRACE, to the goal:
(IMPLIES (AND (LISTP TRANQ)
(EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL (TID (CAR TRANQ)) (LOCK-TID X))
(GOOD-TRACE (SERVER (APPEND (WAITERS X) (CDR TRANQ))
(MAKE-OBJ F NIL))
F)
(OBJ? X)
(NOT (OP? (CAR TRANQ)))
(FIND-WRITE (LOCK-TID X) (CDR TRANQ))
(GOOD-TRANQ (APPEND (WAITERS X)
(CONS (CAR TRANQ)
(REMOVE-WRITE (LOCK-TID X)
(CDR TRANQ))))))
(GOOD-TRACE (SERVER (CDR TRANQ)
(MAKE-OBJ (LOCK-TID X)
(APPEND (WAITERS X)
(LIST (CAR TRANQ)))))
(LOCK-TID X))).
This again simplifies, applying OP-TYPE-NOP?, and unfolding the definition
of EQUAL, to:
T.
Case 6. (IMPLIES
(AND (NOT (NLISTP TRANQ))
(NOT (AND (EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL (TID (CAR TRANQ))
(LOCK-TID X))))
(FALSEP (LOCK-TID X))
(EQUAL (OP-TYPE (CAR TRANQ)) 'READ)
(NOT (GOOD-TRANQ-TID (WAITERS (MAKE-OBJ (TID (CAR TRANQ))
(WAITERS X)))
(CDR TRANQ)
(LOCK-TID (MAKE-OBJ (TID (CAR TRANQ))
(WAITERS X)))))
(OBJ? X)
(GOOD-TRANQ-TID (WAITERS X)
TRANQ
(LOCK-TID X)))
(GOOD-TRACE (SERVER TRANQ X)
(LOCK-TID X))).
This simplifies, rewriting with the lemmas WAITERS-MAKE-OBJ,
LOCK-TID-MAKE-OBJ, CDR-CONS, and CAR-CONS, and expanding NLISTP, EQUAL, AND,
GOOD-TRANQ-TID, GOOD-TRANQ, SERVER, FALSEP, and GOOD-TRACE, to the following
two new conjectures:
Case 6.2.
(IMPLIES
(AND (LISTP TRANQ)
(FALSEP (LOCK-TID X))
(EQUAL (OP-TYPE (CAR TRANQ)) 'READ)
(NOT (GOOD-TRANQ (APPEND (WAITERS X)
(REMOVE-WRITE (TID (CAR TRANQ))
(CDR TRANQ)))))
(OBJ? X)
(EQUAL (WAITERS X) NIL)
(GOOD-TRANQ TRANQ))
(OP? (CAR TRANQ))).
But this again simplifies, applying OP-TYPE-NOP?, and unfolding the
function EQUAL, to:
T.
Case 6.1.
(IMPLIES
(AND (LISTP TRANQ)
(FALSEP (LOCK-TID X))
(EQUAL (OP-TYPE (CAR TRANQ)) 'READ)
(NOT (GOOD-TRANQ (APPEND (WAITERS X)
(REMOVE-WRITE (TID (CAR TRANQ))
(CDR TRANQ)))))
(OBJ? X)
(EQUAL (WAITERS X) NIL)
(GOOD-TRANQ TRANQ))
(GOOD-TRACE (SERVER (CDR TRANQ)
(MAKE-OBJ (TID (CAR TRANQ))
(WAITERS X)))
(TID (CAR TRANQ)))).
However this again simplifies, opening up LISTP, APPEND, EQUAL, and
GOOD-TRANQ, to:
T.
Case 5. (IMPLIES (AND (NOT (NLISTP TRANQ))
(NOT (AND (EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL (TID (CAR TRANQ))
(LOCK-TID X))))
(FALSEP (LOCK-TID X))
(EQUAL (OP-TYPE (CAR TRANQ)) 'READ)
(GOOD-TRACE (SERVER (CDR TRANQ)
(MAKE-OBJ (TID (CAR TRANQ))
(WAITERS X)))
(LOCK-TID (MAKE-OBJ (TID (CAR TRANQ))
(WAITERS X))))
(OBJ? X)
(GOOD-TRANQ-TID (WAITERS X)
TRANQ
(LOCK-TID X)))
(GOOD-TRACE (SERVER TRANQ X)
(LOCK-TID X))),
which simplifies, applying LOCK-TID-MAKE-OBJ, CDR-CONS, and CAR-CONS, and
unfolding NLISTP, EQUAL, AND, GOOD-TRANQ-TID, SERVER, FALSEP, and GOOD-TRACE,
to:
(IMPLIES (AND (LISTP TRANQ)
(FALSEP (LOCK-TID X))
(EQUAL (OP-TYPE (CAR TRANQ)) 'READ)
(GOOD-TRACE (SERVER (CDR TRANQ)
(MAKE-OBJ (TID (CAR TRANQ))
(WAITERS X)))
(TID (CAR TRANQ)))
(OBJ? X)
(EQUAL (WAITERS X) NIL)
(GOOD-TRANQ TRANQ))
(OP? (CAR TRANQ))),
which again simplifies, applying the lemma OP-TYPE-NOP?, and opening up the
definition of EQUAL, to:
T.
Case 4. (IMPLIES (AND (NOT (NLISTP TRANQ))
(NOT (AND (EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL (TID (CAR TRANQ))
(LOCK-TID X))))
(FALSEP (LOCK-TID X))
(NOT (EQUAL (OP-TYPE (CAR TRANQ)) 'READ))
(NOT (GOOD-TRANQ-TID (WAITERS X)
(CDR TRANQ)
(LOCK-TID X)))
(OBJ? X)
(GOOD-TRANQ-TID (WAITERS X)
TRANQ
(LOCK-TID X)))
(GOOD-TRACE (SERVER TRANQ X)
(LOCK-TID X))),
which simplifies, unfolding NLISTP, AND, GOOD-TRANQ-TID, and GOOD-TRANQ, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP TRANQ))
(NOT (AND (EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL (TID (CAR TRANQ))
(LOCK-TID X))))
(FALSEP (LOCK-TID X))
(NOT (EQUAL (OP-TYPE (CAR TRANQ)) 'READ))
(GOOD-TRACE (SERVER (CDR TRANQ) X)
(LOCK-TID X))
(OBJ? X)
(GOOD-TRANQ-TID (WAITERS X)
TRANQ
(LOCK-TID X)))
(GOOD-TRACE (SERVER TRANQ X)
(LOCK-TID X))),
which simplifies, applying CDR-CONS and CAR-CONS, and opening up the
definitions of NLISTP, AND, GOOD-TRANQ, GOOD-TRANQ-TID, SERVER, FALSEP,
EQUAL, and GOOD-TRACE, to:
T.
Case 2. (IMPLIES
(AND
(NOT (NLISTP TRANQ))
(NOT (AND (EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL (TID (CAR TRANQ))
(LOCK-TID X))))
(NOT (FALSEP (LOCK-TID X)))
(NOT
(GOOD-TRANQ-TID (WAITERS (MAKE-OBJ (LOCK-TID X)
(APPEND (WAITERS X)
(LIST (CAR TRANQ)))))
(CDR TRANQ)
(LOCK-TID (MAKE-OBJ (LOCK-TID X)
(APPEND (WAITERS X)
(LIST (CAR TRANQ)))))))
(OBJ? X)
(GOOD-TRANQ-TID (WAITERS X)
TRANQ
(LOCK-TID X)))
(GOOD-TRACE (SERVER TRANQ X)
(LOCK-TID X))).
This simplifies, rewriting with WAITERS-MAKE-OBJ, LOCK-TID-MAKE-OBJ,
APPEND-ASSOCIATIVITY, CAR-CONS, and CDR-CONS, and unfolding the definitions
of NLISTP, AND, LISTP, APPEND, GOOD-TRANQ-TID, FIND-WRITE, and REMOVE-WRITE,
to:
T.
Case 1. (IMPLIES
(AND (NOT (NLISTP TRANQ))
(NOT (AND (EQUAL (OP-TYPE (CAR TRANQ)) 'WRITE)
(EQUAL (TID (CAR TRANQ))
(LOCK-TID X))))
(NOT (FALSEP (LOCK-TID X)))
(GOOD-TRACE (SERVER (CDR TRANQ)
(MAKE-OBJ (LOCK-TID X)
(APPEND (WAITERS X)
(LIST (CAR TRANQ)))))
(LOCK-TID (MAKE-OBJ (LOCK-TID X)
(APPEND (WAITERS X)
(LIST (CAR TRANQ))))))
(OBJ? X)
(GOOD-TRANQ-TID (WAITERS X)
TRANQ
(LOCK-TID X)))
(GOOD-TRACE (SERVER TRANQ X)
(LOCK-TID X))),
which simplifies, appealing to the lemma LOCK-TID-MAKE-OBJ, and expanding
NLISTP, AND, REMOVE-WRITE, FIND-WRITE, GOOD-TRANQ-TID, and SERVER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.1 ]
SERVER-SAFETY-MAIN-LEMMA
(PROVE-LEMMA SERVER-SAFETY
(REWRITE)
(IMPLIES (GOOD-TRANQ TRANQ)
(GOOD-TRACE (SERVER TRANQ (MAKE-OBJ F NIL))
F))
((USE (SERVER-SAFETY-MAIN-LEMMA (X (MAKE-OBJ F NIL))))))
This formula can be simplified, using the abbreviations IMPLIES and
WAITERS-MAKE-OBJ, to:
(IMPLIES (AND (IMPLIES (AND (OBJ? (MAKE-OBJ F NIL))
(GOOD-TRANQ-TID NIL TRANQ
(LOCK-TID (MAKE-OBJ F NIL))))
(GOOD-TRACE (SERVER TRANQ (MAKE-OBJ F NIL))
(LOCK-TID (MAKE-OBJ F NIL))))
(GOOD-TRANQ TRANQ))
(GOOD-TRACE (SERVER TRANQ (MAKE-OBJ F NIL))
F)),
which simplifies, expanding the functions OBJ?, LOCK-TID, EQUAL,
GOOD-TRANQ-TID, AND, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
SERVER-SAFETY