# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1524824380 -32400
# Node ID 1eccf1f18a5968846cd713d338febf0ea4068373
# Parent  a6aa2ff5fea40b96a4f9ca8941ded546d8918e2b
add more detail

diff -r a6aa2ff5fea4 -r 1eccf1f18a59 redBlackTreeTest.agda
--- a/redBlackTreeTest.agda	Thu Apr 26 20:09:55 2018 +0900
+++ b/redBlackTreeTest.agda	Fri Apr 27 19:19:40 2018 +0900
@@ -148,6 +148,9 @@
 ... | yes refl = refl
 ... | no neq = ⊥-elim ( neq refl )
 
+---  search -> checkEQ
+---  findNode -> search
+
 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
          → (k : ℕ) (x : ℕ)
          → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
@@ -160,15 +163,32 @@
      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 = lemma5 s
         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)
-           lemma3 with compTri k k 
-           ... | tri≈  _ refl _ = checkEQ x _ refl
-           ... | tri< _ neq _ =  ⊥-elim (neq refl)
-           ... | tri> _ neq _ =  ⊥-elim (neq refl)
+           open stack.SingleLinkedStack
+           open stack.Element
+           lemma6 :  (s : SingleLinkedStack (Node ℕ ℕ) )  → (n2 : Element (Node ℕ ℕ) )
+              → ReplaceNode.replaceNode1 (tree0 s) s (record n1 { key = k ; value = x } ) (λ t →
+                 GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t))
+                        (record { top = Element.next n2 }) (Just (Element.datum n2))
+           lemma6 s n2 with (top s )
+           ...         | Just n3 with compTri (key (datum n2)) (key (datum n3))
+           ...            | tri< _ neq _ =  {!!} -- lemma6 ( record {top = next n3} ) {!!}
+           ...            | tri> _ neq _ =  {!!} -- lemma6 ( record {top = next n3} ) {!!}
+           ...            | tri≈  _ eq _  = {!!}
+           lemma6 s n2 | Nothing  = {!!}
+           lemma5 :  (s : SingleLinkedStack (Node ℕ ℕ) )  → popSingleLinkedStack ( record { top = Just (cons n1 (SingleLinkedStack.top s)) }  )
+               ( \ s1  _ -> (replaceNode (tree0 s1) s1 (record n1 { key = k ; value = x } ) (λ t → 
+                   GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t))) )
+           lemma5 s with (top s)
+           ...      | Just n2  with compTri k k
+           ...            | tri< _ neq _ =  ⊥-elim (neq refl)
+           ...            | tri> _ neq _ =  ⊥-elim (neq refl)
+           ...            | tri≈  _ refl _  = lemma6 s n2
+           lemma5 s | Nothing 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 = {!!}
      lemma0 : clearSingleLinkedStack (record {top = Nothing}) (\s → findNode (tree0 s) s (leafNode k x) n1 (λ  tree1 s n1 → replaceNode tree1 s n1
@@ -177,8 +197,7 @@
 ...  | Nothing = lemma1  
    where 
      lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
-               key   = k ; value = x ; right = Nothing ; left  = Nothing ; color = Red 
-        } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compareT x₁ y  } ) k
+               key   = k ; value = x ; right = Nothing ; left  = Nothing ; color = Red } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compareT x₁ y  } ) k
         ( λ  t x1 → checkT x1 x  ≡ True) 
      lemma1 with compTri k k 
      ... | tri≈  _ refl _ = checkEQ x _ refl