--- a/hoareBinaryTree1.agda	Thu May 30 18:15:36 2024 +0900
+++ b/hoareBinaryTree1.agda	Thu May 30 20:11:07 2024 +0900
@@ -934,6 +934,23 @@
 to-black-eq {n} {A}  (node key₁ ⟪ Red , proj4 ⟫ tree tree₁) eq = refl
 to-black-eq {n} {A}  (node key₁ ⟪ Black , proj4 ⟫ tree tree₁) ()
 
+red-children-eq : {n : Level} {A : Set n}  {tree left right : bt (Color ∧ A)} → {key : ℕ} → {value : A} → {c : Color}
+   → tree ≡ node key ⟪ c , value ⟫ left right
+   → c ≡ Red 
+   → RBtreeInvariant tree
+   → (black-depth tree ≡ black-depth left ) ∧ (black-depth tree ≡ black-depth right)
+red-children-eq {n} {A} {.(node key₁ ⟪ Red , value₁ ⟫ left right)} {left} {right} {.key₁} {.value₁} {Red} refl eq₁ rb2@(rb-red key₁ value₁ x x₁ x₂ rb rb₁) = 
+  ⟪ ( begin
+        black-depth left ⊔ black-depth right ≡⟨ cong (λ k → black-depth left ⊔ k) (sym (RBtreeEQ rb2)) ⟩
+        black-depth left ⊔ black-depth left ≡⟨ ⊔-idem _ ⟩
+        black-depth left ∎  ) ,  (
+     begin
+        black-depth left ⊔ black-depth right ≡⟨ cong (λ k → k ⊔ black-depth right ) (RBtreeEQ rb2) ⟩
+        black-depth right ⊔ black-depth right ≡⟨ ⊔-idem _ ⟩
+        black-depth right ∎ ) ⟫ where open ≡-Reasoning
+
+red-children-eq {n} {A} {tree} {left} {right} {key} {value} {Black} eq () rb
+
 ⊔-succ : {m n : ℕ} → suc (m ⊔ n) ≡ suc m ⊔ suc n
 ⊔-succ {m} {n} = refl
 
@@ -1891,7 +1908,15 @@
           black-depth n1 ∎
              where open ≡-Reasoning
        rb12 : suc (black-depth repl ⊔ black-depth n1) ≡ black-depth (to-black (PG.uncle pg))
-       rb12 = ?
+       rb12 = begin
+          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)) ≡⟨ ? ⟩
+          black-depth (to-black (PG.uncle pg)) ∎
+             where open ≡-Reasoning
        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