--- a/hoareBinaryTree1.agda	Mon Mar 18 21:08:17 2024 +0900
+++ b/hoareBinaryTree1.agda	Tue Mar 19 10:03:04 2024 +0900
@@ -964,23 +964,6 @@
        rr00 : kn < key₁ 
        rr00 = proj1 rr01
 
-ti-replace-left : {n : Level} {A : Set n} → (t1 t2 t : bt (Color ∧ A) ) → (key k : ℕ ) → (value v1 : A) → (c : Color) → treeInvariant (node k ⟪ c , v1 ⟫  t1 t2)
-       → replacedRBTree key value t1 t → treeInvariant (node k ⟪ c , v1 ⟫  t t2)
-ti-replace-left .leaf t2 .(node _ ⟪ Red , _ ⟫ leaf leaf) _ _ _ _ _ ti rbr-leaf = ?
-ti-replace-left .(node _ ⟪ _ , _ ⟫ _ _) t2 .(node _ ⟪ _ , _ ⟫ _ _) _ _ _ _ _ ti rbr-node = ?
-ti-replace-left .(node _ ⟪ _ , _ ⟫ _ _) t2 .(node _ ⟪ _ , _ ⟫ _ _) _ _ _ _ _ ti (rbr-right x rbt) = ?
-ti-replace-left .(node _ ⟪ _ , _ ⟫ _ _) t2 .(node _ ⟪ _ , _ ⟫ _ _) _ _ _ _ _ ti (rbr-left x rbt) = ?
-ti-replace-left .(node _ ⟪ Black , _ ⟫ _ _) t2 .(node _ ⟪ Black , _ ⟫ _ _) _ _ _ _ _ ti (rbr-black-right x rbt) = ?
-ti-replace-left .(node _ ⟪ Black , _ ⟫ _ _) t2 .(node _ ⟪ Black , _ ⟫ _ _) _ _ _ _ _ ti (rbr-black-left x rbt) = ?
-ti-replace-left .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) t2 .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) _ _ _ _ _ ti (rbr-flip-ll x rbt) = ?
-ti-replace-left .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) t2 .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) _ _ _ _ _ ti (rbr-flip-lr x rbt) = ?
-ti-replace-left .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) t2 .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) _ _ _ _ _ ti (rbr-flip-rl x rbt) = ?
-ti-replace-left .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) t2 .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) _ _ _ _ _ ti (rbr-flip-rr x rbt) = ?
-ti-replace-left .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) t2 .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) _ _ _ _ _ ti (rbr-rotate-ll x rbt) = ?
-ti-replace-left .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) t2 .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) _ _ _ _ _ ti (rbr-rotate-rr x rbt) = ?
-ti-replace-left .(node kg ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ _) _) t2 .(node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₂) (node kg ⟪ Red , _ ⟫ t₃ _)) _ _ _ _ _ ti (rbr-rotate-lr t₂ t₃ kg kp kn rbt) = ?
-ti-replace-left .(node kg ⟪ Black , _ ⟫ _ (node kp ⟪ Red , _ ⟫ _ _)) t2 .(node kn ⟪ Black , _ ⟫ (node kg ⟪ Red , _ ⟫ _ t₂) (node kp ⟪ Red , _ ⟫ t₃ _)) _ _ _ _ _ ti (rbr-rotate-rl t₂ t₃ kg kp kn rbt) = ?
-
 RB-repl→ti : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A) ) → (key : ℕ ) → (value : A) → treeInvariant tree 
        → replacedRBTree key value tree repl → treeInvariant repl
 RB-repl→ti .leaf .(node key ⟪ Red , value ⟫ leaf leaf) key value ti rbr-leaf = t-single key ⟪ Red , value ⟫
@@ -1008,7 +991,23 @@
      (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 _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key value ti (rbr-left x trb) = ti-replace-left _ _ _ _ _ _ _ _ ti trb 
+RB-repl→ti .(node key₁ ⟪ _ , _ ⟫ leaf leaf) (node key₁ ⟪ _ , _ ⟫ (node key₂ value₁ left left₁) leaf) key value 
+   (t-single _ .(⟪ _ , _ ⟫)) (rbr-left x trb) = t-left _ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ t-leaf trb) where
+        rr00 : (key₂ < key₁) ∧ tr< key₁ left ∧ tr< key₁ left₁
+        rr00 = RB-repl→ti< _ _ _ _ _ trb x tt
+RB-repl→ti .(node key₂ ⟪ _ , _ ⟫ leaf (node key₁ _ t₁ t₂)) (node key₂ ⟪ _ , _ ⟫ (node key₃ value₁ t t₃) (node key₁ _ t₁ t₂)) key value 
+   (t-right _ key₁ x₁ x₂ x₃ ti) (rbr-left x trb) = t-node _ _ _ (proj1 rr00) x₁  (proj1 (proj2 rr00))(proj2 (proj2 rr00)) x₂ x₃ rr01 ti where
+        rr00 : (key₃ < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₃
+        rr00 = RB-repl→ti< _ _ _ _ _ trb x tt
+        rr01 : treeInvariant (node key₃ value₁ t t₃)
+        rr01 = RB-repl→ti _ _ _ _ t-leaf trb
+RB-repl→ti .(node _ ⟪ _ , _ ⟫ (node key₁ _ _ _) leaf) (node key₃ ⟪ _ , _ ⟫ (node key₂ value₁ t t₁) leaf) key value 
+    (t-left key₁ _ x₁ x₂ x₃ ti) (rbr-left x trb) = t-left key₂ _ ? ? ? (RB-repl→ti _ _ _ _ ti trb) where
+        rr00 : (key₁ < key₂) ∧ tr< key₁ t ∧ tr< key₁ t₁
+        rr00 = ?
+        rr01 : (key₂ < key₃) ∧ tr< key₃ t ∧ tr< key₃ t₁
+        rr01 = RB-repl→ti< _ _ _ _ _ trb x ?
+RB-repl→ti .(node _ ⟪ _ , _ ⟫ (node key₁ _ _ _) (node key₂ _ _ _)) .(node _ ⟪ _ , _ ⟫ _ (node key₂ _ _ _)) key value (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-left x trb) = ?
 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 _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key value ti (rbr-flip-ll x trb) = ?
@@ -1100,7 +1099,7 @@
 replaceRBTNode = ?
 
 --
--- RBT is blanced with the stack, simply rebuild tree without totation
+-- RBT is blanced with the stack, simply rebuild tree without rototation
 --
 rebuildRBT : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A)