Mercurial > hg > Gears > GearsAgda

changeset 852:08213b37782f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 29 Mar 2024 21:56:28 +0900
parents ea0f5b8a3567
children a333ecf93107
files hoareBinaryTree1.agda
diffstat 1 files changed, 11 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Fri Mar 29 20:44:28 2024 +0900
+++ b/hoareBinaryTree1.agda	Fri Mar 29 21:56:28 2024 +0900
@@ -1064,8 +1064,17 @@
         rr02 : treeInvariant (node key₂ ⟪ Red , v2 ⟫ t t₄)
         rr02 = RB-repl→ti _ _ _ _ ti (rbr-right lt 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) = ?
+      (t-right _ _ x₁ x₂ x₃ ti) (rbr-flip-rl x lt lt2 trb) = t-right _ _ x₁ rr00 x₃ (RTtoTI0 _ _ _ _ rr02 r-node ) where
+        rr00 : tr> key₁ t₂
+        rr00 = RB-repl→ti> _ _ _ _ _ trb lt x₂
+        rr02 : treeInvariant (node key₂ ⟪ Red , v2 ⟫ t₂ t₁)
+        rr02 = RB-repl→ti _ _ _ _ ti (rbr-left lt2 trb)
+RB-repl→ti (node _ ⟪ Black , v1 ⟫ (node key₂ ⟪ c2 , v2 ⟫ t t₁) (node _ ⟪ Red , v3 ⟫ t₂ t₃)) (node key₁ ⟪ Red , _ ⟫ .(to-black (node key₂ ⟪ c2 , _ ⟫  _ _)) (node key₃ ⟪ Black , _ ⟫ t₄ t₃)) key value 
+      (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-rl x lt lt2 trb) = t-node key₂ _ _ x₁ x₂ x₃ x₄ rr00 x₆ (RTtoTI0 _ _ _ _ ti r-node ) (RTtoTI0 _ _ _ _ rr02 r-node ) where
+        rr00 : tr> key₁ t₄
+        rr00 = RB-repl→ti> _ _ _ _ _ trb lt x₅
+        rr02 : treeInvariant (node key₃ ⟪ Red , v3 ⟫ t₄ t₃)
+        rr02 = RB-repl→ti _ _ _ _ ti₁ (rbr-left 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) = ?