--- a/hoareBinaryTree1.agda	Mon Jun 03 18:06:01 2024 +0900
+++ b/hoareBinaryTree1.agda	Tue Jun 04 09:59:51 2024 +0900
@@ -710,7 +710,7 @@
 to-black (node key ⟪ _ , value ⟫ t t₁) = (node key ⟪ Black , value ⟫ t t₁)
 
 black-depth : {n : Level} {A : Set n} → (tree : bt (Color ∧ A) ) → ℕ
-black-depth leaf = 0
+black-depth leaf = 1
 black-depth (node key ⟪ Red , value ⟫  t t₁) = black-depth t  ⊔ black-depth t₁
 black-depth (node key ⟪ Black , value ⟫  t t₁) = suc (black-depth t  ⊔ black-depth t₁ )
 
@@ -1732,15 +1732,27 @@
  → stackInvariant key tree1 tree0 stack
  → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) 
  → (exit : (r : RBI key value tree0 stack ) → t ) → t
-replaceRBTNode key value orig rbi ti leaf stack si (case1 refl) exit = exit record {
-     tree = ?
+replaceRBTNode key value .leaf rbi ti leaf .(leaf ∷ []) s-nil (case1 refl) exit = exit record {
+     tree = leaf
    ; repl = node key ⟪ Red , value ⟫ leaf leaf
    ; origti = ti
    ; origrb = rbi
-   ; treerb = ?
+   ; treerb = rb-leaf
+   ; replrb = rb-red _ value refl refl refl  rb-leaf rb-leaf
+   ; si = s-nil
+   ; state = top-black refl (case1 rbr-leaf)
+  }
+replaceRBTNode key value orig rbi ti leaf (leaf ∷ node key₁ value₁ x₁ x₂ ∷ stack) si2@(s-right .leaf .orig tree {k1} {v1} x si) (case1 refl) exit = ?
+replaceRBTNode key value orig rbi ti leaf (leaf ∷ node key₁ ⟪ Black , value₁ ⟫ x₁ x₂ ∷ stack) si2@(s-left .leaf .orig tree {k1} {v1} x si) (case1 refl) exit = ?
+replaceRBTNode key value orig rbi ti leaf (leaf ∷ node key₁ ⟪ Red , value₁ ⟫ x₁ x₂ ∷ stack) si2@(s-left .leaf .orig tree {k1} {v1} x si) (case1 refl) exit = exit record {
+     tree = leaf
+   ; repl = node key ⟪ Red , value ⟫ leaf leaf 
+   ; origti = ti
+   ; origrb = rbi
+   ; treerb = ? -- PGtoRBinvariant1 tree orig rbi stack si
    ; replrb = ?
    ; si = ?
-   ; state = rotate ? ? ?  ?
+   ; state = ?
   }
 replaceRBTNode key value orig rbi ti tree@(node key₁ value₁ left right) stack si (case2 P) exit = exit record {
      tree = tree