# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1523926932 -32400
# Node ID a5ba292e4081097ff8c7aa06e74f25d887241541
# Parent  56a190d3c70abe58aa7916945bf9ee6fac2b151e
lemma3

diff -r 56a190d3c70a -r a5ba292e4081 redBlackTreeTest.agda
--- a/redBlackTreeTest.agda	Tue Apr 17 09:44:06 2018 +0900
+++ b/redBlackTreeTest.agda	Tue Apr 17 10:02:12 2018 +0900
@@ -279,12 +279,15 @@
        putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compareT }) k x (λ t →
        GetRedBlackTree.checkNode t k (λ t₁ x1 → checkT x1 x ≡ True) (root t))
      lemma2 s with compTri k (key n1)
-     ... |  tri≈ le eq 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)
-           lemma3 = {!!}
+           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