--- a/hoareBinaryTree1.agda	Sat May 06 01:31:55 2023 +0900
+++ b/hoareBinaryTree1.agda	Sat May 06 19:21:16 2023 +0900
@@ -568,6 +568,14 @@
 RB→bt {n} A leaf = leaf
 RB→bt {n} A (node key ⟪ c , value ⟫ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁) 
 
+data replacedRBTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt (Color ∧ A) ) → Set n where
+    rbr-leaf : {ca cb : Color} → replacedRBTree key value leaf (node key ⟪ cb , value ⟫ leaf leaf)
+    rbr-node : {value₁ : A} → {ca cb : Color } → {t t₁ : bt (Color ∧ A)} → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ cb , value ⟫ t t₁) 
+    rbr-right : {k : ℕ } {v1 : A} → {ca cb : 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 ⟪ cb , v1 ⟫ t1 t) 
+    rbr-left : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)}
+          → k < key →  replacedRBTree key value t1 t →  replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t t2) 
+
 data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent uncle grand : bt A) → Set n where
     s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } 
         → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand 
@@ -802,9 +810,19 @@
           → stack ≡ tree ∷ to ∷ [] → t
         insertCase12 (node k1 ⟪ Red , v1 ⟫ leaf (node k2 ⟪ Black , v2 ⟫ t1 t2)) (rb-right-red x₁ ro) eq (s-right x s-nil) refl = ?
         insertCase12 (node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) leaf) (rb-left-red x₁ ro) eq (s-right x s-nil) refl = ?
-        insertCase12 (node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) (node k3 ⟪ Black , v3 ⟫ t3 t4)) (rb-node-red x₁ x₂ ro ro₁) eq (s-right x s-nil) refl = exit (node k1 ⟪ Red , v1 ⟫ t1 rot) (node k1 ⟪ Black , v1 ⟫ ? ?) (rb-node-black ? ? ? ?)
-           (subst₂ (λ j k → rotatedTree j k ) eq ? (rr-right ? rr-node rr-node roti))
-           (subst (λ k → replacedTree key ⟪ ? , value ⟫ ? ?) ? (r-right ? ri)) 
+        insertCase12 (node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) (node k3 ⟪ Black , v3 ⟫ t3 t4)) (rb-node-red x₁ x₂ ro ro₁) refl (s-right x s-nil) refl = exit rot1 repl1 ? ins13 ins12 where
+             rot1 : bt (Color ∧ A)
+             rot1 = node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) (node k3 ⟪ Black , v3 ⟫ t3 t4)
+             repl1 : bt (Color ∧ A)
+             repl1 = ?
+             ins12 : replacedTree key ⟪ ? , value ⟫ (child-replaced key rot1) repl1
+             ins12 = ?
+             ins13 : rotatedTree (node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) (node k3 ⟪ Black , v3 ⟫ t3 t4)) rot1
+             ins13 = rr-node
+
+        -- exit (node k1 ⟪ Red , v1 ⟫ t1 rot) (node k1 ⟪ Black , v1 ⟫ ? ?) (rb-node-black ? ? ? ?)
+        --   (subst₂ (λ j k → rotatedTree j k ) eq ? (rr-right ? rr-node rr-node roti))
+        --   (subst (λ k → replacedTree key ⟪ ? , value ⟫ ? ?) ? (r-right ? ri)) 
            -- k1 < key
            --     ⟪ red , k1 ⟫
            --   t1            tree → rot → repl