# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1706226884 -32400
# Node ID 3f6e13350420f1944ba2cb58f82f1441d79e8156
# Parent  aeb14a056896e751b35e95fa006d88ded565c76d
...

diff -r aeb14a056896 -r 3f6e13350420 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Fri Jan 26 04:55:57 2024 +0900
+++ b/hoareBinaryTree1.agda	Fri Jan 26 08:54:44 2024 +0900
@@ -758,19 +758,19 @@
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle            (node kp ⟪ Red   , vp ⟫ t t₁))  
                                     (node kg ⟪ Red ,   vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t t₂))
 
-    rbr-rotate-ll : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}   - case6
+    rbr-rotate-ll : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}   -- case6
          → color t₂ ≡ Red → replacedRBTree key value t₁ t₂
          → 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}   - case6
+    rbr-rotate-rr : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}   -- case6
          → color t₂ ≡ Red → 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₂ )
-    rbr-rotate-lr : {t t₁ t₂ t₃ uncle : bt (Color ∧ A)} {kg kp kn : ℕ} {vg vp vn : A}   - case56
+    rbr-rotate-lr : {t t₁ t₂ t₃ uncle : bt (Color ∧ A)} {kg kp kn : ℕ} {vg vp vn : A}   -- case56
          → replacedRBTree key value t (node kn ⟪ Red , vn ⟫ t₁ t₂)
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₃ t)  uncle) 
                                     (node kn ⟪ Black , vn ⟫ (node kp ⟪ Red , vp ⟫ t₃ t₁) (node kg ⟪ Red , vg ⟫ t₂ uncle))
-    rbr-rotate-rl : {t t₁ t₂ t₃ uncle : bt (Color ∧ A)} {kg kp kn : ℕ} {vg vp vn : A    - case56
+    rbr-rotate-rl : {t t₁ t₂ t₃ uncle : bt (Color ∧ A)} {kg kp kn : ℕ} {vg vp vn : A}   -- case56
          → replacedRBTree key value t (node kn ⟪ Red , vn ⟫ t₁ t₂)
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle                           (node kp ⟪ Red , vp ⟫ t  t₃)) 
                                     (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , vg ⟫ t₁ uncle) (node kp ⟪ Red , vp ⟫ t₂ t₃)) 
@@ -867,6 +867,9 @@
 ... | tri≈ ¬a b ¬c = rbi
 ... | tri> ¬a ¬b c = RBtreeRightDown _ _ rbi
 
+RBTtoRBI  : {n : Level} {A : Set n}  → (tree repl : bt (Color ∧ A)) → (key : ℕ) → (value : A) → RBtreeInvariant tree
+     → replacedRBTree key value tree repl → RBtreeInvariant repl
+RBTtoRBI  = ?
 --
 -- create RBT invariant after findRBT, continue to replaceRBT
 --