#| Specification of a serializable database interface
Wim H. Hesselink, January 9, 2003. Version April 29, 2003

See whh282: 
Eternity Variables to Specify and Prove a Serializable Database. 

Dept. of Computing Science | phone +31 50 3633933
University of Groningen    |    or +31 50 3633939
P.O.Box 800                | fax   +31 50 3633800
9700 AV Groningen          | email: wim@cs.rug.nl
The Netherlands            | http://www.cs.rug.nl/~wim
|#

(note-lib "newprelude")
(enable-theory gen-conc-th)

#| Part 1.  The Algorithm with Auxiliary Variables. 
The bottom value of databases is represented by 0. The system is 
described at three levels: 0, 1, 2. The behaviour xs at level 1 is 
used to construct the eternity variables etMem and etSutno (= etSno).
These variables are modelled as functions and are not included in 
the state space. The behaviour ys at level 2 is proved to project 
to xs and to satisfy the behaviour restrictions.  |#

; Copy values of keys in lis from ar to as, used in instruction 50.
(defn putassoc* (lis ar as)
    (if (nlistp lis) as
        (putassoc (car lis) (lookup (car lis) ar) 
                  (putassoc* (cdr lis) ar as) ) ) )

(prove-lemma lookup-putassoc* (rewrite)
    (equal (cdr (assoc key (putassoc* lis ar as)))
	   (if (member key lis)
	       (cdr (assoc key ar))
	     (cdr (assoc key as)) ) )
    ((enable assoc-put)) )

