# HG changeset patch
# User Moririn
# Date 1700471868 -32400
# Node ID 772a6bb0b6142ecae7c3bb8a8d835fea71341136
# Parent  418ab1fa2acad1a67de03472c1f5db90ea96d8ba
merged

diff -r 418ab1fa2aca -r 772a6bb0b614 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Mon Nov 20 10:31:44 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon Nov 20 18:17:48 2023 +0900
@@ -692,6 +692,16 @@
     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
@@ -910,8 +920,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)