Mercurial > hg > Gears > GearsAgda
changeset 846:0355a1c14c13
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 27 Mar 2024 21:26:10 +0900 |
| parents | 1936bedf26a3 |
| children | 045dd0e43c56 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 1 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Wed Mar 27 19:44:44 2024 +0900 +++ b/hoareBinaryTree1.agda Wed Mar 27 21:26:10 2024 +0900 @@ -1043,7 +1043,7 @@ rr00 : (key₄ < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁ rr00 = RB-repl→ti< _ _ _ _ _ trb x₇ ⟪ x₁ , ⟪ x₃ , x₄ ⟫ ⟫ RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ t₁) leaf) (node key₂ ⟪ Red , _ ⟫ (node key₁ ⟪ Black , _ ⟫ t t₁) .(to-black leaf)) key value - (t-left _ .key₂ x₁ x₂ x₃ ti) (rbr-flip-ll x trb) = t-left _ _ x₁ rr00 x₃ (RB-repl→ti _ _ _ _ ? ?) where + (t-left _ .key₂ x₁ x₂ x₃ ti) (rbr-flip-ll x trb) = t-left _ _ x₁ rr00 x₃ (RB-repl→ti _ _ _ _ (RB-repl→ti _ _ _ _ ti (rbr-left ? trb)) rbr-to-black ) where rr00 : tr< key₂ t rr00 = RB-repl→ti< _ _ _ _ _ trb ? x₂ rr01 : replacedRBTree ? ? (node key₁ ⟪ Red , ? ⟫ ? t₁) (node key₁ ⟪ Black , ? ⟫ t t₁)