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

diff -r ea0f5b8a3567 -r 08213b37782f hoareBinaryTree1.agda
--- 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) = ?