--- a/RedBlackTree.agda	Fri Jan 05 17:23:06 2018 +0900
+++ b/RedBlackTree.agda	Mon Jan 08 18:23:55 2018 +0900
@@ -66,8 +66,13 @@
         ... | GT =  replaceNode tree s grandParent ( record parent { right = Just n0 } ) next
         ... | EQ =  next tree 
 
-rotateRight : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node  a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-rotateRight {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
+-- rotateRight : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node  a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
+-- rotateRight {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next with parent
+-- ... | Nothing = insertCase5 tree s n0 parent grandParent next
+-- ... | Just parent with compare tree (key n0) (key (left parent)))
+--                   | EQ = insetCase5 tree s n0 parent grandParent next
+--                   | _ = insetCase5 tree s n0 parent grandParent next
+
 
 rotateLeft : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
 rotateLeft {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}