Mercurial > hg > Gears > GearsAgda

changeset 891:e8e8ccfd6c44

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 21 May 2024 18:43:44 +0900
parents 6a5fe1c4855a
children 6eee2a7b5288
files hoareBinaryTree1.agda
diffstat 1 files changed, 100 insertions(+), 40 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Sat May 18 16:03:40 2024 +0900
+++ b/hoareBinaryTree1.agda	Tue May 21 18:43:44 2024 +0900
@@ -696,6 +696,14 @@
 RBtreeRightDown left right (rb-red _ _ x x₁ x₂ rb rb₁) = rb₁
 RBtreeRightDown left right (rb-black _ _ x rb rb₁) = rb₁
 
+RBtreeEQ : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color}
+ → {left right : bt (Color ∧ A)}
+ → RBtreeInvariant (node key ⟪ c , value ⟫ left right)
+ → black-depth left ≡ black-depth right
+RBtreeEQ  (rb-red _ _ x x₁ x₂ rb rb₁) = x₂
+RBtreeEQ  (rb-black _ _ x rb rb₁) = x
+
+
 --
 --  findRBT exit with replaced node
 --     case-eq        node value is replaced,  just do replacedTree and rebuild rb-invariant
@@ -752,7 +760,9 @@
 data replacedRBTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt (Color ∧ A) ) → Set n where
     -- no rotation case
     rbr-leaf : replacedRBTree key value leaf (node key ⟪ Red , value ⟫ leaf leaf)
-    rbr-node : {value₁ : A} → {ca : Color } → {t t₁ : bt (Color ∧ A)} → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ ca , value ⟫ t t₁)
+    rbr-node : {value₁ : A} → {ca : Color } → {t t₁ : bt (Color ∧ A)} 
+          → black-depth t ≡ black-depth t₁
+          → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ ca , value ⟫ t t₁)
     rbr-right : {k : ℕ } {v1 : A} → {ca : Color} → {t t1 t2 : bt (Color ∧ A)}  
           → color t2 ≡ color t 
           → k < key →  replacedRBTree key value t2 t →  replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ ca , v1 ⟫ t1 t)
@@ -770,19 +780,19 @@
 
     -- case2 both parent and uncle are red (should we check uncle color?), flip color and up
     rbr-flip-ll : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
-         → color t₂ ≡ Red → key < kp  → replacedRBTree key value t₁ t₂
+         → color t₂ ≡ Red → color uncle ≡ Red → key < kp  → replacedRBTree key value t₁ t₂
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red   , vp ⟫ t₁ t)           uncle)
                                     (node kg ⟪ Red ,   vg ⟫ (node kp ⟪ Black , vp ⟫ t₂ t) (to-black uncle))
     rbr-flip-lr : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
-         → color t₂ ≡ Red →  kp < key → key < kg   → replacedRBTree key value t₁ t₂
+         → color t₂ ≡ Red → color uncle ≡ Red →  kp < key → key < kg   → replacedRBTree key value t₁ t₂
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red   , vp ⟫ t t₁)           uncle)
                                     (node kg ⟪ Red ,   vg ⟫ (node kp ⟪ Black , vp ⟫ t t₂) (to-black uncle))
     rbr-flip-rl : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
-         → color t₂ ≡ Red → kg < key → key < kp  → replacedRBTree key value t₁ t₂
+         → color t₂ ≡ Red → color uncle ≡ Red → kg < key → key < kp  → replacedRBTree key value t₁ t₂
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle            (node kp ⟪ Red   , vp ⟫ t₁ t))
                                     (node kg ⟪ Red ,   vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t₂ t))
     rbr-flip-rr : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
-         → color t₂ ≡ Red → kp < key   → replacedRBTree key value t₁ t₂
+         → color t₂ ≡ Red → color uncle ≡ Red → kp < key   → replacedRBTree key value t₁ t₂
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle            (node kp ⟪ Red   , vp ⟫ t t₁))
                                     (node kg ⟪ Red ,   vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t t₂))
 
@@ -864,10 +874,55 @@
 tr<-to-black {n} {A} {key} {leaf} tr = tt
 tr<-to-black {n} {A} {key} {node key₁ value tree tree₁} tr = tr
 
