--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaTreeProof.agda	Tue Feb 09 18:44:53 2021 +0900
@@ -0,0 +1,34 @@
+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 = compare2 }
+
+putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
+         -> (k : ℕ) (x : ℕ)
+         -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
+         (\ t -> getRedBlackTree t k (\ t x1 -> check2 x1 x  ≡ True))
+putTest1 n k x with n
+...  | Just n1 = lemma2 ( record { top = Nothing } )
+   where
+     lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) -> putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t →
+         GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t))
+     lemma2 s with compare2 k (key n1)
+     ... |  EQ = lemma3 {!!}
+        where
+           lemma3 : compare2 k (key n1) ≡  EQ -> 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 → compare2 x₁ y  } ) k ( \ t x1 -> check2 x1 x  ≡ True)
+           lemma3 eq with compare2 x x | putTest1Lemma2 x
+           ... | EQ | refl with compare2 k (key n1)  | eq
+           ...              | EQ | refl with compare2 x x | putTest1Lemma2 x
+           ...                    | EQ | refl = refl
+     ... |  GT = {!!}
+     ... |  LT = {!!}
+
+...  | 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 → compare2 x₁ y  } ) k
+        ( \ t x1 -> check2 x1 x  ≡ True)
+     lemma1 with compare2 k k | putTest1Lemma2 k
+     ... | EQ | refl with compare2 x x | putTest1Lemma2 x
+     ...              | EQ | refl = refl