;;;-*-Lisp-*-

;; An important fact about sel/store: the order of disjoint stores
;; doesn't matter.
;(FORALL (s i vi j vj k)
;  (IMPLIES
;   (NEQ i j)
;   (FORALL (k) (EQ (select (store (store s i vi) j vj) k)
;		   (select (store (store s j vj) i vi) k)))))

;; By extensionality, I will therefore assume
;(BG_PUSH
; (FORALL (s i vi j vj)
;   (IMPLIES
;    (NEQ i j)
;    (EQ (store (store s i vi) j vj) (store (store s j vj) i vi))))
; )


;;; abs-queue.simp

(BG_PUSH
 ;; Forget about normal forms!
 ;; We will consider EmptyQ, singleton, and concat as the constructors.
 ;; All the non-constructors will be defined over these constructors. 

 ;; As distinct constructors that are normal forms, they are distinct.
 (FORALL (v) (NEQ (singleton v) EmptyQ))
 (FORALL (q1 q2)
   (PATS (NEQ (concat q1 q2) EmptyQ))
   (IMPLIES (NEQ q1 EmptyQ) (NEQ (concat q1 q2) EmptyQ)))
 (FORALL (q1 q2)
   (PATS (NEQ (concat q1 q2) EmptyQ))
   (IMPLIES (NEQ q2 EmptyQ) (NEQ (concat q1 q2) EmptyQ)))

 ;; EmptyQ is a left and right identity for concat.
 (FORALL (q) (EQ (concat q EmptyQ) q))
 (FORALL (q) (EQ (concat EmptyQ q) q))

 ;; concat is associative.
 (FORALL (q1 q2 q3) (EQ (concat q1 (concat q2 q3))
			(concat (concat q1 q2) q3)))

 ;; Define pushL and pushR
 (FORALL (q v)
   (PATS (pushL q v))
   (EQ (pushL q v) (concat (singleton v) q)))
 (FORALL (q v)
   (PATS (pushR q v))
   (EQ (pushR q v) (concat q (singleton v))))

 ;; Now define the peek observers, peekR and peekL.  Neither is defined on
 ;; empty queues.
 (FORALL (v)
   (PATS (peekR (singleton v)))
   (EQ (peekR (singleton v)) v))
 (FORALL (q1 q2)
   (PATS (peekR (concat q1 q2)))
   (IMPLIES (NEQ q2 EmptyQ)
	    (EQ (peekR (concat q1 q2)) (peekR q2))))

 (FORALL (v)
   (PATS (peekL (singleton v)))
   (EQ (peekL (singleton v)) v))
 (FORALL (q1 q2)
   (PATS (peekL (concat q1 q2)))
   (IMPLIES (NEQ q1 EmptyQ)
	    (EQ (peekL (concat q1 q2)) (peekL q1))))

 ;; Now we define "pop" mutators.
 (FORALL (v)
   (PATS (popR (singleton v)))
   (EQ (popR (singleton v)) EmptyQ))
 (FORALL (q1 q2)
   (PATS (popR (concat q1 q2)))
   (IMPLIES (NEQ q2 EmptyQ)
	    (EQ (popR (concat q1 q2)) (concat q1 (popR q2))))) 

 (FORALL (v)
   (PATS (popL (singleton v)))
   (EQ (popL (singleton v)) EmptyQ))
 (FORALL (q1 q2)
   (PATS (popL (concat q1 q2)))
   (IMPLIES (NEQ q1 EmptyQ)
	    (EQ (popL (concat q1 q2)) (concat (popL q1) q2))))

 ;; We define a len function, for use in induction.
 (EQ (len EmptyQ) 0)
 (FORALL (v) (EQ (len (singleton v)) 1))
 (FORALL (q1 q2)
   (PATS (len (concat q1 q2)))
   (EQ (len (concat q1 q2)) (+ (len q1) (len q2))))
)

