# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1711542370 -32400
# Node ID 0355a1c14c13fc720fa19fd36adf6f80fb864f85
# Parent  1936bedf26a345b3344bc78170becc111f9367cd
...

diff -r 1936bedf26a3 -r 0355a1c14c13 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Wed Mar 27 19:44:44 2024 +0900
+++ b/hoareBinaryTree1.agda	Wed Mar 27 21:26:10 2024 +0900
@@ -1043,7 +1043,7 @@
         rr00 : (key₄ < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁
         rr00 = RB-repl→ti< _ _ _ _ _ trb x₇ ⟪ x₁ , ⟪ x₃ , x₄ ⟫ ⟫
 RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ t₁) leaf) (node key₂ ⟪ Red , _ ⟫ (node key₁ ⟪ Black , _ ⟫ t t₁) .(to-black leaf)) key value 
-      (t-left _ .key₂ x₁ x₂ x₃ ti) (rbr-flip-ll x trb) = t-left _ _ x₁ rr00 x₃ (RB-repl→ti _ _ _ _ ? ?) where
+      (t-left _ .key₂ x₁ x₂ x₃ ti) (rbr-flip-ll x trb) = t-left _ _ x₁ rr00 x₃ (RB-repl→ti _ _ _ _ (RB-repl→ti _ _ _ _ ti (rbr-left ? trb)) rbr-to-black ) where
         rr00 : tr< key₂ t 
         rr00 = RB-repl→ti< _ _ _ _ _ trb ? x₂
         rr01 : replacedRBTree ? ? (node key₁ ⟪ Red , ? ⟫ ? t₁) (node key₁ ⟪ Black , ? ⟫ t t₁)