;(in-package "ACL2")

(include-book "data-structures/structures" :dir :system)


(defstructure rb key value color left right)
    
(defun rb-rotate (a1 a2 a3 t1 t2 t3 t4)
  (rb (rb-key a2) (rb-value a2) 'red
      (rb (rb-key a1) (rb-value a1) 'black t1 t2)
      (rb (rb-key a3) (rb-value a3) 'black t3 t4)))

(defun rb-balance-left-case-1 (tree)
#|
  (rb-rotate (rb-left (rb-left tree))
	     (rb-left tree)
	     tree
	     (rb-left (rb-left (rb-left tree)))
	     (rb-right (rb-left (rb-left tree)))
	     (rb-right (rb-left tree))
	     (rb-right tree))
|#
  (let* ((a3 tree)
	 (a2 (rb-left a3))
	 (a1 (rb-left a2))
	 (t1 (rb-left a1))
	 (t2 (rb-right a1))
	 (t3 (rb-right a2))
	 (t4 (rb-right a3)))
    (rb (rb-key a2) (rb-value a2) 'red
	(rb (rb-key a1) (rb-value a1) 'black t1 t2)
	(rb (rb-key a3) (rb-value a3) 'black t3 t4)))
)

(defun rb-balance-left-case-2 (tree)
#|
  (rb-rotate (rb-left tree)
	     (rb-right (rb-left tree))
	     tree
	     (rb-left (rb-left tree))
	     (rb-left (rb-right (rb-left tree)))
	     (rb-right (rb-right (rb-left tree)))
	     (rb-right tree))
|#
  (let* ((a3 tree)
	 (a1 (rb-left a3))
	 (a2 (rb-right a1))
	 (t1 (rb-left a1))
	 (t2 (rb-left a2))
	 (t3 (rb-right a2))
	 (t4 (rb-right a3)))
    (rb (rb-key a2) (rb-value a2) 'red
	(rb (rb-key a1) (rb-value a1) 'black t1 t2)
	(rb (rb-key a3) (rb-value a3) 'black t3 t4)))
  )

(defun rb-balance-left (tree)
  (cond ((or (not (rb-p tree))
	     (equal (rb-color tree) 'red)
	     (not (rb-p (rb-left tree)))
	     (not (equal (rb-color (rb-left tree)) 'red)))
	 tree)
	((and (rb-p (rb-left (rb-left tree)))
	      (equal (rb-color (rb-left (rb-left tree))) 'red))
	 (rb-balance-left-case-1 tree))
	((and (rb-p (rb-right (rb-left tree)))
	      (equal (rb-color (rb-right (rb-left tree))) 'red))
	 (rb-balance-left-case-2 tree))
	(t tree)))
    
(defun rb-balance-right-case-1 (tree)
#|
  (rb-rotate tree
	     (rb-left (rb-right tree))
	     (rb-right tree)
	     (rb-left tree)
	     (rb-left (rb-left (rb-right tree)))
	     (rb-right (rb-left (rb-right tree)))
	     (rb-right (rb-right tree)))
|#
  (let* ((a1 tree)
	 (a3 (rb-right a1))
	 (a2 (rb-left a3))
	 (t1 (rb-left a1))
	 (t2 (rb-left a2))
	 (t3 (rb-right a2))
	 (t4 (rb-right a3)))
    (rb (rb-key a2) (rb-value a2) 'red
	(rb (rb-key a1) (rb-value a1) 'black t1 t2)
	(rb (rb-key a3) (rb-value a3) 'black t3 t4)))
  )

(defun rb-balance-right-case-2 (tree)
#|
  (rb-rotate tree
	     (rb-right tree)
	     (rb-right (rb-right tree))
	     (rb-left tree)
	     (rb-left (rb-right tree))
	     (rb-left (rb-right (rb-right tree)))
	     (rb-right (rb-right (rb-right tree))))
|#
  (let* ((a1 tree)
	 (a2 (rb-right a1))
	 (a3 (rb-right a2))
	 (t1 (rb-left a1))
	 (t2 (rb-left a2))
	 (t3 (rb-left a3))
	 (t4 (rb-right a3)))
    (rb (rb-key a2) (rb-value a2) 'red
	(rb (rb-key a1) (rb-value a1) 'black t1 t2)
	(rb (rb-key a3) (rb-value a3) 'black t3 t4)))
  )

(defun rb-balance-right (tree)
  (cond ((or (not (rb-p tree))
	     (equal (rb-color tree) 'red)
	     (not (rb-p (rb-right tree)))
	     (not (equal (rb-color (Rb-right tree)) 'red)))
	 tree)
	((and (rb-p (rb-left (rb-right tree)))
	      (equal (rb-color (rb-left (rb-right tree))) 'red))
	 (rb-balance-right-case-1 tree))
	((and (rb-p (rb-right (rb-right tree)))
	      (equal (rb-color (rb-right (rb-right tree))) 'red))
	 (rb-balance-right-case-2 tree))
	(t tree)))
    
(defun rb-insert-aux (key value tree)
  (cond ((not (rb-p tree))
	 (rb key value 'red nil nil))
	((equal key (rb-key tree))
	 (update-rb tree :value value))
	((lexorder key (rb-key tree))
	 (rb-balance-left (update-rb tree
                                     :left (rb-insert-aux key 
                                                          value
                                                          (rb-left tree)))))
	(t
	 (rb-balance-right (update-rb tree
                                      :right (rb-insert-aux key
                                                            value
                                                            (rb-right tree)))))))

(defun rb-insert (key value tree)
  (update-rb (rb-insert-aux key value tree) :color 'black))
    
(defun rb-lookup (key tree)
  (cond ((not (rb-p tree))
         nil)
        ((equal key (rb-key tree))
         (rb-value tree))
        ((lexorder key (rb-key tree))
         (rb-lookup key (rb-left tree)))
        (t
         (rb-lookup key (rb-right tree)))))
    
(defun min-lexorder (a b)
  (if (lexorder a b) a b))

(defun tree-min (tree)
  (if (rb-p tree)
      (if (and (rb-p (rb-left tree))
               (rb-p (rb-right tree)))
          (min-lexorder (rb-key tree) 
			(min-lexorder (tree-min (rb-left tree))
				      (tree-min (rb-right tree))))
        (if (rb-p (rb-left tree))
            (min-lexorder (rb-key tree)
			  (tree-min (rb-left tree)))
          (if (rb-p (rb-right tree))
              (min-lexorder (rb-key tree)
			    (tree-min (rb-right tree)))
            (rb-key tree))))
    nil))
    
(defun max-lexorder (a b)
  (if (lexorder a b) b a))

(defun tree-max (tree)
  (if (rb-p tree)
      (if (and (rb-p (rb-left tree))
               (rb-p (rb-right tree)))
          (max-lexorder (rb-key tree) 
			(max-lexorder (tree-max (rb-left tree))
				      (tree-max (rb-right tree))))
        (if (rb-p (rb-left tree))
            (max-lexorder (rb-key tree)
			  (tree-max (rb-left tree)))
          (if (rb-p (rb-right tree))
              (max-lexorder (rb-key tree)
			    (tree-max (rb-right tree)))
            (rb-key tree))))
    nil))
    
(defun strict-lexorder (a b)
  (if (equal a b)
      nil
    (lexorder a b)))

(defun ordered-tree-p (tree)
  (if (rb-p tree)
      (and (ordered-tree-p (rb-left tree))
           (ordered-tree-p (rb-right tree))
           (or (not (rb-p (rb-left tree)))
               (strict-lexorder (tree-max (rb-left tree)) (rb-key tree)))
           (or (not (rb-p (rb-right tree)))
               (strict-lexorder (rb-key tree) (tree-min (rb-right tree)))))
    t))
    

(defthm tree-min-lexorder-tree-max
  (lexorder (tree-min tree) (tree-max tree)))

(defthm ordered-max-left-lexorder-min-right
  (implies (and (ordered-tree-p tree)
		(rb-p tree)
		(rb-p (rb-left tree))
		(rb-p (rb-right tree)))
	   (and (not (equal (tree-max (rb-left tree))
			    (tree-min (rb-right tree))))
		(lexorder (tree-max (rb-left tree))
			  (tree-min (rb-right tree))))))

(defthm ordered-min-left-lexorder-min-right
  (implies (and (ordered-tree-p tree)
		(rb-p tree)
		(rb-p (rb-left tree))
		(rb-p (rb-right tree)))
	   (and (not (equal (tree-min (rb-left tree))
			    (tree-min (rb-right tree))))
		(lexorder (tree-min (rb-left tree))
			  (tree-min (rb-right tree)))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance tree-min-lexorder-tree-max
			    (tree (rb-left tree)))
		 (:instance ordered-max-left-lexorder-min-right))
	   :in-theory (disable tree-min-lexorder-tree-max
			       ordered-max-left-lexorder-min-right))))

(defthm ordered-min-left-lexorder-max-right
  (implies (and (ordered-tree-p tree)
		(rb-p tree)
		(rb-p (rb-left tree))
		(rb-p (rb-right tree)))
	   (and (not (equal (tree-min (rb-left tree))
			    (tree-max (rb-right tree))))
		(lexorder (tree-min (rb-left tree))
			  (tree-max (rb-right tree)))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance tree-min-lexorder-tree-max
			    (tree (rb-right tree)))
		 (:instance ordered-min-left-lexorder-min-right))
	   :in-theory (disable tree-min-lexorder-tree-max
			       ordered-min-left-lexorder-min-right))))

(defthm ordered-max-left-lexorder-max-right
  (implies (and (ordered-tree-p tree)
		(rb-p tree)
		(rb-p (rb-left tree))
		(rb-p (rb-right tree)))
	   (and (not (equal (tree-max (rb-left tree))
			    (tree-max (rb-right tree))))
		(lexorder (tree-max (rb-left tree))
			  (tree-max (rb-right tree)))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance tree-min-lexorder-tree-max
			    (tree (rb-right tree)))
		 (:instance ordered-max-left-lexorder-min-right))
	   :in-theory (disable tree-min-lexorder-tree-max
			       ordered-max-left-lexorder-min-right
			       lexorder-transitive))
	  ("Subgoal 1"
	   :in-theory (disable tree-min-lexorder-tree-max))))

(defthm ordered-min-left-lexorder-root
  (implies (and (ordered-tree-p tree)
		(rb-p tree)
		(rb-p (rb-left tree)))
	   (and (not (equal (tree-min (rb-left tree))
			    (rb-key tree)))
		(lexorder (tree-min (rb-left tree))
			  (rb-key tree))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance tree-min-lexorder-tree-max
			    (tree (rb-left tree))))
	   :in-theory (disable tree-min-lexorder-tree-max))))

(defthm ordered-root-lexorder-max-right
  (implies (and (ordered-tree-p tree)
		(rb-p tree)
		(rb-p (rb-right tree)))
	   (and (not (equal (rb-key tree)
			    (tree-max (rb-right tree))))
		(lexorder (rb-key tree)
			  (tree-max (rb-right tree)))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance tree-min-lexorder-tree-max
			    (tree (rb-right tree))))
	   :in-theory (disable tree-min-lexorder-tree-max))))

(defthm ordered-left-lexorder-root-forward
  (implies (and (ordered-tree-p tree)
		(rb-p tree)
		(rb-p (rb-left tree)))
	   (and (strict-lexorder (rb-key (rb-left tree))
				 (rb-key tree))
		(strict-lexorder (tree-max (rb-left tree))
				 (rb-key tree))
		(ordered-tree-p (rb-left tree))))
  :rule-classes (:forward-chaining))

(defthm ordered-root-lexorder-right-forward
  (implies (and (ordered-tree-p tree)
		(rb-p tree)
		(rb-p (rb-right tree)))
	   (and (strict-lexorder (rb-key tree)
				 (rb-key (rb-right tree)))
		(strict-lexorder (rb-key tree)
				 (tree-min (rb-right tree)))
		(ordered-tree-p (rb-right tree))))
  :rule-classes (:forward-chaining))

(defthm ordered-left-lexorder-right-forward
  (implies (and (ordered-tree-p tree)
		(rb-p tree)
		(rb-p (rb-left tree))
		(rb-p (rb-right tree)))
	   (and (strict-lexorder (rb-key (rb-left tree))
				 (rb-key (rb-right tree)))
		(ordered-tree-p (rb-left tree))
		(strict-lexorder (tree-max (rb-left tree))
				 (tree-min (rb-right tree)))
		(ordered-tree-p (rb-right tree))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance ordered-left-lexorder-root-forward)
		 (:instance ordered-root-lexorder-right-forward))))
  :rule-classes (:forward-chaining))
    
					;(set-match-free-error nil)

(defthm lexorder-anti-reflexive-x-y-z
  (implies (and (lexorder x y)
		(lexorder y z)
		(lexorder z x))
	   (equal (equal x z) t))
  :hints (("Goal"
	   :use ((:instance lexorder-transitive))
	   :in-theory (disable lexorder-transitive))))

(defthm assoc-min-lexorder
  (equal (min-lexorder (min-lexorder a b) c)
	 (min-lexorder a (min-lexorder b c))))

(defthm commutavity-min-lexorder
  (equal (min-lexorder b a)
	 (min-lexorder a b)))

(defthm commutavity-2-min-lexorder
  (equal (min-lexorder b (min-lexorder a c))
	 (min-lexorder a (min-lexorder b c))))

(defthm assoc-max-lexorder
  (equal (max-lexorder (max-lexorder a b) c)
	 (max-lexorder a (max-lexorder b c))))

(defthm commutavity-max-lexorder
  (equal (max-lexorder b a)
	 (max-lexorder a b)))

(defthm commutavity-2-max-lexorder
  (equal (max-lexorder b (max-lexorder a c))
	 (max-lexorder a (max-lexorder b c))))

(defthm lexorder-inequality-chain-forward-1
  (implies (and (lexorder x y)
		(lexorder y z)
		(not (equal x y)))
	   (and (lexorder x z)
		(not (equal x z))))
  :rule-classes (:forward-chaining))

(defthm lexorder-inequality-chain-forward-2
  (implies (and (lexorder x y)
		(lexorder y z)
		(not (equal y z)))
	   (and (lexorder x z)
		(not (equal x z))))
  :rule-classes (:forward-chaining))

(defthm lexorder-strict-inequality
  (implies (and (lexorder x y)
		(lexorder y z)
		(or (not (equal x y))
		    (not (equal y z))))
	   (and (lexorder x z)
		(not (equal x z))))
  :rule-classes (:forward-chaining))
    
(defun min-lexorder-tree (a tree)
  (if (rb-p tree)
       (min-lexorder a (tree-min tree))
     a))

(defthm tree-min-left-case-1
  (let* ((a3 tree)
	 (a2 (rb-left a3))
	 (a1 (rb-left a2))
	 (t1 (rb-left a1))
	 (t2 (rb-right a1))
	 (t3 (rb-right a2))
	 (t4 (rb-right a3)))
    (implies (and (rb-p a1)
		  (rb-p a2)
		  (rb-p a3))
	     (equal (tree-min tree)
		    (min-lexorder-tree
		     (min-lexorder-tree
		      (min-lexorder-tree 
		       (min-lexorder-tree 
			(min-lexorder (rb-key a1)
				      (min-lexorder (rb-key a2)
						    (rb-key a3)))
			t1)
		       t2)
		      t3)
		     t4))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable min-lexorder))))
      
(defthm tree-min-left-case-2
  (let* ((a3 tree)
	 (a1 (rb-left a3))
	 (a2 (rb-right a1))
	 (t1 (rb-left a1))
	 (t2 (rb-left a2))
	 (t3 (rb-right a2))
	 (t4 (rb-right a3)))
    (implies (and (rb-p a1)
		  (rb-p a2)
		  (rb-p a3))
	     (equal (tree-min tree)
		    (min-lexorder-tree
		     (min-lexorder-tree
		      (min-lexorder-tree 
		       (min-lexorder-tree 
			(min-lexorder (rb-key a1)
				      (min-lexorder (rb-key a2)
						    (rb-key a3)))
			t1)
		       t2)
		      t3)
		     t4))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable min-lexorder))))

(defthm tree-min-right-case-1
  (let* ((a1 tree)
	 (a3 (rb-right a1))
	 (a2 (rb-left a3))
	 (t1 (rb-left a1))
	 (t2 (rb-left a2))
	 (t3 (rb-right a2))
	 (t4 (rb-right a3)))
    (implies (and (rb-p a1)
		  (rb-p a2)
		  (rb-p a3))
	     (equal (tree-min tree)
		    (min-lexorder-tree
		     (min-lexorder-tree
		      (min-lexorder-tree 
		       (min-lexorder-tree 
			(min-lexorder (rb-key a1)
				      (min-lexorder (rb-key a2)
						    (rb-key a3)))
			t1)
		       t2)
		      t3)
		     t4))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable min-lexorder))))

(defthm tree-min-right-case-2
  (let* ((a1 tree)
	 (a2 (rb-right a1))
	 (a3 (rb-right a2))
	 (t1 (rb-left a1))
	 (t2 (rb-left a2))
	 (t3 (rb-left a3))
	 (t4 (rb-right a3)))
    (implies (and (rb-p a1)
		  (rb-p a2)
		  (rb-p a3))
	     (equal (tree-min tree)
		    (min-lexorder-tree
		     (min-lexorder-tree
		      (min-lexorder-tree 
		       (min-lexorder-tree 
			(min-lexorder (rb-key a1)
				      (min-lexorder (rb-key a2)
						    (rb-key a3)))
			t1)
		       t2)
		      t3)
		     t4))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable min-lexorder))))
      
(defthm tree-min-after-balance
  (let ((tree (rb (rb-key a2) (rb-value a2) 'red
		  (rb (rb-key a1) (rb-value a1) 'black t1 t2)
		  (rb (rb-key a3) (rb-value a3) 'black t3 t4))))
    (implies (and (rb-p a1)
		  (rb-p a2)
		  (rb-p a3))
	     (equal (tree-min tree)
		    (min-lexorder-tree
		     (min-lexorder-tree
		      (min-lexorder-tree 
		       (min-lexorder-tree 
			(min-lexorder (rb-key a1)
				      (min-lexorder (rb-key a2)
						    (rb-key a3)))
			t1)
		       t2)
		      t3)
		     t4))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable min-lexorder))))
      
(defthm tree-min-balance-left
  (equal (tree-min (rb-balance-left tree))
	 (tree-min tree))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable min-lexorder))))
      
(defthm tree-min-balance-right
  (equal (tree-min (rb-balance-right tree))
	 (tree-min tree))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable min-lexorder))))

(defun max-lexorder-tree (a tree)
  (if (rb-p tree)
       (max-lexorder a (tree-max tree))
     a))

(defthm tree-max-left-case-1
  (let* ((a3 tree)
	 (a2 (rb-left a3))
	 (a1 (rb-left a2))
	 (t1 (rb-left a1))
	 (t2 (rb-right a1))
	 (t3 (rb-right a2))
	 (t4 (rb-right a3)))
    (implies (and (rb-p a1)
		  (rb-p a2)
		  (rb-p a3))
	     (equal (tree-max tree)
		    (max-lexorder-tree
		     (max-lexorder-tree
		      (max-lexorder-tree 
		       (max-lexorder-tree 
			(max-lexorder (rb-key a1)
				      (max-lexorder (rb-key a2)
						    (rb-key a3)))
			t1)
		       t2)
		      t3)
		     t4))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable max-lexorder))))

(defthm tree-max-left-case-2
  (let* ((a3 tree)
	 (a1 (rb-left a3))
	 (a2 (rb-right a1))
	 (t1 (rb-left a1))
	 (t2 (rb-left a2))
	 (t3 (rb-right a2))
	 (t4 (rb-right a3)))
    (implies (and (rb-p a1)
		  (rb-p a2)
		  (rb-p a3))
	     (equal (tree-max tree)
		    (max-lexorder-tree
		     (max-lexorder-tree
		      (max-lexorder-tree 
		       (max-lexorder-tree 
			(max-lexorder (rb-key a1)
				      (max-lexorder (rb-key a2)
						    (rb-key a3)))
			t1)
		       t2)
		      t3)
		     t4))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable max-lexorder))))

(defthm tree-max-right-case-1
  (let* ((a1 tree)
	 (a3 (rb-right a1))
	 (a2 (rb-left a3))
	 (t1 (rb-left a1))
	 (t2 (rb-left a2))
	 (t3 (rb-right a2))
	 (t4 (rb-right a3)))
    (implies (and (rb-p a1)
		  (rb-p a2)
		  (rb-p a3))
	     (equal (tree-max tree)
		    (max-lexorder-tree
		     (max-lexorder-tree
		      (max-lexorder-tree 
		       (max-lexorder-tree 
			(max-lexorder (rb-key a1)
				      (max-lexorder (rb-key a2)
						    (rb-key a3)))
			t1)
		       t2)
		      t3)
		     t4))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable max-lexorder))))

(defthm tree-max-right-case-2
  (let* ((a1 tree)
	 (a2 (rb-right a1))
	 (a3 (rb-right a2))
	 (t1 (rb-left a1))
	 (t2 (rb-left a2))
	 (t3 (rb-left a3))
	 (t4 (rb-right a3)))
    (implies (and (rb-p a1)
		  (rb-p a2)
		  (rb-p a3))
	     (equal (tree-max tree)
		    (max-lexorder-tree
		     (max-lexorder-tree
		      (max-lexorder-tree 
		       (max-lexorder-tree 
			(max-lexorder (rb-key a1)
				      (max-lexorder (rb-key a2)
						    (rb-key a3)))
			t1)
		       t2)
		      t3)
		     t4))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable max-lexorder))))

(defthm tree-max-after-balance
  (let ((tree (rb (rb-key a2) (rb-value a2) 'red
		  (rb (rb-key a1) (rb-value a1) 'black t1 t2)
		  (rb (rb-key a3) (rb-value a3) 'black t3 t4))))
    (implies (and (rb-p a1)
		  (rb-p a2)
		  (rb-p a3))
	     (equal (tree-max tree)
		    (max-lexorder-tree
		     (max-lexorder-tree
		      (max-lexorder-tree 
		       (max-lexorder-tree 
			(max-lexorder (rb-key a1)
				      (max-lexorder (rb-key a2)
						    (rb-key a3)))
			t1)
		       t2)
		      t3)
		     t4))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable max-lexorder))))

(defthm tree-max-balance-left
  (equal (tree-max (rb-balance-left tree))
	 (tree-max tree))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable max-lexorder))))

(defthm tree-max-balance-right
  (equal (tree-max (rb-balance-right tree))
	 (tree-max tree))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable max-lexorder))))
      
(defthm ordered-balance-inequalities-result
  (implies (and (rb-p a1)
		(rb-p a2)
		(rb-p a3)
		(strict-lexorder (rb-key a1) (rb-key a2))
		(strict-lexorder (rb-key a2) (rb-key a3))
		(implies (rb-p t1)
			 (strict-lexorder (tree-max t1) (rb-key a1)))
		(implies (rb-p t2)
			 (strict-lexorder (rb-key a1) (tree-min t2)))
		(implies (rb-p t2)
			 (strict-lexorder (tree-max t2) (rb-key a2)))
		(implies (rb-p t3)
			 (strict-lexorder (tree-max t3) (rb-key a3)))
		(implies (rb-p t3)
			 (strict-lexorder (rb-key a2) (tree-min t3)))
		(implies (rb-p t4)
			 (strict-lexorder (rb-key a3) (tree-min t4)))
		(ordered-tree-p t1)
		(ordered-tree-p t2)
		(ordered-tree-p t3)
		(ordered-tree-p t4))
	   (ordered-tree-p (rb (rb-key a2) (rb-value a2) c1
			       (rb (rb-key a1) (rb-value a1) c2 t1 t2)
			       (rb (rb-key a3) (rb-value a3) c3 t3 t4))))
  :hints (("Goal" :do-not-induct t)))
      
(defthm ordered-balance-inequalities-left-case-1
  (let* ((a3 tree)
	 (a2 (rb-left a3))
	 (a1 (rb-left a2))
	 (t1 (rb-left a1))
	 (t2 (rb-right a1))
	 (t3 (rb-right a2))
	 (t4 (rb-right a3)))
    (implies (and (ordered-tree-p tree)
		  (rb-p a1)
		  (rb-p a2)
		  (rb-p a3))
	     (and (strict-lexorder (rb-key a1) (rb-key a2))
		  (strict-lexorder (rb-key a2) (rb-key a3))
		  (implies (rb-p t1)
			   (strict-lexorder (tree-max t1) (rb-key a1)))
		  (implies (rb-p t2)
			   (strict-lexorder (rb-key a1) (tree-min t2)))
		  (implies (rb-p t2)
			   (strict-lexorder (tree-max t2) (rb-key a2)))
		  (implies (rb-p t3)
			   (strict-lexorder (tree-max t3) (rb-key a3)))
		  (implies (rb-p t3)
			   (strict-lexorder (rb-key a2) (tree-min t3)))
		  (implies (rb-p t4)
			   (strict-lexorder (rb-key a3) (tree-min t4))))))
  :hints (("Goal" :do-not-induct t)))
      
(defthm ordered-balance-left-case-1
  (implies (and (ordered-tree-p tree)
		(rb-p tree)
		(rb-p (rb-left tree))
		(rb-p (rb-left (rb-left tree))))
	   (ordered-tree-p (rb-balance-left-case-1 tree)))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance ordered-balance-inequalities-left-case-1)
		 (:instance ordered-balance-inequalities-result
			    (a3 tree)
			    (a2 (rb-left tree))
			    (a1 (rb-left (rb-left tree)))
			    (t1 (rb-left (rb-left (rb-left tree))))
			    (t2 (rb-right (rb-left (rb-left tree))))
			    (t3 (rb-right (rb-left tree)))
			    (t4 (rb-right tree))
			    (c1 'red)
			    (c2 'black)
			    (c3 'black)))
	   :in-theory '((:definition rb-balance-left-case-1)
			(:definition ordered-tree-p)))))
      
(defthm ordered-balance-inequalities-left-case-2
  (let* ((a3 tree)
	 (a1 (rb-left a3))
	 (a2 (rb-right a1))
	 (t1 (rb-left a1))
	 (t2 (rb-left a2))
	 (t3 (rb-right a2))
	 (t4 (rb-right a3)))
    (implies (and (ordered-tree-p tree)
		  (rb-p a1)
		  (rb-p a2)
		  (rb-p a3))
	     (and (strict-lexorder (rb-key a1) (rb-key a2))
		  (strict-lexorder (rb-key a2) (rb-key a3))
		  (implies (rb-p t1)
			   (strict-lexorder (tree-max t1) (rb-key a1)))
		  (implies (rb-p t2)
			   (strict-lexorder (rb-key a1) (tree-min t2)))
		  (implies (rb-p t2)
			   (strict-lexorder (tree-max t2) (rb-key a2)))
		  (implies (rb-p t3)
			   (strict-lexorder (tree-max t3) (rb-key a3)))
		  (implies (rb-p t3)
			   (strict-lexorder (rb-key a2) (tree-min t3)))
		  (implies (rb-p t4)
			   (strict-lexorder (rb-key a3) (tree-min t4))))))
  :hints (("Goal" :do-not-induct t)))

(defthm ordered-balance-left-case-2
  (implies (and (ordered-tree-p tree)
		(rb-p tree)
		(rb-p (rb-left tree))
		(rb-p (rb-right (rb-left tree))))
	   (ordered-tree-p (rb-balance-left-case-2 tree)))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance ordered-balance-inequalities-left-case-2)
		 (:instance ordered-balance-inequalities-result
			    (a3 tree)
			    (a1 (rb-left tree))
			    (a2 (rb-right (rb-left tree)))
			    (t1 (rb-left (rb-left tree)))
			    (t2 (rb-left (rb-right (rb-left tree))))
			    (t3 (rb-right (rb-right (rb-left tree))))
			    (t4 (rb-right tree))
			    (c1 'red)
			    (c2 'black)
			    (c3 'black)))
	   :in-theory '((:definition rb-balance-left-case-2)
			(:definition ordered-tree-p)))))


(defthm ordered-balance-inequalities-right-case-1
  (let* ((a1 tree)
	 (a3 (rb-right a1))
	 (a2 (rb-left a3))
	 (t1 (rb-left a1))
	 (t2 (rb-left a2))
	 (t3 (rb-right a2))
	 (t4 (rb-right a3)))
    (implies (and (ordered-tree-p tree)
		  (rb-p a1)
		  (rb-p a2)
		  (rb-p a3))
	     (and (strict-lexorder (rb-key a1) (rb-key a2))
		  (strict-lexorder (rb-key a2) (rb-key a3))
		  (implies (rb-p t1)
			   (strict-lexorder (tree-max t1) (rb-key a1)))
		  (implies (rb-p t2)
			   (strict-lexorder (rb-key a1) (tree-min t2)))
		  (implies (rb-p t2)
			   (strict-lexorder (tree-max t2) (rb-key a2)))
		  (implies (rb-p t3)
			   (strict-lexorder (tree-max t3) (rb-key a3)))
		  (implies (rb-p t3)
			   (strict-lexorder (rb-key a2) (tree-min t3)))
		  (implies (rb-p t4)
			   (strict-lexorder (rb-key a3) (tree-min t4))))))
  :hints (("Goal" :do-not-induct t)))

(defthm ordered-balance-right-case-1
  (implies (and (ordered-tree-p tree)
		(rb-p tree)
		(rb-p (rb-right tree))
		(rb-p (rb-left (rb-right tree))))
	   (ordered-tree-p (rb-balance-right-case-1 tree)))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance ordered-balance-inequalities-right-case-1)
		 (:instance ordered-balance-inequalities-result
			    (a1 tree)
			    (a3 (rb-right tree))
			    (a2 (rb-left (rb-right tree)))
			    (t1 (rb-left tree))
			    (t2 (rb-left (rb-left (rb-right tree))))
			    (t3 (rb-right (rb-left (rb-right tree))))
			    (t4 (rb-right (rb-right tree)))
			    (c1 'red)
			    (c2 'black)
			    (c3 'black)))
	   :in-theory '((:definition rb-balance-right-case-1)
			(:definition ordered-tree-p)))))

(defthm ordered-balance-inequalities-right-case-2
  (let* ((a1 tree)
	 (a2 (rb-right a1))
	 (a3 (rb-right a2))
	 (t1 (rb-left a1))
	 (t2 (rb-left a2))
	 (t3 (rb-left a3))
	 (t4 (rb-right a3)))
    (implies (and (ordered-tree-p tree)
		  (rb-p a1)
		  (rb-p a2)
		  (rb-p a3))
	     (and (strict-lexorder (rb-key a1) (rb-key a2))
		  (strict-lexorder (rb-key a2) (rb-key a3))
		  (implies (rb-p t1)
			   (strict-lexorder (tree-max t1) (rb-key a1)))
		  (implies (rb-p t2)
			   (strict-lexorder (rb-key a1) (tree-min t2)))
		  (implies (rb-p t2)
			   (strict-lexorder (tree-max t2) (rb-key a2)))
		  (implies (rb-p t3)
			   (strict-lexorder (tree-max t3) (rb-key a3)))
		  (implies (rb-p t3)
			   (strict-lexorder (rb-key a2) (tree-min t3)))
		  (implies (rb-p t4)
			   (strict-lexorder (rb-key a3) (tree-min t4))))))
  :hints (("Goal" :do-not-induct t)))

(defthm ordered-balance-right-case-2
  (implies (and (ordered-tree-p tree)
		(rb-p tree)
		(rb-p (rb-right tree))
		(rb-p (rb-right (rb-right tree))))
	   (ordered-tree-p (rb-balance-right-case-2 tree)))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance ordered-balance-inequalities-right-case-2)
		 (:instance ordered-balance-inequalities-result
			    (a1 tree)
			    (a2 (rb-right tree))
			    (a3 (rb-right (rb-right tree)))
			    (t1 (rb-left tree))
			    (t2 (rb-left (rb-right tree)))
			    (t3 (rb-left (rb-right (rb-right tree))))
			    (t4 (rb-right (rb-right (rb-right tree))))
			    (c1 'red)
			    (c2 'black)
			    (c3 'black)))
	   :in-theory '((:definition rb-balance-right-case-2)
			(:definition ordered-tree-p)))))
      
(defthm ordered-balance-left
  (implies (ordered-tree-p tree)
	   (ordered-tree-p (rb-balance-left tree)))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable rb-balance-left-case-1
			       rb-balance-left-case-2))))

(defthm ordered-balance-right
  (implies (ordered-tree-p tree)
	   (ordered-tree-p (rb-balance-right tree)))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable rb-balance-right-case-1
			       rb-balance-right-case-2))))

      
(defthm lookup-balance-left-case-1
  (implies (and (ordered-tree-p tree)
		(rb-p tree)
		(rb-p (rb-left tree))
		(rb-p (rb-left (rb-left tree))))
	   (equal (rb-lookup key (rb-balance-left-case-1 tree))
		  (rb-lookup key tree)))
  :hints (("Goal" :do-not-induct t)))

(defthm lookup-balance-left-case-2
  (implies (and (ordered-tree-p tree)
		(rb-p tree)
		(rb-p (rb-left tree))
		(rb-p (rb-right (rb-left tree))))
	   (equal (rb-lookup key (rb-balance-left-case-2 tree))
		  (rb-lookup key tree)))
  :hints (("Goal" :do-not-induct t)))

(defthm lookup-balance-left
  (implies (ordered-tree-p tree)
	   (equal (rb-lookup key (rb-balance-left tree))
		  (rb-lookup key tree)))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable rb-balance-left-case-1
			       rb-balance-left-case-2))))

      
(defthm lookup-balance-right-case-1
  (implies (and (ordered-tree-p tree)
		(rb-p tree)
		(rb-p (rb-right tree))
		(rb-p (rb-left (rb-right tree))))
	   (equal (rb-lookup key (rb-balance-right-case-1 tree))
		  (rb-lookup key tree)))
  :hints (("Goal" :do-not-induct t)))

(defthm lookup-balance-right-case-2
  (implies (and (ordered-tree-p tree)
		(rb-p tree)
		(rb-p (rb-right tree))
		(rb-p (rb-right (rb-right tree))))
	   (equal (rb-lookup key (rb-balance-right-case-2 tree))
		  (rb-lookup key tree)))
  :hints (("Goal" :do-not-induct t)))

(defthm lookup-balance-right
  (implies (ordered-tree-p tree)
	   (equal (rb-lookup key (rb-balance-right tree))
		  (rb-lookup key tree)))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable rb-balance-right-case-1
			       rb-balance-right-case-2))))
      
(defthm ordered-set-color
  (implies (rb-p tree)
	   (equal (ordered-tree-p (update-rb tree :color color))
		  (ordered-tree-p tree))))

(defthm rb-p-insert-aux
  (rb-p (rb-insert-aux key value tree)))

(defthm ordered-set-color-insert-aux
  (equal (ordered-tree-p (update-rb (rb-insert-aux key value tree)
                                    :color color))
	 (ordered-tree-p (rb-insert-aux key value tree))))
      
(defthm ordered-set-left
  (implies (and (ordered-tree-p (rb-right tree))
		(implies (rb-p (rb-right tree))
			 (strict-lexorder (rb-key tree)
					  (tree-min (rb-right tree))))
		(ordered-tree-p left)
		(implies (rb-p left)
			 (strict-lexorder (tree-max left)
					  (rb-key tree))))
	   (ordered-tree-p (update-rb tree :left left)))
  :hints (("Goal" :do-not-induct t)))
      
(defthm ordered-set-right
  (implies (and (ordered-tree-p (rb-left tree))
		(implies (rb-p (rb-left tree))
			 (strict-lexorder (tree-max (rb-left tree))
					  (rb-key tree)))
		(ordered-tree-p right)
		(implies (rb-p right)
			 (strict-lexorder (rb-key tree)
					  (tree-min right))))
	   (ordered-tree-p (update-rb tree :right right)))
  :hints (("Goal" :do-not-induct t)))    
      
(defthm tree-min-insert-aux
  (equal (tree-min (rb-insert-aux key value tree))
	 (if (rb-p tree)
	     (if (lexorder key (tree-min tree))
		 key
	       (tree-min tree))
	   key))
  :hints (("Goal"
	   :induct (rb-insert-aux key value tree)
	   :in-theory (disable rb-balance-left
			       rb-balance-right))))
      
(defthm tree-max-insert-aux
  (equal (tree-max (rb-insert-aux key value tree))
	 (if (rb-p tree)
	     (if (lexorder key (tree-max tree))
		 (tree-max tree)
	       key)
	   key))
  :hints (("Goal"
	   :induct (rb-insert-aux key value tree)
	   :in-theory (disable rb-balance-left
			       rb-balance-right))))
      
(defthm ordered-insert-aux-lemma-1
    (implies (and (rb-p tree)
		  (not (equal key (rb-key tree)))
		  (lexorder key (rb-key tree))
		  (ordered-tree-p (rb-insert-aux key value (rb-left tree)))
		  (ordered-tree-p tree))
	     (ordered-tree-p (rb-insert-aux key value tree)))
    :hints (("Goal" :do-not-induct t
	     :use ((:instance ordered-set-left
			      (left (rb-insert-aux key value (rb-left tree))))
		   (:instance ordered-balance-left
			      (tree (update-rb tree :left (rb-insert-aux key value (rb-left tree))))))
	     :in-theory (disable ordered-set-left
				 ordered-balance-left
				 rb-balance-left
				 rb-balance-right)
	   ))
  :rule-classes nil)

(defthm ordered-insert-aux-lemma-2
    (implies (and (rb-p tree)
		  (not (equal key (rb-key tree)))
		  (not (lexorder key (rb-key tree)))
		  (ordered-tree-p (rb-insert-aux key value (rb-right tree)))
		  (ordered-tree-p tree))
	     (ordered-tree-p (rb-insert-aux key value tree)))
    :hints (("Goal"
	     :use ((:instance ordered-set-right
			      (right (rb-insert-aux key value (rb-right tree)))))
	     :in-theory (disable ordered-set-right
				 rb-balance-left
				 rb-balance-right)
	     ))
    :rule-classes nil)
      
(defthm ordered-insert-aux
   (implies (ordered-tree-p tree)
	    (ordered-tree-p (rb-insert-aux key value tree)))
   :hints (("Goal"
	    :in-theory (disable rb-balance-left
				rb-balance-right))
	   ("Subgoal *1/6"
	    :by (:instance ordered-insert-aux-lemma-2))
	   ("Subgoal *1/4"
	    :by (:instance ordered-insert-aux-lemma-1))))

(defthm ordered-insert
  (implies (ordered-tree-p tree)
	   (ordered-tree-p (rb-insert key value tree)))
  :hints (("Goal"
	   :in-theory (disable rb-insert-aux))))
      
(defthm lookup-insert-lemma-1
    (implies (and (rb-p tree)
		  (ordered-tree-p tree)
		  (lexorder k (rb-key tree))
		  (not (equal k (rb-key tree))))
	     (ordered-tree-p (update-rb tree
					:left (rb-insert-aux k value (rb-left tree)))))
    :hints (("Goal" :do-not-induct t
	     :use ((:instance ordered-insert-aux
			      (key k)
			      (value value)
			      (tree (rb-left tree))))
	     :in-theory (disable ordered-insert-aux
				 rb-balance-left
				 rb-balance-right))))

(defthm lookup-insert-lemma-2
    (implies (and (rb-p tree)
		  (ordered-tree-p tree)
		  (lexorder (rb-key tree) k)
		  (not (equal  (rb-key tree) k)))
	     (ordered-tree-p (update-rb tree
					:right (rb-insert-aux k value (rb-right tree)))))
    :hints (("Goal" :do-not-induct t
	     :use ((:instance ordered-insert-aux
			      (key k)
			      (value value)
			      (tree (rb-right tree))))
	     :in-theory (disable ordered-insert-aux
				 rb-balance-left
				 rb-balance-right))))
      
(defthm lookup-insert-aux
   (implies (ordered-tree-p tree)
	    (equal (rb-lookup k (rb-insert-aux key value tree))
		   (if (equal key k)
		       value
		     (rb-lookup k tree))))
   :hints (("Goal"
	    :in-theory (disable rb-balance-left
				rb-balance-right))))
      

(defthm lookup-set-color
  (implies (rb-p tree)
	   (equal (rb-lookup key (update-rb tree :color color))
		  (rb-lookup key tree))))
      
  
(defthm lookup-insert
  (implies (ordered-tree-p tree)
	   (equal (rb-lookup k (rb-insert key value tree))
		  (if (equal key k)
		      value
		    (rb-lookup k tree)))))
    
;(defeval$ evl rb-lookup rb-insert ordered-tree-p)