--- a/hoareBinaryTree1.agda	Sat Oct 28 10:47:31 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon Nov 13 18:55:58 2023 +0900
@@ -669,6 +669,15 @@
     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)
 
+RBtreeCopy : {n m : Level} {A : Set n} {t : Set m} {key : ℕ} {value : A} {c : Color} → (tree tree0 : bt (Color ∧ A) )
+   → (stack : List  (bt (Color ∧ A)) )
+   → ( treeInvariant tree ∧  stackInvariant key tree tree0 stack)
+   → ( next : (tree tree0 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) 
+       → ( treeInvariant tree ∧  stackInvariant key tree tree0 stack )
+       → replacedRBTree key value tree0 tree → t ) 
+   → ( exit : (repl : bt (Color ∧ A)) → replacedRBTree key value tree0 repl → t ) → t
+RBtreeCopy = ?
+
 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
@@ -882,8 +891,8 @@
     insertCase10 : (tr0 : bt (Color ∧ A)) → tr0 ≡ RBI.rot r → color tr0 ≡ Black → t
     insertCase10 leaf eq refl = exit repl stack ? r     -- no stack, replace top node
     insertCase10 tr0@(node key₁ ⟪ Black , value₁ ⟫ left right) tr0=rot refl with <-cmp key key₁ 
-    ... | tri< a ¬b ¬c = exit ? stack ? ?     
-    ... | tri≈ ¬a b ¬c = ?
+    ... | tri< a ¬b ¬c = ?
+    ... | tri≈ ¬a b ¬c = next ? ? ? ?
     ... | tri> ¬a ¬b c = ?
     insertCase1 : t
     insertCase1 with stackToPG (RBI.tree r) orig stack (RBI.si r)