Mercurial > hg > Gears > GearsAgda
changeset 889:e753aea361ea
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 15 May 2024 14:13:41 +0900 |
| parents | 5b6225b81409 |
| children | 6a5fe1c4855a |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 468 insertions(+), 463 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Mon May 13 21:59:18 2024 +0900 +++ b/hoareBinaryTree1.agda Wed May 15 14:13:41 2024 +0900 @@ -798,11 +798,11 @@ data replacedRBTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt (Color ∧ A) ) → Set n where -- no rotation case rbr-leaf : replacedRBTree key value leaf (node key ⟪ Red , value ⟫ leaf leaf) - rbr-node : {value₁ : A} → {ca ca1 : Color } → {t t₁ : bt (Color ∧ A)} → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ ca1 , value ⟫ t t₁) - rbr-right : {k : ℕ } {v1 : A} → {ca ca1 : Color} → {t t1 t2 : bt (Color ∧ A)} - → k < key → replacedRBTree key value t2 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ ca1 , v1 ⟫ t1 t) - rbr-left : {k : ℕ } {v1 : A} → {ca ca1 : Color} → {t t1 t2 : bt (Color ∧ A)} - → key < k → replacedRBTree key value t1 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ ca1 , v1 ⟫ t t2) -- k < key → key < k + 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)} + → 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)} + → 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 -- 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₂ @@ -981,461 +981,462 @@ RB-repl→ti : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A) ) → (key : ℕ ) → (value : A) → treeInvariant tree → replacedRBTree key value tree repl → treeInvariant repl -RB-repl→ti .leaf .(node key ⟪ Red , value ⟫ leaf leaf) key value ti rbr-leaf = t-single key ⟪ Red , value ⟫ -RB-repl→ti .(node key ⟪ _ , _ ⟫ leaf leaf) .(node key ⟪ _ , value ⟫ leaf leaf) key value (t-single .key .(⟪ _ , _ ⟫)) rbr-node = t-single key ⟪ _ , value ⟫ -RB-repl→ti .(node key ⟪ _ , _ ⟫ leaf (node key₁ _ _ _)) .(node key ⟪ _ , value ⟫ leaf (node key₁ _ _ _)) key value - (t-right .key key₁ x x₁ x₂ ti) rbr-node = t-right key key₁ x x₁ x₂ ti -RB-repl→ti .(node key ⟪ _ , _ ⟫ (node key₁ _ _ _) leaf) .(node key ⟪ _ , value ⟫ (node key₁ _ _ _) leaf) key value - (t-left key₁ .key x x₁ x₂ ti) rbr-node = t-left key₁ key x x₁ x₂ ti -RB-repl→ti .(node key ⟪ _ , _ ⟫ (node key₁ _ _ _) (node key₂ _ _ _)) .(node key ⟪ _ , value ⟫ (node key₁ _ _ _) (node key₂ _ _ _)) key value - (t-node key₁ .key key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) rbr-node = t-node key₁ key key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁ -RB-repl→ti (node key₁ ⟪ ca , v1 ⟫ leaf leaf) (node key₁ ⟪ ca1 , 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₂ ⟪ ca1 , 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₃ ⟪ ca1 , 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 = ? +-- 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 @@ -1622,20 +1623,24 @@ 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₁ ⟪ Black , proj2 value₁ ⟫ left right) (orig ∷ []) refl record { + ... | tri< a ¬b ¬c | cr = exit (node key₁ value₁ repl right) (orig ∷ []) refl record { tree = orig ; origti = RBI.origti r ; origrb = RBI.origrb r ; treerb = RBI.origrb r - ; replrb = ? + ; replrb = ? -- subst (λ k → RBtreeInvariant (node key₁ k repl right)) ? (rb-left-red ? ? ?) ; si = s-nil - ; rotated = ? + ; rotated = 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 + rb06 : RBtreeInvariant (to-red (node key₁ value₁ repl right)) + rb06 = rb-node-red ? ? ? ? ? ... | 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