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

diff -r 590e1435e41e -r 1936bedf26a3 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Thu Mar 21 16:31:16 2024 +0900
+++ b/hoareBinaryTree1.agda	Wed Mar 27 19:44:44 2024 +0900
@@ -785,11 +785,11 @@
     -- no rotation case
     rbr-leaf : replacedRBTree key value leaf (node key ⟪ Red , value ⟫ leaf leaf)
     rbr-node : {value₁ : A} → {ca : Color } → {t t₁ : bt (Color ∧ A)} → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ ca , value ⟫ t t₁)
+    rbr-to-black : {value₁ : A} → {t t₁ : bt (Color ∧ A)} → replacedRBTree key value (node key ⟪ Red , value₁ ⟫ t t₁) (node key ⟪ Black , value ⟫ t t₁)
     rbr-right : {k : ℕ } {v1 : A} → {ca : Color} → {t t1 t2 : bt (Color ∧ A)}
           → k < key →  replacedRBTree key value t2 t →  replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ ca , v1 ⟫ t1 t)
     rbr-left  : {k : ℕ } {v1 : A} → {ca : Color} → {t t1 t2 : bt (Color ∧ A)}
           → key < k →  replacedRBTree key value t1 t →  replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ ca , v1 ⟫ t t2) -- k < key → key < k
-
     -- case1 parent is black
     rbr-black-right : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ}
          → color t₂ ≡ Red → key₁ < key  → replacedRBTree key value t₁ t₂
@@ -892,6 +892,7 @@
      → replacedRBTree key value tree repl → key₁ < key → tr> key₁ tree → tr> key₁ repl
 RB-repl→ti> .leaf .(node key ⟪ Red , value ⟫ leaf leaf) key key₁ value rbr-leaf lt tr = ⟪ lt , ⟪ tt , tt ⟫ ⟫
 RB-repl→ti> .(node key ⟪ _ , _ ⟫ _ _) .(node key ⟪ _ , value ⟫ _ _) key key₁ value rbr-node lt tr = tr
+RB-repl→ti> .(node key ⟪ _ , _ ⟫ _ _) .(node key ⟪ _ , value ⟫ _ _) key key₁ value rbr-to-black lt tr = tr
 RB-repl→ti> .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-right x rbt) lt tr
    = ⟪ 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
@@ -930,6 +931,7 @@
      → replacedRBTree key value tree repl → key < key₁ → tr< key₁ tree → tr< key₁ repl
 RB-repl→ti< .leaf .(node key ⟪ Red , value ⟫ leaf leaf) key key₁ value rbr-leaf lt tr = ⟪ lt , ⟪ tt , tt ⟫ ⟫
 RB-repl→ti< .(node key ⟪ _ , _ ⟫ _ _) .(node key ⟪ _ , value ⟫ _ _) key key₁ value rbr-node lt tr = tr
+RB-repl→ti< .(node key ⟪ _ , _ ⟫ _ _) .(node key ⟪ _ , value ⟫ _ _) key key₁ value rbr-to-black lt tr = tr
 RB-repl→ti< .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-right x rbt) lt tr
    = ⟪ 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
@@ -1040,10 +1042,12 @@
      (t-node key₁ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-black-left x 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 key₂ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ t₁) leaf) (node key₂ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ t t₁) .(to-black leaf)) key value 
-      (t-left _ .key₂ x₁ x₂ x₃ ti) (rbr-flip-ll x trb) = t-left _ _ ? ? ? (RB-repl→ti ? _ ? ? ? ?) where
-        rr00 : tr< ? t 
-        rr00 = RB-repl→ti< _ _ _ _ _ trb ? ?
+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
+        rr00 : tr< key₂ t 
+        rr00 = RB-repl→ti< _ _ _ _ _ trb ? x₂
+        rr01 : replacedRBTree ? ? (node key₁ ⟪ Red , ? ⟫ ? t₁) (node key₁ ⟪ Black , ? ⟫ t t₁)
+        rr01 = ?
 RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ t₁) (node key₃ _ _ _)) (node key₂ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ t t₁) .(to-black (node key₃ _ _ _))) key value (t-node _ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti 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) = ?
@@ -1052,6 +1056,7 @@
 RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) key value ti (rbr-rotate-rr x 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 key ⟪ Red , _ ⟫ _ _) .(node key ⟪ Black , value ⟫ _ _) key value ti rbr-to-black = ?
 
 --
 -- if we consider tree invariant, this may be much simpler and faster