# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1516177901 -32400
# Node ID 2476f7123dc3118d2ee0e4a6e124b01ac216ee7d
# Parent  bc3208d510cdf548f15af3ecb586af1c88a40159
root = Nothing case passed on putTest1

diff -r bc3208d510cd -r 2476f7123dc3 redBlackTreeTest.agda
--- a/redBlackTreeTest.agda	Tue Jan 16 17:14:29 2018 +0900
+++ b/redBlackTreeTest.agda	Wed Jan 17 17:31:41 2018 +0900
@@ -153,9 +153,14 @@
 putTest1Lemma3 : (k : ℕ)  -> compareℕ k k ≡ EQ
 putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k  ) 
 
-compareLemma1 : (x  y : ℕ)  -> compareℕ x y ≡ EQ -> x  ≡ y
-compareLemma1 x y eq with compareℕ x y  | eq 
-... | EQ | refl = ?
+compareLemma1 : (x  y : ℕ)  -> compare2 x y ≡ EQ -> x  ≡ y
+compareLemma1 zero zero refl = refl
+compareLemma1 zero (suc _) () 
+compareLemma1 (suc _) zero () 
+compareLemma1 (suc x) (suc y) eq = cong ( \z -> ℕ.suc z ) ( compareLemma1 x y ( trans lemma2 eq ) )
+   where
+      lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y
+      lemma2 = refl
 
 
 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
@@ -170,7 +175,6 @@
                key   = k ; value = x ; right = Nothing ; left  = Nothing ; color = Red 
         } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y  } ) k
         ( \ t x1 -> check2 x1 x  ≡ True) 
-     lemma1 = {!!}
-
-
-
+     lemma1 with compare2 k k | putTest1Lemma2 k
+     ... | EQ | refl with compare2 x x | putTest1Lemma2 x
+     ...              | EQ | refl = refl