# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1712138578 -32400
# Node ID 35c09d99840c96ba4afab3068bc19e5a5295c7f0
# Parent  d181dd6068778efc6a04b30b4c8b80fc0acc33a6
...

diff -r d181dd606877 -r 35c09d99840c hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Tue Apr 02 20:42:52 2024 +0900
+++ b/hoareBinaryTree1.agda	Wed Apr 03 19:02:58 2024 +0900
@@ -828,7 +828,7 @@
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₁ t)    uncle)
                                     (node kp ⟪ Black , vp ⟫ t₂                             (node kg ⟪ Red , vg ⟫ t uncle))
     rbr-rotate-rr : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
-         → color t₂ ≡ Red → key < kp → replacedRBTree key value t₁ t₂
+         → color t₂ ≡ Red → kg < key → replacedRBTree key value t₁ t₂
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle                          (node kp ⟪ Red   , vp ⟫ t t₁))
                                     (node kp ⟪ Black , vp ⟫ (node kg ⟪ Red , vg ⟫ uncle t) t₂ )
     -- case56 the node is inner, make it outer and rotate grand
@@ -1156,7 +1156,17 @@
         rr03 = RTtoTI0 _ _ _ _(t-node _ _ _ {_} {value₁} {_} {_} {_} {_} {_} (proj1 x₄) x₂ (proj1 (proj2 x₄)) (proj2 (proj2 x₄)) x₅ x₆ ti₂ ti₁) r-node
         rr05 : tr> key₂ t₂
         rr05 = <-tr> x₅ x₁
-RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) key value ti (rbr-rotate-rr x lt trb) = ?
+RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ .leaf (node key₂ ⟪ Red , v2 ⟫ .leaf .leaf)) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₃ value₁ t₃ t₄)) key value 
+    (t-right .key₁ .key₂ x₁ x₂ x₃ (t-single .key₂ .(⟪ Red , v2 ⟫))) (rbr-rotate-rr x lt trb) = t-node _ _ _ x₁ ? tt tt ? ? (t-single _ _) (RB-repl→ti _ _ _ _ t-leaf trb) where
+        rr00 : (key₁ < key₃) ∧ tr> key₁ t₃ ∧ tr> key₁ t₄
+        rr00 = RB-repl→ti> _ _ _ _ _ trb lt tt
+RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ .leaf (node key₂ ⟪ Red , v2 ⟫ .leaf .(node key₃ _ _ _))) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) t₃) key value (t-right .key₁ .key₂ x₁ x₂ x₃ (t-right .key₂ key₃ x₄ x₅ x₆ ti)) (rbr-rotate-rr x lt trb) = ?
+RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ .leaf (node key₂ ⟪ Red , v2 ⟫ .(node key₃ _ _ _) .leaf)) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) t₃) key value (t-right .key₁ .key₂ x₁ x₂ x₃ (t-left key₃ .key₂ x₄ x₅ x₆ ti)) (rbr-rotate-rr x lt trb) = ?
+RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ .leaf (node key₂ ⟪ Red , v2 ⟫ .(node key₃ _ _ _) .(node key₄ _ _ _))) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) t₃) key value (t-right .key₁ .key₂ x₁ x₂ x₃ (t-node key₃ .key₂ key₄ x₄ x₅ x₆ x₇ x₈ x₉ ti ti₁)) (rbr-rotate-rr x lt trb) = ?
+RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ .(node key₃ _ _ _) (node key₂ ⟪ Red , v2 ⟫ .leaf .leaf)) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) t₃) key value (t-node key₃ .key₁ .key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti (t-single .key₂ .(⟪ Red , v2 ⟫))) (rbr-rotate-rr x lt trb) = ?
+RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ .(node key₃ _ _ _) (node key₂ ⟪ Red , v2 ⟫ .leaf .(node key₄ _ _ _))) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) t₃) key value (t-node key₃ .key₁ .key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti (t-right .key₂ key₄ x₇ x₈ x₉ ti₁)) (rbr-rotate-rr x lt trb) = ?
+RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ .(node key₃ _ _ _) (node key₂ ⟪ Red , v2 ⟫ .(node key₄ _ _ _) .leaf)) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) t₃) key value (t-node key₃ .key₁ .key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti (t-left key₄ .key₂ x₇ x₈ x₉ ti₁)) (rbr-rotate-rr x lt trb) = ?
+RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ .(node key₃ _ _ _) (node key₂ ⟪ Red , v2 ⟫ .(node key₄ _ _ _) .(node key₅ _ _ _))) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) t₃) key value (t-node key₃ .key₁ .key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti (t-node key₄ .key₂ key₅ x₇ x₈ x₉ x₁₀ x₁₁ x₁₂ ti₁ ti₂)) (rbr-rotate-rr x lt 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) = ?
 RB-repl→ti .(node kg ⟪ Black , _ ⟫ _ (node kp ⟪ Red , _ ⟫ _ _)) .(node kn ⟪ Black , _ ⟫ (node kg ⟪ Red , _ ⟫ _ t₂) (node kp ⟪ Red , _ ⟫ t₃ _)) key value ti (rbr-rotate-rl t₂ t₃ kg kp kn trb) = ?