--- a/hoareBinaryTree1.agda	Thu May 30 20:11:07 2024 +0900
+++ b/hoareBinaryTree1.agda	Fri May 31 10:46:03 2024 +0900
@@ -280,6 +280,36 @@
 ... | tri≈ ¬a b ¬c = node key₁ value left right
 ... | tri> ¬a ¬b c = right
 
+child-replaced-left :  {n : Level} {A : Set n} {key key₁ : ℕ}  {value : A}  {left right : bt A}  
+   → key < key₁
+   → child-replaced key (node key₁ value left right) ≡ left
+child-replaced-left {n} {A} {key} {key₁} {value} {left} {right} lt = ch00 (node key₁ value left right) refl lt where
+     ch00 : (tree : bt A) → tree ≡ node key₁ value left right → key < key₁ → child-replaced key tree ≡ left
+     ch00 (node key₁ value tree tree₁) refl lt1 with <-cmp key key₁
+     ... | tri< a ¬b ¬c = refl
+     ... | tri≈ ¬a b ¬c = ⊥-elim (¬a lt1)
+     ... | tri> ¬a ¬b c = ⊥-elim (¬a lt1)
+
+child-replaced-right :  {n : Level} {A : Set n} {key key₁ : ℕ}  {value : A}  {left right : bt A}  
+   → key₁ < key
+   → child-replaced key (node key₁ value left right) ≡ right
+child-replaced-right {n} {A} {key} {key₁} {value} {left} {right} lt = ch00 (node key₁ value left right) refl lt where
+     ch00 : (tree : bt A) → tree ≡ node key₁ value left right → key₁ < key → child-replaced key tree ≡ right
+     ch00 (node key₁ value tree tree₁) refl lt1 with <-cmp key key₁
+     ... | tri< a ¬b ¬c = ⊥-elim (¬c lt1)
+     ... | tri≈ ¬a b ¬c = ⊥-elim (¬c lt1)
+     ... | tri> ¬a ¬b c = refl
+
+child-replaced-eq :  {n : Level} {A : Set n} {key key₁ : ℕ}  {value : A}  {left right : bt A}  
+   → key₁ ≡ key
+   → child-replaced key (node key₁ value left right) ≡ node key₁ value left right
+child-replaced-eq {n} {A} {key} {key₁} {value} {left} {right} lt = ch00 (node key₁ value left right) refl lt where
+     ch00 : (tree : bt A) → tree ≡ node key₁ value left right → key₁ ≡ key → child-replaced key tree ≡ node key₁ value left right
+     ch00 (node key₁ value tree tree₁) refl lt1 with <-cmp key key₁
+     ... | tri< a ¬b ¬c = ⊥-elim (¬b (sym lt1))
+     ... | tri≈ ¬a b ¬c = refl
+     ... | tri> ¬a ¬b c = ⊥-elim (¬b (sym lt1))
+
 record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A ) (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where
    field
      tree0 : bt A
@@ -1912,11 +1942,19 @@
           suc (black-depth repl ⊔ black-depth n1) ≡⟨ cong (λ k → suc (k ⊔ black-depth n1)) (sym (RB-repl→eq _ _ (RBI.treerb r) rot)) ⟩
           suc (black-depth (RBI.tree r) ⊔ black-depth n1) ≡⟨ cong (λ k → suc (k ⊔ black-depth n1)) (RBtreeEQ (subst (λ k → RBtreeInvariant k) x rb03)) ⟩
           suc (black-depth n1 ⊔ black-depth n1) ≡⟨ ⊔-idem _ ⟩
-          suc (black-depth n1 ) ≡⟨ ? ⟩
-          suc (black-depth (PG.parent pg)) ≡⟨ ? ⟩
-          suc (black-depth (PG.uncle pg)) ≡⟨ ? ⟩
+          suc (black-depth n1 ) ≡⟨ cong suc (sym (proj2 (red-children-eq x (cong proj1 rb11) rb03 ))) ⟩
+          suc (black-depth (PG.parent pg)) ≡⟨ cong suc (RBtreeEQ (subst (λ k → RBtreeInvariant k) x₁ rb01)) ⟩
+          suc (black-depth (PG.uncle pg)) ≡⟨ to-black-eq (PG.uncle pg) (cong color uneq ) ⟩
           black-depth (to-black (PG.uncle pg)) ∎
              where open ≡-Reasoning
+       rb16 :  (tree : bt (Color ∧ A)) 
+          → tree ≡ node kg vg (PG.parent pg) (PG.uncle pg)
+          → (ti : treeInvariant (node kg vg (PG.parent pg) (PG.uncle pg))) → child-replaced key tree ≡ PG.parent pg
+       rb16 leaf eq ti = ?
+       rb16 (node key₁ value tree tree₁) eq ti with <-cmp key key₁
+       ... | tri< a ¬b ¬c = ?
+       ... | tri≈ ¬a b ¬c = ?
+       ... | tri> ¬a ¬b c = ?
        rb14 : suc (black-depth repl ⊔ black-depth n1) ⊔ black-depth (to-black (PG.uncle pg)) ≡ black-depth (child-replaced key (PG.grand pg))
        rb14 = ?
        rb15 : suc (length (PG.rest pg)) < length stack