+to-black-eq : {n : Level} {A : Set n} {key : ℕ} {tree : bt (Color ∧ A)} → color tree ≡ Red → suc (black-depth tree) ≡ black-depth (to-black tree)
+to-black-eq {n} {A} {key} {leaf} ()
+to-black-eq {n} {A} {key} {node key₁ ⟪ Red , proj4 ⟫ tree tree₁} eq = refl
+to-black-eq {n} {A} {key} {node key₁ ⟪ Black , proj4 ⟫ tree tree₁} ()
+
+to-black-node-eq : {n : Level} {A : Set n} {key kn : ℕ} {value vn : A} {t₁ t₂ t₃ : bt (Color ∧ A)} 
+    → replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)
+    → ( black-depth t₁ ≡ black-depth t₂ ) ∧ ( black-depth t₁ ≡ black-depth t₃ )
+to-black-node-eq {n} {A} {key} {.key} {t₂} {.t₂} rbr-leaf = ⟪ refl , refl ⟫
+to-black-node-eq {n} {A} {key} {.key} {t₂} {.t₂} (rbr-node eq) = ⟪ trans ? (⊔-idem _) ,  ? ⟫
+to-black-node-eq {n} {A} {key} {t₁} {t₂} {t₃} (rbr-right x x₁ rr) = ?
+to-black-node-eq {n} {A} {key} {t₁} {t₂} {t₃} (rbr-left x x₁ rr) = ?
+to-black-node-eq {n} {A} {key} {t₁} {t₂} {t₃} (rbr-flip-ll x x₁ x₂ rr) = ?
+to-black-node-eq {n} {A} {key} {t₁} {t₂} {t₃} (rbr-flip-lr x x₁ x₂ x₃ rr) = ?
+to-black-node-eq {n} {A} {key} {t₁} {t₂} {t₃} (rbr-flip-rl x x₁ x₂ x₃ rr) = ?
+to-black-node-eq {n} {A} {key} {t₁} {t₂} {t₃} (rbr-flip-rr x x₁ x₂ rr) = ?
+
+RB-repl→eq  : {n : Level} {A : Set n}  → (tree repl : bt (Color ∧ A)) → {key : ℕ} → {value : A}
+     → replacedRBTree key value tree repl → black-depth tree ≡ black-depth repl
+RB-repl→eq {n} {A} .leaf .(node _ ⟪ Red , _ ⟫ leaf leaf) rbr-leaf = refl
+RB-repl→eq {n} {A} (node _ ⟪ Red , _ ⟫ _ _) .(node _ ⟪ Red , _ ⟫ _ _) (rbr-node _) = refl
+RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) (rbr-node _) = refl
+RB-repl→eq {n} {A} (node _ ⟪ Red , _ ⟫ left _) .(node _ ⟪ _ , _ ⟫ _ _) (rbr-right x x₁ t) = 
+   cong (λ k → black-depth left ⊔ k ) (RB-repl→eq _ _ t) 
+RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ left _) .(node _ ⟪ _ , _ ⟫ _ _) (rbr-right x x₁ t) = 
+   cong (λ k → suc (black-depth left ⊔ k )) (RB-repl→eq _ _ t) 
+RB-repl→eq {n} {A} (node _ ⟪ Red , _ ⟫ _ right) .(node _ ⟪ _ , _ ⟫ _ _) (rbr-left x x₁ t) = 
+   cong (λ k → k ⊔ black-depth right ) (RB-repl→eq _ _ t)
+RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ _ right) .(node _ ⟪ _ , _ ⟫ _ _) (rbr-left x x₁ t) =
+   cong (λ k → suc (k ⊔ black-depth right )) (RB-repl→eq _ _ t)
+RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ t₁ _) .(node _ ⟪ Black , _ ⟫ _ _) (rbr-black-right x x₁ t) = 
+   cong (λ k → suc (black-depth t₁ ⊔ k)) (RB-repl→eq _ _ t)
+RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ _ t₁) .(node _ ⟪ Black , _ ⟫ _ _) (rbr-black-left x x₁ t) = 
+   cong (λ k → suc (k ⊔ black-depth t₁ )) (RB-repl→eq _ _ t)
+RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ t₁ t₂) t₃) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) (rbr-flip-ll x x₁ x₂ t) = 
+   trans (cong suc (⊔-assoc (black-depth t₁) (black-depth t₂) (black-depth t₃) )) ? -- ( cong (λ k → (black-depth t₁ ⊔ black-depth t₂ ⊔ k)) (RB-repl→eq _ _ t))
+RB-repl→eq {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) (rbr-flip-lr x x₁ x₂ x₃ t) = ?
+RB-repl→eq {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) (rbr-flip-rl x x₁ x₂ x₃ t) = ?
+RB-repl→eq {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) (rbr-flip-rr x x₁ x₂ t) = ?
+RB-repl→eq {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) (rbr-rotate-ll x x₁ t) = ?
+RB-repl→eq {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) (rbr-rotate-rr x x₁ t) = ?
+RB-repl→eq {n} {A} .(node kg ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ _) _) .(node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₂) (node kg ⟪ Red , _ ⟫ t₃ _)) (rbr-rotate-lr t₂ t₃ kg kp kn x x₁ x₂ t) = ?
+RB-repl→eq {n} {A} .(node kg ⟪ Black , _ ⟫ _ (node kp ⟪ Red , _ ⟫ _ _)) .(node kn ⟪ Black , _ ⟫ (node kg ⟪ Red , _ ⟫ _ t₂) (node kp ⟪ Red , _ ⟫ t₃ _)) (rbr-rotate-rl t₂ t₃ kg kp kn x x₁ x₂ t) = ?
+
+     
 RB-repl→ti>  : {n : Level} {A : Set n}  → (tree repl : bt (Color ∧ A)) → (key key₁ : ℕ) → (value : A)
      → replacedRBTree key value tree repl → key₁ < key → tr> key₁ tree → tr> key₁ repl
 RB-repl→ti> .leaf .(node key ⟪ Red , value ⟫ leaf leaf) key key₁ value rbr-leaf lt tr = ⟪ lt , ⟪ tt , tt ⟫ ⟫
