--- a/RedBlackTree.agda	Mon Jan 08 18:50:45 2018 +0900
+++ b/RedBlackTree.agda	Mon Jan 08 19:43:49 2018 +0900
@@ -90,8 +90,22 @@
 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 = {!!}
+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 -> Maybe (Node a k) -> Maybe (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
+  with parent | grandParent
+... | Nothing | _ = {!!}
+... | _ | Nothing = {!!}
+... | Just parent1 | Just grandParent1
+       with  (right parent1) | (left grandParent1)
+...    | Nothing | _ = {!!}
+...    | _ | Nothing = {!!}
+...    | Just rightParent | Just leftGrandParent with compare tree (key n0) (key rightParent) | compare tree (key parent1) (key leftGrandParent)
+...                                              | EQ | EQ = {!!}
+...                                              | _ | _  = {!!}
+
+
+
+
 
 {-# 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
@@ -101,14 +115,14 @@
           -- 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 tree s n0 parent grandParent next
-    ... | Nothing | Just uncle  = insertCase4 tree s n0 parent grandParent next
+    ... | Nothing | Nothing = insertCase4 tree s n0 Nothing Nothing next
+    ... | Nothing | Just uncle  = insertCase4 tree s n0 Nothing (Just uncle) next
     ... | Just uncle | _  with compare tree ( key uncle ) ( key parent )
-    ...                   | EQ =  insertCase4 tree s n0 parent grandParent next
+    ...                   | EQ =  insertCase4 tree s n0 (Just uncle) {!!} 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 tree s n0 parent grandParent next
+    ...                           | Black = insertCase4 tree s n0 (Just uncle) {!!} 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