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

diff -r 35c09d99840c -r 7c1afe76e743 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Wed Apr 03 19:02:58 2024 +0900
+++ b/hoareBinaryTree1.agda	Thu Apr 04 18:29:11 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 → 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 kp ⟪ Black , vp ⟫ (node kg ⟪ Red , vg ⟫ uncle t) t₂ )
     -- case56 the node is inner, make it outer and rotate grand
@@ -1156,19 +1156,43 @@
         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 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₄
+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 , _ ⟫))) (rbr-rotate-rr x lt trb) 
+      = t-node _ _ _ x₁ (proj1 rr00) tt tt (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (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₃ value₃ t t₁))) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₄ value₁ t₃ t₄)) key value 
+   (t-right .key₁ .key₂ x₁ x₂ x₃ (t-right .key₂ key₃ x₄ x₅ x₆ ti)) (rbr-rotate-rr x lt trb) 
+      = t-node _ _ _ x₁ (proj1 rr00) tt tt (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (t-single _ _ ) (RB-repl→ti _ _ _ _ ti trb) where
+        rr00 : (key₂ < key₄) ∧ tr> key₂ t₃ ∧ tr> key₂ t₄
+        rr00 = RB-repl→ti> _ _ _ _ _ trb lt ⟪ x₄ , ⟪ x₅ , x₆ ⟫ ⟫ 
+RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ leaf (node key₂ ⟪ Red , v2 ⟫ (node key₃ _ _ _) leaf)) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₄ value₁ t₃ t₄)) key value 
+    (t-right .key₁ .key₂ x₁ x₂ x₃ (t-left key₃ .key₂ x₄ x₅ x₆ ti)) (rbr-rotate-rr x lt trb) 
+       = t-node _ _ _ x₁ (proj1 rr00) tt ⟪ x₄ , ⟪ x₅ , x₆ ⟫ ⟫ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (t-right _ _ (proj1 x₂) (proj1 (proj2 x₂)) (proj2 (proj2 x₂)) ti)  (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 ⟫ leaf (node key₂ ⟪ Red , v2 ⟫ (node key₃ _ _ _) (node key₄ _ _ _))) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₅ value₁ t₃ 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) = t-node _ _ _ x₁ (proj1 rr00) tt ⟪ x₄ , ⟪ x₆ , x₇ ⟫ ⟫ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (t-right _ _ (proj1 x₂) (proj1 (proj2 x₂)) (proj2 (proj2 x₂)) ti) (RB-repl→ti _ _ _ _ ti₁ trb) where
+        rr00 : (key₂ < key₅) ∧ tr> key₂ t₃ ∧ tr> key₂ t₄
+        rr00 = RB-repl→ti> _ _ _ _ _ trb lt ⟪ x₅ , ⟪ x₈ , x₉ ⟫ ⟫
+RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ .(node key₃ _ _ _) (node key₂ ⟪ Red , v2 ⟫ .leaf .leaf)) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₄ value₁ t₃ 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) 
+     = t-node _ _ _ x₂ (proj1 rr00) ⟪ <-trans x₁ x₂ , ⟪ >-tr< x₃ x₂ , >-tr< x₄ x₂ ⟫ ⟫  tt (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (t-left _ _ x₁ x₃ x₄ ti) (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 ⟫ (node key₃ v3 t t₁) (node key₂ ⟪ Red , v2 ⟫ leaf (node key₄ _ _ _))) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₅ value₁ t₃ 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) 
+      = t-node _ _ _ x₂ (proj1 rr00) ⟪ <-trans x₁ x₂ , ⟪ >-tr< x₃ x₂ , >-tr< x₄ x₂ ⟫ ⟫ tt (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (t-left _ _ x₁ x₃ x₄ ti) (RB-repl→ti _ _ _ _ ti₁ trb) where
+        rr00 : (key₂ < key₅) ∧ tr> key₂ t₃ ∧ tr> key₂ t₄
+        rr00 = RB-repl→ti> _ _ _ _ _ trb lt ⟪ x₇ , ⟪ x₈ , x₉ ⟫ ⟫
+RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₃ _ _ _) (node key₂ ⟪ Red , v2 ⟫ (node key₄ _ _ _) leaf)) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₅ value₁ t₃ 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) = t-node _ _ _ x₂ (proj1 rr00) ⟪ ? , ⟪ ? , ? ⟫ ⟫ ? (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (t-node _ _ _  ? ? ? ? ? ? ? ?) (RB-repl→ti _ _ _ _ ? 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 ⟫ .(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) = ?
+RB-repl→ti .(node kg ⟪ Black , _ ⟫ _ (node kp ⟪ Red , _ ⟫ _ _)) .(node kn ⟪ Black , _ ⟫ (node kg ⟪ Red , _ ⟫ _ t₂) (node kp ⟪ Red , _ ⟫ leaf _)) key value ti (rbr-rotate-rl t₂ leaf kg kp kn trb) = ?
+RB-repl→ti .(node kg ⟪ Black , _ ⟫ _ (node kp ⟪ Red , _ ⟫ _ _)) .(node kn ⟪ Black , _ ⟫ (node kg ⟪ Red , _ ⟫ _ t₂) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value ti (rbr-rotate-rl t₂ (node key₁ value₁ t₃ t₄) kg kp kn trb) = ?
 
 --
 -- if we consider tree invariant, this may be much simpler and faster