(>= (len EmptyQ) 0)
(FORALL (v) (>= (len (singleton v)) 0))
(FORALL (q1 q2)
  (IMPLIES (AND (>= (len q1) 0)
		(>= (len q2) 0))
	   (>= (len (concat q1 q2)) 0)))

;; Therefore we can assume by data type induction:
(BG_PUSH
 (FORALL (q) (PATS (len q)) (>= (len q) 0)))

;; Here are our concrete variables:
;;  The fields of a node (each of which is a map, indexed by node
;;  values):
;;    left: Node
;;    left_del: Bool
;;    right: Node
;;    right_del: Bool
;;    value: {sentL, sentR, NullVal, Val}
;;  
;; In addition, we have an auxiliary (aka "ghost" or "abstract") variable
;; that represents the sequence of concrete nodes relevant to the current
;; state of the system.  This will be a map indexed by integers, and two 
;; integer indices indicating the left and right indices of the used
;; parts of the sequence.

(BG_PUSH
 (DISTINCT sentL sentR NullVal))

(DEFPRED (IsVal v)
  (AND
   (NEQ v sentL)
   (NEQ v sentR)
   (NEQ v NullVal)))

(DEFPRED (RepInv left left_del right right_del value l r s)
  (AND
   ;; We'll talk first about the sequence of nodes.
   (LBL RgtL (> r l))

   ;; The left and right elements are the sentinels.
   (LBL LeftSent
     (AND
      (EQ (select s l) SL)
      (EQ (select value SL) sentL)))
   (LBL RightSent
     (AND
      (EQ (select s r) SR)
      (EQ (select value SR) sentR)))

   ;; All elements of the sequence are distinct.
   (LBL DistinctNodes
     (FORALL (i j)
       (IMPLIES
	(AND (>= i l) (<= i r) (>= j l) (<= j r)
	     ;; Below is a way to say i < j, and i and j are ints.
	     (<= (+ i 1) j)
	     )
	(NEQ (select s i) (select s j)))))

   ;; The right pointers point forward in the sequence.
   (LBL RightPointers
     (FORALL (i)
       (IMPLIES
	(AND (>= i l) (< i r))
	(EQ (select right (select s i)) (select s (+ i 1)))))
     )

   ;; And the left pointers point backwards.
   (LBL LeftPointers
     (FORALL (i)
       (IMPLIES
	(AND (> i l) (<= i r))
	(EQ (select left (select s i)) (select s (- i 1))))))

   ;(LBL OnlyRSentinelCanHaveLDeletedBitSet
   ;(FORALL (i)
   ;(IMPLIES
   ;(AND (>= i l) (< i r))
   ;(NEQ (select left_del (select s i)) 1))))

   ;(LBL OnlyLSentinelCanHaveRDeletedBitSet
   ;(FORALL (i)
   ;(IMPLIES
   ;(AND (> i l) (<= i r))
   ;(NEQ (select right_del (select s i)) 1))))

   (LBL LeftDeletedNodeHasNullVal
     (IMPLIES
      (EQ (select left_del SR) 1)
      (EQ (select value (select left SR)) NullVal)))
	  
   (LBL RightDeletedNodeHasNullVal
     (IMPLIES
      (EQ (select right_del SL) 1)
      (EQ (select value (select right SL)) NullVal)))

   (LBL NullLeftValImpliesDeletedLeftOrRight
     (IMPLIES
      (EQ (select value (select right SL)) NullVal)
      (OR (EQ (select right_del SL) 1)
	  (AND (EQ (select left SR)
		   (select right SL))
	       (EQ (select left_del SR) 1)
	       (NEQ (select right_del SL) 1)
	       ))))

   (LBL NullRightValImpliesDeletedRightOrLeft
     (IMPLIES
      (EQ (select value (select left SR)) NullVal)
      (OR (EQ (select left_del SR) 1)
	  (AND (EQ (select right SL)
		   (select left SR))
	       (EQ (select right_del SL) 1)
	       (NEQ (select left_del SR) 1)
	       ))))

   ;; There are four cases, depending on deletion status.
   (LBL NonDelNonSentNodesHaveRealValsA
     (FORALL (k)
       (PATS (select value (select s k)))
       (IMPLIES
	(AND
	 (NEQ (select right_del SL) 1)
	 (NEQ (select left_del SR) 1)
	 (> k l) (< k r)
	 )
	(IsVal (select value (select s k))))))

   (LBL NonDelNonSentNodesHaveRealValsB
     (FORALL (k)
       (PATS (select value (select s k)))
       (IMPLIES
	(AND
	 (NEQ (select right_del SL) 1)
	 (EQ (select left_del SR) 1)
	 (> k l) (< k (- r 1))
	 )
	(IsVal (select value (select s k))))))
   (LBL NonDelNonSentNodesHaveRealValsC
     (FORALL (k)
       (PATS (select value (select s k)))
       (IMPLIES
	(AND
	 (EQ (select right_del SL) 1)
	 (NEQ (select left_del SR) 1)
	 (> k (+ l 1)) (< k r)
	 )
	(IsVal (select value (select s k))))))

   (LBL NonDelNonSentNodesHaveRealValsD
     (FORALL (k)
       (PATS (select value (select s k)))
       (IMPLIES
	(AND
	 (EQ (select right_del SL) 1)
	 (EQ (select left_del SR) 1)
	 (> k (+ l 1)) (< k (- r 1))
	 )
	(IsVal (select value (select s k))))))

   ))

