Mercurial > hg > Gears > GearsAgda
changeset 890:6a5fe1c4855a
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 18 May 2024 16:03:40 +0900 |
| parents | e753aea361ea |
| children | e8e8ccfd6c44 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 545 insertions(+), 584 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Wed May 15 14:13:41 2024 +0900 +++ b/hoareBinaryTree1.agda Sat May 18 16:03:40 2024 +0900 @@ -662,37 +662,17 @@ suc≢zero : {m : ℕ } → suc m ≡ zero → ⊥ suc≢zero () - data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where rb-leaf : RBtreeInvariant leaf - rb-single : {c : Color} → (key : ℕ) → (value : A) → RBtreeInvariant (node key ⟪ c , value ⟫ leaf leaf) - rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ - → black-depth t ≡ black-depth t₁ - → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) - → RBtreeInvariant (node key ⟪ Red , value ⟫ leaf (node key₁ ⟪ Black , value₁ ⟫ t t₁)) - rb-right-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {c : Color} - → black-depth t ≡ black-depth t₁ - → RBtreeInvariant (node key₁ ⟪ c , value₁ ⟫ t t₁) - → RBtreeInvariant (node key ⟪ Black , value ⟫ leaf (node key₁ ⟪ c , value₁ ⟫ t t₁)) - rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key₁ < key - → black-depth t ≡ black-depth t₁ - → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) - → RBtreeInvariant (node key ⟪ Red , value ⟫ (node key₁ ⟪ Black , value₁ ⟫ t t₁) leaf ) - rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → {c : Color} → key₁ < key - → black-depth t ≡ black-depth t₁ - → RBtreeInvariant (node key₁ ⟪ c , value₁ ⟫ t t₁) - → RBtreeInvariant (node key ⟪ Black , value ⟫ (node key₁ ⟪ c , value₁ ⟫ t t₁) leaf) - rb-node-red : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ - → black-depth (node key ⟪ Black , value ⟫ t₁ t₂) ≡ black-depth (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄) - → RBtreeInvariant (node key ⟪ Black , value ⟫ t₁ t₂) - → RBtreeInvariant (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄) - → RBtreeInvariant (node key₁ ⟪ Red , value₁ ⟫ (node key ⟪ Black , value ⟫ t₁ t₂) (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄)) - rb-node-black : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ - → {c c₁ : Color} - → black-depth (node key ⟪ c , value ⟫ t₁ t₂) ≡ black-depth (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄) - → RBtreeInvariant (node key ⟪ c , value ⟫ t₁ t₂) - → RBtreeInvariant (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄) - → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ (node key ⟪ c , value ⟫ t₁ t₂) (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄)) + 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)} + → black-depth left ≡ black-depth right + → RBtreeInvariant left → RBtreeInvariant right + → RBtreeInvariant (node key ⟪ Black , value ⟫ left right) RightDown : {n : Level} {A : Set n} → bt (Color ∧ A) → bt (Color ∧ A) RightDown leaf = leaf @@ -702,38 +682,19 @@ LeftDown (node key ⟪ c , value ⟫ t1 t2 ) = t1 RBtreeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color} - → (tleft tright : bt (Color ∧ A)) - → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright) - → RBtreeInvariant tleft -RBtreeLeftDown leaf leaf (rb-single k1 v) = rb-leaf -RBtreeLeftDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-red x bde rbti) = rb-leaf -RBtreeLeftDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-black x bde rbti) = rb-leaf -RBtreeLeftDown leaf (node key ⟪ Red , value ⟫ t1 t2 ) (rb-right-black x bde rbti)= rb-leaf -RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-black x bde ti) = ti -RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-red x bde ti)= ti -RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) leaf (rb-left-black x bde ti) = ti -RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til tir) = til -RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til tir) = til -RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til tir) = til -RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til tir) = til -RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til tir) = til + → (left right : bt (Color ∧ A)) + → RBtreeInvariant (node key ⟪ c , value ⟫ left right) + → RBtreeInvariant left +RBtreeLeftDown left right (rb-red _ _ x x₁ x₂ rb rb₁) = rb +RBtreeLeftDown left right (rb-black _ _ x rb rb₁) = rb + RBtreeRightDown : {n : Level} {A : Set n} { key : ℕ} {value : A} {c : Color} - → (tleft tright : bt (Color ∧ A)) - → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright) - → RBtreeInvariant tright -RBtreeRightDown leaf leaf (rb-single k1 v1 ) = rb-leaf -RBtreeRightDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-red x bde rbti) = rbti -RBtreeRightDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-black x bde rbti) = rbti -RBtreeRightDown leaf (node key ⟪ Red , value ⟫ t1 t2 ) (rb-right-black x bde rbti)= rbti -RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-black x bde ti) = rb-leaf -RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-red x bde ti) = rb-leaf -RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) leaf (rb-left-black x bde ti) = rb-leaf -RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til tir) = tir -RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til tir) = tir -RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til tir) = tir -RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til tir) = tir -RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til tir) = tir + → (left right : bt (Color ∧ A)) + → RBtreeInvariant (node key ⟪ c , value ⟫ left right) + → RBtreeInvariant right +RBtreeRightDown left right (rb-red _ _ x x₁ x₂ rb rb₁) = rb₁ +RBtreeRightDown left right (rb-black _ _ x rb rb₁) = rb₁ -- -- findRBT exit with replaced node @@ -779,19 +740,12 @@ testRBTree0 : bt (Color ∧ ℕ) testRBTree0 = node 8 ⟪ Black , 800 ⟫ (node 5 ⟪ Red , 500 ⟫ (node 2 ⟪ Black , 200 ⟫ leaf leaf) (node 6 ⟪ Black , 600 ⟫ leaf leaf)) (node 10 ⟪ Red , 1000 ⟫ (leaf) (node 15 ⟪ Black , 1500 ⟫ (node 14 ⟪ Red , 1400 ⟫ leaf leaf) leaf)) -record result {n : Level} {A : Set n} {key : ℕ} {tree0 : bt (Color ∧ A)} : Set n where - field - tree : bt (Color ∧ A) - stack : List (bt (Color ∧ A)) - ti : RBtreeInvariant tree - si : stackInvariant key tree tree0 stack +-- testRBI0 : RBtreeInvariant testRBTree0 +-- testRBI0 = rb-node-black (add< 2) (add< 1) refl (rb-node-red (add< 2) (add< 0) refl (rb-single 2 200) (rb-single 6 600)) (rb-right-red (add< 4) refl (rb-left-black (add< 0) refl (rb-single 14 1400) )) -testRBI0 : RBtreeInvariant testRBTree0 -testRBI0 = rb-node-black (add< 2) (add< 1) refl (rb-node-red (add< 2) (add< 0) refl (rb-single 2 200) (rb-single 6 600)) (rb-right-red (add< 4) refl (rb-left-black (add< 0) refl (rb-single 14 1400) )) - -findRBTreeTest : result -findRBTreeTest = findTest 14 testRBTree0 testRBI0 - $ λ tr s P O → (record {tree = tr ; stack = s ; ti = (proj1 P) ; si = (proj2 P)}) +-- findRBTreeTest : result +-- findRBTreeTest = findTest 14 testRBTree0 testRBI0 +-- $ λ tr s P O → (record {tree = tr ; stack = s ; ti = (proj1 P) ; si = (proj2 P)}) -- create replaceRBTree with rotate @@ -799,10 +753,13 @@ -- 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-right : {k : ℕ } {v1 : A} → {ca : Color} → {t t1 t2 : bt (Color ∧ A)} + 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 → 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 rbr-black-right : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} → color t₂ ≡ Red → key₁ < key → replacedRBTree key value t₁ t₂ @@ -840,12 +797,12 @@ (node kp ⟪ Black , vp ⟫ (node kg ⟪ Red , vg ⟫ uncle t) t₂ ) -- case56 the node is inner, make it outer and rotate grand rbr-rotate-lr : {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} - → kp < key → key < kg + → color t₃ ≡ Red → kp < key → key < kg → replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃) → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁) uncle) (node kn ⟪ Black , vn ⟫ (node kp ⟪ Red , vp ⟫ t t₂) (node kg ⟪ Red , vg ⟫ t₃ uncle)) rbr-rotate-rl : {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} - → kg < key → key < kp + → color t₃ ≡ Red → kg < key → key < kp → replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃) → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t₁ t)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , vg ⟫ uncle t₂) (node kp ⟪ Red , vp ⟫ t₃ t)) @@ -878,11 +835,16 @@ -- color repl ≡ Red ∧ black-depth repl ≡ suc (black-depth tree) -- -data RBI-state {n : Level} {A : Set n} (key : ℕ) : (tree repl : bt (Color ∧ A) ) → Set n where - rebuild : {tree repl : bt (Color ∧ A) } → black-depth repl ≡ black-depth (child-replaced key tree) - → RBI-state key tree repl -- one stage up - rotate : {tree repl : bt (Color ∧ A) } → color repl ≡ Red → black-depth repl ≡ black-depth (child-replaced key tree) - → RBI-state key tree repl -- two stages up +data RBI-state {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree repl : bt (Color ∧ A) ) → (stak : List (bt (Color ∧ A))) → Set n where + rebuild : {tree repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → black-depth repl ≡ black-depth (child-replaced key tree) + → (rotated : replacedRBTree key value tree repl) + → RBI-state key value tree repl stack -- one stage up + 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 ∷ [] + → (rotated : replacedRBTree key value (to-black tree) repl) + → 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 @@ -892,8 +854,7 @@ treerb : RBtreeInvariant tree -- tree node te be replaced replrb : RBtreeInvariant repl si : stackInvariant key tree orig stack - rotated : replacedRBTree key value tree repl - state : RBI-state key tree repl + state : RBI-state key value tree repl stack tr>-to-black : {n : Level} {A : Set n} {key : ℕ} {tree : bt (Color ∧ A)} → tr> key tree → tr> key (to-black tree) tr>-to-black {n} {A} {key} {leaf} tr = tt @@ -907,9 +868,9 @@ → 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 _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-right x rbt) lt 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 +RB-repl→ti> .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-left _ x rbt) lt tr = ⟪ proj1 tr , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt (proj1 (proj2 tr)) , proj2 (proj2 tr) ⟫ ⟫ RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-right x _ rbt) lt tr = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti> _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫ @@ -929,13 +890,13 @@ RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) key key₁ value (rbr-rotate-rr x lt2 rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr4 , ⟪ ⟪ tr3 , ⟪ tr5 , tr6 ⟫ ⟫ , RB-repl→ti> _ _ _ _ _ rbt lt tr7 ⟫ ⟫ 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 + (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 rr00 : key₁ < kn 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 + (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 : (key₁ < kn) ∧ tr> key₁ left ∧ tr> key₁ right rr01 = RB-repl→ti> _ _ _ _ _ rbt lt tr6 rr00 : key₁ < kn @@ -945,9 +906,9 @@ → 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 _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-right x rbt) lt 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 +RB-repl→ti< .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-left _ x rbt) lt tr = ⟪ proj1 tr , ⟪ RB-repl→ti< _ _ _ _ _ rbt lt (proj1 (proj2 tr)) , proj2 (proj2 tr) ⟫ ⟫ RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-right x _ rbt) lt tr = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti< _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫ @@ -967,13 +928,13 @@ RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) key key₁ value (rbr-rotate-rr x lt2 rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr4 , ⟪ ⟪ tr3 , ⟪ tr5 , tr6 ⟫ ⟫ , RB-repl→ti< _ _ _ _ _ rbt lt tr7 ⟫ ⟫ 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 + (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₁ 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 + (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₁ @@ -981,462 +942,461 @@ 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 = ? --- 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 --- (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 --- (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 = 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 --- (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₁ --- (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 --- (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 --- (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 --- (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 --- (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 --- (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 = 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 --- (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 --- (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 --- (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 --- (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 --- (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 --- (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 --- (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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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₃ --- (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 --- (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 --- rr04 : treeInvariant (node k1 ⟪ Red , c1 ⟫ (node key₂ value₂ t₁ t₄) leaf) --- 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 --- (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 --- (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) --- 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 --- (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 = 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 --- (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 --- rr02 : treeInvariant (node key₄ value₁ t₄ t₅) --- 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₆ --- (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₉ ⟫ ⟫ --- rr02 : treeInvariant (node key₄ value₁ t₄ t₅) --- rr02 = RB-repl→ti _ _ _ _ ti trb --- rr03 : treeInvariant (node key₁ ⟪ Red , c1 ⟫ (node key₅ _ _ _) (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 --- 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 --- (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₁₀ ⟫ ⟫ --- rr02 : treeInvariant (node key₄ value₁ t₄ t₅) --- rr02 = RB-repl→ti _ _ _ _ ti trb --- rr03 : treeInvariant (node key₁ ⟪ Red , c1 ⟫ (node key₆ value₆ t₆ t₇) (node key₃ v3 t₂ t₃)) --- 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) --- = 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) --- = 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) --- = 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 --- (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) --- = 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) --- = 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) --- = 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) --- = 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) = --- 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₅ ⟫ ⟫ --- rr01 : (kn < kg) ∧ ⊤ ∧ ((key₂ < kg ) ∧ tr< kg t₄ ∧ tr< kg t₅ ) -- tr< kg (node key₂ value₂ t₄ t₅) --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₂ --- rr02 = proj2 (proj2 rr01) --- 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 = --- 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₅ ⟫ ⟫ --- rr02 = proj1 (proj2 rr00) --- rr01 : (kn < kg) ∧ ((key₂ < kg) ∧ tr< kg t₃ ∧ tr< kg t₅) ∧ ⊤ --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 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 , _ ⟫ (node key₃ value₃ t₄ t₆) _)) 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₅) .(node key₃ value₃ t₄ t₆) kg kp kn lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti trb --- ... | t-node .key₂ .kn .key₃ x₆ x₇ x₈ x₉ x₁₀ x₁₁ t t₇ = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt ⟪ x₆ , ⟪ x₈ , x₉ ⟫ ⟫ ⟪ x₇ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ tt (t-right _ _ (proj1 rr02) (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) t) (t-left _ _ (proj1 rr03) (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) t₇) where --- rr00 : (kp < kn) ∧ ((kp < key₂) ∧ tr> kp t₃ ∧ tr> kp t₅) ∧ ((kp < key₃) ∧ tr> kp t₄ ∧ tr> kp t₆ ) --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₃ , ⟪ x₄ , x₅ ⟫ ⟫ --- rr02 = proj1 (proj2 rr00) --- rr01 : (kn < kg) ∧ ((key₂ < kg) ∧ tr< kg t₃ ∧ tr< kg t₅) ∧ ((key₃ < kg) ∧ tr< kg t₄ ∧ tr< kg t₆ ) --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₂ --- rr03 = proj2 (proj2 rr01) --- RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ (node key₂ value₂ t₅ t₆) (node key₁ value₁ t₁ t₂)) leaf) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₃) (node kg ⟪ Red , _ ⟫ t₄ _)) key value (t-left .kp .kg x x₁ x₂ (t-node key₂ .kp .key₁ x₃ x₄ x₅ x₆ x₇ x₈ ti ti₁)) (rbr-rotate-lr t₃ t₄ kg kp kn lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti₁ trb --- ... | t-single .kn .(⟪ Red , _ ⟫) = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x₃ (proj1 rr00) , ⟪ >-tr< x₅ (proj1 rr00) , >-tr< x₆ (proj1 rr00) ⟫ ⟫ tt tt tt (t-left _ _ x₃ x₅ x₆ ti) (t-single _ _) where --- rr00 : (kp < kn) ∧ ⊤ ∧ ⊤ --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₄ , ⟪ x₇ , x₈ ⟫ ⟫ --- rr01 : (kn < kg) ∧ ⊤ ∧ ⊤ --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₂ --- ... | t-right .kn key₃ {v1} {v3} {t₇} {t₈} x₉ x₁₀ x₁₁ t = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x₃ (proj1 rr00) , ⟪ >-tr< x₅ (proj1 rr00) , >-tr< x₆ (proj1 rr00) ⟫ ⟫ tt ⟪ x₉ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ tt (t-left _ _ x₃ x₅ x₆ ti) (t-left _ _ (proj1 rr03) (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) (treeRightDown _ _ (RB-repl→ti _ _ _ _ ti₁ trb))) where --- rr00 : (kp < kn) ∧ ⊤ ∧ ((kp < key₃) ∧ tr> kp t₇ ∧ tr> kp t₈) -- tr> kp (node key₃ v3 t₇ t₈) --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₄ , ⟪ x₇ , x₈ ⟫ ⟫ --- rr02 = proj1 (proj2 rr00) --- rr01 : (kn < kg) ∧ ⊤ ∧ ((key₃ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) -- tr< kg (node key₃ v3 t₇ t₈) --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₂ --- rr03 = proj2 (proj2 rr01) --- ... | t-left key₃ .kn {v1} {v3} {t₇} {t₈} x₉ x₁₀ x₁₁ t = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x₃ (proj1 rr00) , ⟪ >-tr< x₅ (proj1 rr00) , >-tr< x₆ (proj1 rr00) ⟫ ⟫ ⟪ x₉ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ tt tt (t-node key₂ kp key₃ x₃ (proj1 rr02) x₅ x₆ (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) ti (treeLeftDown _ _ (RB-repl→ti _ _ _ _ ti₁ trb))) (t-single _ _) where --- rr00 : (kp < kn) ∧ ((kp < key₃) ∧ tr> kp t₇ ∧ tr> kp t₈) ∧ ⊤ --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₄ , ⟪ x₇ , x₈ ⟫ ⟫ --- rr02 = proj1 (proj2 rr00) --- rr01 : (kn < kg) ∧ ((key₃ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) ∧ ⊤ --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₂ --- ... | t-node key₃ .kn key₄ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀} x₉ x₁₀ x₁₁ x₁₂ x₁₃ x₁₄ t t₃ = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x₃ (proj1 rr00) , ⟪ >-tr< x₅ (proj1 rr00) , >-tr< x₆ (proj1 rr00) ⟫ ⟫ ⟪ x₉ , ⟪ x₁₁ , x₁₂ ⟫ ⟫ ⟪ x₁₀ , ⟪ x₁₃ , x₁₄ ⟫ ⟫ tt (t-node _ _ _ x₃ (proj1 rr02) x₅ x₆ (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) ti (treeLeftDown _ _ (RB-repl→ti _ _ _ _ ti₁ trb))) (t-left _ _ (proj1 rr03) (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) t₃) where --- rr00 : (kp < kn) ∧ ((kp < key₃) ∧ tr> kp t₇ ∧ tr> kp t₈) ∧ ((kp < key₄) ∧ tr> kp t₉ ∧ tr> kp t₁₀) --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₄ , ⟪ x₇ , x₈ ⟫ ⟫ --- rr02 = proj1 (proj2 rr00) --- rr01 : (kn < kg) ∧ ((key₃ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) ∧ ((key₄ < kg) ∧ tr< kg t₉ ∧ tr< kg t₁₀) --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₂ --- rr03 = proj2 (proj2 rr01) --- RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .leaf leaf) (node key₂ value₂ t₅ t₆)) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ .leaf) (node kg ⟪ Red , _ ⟫ .leaf _)) .kn _ (t-node .kp .kg key₂ x x₁ x₂ x₃ x₄ x₅ (t-single .kp .(⟪ Red , v2 ⟫)) ti₁) (rbr-rotate-lr .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 , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .(node key _ _ _) leaf) (node key₂ value₂ t₅ t₆)) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ .leaf) (node kg ⟪ Red , _ ⟫ .leaf _)) .kn _ (t-node .kp .kg key₂ x x₁ x₂ x₃ x₄ x₅ (t-left key .kp x₆ x₇ x₈ ti) 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 ⟪ <-trans lt2 x₁ , ⟪ <-tr> x₄ lt2 , <-tr> x₅ lt2 ⟫ ⟫ (t-left _ _ x₆ x₇ x₈ ti) (t-right _ _ x₁ x₄ x₅ ti₁) --- RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .leaf (node key₁ value₁ t₁ t₂)) .(node key₂ _ _ _)) (node kn ⟪ Black , value₃ ⟫ (node kp ⟪ Red , _ ⟫ _ t₃) (node kg ⟪ Red , _ ⟫ t₄ _)) key value (t-node .kp .kg key₂ x x₁ x₂ x₃ x₄ x₅ (t-right .kp .key₁ x₆ x₇ x₈ ti) ti₁) (rbr-rotate-lr t₃ t₄ kg kp kn lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti trb --- ... | t-single .kn .(⟪ Red , value₃ ⟫) = 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 : (kp < kn) ∧ ⊤ ∧ ⊤ --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫ --- rr01 : (kn < kg) ∧ ⊤ ∧ ⊤ --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃ --- ... | t-right .kn key₃ {v1} {v3} {t₇} {t₈} x₉ x₁₀ x₁₁ t = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt tt ⟪ x₉ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ ⟪ <-trans (proj1 rr01) x₁ , ⟪ <-tr> x₄ (proj1 rr01) , <-tr> x₅ (proj1 rr01) ⟫ ⟫ (t-single _ _) (t-node _ _ _ (proj1 rr03) x₁ (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) x₄ x₅ (treeRightDown _ _ (RB-repl→ti _ _ _ _ ti trb)) ti₁) where --- rr00 : (kp < kn) ∧ ⊤ ∧ ((kp < key₃) ∧ tr> kp t₇ ∧ tr> kp t₈) --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫ --- rr02 = proj1 (proj2 rr00) --- rr01 : (kn < kg) ∧ ⊤ ∧ ((key₃ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃ --- rr03 = proj2 (proj2 rr01) --- ... | t-left key₃ .kn {v1} {v3} {t₇} {t₈} x₉ x₁₀ x₁₁ t = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt ⟪ x₉ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ tt ⟪ <-trans (proj1 rr01) x₁ , ⟪ <-tr> x₄ (proj1 rr01) , <-tr> x₅ (proj1 rr01) ⟫ ⟫ (t-right _ _ (proj1 rr02) (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) (treeLeftDown _ _ (RB-repl→ti _ _ _ _ ti trb))) (t-right _ _ x₁ x₄ x₅ ti₁) where --- rr00 : (kp < kn) ∧ ((kp < key₃) ∧ tr> kp t₇ ∧ tr> kp t₈) ∧ ⊤ --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫ --- rr02 = proj1 (proj2 rr00) --- rr01 : (kn < kg) ∧ ((key₃ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) ∧ ⊤ --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃ --- rr03 = proj1 (proj2 rr01) --- ... | t-node key₃ .kn key₄ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀} x₉ x₁₀ x₁₁ x₁₂ x₁₃ x₁₄ t t₃ = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt ⟪ x₉ , ⟪ x₁₁ , x₁₂ ⟫ ⟫ ⟪ x₁₀ , ⟪ x₁₃ , x₁₄ ⟫ ⟫ ⟪ <-trans (proj1 rr01) x₁ , ⟪ <-tr> x₄ (proj1 rr01) , <-tr> x₅ (proj1 rr01) ⟫ ⟫ (t-right _ _ (proj1 rr02) (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) (treeLeftDown _ _ (RB-repl→ti _ _ _ _ ti trb))) (t-node _ _ _ (proj1 rr03) x₁ (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) x₄ x₅ t₃ ti₁) where --- rr00 : (kp < kn) ∧ ((kp < key₃) ∧ tr> kp t₇ ∧ tr> kp t₈) ∧ ((kp < key₄) ∧ tr> kp t₉ ∧ tr> kp t₁₀) --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫ --- rr02 = proj1 (proj2 rr00) --- rr01 : (kn < kg) ∧ ((key₃ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) ∧ ((key₄ < kg) ∧ tr< kg t₉ ∧ tr< kg t₁₀) --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃ --- rr03 = proj2 (proj2 rr01) --- RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .(node key₃ _ _ _) (node key₁ value₁ t₁ t₂)) .(node key₂ _ _ _)) (node kn ⟪ Black , value₃ ⟫ (node kp ⟪ Red , _ ⟫ _ t₃) (node kg ⟪ Red , _ ⟫ t₄ _)) key value (t-node .kp .kg key₂ x x₁ x₂ x₃ x₄ x₅ (t-node key₃ .kp .key₁ x₆ x₇ x₈ x₉ x₁₀ x₁₁ ti ti₂) ti₁) (rbr-rotate-lr t₃ t₄ kg kp kn lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti₂ trb --- ... | t-single .kn .(⟪ Red , value₃ ⟫) = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x₆ (proj1 rr00) , ⟪ >-tr< x₈ (proj1 rr00) , >-tr< x₉ (proj1 rr00) ⟫ ⟫ tt tt ⟪ <-trans (proj1 rr01) x₁ , ⟪ <-tr> x₄ (proj1 rr01) , <-tr> x₅ (proj1 rr01) ⟫ ⟫ (t-left _ _ x₆ x₈ x₉ ti) (t-right _ _ x₁ x₄ x₅ ti₁) where --- rr00 : (kp < kn) ∧ ⊤ ∧ ⊤ --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₇ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ --- rr01 : (kn < kg) ∧ ⊤ ∧ ⊤ --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃ --- ... | t-right .kn key₄ {v1} {v3} {t₇} {t₈} x₁₂ x₁₃ x₁₄ t = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x₆ (proj1 rr00) , ⟪ >-tr< x₈ (proj1 rr00) , >-tr< x₉ (proj1 rr00) ⟫ ⟫ tt ⟪ x₁₂ , ⟪ x₁₃ , x₁₄ ⟫ ⟫ ⟪ <-trans (proj1 rr01) x₁ , ⟪ <-tr> x₄ (proj1 rr01) , <-tr> x₅ (proj1 rr01) ⟫ ⟫ (t-left _ _ x₆ x₈ x₉ ti) (t-node _ _ _ (proj1 rr03) x₁ (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) x₄ x₅ (treeRightDown _ _ (RB-repl→ti _ _ _ _ ti₂ trb)) ti₁ ) where --- rr00 : (kp < kn) ∧ ⊤ ∧ ((kp < key₄) ∧ tr> kp t₇ ∧ tr> kp t₈) --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₇ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ --- rr02 = proj2 (proj2 rr00) --- rr01 : (kn < kg) ∧ ⊤ ∧ ((key₄ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃ --- rr03 = proj2 (proj2 rr01) --- ... | t-left key₄ .kn {v1} {v3} {t₇} {t₈} x₁₂ x₁₃ x₁₄ t = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x₆ (proj1 rr00) , ⟪ >-tr< x₈ (proj1 rr00) , >-tr< x₉ (proj1 rr00) ⟫ ⟫ ⟪ x₁₂ , ⟪ x₁₃ , x₁₄ ⟫ ⟫ tt ⟪ <-trans (proj1 rr01) x₁ , ⟪ <-tr> x₄ (proj1 rr01) , <-tr> x₅ (proj1 rr01) ⟫ ⟫ (t-node _ _ _ x₆ (proj1 rr02) x₈ x₉ (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) ti (treeLeftDown _ _ (RB-repl→ti _ _ _ _ ti₂ trb)) ) (t-right _ _ x₁ x₄ x₅ ti₁) where --- rr00 : (kp < kn) ∧ ((kp < key₄) ∧ tr> kp t₇ ∧ tr> kp t₈) ∧ ⊤ --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₇ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ --- rr02 = proj1 (proj2 rr00) --- rr01 : (kn < kg) ∧ ((key₄ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) ∧ ⊤ --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃ --- rr03 = proj1 (proj2 rr01) --- ... | t-node key₄ .kn key₅ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀}x₁₂ x₁₃ x₁₄ x₁₅ x₁₆ x₁₇ t t₃ = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x₆ (proj1 rr00) , ⟪ >-tr< x₈ (proj1 rr00) , >-tr< x₉ (proj1 rr00) ⟫ ⟫ ⟪ x₁₂ , ⟪ x₁₄ , x₁₅ ⟫ ⟫ ⟪ x₁₃ , ⟪ x₁₆ , x₁₇ ⟫ ⟫ ⟪ <-trans (proj1 rr01) x₁ , ⟪ <-tr> x₄ (proj1 rr01) , <-tr> x₅ (proj1 rr01) ⟫ ⟫ (t-node _ _ _ x₆ (proj1 rr02) x₈ x₉ (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) ti t ) (t-node _ _ _ (proj1 rr04) x₁ (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) x₄ x₅ (treeRightDown _ _ (RB-repl→ti _ _ _ _ ti₂ trb)) ti₁ ) where --- rr00 : (kp < kn) ∧ ((kp < key₄) ∧ tr> kp t₇ ∧ tr> kp t₈) ∧ ((kp < key₅) ∧ tr> kp t₉ ∧ tr> kp t₁₀) --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₇ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ --- rr02 = proj1 (proj2 rr00) --- rr05 = proj2 (proj2 rr00) --- rr01 : (kn < kg) ∧ ((key₄ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) ∧ ((key₅ < kg) ∧ tr< kg t₉ ∧ tr< kg t₁₀) --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃ --- 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 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₁ --- rr01 : (kn < kp) ∧ ⊤ ∧ ⊤ --- 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 (node key₁ value₁ t₂ t₃)) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-right .kg .kp x x₁ x₂ (t-left key₂ .kp x₃ x₄ x₅ ti)) (rbr-rotate-rl .(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 : (kg < kn) ∧ ((kg < key₁) ∧ tr> kg t₂ ∧ tr> kg t₃) ∧ ⊤ --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₁ --- rr02 = proj1 (proj2 rr00) --- rr01 : (kn < kp) ∧ ((key₁ < kp) ∧ tr< kp t₂ ∧ tr< kp t₃) ∧ ⊤ --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₃ , ⟪ x₄ , x₅ ⟫ ⟫ --- RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₂ _ _ _) .(node key₃ _ _ _))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf (node key₁ value₁ t₂ t₃)) (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 .(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 ⟪ <-trans (proj1 rr01) x₄ , ⟪ <-tr> x₇ (proj1 rr01) , <-tr> x₈ (proj1 rr01) ⟫ ⟫ (t-right _ _ (proj1 rr02) (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) t) (t-right _ _ x₄ x₇ x₈ ti₁) where --- rr00 : (kg < kn) ∧ ((kg < key₁) ∧ tr> kg t₂ ∧ tr> kg t₃) ∧ ⊤ --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₁ --- rr02 = proj1 (proj2 rr00) --- rr01 : (kn < kp) ∧ ((key₁ < kp) ∧ tr< kp t₂ ∧ tr< kp t₃) ∧ ⊤ --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₃ , ⟪ x₅ , x₆ ⟫ ⟫ --- RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .leaf .leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) .leaf) (node kp ⟪ Red , _ ⟫ leaf _)) .kn .vn (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti (t-single .kp .(⟪ Red , vp ⟫))) (rbr-rotate-rl .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 , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .leaf .(node key₂ _ _ _))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) .leaf) (node kp ⟪ Red , _ ⟫ leaf _)) .kn .vn (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti (t-right .kp key₂ x₆ x₇ x₈ ti₁)) (rbr-rotate-rl .leaf .leaf kg kp kn lt1 lt2 rbr-leaf) = t-node _ _ _ lt1 lt2 ⟪ <-trans x lt1 , ⟪ >-tr< x₂ lt1 , >-tr< x₃ lt1 ⟫ ⟫ tt tt ⟪ <-trans lt2 x₆ , ⟪ <-tr> x₇ lt2 , <-tr> x₈ lt2 ⟫ ⟫ (t-left _ _ x x₂ x₃ ti) (t-right _ _ x₆ x₇ x₈ ti₁) --- RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₂ _ _ _) .leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) t₂) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti (t-left key₂ .kp x₆ x₇ x₈ ti₁)) (rbr-rotate-rl t₂ .leaf kg kp kn lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti₁ trb --- ... | t-single .kn .(⟪ Red , vn ⟫) = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x (proj1 rr00) , ⟪ >-tr< x₂ (proj1 rr00) , >-tr< x₃ (proj1 rr00) ⟫ ⟫ tt tt tt (t-left _ _ x x₂ x₃ ti) (t-single _ _) where --- rr00 : (kg < kn) ∧ ⊤ ∧ ⊤ --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₄ --- rr01 : (kn < kp) ∧ ⊤ ∧ ⊤ --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫ --- ... | t-left key₃ .kn {v1} {v3} {t₇} {t₃} x₉ x₁₀ x₁₁ ti₀ = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x (proj1 rr00) , ⟪ >-tr< x₂ (proj1 rr00) , >-tr< x₃ (proj1 rr00) ⟫ ⟫ ⟪ x₉ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ tt tt (t-node _ _ _ x (proj1 rr02) x₂ x₃ (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) ti ti₀) (t-single _ _) where --- rr00 : (kg < kn) ∧ ((kg < key₃) ∧ tr> kg t₇ ∧ tr> kg t₃) ∧ ⊤ --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₄ --- rr02 = proj1 (proj2 rr00) --- rr01 : (kn < kp) ∧ ((key₃ < kp) ∧ tr< kp t₇ ∧ tr< kp t₃) ∧ ⊤ --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫ --- rr03 = proj1 (proj2 rr01) --- RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₂ _ _ _) .(node key₃ _ _ _))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) t₂) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti (t-node key₂ .kp key₃ x₆ x₇ x₈ x₉ x₁₀ x₁₁ ti₁ ti₂)) (rbr-rotate-rl t₂ .leaf kg kp kn lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti₁ trb --- ... | t-single .kn .(⟪ Red , vn ⟫) = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x (proj1 rr00) , ⟪ >-tr< x₂ (proj1 rr00) , >-tr< x₃ (proj1 rr00) ⟫ ⟫ tt tt ⟪ <-trans (proj1 rr01) x₇ , ⟪ <-tr> x₁₀ (proj1 rr01) , <-tr> x₁₁ (proj1 rr01) ⟫ ⟫ (t-left _ _ x x₂ x₃ ti) (t-right _ _ x₇ x₁₀ x₁₁ ti₂) where --- rr00 : (kg < kn) ∧ ⊤ ∧ ⊤ --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₄ --- rr02 = proj1 (proj2 rr00) --- rr01 : (kn < kp) ∧ ⊤ ∧ ⊤ --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₆ , ⟪ x₈ , x₉ ⟫ ⟫ --- ... | t-left key₄ .kn {v1} {v3} {t₇} {t₃} x₁₂ x₁₃ x₁₄ ti₀ = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x (proj1 rr00) , ⟪ >-tr< x₂ (proj1 rr00) , >-tr< x₃ (proj1 rr00) ⟫ ⟫ ⟪ x₁₂ , ⟪ x₁₃ , x₁₄ ⟫ ⟫ tt ⟪ <-trans (proj1 rr01) x₇ , ⟪ <-tr> x₁₀ (proj1 rr01) , <-tr> x₁₁ (proj1 rr01) ⟫ ⟫ (t-node _ _ _ x (proj1 rr02) x₂ x₃ (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) ti ti₀) (t-right _ _ x₇ x₁₀ x₁₁ ti₂) where --- rr00 : (kg < kn) ∧ ((kg < key₄) ∧ tr> kg t₇ ∧ tr> kg t₃) ∧ ⊤ --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₄ --- rr02 = proj1 (proj2 rr00) --- rr01 : (kn < kp) ∧ ((key₄ < kp) ∧ tr< kp t₇ ∧ tr< kp t₃) ∧ ⊤ --- 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 = RB-repl→ti> _ _ _ _ _ trb lt1 x₁ --- rr02 = proj2 (proj2 rr00) --- rr01 : (kn < kp) ∧ ⊤ ∧ ((key₁ < kp) ∧ tr< kp t₃ ∧ tr< kp t₄) --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₃ , ⟪ x₄ , x₅ ⟫ ⟫ --- rr03 = proj2 (proj2 rr01) --- ... | t-node key₃ .kn .key₁ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x₆ x₇ x₈ x₉ x₁₀ x₁₁ t t₁ = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt ⟪ x₆ , ⟪ x₈ , x₉ ⟫ ⟫ ⟪ x₇ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ tt (t-right _ _ (proj1 rr02) (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) t) (t-left _ _ (proj1 rr03) (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) t₁) where --- rr00 : (kg < kn) ∧ ((kg < key₃) ∧ tr> kg t₇ ∧ tr> kg t₈) ∧ ((kg < key₁) ∧ tr> kg t₃ ∧ tr> kg t₄) --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₁ --- rr02 = proj1 (proj2 rr00) --- rr04 = proj2 (proj2 rr00) --- rr01 : (kn < kp) ∧ ((key₃ < kp) ∧ tr< kp t₇ ∧ tr< kp t₈) ∧ ((key₁ < kp) ∧ tr< kp t₃ ∧ tr< kp t₄) --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₃ , ⟪ x₄ , x₅ ⟫ ⟫ --- rr03 = proj2 (proj2 rr01) --- RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₂ _ _ _) .(node key₃ _ _ _))) (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-node key₂ .kp key₃ x₃ x₄ x₅ x₆ x₇ x₈ ti 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₁₁ ⟫ ⟫ ⟪ <-trans (proj1 rr01) x₄ , ⟪ <-tr> x₇ (proj1 rr01) , <-tr> x₈ (proj1 rr01) ⟫ ⟫ (t-single _ _) (t-node _ _ _ (proj1 rr03) x₄ (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) x₇ x₈ t ti₁ ) where --- rr00 : (kg < kn) ∧ ⊤ ∧ ((kg < key₁) ∧ tr> kg t₃ ∧ tr> kg t₄) --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₁ --- rr01 : (kn < kp) ∧ ⊤ ∧ ((key₁ < kp) ∧ tr< kp t₃ ∧ tr< kp t₄) --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₃ , ⟪ x₅ , x₆ ⟫ ⟫ --- rr03 = proj2 (proj2 rr01) --- ... | t-node key₄ .kn .key₁ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x₉ x₁₀ x₁₁ x₁₂ x₁₃ x₁₄ t t₁ = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt ⟪ x₉ , ⟪ x₁₁ , x₁₂ ⟫ ⟫ ⟪ x₁₀ , ⟪ x₁₃ , x₁₄ ⟫ ⟫ ⟪ <-trans (proj1 rr01) x₄ , ⟪ <-tr> x₇ (proj1 rr01) , <-tr> x₈ (proj1 rr01) ⟫ ⟫ (t-right _ _ (proj1 rr02) (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) t) (t-node _ _ _ (proj1 rr04) x₄ (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) x₇ x₈ t₁ ti₁ ) where --- rr00 : (kg < kn) ∧ ((kg < key₄) ∧ tr> kg t₇ ∧ tr> kg t₈) ∧ ((kg < key₁) ∧ tr> kg t₃ ∧ tr> kg t₄) --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₁ --- rr02 = proj1 (proj2 rr00) --- rr05 = proj2 (proj2 rr00) --- rr01 : (kn < kp) ∧ ((key₄ < kp) ∧ tr< kp t₇ ∧ tr< kp t₈) ∧ ((key₁ < kp) ∧ tr< kp t₃ ∧ tr< kp t₄) --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₃ , ⟪ x₅ , x₆ ⟫ ⟫ --- rr03 = proj1 (proj2 rr01) --- rr04 = proj2 (proj2 rr01) --- RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₃ _ _ _) .leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₂ _ _ _) t₂) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-node key₂ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti (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) ⟪ <-trans x (proj1 rr00) , ⟪ >-tr< x₂ (proj1 rr00) , >-tr< x₃ (proj1 rr00) ⟫ ⟫ tt ⟪ x₉ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ tt (t-left _ _ x x₂ x₃ ti ) (t-left _ _ (proj1 rr03) (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) t) where --- 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₄) --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫ --- rr03 = proj2 (proj2 rr01) --- ... | t-node key₄ .kn .key₁ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x₉ x₁₀ x₁₁ x₁₂ x₁₃ x₁₄ t t₁ = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x (proj1 rr00) , ⟪ >-tr< x₂ (proj1 rr00) , >-tr< x₃ (proj1 rr00) ⟫ ⟫ ⟪ x₉ , ⟪ x₁₁ , x₁₂ ⟫ ⟫ ⟪ x₁₀ , ⟪ x₁₃ , x₁₄ ⟫ ⟫ tt (t-node _ _ _ x (proj1 rr02) x₂ x₃ (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) ti t) (t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) t₁) where --- rr00 : (kg < kn) ∧ ((kg < key₄) ∧ tr> kg t₇ ∧ tr> kg t₈) ∧ ((kg < key₁) ∧ tr> kg t₃ ∧ tr> kg t₄) --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₄ --- rr02 = proj1 (proj2 rr00) --- rr05 = proj2 (proj2 rr00) --- rr01 : (kn < kp) ∧ ((key₄ < kp) ∧ tr< kp t₇ ∧ tr< kp t₈) ∧ ((key₁ < kp) ∧ tr< kp t₃ ∧ tr< kp t₄) --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫ --- rr03 = proj1 (proj2 rr01) --- rr04 = proj2 (proj2 rr01) --- RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₃ _ _ _) .(node key₄ _ _ _))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₂ _ _ _) t₂) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-node key₂ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti (t-node key₃ .kp key₄ x₆ x₇ x₈ x₉ x₁₀ x₁₁ ti₁ 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) ⟪ <-trans x (proj1 rr00) , ⟪ >-tr< x₂ (proj1 rr00) , >-tr< x₃ (proj1 rr00) ⟫ ⟫ tt ⟪ x₁₂ , ⟪ x₁₃ , x₁₄ ⟫ ⟫ ⟪ <-trans (proj1 rr01) x₇ , ⟪ <-tr> x₁₀ (proj1 rr01) , <-tr> x₁₁ (proj1 rr01) ⟫ ⟫ (t-left _ _ x x₂ x₃ ti) (t-node _ _ _ (proj1 rr03) x₇ (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) x₁₀ x₁₁ t ti₂ ) where --- 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₄) --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₆ , ⟪ x₈ , x₉ ⟫ ⟫ --- rr03 = proj2 (proj2 rr01) --- ... | t-node key₅ .kn .key₁ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x₁₂ x₁₃ x₁₄ x₁₅ x₁₆ x₁₇ t t₁ = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x (proj1 rr00) , ⟪ >-tr< x₂ (proj1 rr00) , >-tr< x₃ (proj1 rr00) ⟫ ⟫ ⟪ x₁₂ , ⟪ x₁₄ , x₁₅ ⟫ ⟫ ⟪ x₁₃ , ⟪ x₁₆ , x₁₇ ⟫ ⟫ ⟪ <-trans (proj1 rr01) x₇ , ⟪ <-tr> x₁₀ (proj1 rr01) , <-tr> x₁₁ (proj1 rr01) ⟫ ⟫ (t-node _ _ _ x (proj1 rr02) x₂ x₃ (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) ti t ) (t-node _ _ _ (proj1 rr04) x₇ (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) x₁₀ x₁₁ t₁ ti₂ ) where --- rr00 : (kg < kn) ∧ ((kg < key₅) ∧ tr> kg t₇ ∧ tr> kg t₈) ∧ ((kg < key₁) ∧ tr> kg t₃ ∧ tr> kg t₄) --- rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₄ --- rr02 = proj1 (proj2 rr00) --- rr05 = proj2 (proj2 rr00) --- rr01 : (kn < kp) ∧ ((key₅ < kp) ∧ tr< kp t₇ ∧ tr< kp t₈) ∧ ((key₁ < kp) ∧ tr< kp t₃ ∧ tr< kp t₄) --- rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₆ , ⟪ x₈ , x₉ ⟫ ⟫ --- rr03 = proj1 (proj2 rr01) --- rr04 = proj2 (proj2 rr01) --- +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 + (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 + (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 = 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 + (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₁ + (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 + (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 + (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 + (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 + (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 + (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 = 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 + (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 + (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 + (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 + (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 + (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 + (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 + (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 + 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 + 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 + 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 + 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 + 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 + 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 + 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₃ + (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 + (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 + rr04 : treeInvariant (node k1 ⟪ Red , c1 ⟫ (node key₂ value₂ t₁ t₄) leaf) + 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 + (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 + (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) + 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 + (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 = 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 + (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 + rr02 : treeInvariant (node key₄ value₁ t₄ t₅) + 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₆ + (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₉ ⟫ ⟫ + rr02 : treeInvariant (node key₄ value₁ t₄ t₅) + rr02 = RB-repl→ti _ _ _ _ ti trb + rr03 : treeInvariant (node key₁ ⟪ Red , c1 ⟫ (node key₅ _ _ _) (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 + 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 + (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₁₀ ⟫ ⟫ + rr02 : treeInvariant (node key₄ value₁ t₄ t₅) + rr02 = RB-repl→ti _ _ _ _ ti trb + rr03 : treeInvariant (node key₁ ⟪ Red , c1 ⟫ (node key₆ value₆ t₆ t₇) (node key₃ v3 t₂ t₃)) + 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) + = 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) + = 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) + = 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 + (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) + = 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) + = 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) + = 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) + = 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) = + 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₅ ⟫ ⟫ + rr01 : (kn < kg) ∧ ⊤ ∧ ((key₂ < kg ) ∧ tr< kg t₄ ∧ tr< kg t₅ ) -- tr< kg (node key₂ value₂ t₄ t₅) + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₂ + rr02 = proj2 (proj2 rr01) + 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 = + 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₅ ⟫ ⟫ + rr02 = proj1 (proj2 rr00) + rr01 : (kn < kg) ∧ ((key₂ < kg) ∧ tr< kg t₃ ∧ tr< kg t₅) ∧ ⊤ + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 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 , _ ⟫ (node key₃ value₃ t₄ t₆) _)) 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₅) .(node key₃ value₃ t₄ t₆) kg kp kn _ lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti trb +... | t-node .key₂ .kn .key₃ x₆ x₇ x₈ x₉ x₁₀ x₁₁ t t₇ = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt ⟪ x₆ , ⟪ x₈ , x₉ ⟫ ⟫ ⟪ x₇ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ tt (t-right _ _ (proj1 rr02) (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) t) (t-left _ _ (proj1 rr03) (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) t₇) where + rr00 : (kp < kn) ∧ ((kp < key₂) ∧ tr> kp t₃ ∧ tr> kp t₅) ∧ ((kp < key₃) ∧ tr> kp t₄ ∧ tr> kp t₆ ) + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₃ , ⟪ x₄ , x₅ ⟫ ⟫ + rr02 = proj1 (proj2 rr00) + rr01 : (kn < kg) ∧ ((key₂ < kg) ∧ tr< kg t₃ ∧ tr< kg t₅) ∧ ((key₃ < kg) ∧ tr< kg t₄ ∧ tr< kg t₆ ) + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₂ + rr03 = proj2 (proj2 rr01) +RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ (node key₂ value₂ t₅ t₆) (node key₁ value₁ t₁ t₂)) leaf) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₃) (node kg ⟪ Red , _ ⟫ t₄ _)) key value (t-left .kp .kg x x₁ x₂ (t-node key₂ .kp .key₁ x₃ x₄ x₅ x₆ x₇ x₈ ti ti₁)) (rbr-rotate-lr t₃ t₄ kg kp kn _ lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti₁ trb +... | t-single .kn .(⟪ Red , _ ⟫) = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x₃ (proj1 rr00) , ⟪ >-tr< x₅ (proj1 rr00) , >-tr< x₆ (proj1 rr00) ⟫ ⟫ tt tt tt (t-left _ _ x₃ x₅ x₆ ti) (t-single _ _) where + rr00 : (kp < kn) ∧ ⊤ ∧ ⊤ + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₄ , ⟪ x₇ , x₈ ⟫ ⟫ + rr01 : (kn < kg) ∧ ⊤ ∧ ⊤ + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₂ +... | t-right .kn key₃ {v1} {v3} {t₇} {t₈} x₉ x₁₀ x₁₁ t = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x₃ (proj1 rr00) , ⟪ >-tr< x₅ (proj1 rr00) , >-tr< x₆ (proj1 rr00) ⟫ ⟫ tt ⟪ x₉ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ tt (t-left _ _ x₃ x₅ x₆ ti) (t-left _ _ (proj1 rr03) (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) (treeRightDown _ _ (RB-repl→ti _ _ _ _ ti₁ trb))) where + rr00 : (kp < kn) ∧ ⊤ ∧ ((kp < key₃) ∧ tr> kp t₇ ∧ tr> kp t₈) -- tr> kp (node key₃ v3 t₇ t₈) + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₄ , ⟪ x₇ , x₈ ⟫ ⟫ + rr02 = proj1 (proj2 rr00) + rr01 : (kn < kg) ∧ ⊤ ∧ ((key₃ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) -- tr< kg (node key₃ v3 t₇ t₈) + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₂ + rr03 = proj2 (proj2 rr01) +... | t-left key₃ .kn {v1} {v3} {t₇} {t₈} x₉ x₁₀ x₁₁ t = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x₃ (proj1 rr00) , ⟪ >-tr< x₅ (proj1 rr00) , >-tr< x₆ (proj1 rr00) ⟫ ⟫ ⟪ x₉ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ tt tt (t-node key₂ kp key₃ x₃ (proj1 rr02) x₅ x₆ (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) ti (treeLeftDown _ _ (RB-repl→ti _ _ _ _ ti₁ trb))) (t-single _ _) where + rr00 : (kp < kn) ∧ ((kp < key₃) ∧ tr> kp t₇ ∧ tr> kp t₈) ∧ ⊤ + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₄ , ⟪ x₇ , x₈ ⟫ ⟫ + rr02 = proj1 (proj2 rr00) + rr01 : (kn < kg) ∧ ((key₃ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) ∧ ⊤ + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₂ +... | t-node key₃ .kn key₄ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀} x₉ x₁₀ x₁₁ x₁₂ x₁₃ x₁₄ t t₃ = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x₃ (proj1 rr00) , ⟪ >-tr< x₅ (proj1 rr00) , >-tr< x₆ (proj1 rr00) ⟫ ⟫ ⟪ x₉ , ⟪ x₁₁ , x₁₂ ⟫ ⟫ ⟪ x₁₀ , ⟪ x₁₃ , x₁₄ ⟫ ⟫ tt (t-node _ _ _ x₃ (proj1 rr02) x₅ x₆ (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) ti (treeLeftDown _ _ (RB-repl→ti _ _ _ _ ti₁ trb))) (t-left _ _ (proj1 rr03) (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) t₃) where + rr00 : (kp < kn) ∧ ((kp < key₃) ∧ tr> kp t₇ ∧ tr> kp t₈) ∧ ((kp < key₄) ∧ tr> kp t₉ ∧ tr> kp t₁₀) + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₄ , ⟪ x₇ , x₈ ⟫ ⟫ + rr02 = proj1 (proj2 rr00) + rr01 : (kn < kg) ∧ ((key₃ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) ∧ ((key₄ < kg) ∧ tr< kg t₉ ∧ tr< kg t₁₀) + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₂ + rr03 = proj2 (proj2 rr01) +RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .leaf leaf) (node key₂ value₂ t₅ t₆)) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ .leaf) (node kg ⟪ Red , _ ⟫ .leaf _)) .kn _ (t-node .kp .kg key₂ x x₁ x₂ x₃ x₄ x₅ (t-single .kp .(⟪ Red , v2 ⟫)) ti₁) (rbr-rotate-lr .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 , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .(node key _ _ _) leaf) (node key₂ value₂ t₅ t₆)) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ .leaf) (node kg ⟪ Red , _ ⟫ .leaf _)) .kn _ (t-node .kp .kg key₂ x x₁ x₂ x₃ x₄ x₅ (t-left key .kp x₆ x₇ x₈ ti) 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 ⟪ <-trans lt2 x₁ , ⟪ <-tr> x₄ lt2 , <-tr> x₅ lt2 ⟫ ⟫ (t-left _ _ x₆ x₇ x₈ ti) (t-right _ _ x₁ x₄ x₅ ti₁) +RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .leaf (node key₁ value₁ t₁ t₂)) .(node key₂ _ _ _)) (node kn ⟪ Black , value₃ ⟫ (node kp ⟪ Red , _ ⟫ _ t₃) (node kg ⟪ Red , _ ⟫ t₄ _)) key value (t-node .kp .kg key₂ x x₁ x₂ x₃ x₄ x₅ (t-right .kp .key₁ x₆ x₇ x₈ ti) ti₁) (rbr-rotate-lr t₃ t₄ kg kp kn _ lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti trb +... | t-single .kn .(⟪ Red , value₃ ⟫) = 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 : (kp < kn) ∧ ⊤ ∧ ⊤ + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫ + rr01 : (kn < kg) ∧ ⊤ ∧ ⊤ + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃ +... | t-right .kn key₃ {v1} {v3} {t₇} {t₈} x₉ x₁₀ x₁₁ t = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt tt ⟪ x₉ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ ⟪ <-trans (proj1 rr01) x₁ , ⟪ <-tr> x₄ (proj1 rr01) , <-tr> x₅ (proj1 rr01) ⟫ ⟫ (t-single _ _) (t-node _ _ _ (proj1 rr03) x₁ (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) x₄ x₅ (treeRightDown _ _ (RB-repl→ti _ _ _ _ ti trb)) ti₁) where + rr00 : (kp < kn) ∧ ⊤ ∧ ((kp < key₃) ∧ tr> kp t₇ ∧ tr> kp t₈) + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫ + rr02 = proj1 (proj2 rr00) + rr01 : (kn < kg) ∧ ⊤ ∧ ((key₃ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃ + rr03 = proj2 (proj2 rr01) +... | t-left key₃ .kn {v1} {v3} {t₇} {t₈} x₉ x₁₀ x₁₁ t = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt ⟪ x₉ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ tt ⟪ <-trans (proj1 rr01) x₁ , ⟪ <-tr> x₄ (proj1 rr01) , <-tr> x₅ (proj1 rr01) ⟫ ⟫ (t-right _ _ (proj1 rr02) (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) (treeLeftDown _ _ (RB-repl→ti _ _ _ _ ti trb))) (t-right _ _ x₁ x₄ x₅ ti₁) where + rr00 : (kp < kn) ∧ ((kp < key₃) ∧ tr> kp t₇ ∧ tr> kp t₈) ∧ ⊤ + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫ + rr02 = proj1 (proj2 rr00) + rr01 : (kn < kg) ∧ ((key₃ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) ∧ ⊤ + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃ + rr03 = proj1 (proj2 rr01) +... | t-node key₃ .kn key₄ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀} x₉ x₁₀ x₁₁ x₁₂ x₁₃ x₁₄ t t₃ = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt ⟪ x₉ , ⟪ x₁₁ , x₁₂ ⟫ ⟫ ⟪ x₁₀ , ⟪ x₁₃ , x₁₄ ⟫ ⟫ ⟪ <-trans (proj1 rr01) x₁ , ⟪ <-tr> x₄ (proj1 rr01) , <-tr> x₅ (proj1 rr01) ⟫ ⟫ (t-right _ _ (proj1 rr02) (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) (treeLeftDown _ _ (RB-repl→ti _ _ _ _ ti trb))) (t-node _ _ _ (proj1 rr03) x₁ (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) x₄ x₅ t₃ ti₁) where + rr00 : (kp < kn) ∧ ((kp < key₃) ∧ tr> kp t₇ ∧ tr> kp t₈) ∧ ((kp < key₄) ∧ tr> kp t₉ ∧ tr> kp t₁₀) + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫ + rr02 = proj1 (proj2 rr00) + rr01 : (kn < kg) ∧ ((key₃ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) ∧ ((key₄ < kg) ∧ tr< kg t₉ ∧ tr< kg t₁₀) + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃ + rr03 = proj2 (proj2 rr01) +RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .(node key₃ _ _ _) (node key₁ value₁ t₁ t₂)) .(node key₂ _ _ _)) (node kn ⟪ Black , value₃ ⟫ (node kp ⟪ Red , _ ⟫ _ t₃) (node kg ⟪ Red , _ ⟫ t₄ _)) key value (t-node .kp .kg key₂ x x₁ x₂ x₃ x₄ x₅ (t-node key₃ .kp .key₁ x₆ x₇ x₈ x₉ x₁₀ x₁₁ ti ti₂) ti₁) (rbr-rotate-lr t₃ t₄ kg kp kn _ lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti₂ trb +... | t-single .kn .(⟪ Red , value₃ ⟫) = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x₆ (proj1 rr00) , ⟪ >-tr< x₈ (proj1 rr00) , >-tr< x₉ (proj1 rr00) ⟫ ⟫ tt tt ⟪ <-trans (proj1 rr01) x₁ , ⟪ <-tr> x₄ (proj1 rr01) , <-tr> x₅ (proj1 rr01) ⟫ ⟫ (t-left _ _ x₆ x₈ x₉ ti) (t-right _ _ x₁ x₄ x₅ ti₁) where + rr00 : (kp < kn) ∧ ⊤ ∧ ⊤ + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₇ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ + rr01 : (kn < kg) ∧ ⊤ ∧ ⊤ + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃ +... | t-right .kn key₄ {v1} {v3} {t₇} {t₈} x₁₂ x₁₃ x₁₄ t = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x₆ (proj1 rr00) , ⟪ >-tr< x₈ (proj1 rr00) , >-tr< x₉ (proj1 rr00) ⟫ ⟫ tt ⟪ x₁₂ , ⟪ x₁₃ , x₁₄ ⟫ ⟫ ⟪ <-trans (proj1 rr01) x₁ , ⟪ <-tr> x₄ (proj1 rr01) , <-tr> x₅ (proj1 rr01) ⟫ ⟫ (t-left _ _ x₆ x₈ x₉ ti) (t-node _ _ _ (proj1 rr03) x₁ (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) x₄ x₅ (treeRightDown _ _ (RB-repl→ti _ _ _ _ ti₂ trb)) ti₁ ) where + rr00 : (kp < kn) ∧ ⊤ ∧ ((kp < key₄) ∧ tr> kp t₇ ∧ tr> kp t₈) + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₇ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ + rr02 = proj2 (proj2 rr00) + rr01 : (kn < kg) ∧ ⊤ ∧ ((key₄ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃ + rr03 = proj2 (proj2 rr01) +... | t-left key₄ .kn {v1} {v3} {t₇} {t₈} x₁₂ x₁₃ x₁₄ t = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x₆ (proj1 rr00) , ⟪ >-tr< x₈ (proj1 rr00) , >-tr< x₉ (proj1 rr00) ⟫ ⟫ ⟪ x₁₂ , ⟪ x₁₃ , x₁₄ ⟫ ⟫ tt ⟪ <-trans (proj1 rr01) x₁ , ⟪ <-tr> x₄ (proj1 rr01) , <-tr> x₅ (proj1 rr01) ⟫ ⟫ (t-node _ _ _ x₆ (proj1 rr02) x₈ x₉ (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) ti (treeLeftDown _ _ (RB-repl→ti _ _ _ _ ti₂ trb)) ) (t-right _ _ x₁ x₄ x₅ ti₁) where + rr00 : (kp < kn) ∧ ((kp < key₄) ∧ tr> kp t₇ ∧ tr> kp t₈) ∧ ⊤ + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₇ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ + rr02 = proj1 (proj2 rr00) + rr01 : (kn < kg) ∧ ((key₄ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) ∧ ⊤ + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃ + rr03 = proj1 (proj2 rr01) +... | t-node key₄ .kn key₅ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀}x₁₂ x₁₃ x₁₄ x₁₅ x₁₆ x₁₇ t t₃ = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x₆ (proj1 rr00) , ⟪ >-tr< x₈ (proj1 rr00) , >-tr< x₉ (proj1 rr00) ⟫ ⟫ ⟪ x₁₂ , ⟪ x₁₄ , x₁₅ ⟫ ⟫ ⟪ x₁₃ , ⟪ x₁₆ , x₁₇ ⟫ ⟫ ⟪ <-trans (proj1 rr01) x₁ , ⟪ <-tr> x₄ (proj1 rr01) , <-tr> x₅ (proj1 rr01) ⟫ ⟫ (t-node _ _ _ x₆ (proj1 rr02) x₈ x₉ (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) ti t ) (t-node _ _ _ (proj1 rr04) x₁ (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) x₄ x₅ (treeRightDown _ _ (RB-repl→ti _ _ _ _ ti₂ trb)) ti₁ ) where + rr00 : (kp < kn) ∧ ((kp < key₄) ∧ tr> kp t₇ ∧ tr> kp t₈) ∧ ((kp < key₅) ∧ tr> kp t₉ ∧ tr> kp t₁₀) + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 ⟪ x₇ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ + rr02 = proj1 (proj2 rr00) + rr05 = proj2 (proj2 rr00) + rr01 : (kn < kg) ∧ ((key₄ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈) ∧ ((key₅ < kg) ∧ tr< kg t₉ ∧ tr< kg t₁₀) + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃ + 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 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₁ + rr01 : (kn < kp) ∧ ⊤ ∧ ⊤ + 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 (node key₁ value₁ t₂ t₃)) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-right .kg .kp x x₁ x₂ (t-left key₂ .kp x₃ x₄ x₅ ti)) (rbr-rotate-rl .(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 : (kg < kn) ∧ ((kg < key₁) ∧ tr> kg t₂ ∧ tr> kg t₃) ∧ ⊤ + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₁ + rr02 = proj1 (proj2 rr00) + rr01 : (kn < kp) ∧ ((key₁ < kp) ∧ tr< kp t₂ ∧ tr< kp t₃) ∧ ⊤ + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₃ , ⟪ x₄ , x₅ ⟫ ⟫ +RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₂ _ _ _) .(node key₃ _ _ _))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf (node key₁ value₁ t₂ t₃)) (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 .(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 ⟪ <-trans (proj1 rr01) x₄ , ⟪ <-tr> x₇ (proj1 rr01) , <-tr> x₈ (proj1 rr01) ⟫ ⟫ (t-right _ _ (proj1 rr02) (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) t) (t-right _ _ x₄ x₇ x₈ ti₁) where + rr00 : (kg < kn) ∧ ((kg < key₁) ∧ tr> kg t₂ ∧ tr> kg t₃) ∧ ⊤ + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₁ + rr02 = proj1 (proj2 rr00) + rr01 : (kn < kp) ∧ ((key₁ < kp) ∧ tr< kp t₂ ∧ tr< kp t₃) ∧ ⊤ + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₃ , ⟪ x₅ , x₆ ⟫ ⟫ +RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .leaf .leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) .leaf) (node kp ⟪ Red , _ ⟫ leaf _)) .kn .vn (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti (t-single .kp .(⟪ Red , vp ⟫))) (rbr-rotate-rl .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 , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .leaf .(node key₂ _ _ _))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) .leaf) (node kp ⟪ Red , _ ⟫ leaf _)) .kn .vn (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti (t-right .kp key₂ x₆ x₇ x₈ ti₁)) (rbr-rotate-rl .leaf .leaf kg kp kn _ lt1 lt2 rbr-leaf) = t-node _ _ _ lt1 lt2 ⟪ <-trans x lt1 , ⟪ >-tr< x₂ lt1 , >-tr< x₃ lt1 ⟫ ⟫ tt tt ⟪ <-trans lt2 x₆ , ⟪ <-tr> x₇ lt2 , <-tr> x₈ lt2 ⟫ ⟫ (t-left _ _ x x₂ x₃ ti) (t-right _ _ x₆ x₇ x₈ ti₁) +RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₂ _ _ _) .leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) t₂) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti (t-left key₂ .kp x₆ x₇ x₈ ti₁)) (rbr-rotate-rl t₂ .leaf kg kp kn _ lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti₁ trb +... | t-single .kn .(⟪ Red , vn ⟫) = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x (proj1 rr00) , ⟪ >-tr< x₂ (proj1 rr00) , >-tr< x₃ (proj1 rr00) ⟫ ⟫ tt tt tt (t-left _ _ x x₂ x₃ ti) (t-single _ _) where + rr00 : (kg < kn) ∧ ⊤ ∧ ⊤ + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₄ + rr01 : (kn < kp) ∧ ⊤ ∧ ⊤ + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫ +... | t-left key₃ .kn {v1} {v3} {t₇} {t₃} x₉ x₁₀ x₁₁ ti₀ = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x (proj1 rr00) , ⟪ >-tr< x₂ (proj1 rr00) , >-tr< x₃ (proj1 rr00) ⟫ ⟫ ⟪ x₉ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ tt tt (t-node _ _ _ x (proj1 rr02) x₂ x₃ (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) ti ti₀) (t-single _ _) where + rr00 : (kg < kn) ∧ ((kg < key₃) ∧ tr> kg t₇ ∧ tr> kg t₃) ∧ ⊤ + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₄ + rr02 = proj1 (proj2 rr00) + rr01 : (kn < kp) ∧ ((key₃ < kp) ∧ tr< kp t₇ ∧ tr< kp t₃) ∧ ⊤ + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫ + rr03 = proj1 (proj2 rr01) +RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₂ _ _ _) .(node key₃ _ _ _))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) t₂) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti (t-node key₂ .kp key₃ x₆ x₇ x₈ x₉ x₁₀ x₁₁ ti₁ ti₂)) (rbr-rotate-rl t₂ .leaf kg kp kn _ lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti₁ trb +... | t-single .kn .(⟪ Red , vn ⟫) = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x (proj1 rr00) , ⟪ >-tr< x₂ (proj1 rr00) , >-tr< x₃ (proj1 rr00) ⟫ ⟫ tt tt ⟪ <-trans (proj1 rr01) x₇ , ⟪ <-tr> x₁₀ (proj1 rr01) , <-tr> x₁₁ (proj1 rr01) ⟫ ⟫ (t-left _ _ x x₂ x₃ ti) (t-right _ _ x₇ x₁₀ x₁₁ ti₂) where + rr00 : (kg < kn) ∧ ⊤ ∧ ⊤ + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₄ + rr02 = proj1 (proj2 rr00) + rr01 : (kn < kp) ∧ ⊤ ∧ ⊤ + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₆ , ⟪ x₈ , x₉ ⟫ ⟫ +... | t-left key₄ .kn {v1} {v3} {t₇} {t₃} x₁₂ x₁₃ x₁₄ ti₀ = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x (proj1 rr00) , ⟪ >-tr< x₂ (proj1 rr00) , >-tr< x₃ (proj1 rr00) ⟫ ⟫ ⟪ x₁₂ , ⟪ x₁₃ , x₁₄ ⟫ ⟫ tt ⟪ <-trans (proj1 rr01) x₇ , ⟪ <-tr> x₁₀ (proj1 rr01) , <-tr> x₁₁ (proj1 rr01) ⟫ ⟫ (t-node _ _ _ x (proj1 rr02) x₂ x₃ (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) ti ti₀) (t-right _ _ x₇ x₁₀ x₁₁ ti₂) where + rr00 : (kg < kn) ∧ ((kg < key₄) ∧ tr> kg t₇ ∧ tr> kg t₃) ∧ ⊤ + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₄ + rr02 = proj1 (proj2 rr00) + rr01 : (kn < kp) ∧ ((key₄ < kp) ∧ tr< kp t₇ ∧ tr< kp t₃) ∧ ⊤ + 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 = RB-repl→ti> _ _ _ _ _ trb lt1 x₁ + rr02 = proj2 (proj2 rr00) + rr01 : (kn < kp) ∧ ⊤ ∧ ((key₁ < kp) ∧ tr< kp t₃ ∧ tr< kp t₄) + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₃ , ⟪ x₄ , x₅ ⟫ ⟫ + rr03 = proj2 (proj2 rr01) +... | t-node key₃ .kn .key₁ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x₆ x₇ x₈ x₉ x₁₀ x₁₁ t t₁ = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt ⟪ x₆ , ⟪ x₈ , x₉ ⟫ ⟫ ⟪ x₇ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ tt (t-right _ _ (proj1 rr02) (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) t) (t-left _ _ (proj1 rr03) (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) t₁) where + rr00 : (kg < kn) ∧ ((kg < key₃) ∧ tr> kg t₇ ∧ tr> kg t₈) ∧ ((kg < key₁) ∧ tr> kg t₃ ∧ tr> kg t₄) + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₁ + rr02 = proj1 (proj2 rr00) + rr04 = proj2 (proj2 rr00) + rr01 : (kn < kp) ∧ ((key₃ < kp) ∧ tr< kp t₇ ∧ tr< kp t₈) ∧ ((key₁ < kp) ∧ tr< kp t₃ ∧ tr< kp t₄) + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₃ , ⟪ x₄ , x₅ ⟫ ⟫ + rr03 = proj2 (proj2 rr01) +RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₂ _ _ _) .(node key₃ _ _ _))) (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-node key₂ .kp key₃ x₃ x₄ x₅ x₆ x₇ x₈ ti 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₁₁ ⟫ ⟫ ⟪ <-trans (proj1 rr01) x₄ , ⟪ <-tr> x₇ (proj1 rr01) , <-tr> x₈ (proj1 rr01) ⟫ ⟫ (t-single _ _) (t-node _ _ _ (proj1 rr03) x₄ (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) x₇ x₈ t ti₁ ) where + rr00 : (kg < kn) ∧ ⊤ ∧ ((kg < key₁) ∧ tr> kg t₃ ∧ tr> kg t₄) + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₁ + rr01 : (kn < kp) ∧ ⊤ ∧ ((key₁ < kp) ∧ tr< kp t₃ ∧ tr< kp t₄) + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₃ , ⟪ x₅ , x₆ ⟫ ⟫ + rr03 = proj2 (proj2 rr01) +... | t-node key₄ .kn .key₁ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x₉ x₁₀ x₁₁ x₁₂ x₁₃ x₁₄ t t₁ = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt ⟪ x₉ , ⟪ x₁₁ , x₁₂ ⟫ ⟫ ⟪ x₁₀ , ⟪ x₁₃ , x₁₄ ⟫ ⟫ ⟪ <-trans (proj1 rr01) x₄ , ⟪ <-tr> x₇ (proj1 rr01) , <-tr> x₈ (proj1 rr01) ⟫ ⟫ (t-right _ _ (proj1 rr02) (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) t) (t-node _ _ _ (proj1 rr04) x₄ (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) x₇ x₈ t₁ ti₁ ) where + rr00 : (kg < kn) ∧ ((kg < key₄) ∧ tr> kg t₇ ∧ tr> kg t₈) ∧ ((kg < key₁) ∧ tr> kg t₃ ∧ tr> kg t₄) + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₁ + rr02 = proj1 (proj2 rr00) + rr05 = proj2 (proj2 rr00) + rr01 : (kn < kp) ∧ ((key₄ < kp) ∧ tr< kp t₇ ∧ tr< kp t₈) ∧ ((key₁ < kp) ∧ tr< kp t₃ ∧ tr< kp t₄) + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₃ , ⟪ x₅ , x₆ ⟫ ⟫ + rr03 = proj1 (proj2 rr01) + rr04 = proj2 (proj2 rr01) +RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₃ _ _ _) .leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₂ _ _ _) t₂) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-node key₂ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti (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) ⟪ <-trans x (proj1 rr00) , ⟪ >-tr< x₂ (proj1 rr00) , >-tr< x₃ (proj1 rr00) ⟫ ⟫ tt ⟪ x₉ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ tt (t-left _ _ x x₂ x₃ ti ) (t-left _ _ (proj1 rr03) (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) t) where + 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₄) + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫ + rr03 = proj2 (proj2 rr01) +... | t-node key₄ .kn .key₁ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x₉ x₁₀ x₁₁ x₁₂ x₁₃ x₁₄ t t₁ = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x (proj1 rr00) , ⟪ >-tr< x₂ (proj1 rr00) , >-tr< x₃ (proj1 rr00) ⟫ ⟫ ⟪ x₉ , ⟪ x₁₁ , x₁₂ ⟫ ⟫ ⟪ x₁₀ , ⟪ x₁₃ , x₁₄ ⟫ ⟫ tt (t-node _ _ _ x (proj1 rr02) x₂ x₃ (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) ti t) (t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) t₁) where + rr00 : (kg < kn) ∧ ((kg < key₄) ∧ tr> kg t₇ ∧ tr> kg t₈) ∧ ((kg < key₁) ∧ tr> kg t₃ ∧ tr> kg t₄) + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₄ + rr02 = proj1 (proj2 rr00) + rr05 = proj2 (proj2 rr00) + rr01 : (kn < kp) ∧ ((key₄ < kp) ∧ tr< kp t₇ ∧ tr< kp t₈) ∧ ((key₁ < kp) ∧ tr< kp t₃ ∧ tr< kp t₄) + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫ + rr03 = proj1 (proj2 rr01) + rr04 = proj2 (proj2 rr01) +RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₃ _ _ _) .(node key₄ _ _ _))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₂ _ _ _) t₂) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-node key₂ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti (t-node key₃ .kp key₄ x₆ x₇ x₈ x₉ x₁₀ x₁₁ ti₁ 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) ⟪ <-trans x (proj1 rr00) , ⟪ >-tr< x₂ (proj1 rr00) , >-tr< x₃ (proj1 rr00) ⟫ ⟫ tt ⟪ x₁₂ , ⟪ x₁₃ , x₁₄ ⟫ ⟫ ⟪ <-trans (proj1 rr01) x₇ , ⟪ <-tr> x₁₀ (proj1 rr01) , <-tr> x₁₁ (proj1 rr01) ⟫ ⟫ (t-left _ _ x x₂ x₃ ti) (t-node _ _ _ (proj1 rr03) x₇ (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) x₁₀ x₁₁ t ti₂ ) where + 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₄) + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₆ , ⟪ x₈ , x₉ ⟫ ⟫ + rr03 = proj2 (proj2 rr01) +... | t-node key₅ .kn .key₁ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x₁₂ x₁₃ x₁₄ x₁₅ x₁₆ x₁₇ t t₁ = t-node _ _ _ (proj1 rr00) (proj1 rr01) ⟪ <-trans x (proj1 rr00) , ⟪ >-tr< x₂ (proj1 rr00) , >-tr< x₃ (proj1 rr00) ⟫ ⟫ ⟪ x₁₂ , ⟪ x₁₄ , x₁₅ ⟫ ⟫ ⟪ x₁₃ , ⟪ x₁₆ , x₁₇ ⟫ ⟫ ⟪ <-trans (proj1 rr01) x₇ , ⟪ <-tr> x₁₀ (proj1 rr01) , <-tr> x₁₁ (proj1 rr01) ⟫ ⟫ (t-node _ _ _ x (proj1 rr02) x₂ x₃ (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) ti t ) (t-node _ _ _ (proj1 rr04) x₇ (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) x₁₀ x₁₁ t₁ ti₂ ) where + rr00 : (kg < kn) ∧ ((kg < key₅) ∧ tr> kg t₇ ∧ tr> kg t₈) ∧ ((kg < key₁) ∧ tr> kg t₃ ∧ tr> kg t₄) + rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₄ + rr02 = proj1 (proj2 rr00) + rr05 = proj2 (proj2 rr00) + rr01 : (kn < kp) ∧ ((key₅ < kp) ∧ tr< kp t₇ ∧ tr< kp t₈) ∧ ((key₁ < kp) ∧ tr< kp t₃ ∧ tr< kp t₄) + rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₆ , ⟪ x₈ , x₉ ⟫ ⟫ + rr03 = proj1 (proj2 rr01) + rr04 = proj2 (proj2 rr01) + -- -- if we consider tree invariant, this may be much simpler and faster @@ -1515,7 +1475,7 @@ → (stack : List (bt (Color ∧ A))) → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → (exit : (r : RBI key value tree0 tree1 stack ) → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )) → t -replaceRBTNode key value tree0 rbi tree1 stack rbi-stack exit = ? +replaceRBTNode key value tree0 rbi tree1 stack rbi-stack exit = {!!} -- -- RBT is blanced with the stack, simply rebuild tree without rototation @@ -1533,7 +1493,7 @@ → stack1 ≡ (orig ∷ []) → RBI key value orig repl stack1 → t ) → t -rebuildRBT key value orig repl stack r bdepth-eq next exit = ? +rebuildRBT key value orig repl stack r bdepth-eq next exit = {!!} insertCase5 : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) @@ -1551,24 +1511,24 @@ -- node-key grand < node-key repl < node-key parent → rotateRight parent then insertCase6 -- else insertCase6 insertCase51 : (tree1 grand : bt (Color ∧ A)) → tree1 ≡ tree → grand ≡ PG.grand pg → t - insertCase51 leaf grand teq geq = next ? ? ? ? - insertCase51 (node kr vr rleft rright) leaf teq geq = ? -- can't happen + insertCase51 leaf grand teq geq = next {!!} {!!} {!!} {!!} + insertCase51 (node kr vr rleft rright) leaf teq geq = {!!} -- can't happen insertCase51 (node kr vr rleft rright) (node kg vg grand grand₁) teq geq with <-cmp kr kg ... | tri< a ¬b ¬c = insertCase511 (PG.parent pg) refl where insertCase511 : (parent : bt (Color ∧ A)) → parent ≡ PG.parent pg → t insertCase511 leaf peq = ⊥-elim (proj2 (pg-prop-1 _ tree orig stack pg) (sym peq) ) insertCase511 (node key₂ ⟪ co , value ⟫ n1 n2) peq with <-cmp key key₂ - ... | tri< a ¬b ¬c = next ? ? ? ? - ... | tri≈ ¬a b ¬c = ? -- can't happen - ... | tri> ¬a ¬b c = next ? ? ? ? --- rotareRight → insertCase6 key value orig ? stack ? pg next exit - ... | tri≈ ¬a b ¬c = ? -- can't happen - ... | tri> ¬a ¬b c = ? where + ... | tri< a ¬b ¬c = next {!!} {!!} {!!} {!!} + ... | tri≈ ¬a b ¬c = {!!} -- can't happen + ... | tri> ¬a ¬b c = next {!!} {!!} {!!} {!!} --- rotareRight → insertCase6 key value orig ? stack ? pg next exit + ... | tri≈ ¬a b ¬c = {!!} -- can't happen + ... | tri> ¬a ¬b c = {!!} where insertCase511 : (parent : bt (Color ∧ A)) → parent ≡ PG.parent pg → t insertCase511 leaf peq = ⊥-elim (proj2 (pg-prop-1 _ tree orig stack pg) (sym peq) ) insertCase511 (node key₂ ⟪ co , value ⟫ n1 n2) peq with <-cmp key key₂ - ... | tri< a ¬b ¬c = next ? ? ? ? --- rotareLeft → insertCase6 key value orig ? stack ? pg next exit - ... | tri≈ ¬a b ¬c = ? -- can't happen - ... | tri> ¬a ¬b c = next ? ? ? ? + ... | tri< a ¬b ¬c = next {!!} {!!} {!!} {!!} --- rotareLeft → insertCase6 key value orig ? stack ? pg next exit + ... | tri≈ ¬a b ¬c = {!!} -- can't happen + ... | tri> ¬a ¬b c = next {!!} {!!} {!!} {!!} -- -- replaced node increase blackdepth, so we need tree rotate @@ -1603,8 +1563,9 @@ → RBI key value orig repl stack1 → t ) → t replaceRBP {n} {m} {A} {t} key value orig repl stack r next exit with RBI.state r -... | rebuild bdepth-eq = rebuildRBT key value orig repl stack r bdepth-eq next exit -... | rotate repl-red pbdeth< with stackToPG (RBI.tree r) orig stack (RBI.si 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) ... | case1 eq = exit repl stack eq r -- no stack, replace top node ... | case2 (case1 eq) = insertCase12 orig refl (RBI.si r) where -- @@ -1623,24 +1584,26 @@ rb04 refl refl (s-right tree leaf tree₁ x si) = si-property2 _ (s-right tree leaf tree₁ x si) refl rb04 refl refl (s-left tree₁ leaf tree x si) = si-property2 _ (s-left tree₁ leaf tree x si) refl insertCase12 tr0@(node key₁ value₁ left right) refl si with <-cmp key key₁ | child-replaced key (node key₁ value₁ left right) in creq - ... | tri< a ¬b ¬c | cr = exit (node key₁ value₁ repl right) (orig ∷ []) refl record { + ... | tri< a ¬b ¬c | cr = exit (to-black (node key₁ value₁ repl right)) (orig ∷ []) refl record { tree = orig ; 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 = {!!} -- subst (λ k → RBtreeInvariant (node key₁ k repl right)) ? (rb-left-red ? ? ?) ; si = s-nil - ; rotated = rbr-left a (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) (RBI.rotated r)) - ; state = rebuild ? + -- 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 {!!} {!!} } 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 + -- rb05 : replacedRBTree key value (RBI.tree r) repl + -- rb05 = RBI.rotated r rb06 : RBtreeInvariant (to-red (node key₁ value₁ repl right)) - rb06 = rb-node-red ? ? ? ? ? + rb06 = {!!} ... | 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 @@ -1665,37 +1628,35 @@ ; origti = RBI.origti r ; origrb = RBI.origrb r ; treerb = RBI.origrb r - ; replrb = ? + ; replrb = {!!} ; si = s-nil - ; rotated = ? - ; state = rebuild ? + ; state = top-black {!!} {!!} } where - rb09 : {n : Level} {A : Set n} → {key key1 key2 : ℕ} {value value1 : A} {t1 t2 : bt (Color ∧ A)} - → RBtreeInvariant (node key ⟪ Red , value ⟫ leaf (node key1 ⟪ Black , value1 ⟫ t1 t2)) - → key < key1 - rb09 (rb-right-red x x0 x2) = x + -- rb09 : {n : Level} {A : Set n} → {key key1 key2 : ℕ} {value value1 : A} {t1 t2 : bt (Color ∧ A)} + -- → RBtreeInvariant (node key ⟪ Red , value ⟫ leaf (node key1 ⟪ Black , value1 ⟫ t1 t2)) + -- → key < key1 + -- rb09 (rb-right-red x x0 x2) = x -- rb05 should more general tkey : {n : Level} {A : Set n } → (rbt : bt (Color ∧ A)) → ℕ tkey (node key value t t2) = key tkey leaf = {!!} -- key is none ... | case2 (case2 pg) with PG.uncle pg in uneq -... | leaf = ? -- insertCase5 -... | node key₁ ⟪ Black , value₁ ⟫ t₁ t₂ = ? -- insertCase5 +... | leaf = {!!} -- insertCase5 +... | node key₁ ⟪ Black , value₁ ⟫ t₁ t₂ = {!!} -- insertCase5 ... | node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ with PG.pg pg ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = next (to-red (node kg vg (to-black (node kp vp repl n1)) (to-black (PG.uncle pg)))) (PG.rest pg) record { tree = PG.grand pg ; origti = RBI.origti r ; origrb = RBI.origrb r - ; treerb = ? - ; replrb = ? - ; si = ? - ; rotated = ? - ; state = rotate refl ? - } ? -... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? -... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? -... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? + ; treerb = {!!} + ; replrb = {!!} + ; si = {!!} + ; state = rotate refl {!!} {!!} + } {!!} +... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!} +... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!} +... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}