-RB-repl→ti> .(node key ⟪ _ , _ ⟫ _ _) .(node key ⟪ _ , value ⟫ _ _) key key₁ value rbr-node lt tr = tr
+RB-repl→ti> .(node key ⟪ _ , _ ⟫ _ _) .(node key ⟪ _ , value ⟫ _ _) key key₁ value (rbr-node _) lt tr = tr
 RB-repl→ti> .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-right _ x rbt) lt tr
    = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti> _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫
 RB-repl→ti> .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-left _ x rbt) lt tr
@@ -876,15 +931,15 @@
    = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti> _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫
 RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-left x _ rbt) lt tr
    = ⟪ proj1 tr , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt (proj1 (proj2 tr)) , proj2 (proj2 tr) ⟫ ⟫
-RB-repl→ti> .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value (rbr-flip-ll x _ rbt) lt tr
+RB-repl→ti> .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value (rbr-flip-ll x _ _ rbt) lt tr
    = ⟪ proj1 tr , ⟪ ⟪ proj1 (proj1 (proj2 tr))  , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt (proj1 (proj2 (proj1 (proj2 tr))))
        , proj2 (proj2 (proj1 (proj2 tr))) ⟫ ⟫  , tr>-to-black (proj2 (proj2 tr)) ⟫ ⟫
 RB-repl→ti> .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value
