Mercurial > hg > Gears > GearsAgda
changeset 938:cf9de6f45d50
rbr-flip
done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 14 Jun 2024 19:38:15 +0900 |
| parents | a452a969c910 |
| children | 3fee93d41dc1 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 2 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Fri Jun 14 18:01:03 2024 +0900 +++ b/hoareBinaryTree1.agda Fri Jun 14 19:38:15 2024 +0900 @@ -1336,10 +1336,9 @@ rr02 = ⟪ proj1 x₆ , ⟪ <-tr> x₁₁ x₂ , <-tr> x₁₂ x₂ ⟫ ⟫ RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ leaf (node key₂ ⟪ Red , v2 ⟫ t t₁)) (node _ ⟪ Red , _ ⟫ .(to-black leaf) (node _ ⟪ Black , v2 ⟫ t t₂)) key value (t-right _ _ x₁ x₂ x₃ ti) (rbr-flip-rr x () lt trb) -RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ c2 , v2 ⟫ t t₁) (node key₃ ⟪ Red , c3 ⟫ leaf t₃)) (node _ ⟪ Red , _ ⟫ .(to-black (node key₂ ⟪ c2 , v2 ⟫ t t₁)) (node _ ⟪ Black , c3 ⟫ .leaf (node key₄ value₁ t₄ t₅))) key value (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-rr x y lt trb) - = t-node _ _ _ x₁ x₂ x₃ x₄ x₅ rr01 (replaceTree1 _ _ _ ti) (t-right _ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ (treeRightDown _ _ ti₁) trb)) where +RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ c2 , v2 ⟫ t t₁) (node key₃ ⟪ Red , c3 ⟫ leaf t₃)) (node _ ⟪ Red , _ ⟫ .(to-black (node key₂ ⟪ c2 , v2 ⟫ t t₁)) (node _ ⟪ Black , c3 ⟫ .leaf (node key₄ value₁ t₄ t₅))) key value (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-rr x y lt trb) = t-node _ _ _ x₁ x₂ x₃ x₄ x₅ rr01 (replaceTree1 _ _ _ ti) (t-right _ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ (treeRightDown _ _ ti₁) trb)) where rr00 : (key₃ < key₄) ∧ tr> key₃ t₄ ∧ tr> key₃ t₅ - rr00 = ? + rr00 = RB-repl→ti> _ _ _ _ _ trb lt (proj2 (ti-property1 ti₁)) rr01 : (key₁ < key₄) ∧ tr> key₁ t₄ ∧ tr> key₁ t₅ rr01 = RB-repl→ti> _ _ _ _ _ trb (<-trans x₂ lt) x₆ RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ c2 , v2 ⟫ t t₁) (node key₃ ⟪ Red , c3 ⟫ (node key₄ value₁ t₂ t₅) .leaf)) (node _ ⟪ Red , _ ⟫ .(to-black (node key₂ ⟪ c2 , v2 ⟫ t t₁)) (node _ ⟪ Black , c3 ⟫ .(node key₄ value₁ t₂ t₅) (node key₅ value₂ t₄ t₆))) key value (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti (t-left .key₄ .key₃ x₇ x₈ x₉ ti₁)) (rbr-flip-rr x y lt trb) = t-node _ _ _ x₁ x₂ x₃ x₄ x₅ rr02 (replaceTree1 _ _ _ ti) (t-node _ _ _ x₇ (proj1 rr00) x₈ x₉ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) ti₁ (RB-repl→ti _ _ _ _ t-leaf trb)) where