--- a/src/parallel_execution/RedBlackTree.agda	Thu Jan 04 23:15:32 2018 +0900
+++ b/src/parallel_execution/RedBlackTree.agda	Thu Jan 04 23:43:18 2018 +0900
@@ -52,6 +52,7 @@
 --
 -- put new node at parent node, and rebuild tree to the top
 --
+{-# TERMINATING #-}   -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html
 replaceNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
 replaceNode {n} {m} {t} {a} {k} {si} tree s parent n0 next = popStack s (
       \s grandParent -> replaceNode1 s grandParent ( compare tree (key parent) (key n0) ) )
@@ -65,20 +66,34 @@
         ... | GT =  replaceNode tree s grandParent ( record parent { right = Just n0 } ) next
         ... | EQ =  next tree 
 
-insertNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
+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 = {!!}
+
+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 = {!!}
+
+insertCase5 : {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
+insertCase5 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
+
+insertCase4 : {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
+insertCase4 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
+
+{-# TERMINATING #-}
+insertNode : {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 -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
 insertNode {n} {m} {t} {a} {k} {si} tree s n0 next = get2Stack s (\ s d1 d2 -> insertCase1 s n0 d1 d2 )
    where
-    insertCase1 : Stack (Node a k) si -> Node a k -> Maybe (Node a k) -> Maybe (Node a k) -> t    -- placed here to allo mutual recursion
+    insertCase1 : Stack (Node a k) si -> Node a k -> Maybe (Node a k) -> Maybe (Node a k) -> t    -- placed here to allow mutual recursion
+          -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html
     insertCase3 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t
     insertCase3 s n0 parent grandParent with left grandParent | right grandParent
-    ... | Nothing | Nothing = {!!}     -- insertCase4
-    ... | Nothing | Just uncle  = {!!} -- insertCase4
+    ... | Nothing | Nothing = insertCase4 tree s n0 parent grandParent next
+    ... | Nothing | Just uncle  = insertCase4 tree s n0 parent grandParent next
     ... | Just uncle | _  with compare tree ( key uncle ) ( key parent )
-    ...                   | EQ = {!!} -- insertCase4
+    ...                   | EQ =  insertCase4 tree s n0 parent grandParent next
     ...                   | _ with color uncle
     ...                           | Red = pop2Stack s ( \s p0 p1 -> insertCase1 s ( 
            record grandParent { color = Red ; left = Just ( record parent { color = Black ; left = Just n0 } )  ; right = Just ( record uncle { color = Black } ) }) p0 p1 )
-    ...                           | Black = {!!} -- insertCase4
+    ...                           | Black = insertCase4 tree s n0 parent grandParent next
     insertCase2 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t
     insertCase2 s n0 parent grandParent with color parent
     ... | Black = replaceNode tree s grandParent n0 next