-   (rbr-flip-lr x _ _ rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 ,  RB-repl→ti> _ _ _ _ _ rbt lt tr7 ⟫ ⟫  , tr>-to-black tr5 ⟫ ⟫
+   (rbr-flip-lr x _ _ _ rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 ,  RB-repl→ti> _ _ _ _ _ rbt lt tr7 ⟫ ⟫  , tr>-to-black tr5 ⟫ ⟫
 RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key key₁ value
-   (rbr-flip-rl x _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫  ⟫ ⟫ = ⟪ tr3 , ⟪ tr>-to-black tr5 , ⟪ tr4 , ⟪  RB-repl→ti> _ _ _ _ _ rbt lt tr6 , tr7 ⟫ ⟫   ⟫ ⟫
+   (rbr-flip-rl x _ _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫  ⟫ ⟫ = ⟪ tr3 , ⟪ tr>-to-black tr5 , ⟪ tr4 , ⟪  RB-repl→ti> _ _ _ _ _ rbt lt tr6 , tr7 ⟫ ⟫   ⟫ ⟫
 RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key key₁ value
-   (rbr-flip-rr x _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr3 , ⟪ tr>-to-black tr5 , ⟪ tr4 , ⟪ tr6 ,  RB-repl→ti> _ _ _ _ _ rbt lt tr7 ⟫ ⟫   ⟫ ⟫
+   (rbr-flip-rr x _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr3 , ⟪ tr>-to-black tr5 , ⟪ tr4 , ⟪ tr6 ,  RB-repl→ti> _ _ _ _ _ rbt lt tr7 ⟫ ⟫   ⟫ ⟫
 RB-repl→ti> .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value
    (rbr-rotate-ll x lt2 rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5  ⟫ ⟫  = ⟪ tr4 , ⟪  RB-repl→ti> _ _ _ _ _ rbt lt tr6 , ⟪ tr3 , ⟪ tr7 , tr5 ⟫ ⟫ ⟫ ⟫
 RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) key key₁ value
@@ -905,7 +960,7 @@
 RB-repl→ti<  : {n : Level} {A : Set n}  → (tree repl : bt (Color ∧ A)) → (key key₁ : ℕ) → (value : A)
      → replacedRBTree key value tree repl → key < key₁ → tr< key₁ tree → tr< key₁ repl
 RB-repl→ti< .leaf .(node key ⟪ Red , value ⟫ leaf leaf) key key₁ value rbr-leaf lt tr = ⟪ lt , ⟪ tt , tt ⟫ ⟫
-RB-repl→ti< .(node key ⟪ _ , _ ⟫ _ _) .(node key ⟪ _ , value ⟫ _ _) key key₁ value rbr-node lt tr = tr
+RB-repl→ti< .(node key ⟪ _ , _ ⟫ _ _) .(node key ⟪ _ , value ⟫ _ _) key key₁ value (rbr-node _) lt tr = tr
 RB-repl→ti< .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-right _ x rbt) lt tr
    = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti< _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫
 RB-repl→ti< .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-left _ x rbt) lt tr
@@ -914,15 +969,15 @@
    = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti< _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫
 RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-left x _ rbt) lt tr
    = ⟪ proj1 tr , ⟪ RB-repl→ti< _ _ _ _ _ rbt lt (proj1 (proj2 tr)) , proj2 (proj2 tr) ⟫ ⟫
-RB-repl→ti< .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value (rbr-flip-ll x _ rbt) lt tr
+RB-repl→ti< .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value (rbr-flip-ll x _ _ rbt) lt tr
    = ⟪ proj1 tr , ⟪ ⟪ proj1 (proj1 (proj2 tr))  , ⟪ RB-repl→ti< _ _ _ _ _ rbt lt (proj1 (proj2 (proj1 (proj2 tr))))
        , proj2 (proj2 (proj1 (proj2 tr))) ⟫ ⟫  , tr<-to-black (proj2 (proj2 tr)) ⟫ ⟫
 RB-repl→ti< .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value
-   (rbr-flip-lr x _ _ rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 ,  RB-repl→ti< _ _ _ _ _ rbt lt tr7 ⟫ ⟫  , tr<-to-black tr5 ⟫ ⟫
+   (rbr-flip-lr x _ _ _ rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 ,  RB-repl→ti< _ _ _ _ _ rbt lt tr7 ⟫ ⟫  , tr<-to-black tr5 ⟫ ⟫
 RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key key₁ value
-   (rbr-flip-rl x _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫  ⟫ ⟫ = ⟪ tr3 , ⟪ tr<-to-black tr5 , ⟪ tr4 , ⟪  RB-repl→ti< _ _ _ _ _ rbt lt tr6 , tr7 ⟫ ⟫   ⟫ ⟫
+   (rbr-flip-rl x _ _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫  ⟫ ⟫ = ⟪ tr3 , ⟪ tr<-to-black tr5 , ⟪ tr4 , ⟪  RB-repl→ti< _ _ _ _ _ rbt lt tr6 , tr7 ⟫ ⟫   ⟫ ⟫
 RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key key₁ value
-   (rbr-flip-rr x _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr3 , ⟪ tr<-to-black tr5 , ⟪ tr4 , ⟪ tr6 ,  RB-repl→ti< _ _ _ _ _ rbt lt tr7 ⟫ ⟫   ⟫ ⟫
+   (rbr-flip-rr x _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr3 , ⟪ tr<-to-black tr5 , ⟪ tr4 , ⟪ tr6 ,  RB-repl→ti< _ _ _ _ _ rbt lt tr7 ⟫ ⟫   ⟫ ⟫
 RB-repl→ti< .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value
    (rbr-rotate-ll x lt2 rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5  ⟫ ⟫  = ⟪ tr4 , ⟪  RB-repl→ti< _ _ _ _ _ rbt lt tr6 , ⟪ tr3 , ⟪ tr7 , tr5 ⟫ ⟫ ⟫ ⟫
 RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) key key₁ value
@@ -943,13 +998,13 @@
 RB-repl→ti : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A) ) → (key : ℕ ) → (value : A) → treeInvariant tree 
        → replacedRBTree key value tree repl → treeInvariant repl
 RB-repl→ti .leaf .(node key ⟪ Red , value ⟫ leaf leaf) key value ti rbr-leaf = t-single key ⟪ Red , value ⟫
-RB-repl→ti .(node key ⟪ _ , _ ⟫ leaf leaf) .(node key ⟪ _ , value ⟫ leaf leaf) key value (t-single .key .(⟪ _ , _ ⟫)) rbr-node = t-single key ⟪ _ , value ⟫
+RB-repl→ti .(node key ⟪ _ , _ ⟫ leaf leaf) .(node key ⟪ _ , value ⟫ leaf leaf) key value (t-single .key .(⟪ _ , _ ⟫)) (rbr-node _) = t-single key ⟪ _ , value ⟫
 RB-repl→ti .(node key ⟪ _ , _ ⟫ leaf (node key₁ _ _ _)) .(node key ⟪ _ , value ⟫ leaf (node key₁ _ _ _)) key value 
-   (t-right .key key₁ x x₁ x₂ ti) rbr-node = t-right key key₁ x x₁ x₂ ti
+   (t-right .key key₁ x x₁ x₂ ti) (rbr-node _) = t-right key key₁ x x₁ x₂ ti
 RB-repl→ti .(node key ⟪ _ , _ ⟫ (node key₁ _ _ _) leaf) .(node key ⟪ _ , value ⟫ (node key₁ _ _ _) leaf) key value 
-   (t-left key₁ .key x x₁ x₂ ti) rbr-node = t-left key₁ key x x₁ x₂ ti
+   (t-left key₁ .key x x₁ x₂ ti) (rbr-node _) = t-left key₁ key x x₁ x₂ ti
 RB-repl→ti .(node key ⟪ _ , _ ⟫ (node key₁ _ _ _) (node key₂ _ _ _)) .(node key ⟪ _ , value ⟫ (node key₁ _ _ _) (node key₂ _ _ _)) key value 
-   (t-node key₁ .key key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) rbr-node = t-node key₁ key key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁
+   (t-node key₁ .key key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-node _) = t-node key₁ key key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁
 RB-repl→ti (node key₁ ⟪ ca , v1 ⟫ leaf leaf) (node key₁ ⟪ ca , v1 ⟫ leaf tree@(node key₂ value₁ t t₁)) key value 
    (t-single key₁ ⟪ ca , v1 ⟫) (rbr-right _ x trb) = t-right _ _  (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ t-leaf trb) where
         rr00 : (key₁ < key₂ ) ∧ tr> key₁ t ∧ tr> key₁ t₁
@@ -1017,49 +1072,49 @@
         rr00 : (key₄ < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁
         rr00 = RB-repl→ti< _ _ _ _ _ trb x₇ ⟪ x₁ , ⟪ x₃ , x₄ ⟫ ⟫
 RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ t₁) leaf) (node key₂ ⟪ Red , value₁ ⟫ (node key₁ ⟪ Black , value₂ ⟫ t t₁) .(to-black leaf)) key value 
-      (t-left _ .key₂ x₁ x₂ x₃ ti) (rbr-flip-ll x lt trb) = t-left _ _ x₁ rr00 x₃ (RTtoTI0 _ _ _ _ rr02 r-node ) where
+      (t-left _ .key₂ x₁ x₂ x₃ ti) (rbr-flip-ll x _ lt trb) = t-left _ _ x₁ rr00 x₃ (RTtoTI0 _ _ _ _ rr02 r-node ) where
         rr00 : tr< key₂ t 
         rr00 = RB-repl→ti< _ _ _ _ _ trb (<-trans lt x₁) x₂
         rr02 : treeInvariant (node key₁ ⟪ Red , value₂  ⟫ t t₁)
         rr02 = RB-repl→ti _ _ _ _ ti (rbr-left _ lt trb)
 RB-repl→ti (node key₂ ⟪ Black , _ ⟫ (node key₁ ⟪ Red , _ ⟫ t₀ t₁) (node key₃ ⟪ c1 , v1 ⟫  left right)) (node key₂ ⟪ Red , value₁ ⟫ (node _ ⟪ Black , value₂ ⟫ t t₁) (node key₃ ⟪ Black , v1 ⟫  left  right)) key value 
-       (t-node _ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-ll x lt trb) = t-node _ _ _ x₁ x₂ rr00 x₄ x₅ x₆ (RTtoTI0 _ _ _ _ rr02 r-node ) (RTtoTI0 _ _ _ _ ti₁ r-node ) where
+       (t-node _ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-ll x _ lt trb) = t-node _ _ _ x₁ x₂ rr00 x₄ x₅ x₆ (RTtoTI0 _ _ _ _ rr02 r-node ) (RTtoTI0 _ _ _ _ ti₁ r-node ) where
         rr00 : tr< key₂ t
         rr00 = RB-repl→ti< _ _ _ _ _ trb (<-trans lt x₁)  x₃
         rr02 : treeInvariant (node key₁ ⟪ Red , value₂ ⟫ t t₁)
         rr02  = RB-repl→ti _ _ _ _ ti (rbr-left _ lt trb)
 RB-repl→ti (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ left right) leaf) (node key₂ ⟪ Red , v1 ⟫ (node key₃ ⟪ Black , v2 ⟫ left right₁) leaf) key value 
-      (t-left _ _ x₁ x₂ x₃ ti) (rbr-flip-lr x lt lt2 trb) = t-left _ _ x₁ x₂ rr00 (RTtoTI0 _ _ _ _ rr02 r-node ) where
+      (t-left _ _ x₁ x₂ x₃ ti) (rbr-flip-lr x _ lt lt2 trb) = t-left _ _ x₁ x₂ rr00 (RTtoTI0 _ _ _ _ rr02 r-node ) where
         rr00 : tr< key₂ right₁
         rr00 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃
         rr02 : treeInvariant (node key₃ ⟪ Red , v2 ⟫ left right₁ )
         rr02 = RB-repl→ti _ _ _ _ ti (rbr-right _ lt trb)
 RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ Red , v2 ⟫ t t₁) (node key₃ ⟪ c3 , v3 ⟫ t₂ t₃)) (node key₁ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ t t₄) .(to-black (node key₃ ⟪ c3 , _ ⟫ _ _))) key value 
-      (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-lr x lt lt2 trb) = t-node _ _ _ x₁ x₂ x₃ rr00 x₅ x₆ (RTtoTI0 _ _ _ _ rr02 r-node ) (RTtoTI0 _ _ _ _ ti₁ r-node ) where
+      (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-lr x _ lt lt2 trb) = t-node _ _ _ x₁ x₂ x₃ rr00 x₅ x₆ (RTtoTI0 _ _ _ _ rr02 r-node ) (RTtoTI0 _ _ _ _ ti₁ r-node ) where
         rr00 : tr< key₁ t₄
         rr00 = RB-repl→ti< _ _ _ _ _ trb lt2 x₄
         rr02 : treeInvariant (node key₂ ⟪ Red , v2 ⟫ t t₄)
         rr02 = RB-repl→ti _ _ _ _ ti (rbr-right _ lt trb)
 RB-repl→ti (node _ ⟪ Black , _ ⟫ leaf (node _ ⟪ Red , _ ⟫ t t₁)) (node key₁ ⟪ Red , v1 ⟫ .(to-black leaf) (node key₂ ⟪ Black , v2 ⟫ t₂ t₁)) key value 
-      (t-right _ _ x₁ x₂ x₃ ti) (rbr-flip-rl x lt lt2 trb) = t-right _ _ x₁ rr00 x₃ (RTtoTI0 _ _ _ _ rr02 r-node ) where
+      (t-right _ _ x₁ x₂ x₃ ti) (rbr-flip-rl x _ lt lt2 trb) = t-right _ _ x₁ rr00 x₃ (RTtoTI0 _ _ _ _ rr02 r-node ) where
         rr00 : tr> key₁ t₂
         rr00 = RB-repl→ti> _ _ _ _ _ trb lt x₂
         rr02 : treeInvariant (node key₂ ⟪ Red , v2 ⟫ t₂ t₁)
         rr02 = RB-repl→ti _ _ _ _ ti (rbr-left _ lt2 trb)
 RB-repl→ti (node _ ⟪ Black , v1 ⟫ (node key₂ ⟪ c2 , v2 ⟫ t t₁) (node _ ⟪ Red , v3 ⟫ t₂ t₃)) (node key₁ ⟪ Red , _ ⟫ .(to-black (node key₂ ⟪ c2 , _ ⟫  _ _)) (node key₃ ⟪ Black , _ ⟫ t₄ t₃)) key value 
-      (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-rl x lt lt2 trb) = t-node key₂ _ _ x₁ x₂ x₃ x₄ rr00 x₆ (RTtoTI0 _ _ _ _ ti r-node ) (RTtoTI0 _ _ _ _ rr02 r-node ) where
+      (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-rl x _ lt lt2 trb) = t-node key₂ _ _ x₁ x₂ x₃ x₄ rr00 x₆ (RTtoTI0 _ _ _ _ ti r-node ) (RTtoTI0 _ _ _ _ rr02 r-node ) where
         rr00 : tr> key₁ t₄
         rr00 = RB-repl→ti> _ _ _ _ _ trb lt x₅
         rr02 : treeInvariant (node key₃ ⟪ Red , v3 ⟫ t₄ t₃)
         rr02 = RB-repl→ti _ _ _ _ ti₁ (rbr-left _ lt2 trb)
 RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ leaf (node key₂ ⟪ Red , v2 ⟫ t t₁)) (node _ ⟪ Red , _ ⟫ .(to-black leaf) (node _ ⟪ Black , v2 ⟫ t t₂)) key value 
-    (t-right _ _ x₁ x₂ x₃ ti) (rbr-flip-rr x lt trb) = t-right _ _ x₁ x₂ rr00 (RTtoTI0 _ _ _ _ rr02 r-node ) where
+    (t-right _ _ x₁ x₂ x₃ ti) (rbr-flip-rr x _ lt trb) = t-right _ _ x₁ x₂ rr00 (RTtoTI0 _ _ _ _ rr02 r-node ) where
         rr00 : tr> key₁ t₂
         rr00 = RB-repl→ti> _ _ _ _ _ trb (<-trans x₁ lt )  x₃
         rr02 : treeInvariant (node key₂ ⟪ Red , v2 ⟫ t t₂)
         rr02 = RB-repl→ti _ _ _ _ ti (rbr-right _ lt trb)
 RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ c2 , v2 ⟫ t t₁) (node key₃ ⟪ Red , c3 ⟫ t₂ t₃)) (node _ ⟪ Red , _ ⟫ .(to-black (node key₂ ⟪ c2 , _ ⟫ _ _)) (node _ ⟪ Black , c3 ⟫ t₂ t₄)) key value 
