|
954
|
1 -- {-# OPTIONS --cubical-compatible --safe #-}
|
|
|
2 {-# OPTIONS --allow-unsolved-metas --cubical-compatible #-}
|
|
|
3 module RBTree1 where
|
|
|
4
|
|
|
5 open import Level hiding (suc ; zero ; _⊔_ )
|
|
|
6
|
|
|
7 open import Data.Nat hiding (compare)
|
|
|
8 open import Data.Nat.Properties as NatProp
|
|
|
9 open import Data.Maybe
|
|
|
10 open import Data.Maybe.Properties
|
|
|
11 open import Data.Empty
|
|
|
12 open import Data.Unit
|
|
|
13 open import Data.List
|
|
|
14 open import Data.List.Properties
|
|
|
15 open import Data.Product
|
|
|
16
|
|
|
17 open import Function as F hiding (const)
|
|
|
18
|
|
|
19 open import Relation.Binary
|
|
|
20 open import Relation.Binary.PropositionalEquality
|
|
|
21 open import Relation.Nullary
|
|
|
22 open import logic
|
|
|
23 open import nat
|
|
|
24
|
|
|
25 open import BTree
|
|
|
26 open import RBTreeBase
|
|
|
27
|
|
|
28 open _∧_
|
|
|
29
|
|
|
30
|
|
|
31 RB-repl→ti-lem03 : {n : Level} {A : Set n} {key k : ℕ} {value v1 : A} {ca : Color} {t t1 t2 : bt (Color ∧ A)} (x : color t1 ≡ color t) (x₁ : key < k)
|
|
|
32 (rbt : replacedRBTree key value t1 t) → (treeInvariant t1 → treeInvariant t) → treeInvariant (node k ⟪ ca , v1 ⟫ t1 t2) → treeInvariant (node k ⟪ ca , v1 ⟫ t t2)
|
|
|
33 RB-repl→ti-lem03 {n} {A} {key} {k} {value} {v1} {ca} {t} {t1} {t2} ceq x₁ rbt prev ti = lem21 (node k ⟪ ca , v1 ⟫ t1 t2) ti refl rbt where
|
|
|
34 lem22 : treeInvariant t
|
|
|
35 lem22 = prev (treeLeftDown _ _ ti)
|
|
|
36 lem21 : (tree : bt (Color ∧ A)) → treeInvariant tree → tree ≡ node k ⟪ ca , v1 ⟫ t1 t2 → replacedRBTree key value t1 t → treeInvariant (node k ⟪ ca , v1 ⟫ t t2)
|
|
|
37 lem21 .leaf t-leaf () rbt
|
|
|
38 lem21 .(node k₃ value₁ leaf leaf) (t-single k₃ value₁) eq rbr-leaf = subst treeInvariant
|
|
|
39 (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left key k₃ (subst (λ k → key < k) (sym lem23) x₁) tt tt lem22) where
|
|
|
40 lem23 : k₃ ≡ k
|
|
|
41 lem23 = just-injective (cong node-key eq)
|
|
|
42 lem21 .(node key value leaf leaf) (t-single key value) () rbr-node
|
|
|
43 lem21 .(node key value leaf leaf) (t-single key value) () (rbr-right x x₁ rbt)
|
|
|
44 lem21 .(node key value leaf leaf) (t-single key value) () (rbr-left x x₁ rbt)
|
|
|
45 lem21 .(node key value leaf leaf) (t-single key value) () (rbr-black-right x x₁ rbt)
|
|
|
46 lem21 .(node key value leaf leaf) (t-single key value) () (rbr-black-left x x₁ rbt)
|
|
|
47 lem21 .(node key value leaf leaf) (t-single key value) () (rbr-flip-ll x x₁ x₂ rbt)
|
|
|
48 lem21 .(node key value leaf leaf) (t-single key value) () (rbr-flip-lr x x₁ x₂ x₃ rbt)
|
|
|
49 lem21 .(node key value leaf leaf) (t-single key value) () (rbr-flip-rl x x₁ x₂ x₃ rbt)
|
|
|
50 lem21 .(node key value leaf leaf) (t-single key value) () (rbr-flip-rr x x₁ x₂ rbt)
|
|
|
51 lem21 .(node key value leaf leaf) (t-single key value) () (rbr-rotate-ll x x₁ rbt)
|
|
|
52 lem21 .(node key value leaf leaf) (t-single key value) () (rbr-rotate-rr x x₁ rbt)
|
|
|
53 lem21 .(node key value leaf leaf) (t-single key value) () (rbr-rotate-lr t₂ t₃ kg kp kn x x₁ x₂ rbt)
|
|
|
54 lem21 .(node key value leaf leaf) (t-single key value) () (rbr-rotate-rl t₂ t₃ kg kp kn x x₁ x₂ rbt)
|
|
|
55 lem21 .(node k₄ _ leaf (node k₃ _ _ _)) (t-right k₄ k₃ x x₁₀ x₂ ti₁) eq rbr-leaf = subst treeInvariant
|
|
|
56 (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-node _ _ k₃ (subst (λ j → key < j) (sym lem23) x₁) x tt tt x₁₀ x₂ (t-single _ _) ti₁ ) where
|
|
|
57 lem23 : k₄ ≡ k
|
|
|
58 lem23 = just-injective (cong node-key eq )
|
|
|
59 lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () rbr-node
|
|
|
60 lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-right x₃ x₄ rbt)
|
|
|
61 lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-left x₃ x₄ rbt)
|
|
|
62 lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-black-right x₃ x₄ rbt)
|
|
|
63 lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-black-left x₃ x₄ rbt)
|
|
|
64 lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-ll x₃ x₄ x₅ rbt)
|
|
|
65 lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-lr x₃ x₄ x₅ x₆ rbt)
|
|
|
66 lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-rl x₃ x₄ x₅ x₆ rbt)
|
|
|
67 lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-rr x₃ x₄ x₅ rbt)
|
|
|
68 lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-rotate-ll x₃ x₄ rbt)
|
|
|
69 lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-rotate-rr x₃ x₄ rbt)
|
|
|
70 lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-rotate-lr t₂ t₃ kg kp kn x₃ x₄ x₅ rbt)
|
|
|
71 lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-rotate-rl t₂ t₃ kg kp kn x₃ x₄ x₅ rbt)
|
|
|
72 lem21 (node k₄ _ (node k₃ _ t₁ t₂) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-node {_} {_} {t₃} {t₄} ) = subst treeInvariant
|
|
|
73 (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left key k₄ (proj1 rr04) (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) lem22 ) where
|
|
|
74 lem23 : k₄ ≡ k
|
|
|
75 lem23 = just-injective (cong node-key eq )
|
|
|
76 rr04 : (key < k₄) ∧ tr< k₄ t₃ ∧ tr< k₄ t₄
|
|
|
77 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
78 lem21 (node k₄ _ (node k₃ _ t₁ t₂) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₁₁ x₃ rbt) = subst treeInvariant
|
|
|
79 (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 rr04) (proj1 (proj2 rr04)) rr02 lem22 ) where
|
|
|
80 lem23 : k₄ ≡ k
|
|
|
81 lem23 = just-injective (cong node-key eq )
|
|
|
82 rr04 : (k₁ < k₄) ∧ tr< k₄ t₄ ∧ tr< k₄ t₅
|
|
|
83 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
84 rr02 : tr< k₄ t₃
|
|
|
85 rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj2 (proj2 rr04))
|
|
|
86 lem21 (node k₄ _ (node k₃ _ t₁ t₂) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-left {k₁} {_} {_} {t₃} {t₄} {t₅} x₁₁ x₃ rbt) = subst treeInvariant
|
|
|
87 (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 rr04) rr02 (proj2 (proj2 rr04)) lem22 ) where
|
|
|
88 lem23 : k₄ ≡ k
|
|
|
89 lem23 = just-injective (cong node-key eq )
|
|
|
90 rr04 : (k₁ < k₄) ∧ tr< k₄ t₄ ∧ tr< k₄ t₅
|
|
|
91 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
92 rr02 : tr< k₄ t₃
|
|
|
93 rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj1 (proj2 rr04))
|
|
|
94 lem21 .(node k₄ _ (node k₃ _ _ _) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂} x₁₁ x₃ rbt) = subst treeInvariant
|
|
|
95 (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 rr04) (proj1 (proj2 rr04)) rr02 lem22 ) where
|
|
|
96 lem23 : k₄ ≡ k
|
|
|
97 lem23 = just-injective (cong node-key eq )
|
|
|
98 rr04 : (k₂ < k₄) ∧ tr< k₄ t₁ ∧ tr< k₄ t₂
|
|
|
99 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
100 rr02 : tr< k₄ t₃
|
|
|
101 rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj2 (proj2 rr04))
|
|
|
102 lem21 .(node k₄ _ (node k₃ _ _ _) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂} x₁₁ x₃ rbt) = subst treeInvariant
|
|
|
103 (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 rr04) rr02 (proj2 (proj2 rr04)) lem22 ) where
|
|
|
104 lem23 : k₄ ≡ k
|
|
|
105 lem23 = just-injective (cong node-key eq )
|
|
|
106 rr04 : (k₂ < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₁
|
|
|
107 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
108 rr02 : tr< k₄ t₃
|
|
|
109 rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj1 (proj2 rr04))
|
|
|
110 lem21 .(node k₄ _ (node k₃ _ _ _) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-flip-ll x₁₁ x₃ x₄ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
111 lem21 .(node k₄ _ (node k₃ _ _ _) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-flip-lr x₁₁ x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
112 lem21 .(node k₄ _ (node k₃ _ _ _) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-flip-rl x₁₁ x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
113 lem21 .(node k₄ _ (node k₃ _ _ _) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-flip-rr x₁₁ x₃ x₄ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
114 lem21 .(node k₄ _ (node k₃ _ _ _) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-rotate-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} x₁₁ x₃ rbt) = subst treeInvariant
|
|
|
115 (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 (proj1 (proj2 rr04))) rr02
|
|
|
116 ⟪ proj1 rr04 , ⟪ proj2 (proj2 (proj1 (proj2 rr04))) , proj2 (proj2 rr04) ⟫ ⟫ lem22 ) where
|
|
|
117 lem23 : k₄ ≡ k
|
|
|
118 lem23 = just-injective (cong node-key eq )
|
|
|
119 rr04 : (kg < k₄) ∧ ((kp < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₁ ) ∧ tr< k₄ uncle
|
|
|
120 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
121 rr02 : tr< k₄ t₃
|
|
|
122 rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj1 (proj2 (proj1 (proj2 rr04))))
|
|
|
123 lem21 .(node k₄ _ (node k₃ _ _ _) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-rotate-rr {t₁} {t₂} {t₃} {uncle} {kg} {kp} x₁₁ x₃ rbt) = subst treeInvariant
|
|
|
124 (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 (proj2 (proj2 rr04)))
|
|
|
125 ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ rr02 lem22 ) where
|
|
|
126 lem23 : k₄ ≡ k
|
|
|
127 lem23 = just-injective (cong node-key eq )
|
|
|
128 rr04 : (kg < k₄) ∧ tr< k₄ uncle ∧ ((kp < k₄) ∧ tr< k₄ t₁ ∧ tr< k₄ t₂)
|
|
|
129 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
130 rr02 : tr< k₄ t₃
|
|
|
131 rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj2 (proj2 (proj2 (proj2 rr04))))
|
|
|
132 lem21 .(node k₄ _ (node k₃ _ _ _) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₁₁ x₃ x₄ rbt) = subst treeInvariant
|
|
|
133 (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 rr02)
|
|
|
134 ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , proj1 (proj2 rr02) ⟫ ⟫ ⟪ proj1 rr04 , ⟪ proj2 (proj2 rr02) , proj2 (proj2 rr04) ⟫ ⟫ lem22 ) where
|
|
|
135 lem23 : k₄ ≡ k
|
|
|
136 lem23 = just-injective (cong node-key eq )
|
|
|
137 rr04 : (kg < k₄) ∧ ((kp < k₄) ∧ tr< k₄ t ∧ tr< k₄ t₁) ∧ tr< k₄ uncle
|
|
|
138 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
139 rr02 : (kn < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₃
|
|
|
140 rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj2 (proj2 (proj1 (proj2 rr04))))
|
|
|
141 lem21 .(node k₄ _ (node k₃ _ _ _) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₁₁ x₃ x₄ rbt) = subst treeInvariant
|
|
|
142 (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 rr02)
|
|
|
143 ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 rr02) ⟫ ⟫ ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj2 (proj2 rr02) , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ lem22 ) where
|
|
|
144 lem23 : k₄ ≡ k
|
|
|
145 lem23 = just-injective (cong node-key eq )
|
|
|
146 rr04 : (kg < k₄) ∧ tr< k₄ uncle ∧ ((kp < k₄) ∧ tr< k₄ t₁ ∧ tr< k₄ t)
|
|
|
147 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
148 rr02 : (kn < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₃
|
|
|
149 rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj1 (proj2 (proj2 (proj2 rr04))))
|
|
|
150 lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-node {_} {_} {t₃} {t₄}) = subst treeInvariant
|
|
|
151 (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) x₁₀ (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) x₄ x₅ lem22 ti₂) where
|
|
|
152 lem23 : k₄ ≡ k
|
|
|
153 lem23 = just-injective (cong node-key eq)
|
|
|
154 rr04 : (key < k₄) ∧ tr< k₄ t₃ ∧ tr< k₄ t₄
|
|
|
155 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
156 lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₁₁ x₆ rbt) = subst treeInvariant
|
|
|
157 (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) x₁₀ (proj1 (proj2 rr04)) rr02 x₄ x₅ lem22 ti₂) where
|
|
|
158 lem23 : k₄ ≡ k
|
|
|
159 lem23 = just-injective (cong node-key eq)
|
|
|
160 rr04 : (k₁ < k₄) ∧ tr< k₄ t₄ ∧ tr< k₄ t₅
|
|
|
161 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
162 rr02 : tr< k₄ t₃
|
|
|
163 rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj2 (proj2 rr04))
|
|
|
164 lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-left {k₁} {_} {_} {t₃} {t₄} {t₅} x₁₁ x₆ rbt) = subst treeInvariant
|
|
|
165 (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) x₁₀ rr02 (proj2 (proj2 rr04)) x₄ x₅ lem22 ti₂) where
|
|
|
166 lem23 : k₄ ≡ k
|
|
|
167 lem23 = just-injective (cong node-key eq)
|
|
|
168 rr04 : (k₁ < k₄) ∧ tr< k₄ t₄ ∧ tr< k₄ t₅
|
|
|
169 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
170 rr02 : tr< k₄ t₃
|
|
|
171 rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj1 (proj2 rr04))
|
|
|
172 lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂} x₁₁ x₆ rbt) = subst treeInvariant
|
|
|
173 (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) x₁₀ (proj1 (proj2 rr04)) rr02 x₄ x₅ lem22 ti₂) where
|
|
|
174 lem23 : k₄ ≡ k
|
|
|
175 lem23 = just-injective (cong node-key eq)
|
|
|
176 rr04 : (k₂ < k₄) ∧ tr< k₄ t₁ ∧ tr< k₄ t₂
|
|
|
177 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
178 rr02 : tr< k₄ t₃
|
|
|
179 rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj2 (proj2 rr04))
|
|
|
180 lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂} x₁₁ x₆ rbt) = subst treeInvariant
|
|
|
181 (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) x₁₀ rr02 (proj2 (proj2 rr04)) x₄ x₅ lem22 ti₂) where
|
|
|
182 lem23 : k₄ ≡ k
|
|
|
183 lem23 = just-injective (cong node-key eq)
|
|
|
184 rr04 : (k₂ < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₁
|
|
|
185 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
186 rr02 : tr< k₄ t₃
|
|
|
187 rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj1 (proj2 rr04))
|
|
|
188 lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-ll x₁ x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
189 lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-rr x₁ x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
190 lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-rl x₁ x₆ x₇ x₈ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
191 lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-lr x₁ x₆ x₇ x₈ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
192 lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} x₁₁ x₆ rbt) = subst treeInvariant
|
|
|
193 (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 (proj1 (proj2 rr04))) x₁₀ rr02
|
|
|
194 ⟪ proj1 rr04 , ⟪ proj2 (proj2 (proj1 (proj2 rr04))) , proj2 (proj2 rr04) ⟫ ⟫ x₄ x₅ lem22 ti₂) where
|
|
|
195 lem23 : k₄ ≡ k
|
|
|
196 lem23 = just-injective (cong node-key eq)
|
|
|
197 rr04 : (kg < k₄) ∧ ((kp < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₁) ∧ tr< k₄ uncle
|
|
|
198 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
199 rr02 : tr< k₄ t₃
|
|
|
200 rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj1 (proj2 (proj1 (proj2 rr04))))
|
|
|
201 lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-rr {t₁} {t₂} {t₃} {uncle} {kg} {kp} x₁₁ x₆ rbt) = subst treeInvariant
|
|
|
202 (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 (proj2 (proj2 rr04))) x₁₀
|
|
|
203 ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ rr02 x₄ x₅ lem22 ti₂) where
|
|
|
204 lem23 : k₄ ≡ k
|
|
|
205 lem23 = just-injective (cong node-key eq)
|
|
|
206 rr04 : (kg < k₄) ∧ tr< k₄ uncle ∧ ((kp < k₄) ∧ tr< k₄ t₁ ∧ tr< k₄ t₂)
|
|
|
207 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
208 rr02 : tr< k₄ t₃
|
|
|
209 rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj2 (proj2 (proj2 (proj2 rr04))))
|
|
|
210 lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₁₁ x₆ x₇ rbt) = subst treeInvariant
|
|
|
211 (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr02) x₁₀
|
|
|
212 ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , proj1 (proj2 rr02) ⟫ ⟫ ⟪ proj1 rr04 , ⟪ proj2 (proj2 rr02) , proj2 (proj2 rr04) ⟫ ⟫
|
|
|
213 x₄ x₅ lem22 ti₂) where
|
|
|
214 lem23 : k₄ ≡ k
|
|
|
215 lem23 = just-injective (cong node-key eq)
|
|
|
216 rr04 : (kg < k₄) ∧ ((kp < k₄) ∧ tr< k₄ t ∧ tr< k₄ t₁) ∧ tr< k₄ uncle
|
|
|
217 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
218 rr02 : (kn < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₃
|
|
|
219 rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj2 (proj2 (proj1 (proj2 rr04))))
|
|
|
220 lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₁₁ x₆ x₇ rbt) = subst treeInvariant
|
|
|
221 (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr02) x₁₀
|
|
|
222 ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 rr02) ⟫ ⟫ ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj2 (proj2 rr02) , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫
|
|
|
223 x₄ x₅ lem22 ti₂) where
|
|
|
224 lem23 : k₄ ≡ k
|
|
|
225 lem23 = just-injective (cong node-key eq)
|
|
|
226 rr04 : (kg < k₄) ∧ tr< k₄ uncle ∧ ((kp < k₄) ∧ tr< k₄ t₁ ∧ tr< k₄ t)
|
|
|
227 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
228 rr02 : (kn < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₃
|
|
|
229 rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj1 (proj2 (proj2 (proj2 rr04))))
|
|
|
230
|
|
|
231 RB-repl→ti-lem04 : {n : Level} {A : Set n} {key : ℕ} {value : A} {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} (x : color t₂ ≡ Red) (x₁ : key₁ < key)
|
|
|
232 (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁)
|
|
|
233 → treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₂)
|
|
|
234 RB-repl→ti-lem04 {n} {A} {key} {value} {t} {t1} {t2} {v1} {k} ceq x₁ rbt prev ti = lem21 (node k ⟪ Black , v1 ⟫ t t1) ti refl rbt where
|
|
|
235 lem22 : treeInvariant t2
|
|
|
236 lem22 = prev (treeRightDown _ _ ti)
|
|
|
237 lem21 : (tree : bt (Color ∧ A)) → treeInvariant tree → tree ≡ node k ⟪ Black , v1 ⟫ t t1 → replacedRBTree key value t1 t2 → treeInvariant (node k ⟪ Black , v1 ⟫ t t2)
|
|
|
238 lem21 _ t-leaf () rbt
|
|
|
239 lem21 _ (t-single key value) eq rbr-leaf = subst treeInvariant (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ x₁ _ _ lem22)
|
|
|
240 lem21 _ (t-single key value) () (rbr-node {_} {_} {t₃} {t₄})
|
|
|
241 lem21 _ (t-single key value) () (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt)
|
|
|
242 lem21 _ (t-single key value) () (rbr-left {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt)
|
|
|
243 lem21 _ (t-single key value) () (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt)
|
|
|
244 lem21 _ (t-single key value) () (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt)
|
|
|
245 lem21 _ (t-single key value) () (rbr-flip-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt)
|
|
|
246 lem21 _ (t-single key value) () (rbr-flip-lr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt)
|
|
|
247 lem21 _ (t-single key value) () (rbr-flip-rl {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt)
|
|
|
248 lem21 _ (t-single key value) () (rbr-flip-rr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt)
|
|
|
249 lem21 _ (t-single key value) () (rbr-rotate-ll {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt)
|
|
|
250 lem21 _ (t-single key value) () (rbr-rotate-rr {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt)
|
|
|
251 lem21 _ (t-single key value) () (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt)
|
|
|
252 lem21 _ (t-single key value) () (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt)
|
|
|
253 lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) () rbr-leaf
|
|
|
254 lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-node {_} {_} {t₃} {t₄}) = subst treeInvariant
|
|
|
255 (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ x₁ (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) lem22) where
|
|
|
256 rr04 : (k < _ ) ∧ tr> k t₃ ∧ tr> k t₄
|
|
|
257 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
258 lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) = subst treeInvariant
|
|
|
259 (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04) (proj1 (proj2 rr04)) rr02 lem22) where
|
|
|
260 rr04 : (k < k₁ ) ∧ tr> k t₄ ∧ tr> k t₅
|
|
|
261 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
262 rr02 : tr> k t₃
|
|
|
263 rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 rr04))
|
|
|
264 lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-left {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) = subst treeInvariant
|
|
|
265 (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04) rr02 (proj2 (proj2 rr04)) lem22) where
|
|
|
266 rr04 : (k < k₁) ∧ tr> k t₄ ∧ tr> k t₅
|
|
|
267 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
268 rr02 : tr> k t₃
|
|
|
269 rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 rr04))
|
|
|
270 lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt) = subst treeInvariant
|
|
|
271 (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04) (proj1 (proj2 rr04)) rr02 lem22) where
|
|
|
272 rr04 : (k < k₂) ∧ tr> k t₁ ∧ tr> k t₂
|
|
|
273 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
274 rr02 : tr> k t₃
|
|
|
275 rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 rr04))
|
|
|
276 lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt) = subst treeInvariant
|
|
|
277 (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04) rr02 (proj2 (proj2 rr04)) lem22) where
|
|
|
278 rr04 : (k < k₂) ∧ tr> k t₂ ∧ tr> k t₁
|
|
|
279 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
280 rr02 : tr> k t₃
|
|
|
281 rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 rr04))
|
|
|
282 lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-flip-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) = subst treeInvariant
|
|
|
283 (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04)
|
|
|
284 ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ rr02 , proj2 (proj2 (proj1 (proj2 rr04))) ⟫ ⟫ (tr>-to-black (proj2 (proj2 rr04))) lem22) where
|
|
|
285 rr04 : (k < kg) ∧ ((k < kp) ∧ tr> k t₂ ∧ tr> k t₁) ∧ tr> k uncle
|
|
|
286 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
287 rr02 : tr> k t₃
|
|
|
288 rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj1 (proj2 rr04))) )
|
|
|
289 lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-flip-lr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt) = subst treeInvariant
|
|
|
290 (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04)
|
|
|
291 ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , rr02 ⟫ ⟫ (tr>-to-black (proj2 (proj2 rr04))) lem22) where
|
|
|
292 rr04 : (k < kg) ∧ ((k < kp) ∧ tr> k t₁ ∧ tr> k t₂) ∧ tr> k uncle
|
|
|
293 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
294 rr02 : tr> k t₃
|
|
|
295 rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj1 (proj2 rr04))))
|
|
|
296 lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-flip-rl {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt) = subst treeInvariant
|
|
|
297 (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04)
|
|
|
298 (tr>-to-black (proj1 (proj2 rr04))) ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ rr02 , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ lem22) where
|
|
|
299 rr04 : (k < kg) ∧ tr> k uncle ∧ ((k < kp) ∧ tr> k t₂ ∧ tr> k t₁)
|
|
|
300 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
301 rr02 : tr> k t₃
|
|
|
302 rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj2 (proj2 rr04))) )
|
|
|
303 lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-flip-rr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) = subst treeInvariant
|
|
|
304 (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04)
|
|
|
305 (tr>-to-black (proj1 (proj2 rr04))) ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj1 (proj2 (proj2 (proj2 rr04))) , rr02 ⟫ ⟫ lem22) where
|
|
|
306 rr04 : (k < kg) ∧ tr> k uncle ∧ ((k < kp) ∧ tr> k t₁ ∧ tr> k t₂)
|
|
|
307 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
308 rr02 : tr> k t₃
|
|
|
309 rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj2 (proj2 rr04))) )
|
|
|
310 lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-ll {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
311 lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-rr {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
312 lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
313 lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
314 lem21 _ (t-left key₂ key₁ {_} {_} {t} {t₁} x x₁₀ x₂ ti₁) eq rbr-leaf = subst treeInvariant (node-cong refl refl (just-injective (cong node-left eq)) refl)
|
|
|
315 (t-node _ _ _ (subst (λ j → key₂ < j ) lem23 x) x₁ (subst (λ k → tr< k t) lem23 x₁₀) (subst (λ k → tr< k t₁) lem23 x₂) tt tt ti₁ lem22) where
|
|
|
316 lem23 : key₁ ≡ k
|
|
|
317 lem23 = just-injective (cong node-key eq)
|
|
|
318 lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) eq (rbr-node {_} {_} {t₃} {t₄}) = subst treeInvariant
|
|
|
319 (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₂ < j ) lem23 x) x₁
|
|
|
320 (subst (λ k → tr< k t₁) lem23 x₁₀) (subst (λ k → tr< k t₂) lem23 x₂) (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) ti₁ lem22) where
|
|
|
321 lem23 : key₁ ≡ k
|
|
|
322 lem23 = just-injective (cong node-key eq)
|
|
|
323 rr04 : (k < key) ∧ tr> k t₃ ∧ tr> k t₄
|
|
|
324 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
325 lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) () (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt)
|
|
|
326 lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) () (rbr-left {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt)
|
|
|
327 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) () (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt)
|
|
|
328 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) () (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt)
|
|
|
329 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) () (rbr-flip-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt)
|
|
|
330 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) () (rbr-flip-lr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt)
|
|
|
331 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) () (rbr-flip-rl {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt)
|
|
|
332 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) () (rbr-flip-rr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt)
|
|
|
333 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-ll {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
334 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-rr {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
335 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
336 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
337 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) () rbr-leaf
|
|
|
338 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-node {_} {_} {t₃} {t₄}) = subst treeInvariant
|
|
|
339 (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) x₁
|
|
|
340 (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃) (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) ti₁ lem22) where
|
|
|
341 lem23 : key₁ ≡ k
|
|
|
342 lem23 = just-injective (cong node-key eq)
|
|
|
343 rr04 : (k < key ) ∧ tr> k t₃ ∧ tr> k t₄
|
|
|
344 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
345 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-right {k₃} {_} {_} {t₃} {t₄} {t₅} x₆ x₇ rbt) = subst treeInvariant
|
|
|
346 (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) (proj1 rr04)
|
|
|
347 (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃) (proj1 (proj2 rr04)) rr02 ti₁ lem22) where
|
|
|
348 lem23 : key₁ ≡ k
|
|
|
349 lem23 = just-injective (cong node-key eq)
|
|
|
350 rr04 : (k < k₃) ∧ tr> k t₄ ∧ tr> k t₅
|
|
|
351 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
352 rr02 : tr> k t₃
|
|
|
353 rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 rr04))
|
|
|
354 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-left {k₃} {_} {_} {t₃} {t₄} {t₅} x₆ x₇ rbt) = subst treeInvariant
|
|
|
355 (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) (proj1 rr04)
|
|
|
356 (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃) rr02 (proj2 (proj2 rr04)) ti₁ lem22) where
|
|
|
357 lem23 : key₁ ≡ k
|
|
|
358 lem23 = just-injective (cong node-key eq)
|
|
|
359 rr04 : (k < k₃) ∧ tr> k t₄ ∧ tr> k t₅
|
|
|
360 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
361 rr02 : tr> k t₃
|
|
|
362 rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 rr04))
|
|
|
363 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-black-right {t₃} {t₄} {t₅} x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
364 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-black-left {t₃} {t₄} {t₅} x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
365 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-ll {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x₆ x₇ x₈ rbt)
|
|
|
366 = subst treeInvariant
|
|
|
367 (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) (proj1 rr04)
|
|
|
368 (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃)
|
|
|
369 ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ rr02 , proj2 (proj2 (proj1 (proj2 rr04))) ⟫ ⟫ ( tr>-to-black (proj2 (proj2 rr04))) ti₁ lem22) where
|
|
|
370 lem23 : key₁ ≡ k
|
|
|
371 lem23 = just-injective (cong node-key eq)
|
|
|
372 rr04 : (k < kg) ∧ ((k < kp) ∧ tr> k t₁ ∧ tr> k t) ∧ tr> k uncle
|
|
|
373 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
374 rr02 : tr> k t₂
|
|
|
375 rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj1 (proj2 rr04))) )
|
|
|
376 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-lr {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x₆ x₇ x₈ x₉ rbt)
|
|
|
377 = subst treeInvariant
|
|
|
378 (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) (proj1 rr04)
|
|
|
379 (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃)
|
|
|
380 ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , rr02 ⟫ ⟫ ( tr>-to-black (proj2 (proj2 rr04))) ti₁ lem22) where
|
|
|
381 lem23 : key₁ ≡ k
|
|
|
382 lem23 = just-injective (cong node-key eq)
|
|
|
383 rr04 : (k < kg) ∧ ((k < kp) ∧ tr> k t ∧ tr> k t₁) ∧ tr> k uncle
|
|
|
384 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
385 rr02 : tr> k t₂
|
|
|
386 rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj1 (proj2 rr04))) )
|
|
|
387 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-rl {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x₆ x₇ x₈ x₉ rbt)
|
|
|
388 = subst treeInvariant
|
|
|
389 (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) (proj1 rr04)
|
|
|
390 (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃)
|
|
|
391 (tr>-to-black (proj1 (proj2 rr04))) ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ rr02 , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ ti₁ lem22) where
|
|
|
392 lem23 : key₁ ≡ k
|
|
|
393 lem23 = just-injective (cong node-key eq)
|
|
|
394 rr04 : (k < kg) ∧ tr> k uncle ∧ ((k < kp) ∧ tr> k t₁ ∧ tr> k t)
|
|
|
395 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
396 rr02 : tr> k t₂
|
|
|
397 rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj2 (proj2 rr04))) )
|
|
|
398 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-rr {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x₆ x₇ x₈ rbt)
|
|
|
399 = subst treeInvariant
|
|
|
400 (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) (proj1 rr04)
|
|
|
401 (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃)
|
|
|
402 (tr>-to-black (proj1 (proj2 rr04))) ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj1 (proj2 (proj2 (proj2 rr04))) , rr02 ⟫ ⟫ ti₁ lem22) where
|
|
|
403 lem23 : key₁ ≡ k
|
|
|
404 lem23 = just-injective (cong node-key eq)
|
|
|
405 rr04 : (k < kg) ∧ tr> k uncle ∧ ((k < kp) ∧ tr> k t ∧ tr> k t₁)
|
|
|
406 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
407 rr02 : tr> k t₂
|
|
|
408 rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj2 (proj2 rr04))) )
|
|
|
409 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-rr x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
410 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-ll x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
411 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₆ x₇ x₈ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
412 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₆ x₇ x₈ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
413
|
|
|
414 RB-repl→ti-lem05 : {n : Level} {A : Set n} {key : ℕ} {value : A} {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} (x : color t₂ ≡ Red) (x₁ : key < key₁)
|
|
|
415 (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t₁ t)
|
|
|
416 → treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t₂ t)
|
|
|
417 RB-repl→ti-lem05 {n} {A} {key} {value} {t} {t1} {t2} {v1} {k} ceq x₁ rbt prev ti = lem21 (node k ⟪ Black , v1 ⟫ t1 t) ti refl rbt where
|
|
|
418 lem22 : treeInvariant t2
|
|
|
419 lem22 = prev (treeLeftDown _ _ ti )
|
|
|
420 lem21 : (tree : bt (Color ∧ A)) → treeInvariant tree → tree ≡ node k ⟪ Black , v1 ⟫ t1 t → replacedRBTree key value t1 t2 → treeInvariant (node k ⟪ Black , v1 ⟫ t2 t)
|
|
|
421 lem21 _ t-leaf () rbt
|
|
|
422 lem21 _ (t-single key value) eq rbr-leaf = subst treeInvariant (node-cong refl refl refl (just-injective (cong node-right eq)) ) (t-left _ _ x₁ _ _ lem22)
|
|
|
423 lem21 _ (t-single key value) () (rbr-node {_} {_} {t₃} {t₄})
|
|
|
424 lem21 _ (t-single key value) () (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt)
|
|
|
425 lem21 _ (t-single key value) () (rbr-left {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt)
|
|
|
426 lem21 _ (t-single key value) () (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt)
|
|
|
427 lem21 _ (t-single key value) () (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt)
|
|
|
428 lem21 _ (t-single key value) () (rbr-flip-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt)
|
|
|
429 lem21 _ (t-single key value) () (rbr-flip-lr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt)
|
|
|
430 lem21 _ (t-single key value) () (rbr-flip-rl {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt)
|
|
|
431 lem21 _ (t-single key value) () (rbr-flip-rr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt)
|
|
|
432 lem21 _ (t-single key value) () (rbr-rotate-ll {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt)
|
|
|
433 lem21 _ (t-single key value) () (rbr-rotate-rr {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt)
|
|
|
434 lem21 _ (t-single key value) () (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt)
|
|
|
435 lem21 _ (t-single key value) () (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt)
|
|
|
436 lem21 _ (t-right key₂ key₁ {v1} {v2} {t} {t₁} x x₁₀ x₂ ti₁) eq rbr-leaf = subst treeInvariant (node-cong refl refl refl (just-injective (cong node-right eq)) )
|
|
|
437 (t-node _ _ _ x₁ (subst (λ j → j < key₁) lem23 x) tt tt (subst (λ k → tr> k t) lem23 x₁₀ ) (subst (λ k → tr> k t₁) lem23 x₂ ) (t-single _ _) ti₁) where
|
|
|
438 lem23 : key₂ ≡ k
|
|
|
439 lem23 = just-injective (cong node-key eq)
|
|
|
440 lem21 _ (t-right key₂ key₁ {v1} {v2} {t} {t₁} x x₁₀ x₂ ti₁) () (rbr-node {_} {_} {t₃} {t₄})
|
|
|
441 lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt)
|
|
|
442 lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-left {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt)
|
|
|
443 lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt)
|
|
|
444 lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt)
|
|
|
445 lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt)
|
|
|
446 lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-lr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt)
|
|
|
447 lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-rl {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt)
|
|
|
448 lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-rr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt)
|
|
|
449 lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-ll {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
450 lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-rr {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
451 lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
452 lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
453 lem21 _ (t-left key₂ key₁ {_} {_} {t} {t₁} x x₁₀ x₂ ti₁) () rbr-leaf
|
|
|
454 lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) eq (rbr-node {_} {_} {t₃} {t₄}) = subst treeInvariant
|
|
|
455 (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) lem22 ) where
|
|
|
456 rr04 : (key < k) ∧ tr< k t₃ ∧ tr< k t₄
|
|
|
457 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
458 lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) eq (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) = subst treeInvariant
|
|
|
459 (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) rr02 lem22 ) where
|
|
|
460 rr04 : (k₁ < k) ∧ tr< k t₄ ∧ tr< k t₅
|
|
|
461 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
462 rr02 : tr< k t₃
|
|
|
463 rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 rr04))
|
|
|
464 lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) eq (rbr-left {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) = subst treeInvariant
|
|
|
465 (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) rr02 (proj2 (proj2 rr04)) lem22 ) where
|
|
|
466 rr04 : (k₁ < k) ∧ tr< k t₄ ∧ tr< k t₅
|
|
|
467 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
468 rr02 : tr< k t₃
|
|
|
469 rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 rr04))
|
|
|
470 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
471 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
472 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-flip-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) = subst treeInvariant
|
|
|
473 (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) ⟪ proj1 (proj1 (proj2 rr04)) ,
|
|
|
474 ⟪ rr02 , proj2 (proj2 (proj1 (proj2 rr04))) ⟫ ⟫ (tr<-to-black (proj2 (proj2 rr04))) lem22 ) where
|
|
|
475 rr04 : (kg < k) ∧ ((kp < k) ∧ tr< k t₂ ∧ tr< k t₁) ∧ tr< k uncle
|
|
|
476 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
477 rr02 : tr< k t₃
|
|
|
478 rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj1 (proj2 rr04))) )
|
|
|
479 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-flip-lr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt) = subst treeInvariant
|
|
|
480 (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) ⟪ proj1 (proj1 (proj2 rr04)) ,
|
|
|
481 ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , rr02 ⟫ ⟫ (tr<-to-black (proj2 (proj2 rr04))) lem22 ) where
|
|
|
482 rr04 : (kg < k) ∧ ((kp < k) ∧ tr< k t₁ ∧ tr< k t₂) ∧ tr< k uncle
|
|
|
483 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
484 rr02 : tr< k t₃
|
|
|
485 rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj1 (proj2 rr04))) )
|
|
|
486 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-flip-rl {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt) = subst treeInvariant
|
|
|
487 (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) (tr<-to-black (proj1 (proj2 rr04)))
|
|
|
488 ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ rr02 , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ lem22 ) where
|
|
|
489 rr04 : (kg < k) ∧ tr< k uncle ∧ ((kp < k) ∧ tr< k t₂ ∧ tr< k t₁)
|
|
|
490 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
491 rr02 : tr< k t₃
|
|
|
492 rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj2 (proj2 rr04))) )
|
|
|
493 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-flip-rr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) = subst treeInvariant
|
|
|
494 (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) (tr<-to-black (proj1 (proj2 rr04)))
|
|
|
495 ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj1 (proj2 (proj2 (proj2 rr04))) , rr02 ⟫ ⟫ lem22 ) where
|
|
|
496 rr04 : (kg < k) ∧ tr< k uncle ∧ ((kp < k) ∧ tr< k t₁ ∧ tr< k t₂)
|
|
|
497 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
498 rr02 : tr< k t₃
|
|
|
499 rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj2 (proj2 rr04))) )
|
|
|
500 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-ll {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
501 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-rr {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
502 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
503 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
504 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) () rbr-leaf
|
|
|
505 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-node {_} {_} {t₃} {t₄}) = subst treeInvariant
|
|
|
506 (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀)
|
|
|
507 (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) (subst (λ j → tr> j t₁₀) lem23 x₄) (subst (λ j → tr> j t₁₁) lem23 x₅) lem22 ti₂) where
|
|
|
508 lem23 : key₁ ≡ k
|
|
|
509 lem23 = just-injective (cong node-key eq)
|
|
|
510 rr04 : (key < k) ∧ tr< k t₃ ∧ tr< k t₄
|
|
|
511 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
512 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-right {k₃} {_} {_} {t₃} {t₄} {t₅} x₆ x₇ rbt) = subst treeInvariant
|
|
|
513 (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀)
|
|
|
514 (proj1 (proj2 rr04)) rr02 (subst (λ k → tr> k t₉) lem23 x₄) (subst (λ k → tr> k t₁₀) lem23 x₅) lem22 ti₂) where
|
|
|
515 lem23 : key₁ ≡ k
|
|
|
516 lem23 = just-injective (cong node-key eq)
|
|
|
517 rr04 : (k₃ < k) ∧ tr< k t₄ ∧ tr< k t₅
|
|
|
518 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
519 rr02 : tr< k t₃
|
|
|
520 rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 rr04))
|
|
|
521 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-left {k₃} {_} {_} {t₃} {t₄} {t₅} x₆ x₇ rbt) = subst treeInvariant
|
|
|
522 (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀)
|
|
|
523 rr02 (proj2 (proj2 rr04)) (subst (λ k → tr> k t₉) lem23 x₄) (subst (λ k → tr> k t₁₀) lem23 x₅) lem22 ti₂) where
|
|
|
524 lem23 : key₁ ≡ k
|
|
|
525 lem23 = just-injective (cong node-key eq)
|
|
|
526 rr04 : (k₃ < k) ∧ tr< k t₄ ∧ tr< k t₅
|
|
|
527 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
528 rr02 : tr< k t₃
|
|
|
529 rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 rr04))
|
|
|
530 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-black-right {t₃} {t₄} {t₅} x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
531 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-black-left {t₃} {t₄} {t₅} x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
532 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-ll {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x₆ x₇ x₈ rbt)
|
|
|
533 = subst treeInvariant
|
|
|
534 (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀)
|
|
|
535 ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ rr02 , proj2 (proj2 (proj1 (proj2 rr04))) ⟫ ⟫ (tr<-to-black (proj2 (proj2 rr04))) (subst (λ k → tr> k t₉) lem23 x₄) (subst (λ k → tr> k t₁₀) lem23 x₅) lem22 ti₂) where
|
|
|
536 lem23 : key₁ ≡ k
|
|
|
537 lem23 = just-injective (cong node-key eq)
|
|
|
538 rr04 : (kg < k) ∧ ((kp < k) ∧ tr< k t₁ ∧ tr< k t) ∧ tr< k uncle
|
|
|
539 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
540 rr02 : tr< k t₂
|
|
|
541 rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj1 (proj2 rr04))) )
|
|
|
542 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-lr {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x₆ x₇ x₈ x₉ rbt)
|
|
|
543 = subst treeInvariant
|
|
|
544 (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀)
|
|
|
545 ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , rr02 ⟫ ⟫ (tr<-to-black (proj2 (proj2 rr04))) (subst (λ k → tr> k t₉) lem23 x₄) (subst (λ k → tr> k t₁₀) lem23 x₅) lem22 ti₂) where
|
|
|
546 lem23 : key₁ ≡ k
|
|
|
547 lem23 = just-injective (cong node-key eq)
|
|
|
548 rr04 : (kg < k) ∧ ((kp < k) ∧ tr< k t ∧ tr< k t₁) ∧ tr< k uncle
|
|
|
549 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
550 rr02 : tr< k t₂
|
|
|
551 rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj1 (proj2 rr04))) )
|
|
|
552 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-rl {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x₆ x₇ x₈ x₉ rbt)
|
|
|
553 = subst treeInvariant
|
|
|
554 (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀)
|
|
|
555 (tr<-to-black (proj1 (proj2 rr04))) ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ rr02 , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ (subst (λ k → tr> k t₉) lem23 x₄) (subst (λ k → tr> k t₁₀) lem23 x₅) lem22 ti₂) where
|
|
|
556 lem23 : key₁ ≡ k
|
|
|
557 lem23 = just-injective (cong node-key eq)
|
|
|
558 rr04 : (kg < k) ∧ tr< k uncle ∧ ((kp < k) ∧ tr< k t₁ ∧ tr< k t)
|
|
|
559 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
560 rr02 : tr< k t₂
|
|
|
561 rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj2 (proj2 rr04))) )
|
|
|
562 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-rr {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x₆ x₇ x₈ rbt)
|
|
|
563 = subst treeInvariant
|
|
|
564 (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀)
|
|
|
565 (tr<-to-black (proj1 (proj2 rr04))) ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj1 (proj2 (proj2 (proj2 rr04))) , rr02 ⟫ ⟫ (subst (λ k → tr> k t₉) lem23 x₄) (subst (λ k → tr> k t₁₀) lem23 x₅) lem22 ti₂) where
|
|
|
566 lem23 : key₁ ≡ k
|
|
|
567 lem23 = just-injective (cong node-key eq)
|
|
|
568 rr04 : (kg < k) ∧ tr< k uncle ∧ ((kp < k) ∧ tr< k t ∧ tr< k t₁)
|
|
|
569 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
570 rr02 : tr< k t₂
|
|
|
571 rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj2 (proj2 rr04))) )
|
|
|
572 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-rr x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
573 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-ll x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
574 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₆ x₇ x₈ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
575 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₆ x₇ x₈ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
576
|
|
|
577
|
|
|
578
|
|
|
579 to-black-treeInvariant : {n : Level} {A : Set n} → (t : bt (Color ∧ A) ) → treeInvariant t → treeInvariant (to-black t)
|
|
|
580 to-black-treeInvariant {n} {A} .leaf t-leaf = t-leaf
|
|
|
581 to-black-treeInvariant {n} {A} .(node key value leaf leaf) (t-single key value) = t-single key _
|
|
|
582 to-black-treeInvariant {n} {A} .(node key _ leaf (node key₁ _ _ _)) (t-right key key₁ x x₁ x₂ ti) = t-right key key₁ x x₁ x₂ ti
|
|
|
583 to-black-treeInvariant {n} {A} .(node key₁ _ (node key _ _ _) leaf) (t-left key key₁ x x₁ x₂ ti) = t-left key key₁ x x₁ x₂ ti
|
|
|
584 to-black-treeInvariant {n} {A} .(node key₁ _ (node key _ _ _) (node key₂ _ _ _)) (t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) = t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁
|
|
|
585
|
|
|
586 RB→t2notLeaf : {n : Level} {A : Set n} {key : ℕ} {value : A} → (t₁ t₂ : bt (Color ∧ A) ) → (rbt : replacedRBTree key value t₁ t₂) → IsNode t₂
|
|
|
587 RB→t2notLeaf {n} {A} {k} {v} .leaf .(node k ⟪ Red , v ⟫ leaf leaf) rbr-leaf = record { key = k ; value = ⟪ Red , v ⟫ ; left = leaf ; right = leaf ; t=node = refl }
|
|
|
588 RB→t2notLeaf {n} {A} {k} {v} .(node k ⟪ _ , _ ⟫ _ _) .(node k ⟪ _ , v ⟫ _ _) rbr-node = record { key = k ; value = ⟪ _ , v ⟫ ; left = _ ; right = _ ; t=node = refl }
|
|
|
589 RB→t2notLeaf {n} {A} {k} {v} .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) (rbr-right x x₁ rbt) = record { key = _ ; value = _ ; left = _ ; right = _; t=node = refl }
|
|
|
590 RB→t2notLeaf {n} {A} {k} {v} .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) (rbr-left x x₁ rbt) = record { key = _ ; value = _ ; left = _ ; right = _; t=node = refl }
|
|
|
591 RB→t2notLeaf {n} {A} {k} {v} .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) (rbr-black-right x x₁ rbt) = record { key = _ ; value = _ ; left = _ ; right = _; t=node = refl }
|
|
|
592 RB→t2notLeaf {n} {A} {k} {v} .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) (rbr-black-left x x₁ rbt) = record { key = _ ; value = _ ; left = _ ; right = _; t=node = refl }
|
|
|
593 RB→t2notLeaf {n} {A} {k} {v} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) (rbr-flip-ll x x₁ x₂ rbt) = record { key = _ ; value = _ ; left = _ ; right = _; t=node = refl }
|
|
|
594 RB→t2notLeaf {n} {A} {k} {v} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) (rbr-flip-lr x x₁ x₂ x₃ rbt) = record { key = _ ; value = _ ; left = _ ; right = _; t=node = refl }
|
|
|
595 RB→t2notLeaf {n} {A} {k} {v} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) (rbr-flip-rl x x₁ x₂ x₃ rbt) = record { key = _ ; value = _ ; left = _ ; right = _; t=node = refl }
|
|
|
596 RB→t2notLeaf {n} {A} {k} {v} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) (rbr-flip-rr x x₁ x₂ rbt) = record { key = _ ; value = _ ; left = _ ; right = _; t=node = refl }
|
|
|
597 RB→t2notLeaf {n} {A} {k} {v} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) (rbr-rotate-ll x x₁ rbt) = record { key = _ ; value = _ ; left = _ ; right = _; t=node = refl }
|
|
|
598 RB→t2notLeaf {n} {A} {k} {v} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) (rbr-rotate-rr x x₁ rbt) = record { key = _ ; value = _ ; left = _ ; right = _; t=node = refl }
|
|
|
599 RB→t2notLeaf {n} {A} {k} {v} .(node kg ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ _) _) .(node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₂) (node kg ⟪ Red , _ ⟫ t₃ _)) (rbr-rotate-lr t₂ t₃ kg kp kn x x₁ x₂ rbt) = record { key = kn ; value = ⟪ Black , _ ⟫ ; left = _ ; right = _; t=node = refl }
|
|
|
600 RB→t2notLeaf {n} {A} {k} {v} .(node kg ⟪ Black , _ ⟫ _ (node kp ⟪ Red , _ ⟫ _ _)) .(node kn ⟪ Black , _ ⟫ (node kg ⟪ Red , _ ⟫ _ t₂) (node kp ⟪ Red , _ ⟫ t₃ _)) (rbr-rotate-rl t₂ t₃ kg kp kn x x₁ x₂ rbt) = record { key = kn ; value = ⟪ Black , _ ⟫ ; left = _ ; right = _; t=node = refl }
|
|
|
601
|
|
|
602
|
|
|
603 RB-repl→ti-lem06 : {n : Level} {A : Set n} {key : ℕ} {value : A} {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red)
|
|
|
604 (x₁ : color uncle ≡ Red) (x₂ : key < kp) (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂)
|
|
|
605 → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₁ t) uncle)
|
|
|
606 → treeInvariant (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t₂ t) (to-black uncle))
|
|
|
607 RB-repl→ti-lem06 {n} {A} {key} {value} {t} {t1} {t2} {uncle} {kg} {kp} {vg} {vp} ceq ueq x₁ rbt prev ti
|
|
|
608 = lem21 (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t1 t) uncle) ti refl rbt where
|
|
|
609 lem22 : treeInvariant t2
|
|
|
610 lem22 = prev (treeLeftDown _ _ (treeLeftDown _ _ ti ))
|
|
|
611 lem25 : treeInvariant t
|
|
|
612 lem25 = treeRightDown _ _ (treeLeftDown _ _ ti)
|
|
|
613 lem21 : (tree : bt (Color ∧ A)) → treeInvariant tree → tree ≡ (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t1 t) uncle) → replacedRBTree key value t1 t2
|
|
|
614 → treeInvariant (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t2 t) (to-black uncle))
|
|
|
615 lem21 _ t-leaf () rbt
|
|
|
616 lem21 _ (t-single key value) () _
|
|
|
617 lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) () _
|
|
|
618 lem21 _ (t-left key₂ key₁ {_} {_} {t} {t₁} x x₁₀ x₂ ti₁) eq rbr-leaf = subst treeInvariant (node-cong refl refl refl (subst (λ k → leaf ≡ to-black k ) lem24 refl) )
|
|
|
619 (t-left _ _ (proj1 rr04) ⟪ rr07 , ⟪ tt , tt ⟫ ⟫ (proj2 (proj2 rr04)) (subst (λ k → treeInvariant (node kp ⟪ Black , vp ⟫ (node key ⟪ Red , value ⟫ leaf leaf) k ))
|
|
|
620 (just-injective (cong node-right (just-injective (cong node-left eq)))) (rr05 t₁ refl rr06) )) where
|
|
|
621 lem24 : leaf ≡ uncle
|
|
|
622 lem24 = just-injective (cong node-right eq)
|
|
|
623 lem23 : key₁ ≡ kg
|
|
|
624 lem23 = just-injective (cong node-key eq)
|
|
|
625 rr04 : (kp < kg) ∧ ⊤ ∧ tr< kg _
|
|
|
626 rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
|
|
|
627 rr06 : treeInvariant t₁
|
|
|
628 rr06 = treeRightDown _ _ ti₁
|
|
|
629 rr07 : key < kg
|
|
|
630 rr07 = <-trans x₁ (proj1 rr04)
|
|
|
631 rr05 : (tree : bt (Color ∧ A)) → tree ≡ t₁ → treeInvariant tree → treeInvariant (node kp ⟪ Black , vp ⟫ (node key ⟪ Red , value ⟫ leaf leaf) tree)
|
|
|
632 rr05 .leaf eq₁ t-leaf = t-left _ _ x₁ tt tt (t-single _ _)
|
|
|
633 rr05 .(node key₃ value leaf leaf) eq₁ ti₃@(t-single key₃ value) = t-node _ _ _ x₁ rr09 tt tt tt tt (t-single _ _) (t-single _ _) where
|
|
|
634 rr08 : (key₂ < key₃) ∧ ⊤ ∧ ⊤
|
|
|
635 rr08 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (node-cong refl refl refl (sym eq₁)) ti₁))
|
|
|
636 rr09 : kp < key₃
|
|
|
637 rr09 = subst (λ k → k < key₃) (just-injective (cong node-key (just-injective (cong node-left eq)))) (proj1 rr08)
|
|
|
638 rr05 .(node key₃ _ leaf (node key₁ _ _ _)) eq₁ ti₃@(t-right key₃ key₁ {_} {_} {t₃} {t₄} x x₁₀ x₂ ti₂) = t-node _ _ _ x₁ (proj1 rr08) tt tt tt
|
|
|
639 ⟪ <-trans (proj1 rr08) x , ⟪ proj1 (proj2 (proj2 (proj2 rr08))) , proj2 (proj2 (proj2 (proj2 rr08))) ⟫ ⟫ (t-single _ _) ti₃ where
|
|
|
640 rr08 : (kp < key₃) ∧ ⊤ ∧ ((kp < key₁) ∧ tr> kp t₃ ∧ tr> kp t₄)
|
|
|
641 rr08 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (node-cong (just-injective (cong node-key (just-injective (cong node-left eq)))) refl refl (sym eq₁)) ti₁))
|
|
|
642 rr05 .(node key₁ _ (node key₃ _ _ _) leaf) eq₁ ti₃@(t-left key₃ key₁ {_} {_} {t₃} {t₄} x x₁₀ x₂ ti₂) = t-node _ _ _ x₁ (proj1 rr08) tt tt
|
|
|
643 (proj1 (proj2 rr08)) tt (t-single _ _) ti₃ where
|
|
|
644 rr08 : (kp < key₁) ∧ ((kp < key₃) ∧ tr> kp t₃ ∧ tr> kp t₄) ∧ ⊤
|
|
|
645 rr08 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (node-cong (just-injective (cong node-key (just-injective (cong node-left eq)))) refl refl (sym eq₁)) ti₁))
|
|
|
646 rr05 .(node key₁ _ (node key₃ _ _ _) (node key₂ _ _ _)) eq₁ ti₄@(t-node key₃ key₁ key₂ {_} {_} {_} {t₃} {t₄} {t₅} {t₆} x x₁₀ x₂ x₃ x₄ x₅ ti₂ ti₃)
|
|
|
647 = t-node _ _ _ x₁ (proj1 rr08) tt tt (proj1 (proj2 rr08)) (proj2 (proj2 rr08)) (t-single _ _) ti₄ where
|
|
|
648 rr08 : (kp < key₁) ∧ ((kp < key₃) ∧ tr> kp t₃ ∧ tr> kp t₄) ∧ ((kp < key₂) ∧ tr> kp t₅ ∧ tr> kp t₆)
|
|
|
649 rr08 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (node-cong (just-injective (cong node-key (just-injective (cong node-left eq)))) refl refl (sym eq₁)) ti₁))
|
|
|
650 lem21 _ (t-left key₂ key₁ {value₁} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) eq (rbr-node {v₁} {ca} {t₃} {t₄}) = rr05 t refl lem25 where
|
|
|
651 lem23 : key₁ ≡ kg
|
|
|
652 lem23 = just-injective (cong node-key eq)
|
|
|
653 lem24 : leaf ≡ uncle
|
|
|
654 lem24 = just-injective (cong node-right eq)
|
|
|
655 rr04 : (kp < kg) ∧ ((key < kg) ∧ tr< kg t₃ ∧ tr< kg t₄) ∧ tr< kg t
|
|
|
656 rr04 = proj1 (ti-property1 ti)
|
|
|
657 rr08 : (key < kp) ∧ tr< kp t₃ ∧ tr< kp t₄
|
|
|
658 rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
|
|
|
659 rr05 : (tree : bt (Color ∧ A)) → tree ≡ t → treeInvariant tree
|
|
|
660 → treeInvariant (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ (node key ⟪ ca , value ⟫ t₃ t₄) t) (to-black uncle))
|
|
|
661 rr05 _ eq₁ t-leaf = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁) (subst (λ k → leaf ≡ to-black k ) lem24 refl))
|
|
|
662 ( t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) tt (t-left _ _ x₁ (proj1 (proj2 rr08)) (proj2 (proj2 rr08)) lem22 ))
|
|
|
663 rr05 _ eq₁ (t-single key₃ value) = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁)
|
|
|
664 (subst (λ k → leaf ≡ to-black k ) lem24 refl))
|
|
|
665 ( t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ tt , tt ⟫ ⟫
|
|
|
666 (t-node _ _ _ (proj1 rr08) rr10 (proj1 (proj2 rr08)) (proj2 (proj2 rr08)) tt tt lem22 (t-single _ _) )) where
|
|
|
667 rr09 : (kp < kg) ∧ ((key < kg) ∧ tr< kg t₃ ∧ tr< kg t₄) ∧ ((key₃ < kg) ∧ ⊤ ∧ ⊤ )
|
|
|
668 rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node key ⟪ ca , v₁ ⟫ t₃ t₄) k) uncle))
|
|
|
669 (sym eq₁) ti))
|
|
|
670 rr10 : kp < key₃
|
|
|
671 rr10 = proj1 (subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti))))
|
|
|
672 rr05 _ eq₁ (t-right key₃ key₁ {_} {_} {t₅} {t₆} y y₁ y₂ ti₁) = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁)
|
|
|
673 (subst (λ k → leaf ≡ to-black k ) lem24 refl))
|
|
|
674 ( t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ tt , proj2 (proj2 (proj2 (proj2 rr09))) ⟫ ⟫
|
|
|
675 (t-node _ _ _ (proj1 rr08) rr10 (proj1 (proj2 rr08)) (proj2 (proj2 rr08)) tt
|
|
|
676 ⟪ <-trans rr10 y , ⟪ <-tr> y₁ rr10 , <-tr> y₂ rr10 ⟫ ⟫ lem22 (t-right _ _ y y₁ y₂ ti₁) )) where
|
|
|
677 rr09 : (kp < kg) ∧ ((key < kg) ∧ tr< kg t₃ ∧ tr< kg t₄) ∧ ((key₃ < kg) ∧ ⊤ ∧ ( (key₁ < kg) ∧ tr< kg t₅ ∧ tr< kg t₆ ) )
|
|
|
678 rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node key ⟪ ca , v₁ ⟫ t₃ t₄) k) uncle))
|
|
|
679 (sym eq₁) ti))
|
|
|
680 rr10 : kp < key₃
|
|
|
681 rr10 = proj1 (subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti))))
|
|
|
682 rr05 _ eq₁ (t-left key₃ key₁ {_} {_} {t₅} {t₆} y y₁ y₂ ti₁) = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁)
|
|
|
683 (subst (λ k → leaf ≡ to-black k ) lem24 refl))
|
|
|
684 ( t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ proj1 (proj2 (proj2 (proj2 rr09))) , tt ⟫ ⟫
|
|
|
685 (t-node _ _ _ (proj1 rr08) (proj1 rr10) (proj1 (proj2 rr08)) (proj2 (proj2 rr08))
|
|
|
686 ⟪ proj1 (proj1 (proj2 rr10)) , ⟪ proj1 (proj2 (proj1 (proj2 rr10))) , proj2 (proj2 (proj1 (proj2 rr10))) ⟫ ⟫ tt lem22 (t-left _ _ y y₁ y₂ ti₁) )) where
|
|
|
687 rr09 : (kp < kg) ∧ ((key < kg) ∧ tr< kg t₃ ∧ tr< kg t₄) ∧ ((key₁ < kg) ∧ ( (key₃ < kg) ∧ tr< kg t₅ ∧ tr< kg t₆ ) ∧ ⊤ )
|
|
|
688 rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node key ⟪ ca , v₁ ⟫ t₃ t₄) k) uncle))
|
|
|
689 (sym eq₁) ti))
|
|
|
690 rr10 : (kp < key₁ ) ∧ ((kp < key₃) ∧ tr> kp t₅ ∧ tr> kp t₆) ∧ ⊤
|
|
|
691 rr10 = subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
|
|
|
692 rr05 _ eq₁ (t-node key₃ key₁ key₂ {_} {_} {_} {t₅} {t₆} {t₇} {t₈} y y₁ y₂ y₃ y₄ y₅ ti₁ ti₂)
|
|
|
693 = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁)
|
|
|
694 (subst (λ k → leaf ≡ to-black k ) lem24 refl))
|
|
|
695 ( t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ proj1 (proj2 (proj2 (proj2 rr09))) , proj2 (proj2 (proj2 (proj2 rr09))) ⟫ ⟫
|
|
|
696 (t-node _ _ _ (proj1 rr08) (proj1 rr10) (proj1 (proj2 rr08)) (proj2 (proj2 rr08))
|
|
|
697 ⟪ proj1 (proj1 (proj2 rr10)) , ⟪ proj1 (proj2 (proj1 (proj2 rr10))) , proj2 (proj2 (proj1 (proj2 rr10))) ⟫ ⟫ (proj2 (proj2 rr10)) lem22
|
|
|
698 (t-node _ _ _ y y₁ y₂ y₃ y₄ y₅ ti₁ ti₂))) where
|
|
|
699 rr09 : (kp < kg) ∧ ((key < kg) ∧ tr< kg t₃ ∧ tr< kg t₄) ∧ ((key₁ < kg) ∧ ( (key₃ < kg) ∧ tr< kg t₅ ∧ tr< kg t₆ ) ∧ ( (key₂ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈ ) )
|
|
|
700 rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node key ⟪ ca , v₁ ⟫ t₃ t₄) k) uncle))
|
|
|
701 (sym eq₁) ti))
|
|
|
702 rr10 : (kp < key₁ ) ∧ ((kp < key₃) ∧ tr> kp t₅ ∧ tr> kp t₆) ∧ ((kp < key₂) ∧ tr> kp t₇ ∧ tr> kp t₈)
|
|
|
703 rr10 = subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
|
|
|
704 lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) eq (rbr-right {k₁} {v₁} {ca} {t₃} {t₄} {t₅} x₃ x₄ rbt) = rr05 t refl lem25 where
|
|
|
705 lem23 : key₁ ≡ kg
|
|
|
706 lem23 = just-injective (cong node-key eq)
|
|
|
707 lem24 : leaf ≡ uncle
|
|
|
708 lem24 = just-injective (cong node-right eq)
|
|
|
709 rr04 : (kp < kg) ∧ ((k₁ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ tr< kg t
|
|
|
710 rr04 = proj1 (ti-property1 ti)
|
|
|
711 rr08 : (k₁ < kp) ∧ tr< kp t₄ ∧ tr< kp t₅
|
|
|
712 rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
|
|
|
713 rr03 : tr< kp t₃
|
|
|
714 rr03 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 rr08))
|
|
|
715 rr05 : (tree : bt (Color ∧ A)) → tree ≡ t → treeInvariant tree
|
|
|
716 → treeInvariant (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ (node k₁ ⟪ ca , v₁ ⟫ t₄ t₃) t) (to-black uncle))
|
|
|
717 rr05 _ eq₁ t-leaf = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁) (subst (λ k → leaf ≡ to-black k ) lem24 refl))
|
|
|
718 ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , >-tr< rr03 (proj1 rr04) ⟫ ⟫ tt
|
|
|
719 (t-left _ _ (proj1 rr08) (proj1 (proj2 rr08)) rr03 lem22 ))
|
|
|
720 rr05 _ eq₁ (t-single key₃ value) = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁)
|
|
|
721 (subst (λ k → leaf ≡ to-black k ) lem24 refl))
|
|
|
722 ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , >-tr< rr03 (proj1 rr04) ⟫ ⟫ ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ tt , tt ⟫ ⟫
|
|
|
723 (t-node _ _ _ (proj1 rr08) rr10 (proj1 (proj2 rr08)) rr03 tt tt lem22 (t-single _ _) )) where
|
|
|
724 rr09 : (kp < kg) ∧ ((k₁ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ ((key₃ < kg) ∧ ⊤ ∧ ⊤ )
|
|
|
725 rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node k₁ ⟪ ca , v₁ ⟫ t₄ t₅) k) uncle))
|
|
|
726 (sym eq₁) ti))
|
|
|
727 rr10 : kp < key₃
|
|
|
728 rr10 = proj1 (subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti))))
|
|
|
729 rr05 _ eq₁ (t-right key₃ key₁ {_} {_} {t₆} {t₇} y y₁ y₂ ti₁) = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁)
|
|
|
730 (subst (λ k → leaf ≡ to-black k ) lem24 refl))
|
|
|
731 ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , >-tr< rr03 (proj1 rr04) ⟫ ⟫ ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ tt , proj2 (proj2 (proj2 (proj2 rr09))) ⟫ ⟫
|
|
|
732 (t-node _ _ _ (proj1 rr08) rr10 (proj1 (proj2 rr08)) rr03 tt
|
|
|
733 ⟪ <-trans rr10 y , ⟪ <-tr> y₁ rr10 , <-tr> y₂ rr10 ⟫ ⟫ lem22 (t-right _ _ y y₁ y₂ ti₁) )) where
|
|
|
734 rr09 : (kp < kg) ∧ ((k₁ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ ((key₃ < kg) ∧ ⊤ ∧ ( (key₁ < kg) ∧ tr< kg t₆ ∧ tr< kg t₇ ) )
|
|
|
735 rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node k₁ ⟪ ca , v₁ ⟫ t₄ t₅) k) uncle))
|
|
|
736 (sym eq₁) ti))
|
|
|
737 rr10 : kp < key₃
|
|
|
738 rr10 = proj1 (subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti))))
|
|
|
739 rr05 _ eq₁ (t-left key₃ key₁ {_} {_} {t₆} {t₇} y y₁ y₂ ti₁) = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁)
|
|
|
740 (subst (λ k → leaf ≡ to-black k ) lem24 refl))
|
|
|
741 ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , >-tr< rr03 (proj1 rr04) ⟫ ⟫ ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ proj1 (proj2 (proj2 (proj2 rr09))) , tt ⟫ ⟫
|
|
|
742 (t-node _ _ _ (proj1 rr08) (proj1 rr10) (proj1 (proj2 rr08)) rr03
|
|
|
743 ⟪ proj1 (proj1 (proj2 rr10)) , ⟪ proj1 (proj2 (proj1 (proj2 rr10))) , proj2 (proj2 (proj1 (proj2 rr10))) ⟫ ⟫ tt lem22 (t-left _ _ y y₁ y₂ ti₁) )) where
|
|
|
744 rr09 : (kp < kg) ∧ ((k₁ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ ((key₁ < kg) ∧ ( (key₃ < kg) ∧ tr< kg t₆ ∧ tr< kg t₇ ) ∧ ⊤ )
|
|
|
745 rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node k₁ ⟪ ca , v₁ ⟫ t₄ t₅) k) uncle))
|
|
|
746 (sym eq₁) ti))
|
|
|
747 rr10 : (kp < key₁ ) ∧ ((kp < key₃) ∧ tr> kp t₆ ∧ tr> kp t₇) ∧ ⊤
|
|
|
748 rr10 = subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
|
|
|
749 rr05 _ eq₁ (t-node key₃ key₁ key₂ {_} {_} {_} {t₆} {t₇} {t₈} {t₉} y y₁ y₂ y₃ y₄ y₅ ti₁ ti₂)
|
|
|
750 = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁)
|
|
|
751 (subst (λ k → leaf ≡ to-black k ) lem24 refl))
|
|
|
752 ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , >-tr< rr03 (proj1 rr04) ⟫ ⟫ ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ proj1 (proj2 (proj2 (proj2 rr09))) , proj2 (proj2 (proj2 (proj2 rr09))) ⟫ ⟫
|
|
|
753 (t-node _ _ _ (proj1 rr08) (proj1 rr10) (proj1 (proj2 rr08)) rr03
|
|
|
754 ⟪ proj1 (proj1 (proj2 rr10)) , ⟪ proj1 (proj2 (proj1 (proj2 rr10))) , proj2 (proj2 (proj1 (proj2 rr10))) ⟫ ⟫ (proj2 (proj2 rr10)) lem22
|
|
|
755 (t-node _ _ _ y y₁ y₂ y₃ y₄ y₅ ti₁ ti₂))) where
|
|
|
756 rr09 : (kp < kg) ∧ ((k₁ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ ((key₁ < kg) ∧ ( (key₃ < kg) ∧ tr< kg t₆ ∧ tr< kg t₇ ) ∧ ( (key₂ < kg) ∧ tr< kg t₈ ∧ tr< kg t₉ ) )
|
|
|
757 rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node k₁ ⟪ ca , v₁ ⟫ t₄ t₅) k) uncle))
|
|
|
758 (sym eq₁) ti))
|
|
|
759 rr10 : (kp < key₁ ) ∧ ((kp < key₃) ∧ tr> kp t₆ ∧ tr> kp t₇) ∧ ((kp < key₂) ∧ tr> kp t₈ ∧ tr> kp t₉)
|
|
|
760 rr10 = subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
|
|
|
761 lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) eq (rbr-left {k₁} {v₁} {ca} {t₃} {t₄} {t₅} x₃ x₄ rbt) =
|
|
|
762 subst treeInvariant (node-cong refl refl refl (subst (λ k → leaf ≡ to-black k ) lem24 refl))
|
|
|
763 ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04) , ⟪ >-tr< rr03 (proj1 rr04) , proj2 (proj2 (proj1 (proj2 rr04))) ⟫ ⟫ (proj2 (proj2 rr04)) rr06) where
|
|
|
764 lem23 : key₁ ≡ kg
|
|
|
765 lem23 = just-injective (cong node-key eq)
|
|
|
766 lem24 : leaf ≡ uncle
|
|
|
767 lem24 = just-injective (cong node-right eq)
|
|
|
768 rr04 : (kp < kg) ∧ ((k₁ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ tr< kg t
|
|
|
769 rr04 = proj1 (ti-property1 ti)
|
|
|
770 rr08 : (k₁ < kp) ∧ tr< kp t₄ ∧ tr< kp t₅
|
|
|
771 rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
|
|
|
772 rr03 : tr< kp t₃
|
|
|
773 rr03 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 rr08))
|
|
|
774 rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node k₁ ⟪ ca , v₁ ⟫ t₃ t₅) t)
|
|
|
775 rr06 with node→leaf∨IsNode t
|
|
|
776 ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) rr03 (proj2 (proj2 rr08)) lem22 )
|
|
|
777 ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) rr03 (proj2 (proj2 rr08)) (proj1 (proj2 rr11)) (proj2 (proj2 rr11))
|
|
|
778 lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
|
|
|
779 rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)
|
|
|
780 rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
|
|
|
781 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt) =
|
|
|
782 subst treeInvariant (node-cong refl refl refl (subst (λ k → leaf ≡ to-black k ) lem24 refl))
|
|
|
783 ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , >-tr< rr03 (proj1 rr04) ⟫ ⟫ (proj2 (proj2 rr04)) rr06) where
|
|
|
784 lem23 : key₁ ≡ kg
|
|
|
785 lem23 = just-injective (cong node-key eq)
|
|
|
786 lem24 : leaf ≡ uncle
|
|
|
787 lem24 = just-injective (cong node-right eq)
|
|
|
788 rr04 : (kp < kg) ∧ ((_ < kg) ∧ tr< kg t₁ ∧ tr< kg t₂) ∧ tr< kg t
|
|
|
789 rr04 = proj1 (ti-property1 ti)
|
|
|
790 rr08 : (_ < kp) ∧ tr< kp t₁ ∧ tr< kp t₂
|
|
|
791 rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
|
|
|
792 rr03 : tr< kp t₃
|
|
|
793 rr03 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 rr08))
|
|
|
794 rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node _ ⟪ _ , _ ⟫ t₁ t₃) t)
|
|
|
795 rr06 with node→leaf∨IsNode t
|
|
|
796 ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) (proj1 (proj2 rr08)) rr03 lem22 )
|
|
|
797 ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) (proj1 (proj2 rr08))
|
|
|
798 rr03 (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
|
|
|
799 rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)
|
|
|
800 rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
|
|
|
801 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt) =
|
|
|
802 subst treeInvariant (node-cong refl refl refl (subst (λ k → leaf ≡ to-black k ) lem24 refl))
|
|
|
803 ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04) , ⟪ >-tr< rr03 (proj1 rr04) , proj2 (proj2 (proj1 (proj2 rr04))) ⟫ ⟫ (proj2 (proj2 rr04)) rr06 ) where
|
|
|
804 lem23 : key₁ ≡ kg
|
|
|
805 lem23 = just-injective (cong node-key eq)
|
|
|
806 lem24 : leaf ≡ uncle
|
|
|
807 lem24 = just-injective (cong node-right eq)
|
|
|
808 rr04 : (kp < kg) ∧ ((_ < kg) ∧ tr< kg t₂ ∧ tr< kg t₁) ∧ tr< kg t
|
|
|
809 rr04 = proj1 (ti-property1 ti)
|
|
|
810 rr08 : (_ < kp) ∧ tr< kp t₂ ∧ tr< kp t₁
|
|
|
811 rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
|
|
|
812 rr03 : tr< kp t₃
|
|
|
813 rr03 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 rr08))
|
|
|
814 rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node _ ⟪ _ , _ ⟫ t₃ t₁) t)
|
|
|
815 rr06 with node→leaf∨IsNode t
|
|
|
816 ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) rr03 (proj2 (proj2 rr08)) lem22 )
|
|
|
817 ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) rr03
|
|
|
818 (proj2 (proj2 rr08)) (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
|
|
|
819 rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)
|
|
|
820 rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
|
|
|
821 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-flip-ll {t₁} {t₂} {t₃} {t₆} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt)
|
|
|
822 = ⊥-elim (⊥-color (trans (sym lem26) ueq) ) where
|
|
|
823 lem26 : color uncle ≡ Black
|
|
|
824 lem26 = subst (λ k → color k ≡ Black) (just-injective (cong node-right eq )) refl
|
|
|
825 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-flip-lr {t₁} {t₂} {t₃} {t₆} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt)
|
|
|
826 = ⊥-elim (⊥-color (trans (sym lem26) ueq) ) where
|
|
|
827 lem26 : color uncle ≡ Black
|
|
|
828 lem26 = subst (λ k → color k ≡ Black) (just-injective (cong node-right eq )) refl
|
|
|
829 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-flip-rl {t₁} {t₂} {t₃} {t₆} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt)
|
|
|
830 = ⊥-elim (⊥-color (trans (sym lem26) ueq) ) where
|
|
|
831 lem26 : color uncle ≡ Black
|
|
|
832 lem26 = subst (λ k → color k ≡ Black) (just-injective (cong node-right eq )) refl
|
|
|
833 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-flip-rr {t₁} {t₂} {t₃} {t₆} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt)
|
|
|
834 = ⊥-elim (⊥-color (trans (sym lem26) ueq) ) where
|
|
|
835 lem26 : color uncle ≡ Black
|
|
|
836 lem26 = subst (λ k → color k ≡ Black) (just-injective (cong node-right eq )) refl
|
|
|
837 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-ll {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
838 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-rr {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
839 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
840 lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
841 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq rbr-leaf =
|
|
|
842 subst treeInvariant (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (proj1 rr03) ⟪ <-trans x₁ (proj1 rr04) , ⟪ tt , tt ⟫ ⟫ (proj2 (proj2 rr04))
|
|
|
843 (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) rr06 (to-black-treeInvariant _ ti₂)) where
|
|
|
844 lem23 : key₁ ≡ kg
|
|
|
845 lem23 = just-injective (cong node-key eq)
|
|
|
846 lem24 : node key₂ v2 t₁₀ t₁₁ ≡ uncle
|
|
|
847 lem24 = just-injective (cong node-right eq)
|
|
|
848 rr04 : (kp < kg) ∧ ⊤ ∧ tr< kg t
|
|
|
849 rr04 = proj1 (ti-property1 ti)
|
|
|
850 rr03 : (kg < key₂) ∧ tr> kg t₁₀ ∧ tr> kg t₁₁
|
|
|
851 rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ _ t) k)) (sym lem24) ti))
|
|
|
852 rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ _ t)
|
|
|
853 rr06 with node→leaf∨IsNode t
|
|
|
854 ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ x₁ tt tt lem22 )
|
|
|
855 ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ x₁ (proj1 rr11) tt
|
|
|
856 tt (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
|
|
|
857 rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)
|
|
|
858 rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
|
|
|
859 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-node {_} {_} {t₃} {t₄}) =
|
|
|
860 subst treeInvariant (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (proj1 rr03) (proj1 (proj2 rr04)) (proj2 (proj2 rr04))
|
|
|
861 (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) rr06 (to-black-treeInvariant _ ti₂)) where
|
|
|
862 lem23 : key₁ ≡ kg
|
|
|
863 lem23 = just-injective (cong node-key eq)
|
|
|
864 lem24 : node key₂ v2 t₁₀ t₁₁ ≡ uncle
|
|
|
865 lem24 = just-injective (cong node-right eq)
|
|
|
866 rr04 : (kp < kg) ∧ ((key < kg) ∧ tr< kg t₃ ∧ tr< kg t₄) ∧ tr< kg t
|
|
|
867 rr04 = proj1 (ti-property1 ti)
|
|
|
868 rr08 : (key < kp) ∧ tr< kp t₃ ∧ tr< kp t₄
|
|
|
869 rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
|
|
|
870 rr03 : (kg < key₂) ∧ tr> kg t₁₀ ∧ tr> kg t₁₁
|
|
|
871 rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node key ⟪ _ , _ ⟫ t₃ t₄) t) k)) (sym lem24) ti))
|
|
|
872 rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node _ ⟪ _ , _ ⟫ t₃ t₄) t)
|
|
|
873 rr06 with node→leaf∨IsNode t
|
|
|
874 ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) (proj1 (proj2 rr08)) (proj2 (proj2 rr08)) lem22 )
|
|
|
875 ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) (proj1 (proj2 rr08))
|
|
|
876 (proj2 (proj2 rr08)) (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
|
|
|
877 rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)
|
|
|
878 rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
|
|
|
879 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-right {k₃} {_} {_} {t₃} {t₄} {t₅} x₆ x₇ rbt) =
|
|
|
880 subst treeInvariant (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (proj1 rr03)
|
|
|
881 ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , >-tr< rr05 (proj1 rr04) ⟫ ⟫ (proj2 (proj2 rr04))
|
|
|
882 (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) rr06 (to-black-treeInvariant _ ti₂)) where
|
|
|
883 lem23 : key₁ ≡ kg
|
|
|
884 lem23 = just-injective (cong node-key eq)
|
|
|
885 lem24 : node key₂ v2 t₁₀ t₁₁ ≡ uncle
|
|
|
886 lem24 = just-injective (cong node-right eq)
|
|
|
887 rr04 : (kp < kg) ∧ ((k₃ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ tr< kg t
|
|
|
888 rr04 = proj1 (ti-property1 ti)
|
|
|
889 rr08 : (k₃ < kp) ∧ tr< kp t₄ ∧ tr< kp t₅
|
|
|
890 rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
|
|
|
891 rr03 : (kg < key₂) ∧ tr> kg t₁₀ ∧ tr> kg t₁₁
|
|
|
892 rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node k₃ ⟪ _ , _ ⟫ t₄ t₅) t) k)) (sym lem24) ti))
|
|
|
893 rr05 : tr< kp t₃
|
|
|
894 rr05 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 rr08))
|
|
|
895 rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node k₃ ⟪ _ , _ ⟫ t₄ t₃) t)
|
|
|
896 rr06 with node→leaf∨IsNode t
|
|
|
897 ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) (proj1 (proj2 rr08)) rr05 lem22)
|
|
|
898 ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) (proj1 (proj2 rr08))
|
|
|
899 rr05 (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
|
|
|
900 rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)
|
|
|
901 rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
|
|
|
902 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-left {k₃} {_} {_} {t₃} {t₄} {t₅} x₆ x₇ rbt) =
|
|
|
903 subst treeInvariant (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (proj1 rr03)
|
|
|
904 ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ >-tr< rr05 (proj1 rr04) , proj2 (proj2 (proj1 (proj2 rr04))) ⟫ ⟫ (proj2 (proj2 rr04))
|
|
|
905 (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) rr06 (to-black-treeInvariant _ ti₂)) where
|
|
|
906 lem23 : key₁ ≡ kg
|
|
|
907 lem23 = just-injective (cong node-key eq)
|
|
|
908 lem24 : node key₂ v2 t₁₀ t₁₁ ≡ uncle
|
|
|
909 lem24 = just-injective (cong node-right eq)
|
|
|
910 rr04 : (kp < kg) ∧ ((k₃ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ tr< kg t
|
|
|
911 rr04 = proj1 (ti-property1 ti)
|
|
|
912 rr08 : (k₃ < kp) ∧ tr< kp t₄ ∧ tr< kp t₅
|
|
|
913 rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
|
|
|
914 rr03 : (kg < key₂) ∧ tr> kg t₁₀ ∧ tr> kg t₁₁
|
|
|
915 rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node k₃ ⟪ _ , _ ⟫ t₄ t₅) t) k)) (sym lem24) ti))
|
|
|
916 rr05 : tr< kp t₃
|
|
|
917 rr05 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 rr08))
|
|
|
918 rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node k₃ ⟪ _ , _ ⟫ t₃ t₅) t)
|
|
|
919 rr06 with node→leaf∨IsNode t
|
|
|
920 ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) rr05 (proj2 (proj2 rr08)) lem22)
|
|
|
921 ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) rr05
|
|
|
922 (proj2 (proj2 rr08)) (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
|
|
|
923 rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)
|
|
|
924 rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
|
|
|
925 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-black-right {t₃} {t₄} {t₅} x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
926 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-black-left {t₃} {t₄} {t₅} x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
927 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-ll {t₄} {t₁} {t₂} {t₃} {kg₁} {kp₁} {vg₁} {vp₁} x₆ x₇ x₈ rbt) =
|
|
|
928 subst treeInvariant (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (subst (λ k → k < key₂) lem23 (proj1 rr03))
|
|
|
929 ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ ⟪ <-trans (proj1 (proj1 (proj2 rr08))) (proj1 rr04) ,
|
|
|
930 ⟪ >-tr< rr05 (proj1 rr04) , proj2 (proj2 (proj1 (proj2 (proj1 (proj2 rr04))))) ⟫ ⟫ , tr<-to-black (proj2 (proj2 (proj1 (proj2 rr04)))) ⟫ ⟫ (proj2 (proj2 rr04))
|
|
|
931 (subst (λ k → tr> k t₁₀) lem23 (proj1 (proj2 rr03))) (subst (λ k → tr> k t₁₁) lem23 (proj2 (proj2 rr03))) rr06 (to-black-treeInvariant _ ti₂)) where
|
|
|
932 lem23 : key₁ ≡ kg
|
|
|
933 lem23 = just-injective (cong node-key eq)
|
|
|
934 lem24 : node key₂ v2 t₁₀ t₁₁ ≡ uncle
|
|
|
935 lem24 = just-injective (cong node-right eq)
|
|
|
936 rr04 : (kp < kg) ∧ ((kg₁ < kg) ∧ ((kp₁ < kg) ∧ tr< kg t₁ ∧ tr< kg t₄) ∧ tr< kg t₃ ) ∧ tr< kg t
|
|
|
937 rr04 = proj1 (ti-property1 ti)
|
|
|
938 rr08 : (kg₁ < kp) ∧ ((kp₁ < kp) ∧ tr< kp t₁ ∧ tr< kp t₄) ∧ tr< kp t₃
|
|
|
939 rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
|
|
|
940 rr03 : (key₁ < key₂) ∧ tr> key₁ t₁₀ ∧ tr> key₁ t₁₁
|
|
|
941 rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (sym eq) ti ))
|
|
|
942 rr05 : tr< kp t₂
|
|
|
943 rr05 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj1 (proj2 rr08))))
|
|
|
944 rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node kg₁ ⟪ Red , vg₁ ⟫ (node kp₁ ⟪ Black , vp₁ ⟫ t₂ t₄) (to-black t₃)) t)
|
|
|
945 rr06 with node→leaf∨IsNode t
|
|
|
946 ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) ⟪ proj1 (proj1 (proj2 rr08)) ,
|
|
|
947 ⟪ rr05 , proj2 (proj2 (proj1 (proj2 rr08))) ⟫ ⟫ (tr<-to-black (proj2 (proj2 rr08))) lem22)
|
|
|
948 ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11)
|
|
|
949 ⟪ proj1 (proj1 (proj2 rr08)) , ⟪ rr05 , proj2 (proj2 (proj1 (proj2 rr08))) ⟫ ⟫
|
|
|
950 (tr<-to-black (proj2 (proj2 rr08))) (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
|
|
|
951 rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)
|
|
|
952 rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
|
|
|
953 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-lr {t₀} {t₁} {t₂} {t₃} {kg₁} {kp₁} {vg₁} {vp₁} x₆ x₇ x₈ x₉ rbt) =
|
|
|
954 subst treeInvariant (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (subst (λ k → k < key₂) lem23 (proj1 rr03))
|
|
|
955 ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ ⟪ <-trans (proj1 (proj1 (proj2 rr08))) (proj1 rr04) ,
|
|
|
956 ⟪ proj1 (proj2 (proj1 (proj2 (proj1 (proj2 rr04))))) , >-tr< rr05 (proj1 rr04) ⟫ ⟫ , tr<-to-black (proj2 (proj2 (proj1 (proj2 rr04)))) ⟫ ⟫ (proj2 (proj2 rr04))
|
|
|
957 (subst (λ k → tr> k t₁₀) lem23 (proj1 (proj2 rr03))) (subst (λ k → tr> k t₁₁) lem23 (proj2 (proj2 rr03))) rr06 (to-black-treeInvariant _ ti₂)) where
|
|
|
958 lem23 : key₁ ≡ kg
|
|
|
959 lem23 = just-injective (cong node-key eq)
|
|
|
960 lem24 : node key₂ v2 t₁₀ t₁₁ ≡ uncle
|
|
|
961 lem24 = just-injective (cong node-right eq)
|
|
|
962 rr04 : (kp < kg) ∧ ((kg₁ < kg) ∧ ((kp₁ < kg) ∧ tr< kg t₀ ∧ tr< kg t₁) ∧ tr< kg t₃ ) ∧ tr< kg t
|
|
|
963 rr04 = proj1 (ti-property1 ti)
|
|
|
964 rr08 : (kg₁ < kp) ∧ ((kp₁ < kp) ∧ tr< kp t₀ ∧ tr< kp t₁) ∧ tr< kp t₃
|
|
|
965 rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
|
|
|
966 rr03 : (key₁ < key₂) ∧ tr> key₁ t₁₀ ∧ tr> key₁ t₁₁
|
|
|
967 rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (sym eq) ti ))
|
|
|
968 rr05 : tr< kp t₂
|
|
|
969 rr05 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj1 (proj2 rr08))))
|
|
|
970 rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node kg₁ ⟪ Red , vg₁ ⟫ (node kp₁ ⟪ Black , _ ⟫ t₀ t₂) (to-black t₃)) t)
|
|
|
971 rr06 with node→leaf∨IsNode t
|
|
|
972 ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) ⟪ proj1 (proj1 (proj2 rr08)) ,
|
|
|
973 ⟪ proj1 (proj2 (proj1 (proj2 rr08))) , rr05 ⟫ ⟫ (tr<-to-black (proj2 (proj2 rr08))) lem22)
|
|
|
974 ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11)
|
|
|
975 ⟪ proj1 (proj1 (proj2 rr08)) , ⟪ proj1 (proj2 (proj1 (proj2 rr08))) , rr05 ⟫ ⟫
|
|
|
976 (tr<-to-black (proj2 (proj2 rr08))) (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
|
|
|
977 rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)
|
|
|
978 rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
|
|
|
979 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-rl {t₀} {t₁} {t₂} {t₃} {kg₁} {kp₁} {vg₁} {vp₁} x₆ x₇ x₈ x₉ rbt) =
|
|
|
980 subst treeInvariant (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (subst (λ k → k < key₂) lem23 (proj1 rr03))
|
|
|
981 ⟪ proj1 (proj1 (proj2 rr04)) , ⟪
|
|
|
982 tr<-to-black (proj1 (proj2 (proj1 (proj2 rr04)))) , ⟪ proj1 (proj2 (proj2 (proj1 (proj2 rr04)))) ,
|
|
|
983 ⟪ >-tr< rr05 (proj1 rr04) , proj2 (proj2 (proj2 (proj2 (proj1 (proj2 rr04))))) ⟫ ⟫ ⟫ ⟫ (proj2 (proj2 rr04))
|
|
|
984 (subst (λ k → tr> k t₁₀) lem23 (proj1 (proj2 rr03))) (subst (λ k → tr> k t₁₁) lem23 (proj2 (proj2 rr03))) rr06 (to-black-treeInvariant _ ti₂)) where
|
|
|
985 lem23 : key₁ ≡ kg
|
|
|
986 lem23 = just-injective (cong node-key eq)
|
|
|
987 lem24 : node key₂ v2 t₁₀ t₁₁ ≡ uncle
|
|
|
988 lem24 = just-injective (cong node-right eq)
|
|
|
989 rr04 : (kp < kg) ∧ ((kg₁ < kg) ∧ tr< kg t₃ ∧ ((kp₁ < kg) ∧ tr< kg t₁ ∧ tr< kg t₀) ) ∧ tr< kg t
|
|
|
990 rr04 = proj1 (ti-property1 ti)
|
|
|
991 rr08 : (kg₁ < kp) ∧ tr< kp t₃ ∧ ((kp₁ < kp) ∧ tr< kp t₁ ∧ tr< kp t₀)
|
|
|
992 rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
|
|
|
993 rr03 : (key₁ < key₂) ∧ tr> key₁ t₁₀ ∧ tr> key₁ t₁₁
|
|
|
994 rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (sym eq) ti ))
|
|
|
995 rr05 : tr< kp t₂
|
|
|
996 rr05 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj2 (proj2 rr08))))
|
|
|
997 rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node kg₁ ⟪ Red , vg₁ ⟫ (to-black t₃) (node kp₁ ⟪ Black , vp₁ ⟫ t₂ t₀)) t)
|
|
|
998 rr06 with node→leaf∨IsNode t
|
|
|
999 ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) (tr<-to-black (proj1 (proj2 rr08)))
|
|
|
1000 ⟪ proj1 (proj2 (proj2 rr08)) , ⟪ rr05 , proj2 (proj2 (proj2 (proj2 rr08))) ⟫ ⟫ lem22)
|
|
|
1001 ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11)
|
|
|
1002 (tr<-to-black (proj1 (proj2 rr08))) ⟪ proj1 (proj2 (proj2 rr08)) , ⟪ rr05 , proj2 (proj2 (proj2 (proj2 rr08))) ⟫ ⟫
|
|
|
1003 (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
|
|
|
1004 rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)
|
|
|
1005 rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
|
|
|
1006 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-rr {t₀} {t₁} {t₂} {t₃} {kg₁} {kp₁} {vg₁} {vp₁} x₆ x₇ x₈ rbt) =
|
|
|
1007 subst treeInvariant (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (subst (λ k → k < key₂) lem23 (proj1 rr03))
|
|
|
1008 ⟪ proj1 (proj1 (proj2 rr04)) , ⟪
|
|
|
1009 tr<-to-black (proj1 (proj2 (proj1 (proj2 rr04)))) , ⟪ proj1 (proj2 (proj2 (proj1 (proj2 rr04)))) ,
|
|
|
1010 ⟪ proj1 (proj2 (proj2 (proj2 (proj1 (proj2 rr04))))) , >-tr< rr05 (proj1 rr04) ⟫ ⟫ ⟫ ⟫ (proj2 (proj2 rr04))
|
|
|
1011 (subst (λ k → tr> k t₁₀) lem23 (proj1 (proj2 rr03))) (subst (λ k → tr> k t₁₁) lem23 (proj2 (proj2 rr03))) rr06 (to-black-treeInvariant _ ti₂)) where
|
|
|
1012 lem23 : key₁ ≡ kg
|
|
|
1013 lem23 = just-injective (cong node-key eq)
|
|
|
1014 lem24 : node key₂ v2 t₁₀ t₁₁ ≡ uncle
|
|
|
1015 lem24 = just-injective (cong node-right eq)
|
|
|
1016 rr04 : (kp < kg) ∧ ((kg₁ < kg) ∧ tr< kg t₃ ∧ ((kp₁ < kg) ∧ tr< kg t₀ ∧ tr< kg t₁) ) ∧ tr< kg t
|
|
|
1017 rr04 = proj1 (ti-property1 ti)
|
|
|
1018 rr08 : (kg₁ < kp) ∧ tr< kp t₃ ∧ ((kp₁ < kp) ∧ tr< kp t₀ ∧ tr< kp t₁)
|
|
|
1019 rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
|
|
|
1020 rr03 : (key₁ < key₂) ∧ tr> key₁ t₁₀ ∧ tr> key₁ t₁₁
|
|
|
1021 rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (sym eq) ti ))
|
|
|
1022 rr05 : tr< kp t₂
|
|
|
1023 rr05 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj2 (proj2 rr08))))
|
|
|
1024 rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node kg₁ ⟪ Red , vg₁ ⟫ (to-black t₃) (node kp₁ ⟪ Black , vp₁ ⟫ t₀ t₂)) t)
|
|
|
1025 rr06 with node→leaf∨IsNode t
|
|
|
1026 ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) (tr<-to-black (proj1 (proj2 rr08)))
|
|
|
1027 ⟪ proj1 (proj2 (proj2 rr08)) , ⟪ proj1 (proj2 (proj2 (proj2 rr08))) , rr05 ⟫ ⟫ lem22)
|
|
|
1028 ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11)
|
|
|
1029 (tr<-to-black (proj1 (proj2 rr08))) ⟪ proj1 (proj2 (proj2 rr08)) , ⟪ proj1 (proj2 (proj2 (proj2 rr08))) , rr05 ⟫ ⟫
|
|
|
1030 (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
|
|
|
1031 rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)
|
|
|
1032 rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
|
|
|
1033 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-rr x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
1034 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-ll x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
1035 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₆ x₇ x₈ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
1036 lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₆ x₇ x₈ rbt) = ⊥-elim (⊥-color ceq)
|
|
|
1037
|
|
|
1038
|
|
|
1039
|
|
|
1040 RB-repl→ti-lem07 : {n : Level} {A : Set n} {key : ℕ} {value : A} {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
|
|
|
1041 (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key) (x₃ : key < kg) (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂)
|
|
|
1042 → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁) uncle)
|
|
|
1043 → treeInvariant (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t t₂) (to-black uncle))
|
|
|
1044 RB-repl→ti-lem07 = ?
|
|
|
1045
|
|
|
1046 RB-repl→ti-lem08 : {n : Level} {A : Set n} {key : ℕ} {value : A} → {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
|
|
|
1047 (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kg < key) (x₃ : key < kp) (rbt : replacedRBTree key value t₁ t₂)
|
|
|
1048 → (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t₁ t))
|
|
|
1049 → treeInvariant (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t₂ t))
|
|
|
1050 RB-repl→ti-lem08 = ?
|
|
|
1051
|
|
|
1052 RB-repl→ti-lem09 : {n : Level} {A : Set n} {key : ℕ} {value : A} → {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
|
|
|
1053 (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key) (rbt : replacedRBTree key value t₁ t₂) →
|
|
|
1054 (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t t₁)) →
|
|
|
1055 treeInvariant (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t t₂))
|
|
|
1056 RB-repl→ti-lem09 = ?
|
|
|
1057
|
|
|
1058 RB-repl→ti-lem10 : {n : Level} {A : Set n} {key : ℕ} {value : A} → {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
|
|
|
1059 (x : color t₂ ≡ Red) (x₁ : key < kp) (rbt : replacedRBTree key value t₁ t₂) →
|
|
|
1060 (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₁ t) uncle) →
|
|
|
1061 treeInvariant (node kp ⟪ Black , vp ⟫ t₂ (node kg ⟪ Red , vg ⟫ t uncle))
|
|
|
1062 RB-repl→ti-lem10 = ?
|
|
|
1063
|
|
|
1064 RB-repl→ti-lem11 : {n : Level} {A : Set n} {key : ℕ} {value : A} → {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
|
|
|
1065 (x : color t₂ ≡ Red) (x₁ : kp < key) (rbt : replacedRBTree key value t₁ t₂) →
|
|
|
1066 (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t t₁)) →
|
|
|
1067 treeInvariant (node kp ⟪ Black , vp ⟫ (node kg ⟪ Red , vg ⟫ uncle t) t₂)
|
|
|
1068 RB-repl→ti-lem11 = ?
|
|
|
1069
|
|
|
1070 RB-repl→ti-lem12 : {n : Level} {A : Set n} {key : ℕ} {value : A} → {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} (x : color t₃ ≡ Black)
|
|
|
1071 (x₁ : kp < key) (x₂ : key < kg) (rbt : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) →
|
|
|
1072 (treeInvariant t₁ → treeInvariant (node kn ⟪ Red , vn ⟫ t₂ t₃)) → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁) uncle) →
|
|
|
1073 treeInvariant (node kn ⟪ Black , vn ⟫ (node kp ⟪ Red , vp ⟫ t t₂) (node kg ⟪ Red , vg ⟫ t₃ uncle))
|
|
|
1074 RB-repl→ti-lem12 = ?
|
|
|
1075
|
|
|
1076 RB-repl→ti-lem13 : {n : Level} {A : Set n} {key : ℕ} {value : A} → {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} (x : color t₃ ≡ Black)
|
|
|
1077 (x₁ : kg < key) (x₂ : key < kp) (rbt : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) →
|
|
|
1078 (treeInvariant t₁ → treeInvariant (node kn ⟪ Red , vn ⟫ t₂ t₃)) → treeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t₁ t)) →
|
|
|
1079 treeInvariant (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , vg ⟫ uncle t₂) (node kp ⟪ Red , vp ⟫ t₃ t))
|
|
|
1080 RB-repl→ti-lem13 = ?
|
|
|
1081
|
|
|
1082
|
|
|
1083 RB-repl→ti : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A) ) → (key : ℕ ) → (value : A) → treeInvariant tree
|
|
|
1084 → replacedRBTree key value tree repl → treeInvariant repl
|
|
|
1085 RB-repl→ti {n} {A} tree repl key value ti rbr = RBTI-induction A tree tree repl key value refl rbr {λ key value b a rbr → treeInvariant b → treeInvariant a }
|
|
|
1086 ⟪ lem00 , ⟪ lem01 , ⟪ lem02 , ⟪ RB-repl→ti-lem03 , ⟪ RB-repl→ti-lem04 , ⟪ RB-repl→ti-lem05 ,
|
|
|
1087 ⟪ RB-repl→ti-lem06 , ⟪ RB-repl→ti-lem07 , ⟪ RB-repl→ti-lem08 , ⟪ RB-repl→ti-lem09 , ⟪ RB-repl→ti-lem10 , ⟪ RB-repl→ti-lem11
|
|
|
1088 , ⟪ RB-repl→ti-lem12 , RB-repl→ti-lem13 ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ti where
|
|
|
1089 lem00 : treeInvariant leaf → treeInvariant (node key ⟪ Red , value ⟫ leaf leaf)
|
|
|
1090 lem00 ti = t-single key ⟪ Red , value ⟫
|
|
|
1091 lem01 : (ca : Color) (value₂ : A) (t t₁ : bt (Color ∧ A)) → treeInvariant (node key ⟪ ca , value₂ ⟫ t t₁) → treeInvariant (node key ⟪ ca , value ⟫ t t₁)
|
|
|
1092 lem01 ca v2 t t₁ ti = lem20 (node key ⟪ ca , v2 ⟫ t t₁) ti refl where
|
|
|
1093 lem20 : (tree : bt (Color ∧ A)) → treeInvariant tree → tree ≡ node key ⟪ ca , v2 ⟫ t t₁ → treeInvariant (node key ⟪ ca , value ⟫ t t₁)
|
|
|
1094 lem20 .leaf t-leaf ()
|
|
|
1095 lem20 (node key v3 leaf leaf) (t-single key v3) eq = subst treeInvariant
|
|
|
1096 (node-cong (just-injective (cong node-key eq)) refl (just-injective (cong node-left eq)) (just-injective (cong node-right eq))) (t-single key ⟪ ca , value ⟫)
|
|
|
1097 lem20 (node key _ leaf (node key₁ _ _ _)) (t-right key key₁ x x₁ x₂ ti) eq = subst treeInvariant
|
|
|
1098 (node-cong (just-injective (cong node-key eq)) refl (just-injective (cong node-left eq)) (just-injective (cong node-right eq))) (t-right key key₁ x x₁ x₂ ti)
|
|
|
1099 lem20 (node key₁ _ (node key _ _ _) leaf) (t-left key key₁ x x₁ x₂ ti) eq = subst treeInvariant
|
|
|
1100 (node-cong (just-injective (cong node-key eq)) refl (just-injective (cong node-left eq)) (just-injective (cong node-right eq))) (t-left key key₁ x x₁ x₂ ti)
|
|
|
1101 lem20 (node key₁ _ (node key _ _ _) (node key₂ _ _ _)) (t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) eq = subst treeInvariant
|
|
|
1102 (node-cong (just-injective (cong node-key eq)) refl (just-injective (cong node-left eq)) (just-injective (cong node-right eq)))
|
|
|
1103 (t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁)
|
|
|
1104 lem02 : {k : ℕ} {v1 : A} {ca : Color} {t t1 t2 : bt (Color ∧ A)} (x : color t2 ≡ color t) (x₁ : k < key)
|
|
|
1105 (rbt : replacedRBTree key value t2 t) → (treeInvariant t2 → treeInvariant t) → treeInvariant (node k ⟪ ca , v1 ⟫ t1 t2) → treeInvariant (node k ⟪ ca , v1 ⟫ t1 t)
|
|
|
1106 lem02 {k} {v1} {ca} {t} {t1} {t2} ceq x₁ rbt prev ti = lem21 (node k ⟪ ca , v1 ⟫ t1 t2) ti refl rbt where
|
|
|
1107 lem22 : treeInvariant t
|
|
|
1108 lem22 = prev (treeRightDown _ _ ti)
|
|
|
1109 lem21 : (tree : bt (Color ∧ A)) → treeInvariant tree → tree ≡ node k ⟪ ca , v1 ⟫ t1 t2 → replacedRBTree key value t2 t → treeInvariant (node k ⟪ ca , v1 ⟫ t1 t)
|
|
|
1110 lem21 .leaf t-leaf ()
|
|
|
1111 lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) eq rbr-leaf = subst treeInvariant
|
|
|
1112 (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₁ _ (subst (λ k → k < key) (sym lem23) x₁) tt tt lem22) where
|
|
|
1113 lem23 : k₁ ≡ k
|
|
|
1114 lem23 = just-injective (cong node-key eq)
|
|
|
1115 lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () rbr-node
|
|
|
1116 lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-right x x₁ rbt)
|
|
|
1117 lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-left x x₁ rbt)
|
|
|
1118 lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-black-right x x₁ rbt)
|
|
|
1119 lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-black-left x x₁ rbt)
|
|
|
1120 lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-flip-ll x x₁ x₂ rbt)
|
|
|
1121 lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-flip-lr x x₁ x₂ x₃ rbt)
|
|
|
1122 lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-flip-rl x x₁ x₂ x₃ rbt)
|
|
|
1123 lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-flip-rr x x₁ x₂ rbt)
|
|
|
1124 lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-rotate-ll x x₁ rbt)
|
|
|
1125 lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-rotate-rr x x₁ rbt)
|
|
|
1126 lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-rotate-lr t₂ t₃ kg kp kn x x₁ x₂ rbt)
|
|
|
1127 lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-rotate-rl t₂ t₃ kg kp kn x x₁ x₂ rbt)
|
|
|
1128 lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₄ x₂ ti) eq rbr-leaf = subst treeInvariant
|
|
|
1129 (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ (subst (λ k → k < key) (sym lem23) x₁) tt tt lem22) where
|
|
|
1130 lem23 : k₃ ≡ k
|
|
|
1131 lem23 = just-injective (cong node-key eq)
|
|
|
1132 lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti) eq (rbr-node {_} {_} {left} {right}) = subst treeInvariant
|
|
|
1133 (node-cong lem23 refl (just-injective (cong node-left eq)) refl)
|
|
|
1134 (t-right k₃ _ (subst (λ k → k < key) (sym lem23) x₁) (subst (λ k → tr> k₃ k) lem24 x₁₀) (subst (λ k → tr> k₃ k) lem25 x₂) lem22) where
|
|
|
1135 lem23 : k₃ ≡ k
|
|
|
1136 lem23 = just-injective (cong node-key eq)
|
|
|
1137 lem24 : t₁ ≡ left
|
|
|
1138 lem24 = just-injective (cong node-left (just-injective (cong node-right eq)))
|
|
|
1139 lem25 : t₂ ≡ right
|
|
|
1140 lem25 = just-injective (cong node-right (just-injective (cong node-right eq)))
|
|
|
1141 lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ {_} {_} {left} {right} x x₁₀ x₂ ti) eq (rbr-right {k₂} {_} {_} {t₁} {t₂} {t₃} x₃ x₄ trb) = subst treeInvariant
|
|
|
1142 (node-cong lem23 refl (just-injective (cong node-left eq)) refl)
|
|
|
1143 (t-right k₃ _ (subst (λ k → k₃ < k) lem26 x) (subst (λ k → tr> k₃ k) lem24 x₁₀) rr01 lem22) where
|
|
|
1144 lem23 : k₃ ≡ k
|
|
|
1145 lem23 = just-injective (cong node-key eq)
|
|
|
1146 lem26 : k₁ ≡ k₂
|
|
|
1147 lem26 = just-injective (cong node-key (just-injective (cong node-right eq)))
|
|
|
1148 lem24 : left ≡ t₂
|
|
|
1149 lem24 = just-injective (cong node-left (just-injective (cong node-right eq)))
|
|
|
1150 rr01 : tr> k₃ t₁
|
|
|
1151 rr01 = RB-repl→ti> _ _ _ _ _ trb (<-trans (subst (λ k → k₃ < k ) lem26 x ) x₄ )
|
|
|
1152 (subst (λ j → tr> k₃ j) (just-injective (cong node-right (just-injective (cong node-right eq)))) x₂ )
|
|
|
1153 lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ {_} {_} {left} {right} x x₁₀ x₂ ti) eq (rbr-left {k₂} {_} {_} {t₁} {t₂} {t₃} x₃ x₄ rbt) = subst treeInvariant
|
|
|
1154 (node-cong lem23 refl (just-injective (cong node-left eq)) refl)
|
|
|
1155 (t-right k₃ _ (subst (λ k → k₃ < k) lem26 x) rr02 rr01 lem22) where
|
|
|
1156 lem23 : k₃ ≡ k
|
|
|
1157 lem23 = just-injective (cong node-key eq)
|
|
|
1158 lem26 : k₁ ≡ k₂
|
|
|
1159 lem26 = just-injective (cong node-key (just-injective (cong node-right eq)))
|
|
|
1160 rr01 : tr> k₃ t₃
|
|
|
1161 rr01 = subst (λ k → tr> k₃ k) (just-injective (cong node-right (just-injective (cong node-right eq)))) x₂
|
|
|
1162 rr02 : tr> k₃ t₁
|
|
|
1163 rr02 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁)
|
|
|
1164 (subst (λ j → tr> k₃ j) (just-injective (cong node-left (just-injective (cong node-right eq)))) x₁₀ )
|
|
|
1165 lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ {_} {_} {left} {right} x x₁₀ x₂ ti) eq (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt) = subst treeInvariant
|
|
|
1166 (node-cong lem23 refl (just-injective (cong node-left eq)) refl)
|
|
|
1167 (t-right k₃ _ (subst (λ k → k₃ < k) lem26 x) rr01 rr02 lem22) where
|
|
|
1168 lem23 : k₃ ≡ k
|
|
|
1169 lem23 = just-injective (cong node-key eq)
|
|
|
1170 lem26 : k₁ ≡ k₂
|
|
|
1171 lem26 = just-injective (cong node-key (just-injective (cong node-right eq)))
|
|
|
1172 rr01 : tr> k₃ t₁
|
|
|
1173 rr01 = subst (λ k → tr> k₃ k) (just-injective (cong node-left (just-injective (cong node-right eq)))) x₁₀
|
|
|
1174 rr02 : tr> k₃ t₃
|
|
|
1175 rr02 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁)
|
|
|
1176 (subst (λ k → tr> k₃ k) (just-injective (cong node-right (just-injective (cong node-right eq)))) x₂ )
|
|
|
1177 lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ {_} {_} {left} {right} x x₁₀ x₂ ti) eq (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt) = subst treeInvariant
|
|
|
1178 (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ (subst (λ k → k₃ < k) lem26 x) rr02 rr01 lem22) where
|
|
|
1179 lem23 : k₃ ≡ k
|
|
|
1180 lem23 = just-injective (cong node-key eq)
|
|
|
1181 lem26 : k₁ ≡ k₂
|
|
|
1182 lem26 = just-injective (cong node-key (just-injective (cong node-right eq)))
|
|
|
1183 rr01 : tr> k₃ t₁
|
|
|
1184 rr01 = subst (λ k → tr> k₃ k) (just-injective (cong node-right (just-injective (cong node-right eq)))) x₂
|
|
|
1185 rr02 : tr> k₃ t₃
|
|
|
1186 rr02 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁)
|
|
|
1187 (subst (λ k → tr> k₃ k) (just-injective (cong node-left (just-injective (cong node-right eq)))) x₁₀ )
|
|
|
1188 lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti) eq (rbr-flip-ll x₃ x₄ x₅ rbt) = ⊥-elim ( ⊥-color ceq )
|
|
|
1189 lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti) eq (rbr-flip-lr x₃ x₄ x₅ x₆ rbt) = ⊥-elim ( ⊥-color ceq )
|
|
|
1190 lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti) eq (rbr-flip-rl x₃ x₄ x₅ x₆ rbt) = ⊥-elim ( ⊥-color ceq )
|
|
|
1191 lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti) eq (rbr-flip-rr x₃ x₄ x₅ rbt) = ⊥-elim ( ⊥-color ceq )
|
|
|
1192 lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ {_} {_} {left} {right} x x₁₀ x₂ ti₁) eq (rbr-rotate-ll {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt)
|
|
|
1193 = subst treeInvariant
|
|
|
1194 (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ lem27 rr02 rr01 lem22) where
|
|
|
1195 lem23 : k₃ ≡ k
|
|
|
1196 lem23 = just-injective (cong node-key eq)
|
|
|
1197 lem27 : k₃ < kp
|
|
|
1198 lem27 = subst (λ k → k < kp) (sym lem23) (<-trans x₁ x₄)
|
|
|
1199 rr04 : (k₃ < kg) ∧ ((k₃ < kp) ∧ tr> k₃ t₁ ∧ tr> k₃ t) ∧ tr> k₃ uncle
|
|
|
1200 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
1201 rr01 : (k₃ < kg) ∧ tr> k₃ t ∧ tr> k₃ uncle
|
|
|
1202 rr01 = ⟪ proj1 rr04 , ⟪ proj2 (proj2 (proj1 (proj2 rr04))) , proj2 (proj2 rr04) ⟫ ⟫
|
|
|
1203 rr02 : tr> k₃ t₂
|
|
|
1204 rr02 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 (proj1 (proj2 rr04))))
|
|
|
1205 lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-rr {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt)
|
|
|
1206 = subst treeInvariant
|
|
|
1207 (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ lem27 rr01 rr02 lem22) where
|
|
|
1208 lem23 : k₃ ≡ k
|
|
|
1209 lem23 = just-injective (cong node-key eq)
|
|
|
1210 rr04 : (k₃ < kg) ∧ tr> k₃ uncle ∧ ((k₃ < kp) ∧ tr> k₃ t ∧ tr> k₃ t₁)
|
|
|
1211 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
1212 lem27 : k₃ < kp
|
|
|
1213 lem27 = proj1 (proj2 (proj2 rr04))
|
|
|
1214 rr01 : (k₃ < kg) ∧ tr> k₃ uncle ∧ tr> k₃ t
|
|
|
1215 rr01 = ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫
|
|
|
1216 rr02 : tr> k₃ t₂
|
|
|
1217 rr02 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 (proj2 (proj2 rr04))))
|
|
|
1218 lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt)
|
|
|
1219 = subst treeInvariant
|
|
|
1220 (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ lem27 rr05 rr06 lem22) where
|
|
|
1221 lem23 : k₃ ≡ k
|
|
|
1222 lem23 = just-injective (cong node-key eq)
|
|
|
1223 rr04 : (k₃ < kg) ∧ ((k₃ < kp) ∧ tr> k₃ t ∧ tr> k₃ t₁) ∧ tr> k₃ uncle
|
|
|
1224 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
1225 rr01 : (k₃ < kn) ∧ tr> k₃ t₂ ∧ tr> k₃ t₃
|
|
|
1226 rr01 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 (proj1 (proj2 rr04))))
|
|
|
1227 lem27 : k₃ < kn
|
|
|
1228 lem27 = proj1 rr01
|
|
|
1229 rr05 : (k₃ < kp) ∧ tr> k₃ t ∧ tr> k₃ t₂
|
|
|
1230 rr05 = ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , proj1 (proj2 rr01) ⟫ ⟫
|
|
|
1231 rr06 : (k₃ < kg) ∧ tr> k₃ t₃ ∧ tr> k₃ uncle
|
|
|
1232 rr06 = ⟪ proj1 rr04 , ⟪ proj2 (proj2 rr01) , proj2 (proj2 rr04) ⟫ ⟫
|
|
|
1233 lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt)
|
|
|
1234 = subst treeInvariant
|
|
|
1235 (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ lem27 rr05 rr06 lem22) where
|
|
|
1236 lem23 : k₃ ≡ k
|
|
|
1237 lem23 = just-injective (cong node-key eq)
|
|
|
1238 rr04 : (k₃ < kg) ∧ tr> k₃ uncle ∧ ( (k₃ < kp) ∧ tr> k₃ t₁ ∧ tr> k₃ t)
|
|
|
1239 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
1240 rr01 : (k₃ < kn) ∧ tr> k₃ t₂ ∧ tr> k₃ t₃
|
|
|
1241 rr01 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 (proj2 (proj2 rr04))) )
|
|
|
1242 lem27 : k₃ < kn
|
|
|
1243 lem27 = proj1 rr01
|
|
|
1244 rr05 : (k₃ < kg) ∧ tr> k₃ uncle ∧ tr> k₃ t₂
|
|
|
1245 rr05 = ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 rr01) ⟫ ⟫
|
|
|
1246 rr06 : (k₃ < kp) ∧ tr> k₃ t₃ ∧ tr> k₃ t
|
|
|
1247 rr06 = ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj2 (proj2 rr01) , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫
|
|
|
1248 lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti₁) eq rbr-leaf = subst treeInvariant
|
|
|
1249 (node-cong lem23 refl (just-injective (cong node-left eq)) refl)
|
|
|
1250 (t-node _ _ _ x (subst (λ j → j < key) (sym lem23) x₁) x₁₀ x₂ tt tt ti₁ (t-single key ⟪ Red , value ⟫)) where
|
|
|
1251 lem23 : k₃ ≡ k
|
|
|
1252 lem23 = just-injective (cong node-key eq)
|
|
|
1253 lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () rbr-node
|
|
|
1254 lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-right x₃ x₄ rbt)
|
|
|
1255 lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-left x₃ x₄ rbt)
|
|
|
1256 lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-black-right x₃ x₄ rbt)
|
|
|
1257 lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-black-left x₃ x₄ rbt)
|
|
|
1258 lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-flip-ll x₃ x₄ x₅ rbt)
|
|
|
1259 lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-flip-lr x₃ x₄ x₅ x₆ rbt)
|
|
|
1260 lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-flip-rl x₃ x₄ x₅ x₆ rbt)
|
|
|
1261 lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-flip-rr x₃ x₄ x₅ rbt)
|
|
|
1262 lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-rotate-ll x₃ x₄ rbt)
|
|
|
1263 lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-rotate-rr x₃ x₄ rbt)
|
|
|
1264 lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-rotate-lr t₂ t₃ kg kp kn x₃ x₄ x₅ rbt)
|
|
|
1265 lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-rotate-rl t₂ t₃ kg kp kn x₃ x₄ x₅ rbt)
|
|
|
1266 lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti ti₁) () rbr-leaf
|
|
|
1267 lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ {_} {_} {_} {t} {t₁} {t₂} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-node {_} {_} {t₃} {t₄})
|
|
|
1268 = subst treeInvariant
|
|
|
1269 (node-cong lem23 refl (just-injective (cong node-left eq)) refl)
|
|
|
1270 (t-node _ _ _ x (subst (λ j → j < key) (sym lem23) x₁) x₂ x₃ (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) ti₁ lem22) where
|
|
|
1271 lem23 : k₁ ≡ k
|
|
|
1272 lem23 = just-injective (cong node-key eq)
|
|
|
1273 rr04 : (k₁ < key) ∧ tr> k₁ t₃ ∧ tr> k₁ t₄
|
|
|
1274 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
1275 lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-right {k₃} {_} {_} {t₁} {t₂} {t₃} x₆ x₇ rbt)
|
|
|
1276 = subst treeInvariant
|
|
|
1277 (node-cong lem23 refl (just-injective (cong node-left eq)) refl)
|
|
|
1278 (t-node _ _ _ x (proj1 rr04) x₂ x₃ (proj1 (proj2 rr04)) rr05 ti₁ lem22) where
|
|
|
1279 lem23 : k₁ ≡ k
|
|
|
1280 lem23 = just-injective (cong node-key eq)
|
|
|
1281 rr04 : (k₁ < k₃) ∧ tr> k₁ t₂ ∧ tr> k₁ t₃
|
|
|
1282 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
|
|
|
1283 rr05 : tr> k₁ t₁
|
|
|
1284 rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 rr04))
|
|
|
1285 lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-left {k₃} {_} {_} {t₁} {t₂} {t₃} x₆ x₇ rbt)
|
|
|
1286 = subst treeInvariant
|
|
|
1287 (node-cong lem23 refl (just-injective (cong node-left eq)) refl)
|
|
|
1288 (t-node _ _ _ x (proj1 rr04) x₂ x₃ rr05 (proj2 (proj2 rr04)) ti₁ lem22) where
|
|
|
1289 lem23 : k₁ ≡ k
|
|
|
1290 lem23 = just-injective (cong node-key eq)
|
|
|
1291 rr04 : (k₁ < k₃) ∧ tr> k₁ t₂ ∧ tr> k₁ t₃
|
|
|
1292 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti ))
|
|
|
1293 rr05 : tr> k₁ t₁
|
|
|
1294 rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 rr04))
|
|
|
1295 lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-black-right {t₁} {t₂} {t₃} {_} {k₃} x₆ x₇ rbt)
|
|
|
1296 = subst treeInvariant
|
|
|
1297 (node-cong lem23 refl (just-injective (cong node-left eq)) refl)
|
|
|
1298 (t-node _ _ _ x (proj1 rr04) x₂ x₃ (proj1 (proj2 rr04)) rr05 ti₁ lem22) where
|
|
|
1299 lem23 : k₁ ≡ k
|
|
|
1300 lem23 = just-injective (cong node-key eq)
|
|
|
1301 rr04 : (k₁ < k₃) ∧ tr> k₁ t₁ ∧ tr> k₁ t₂
|
|
|
1302 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti ))
|
|
|
1303 rr05 : tr> k₁ t₃
|
|
|
1304 rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 rr04))
|
|
|
1305 lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-black-left {t₁} {t₂} {t₃} {_} {k₃} x₆ x₇ rbt)
|
|
|
1306 = subst treeInvariant
|
|
|
1307 (node-cong lem23 refl (just-injective (cong node-left eq)) refl)
|
|
|
1308 (t-node _ _ _ x (proj1 rr04) x₂ x₃ rr05 (proj2 (proj2 rr04)) ti₁ lem22) where
|
|
|
1309 lem23 : k₁ ≡ k
|
|
|
1310 lem23 = just-injective (cong node-key eq)
|
|
|
1311 rr04 : (k₁ < k₃) ∧ tr> k₁ t₂ ∧ tr> k₁ t₁
|
|
|
1312 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti ))
|
|
|
1313 rr05 : tr> k₁ t₃
|
|
|
1314 rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 rr04))
|
|
|
1315 lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti ti₁) eq (rbr-flip-ll x₆ x₇ x₈ rbt) = ⊥-elim ( ⊥-color ceq )
|
|
|
1316 lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti ti₁) eq (rbr-flip-lr x₆ x₇ x₈ x₉ rbt) = ⊥-elim ( ⊥-color ceq )
|
|
|
1317 lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti ti₁) eq (rbr-flip-rl x₆ x₇ x₈ x₉ rbt) = ⊥-elim ( ⊥-color ceq )
|
|
|
1318 lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti ti₁) eq (rbr-flip-rr x₆ x₇ x₈ rbt) = ⊥-elim ( ⊥-color ceq )
|
|
|
1319 lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} x₆ x₇ rbt)
|
|
|
1320 = subst treeInvariant
|
|
|
1321 (node-cong lem23 refl (just-injective (cong node-left eq)) refl)
|
|
|
1322 (t-node _ _ _ x (proj1 (proj1 (proj2 rr04))) x₂ x₃ rr05 ⟪ proj1 rr04 , ⟪ proj2 (proj2 (proj1 (proj2 rr04))) , proj2 (proj2 rr04) ⟫ ⟫ ti₁ lem22) where
|
|
|
1323 lem23 : k₁ ≡ k
|
|
|
1324 lem23 = just-injective (cong node-key eq)
|
|
|
1325 rr04 : (k₁ < kg) ∧ ((k₁ < kp) ∧ tr> k₁ t₂ ∧ tr> k₁ t₁) ∧ tr> k₁ uncle
|
|
|
1326 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti ))
|
|
|
1327 rr05 : tr> k₁ t₃
|
|
|
1328 rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 (proj1 (proj2 rr04))))
|
|
|
1329 lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-rr {t₁} {t₂} {t₃} {uncle} {kg} {kp} x₆ x₇ rbt)
|
|
|
1330 = subst treeInvariant
|
|
|
1331 (node-cong lem23 refl (just-injective (cong node-left eq)) refl)
|
|
|
1332 (t-node _ _ _ x (proj1 (proj2 (proj2 rr04))) x₂ x₃ ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ rr05 ti₁ lem22) where
|
|
|
1333 lem23 : k₁ ≡ k
|
|
|
1334 lem23 = just-injective (cong node-key eq)
|
|
|
1335 rr04 : (k₁ < kg) ∧ tr> k₁ uncle ∧ ((k₁ < kp) ∧ tr> k₁ t₁ ∧ tr> k₁ t₂)
|
|
|
1336 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti ))
|
|
|
1337 rr05 : tr> k₁ t₃
|
|
|
1338 rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 (proj2 (proj2 rr04))))
|
|
|
1339 lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₆ x₇ x₈ rbt)
|
|
|
1340 = subst treeInvariant
|
|
|
1341 (node-cong lem23 refl (just-injective (cong node-left eq)) refl)
|
|
|
1342 (t-node _ _ _ x (proj1 rr05) x₂ x₃ ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , proj1 (proj2 rr05) ⟫ ⟫
|
|
|
1343 ⟪ proj1 rr04 , ⟪ proj2 (proj2 rr05) , proj2 (proj2 rr04) ⟫ ⟫ ti₁ lem22) where
|
|
|
1344 lem23 : k₁ ≡ k
|
|
|
1345 lem23 = just-injective (cong node-key eq)
|
|
|
1346 rr04 : (k₁ < kg) ∧ ((k₁ < kp) ∧ tr> k₁ t ∧ tr> k₁ t₁) ∧ tr> k₁ uncle
|
|
|
1347 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti ))
|
|
|
1348 rr05 : (k₁ < kn) ∧ tr> k₁ t₂ ∧ tr> k₁ t₃
|
|
|
1349 rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 (proj1 (proj2 rr04))))
|
|
|
1350 lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₆ x₇ x₈ rbt)
|
|
|
1351 = subst treeInvariant
|
|
|
1352 (node-cong lem23 refl (just-injective (cong node-left eq)) refl)
|
|
|
1353 (t-node _ _ _ x (proj1 rr05) x₂ x₃ ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 rr05) ⟫ ⟫
|
|
|
1354 ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj2 (proj2 rr05) , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ ti₁ lem22) where
|
|
|
1355 lem23 : k₁ ≡ k
|
|
|
1356 lem23 = just-injective (cong node-key eq)
|
|
|
1357 rr04 : (k₁ < kg) ∧ tr> k₁ uncle ∧ ((k₁ < kp) ∧ tr> k₁ t₁ ∧ tr> k₁ t)
|
|
|
1358 rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti ))
|
|
|
1359 rr05 : (k₁ < kn) ∧ tr> k₁ t₂ ∧ tr> k₁ t₃
|
|
|
1360 rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 (proj2 (proj2 rr04))))
|
|
|
1361
|
