Mercurial > hg > Gears > GearsAgda
changeset 851:ea0f5b8a3567
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 29 Mar 2024 20:44:28 +0900 |
| parents | 8647f4c5797c |
| children | 08213b37782f |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 5 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Fri Mar 29 16:14:32 2024 +0900 +++ b/hoareBinaryTree1.agda Fri Mar 29 20:44:28 2024 +0900 @@ -1058,12 +1058,14 @@ rr02 : treeInvariant (node key₃ ⟪ Red , v2 ⟫ left right₁ ) rr02 = RB-repl→ti _ _ _ _ ti (rbr-right lt trb) RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ Red , v2 ⟫ t t₁) (node key₃ ⟪ c3 , v3 ⟫ t₂ t₃)) (node key₁ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ t t₄) .(to-black (node key₃ ⟪ c3 , _ ⟫ _ _))) key value - (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-lr x lt lt2 trb) = t-node _ _ _ x₁ x₂ x₄ rr00 x₅ x₆ (RTtoTI0 _ _ _ _ rr02 r-node ) (RTtoTI0 _ _ _ _ ti₁ r-node ) where + (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-lr x lt lt2 trb) = t-node _ _ _ x₁ x₂ x₃ rr00 x₅ x₆ (RTtoTI0 _ _ _ _ rr02 r-node ) (RTtoTI0 _ _ _ _ ti₁ r-node ) where rr00 : tr< key₁ t₄ - rr00 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃ + rr00 = RB-repl→ti< _ _ _ _ _ trb lt2 x₄ rr02 : treeInvariant (node key₂ ⟪ Red , v2 ⟫ t t₄) rr02 = RB-repl→ti _ _ _ _ ti (rbr-right lt trb) -RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key value ti (rbr-flip-rl x lt lt2 trb) = ? +RB-repl→ti (node _ ⟪ Black , _ ⟫ leaf (node _ ⟪ Red , _ ⟫ t t₁)) (node key₁ ⟪ Red , v1 ⟫ .(to-black leaf) (node key₂ ⟪ Black , v2 ⟫ t₂ t₁)) key value + (t-right _ _ x₁ x₂ x₃ ti) (rbr-flip-rl x lt lt2 trb) = ? +RB-repl→ti .(node _ ⟪ Black , _ ⟫ (node key₁ _ _ _) (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black (node key₁ _ _ _)) (node _ ⟪ Black , _ ⟫ _ _)) key value (t-node key₁ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-rl x lt lt2 trb) = ? RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key value ti (rbr-flip-rr x lt trb) = ? RB-repl→ti .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) key value ti (rbr-rotate-ll x trb) = ? RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) key value ti (rbr-rotate-rr x trb) = ?