--- a/hoareBinaryTree1.agda	Thu Jun 13 00:50:25 2024 +0900
+++ b/hoareBinaryTree1.agda	Thu Jun 13 10:54:31 2024 +0900
@@ -1266,11 +1266,19 @@
         rr00 : (key₄ < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁
         rr00 = RB-repl→ti< _ _ _ _ _ trb x₇ ⟪ x₁ , ⟪ x₃ , x₄ ⟫ ⟫
 RB-repl→ti .(node key₂ ⟪ Black , value₁ ⟫ (node key₁ ⟪ Red , value₂ ⟫ _ t₁) leaf) (node key₂ ⟪ Red , value₁ ⟫ (node key₁ ⟪ Black , value₂ ⟫ t t₁) .(to-black leaf)) key value (t-left _ .key₂ x₁ x₂ x₃ ti) (rbr-flip-ll x () lt trb)
-RB-repl→ti (node key₂ ⟪ Black , _ ⟫ (node key₁ ⟪ Red , _ ⟫ t₀ leaf) (node key₃ ⟪ c1 , v1 ⟫ left right)) (node key₂ ⟪ Red , value₁ ⟫ (node _ ⟪ Black , value₂ ⟫ (node key₄ value₃ t t₁) .leaf) (node key₃ ⟪ Black , v1 ⟫ left right)) key value (t-node _ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-ll x y lt trb) = ?
-RB-repl→ti (node key₂ ⟪ Black , _ ⟫ (node key₁ ⟪ Red , _ ⟫ t₀ (node key₄ value₃ t₁ t₂)) (node key₃ ⟪ c0 , v1 ⟫ left right)) (node key₂ ⟪ Red , value₁ ⟫ (node _ ⟪ Black , value₂ ⟫ (node key₅ value₄ t t₃) .(node key₄ value₃ t₁ t₂)) (node key₃ ⟪ Black , v1 ⟫ left right)) key value (t-node _ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-ll x y lt trb) 
-    = t-node _ _ _ ? ? ? ? ? ? (t-node _ _ _ ? ? ? ? ? ? ? ?) ? where
-        rr00 : ?
-        rr00 = ?
+RB-repl→ti (node key₂ ⟪ Black , _ ⟫ (node key₁ ⟪ Red , _ ⟫ t₀ leaf) (node key₃ ⟪ c1 , v1 ⟫ left right)) (node key₂ ⟪ Red , value₁ ⟫ (node _ ⟪ Black , value₂ ⟫ (node key₄ value₃ t t₁) .leaf) (node key₃ ⟪ Black , v1 ⟫ left right)) key value (t-node _ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-ll x y lt trb) 
+    = t-node _ _ _ ? ? ? ? ? ? (t-left _ _ ? ? ? (RB-repl→ti _ _ _ _ ? trb)) (replaceTree1 _ _ _ ti₁) where
+        rr00 : (key₄ < key₁) ∧ tr< key₁ t ∧ tr< key₁ t₁
+        rr00 = RB-repl→ti< _ _ _ _ _ trb lt ?
+RB-repl→ti (node key₂ ⟪ Black , _ ⟫ (node key₁ ⟪ Red , _ ⟫ .leaf (node key₄ value₃ t₁ t₂)) (node key₃ ⟪ c0 , v1 ⟫ left right)) (node key₂ ⟪ Red , value₁ ⟫ (node _ ⟪ Black , value₂ ⟫ (node key₅ value₄ t t₃) .(node key₄ value₃ t₁ t₂)) (node key₃ ⟪ Black , v1 ⟫ left right)) key value (t-node _ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ (t-right .key₁ .key₄ x₇ x₈ x₉ ti) ti₁) (rbr-flip-ll x y lt trb) 
+    = t-node _ _ _ x₁ x₂ ⟪ <-trans (proj1 rr00) x₁ , ⟪ >-tr< (proj1 (proj2 rr00)) x₁  , >-tr< (proj2 (proj2 rr00)) x₁  ⟫ ⟫  x₄ x₅ x₆ (t-node _ _ _ (proj1 rr00) x₇ (proj1 (proj2 rr00)) (proj2 (proj2 (rr00))) x₈ x₉ (RB-repl→ti _ _ _ _ t-leaf trb) ti) (replaceTree1 _ _ _ ti₁) where
+        rr00 : (key₅ < key₁) ∧ tr< key₁ t ∧ tr< key₁ t₃
+        rr00 = RB-repl→ti< _ _ _ _ _ trb lt tt
+RB-repl→ti (node key₂ ⟪ Black , _ ⟫ (node key₁ ⟪ Red , _ ⟫ .(node key₆ _ _ _) (node key₄ value₃ t₁ t₂)) (node key₃ ⟪ c0 , v1 ⟫ left right)) (node key₂ ⟪ Red , value₁ ⟫ (node _ ⟪ Black , value₂ ⟫ (node key₅ value₄ t t₃) .(node key₄ value₃ t₁ t₂)) (node key₃ ⟪ Black , v1 ⟫ left right)) key value (t-node _ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ (t-node key₆ .key₁ .key₄ x₇ x₈ x₉ x₁₀ x₁₁ x₁₂ ti ti₂) ti₁) (rbr-flip-ll x y lt trb) 
+   = t-node _ _ _ x₁ x₂  ⟪ <-trans (proj1 rr00) x₁ , ⟪ >-tr< (proj1 (proj2 rr00)) x₁ , >-tr< (proj2 (proj2 rr00)) x₁ ⟫ ⟫  
+     x₄ x₅ x₆ (t-node _ _ _ (proj1 rr00) x₈ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) x₁₁ x₁₂ (RB-repl→ti _ _ _ _ ti trb) ti₂) (replaceTree1 _ _ _ ti₁) where
+        rr00 : (key₅ < key₁) ∧ tr< key₁ t ∧ tr< key₁ t₃ 
+        rr00 = RB-repl→ti< _ _ _ _ _ trb lt ⟪ x₇ , ⟪ x₉ , x₁₀ ⟫ ⟫
 RB-repl→ti (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ left right) leaf) (node key₂ ⟪ Red , v1 ⟫ (node key₃ ⟪ Black , v2 ⟫ left right₁) leaf) key value
       (t-left _ _ x₁ x₂ x₃ ti) (rbr-flip-lr x () lt lt2 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