(defn sdi-prog () ; the main algorithm with auxiliary variables
    '( (0  (put res 'abort)
	   (put ownset 'nil)
	   (put tlist 'nil)
	   (put actor 'env)
	   (put turn 1)
	   (put pc 10) )
       (10 (if (get$ oracle)
	       ((put inv 'begin)
		(put evf (add1 (get$ oracle)))
		(put nr 0) 
		(put sysAb (false))
		(put turn 3)
		(put pc 20) )
	     (put pc 10) )
	   (put actor 'env)
	   (put oracle (nextor oracle)) )
       (15 (put evf (sub1 evf))
	   (put inv (norin evf (inv$ oracle)))
	   (put accessed (if (listp inv) (cons (car inv) accessed) accessed))
	   (put turn 3)
	   (put actor 'env)
	   (put oracle (nextor oracle))
	   (put pc 20) )
       (20 (put actor 'db)
	   (put pc (if (equal inv 'begin) 21
		     (if (listp inv) 30
		       (if (equal inv 'end) 50 40) ) )))
       (21 (put res 'begin)
	   (put mnr (etSutno  (add1 cnt) self))
	   (put val (if (zerop mnr) 0 (etMem (sub1 mnr))))
	   (put start val)
	   (put actor 'db)
	   (put turn 2)
	   (put pc 15) )
       (30 (put iob (car inv))
	   (put actor 'db)
	   (if (member iob ownset) (put pc 33)) )
       (31 (put actor 'db)
	   (if (equal (lookup iob owner) 0)
	       (put owner (putassoc iob self owner))
	       ((put sysAb (true))
		(put pc 40) ) ))
       (32 (put ownset (add-to-set iob ownset))
	   (put actor 'db)
	   (put pridb (putassoc iob (lookup iob db) pridb)) )
       (33 (put actor 'db)
	   (put res 
		(res$ (cdr inv) (lookup iob pridb) oracle))
	   (put val 
		(if (equal val 0) val
		  (putassoc iob 
			    (newval$ (cdr inv) (lookup iob pridb) oracle)
			    val ) ) )
	   (put pridb 
		(putassoc iob 
			  (newval$ (cdr inv) (lookup iob pridb) oracle) 
			  pridb) )
	   (put oracle (nextor oracle))
	   (put turn 2)
	   (put pc 15) )
       (40 (put actor 'db)
	   (put cnt (add1 cnt)) 
	   (put hiSutno (cons (cons cnt '0) hiSutno)) )
       (41 (put actor 'db)
	   (if (listp ownset)
	       ((put owner (putassoc (car ownset) 0 owner))
		(put ownset (cdr ownset))
		(put pc 41) ) ))
       (42 (put actor 'db)
	   (put accessed 'nil)
	   (put mnr 0) 
	   (put start 0)
	   (put val 0)
	   (put res 'abort)
           (put turn 1)
	   (put pc 10) )
       (50 (put actor 'db)
	   (put hiMem 
		(cons (cons (add1 gnr) 
			    (putassoc* ownset pridb (lookup gnr hiMem)) )
		      hiMem ))
	   (put gnr (add1 gnr))
	   (put nr gnr)
	   (put cnt (add1 cnt))
	   (put hiSutno (cons (cons cnt gnr) hiSutno))
	   (put tlist ownset) )
       (51 (put actor 'db)
	   (if (listp tlist)
	       ((put db 
		     (putassoc (car tlist) 
			       (lookup (car tlist) pridb) 
			       db ) )
		(put tlist (cdr tlist))
		(put pc 51) ) ))
       (52 (put actor 'db)
	   (if (listp ownset)
	       ((put owner (putassoc (car ownset) 0 owner))
		(put ownset (cdr ownset))
		(put pc 52) ) ))
       (53 (put actor 'db)
	   (put res 'end )
           (put accessed 'nil)
	   (put mnr 0) 
	   (put start 0)
	   (put val 0)
	   (put turn 1)
	   (put pc 10) ) ) )

; shared variables
(defn sdi-shared () '(db owner hiMem gnr actor) )

; shared implementation variables 
(defn db (x)         (lookup 'db (cdr x)) ) 
(defn owner (x)      (lookup 'owner (cdr x)) )
; shared specification variables
(defn gnr (x)        (lookup 'gnr (cdr x)))
; approximating ghost variable
(defn hiMem (x)      (lookup 'hiMem (cdr x)) )
; signature
(defn actor (x)      (lookup 'actor (cdr x)) )

; private variables, first the visible ones
(defn inv (q x)      (lookup 'inv (privstate q x)))
(defn res (q x)      (lookup 'res (privstate q x)))
(defn turn (q x)     (lookup 'turn (privstate q x)))
(defn accessed (q x) (lookup 'accessed (privstate q x)))
; private implementation variables
(defn iob (q x)      (lookup 'iob (privstate q x)))      
(defn pridb (q x)    (lookup 'pridb (privstate q x)))
(defn ownset (q x)   (lookup 'ownset (privstate q x)))
(defn tlist (q x)    (lookup 'tlist (privstate q x)))
(defn oracle (q x)   (lookup 'oracle (privstate q x)))
; private specification variables
(defn nr (q x)       (lookup 'nr (privstate q x)))
(defn sysAb (q x)    (lookup 'sysAb (privstate q x)))
(defn evf (q x)      (lookup 'evf (privstate q x)))
; aproximating ghost variables
(defn cnt (q x)      (lookup 'cnt (privstate q x)))
(defn hiSutno (q x)  (lookup 'hiSutno (privstate q x))) ; = hiSno
; prophetic history variables
(defn mnr (q x)      (lookup 'mnr (privstate q x)))
(defn start (q x)    (lookup 'start (privstate q x)))
(defn val (q x)      (lookup 'val (privstate q x)))

(defn level0 ()
    '(pc self inv res turn iob pridb ownset tlist db owner oracle evf) )

(defn level1 ()
    (append (level0) '(hiMem gnr cnt hiSutno)) )

(defn level2 ()
    (append (level1) '(start val accessed nr sysAb mnr actor)) )

(defn sdi-prog1 ()
    (unghost-pc (level1) (sdi-prog)) )

(prove-lemma sdi-prog1-equals (rewrite)
  (equal (sdi-prog1)
	 '(( 0 (put res 'abort)
	       (put ownset 'nil)
	       (put tlist 'nil)
	       (put turn 1)
	       (put pc 10) )
	   (10 (if (get$ oracle)
		   ((put inv 'begin)
		    (put evf (add1 (get$ oracle)))
		    (put turn 3)
		    (put pc 20) )
		 (put pc 10) )
	       (put oracle (nextor oracle)) )
	   (15 (put evf (sub1 evf))
	       (put inv (norin evf (inv$ oracle)))
	       (put turn 3)
	       (put oracle (nextor oracle))
	       (put pc 20) )
	   (20 (put pc (if (equal inv 'begin) 21
			 (if (listp inv) 30
			   (if (equal inv 'end) 50 40) ) )))
	   (21 (PUT RES 'BEGIN)
	       (PUT TURN 2)
	       (PUT PC 15))
	   (30 (PUT IOB (CAR INV))
	       (IF (MEMBER IOB OWNSET) (PUT PC 33)))
	   (31 (IF (EQUAL (LOOKUP IOB OWNER) 0)
		   (PUT OWNER (PUTASSOC IOB SELF OWNER))
		   (PUT PC 40)))
	   (32 (PUT OWNSET (ADD-TO-SET IOB OWNSET))
	       (PUT PRIDB (PUTASSOC IOB (LOOKUP IOB DB) PRIDB)))
	   (33 (PUT RES
		    (RES$ (CDR INV) (LOOKUP IOB PRIDB) ORACLE))
	       (PUT PRIDB
		    (PUTASSOC IOB
			      (NEWVAL$ (CDR INV)
				       (LOOKUP IOB PRIDB)
				       ORACLE)
			      PRIDB))
	       (PUT ORACLE (NEXTOR ORACLE))
	       (PUT TURN 2)
	       (PUT PC 15))
	   (40 (PUT CNT (ADD1 CNT))
	       (PUT HISUTNO (CONS (CONS CNT '0) HISUTNO)) )
	   (41 (IF (LISTP OWNSET)
		   ((PUT OWNER (PUTASSOC (CAR OWNSET) 0 OWNER))
		    (PUT OWNSET (CDR OWNSET))
		    (PUT PC 41))))
	   (42 (PUT RES 'ABORT)
	       (PUT TURN 1)
	       (PUT PC 10))
	   (50 (PUT HIMEM
		    (CONS (CONS (ADD1 GNR)
				(PUTASSOC* OWNSET PRIDB (LOOKUP GNR HIMEM)))
			  HIMEM))
	       (PUT GNR (ADD1 GNR))
	       (PUT CNT (ADD1 CNT))
	       (PUT HISUTNO (CONS (CONS CNT GNR) HISUTNO))
	       (PUT TLIST OWNSET))
	   (51 (IF (LISTP TLIST)
		   ((PUT DB
			 (PUTASSOC (CAR TLIST)
				   (LOOKUP (CAR TLIST) PRIDB)
				   DB))
		    (PUT TLIST (CDR TLIST))
		    (PUT PC 51))))
	   (52 (IF (LISTP OWNSET)
		   ((PUT OWNER (PUTASSOC (CAR OWNSET) 0 OWNER))
		    (PUT OWNSET (CDR OWNSET))
		    (PUT PC 52))))
	   (53 (PUT RES 'END)
	       (PUT TURN 1)
	       (PUT PC 10) ) ) ) )

(defn sdi-prog0 ()
    (unghost-pc (level0) (sdi-prog1)) ) ; unghost is from newprelude

(dcl get$ (ora))
(dcl newval$ (a b c))
(dcl inv$ (ora))

; Normal invocations are lists or 'end or 'abort.
(defn norin (upb inv)
    (if (or (zerop upb) 
	    (not (listp inv)) )
	(if inv 'end 'abort)
      inv ) )

; Normal results differ from 'end and 'abort.
(constrain result-axiom (rewrite)
    (and (not (equal (res$ a b c) 'end))
	 (not (equal (res$ a b c) 'abort)) )
    ((res$ (lambda (a b c) 1))) )

(defn applym (fun args)
    (case fun
	  (get$ (get$ (car args)))
	  (newval$ (newval$ (car args) (cadr args) (caddr args)))
	  (inv$ (inv$ (car args)))
	  (res$ (res$ (car args) (cadr args) (caddr args)))
	  (otherwise (apply$ fun args)) ) )

(defn evalm (flag x a)
    (if (equal flag 'list)
	(if (nlistp x) nil
	  (cons (evalm t (car x) a)
		(evalm 'list (cdr x) a) ) )
      (if (litatom x) (cdr (assoc x a))
          (if (nlistp x) x
	    (if (equal (car x) 'quote) (cadr x)
	      (applym (car x) (evalm 'list (cdr x) a)) ) ) ) ) )

(defn exem (d q cmd x)
    (cond ((nlistp cmd) x)
          ((nlistp (car cmd))
           (case (car cmd)
                 (put (putgen d q (cadr cmd) 
                              (evalm t (caddr cmd) (view d q x))
                              x ))
                 (if (if (evalm t (cadr cmd) (view d q x))
                         (exem d q (caddr cmd) x)
                         (exem d q (cadddr cmd) x) ))
                 (otherwise x) ) )
          (t (exem d q (cdr cmd) 
                  (exem d q (car cmd) x) )) ) )

(defn exepcm (d q cmd x)
    (exem d q (cdr (assoc (pc q x) cmd))
	  (putlocal q 'pc (add1 (pc q x)) x) ) )

(functionally-instantiate exepcm-project-unghost (rewrite)
    (implies (and (pure-cmd-pc vars cmd)
		  (member 'self vars)
		  (member 'pc vars) )
	     (equal (concproject vars (exepcm d q cmd x)) 
		    (exepcm (intersection d vars) q
			   (unghost-pc vars cmd)
			   (concproject vars x) ) ) )
    exepc-project-unghost
    ((exe exem) (eval evalm) (apply applym) (exepc exepcm)) )

(defn sdi-shared0 () '(db owner))
(defn sdi-shared1 () '(db owner hiMem gnr) )

(defn step0 (p x)   
    (exepcm (sdi-shared0) p (sdi-prog0) x) )

(defn step1 (p x)   
    (exepcm (sdi-shared1) p (sdi-prog1) x) )

(prove-lemma pure-cmd-pc-level0-sdi-prog1 (rewrite)
    (pure-cmd-pc (level0) (sdi-prog1))
    ((enable pure-cmd-pc pure-cmd pure unghost-pc unghost0 unghost cleanup)
     (do-not-induct t)) ) ; [ 0.0 0.9 0.0 ]

(prove-lemma members-level0 (rewrite)
    (and (member 'self (level0))
	 (member 'pc (level0)) ) )

(prove-lemma shared-in-level0 (rewrite)
    (equal (intersection (sdi-shared1) (level0))
	   (sdi-shared0) ) 
    ((enable intersection)) )

(lemma projected-1-0 (rewrite)
    (equal (concproject (level0) (step1 q x))
	   (step0 q (concproject (level0) x)) )
    ((enable exepcm-project-unghost pure-cmd-pc pure-cmd
	     pure-cmd-pc-level0-sdi-prog1 members-level0 shared-in-level0
	     sdi-prog0 step0 step1 )
     (do-not-induct t) ) )

#| Construction of an initial state and an arbitrary behaviour.
For the case with history variables. |# 

(constrain db0-constraint (rewrite) ; initial database, must not be false
    (not (equal (db0) 0))
    ((db0 (lambda () nil))) )

(defn initstate () ; initial global state
    (cons nil
	  (list (cons 'db (db0))
		(cons 'hiMem (list (cons 0 (db0)))) ) ) )

#| (round n) is the n-th acting process/key, counting from 1.
Process q is owner of object ob iff (lookup ob (owner x)) = q. 
No process owns object ob iff (lookup ob (owner x)) = 0. Therefore, 
process 0 is not allowed. We thus forbid  (round n) = 0. 
Every process that has been scheduled once, will be scheduled 
infinitely often, though it need not leave location pc = 10.  |# 

(constrain round-robin (rewrite)
    (and (not (equal (round n) 0))
	 (equal (round (fix n)) (round n))
	 (implies (and (not (equal n 0))
		       (numberp n) )
		  (lessp n (robin n)) )
	 (numberp (robin n))
	 (equal (round (robin n)) (round n)) )
    ((round (lambda (n) 1))
     (robin (lambda (n) (if (zerop n) 0 (add1 n)))) ) )

(defn next-robin (q n)
    (cond ((zerop n) 0)
	  ((equal (round n) q) (robin n))
	  (t (next-robin q (sub1 n))) ) )

(prove-lemma round-next-robin (rewrite)
    (implies (not (equal (next-robin q n) 0))
	     (equal (round (next-robin q n)) q) ) )

(prove-lemma aux-robin (rewrite)
    (implies (equal (next-robin q n) (add1 n))
	     (equal (round (add1 n)) q) )
    ((use (round-next-robin)) (do-not-induct t)) )

(defn rr-reached (n)
    (if (zerop n) nil
      (madd-to-set (round n) (rr-reached (sub1 n))) ) )

(prove-lemma rr-reached-round-next-robin (rewrite)
    (implies (member q (rr-reached n))
	     (equal (round (next-robin q n)) q) ) )

(prove-lemma rr-reached-lessp-next-robin (rewrite)
    (implies (member q (rr-reached n))
	     (lessp n (next-robin q n)) ) )

(defn xs (n)
  (if (zerop n) (initstate)
    (step1 (round n) (xs (sub1 n))) ) )

#| Recall that Hilbert's epsilon function chooses an element that satisfies
its argument whenever that is possible. So, it satisfies the axiom 
   forall x, phi ::  phi(x)  implies  phi(eps(phi)) .
Note however that eps is a higher-order function, so in NQTHM we have to 
postulate this for every specific instance or family of related instances 
phi. |# 

(dcl eps-glob (i))

(add-axiom hilbert-global (rewrite)
    (implies (lessp i (add1 (gnr (xs n))))
	     (lessp i (add1 (gnr (xs (eps-glob i))))) ) )

(dcl eps-priv (i q))

(add-axiom hilbert-priv (rewrite)
    (implies (lessp i (add1 (cnt q (xs n))))
	     (lessp i (add1 (cnt q (xs (eps-priv i q))))) ) )

#| We analyse how hiMem, gnr, hiSutno and cnt are modified to determine 
the approximated value of the eternity variables etMem and etSutno. |#

(prove-lemma gnr-step1 (rewrite)
    (equal (gnr (step1 p x))
	   (case (pc p x)
		 (50 (add1 (gnr x)))
		 (otherwise (gnr x)) ) )
    ((do-not-induct t)) ) ; [ 0.0 7.5 0.0 ]

(prove-lemma hiMem-step1 (rewrite)
    (equal (hiMem (step1 p x))
	   (case (pc p x)
		 (50 (cons 
		      (cons (add1 (gnr x))
			    (putassoc* (ownset p x)
				       (pridb p x)
				       (lookup (gnr x) 
					       (hiMem x) ) ) )
		      (hiMem x) ))
		 (otherwise (hiMem x)) ) )
    ((do-not-induct t)) ) ; [ 0.0 7.9 0.1 ]

(prove-lemma cnt-step1 (rewrite)
    (equal (cnt q (step1 p x))
	   (if (and (member (pc p x) '(40 50))
                    (equal p q) )
	       (add1 (cnt q x))
	     (cnt q x) ) )
    ((do-not-induct t)) ) ; [ 0.0 9.4 0.1 ]

(prove-lemma hiSutno-step1 (rewrite)
    (equal (hiSutno q (step1 p x))
	   (if (and (member (pc p x) '(40 50))
		    (equal p q) )
	       (cons (cons (add1 (cnt p x))
			   (if (equal (pc p x) 50) (add1 (gnr x)) 0) )
		     (hiSutno p x) )
	     (hiSutno q x) ) )
    ((do-not-induct t)) ) ; [ 0.0 9.7 0.1 ]

(lemma hiMem-remains-constant (rewrite)
    (implies (and (lessp i (add1 (gnr (xs n))))
		  (not (lessp m n)) )
	     (and (lessp i (add1 (gnr (xs m))))
		  (equal (lookup i (hiMem (xs n)))
			 (lookup i (hiMem (xs m))) ) ) ) 
    ((induct (xs m)) (do-not-induct t)
     (enable xs gnr-step1 hiMem-step1 lookup) ) ) ; [ 0.0 0.2 0.1 ]

(lemma hiMem-remains-constant-sym (rewrite)
    (implies (and (lessp i (add1 (gnr (xs n))))
		  (lessp i (add1 (gnr (xs m)))) )
	     (equal (lookup i (hiMem (xs n)))
		    (lookup i (hiMem (xs m))) ) )
    ((use (hiMem-remains-constant) 
	  (hiMem-remains-constant (n m) (m n)) )
     (do-not-induct t)) )

(defn etMem (i) 
    (lookup i (hiMem (xs (eps-glob i)))) )

(defn rq0 (i x) 
    (implies (lessp i (add1 (gnr x)))
	     (equal (lookup i (hiMem x))
		    (etMem i) ) ) )

(lemma behaviour-restriction-rq0 (rewrite)
    (rq0 i (xs n))
    ((enable etMem rq0)
     (use (hiMem-remains-constant-sym (m (eps-glob i)))
	  (hilbert-global) )
     (do-not-induct t) ) )

(lemma hiSutno-remains-constant (rewrite)
    (implies (and (lessp i (add1 (cnt q (xs n))))
		  (not (lessp m n)) )
	     (and (lessp i (add1 (cnt q (xs m))))
		  (equal (lookup i (hiSutno q (xs n)))
			 (lookup i (hiSutno q (xs m))) ) ) ) 
    ((induct (xs m)) (do-not-induct t)
     (enable hiSutno-step1 cnt-step1 xs lookup) ) ) ; [ 0.0 0.2 0.0 ]

(lemma hiSutno-remains-constant-sym (rewrite)
    (implies (and (lessp i (add1 (cnt q (xs n))))
		  (lessp i (add1 (cnt q (xs m)))) )
	     (equal (lookup i (hiSutno q (xs n)))
		    (lookup i (hiSutno q (xs m))) ) )
    ((use (hiSutno-remains-constant) 
	  (hiSutno-remains-constant (n m) (m n)) )
     (do-not-induct t)) ) 

(defn etSutno (i q) 
    (lookup i (hiSutno q (xs (eps-priv i q)))) )

(defn rq1 (i q x) 
    (implies (lessp i (add1 (cnt q x)))
	     (equal (lookup i (hiSutno q x))
		    (etSutno i q) ) ) )

(lemma behaviour-restriction-rq1 (rewrite)
    (rq1 i q (xs n))
    ((enable rq1 etSutno)
     (use (hiSutno-remains-constant-sym (m (eps-priv i q)))
	  (hilbert-priv) )
     (do-not-induct t) ) )

#| We now form the history extension K3 of the eternity extension K2.
We first extend applym with the new functions etMem and etSutno. |#

(constrain objects-axiom (rewrite)
    (obj-condition iv oval
		   (newval$ iv oval ora)
		   (res$ iv oval ora) ) 
    ((obj-condition (lambda (iv oval ovaln res) t))) )

(defn delete (a xs)
    (cond ((nlistp xs) xs)
	  ((equal a (car xs)) (delete a (cdr xs)))
	  (t (cons (car xs) (delete a (cdr xs)))) ) )

(lemma member-delete (rewrite)
    (equal (member y (delete a xs))
	   (and (not (equal y a))
		(member y xs) ) ) 
    ((enable delete)) )

(defn except-lookup (key xs ys)
    (eqlis-lookup (delete key (append (strip-cars xs) (strip-cars ys)))
		  xs ys) )

(lemma lookup-outside-again (rewrite)
    (implies (not (member ob (strip-cars db)))
	     (equal (lookup ob db) 0) )
    ((enable subset-reflexive)
     (use (lookup-outside-subdomain (os (strip-cars db))))
     (do-not-induct t) ) )

(lemma member-append (rewrite)
    (equal (member x (append xs ys))
	   (or (member x xs) (member x ys)) ) )

(lemma except-lookup-all (rewrite)
    (implies (and (except-lookup key db0 db1)
		  (not (equal key ob)) )
	     (equal (lookup ob db0) (lookup ob db1)) ) 
    ((enable except-lookup member-append lookup-outside-again member-delete)
     (use (lookup-inside-subdomain 
	   (os (delete key (append (strip-cars db0) (strip-cars db1)))) ))
     (do-not-induct t) ) )

(lemma eqlis-lookup-putassoc (rewrite)
    (implies (not (member key lis))
	     (eqlis-lookup lis db (putassoc key val db)) ) 
    ((enable assoc-put lookup eqlis-lookup)) )

(lemma except-lookup-putassoc (rewrite)
    (except-lookup key db (putassoc key val db))
    ((enable eqlis-lookup-putassoc except-lookup member-delete)
     (do-not-induct t) ) )

(defn db-condition (inv val valn res)
    (if (not (equal val 0))
	(and (except-lookup (car inv) val valn)
	     (obj-condition (cdr inv) 
			    (lookup (car inv) val) 
			    (lookup (car inv) valn)
			    res ) )
      (equal valn 0) ) )

#| Note that apply$ cannot handle db-condition since it contains the 
   axiomatically introduced function obj-condition. |#

(defn applyn (fun args)
    (case fun
	  (etMem (etMem (car args)))
	  (etSutno (etSutno (car args) (cadr args)))
	  (get$ (get$ (car args)))
	  (newval$ (newval$ (car args) (cadr args) (caddr args)))
	  (inv$ (inv$ (car args)))
	  (res$ (res$ (car args) (cadr args) (caddr args)))
	  (obj-condition 
	   (obj-condition (car args) (cadr args) 
			  (caddr args) (cadddr args) ) )
	  (db-condition 
	   (db-condition (car args) (cadr args) 
			  (caddr args) (cadddr args) ) )
	  (otherwise (apply$ fun args)) ) )

(defn evaln (flag x a)
    (if (equal flag 'list)
	(if (nlistp x) nil
	  (cons (evaln t (car x) a)
		(evaln 'list (cdr x) a) ) )
      (if (litatom x) (cdr (assoc x a))
          (if (nlistp x) x
	    (if (equal (car x) 'quote) (cadr x)
	      (applyn (car x) (evaln 'list (cdr x) a)) ) ) ) ) )

(defn exen (d q cmd x)
    (cond ((nlistp cmd) x)
          ((nlistp (car cmd))
           (case (car cmd)
                 (put (putgen d q (cadr cmd) 
                              (evaln t (caddr cmd) (view d q x))
                              x ))
                 (if (if (evaln t (cadr cmd) (view d q x))
                         (exen d q (caddr cmd) x)
                         (exen d q (cadddr cmd) x) ))
                 (otherwise x) ) )
          (t (exen d q (cdr cmd) 
                  (exen d q (car cmd) x) )) ) )

(defn exepcn (d q cmd x)
    (exen d q (cdr (assoc (pc q x) cmd))
	  (putlocal q 'pc (add1 (pc q x)) x) ) )

(functionally-instantiate exepcn-project-unghost (rewrite)
    (implies (and (pure-cmd-pc vars cmd)
		  (member 'self vars)
		  (member 'pc vars) )
	     (equal (concproject vars (exepcn d q cmd x)) 
		    (exepcn (intersection d vars) q
			    (unghost-pc vars cmd)
			    (concproject vars x) ) ) )
    exepc-project-unghost
    ((exe exen) (eval evaln) (apply applyn) (exepc exepcn)) 
    ((disable putlocal putgen view shared privstate hiMem hiSutno etMem 
	      etSutno)
     (do-not-induct t) ) ) ; [ 0.0 0.0 0.0 ]

(functionally-instantiate private-vars-exepcn (rewrite)
    (implies (not (equal p q)) 
             (equal (privstate q (exepcn d p cmd x))
                    (privstate q x) ) ) 
    private-vars-exepc
    ((exe exen) (eval evaln) (apply applyn) (exepc exepcn)) 
    ((disable putlocal putgen view shared privstate hiMem hiSutno etMem 
	      etSutno)
     (do-not-induct t) ) ) ; [ 0.0 0.0 0.0 ]

(functionally-instantiate processes-exepcn (rewrite)
    (equal (processes (exepcn d q cmd x))
	   (madd-to-set q (processes x)) )
    processes-exepc
    ((exe exen) (eval evaln) (apply applyn) (exepc exepcn)) 
    ((disable putlocal putgen view shared privstate hiMem hiSutno etMem 
	      etSutno)
     (do-not-induct t) ) ) ; [ 0.0 0.0 0.0 ]

(defn step (p x)   
    (exepcn (sdi-shared) p (sdi-prog) x) )

(defn step1n (p x)   
    (exepcn (sdi-shared1) p (sdi-prog1) x) )

(prove-lemma pure-cmd-pc-level1-sdi-prog (rewrite)
    (pure-cmd-pc (level1) (sdi-prog))
    ((do-not-induct t)) ) ; [ 0.0 0.7 0.0 ]

(prove-lemma members-level1 (rewrite)
    (and (member 'self (level1))
	 (member 'pc (level1)) ) )

(prove-lemma shared-in-level1 (rewrite)
    (equal (intersection (sdi-shared) (level1))
	   (sdi-shared1) ) )

(lemma projected-2-1n (rewrite)
    (equal (concproject (level1) (step q x))
	   (step1n q (concproject (level1) x)) )
    ((enable exepcn-project-unghost pure-cmd-pc pure-cmd
	     pure-cmd-pc-level1-sdi-prog members-level1 shared-in-level1
	     sdi-prog1 step1n step )
     (do-not-induct t) ) )

#| We prove that step1n = step1 |#

(defn free-from-fun (flag lis exp)
    (cond ((equal flag 'list) 
	   (if (nlistp exp) t
	     (and (free-from-fun t lis (car exp))
		  (free-from-fun 'list lis (cdr exp)) ) ) )
	  ((nlistp exp) t)
	  ((equal (car exp) 'quote) t)
	  (t (and (not (member (car exp) lis))
		  (free-from-fun 'list lis (cdr exp)))) ) )

(defn new-funs () '(etMem etSutno obj-condition db-condition))

(lemma evaln=evalm (rewrite)
    (implies (free-from-fun flag (new-funs) x)
	     (equal (evaln flag x a)
		    (evalm flag x a) ) )
    ((enable evalm evaln applyn applym new-funs free-from-fun)) )

(defn free-from-fun-cmd (lis cmd)
    (cond ((nlistp cmd) t)
	  ((nlistp (car cmd))
	   (case (car cmd)
		 (put (free-from-fun t lis (caddr cmd)))
		 (if (and (free-from-fun t lis (cadr cmd))
			  (free-from-fun-cmd lis (caddr cmd))
			  (free-from-fun-cmd lis (cadddr cmd)) ))
		 (otherwise t) ) )
	  (t (and (free-from-fun-cmd lis (car cmd))
		  (free-from-fun-cmd lis (cdr cmd)) )) ) )

(lemma exen=exem (rewrite)
    (implies (free-from-fun-cmd (new-funs) cmd)
	     (equal (exen d q cmd x)
		    (exem d q cmd x) ) )
    ((enable exem exen free-from-fun-cmd evaln=evalm)) )

(defn free-from-fun-cmd-pc (lis cmd)
    (if (nlistp cmd) t
      (and (free-from-fun-cmd lis (cdar cmd))
	   (free-from-fun-cmd-pc lis (cdr cmd)) ) ) )

(lemma exepcn=exepcm (rewrite)
    (implies (free-from-fun-cmd-pc (new-funs) cmd)
	     (equal (exepcn d q cmd x)
		    (exepcm d q cmd x) ) )
    ((enable exen=exem exepcm exepcn free-from-fun-cmd-pc exem exen)) )

(prove-lemma sdi-prog1-without-etMem-etSutno (rewrite)
    (free-from-fun-cmd-pc (new-funs) (sdi-prog1))
    ((do-not-induct t)) )

(lemma step1n=step1 (rewrite)
    (equal (step1n p x) (step1 p x))
    ((enable step1n step1 exepcn=exepcm sdi-prog1-without-etMem-etSutno)
     (do-not-induct t)) )

; The behaviour ys in the eternity extension K3
(defn ys (n)
    (if (zerop n) (initstate)
      (step (round n) (ys (sub1 n))) ) )

; We turn to the proofs of the behaviour restrictions for ys

(lemma init-concproject-2-1 (rewrite)
    (equal (concproject (level1) (initstate))
	   (initstate) )
    ((enable concproject level0 level1 project map2project initstate)
     (do-not-induct t) ) )

(lemma xs-projection-of-ys (rewrite)
    (equal (xs n) 
	   (concproject (level1) (ys n)) )
    ((enable xs ys init-concproject-2-1 projected-2-1n step1n=step1)) )

(lemma gnr-concproject (rewrite)
    (equal (gnr (concproject (level1) x))
	   (gnr x) )
    ((enable gnr concproject level0 level1 assoc-project lookup project)
     (do-not-induct t) ) )

(lemma hiMem-concproject (rewrite)
    (equal (hiMem (concproject (level1) x))
	   (hiMem x) )
    ((enable hiMem concproject level0 level1 assoc-project lookup project)
     (do-not-induct t) ) )

(lemma rq0-for-ys (rewrite)
    (rq0 i (ys n))
    ((use (behaviour-restriction-rq0))
     (enable rq0 xs-projection-of-ys gnr-concproject hiMem-concproject )
     (do-not-induct t) ) )

(lemma cnt-concproject (rewrite)
    (equal (cnt q (concproject (level1) x))
	   (cnt q x) )
    ((enable level1 level0 cnt concproject-private)) )

(lemma hiSutno-concproject (rewrite)
    (equal (hiSutno q (concproject (level1) x))
	   (hiSutno q x) )
    ((enable level1 level0 hiSutno concproject-private)) )

(lemma rq1-for-ys (rewrite)
    (rq1 i q (ys n))
    ((use (behaviour-restriction-rq1))
     (enable rq1 xs-projection-of-ys cnt-concproject hiSutno-concproject )
     (do-not-induct t) ) )

#| Part 2. The semantic lemmas for sdi-prog |#

(disable-theory t) 
(enable-theory ground-zero)
(enable-theory gen-conc-th) 

(enable-theory 
 (db owner oracle hiMem accessed gnr inv res turn iob pridb ownset tlist nr 
     sysAb evf cnt hiSutno mnr start val step exepcn exen evaln 
     applyn applym sdi-shared sdi-prog private-vars-exepcn ) )

(defn new-pc (q x)
    (if (member (pc q x) '(0 42 53)) 10
      (if (member (pc q x) '(21 33)) 15
	(case (pc q x)
	      (10 (if (get$ (oracle q x)) 20 10))
	      (15 20)
	      (20 (if (listp (inv q x)) 30
		    (case (inv q x)
			  (begin 21)
			  (end 50)
			  (otherwise 40) ) ))
	      (30 (if (member (car (inv q x))
			      (ownset q x) )
		      33 31 ))
	      (31 (if (equal (lookup (iob q x) (owner x)) 0)
		      32 40 ))
	      (41 (if (listp (ownset q x)) 41 42))
	      (51 (if (listp (tlist q x)) 51 52))
	      (52 (if (listp (ownset q x)) 52 53))
	      (otherwise (add1 (pc q x))) ) ) ) )

(prove-lemma pc-step-eq (rewrite)
    (equal (pc p (step p x))
           (new-pc p x) ) 
    ((do-not-induct t)) ) ; [ 0.0 20.4 0.1 ]

(lemma pc-step-dif (rewrite)
    (implies (not (equal p q))
             (equal (pc q (step p x))
                    (pc q x) ) )
    ((enable step private-vars-exepcn pc)
     (do-not-induct t)) ) ; [ 0.0 0.0 0.0 ]

(lemma pc-step (rewrite)
    (equal (pc q (step p x))
           (if (equal p q) (new-pc p x) 
               (pc q x) ) )
    ((enable pc-step-eq) (use (pc-step-dif))
     (do-not-induct t)) ) ; [ 0.0 0.0 0.0 ]

(prove-lemma inv-step-eq (rewrite)
    (equal (inv p (step p x))
	   (case (pc p x) 
		 (10 (if (get$ (oracle p x)) 'begin (inv p x)))
		 (15 (norin (sub1 (evf p x)) (inv$ (oracle p x)))) 
		 (otherwise (inv p x)) ) )
    ((do-not-induct t)) ) ; [ 0.0 15.4 0.1 ]

(lemma inv-step-dif (rewrite)
    (implies (not (equal p q))
             (equal (inv q (step p x))
                    (inv q x) ) )
    ((enable step private-vars-exepcn inv)
     (do-not-induct t)) ) ; [ 0.0 0.0 0.0 ]

(lemma inv-step (rewrite)
    (equal (inv q (step p x))
	   (if (equal p q) 
	       (case (pc p x) 
		     (10 (if (get$ (oracle p x)) 'begin (inv p x)))
		     (15 (norin (sub1 (evf p x)) (inv$ (oracle p x)))) 
		     (otherwise (inv p x)) ) 
	     (inv q x) ) )
    ((use (inv-step-dif)) (enable inv-step-eq)
     (do-not-induct t)) ) ; 

(prove-lemma evf-step-eq (rewrite)
    (equal (evf p (step p x))
	   (case (pc p x)
		 (10 (if (get$ (oracle p x)) 
			 (add1 (get$ (oracle p x)) )
		       (evf p x) ))
		 (15 (sub1 (evf p x)))
		 (otherwise (evf p x)) ) )
    ((do-not-induct t)) ) ; [ 0.0 15.4 0.1 ]

(lemma evf-step-dif (rewrite)
    (implies (not (equal p q))
             (equal (evf q (step p x))
                    (evf q x) ) )
    ((enable step private-vars-exepcn evf)
     (do-not-induct t)) ) ; [ 0.0 0.0 0.0 ]

(lemma evf-step (rewrite)
    (equal (evf q (step p x))
	   (if (equal p q)
	       (case (pc p x) 
		     (10 (if (get$ (oracle p x)) 
			     (add1 (get$ (oracle p x)) )
			   (evf p x) ))
		     (15 (sub1 (evf p x)))
		     (otherwise (evf p x)) )
	     (evf q x) ) )
    ((use (evf-step-dif)) (enable evf-step-eq)
     (do-not-induct t)) ) ; 

(prove-lemma start-step-eq (rewrite)
    (equal (start p (step p x))
	   (case (pc p x)
		 (21 (let ((mnr (etSutno (add1 (cnt p x)) p) ))
		       (if (zerop mnr) 0
			 (etMem (sub1 mnr)) ) ))
		 (42 0) 
		 (53 0)
		 (otherwise (start p x)) ) )
    ((do-not-induct t)) ) ; [ 0.0 19.1 0.1 ]

(lemma start-step-dif (rewrite)
    (implies (not (equal p q))
             (equal (start q (step p x))
                    (start q x) ) )
    ((enable step private-vars-exepcn start)
     (do-not-induct t)) ) ; [ 0.0 0.0 0.0 ]

(lemma start-step (rewrite)
    (equal (start q (step p x))
	   (if (equal p q)
	       (case (pc p x)
		     (21 (let ((mnr (etSutno (add1 (cnt p x)) p) ))
		       (if (zerop mnr) 0
			 (etMem (sub1 mnr)) ) ))
		     (42 0) 
		     (53 0)
		     (otherwise (start q x)) ) 
	     (start q x) ) )
    ((use (start-step-dif)) (enable start-step-eq)
     (do-not-induct t)) ) 

(prove-lemma cnt-step-eq (rewrite)
    (equal (cnt p (step p x))
	   (if (member (pc p x) '(40 50))
	       (add1 (cnt p x))
	     (cnt p x) ) )
    ((do-not-induct t)) ) ; [ 0.0 18.4 0.0 ]

(lemma cnt-step-dif (rewrite)
    (implies (not (equal p q))
             (equal (cnt q (step p x))
                    (cnt q x) ) )
    ((enable step private-vars-exepcn cnt)
     (do-not-induct t)) ) ; [ 0.0 0.0 0.0 ]

(lemma cnt-step (rewrite)
    (equal (cnt q (step p x))
	   (if (and (member (pc p x) '(40 50))
                    (equal p q) )
	       (add1 (cnt q x))
	     (cnt q x) ) )
    ((use (cnt-step-dif)) (enable cnt-step-eq)
     (do-not-induct t)) ) 

(prove-lemma nr-step-eq (rewrite)
    (equal (nr p (step p x))
	   (case (pc p x) 
		 (10 (if (get$ (oracle p x)) 0 (nr p x)))
		 (50 (add1 (gnr x)))
		 (otherwise (nr p x)) ) )
    ((do-not-induct t)) ) ; [ 0.0 18.5 0.1 ]

(lemma nr-step-dif (rewrite)
    (implies (not (equal p q))
             (equal (nr q (step p x))
                    (nr q x) ) )
    ((enable step private-vars-exepcn nr)
     (do-not-induct t)) ) ; [ 0.0 0.0 0.0 ]

(lemma nr-step (rewrite)
    (equal (nr q (step p x))
	   (if (equal p q) 
	       (case (pc p x) 
		     (10 (if (get$ (oracle p x)) 0 (nr p x)))
		     (50 (add1 (gnr x)))
		     (otherwise (nr q x)) )
	     (nr q x) ) )
    ((use (nr-step-dif)) (enable nr-step-eq)
     (do-not-induct t)) ) 

(prove-lemma mnr-step-eq (rewrite)
    (equal (mnr p (step p x))
	   (case (pc p x)
		 (42 0) 
		 (53 0) 
		 (21 (etSutno (add1 (cnt p x)) p))
		 (otherwise (mnr p x)) ) )
    ((do-not-induct t)) ) ; [ 0.0 18.6 0.1 ]

(lemma mnr-step-dif (rewrite)
    (implies (not (equal p q))
             (equal (mnr q (step p x))
                    (mnr q x) ) )
    ((enable step private-vars-exepcn mnr)
     (do-not-induct t)) ) ; [ 0.0 0.0 0.0 ]

(lemma mnr-step (rewrite)
    (equal (mnr q (step p x))
	   (if (equal p q)
	       (case (pc p x) 
		     (42 0) 
		     (53 0) 
		     (21 (etSutno (add1 (cnt p x)) p))
		     (otherwise (mnr p x)) )
	     (mnr q x) ) )
    ((use (mnr-step-dif)) (enable mnr-step-eq)
     (do-not-induct t)) ) 

(prove-lemma res-step-eq (rewrite)
    (equal (res p (step p x))
	   (case (pc p x)
		 (21 'begin)
		 ( 0 'abort)
		 (42 'abort)
		 (53 'end)
		 (33 (res$ (cdr (inv p x))
			   (lookup (iob p x) (pridb p x))
			   (oracle p x) ))
		 (otherwise (res p x)) ) )
    ((do-not-induct t)) ) ; [ 0.0 19.9 0.0 ]

(lemma res-step-dif (rewrite)
    (implies (not (equal p q))
             (equal (res q (step p x))
                    (res q x) ) )
    ((enable step private-vars-exepcn res)
     (do-not-induct t)) ) ; [ 0.0 0.0 0.0 ]

(lemma res-step (rewrite)
    (equal (res q (step p x))
	   (if (equal p q)
               (case (pc p x)
		     (21 'begin)
		     ( 0 'abort)
		     (42 'abort)
		     (53 'end)
		     (33 (res$ (cdr (inv p x))
			       (lookup (iob p x) (pridb p x))
			       (oracle p x) ))
		     (otherwise (res p x)) )
	       (res q x) ) )
    ((use (res-step-dif)) (enable res-step-eq)
     (do-not-induct t)) ) 

(prove-lemma tlist-step-eq (rewrite)
    (equal (tlist p (step p x))
	   (case (pc p x)
		 ( 0 nil)
		 (50 (ownset p x))
		 (51 (if (listp (tlist p x)) 
			 (cdr (tlist p x))
		       (tlist p x) ))
		 (otherwise (tlist p x)) ) )
    ((do-not-induct t)) ) ; [ 0.0 37.3 0.3 ]

(lemma tlist-step-dif (rewrite)
    (implies (not (equal p q))
             (equal (tlist q (step p x))
                    (tlist q x) ) )
    ((enable step private-vars-exepcn tlist)
     (do-not-induct t)) ) ; [ 0.0 0.0 0.0 ]

(lemma tlist-step (rewrite)
    (equal (tlist q (step p x))
	   (if (equal p q)
               (case (pc p x)
		     ( 0 nil)
		     (50 (ownset p x))
		     (51 (if (listp (tlist p x)) 
			     (cdr (tlist p x))
			     (tlist p x) ))
		     (otherwise (tlist p x)) )
	       (tlist q x) ) )
    ((use (tlist-step-dif)) (enable tlist-step-eq)
     (do-not-induct t)) ) 

(prove-lemma ownset-step-eq (rewrite)
    (equal (ownset p (step p x))
	   (case (pc p x)
		 (0 nil)
		 (32 (add-to-set (iob p x) (ownset p x)))
		 (41 (if (listp (ownset p x)) 
			 (cdr (ownset p x))
		       (ownset p x) ))
		 (52 (if (listp (ownset p x)) 
			 (cdr (ownset p x))
		       (ownset p x) ))
		 (otherwise (ownset p x)) ) )
    ((do-not-induct t)) ) ; 

(lemma ownset-step-dif (rewrite)
    (implies (not (equal p q))
             (equal (ownset q (step p x))
                    (ownset q x) ) )
    ((enable step private-vars-exepcn ownset)
     (do-not-induct t)) ) ; [ 0.0 0.0 0.0 ]

(lemma ownset-step (rewrite)
    (equal (ownset q (step p x))
	   (if (equal p q)
               (case (pc p x)
		     (0 nil)
		     (32 (add-to-set (iob p x) (ownset p x)))
		     (41 (if (listp (ownset p x)) 
			     (cdr (ownset p x))
			     (ownset p x) ))
		     (52 (if (listp (ownset p x)) 
			     (cdr (ownset p x))
			     (ownset p x) ))
		     (otherwise (ownset p x)) )
	       (ownset q x) ) )
    ((use (ownset-step-dif)) (enable ownset-step-eq)
     (do-not-induct t)) ) 

(prove-lemma hiSutno-step-eq (rewrite)
    (equal (hiSutno p (step p x))
	   (if (member (pc p x) '(40 50))
	       (cons (cons (add1 (cnt p x))
			   (if (equal (pc p x) 50) (add1 (gnr x)) 0) )
		     (hiSutno p x) )
	     (hiSutno p x) ) )
    ((do-not-induct t)) ) ; [ 0.0 19.4 0.1 ]

(lemma hiSutno-step-dif (rewrite)
    (implies (not (equal p q))
             (equal (hiSutno q (step p x))
                    (hiSutno q x) ) )
    ((enable step private-vars-exepcn hiSutno)
     (do-not-induct t)) ) ; [ 0.0 0.0 0.0 ]

(lemma hiSutno-step (rewrite)
    (equal (hiSutno q (step p x))
	   (if (and (member (pc p x) '(40 50))
		    (equal p q) )
	       (cons (cons (add1 (cnt p x))
			   (if (equal (pc p x) 50) (add1 (gnr x)) 0) )
		     (hiSutno p x) )
	     (hiSutno q x) ) )
    ((use (hiSutno-step-dif)) (enable hiSutno-step-eq)
     (do-not-induct t)) ) 

(prove-lemma sysAb-step-eq (rewrite)
    (equal (sysAb p (step p x))
	   (case (pc p x)
		 (10 (if (get$ (oracle p x)) f (sysAb p x)))
		 (31 (if (equal (lookup (iob p x) (owner x)) 0)
			 (sysAb p x)
		       t ))
		 (otherwise (sysAb p x)) ) )
    ((do-not-induct t)) ) ; [ 0.0 19.3 0.0 ]

(lemma sysAb-step-dif (rewrite)
    (implies (not (equal p q))
             (equal (sysAb q (step p x))
                    (sysAb q x) ) )
    ((enable step private-vars-exepcn sysAb)
     (do-not-induct t)) ) ; [ 0.0 0.0 0.0 ]

(lemma sysAb-step (rewrite)
    (equal (sysAb q (step p x))
	   (if (equal p q) 
	       (case (pc q x)
		     (10 (if (get$ (oracle p x)) f (sysAb p x)))
		     (31 (if (equal (lookup (iob q x) (owner x)) 0)
			     (sysAb q x)
			   t ))
		     (otherwise (sysAb q x)) )
	     (sysAb q x) ) )
    ((use (sysAb-step-dif)) (enable sysAb-step-eq)
     (do-not-induct t)) ) 

(prove-lemma iob-step-eq (rewrite)
    (equal (iob p (step p x))
	   (if (equal (pc p x) 30)
	       (car (inv p x))
	     (iob p x) ) )
    ((do-not-induct t)) ) ; [ 0.0 18.1 0.0 ]

(lemma iob-step-dif (rewrite)
    (implies (not (equal p q))
             (equal (iob q (step p x))
                    (iob q x) ) )
    ((enable step private-vars-exepcn iob)
     (do-not-induct t)) ) ; [ 0.0 0.0 0.0 ]

(lemma iob-step (rewrite)
    (equal (iob q (step p x))
	   (if (and (equal (pc p x) 30)
                    (equal p q) )
	       (car (inv p x))
	     (iob q x) ) )
    ((use (iob-step-dif)) (enable iob-step-eq)
     (do-not-induct t)) ) 

(prove-lemma pridb-step-eq (rewrite)
    (equal (pridb p (step p x))
	   (case (pc p x)
		 (32 (putassoc (iob p x)
			       (lookup (iob p x) (db x))
			       (pridb p x) ))
		 (33 (putassoc (iob p x)
			       (newval$ (cdr (inv p x))
					(lookup (iob p x) (pridb p x))
					(oracle p x) )
				   (pridb p x) ))
		 (otherwise (pridb p x)) ) )
    ((do-not-induct t)) ) ; [ 0.0 19.9 0.1 ]

(lemma pridb-step-dif (rewrite)
    (implies (not (equal p q))
             (equal (pridb q (step p x))
                    (pridb q x) ) )
    ((enable step private-vars-exepcn pridb)
     (do-not-induct t)) ) ; [ 0.0 0.0 0.0 ]

(lemma pridb-step (rewrite)
    (equal (pridb q (step p x))
	   (if (equal p q) 
	       (case (pc p x)
		     (32 (putassoc (iob p x)
				   (lookup (iob p x) (db x))
				   (pridb p x) ))
		     (33 (putassoc (iob p x)
				   (newval$ (cdr (inv p x))
					    (lookup (iob p x) (pridb p x))
					    (oracle p x) )
				   (pridb p x) ))
		     (otherwise (pridb q x)) )
	     (pridb q x) ) )
    ((use (pridb-step-dif)) (enable pridb-step-eq)
     (do-not-induct t)) ) 

(prove-lemma val-step-eq (rewrite)
    (equal (val p (step p x))
	   (case (pc p x)
		 (21 (let ((mnr (etSutno (add1 (cnt p x)) p) ))
			   (if (zerop mnr) 0
			     (etMem (sub1 mnr)) ) ))
		 (33 (if (equal (val p x) 0)
			 (val p x)
		       (putassoc (iob p x)
				 (newval$ (cdr (inv p x))
					  (lookup (iob p x) (pridb p x))
					  (oracle p x) )
				 (val p x) ) ))
		 (42 0) 
		 (53 0)
		 (otherwise (val p x)) ) )
    ((do-not-induct t)) ) ; [ 0.0 23.9 0.1 ]

(lemma val-step-dif (rewrite)
    (implies (not (equal p q))
             (equal (val q (step p x))
                    (val q x) ) )
    ((enable step private-vars-exepcn val)
     (do-not-induct t)) ) ; [ 0.0 0.0 0.0 ]

(lemma val-step (rewrite)
    (equal (val q (step p x))
	   (if (equal p q)
	       (case (pc p x)
		     (21 (let ((mnr (etSutno (add1 (cnt p x)) p) ))
			   (if (zerop mnr) 0
			     (etMem (sub1 mnr)) ) ))
		     (33 (if (equal (val p x) 0)
			     (val p x)
			   (putassoc (iob p x)
				     (newval$ (cdr (inv p x))
					      (lookup (iob p x) 
						      (pridb p x) )
					      (oracle p x) )
				     (val p x) ) ))
		     (42 0) 
		     (53 0)
		     (otherwise (val q x)) )
	     (val q x) ) )
    ((use (val-step-dif)) (enable val-step-eq)
     (do-not-induct t)) ) 

(prove-lemma accessed-step-eq (rewrite)
    (equal (accessed p (step p x))
	   (case (pc p x)
		 (15 (if (listp (norin (sub1 (evf p x))
				       (inv$ (oracle p x)) ))
			 (cons (car (norin (sub1 (evf p x))
					   (inv$ (oracle p x))))
			       (accessed p x) )
		       (accessed p x) ))
		 (42 nil)
		 (53 nil)
		 (otherwise (accessed p x)) ) )
    ((do-not-induct t)) ) ; [ 0.0 15.9 0.0 ]

(lemma accessed-step-dif (rewrite)
    (implies (not (equal p q))
             (equal (accessed q (step p x))
                    (accessed q x) ) )
    ((enable step private-vars-exepcn accessed)
     (do-not-induct t)) ) ; [ 0.0 0.0 0.0 ]

(lemma accessed-step (rewrite)
    (equal (accessed q (step p x))
	   (if (equal p q) 
	       (case (pc p x)
		     (15 (if (listp (norin (sub1 (evf p x))
				       (inv$ (oracle p x)) ))
			     (cons (car (norin (sub1 (evf p x))
					   (inv$ (oracle p x))))
				   (accessed p x) )
			   (accessed p x) ))
		     (42 nil)
		     (53 nil)
		     (otherwise (accessed p x)) )
	     (accessed q x) ) )
    ((use (accessed-step-dif)) (enable accessed-step-eq)
     (do-not-induct t)) ) 

(prove-lemma turn-step-eq (rewrite)
    (equal (turn p (step p x))
	   (case (pc p x) 
		 ( 0 1)
		 (10 (if (get$ (oracle p x)) 3 (turn p x)))
		 (15 3)
		 (21 2)
		 (33 2)
		 (42 1)
		 (53 1)
		 (otherwise (turn p x)) ) )
    ((do-not-induct t)) ) ; [ 0.0 15.9 0.0 ]

(lemma turn-step-dif (rewrite)
    (implies (not (equal p q))
             (equal (turn q (step p x))
                    (turn q x) ) )
    ((enable step private-vars-exepcn turn)
     (do-not-induct t)) ) ; [ 0.0 0.0 0.0 ]

(lemma turn-step (rewrite)
    (equal (turn q (step p x))
	   (if (equal p q) 
	       (case (pc p x) 
		     ( 0 1)
		     (10 (if (get$ (oracle p x)) 3 (turn p x)))
		     (15 3)
		     (21 2)
		     (33 2)
		     (42 1)
		     (53 1)
		     (otherwise (turn p x)) )
	     (turn q x) ) )
    ((use (turn-step-dif)) (enable turn-step-eq)
     (do-not-induct t)) ) 

; the shared variables are '(db owner hiMem gnr actor)
(prove-lemma gnr-step (rewrite)
    (equal (gnr (step p x))
	   (case (pc p x)
		 (50 (add1 (gnr x)))
		 (otherwise (gnr x)) ) )
    ((do-not-induct t)) ) ; [ 0.0 18.1 0.1 ]

(prove-lemma db-step (rewrite)
    (equal (db (step p x))
	   (case (pc p x)
		 (51 (if (listp (tlist p x))
			 (putassoc (car (tlist p x))
				   (lookup (car (tlist p x)) 
					   (pridb p x) )
				   (db x) )
		       (db x) ))
		 (otherwise (db x)) ) )
    ((do-not-induct t)) ) ; [ 0.0 37.5 0.1 ]

(prove-lemma hiMem-step (rewrite)
    (equal (hiMem (step p x))
	   (case (pc p x)
		 (50 (cons 
		      (cons (add1 (gnr x))
			    (putassoc* (ownset p x)
				       (pridb p x)
				       (lookup (gnr x) 
					       (hiMem x) ) ) )
		      (hiMem x) ))
		 (otherwise (hiMem x)) ) )
    ((do-not-induct t)) ) ; [ 0.0 18.6 0.1 ]

(prove-lemma actor-step (rewrite)
    (equal (actor (step p x))
	   (cond ((member (pc p x) '(0 10 15)) 'env)
		 ((member (pc p x) '(20 21 30 31 32 33 40 41 42 50 51 52 53))
		  'db)
		 (t (actor x)) ) )
    ((do-not-induct t) (enable actor)) ) ; [ 0.0 36.6 0.1 ]

(prove-lemma owner-step (rewrite)
    (equal (owner (step p x))
	   (case (pc p x)
		 (41 (if (listp (ownset p x))
			 (putassoc (car (ownset p x)) 0 (owner x))
		       (owner x) ))
		 (52 (if (listp (ownset p x))
			 (putassoc (car (ownset p x)) 0 (owner x))
		       (owner x) ))
		 (31 (if (equal (lookup (iob p x) (owner x)) 0) 
			 (putassoc (iob p x) p (owner x))
		       (owner x) ))
		 (otherwise (owner x)) ) )
    ((do-not-induct t)) ) ; [ 0.0 30.3 0.2 ]

#| Part 3. Specification and Proof Obligations
With interpretation and semantic lemmas, followed by the verification 
that ys satisfies the specification if it satisfies the invariants dq*. |#

(defn common (xs ys)
    (cond ((nlistp xs) f)
	  ((member (car xs) ys) (list (car xs)))
	  (t (common (cdr xs) ys)) ) )

(lemma common-implied (rewrite)
    (implies (and (member a xs)
		  (member a ys) )
	     (common xs ys) ) 
    ((enable common)) )

(lemma common-implies (rewrite)
    (let ((a (common xs ys)))    
      (implies a 
	       (and (member (car a) xs)
		    (member (car a) ys) ) ) )
    ((enable common)) )

(defn find-conflict (q plist x)
    (cond ((nlistp plist) f)
	  ((and (not (equal q (car plist)))
		(common (accessed q x) (accessed (car plist) x)) )
	   plist )
	  (t (find-conflict q (cdr plist) x)) ) )

(lemma find-conflict-implied (rewrite)
    (implies (and (common (accessed q x) (accessed r x))
		  (member r plist)
		  (not (equal q r)) )
	     (find-conflict q plist x) )
    ((enable find-conflict)) )

(lemma find-conflict-implies (rewrite)
    (let ((pl (find-conflict q plist x)))
      (implies pl
	       (and (common (accessed q x) (accessed (car pl) x))
		    (listp pl)
		    (not (equal q (car pl))) ) ) )
    ((enable find-conflict)) )

(defn exists-conflict (q x)
    (find-conflict q (processes x) x) )

(lemma accessed-outside (rewrite)
    (implies (not (member q (processes x)))
	     (equal (accessed q x) 0) )
    ((enable accessed lookup privstate-outside)
     (do-not-induct t) ) )

(lemma conflict-implies-exists-conflict (rewrite)
    (implies (and (member ob (accessed q x))
		  (member ob (accessed r x))
		  (not (equal q r)) )
             (exists-conflict q x) )
    ((enable exists-conflict accessed-outside common-implied)
     (use (find-conflict-implied (plist (processes x))))
     (do-not-induct t) ) )

(defn eval2 (flag x as bs) 
    (if (equal flag 'list)
	(if (nlistp x) nil
	  (cons (eval2 t (car x) as bs)
		(eval2 'list (cdr x) as bs) ) )
      (cond ((litatom x) (cdr (assoc x as)))
            ((nlistp x) x)
	    (t (case (car x) 
		     (quote (cadr x))
		     (new (eval2 t (cadr x) bs as)) 
		     (or (lor (eval2 'list (cdr x) as bs))) 
		     (and (land (eval2 'list (cdr x) as bs))) 
		     (unchanged (eqlis-lookup (cdr x) as bs))
		     (otherwise 
		      (applyn (car x) 
			      (eval2 'list (cdr x) as bs) ) ) )) ) ) )

(defn interpret (d spec q x y)
    (eval2 t spec (sview d q x) (sview d q y)) )

(defn sp-begin ()
   '(and (equal turn 3)
	 (equal (new turn) 2)
	 (unchanged gnr accessed nr sysAb)
	 (equal inv 'begin)
	 (equal (new res) 'begin)
	 (equal (new start) (new val)) ) )

(defn sp-invoke ()
   '(and (equal turn 3)
	 (equal (new turn) 2)
	 (unchanged gnr accessed nr sysAb start)
	 (listp inv)
	 (db-condition inv val (new val) (new res))
	 (not (member (new res) '(end abort))) ) )

(defn sp-abort ()
   '(and (equal turn 3)
	 (equal (new turn) 1)
	 (unchanged gnr)
	 (equal nr 0)
	 (or (equal inv 'abort) sysAb )
	 (equal (new accessed) 'nil)
	 (equal (new res) 'abort) ) )

(defn sp-end ()
   '(and (equal turn 3)
	 (equal (new turn) 1)
	 (unchanged gnr)
	 (lessp 0 nr)
	 (equal inv 'end)
	 (eq-lookup start (etMem (sub1 nr)))
	 (eq-lookup val (etMem nr)) 
	 (equal (new accessed) 'nil)
	 (equal (new res) 'end) ) )

(defn sp-serial ()
   '(and (member turn '(2 3))
	 (unchanged turn accessed start val sysAb)
	 (equal nr 0)
	 (equal (new gnr) (add1 gnr))
	 (equal (new nr) (add1 gnr)) 
	 (or (equal turn 3) (unchanged res)) ) )

(defn sp-conflict ()
   '(and (or (iff (new sysAb) sysAb)
	     (and (exists-conflict self global-state)
		  (not sysAb) ) )
	 (unchanged gnr turn accessed start val nr)
	 (or (equal turn 3) (unchanged res)) ) )

(defn sdi-spec ()
   `(or (not (equal (new actor) 'db))
        (and (unchanged evf inv)
	     ,(list 'or 
		    (sp-begin) 
		    (sp-invoke)
		    (sp-abort)
		    (sp-end)
		    (sp-serial)
		    (sp-conflict) ) ) ) )

(defn sdinext (q x y)
    (interpret (sdi-shared) (sdi-spec) q x y) )

(defn rel-begin (q x y)
    (and (equal (turn q x) 3)
	 (equal (turn q y) 2)
	 (equal (inv q x) (inv q y))
	 (equal (evf q x) (evf q y)) 
	 (equal (gnr x) (gnr y))
	 (equal (accessed q x) (accessed q y))
	 (equal (nr q x) (nr q y)) 
	 (equal (sysAb q x) (sysAb q y)) 
	 (equal (inv q x) 'begin)
	 (equal (res q y) 'begin)
	 (equal (start q y) (val q y)) ) )
	 
(defn rel-invoke (q x y)
    (and (equal (turn q x) 3)
	 (equal (turn q y) 2)
	 (equal (inv q x) (inv q y))
	 (equal (evf q x) (evf q y)) 
	 (equal (gnr x) (gnr y))
	 (equal (accessed q x) (accessed q y))
	 (equal (nr q x) (nr q y)) 
	 (equal (sysAb q x) (sysAb q y)) 
	 (listp (inv q x))
	 (equal (start q x) (start q y))
	 (db-condition (inv q x) (val q x)
		       (val q y) (res q y) )
	 (not (member (res q y) '(end abort))) ) )
	 
(defn rel-abort (q x y)
    (and (equal (turn q x) 3)
	 (equal (turn q y) 1)
	 (equal (inv q x) (inv q y))
	 (equal (evf q x) (evf q y)) 
	 (equal (gnr x) (gnr y))
	 (equal (accessed q y) nil)
	 (equal (nr q x) 0)
	 (or (equal (inv q x) 'abort)
	     (sysAb q x) )
	 (equal (res q y) 'abort) ) ) 

(defn rel-end (q x y)
    (and (equal (turn q x) 3)
	 (equal (turn q y) 1)
	 (equal (inv q x) (inv q y))
	 (equal (evf q x) (evf q y)) 
	 (equal (gnr x) (gnr y))
	 (equal (accessed q y) nil)
	 (equal (inv q x) 'end)
	 (equal (res q y) 'end)
	 (lessp 0 (nr q x))
	 (eq-lookup (start q x)
		    (etMem (sub1 (nr q x))) )
	 (eq-lookup (val q x)
		    (etMem (nr q x)) ) ) )

(defn serialization (q x y)
    (and (equal (inv q x) (inv q y))
	 (equal (evf q x) (evf q y)) 
	 (equal (turn q x) (turn q y))
	 (equal (accessed q x) (accessed q y))
	 (equal (start q x) (start q y))
	 (equal (val q x) (val q y)) 
	 (equal (sysAb q x) (sysAb q y)) 
	 (member (turn q x) '(2 3))
	 (equal (nr q x) 0) 
	 (equal (gnr y) (add1 (gnr x)))
	 (equal (nr q y) (add1 (gnr x)))
	 (or (equal (turn q x) 3)
	     (equal (res q x) (res q y)) ) ) )

(defn silent (q x y)
    (and (equal (inv q x) (inv q y))
	 (equal (evf q x) (evf q y)) 
	 (equal (turn q x) (turn q y))
	 (equal (accessed q x) (accessed q y))
	 (equal (start q x) (start q y))
	 (equal (val q x) (val q y))  
	 (equal (gnr x) (gnr y))
	 (equal (nr q x) (nr q y))
	 (or (equal (turn q x) 3)
	     (equal (res q x) (res q y)) ) 
	 (or (and (not (sysAb q x))
		  (exists-conflict q x) )
	     (iff (sysAb q y) (sysAb q x)) ) ) )

(deftheory next-theory
    (turn inv res gnr start val nr sysAb accessed sdi-spec actor
	  sview sdinext sdi-shared interpret eval2 applyn evf
	  land lor shared cleanalist lookup privstate eqlis-lookup 
	  sp-begin sp-invoke sp-abort sp-end sp-serial sp-conflict
	  rel-begin rel-invoke rel-abort rel-end serialization silent) )

#| First the semantic lemmas that assert the implications of sdinext. 
These are not used in the proof, but serve to indicate that the 
syntactic construction of sdinext corresponds to the intentions. |#

(lemma sdinext-implies-rel-begin (rewrite)
    (implies (and (sdinext q x y)
		  (equal (actor y) 'db)
		  (equal (inv q x) 'begin)
		  (not (equal (turn q x) 2))
		  (equal (turn q y) 2) )
	     (rel-begin q x y) )
    ((enable-theory next-theory)
     (do-not-induct t) ) ) ; [ 0.0 3.7 0.0 ]

(lemma sdinext-implies-rel-invoke (rewrite)
    (implies (and (sdinext q x y)
		  (equal (actor y) 'db)
		  (not (equal (inv q x) 'begin))
		  (not (equal (turn q x) 2))
		  (equal (turn q y) 2) )
	     (rel-invoke q x y) )
    ((enable-theory next-theory)
     (do-not-induct t) ) ) ; [ 0.0 3.7 0.0 ]

(lemma sdinext-implies-rel-abort (rewrite)
    (implies (and (sdinext q x y)
		  (equal (actor y) 'db)
		  (equal (res q y) 'abort)
		  (not (equal (turn q x) (turn q y)))
		  (not (equal (turn q y) 2)) )
	     (rel-abort q x y) )
    ((enable-theory next-theory)
     (do-not-induct t) ) ) ; [ 0.0 3.8 0.0 ]

(lemma sdinext-implies-rel-end (rewrite)
    (implies (and (sdinext q x y)
		  (equal (actor y) 'db)
		  (not (equal (res q y) 'abort))
		  (not (equal (turn q x) (turn q y)))
		  (not (equal (turn q y) 2)) )
	     (rel-end q x y) )
    ((enable-theory next-theory)
     (do-not-induct t) ) ) ; [ 0.0 1.9 0.0 ]

(lemma sdinext-implies-serialization (rewrite)
    (implies (and (sdinext q x y)
		  (equal (actor y) 'db)
		  (not (equal (gnr x) (gnr y))) )
	     (serialization q x y) )
    ((enable-theory next-theory)
     (do-not-induct t) ) ) ; [ 0.0 1.7 0.0 ]

(lemma sdinext-implies-silent (rewrite)
    (implies (and (sdinext q x y)
		  (equal (actor y) 'db)
		  (equal (gnr x) (gnr y))
		  (equal (turn q x) (turn q y)) )
	     (silent q x y) )
    ((enable-theory next-theory)
     (do-not-induct t) ) ) ; [ 0.0 4.3 0.1 ]

(lemma sdinext-implies (rewrite)
    (implies (sdinext q x y)
	     (or (not (equal (actor y) 'db))
		 (rel-begin q x y)
		 (rel-invoke q x y)
		 (rel-abort q x y)
		 (rel-end q x y)
		 (serialization q x y) 
		 (silent q x y) ) )
    ((enable sdinext-implies-rel-invoke sdinext-implies-serialization)
     (use (sdinext-implies-rel-begin)
	  (sdinext-implies-rel-abort)
	  (sdinext-implies-rel-end)
	  (sdinext-implies-silent) )
     (do-not-induct t) ) ) ; triv

#| The following semantic lemmas assert cases where sdinext is 
implied. These lemmas serve to ensure that behaviour ys satisfies the 
specification. |# 

(lemma env-sat-sdinext (rewrite)
    (implies (not (equal (actor y) 'db))
             (sdinext q x y) )
    ((enable-theory next-theory)
     (do-not-induct t) ) ) ; [ 0.0 3.0 0.0 ]

(lemma rel-begin-implies-sdinext (rewrite)
    (implies (rel-begin q x y)
             (sdinext q x y) )
    ((enable-theory next-theory)
     (do-not-induct t) ) ) ; [ 0.0 5.0 0.0 ]

(lemma rel-invoke-implies-sdinext (rewrite)
    (implies (rel-invoke q x y)
             (sdinext q x y) )
    ((enable-theory next-theory)
     (do-not-induct t) ) ) ; [ 0.0 5.0 0.0 ]

(lemma rel-abort-implies-sdinext (rewrite)
    (implies (rel-abort q x y)
             (sdinext q x y) )
    ((enable-theory next-theory)
     (do-not-induct t) ) ) ; [ 0.0 5.0 0.0 ]

(lemma rel-end-implies-sdinext (rewrite)
    (implies (rel-end q x y)
             (sdinext q x y) )
    ((enable-theory next-theory)
     (do-not-induct t) ) ) ; [ 0.0 5.0 0.0 ]

(lemma serialization-implies-sdinext (rewrite)
    (implies (serialization q x y)
             (sdinext q x y) )
    ((enable-theory next-theory)
     (do-not-induct t) ) ) ; [ 0.0 6.4 0.0 ]

(lemma silent-implies-sdinext (rewrite)
    (implies (silent q x y)
             (sdinext q x y) )
    ((enable-theory next-theory)
     (do-not-induct t) ) ) ; [ 0.0 22.1 0.0 ]

(lemma sdinext-equiv () ; just to verify
    (iff (sdinext q x y)
	 (or (not (equal (actor y) 'db))
	     (rel-begin q x y)
	     (rel-invoke q x y)
	     (rel-abort q x y)
	     (rel-end q x y)
	     (serialization q x y) 
	     (silent q x y) ) )
    ((enable env-sat-sdinext rel-begin-implies-sdinext 
	     rel-invoke-implies-sdinext rel-abort-implies-sdinext 
	     rel-end-implies-sdinext serialization-implies-sdinext 
	     silent-implies-sdinext)
     (use (sdinext-implies))
     (do-not-induct t) ) ) ; triv

(lemma ys-step (rewrite)
    (equal (ys (add1 n)) (step (round (add1 n)) (ys n))) 
    ((enable ys)) )

(defn dq0 (q x)
    (implies (lessp 15 (pc q x))
	     (equal (turn q x) 3) ) )

(defn dq1 (q x)
    (implies (equal (pc q x) 21)
	     (equal (inv q x) 'begin) ) )

(defn dq2 (q x)
    (implies  (equal (pc q x) 31)
	      (or (equal (lookup (iob q x) (owner x)) 0) 
		  (exists-conflict q x) ) ) )

(defn dq3 (q x) 
    (implies (equal (pc q x) '33)
	     (and (listp (inv q x))
		  (equal (iob q x) (car (inv q x)))
		  (or (equal (val q x) 0)
		      (equal (lookup (iob q x) (pridb q x) )
			     (lookup (iob q x) (val q x)) ) ) ) ) )

(defn dq4 (q x)
    (implies (equal (pc q x) 42)
	     (and (equal (nr q x) 0)
		  (or (equal (inv q x) 'abort)
		      (sysAb q x) ) ) ) )

(defn dq5 (q x) 
    (implies (equal (pc q x) 50)
	     (equal (nr q x) 0) ) )

(defn dq6 (q x)
    (implies (equal (pc q x) 53)
	     (and (not (zerop (nr q x)))
		  (equal (inv q x) 'end)
		  (eq-lookup (start q x) (etMem (sub1 (nr q x))))
		  (eq-lookup (val q x) (etMem (nr q x))) ) ) )

(deftheory behav-spec-theory 
    (pc-step new-pc inv-step start-step cnt-step sysAb-step mnr-step
     res-step tlist-step ownset-step accessed-step nr-step iob-step
     hiSutno-step pridb-step val-step gnr-step evf-step db-step
     hiMem-step owner-step turn-step  madd-to-set-member-equal 
     member-madd-to-set ys-step actor-step rel-begin rel-invoke rel-abort
     rel-end serialization silent dq0 dq1 dq2 dq3 dq4 dq5 dq6) )

(lemma ys-silent-list (rewrite)
    (implies (not (member (pc (round (add1 n)) (ys n))
			  '(0 10 15 21 31 33 42 50 53) ))
	     (silent (round (add1 n)) (ys n) (ys (add1 n))) )
    ((enable-theory behav-spec-theory)
     (enable silent)
     (do-not-induct t) ) ) ; triv

(lemma ys-env-list (rewrite)
    (implies (member (pc (round (add1 n)) (ys n)) '(0 10 15) )
	     (equal (actor (ys (add1 n))) 'env) )
    ((enable-theory behav-spec-theory)
     (do-not-induct t) ) ) ; triv

(lemma ys-sdinext-list (rewrite)
    (implies (not (member (pc (round (add1 n)) (ys n))
			  '(21 31 33 42 50 53) ))
	     (sdinext (round (add1 n)) (ys n) (ys (add1 n))) )
    ((use (ys-silent-list))
     (enable env-sat-sdinext silent-implies-sdinext ys-env-list)
     (do-not-induct t) ) ) ; triv

(lemma ys-response-at-21 (rewrite)
    (implies (and (member (pc (round (add1 n)) (ys n)) '(21))
		  (dq0 (round (add1 n)) (ys n)) 
		  (dq1 (round (add1 n)) (ys n)) )
	     (rel-begin (round (add1 n)) (ys n) (ys (add1 n))) )
    ((enable-theory behav-spec-theory)
     (do-not-induct t) ) )

(lemma ys-silent-at-31 (rewrite)
    (implies (and (member (pc (round (add1 n)) (ys n)) '(31))
		  (dq2 (round (add1 n)) (ys n)) )
	     (silent (round (add1 n)) (ys n) (ys (add1 n))) )
    ((enable-theory behav-spec-theory)
     (do-not-induct t) ) )

(lemma ys-response-at-33 (rewrite)
    (implies (and (member (pc (round (add1 n)) (ys n)) '(33))
		  (dq0 (round (add1 n)) (ys n)) 
		  (dq3 (round (add1 n)) (ys n)) )
	     (rel-invoke (round (add1 n)) (ys n) (ys (add1 n))) )
    ((enable-theory behav-spec-theory)
     (enable result-axiom db-condition except-lookup-putassoc 
	     assoc-put lookup objects-axiom)
     (do-not-induct t) ) )

(lemma ys-terminating-at-42 (rewrite)
    (implies (and (member (pc (round (add1 n)) (ys n)) '(42))
		  (dq0 (round (add1 n)) (ys n)) 
		  (dq4 (round (add1 n)) (ys n)) )
	     (rel-abort (round (add1 n)) (ys n) (ys (add1 n))) )
    ((enable-theory behav-spec-theory)
     (do-not-induct t) ) )

(lemma ys-synchro-at-50 (rewrite)
    (implies (and (member (pc (round (add1 n)) (ys n)) '(50))
		  (dq0 (round (add1 n)) (ys n)) 
		  (dq5 (round (add1 n))(ys n)) )
	     (serialization (round (add1 n)) (ys n) (ys (add1 n))) )
    ((enable-theory behav-spec-theory)
     (do-not-induct t) ) )

(lemma ys-terminating-at-53 (rewrite)
    (implies (and (member (pc (round (add1 n)) (ys n)) '(53))
		  (dq0 (round (add1 n)) (ys n)) 
		  (dq6 (round (add1 n))(ys n)) )
	     (rel-end (round (add1 n)) (ys n) (ys (add1 n))) )
    ((enable-theory behav-spec-theory)
     (do-not-induct t) ) )

(defn dq* (q x)
    (and (dq0 q x) (dq1 q x) (dq2 q x) (dq3 q x) 
	 (dq4 q x) (dq5 q x) (dq6 q x) ) )

(lemma ys-dq* (rewrite)
    (implies (dq* (round (add1 n)) (ys n)) 
	     (sdinext (round (add1 n)) (ys n) (ys (add1 n))) )
    ((enable dq* ys-response-at-21 ys-silent-at-31 ys-response-at-33 
	     ys-terminating-at-42 ys-synchro-at-50 ys-terminating-at-53 
	     rel-begin-implies-sdinext rel-invoke-implies-sdinext 
	     rel-abort-implies-sdinext rel-end-implies-sdinext 
	     serialization-implies-sdinext silent-implies-sdinext )
     (use (ys-sdinext-list))
     (do-not-induct t) ) )

#| Part 4. Forward Invariants up to Kq5
Leading to the proof that ys satisfies dq0, dq1, dq2, dq4, dq5, and 
partial results for dq3 and dq6. |#

(disable-theory t)
(enable-theory ground-zero)

(enable-theory
    (pc-step new-pc inv-step start-step cnt-step sysAb-step
     mnr-step res-step tlist-step ownset-step accessed-step nr-step
     hiSutno-step iob-step pridb-step val-step gnr-step evf-step
     db-step hiMem-step owner-step turn-step  madd-to-set-member-equal 
     member-madd-to-set dq0 dq1 dq2 dq3 dq5 dq6 dq6 assoc-put lookup) )

(lemma processes-step (rewrite)
    (equal (processes (step p x))
	   (madd-to-set p (processes x)) )
    ((enable processes-exepcn step)) )

; Non-active processes hold no private variables

(lemma private-outside (rewrite)
    (implies (not (member q (processes x)))
	     (and (equal (pc q x) 0)
		  (equal (start q x) 0)
		  (equal (ownset q x) 0)
		  (equal (tlist q x) 0)
		  (equal (cnt q x) 0)
		  (equal (turn q x) 0)
		  (equal (inv q x) 0)
		  (equal (mnr q x) 0)
		  (equal (nr q x) 0)
		  (equal (val q x) 0) ) )
    ((enable start cnt turn inv mnr nr val ownset lookup pc 
	     tlist privstate-outside)
     (do-not-induct t) ) )

(defn inside-prog (q x) 
    (member (pc q x) '(0 10 15 20 21 30 31 32 33 40 41 42 50 51 52 53)) )

(lemma inside-prog-kept-valid (rewrite)
    (implies (inside-prog q x)
	     (inside-prog q (step p x)) )
    ((enable inside-prog new-pc pc-step) 
     (do-not-induct t)) ) ; [ 0.0 3.5 0.0 ]

(prove-lemma dq0-kept-valid (rewrite)
    (implies (dq0 q x)
	     (dq0 q (step p x)) )
    ((do-not-induct t)) ) ; 

(prove-lemma dq1-kept-valid (rewrite)
    (implies (dq1 q x)
	     (dq1 q (step p x)) )
    ((do-not-induct t)) )

(defn jq0 (q x) 
    (implies (member (pc q x) '(31 32 33))
	     (member (iob q x) (accessed q x)) ) )

(defn jq1 (ob x)
    (or (equal (lookup ob (owner x)) 0)
        (member ob (accessed (lookup ob (owner x)) x)) ) )

(defn jq2 (q x)
    (not (and (member (pc q x) '(31 32))
	      (member (iob q x) (ownset q x)) )) )

(defn jq3 (ob q x)
    (implies (and (equal (lookup ob (owner x)) q)
		  (not (equal q 0))
		  (not (member ob (ownset q x))) )
	     (and (equal (pc q x) 32)
		  (equal (iob q x) ob) ) ) )

(lemma dq2-implied (rewrite)
    (implies (and (jq0 q x)
		  (jq1 (iob q x) x)
		  (jq2 q x)
		  (jq3 (iob q x) q x) )
	     (dq2 q x) )
    ((enable jq0 jq1 jq2 jq3 dq2 conflict-implies-exists-conflict)
     (do-not-induct t)) )

(prove-lemma jq0-list (rewrite)
    (implies (and (jq0 q x)
		  (not (member (pc p x) '(30))) )
	     (jq0 q (step p x)) )
    ((do-not-induct t)) ) ; [ 0.0 0.3 0.1 ]

(defn jq4a (q x)
    (implies (member (pc q x) '(30))
	     (member (car (inv q x)) (accessed q x)) ) )

(defn jq4b (q x)
    (implies (and (member (pc q x) '(20))
		  (listp (inv q x)) )
	     (member (car (inv q x)) (accessed q x)) ) )

(prove-lemma jq0-at-30 (rewrite)
    (implies (and (jq0 q x)
		  (jq4a q x)
		  (equal (pc p x) 30) )
	     (jq0 q (step p x)) )
    ((do-not-induct t)) )

(lemma jq0-kept-valid (rewrite)
    (implies (and (jq0 q x)
		  (jq4a q x) )
	     (jq0 q (step p x)) )
    ((use (jq0-list)) (enable jq0-at-30)
     (do-not-induct t)) )

(prove-lemma jq1-list (rewrite)
    (implies (and (jq1 ob x)
		  (not (member (pc p x) '(31 42 53))) )
	     (jq1 ob (step p x)) )
    ((do-not-induct t)) ) ; [ 0.0 0.3 0.1 ]

(prove-lemma jq1-at-31 (rewrite)
    (implies (and (jq1 ob x)
		  (jq0 p x)
		  (equal (pc p x) 31) )
	     (jq1 ob (step p x)) )
    ((do-not-induct t)) )

(defn jq5 (q x) 
    (implies (member (pc q x) '(0 10 42 53))
             (nlistp (ownset q x)) ) )

(prove-lemma jq1-at-42-53 (rewrite)
    (implies (and (jq1 ob x)
		  (jq3 ob p x)
		  (jq5 p x)
		  (member (pc p x) '(42 53)) )
	     (jq1 ob (step p x)) )
    ((do-not-induct t)) )

(lemma jq1-kept-valid (rewrite)
    (implies (and (jq1 ob x)
		  (jq3 ob p x)
		  (jq5 p x)
		  (jq0 p x) )
	     (jq1 ob (step p x)) )
    ((use (jq1-list)) (enable jq1-at-31 jq1-at-42-53)
     (do-not-induct t)) )

(prove-lemma jq2-kept-valid (rewrite)
    (implies (jq2 q x)
	     (jq2 q (step p x)) )
    ((do-not-induct t)) )

(prove-lemma jq3-list (rewrite)
    (implies (and (jq3 ob q x)
		  (not (member (pc p x) '(0))) )
	     (jq3 ob q (step p x)) )
    ((do-not-induct t)) ) ; [ 0.0 0.8 0.5 ]
 
(defn outside-pc (q x)
    (implies (equal (pc q x) 0) 
	     (not (member q (processes x))) ) )

(prove-lemma outside-pc-kept-valid (rewrite)
    (implies (outside-pc q x)
	     (outside-pc q (step p x)) )
    ((do-not-induct t)) ) ; triv

(prove-lemma jq3-at-0 (rewrite)
    (implies (and (jq3 ob q x)
		  (outside-pc q x)
		  (member (pc p x) '(0)) )
	     (jq3 ob q (step p x)) )
    ((do-not-induct t)) ) ; [ 0.0 0.8 0.5 ]
 
(lemma jq3-kept-valid (rewrite)
    (implies (and (jq3 ob q x)
		  (outside-pc q x) )
	     (jq3 ob q (step p x)) )
    ((use (jq3-list)) (enable jq3-at-0)
     (do-not-induct t)) )

(prove-lemma jq4a-list (rewrite)
    (implies (and (jq4a q x)
		  (not (member (pc p x) '(20 29))) )
	     (jq4a q (step p x)) )
    ((do-not-induct t)) ) ; [ 0.0 0.3 0.1 ]

(prove-lemma jq4a-at-20 (rewrite)
    (implies (and (jq4a q x)
		  (jq4b q x)
		  (equal (pc p x) 20) )
	     (jq4a q (step p x)) )
    ((do-not-induct t)) )

(prove-lemma jq4a-at-29 (rewrite)
    (implies (and (jq4a q x)
		  (inside-prog q x)
		  (equal (pc p x) 29) )
	     (jq4a q (step p x)) )
    ((do-not-induct t)) )

(lemma jq4a-kept-valid (rewrite)
    (implies (and (jq4a q x)
		  (inside-prog q x)
		  (jq4b q x) )
	     (jq4a q (step p x)) )
    ((use (jq4a-list)) (enable jq4a-at-20 jq4a-at-29)
     (do-not-induct t)) )

(prove-lemma jq4b-list (rewrite)
    (implies (and (jq4b q x)
		  (not (member (pc q x) '(19))) )
	     (jq4b q (step p x)) )
    ((do-not-induct t)) )

(prove-lemma jq4b-at-19 (rewrite)
    (implies (and (jq4b q x)
		  (inside-prog q x)
		  (member (pc q x) '(19)) )
	     (jq4b q (step p x)) )
    ((do-not-induct t)) )

(lemma jq4b-kept-valid (rewrite)
    (implies (and (jq4b q x)
		  (inside-prog q x) )
	     (jq4b q (step p x)) )
    ((use (jq4b-list)) (enable jq4b-at-19)
     (do-not-induct t)) )

(prove-lemma jq5-list (rewrite)
    (implies (and (jq5 q x)
		  (not (member (pc p x) '(9))) )
	     (jq5 q (step p x)) )
    ((do-not-induct t)) )

(prove-lemma jq5-at-9 (rewrite)
    (implies (and (jq5 q x)
		  (inside-prog q x)
		  (equal (pc p x) 9) )
	     (jq5 q (step p x)) )
    ((do-not-induct t)) )

(lemma jq5-kept-valid (rewrite)
    (implies (and (jq5 q x)
		  (inside-prog q x) )
	     (jq5 q (step p x)) )
    ((use (jq5-list)) (enable jq5-at-9)
     (do-not-induct t)) )

(defn kq0 (q x)
    (or (member (pc q x) '(0 10 51 52 53))
	(equal (nr q x) 0) ) )

(prove-lemma kq0-kept-valid (rewrite)
    (implies (kq0 q x)
	     (kq0 q (step p x)) )
    ((do-not-induct t)) ) ; [ 0.0 0.3 0.1 ]

(defn kq1 (q x)
    (implies (member (pc q x) '(40 41 42))
	     (or (equal (inv q x) 'abort)
		 (sysAb q x) ) ) )

(prove-lemma kq1-list (rewrite)
    (implies (and (kq1 q x)
		  (not (member (pc p x) '(20 39))) )
	     (kq1 q (step p x)) )
    ((do-not-induct t)) ) ; [ 0.0 0.3 0.1 ]

(defn good-invoc (q x)
    (implies (equal (pc q x) 20)
	     (or (listp (inv q x))
		 (member (inv q x) '(begin abort end)) ) ) )

(prove-lemma good-invoc-list (rewrite)
    (implies (and (good-invoc q x)
		  (not (member (pc p x) '(15 19))) )
	     (good-invoc q (step p x)) )
    ((do-not-induct t)) )

(prove-lemma good-invoc-19 (rewrite)
    (implies (and (good-invoc q x)
		  (member (pc p x) '(19))
		  (inside-prog q x) )
	     (good-invoc q (step p x)) )
    ((do-not-induct t)) ) ; [ 0.0 0.6 0.0 ]

(prove-lemma good-invoc-15 (rewrite)
    (implies (and (good-invoc q x)
		  (member (pc p x) '(15)) )
	     (good-invoc q (step p x)) )
    ((do-not-induct t) (enable norin)) ) ; [ 0.0 0.1 0.0 ]

(lemma good-invoc-kept-valid (rewrite)
    (implies (and (good-invoc q x)
		  (inside-prog q x) )
	     (good-invoc q (step p x)) )
    ((use (good-invoc-list)) (enable good-invoc-15 good-invoc-19)
     (do-not-induct t)) ) ; [ 0.0 0.6 0.0 ]

(prove-lemma kq1-at-39 (rewrite)
    (implies (and (kq1 q x)
		  (inside-prog q x)
		  (equal (pc p x) 39) )
	     (kq1 q (step p x)) )
    ((do-not-induct t)) )

(prove-lemma kq1-at-20 (rewrite)
    (implies (and (kq1 q x)
		  (good-invoc q x)
		  (equal (pc p x) 20) )
	     (kq1 q (step p x)) )
    ((do-not-induct t)) )

(lemma kq1-kept-valid (rewrite)
    (implies (and (kq1 q x)
		  (inside-prog q x)
		  (good-invoc q x) )
	     (kq1 q (step p x)) )
    ((use (kq1-list)) (enable kq1-at-20 kq1-at-39)
     (do-not-induct t)) )
 
(lemma dq4-implied (rewrite)
    (implies (and (kq1 q x)
		  (kq0 q x) )
	     (dq4 q x) ) 
    ((enable kq1 kq0 dq4) (do-not-induct t) ) )

(lemma dq5-implied (rewrite)
    (implies (kq0 q x)
	     (dq5 q x) )
    ((enable kq0 dq5)) )

(defn kq2 (q x)
    (implies (member (pc q x) '(30 31 32 33))
	     (listp (inv q x)) ) )

(prove-lemma kq2-list (rewrite)
    (implies (and (kq2 q x)
		  (not (member (pc q x) '(29))) )
	     (kq2 q (step p x)) ) 
    ((do-not-induct t)) )
 
(prove-lemma kq2-at-29 (rewrite)
    (implies (and (kq2 q x)
		  (member (pc q x) '(29))
		  (inside-prog q x) )
	     (kq2 q (step p x)) ) 
    ((do-not-induct t)) )
 
(lemma kq2-kept-valid (rewrite)
    (implies (and (kq2 q x)
		  (inside-prog q x) )
	     (kq2 q (step p x)) ) 
    ((use (kq2-list)) (enable kq2-at-29)
     (do-not-induct t)) )

(defn kq3 (q x) 
    (implies (member (pc q x) '(31 32 33))
	     (equal (iob q x) (car (inv q x))) ) )

(prove-lemma kq3-kept-valid (rewrite)
    (implies (kq3 q x)
	     (kq3 q (step p x)) ) 
    ((do-not-induct t)) )
 
(defn kq4 (q x)
    (implies (member (pc q x) '(50 51 52 53))
             (equal (inv q x) 'end) ) )

(prove-lemma kq4-list (rewrite)
    (implies (and (kq4 q x)
		  (not (member (pc p x) '(49))) )
	     (kq4 q (step p x)) )
    ((do-not-induct t)) ) ; [ 0.0 0.3 0.1 ]

(prove-lemma kq4-at-49 (rewrite)
    (implies (and (kq4 q x)
		  (inside-prog q x)
		  (equal (pc p x) 49) )
	     (kq4 q (step p x)) )
    ((do-not-induct t)) )

(lemma kq4-kept-valid (rewrite)
    (implies (and (kq4 q x)
		  (inside-prog q x) )
	     (kq4 q (step p x)) )
    ((use (kq4-list)) (enable kq4-at-49)
     (do-not-induct t)) )

(defn kq5 (q x)
    (implies (member (pc q x) '(51 52 53))
	     (and (equal (nr q x) (lookup (cnt q x) (hiSutno q x)))
		  (not (zerop (nr q x))) ) ) )

(prove-lemma kq5-kept-valid (rewrite)
    (implies (kq5 q x)
	     (kq5 q (step p x)) )
    ((do-not-induct t)) ) ; [ 0.0 0.4 0.1 ]

#| Part 5. The proofs of Dq3 and Dq6 under assumption of Yq0 |#

(defn lq0 (q x)
  (equal (start q x)
	 (if (zerop (mnr q x)) 0
	   (etMem (sub1 (mnr q x))) ) ) )

(prove-lemma lq0-kept-valid (rewrite)
    (implies (lq0 q x)
	     (lq0 q (step p x)) )
    ((do-not-induct t)) )

(defn lq1 (q x)
    (implies (member (pc q x) '(15 30 31 32 33 40 50))
	     (equal (mnr q x) (etSutno (add1 (cnt q x)) q)) ) )

(defn lq1b (q x)
    (implies (and (equal (pc q x) 20)
		  (not (equal (inv q x) 'begin)) )
	     (equal (mnr q x) (etSutno (add1 (cnt q x)) q)) ) )

(prove-lemma lq1-list (rewrite)
    (implies (and (lq1 q x)
		  (not (member (pc p x) '(14 20 29 39 49))) )
	     (lq1 q (step p x)) )
    ((do-not-induct t)) ) ; [ 0.0 0.6 0.1 ]

(prove-lemma lq1-at-14-29-39-49 (rewrite)
    (implies (and (lq1 q x)
		  (inside-prog q x)
		  (member (pc p x) '(14 29 39 49)) )
	     (lq1 q (step p x)) )
    ((do-not-induct t)) ) ; [ 0.0 1.9 0.1 ]

(prove-lemma lq1-at-20 (rewrite)
    (implies (and (lq1 q x)
		  (lq1b q x)
		  (member (pc p x) '(20)) )
	     (lq1 q (step p x)) )
    ((do-not-induct t)) ) ; [ 0.0 1.9 0.1 ]

(lemma lq1-kept-valid (rewrite)
    (implies (and (lq1 q x)
		  (lq1b q x)
		  (inside-prog q x) )
	     (lq1 q (step p x)) )
    ((use (lq1-list)) (enable lq1-at-20 lq1-at-14-29-39-49)
     (do-not-induct t)) )

(prove-lemma lq1b-list (rewrite)
    (implies (and (lq1b q x)
		  (not (member (pc p x) '(15 19))) )
	     (lq1b q (step p x)) )
    ((do-not-induct t)) ) ; [ 0.0 0.6 0.1 ]

(prove-lemma lq1b-at-19 (rewrite)
    (implies (and (lq1b q x)
		  (inside-prog q x)
		  (member (pc p x) '(19)) )
	     (lq1b q (step p x)) )
    ((do-not-induct t)) ) ; [ 0.0 1.9 0.1 ]

(prove-lemma lq1b-at-15 (rewrite)
    (implies (and (lq1b q x)
		  (lq1 q x)
		  (member (pc p x) '(15)) )
	     (lq1b q (step p x)) )
    ((do-not-induct t)) ) ; [ 0.0 1.9 0.1 ]

(lemma lq1b-kept-valid (rewrite)
    (implies (and (lq1b q x)
		  (lq1 q x)
		  (inside-prog q x) )
	     (lq1b q (step p x)) )
    ((use (lq1b-list)) (enable lq1b-at-15 lq1b-at-19)
     (do-not-induct t)) )

(defn lq2 (q x)
    (implies (member (pc q x) '(41 42 51 52 53))
	     (equal (mnr q x) (etSutno (cnt q x) q)) ) )

(prove-lemma lq2-list (rewrite)
    (implies (and (lq2 q x)
		  (not (member (pc p x) '(40 50))) )
	     (lq2 q (step p x)) )
    ((do-not-induct t)) ) ; 

(prove-lemma lq2-at-40-50 (rewrite)
    (implies (and (lq2 q x)
		  (lq1 q x)
		  (member (pc p x) '(40 50)) )
	     (lq2 q (step p x)) )
    ((do-not-induct t)) )

(lemma lq2-kept-valid (rewrite)
    (implies (and (lq2 q x)
		  (lq1 q x) )
	     (lq2 q (step p x)) )
    ((use (lq2-list)) (enable lq2-at-40-50)
     (do-not-induct t)) )

(defn mnr=nr (q x) ; aq0
    (implies (member (pc q x) '(51 52 53))
	     (equal (mnr q x) (nr q x)) ) )

(lemma mnr=nr-implied (rewrite)
    (implies (and (kq5 q x)
		  (lq2 q x)
		  (rq1 (cnt q x) q x) )
	     (mnr=nr q x) )
    ((enable kq5 lq2 rq1 mnr=nr)
     (do-not-induct t)) )

(defn start=etMem (q x) ; aq1
    (implies (member (pc q x) '(51 52 53))
	     (equal (start q x) (etMem (sub1 (nr q x)))) ) )

(prove-lemma start=etMem-implied (rewrite)
    (implies (and (kq5 q x)
		  (lq0 q x)
		  (mnr=nr q x) )
	     (start=etMem q x) )
    ((do-not-induct t)) )

(defn lq3 (q x)
    (lessp (nr q x) (add1 (gnr x))) ) 

(prove-lemma lq3-kept-valid (rewrite)
    (implies (lq3 q x)
	     (lq3 q (step p x)) )
    ((do-not-induct t)) )
 
(defn nzero-under (n as) ; (for all i < n : as[i] \ne 0) 
    (if (zerop n) t
        (and (not (equal (cdr (assoc (sub1 n) as)) 0))
	     (nzero-under (sub1 n) as) ) ) )

(lemma nzero-under-lookup (rewrite)
    (implies (and (nzero-under n as)
		  (numberp m)
		  (lessp m n ) )
             (not (equal (lookup m as) 0)) )
    ((induct (nzero-under n as)) (do-not-induct t)
     (enable lookup nzero-under)) )

(lemma nzero-putassoc* (rewrite)
    (implies (not (equal hi 0))
	     (not (equal (putassoc* os pr hi) 0)) )
    ((enable putassoc*)) )

(lemma nzero-cons (rewrite)
    (implies (and (nzero-under n hi)
		  (not (lessp a n)) )
	     (nzero-under n (cons (cons a b) hi)) ) 
    ((induct (nzero-under n hi)) (do-not-induct t)
     (enable nzero-under)) )

(defn lq4 (x)
    (nzero-under (add1 (gnr x)) (hiMem x)) )

(defn numberp-gnr (x)
    (numberp (gnr x)) )

(prove-lemma numberp-gnr-kept-valid (rewrite)
    (implies (numberp-gnr x)
	     (numberp-gnr (step p x)) )
    ((do-not-induct t)) )

(prove-lemma lq4-kept-valid (rewrite)
    (implies (and (lq4 x)
		  (numberp-gnr x) )
	     (lq4 (step p x)) ) 
    ((do-not-induct t)) )
 
(defn start-ne-bot (q x) ; aq2
    (not (and (member (pc q x) '(51 52 53))
	      (equal (start q x) 0) )) )

(lemma start-ne-bot-implied (rewrite)
    (implies (and (start=etMem q x)
		  (lq3 q x)
		  (lq4 x)
		  (rq0 (sub1 (nr q x)) x) )
	     (start-ne-bot q x) )
    ((enable start-ne-bot start=etMem nzero-under-lookup lq3 lq4 rq0) 
     (do-not-induct t)) )

(defn yq0 (ob q x) ; proof of invariance is postponed
    (implies (and (member ob (ownset q x))
		  (not (equal (val q x) 0)) )
	     (equal (lookup ob (pridb q x) )
		    (lookup ob (val q x)) ) ) )

(defn lq5 (q x) 
    (implies (member (pc q x) '(33))
	     (member (iob q x) (ownset q x)) ) )

(prove-lemma lq5-kept-valid (rewrite)
    (implies (lq5 q x)
	     (lq5 q (step p x)) )
    ((do-not-induct t)) )

(lemma dq3-implied (rewrite)
    (implies (and (kq2 q x)
		  (kq3 q x)
		  (lq5 q x)
		  (yq0 (iob q x) q x) )
	     (dq3 q x) )
    ((enable kq3 kq2 lq5 yq0 dq3)) )

(defn yq1 (q x)
    (implies (member (pc q x) '(52 53))
	     (eq-lookup (val q x) (etMem (nr q x))) ) )

(lemma dq6-implied (rewrite)
    (implies (and (yq1 q x)
		  (kq5 q x)
		  (kq4 q x)
		  (start=etMem q x) )
	     (dq6 q x) ) 
    ((enable yq1 dq6 kq5 kq4 start=etMem eq-lookup-reflexive)) )

(defn aq3 (q x)
    (implies (member (pc q x) '(51))
	     (eq-lookup (val q x) (etMem (nr q x))) ) )
 
(prove-lemma yq1-list (rewrite)
    (implies (and (yq1 q x)
		  (not (member (pc p x) '(51))) )
	     (yq1 q (step p x)) )
    ((disable eq-lookup) 
     (do-not-induct t)) ) ; [ 0.0 0.3 0.1 ]

(prove-lemma yq1-at-51 (rewrite)
    (implies (and (yq1 q x)  
		  (aq3 q x)
		  (member (pc p x) '(51)) )
	     (yq1 q (step p x)) )
    ((do-not-induct t)) )

(lemma yq1-kept-valid (rewrite)
    (implies (and (yq1 q x)
		  (aq3 q x)
		  (kq0 q x) )
	     (yq1 q (step p x)) )
    ((use (yq1-list)) (enable yq1-at-51)
     (do-not-induct t)) )

(defn aq3a (ob q x) 
    (implies (equal (pc q x) 51)
	     (equal (lookup ob (val q x))
		    (if (member ob (ownset q x))
			(lookup ob (pridb q x))
		      (lookup ob (etMem (sub1 (mnr q x)))) ) ) ) )

(defn mq0 (q x)
     (equal (equal (val q x) 0)
	    (equal (start q x) 0) ) )

(prove-lemma mq0-kept-valid (rewrite)
    (implies (mq0 q x)
	     (mq0 q (step p x)) )
    ((do-not-induct t)) )

(defn mq1 (ob q x)
    (or (equal (start q x) 0)
	(member (pc q x) '(41 42 52 53))
	(member ob (ownset q x))
	(equal (lookup ob (etMem (sub1 (mnr q x))))
	       (lookup ob (val q x)) ) ) )

(prove-lemma mq1-list (rewrite)
    (implies (and (mq1 ob q x)
		  (not (member (pc p x) '(0 33))) )
	     (mq1 ob q (step p x)) )
    ((do-not-induct t)) ) ; [ 0.0 0.3 0.1 ]

(prove-lemma mq1-at-0 (rewrite)
    (implies (and (mq1 ob q x)
		  (outside-pc q x)
		  (equal (pc p x) 0) )
	     (mq1 ob q (step p x)) )
    ((enable lookup) (do-not-induct t)) )

(prove-lemma mq1-at-33 (rewrite)
    (implies (and (mq1 ob q x)
		  (lq5 q x)
		  (equal (pc p x) 33) )
	     (mq1 ob q (step p x)) )
    ((enable lookup) (do-not-induct t)) )

(lemma mq1-kept-valid (rewrite)
    (implies (and (mq1 ob q x)
		  (outside-pc q x)
		  (lq5 q x) )
	     (mq1 ob q (step p x)) )
    ((use (mq1-list)) (enable mq1-at-33 mq1-at-0)
     (do-not-induct t)) )

(lemma aq3a-implied (rewrite)
    (implies (and (yq0 ob q x)
		  (mq0 q x)
		  (start-ne-bot q x)
		  (mq1 ob q x) )
	     (aq3a ob q x) ) 
    ((enable private-outside yq0 mq0 start-ne-bot mq1 aq3a)) )

(defn mq2 (ob q x)
    (implies (equal (pc q x) 51)
	     (equal (lookup ob (lookup (nr q x) (hiMem x)))
		    (if (member ob (ownset q x))
			(lookup ob (pridb q x))
		      (lookup ob (lookup (sub1 (nr q x)) (hiMem x))) ) ) ) )

(prove-lemma mq2-list (rewrite)
    (implies (and (mq2 ob q x)
		  (not (member (pc p x) '(50))) )
	     (mq2 ob q (step p x)) )
    ((do-not-induct t)) ) ; [ 0.0 2.8 1.1 ]

(prove-lemma mq2-at-50 (rewrite)
    (implies (and (mq2 ob q x)  
		  (lq3 q x)  
		  (numberp-gnr x)
		  (member (pc p x) '(50)) )
	     (mq2 ob q (step p x)) )
    ((enable lookup-putassoc* lookup) (do-not-induct t)) )

(lemma mq2-kept-valid (rewrite)
    (implies (and (mq2 ob q x)
		  (lq3 q x)  
		  (numberp-gnr x) )
	     (mq2 ob q (step p x)) )
    ((use (mq2-list)) (enable mq2-at-50)
     (do-not-induct t)) )

(defn val=etMem (ob q x) ; aq3-pointwise
    (implies (member (pc q x) '(51))
	     (equal (lookup ob (val q x))
		    (lookup ob (etMem (nr q x))) ) ) )

(lemma val=etMem-implied (rewrite)
    (implies (and (aq3a ob q x)
		  (kq5 q x)
                  (lq3 q x)
                  (mq2 ob q x)
                  (rq0 (sub1 (nr q x)) x)
		  (rq0 (nr q x) x)
		  (mnr=nr q x) )
	     (val=etMem ob q x) )
    ((enable aq3a kq5 lq3 mq2 mnr=nr rq0 val=etMem)) )

#| Part 6. Preparation of the proof of Yq0 |#

(defn nq0 (o x) 
    (or (member o (tlist (lookup o (owner x)) x))
	(equal (lookup o (db x))
	       (lookup o (lookup (gnr x) (hiMem x))) ) ) )

(prove-lemma nq0-list (rewrite)
    (implies (and (nq0 ob x)
		  (not (member (pc p x) '(0 41 50 51 52 31))) )
	     (nq0 ob (step p x)) )
    ((do-not-induct t)) )

(defn nq1 (ob q x)
    (implies (member ob (ownset q x))
	     (equal (lookup ob (owner x)) q) ) )

(defn nq2 (q x)
    (implies (listp (tlist q x))
	     (member (pc q x) '(51)) ) )

(defn nq3 (q x)
    (subset (tlist q x) (ownset q x)) )

(defn nq4 (ob q x)
    (implies (and (member ob (ownset q x))
		  (equal (pc q x) 51) )
	     (equal (lookup ob (pridb q x))
		    (lookup ob (lookup (gnr x) (hiMem x))) ) ) )

(defn process-ne-0 (x)
    (not (member 0 (processes x))) )

(prove-lemma nq0-at-41-52 (rewrite)
    (implies (and (nq0 ob x)
		  (nq2 p x)
		  (nq1 ob p x)
		  (member (pc p x) '(41 52)) )
	     (nq0 ob (step p x)) )
    ((do-not-induct t)) )

(prove-lemma nq0-at-50 (rewrite)
    (implies (and (nq0 ob x)
		  (nq1 ob p x)
		  (nq2 p x)
		  (equal (pc p x) 50) )
	     (nq0 ob (step p x)) )
    ((enable lookup lookup-putassoc* member-subset) (do-not-induct t)) )

(prove-lemma nq0-at-51 (rewrite)
    (implies (and (nq0 ob x)
		  (nq3 p x)
		  (nq4 ob p x)
		  (equal (pc p x) 51) )
	     (nq0 ob (step p x)) )
    ((enable subset lookup) (do-not-induct t)) )

(prove-lemma nq0-at-31 (rewrite)
    (implies (and (nq0 ob x)
		  (process-ne-0 x)
		  (equal (pc p x) 31) )
	     (nq0 ob (step p x)) )
    ((do-not-induct t)) )

(prove-lemma nq0-at-0 (rewrite)
    (implies (and (nq0 ob x)
		  (outside-pc p x)
		  (equal (pc p x) 0) )
	     (nq0 ob (step p x)) )
    ((do-not-induct t)) )

(lemma nq0-kept-valid (rewrite)
    (implies (and (nq0 ob x)
		  (nq3 p x)
		  (nq2 p x)
		  (nq1 ob p x)
		  (nq4 ob p x)
		  (outside-pc p x)
		  (process-ne-0 x) )
	     (nq0 ob (step p x)) )
    ((enable nq0-at-50 nq0-at-0 nq0-at-31 nq0-at-41-52 nq0-at-51)
     (use (nq0-list)) (do-not-induct t)) )

(prove-lemma nq1-list (rewrite)
    (implies (and (nq1 i q x)
		  (not (member (pc p x) '(41 52 31 32))) )
	     (nq1 i q (step p x)) )
    ((do-not-induct t)) )

(prove-lemma nq1-at-31 (rewrite)
    (implies (and (nq1 i q x)
		  (process-ne-0 x)
		  (equal (pc p x) 31) )
	     (nq1 i q (step p x)) )
    ((do-not-induct t)) )

(defn is-set (lis)
    (if (nlistp lis) t
      (and (is-set (cdr lis))
	   (not (member (car lis) (cdr lis))) ) ) )

(defn is-set-ownset (q x)
    (is-set (ownset q x)) )

(defn nq5 (q x)
    (implies (member (pc q x) '(32 33))
	     (equal (lookup (iob q x) (owner x)) q) ) )

(prove-lemma nq1-at-41-52 (rewrite)
    (implies (and (nq1 i q x)
		  (nq1 i p x)
		  (is-set-ownset q x)
		  (member (pc p x) '(41 52)) )
	     (nq1 i q (step p x)) )
    ((do-not-induct t)) )

(prove-lemma nq1-at-32 (rewrite)
    (implies (and (nq1 i q x)
		  (nq5 p x)
		  (equal (pc p x) 32) )
	     (nq1 i q (step p x)) )
    ((do-not-induct t)) )

(lemma nq1-kept-valid (rewrite)
    (implies (and (nq1 i q x)
		  (nq1 i p x)
		  (nq5 p x)
		  (is-set-ownset q x)
		  (process-ne-0 x) )
	     (nq1 i q (step p x)) )
    ((use (nq1-list)) (enable nq1-at-41-52 nq1-at-32 nq1-at-31)
     (do-not-induct t)) )

(prove-lemma is-set-ownset-kept-valid (rewrite)
    (implies (is-set-ownset q x)
	     (is-set-ownset q (step p x)) )
    ((do-not-induct t)) )

(prove-lemma nq2-kept-valid (rewrite)
    (implies (nq2 q x)
	     (nq2 q (step p x)) )
    ((do-not-induct t)) )

(enable-theory 
   (subset member-subset subset-extended subset-reflexive subset-append) )

(prove-lemma nq3-list (rewrite)
    (implies (and (nq3 q x)
		  (not (member (pc p x) '(41 52))) )
	     (nq3 q (step p x)) )
    ((do-not-induct t)) )

(prove-lemma nq3-at-41-52 (rewrite)
    (implies (and (nq3 q x)
		  (nq2 q x)
		  (member (pc p x) '(41 52)) )
	     (nq3 q (step p x)) )
    ((do-not-induct t)) )

(lemma nq3-kept-valid (rewrite)
    (implies (and (nq3 q x)
		  (nq2 q x) )
	     (nq3 q (step p x)) )
    ((use (nq3-list)) (enable nq3-at-41-52)
     (do-not-induct t)) )

(prove-lemma nq4-list (rewrite)
    (implies (and (nq4 ob q x)
		  (not (member (pc p x) '(50))) )
	     (nq4 ob q (step p x)) )
    ((do-not-induct t)) )

(prove-lemma nq4-at-50-dif (rewrite)
    (implies (and (nq4 ob q x)
		  (nq1 ob p x)
		  (nq1 ob q x)
		  (not (equal p q))
		  (equal (pc p x) 50) )
	     (nq4 ob q (step p x)) )
    ((enable lookup lookup-putassoc*) (do-not-induct t)) )

(prove-lemma nq4-at-50-eq (rewrite)
    (implies (and (nq4 ob p x)
		  (equal (pc p x) 50) )
	     (nq4 ob p (step p x)) )
    ((enable lookup lookup-putassoc*) 
     (do-not-induct t)) )

(lemma nq4-kept-valid (rewrite)
    (implies (and (nq4 ob q x)
		  (nq1 ob p x)
		  (nq1 ob q x) )
	     (nq4 ob q (step p x)) )
    ((use (nq4-list) (nq4-at-50-dif))
     (enable nq4-at-50-eq)
     (do-not-induct t)) )

(prove-lemma process-ne-0-kept-valid (rewrite)
    (implies (and (process-ne-0 x)
		  (not (equal p 0)) )
	     (process-ne-0 (step p x)) )
    ((do-not-induct t)) )

(prove-lemma nq5-list (rewrite)
    (implies (and (nq5 q x)
		  (not (member (pc p x) '(41 52 30 31))) )
	     (nq5 q (step p x)) )
    ((do-not-induct t)) )

(prove-lemma nq5-at-41-52 (rewrite)
    (implies (and (nq5 q x)
		  (nq1 (iob q x) p x)
		  (member (pc p x) '(41 52)) )
	     (nq5 q (step p x)) )
    ((do-not-induct t)) )

(prove-lemma nq5-at-30 (rewrite)
    (implies (and (nq5 q x)
		  (nq1 (car (inv q x)) p x)
		  (equal (pc p x) 30) )
	     (nq5 q (step p x)) )
    ((do-not-induct t)) )

(prove-lemma nq5-at-31 (rewrite)
    (implies (and (nq5 q x)
		  (process-ne-0 x)
		  (equal (pc p x) 31) )
	     (nq5 q (step p x)) )
    ((do-not-induct t)) )

(lemma nq5-kept-valid (rewrite)
    (implies (and (nq5 q x)
		  (process-ne-0 x)
		  (nq1 (iob q x) p x)
		  (nq1 (car (inv q x)) p x) )
	     (nq5 q (step p x)) )
    ((use (nq5-list)) (enable nq5-at-41-52 nq5-at-30 nq5-at-31)
     (do-not-induct t)) )

(defn pq0 (q x) 
    (implies (or (equal (pc q x) 21)
		 (and (equal (pc q x) 20)
		      (equal (inv q x) 'begin) ) )
             (nlistp (ownset q x)) ) )

(prove-lemma pq0-list (rewrite)
    (implies (and (pq0 q x)
		  (not (member (pc p x) '(10 19))) )
	     (pq0 q (step p x)) )
    ((enable norin) (do-not-induct t)) ) ; [ 0.0 0.3 0.1 ]

(prove-lemma pq0-at-19 (rewrite)
    (implies (and (pq0 q x)
		  (inside-prog q x)
		  (member (pc p x) '(19)) )
	     (pq0 q (step p x)) )
    ((do-not-induct t)) ) ; [ 0.0 0.3 0.1 ]

(prove-lemma pq0-at-10 (rewrite)
    (implies (and (pq0 q x)
		  (jq5 q x)
		  (member (pc p x) '(10)) )
	     (pq0 q (step p x)) )
    ((do-not-induct t)) ) ; [ 0.0 0.3 0.1 ]

(lemma pq0-kept-valid (rewrite)
    (implies (and (pq0 q x)
		  (jq5 q x)
		  (inside-prog q x) )
	     (pq0 q (step p x)) ) 
    ((use (pq0-list)) (enable pq0-at-19 pq0-at-10)
     (do-not-induct t)) )

(defn pq1 (q x)
    (implies (member (pc q x) '(41 42))
	     (equal (lookup (cnt q x) (hiSutno q x)) 0) ) )

(prove-lemma pq1-kept-valid (rewrite)
    (implies (pq1 q x)
	     (pq1 q (step p x)) )
    ((do-not-induct t)) )

(defn start=bot (q x) ; bq4
    (implies (member (pc q x) '(41 42))
	     (equal (start q x) 0) ) )

(lemma start=bot-implied (rewrite)
    (implies (and (lq2 q x)
		  (lq0 q x)
		  (pq1 q x)
		  (rq1 (cnt q x) q x) )
	     (start=bot q x) ) 
    ((enable rq1 lq2 lq0 pq1 start=bot)
     (do-not-induct t) ) )

(defn pq2 (q x)
    (not (and (equal (pc q x) 15)
	      (zerop (evf q x)) )) )

(defn pq3 (q x)
    (implies (and (not (member (pc q x) '(0 10)))
		  (zerop (evf q x)) )
	     (member (inv q x) '(abort end)) ) )

(lemma pq2-list (rewrite)
    (implies (and (pq2 q x)
		  (not (member (pc p x) '(14 21 33))) )
	     (pq2 q (step p x)) )
    ((enable pq2 evf-step res-step pc-step new-pc )
     (do-not-induct t) ) ) 

(lemma pq2-at-endings (rewrite)
    (implies (and (pq2 q x)
		  (pq3 q x)
		  (dq1 q x)
		  (kq2 q x)
		  (member (pc p x) '(21 33)) )
	     (pq2 q (step p x)) )
    ((enable pq3 pq2 evf-step res-step pc-step new-pc dq1 kq2 )
     (do-not-induct t) ) ) 

(lemma pq2-at-14 (rewrite)
    (implies (and (pq2 q x)
		  (inside-prog q x)
		  (member (pc p x) '(14)) )
	     (pq2 q (step p x)) )
    ((enable pq2 evf-step pc-step new-pc inside-prog )
     (do-not-induct t) ) ) 

(lemma pq2-kept-valid (rewrite)
    (implies (and (pq2 q x)
		  (dq1 q x)
		  (kq2 q x)
		  (inside-prog q x)
		  (pq3 q x) )
	     (pq2 q (step p x)) )
    ((enable pq2-at-endings pq2-at-14) 
     (use (pq2-list))
     (do-not-induct t) ) ) 

(lemma pq3-kept-valid (rewrite)
    (implies (pq3 q x)
	     (pq3 q (step p x)) )
    ((enable private-outside member-madd-to-set pq3 evf-step 
	     processes-step inv-step norin pc-step new-pc )
     (do-not-induct t) ) ) ; [ 0.0 0.3 0.0 ]

; to construct the list of nonzero keys that own objects
(defn strip-cdrs-nz (as)
    (cond ((nlistp as) nil)
	  ((equal (cdar as) 0) (strip-cdrs-nz (cdr as)))
	  (t (cons (cdar as) (strip-cdrs-nz (cdr as)))) ) )

(lemma lookup-strip-cdrs (rewrite)
    (implies (not (equal (cdr (assoc x as)) 0))
	     (member (cdr (assoc x as)) (strip-cdrs-nz as)) )
    ((enable strip-cdrs-nz)) )

(lemma subset-madd-to-set (rewrite)
    (implies (subset x y)
	     (subset x (madd-to-set a y)) )
    ((enable subset member-madd-to-set)) )

(lemma strip-cdrs-putassoc (rewrite)
    (implies (subset (strip-cdrs-nz as) ys)
	     (subset (strip-cdrs-nz (putassoc key w as))
		     (madd-to-set w ys) ) )
    ((enable member-madd-to-set subset strip-cdrs-nz putassoc)
     (do-not-generalize t) ) )

(lemma strip-cdrs-putassoc-0 (rewrite)
    (implies (subset (strip-cdrs-nz as) ys)
	     (subset (strip-cdrs-nz (putassoc key 0 as))
		     (madd-to-set w ys) ) )
    ((enable member-madd-to-set subset strip-cdrs-nz putassoc)
     (do-not-generalize t) ) )

(defn owners (x)
    (strip-cdrs-nz (owner x))) )

(lemma owner-in-owners (rewrite)
    (implies (not (equal (cdr (assoc ob (owner x))) 0))
	     (member (cdr (assoc ob (owner x))) (owners x)) )
    ((enable owners lookup-strip-cdrs)) )

(defn jq8 (x)
    (subset (owners x) (processes x)) )

(prove-lemma jq8-kept-valid (rewrite)
    (implies (jq8 x)
	     (jq8 (step p x)) )
    ((do-not-induct t)) ) 

; We turn towards the construction of the global forward invariant 
; First universal quantification over all objects 

(prove-lemma not-member-strip-cars (rewrite)
    (implies (not (member x (strip-cars alist)))
	     (equal (lookup x alist) 0) ) 
    ((enable lookup)) )

(defn jq1* (os x)
    (if (nlistp os) t
      (and (jq1 (car os) x)
	   (jq1* (cdr os) x) ) ) )

(lemma jq1*-implies-jq1-inside (rewrite)
    (implies (and (jq1* os x)
		  (member ob os) )
	     (jq1 ob x) )
    ((enable jq1*)) )

(lemma jq1-implied-outside (rewrite)
    (implies (not (member ob (strip-cars (owner x))))
	     (jq1 ob x) )
    ((enable not-member-strip-cars jq1)) )

(defn jq1+ (x)
    (jq1* (strip-cars (owner x)) x) )

(lemma jq1+-implies-jq1 (rewrite)
    (implies (jq1+ x)
	     (jq1 ob x) )
    ((enable jq1+ jq1*-implies-jq1-inside)
     (use (jq1-implied-outside)) ) )

(defn jq3* (os q x)
    (if (nlistp os) t
      (and (jq3 (car os) q x)
	   (jq3* (cdr os) q x) ) ) )

(lemma jq3*-implies-jq3-inside (rewrite)
    (implies (and (jq3* os q x)
		  (member ob os) )
	     (jq3 ob q x) )
    ((enable jq3*)) )

(lemma jq3-implied-outside (rewrite)
    (implies (not (member ob (strip-cars (owner x))))
	     (jq3 ob q x) )
    ((enable not-member-strip-cars jq3)) )

(defn jq3+ (q x)
    (jq3* (strip-cars (owner x)) q x) )

(lemma jq3+-implies-jq3 (rewrite)
    (implies (jq3+ q x)
	     (jq3 ob q x) )
    ((enable jq3+ jq3*-implies-jq3-inside)
     (use (jq3-implied-outside)) ) )

(lemma jq1*kept-valid (rewrite)
    (implies (and (jq1+ x)
		  (jq3+ p x)
		  (jq5 p x)
		  (jq0 p x) )
	     (jq1* os (step p x)) )
    ((enable jq1* jq1-kept-valid jq1+-implies-jq1 jq3+-implies-jq3 )) )

(lemma jq1+kept-valid (rewrite)
    (implies (and (jq1+ x)
		  (jq3+ p x)
		  (jq5 p x)
		  (jq0 p x) )
	     (jq1+ (step p x)) )
    ((enable jq1*kept-valid) (expand(jq1+ (step p x)))) )

(lemma jq3*kept-valid (rewrite)
    (implies (and (jq3+ q x)
		  (outside-pc q x) )
	     (jq3* os q (step p x)) )
    ((enable jq3* jq3-kept-valid jq3+-implies-jq3 )) )

(lemma jq3+kept-valid (rewrite)
    (implies (and (jq3+ q x)
		  (outside-pc q x) )
	     (jq3+ q (step p x)) )
    ((enable jq3*kept-valid) (expand(jq3+ q (step p x)))) )

(defn nq0* (os x)
    (if (nlistp os) t
      (and (nq0 (car os) x)
	   (nq0* (cdr os) x) ) ) )

(lemma nq0*-implies-nq0-inside (rewrite)
    (implies (and (nq0* os x)
		  (member ob os) )
	     (nq0 ob x) )
    ((enable nq0*)) )

(defn nq0+ (x)
    (nq0* (append (strip-cars (lookup (gnr x) (hiMem x)))
		  (strip-cars (db x)) )
	  x ) )

(lemma nq0-implied-outside (rewrite)
    (implies (not (member ob (append (strip-cars (lookup (gnr x) (hiMem x)))
				     (strip-cars (db x)) )))
	     (nq0 ob x) )
    ((enable member-append not-member-strip-cars nq0)) )

(lemma nq0+-implies-nq0 (rewrite)
    (implies (nq0+ x)
	     (nq0 ob x) )
    ((enable nq0+ nq0*-implies-nq0-inside)
     (use (nq0-implied-outside)) ) )

(defn nq1* (os q x)
    (if (nlistp os) t
      (and (nq1 (car os) q x)
	   (nq1* (cdr os) q x) ) ) )

(lemma nq1*-implies-nq1-inside (rewrite)
    (implies (and (nq1* os q x)
		  (member ob os) )
	     (nq1 ob q x) )
    ((enable nq1*)) )

(lemma nq1-implied-outside (rewrite)
    (implies (not (member ob (ownset q x)))
	     (nq1 ob q x) )
    ((enable not-member-strip-cars nq1)) )

(defn nq1+ (q x)
    (nq1* (ownset q x) q x) )

(lemma nq1+-implies-nq1 (rewrite)
    (implies (nq1+ q x)
	     (nq1 ob q x) )
    ((enable nq1+ nq1*-implies-nq1-inside)
     (use (nq1-implied-outside)) ) )

(defn nq4* (os q x)
    (if (nlistp os) t
      (and (nq4 (car os) q x)
	   (nq4* (cdr os) q x) ) ) )

(lemma nq4*-implies-nq4-inside (rewrite)
    (implies (and (nq4* os q x)
		  (member ob os) )
	     (nq4 ob q x) )
    ((enable nq4*)) )

(lemma nq4-implied-outside (rewrite)
    (implies (not (member ob (ownset q x)))
	     (nq4 ob q x) )
    ((enable not-member-strip-cars nq4)) )

(defn nq4+ (q x)
    (nq4* (ownset q x) q x) )

(lemma nq4+-implies-nq4 (rewrite)
    (implies (nq4+ q x)
	     (nq4 ob q x) )
    ((enable nq4+ nq4*-implies-nq4-inside)
     (use (nq4-implied-outside)) ) )

(lemma nq0*kept-valid (rewrite)
    (implies (and (nq0+ x)
		  (nq3 p x)
		  (nq2 p x)
		  (nq1+ p x)
		  (nq4+ p x)
		  (outside-pc p x)
		  (process-ne-0 x) )
	     (nq0* os (step p x)) )
    ((enable nq0* nq0-kept-valid nq0+-implies-nq0 nq1+-implies-nq1 
	     nq4+-implies-nq4 )) )

(lemma nq0+kept-valid (rewrite)
    (implies (and (nq0+ x)
		  (nq3 p x)
		  (nq2 p x)
		  (nq1+ p x)
		  (nq4+ p x)
		  (outside-pc p x)
		  (process-ne-0 x) )
	     (nq0+ (step p x)) )
    ((enable nq0*kept-valid) (expand(nq0+ (step p x)))) )

(lemma nq1*kept-valid (rewrite)
    (implies (and (nq1+ q x)
		  (nq1+ p x)
		  (nq5 p x)
		  (is-set-ownset q x)
		  (process-ne-0 x) )
	     (nq1* os q (step p x)) )
    ((enable nq1* nq1+-implies-nq1 nq1-kept-valid)) )

(lemma nq1+kept-valid (rewrite)
    (implies (and (nq1+ q x)
		  (nq1+ p x)
		  (nq5 p x)
		  (is-set-ownset q x)
		  (process-ne-0 x) )
	     (nq1+ q (step p x)) )
    ((enable nq1*kept-valid) (expand(nq1+ q (step p x)))) )

(lemma nq4*kept-valid (rewrite)
    (implies (and (nq4+ q x)
		  (nq1+ p x)
		  (nq1+ q x) )
	     (nq4* os q (step p x)) )
    ((enable nq4* nq1+-implies-nq1 nq4+-implies-nq4 nq4-kept-valid)) )

(lemma nq4+kept-valid (rewrite)
    (implies (and (nq4+ q x)
		  (nq1+ p x)
		  (nq1+ q x) )
	     (nq4+ q (step p x)) )
    ((enable nq4*kept-valid) (expand(nq4+ q (step p x)))) )

(defn mq1* (os q x)
    (if (nlistp os) t
      (and (mq1 (car os) q x)
	   (mq1* (cdr os) q x) ) ) )

(lemma mq1*-implies-mq1-inside (rewrite)
    (implies (and (mq1* os q x)
		  (member ob os) )
	     (mq1 ob q x) )
    ((enable mq1*)) )

(lemma mq1-implied-outside (rewrite)
    (implies (not (member ob (append (strip-cars (etMem (sub1 (mnr q x))))
				     (strip-cars (val q x)) )))
	     (mq1 ob q x) )
    ((enable not-member-strip-cars member-append mq1)) )

(defn mq1+ (q x)
    (mq1* (append (strip-cars (etMem (sub1 (mnr q x))))
		  (strip-cars (val q x)) )
	  q x) )

(lemma mq1+-implies-mq1 (rewrite)
    (implies (mq1+ q x)
	     (mq1 ob q x) )
    ((enable mq1+ mq1*-implies-mq1-inside)
     (use (mq1-implied-outside)) ) )

(lemma mq1*kept-valid (rewrite)
    (implies (and (mq1+ q x)
		  (outside-pc q x)
		  (lq5 q x) )
	     (mq1* os q (step p x)) )
    ((enable mq1* mq1+-implies-mq1 mq1-kept-valid)) )

(lemma mq1+kept-valid (rewrite)
    (implies (and (mq1+ q x)
		  (outside-pc q x)
		  (lq5 q x) )
	     (mq1+ q (step p x)) )
    ((enable mq1*kept-valid) (expand(mq1+ q (step p x)))) )

(defn mq2* (os q x)
    (if (nlistp os) t
      (and (mq2 (car os) q x)
	   (mq2* (cdr os) q x) ) ) )

(lemma mq2*-implies-mq2-inside (rewrite)
    (implies (and (mq2* os q x)
		  (member ob os) )
	     (mq2 ob q x) )
    ((enable mq2*)) )

(lemma mq2-implied-outside (rewrite)
    (implies (not (member ob 
			  (append 
			   (strip-cars (lookup (nr q x) (hiMem x)))
			   (append (strip-cars (lookup (sub1 (nr q x)) 
						       (hiMem x) ))
				   (strip-cars (pridb q x)) ) ) ))

	     (mq2 ob q x) )
    ((enable not-member-strip-cars member-append mq2)) )

(defn mq2+ (q x)
    (mq2* (append (strip-cars (lookup (nr q x) (hiMem x)))
		  (append (strip-cars (lookup (sub1 (nr q x)) 
					      (hiMem x) ))
			  (strip-cars (pridb q x)) ) )
	  q x) )

(lemma mq2+-implies-mq2 (rewrite)
    (implies (mq2+ q x)
	     (mq2 ob q x) )
    ((enable mq2+ mq2*-implies-mq2-inside)
     (use (mq2-implied-outside)) ) )

(lemma mq2*kept-valid (rewrite)
    (implies (and (mq2+ q x)
		  (lq3 q x)  
		  (numberp-gnr x) )
	     (mq2* os q (step p x)) )
    ((enable mq2* mq2+-implies-mq2 mq2-kept-valid)) )

(lemma mq2+kept-valid (rewrite)
    (implies (and (mq2+ q x)
		  (lq3 q x)  
		  (numberp-gnr x) )
	     (mq2+ q (step p x)) )
    ((enable mq2*kept-valid) (expand(mq2+ q (step p x)))) )

#| Construction of the global strong invariant  |#

(defn forwinvq (q x) 
    (and (dq0 q x)  (dq1 q x)  (kq1 q x)  (jq0 q x) 
	 (jq2 q x)  (jq3+ q x) (jq4a q x) (jq4b q x) 
	 (jq5 q x)  (pq1 q x)  (lq3 q x)  (inside-prog q x)
	 (kq0 q x)  (lq1 q x)  (lq1b q x) (lq2 q x)  (lq0 q x)
	 (mq0 q x)  (nq3 q x)  (nq2 q x)  (nq1+ q x) 
	 (nq4+ q x) (nq5 q x)  (kq5 q x)  (pq0 q x)  
	 (mq1+ q x) (lq5 q x)  (pq2 q x)  (pq3 q x)  
	 (kq4 q x)  (mq2+ q x) (kq2 q x)  (kq3 q x)  
	 (outside-pc q x) (good-invoc q x) (is-set-ownset q x) ) )

(prove-lemma jq3*-outside (rewrite)
    (implies (and (not (member q (processes x)))
		  (jq8 x) )
	     (jq3* oblist q x) ) 
    ((do-not-generalize t)
     (disable owners) ) )

(lemma mq1*-outside (rewrite)
    (implies (not (member q (processes x)))
	     (mq1* oblist q x) )
    ((enable private-outside mq1* mq1)) )

(lemma mq2*-outside (rewrite)
    (implies (not (member q (processes x)))
	     (mq2* oblist q x) )
    ((enable private-outside mq2* mq2)) )

(prove-lemma forwinvq-outside (rewrite)
    (implies (and (not (member q (processes x)))
		  (jq8 x) )
	     (forwinvq q x) )
    ((do-not-induct t)) )

(defn forwinvq* (plist x)
    (if (nlistp plist) t
      (and (forwinvq (car plist) x)
	   (forwinvq* (cdr plist) x) ) ) )

(lemma forwinvq*implies-forwinvq (rewrite)
    (implies (and (member q plist)
		  (forwinvq* plist x) )
	     (forwinvq q x) )
    ((enable forwinvq*)) ) 

(defn forwardinv (x)
    (and (forwinvq* (processes x) x)
	 (jq1+ x) (nq0+ x) (process-ne-0 x) 
	 (lq4 x)  (jq8 x)  (numberp-gnr x) ) )

(lemma forwardinv-implies-global (rewrite)
    (implies (forwardinv x)
	     (and (jq1+ x)  (nq0+ x)  (jq8 x)  (process-ne-0 x) 
		  (lq4 x)   (numberp-gnr x)    (forwinvq q x) ) )
    ((use (forwinvq*implies-forwinvq (plist (processes x))))
     (enable forwardinv forwinvq-outside) (do-not-induct t)) ) 

(lemma forwardinv-implies (rewrite)
    (implies (forwardinv x)
	     (and (dq0 q x)  (dq1 q x)  (jq0 q x)  (outside-pc q x)
		  (jq2 q x)  (jq3+ q x) (jq4a q x) (jq4b q x) 
		  (jq5 q x)  (pq1 q x)  (kq1 q x)  (inside-prog q x)
		  (kq0 q x)  (lq1 q x)  (lq1b q x) (lq2 q x)  (lq0 q x)  
		  (mq0 q x)  (nq3 q x)  (nq2 q x)  (nq1+ q x) 
		  (nq4+ q x) (nq5 q x)  (kq5 q x)  (lq3 q x) 
		  (mq1+ q x) (lq5 q x)  (pq2 q x)  (pq3 q x)  
		  (kq4 q x)  (mq2+ q x) (kq2 q x)  (kq3 q x)  (pq0 q x)  
		  (good-invoc q x) (kq5 q x) (is-set-ownset q x) ) )
    ((use (forwardinv-implies-global))
     (enable forwinvq) (do-not-induct t)) ) 

(lemma forwinvq-step (rewrite)
    (implies (and (forwardinv x)
		  (not (equal p 0)) )
	     (forwinvq q (step p x)) )
    ((enable forwardinv-implies forwinvq dq0-kept-valid  
	     dq1-kept-valid jq0-kept-valid jq2-kept-valid jq3+kept-valid 
	     jq4a-kept-valid jq4b-kept-valid jq5-kept-valid 
	     pq1-kept-valid lq2-kept-valid lq1-kept-valid  lq1b-kept-valid 
	     inside-prog-kept-valid forwardinv-implies-global
	     lq0-kept-valid kq1-kept-valid mq0-kept-valid nq3-kept-valid 
	     nq2-kept-valid nq4+kept-valid kq5-kept-valid kq3-kept-valid 
	     lq3-kept-valid is-set-ownset-kept-valid nq1+-implies-nq1 
	     mq1+kept-valid lq5-kept-valid pq2-kept-valid pq3-kept-valid 
	     kq4-kept-valid kq2-kept-valid pq0-kept-valid kq0-kept-valid 
	     mq2+kept-valid good-invoc-kept-valid nq5-kept-valid
	     nq1+kept-valid outside-pc-kept-valid jq8-kept-valid )
     (do-not-induct t) ) )

(lemma forwinvq*step (rewrite)
    (implies (and (forwardinv x)
		  (not (equal p 0)) )
	     (forwinvq* lis (step p x)) )
    ((enable forwinvq* forwinvq-step)) )

(lemma forwardinv-step (rewrite)
    (implies (and (forwardinv x)
		  (not (equal p 0)) )
	     (forwardinv (step p x)) )
    ((expand (forwardinv (step p x)))
     (enable forwinvq*step forwardinv-implies forwardinv-implies-global 
	     subset-reflexive jq1+kept-valid process-ne-0-kept-valid
	     nq0+kept-valid lq4-kept-valid jq8-kept-valid 
	     numberp-gnr-kept-valid )
     (do-not-induct t) ) )

#| The initial predicate |# 

(defn initpred (x)
    (and (equal (gnr x) 0)
	 (equal (strip-cars (hiMem x)) '(0))
	 (equal (lookup 0 (hiMem x)) (db x))
	 (nzero-under 1 (hiMem x))
	 (nlistp (processes x))
	 (nlistp (owner x)) ) ) 

(lemma init-forwinvq (rewrite)
    (implies (initpred x) 
	     (forwinvq q x) )
    ((enable owners strip-cdrs-nz subset initpred jq8)
     (use (forwinvq-outside))
     (do-not-induct t) ) )

(lemma init-forwinvq* (rewrite)
    (implies (initpred x)
	     (forwinvq* plist x) )
    ((enable init-forwinvq forwinvq*)) )

(lemma nq0*init (rewrite)
    (implies (and (equal (lookup 0 (hiMem x)) (db x))
		  (equal (gnr x) 0) )
	     (nq0* os x) )
    ((enable nq0* nq0)) )

(lemma init-forwardinv (rewrite)
    (implies (initpred x)
	     (forwardinv x) )
    ((enable initpred forwardinv init-forwinvq* nq0*init numberp-gnr lq4
	     jq1+ jq1* nq0+ process-ne-0 jq8 owners strip-cdrs-nz subset )
     (do-not-induct t) ) )

(lemma initpred-initstate (rewrite)
    (initpred (initstate))
    ((enable lookup initstate initpred gnr hiMem db nzero-under owner tlist
	     privstate db0-constraint processes)
     (do-not-induct t) ) )

(lemma forwardinv-ys (rewrite)
    (forwardinv (ys n))
    ((enable ys initpred-initstate forwardinv-step round-robin 
	     init-forwardinv )) )

(lemma dq0-dq1-dq2-dq4-dq5-ys (rewrite)
    (and (dq0 q (ys n))
	 (dq1 q (ys n))
	 (dq2 q (ys n))
	 (dq4 q (ys n))
	 (dq5 q (ys n)) )
    ((enable forwardinv-implies forwardinv-ys 
	     forwardinv-implies-global jq1+-implies-jq1 jq3+-implies-jq3
	     dq2-implied dq4-implied dq5-implied)) )

(lemma mnr=nr-implied-again (rewrite) ; aq0
    (implies (and (forwardinv x)
		  (rq1 (cnt q x) q x) )
	     (mnr=nr q x) )
    ((enable mnr=nr-implied forwardinv-implies )
     (do-not-induct t)) )

#| Part 7. Backward Invariants. |# 

(defn qzq1 (ob q x)
    (implies (member ob (ownset q x)) 
	     (or (equal (start q x) 0)
		 (member (pc q x) '(51 52))
		 (equal (lookup ob (lookup (gnr x) (hiMem x)))
			(lookup ob (etMem (sub1 (mnr q x)))) ) ) ) )

(prove-lemma qzq1-back-dif-list (rewrite)
    (implies (and (qzq1 ob q (step p x))
		  (not (equal p q))
		  (not (member (pc p x) '(50))) )
             (qzq1 ob q x) ) 
    ((do-not-induct t)) )

(lemma qzq1-back-dif-50 (rewrite)
    (implies (and (qzq1 ob q (step p x))
		  (nq1 ob p x)
		  (nq1 ob q x)
		  (not (equal p q))
		  (member (pc p x) '(50)) )
             (qzq1 ob q x) ) 
    ((enable qzq1 nq1 mnr-step pc-step new-pc hiMem-step start-step 
	     ownset-step lookup gnr-step lookup-putassoc*) 
     (do-not-induct t)) ) ; 

(lemma qzq1-back-dif (rewrite)
    (implies (and (qzq1 ob q (step p x))
		  (nq1 ob p x)
		  (nq1 ob q x)
		  (not (equal p q)) )
             (qzq1 ob q x) ) 
    ((enable qzq1-back-dif-50) (use (qzq1-back-dif-list))
     (do-not-induct t)) )

(prove-lemma qzq1-back-eq-list (rewrite)
    (implies (and (qzq1 ob p (step p x))
		  (not (member (pc p x) '(0 21 41 42 50 53))) )
             (qzq1 ob p x) ) 
    ((do-not-induct t)) )

(prove-lemma qzq1-back-eq-0-42-53 (rewrite)
    (implies (and (jq5 p x)
		  (member (pc p x) '(0 42 53)) )
             (qzq1 ob p x) ) 
    ((do-not-induct t)) ) ; [ 0.0 0.1 0.0 ]

(prove-lemma qzq1-back-eq-41 (rewrite)
    (implies (and (start=bot p x)
		  (member (pc p x) '(41)) )
             (qzq1 ob p x) ) 
    ((do-not-induct t)) ) ; [ 0.0 0.1 0.0 ]

(prove-lemma qzq1-back-eq-21 (rewrite)
    (implies (and (pq0 p x)
		  (member (pc p x) '(21)) )
             (qzq1 ob p x) ) 
    ((do-not-induct t)) ) ; [ 0.0 0.1 0.0 ]

(prove-lemma qzq1-back-eq-50 (rewrite)
    (implies (and (numberp-gnr x)
		  (lq1 p x)
		  (member (pc p x) '(50))
		  (rq1 (add1 (cnt p x)) p (step p x))
                  (rq0 (gnr x) x) )
             (qzq1 ob p x) ) 
    ((enable rq0 rq1) (do-not-induct t)) ) ; [ 0.1 0.1 0.0 ]

(lemma qzq1-back-eq (rewrite)
    (implies (and (qzq1 ob p (step p x))
		  (jq5 p x)
		  (pq0 p x)
		  (numberp-gnr x)
		  (lq1 p x)
		  (start=bot p x)
		  (rq1 (add1 (cnt p x)) p (step p x))
                  (rq0 (gnr x) x) )
             (qzq1 ob p x) ) 
    ((use (qzq1-back-eq-list))
     (enable qzq1-back-eq-0-42-53 qzq1-back-eq-41 
	     qzq1-back-eq-21 qzq1-back-eq-50 )
     (do-not-induct t)) ) ; 

(lemma qzq1-back-all (rewrite) ; (B1)
    (implies (and (qzq1 ob q (step p x))
		  (nq1 ob p x)
		  (nq1 ob q x)
		  (jq5 q x)
		  (pq0 q x)
		  (numberp-gnr x)
		  (lq1 q x)
		  (start=bot q x)
		  (rq1 (add1 (cnt q x)) q (step p x))
                  (rq0 (gnr x) x) )
             (qzq1 ob q x) ) 
    ((enable qzq1-back-eq) (use (qzq1-back-dif))
     (do-not-induct t)) )

(defn qzq0 (q x)
    (implies (and (not (equal (start q x) 0))
		  (equal (pc q x) 32) )
	     (equal (lookup (iob q x) 
			    (lookup (gnr x) (hiMem x)) )
		    (lookup (iob q x) 
			    (etMem (sub1 (mnr q x))) ) ) ) )

(prove-lemma qzq0-back-dif-list (rewrite)
    (implies (and (qzq0 q (step p x))
		  (not (equal p q))
		  (not (member (pc p x) '(50))) )
             (qzq0 q x) ) 
    ((do-not-induct t)) )

(prove-lemma qzq0-back-dif-50 (rewrite)
    (implies (and (qzq0 q (step p x))
		  (nq1 (iob q x) p x)
		  (nq5 q x)
		  (not (equal p q))
		  (member (pc p x) '(50)) )
             (qzq0 q x) ) 
    ((enable lookup-putassoc*) (do-not-induct t)) ) ; [ 0.0 0.6 0.0 ]

(lemma qzq0-back-dif (rewrite)
    (implies (and (qzq0 q (step p x))
		  (nq1 (iob q x) p x)
		  (nq5 q x)
		  (not (equal p q)) )
             (qzq0 q x) ) 
    ((use (qzq0-back-dif-list)) (enable qzq0-back-dif-50) 
     (do-not-induct t)) ) ;

(prove-lemma qzq0-back-eq-list (rewrite)
    (implies (and (qzq0 p (step p x))
		  (not (member (pc p x) '(32))) )
             (qzq0 p x) ) 
    ((do-not-induct t)) )

(lemma qzq0-back-eq-32 (rewrite)
    (implies (and (qzq1 (iob p x) p (step p x)) 
		  (member (pc p x) '(32)) )
             (qzq0 p x) ) 
    ((enable qzq1 qzq0 pc-step new-pc himem-step gnr-step mnr-step 
	     start-step ownset-step) 
     (do-not-induct t)) ) ; 

(lemma qzq0-back-eq (rewrite)
    (implies (and (qzq0 p (step p x))
		  (qzq1 (iob p x) p (step p x)) )
             (qzq0 p x) ) 
    ((enable qzq0-back-eq-32) (use (qzq0-back-eq-list))
     (do-not-induct t)) ) ; 

(lemma qzq0-back-all (rewrite) ; (B0)
    (implies (and (qzq0 q (step p x))
		  (nq1 (iob q x) p x)
		  (nq5 q x)
		  (qzq1 (iob q x) q (step p x)) )
             (qzq0 q x) ) 
    ((use (qzq0-back-dif)) (enable qzq0-back-eq) (do-not-induct t)) )

(defn val=db (q x) ; aq4
    (implies (and (not (equal (start q x) 0))
		  (equal (pc q x) 32) )
	     (equal (lookup (iob q x) (db x))
		    (lookup (iob q x) (val q x)) ) ) )

(lemma val=db-implied (rewrite)
    (implies (and (qzq0 q x)
		  (jq2 q x)
		  (mq1 (iob q x) q x)
		  (nq0 (iob q x) x)
		  (nq2 q x)
		  (nq5 q x) )
	     (val=db q x) )
    ((enable qzq0 nq0 mq1 nq5 nq2 jq2 val=db private-outside)
     (do-not-induct t) ) )

(lemma val=db-implied-again (rewrite) ; aq4
    (implies (and (qzq0 q x)
		  (forwardinv x) )
	     (val=db q x) )
    ((enable val=db-implied forwardinv-implies-global forwardinv-implies  
	     mq1+-implies-mq1 nq0+-implies-nq0 )
     (do-not-induct t) ) )

(prove-lemma yq0-list (rewrite)
    (implies (and (yq0 ob q x)
		  (not (member (pc p x) '(21 32 33))) )
	     (yq0 ob q (step p x)) )
    ((do-not-induct t)) )

(prove-lemma yq0-at-33 (rewrite)
    (implies (and (yq0 ob q x)
		  (member (pc p x) '(33)) )
	     (yq0 ob q (step p x)) )
    ((enable lookup) (do-not-induct t)) )

(prove-lemma yq0-at-21 (rewrite)
    (implies (and (yq0 ob q x)
		  (pq0 q x)
		  (member (pc p x) '(21)) )
	     (yq0 ob q (step p x)) )
    ((do-not-induct t)) )

(lemma yq0-at-32 (rewrite)
    (implies (and (yq0 ob q x)
		  (mq0 q x)
		  (val=db q x)
		  (member (pc p x) '(32)) )
	     (yq0 ob q (step p x)) )
    ((enable assoc-put yq0 mq0 val=db pridb-step val-step lookup
	     ownset-step) 
     (do-not-induct t)) )

(lemma yq0-kept-valid (rewrite)
    (implies (and (yq0 ob q x)
		  (val=db q x)
		  (pq0 q x)
		  (mq0 q x) )
	     (yq0 ob q (step p x)) )
    ((use (yq0-list)) (enable yq0-at-21 yq0-at-32 yq0-at-33)
     (do-not-induct t)) )

(lemma start=etMem-implied-again (rewrite) ; aq1
    (implies (and (forwardinv x)
		  (rq1 (cnt q x) q x) )
	     (start=etMem q x) )
    ((enable start=etMem-implied mnr=nr-implied-again forwardinv-implies )
     (do-not-induct t)) )

(lemma dq6-implied-again (rewrite)
    (implies (and (forwardinv x)
		  (yq1 q x)
		  (rq1 (cnt q x) q x) )
	     (dq6 q x) ) 
    ((enable dq6-implied forwardinv-implies start=etMem-implied-again )
     (do-not-induct t)) )

(lemma start-ne-bot-implied-again (rewrite) ; aq2
    (implies (and (forwardinv x)
		  (rq1 (cnt q x) q x)
		  (rq0 (sub1 (nr q x)) x) )
	     (start-ne-bot q x) )
    ((enable start-ne-bot-implied forwardinv-implies
	     forwardinv-implies-global start=etMem-implied-again )
     (do-not-induct t)) )

(lemma val=etMem-implied-again (rewrite)
    (implies (and (yq0 ob q x)
		  (forwardinv x)
		  (rq1 (cnt q x) q x)
		  (rq0 (sub1 (nr q x)) x)
		  (rq0 (nr q x) x) )
	     (val=etMem ob q x) )
    ((enable mnr=nr-implied-again aq3a-implied forwardinv-implies 
	     start-ne-bot-implied-again val=etMem-implied mq1+-implies-mq1 
	     mq2+-implies-mq2)) )

; Universal quantification over objects for yq0.

(defn yq0* (os q x)
    (if (nlistp os) t
      (and (yq0 (car os) q x)
	   (yq0* (cdr os) q x) ) ) )

(lemma yq0*-implies-yq0-inside (rewrite)
    (implies (and (yq0* os q x)
		  (member ob os) )
	     (yq0 ob q x) )
    ((enable yq0*)) )

(lemma yq0-implied-outside (rewrite)
    (implies (not (member ob (ownset q x)))
	     (yq0 ob q x) )
    ((enable not-member-strip-cars yq0)) )

(defn yq0+ (q x)
    (yq0* (ownset q x) q x) )

(lemma yq0+-implies-yq0 (rewrite)
    (implies (yq0+ q x)
	     (yq0 ob q x) )
    ((enable yq0+ yq0*-implies-yq0-inside)
     (use (yq0-implied-outside)) ) )

(lemma yq0*kept-valid (rewrite)
    (implies (and (yq0+ q x)
		  (val=db q x)
		  (pq0 q x)
		  (mq0 q x) )
	     (yq0* os q (step p x)) )
    ((enable yq0* yq0+-implies-yq0 yq0-kept-valid)) )

(lemma yq0+kept-valid (rewrite)
    (implies (and (yq0+ q x)
		  (val=db q x)
		  (pq0 q x)
		  (mq0 q x) )
	     (yq0+ q (step p x)) )
    ((enable yq0*kept-valid) (expand(yq0+ q (step p x)))) )

(defn val=etMem* (os q x)
    (if (nlistp os) t
      (and (val=etMem (car os) q x)
	   (val=etMem* (cdr os) q x) ) ) )

(lemma val=etMem*-implies-val=etMem-inside (rewrite)
    (implies (and (val=etMem* os q x)
		  (member ob os) )
	     (val=etMem ob q x) )
    ((enable val=etMem*)) )

(lemma val=etMem-implied-outside (rewrite)
    (implies (not (member ob (append (strip-cars (etMem (nr q x)))
				     (strip-cars (val q x)) )))
	     (val=etMem ob q x) )
    ((enable not-member-strip-cars member-append val=etMem)) )

(defn val=etMem+ (q x)
    (val=etMem* (append (strip-cars (etMem (nr q x)))
			(strip-cars (val q x)) )
		q x) )

(lemma val=etMem+-implies-val=etMem (rewrite)
    (implies (val=etMem+ q x)
	     (val=etMem ob q x) )
    ((enable val=etMem+ val=etMem*-implies-val=etMem-inside)
     (use (val=etMem-implied-outside)) ) )

(lemma val=etMem*implied (rewrite)
    (implies (and (yq0+ q x)
		  (forwardinv x)
		  (rq1 (cnt q x) q x)
		  (rq0 (sub1 (nr q x)) x)
		  (rq0 (nr q x) x) )
	     (val=etMem* os q x) )
    ((enable yq0+-implies-yq0 val=etMem-implied-again val=etMem*)) )

(lemma val=etMem+implied (rewrite)
    (implies (and (yq0+ q x)
		  (forwardinv x)
		  (rq1 (cnt q x) q x)
		  (rq0 (sub1 (nr q x)) x)
		  (rq0 (nr q x) x) )
	     (val=etMem+ q x) )
    ((enable val=etMem+ val=etMem*implied)) )

(lemma val=etMem+implies (rewrite)
    (implies (and (val=etMem+ q x)
		  (equal (pc q x) 51) )
	     (eqlis-lookup os (val q x) (etMem (nr q x))) )
    ((enable eqlis-lookup  val=etMem)
     (induct (eqlis-lookup os xs ys))
     (use (val=etMem+-implies-val=etMem (ob (car os))))
     (do-not-induct t) ) ) 

(lemma val=etMem+implies-aq3 (rewrite)
    (implies (val=etMem+ q x)
	     (aq3 q x) )
    ((enable aq3 eq-lookup val=etMem+implies)
     (do-not-induct t) ) ) 

(lemma aq3-implied (rewrite)
    (implies (and (yq0+ q x)
		  (forwardinv x)
		  (rq1 (cnt q x) q x)
		  (rq0 (sub1 (nr q x)) x)
		  (rq0 (nr q x) x) )
	     (aq3 q x) )
    ((enable val=etMem+implied val=etMem+implies-aq3)) )

(lemma qzq1-back-again (rewrite)
    (implies (and (qzq1 ob q (step p x));
		  (forwardinv x)
		  (rq0 (gnr x) x)
		  (rq1 (cnt q x) q x)
		  (rq1 (add1 (cnt q x)) q (step p x)) ) 
             (qzq1 ob q x) ) 
    ((enable qzq1-back-all forwardinv-implies forwardinv-implies-global 
	     start=bot-implied nq1+-implies-nq1 ) 
     (do-not-induct t)) )

(defn qzq1* (os q x)
    (if (nlistp os) t
      (and (qzq1 (car os) q x)
	   (qzq1* (cdr os) q x) ) ) )

(lemma qzq1*-implies-qzq1-inside (rewrite)
    (implies (and (qzq1* os q x)
		  (member ob os) )
	     (qzq1 ob q x) )
    ((enable qzq1*)) )

(lemma qzq1-implied-outside (rewrite)
    (implies (not (member ob (ownset q x)))
	     (qzq1 ob q x) )
    ((enable not-member-strip-cars qzq1)) )

(defn qzq1+ (q x)
    (qzq1* (ownset q x) q x) )

(lemma qzq1+-implies-qzq1 (rewrite)
    (implies (qzq1+ q x)
	     (qzq1 ob q x) )
    ((enable qzq1+ qzq1*-implies-qzq1-inside)
     (use (qzq1-implied-outside)) ) )

(lemma qzq1*back (rewrite)
    (implies (and (qzq1+ q (step p x));
		  (forwardinv x)
		  (rq0 (gnr x) x)
		  (rq1 (cnt q x) q x)
		  (rq1 (add1 (cnt q x)) q (step p x)) ) ;
             (qzq1* os q x) ) 
    ((induct (qzq1* os q x)) (do-not-induct t)
     (enable qzq1* qzq1+-implies-qzq1)
     (use (qzq1-back-again (ob (car os)))) ) )

(lemma qzq1+back (rewrite)
    (implies (and (qzq1+ q (step p x));
		  (forwardinv  x)
		  (rq0 (gnr x) x)
		  (rq1 (cnt q x) q x)
		  (rq1 (add1 (cnt q x)) q (step p x)) ) ;
             (qzq1+ q x) ) 
    ((do-not-induct t) (expand (qzq1+ q x))
     (enable qzq1*back) ) )

(lemma qzq0-back-again (rewrite)
    (implies (and (qzq0 q (step p x))
		  (forwardinv x)
		  (qzq1+ q (step p x)) )
             (qzq0 q x) ) 
    ((enable qzq0-back-all qzq1+-implies-qzq1 nq1+-implies-nq1 
	     forwardinv-implies )
     (do-not-induct t)) )

(lemma yq0+kept-valid-again (rewrite)
    (implies (and (yq0+ q x)
		  (qzq0 q x)
		  (forwardinv x) )
	     (yq0+ q (step p x)) )
    ((enable yq0+kept-valid forwardinv-implies val=db-implied-again)
     (do-not-induct t)) )

(lemma yq1-kept-valid-again (rewrite)
    (implies (and (yq1 q x)
		  (yq0+ q x)
		  (forwardinv x)
		  (rq0 (sub1 (nr q x)) x)
		  (rq0 (nr q x) x)
		  (rq1 (cnt q x) q x) )
	     (yq1 q (step p x)) )
    ((enable yq1-kept-valid forwardinv-implies aq3-implied )
     (do-not-induct t)) )

(lemma dq3-implied-again (rewrite)
    (implies (and (forwardinv x)
		  (yq0+ q x) )
	     (dq3 q x) )
    ((enable dq3-implied yq0+-implies-yq0 forwardinv-implies )
     (do-not-induct t)) )

(lemma initpred-implies-yq0-yq1 (rewrite)
    (implies (initpred x)
	     (and (yq0 ob q x)
		  (yq1 q x) ) )
    ((enable private-outside private-outside yq0 yq1 initpred)) )

(lemma initpred-implies-yq0* (rewrite)
    (implies (initpred x)
	     (yq0* os q x) )
    ((enable yq0* initpred-implies-yq0-yq1)) )

(lemma initpred-implies-yq0+ (rewrite)
    (implies (initpred x)
	     (yq0+ q x) )
    ((enable yq0+ initpred-implies-yq0*)) )

(lemma processes-initstate (rewrite)
    (equal (processes (initstate)) nil)
    ((enable processes initstate)) )

(lemma processes-ys (rewrite)
    (equal (processes (ys n))
	   (rr-reached n) )
    ((enable rr-reached ys processes-step processes-initstate)) )

#| Part 8. Progress |#

(defn vf0 (q x)
    (if (member (pc q x) '(10 15)) 0
      (difference 60 (pc q x)) ) )

(defn length (xs)
    (if (nlistp xs) 0
      (add1 (length (cdr xs))) ) )

(defn vf1 (q x)
    (if (member (pc q x) '(10 15 32 33))
	(vf0 q x)
      (plus (length (ownset q x)) (vf0 q x)) ) )

(defn vf2 (q x)
    (cond ((member (pc q x) '(20 50))
	   (plus (vf1 q x) (length (ownset q x))) )
	  ((equal (pc q x) 51)
	   (plus (vf1 q x) (length (tlist q x))) )
	  (t (vf1 q x)) ) )

(prove-lemma vf2-decreases (rewrite)
    (implies (and (inside-prog q x)
		  (not (member (pc q x) '(10 15))) )
	     (lessp (vf2 q (step q x)) (vf2 q x)) ) 
    ((do-not-induct t)) )

(lemma vf2-decreases-again (rewrite)
    (implies (and (forwardinv x)
		  (not (member (pc q x) '(10 15))) )
	     (lessp (vf2 q (step q x)) (vf2 q x)) ) 
    ((enable forwardinv-implies vf2-decreases)
     (do-not-induct t)) )

(prove-lemma vf2-dif (rewrite)
    (implies (not (equal p q))
	     (equal (vf2 q (step p x)) (vf2 q x)) ) 
    ((do-not-induct t)) )

#| The abstract theory vfsearch |#

(dcl postcondition (x))

(defn found (n lim) ; linear search with variable upper bound
    (if (lessp n lim) 
	(if (postcondition (fix n)) (fix n)
	  (found (add1 n) lim) )
      f )
    ((lessp (difference lim n))) )

(lemma post-found (rewrite)
    (implies (found n lim)
	     (postcondition (found n lim)) ) 
    ((enable found)) )

(lemma numberp-found (rewrite)
    (implies (found n lim)
	     (numberp (found n lim)) ) )

(lemma found-lessp (rewrite)
    (implies (found n lim)
	     (lessp (found n lim) lim) ) 
    ((enable found)) )

(lemma found-not-lessp (rewrite)
    (implies (found n lim)
	     (not (lessp (found n lim) n)) ) 
    ((enable found)) )

(lemma found-implies (rewrite)
    (implies (found n lim)
	     (and (not (lessp (found n lim) n))
		  (numberp (found n lim))
		  (lessp (found n lim) lim)
		  (postcondition (found n lim)) ) )
    ((enable post-found numberp-found found-lessp found-not-lessp )) )

(lemma found-first-0 (rewrite)
    (implies (and (lessp m (found n lim))
		  (not (lessp m n))
		  (numberp m) 
		  (numberp n) ) 
	     (not (postcondition m)) )
    ((enable found)) )

(lemma found-fix (rewrite)
    (equal (found (fix n) lim) 
	   (found n lim) )
    ((enable found)) )

(lemma found-first (rewrite)
    (implies (and (lessp m (found n lim))
		  (not (lessp m n))
		  (numberp m) ) 
	     (not (postcondition m)) )
    ((use (found-first-0 (n (fix n))))
     (enable found found-fix)
     (do-not-induct t) ) )

(lemma not-found-implies (rewrite)
    (implies (and (not (found n lim))
		  (lessp m lim)
		  (not (lessp m n)) 
		  (numberp n)
		  (numberp m) )
	     (not (postcondition m)) ) 
    ((enable found)) )

(constrain invar-axiom (rewrite)
    (and (implies (and (invar n)
		       (not (postcondition (add1 n))) )
		  (invar (add1 n)) )
	 (implies (invar n) (numberp n)) )
    ((invar (lambda (n) f))) )

(defn recurs1 (r m)
    (if (not (lessp r m)) 0
      (recurs1 r (sub1 m)) ) )

(lemma before-found-invar-0 (rewrite)
    (implies (and (invar k)
		  (not (lessp (add1 k) n))
		  (lessp m (found n lim))
		  (not (lessp m k))
		  (numberp m) )
	     (invar m) )
    ((induct (recurs1 k m))
     (use (found-first))
     (enable invar-axiom)
     (do-not-induct t) ) )

(lemma before-found-invar (rewrite)
    (implies (and (invar n)
		  (lessp m (found (add1 n) lim))
		  (not (lessp m n))
		  (numberp m) )
	     (invar m) )
    ((use (before-found-invar-0 (n (add1 n)) (k n)))
     (do-not-induct t) ) )

; a variant function to guarantee termination of unbounded linear search
(constrain vf-forw-axiom (rewrite)
    (and (implies (prec n)
		  (and (or (postcondition (add1 n))
			   (prec (add1 n)) )
		       (numberp n)
		       (numberp (vf n))
		       (not (equal (vf n) 0))
		       (not (lessp (vf n) (vf (add1 n))))
		       (implies (prec (forw n))
				(not (lessp (sub1 (vf (forw n)))
					    (vf (add1 (forw n))) )) ) ) )
	 (numberp (forw n))
	 (not (lessp (forw n) n)) )		 
    ((forw (lambda (n) (fix n))) ; next point where vf decreases
     (prec (lambda (n) f)) ; condition while searching is relevant
     (vf (lambda (n) 0)) #| variant function |# ) )

; dissection of the axiom into five cases
(lemma prec-post-axiom (rewrite)
    (implies (and (prec n)
		  (not (postcondition (add1 n))) )
	     (prec (add1 n)) )
    ((use (vf-forw-axiom))) )

(lemma vf-axiom-1 (rewrite)
    (implies (prec n)
	     (and (numberp n)
		  (numberp (vf n))
		  (not (equal (vf n) 0)) ) )
    ((enable vf-forw-axiom)) )

(lemma vf-axiom-2 (rewrite)
    (implies (prec n)
	     (not (lessp (vf n) (vf (add1 n)))) )
    ((enable vf-forw-axiom)) )

(lemma forw-axiom-1 (rewrite)
    (and (not (lessp (forw n) n))
	 (numberp (forw n)) )
    ((enable vf-forw-axiom)) )

(lemma forw-axiom-2 (rewrite)
    (implies (and (prec n)
		  (prec (forw n)) )
	     (not (lessp (sub1 (vf (forw n)))
			 (vf (add1 (forw n))) )) )
    ((use (vf-forw-axiom))
     (do-not-induct t) ) )

(lemma not-found-prec (rewrite)
    (implies (and (not (found r lim)) 
		  (prec r)
		  (not (lessp m r))
		  (lessp m lim)
		  (numberp m) )
	     (prec m) ) 
    ((induct (recurs1 r m))
     (enable vf-axiom-1 not-found-implies prec-post-axiom)
     (do-not-induct t) ) )

(lemma not-found-descending (rewrite)
    (implies (and (not (found r lim)) 
		  (prec r)
		  (lessp m lim)
		  (not (lessp m r))
		  (numberp m) )
	     (not (lessp (vf m) (vf (add1 m)))) )
    ((enable vf-axiom-2 not-found-prec not-found-implies)
     (do-not-induct t) ) )

(lemma not-found-descending-long (rewrite)
    (implies (and (not (found r lim)) 
		  (prec r)
		  (not (lessp lim p))
		  (lessp m p)
		  (not (lessp m r))
		  (numberp m) )
	     (not (lessp (vf m) (vf p))) ) 
    ((induct (recurs1 r p))
     (expand (plus 1 m))
     (enable not-found-descending)
     (do-not-induct t) ) )

(lemma leq-transitive ()
    (implies (and (not (lessp x y))
		  (not (lessp y z)) )
	     (not (lessp x z)) ) )

(lemma not-found-decreasing (rewrite)
    (implies (and (not (found r lim)) 
		  (prec r)
		  (lessp (forw n) lim)
		  (not (lessp n r))
		  (numberp n) )
	     (not (lessp (sub1 (vf n))
			 (vf (add1 (forw n))) )) )
    ((use (not-found-descending-long (m n) (p (forw n)))
	  (leq-transitive (x (sub1 (vf n)))
			  (y (sub1 (vf (forw n))))
			  (z (vf (add1 (forw n)))) )
	  (forw-axiom-2) )
     (enable not-found-prec forw-axiom-1 forw-axiom-2) 
     (do-not-induct t) ) )

(defn forw* (k n) 
    (if (zerop k) (fix n)
      (add1 (forw (forw* (sub1 k) n))) ) )

(lemma leq-forw* (rewrite)
    (not (lessp (forw* k n) n))
    ((enable forw*  forw-axiom-1)) )

(lemma not-found-decreasing* (rewrite)
    (implies (and (not (found r lim)) 
		  (prec r)
		  (lessp (forw* k n) lim)
		  (not (lessp n r))
		  (numberp n) )
	     (not (lessp (vf n)
			 (plus k (vf (forw* k n))) )) )
    ((enable forw-axiom-1 leq-forw* forw* not-found-prec 
	     not-found-decreasing)
     (use (vf-axiom-1 (n (forw* (sub1 k) n))) )
     (induct (forw* k n)) (do-not-induct t) ) )

(lemma lessp-aux ()
    (implies (and (not (lessp x (plus x y)))
		  (numberp y) )
	     (equal y 0) ) )

(defn leap (r)
    (found r (add1 (forw* (vf r) r))) )

(lemma prec-implies-found (rewrite)
    (implies (prec r)
	     (leap r) )
    ((use (not-found-decreasing* (lim (add1 (forw* (vf r) r)))
				 (n r) (k (vf r)) ) 
	  (lessp-aux (x (vf r)) (y (vf (forw* (vf r) r)))) )
     (enable leap leq-forw* not-found-prec vf-axiom-1)
     (do-not-induct t) ) )

(lemma prec-leap-to-postcondition (rewrite)
    (implies (prec r)
	     (and (not (lessp (leap r) r))
		  (numberp (leap r))
		  (postcondition (leap r)) ) )
    ((use (prec-implies-found)) 
     (enable leap found-implies)) )
    
#| Now for the applications |#

(defn environ (q n)
    (member (pc q (ys n)) '(0 10 15)) )

(defn found-environ (q n lim)
    (if (lessp n lim)
	(if (environ q (fix n)) (fix n)
	  (found-environ q (add1 n) lim) )
      f )
    ((lessp (difference lim n))) )

(defn atSystem (q n)
    (and (numberp n)
	 (not (member (pc q (ys n)) '(0 10 15))) ) )

(lemma atSystem-environ (rewrite)
    (implies (and (atSystem q n)
		  (not (environ q (add1 n))) )
	     (atSystem q (add1 n)) )
    ((enable member-madd-to-set processes-ys rr-reached processes-step 
	     atSystem environ pc-step ys new-pc)
     (do-not-induct t) ) )

(defn vf3 (q n)
    (vf2 q (ys n)) )

(lemma inside-prog-ys (rewrite)
    (inside-prog q (ys n)) 
    ((enable forwardinv-ys forwardinv-implies )) )

(lemma vf3-satis-1 (rewrite)
    (implies (atSystem q n)
	     (and (numberp n)
		  (numberp (vf3 q n))
		  (not (equal (vf3 q n) 0)) ) )
    ((enable vf3 vf2 vf1 vf0 atSystem  inside-prog )
     (use (inside-prog-ys))
     (do-not-induct t) ) )

(lemma vf3-satis-2 (rewrite)
    (implies (atSystem q n)
	     (not (lessp (vf3 q n) (vf3 q (add1 n)))) )
    ((enable forwardinv-ys vf2-decreases-again vf3 atSystem ys 
	     initpred-initstate init-forwardinv)
     (use (vf2-dif (x (ys n)) (p (round (add1 n)))))
     (do-not-induct t) ) )

(defn forward3 (q n)
    (if (member q (rr-reached n))
	(sub1 (next-robin q n))
      (fix n) ) )

(lemma forward3-satis-1 (rewrite)
    (and (not (lessp (forward3 q n) n))
	 (numberp (forward3 q n)) )
    ((enable forward3 rr-reached-lessp-next-robin)
     (do-not-induct t) ) )

(lemma forward3-satis-2 (rewrite)
    (implies (and (atSystem q n)
		  (atSystem q (forward3 q n)) )
	     (not (lessp (sub1 (vf3 q (forward3 q n)))
			 (vf3 q (add1 (forward3 q n))) )) )
    ((enable atSystem forward3 rr-reached-lessp-next-robin vf3 ys 
	     forwardinv-ys rr-reached-round-next-robin vf2-decreases-again 
	     processes-ys private-outside )
     (use (rr-reached-lessp-next-robin))
     (do-not-induct t) ) )

(defn forward3* (q k n) 
    (if (zerop k) (fix n)
      (add1 (forward3 q (forward3* q (sub1 k) n))) ) )

(defn to-environ (q r)
    (found-environ q r (add1 (forward3* q (vf3 q r) r))) )

(functionally-instantiate environ-to-environ (rewrite)
    (implies (atSystem q r)
	     (and (not (lessp (to-environ q r) r))
		  (numberp (to-environ q r))
		  (environ q (to-environ q r)) ) )
    prec-leap-to-postcondition
    ((prec (lambda (n) (atSystem q n)))
     (found (lambda (n lim) (found-environ q n lim)))
     (postcondition (lambda (n) (environ q n)))
     (vf (lambda (n) (vf3 q n)))
     (forw (lambda (n) (forward3 q n)))
     (forw* (lambda (k n) (forward3* q k n)))
     (leap (lambda (n) (to-environ q n))) )
    ((disable-theory t) (enable-theory ground-zero)
     (enable atSystem-environ vf3-satis-1 vf3-satis-2 forward3-satis-1 
	     forward3-satis-2 forward3* to-environ found-environ )
     (do-not-induct t)) ) )

(defn idle (q n) 
    (lessp (pc q (ys n)) 15) )

(defn found-idle (q n lim)
    (if (lessp n lim)
	(if (idle q (fix n)) (fix n)
	  (found-idle q (add1 n) lim) )
      f )
    ((lessp (difference lim n))) )

(defn approx-idle (q n)
    (and (numberp n)
	 (member (pc q (ys n)) '(20 40 41 42 50 51 52 53))
	 (member (inv q (ys n)) '(abort end)) ) )

(lemma approx-idle-idle (rewrite)
    (implies (and (approx-idle q n)
		  (not (idle q (add1 n))) )
	     (approx-idle q (add1 n)) )
    ((enable member-madd-to-set processes-ys rr-reached processes-step 
	     approx-idle idle pc-step ys new-pc inv-step res-step)
     (do-not-induct t) ) )

(lemma approx-idle-atSystem (rewrite)
    (implies (approx-idle q n)
	     (and (numberp n)
		  (numberp (vf3 q n))
		  (not (equal (vf3 q n) 0))
		  (not (lessp (vf3 q n) (vf3 q (add1 n))))
		  (implies (approx-idle q (forward3 q n))
			   (not (lessp (sub1 (vf3 q (forward3 q n)))
				       (vf3 q (add1 (forward3 q n))) )) ) ) )
    ((enable approx-idle atSystem vf3-satis-1 vf3-satis-2 forward3-satis-2)) )

(defn to-idle (q r)
    (found-idle q r (add1 (forward3* q (vf3 q r) r))) )

(functionally-instantiate approx-idle-to-idle (rewrite)
    (implies (approx-idle q r)
	     (and (not (lessp (to-idle q r) r))
		  (numberp (to-idle q r))
		  (idle q (to-idle q r)) ) )
    prec-leap-to-postcondition
    ((prec (lambda (n) (approx-idle q n)))
     (found (lambda (n lim) (found-idle q n lim)))
     (postcondition (lambda (n) (idle q n)))
     (vf (lambda (n) (vf3 q n)))
     (forw (lambda (n) (forward3 q n)))
     (forw* (lambda (k n) (forward3* q k n)))
     (leap (lambda (n) (to-idle q n))) )
    ((disable-theory t) (enable-theory ground-zero)
     (enable approx-idle-idle found-idle forward3-satis-1 to-idle 
	     approx-idle-atSystem forward3* )
     (do-not-induct t)) ) )

(defn busy (q n) 
    (not (or (idle q n)
	     (approx-idle q n) )) )

(defn vf4 (q n) 
    (add1 (evf q (ys n))) )

(lemma pc-initstate (rewrite)
    (equal (pc q (initstate)) 0)
    ((enable lookup initstate privstate pc)) )

(lemma vf4-satis-1 (rewrite)
    (implies (busy q n)
	     (and (numberp n)
		  (not (equal n 0))
		  (numberp (vf4 q n))
		  (not (equal (vf4 q n) 0)) ) )
    ((enable busy idle vf4 rr-reached ys pc-initstate)
     (do-not-induct t) ) )

(lemma vf4-satis-2 (rewrite)
    (implies (busy q n)
	     (not (lessp (vf4 q n) (vf4 q (add1 n)))) )
    ((enable busy idle vf4 evf-step ys private-outside)
     (do-not-induct t) ) )

(defn busy-to-environ (q n)
    (if (or (environ q n) 
	    (not (atSystem q n)) )
	(fix n)
      (to-environ q n) ) )

(lemma busy-to-environ-satis-1 (rewrite)
    (and (not (lessp (busy-to-environ q n) n))
	 (numberp (busy-to-environ q n)) )
    ((enable busy-to-environ environ-to-environ)) )

(lemma busy-implies (rewrite)
    (implies (and (busy q n)
		  (not (environ q n)) )
	     (atSystem q n) )
    ((enable busy environ atSystem rr-reached ys pc-initstate)
     (do-not-induct t) ) )

(lemma busy-busy-to-environ (rewrite)
    (implies (busy q n)
	     (environ q (busy-to-environ q n)) )
    ((enable vf4-satis-1 busy-to-environ busy-implies environ-to-environ)) )

(defn busy-env (q n)
    (and (busy q n)
	 (environ q n) ) )

(lemma pq2-ys (rewrite)
    (pq2 q (ys n))
    ((enable  forwardinv-ys forwardinv-implies)) )

(lemma busy-env-vf4-decreases-eq (rewrite)
    (implies (and (busy-env q n)
		  (equal (round (add1 n)) q) )
	     (not (lessp (sub1 (vf4 q n))
			 (vf4 q (add1 n)) )) )
    ((enable busy-env environ busy vf4 ys evf-step pq2
	     pc-initstate idle approx-idle )
     (use (pq2-ys)) (do-not-induct t) ) )
    
(lemma busy-env-invar (rewrite)
    (implies (and (busy-env q n)
		  (not (equal (round (add1 n)) q)) )
	     (busy-env q (add1 n)) )
    ((enable busy-env busy environ ys new-pc pc-initstate
	     processes-initstate idle approx-idle
	     pc-step processes-step member-madd-to-set inv-step res-step)
     (do-not-induct t) ) )
    
(defn found-process (q n lim)
    (if (lessp n lim) 
	(if (equal (round (fix n)) q)
	    (fix n)
	  (found-process q (add1 n) lim) )
      f )
    ((lessp (difference lim n))) )

(functionally-instantiate before-found-process-invar (rewrite)
    (implies (and (busy-env q n)
		  (lessp m (found-process q (add1 n) lim))
		  (not (lessp m n))
		  (numberp m) )
	     (busy-env q m) )
    before-found-invar
    ((found (lambda (n lim) (found-process q n lim)))
     (invar (lambda (n) (busy-env q n)))
     (postcondition (lambda (n) (equal (round (fix n)) q))) )
    ((enable ys) (do-not-induct t)) )

(functionally-instantiate not-found-process-implies (rewrite)
    (implies (and (not (found-process q n lim))
		  (lessp m lim)
		  (not (lessp m n)) 
		  (numberp n)
		  (numberp m) )
	     (not (equal (round (fix m)) q)) )
    not-found-implies 
    ((found (lambda (n lim) (found-process q n lim)))
     (postcondition (lambda (n) (equal (round (fix n)) q))) ) )

(functionally-instantiate found-process-implies (rewrite)
    (implies (found-process q n lim)
	     (and (not (lessp (found-process q n lim) n))
		  (numberp (found-process q n lim))
		  (lessp (found-process q n lim) lim)
		  (equal (round (fix (found-process q n lim))) q) ) )
    found-implies
    ((found (lambda (n lim) (found-process q n lim)))
     (postcondition (lambda (n) (equal (round (fix n)) q))) ) )

(defn next-process (q n)
    (found-process q (add1 n) (add1 (next-robin q n))) )

(lemma found-process-next-robin (rewrite)
    (implies (member q (processes (ys n)))
	     (next-process q n) )
    ((enable next-process rr-reached-round-next-robin rr-reached 
	     rr-reached-lessp-next-robin processes-ys )
     (use (not-found-process-implies (n (add1 n))
				     (m (next-robin q n))
				     (lim (add1 (next-robin q n))) ))
     (do-not-induct t) ) )

(lemma next-process-sat (rewrite)
    (implies (member q (processes (ys n)))
	     (and (lessp n (next-process q n))
		  (numberp (next-process q n)) 
		  (equal (round (next-process q n)) q) ) )
    ((enable next-process round-robin)
     (use (found-process-implies (n (add1 n)) 
				 (lim (add1 (next-robin q n))) )
	  (found-process-next-robin) )
     (do-not-induct t) ) )

(lemma busy-env-kept (rewrite)
    (implies (and (busy-env q n)
		  (lessp n (next-process q n)) )
	     (busy-env q (sub1 (next-process q n))) )
    ((enable next-process)
     (use (before-found-process-invar (m (sub1 (next-process q n)))
				      (lim (add1 (next-robin q n))) ))
     (do-not-induct t) ) )

(lemma busy-env-implies-processes (rewrite) 
    (implies (busy-env q n)
	     (member q (processes (ys n))) )
    ((enable busy-env busy idle private-outside)) )
    
(lemma busy-env-vf4-decreases (rewrite) 
    (implies (busy-env q n)
	     (not (lessp (sub1 (vf4 q (sub1 (next-process q n))))
			 (vf4 q (next-process q n)) )) )
    ((enable busy-env-implies-processes busy-env-kept next-process-sat) 
     (use (busy-env-vf4-decreases-eq (n (sub1 (next-process q n)))))
     (do-not-induct t) ) )

(defn forward4 (q n)
    (let ((bte (busy-to-environ q n)))
      (if (busy q bte)
	  (sub1 (next-process q bte))
	bte ) ) )

(lemma forward4-satis-1 (rewrite)
    (and (not (lessp (forward4 q n) n))
	 (numberp (forward4 q n)) )
    ((enable busy idle forward4 busy-to-environ-satis-1 next-process-sat)
     (use (private-outside (x (ys (busy-to-environ q n)))))
     (do-not-induct t) ) )

(lemma forward4-satis-2 (rewrite)
    (implies (and (busy q n)
		  (busy q (forward4 q n)) )
	     (not (lessp (sub1 (vf4 q (forward4 q n)))
			 (vf4 q (add1 (forward4 q n))) )) )
    ((enable forward4 busy next-process-sat busy-env-vf4-decreases 
	     busy-busy-to-environ busy-env idle)
     (use (private-outside (x (ys (busy-to-environ q n)))))
     (do-not-induct t) ) )

(defn forward4* (q k n) 
    (if (zerop k) (fix n)
      (add1 (forward4 q (forward4* q (sub1 k) n))) ) )

(defn found-almost-idle (q n lim)
    (if (lessp n lim)
	(if (busy q (fix n))
	    (found-almost-idle q (add1 n) lim) 
	  (fix n) )
      f )
    ((lessp (difference lim n))) )

(defn leap4 (q r)
    (found-almost-idle q r (add1 (forward4* q (vf4 q r) r))) )

(functionally-instantiate busy-leap-to-almost-idle (rewrite)
    (implies (busy q r)
	     (and (not (lessp (leap4 q r) r))
		  (numberp (leap4 q r))
		  (not (busy q (leap4 q r))) ) ) 
    prec-leap-to-postcondition
    ((prec (lambda (n) (busy q n)))
     (vf (lambda (n) (vf4 q n)))
     (forw (lambda (n) (forward4 q n)))
     (forw* (lambda (k n) (forward4* q k n)))
     (postcondition (lambda (n) (not (busy q n))))
     (found (lambda (n lim) (found-almost-idle q n lim)))
     (leap (lambda (n) (leap4 q n))) ) 
    ((disable-theory t) (enable-theory ground-zero)
     (enable forward4-satis-1 forward4-satis-2 forward4* vf4-satis-1 leap4
	      vf4-satis-2 found-almost-idle ) 
     (do-not-induct t) ) )
    
(defn going-idle (q n)
    (cond ((busy q n) (leap4 q n))
	  ((approx-idle q n) (to-idle q n))
	  (t (fix n)) ) )

(lemma going-idle-forward (rewrite)
    (and (not (lessp (going-idle q r) r))
	 (numberp (going-idle q r)) )
    ((enable going-idle busy-leap-to-almost-idle approx-idle-to-idle)) )

(lemma towards-almost-idle (rewrite)
    (implies (busy q r)
	     (not (busy q (going-idle q r))) )  
    ((enable going-idle busy-leap-to-almost-idle) 
     (do-not-induct t) ) )

(defn reaching-idle (q n)
    (cond ((idle q n) (fix n))
	  ((approx-idle q n) (to-idle q n))
	  ((idle q (going-idle q n)) (going-idle q n)) 
	  ((member q (processes (ys n))) 
	   (to-idle q (going-idle q n)) )
	  (t (fix n)) ) )

(lemma reaching-idle-forward (rewrite)
    (and (not (lessp (reaching-idle q r) r))
	 (numberp (reaching-idle q r)) )
    ((enable going-idle-forward reaching-idle busy approx-idle-to-idle )
     (use (towards-almost-idle))
     (do-not-induct t)) )

(lemma reaching-idle-idle (rewrite)
    (implies (member q (processes (ys r)))
	     (idle q (reaching-idle q r)) )  
    ((enable reaching-idle approx-idle-to-idle processes-ys rr-reached busy)
     (use (towards-almost-idle))
     (do-not-induct t) ) )

#| Part 9. Validity of the Backward Invariants |#

(lemma qzq1*at-idle-state (rewrite)
    (implies (and (lessp (pc q x) 15)
		  (inside-prog q x)
		  (jq5 q x) )
	     (qzq1* os q x) )
    ((enable inside-prog jq5 qzq1* qzq1)) )

(lemma qzq1+at-idle-state (rewrite)
    (implies (and (lessp (pc q x) 15)
		  (forwardinv x) )
	     (qzq1+ q x) )
    ((enable forwardinv-implies qzq1*at-idle-state qzq1+)) )

(lemma qzq1+at-idle (rewrite)
    (implies (idle q n)
	     (qzq1+ q (ys n)) )
    ((enable qzq1+at-idle-state idle forwardinv-ys)) )

(lemma qzq1+back-ys (rewrite)
    (implies (qzq1+ q (ys (add1 n)))
             (qzq1+ q (ys n)) )
    ((do-not-induct t) 
     (use (rq1-for-ys (i (cnt q (ys n))))
	  (rq1-for-ys (i (add1 (cnt q (ys n)))) (n (add1 n))) )
     (enable qzq1+back ys-step forwardinv-ys rq0-for-ys) ) )

(lemma qzq1*outside-state (rewrite)
    (implies (not (member q (processes x)))
	     (qzq1* os q x) )
    ((enable private-outside qzq1* qzq1)) )

(lemma qzq1+outside-state (rewrite)
    (implies (not (member q (processes x)))
	     (qzq1+ q x) )
    ((enable qzq1*outside-state qzq1+)) )

(constrain backward-axiom (rewrite)
    (and (implies (back (add1 n))
		  (back n) )
	 (implies (sufficient-back n)
		  (back n) )
	 (implies (not (sufficient-back n))
		  (and (back (jump n)) 
		       (numberp n) ) )
	 (numberp (jump n))
	 (not (lessp (jump n) n)) )
    ((back (lambda (n) t))
     (sufficient-back (lambda (n) t))
     (jump (lambda (n) (add1 n))) ) )

(defn recurs2 (i k)
    (if (lessp k i) t
      (recurs2 (add1 i) k) )
    ((lessp (difference (add1 k) i))) )

(lemma back-back (rewrite)
    (implies (and (back k)
		  (not (lessp k i))
		  (numberp k)
		  (numberp i) )
	     (back i) ) 
    ((induct (recurs2 i k)) 
     (enable backward-axiom)
     (do-not-induct t) ) )

(lemma sufficient-back-suffices (rewrite)
    (implies (sufficient-back i)
	     (back i) )
    ((enable backward-axiom)) )

(lemma back-theorem (rewrite)
    (back i) 
    ((enable back-back backward-axiom)
     (use (sufficient-back-suffices)
	  (back-back (k (jump i))))
     (do-not-induct t) ) )

(functionally-instantiate qzq1+ys (rewrite)
    (qzq1+ q (ys i))
    back-theorem 
    ((back (lambda (n) (qzq1+ q (ys n))))
     (sufficient-back (lambda (n) (not (member q (processes (ys n))))))
     (jump (lambda (n) (reaching-idle q n))) )
    ((disable-theory t) (enable-theory ground-zero)
     (use (qzq1+outside-state (x (ys n))))
     (enable qzq1+back-ys reaching-idle-idle reaching-idle-forward 
	     qzq1+at-idle processes-ys rr-reached) 
     (do-not-induct t)) )

(lemma qzq0-back-ys (rewrite)
    (implies (qzq0 q (ys (add1 n)))
             (qzq0 q (ys n)) )
    ((use  (qzq1+ys (i (add1 n))) )
     (enable qzq0-back-again ys-step qzq1+ys forwardinv-ys) 
     (do-not-induct t) ) )

(lemma qzq0-at-idle (rewrite)
    (implies (idle q n)
	     (qzq0 q (ys n)) )
    ((enable idle qzq0)) )

(lemma qzq0-outside-state (rewrite)
    (implies (not (member q (processes x)))
	     (qzq0 q x) )
    ((enable private-outside qzq0)) )

(functionally-instantiate qzq0-ys (rewrite)
    (qzq0 q (ys i))
    back-theorem 
    ((back (lambda (n) (qzq0 q (ys n))))
     (sufficient-back (lambda (n) (not (member q (processes (ys n))))))
     (jump (lambda (n) (reaching-idle q n))) )
    ((disable-theory t) (enable-theory ground-zero)
     (use (qzq0-outside-state (x (ys n))))
     (enable qzq0-back-ys reaching-idle-idle reaching-idle-forward 
	     qzq0-at-idle processes-ys rr-reached) 
     (do-not-induct t)) )

(lemma initpred-ys-0 (rewrite)
    (implies (zerop n)
	     (initpred (ys n)) )
    ((enable ys initpred-initstate)) )

(lemma yq0+ys (rewrite)
    (yq0+ q (ys n))
    ((enable qzq0-ys yq0+kept-valid-again initpred-implies-yq0+ 
	     initpred-ys-0 forwardinv-ys ys-step )
     (induct (ys n)) ) )

(lemma dq3-ys (rewrite)
    (dq3 q (ys n))
    ((enable dq3-implied-again  yq0+ys forwardinv-ys)
     (do-not-induct t)) )

(lemma start-ne-bot-ys (rewrite)
    (start-ne-bot q (ys n))
    ((enable start-ne-bot-implied-again rq0-for-ys rq1-for-ys 
	     forwardinv-ys)
     (do-not-induct t)) )

(lemma yq1-ys (rewrite)
    (yq1 q (ys n))
    ((enable yq0+ys yq1-kept-valid-again initpred-implies-yq0-yq1 
	     initpred-ys-0 forwardinv-ys rq0-for-ys rq1-for-ys ys-step )
     (induct (ys n)) ) )

(lemma dq6-ys (rewrite)
    (dq6 q (ys n))
    ((enable dq6-implied-again yq1-ys rq1-for-ys forwardinv-ys)
     (do-not-induct t)) )

#| Conclusion. An arbitrary behaviour xs is constructed from a given 
initial database db0 with axiom "db0-constraint", a scheduling function 
round with its fairness witness robin with axiom "round-robin", the oracle 
functions for nondeterminacy get$, newval$, inv$, and res$ constrained by 
"result-axiom". On top of this we only needed the choice functions eps-glob 
and eps-priv constrained by the choice axioms hilbert-global and 
hilbert-priv to construct eternity variables etMem and etSutno and a 
behaviour ys. We can now complete the proof that ys satisfies the
relational specification. |#

(lemma ys-sdinext (rewrite)
    (sdinext (round (add1 n)) (ys n) (ys (add1 n)))
    ((enable ys-dq* dq* dq0-dq1-dq2-dq4-dq5-ys dq3-ys dq6-ys)
     (do-not-induct t) ) )

(make-lib "sdi")

#| Overview.
line   17  Part 1. The Algorithm with Auxiliary Variables
line  833  Part 2. The Semantic Lemmas
line 1450  Part 3. Specification and Proof Obligations
line 1964  Part 4. Forward Invariants
line 2364  Part 5. The proofs of Dq3 and Dq6 under assumption of Yq0
line 2716  Part 6. Preparation of the proof of Yq0, 
                   construction and initialization of global invariant
line 3590  Part 7. Backward Invariants
line 4079  Part 8. Progress
line 4777  Part 9. Validity of the Backward Invariants
line 4945  End |#