;; Now we axiomatize the abstraction function.
(BG_PUSH
 ;; Define AbsFuncContig (this version takes value, to translate nodes to
 ;; values.
 (FORALL (s i j value)
   (IMPLIES (<= j i)
   (EQ (AbsFuncContig s i j value) EmptyQ)))
 ;; We introduce AbsFuncContigRest here to control the matching...
 (FORALL (i j s value)
   (PATS (AbsFuncContig s i j value))
   (IMPLIES (< i j)
	    (EQ (AbsFuncContig s i j value)
		(pushR (AbsFuncContigRest s i (- j 1) value)
		       (select value (select s (- j 1)))))))
 ;; ...but it's really just another name for the same function.
 (FORALL (i j s value)
   (PATS (AbsFuncContig s i j value))
   (EQ (AbsFuncContig s i j value) (AbsFuncContigRest s i j value)))

 (FORALL (s i value)
   (EQ (AbsFuncContigRest s i i value) EmptyQ))

 ;; Now define AbsFunc in terms of AbsFuncContig.
 ;; There are 4 definitions, depending on the deleted bits.
 (FORALL (s l r left_del right_del value)
   (PATS (AbsFunc s l r left_del right_del value))
   (IMPLIES
    (AND (NEQ (select right_del SL) 1)
	 (NEQ (select left_del SR) 1))
    (EQ (AbsFunc s l r left_del right_del value)
	(AbsFuncContig s (+ l 1) r value))))
 
 (FORALL (s l r left_del right_del value)
   (PATS (AbsFunc s l r left_del right_del value))
   (IMPLIES
    (AND (NEQ (select right_del SL) 1)
	 (EQ (select left_del SR) 1))
    (EQ (AbsFunc s l r left_del right_del value)
	(AbsFuncContig s (+ l 1) (- r 1) value))))
 
 (FORALL (s l r left_del right_del value)
   (PATS (AbsFunc s l r left_del right_del value))
   (IMPLIES
    (AND (EQ (select right_del SL) 1)
	 (NEQ (select left_del SR) 1))
    (EQ (AbsFunc s l r left_del right_del value)
	(AbsFuncContig s (+ l 2) r value))))
 
 (FORALL (s l r left_del right_del value)
   (PATS (AbsFunc s l r left_del right_del value))
   (IMPLIES
    (AND (EQ (select right_del SL) 1)
	 (EQ (select left_del SR) 1))
    (EQ (AbsFunc s l r left_del right_del value)
	(AbsFuncContig s (+ l 2) (- r 1) value))))
) 

;; Finally (I hope!) we need a rule that exposes the left side of an
;; AbsFuncContig; namely the fact in the next BG_PUSH.  We prove this
;; by induction.

;; Base case
(FORALL (i s value)
  (IMPLIES (AND (>= i 0) (< i (+ (+ i 1) 0)))
	   (EQ (AbsFuncContig s i (+ (+ i 1) 0) value)
	       (pushL (AbsFuncContigRest s (+ i 1) (+ (+ i 1) 0) value)
		      (select value (select s i))))))
(FORALL (n)
  (IMPLIES
   (AND (>= n 0)
	(FORALL (i j s)
	  (PATS (AbsFuncContigRest s i j value))
	  (IMPLIES (AND (< i j) (<= (- j i) n))
		   (EQ (AbsFuncContigRest s i j value)
		       (pushL (AbsFuncContigRest s (+ i 1) j value)
			      (select value (select s i)))))))
   (FORALL (s i)
     (EQ (AbsFuncContig s i (+ i (+ n 1)) value)
	 (pushL (AbsFuncContig s (+ i 1) (+ i (+ n 1)) value)
		(select value (select s i)))))
   ))

;; Since the above is true for all n, we can assume the general form.
(BG_PUSH
 (FORALL (i j s value)
   (PATS (AbsFuncContig s i j value))
   (IMPLIES (< i j)
	    (EQ (AbsFuncContig s i j value)
		(pushL (AbsFuncContigRest s (+ i 1) j value)
		       (select value (select s i))))))
)

(BG_PUSH
 (FORALL (s l r i v value)
   (IMPLIES (AND (>= r l) (OR (< i l) (>= i r)))
	    (EQ (AbsFuncContig (store s i v) l r value)
		(AbsFuncContig s l r value))))

 ;; And we assume the same thing for AbsFuncContigRest.
 (FORALL (s l r i v value)
   (IMPLIES (AND (>= r l) (OR (< i l) (>= i r)))
	    (EQ (AbsFuncContigRest (store s i v) l r value)
		(AbsFuncContigRest s l r value))))

 )

;; We wish to prove the formula in the next BG_PUSH.
;; We do so by induction over the difference between j and i.

(FORALL (left left_del right right_del value l r s)
  (IMPLIES
   (RepInv left left_del right right_del value l r s)
   (FORALL (i k v)
     (PATS (AbsFuncContigRest s i (+ i 0) (store value (select s k) v)))
     (IMPLIES
      (AND
       (<= l i) (< i r)
       (<= l k) (< k r)
       (<= i k)
       )
      (EQ (AbsFuncContigRest s i (+ i 0) (store value (select s k) v))
	  (AbsFuncContigRest s i (+ i 0) value))))))

(LBL InductionStep
  (FORALL (left left_del right right_del value l r s)
    (IMPLIES
     (RepInv left left_del right right_del value l r s)
     (FORALL (n)
       (IMPLIES
	(FORALL (i j k v)
	  (PATS (AbsFuncContigRest s i j (store value (select s k) v)))
	  (IMPLIES
	   (AND
	    (<= l i) (< i r)
	    (<= l j) (< j r)
	    (<= l k) (< k r)
	    (<= i j)
	    (<= j k)
	    (< (- j i) n)
	    )
	   (EQ (AbsFuncContigRest s i j (store value (select s k) v))
	       (AbsFuncContigRest s i j value))))
	(FORALL (i k v)
	  (IMPLIES
	   (AND
	    (<= l i) (< i r)
	    (<= l (+ i n)) (< (+ i n) r)
	    (<= l k) (< k r)
	    (<= i (+ i n))
	    (<= (+ i n) k)
	    )
	   (EQ (AbsFuncContig s i (+ i n) (store value (select s k) v))
	       (AbsFuncContig s i (+ i n) value))))))))
  )

;; Therefore we are justified in assuming the theorem for all n.
(BG_PUSH
 (FORALL (left left_del right right_del value l r s)
   (IMPLIES
    (RepInv left left_del right right_del value l r s)
    (FORALL (i j k v)
      (PATS (AbsFuncContigRest s i j (store value (select s k) v)))
      (IMPLIES
       (AND
	(<= l i) (< i r)
	(<= l j) (< j r)
	(<= l k) (< k r)
	(<= i j)
	(<= j k)
	)
       (EQ (AbsFuncContigRest s i j (store value (select s k) v))
	   (AbsFuncContigRest s i j value))))))
 )


;; True iff:
;;   "newNode" is distinct from all elements of the seqence (l r s)
;;   newNode.value == v
;;   newNode.left == leftPtr
;;   newNode.right == rightPtr
;;   NOT newNode.left_del
;;   NOT newNode.right_del
(DEFPRED (NewWRTSeq newNode l r s
		    value v
		    left leftPtr
		    right rightPtr
		    left_del right_del)
  (AND
   (FORALL (i)
     (IMPLIES (AND (>= i l) (<= i r))
	      (NEQ (select s i) newNode)))
   (EQ (select value newNode) v)
   (EQ (select left newNode) leftPtr)
   (EQ (select right newNode) rightPtr)
   (NEQ (select left_del newNode) 1)
   (NEQ (select right_del newNode) 1)
   ))


;; VC's:

;; Prove that the initial configuration satisfies the rep invariant
;; and corresponds to an empty abstract queue.

;; The initial conditions:
;; SL # SR
;; l = 0
;; r = 1
;; s = (store (store AnyS 0 SL) 1 SR)
;; left = (store AnyLeft SR SL)
;; left_del = (store AnyLeftDel SR 0)
;; right = (store AnyRight SL SR)
;; right_del = (store AnyRightDel SL 0)
;; value = (store (store AnyVal SL sentL) SR sentR)

(FORALL (AnyS AnyLeft AnyLeftDel AnyRight AnyRightDel AnyVal)
  (IMPLIES
   (NEQ SL SR)
   (AND
    (RepInv
     (store AnyLeft SR SL)
     (store (store AnyLeftDel SR 0) SL 0)
     (store AnyRight SL SR)
     (store (store AnyRightDel SL 0) SR 0)
     (store (store AnyVal SL sentL)
	    SR sentR)
     0 1 (store (store AnyS 0 SL) 1 SR))
    (EQ 
     (AbsFunc 
      (store (store AnyS 0 SL) 1 SR)
      0 1
     (store (store AnyLeftDel SR 0) SL 0)
     (store (store AnyRightDel SL 0) SR 0)
     (store (store AnyVal SL sentL)
	    SR sentR))
     EmptyQ)
    )))

;; pushR -- DCAS at line 16, return at line 18.
(FORALL (left left_del right right_del value l r s newR v)
  (IMPLIES
   (AND
    (RepInv left left_del right right_del value l r s)
    (IsVal v)
    (NEQ (select left_del SR) 1) ;; Confirmed by DCAS
    (NewWRTSeq newR l r s value v
	       left (select left SR)
	       right SR
	       left_del right_del)
    )
   (AND
    (LBL RepInvPreserved
      (RepInv (store left SR newR)
	      left_del
	      (store right (select left SR) newR)
	      right_del
	      value
	      l (+ r 1)
	      (store (store s (+ r 1) SR)
		     r newR)))
    (LBL ProperTransition
      (EQ (AbsFunc 
	   (store (store s (+ r 1) SR) r newR)
	   l (+ r 1)
	   left_del right_del value)
	  (pushR (AbsFunc s l r left_del right_del value) v))
      )
    )))


;; popR -- read at line 3; return at line 5
(FORALL (left left_del right right_del value l r s)
  (IMPLIES
   (AND
    (RepInv left left_del right right_del value l r s)
    (EQ (select value (select left SR)) sentL)
    )
   (EQ (AbsFunc s l r left_del right_del value) EmptyQ)))

;; popR -- DCAS at line 9; return at line 11
(FORALL (left left_del right right_del value l r s)
  (IMPLIES
   (AND
    (RepInv left left_del right right_del value l r s)
    (EQ (select value (select left SR)) NullVal)
    (NEQ (select left_del SR) 1)
    )
   (EQ (AbsFunc s l r left_del right_del value) EmptyQ)))

;; popR -- DCAS at line 16; return at line 18
(FORALL (left left_del right right_del value l r s)
  (IMPLIES
   (AND
    (NEQ (select value (select left SR)) sentL)
    (RepInv left left_del right right_del value l r s)
    (NEQ (select value (select left SR)) NullVal)
    (NEQ (select left_del SR) 1)
    )
   (AND
    (LBL RepInvPreserved
      (RepInv left
	      (store left_del SR 1)
	      right
	      right_del
	      (store value (select left SR) NullVal)
	      l r s)
      )
    (LBL Precondition
      (NEQ (AbsFunc s l r left_del right_del value) EmptyQ)
      )
    (LBL ProperTransition
      (EQ (AbsFunc 
	   s
	   l r
	   (store left_del SR 1)
	   right_del
	   (store value (select left SR) NullVal)
	   )
	  (popR (AbsFunc s l r left_del right_del value)))
      )
    (LBL ProperReturnVal
      (EQ (select value (select left SR))
	  (peekR (AbsFunc s l r left_del right_del value)))
      )
    )))

;; pushL -- DCAS at line 16, return at line 18.
(FORALL (left left_del right right_del value l r s newL v)
  (IMPLIES
   (AND
    (RepInv left left_del right right_del value l r s)
    (IsVal v)
    (NEQ (select right_del SL) 1) ;; Confirmed by DCAS
    (NewWRTSeq newL l r s value v
	       left SL
	       right (select right SL)
	       left_del right_del)
    )
   (AND
    (LBL RepInvPreserved
      (RepInv (store left (select right SL) newL)
	      left_del
	      (store right SL newL)
	      right_del
	      value
	      (- l 1) r
	      (store (store s (- l 1) SL) l newL)))
    (LBL ProperTransition
      (EQ (AbsFunc 
	   (store (store s (- l 1) SL) l newL)
	   (- l 1) r
	   left_del right_del value)
	  (pushL (AbsFunc s l r left_del right_del value) v))
      )
    )))


;; popL -- read at line 3; return at line 5
(FORALL (left left_del right right_del value l r s)
  (IMPLIES
   (AND
    (RepInv left left_del right right_del value l r s)
    (EQ (select value (select left SR)) sentL)
    )
   (EQ (AbsFunc s l r left_del right_del value) EmptyQ)))

;; popL -- DCAS at line 9; return at line 11
(FORALL (left left_del right right_del value l r s)
  (IMPLIES
   (AND
    (RepInv left left_del right right_del value l r s)
    (EQ (select value (select left SR)) NullVal)
    (NEQ (select left_del SR) 1)
    )
   (EQ (AbsFunc s l r left_del right_del value) EmptyQ)))

;; popL -- DCAS at line 16; return at line 18
(FORALL (left left_del right right_del value l r s)
  (IMPLIES
   (AND
    (NEQ (select value (select left SR)) sentL)
    (RepInv left left_del right right_del value l r s)
    (NEQ (select value (select left SR)) NullVal)
    (NEQ (select left_del SR) 1)
    )
   (AND
    (LBL RepInvPreserved
      (RepInv left
	      (store left_del SR 1)
	      right
	      right_del
	      (store value (select left SR) NullVal)
	      l r s)
      )
    (LBL Precondition
      (NEQ (AbsFunc s l r left_del right_del value) EmptyQ)
      )
    (LBL ProperTransition
      (EQ (AbsFunc 
	   s
	   l r
	   (store left_del SR 1)
	   right_del
	   (store value (select left SR) NullVal)
	   )
	  (popR (AbsFunc s l r left_del right_del value)))
      )
    (LBL ProperReturnVal
      (EQ (select value (select left SR))
	  (peekR (AbsFunc s l r left_del right_del value)))
      )
    )))

;; deleteRight -- read at line 3; return at line 4.  Nothing to prove.
 
;; deleteRight -- DCAS at line 11; return at line 13.
(FORALL (left left_del right right_del value l r s)
  (IMPLIES
   (AND
    (RepInv left left_del right right_del value l r s)
    (EQ (select left_del SR) 1)
    (EQ (select right (select left (select left SR)))
	(select left SR))
    )
   (AND
    (LBL RepInvPreserved
      (RepInv
       (store left SR
	      (select left (select left SR)))
       (store left_del SR 0)
       (store right (select left (select left SR))
	      SR)
       (store right_del
	      (select left (select left SR)) 0)
       value
       l
       (- r 1)
       (store s (- r 1) SR))
      )
    (LBL AbsValPreserved
      (EQ (AbsFunc 
	   (store s (- r 1) SR)
	   l
	   (- r 1)
	   (store left_del SR 0)
	   (store right_del
                  (select left (select left SR)) 0)
	   value)
	  (AbsFunc s l r left_del right_del value))
      )
    )))

;; deleteRight -- DCAS at line 23; return at line 25.
(FORALL (left left_del right right_del value l r s)
  (IMPLIES
   (AND
    (RepInv left left_del right right_del value l r s)
    (EQ (select left_del SR) 1)
    (EQ (select value (select left (select left SR))) NullVal)
    (EQ (select right_del SL) 1)
    )
   (AND
    (LBL RepInvPreserved
      (RepInv (store left SR SL)
	      (store left_del SR 0)
	      (store right SL SR)
	      (store right_del SL 0)
	      value
	      0
	      1
	      (store (store s 0 SL) 1 SR))
      )
    (LBL AbsValPreserved
      (EQ (AbsFunc 
	   (store (store s 0 SL) 1 SR)
	   0
	   1
	   (store left_del SR 0)
	   (store right_del SL 0)
	   value)
	  (AbsFunc s l r left_del right_del value))
      )
    )))

;; deleteLeft -- read at line 3; return at line 4.  Nothing to prove.
 
;; deleteLeft -- DCAS at line 11; return at line 13.
(FORALL (left left_del right right_del value l r s)
  (IMPLIES
   (AND
    (RepInv left left_del right right_del value l r s)
    (EQ (select right_del SL) 1)
    (NEQ (select value (select right (select right SL))) NullVal)
    (EQ (select left (select right (select right SL)))
	(select right SL))
    )
   (AND
    (LBL RepInvPreserved
      (RepInv (store left (select right (select right SL))
		     SL)
	      (store left_del (select right (select right SL)) 0)
	      (store right SL
		     (select right (select right SL)))
	      (store right_del SL 0)
	      value
	      (+ l 1)
	      r
	      (store s (+ l 1) SL))
      )
    (LBL AbsValPreserved
      (EQ (AbsFunc 
	   (store s (+ l 1) SL)
	   (+ l 1)
	   r
	   (store left_del (select right (select right SL)) 0)
	   (store right_del SL 0)
	   value)
	  (AbsFunc s l r left_del right_del value))
      )
    )))

;; deleteLeft -- DCAS at line 23; return at line 25.
(FORALL (left left_del right right_del value l r s)
  (IMPLIES
   (AND
    (RepInv left left_del right right_del value l r s)
    (EQ (select right_del SL) 1)
    (EQ (select value (select right (select right SL))) NullVal)
    (EQ (select left_del SR) 1)
    )
   (AND
    (LBL RepInvPreserved
      (RepInv (store left SR SL)
	      (store left_del SR 0)
	      (store right SL SR)
	      (store right_del SL 0)
	      value
	      0
	      1
	      (store (store s 0 SL) 1 SR))
      )
    (LBL AbsValPreserved
      (EQ (AbsFunc 
	   (store (store s 0 SL) 1 SR)
	   0
	   1
	   (store left_del SR 0)
	   (store right_del SL 0)
	   value)
	  (AbsFunc s l r left_del right_del value))
      )
    )))