# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1711769286 -32400
# Node ID a333ecf931076c20b99888eee30ba67c2d6c69bf
# Parent  08213b37782f96b42cd36ff40f2f7aa585317546
...

diff -r 08213b37782f -r a333ecf93107 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Fri Mar 29 21:56:28 2024 +0900
+++ b/hoareBinaryTree1.agda	Sat Mar 30 12:28:06 2024 +0900
@@ -811,7 +811,7 @@
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle            (node kp ⟪ Red   , vp ⟫ t₁ t))
                                     (node kg ⟪ Red ,   vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t₂ t))
     rbr-flip-rr : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
-         → color t₂ ≡ Red → kg < key   → replacedRBTree key value t₁ t₂
+         → color t₂ ≡ Red → kp < key   → replacedRBTree key value t₁ t₂
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle            (node kp ⟪ Red   , vp ⟫ t t₁))
                                     (node kg ⟪ Red ,   vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t t₂))
 
@@ -1075,7 +1075,18 @@
         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 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) = t-right _ _ x₁ x₂ rr00 (RTtoTI0 _ _ _ _ rr02 r-node ) where
+        rr00 : tr> key₁ t₂
+        rr00 = RB-repl→ti> _ _ _ _ _ trb (<-trans x₁ lt )  x₃
+        rr02 : treeInvariant (node key₂ ⟪ Red , v2 ⟫ t t₂)
+        rr02 = RB-repl→ti _ _ _ _ ti (rbr-right lt trb)
+RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ c2 , v2 ⟫ t t₁) (node key₃ ⟪ Red , c3 ⟫ t₂ t₃)) (node _ ⟪ Red , _ ⟫ .(to-black (node key₂ ⟪ c2 , _ ⟫ _ _)) (node _ ⟪ Black , c3 ⟫ t₂ t₄)) key value 
+    (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-rr x lt trb) = t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ rr00 (RTtoTI0 _ _ _ _ ti r-node ) (RTtoTI0 _ _ _ _ rr02 r-node ) where
+        rr00 : tr> key₁ t₄
+        rr00 = RB-repl→ti> _ _ _ _ _ trb (<-trans x₂ lt) x₆
+        rr02 : treeInvariant (node key₃ ⟪ Red , c3 ⟫ t₂ t₄)
+        rr02 = RB-repl→ti _ _ _ _ ti₁ (rbr-right 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) = ?
 RB-repl→ti .(node kg ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ _) _) .(node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₂) (node kg ⟪ Red , _ ⟫ t₃ _)) key value ti (rbr-rotate-lr t₂ t₃ kg kp kn trb) = ?