-    (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-rr x lt trb) = t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ rr00 (RTtoTI0 _ _ _ _ ti r-node ) (RTtoTI0 _ _ _ _ rr02 r-node ) where
+    (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-rr x _ lt trb) = t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ rr00 (RTtoTI0 _ _ _ _ ti r-node ) (RTtoTI0 _ _ _ _ rr02 r-node ) where
         rr00 : tr> key₁ t₄
         rr00 = RB-repl→ti> _ _ _ _ _ trb (<-trans x₂ lt) x₆
         rr02 : treeInvariant (node key₃ ⟪ Red , c3 ⟫ t₂ t₄)
@@ -1169,7 +1224,7 @@
 RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ leaf leaf) .leaf) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ leaf) (node kg ⟪ Red , _ ⟫ leaf _)) .kn _ (t-left .kp .kg x x₁ x₂ ti) (rbr-rotate-lr .leaf .leaf kg kp kn _ lt1 lt2 rbr-leaf) = t-node _ _ _ lt1 lt2 tt tt tt tt (t-single _ _) (t-single _ _)
 RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ (node key₁ value₁ t t₁) leaf) .leaf) (node kn ⟪ Black , v3 ⟫ (node kp ⟪ Red , _ ⟫ _ leaf) (node kg ⟪ Red , _ ⟫ leaf _)) .kn .v3 (t-left .kp .kg x x₁ x₂ (t-left .key₁ .kp x₃ x₄ x₅ ti)) (rbr-rotate-lr .leaf .leaf kg kp kn _ lt1 lt2 rbr-leaf) = 
     t-node _ _ _ lt1 lt2 ⟪ <-trans x₃ lt1  , ⟪ >-tr< x₄ lt1  , >-tr< x₅ lt1 ⟫ ⟫  tt tt tt (t-left _ _ x₃ x₄ x₅ ti) (t-single _ _) 
-RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .leaf (node key₁ .(⟪ Red , _ ⟫) .leaf .leaf)) .leaf) (node .key₁ ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ leaf) (node kg ⟪ Red , _ ⟫ leaf _)) .key₁ _ (t-left .kp .kg x x₁ x₂ (t-right .kp .key₁ x₃ x₄ x₅ ti)) (rbr-rotate-lr .leaf .leaf kg kp .key₁ _ lt1 lt2 rbr-node) = t-node _ _ _ lt1 lt2 tt tt tt tt (t-single _ _) (t-single _ _) 
+RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .leaf (node key₁ .(⟪ Red , _ ⟫) .leaf .leaf)) .leaf) (node .key₁ ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ leaf) (node kg ⟪ Red , _ ⟫ leaf _)) .key₁ _ (t-left .kp .kg x x₁ x₂ (t-right .kp .key₁ x₃ x₄ x₅ ti)) (rbr-rotate-lr .leaf .leaf kg kp .key₁ _ lt1 lt2 (rbr-node _)) = t-node _ _ _ lt1 lt2 tt tt tt tt (t-single _ _) (t-single _ _) 
 RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .leaf (node key₁ value₁ t₁ t₂)) .leaf) (node kn ⟪ Black , value₃ ⟫ (node kp ⟪ Red , _ ⟫ _ leaf) (node kg ⟪ Red , _ ⟫ (node key₂ value₂ t₄ t₅) t₆)) key value (t-left .kp .kg x x₁ x₂ (t-right .kp .key₁ x₃ x₄ x₅ ti)) (rbr-rotate-lr .leaf .(node key₂ value₂ t₄ t₅) kg kp kn _ lt1 lt2 trb) = 
    t-node _ _ _ (proj1 rr00) (proj1 rr01) tt tt rr03 tt (t-single _ _) (t-left _ _ (proj1 rr02) (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) (treeRightDown _ _ ( RB-repl→ti _ _ _ _ ti trb))) where
         rr00 : (kp < kn) ∧ ⊤ ∧ ((kp < key₂) ∧ tr> kp t₄ ∧ tr> kp t₅ )
