Mercurial > hg > Gears > GearsAgda
changeset 893:78d98511779a
... rbrtree eq
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 27 May 2024 08:46:10 +0900 |
| parents | 6eee2a7b5288 |
| children | 9570d950d440 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 153 insertions(+), 133 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Wed May 22 10:58:34 2024 +0900 +++ b/hoareBinaryTree1.agda Mon May 27 08:46:10 2024 +0900 @@ -664,12 +664,12 @@ data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where rb-leaf : RBtreeInvariant leaf - rb-red : (key : ℕ) → (value : A) → {left right : bt (Color ∧ A)} + rb-red : (key : ℕ) → (value : A) → {left right : bt (Color ∧ A)} → color left ≡ Black → color right ≡ Black → black-depth left ≡ black-depth right → RBtreeInvariant left → RBtreeInvariant right → RBtreeInvariant (node key ⟪ Red , value ⟫ left right) - rb-black : (key : ℕ) → (value : A) → {left right : bt (Color ∧ A)} + rb-black : (key : ℕ) → (value : A) → {left right : bt (Color ∧ A)} → black-depth left ≡ black-depth right → RBtreeInvariant left → RBtreeInvariant right → RBtreeInvariant (node key ⟪ Black , value ⟫ left right) @@ -760,14 +760,13 @@ 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)} - → black-depth t ≡ black-depth t₁ + 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-right : {k : ℕ } {v1 : A} → {ca : Color} → {t t1 t2 : bt (Color ∧ A)} - → color t2 ≡ color 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) rbr-left : {k : ℕ } {v1 : A} → {ca : Color} → {t t1 t2 : bt (Color ∧ A)} - → color t1 ≡ color t + → color t1 ≡ color t → key < k → replacedRBTree key value t1 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ ca , v1 ⟫ t t2) -- k < key → key < k -- in all other case, color of replaced node is changed from Black to Red -- case1 parent is black @@ -852,9 +851,9 @@ rotate : {tree repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → color repl ≡ Red → black-depth repl ≡ black-depth (child-replaced key tree) → (rotated : replacedRBTree key value tree repl) → RBI-state key value tree repl stack -- two stages up - top-black : {tree repl : bt (Color ∧ A) } → {stack : List (bt (Color ∧ A))} → stack ≡ tree ∷ [] + top-black : {tree repl : bt (Color ∧ A) } → {stack : List (bt (Color ∧ A))} → stack ≡ tree ∷ [] → (rotated : replacedRBTree key value (to-black tree) repl) - → RBI-state key value tree repl stack + → RBI-state key value tree repl stack record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A))) : Set n where field @@ -874,57 +873,77 @@ 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-eq : {n : Level} {A : Set n} (tree : bt (Color ∧ A)) → color tree ≡ Red → suc (black-depth tree) ≡ black-depth (to-black tree) +to-black-eq {n} {A} (leaf) () +to-black-eq {n} {A} (node key₁ ⟪ Red , proj4 ⟫ tree tree₁) eq = refl +to-black-eq {n} {A} (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₂} {_} {t₃} {t₄} (rbr-node eq) = - ⟪ trans (cong (λ k → black-depth t₃ ⊔ k) (sym eq) ) (⊔-idem _) , - trans (cong (λ k → k ⊔ black-depth t₄ ) eq ) (⊔-idem _) ⟫ -to-black-node-eq {n} {A} {key} {t₁} {t₂} {t₃} {.(node t₁ ⟪ Red , t₃ ⟫ t₅ t₉)} {t₅} {node key₁ value t₆ t₇} (rbr-right {_} {_} {_} {.(node key₁ value t₆ t₇)} {.t₅} {t₉} 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) = ? +⊔-succ : {m n : ℕ} → suc (m ⊔ n) ≡ suc m ⊔ suc n +⊔-succ {m} {n} = refl RB-repl→eq : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A)) → {key : ℕ} → {value : A} + → RBtreeInvariant tree → 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→eq {n} {A} .leaf .(node _ ⟪ Red , _ ⟫ leaf leaf) rbt rbr-leaf = refl +RB-repl→eq {n} {A} (node _ ⟪ Red , _ ⟫ _ _) .(node _ ⟪ Red , _ ⟫ _ _) rbt rbr-node = refl +RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) rbt rbr-node = refl +RB-repl→eq {n} {A} (node _ ⟪ Red , _ ⟫ left _) .(node _ ⟪ Red , _ ⟫ left _) (rb-red _ _ x₂ x₃ x₄ rbt rbt₁) (rbr-right x x₁ t) = + cong (λ k → black-depth left ⊔ k ) (RB-repl→eq _ _ rbt₁ t) +RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ left _) .(node _ ⟪ Black , _ ⟫ left _) (rb-black _ _ x₂ rbt rbt₁) (rbr-right x x₁ t) = + cong (λ k → suc (black-depth left ⊔ k)) (RB-repl→eq _ _ rbt₁ t) +RB-repl→eq {n} {A} (node _ ⟪ Red , _ ⟫ _ right) .(node _ ⟪ Red , _ ⟫ _ right) (rb-red _ _ x₂ x₃ x₄ rbt rbt₁) (rbr-left x x₁ t) = cong (λ k → k ⊔ black-depth right) (RB-repl→eq _ _ rbt t) +RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ _ right) .(node _ ⟪ Black , _ ⟫ _ right) (rb-black _ _ x₂ rbt rbt₁) (rbr-left x x₁ t) = cong (λ k → suc (k ⊔ black-depth right)) (RB-repl→eq _ _ rbt t) +RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ t₁ _) .(node _ ⟪ Black , _ ⟫ t₁ _) (rb-black _ _ x₂ rbt rbt₁) (rbr-black-right x x₁ t) = cong (λ k → suc (black-depth t₁ ⊔ k)) (RB-repl→eq _ _ rbt₁ t) +RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ _ t₁) .(node _ ⟪ Black , _ ⟫ _ t₁) (rb-black _ _ x₂ rbt rbt₁) (rbr-black-left x x₁ t) = cong (λ k → suc (k ⊔ black-depth t₁)) (RB-repl→eq _ _ rbt t) +RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ t₁ t₂) t₃) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ t₄ t₂) (to-black t₃)) (rb-black _ _ x₃ (rb-red _ _ x₄ x₅ x₆ rbt rbt₂) rbt₁) (rbr-flip-ll {_} {_} {t₄} x x₁ x₂ t) = begin + suc (black-depth t₁ ⊔ black-depth t₂ ⊔ black-depth t₃) ≡⟨ cong (λ k → suc (k ⊔ black-depth t₂ ⊔ black-depth t₃)) (RB-repl→eq _ _ rbt t) ⟩ + suc (black-depth t₄ ⊔ black-depth t₂) ⊔ suc (black-depth t₃) ≡⟨ cong (λ k → suc (black-depth t₄ ⊔ black-depth t₂) ⊔ k ) ( to-black-eq t₃ x₁ ) ⟩ + suc (black-depth t₄ ⊔ black-depth t₂) ⊔ black-depth (to-black t₃) ∎ + where open ≡-Reasoning +RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ t₁ t₂) t₃) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ t₁ t₄) (to-black t₃)) (rb-black _ _ x₄ (rb-red _ _ x₅ x₆ x₇ rbt rbt₂) rbt₁) (rbr-flip-lr {_} {_} {t₄} x x₁ x₂ x₃ t) = begin + suc (black-depth t₁ ⊔ black-depth t₂) ⊔ suc (black-depth t₃) ≡⟨ cong (λ k → suc (black-depth t₁ ⊔ black-depth t₂) ⊔ k ) ( to-black-eq t₃ x₁ ) ⟩ + suc (black-depth t₁ ⊔ black-depth t₂) ⊔ black-depth (to-black t₃) ≡⟨ cong (λ k → suc (black-depth t₁ ⊔ k ) ⊔ black-depth (to-black t₃)) (RB-repl→eq _ _ rbt₂ t) ⟩ + suc (black-depth t₁ ⊔ black-depth t₄) ⊔ black-depth (to-black t₃) ∎ + where open ≡-Reasoning +RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black t₄) (node _ ⟪ Black , _ ⟫ t₃ t₁)) (rb-black _ _ x₄ rbt (rb-red _ _ x₅ x₆ x₇ rbt₁ rbt₂)) (rbr-flip-rl {t₁} {t₂} {t₃} {t₄} x x₁ x₂ x₃ t) = begin + suc (black-depth t₄ ⊔ (black-depth t₂ ⊔ black-depth t₁)) ≡⟨ cong (λ k → suc (black-depth t₄ ⊔ ( k ⊔ black-depth t₁)) ) (RB-repl→eq _ _ rbt₁ t) ⟩ + suc (black-depth t₄ ⊔ (black-depth t₃ ⊔ black-depth t₁)) ≡⟨ cong (λ k → k ⊔ suc (black-depth t₃ ⊔ black-depth t₁)) ( to-black-eq t₄ x₁ ) ⟩ + black-depth (to-black t₄) ⊔ suc (black-depth t₃ ⊔ black-depth t₁) ∎ + where open ≡-Reasoning +RB-repl→eq {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) (rb-black _ _ x₃ rbt (rb-red _ _ x₄ x₅ x₆ rbt₁ rbt₂)) (rbr-flip-rr {t₁} {t₂} {t₃} {t₄} x x₁ x₂ t) = begin + suc (black-depth t₄ ⊔ (black-depth t₁ ⊔ black-depth t₂)) ≡⟨ cong (λ k → suc (black-depth t₄ ⊔ (black-depth t₁ ⊔ k ))) ( RB-repl→eq _ _ rbt₂ t) ⟩ + suc (black-depth t₄ ⊔ (black-depth t₁ ⊔ black-depth t₃)) ≡⟨ cong (λ k → k ⊔ suc (black-depth t₁ ⊔ black-depth t₃)) ( to-black-eq t₄ x₁ ) ⟩ + black-depth (to-black t₄) ⊔ suc (black-depth t₁ ⊔ black-depth t₃) ∎ + where open ≡-Reasoning +RB-repl→eq {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) (rb-black _ _ x₂ (rb-red _ _ x₃ x₄ x₅ rbt rbt₂) rbt₁) (rbr-rotate-ll {t₁} {t₂} {t₃} {t₄} x x₁ t) = begin + suc (black-depth t₂ ⊔ black-depth t₁ ⊔ black-depth t₄) ≡⟨ cong suc ( ⊔-assoc (black-depth t₂) (black-depth t₁) (black-depth t₄)) ⟩ + suc (black-depth t₂ ⊔ (black-depth t₁ ⊔ black-depth t₄)) ≡⟨ cong (λ k → suc (k ⊔ (black-depth t₁ ⊔ black-depth t₄)) ) (RB-repl→eq _ _ rbt t) ⟩ + suc (black-depth t₃ ⊔ (black-depth t₁ ⊔ black-depth t₄)) ∎ + where open ≡-Reasoning +RB-repl→eq {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) (rb-black _ _ x₂ rbt (rb-red _ _ x₃ x₄ x₅ rbt₁ rbt₂)) (rbr-rotate-rr {t₁} {t₂} {t₃} {t₄} x x₁ t) = begin + suc (black-depth t₄ ⊔ (black-depth t₁ ⊔ black-depth t₂)) ≡⟨ cong (λ k → suc (black-depth t₄ ⊔ (black-depth t₁ ⊔ k ))) ( RB-repl→eq _ _ rbt₂ t) ⟩ + suc (black-depth t₄ ⊔ (black-depth t₁ ⊔ black-depth t₃)) ≡⟨ cong suc (sym ( ⊔-assoc (black-depth t₄) (black-depth t₁) (black-depth t₃))) ⟩ + suc (black-depth t₄ ⊔ black-depth t₁ ⊔ black-depth t₃) ∎ + where open ≡-Reasoning +RB-repl→eq {n} {A} .(node kg ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ _) _) .(node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₂) (node kg ⟪ Red , _ ⟫ t₃ _)) (rb-black .kg _ x₃ (rb-red .kp _ x₄ x₅ x₆ rbt rbt₂) rbt₁) (rbr-rotate-lr {t₀} {t₁} {uncle} t₂ t₃ kg kp kn x x₁ x₂ t) = begin + suc (black-depth t₀ ⊔ black-depth t₁ ⊔ black-depth uncle) ≡⟨ cong suc ( ⊔-assoc (black-depth t₀) (black-depth t₁) (black-depth uncle)) ⟩ + suc (black-depth t₀ ⊔ (black-depth t₁ ⊔ black-depth uncle)) ≡⟨ cong (λ k → suc (black-depth t₀ ⊔ (k ⊔ black-depth uncle))) (RB-repl→eq _ _ rbt₂ t) ⟩ + suc (black-depth t₀ ⊔ ((black-depth t₂ ⊔ black-depth t₃) ⊔ black-depth uncle)) ≡⟨ cong (λ k → suc (black-depth t₀ ⊔ k )) ( ⊔-assoc (black-depth t₂) (black-depth t₃) (black-depth uncle)) ⟩ + suc (black-depth t₀ ⊔ (black-depth t₂ ⊔ (black-depth t₃ ⊔ black-depth uncle))) ≡⟨ cong suc (sym ( ⊔-assoc (black-depth t₀) (black-depth t₂) (black-depth t₃ ⊔ black-depth uncle))) ⟩ + suc (black-depth t₀ ⊔ black-depth t₂ ⊔ (black-depth t₃ ⊔ black-depth uncle)) ∎ + where open ≡-Reasoning +RB-repl→eq {n} {A} .(node kg ⟪ Black , _ ⟫ _ (node kp ⟪ Red , _ ⟫ _ _)) .(node kn ⟪ Black , _ ⟫ (node kg ⟪ Red , _ ⟫ _ t₂) (node kp ⟪ Red , _ ⟫ t₃ _)) (rb-black .kg _ x₃ rbt (rb-red .kp _ x₄ x₅ x₆ rbt₁ rbt₂)) (rbr-rotate-rl {t₀} {t₁} {uncle} t₂ t₃ kg kp kn x x₁ x₂ t) = begin + suc (black-depth uncle ⊔ (black-depth t₁ ⊔ black-depth t₀)) ≡⟨ cong (λ k → suc (black-depth uncle ⊔ (k ⊔ black-depth t₀))) (RB-repl→eq _ _ rbt₁ t) ⟩ + suc (black-depth uncle ⊔ ((black-depth t₂ ⊔ black-depth t₃) ⊔ black-depth t₀)) ≡⟨ cong (λ k → suc (black-depth uncle ⊔ k)) ( ⊔-assoc (black-depth t₂) (black-depth t₃) (black-depth t₀)) ⟩ + suc (black-depth uncle ⊔ (black-depth t₂ ⊔ (black-depth t₃ ⊔ black-depth t₀))) ≡⟨ cong suc (sym ( ⊔-assoc (black-depth uncle) (black-depth t₂) (black-depth t₃ ⊔ black-depth t₀))) ⟩ + suc (black-depth uncle ⊔ black-depth t₂ ⊔ (black-depth t₃ ⊔ black-depth t₀)) ∎ + where open ≡-Reasoning - + 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 @@ -949,7 +968,7 @@ RB-repl→ti> (node kg ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ _) _) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value (rbr-rotate-lr left right _ _ kn _ _ _ rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ rr00 , ⟪ ⟪ tr4 , ⟪ tr6 , proj1 (proj2 rr01) ⟫ ⟫ , ⟪ tr3 , ⟪ proj2 (proj2 rr01) , tr5 ⟫ ⟫ ⟫ ⟫ where rr01 : (key₁ < kn) ∧ tr> key₁ left ∧ tr> key₁ right - rr01 = RB-repl→ti> _ _ _ _ _ rbt lt tr7 + rr01 = RB-repl→ti> _ _ _ _ _ rbt lt tr7 rr00 : key₁ < kn rr00 = proj1 rr01 RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value @@ -962,7 +981,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 @@ -987,145 +1006,145 @@ RB-repl→ti< (node kg ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ _) _) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value (rbr-rotate-lr left right _ _ kn _ _ _ rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ rr00 , ⟪ ⟪ tr4 , ⟪ tr6 , proj1 (proj2 rr01) ⟫ ⟫ , ⟪ tr3 , ⟪ proj2 (proj2 rr01) , tr5 ⟫ ⟫ ⟫ ⟫ where rr01 : (kn < key₁ ) ∧ tr< key₁ left ∧ tr< key₁ right - rr01 = RB-repl→ti< _ _ _ _ _ rbt lt tr7 - rr00 : kn < key₁ + rr01 = RB-repl→ti< _ _ _ _ _ rbt lt tr7 + rr00 : kn < key₁ rr00 = proj1 rr01 RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value (rbr-rotate-rl left right kg kp kn _ _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ rr00 , ⟪ ⟪ tr3 , ⟪ tr5 , proj1 (proj2 rr01) ⟫ ⟫ , ⟪ tr4 , ⟪ proj2 (proj2 rr01) , tr7 ⟫ ⟫ ⟫ ⟫ where rr01 : (kn < key₁ ) ∧ tr< key₁ left ∧ tr< key₁ right rr01 = RB-repl→ti< _ _ _ _ _ rbt lt tr6 - rr00 : kn < key₁ + rr00 : kn < key₁ rr00 = proj1 rr01 -RB-repl→ti : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A) ) → (key : ℕ ) → (value : A) → treeInvariant tree +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 (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 -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 -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₁ -RB-repl→ti (node key₁ ⟪ ca , v1 ⟫ leaf leaf) (node key₁ ⟪ ca , v1 ⟫ leaf tree@(node key₂ value₁ t t₁)) 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 +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 +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₁ +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₁ rr00 = RB-repl→ti> _ _ _ _ _ trb x tt -RB-repl→ti (node _ ⟪ _ , _ ⟫ leaf (node key₁ _ _ _)) (node key₂ ⟪ ca , v1 ⟫ leaf (node key₃ value₁ t t₁)) key value +RB-repl→ti (node _ ⟪ _ , _ ⟫ leaf (node key₁ _ _ _)) (node key₂ ⟪ ca , v1 ⟫ leaf (node key₃ value₁ t t₁)) key value (t-right _ key₁ x₁ x₂ x₃ ti) (rbr-right _ x trb) = t-right _ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ ti trb) where - rr00 : (key₂ < key₃) ∧ tr> key₂ t ∧ tr> key₂ t₁ + rr00 : (key₂ < key₃) ∧ tr> key₂ t ∧ tr> key₂ t₁ rr00 = RB-repl→ti> _ _ _ _ _ trb x ⟪ x₁ , ⟪ x₂ , x₃ ⟫ ⟫ -RB-repl→ti .(node key₂ ⟪ ca , v1 ⟫ (node key₁ value₁ t t₁) leaf) (node key₂ ⟪ ca , v1 ⟫ (node key₁ value₁ t t₁) (node key₃ value₂ t₂ t₃)) key value +RB-repl→ti .(node key₂ ⟪ ca , v1 ⟫ (node key₁ value₁ t t₁) leaf) (node key₂ ⟪ ca , v1 ⟫ (node key₁ value₁ t t₁) (node key₃ value₂ t₂ t₃)) key value (t-left key₁ _ x₁ x₂ x₃ ti) (rbr-right _ x trb) = t-node _ _ _ x₁ (proj1 rr00) x₂ x₃ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) ti (RB-repl→ti _ _ _ _ t-leaf trb) where rr00 : (key₂ < key₃) ∧ tr> key₂ t₂ ∧ tr> key₂ t₃ rr00 = RB-repl→ti> _ _ _ _ _ trb x tt -RB-repl→ti .(node key₃ ⟪ ca , v1 ⟫ (node key₁ v2 t₁ t₂) (node key₂ _ _ _)) (node key₃ ⟪ ca , v1 ⟫ (node key₁ v2 t₁ t₂) (node key₄ value₁ t₃ t₄)) key value - (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-right _ x trb) = t-node _ _ _ x₁ +RB-repl→ti .(node key₃ ⟪ ca , v1 ⟫ (node key₁ v2 t₁ t₂) (node key₂ _ _ _)) (node key₃ ⟪ ca , v1 ⟫ (node key₁ v2 t₁ t₂) (node key₄ value₁ t₃ t₄)) key value + (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-right _ x trb) = t-node _ _ _ x₁ (proj1 rr00) x₃ x₄ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) ti (RB-repl→ti _ _ _ _ ti₁ trb) where rr00 : (key₃ < key₄) ∧ tr> key₃ t₃ ∧ tr> key₃ t₄ rr00 = RB-repl→ti> _ _ _ _ _ trb x ⟪ x₂ , ⟪ x₅ , x₆ ⟫ ⟫ -RB-repl→ti .(node key₁ ⟪ _ , _ ⟫ leaf leaf) (node key₁ ⟪ _ , _ ⟫ (node key₂ value₁ left left₁) leaf) key value +RB-repl→ti .(node key₁ ⟪ _ , _ ⟫ leaf leaf) (node key₁ ⟪ _ , _ ⟫ (node key₂ value₁ left left₁) leaf) key value (t-single _ .(⟪ _ , _ ⟫)) (rbr-left _ x trb) = t-left _ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ t-leaf trb) where rr00 : (key₂ < key₁) ∧ tr< key₁ left ∧ tr< key₁ left₁ rr00 = RB-repl→ti< _ _ _ _ _ trb x tt -RB-repl→ti .(node key₂ ⟪ _ , _ ⟫ leaf (node key₁ _ t₁ t₂)) (node key₂ ⟪ _ , _ ⟫ (node key₃ value₁ t t₃) (node key₁ _ t₁ t₂)) key value +RB-repl→ti .(node key₂ ⟪ _ , _ ⟫ leaf (node key₁ _ t₁ t₂)) (node key₂ ⟪ _ , _ ⟫ (node key₃ value₁ t t₃) (node key₁ _ t₁ t₂)) key value (t-right _ key₁ x₁ x₂ x₃ ti) (rbr-left _ x trb) = t-node _ _ _ (proj1 rr00) x₁ (proj1 (proj2 rr00))(proj2 (proj2 rr00)) x₂ x₃ rr01 ti where rr00 : (key₃ < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₃ rr00 = RB-repl→ti< _ _ _ _ _ trb x tt rr01 : treeInvariant (node key₃ value₁ t t₃) rr01 = RB-repl→ti _ _ _ _ t-leaf trb -RB-repl→ti .(node _ ⟪ _ , _ ⟫ (node key₁ _ _ _) leaf) (node key₃ ⟪ _ , _ ⟫ (node key₂ value₁ t t₁) leaf) key value +RB-repl→ti .(node _ ⟪ _ , _ ⟫ (node key₁ _ _ _) leaf) (node key₃ ⟪ _ , _ ⟫ (node key₂ value₁ t t₁) leaf) key value (t-left key₁ _ x₁ x₂ x₃ ti) (rbr-left _ x trb) = t-left key₂ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ ti trb) where rr00 : (key₂ < key₃) ∧ tr< key₃ t ∧ tr< key₃ t₁ rr00 = RB-repl→ti< _ _ _ _ _ trb x ⟪ x₁ , ⟪ x₂ , x₃ ⟫ ⟫ -RB-repl→ti .(node key₃ ⟪ _ , _ ⟫ (node key₁ _ _ _) (node key₂ _ t₁ t₂)) (node key₃ ⟪ _ , _ ⟫ (node key₄ value₁ t t₃) (node key₂ _ t₁ t₂)) key value +RB-repl→ti .(node key₃ ⟪ _ , _ ⟫ (node key₁ _ _ _) (node key₂ _ t₁ t₂)) (node key₃ ⟪ _ , _ ⟫ (node key₄ value₁ t t₃) (node key₂ _ t₁ t₂)) key value (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-left _ x trb) = t-node _ _ _ (proj1 rr00) x₂ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) x₅ x₆ (RB-repl→ti _ _ _ _ ti trb) ti₁ where rr00 : (key₄ < key₃) ∧ tr< key₃ t ∧ tr< key₃ t₃ rr00 = RB-repl→ti< _ _ _ _ _ trb x ⟪ x₁ , ⟪ x₃ , x₄ ⟫ ⟫ -RB-repl→ti .(node x₁ ⟪ Black , c ⟫ leaf leaf) (node x₁ ⟪ Black , c ⟫ leaf (node key₁ value₁ t t₁)) key value +RB-repl→ti .(node x₁ ⟪ Black , c ⟫ leaf leaf) (node x₁ ⟪ Black , c ⟫ leaf (node key₁ value₁ t t₁)) key value (t-single x₂ .(⟪ Black , c ⟫)) (rbr-black-right x x₄ trb) = t-right _ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ t-leaf trb) where - rr00 : (x₁ < key₁) ∧ tr> x₁ t ∧ tr> x₁ t₁ + rr00 : (x₁ < key₁) ∧ tr> x₁ t ∧ tr> x₁ t₁ rr00 = RB-repl→ti> _ _ _ _ _ trb x₄ tt -RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ leaf (node key₁ _ _ _)) (node key₂ ⟪ Black , _ ⟫ leaf (node key₃ value₁ t₂ t₃)) key value +RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ leaf (node key₁ _ _ _)) (node key₂ ⟪ Black , _ ⟫ leaf (node key₃ value₁ t₂ t₃)) key value (t-right _ key₁ x₁ x₂ x₃ ti) (rbr-black-right x x₄ trb) = t-right _ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ ti trb) where 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 key₁ _ _ _) leaf) (node key₂ ⟪ Black , _ ⟫ (node key₁ _ _ _) (node key₃ value₁ t₂ t₃)) key value (t-left key₁ _ x₁ x₂ x₃ ti) (rbr-black-right x x₄ trb) = t-node _ _ _ x₁ (proj1 rr00) x₂ x₃ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) ti (RB-repl→ti _ _ _ _ t-leaf trb) where rr00 : (key₂ < key₃) ∧ tr> key₂ t₂ ∧ tr> key₂ t₃ rr00 = RB-repl→ti> _ _ _ _ _ trb x₄ tt -RB-repl→ti .(node key₃ ⟪ Black , _ ⟫ (node key₁ _ _ _) (node key₂ _ _ _)) (node key₃ ⟪ Black , _ ⟫ (node key₁ _ _ _) (node key₄ value₁ t₂ t₃)) key value +RB-repl→ti .(node key₃ ⟪ Black , _ ⟫ (node key₁ _ _ _) (node key₂ _ _ _)) (node key₃ ⟪ Black , _ ⟫ (node key₁ _ _ _) (node key₄ value₁ t₂ t₃)) key value (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-black-right x x₇ trb) = t-node _ _ _ x₁ (proj1 rr00) x₃ x₄ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) ti (RB-repl→ti _ _ _ _ ti₁ trb) where rr00 : (key₃ < key₄) ∧ tr> key₃ t₂ ∧ tr> key₃ t₃ rr00 = RB-repl→ti> _ _ _ _ _ trb x₇ ⟪ x₂ , ⟪ x₅ , x₆ ⟫ ⟫ -RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ leaf leaf) (node key₂ ⟪ Black , _ ⟫ (node key₁ value₁ t t₁) .leaf) key value +RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ leaf leaf) (node key₂ ⟪ Black , _ ⟫ (node key₁ value₁ t t₁) .leaf) key value (t-single .key₂ .(⟪ Black , _ ⟫)) (rbr-black-left x x₇ trb) = t-left _ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ t-leaf trb) where rr00 : (key₁ < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁ rr00 = RB-repl→ti< _ _ _ _ _ trb x₇ tt -RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ leaf (node key₁ _ _ _)) (node key₂ ⟪ Black , _ ⟫ (node key₃ value₁ t t₁) .(node key₁ _ _ _)) key value +RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ leaf (node key₁ _ _ _)) (node key₂ ⟪ Black , _ ⟫ (node key₃ value₁ t t₁) .(node key₁ _ _ _)) key value (t-right .key₂ key₁ x₁ x₂ x₃ ti) (rbr-black-left x x₇ trb) = t-node _ _ _ (proj1 rr00) x₁ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) x₂ x₃ (RB-repl→ti _ _ _ _ t-leaf trb) ti where rr00 : (key₃ < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁ rr00 = RB-repl→ti< _ _ _ _ _ trb x₇ tt -RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ (node key₁ _ _ _) leaf) (node key₂ ⟪ Black , _ ⟫ (node key₃ value₁ t t₁) .leaf) key value +RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ (node key₁ _ _ _) leaf) (node key₂ ⟪ Black , _ ⟫ (node key₃ value₁ t t₁) .leaf) key value (t-left key₁ .key₂ x₁ x₂ x₃ ti) (rbr-black-left x x₇ trb) = t-left _ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ ti trb) where 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 key₁ _ _ _) (node key₃ _ _ _)) (node key₂ ⟪ Black , _ ⟫ (node key₄ value₁ t t₁) .(node key₃ _ _ _)) key value +RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ (node key₁ _ _ _) (node key₃ _ _ _)) (node key₂ ⟪ Black , _ ⟫ (node key₄ value₁ t t₁) .(node key₃ _ _ _)) key value (t-node key₁ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-black-left x x₇ trb) = t-node _ _ _ (proj1 rr00) x₂ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) x₅ x₆ (RB-repl→ti _ _ _ _ ti trb) ti₁ where 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 +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 - rr00 : tr< key₂ t + 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 +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 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 +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 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 +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 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 +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 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 +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 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 +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 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 +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 rr00 : tr> key₁ t₄ rr00 = RB-repl→ti> _ _ _ _ _ trb (<-trans x₂ lt) x₆ rr02 : treeInvariant (node key₃ ⟪ Red , c3 ⟫ t₂ t₄) rr02 = RB-repl→ti _ _ _ _ ti₁ (rbr-right _ lt trb) -RB-repl→ti {_} {A} (node k1 ⟪ Black , c1 ⟫ (node k2 ⟪ Red , c2 ⟫ .leaf .leaf) leaf) (node _ ⟪ Black , _ ⟫ (node key₁ value₁ t₂ t₃) (node _ ⟪ Red , _ ⟫ .leaf leaf)) key value (t-left _ _ x₁ x₂ x₃ +RB-repl→ti {_} {A} (node k1 ⟪ Black , c1 ⟫ (node k2 ⟪ Red , c2 ⟫ .leaf .leaf) leaf) (node _ ⟪ Black , _ ⟫ (node key₁ value₁ t₂ t₃) (node _ ⟪ Red , _ ⟫ .leaf leaf)) key value (t-left _ _ x₁ x₂ x₃ (t-single .k2 .(⟪ Red , c2 ⟫))) (rbr-rotate-ll x lt trb) = t-node _ _ _ (proj1 rr10) x₁ (proj1 (proj2 rr10)) (proj2 (proj2 rr10)) tt tt (RB-repl→ti _ _ _ _ t-leaf trb) (t-single _ _ ) where rr10 : (key₁ < k2 ) ∧ tr< k2 t₂ ∧ tr< k2 t₃ - rr10 = RB-repl→ti< _ _ _ _ _ trb lt tt -RB-repl→ti {_} {A} (node k1 ⟪ Black , c1 ⟫ (node k2 ⟪ Red , c2 ⟫ .leaf .(node key₂ _ _ _)) leaf) (node _ ⟪ Black , _ ⟫ (node key₁ value₁ t₂ t₃) (node _ ⟪ Red , _ ⟫ (node key₂ value₂ t₁ t₄) leaf)) key value + rr10 = RB-repl→ti< _ _ _ _ _ trb lt tt +RB-repl→ti {_} {A} (node k1 ⟪ Black , c1 ⟫ (node k2 ⟪ Red , c2 ⟫ .leaf .(node key₂ _ _ _)) leaf) (node _ ⟪ Black , _ ⟫ (node key₁ value₁ t₂ t₃) (node _ ⟪ Red , _ ⟫ (node key₂ value₂ t₁ t₄) leaf)) key value (t-left _ _ x₁ x₂ x₃ (t-right .k2 key₂ x₄ x₅ x₆ ti)) (rbr-rotate-ll x lt trb) = t-node _ _ _ (proj1 rr10) x₁ (proj1 (proj2 rr10)) (proj2 (proj2 rr10)) ⟪ x₄ , ⟪ x₅ , x₆ ⟫ ⟫ tt rr05 rr04 where rr10 : (key₁ < k2 ) ∧ tr< k2 t₂ ∧ tr< k2 t₃ rr10 = RB-repl→ti< _ _ _ _ _ trb lt tt @@ -1133,29 +1152,29 @@ rr04 = RTtoTI0 _ _ _ _ (t-left key₂ _ {_} {⟪ Red , c1 ⟫} {t₁} {t₄} (proj1 x₃) (proj1 (proj2 x₃)) (proj2 (proj2 x₃)) ti) r-node rr05 : treeInvariant (node key₁ value₁ t₂ t₃) rr05 = RB-repl→ti _ _ _ _ t-leaf trb -RB-repl→ti {_} {A} (node k1 ⟪ Black , c1 ⟫ (node k2 ⟪ Red , c2 ⟫ (node key₂ value₂ t₁ t₄) .leaf) leaf) (node _ ⟪ Black , _ ⟫ (node key₁ value₁ t₂ t₃) (node _ ⟪ Red , _ ⟫ .leaf leaf)) key value +RB-repl→ti {_} {A} (node k1 ⟪ Black , c1 ⟫ (node k2 ⟪ Red , c2 ⟫ (node key₂ value₂ t₁ t₄) .leaf) leaf) (node _ ⟪ Black , _ ⟫ (node key₁ value₁ t₂ t₃) (node _ ⟪ Red , _ ⟫ .leaf leaf)) key value (t-left _ _ x₁ x₂ x₃ (t-left key₂ .k2 x₄ x₅ x₆ ti)) (rbr-rotate-ll x lt trb) = t-node _ _ _ (proj1 rr10) x₁ (proj1 (proj2 rr10)) (proj2 (proj2 rr10)) tt tt (RB-repl→ti _ _ _ _ ti trb) (t-single _ _) where rr10 : (key₁ < k2 ) ∧ tr< k2 t₂ ∧ tr< k2 t₃ rr10 = RB-repl→ti< _ _ _ _ _ trb lt ⟪ x₄ , ⟪ x₅ , x₆ ⟫ ⟫ -RB-repl→ti {_} {A} (node k1 ⟪ Black , c1 ⟫ (node k2 ⟪ Red , c2 ⟫ (node key₂ value₃ left right) (node key₃ value₂ t₄ t₅)) leaf) (node _ ⟪ Black , _ ⟫ (node key₁ value₁ t₂ t₃) (node _ ⟪ Red , _ ⟫ .(node key₃ _ _ _) leaf)) key value +RB-repl→ti {_} {A} (node k1 ⟪ Black , c1 ⟫ (node k2 ⟪ Red , c2 ⟫ (node key₂ value₃ left right) (node key₃ value₂ t₄ t₅)) leaf) (node _ ⟪ Black , _ ⟫ (node key₁ value₁ t₂ t₃) (node _ ⟪ Red , _ ⟫ .(node key₃ _ _ _) leaf)) key value (t-left _ _ x₁ x₂ x₃ (t-node key₂ .k2 key₃ x₄ x₅ x₆ x₇ x₈ x₉ ti ti₁)) (rbr-rotate-ll x lt trb) = t-node _ _ _ (proj1 rr10) x₁ (proj1 (proj2 rr10)) (proj2 (proj2 rr10)) ⟪ x₅ , ⟪ x₈ , x₉ ⟫ ⟫ tt rr05 rr04 where rr06 : key < k2 rr06 = lt rr10 : (key₁ < k2) ∧ tr< k2 t₂ ∧ tr< k2 t₃ rr10 = RB-repl→ti< _ _ _ _ _ trb rr06 ⟪ x₄ , ⟪ x₆ , x₇ ⟫ ⟫ rr04 : treeInvariant (node k1 ⟪ Red , c1 ⟫ (node key₃ value₂ t₄ t₅) leaf) - rr04 = RTtoTI0 _ _ _ _ (t-left _ _ (proj1 x₃) (proj1 (proj2 x₃)) (proj2 (proj2 x₃)) ti₁ ) (r-left (proj1 x₃) r-node) + rr04 = RTtoTI0 _ _ _ _ (t-left _ _ (proj1 x₃) (proj1 (proj2 x₃)) (proj2 (proj2 x₃)) ti₁ ) (r-left (proj1 x₃) r-node) rr05 : treeInvariant (node key₁ value₁ t₂ t₃) rr05 = RB-repl→ti _ _ _ _ ti trb -RB-repl→ti (node key₁ ⟪ Black , c1 ⟫ (node key₂ ⟪ Red , c2 ⟫ .leaf .leaf) (node key₃ v3 t₂ t₃)) (node _ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) (node _ ⟪ Red , _ ⟫ .leaf (node key₃ _ _ _))) key value +RB-repl→ti (node key₁ ⟪ Black , c1 ⟫ (node key₂ ⟪ Red , c2 ⟫ .leaf .leaf) (node key₃ v3 t₂ t₃)) (node _ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) (node _ ⟪ Red , _ ⟫ .leaf (node key₃ _ _ _))) key value (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ (t-single .key₂ .(⟪ Red , c2 ⟫)) ti₁) (rbr-rotate-ll x lt trb) = t-node _ _ _ (proj1 rr00) x₁ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) tt ⟪ <-trans x₁ x₂ , ⟪ <-tr> x₅ x₁ , <-tr> x₆ x₁ ⟫ ⟫ rr02 rr03 where rr00 : (key₄ < key₂) ∧ tr< key₂ t₄ ∧ tr< key₂ t₅ rr00 = RB-repl→ti< _ _ _ _ _ trb lt tt - rr02 : treeInvariant (node key₄ value₁ t₄ t₅) + rr02 : treeInvariant (node key₄ value₁ t₄ t₅) rr02 = RB-repl→ti _ _ _ _ t-leaf trb rr03 : treeInvariant (node key₁ ⟪ Red , c1 ⟫ leaf (node key₃ v3 t₂ t₃)) rr03 = RTtoTI0 _ _ _ _ (t-right _ _ {v3} {_} x₂ x₅ x₆ ti₁) r-node -RB-repl→ti (node key₁ ⟪ Black , c1 ⟫ (node key₂ ⟪ Red , c2 ⟫ leaf (node key₅ _ _ _)) (node key₃ v3 t₂ t₃)) (node _ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) (node _ ⟪ Red , _ ⟫ (node key₅ value₂ t₁ t₆) (node key₃ _ _ _))) key value +RB-repl→ti (node key₁ ⟪ Black , c1 ⟫ (node key₂ ⟪ Red , c2 ⟫ leaf (node key₅ _ _ _)) (node key₃ v3 t₂ t₃)) (node _ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) (node _ ⟪ Red , _ ⟫ (node key₅ value₂ t₁ t₆) (node key₃ _ _ _))) key value (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ (t-right .key₂ key₅ x₇ x₈ x₉ ti) ti₁) (rbr-rotate-ll x lt trb) = t-node _ _ _ (proj1 rr00) x₁ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) ⟪ x₇ , ⟪ x₈ , x₉ ⟫ ⟫ ⟪ <-trans x₁ x₂ , ⟪ <-tr> x₅ x₁ , <-tr> x₆ x₁ ⟫ ⟫ rr02 rr03 where rr00 : (key₄ < key₂) ∧ tr< key₂ t₄ ∧ tr< key₂ t₅ rr00 = RB-repl→ti< _ _ _ _ _ trb lt tt @@ -1163,7 +1182,7 @@ rr02 = RB-repl→ti _ _ _ _ t-leaf trb rr03 : treeInvariant (node key₁ ⟪ Red , c1 ⟫ (node key₅ value₂ t₁ t₆) (node key₃ v3 t₂ t₃)) rr03 = RTtoTI0 _ _ _ _ (t-node _ _ _ {_} {v3} {_} {_} {_} {_} {_} (proj1 x₄) x₂ (proj1 (proj2 x₄)) (proj2 (proj2 x₄)) x₅ x₆ ti ti₁ ) r-node -RB-repl→ti (node key₁ ⟪ Black , c1 ⟫ (node key₂ ⟪ Red , c2 ⟫ .(node key₅ _ _ _) .leaf) (node key₃ v3 t₂ t₃)) (node _ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) (node _ ⟪ Red , _ ⟫ .leaf (node key₃ _ _ _))) key value (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ +RB-repl→ti (node key₁ ⟪ Black , c1 ⟫ (node key₂ ⟪ Red , c2 ⟫ .(node key₅ _ _ _) .leaf) (node key₃ v3 t₂ t₃)) (node _ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) (node _ ⟪ Red , _ ⟫ .leaf (node key₃ _ _ _))) key value (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ (t-left key₅ .key₂ x₇ x₈ x₉ ti) ti₁) (rbr-rotate-ll x lt trb) = t-node _ _ _ (proj1 rr00) x₁ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) tt ⟪ <-trans x₁ x₂ , ⟪ <-tr> x₅ x₁ , <-tr> x₆ x₁ ⟫ ⟫ rr02 rr04 where rr00 : (key₄ < key₂) ∧ tr< key₂ t₄ ∧ tr< key₂ t₅ rr00 = RB-repl→ti< _ _ _ _ _ trb lt ⟪ x₇ , ⟪ x₈ , x₉ ⟫ ⟫ @@ -1173,7 +1192,7 @@ rr03 = RTtoTI0 _ _ _ _ (t-node _ _ _ {_} {v3} {_} {_} {_} {_} {_} (proj1 x₃) x₂ (proj1 (proj2 x₃)) (proj2 (proj2 x₃)) x₅ x₆ ti ti₁) r-node rr04 : treeInvariant (node key₁ ⟪ Red , c1 ⟫ leaf (node key₃ v3 t₂ t₃)) rr04 = RTtoTI0 _ _ _ _ (t-right _ _ {v3} {_} x₂ x₅ x₆ ti₁) r-node -RB-repl→ti {_} {A} (node key₁ ⟪ Black , c1 ⟫ (node key₂ ⟪ Red , c2 ⟫ .(node key₅ _ _ _) (node key₆ value₆ t₆ t₇)) (node key₃ v3 t₂ t₃)) (node _ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) (node _ ⟪ Red , _ ⟫ .(node key₆ _ _ _) (node key₃ _ _ _))) key value +RB-repl→ti {_} {A} (node key₁ ⟪ Black , c1 ⟫ (node key₂ ⟪ Red , c2 ⟫ .(node key₅ _ _ _) (node key₆ value₆ t₆ t₇)) (node key₃ v3 t₂ t₃)) (node _ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) (node _ ⟪ Red , _ ⟫ .(node key₆ _ _ _) (node key₃ _ _ _))) key value (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ (t-node key₅ .key₂ key₆ x₇ x₈ x₉ x₁₀ x₁₁ x₁₂ ti ti₂) ti₁) (rbr-rotate-ll x lt trb) = t-node _ _ _ (proj1 rr00) x₁ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) ⟪ x₈ , ⟪ x₁₁ , x₁₂ ⟫ ⟫ ⟪ <-trans x₁ x₂ , ⟪ rr05 , <-tr> x₆ x₁ ⟫ ⟫ rr02 rr03 where rr00 : (key₄ < key₂) ∧ tr< key₂ t₄ ∧ tr< key₂ t₅ rr00 = RB-repl→ti< _ _ _ _ _ trb lt ⟪ x₇ , ⟪ x₉ , x₁₀ ⟫ ⟫ @@ -1183,51 +1202,51 @@ rr03 = RTtoTI0 _ _ _ _(t-node _ _ _ {_} {value₁} {_} {_} {_} {_} {_} (proj1 x₄) x₂ (proj1 (proj2 x₄)) (proj2 (proj2 x₄)) x₅ x₆ ti₂ ti₁) r-node rr05 : tr> key₂ t₂ rr05 = <-tr> x₅ x₁ -RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ leaf (node key₂ ⟪ Red , v2 ⟫ leaf leaf)) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₃ value₁ t₃ t₄)) key value - (t-right .key₁ .key₂ x₁ x₂ x₃ (t-single .key₂ .(⟪ Red , _ ⟫))) (rbr-rotate-rr x lt trb) +RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ leaf (node key₂ ⟪ Red , v2 ⟫ leaf leaf)) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₃ value₁ t₃ t₄)) key value + (t-right .key₁ .key₂ x₁ x₂ x₃ (t-single .key₂ .(⟪ Red , _ ⟫))) (rbr-rotate-rr x lt trb) = t-node _ _ _ x₁ (proj1 rr00) tt tt (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (t-single _ _) (RB-repl→ti _ _ _ _ t-leaf trb) where rr00 : (key₂ < key₃) ∧ tr> key₂ t₃ ∧ tr> key₂ t₄ rr00 = RB-repl→ti> _ _ _ _ _ trb lt tt -RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ leaf (node key₂ ⟪ Red , v2 ⟫ leaf (node key₃ value₃ t t₁))) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₄ value₁ t₃ t₄)) key value - (t-right .key₁ .key₂ x₁ x₂ x₃ (t-right .key₂ key₃ x₄ x₅ x₆ ti)) (rbr-rotate-rr x lt trb) +RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ leaf (node key₂ ⟪ Red , v2 ⟫ leaf (node key₃ value₃ t t₁))) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₄ value₁ t₃ t₄)) key value + (t-right .key₁ .key₂ x₁ x₂ x₃ (t-right .key₂ key₃ x₄ x₅ x₆ ti)) (rbr-rotate-rr x lt trb) = t-node _ _ _ x₁ (proj1 rr00) tt tt (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (t-single _ _ ) (RB-repl→ti _ _ _ _ ti trb) where rr00 : (key₂ < key₄) ∧ tr> key₂ t₃ ∧ tr> key₂ t₄ - rr00 = RB-repl→ti> _ _ _ _ _ trb lt ⟪ x₄ , ⟪ x₅ , x₆ ⟫ ⟫ -RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ leaf (node key₂ ⟪ Red , v2 ⟫ (node key₃ _ _ _) leaf)) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₄ value₁ t₃ t₄)) key value - (t-right .key₁ .key₂ x₁ x₂ x₃ (t-left key₃ .key₂ x₄ x₅ x₆ ti)) (rbr-rotate-rr x lt trb) + rr00 = RB-repl→ti> _ _ _ _ _ trb lt ⟪ x₄ , ⟪ x₅ , x₆ ⟫ ⟫ +RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ leaf (node key₂ ⟪ Red , v2 ⟫ (node key₃ _ _ _) leaf)) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₄ value₁ t₃ t₄)) key value + (t-right .key₁ .key₂ x₁ x₂ x₃ (t-left key₃ .key₂ x₄ x₅ x₆ ti)) (rbr-rotate-rr x lt trb) = t-node _ _ _ x₁ (proj1 rr00) tt ⟪ x₄ , ⟪ x₅ , x₆ ⟫ ⟫ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (t-right _ _ (proj1 x₂) (proj1 (proj2 x₂)) (proj2 (proj2 x₂)) ti) (RB-repl→ti _ _ _ _ t-leaf trb) where rr00 : (key₂ < key₄) ∧ tr> key₂ t₃ ∧ tr> key₂ t₄ rr00 = RB-repl→ti> _ _ _ _ _ trb lt tt -RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ leaf (node key₂ ⟪ Red , v2 ⟫ (node key₃ _ _ _) (node key₄ _ _ _))) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₅ value₁ t₃ t₄)) key value +RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ leaf (node key₂ ⟪ Red , v2 ⟫ (node key₃ _ _ _) (node key₄ _ _ _))) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₅ value₁ t₃ t₄)) key value (t-right .key₁ .key₂ x₁ x₂ x₃ (t-node key₃ .key₂ key₄ x₄ x₅ x₆ x₇ x₈ x₉ ti ti₁)) (rbr-rotate-rr x lt trb) = t-node _ _ _ x₁ (proj1 rr00) tt ⟪ x₄ , ⟪ x₆ , x₇ ⟫ ⟫ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (t-right _ _ (proj1 x₂) (proj1 (proj2 x₂)) (proj2 (proj2 x₂)) ti) (RB-repl→ti _ _ _ _ ti₁ trb) where rr00 : (key₂ < key₅) ∧ tr> key₂ t₃ ∧ tr> key₂ t₄ rr00 = RB-repl→ti> _ _ _ _ _ trb lt ⟪ x₅ , ⟪ x₈ , x₉ ⟫ ⟫ -RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ .(node key₃ _ _ _) (node key₂ ⟪ Red , v2 ⟫ .leaf .leaf)) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₄ value₁ t₃ t₄)) key value - (t-node key₃ .key₁ .key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti (t-single .key₂ .(⟪ Red , v2 ⟫))) (rbr-rotate-rr x lt trb) +RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ .(node key₃ _ _ _) (node key₂ ⟪ Red , v2 ⟫ .leaf .leaf)) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₄ value₁ t₃ t₄)) key value + (t-node key₃ .key₁ .key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti (t-single .key₂ .(⟪ Red , v2 ⟫))) (rbr-rotate-rr x lt trb) = t-node _ _ _ x₂ (proj1 rr00) ⟪ <-trans x₁ x₂ , ⟪ >-tr< x₃ x₂ , >-tr< x₄ x₂ ⟫ ⟫ tt (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (t-left _ _ x₁ x₃ x₄ ti) (RB-repl→ti _ _ _ _ t-leaf trb) where rr00 : (key₂ < key₄) ∧ tr> key₂ t₃ ∧ tr> key₂ t₄ rr00 = RB-repl→ti> _ _ _ _ _ trb lt tt -RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₃ v3 t t₁) (node key₂ ⟪ Red , v2 ⟫ leaf (node key₄ _ _ _))) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₅ value₁ t₃ t₄)) key value - (t-node key₃ .key₁ .key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti (t-right .key₂ key₄ x₇ x₈ x₉ ti₁)) (rbr-rotate-rr x lt trb) +RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₃ v3 t t₁) (node key₂ ⟪ Red , v2 ⟫ leaf (node key₄ _ _ _))) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₅ value₁ t₃ t₄)) key value + (t-node key₃ .key₁ .key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti (t-right .key₂ key₄ x₇ x₈ x₉ ti₁)) (rbr-rotate-rr x lt trb) = t-node _ _ _ x₂ (proj1 rr00) ⟪ <-trans x₁ x₂ , ⟪ >-tr< x₃ x₂ , >-tr< x₄ x₂ ⟫ ⟫ tt (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (t-left _ _ x₁ x₃ x₄ ti) (RB-repl→ti _ _ _ _ ti₁ trb) where rr00 : (key₂ < key₅) ∧ tr> key₂ t₃ ∧ tr> key₂ t₄ rr00 = RB-repl→ti> _ _ _ _ _ trb lt ⟪ x₇ , ⟪ x₈ , x₉ ⟫ ⟫ -RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₃ _ _ _) (node key₂ ⟪ Red , v2 ⟫ (node key₄ _ _ _) leaf)) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₅ value₁ t₃ t₄)) key value - (t-node key₃ key₁ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti (t-left key₄ key₂ x₇ x₈ x₉ ti₁)) (rbr-rotate-rr x lt trb) +RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₃ _ _ _) (node key₂ ⟪ Red , v2 ⟫ (node key₄ _ _ _) leaf)) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₅ value₁ t₃ t₄)) key value + (t-node key₃ key₁ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti (t-left key₄ key₂ x₇ x₈ x₉ ti₁)) (rbr-rotate-rr x lt trb) = t-node _ _ _ x₂ (proj1 rr00) ⟪ <-trans x₁ x₂ , ⟪ >-tr< x₃ x₂ , >-tr< x₄ x₂ ⟫ ⟫ ⟪ x₇ , ⟪ x₈ , x₉ ⟫ ⟫ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (t-node _ _ _ x₁ (proj1 x₅) x₃ x₄ (proj1 (proj2 x₅)) (proj2 (proj2 x₅)) ti ti₁) (RB-repl→ti _ _ _ _ t-leaf trb) where rr00 : (key₂ < key₅) ∧ tr> key₂ t₃ ∧ tr> key₂ t₄ rr00 = RB-repl→ti> _ _ _ _ _ trb lt tt -RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₃ _ _ _) (node key₂ ⟪ Red , v2 ⟫ (node key₄ _ left right) (node key₅ _ _ _))) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₆ value₁ t₃ t₄)) key value - (t-node key₃ key₁ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti (t-node key₄ key₂ key₅ x₇ x₈ x₉ x₁₀ x₁₁ x₁₂ ti₁ ti₂)) (rbr-rotate-rr x lt trb) +RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₃ _ _ _) (node key₂ ⟪ Red , v2 ⟫ (node key₄ _ left right) (node key₅ _ _ _))) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₆ value₁ t₃ t₄)) key value + (t-node key₃ key₁ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti (t-node key₄ key₂ key₅ x₇ x₈ x₉ x₁₀ x₁₁ x₁₂ ti₁ ti₂)) (rbr-rotate-rr x lt trb) = t-node _ _ _ x₂ (proj1 rr00) ⟪ <-trans x₁ x₂ , ⟪ >-tr< x₃ x₂ , >-tr< x₄ x₂ ⟫ ⟫ ⟪ x₇ , ⟪ x₉ , x₁₀ ⟫ ⟫ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RTtoTI0 _ _ _ _ (t-node _ _ _ {_} {value₁} x₁ (proj1 x₅) x₃ x₄ (proj1 (proj2 x₅)) (proj2 (proj2 x₅)) ti ti₁ ) r-node ) (RB-repl→ti _ _ _ _ ti₂ trb) where rr00 : (key₂ < key₆) ∧ tr> key₂ t₃ ∧ tr> key₂ t₄ rr00 = RB-repl→ti> _ _ _ _ _ trb lt ⟪ x₈ , ⟪ x₁₁ , x₁₂ ⟫ ⟫ 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₁ 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) = +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₁ 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₅ ) rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₃ , ⟪ x₄ , x₅ ⟫ ⟫ @@ -1237,8 +1256,8 @@ rr03 : (kn < key₂) ∧ tr> kn t₄ ∧ tr> kn t₅ rr03 with RB-repl→ti _ _ _ _ ti trb ... | t-right .kn .key₂ x x₁ x₂ t = ⟪ x , ⟪ x₁ , x₂ ⟫ ⟫ -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 , _ ⟫ _ (node key₂ value₂ t₃ t₅)) (node kg ⟪ Red , _ ⟫ leaf _)) key value (t-left .kp .kg x x₁ x₂ (t-right .kp .key₁ x₃ x₄ x₅ ti)) (rbr-rotate-lr .(node key₂ value₂ t₃ t₅) .leaf kg kp kn _ lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti trb -... | t-left .key₂ .kn x₆ x₇ x₈ t = +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 , _ ⟫ _ (node key₂ value₂ t₃ t₅)) (node kg ⟪ Red , _ ⟫ leaf _)) key value (t-left .kp .kg x x₁ x₂ (t-right .kp .key₁ x₃ x₄ x₅ ti)) (rbr-rotate-lr .(node key₂ value₂ t₃ t₅) .leaf kg kp kn _ lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti trb +... | t-left .key₂ .kn x₆ x₇ x₈ t = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫ tt tt (t-right _ _ (proj1 rr02) (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) t) (t-single _ _) where rr00 : (kp < kn) ∧ ((kp < key₂) ∧ tr> kp t₃ ∧ tr> kp t₅) ∧ ⊤ rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₃ , ⟪ x₄ , x₅ ⟫ ⟫ @@ -1338,8 +1357,8 @@ 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 ⟫ .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 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) ∧ ⊤ ∧ ⊤ rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₁ @@ -1389,7 +1408,7 @@ rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₆ , ⟪ x₈ , x₉ ⟫ ⟫ RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₂ _ _ _) .leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf t₂) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-right .kg .kp x x₁ x₂ (t-left key₂ .kp x₃ x₄ x₅ ti)) (rbr-rotate-rl t₂ .(node key₁ value₁ t₃ t₄) kg kp kn _ lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti trb ... | t-right .kn .key₁ x₆ x₇ x₈ t = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt tt ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫ tt (t-single _ _) (t-left _ _ (proj1 rr03) (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) t) where - rr00 : (kg < kn) ∧ ⊤ ∧ ((kg < key₁) ∧ tr> kg t₃ ∧ tr> kg t₄) + rr00 : (kg < kn) ∧ ⊤ ∧ ((kg < key₁) ∧ tr> kg t₃ ∧ tr> kg t₄) rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₁ rr02 = proj2 (proj2 rr00) rr01 : (kn < kp) ∧ ⊤ ∧ ((key₁ < kp) ∧ tr< kp t₃ ∧ tr< kp t₄) @@ -1661,13 +1680,13 @@ ... | 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 repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ + black-depth (RBI.tree r) ≡⟨ cong black-depth (sym (rb04 si eq refl)) ⟩ black-depth left ≡⟨ (RBtreeEQ (RBI.origrb r)) ⟩ - black-depth right ∎ + 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 ∷ [] + 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 → key ≡ key₁ → ⊥ @@ -1678,7 +1697,7 @@ 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 ... | refl = ⊥-elim ( nat-<> x c ) - -- + -- -- RBI key value (node key₁ ⟪ Black , value₄ ⟫ left right) repl stack -- insertCase13 : (v : Color ∧ A ) → v ≡ value₁ → black-depth repl ≡ black-depth (child-replaced key (RBI.tree r)) → t @@ -1722,3 +1741,4 @@ +