--- a/RedBlackTree.agda	Tue Apr 17 10:14:16 2018 +0900
+++ b/RedBlackTree.agda	Thu Apr 26 20:09:55 2018 +0900
@@ -58,7 +58,7 @@
 replaceNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) ->  Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
 replaceNode {n} {m} {t} {a} {k} tree s n0 next = popSingleLinkedStack s (
       \s parent -> replaceNode1 s parent)
-        where
+       module ReplaceNode where
           replaceNode1 : SingleLinkedStack (Node a k) -> Maybe ( Node a k ) -> t 
           replaceNode1 s Nothing = next ( record tree { root = Just (record n0 { color = Black}) } )
           replaceNode1 s (Just n1) with compare tree (key n1) (key n0)
@@ -173,7 +173,7 @@
 -- 
 findNode : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> t) -> t
 findNode {n} {m} {a} {k}  {t} tree s n0 n1 next = pushSingleLinkedStack s n1 (\ s -> findNode1 s n1)
-  where
+  module FindNode where
     findNode2 : SingleLinkedStack (Node a k) -> (Maybe (Node a k)) -> t
     findNode2 s Nothing = next tree s n0
     findNode2 s (Just n) = findNode tree s n0 n next

--- a/redBlackTreeTest.agda	Tue Apr 17 10:14:16 2018 +0900
+++ b/redBlackTreeTest.agda	Thu Apr 26 20:09:55 2018 +0900
@@ -144,33 +144,37 @@
 ... |  tri< lt neq _ =  ⊥-elim (neq refl)
 
 checkEQ' :  {m : Level }  ( x y :  ℕ ) -> ( eq : x  ≡ y  ) -> ( x  ≟ y ) ≡ yes eq
-checkEQ' x y refl with  x  ≟ y
+checkEQ' x y refl with  x ≟ y
 ... | yes refl = refl
 ... | no neq = ⊥-elim ( neq refl )
 
 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
-         → (k : ℕ) (x : ℕ) 
+         → (k : ℕ) (x : ℕ)
          → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
-         (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True)) 
+           (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True)) 
 putTest1 n k x with n
-...  | Just n1 = lemma2 ( record { top = Nothing } )
+...  | Just n1 = lemma0
    where
-     lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) →
-       putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compareT }) k x (λ t →
-       GetRedBlackTree.checkNode t k (λ t₁ x1 → checkT x1 x ≡ True) (root t))
+     tree0 : (s : SingleLinkedStack (Node ℕ ℕ) ) → RedBlackTree ℕ ℕ
+     tree0 s = record { root = Just n1 ; nodeStack = s ; compare = compareT }
+     lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) → findNode (tree0 s) s (leafNode k x) n1 (λ  tree1 s n1 → replaceNode tree1 s n1
+              (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True)))
      lemma2 s with compTri k (key n1)
-     ... |  tri≈ le refl gt = lemma3
+     ... |  tri≈ le refl gt = {!!} -- lemma3
         where 
            lemma3 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
                key   = key n1 ; value = x ; right = right n1 ; left  = left n1 ; color = Black
-               } ) ; nodeStack = s ; compare = λ x₁ y → compareT x₁ y  } ) k ( λ  t x1 → checkT x1 x  ≡ True)
+               } ) ; nodeStack = s ; compare = λ x₁ y → compareT x₁ y  } ) k ( λ  t x1 → checkT x1 x ≡ True)
            lemma3 with compTri k k 
            ... | tri≈  _ refl _ = checkEQ x _ refl
            ... | tri< _ neq _ =  ⊥-elim (neq refl)
            ... | tri> _ neq _ =  ⊥-elim (neq refl)
      ... |  tri> le eq gt = {!!}
      ... |  tri< le eq gt = {!!}
-...  | Nothing =  lemma1  
+     lemma0 : clearSingleLinkedStack (record {top = Nothing}) (\s → findNode (tree0 s) s (leafNode k x) n1 (λ  tree1 s n1 → replaceNode tree1 s n1
+              (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True))))
+     lemma0 = lemma2 (record {top = Nothing})              
+...  | Nothing = lemma1  
    where 
      lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
                key   = k ; value = x ; right = Nothing ; left  = Nothing ; color = Red