@@ -1281,7 +1336,7 @@
         rr03 = proj1 (proj2 rr01)
         rr04 = proj2 (proj2 rr01)
 RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .leaf leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ leaf _)) .kn .vn (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .leaf .leaf kg kp kn _ lt1 lt2 rbr-leaf) = t-node _ _ _ lt1 lt2 tt tt tt tt (t-single _ _) (t-single _ _)
-RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node kn ⟪ Red , _ ⟫ leaf leaf) leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ leaf _)) .kn .vn (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .leaf .leaf kg kp kn _ lt1 lt2 rbr-node) = t-node _ _ _ lt1 lt2 tt tt tt tt (t-single _ _) (t-single _ _) 
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node kn ⟪ Red , _ ⟫ leaf leaf) leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ leaf _)) .kn .vn (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .leaf .leaf kg kp kn _ lt1 lt2 (rbr-node _)) = t-node _ _ _ lt1 lt2 tt tt tt tt (t-single _ _) (t-single _ _) 
 RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .leaf (node key₁ value₁ t₅ t₆))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ leaf _)) .kn .vn (t-right .kg .kp x x₁ x₂ (t-right .kp .key₁ x₃ x₄ x₅ ti)) (rbr-rotate-rl .leaf .leaf kg kp kn _ lt1 lt2 rbr-leaf) = t-node _ _ _ lt1 lt2 tt tt tt ⟪ <-trans lt2 x₃ , ⟪ <-tr> x₄ lt2 , <-tr> x₅ lt2 ⟫ ⟫  (t-single _ _) (t-right _ _ x₃ x₄ x₅ ti) 
 RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₂ _ _ _) (node key₁ value₁ t₅ t₆))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-right .kg .kp x x₁ x₂ (t-node key₂ .kp .key₁ x₃ x₄ x₅ x₆ x₇ x₈ ti ti₁)) (rbr-rotate-rl .leaf .leaf kg kp kn _ lt1 lt2 trb) = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt tt tt ⟪ <-trans (proj1 rr01) x₄ , ⟪ <-tr> x₇ (proj1 rr01) , <-tr> x₈ (proj1 rr01) ⟫ ⟫  (t-single _ _) (t-right _ _ x₄ x₇ x₈ ti₁) where
         rr00 : (kg < kn) ∧ ⊤ ∧ ⊤
