Mercurial > hg > Gears > GearsAgda
changeset 869:adc1c927513c
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 05 Apr 2024 10:35:28 +0900 |
| parents | 85cd4d55db75 |
| children | 315efbf0148f |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 1 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Fri Apr 05 10:03:45 2024 +0900 +++ b/hoareBinaryTree1.agda Fri Apr 05 10:35:28 2024 +0900 @@ -1190,7 +1190,7 @@ = t-node _ _ _ x₂ (proj1 rr00) ⟪ <-trans x₁ x₂ , ⟪ >-tr< x₃ x₂ , >-tr< x₄ x₂ ⟫ ⟫ ⟪ x₇ , ⟪ x₈ , x₉ ⟫ ⟫ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (t-node _ _ _ x₁ (proj1 x₅) x₃ x₄ (proj1 (proj2 x₅)) (proj2 (proj2 x₅)) ti ti₁) (RB-repl→ti _ _ _ _ t-leaf trb) where rr00 : (key₂ < key₅) ∧ tr> key₂ t₃ ∧ tr> key₂ t₄ rr00 = RB-repl→ti> _ _ _ _ _ trb lt tt -RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₃ _ _ _) (node key₂ ⟪ Red , v2 ⟫ (node key₄ _ _ _) (node key₅ _ _ _))) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₆ value₁ t₃ t₄)) key value +RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₃ _ _ _) (node key₂ ⟪ Red , v2 ⟫ (node key₄ _ left right) (node key₅ _ _ _))) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₆ value₁ t₃ t₄)) key value (t-node key₃ key₁ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti (t-node key₄ key₂ key₅ x₇ x₈ x₉ x₁₀ x₁₁ x₁₂ ti₁ ti₂)) (rbr-rotate-rr x lt trb) = t-node _ _ _ x₂ (proj1 rr00) ⟪ <-trans x₁ x₂ , ⟪ >-tr< x₃ x₂ , >-tr< x₄ x₂ ⟫ ⟫ ⟪ x₇ , ⟪ x₉ , x₁₀ ⟫ ⟫ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RTtoTI0 _ _ _ _ (t-node _ _ _ {_} {value₁} x₁ (proj1 x₅) x₃ x₄ (<-tr> ? ?) ? ti ti₁ ) r-node ) (RB-repl→ti _ _ _ _ ti₂ trb) where