--- a/hoareBinaryTree1.agda	Sun Mar 17 12:44:37 2024 +0900
+++ b/hoareBinaryTree1.agda	Sun Mar 17 20:29:43 2024 +0900
@@ -964,9 +964,34 @@
        rr00 : kn < key₁ 
        rr00 = proj1 rr01
 
-RB-repl→ti : {n : Level} {A : Set n} → {key : ℕ } → {value : A} → {tree repl : bt (Color ∧ A) }
-     → treeInvariant tree → replacedRBTree key value tree repl → treeInvariant repl
-RB-repl→ti = ?
+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 ⟫
+RB-repl→ti .(node key ⟪ _ , _ ⟫ leaf leaf) .(node key ⟪ _ , value ⟫ leaf leaf) key value (t-single .key .(⟪ _ , _ ⟫)) rbr-node = t-single key ⟪ _ , value ⟫
+RB-repl→ti .(node key ⟪ _ , _ ⟫ leaf (node key₁ _ _ _)) .(node key ⟪ _ , value ⟫ leaf (node key₁ _ _ _)) key value 
+   (t-right .key key₁ x x₁ x₂ ti) rbr-node = t-right key key₁ x x₁ x₂ ti
+RB-repl→ti .(node key ⟪ _ , _ ⟫ (node key₁ _ _ _) leaf) .(node key ⟪ _ , value ⟫ (node key₁ _ _ _) leaf) key value 
+   (t-left key₁ .key x x₁ x₂ ti) rbr-node = t-left key₁ key x x₁ x₂ ti
+RB-repl→ti .(node key ⟪ _ , _ ⟫ (node key₁ _ _ _) (node key₂ _ _ _)) .(node key ⟪ _ , value ⟫ (node key₁ _ _ _) (node key₂ _ _ _)) key value 
+   (t-node key₁ .key key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) rbr-node = t-node key₁ key key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁
+RB-repl→ti (node key₁ ⟪ ca , v1 ⟫ leaf leaf) (node key₁ ⟪ ca , v1 ⟫ leaf tree@(node key₂ value₁ t t₁)) key value 
+   (t-single key₁ ⟪ ca , v1 ⟫) (rbr-right x trb) = t-right _ _  (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (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 _ ⟪ _ , _ ⟫ leaf (node key₁ _ _ _)) .(node _ ⟪ _ , _ ⟫ leaf _) key value (t-right _ key₁ x₁ x₂ x₃ ti) (rbr-right x trb) = ?
+RB-repl→ti .(node _ ⟪ _ , _ ⟫ (node key₁ _ _ _) leaf) .(node _ ⟪ _ , _ ⟫ (node key₁ _ _ _) _) key value (t-left key₁ _ x₁ x₂ x₃ ti) (rbr-right x trb) = ?
+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-right x trb) = ?
+RB-repl→ti .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key value 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) = ?
+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) = ?
+RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key value ti (rbr-flip-rr x trb) = ?
+RB-repl→ti .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) key value ti (rbr-rotate-ll x trb) = ?
+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) = ?
 
 --
 -- if we consider tree invariant, this may be much simpler and faster