--- a/hoareBinaryTree1.agda	Sat Apr 22 14:54:28 2023 +0900
+++ b/hoareBinaryTree1.agda	Sat Apr 22 19:15:59 2023 +0900
@@ -566,6 +566,9 @@
 color : {n : Level} (A : Set n) {key d : ℕ} {c : Color } → (rb : RBTree A key c d ) → Color
 color {n} A {k} {d} {c} rb = c
 
+rb-key : {n : Level} (A : Set n) {key d : ℕ} {c : Color } → (rb : RBTree A key c d ) → ℕ
+rb-key {n} A {k} {d} {c} rb = k
+
 RB→bt : {n : Level} (A : Set n) {key d : ℕ} {c : Color } → (rb : RBTree A key c d ) → bt A
 RB→bt {n} A (rb-leaf _) = leaf
 RB→bt {n} A (rb-single key value _) = node key value leaf leaf
@@ -656,25 +659,28 @@
         → length stack1 < length stack  → t )
      → (exit : {k1 d1 : ℕ} {c1 : Color} → (repl1 : RBTree A k1 c1 d1 ) → (rot : bt A )
          → (ri : rotatedTree (RB→bt A orig) rot ) → replacedTree key value rot (RB→bt A repl1) → t ) → t
-replaceRBP {n} {m} {A} {t} key value {_} {key1} orig tree stack si next exit = insertCase1 stack _ _ refl refl si where
+replaceRBP {n} {m} {A} {t} key value {_} {key1} orig tree stack si next exit = insertCase1 tree stack _ _ refl refl si where
     insertCase2 : {k0 k1 d0 d1 d2 : ℕ} {c0 c1 c2 : Color} → (tree : RBTree A k0 c0 d0) 
       → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) 
       → (stack : List (bt A)) → (tr to : bt A) → RB→bt A grand ≡ tr →  RB→bt A orig ≡ to → (si : stackInvariant key tr to stack ) 
       → (pg : ParentGrand (RB→bt A tree) (RB→bt A parent) tr ) → t
-    insertCase2 tree parent grand stack tr to treq toeq si pg with color A parent
-    ... | Black = next grand ? ? stack si ?
-    ... | Red = ? where
-        insertCase4 : (key1 : ℕ) → (si : ParentGrand ? ? ? ) →  {k1 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) → t
-        insertCase4 = ?
-        insertCase3 : (key1 : ℕ) → (si : ParentGrand ? ? ? ) →  {k1 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) → t
-        insertCase3 key1 si parent grandparent = ?
-    insertCase1 : (stack : List (bt A)) → (tr to : bt A) → RB→bt A tree ≡ tr →  RB→bt A orig ≡ to → (si : stackInvariant key tr to stack ) → t
-    insertCase1 .(tr ∷ []) tr .tr req oeq s-nil = ?
-    insertCase1 .(tr ∷ node _ _ _ tr ∷ []) tr .(node _ _ _ tr) req oeq (s-right x s-nil) = ?
-    insertCase1 .(tr ∷ node _ _ _ tr ∷ _) tr to req oeq (s-right x (s-right x₁ si)) = ?
-    insertCase1 .(tr ∷ node _ _ _ tr ∷ _) tr to req oeq (s-right x (s-left x₁ si)) = ?
-    insertCase1 .(tr ∷ node _ _ tr _ ∷ []) tr .(node _ _ tr _) req oeq (s-left x s-nil) = ?
-    insertCase1 .(tr ∷ node _ _ tr _ ∷ _) tr to req oeq (s-left x (s-right x₁ si)) = ?
-    insertCase1 .(tr ∷ node _ _ tr _ ∷ _) tr to req oeq (s-left x (s-left x₁ si)) = ?
+    insertCase2 tree parent grand stack tr to treq toeq si pg = ?
+    insertCase1 : {k1 d1 : ℕ} {c1 : Color } (tree : RBTree A k1 c1 d1)
+       (stack : List (bt A)) → (tr to : bt A) → RB→bt A tree ≡ tr →  RB→bt A orig ≡ to → (si : stackInvariant key tr to stack ) → t
+    insertCase1 (rb-leaf _) .(RB→bt A (rb-leaf _) ∷ []) .(RB→bt A (rb-leaf _)) .(RB→bt A (rb-leaf _)) refl oeq s-nil = ?
+    insertCase1 (rb-leaf _) .(RB→bt A (rb-leaf _) ∷ _) .(RB→bt A (rb-leaf _)) to refl oeq (s-right x si) = ?
+    insertCase1 (rb-leaf _) .(RB→bt A (rb-leaf _) ∷ _) .(RB→bt A (rb-leaf _)) to refl oeq (s-left x si) = ?
+    insertCase1 (rb-single _ value _) .(tr ∷ []) tr .tr req oeq s-nil = ?
+    insertCase1 (rb-single _ value _) .(tr ∷ _) tr to req oeq (s-right x si) = ?
+    insertCase1 (rb-single _ value _) .(tr ∷ _) tr to req oeq (s-left x si) = ?
+    insertCase1 (t-right-red _ value x (rb-leaf _)) stack tr to req oeq si = ?
+    insertCase1 (t-right-red _ value x (rb-single _ value₁ .Black)) stack tr to req oeq si = ?
+    insertCase1 (t-right-red _ value x (t-right-black _ value₁ x₁ tree)) stack tr to req oeq si = ?
+    insertCase1 (t-right-red _ value x (t-left-black _ value₁ x₁ tree)) stack tr to req oeq si = ?
+    insertCase1 (t-right-red _ value x (t-node-black _ value₁ x₁ x₂ tree tree₁)) stack tr to req oeq si = ?
+    insertCase1 (t-right-black _ value x tree) stack tr to req oeq si = ?
+    insertCase1 (t-left-red _ value x tree) stack tr to req oeq si = ?
+    insertCase1 (t-left-black _ value x tree) stack tr to req oeq si = ?
+    insertCase1 (t-node-red _ value x x₁ tree tree₁) stack tr to req oeq si = ?
+    insertCase1 (t-node-black _ value x x₁ tree tree₁) stack tr to req oeq si = ?
 
-