# HG changeset patch
# User ryokka
# Date 1515751709 -32400
# Node ID b654ce34c894808109b5641ab6ed2a092ef02b2e
# Parent  b180dc78abcf6eb0d2ada7205d6516bf6c1c71bd
add putTest1Lemma1, putTest1

diff -r b180dc78abcf -r b654ce34c894 redBlackTreeTest.agda
--- a/redBlackTreeTest.agda	Fri Jan 12 18:30:05 2018 +0900
+++ b/redBlackTreeTest.agda	Fri Jan 12 19:08:29 2018 +0900
@@ -113,11 +113,29 @@
 redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ 
 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compareℕ }
 
+
+
+putTest1Lemma1 : (k : ℕ) (x : ℕ) -> Data.Nat.compare 1 1 ≡ Data.Nat.equal 1
+putTest1Lemma1 k x = refl
+
+-- begin
+--     Data.Nat.compare k (key (leafNode k x)) 
+--   ≡⟨ {!!} ⟩
+--     Data.Nat.equal _
+--   ∎
+
+
 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
          -> (k : ℕ) (x : ℕ) 
          -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
          (\ t -> getRedBlackTree t k (\ t x1 -> check1 x1 x  ≡ True)) 
-putTest1 n k x = {!!}
+putTest1 n k x with n
+...  | Just n1 = {!!}
+...  | Nothing = {!!}
+
+
+-- with Data.Nat.compare k (key (leafNode k x))
+-- ...            | Data.Nat.equal _ = ?
 
 -- begin
 --     ?