Mercurial > hg > Gears > GearsAgda
changeset 955:415915a840fe
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 18 Oct 2024 21:03:55 +0900 |
| parents | 08281092430b |
| children | bfc7007177d0 |
| files | RBTree.agda RBTree1.agda |
| diffstat | 2 files changed, 471 insertions(+), 1302 deletions(-) [+] |
line wrap: on
line diff
--- a/RBTree.agda Sun Oct 06 17:59:51 2024 +0900 +++ b/RBTree.agda Fri Oct 18 21:03:55 2024 +0900 @@ -79,40 +79,6 @@ -- findRBTreeTest = findTest 14 testRBTree0 testRBI0 -- $ λ tr s P O → (record {tree = tr ; stack = s ; ti = (proj1 P) ; si = (proj2 P)}) - -PGtoRBinvariant1 : {n : Level} {A : Set n} - → (tree orig : bt (Color ∧ A) ) - → {key : ℕ } - → (rb : RBtreeInvariant orig) - → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) - → RBtreeInvariant tree -PGtoRBinvariant1 tree .tree rb .(tree ∷ []) s-nil = rb -PGtoRBinvariant1 tree orig rb = {!!} - --- --- if we consider tree invariant, this may be much simpler and faster --- -stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A ) - → (stack : List (bt A)) → stackInvariant key tree orig stack - → ( stack ≡ orig ∷ [] ) ∨ ( stack ≡ tree ∷ orig ∷ [] ) ∨ PG A key tree stack -stackToPG {n} {A} {key} = ? - -stackCase1 : {n : Level} {A : Set n} → {key : ℕ } → {tree orig : bt A } - → {stack : List (bt A)} → stackInvariant key tree orig stack - → stack ≡ orig ∷ [] → tree ≡ orig -stackCase1 = ? - -pg-prop-1 : {n : Level} (A : Set n) → (key : ℕ) → (tree orig : bt A ) - → (stack : List (bt A)) → (pg : PG A key tree stack) - → (¬ PG.grand pg ≡ leaf ) ∧ (¬ PG.parent pg ≡ leaf) -pg-prop-1 {_} A _ tree orig stack pg with PG.pg pg -... | s2-s1p2 _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫ -... | s2-1sp2 _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫ -... | s2-s12p _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫ -... | s2-1s2p _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫ - - - -- -- create RBT invariant after findRBT, continue to replaceRBT --
--- a/RBTree1.agda Sun Oct 06 17:59:51 2024 +0900 +++ b/RBTree1.agda Fri Oct 18 21:03:55 2024 +0900 @@ -1,4 +1,3 @@ --- {-# OPTIONS --cubical-compatible --safe #-} {-# OPTIONS --allow-unsolved-metas --cubical-compatible #-} module RBTree1 where @@ -28,561 +27,6 @@ open _∧_ -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) - (rbt : replacedRBTree key value t1 t) → (treeInvariant t1 → treeInvariant t) → treeInvariant (node k ⟪ ca , v1 ⟫ t1 t2) → treeInvariant (node k ⟪ ca , v1 ⟫ t t2) -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 - lem22 : treeInvariant t - lem22 = prev (treeLeftDown _ _ ti) - 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) - lem21 .leaf t-leaf () rbt - lem21 .(node k₃ value₁ leaf leaf) (t-single k₃ value₁) eq rbr-leaf = subst treeInvariant - (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 - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - lem21 .(node key value leaf leaf) (t-single key value) () rbr-node - lem21 .(node key value leaf leaf) (t-single key value) () (rbr-right x x₁ rbt) - lem21 .(node key value leaf leaf) (t-single key value) () (rbr-left x x₁ rbt) - lem21 .(node key value leaf leaf) (t-single key value) () (rbr-black-right x x₁ rbt) - lem21 .(node key value leaf leaf) (t-single key value) () (rbr-black-left x x₁ rbt) - lem21 .(node key value leaf leaf) (t-single key value) () (rbr-flip-ll x x₁ x₂ rbt) - lem21 .(node key value leaf leaf) (t-single key value) () (rbr-flip-lr x x₁ x₂ x₃ rbt) - lem21 .(node key value leaf leaf) (t-single key value) () (rbr-flip-rl x x₁ x₂ x₃ rbt) - lem21 .(node key value leaf leaf) (t-single key value) () (rbr-flip-rr x x₁ x₂ rbt) - lem21 .(node key value leaf leaf) (t-single key value) () (rbr-rotate-ll x x₁ rbt) - lem21 .(node key value leaf leaf) (t-single key value) () (rbr-rotate-rr x x₁ rbt) - lem21 .(node key value leaf leaf) (t-single key value) () (rbr-rotate-lr t₂ t₃ kg kp kn x x₁ x₂ rbt) - lem21 .(node key value leaf leaf) (t-single key value) () (rbr-rotate-rl t₂ t₃ kg kp kn x x₁ x₂ rbt) - lem21 .(node k₄ _ leaf (node k₃ _ _ _)) (t-right k₄ k₃ x x₁₀ x₂ ti₁) eq rbr-leaf = subst treeInvariant - (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 - lem23 : k₄ ≡ k - lem23 = just-injective (cong node-key eq ) - lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () rbr-node - lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-right x₃ x₄ rbt) - lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-left x₃ x₄ rbt) - lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-black-right x₃ x₄ rbt) - lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-black-left x₃ x₄ rbt) - lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-ll x₃ x₄ x₅ rbt) - lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-lr x₃ x₄ x₅ x₆ rbt) - lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-rl x₃ x₄ x₅ x₆ rbt) - lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-rr x₃ x₄ x₅ rbt) - lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-rotate-ll x₃ x₄ rbt) - lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-rotate-rr x₃ x₄ rbt) - 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) - 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) - lem21 (node k₄ _ (node k₃ _ t₁ t₂) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-node {_} {_} {t₃} {t₄} ) = subst treeInvariant - (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 - lem23 : k₄ ≡ k - lem23 = just-injective (cong node-key eq ) - rr04 : (key < k₄) ∧ tr< k₄ t₃ ∧ tr< k₄ t₄ - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - 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 - (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 rr04) (proj1 (proj2 rr04)) rr02 lem22 ) where - lem23 : k₄ ≡ k - lem23 = just-injective (cong node-key eq ) - rr04 : (k₁ < k₄) ∧ tr< k₄ t₄ ∧ tr< k₄ t₅ - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr02 : tr< k₄ t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj2 (proj2 rr04)) - 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 - (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 rr04) rr02 (proj2 (proj2 rr04)) lem22 ) where - lem23 : k₄ ≡ k - lem23 = just-injective (cong node-key eq ) - rr04 : (k₁ < k₄) ∧ tr< k₄ t₄ ∧ tr< k₄ t₅ - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr02 : tr< k₄ t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj1 (proj2 rr04)) - 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 - (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 rr04) (proj1 (proj2 rr04)) rr02 lem22 ) where - lem23 : k₄ ≡ k - lem23 = just-injective (cong node-key eq ) - rr04 : (k₂ < k₄) ∧ tr< k₄ t₁ ∧ tr< k₄ t₂ - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr02 : tr< k₄ t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj2 (proj2 rr04)) - 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 - (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 rr04) rr02 (proj2 (proj2 rr04)) lem22 ) where - lem23 : k₄ ≡ k - lem23 = just-injective (cong node-key eq ) - rr04 : (k₂ < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₁ - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr02 : tr< k₄ t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj1 (proj2 rr04)) - 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) - 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) - 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) - 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) - 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 - (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 (proj1 (proj2 rr04))) rr02 - ⟪ proj1 rr04 , ⟪ proj2 (proj2 (proj1 (proj2 rr04))) , proj2 (proj2 rr04) ⟫ ⟫ lem22 ) where - lem23 : k₄ ≡ k - lem23 = just-injective (cong node-key eq ) - rr04 : (kg < k₄) ∧ ((kp < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₁ ) ∧ tr< k₄ uncle - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr02 : tr< k₄ t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj1 (proj2 (proj1 (proj2 rr04)))) - 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 - (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 (proj2 (proj2 rr04))) - ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ rr02 lem22 ) where - lem23 : k₄ ≡ k - lem23 = just-injective (cong node-key eq ) - rr04 : (kg < k₄) ∧ tr< k₄ uncle ∧ ((kp < k₄) ∧ tr< k₄ t₁ ∧ tr< k₄ t₂) - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr02 : tr< k₄ t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj2 (proj2 (proj2 (proj2 rr04)))) - 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 - (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 rr02) - ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , proj1 (proj2 rr02) ⟫ ⟫ ⟪ proj1 rr04 , ⟪ proj2 (proj2 rr02) , proj2 (proj2 rr04) ⟫ ⟫ lem22 ) where - lem23 : k₄ ≡ k - lem23 = just-injective (cong node-key eq ) - rr04 : (kg < k₄) ∧ ((kp < k₄) ∧ tr< k₄ t ∧ tr< k₄ t₁) ∧ tr< k₄ uncle - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr02 : (kn < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj2 (proj2 (proj1 (proj2 rr04)))) - 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 - (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 rr02) - ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 rr02) ⟫ ⟫ ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj2 (proj2 rr02) , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ lem22 ) where - lem23 : k₄ ≡ k - lem23 = just-injective (cong node-key eq ) - rr04 : (kg < k₄) ∧ tr< k₄ uncle ∧ ((kp < k₄) ∧ tr< k₄ t₁ ∧ tr< k₄ t) - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr02 : (kn < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj1 (proj2 (proj2 (proj2 rr04)))) - 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 - (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 - lem23 : k₄ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (key < k₄) ∧ tr< k₄ t₃ ∧ tr< k₄ t₄ - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - 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 - (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 - lem23 : k₄ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₁ < k₄) ∧ tr< k₄ t₄ ∧ tr< k₄ t₅ - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr02 : tr< k₄ t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj2 (proj2 rr04)) - 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 - (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 - lem23 : k₄ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₁ < k₄) ∧ tr< k₄ t₄ ∧ tr< k₄ t₅ - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr02 : tr< k₄ t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj1 (proj2 rr04)) - 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 - (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 - lem23 : k₄ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₂ < k₄) ∧ tr< k₄ t₁ ∧ tr< k₄ t₂ - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr02 : tr< k₄ t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj2 (proj2 rr04)) - 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 - (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 - lem23 : k₄ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₂ < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₁ - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr02 : tr< k₄ t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj1 (proj2 rr04)) - 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) - 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) - 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) - 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) - 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 - (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 (proj1 (proj2 rr04))) x₁₀ rr02 - ⟪ proj1 rr04 , ⟪ proj2 (proj2 (proj1 (proj2 rr04))) , proj2 (proj2 rr04) ⟫ ⟫ x₄ x₅ lem22 ti₂) where - lem23 : k₄ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (kg < k₄) ∧ ((kp < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₁) ∧ tr< k₄ uncle - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr02 : tr< k₄ t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj1 (proj2 (proj1 (proj2 rr04)))) - 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 - (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 (proj2 (proj2 rr04))) x₁₀ - ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ rr02 x₄ x₅ lem22 ti₂) where - lem23 : k₄ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (kg < k₄) ∧ tr< k₄ uncle ∧ ((kp < k₄) ∧ tr< k₄ t₁ ∧ tr< k₄ t₂) - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr02 : tr< k₄ t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj2 (proj2 (proj2 (proj2 rr04)))) - 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 - (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr02) x₁₀ - ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , proj1 (proj2 rr02) ⟫ ⟫ ⟪ proj1 rr04 , ⟪ proj2 (proj2 rr02) , proj2 (proj2 rr04) ⟫ ⟫ - x₄ x₅ lem22 ti₂) where - lem23 : k₄ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (kg < k₄) ∧ ((kp < k₄) ∧ tr< k₄ t ∧ tr< k₄ t₁) ∧ tr< k₄ uncle - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr02 : (kn < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj2 (proj2 (proj1 (proj2 rr04)))) - 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 - (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr02) x₁₀ - ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 rr02) ⟫ ⟫ ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj2 (proj2 rr02) , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ - x₄ x₅ lem22 ti₂) where - lem23 : k₄ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (kg < k₄) ∧ tr< k₄ uncle ∧ ((kp < k₄) ∧ tr< k₄ t₁ ∧ tr< k₄ t) - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr02 : (kn < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj1 (proj2 (proj2 (proj2 rr04)))) - -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) - (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) - → treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₂) -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 - lem22 : treeInvariant t2 - lem22 = prev (treeRightDown _ _ ti) - 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) - lem21 _ t-leaf () rbt - 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) - lem21 _ (t-single key value) () (rbr-node {_} {_} {t₃} {t₄}) - lem21 _ (t-single key value) () (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) - lem21 _ (t-single key value) () (rbr-left {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) - lem21 _ (t-single key value) () (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt) - lem21 _ (t-single key value) () (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt) - lem21 _ (t-single key value) () (rbr-flip-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) - lem21 _ (t-single key value) () (rbr-flip-lr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt) - lem21 _ (t-single key value) () (rbr-flip-rl {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt) - lem21 _ (t-single key value) () (rbr-flip-rr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) - lem21 _ (t-single key value) () (rbr-rotate-ll {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) - lem21 _ (t-single key value) () (rbr-rotate-rr {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) - lem21 _ (t-single key value) () (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) - lem21 _ (t-single key value) () (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) - lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) () rbr-leaf - lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-node {_} {_} {t₃} {t₄}) = subst treeInvariant - (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ x₁ (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) lem22) where - rr04 : (k < _ ) ∧ tr> k t₃ ∧ tr> k t₄ - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) = subst treeInvariant - (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04) (proj1 (proj2 rr04)) rr02 lem22) where - rr04 : (k < k₁ ) ∧ tr> k t₄ ∧ tr> k t₅ - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr> k t₃ - rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 rr04)) - lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-left {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) = subst treeInvariant - (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04) rr02 (proj2 (proj2 rr04)) lem22) where - rr04 : (k < k₁) ∧ tr> k t₄ ∧ tr> k t₅ - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr> k t₃ - rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 rr04)) - lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt) = subst treeInvariant - (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04) (proj1 (proj2 rr04)) rr02 lem22) where - rr04 : (k < k₂) ∧ tr> k t₁ ∧ tr> k t₂ - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr> k t₃ - rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 rr04)) - lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt) = subst treeInvariant - (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04) rr02 (proj2 (proj2 rr04)) lem22) where - rr04 : (k < k₂) ∧ tr> k t₂ ∧ tr> k t₁ - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr> k t₃ - rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 rr04)) - 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 - (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04) - ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ rr02 , proj2 (proj2 (proj1 (proj2 rr04))) ⟫ ⟫ (tr>-to-black (proj2 (proj2 rr04))) lem22) where - rr04 : (k < kg) ∧ ((k < kp) ∧ tr> k t₂ ∧ tr> k t₁) ∧ tr> k uncle - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr> k t₃ - rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj1 (proj2 rr04))) ) - 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 - (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04) - ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , rr02 ⟫ ⟫ (tr>-to-black (proj2 (proj2 rr04))) lem22) where - rr04 : (k < kg) ∧ ((k < kp) ∧ tr> k t₁ ∧ tr> k t₂) ∧ tr> k uncle - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr> k t₃ - rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj1 (proj2 rr04)))) - 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 - (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04) - (tr>-to-black (proj1 (proj2 rr04))) ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ rr02 , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ lem22) where - rr04 : (k < kg) ∧ tr> k uncle ∧ ((k < kp) ∧ tr> k t₂ ∧ tr> k t₁) - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr> k t₃ - rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj2 (proj2 rr04))) ) - 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 - (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04) - (tr>-to-black (proj1 (proj2 rr04))) ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj1 (proj2 (proj2 (proj2 rr04))) , rr02 ⟫ ⟫ lem22) where - rr04 : (k < kg) ∧ tr> k uncle ∧ ((k < kp) ∧ tr> k t₁ ∧ tr> k t₂) - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr> k t₃ - rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj2 (proj2 rr04))) ) - 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) - 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) - 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) - 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) - 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) - (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 - lem23 : key₁ ≡ k - lem23 = just-injective (cong node-key eq) - lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) eq (rbr-node {_} {_} {t₃} {t₄}) = subst treeInvariant - (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₂ < j ) lem23 x) x₁ - (subst (λ k → tr< k t₁) lem23 x₁₀) (subst (λ k → tr< k t₂) lem23 x₂) (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) ti₁ lem22) where - lem23 : key₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k < key) ∧ tr> k t₃ ∧ tr> k t₄ - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) () (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) - lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) () (rbr-left {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) - lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) () (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt) - lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) () (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt) - 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) - 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) - 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) - 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) - 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) - 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) - 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) - 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) - lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) () rbr-leaf - 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 - (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) x₁ - (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃) (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) ti₁ lem22) where - lem23 : key₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k < key ) ∧ tr> k t₃ ∧ tr> k t₄ - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - 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 - (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) (proj1 rr04) - (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃) (proj1 (proj2 rr04)) rr02 ti₁ lem22) where - lem23 : key₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k < k₃) ∧ tr> k t₄ ∧ tr> k t₅ - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr> k t₃ - rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 rr04)) - 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 - (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) (proj1 rr04) - (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃) rr02 (proj2 (proj2 rr04)) ti₁ lem22) where - lem23 : key₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k < k₃) ∧ tr> k t₄ ∧ tr> k t₅ - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr> k t₃ - rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 rr04)) - 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) - 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) - 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) - = subst treeInvariant - (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) (proj1 rr04) - (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃) - ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ rr02 , proj2 (proj2 (proj1 (proj2 rr04))) ⟫ ⟫ ( tr>-to-black (proj2 (proj2 rr04))) ti₁ lem22) where - lem23 : key₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k < kg) ∧ ((k < kp) ∧ tr> k t₁ ∧ tr> k t) ∧ tr> k uncle - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr> k t₂ - rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj1 (proj2 rr04))) ) - 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) - = subst treeInvariant - (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) (proj1 rr04) - (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃) - ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , rr02 ⟫ ⟫ ( tr>-to-black (proj2 (proj2 rr04))) ti₁ lem22) where - lem23 : key₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k < kg) ∧ ((k < kp) ∧ tr> k t ∧ tr> k t₁) ∧ tr> k uncle - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr> k t₂ - rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj1 (proj2 rr04))) ) - 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) - = subst treeInvariant - (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) (proj1 rr04) - (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃) - (tr>-to-black (proj1 (proj2 rr04))) ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ rr02 , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ ti₁ lem22) where - lem23 : key₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k < kg) ∧ tr> k uncle ∧ ((k < kp) ∧ tr> k t₁ ∧ tr> k t) - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr> k t₂ - rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj2 (proj2 rr04))) ) - 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) - = subst treeInvariant - (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) (proj1 rr04) - (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃) - (tr>-to-black (proj1 (proj2 rr04))) ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj1 (proj2 (proj2 (proj2 rr04))) , rr02 ⟫ ⟫ ti₁ lem22) where - lem23 : key₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k < kg) ∧ tr> k uncle ∧ ((k < kp) ∧ tr> k t ∧ tr> k t₁) - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr> k t₂ - rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj2 (proj2 rr04))) ) - 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) - 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) - 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) - 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) - -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₁) - (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t₁ t) - → treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t₂ t) -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 - lem22 : treeInvariant t2 - lem22 = prev (treeLeftDown _ _ ti ) - 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) - lem21 _ t-leaf () rbt - 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) - lem21 _ (t-single key value) () (rbr-node {_} {_} {t₃} {t₄}) - lem21 _ (t-single key value) () (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) - lem21 _ (t-single key value) () (rbr-left {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) - lem21 _ (t-single key value) () (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt) - lem21 _ (t-single key value) () (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt) - lem21 _ (t-single key value) () (rbr-flip-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) - lem21 _ (t-single key value) () (rbr-flip-lr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt) - lem21 _ (t-single key value) () (rbr-flip-rl {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt) - lem21 _ (t-single key value) () (rbr-flip-rr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) - lem21 _ (t-single key value) () (rbr-rotate-ll {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) - lem21 _ (t-single key value) () (rbr-rotate-rr {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) - lem21 _ (t-single key value) () (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) - lem21 _ (t-single key value) () (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) - 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)) ) - (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 - lem23 : key₂ ≡ k - lem23 = just-injective (cong node-key eq) - lem21 _ (t-right key₂ key₁ {v1} {v2} {t} {t₁} x x₁₀ x₂ ti₁) () (rbr-node {_} {_} {t₃} {t₄}) - lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) - lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-left {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) - lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt) - lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt) - lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) - 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) - 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) - lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-rr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) - 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) - 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) - 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) - 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) - lem21 _ (t-left key₂ key₁ {_} {_} {t} {t₁} x x₁₀ x₂ ti₁) () rbr-leaf - lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) eq (rbr-node {_} {_} {t₃} {t₄}) = subst treeInvariant - (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) lem22 ) where - rr04 : (key < k) ∧ tr< k t₃ ∧ tr< k t₄ - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) eq (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) = subst treeInvariant - (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) rr02 lem22 ) where - rr04 : (k₁ < k) ∧ tr< k t₄ ∧ tr< k t₅ - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr< k t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 rr04)) - lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) eq (rbr-left {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) = subst treeInvariant - (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) rr02 (proj2 (proj2 rr04)) lem22 ) where - rr04 : (k₁ < k) ∧ tr< k t₄ ∧ tr< k t₅ - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr< k t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 rr04)) - 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) - 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) - 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 - (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) ⟪ proj1 (proj1 (proj2 rr04)) , - ⟪ rr02 , proj2 (proj2 (proj1 (proj2 rr04))) ⟫ ⟫ (tr<-to-black (proj2 (proj2 rr04))) lem22 ) where - rr04 : (kg < k) ∧ ((kp < k) ∧ tr< k t₂ ∧ tr< k t₁) ∧ tr< k uncle - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr< k t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj1 (proj2 rr04))) ) - 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 - (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) ⟪ proj1 (proj1 (proj2 rr04)) , - ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , rr02 ⟫ ⟫ (tr<-to-black (proj2 (proj2 rr04))) lem22 ) where - rr04 : (kg < k) ∧ ((kp < k) ∧ tr< k t₁ ∧ tr< k t₂) ∧ tr< k uncle - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr< k t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj1 (proj2 rr04))) ) - 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 - (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) (tr<-to-black (proj1 (proj2 rr04))) - ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ rr02 , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ lem22 ) where - rr04 : (kg < k) ∧ tr< k uncle ∧ ((kp < k) ∧ tr< k t₂ ∧ tr< k t₁) - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr< k t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj2 (proj2 rr04))) ) - 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 - (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) (tr<-to-black (proj1 (proj2 rr04))) - ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj1 (proj2 (proj2 (proj2 rr04))) , rr02 ⟫ ⟫ lem22 ) where - rr04 : (kg < k) ∧ tr< k uncle ∧ ((kp < k) ∧ tr< k t₁ ∧ tr< k t₂) - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr< k t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj2 (proj2 rr04))) ) - 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) - 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) - 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) - 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) - lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) () rbr-leaf - 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 - (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀) - (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) (subst (λ j → tr> j t₁₀) lem23 x₄) (subst (λ j → tr> j t₁₁) lem23 x₅) lem22 ti₂) where - lem23 : key₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (key < k) ∧ tr< k t₃ ∧ tr< k t₄ - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - 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 - (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀) - (proj1 (proj2 rr04)) rr02 (subst (λ k → tr> k t₉) lem23 x₄) (subst (λ k → tr> k t₁₀) lem23 x₅) lem22 ti₂) where - lem23 : key₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₃ < k) ∧ tr< k t₄ ∧ tr< k t₅ - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr< k t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 rr04)) - 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 - (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀) - rr02 (proj2 (proj2 rr04)) (subst (λ k → tr> k t₉) lem23 x₄) (subst (λ k → tr> k t₁₀) lem23 x₅) lem22 ti₂) where - lem23 : key₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₃ < k) ∧ tr< k t₄ ∧ tr< k t₅ - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr< k t₃ - rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 rr04)) - 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) - 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) - 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) - = subst treeInvariant - (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀) - ⟪ 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 - lem23 : key₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (kg < k) ∧ ((kp < k) ∧ tr< k t₁ ∧ tr< k t) ∧ tr< k uncle - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr< k t₂ - rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj1 (proj2 rr04))) ) - 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) - = subst treeInvariant - (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀) - ⟪ 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 - lem23 : key₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (kg < k) ∧ ((kp < k) ∧ tr< k t ∧ tr< k t₁) ∧ tr< k uncle - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr< k t₂ - rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj1 (proj2 rr04))) ) - 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) - = subst treeInvariant - (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀) - (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 - lem23 : key₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (kg < k) ∧ tr< k uncle ∧ ((kp < k) ∧ tr< k t₁ ∧ tr< k t) - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr< k t₂ - rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj2 (proj2 rr04))) ) - 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) - = subst treeInvariant - (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀) - (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 - lem23 : key₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (kg < k) ∧ tr< k uncle ∧ ((kp < k) ∧ tr< k t ∧ tr< k t₁) - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr02 : tr< k t₂ - rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj2 (proj2 rr04))) ) - 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) - 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) - 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) - 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) - - - -to-black-treeInvariant : {n : Level} {A : Set n} → (t : bt (Color ∧ A) ) → treeInvariant t → treeInvariant (to-black t) -to-black-treeInvariant {n} {A} .leaf t-leaf = t-leaf -to-black-treeInvariant {n} {A} .(node key value leaf leaf) (t-single key value) = t-single key _ -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 -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 -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₁ - RB→t2notLeaf : {n : Level} {A : Set n} {key : ℕ} {value : A} → (t₁ t₂ : bt (Color ∧ A) ) → (rbt : replacedRBTree key value t₁ t₂) → IsNode t₂ 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 } RB→t2notLeaf {n} {A} {k} {v} .(node k ⟪ _ , _ ⟫ _ _) .(node k ⟪ _ , v ⟫ _ _) rbr-node = record { key = k ; value = ⟪ _ , v ⟫ ; left = _ ; right = _ ; t=node = refl } @@ -600,762 +44,521 @@ 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 } +tree-construct : {n : Level} (A : Set n) {vg : A} {kg : ℕ} → (uncle t : bt A ) → tr< kg uncle → tr> kg t + → treeInvariant uncle → treeInvariant t → treeInvariant (node kg vg uncle t) +tree-construct A {vg} {kg} uncle t ux tx ui ti with node→leaf∨IsNode t | node→leaf∨IsNode uncle +... | case1 teq | case1 ueq = subst treeInvariant (node-cong refl refl (sym ueq) (sym teq) ) (t-single _ _) +... | case1 teq | case2 un = subst treeInvariant (node-cong refl refl (sym (IsNode.t=node un)) (sym teq) ) (t-left _ _ + (proj1 rr11) (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) (subst treeInvariant (IsNode.t=node un) ui)) where + rr11 : (IsNode.key un < kg ) ∧ tr< kg (IsNode.left un) ∧ tr< kg (IsNode.right un) + rr11 = subst (λ k → tr< kg k) (IsNode.t=node un) ux +... | case2 tn | case1 ueq = subst treeInvariant (node-cong refl refl (sym ueq) (sym (IsNode.t=node tn)) ) (t-right _ _ + (proj1 rr12) (proj1 (proj2 rr12)) (proj2 (proj2 rr12)) (subst treeInvariant (IsNode.t=node tn) ti)) where + rr12 : (kg < IsNode.key tn ) ∧ tr> kg (IsNode.left tn) ∧ tr> kg (IsNode.right tn) + rr12 = subst (λ k → tr> kg k) (IsNode.t=node tn) tx +... | case2 tn | case2 un = subst treeInvariant (node-cong refl refl (sym (IsNode.t=node un)) (sym (IsNode.t=node tn)) ) (t-node _ _ _ + (proj1 rr11) (proj1 rr12) (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) (proj1 (proj2 rr12)) (proj2 (proj2 rr12)) + (subst treeInvariant (IsNode.t=node un) ui) (subst treeInvariant (IsNode.t=node tn) ti)) where + rr11 : (IsNode.key un < kg ) ∧ tr< kg (IsNode.left un) ∧ tr< kg (IsNode.right un) + rr11 = subst (λ k → tr< kg k) (IsNode.t=node un) ux + rr12 : (kg < IsNode.key tn ) ∧ tr> kg (IsNode.left tn) ∧ tr> kg (IsNode.right tn) + rr12 = subst (λ k → tr> kg k) (IsNode.t=node tn) tx + +treeInvariant-to-black : {n : Level} (A : Set n) → {t : bt (Color ∧ A) } → + treeInvariant t → treeInvariant (to-black t) +treeInvariant-to-black A {.leaf} t-leaf = t-leaf +treeInvariant-to-black A {.(node key value leaf leaf)} (t-single key value) = t-single _ _ +treeInvariant-to-black A {.(node key _ leaf (node key₁ _ _ _))} (t-right key key₁ x x₁ x₂ ti) = t-right key key₁ x x₁ x₂ ti +treeInvariant-to-black A {.(node key₁ _ (node key _ _ _) leaf)} (t-left key key₁ x x₁ x₂ ti) = t-left key key₁ x x₁ x₂ ti +treeInvariant-to-black 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₁ + +RB-repl→ti-lem01 : {n : Level} {A : Set n} {key : ℕ} {value : A} (ca : Color) (value₂ : A) (t t₁ : bt (Color ∧ A)) + → treeInvariant (node key ⟪ ca , value₂ ⟫ t t₁) → treeInvariant (node key ⟪ ca , value ⟫ t t₁) +RB-repl→ti-lem01 {n} {A} {key} {value} ca value₂ t t₁ ti = replaceTree1 _ _ _ ti + +RB-repl→ti-lem02 : {n : Level } {A : Set n} {key k : ℕ} {v1 value : A} {ca : Color} {t t1 t2 : bt (Color ∧ A)} (x : color t2 ≡ color t) (x₁ : k < key) (rbt : replacedRBTree key value t2 t) → + (treeInvariant t2 → treeInvariant t) → treeInvariant (node k ⟪ ca , v1 ⟫ t1 t2) → treeInvariant (node k ⟪ ca , v1 ⟫ t1 t) +RB-repl→ti-lem02 {n} {A} {key} {k} {v1} {value} {ca} {t} {t₁} {t₂} ceq x₁ rbt prev ti = lem21 where + rr04 : tr< k t₁ + rr04 = proj1 (ti-property1 ti) + rr02 : tr> k t + rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (ti-property1 ti)) + lem21 : treeInvariant (node k ⟪ ca , v1 ⟫ t₁ t) + lem21 = tree-construct _ _ _ rr04 rr02 (treeLeftDown _ _ ti) (prev (treeRightDown _ _ ti)) + +RB-repl→ti-lem03 : {n : Level} {A : Set n} {key k : ℕ} {value v1 : A} {ca : Color} {t t₁ t₂ : bt (Color ∧ A)} (x : color t₁ ≡ color t) (x₁ : key < k) + (rbt : replacedRBTree key value t₁ t) → (treeInvariant t₁ → treeInvariant t) + → treeInvariant (node k ⟪ ca , v1 ⟫ t₁ t₂) → treeInvariant (node k ⟪ ca , v1 ⟫ t t₂) +RB-repl→ti-lem03 {n} {A} {key} {k} {value} {v1} {ca} {t} {t₁} {t₂} ceq x₁ rbt prev ti = lem21 where + lem22 : treeInvariant t + lem22 = prev (treeLeftDown _ _ ti) + rr04 : tr> k t₂ + rr04 = proj2 (ti-property1 ti) + rr02 : tr< k t + rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (ti-property1 ti)) + lem21 : treeInvariant (node k ⟪ ca , v1 ⟫ t t₂) + lem21 = tree-construct _ _ _ rr02 rr04 lem22 (treeRightDown _ _ ti) + +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) + (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) + → treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₂) +RB-repl→ti-lem04 {n} {A} {key} {value} {t} {t₁} {t₂} {value₁} {key₁} ceq x₁ rbt prev ti = lem21 where + lem22 : treeInvariant t₂ + lem22 = prev (treeRightDown _ _ ti) + rr04 : tr< key₁ t + rr04 = proj1 (ti-property1 ti) + rr02 : tr> key₁ t₂ + rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (ti-property1 ti)) + lem21 : treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₂) + lem21 = tree-construct _ _ _ rr04 rr02 (treeLeftDown _ _ ti) lem22 + +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₁) + (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t₁ t) + → treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t₂ t) +RB-repl→ti-lem05 {n} {A} {key} {value} {t} {t₁} {t₂} {value₁} {key₁} ceq x₁ rbt prev ti = lem21 where + lem22 : treeInvariant t₂ + lem22 = prev (treeLeftDown _ _ ti ) + rr03 : tr< key₁ t₁ + rr03 = proj1 (ti-property1 ti) + rr04 : tr> key₁ t + rr04 = proj2 (ti-property1 ti) + rr02 : tr< key₁ t₂ + rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ rr03 + lem21 : treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t₂ t) + lem21 = tree-construct _ _ _ rr02 rr04 lem22 (treeRightDown _ _ ti) + 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) (x₁ : color uncle ≡ Red) (x₂ : key < kp) (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₁ t) uncle) → treeInvariant (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t₂ t) (to-black uncle)) -RB-repl→ti-lem06 {n} {A} {key} {value} {t} {t1} {t2} {uncle} {kg} {kp} {vg} {vp} ceq ueq x₁ rbt prev ti - = lem21 (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t1 t) uncle) ti refl rbt where - lem22 : treeInvariant t2 +RB-repl→ti-lem06 {n} {A} {key} {value} {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} ceq ueq x₀ rbt prev ti + = lem21 where + lem22 : treeInvariant t₂ lem22 = prev (treeLeftDown _ _ (treeLeftDown _ _ ti )) lem25 : treeInvariant t lem25 = treeRightDown _ _ (treeLeftDown _ _ ti) - lem21 : (tree : bt (Color ∧ A)) → treeInvariant tree → tree ≡ (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t1 t) uncle) → replacedRBTree key value t1 t2 - → treeInvariant (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t2 t) (to-black uncle)) - lem21 _ t-leaf () rbt - lem21 _ (t-single key value) () _ - lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) () _ - 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) ) - (t-left _ _ (proj1 rr04) ⟪ rr07 , ⟪ tt , tt ⟫ ⟫ (proj2 (proj2 rr04)) (subst (λ k → treeInvariant (node kp ⟪ Black , vp ⟫ (node key ⟪ Red , value ⟫ leaf leaf) k )) - (just-injective (cong node-right (just-injective (cong node-left eq)))) (rr05 t₁ refl rr06) )) where - lem24 : leaf ≡ uncle - lem24 = just-injective (cong node-right eq) - lem23 : key₁ ≡ kg - lem23 = just-injective (cong node-key eq) - rr04 : (kp < kg) ∧ ⊤ ∧ tr< kg _ - rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti)) - rr06 : treeInvariant t₁ - rr06 = treeRightDown _ _ ti₁ - rr07 : key < kg - rr07 = <-trans x₁ (proj1 rr04) - rr05 : (tree : bt (Color ∧ A)) → tree ≡ t₁ → treeInvariant tree → treeInvariant (node kp ⟪ Black , vp ⟫ (node key ⟪ Red , value ⟫ leaf leaf) tree) - rr05 .leaf eq₁ t-leaf = t-left _ _ x₁ tt tt (t-single _ _) - 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 - rr08 : (key₂ < key₃) ∧ ⊤ ∧ ⊤ - rr08 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (node-cong refl refl refl (sym eq₁)) ti₁)) - rr09 : kp < key₃ - rr09 = subst (λ k → k < key₃) (just-injective (cong node-key (just-injective (cong node-left eq)))) (proj1 rr08) - 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 - ⟪ <-trans (proj1 rr08) x , ⟪ proj1 (proj2 (proj2 (proj2 rr08))) , proj2 (proj2 (proj2 (proj2 rr08))) ⟫ ⟫ (t-single _ _) ti₃ where - rr08 : (kp < key₃) ∧ ⊤ ∧ ((kp < key₁) ∧ tr> kp t₃ ∧ tr> kp t₄) - 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₁)) - 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 - (proj1 (proj2 rr08)) tt (t-single _ _) ti₃ where - rr08 : (kp < key₁) ∧ ((kp < key₃) ∧ tr> kp t₃ ∧ tr> kp t₄) ∧ ⊤ - 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₁)) - 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₃) - = t-node _ _ _ x₁ (proj1 rr08) tt tt (proj1 (proj2 rr08)) (proj2 (proj2 rr08)) (t-single _ _) ti₄ where - rr08 : (kp < key₁) ∧ ((kp < key₃) ∧ tr> kp t₃ ∧ tr> kp t₄) ∧ ((kp < key₂) ∧ tr> kp t₅ ∧ tr> kp t₆) - 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₁)) - lem21 _ (t-left key₂ key₁ {value₁} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) eq (rbr-node {v₁} {ca} {t₃} {t₄}) = rr05 t refl lem25 where - lem23 : key₁ ≡ kg - lem23 = just-injective (cong node-key eq) - lem24 : leaf ≡ uncle - lem24 = just-injective (cong node-right eq) - rr04 : (kp < kg) ∧ ((key < kg) ∧ tr< kg t₃ ∧ tr< kg t₄) ∧ tr< kg t - rr04 = proj1 (ti-property1 ti) - rr08 : (key < kp) ∧ tr< kp t₃ ∧ tr< kp t₄ - rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti)) - rr05 : (tree : bt (Color ∧ A)) → tree ≡ t → treeInvariant tree - → treeInvariant (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ (node key ⟪ ca , value ⟫ t₃ t₄) t) (to-black uncle)) - rr05 _ eq₁ t-leaf = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁) (subst (λ k → leaf ≡ to-black k ) lem24 refl)) - ( t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) tt (t-left _ _ x₁ (proj1 (proj2 rr08)) (proj2 (proj2 rr08)) lem22 )) - rr05 _ eq₁ (t-single key₃ value) = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁) - (subst (λ k → leaf ≡ to-black k ) lem24 refl)) - ( t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ tt , tt ⟫ ⟫ - (t-node _ _ _ (proj1 rr08) rr10 (proj1 (proj2 rr08)) (proj2 (proj2 rr08)) tt tt lem22 (t-single _ _) )) where - rr09 : (kp < kg) ∧ ((key < kg) ∧ tr< kg t₃ ∧ tr< kg t₄) ∧ ((key₃ < kg) ∧ ⊤ ∧ ⊤ ) - rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node key ⟪ ca , v₁ ⟫ t₃ t₄) k) uncle)) - (sym eq₁) ti)) - rr10 : kp < key₃ - rr10 = proj1 (subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti)))) - rr05 _ eq₁ (t-right key₃ key₁ {_} {_} {t₅} {t₆} y y₁ y₂ ti₁) = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁) - (subst (λ k → leaf ≡ to-black k ) lem24 refl)) - ( t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ tt , proj2 (proj2 (proj2 (proj2 rr09))) ⟫ ⟫ - (t-node _ _ _ (proj1 rr08) rr10 (proj1 (proj2 rr08)) (proj2 (proj2 rr08)) tt - ⟪ <-trans rr10 y , ⟪ <-tr> y₁ rr10 , <-tr> y₂ rr10 ⟫ ⟫ lem22 (t-right _ _ y y₁ y₂ ti₁) )) where - rr09 : (kp < kg) ∧ ((key < kg) ∧ tr< kg t₃ ∧ tr< kg t₄) ∧ ((key₃ < kg) ∧ ⊤ ∧ ( (key₁ < kg) ∧ tr< kg t₅ ∧ tr< kg t₆ ) ) - rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node key ⟪ ca , v₁ ⟫ t₃ t₄) k) uncle)) - (sym eq₁) ti)) - rr10 : kp < key₃ - rr10 = proj1 (subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti)))) - rr05 _ eq₁ (t-left key₃ key₁ {_} {_} {t₅} {t₆} y y₁ y₂ ti₁) = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁) - (subst (λ k → leaf ≡ to-black k ) lem24 refl)) - ( t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ proj1 (proj2 (proj2 (proj2 rr09))) , tt ⟫ ⟫ - (t-node _ _ _ (proj1 rr08) (proj1 rr10) (proj1 (proj2 rr08)) (proj2 (proj2 rr08)) - ⟪ proj1 (proj1 (proj2 rr10)) , ⟪ proj1 (proj2 (proj1 (proj2 rr10))) , proj2 (proj2 (proj1 (proj2 rr10))) ⟫ ⟫ tt lem22 (t-left _ _ y y₁ y₂ ti₁) )) where - rr09 : (kp < kg) ∧ ((key < kg) ∧ tr< kg t₃ ∧ tr< kg t₄) ∧ ((key₁ < kg) ∧ ( (key₃ < kg) ∧ tr< kg t₅ ∧ tr< kg t₆ ) ∧ ⊤ ) - rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node key ⟪ ca , v₁ ⟫ t₃ t₄) k) uncle)) - (sym eq₁) ti)) - rr10 : (kp < key₁ ) ∧ ((kp < key₃) ∧ tr> kp t₅ ∧ tr> kp t₆) ∧ ⊤ - rr10 = subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti))) - rr05 _ eq₁ (t-node key₃ key₁ key₂ {_} {_} {_} {t₅} {t₆} {t₇} {t₈} y y₁ y₂ y₃ y₄ y₅ ti₁ ti₂) - = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁) - (subst (λ k → leaf ≡ to-black k ) lem24 refl)) - ( t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ proj1 (proj2 (proj2 (proj2 rr09))) , proj2 (proj2 (proj2 (proj2 rr09))) ⟫ ⟫ - (t-node _ _ _ (proj1 rr08) (proj1 rr10) (proj1 (proj2 rr08)) (proj2 (proj2 rr08)) - ⟪ proj1 (proj1 (proj2 rr10)) , ⟪ proj1 (proj2 (proj1 (proj2 rr10))) , proj2 (proj2 (proj1 (proj2 rr10))) ⟫ ⟫ (proj2 (proj2 rr10)) lem22 - (t-node _ _ _ y y₁ y₂ y₃ y₄ y₅ ti₁ ti₂))) where - 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₈ ) ) - rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node key ⟪ ca , v₁ ⟫ t₃ t₄) k) uncle)) - (sym eq₁) ti)) - rr10 : (kp < key₁ ) ∧ ((kp < key₃) ∧ tr> kp t₅ ∧ tr> kp t₆) ∧ ((kp < key₂) ∧ tr> kp t₇ ∧ tr> kp t₈) - rr10 = subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti))) - 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 - lem23 : key₁ ≡ kg - lem23 = just-injective (cong node-key eq) - lem24 : leaf ≡ uncle - lem24 = just-injective (cong node-right eq) - rr04 : (kp < kg) ∧ ((k₁ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ tr< kg t - rr04 = proj1 (ti-property1 ti) - rr08 : (k₁ < kp) ∧ tr< kp t₄ ∧ tr< kp t₅ - rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti)) - rr03 : tr< kp t₃ - rr03 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 rr08)) - rr05 : (tree : bt (Color ∧ A)) → tree ≡ t → treeInvariant tree - → treeInvariant (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ (node k₁ ⟪ ca , v₁ ⟫ t₄ t₃) t) (to-black uncle)) - rr05 _ eq₁ t-leaf = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁) (subst (λ k → leaf ≡ to-black k ) lem24 refl)) - ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , >-tr< rr03 (proj1 rr04) ⟫ ⟫ tt - (t-left _ _ (proj1 rr08) (proj1 (proj2 rr08)) rr03 lem22 )) - rr05 _ eq₁ (t-single key₃ value) = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁) - (subst (λ k → leaf ≡ to-black k ) lem24 refl)) - ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , >-tr< rr03 (proj1 rr04) ⟫ ⟫ ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ tt , tt ⟫ ⟫ - (t-node _ _ _ (proj1 rr08) rr10 (proj1 (proj2 rr08)) rr03 tt tt lem22 (t-single _ _) )) where - rr09 : (kp < kg) ∧ ((k₁ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ ((key₃ < kg) ∧ ⊤ ∧ ⊤ ) - rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node k₁ ⟪ ca , v₁ ⟫ t₄ t₅) k) uncle)) - (sym eq₁) ti)) - rr10 : kp < key₃ - rr10 = proj1 (subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti)))) - rr05 _ eq₁ (t-right key₃ key₁ {_} {_} {t₆} {t₇} y y₁ y₂ ti₁) = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁) - (subst (λ k → leaf ≡ to-black k ) lem24 refl)) - ( 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))) ⟫ ⟫ - (t-node _ _ _ (proj1 rr08) rr10 (proj1 (proj2 rr08)) rr03 tt - ⟪ <-trans rr10 y , ⟪ <-tr> y₁ rr10 , <-tr> y₂ rr10 ⟫ ⟫ lem22 (t-right _ _ y y₁ y₂ ti₁) )) where - rr09 : (kp < kg) ∧ ((k₁ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ ((key₃ < kg) ∧ ⊤ ∧ ( (key₁ < kg) ∧ tr< kg t₆ ∧ tr< kg t₇ ) ) - rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node k₁ ⟪ ca , v₁ ⟫ t₄ t₅) k) uncle)) - (sym eq₁) ti)) - rr10 : kp < key₃ - rr10 = proj1 (subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti)))) - rr05 _ eq₁ (t-left key₃ key₁ {_} {_} {t₆} {t₇} y y₁ y₂ ti₁) = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁) - (subst (λ k → leaf ≡ to-black k ) lem24 refl)) - ( 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 ⟫ ⟫ - (t-node _ _ _ (proj1 rr08) (proj1 rr10) (proj1 (proj2 rr08)) rr03 - ⟪ proj1 (proj1 (proj2 rr10)) , ⟪ proj1 (proj2 (proj1 (proj2 rr10))) , proj2 (proj2 (proj1 (proj2 rr10))) ⟫ ⟫ tt lem22 (t-left _ _ y y₁ y₂ ti₁) )) where - rr09 : (kp < kg) ∧ ((k₁ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ ((key₁ < kg) ∧ ( (key₃ < kg) ∧ tr< kg t₆ ∧ tr< kg t₇ ) ∧ ⊤ ) - rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node k₁ ⟪ ca , v₁ ⟫ t₄ t₅) k) uncle)) - (sym eq₁) ti)) - rr10 : (kp < key₁ ) ∧ ((kp < key₃) ∧ tr> kp t₆ ∧ tr> kp t₇) ∧ ⊤ - rr10 = subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti))) - rr05 _ eq₁ (t-node key₃ key₁ key₂ {_} {_} {_} {t₆} {t₇} {t₈} {t₉} y y₁ y₂ y₃ y₄ y₅ ti₁ ti₂) - = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁) - (subst (λ k → leaf ≡ to-black k ) lem24 refl)) - ( 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))) ⟫ ⟫ - (t-node _ _ _ (proj1 rr08) (proj1 rr10) (proj1 (proj2 rr08)) rr03 - ⟪ proj1 (proj1 (proj2 rr10)) , ⟪ proj1 (proj2 (proj1 (proj2 rr10))) , proj2 (proj2 (proj1 (proj2 rr10))) ⟫ ⟫ (proj2 (proj2 rr10)) lem22 - (t-node _ _ _ y y₁ y₂ y₃ y₄ y₅ ti₁ ti₂))) where - 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₉ ) ) - rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node k₁ ⟪ ca , v₁ ⟫ t₄ t₅) k) uncle)) - (sym eq₁) ti)) - rr10 : (kp < key₁ ) ∧ ((kp < key₃) ∧ tr> kp t₆ ∧ tr> kp t₇) ∧ ((kp < key₂) ∧ tr> kp t₈ ∧ tr> kp t₉) - rr10 = subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti))) - lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) eq (rbr-left {k₁} {v₁} {ca} {t₃} {t₄} {t₅} x₃ x₄ rbt) = - subst treeInvariant (node-cong refl refl refl (subst (λ k → leaf ≡ to-black k ) lem24 refl)) - ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04) , ⟪ >-tr< rr03 (proj1 rr04) , proj2 (proj2 (proj1 (proj2 rr04))) ⟫ ⟫ (proj2 (proj2 rr04)) rr06) where - lem23 : key₁ ≡ kg - lem23 = just-injective (cong node-key eq) - lem24 : leaf ≡ uncle - lem24 = just-injective (cong node-right eq) - rr04 : (kp < kg) ∧ ((k₁ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ tr< kg t - rr04 = proj1 (ti-property1 ti) - rr08 : (k₁ < kp) ∧ tr< kp t₄ ∧ tr< kp t₅ - rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti)) - rr03 : tr< kp t₃ - rr03 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 rr08)) - rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node k₁ ⟪ ca , v₁ ⟫ t₃ t₅) t) - rr06 with node→leaf∨IsNode t - ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) rr03 (proj2 (proj2 rr08)) lem22 ) - ... | 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)) - lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where - rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn) - rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti))) - lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt) = - subst treeInvariant (node-cong refl refl refl (subst (λ k → leaf ≡ to-black k ) lem24 refl)) - ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , >-tr< rr03 (proj1 rr04) ⟫ ⟫ (proj2 (proj2 rr04)) rr06) where - lem23 : key₁ ≡ kg - lem23 = just-injective (cong node-key eq) - lem24 : leaf ≡ uncle - lem24 = just-injective (cong node-right eq) - rr04 : (kp < kg) ∧ ((_ < kg) ∧ tr< kg t₁ ∧ tr< kg t₂) ∧ tr< kg t - rr04 = proj1 (ti-property1 ti) - rr08 : (_ < kp) ∧ tr< kp t₁ ∧ tr< kp t₂ - rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti)) - rr03 : tr< kp t₃ - rr03 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 rr08)) - rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node _ ⟪ _ , _ ⟫ t₁ t₃) t) - rr06 with node→leaf∨IsNode t - ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) (proj1 (proj2 rr08)) rr03 lem22 ) - ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) (proj1 (proj2 rr08)) - rr03 (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where - rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn) - rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti))) - lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt) = - subst treeInvariant (node-cong refl refl refl (subst (λ k → leaf ≡ to-black k ) lem24 refl)) - ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04) , ⟪ >-tr< rr03 (proj1 rr04) , proj2 (proj2 (proj1 (proj2 rr04))) ⟫ ⟫ (proj2 (proj2 rr04)) rr06 ) where - lem23 : key₁ ≡ kg - lem23 = just-injective (cong node-key eq) - lem24 : leaf ≡ uncle - lem24 = just-injective (cong node-right eq) - rr04 : (kp < kg) ∧ ((_ < kg) ∧ tr< kg t₂ ∧ tr< kg t₁) ∧ tr< kg t - rr04 = proj1 (ti-property1 ti) - rr08 : (_ < kp) ∧ tr< kp t₂ ∧ tr< kp t₁ - rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti)) - rr03 : tr< kp t₃ - rr03 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 rr08)) - rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node _ ⟪ _ , _ ⟫ t₃ t₁) t) - rr06 with node→leaf∨IsNode t - ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) rr03 (proj2 (proj2 rr08)) lem22 ) - ... | 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)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where - rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn) - rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti))) - 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) - = ⊥-elim (⊥-color (trans (sym lem26) ueq) ) where - lem26 : color uncle ≡ Black - lem26 = subst (λ k → color k ≡ Black) (just-injective (cong node-right eq )) refl - 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) - = ⊥-elim (⊥-color (trans (sym lem26) ueq) ) where - lem26 : color uncle ≡ Black - lem26 = subst (λ k → color k ≡ Black) (just-injective (cong node-right eq )) refl - 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) - = ⊥-elim (⊥-color (trans (sym lem26) ueq) ) where - lem26 : color uncle ≡ Black - lem26 = subst (λ k → color k ≡ Black) (just-injective (cong node-right eq )) refl - 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) - = ⊥-elim (⊥-color (trans (sym lem26) ueq) ) where - lem26 : color uncle ≡ Black - lem26 = subst (λ k → color k ≡ Black) (just-injective (cong node-right eq )) refl - 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) - 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) - 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) - 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) - lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq rbr-leaf = - 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)) - (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) rr06 (to-black-treeInvariant _ ti₂)) where - lem23 : key₁ ≡ kg - lem23 = just-injective (cong node-key eq) - lem24 : node key₂ v2 t₁₀ t₁₁ ≡ uncle - lem24 = just-injective (cong node-right eq) - rr04 : (kp < kg) ∧ ⊤ ∧ tr< kg t - rr04 = proj1 (ti-property1 ti) - rr03 : (kg < key₂) ∧ tr> kg t₁₀ ∧ tr> kg t₁₁ - rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ _ t) k)) (sym lem24) ti)) - rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ _ t) - rr06 with node→leaf∨IsNode t - ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ x₁ tt tt lem22 ) - ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ x₁ (proj1 rr11) tt - tt (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where - rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn) - rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti))) - 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 (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (proj1 rr03) (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) - (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) rr06 (to-black-treeInvariant _ ti₂)) where - lem23 : key₁ ≡ kg - lem23 = just-injective (cong node-key eq) - lem24 : node key₂ v2 t₁₀ t₁₁ ≡ uncle - lem24 = just-injective (cong node-right eq) - rr04 : (kp < kg) ∧ ((key < kg) ∧ tr< kg t₃ ∧ tr< kg t₄) ∧ tr< kg t - rr04 = proj1 (ti-property1 ti) - rr08 : (key < kp) ∧ tr< kp t₃ ∧ tr< kp t₄ - rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti)) - rr03 : (kg < key₂) ∧ tr> kg t₁₀ ∧ tr> kg t₁₁ - rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node key ⟪ _ , _ ⟫ t₃ t₄) t) k)) (sym lem24) ti)) - rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node _ ⟪ _ , _ ⟫ t₃ t₄) t) - rr06 with node→leaf∨IsNode t - ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) (proj1 (proj2 rr08)) (proj2 (proj2 rr08)) lem22 ) - ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) (proj1 (proj2 rr08)) - (proj2 (proj2 rr08)) (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where - rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn) - rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti))) - 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 (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (proj1 rr03) - ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , >-tr< rr05 (proj1 rr04) ⟫ ⟫ (proj2 (proj2 rr04)) - (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) rr06 (to-black-treeInvariant _ ti₂)) where - lem23 : key₁ ≡ kg - lem23 = just-injective (cong node-key eq) - lem24 : node key₂ v2 t₁₀ t₁₁ ≡ uncle - lem24 = just-injective (cong node-right eq) - rr04 : (kp < kg) ∧ ((k₃ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ tr< kg t - rr04 = proj1 (ti-property1 ti) - rr08 : (k₃ < kp) ∧ tr< kp t₄ ∧ tr< kp t₅ - rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti)) - rr03 : (kg < key₂) ∧ tr> kg t₁₀ ∧ tr> kg t₁₁ - rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node k₃ ⟪ _ , _ ⟫ t₄ t₅) t) k)) (sym lem24) ti)) - rr05 : tr< kp t₃ - rr05 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 rr08)) - rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node k₃ ⟪ _ , _ ⟫ t₄ t₃) t) - rr06 with node→leaf∨IsNode t - ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) (proj1 (proj2 rr08)) rr05 lem22) - ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) (proj1 (proj2 rr08)) - rr05 (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where - rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn) - rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti))) - 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 (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (proj1 rr03) - ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ >-tr< rr05 (proj1 rr04) , proj2 (proj2 (proj1 (proj2 rr04))) ⟫ ⟫ (proj2 (proj2 rr04)) - (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) rr06 (to-black-treeInvariant _ ti₂)) where - lem23 : key₁ ≡ kg - lem23 = just-injective (cong node-key eq) - lem24 : node key₂ v2 t₁₀ t₁₁ ≡ uncle - lem24 = just-injective (cong node-right eq) - rr04 : (kp < kg) ∧ ((k₃ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ tr< kg t - rr04 = proj1 (ti-property1 ti) - rr08 : (k₃ < kp) ∧ tr< kp t₄ ∧ tr< kp t₅ - rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti)) - rr03 : (kg < key₂) ∧ tr> kg t₁₀ ∧ tr> kg t₁₁ - rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node k₃ ⟪ _ , _ ⟫ t₄ t₅) t) k)) (sym lem24) ti)) - rr05 : tr< kp t₃ - rr05 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 rr08)) - rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node k₃ ⟪ _ , _ ⟫ t₃ t₅) t) - rr06 with node→leaf∨IsNode t - ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) rr05 (proj2 (proj2 rr08)) lem22) - ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) rr05 - (proj2 (proj2 rr08)) (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where - rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn) - rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti))) - 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) - 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) - 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) = - subst treeInvariant (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (subst (λ k → k < key₂) lem23 (proj1 rr03)) - ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ ⟪ <-trans (proj1 (proj1 (proj2 rr08))) (proj1 rr04) , - ⟪ >-tr< rr05 (proj1 rr04) , proj2 (proj2 (proj1 (proj2 (proj1 (proj2 rr04))))) ⟫ ⟫ , tr<-to-black (proj2 (proj2 (proj1 (proj2 rr04)))) ⟫ ⟫ (proj2 (proj2 rr04)) - (subst (λ k → tr> k t₁₀) lem23 (proj1 (proj2 rr03))) (subst (λ k → tr> k t₁₁) lem23 (proj2 (proj2 rr03))) rr06 (to-black-treeInvariant _ ti₂)) where - lem23 : key₁ ≡ kg - lem23 = just-injective (cong node-key eq) - lem24 : node key₂ v2 t₁₀ t₁₁ ≡ uncle - lem24 = just-injective (cong node-right eq) - rr04 : (kp < kg) ∧ ((kg₁ < kg) ∧ ((kp₁ < kg) ∧ tr< kg t₁ ∧ tr< kg t₄) ∧ tr< kg t₃ ) ∧ tr< kg t - rr04 = proj1 (ti-property1 ti) - rr08 : (kg₁ < kp) ∧ ((kp₁ < kp) ∧ tr< kp t₁ ∧ tr< kp t₄) ∧ tr< kp t₃ - rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti)) - rr03 : (key₁ < key₂) ∧ tr> key₁ t₁₀ ∧ tr> key₁ t₁₁ - rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (sym eq) ti )) - rr05 : tr< kp t₂ - rr05 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj1 (proj2 rr08)))) - rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node kg₁ ⟪ Red , vg₁ ⟫ (node kp₁ ⟪ Black , vp₁ ⟫ t₂ t₄) (to-black t₃)) t) - rr06 with node→leaf∨IsNode t - ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) ⟪ proj1 (proj1 (proj2 rr08)) , - ⟪ rr05 , proj2 (proj2 (proj1 (proj2 rr08))) ⟫ ⟫ (tr<-to-black (proj2 (proj2 rr08))) lem22) - ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) - ⟪ proj1 (proj1 (proj2 rr08)) , ⟪ rr05 , proj2 (proj2 (proj1 (proj2 rr08))) ⟫ ⟫ - (tr<-to-black (proj2 (proj2 rr08))) (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where - rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn) - rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti))) - 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) = - subst treeInvariant (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (subst (λ k → k < key₂) lem23 (proj1 rr03)) - ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ ⟪ <-trans (proj1 (proj1 (proj2 rr08))) (proj1 rr04) , - ⟪ proj1 (proj2 (proj1 (proj2 (proj1 (proj2 rr04))))) , >-tr< rr05 (proj1 rr04) ⟫ ⟫ , tr<-to-black (proj2 (proj2 (proj1 (proj2 rr04)))) ⟫ ⟫ (proj2 (proj2 rr04)) - (subst (λ k → tr> k t₁₀) lem23 (proj1 (proj2 rr03))) (subst (λ k → tr> k t₁₁) lem23 (proj2 (proj2 rr03))) rr06 (to-black-treeInvariant _ ti₂)) where - lem23 : key₁ ≡ kg - lem23 = just-injective (cong node-key eq) - lem24 : node key₂ v2 t₁₀ t₁₁ ≡ uncle - lem24 = just-injective (cong node-right eq) - rr04 : (kp < kg) ∧ ((kg₁ < kg) ∧ ((kp₁ < kg) ∧ tr< kg t₀ ∧ tr< kg t₁) ∧ tr< kg t₃ ) ∧ tr< kg t - rr04 = proj1 (ti-property1 ti) - rr08 : (kg₁ < kp) ∧ ((kp₁ < kp) ∧ tr< kp t₀ ∧ tr< kp t₁) ∧ tr< kp t₃ - rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti)) - rr03 : (key₁ < key₂) ∧ tr> key₁ t₁₀ ∧ tr> key₁ t₁₁ - rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (sym eq) ti )) - rr05 : tr< kp t₂ - rr05 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj1 (proj2 rr08)))) - rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node kg₁ ⟪ Red , vg₁ ⟫ (node kp₁ ⟪ Black , _ ⟫ t₀ t₂) (to-black t₃)) t) - rr06 with node→leaf∨IsNode t - ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) ⟪ proj1 (proj1 (proj2 rr08)) , - ⟪ proj1 (proj2 (proj1 (proj2 rr08))) , rr05 ⟫ ⟫ (tr<-to-black (proj2 (proj2 rr08))) lem22) - ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) - ⟪ proj1 (proj1 (proj2 rr08)) , ⟪ proj1 (proj2 (proj1 (proj2 rr08))) , rr05 ⟫ ⟫ - (tr<-to-black (proj2 (proj2 rr08))) (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where - rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn) - rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti))) - 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) = - subst treeInvariant (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (subst (λ k → k < key₂) lem23 (proj1 rr03)) - ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ - tr<-to-black (proj1 (proj2 (proj1 (proj2 rr04)))) , ⟪ proj1 (proj2 (proj2 (proj1 (proj2 rr04)))) , - ⟪ >-tr< rr05 (proj1 rr04) , proj2 (proj2 (proj2 (proj2 (proj1 (proj2 rr04))))) ⟫ ⟫ ⟫ ⟫ (proj2 (proj2 rr04)) - (subst (λ k → tr> k t₁₀) lem23 (proj1 (proj2 rr03))) (subst (λ k → tr> k t₁₁) lem23 (proj2 (proj2 rr03))) rr06 (to-black-treeInvariant _ ti₂)) where - lem23 : key₁ ≡ kg - lem23 = just-injective (cong node-key eq) - lem24 : node key₂ v2 t₁₀ t₁₁ ≡ uncle - lem24 = just-injective (cong node-right eq) - rr04 : (kp < kg) ∧ ((kg₁ < kg) ∧ tr< kg t₃ ∧ ((kp₁ < kg) ∧ tr< kg t₁ ∧ tr< kg t₀) ) ∧ tr< kg t - rr04 = proj1 (ti-property1 ti) - rr08 : (kg₁ < kp) ∧ tr< kp t₃ ∧ ((kp₁ < kp) ∧ tr< kp t₁ ∧ tr< kp t₀) - rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti)) - rr03 : (key₁ < key₂) ∧ tr> key₁ t₁₀ ∧ tr> key₁ t₁₁ - rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (sym eq) ti )) - rr05 : tr< kp t₂ - rr05 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj2 (proj2 rr08)))) - rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node kg₁ ⟪ Red , vg₁ ⟫ (to-black t₃) (node kp₁ ⟪ Black , vp₁ ⟫ t₂ t₀)) t) - rr06 with node→leaf∨IsNode t - ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) (tr<-to-black (proj1 (proj2 rr08))) - ⟪ proj1 (proj2 (proj2 rr08)) , ⟪ rr05 , proj2 (proj2 (proj2 (proj2 rr08))) ⟫ ⟫ lem22) - ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) - (tr<-to-black (proj1 (proj2 rr08))) ⟪ proj1 (proj2 (proj2 rr08)) , ⟪ rr05 , proj2 (proj2 (proj2 (proj2 rr08))) ⟫ ⟫ - (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where - rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn) - rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti))) - 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) = - subst treeInvariant (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (subst (λ k → k < key₂) lem23 (proj1 rr03)) - ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ - tr<-to-black (proj1 (proj2 (proj1 (proj2 rr04)))) , ⟪ proj1 (proj2 (proj2 (proj1 (proj2 rr04)))) , - ⟪ proj1 (proj2 (proj2 (proj2 (proj1 (proj2 rr04))))) , >-tr< rr05 (proj1 rr04) ⟫ ⟫ ⟫ ⟫ (proj2 (proj2 rr04)) - (subst (λ k → tr> k t₁₀) lem23 (proj1 (proj2 rr03))) (subst (λ k → tr> k t₁₁) lem23 (proj2 (proj2 rr03))) rr06 (to-black-treeInvariant _ ti₂)) where - lem23 : key₁ ≡ kg - lem23 = just-injective (cong node-key eq) - lem24 : node key₂ v2 t₁₀ t₁₁ ≡ uncle - lem24 = just-injective (cong node-right eq) - rr04 : (kp < kg) ∧ ((kg₁ < kg) ∧ tr< kg t₃ ∧ ((kp₁ < kg) ∧ tr< kg t₀ ∧ tr< kg t₁) ) ∧ tr< kg t - rr04 = proj1 (ti-property1 ti) - rr08 : (kg₁ < kp) ∧ tr< kp t₃ ∧ ((kp₁ < kp) ∧ tr< kp t₀ ∧ tr< kp t₁) - rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti)) - rr03 : (key₁ < key₂) ∧ tr> key₁ t₁₀ ∧ tr> key₁ t₁₁ - rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (sym eq) ti )) - rr05 : tr< kp t₂ - rr05 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj2 (proj2 rr08)))) - rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node kg₁ ⟪ Red , vg₁ ⟫ (to-black t₃) (node kp₁ ⟪ Black , vp₁ ⟫ t₀ t₂)) t) - rr06 with node→leaf∨IsNode t - ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) (tr<-to-black (proj1 (proj2 rr08))) - ⟪ proj1 (proj2 (proj2 rr08)) , ⟪ proj1 (proj2 (proj2 (proj2 rr08))) , rr05 ⟫ ⟫ lem22) - ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) - (tr<-to-black (proj1 (proj2 rr08))) ⟪ proj1 (proj2 (proj2 rr08)) , ⟪ proj1 (proj2 (proj2 (proj2 rr08))) , rr05 ⟫ ⟫ - (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where - rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn) - rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti))) - 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) - 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) - 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) - 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) - - + rr05 : (kp < kg) ∧ tr< kg t₁ ∧ tr< kg t + rr05 = proj1 (ti-property1 ti) + rr07 : tr> kg uncle + rr07 = proj2 (ti-property1 ti) + rr08 : tr> kp t + rr08 = proj2 (ti-property1 (treeLeftDown _ _ ti)) + rr10 : tr< kp t₁ + rr10 = proj1 (ti-property1 (treeLeftDown _ _ ti)) + rr09 : tr< kg t₂ + rr09 = RB-repl→ti< _ _ _ _ _ rbt (<-trans x₀ (proj1 rr05)) (proj1 (proj2 rr05)) + rr11 : tr< kp t₂ + rr11 = RB-repl→ti< _ _ _ _ _ rbt x₀ rr10 + lem21 : treeInvariant (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t₂ t) (to-black uncle)) + lem21 = tree-construct _ _ _ ⟪ proj1 rr05 , ⟪ rr09 , proj2 (proj2 rr05) ⟫ ⟫ (tr>-to-black rr07) (tree-construct _ _ _ rr11 rr08 lem22 lem25) + (treeInvariant-to-black A (treeRightDown _ _ ti) ) RB-repl→ti-lem07 : {n : Level} {A : Set n} {key : ℕ} {value : A} {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key) (x₃ : key < kg) (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂) - → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁) uncle) + (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key) (x₃ : key < kg) (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂) + → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁) uncle) → treeInvariant (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t t₂) (to-black uncle)) -RB-repl→ti-lem07 = ? +RB-repl→ti-lem07 {n} {A} {key} {value} {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} ceq ueq x₀ x₁ rbt prev ti + = lem21 where + lem22 : treeInvariant t₂ + lem22 = prev (treeRightDown _ _ (treeLeftDown _ _ ti )) + lem25 : treeInvariant t + lem25 = treeLeftDown _ _ (treeLeftDown _ _ ti) + rr05 : (kp < kg) ∧ tr< kg t ∧ tr< kg t₁ + rr05 = proj1 (ti-property1 ti) + rr07 : tr> kg uncle + rr07 = proj2 (ti-property1 ti) + rr08 : tr< kp t + rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti)) + rr10 : tr> kp t₁ + rr10 = proj2 (ti-property1 (treeLeftDown _ _ ti)) + rr09 : tr> kp t₂ + rr09 = RB-repl→ti> _ _ _ _ _ rbt x₀ rr10 + rr11 : tr< kg t₂ + rr11 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 rr05)) + lem21 : treeInvariant (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t t₂) (to-black uncle)) + lem21 = tree-construct _ _ _ ⟪ proj1 rr05 , ⟪ proj1 (proj2 rr05) , rr11 ⟫ ⟫ (tr>-to-black rr07) + (tree-construct _ _ _ rr08 rr09 lem25 lem22) (treeInvariant-to-black A (treeRightDown _ _ ti) ) RB-repl→ti-lem08 : {n : Level} {A : Set n} {key : ℕ} {value : A} → {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kg < key) (x₃ : key < kp) (rbt : replacedRBTree key value t₁ t₂) - → (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t₁ t)) - → treeInvariant (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t₂ t)) -RB-repl→ti-lem08 = ? + (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kg < key) (x₃ : key < kp) (rbt : replacedRBTree key value t₁ t₂) + → (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t₁ t)) + → treeInvariant (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t₂ t)) +RB-repl→ti-lem08 {n} {A} {key} {value} {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} ceq ueq x₀ x₁ rbt prev ti = lem21 where + lem22 : treeInvariant t₂ + lem22 = prev (treeLeftDown _ _ (treeRightDown _ _ ti )) + lem25 : treeInvariant t + lem25 = treeRightDown _ _ (treeRightDown _ _ ti) + rr05 : (kg < kp) ∧ tr> kg t₁ ∧ tr> kg t + rr05 = proj2 (ti-property1 ti) + rr07 : tr< kg uncle + rr07 = proj1 (ti-property1 ti) + rr08 : tr> kp t + rr08 = proj2 (ti-property1 (treeRightDown _ _ ti)) + rr10 : tr< kp t₁ + rr10 = proj1 (ti-property1 (treeRightDown _ _ ti)) + rr09 : tr< kp t₂ + rr09 = RB-repl→ti< _ _ _ _ _ rbt x₁ rr10 + rr11 : tr> kg t₂ + rr11 = RB-repl→ti> _ _ _ _ _ rbt x₀ (proj1 (proj2 rr05)) + lem21 : treeInvariant (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t₂ t)) + lem21 = tree-construct _ _ _ (tr<-to-black rr07) ⟪ proj1 rr05 , ⟪ rr11 , proj2 (proj2 rr05) ⟫ ⟫ (treeInvariant-to-black A (treeLeftDown _ _ ti) ) + (tree-construct _ _ _ rr09 rr08 lem22 lem25) RB-repl→ti-lem09 : {n : Level} {A : Set n} {key : ℕ} {value : A} → {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key) (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t t₁)) → treeInvariant (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t t₂)) -RB-repl→ti-lem09 = ? +RB-repl→ti-lem09 {n} {A} {key} {value} {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} ceq ueq x₁ rbt prev ti = lem21 where + lem22 : treeInvariant t₂ + lem22 = prev (treeRightDown _ _ (treeRightDown _ _ ti )) + lem25 : treeInvariant t + lem25 = treeLeftDown _ _ ( treeRightDown _ _ ti ) + rr05 : (kg < kp) ∧ tr> kg t ∧ tr> kg t₁ + rr05 = proj2 (ti-property1 ti) + rr07 : tr< kg uncle + rr07 = proj1 (ti-property1 ti) + rr08 : tr> kp t₁ + rr08 = proj2 (ti-property1 (treeRightDown _ _ ti)) + rr10 : tr< kp t + rr10 = proj1 (ti-property1 (treeRightDown _ _ ti)) + rr09 : tr> kp t₂ + rr09 = RB-repl→ti> _ _ _ _ _ rbt x₁ rr08 + lem21 : treeInvariant (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t t₂)) + lem21 = tree-construct _ _ _ (tr<-to-black rr07) ⟪ proj1 rr05 , ⟪ proj1 (proj2 rr05) , <-tr> rr09 (proj1 rr05) ⟫ ⟫ + (treeInvariant-to-black A (treeLeftDown _ _ ti) ) (tree-construct _ _ _ rr10 rr09 lem25 lem22) RB-repl→ti-lem10 : {n : Level} {A : Set n} {key : ℕ} {value : A} → {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : key < kp) (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₁ t) uncle) → treeInvariant (node kp ⟪ Black , vp ⟫ t₂ (node kg ⟪ Red , vg ⟫ t uncle)) -RB-repl→ti-lem10 = ? +RB-repl→ti-lem10 {n} {A} {key} {value} {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} ceq x₁ rbt prev ti = + tree-construct _ _ _ rr09 ⟪ proj1 rr05 , ⟪ rr10 , <-tr> rr07 (proj1 rr05) ⟫ ⟫ lem22 (tree-construct _ _ _ (proj2 (proj2 rr05)) rr07 lem25 lem26) where + lem22 : treeInvariant t₂ + lem22 = prev (treeLeftDown _ _ (treeLeftDown _ _ ti ) ) + lem25 : treeInvariant t + lem25 = treeRightDown _ _ (treeLeftDown _ _ ti ) + lem26 : treeInvariant uncle + lem26 = treeRightDown _ _ ti + rr05 : (kp < kg) ∧ tr< kg t₁ ∧ tr< kg t + rr05 = proj1 (ti-property1 ti) + rr07 : tr> kg uncle + rr07 = proj2 (ti-property1 ti) + rr08 : tr< kp t₁ + rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti)) + rr10 : tr> kp t + rr10 = proj2 (ti-property1 (treeLeftDown _ _ ti)) + rr09 : tr< kp t₂ + rr09 = RB-repl→ti< _ _ _ _ _ rbt x₁ rr08 + RB-repl→ti-lem11 : {n : Level} {A : Set n} {key : ℕ} {value : A} → {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : kp < key) (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t t₁)) → treeInvariant (node kp ⟪ Black , vp ⟫ (node kg ⟪ Red , vg ⟫ uncle t) t₂) -RB-repl→ti-lem11 = ? +RB-repl→ti-lem11 {n} {A} {key} {value} {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} ceq x₁ rbt prev ti = lem21 where + lem22 : treeInvariant t₂ + lem22 = prev (treeRightDown _ _ (treeRightDown _ _ ti ) ) + lem25 : treeInvariant t + lem25 = treeLeftDown _ _ (treeRightDown _ _ ti ) + lem26 : treeInvariant uncle + lem26 = treeLeftDown _ _ ti + rr05 : (kg < kp) ∧ tr> kg t ∧ tr> kg t₁ + rr05 = proj2 (ti-property1 ti) + rr07 : tr< kg uncle + rr07 = proj1 (ti-property1 ti) + rr08 : tr> kp t₁ + rr08 = proj2 (ti-property1 (treeRightDown _ _ ti)) + rr10 : tr< kp t + rr10 = proj1 (ti-property1 (treeRightDown _ _ ti)) + rr09 : tr> kp t₂ + rr09 = RB-repl→ti> _ _ _ _ _ rbt x₁ rr08 + lem21 : treeInvariant (node kp ⟪ Black , vp ⟫ (node kg ⟪ Red , vg ⟫ uncle t) t₂) + lem21 = tree-construct _ _ _ ⟪ proj1 rr05 , ⟪ >-tr< rr07 (proj1 rr05) , rr10 ⟫ ⟫ rr09 (tree-construct _ _ _ rr07 (proj1 (proj2 rr05)) lem26 lem25) lem22 + 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) (x₁ : kp < key) (x₂ : key < kg) (rbt : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) → (treeInvariant t₁ → treeInvariant (node kn ⟪ Red , vn ⟫ t₂ t₃)) → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁) uncle) → treeInvariant (node kn ⟪ Black , vn ⟫ (node kp ⟪ Red , vp ⟫ t t₂) (node kg ⟪ Red , vg ⟫ t₃ uncle)) -RB-repl→ti-lem12 = ? +RB-repl→ti-lem12 {n} {A} {key} {value} {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} ceq x₁ x₂ rbt prev ti = + t-node _ _ _ (proj1 rr09) (proj1 rr11) (>-tr< rr10 (proj1 rr09)) rr24 rr22 (<-tr> rr07 (proj1 rr11) ) rr20 rr21 where + lem22 : treeInvariant t₂ + lem22 = treeLeftDown _ _ (prev (treeRightDown _ _ (treeLeftDown _ _ ti ) )) + lem23 : treeInvariant t₃ + lem23 = treeRightDown _ _ (prev (treeRightDown _ _ (treeLeftDown _ _ ti ) )) + lem25 : treeInvariant t + lem25 = treeLeftDown _ _ (treeLeftDown _ _ ti ) + lem26 : treeInvariant uncle + lem26 = treeRightDown _ _ ti + rr05 : (kp < kg) ∧ tr< kg t ∧ tr< kg t₁ + rr05 = proj1 (ti-property1 ti) + rr07 : tr> kg uncle + rr07 = proj2 (ti-property1 ti) + rr08 : tr> kp t₁ + rr08 = proj2 (ti-property1 (treeLeftDown _ _ ti)) + rr10 : tr< kp t + rr10 = proj1 (ti-property1 (treeLeftDown _ _ ti)) + rr09 : (kp < kn) ∧ tr> kp t₂ ∧ tr> kp t₃ + rr09 = RB-repl→ti> _ _ _ _ _ rbt x₁ rr08 + rr11 : (kn < kg) ∧ tr< kg t₂ ∧ tr< kg t₃ + rr11 = RB-repl→ti< _ _ _ _ _ rbt x₂ (proj2 (proj2 rr05)) + rr20 : treeInvariant (node kp ⟪ Red , vp ⟫ t t₂) + rr20 = tree-construct _ _ _ rr10 (proj1 (proj2 rr09)) lem25 lem22 + rr21 : treeInvariant (node kg ⟪ Red , vg ⟫ t₃ uncle) + rr21 = tree-construct _ _ _ (proj2 (proj2 rr11)) rr07 lem23 lem26 + rr22 : tr> kn t₃ + rr22 = proj2 (ti-property1 (prev (treeRightDown _ _ (treeLeftDown _ _ ti )) )) + rr24 : tr< kn t₂ + rr24 = proj1 (ti-property1 (prev (treeRightDown _ _ (treeLeftDown _ _ ti )) )) 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) (x₁ : kg < key) (x₂ : key < kp) (rbt : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) → (treeInvariant t₁ → treeInvariant (node kn ⟪ Red , vn ⟫ t₂ t₃)) → treeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t₁ t)) → treeInvariant (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , vg ⟫ uncle t₂) (node kp ⟪ Red , vp ⟫ t₃ t)) -RB-repl→ti-lem13 = ? +RB-repl→ti-lem13 {n} {A} {key} {value} {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} ceq x₁ x₂ rbt prev ti = + t-node _ _ _ (proj1 rr09) (proj1 rr11) (>-tr< rr07 (proj1 rr09)) rr24 rr22 (<-tr> rr10 (proj1 rr11)) rr20 rr21 where + lem22 : treeInvariant t₂ + lem22 = treeLeftDown _ _ (prev (treeLeftDown _ _ (treeRightDown _ _ ti ) )) + lem23 : treeInvariant t₃ + lem23 = treeRightDown _ _ (prev (treeLeftDown _ _ (treeRightDown _ _ ti ) )) + lem25 : treeInvariant t + lem25 = treeRightDown _ _ (treeRightDown _ _ ti ) + lem26 : treeInvariant uncle + lem26 = treeLeftDown _ _ ti + rr05 : (kg < kp) ∧ tr> kg t₁ ∧ tr> kg t + rr05 = proj2 (ti-property1 ti) + rr07 : tr< kg uncle + rr07 = proj1 (ti-property1 ti) + rr08 : tr< kp t₁ + rr08 = proj1 (ti-property1 (treeRightDown _ _ ti)) + rr10 : tr> kp t + rr10 = proj2 (ti-property1 (treeRightDown _ _ ti)) + rr09 : (kg < kn) ∧ tr> kg t₂ ∧ tr> kg t₃ + rr09 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 rr05)) + rr11 : (kn < kp) ∧ tr< kp t₂ ∧ tr< kp t₃ + rr11 = RB-repl→ti< _ _ _ _ _ rbt x₂ rr08 + rr20 : treeInvariant (node kg ⟪ Red , vg ⟫ uncle t₂) + rr20 = tree-construct _ _ _ rr07 (proj1 (proj2 rr09)) lem26 lem22 + rr21 : treeInvariant (node kp ⟪ Red , vp ⟫ t₃ t) + rr21 = tree-construct _ _ _ (proj2 (proj2 rr11)) rr10 lem23 lem25 + rr22 : tr> kn t₃ + rr22 = proj2 (ti-property1 (prev (treeLeftDown _ _ (treeRightDown _ _ ti ) ) )) + rr24 : tr< kn t₂ + rr24 = proj1 (ti-property1 (prev (treeLeftDown _ _ (treeRightDown _ _ ti ) ) )) RB-repl→ti : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A) ) → (key : ℕ ) → (value : A) → treeInvariant tree → replacedRBTree key value tree repl → treeInvariant repl RB-repl→ti {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 } - ⟪ lem00 , ⟪ lem01 , ⟪ lem02 , ⟪ RB-repl→ti-lem03 , ⟪ RB-repl→ti-lem04 , ⟪ RB-repl→ti-lem05 , + ⟪ lem00 , ⟪ RB-repl→ti-lem01 , ⟪ RB-repl→ti-lem02 , ⟪ RB-repl→ti-lem03 , ⟪ RB-repl→ti-lem04 , ⟪ RB-repl→ti-lem05 , ⟪ RB-repl→ti-lem06 , ⟪ RB-repl→ti-lem07 , ⟪ RB-repl→ti-lem08 , ⟪ RB-repl→ti-lem09 , ⟪ RB-repl→ti-lem10 , ⟪ RB-repl→ti-lem11 , ⟪ RB-repl→ti-lem12 , RB-repl→ti-lem13 ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ti where lem00 : treeInvariant leaf → treeInvariant (node key ⟪ Red , value ⟫ leaf leaf) lem00 ti = t-single key ⟪ Red , value ⟫ - lem01 : (ca : Color) (value₂ : A) (t t₁ : bt (Color ∧ A)) → treeInvariant (node key ⟪ ca , value₂ ⟫ t t₁) → treeInvariant (node key ⟪ ca , value ⟫ t t₁) - lem01 ca v2 t t₁ ti = lem20 (node key ⟪ ca , v2 ⟫ t t₁) ti refl where - lem20 : (tree : bt (Color ∧ A)) → treeInvariant tree → tree ≡ node key ⟪ ca , v2 ⟫ t t₁ → treeInvariant (node key ⟪ ca , value ⟫ t t₁) - lem20 .leaf t-leaf () - lem20 (node key v3 leaf leaf) (t-single key v3) eq = subst treeInvariant - (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 ⟫) - lem20 (node key _ leaf (node key₁ _ _ _)) (t-right key key₁ x x₁ x₂ ti) eq = subst treeInvariant - (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) - lem20 (node key₁ _ (node key _ _ _) leaf) (t-left key key₁ x x₁ x₂ ti) eq = subst treeInvariant - (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) - lem20 (node key₁ _ (node key _ _ _) (node key₂ _ _ _)) (t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) eq = subst treeInvariant - (node-cong (just-injective (cong node-key eq)) refl (just-injective (cong node-left eq)) (just-injective (cong node-right eq))) - (t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) - lem02 : {k : ℕ} {v1 : A} {ca : Color} {t t1 t2 : bt (Color ∧ A)} (x : color t2 ≡ color t) (x₁ : k < key) - (rbt : replacedRBTree key value t2 t) → (treeInvariant t2 → treeInvariant t) → treeInvariant (node k ⟪ ca , v1 ⟫ t1 t2) → treeInvariant (node k ⟪ ca , v1 ⟫ t1 t) - lem02 {k} {v1} {ca} {t} {t1} {t2} ceq x₁ rbt prev ti = lem21 (node k ⟪ ca , v1 ⟫ t1 t2) ti refl rbt where - lem22 : treeInvariant t - lem22 = prev (treeRightDown _ _ ti) - 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) - lem21 .leaf t-leaf () - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) eq rbr-leaf = subst treeInvariant - (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 - lem23 : k₁ ≡ k - lem23 = just-injective (cong node-key eq) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () rbr-node - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-right x x₁ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-left x x₁ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-black-right x x₁ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-black-left x x₁ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-flip-ll x x₁ x₂ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-flip-lr x x₁ x₂ x₃ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-flip-rl x x₁ x₂ x₃ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-flip-rr x x₁ x₂ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-rotate-ll x x₁ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-rotate-rr x x₁ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-rotate-lr t₂ t₃ kg kp kn x x₁ x₂ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-rotate-rl t₂ t₃ kg kp kn x x₁ x₂ rbt) - lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₄ x₂ ti) eq rbr-leaf = subst treeInvariant - (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 - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti) eq (rbr-node {_} {_} {left} {right}) = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (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 - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - lem24 : t₁ ≡ left - lem24 = just-injective (cong node-left (just-injective (cong node-right eq))) - lem25 : t₂ ≡ right - lem25 = just-injective (cong node-right (just-injective (cong node-right eq))) - 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 - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-right k₃ _ (subst (λ k → k₃ < k) lem26 x) (subst (λ k → tr> k₃ k) lem24 x₁₀) rr01 lem22) where - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - lem26 : k₁ ≡ k₂ - lem26 = just-injective (cong node-key (just-injective (cong node-right eq))) - lem24 : left ≡ t₂ - lem24 = just-injective (cong node-left (just-injective (cong node-right eq))) - rr01 : tr> k₃ t₁ - rr01 = RB-repl→ti> _ _ _ _ _ trb (<-trans (subst (λ k → k₃ < k ) lem26 x ) x₄ ) - (subst (λ j → tr> k₃ j) (just-injective (cong node-right (just-injective (cong node-right eq)))) x₂ ) - 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 - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-right k₃ _ (subst (λ k → k₃ < k) lem26 x) rr02 rr01 lem22) where - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - lem26 : k₁ ≡ k₂ - lem26 = just-injective (cong node-key (just-injective (cong node-right eq))) - rr01 : tr> k₃ t₃ - rr01 = subst (λ k → tr> k₃ k) (just-injective (cong node-right (just-injective (cong node-right eq)))) x₂ - rr02 : tr> k₃ t₁ - rr02 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) - (subst (λ j → tr> k₃ j) (just-injective (cong node-left (just-injective (cong node-right eq)))) x₁₀ ) - 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 - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-right k₃ _ (subst (λ k → k₃ < k) lem26 x) rr01 rr02 lem22) where - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - lem26 : k₁ ≡ k₂ - lem26 = just-injective (cong node-key (just-injective (cong node-right eq))) - rr01 : tr> k₃ t₁ - rr01 = subst (λ k → tr> k₃ k) (just-injective (cong node-left (just-injective (cong node-right eq)))) x₁₀ - rr02 : tr> k₃ t₃ - rr02 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) - (subst (λ k → tr> k₃ k) (just-injective (cong node-right (just-injective (cong node-right eq)))) x₂ ) - 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 - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ (subst (λ k → k₃ < k) lem26 x) rr02 rr01 lem22) where - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - lem26 : k₁ ≡ k₂ - lem26 = just-injective (cong node-key (just-injective (cong node-right eq))) - rr01 : tr> k₃ t₁ - rr01 = subst (λ k → tr> k₃ k) (just-injective (cong node-right (just-injective (cong node-right eq)))) x₂ - rr02 : tr> k₃ t₃ - rr02 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) - (subst (λ k → tr> k₃ k) (just-injective (cong node-left (just-injective (cong node-right eq)))) x₁₀ ) - 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 ) - 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 ) - 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 ) - 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 ) - 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) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ lem27 rr02 rr01 lem22) where - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - lem27 : k₃ < kp - lem27 = subst (λ k → k < kp) (sym lem23) (<-trans x₁ x₄) - rr04 : (k₃ < kg) ∧ ((k₃ < kp) ∧ tr> k₃ t₁ ∧ tr> k₃ t) ∧ tr> k₃ uncle - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr01 : (k₃ < kg) ∧ tr> k₃ t ∧ tr> k₃ uncle - rr01 = ⟪ proj1 rr04 , ⟪ proj2 (proj2 (proj1 (proj2 rr04))) , proj2 (proj2 rr04) ⟫ ⟫ - rr02 : tr> k₃ t₂ - rr02 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 (proj1 (proj2 rr04)))) - 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) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ lem27 rr01 rr02 lem22) where - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₃ < kg) ∧ tr> k₃ uncle ∧ ((k₃ < kp) ∧ tr> k₃ t ∧ tr> k₃ t₁) - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - lem27 : k₃ < kp - lem27 = proj1 (proj2 (proj2 rr04)) - rr01 : (k₃ < kg) ∧ tr> k₃ uncle ∧ tr> k₃ t - rr01 = ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ - rr02 : tr> k₃ t₂ - rr02 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 (proj2 (proj2 rr04)))) - 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) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ lem27 rr05 rr06 lem22) where - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₃ < kg) ∧ ((k₃ < kp) ∧ tr> k₃ t ∧ tr> k₃ t₁) ∧ tr> k₃ uncle - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr01 : (k₃ < kn) ∧ tr> k₃ t₂ ∧ tr> k₃ t₃ - rr01 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 (proj1 (proj2 rr04)))) - lem27 : k₃ < kn - lem27 = proj1 rr01 - rr05 : (k₃ < kp) ∧ tr> k₃ t ∧ tr> k₃ t₂ - rr05 = ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , proj1 (proj2 rr01) ⟫ ⟫ - rr06 : (k₃ < kg) ∧ tr> k₃ t₃ ∧ tr> k₃ uncle - rr06 = ⟪ proj1 rr04 , ⟪ proj2 (proj2 rr01) , proj2 (proj2 rr04) ⟫ ⟫ - 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) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ lem27 rr05 rr06 lem22) where - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₃ < kg) ∧ tr> k₃ uncle ∧ ( (k₃ < kp) ∧ tr> k₃ t₁ ∧ tr> k₃ t) - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr01 : (k₃ < kn) ∧ tr> k₃ t₂ ∧ tr> k₃ t₃ - rr01 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 (proj2 (proj2 rr04))) ) - lem27 : k₃ < kn - lem27 = proj1 rr01 - rr05 : (k₃ < kg) ∧ tr> k₃ uncle ∧ tr> k₃ t₂ - rr05 = ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 rr01) ⟫ ⟫ - rr06 : (k₃ < kp) ∧ tr> k₃ t₃ ∧ tr> k₃ t - rr06 = ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj2 (proj2 rr01) , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti₁) eq rbr-leaf = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-node _ _ _ x (subst (λ j → j < key) (sym lem23) x₁) x₁₀ x₂ tt tt ti₁ (t-single key ⟪ Red , value ⟫)) where - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () rbr-node - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-right x₃ x₄ rbt) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-left x₃ x₄ rbt) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-black-right x₃ x₄ rbt) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-black-left x₃ x₄ rbt) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-flip-ll x₃ x₄ x₅ rbt) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-flip-lr x₃ x₄ x₅ x₆ rbt) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-flip-rl x₃ x₄ x₅ x₆ rbt) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-flip-rr x₃ x₄ x₅ rbt) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-rotate-ll x₃ x₄ rbt) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-rotate-rr x₃ x₄ rbt) - 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) - 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) - lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti ti₁) () rbr-leaf - 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₄}) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-node _ _ _ x (subst (λ j → j < key) (sym lem23) x₁) x₂ x₃ (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) ti₁ lem22) where - lem23 : k₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₁ < key) ∧ tr> k₁ t₃ ∧ tr> k₁ t₄ - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - 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) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-node _ _ _ x (proj1 rr04) x₂ x₃ (proj1 (proj2 rr04)) rr05 ti₁ lem22) where - lem23 : k₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₁ < k₃) ∧ tr> k₁ t₂ ∧ tr> k₁ t₃ - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr05 : tr> k₁ t₁ - rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 rr04)) - 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) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-node _ _ _ x (proj1 rr04) x₂ x₃ rr05 (proj2 (proj2 rr04)) ti₁ lem22) where - lem23 : k₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₁ < k₃) ∧ tr> k₁ t₂ ∧ tr> k₁ t₃ - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti )) - rr05 : tr> k₁ t₁ - rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 rr04)) - 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) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-node _ _ _ x (proj1 rr04) x₂ x₃ (proj1 (proj2 rr04)) rr05 ti₁ lem22) where - lem23 : k₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₁ < k₃) ∧ tr> k₁ t₁ ∧ tr> k₁ t₂ - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti )) - rr05 : tr> k₁ t₃ - rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 rr04)) - 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) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-node _ _ _ x (proj1 rr04) x₂ x₃ rr05 (proj2 (proj2 rr04)) ti₁ lem22) where - lem23 : k₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₁ < k₃) ∧ tr> k₁ t₂ ∧ tr> k₁ t₁ - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti )) - rr05 : tr> k₁ t₃ - rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 rr04)) - 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 ) - 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 ) - 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 ) - 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 ) - 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) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-node _ _ _ x (proj1 (proj1 (proj2 rr04))) x₂ x₃ rr05 ⟪ proj1 rr04 , ⟪ proj2 (proj2 (proj1 (proj2 rr04))) , proj2 (proj2 rr04) ⟫ ⟫ ti₁ lem22) where - lem23 : k₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₁ < kg) ∧ ((k₁ < kp) ∧ tr> k₁ t₂ ∧ tr> k₁ t₁) ∧ tr> k₁ uncle - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti )) - rr05 : tr> k₁ t₃ - rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 (proj1 (proj2 rr04)))) - 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) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-node _ _ _ x (proj1 (proj2 (proj2 rr04))) x₂ x₃ ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ rr05 ti₁ lem22) where - lem23 : k₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₁ < kg) ∧ tr> k₁ uncle ∧ ((k₁ < kp) ∧ tr> k₁ t₁ ∧ tr> k₁ t₂) - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti )) - rr05 : tr> k₁ t₃ - rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 (proj2 (proj2 rr04)))) - 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) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-node _ _ _ x (proj1 rr05) x₂ x₃ ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , proj1 (proj2 rr05) ⟫ ⟫ - ⟪ proj1 rr04 , ⟪ proj2 (proj2 rr05) , proj2 (proj2 rr04) ⟫ ⟫ ti₁ lem22) where - lem23 : k₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₁ < kg) ∧ ((k₁ < kp) ∧ tr> k₁ t ∧ tr> k₁ t₁) ∧ tr> k₁ uncle - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti )) - rr05 : (k₁ < kn) ∧ tr> k₁ t₂ ∧ tr> k₁ t₃ - rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 (proj1 (proj2 rr04)))) - 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) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-node _ _ _ x (proj1 rr05) x₂ x₃ ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 rr05) ⟫ ⟫ - ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj2 (proj2 rr05) , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ ti₁ lem22) where - lem23 : k₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₁ < kg) ∧ tr> k₁ uncle ∧ ((k₁ < kp) ∧ tr> k₁ t₁ ∧ tr> k₁ t) - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti )) - rr05 : (k₁ < kn) ∧ tr> k₁ t₂ ∧ tr> k₁ t₃ - rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 (proj2 (proj2 rr04)))) + + +si-property-4 : {n : Level} {A : Set n} → {key : ℕ } → (tree orig x : bt A ) → (st : List (bt A)) + → st ≡ x ∷ [] + → stackInvariant key tree orig st + → (x ≡ orig) ∧ (x ≡ tree) +si-property-4 {n} {A} {key} tree .tree x .(tree ∷ []) eq s-nil = ⟪ just-injective (cong head (sym eq)) , just-injective (cong head (sym eq)) ⟫ +si-property-4 {n} {A} {key} tree orig x .(tree ∷ _) eq (s-right .tree .orig tree₁ x₁ si) = ⊥-elim ( si-property0 si (just-injective (cong tail eq)) ) +si-property-4 {n} {A} {key} tree orig x .(tree ∷ _) eq (s-left .tree .orig tree₁ x₁ si) = ⊥-elim ( si-property0 si (just-injective (cong tail eq)) ) + +si-property-5 : {n : Level} {A : Set n} → {key : ℕ } → {tree orig x x₁ x₂ : bt A } → {st st' : List (bt A)} + → st ≡ x ∷ x₁ ∷ x₂ ∷ st' + → stackInvariant key tree orig st + → (¬ (x₁ ≡ leaf )) ∧ (¬ (x₂ ≡ leaf )) +si-property-5 {n} {A} {key} () s-nil +si-property-5 {n} {A} {key} () (s-right _ _ tree₁ lt s-nil) +si-property-5 {n} {A} {key} eq (s-right _ _ tree₁ lt (s-right .(node _ _ tree₁ _) _ tree₂ x₁ s-nil)) + = ⟪ (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail eq))) )))) + , (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail (just-injective (cong tail eq))) )))) )) ⟫ +si-property-5 {n} {A} {key} {tree} {orig} {x} {x₁} {x₂} eq (s-right _ _ tree₁ lt si1@(s-right .(node _ _ tree₁ _) _ tree₂ lt₁ + (s-right .(node _ _ tree₂ (node _ _ tree₁ _)) _ tree₃ lt₂ si))) + = ⟪ (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail eq))) )))) + , (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail (just-injective (cong tail eq))) )))) )) ⟫ +si-property-5 {n} {A} {key} eq (s-right _ _ tree₁ x (s-right .(node _ _ tree₁ _) _ tree₂ x₁ (s-left .(node _ _ tree₂ (node _ _ tree₁ _)) _ tree x₂ si))) + = ⟪ (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail eq))) )))) + , (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail (just-injective (cong tail eq))) )))) )) ⟫ +si-property-5 {n} {A} {key} eq (s-right _ _ tree₁ x (s-left .(node _ _ tree₁ _) _ tree x₁ s-nil)) + = ⟪ (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail eq))) )))) + , (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail (just-injective (cong tail eq))) )))) )) ⟫ +si-property-5 {n} {A} {key} eq (s-right _ _ tree₁ x (s-left .(node _ _ tree₁ _) _ tree x₁ (s-right .(node _ _ (node _ _ tree₁ _) tree) _ tree₂ x₂ si))) + = ⟪ (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail eq))) )))) + , (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail (just-injective (cong tail eq))) )))) )) ⟫ +si-property-5 {n} {A} {key} eq (s-right _ _ tree₁ x (s-left .(node _ _ tree₁ _) _ tree x₁ (s-left .(node _ _ (node _ _ tree₁ _) tree) _ tree₂ x₂ si))) + = ⟪ (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail eq))) )))) + , (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail (just-injective (cong tail eq))) )))) )) ⟫ +si-property-5 {n} {A} {key} () (s-left _ _ tree x s-nil) +si-property-5 {n} {A} {key} eq (s-left _ _ tree x (s-right .(node _ _ _ tree) _ tree₁ x₁ s-nil)) + = ⟪ (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail eq))) )))) + , (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail (just-injective (cong tail eq))) )))) )) ⟫ +si-property-5 {n} {A} {key} eq (s-left _ _ tree x (s-right .(node _ _ _ tree) _ tree₁ x₁ (s-right .(node _ _ tree₁ (node _ _ _ tree)) _ tree₂ x₂ si))) + = ⟪ (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail eq))) )))) + , (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail (just-injective (cong tail eq))) )))) )) ⟫ +si-property-5 {n} {A} {key} eq (s-left _ _ tree x (s-right .(node _ _ _ tree) _ tree₁ x₁ (s-left .(node _ _ tree₁ (node _ _ _ tree)) _ tree₂ x₂ si))) + = ⟪ (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail eq))) )))) + , (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail (just-injective (cong tail eq))) )))) )) ⟫ +si-property-5 {n} {A} {key} eq (s-left _ _ tree x (s-left .(node _ _ _ tree) _ tree₁ x₁ s-nil)) + = ⟪ (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail eq))) )))) + , (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail (just-injective (cong tail eq))) )))) )) ⟫ +si-property-5 {n} {A} {key} eq (s-left _ _ tree x (s-left .(node _ _ _ tree) _ tree₁ x₁ (s-right .(node _ _ (node _ _ _ tree) tree₁) _ tree₂ x₂ si))) + = ⟪ (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail eq))) )))) + , (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail (just-injective (cong tail eq))) )))) )) ⟫ +si-property-5 {n} {A} {key} eq (s-left _ _ tree x (s-left .(node _ _ _ tree) _ tree₁ x₁ (s-left .(node _ _ (node _ _ _ tree) tree₁) _ tree₂ x₂ si))) + = ⟪ (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail eq))) )))) + , (λ eq₁ → bt-ne (trans (sym eq₁) (sym ( just-injective (cong head (just-injective (cong tail (just-injective (cong tail eq))) )))) )) ⟫ +-- +-- if we consider tree invariant, this may be much simpler and faster +-- +stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A ) + → (stack : List (bt A)) → stackInvariant key tree orig stack + → ( stack ≡ orig ∷ [] ) ∨ ( stack ≡ tree ∷ orig ∷ [] ) ∨ PG A key tree stack +stackToPG {n} {A} {key} tree orig [] si = ⊥-elim ( si-property0 si refl ) +stackToPG {n} {A} {key} tree orig (x ∷ []) si = case1 (cong (λ k → k ∷ []) (proj1 (si-property-4 tree orig x _ refl si))) +stackToPG {n} {A} {key} tree orig (x ∷ x₁ ∷ []) si = case2 (case1 (cong₂ (λ j k → j ∷ k ∷ []) si03 si02 )) where + si02 : x₁ ≡ orig + si02 = just-injective ( si-property-last _ _ _ _ si ) + si03 : x ≡ tree + si03 = si-property1 si +stackToPG {n} {A} {key} tree orig (x ∷ x₁ ∷ x₂ ∷ stack) si = case2 (case2 (si01 (x ∷ x₁ ∷ x₂ ∷ stack) stack si refl)) where + si01 : (stack stack1 : List (bt A)) → stackInvariant key tree orig stack → stack ≡ (x ∷ x₁ ∷ x₂ ∷ stack1) → PG A key tree stack + si01 _ _ s-nil () + si01 _ _ (s-right tree .(node _ _ tree₁ tree) tree₁ x s-nil) () + si01 stack stack1 si@(s-right tree₁ orig tree₂ {key₂} {v2} {st1} lt1 si₁@(s-right .(node _ _ tree₂ tree₁) .orig tree₃ {key₁} {v1} {st} lt2 si₂)) eq + with node→leaf∨IsNode x₂ + ... | case1 geq = ⊥-elim ( proj2 (si-property-5 eq si) geq ) + ... | case2 gn = record { + parent = x₁ ; uncle = IsNode.left gn ; grand = x₂ + ; pg = s2-1s2p lt1 (sym si03) (trans (IsNode.t=node gn) (node-cong refl refl refl si04 ) ) + ; rest = stack1 + ; stack=gp = cong₂ (λ j k → tree ∷ j ∷ k ) si03 si02 + } where + si02 : st ≡ x₂ ∷ stack1 + si02 = ∷-injectiveʳ ( ∷-injectiveʳ eq) + si03 : node key₂ v2 tree₂ tree₁ ≡ x₁ + si03 = just-injective (cong head (just-injective (cong tail eq))) + si05 : node key₁ v1 tree₃ (node key₂ v2 tree₂ tree₁) ≡ x₂ + si05 = sym (si-property1 (subst₂ (λ j k → stackInvariant key j orig k) refl si02 si₂)) + si04 : IsNode.right gn ≡ x₁ + si04 = begin + IsNode.right gn ≡⟨ just-injective (cong node-right ( begin + _ ≡⟨ sym (IsNode.t=node gn) ⟩ + x₂ ≡⟨ sym si05 ⟩ + node key₁ v1 tree₃ (node key₂ v2 tree₂ tree₁) ≡⟨ cong (λ k → node key₁ v1 tree₃ k ) si03 ⟩ + node key₁ v1 tree₃ x₁ ∎ )) ⟩ + x₁ ∎ where open ≡-Reasoning + si01 _ stack1 si@(s-right tree₃ orig tree₁ {key₂} {v2} lt1 (s-left .(node _ _ tree₁ tree₃) .orig tree₂ {key₁} {v1} {st} lt2 si₂)) eq + with node→leaf∨IsNode x₂ + ... | case1 geq = ⊥-elim ( proj2 (si-property-5 eq si) geq ) + ... | case2 gn = record { + parent = x₁ ; uncle = IsNode.right gn ; grand = x₂ + ; pg = s2-1sp2 lt1 (sym si03) (trans (IsNode.t=node gn) (node-cong refl refl si04 refl ) ) + ; rest = stack1 + ; stack=gp = cong₂ (λ j k → tree ∷ j ∷ k ) si03 si02 + } where + si02 : st ≡ x₂ ∷ stack1 + si02 = ∷-injectiveʳ ( ∷-injectiveʳ eq) + si03 : node key₂ v2 tree₁ tree₃ ≡ x₁ + si03 = just-injective (cong head (just-injective (cong tail eq))) + si05 : node key₁ v1 (node key₂ v2 tree₁ tree₃) tree₂ ≡ x₂ + si05 = sym (si-property1 (subst₂ (λ j k → stackInvariant key j orig k) refl si02 si₂ )) + si04 : IsNode.left gn ≡ x₁ + si04 = begin + IsNode.left gn ≡⟨ just-injective (cong node-left ( begin + _ ≡⟨ sym (IsNode.t=node gn) ⟩ + x₂ ≡⟨ sym si05 ⟩ + node key₁ v1 (node key₂ v2 tree₁ tree₃) tree₂ ≡⟨ cong (λ k → node key₁ v1 k tree₂ ) si03 ⟩ + node key₁ v1 x₁ tree₂ ∎ )) ⟩ + x₁ ∎ where open ≡-Reasoning + si01 _ _ (s-left tree₁ .(node _ _ tree₁ tree) tree x s-nil) () + si01 _ stack1 si@(s-left tree₃ orig tree₁ {key₂} {v2} lt1 (s-right .(node _ _ tree₃ tree₁) .orig tree₂ {key₁} {v1} {st} lt2 si₂)) eq + with node→leaf∨IsNode x₂ + ... | case1 geq = ⊥-elim ( proj2 (si-property-5 eq si) geq ) + ... | case2 gn = record { + parent = x₁ ; uncle = IsNode.left gn ; grand = x₂ + ; pg = s2-s12p lt1 (sym si03) (trans (IsNode.t=node gn) (node-cong refl refl refl si04 ) ) + ; rest = stack1 + ; stack=gp = cong₂ (λ j k → tree ∷ j ∷ k ) si03 si02 + } where + si02 : st ≡ x₂ ∷ stack1 + si02 = ∷-injectiveʳ ( ∷-injectiveʳ eq) + si03 : node key₂ v2 tree₃ tree₁ ≡ x₁ + si03 = just-injective (cong head (just-injective (cong tail eq))) + si05 : node key₁ v1 tree₂ (node key₂ v2 tree₃ tree₁) ≡ x₂ + si05 = sym (si-property1 (subst₂ (λ j k → stackInvariant key j orig k) refl si02 si₂ )) + si04 : IsNode.right gn ≡ x₁ + si04 = begin + IsNode.right gn ≡⟨ just-injective (cong node-right ( begin + _ ≡⟨ sym (IsNode.t=node gn) ⟩ + x₂ ≡⟨ sym si05 ⟩ + node key₁ v1 tree₂ _ ≡⟨ cong (λ k → node key₁ v1 tree₂ k ) si03 ⟩ + node key₁ v1 tree₂ x₁ ∎ )) ⟩ + x₁ ∎ where open ≡-Reasoning + si01 _ stack1 si@(s-left tree₃ orig tree₁ {key₂} {v2} lt1 (s-left .(node _ _ tree₃ tree₁) .orig tree₂ {key₁} {v1} {st} lt2 si₂)) eq + with node→leaf∨IsNode x₂ + ... | case1 geq = ⊥-elim ( proj2 (si-property-5 eq si) geq ) + ... | case2 gn = record { + parent = x₁ ; uncle = IsNode.right gn ; grand = x₂ + ; pg = s2-s1p2 lt1 (sym si03) (trans (IsNode.t=node gn) (node-cong refl refl si04 refl ) ) + ; rest = stack1 + ; stack=gp = cong₂ (λ j k → tree ∷ j ∷ k ) si03 si02 + } where + si02 : st ≡ x₂ ∷ stack1 + si02 = ∷-injectiveʳ ( ∷-injectiveʳ eq) + si03 : node key₂ v2 tree₃ tree₁ ≡ x₁ + si03 = just-injective (cong head (just-injective (cong tail eq))) + si05 : node key₁ v1 (node key₂ v2 tree₃ tree₁) tree₂ ≡ x₂ + si05 = sym (si-property1 (subst₂ (λ j k → stackInvariant key j orig k) refl si02 si₂ )) + si04 : IsNode.left gn ≡ x₁ + si04 = begin + IsNode.left gn ≡⟨ just-injective (cong node-left ( begin + _ ≡⟨ sym (IsNode.t=node gn) ⟩ + x₂ ≡⟨ sym si05 ⟩ + node key₁ v1 _ tree₂ ≡⟨ cong (λ k → node key₁ v1 k tree₂ ) si03 ⟩ + node key₁ v1 x₁ tree₂ ∎ )) ⟩ + x₁ ∎ where open ≡-Reasoning + +stackCase1 : {n : Level} {A : Set n} → {key : ℕ } → {tree orig : bt A } + → {stack : List (bt A)} → stackInvariant key tree orig stack + → stack ≡ orig ∷ [] → tree ≡ orig +stackCase1 {n} {A} {key} {tree} {.tree} {.(tree ∷ [])} s-nil eq = refl +stackCase1 {n} {A} {key} {tree} {orig} {.(tree ∷ _)} (s-right .tree .orig tree₁ x si) eq = ∷-injectiveˡ eq +stackCase1 {n} {A} {key} {tree} {orig} {.(tree ∷ _)} (s-left .tree .orig tree₁ x si) eq = ∷-injectiveˡ eq + +pg-prop-1 : {n : Level} (A : Set n) → (key : ℕ) → (tree orig : bt A ) + → (stack : List (bt A)) → (pg : PG A key tree stack) + → (¬ PG.grand pg ≡ leaf ) ∧ (¬ PG.parent pg ≡ leaf) +pg-prop-1 {_} A _ tree orig stack pg with PG.pg pg +... | s2-s1p2 _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫ +... | s2-1sp2 _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫ +... | s2-s12p _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫ +... | s2-1s2p _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫ + + +PGtoRBinvariant1 : {n : Level} {A : Set n} + → (tree orig : bt (Color ∧ A) ) + → {key : ℕ } + → (rb : RBtreeInvariant orig) + → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) + → RBtreeInvariant tree +PGtoRBinvariant1 tree .tree rb .(tree ∷ []) s-nil = rb +PGtoRBinvariant1 {n} {A} tree orig {key} rb (tree ∷ rest) (s-right .tree .orig tree₁ {key₁} {v1} x si) = rb01 ( node key₁ v1 tree₁ tree) refl si where + rb01 : (tree₂ : bt (Color ∧ A)) → tree₂ ≡ node key₁ v1 tree₁ tree → stackInvariant key tree₂ orig rest → RBtreeInvariant tree + rb01 tree₂ eq si with PGtoRBinvariant1 _ orig rb _ si + ... | rb-leaf = ⊥-elim ( bt-ne eq ) + ... | rb-red key value x x₁ x₂ t t₁ = subst (λ k → RBtreeInvariant k) (just-injective (cong node-right eq)) t₁ + ... | rb-black key value x t t₁ = subst (λ k → RBtreeInvariant k) (just-injective (cong node-right eq)) t₁ +PGtoRBinvariant1 {n} {A} tree orig {key} rb (tree ∷ rest) (s-left .tree .orig tree₁ {key₁} {v1} x si) = rb01 ( node key₁ v1 tree tree₁) refl si where + rb01 : (tree₂ : bt (Color ∧ A)) → tree₂ ≡ node key₁ v1 tree tree₁ → stackInvariant key tree₂ orig rest → RBtreeInvariant tree + rb01 tree₂ eq si with PGtoRBinvariant1 _ orig rb _ si + ... | rb-leaf = ⊥-elim ( bt-ne eq ) + ... | rb-red key value x x₁ x₂ t t₁ = subst (λ k → RBtreeInvariant k) (just-injective (cong node-left eq)) t + ... | rb-black key value x t t₁ = subst (λ k → RBtreeInvariant k) (just-injective (cong node-left eq)) t + + + +