--- a/RedBlackTree.agda	Mon Jan 08 19:43:49 2018 +0900
+++ b/RedBlackTree.agda	Tue Jan 09 07:57:52 2018 +0900
@@ -90,23 +90,16 @@
 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 -> Maybe (Node a k) -> Maybe (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
+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
-  with parent | grandParent
-... | Nothing | _ = {!!}
-... | _ | Nothing = {!!}
-... | Just parent1 | Just grandParent1
-       with  (right parent1) | (left grandParent1)
+       with  (right parent) | (left grandParent)
 ...    | Nothing | _ = {!!}
 ...    | _ | Nothing = {!!}
-...    | Just rightParent | Just leftGrandParent with compare tree (key n0) (key rightParent) | compare tree (key parent1) (key leftGrandParent)
+...    | Just rightParent | Just leftGrandParent with compare tree (key n0) (key rightParent) | compare tree (key parent) (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
 insertNode {n} {m} {t} {a} {k} {si} tree s n0 next = get2Stack s (\ s d1 d2 -> insertCase1 s n0 d1 d2 )
@@ -115,14 +108,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 Nothing Nothing next
-    ... | Nothing | Just uncle  = insertCase4 tree s n0 Nothing (Just uncle) next
+    ... | 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 tree s n0 (Just uncle) {!!} next
+    ...                   | 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 tree s n0 (Just uncle) {!!} next
+    ...                           | 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
@@ -131,7 +124,7 @@
     insertCase1 s n0 Nothing (Just grandParent) = replaceNode tree s grandParent n0 next
     insertCase1 s n0 (Just grandParent) Nothing = replaceNode tree s grandParent n0 next
     insertCase1 s n0 (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent
-      where
+
 
 findNode : {n m : Level } {a k si : Set n} {t : Set m} -> 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 -> Stack (Node a k) si -> Node a k -> t) -> t
 findNode {n} {m} {a} {k} {si} {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1)