@@ -1565,7 +1620,7 @@
 replaceRBP {n} {m} {A} {t} key value orig repl stack r next exit with RBI.state r
 ... | rebuild bdepth-eq rot = rebuildRBT key value orig repl stack r bdepth-eq next exit
 ... | top-black eq rot = {!!}
-... | rotate repl-red pbdeth< rot with stackToPG (RBI.tree r) orig stack (RBI.si r)
+... | rotate repl-red pdepth< rot with stackToPG (RBI.tree r) orig stack (RBI.si r)
 ... | case1 eq  = exit repl stack eq r     -- no stack, replace top node
 ... | case2 (case1 eq) = insertCase12 orig refl (RBI.si r)  where
     --
@@ -1589,21 +1644,26 @@
          ; origti = RBI.origti r
          ; origrb = RBI.origrb r
          ; treerb = RBI.origrb r
-         ; replrb = {!!} -- subst (λ k → RBtreeInvariant (node key₁ k repl right)) ? (rb-left-red ? ? ?)
+         ; replrb = rb-black _ _ rb06 (RBI.replrb r) (RBtreeRightDown _ _ (RBI.origrb r))
          ; si = s-nil
-         -- subst (λ k →  replacedRBTree key value k (node key₁ ⟪ Black , proj2 value₁ ⟫ repl right)) ? (rbr-black-left repl-red a (RBI.rotated r))
-         -- rbr-black-left ? ? ?
-         -- rbr-left a (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) (RBI.rotated r))
-         ; state = rebuild {!!} {!!}
+         ; state = top-black  refl (rbr-black-left repl-red a (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) rot))
          } where
        rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → left ≡ RBI.tree r
        rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x s-nil) refl refl = refl
        rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl with si-property1 si
        ... | refl = ⊥-elim ( nat-<> x a  )
-       -- rb05 : replacedRBTree key value (RBI.tree r) repl
-       -- rb05 = RBI.rotated r
-       rb06 : RBtreeInvariant (to-red (node key₁ value₁ repl right))
-       rb06 = {!!}
+       rb05 : child-replaced key (node key₁ value₁ left right) ≡ left
+       rb05 with <-cmp key key₁
+       ... | tri< a ¬b ¬c = refl
+       ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a)
+       ... | tri> ¬a ¬b c = ⊥-elim (¬a a)
+       rb06 : black-depth repl ≡ black-depth right
+       rb06 = begin
+         black-depth repl ≡⟨ sym (RB-repl→eq _ _ rot) ⟩
+         black-depth (RBI.tree r) ≡⟨ ? ⟩
+         black-depth left ≡⟨ (RBtreeEQ (RBI.origrb r)) ⟩
+         black-depth right ∎ 
+            where open ≡-Reasoning
     ... | tri≈ ¬a b ¬c | cr = ⊥-elim ( rb06 _ eq (RBI.si r) b ) where -- can't happen
        rb06 : (stack    : List (bt (Color ∧ A))) → stack ≡ RBI.tree r ∷ node key₁ value₁ left right ∷ [] 
          →  stackInvariant key (RBI.tree r) (node key₁ value₁ left right) stack
@@ -1611,7 +1671,7 @@
          → ⊥
        rb06 (.right ∷ node key₁ value₁ left right ∷ []) refl (s-right .right .(node key₁ value₁ left right) .left x s-nil) eq = ⊥-elim ( nat-≡< (sym eq) x)
        rb06 (.left ∷ node key₁ value₁ left right ∷ []) refl (s-left .left .(node key₁ value₁ left right) .right x s-nil) eq = ⊥-elim ( nat-≡< eq x)
-    ... | tri> ¬a ¬b c | cr = insertCase13 value₁ refl pbdeth< where
+    ... | tri> ¬a ¬b c | cr = insertCase13 value₁ refl pdepth< where
        rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → right ≡ RBI.tree r
        rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl = refl
        rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x si) refl refl with si-property1 si