# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1711002337 -32400
# Node ID ee2dd920e41432f39fae816383b6523b2f66fb3f
# Parent  27664016173afd1033e91cc249d2341c323157ed
...

diff -r 27664016173a -r ee2dd920e414 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Wed Mar 20 09:08:39 2024 +0900
+++ b/hoareBinaryTree1.agda	Thu Mar 21 15:25:37 2024 +0900
@@ -792,10 +792,10 @@
 
     -- case1 parent is black
     rbr-black-right : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ}
-         → color t₂ ≡ Red → replacedRBTree key value t₁ t₂
+         → color t₂ ≡ Red → key₁ < key  → replacedRBTree key value t₁ t₂
          → replacedRBTree key value (node key₁ ⟪ Black , value₁ ⟫ t t₁) (node key₁ ⟪ Black , value₁ ⟫ t t₂)
     rbr-black-left : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ}
-         → color t₂ ≡ Red → replacedRBTree key value t₁ t₂
+         → color t₂ ≡ Red  → key < key₁ → replacedRBTree key value t₁ t₂
          → replacedRBTree key value (node key₁ ⟪ Black , value₁ ⟫ t₁ t) (node key₁ ⟪ Black , value₁ ⟫ t₂ t)
 
     -- case2 both parent and uncle are red (should we check uncle color?), flip color and up
@@ -896,9 +896,9 @@
    = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti> _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫
 RB-repl→ti> .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-left x rbt) lt tr
    = ⟪ proj1 tr , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt (proj1 (proj2 tr)) , proj2 (proj2 tr) ⟫ ⟫
-RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-right x rbt) lt tr
+RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-right x _ rbt) lt tr
    = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti> _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫
-RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-left x rbt) lt tr
+RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-left x _ rbt) lt tr
    = ⟪ proj1 tr , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt (proj1 (proj2 tr)) , proj2 (proj2 tr) ⟫ ⟫
 RB-repl→ti> .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value (rbr-flip-ll x rbt) lt tr
    = ⟪ proj1 tr , ⟪ ⟪ proj1 (proj1 (proj2 tr))  , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt (proj1 (proj2 (proj1 (proj2 tr))))
@@ -934,9 +934,9 @@
    = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti< _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫
 RB-repl→ti< .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-left x rbt) lt tr
    = ⟪ proj1 tr , ⟪ RB-repl→ti< _ _ _ _ _ rbt lt (proj1 (proj2 tr)) , proj2 (proj2 tr) ⟫ ⟫
-RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-right x rbt) lt tr
+RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-right x _ rbt) lt tr
    = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti< _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫
-RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-left x rbt) lt tr
+RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-left x _ rbt) lt tr
    = ⟪ proj1 tr , ⟪ RB-repl→ti< _ _ _ _ _ rbt lt (proj1 (proj2 tr)) , proj2 (proj2 tr) ⟫ ⟫
 RB-repl→ti< .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value (rbr-flip-ll x rbt) lt tr
    = ⟪ proj1 tr , ⟪ ⟪ proj1 (proj1 (proj2 tr))  , ⟪ RB-repl→ti< _ _ _ _ _ rbt lt (proj1 (proj2 (proj1 (proj2 tr))))
@@ -1006,11 +1006,28 @@
         rr00 : (key₂ < key₃) ∧ tr< key₃ t ∧ tr< key₃ t₁
         rr00 = RB-repl→ti< _ _ _ _ _ trb x ⟪ x₁ , ⟪ x₂ , x₃ ⟫ ⟫
 RB-repl→ti .(node key₃ ⟪ _ , _ ⟫ (node key₁ _ _ _) (node key₂ _ t₁ t₂)) (node key₃ ⟪ _ , _ ⟫ (node key₄ value₁ t t₃) (node key₂ _ t₁ t₂)) key value 
-    (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-left x trb) = t-node _ _ _ ? ? ? ? ? ? (RB-repl→ti _ _ _ _ ti trb) ti₁ where
+    (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-left x trb) = t-node _ _ _ (proj1 rr00) x₂ (proj1 (proj2 rr00))  (proj2 (proj2 rr00))  x₅ x₆ (RB-repl→ti _ _ _ _ ti trb) ti₁ where
         rr00 : (key₄ < key₃) ∧ tr< key₃ t ∧ tr< key₃ t₃
         rr00 = RB-repl→ti< _ _ _ _ _ trb x ⟪ x₁ , ⟪ x₃ , x₄ ⟫ ⟫
-RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key value ti (rbr-black-right x trb) = ?
-RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key value ti (rbr-black-left x trb) = ?
+RB-repl→ti .(node x₁ ⟪ Black , c ⟫ leaf leaf) (node x₁ ⟪ Black , c ⟫ leaf (node key₁ value₁ t t₁)) key value 
+    (t-single x₂ .(⟪ Black , c ⟫)) (rbr-black-right x x₄ trb) = t-right _ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ t-leaf trb) where
+        rr00 : (x₁ < key₁) ∧ tr> x₁ t ∧ tr> x₁ t₁    
+        rr00 = RB-repl→ti> _ _ _ _ _ trb x₄ tt
+RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ leaf (node key₁ _ _ _)) (node key₂ ⟪ Black , _ ⟫ leaf (node key₃ value₁ t₂ t₃)) key value 
+    (t-right _ key₁ x₁ x₂ x₃ ti) (rbr-black-right  x x₄ trb) = t-right _ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ ti trb) where
+        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 key₁ _ _ _) leaf) (node key₂ ⟪ Black , _ ⟫ (node key₁ _ _ _) (node key₃ value₁ t₂ t₃)) key value (t-left key₁ _ x₁ x₂ x₃ ti) (rbr-black-right x x₄ trb) = t-node _ _ _ x₁ (proj1 rr00) x₂ x₃ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) ti (RB-repl→ti _ _ _ _ t-leaf trb) where
+        rr00 : (key₂ < key₃) ∧ tr> key₂ t₂ ∧ tr> key₂ t₃
+        rr00 = RB-repl→ti> _ _ _ _ _ trb x₄ tt
+RB-repl→ti .(node key₃ ⟪ Black , _ ⟫ (node key₁ _ _ _) (node key₂ _ _ _)) (node key₃ ⟪ Black , _ ⟫ (node key₁ _ _ _) (node key₄ value₁ t₂ t₃)) key value 
+      (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-black-right x x₇ trb) = t-node _ _ _ x₁ (proj1 rr00) x₃ x₄ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) ti (RB-repl→ti _ _ _ _ ti₁ trb) where
+        rr00 : (key₃ < key₄) ∧ tr> key₃ t₂ ∧ tr> key₃ t₃
+        rr00 = RB-repl→ti> _ _ _ _ _ trb x₇ ⟪ x₂ , ⟪ x₅ , x₆ ⟫ ⟫
+RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ leaf leaf) (node key₂ ⟪ Black , _ ⟫ t .leaf) key value (t-single .key₂ .(⟪ Black , _ ⟫)) (rbr-black-left x x₇ trb) = ?
+RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ leaf (node key₁ _ _ _)) (node key₂ ⟪ Black , _ ⟫ t .(node key₁ _ _ _)) key value (t-right .key₂ key₁ x₁ x₂ x₃ ti) (rbr-black-left x x₇ trb) = ?
+RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ (node key₁ _ _ _) leaf) (node key₂ ⟪ Black , _ ⟫ t .leaf) key value (t-left key₁ .key₂ x₁ x₂ x₃ ti) (rbr-black-left x x₇ trb) = ?
+RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ (node key₁ _ _ _) (node key₃ _ _ _)) (node key₂ ⟪ Black , _ ⟫ t .(node key₃ _ _ _)) key value (t-node key₁ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-black-left x x₇ trb) = ?
 RB-repl→ti .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key value ti (rbr-flip-ll x trb) = ?
 RB-repl→ti .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key value ti (rbr-flip-lr x trb) = ?
 RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key value ti (rbr-flip-rl x trb) = ?