--- a/hoareBinaryTree1.agda	Sun Jun 02 03:36:07 2024 +0900
+++ b/hoareBinaryTree1.agda	Sun Jun 02 12:29:26 2024 +0900
@@ -1964,14 +1964,46 @@
     replaceRBP1 : t
     replaceRBP1 with RBI.state r
     ... | rebuild ceq bdepth-eq rot = rebuildCase orig refl ceq bdepth-eq rot 
-    ... | top-black eq rot = exit repl stack ? r
+    ... | top-black eq rot = exit repl stack (trans eq (cong (λ k → k ∷ []) rb00)) r where
+        rb00 : RBI.tree r ≡ orig
+        rb00 with si-property-last _ _ _ _ (subst (λ k → stackInvariant key (RBI.tree r) orig k) (eq) (RBI.si r))
+        ... | refl = refl
     ... | rotate repl-red pdepth-eq rot with stackToPG (RBI.tree r) orig stack (RBI.si r)
     ... | case1 eq  = exit repl stack eq r     -- no stack, replace top node
     ... | case2 (case1 eq) = insertCase12 orig refl eq rot (case1 repl-red) (RBI.si r)     -- one level stack, orig is parent of repl
     ... | case2 (case2 pg) with color (PG.parent pg) in pcolor
-    ... | Black = rebuildCase orig refl ? pdepth-eq rot where
-        rb00 : color (RBI.tree r) ≡ color repl   -- we cannot prove this
-        rb00 = black-children-color (RBI.origrb r) rot
+    ... | Black = insertCase1 where
+       rb00 : (pg : PG (Color ∧ A) (RBI.tree r) stack) → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg)
+       rb00 pg = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r)
+       treerb : (pg : PG (Color ∧ A) (RBI.tree r) stack) → RBtreeInvariant (PG.parent pg)
+       treerb pg = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (rb00 pg))
+       rb08 : (pg : PG (Color ∧ A) (RBI.tree r) stack) → treeInvariant (PG.parent pg)
+       rb08 pg = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (rb00 pg))
+       insertCase1 : t
+       insertCase1 with PG.pg pg
+       ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = next rb01 (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
+            tree = PG.parent pg
+            ; ¬leaf = subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())
+            ; origti = RBI.origti r
+            ; origrb = RBI.origrb r
+            ; treerb = treerb pg
+            ; replrb = ?
+            ; si = popStackInvariant _ _ _ _ _ (rb00 pg)
+            ; state = rebuild ? rb05 (subst (λ k → replacedRBTree key value k (node kp vp repl n1) ) (sym x) (rb02 rb04 ))
+           } ? where
+            rb01 : bt (Color ∧ A)
+            rb01 = node kp vp repl n1
+            rb03 : key < kp
+            rb03 = ?
+            rb04 :  ⟪ Black , proj2 vp ⟫ ≡ vp
+            rb04 = ?
+            rb02 : ⟪ Black , proj2 vp ⟫ ≡ vp → replacedRBTree key value (node kp vp (RBI.tree r) n1) (node kp vp repl n1)
+            rb02 eq = subst (λ k → replacedRBTree key value (node kp k (RBI.tree r) n1) (node kp k repl n1)) eq (rbr-black-left repl-red rb03 rot )
+            rb05 : black-depth rb01 ≡ black-depth (PG.parent pg)
+            rb05 = ?
+       ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ?
+       ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ?
+       ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ?
     ... | Red with PG.uncle pg in uneq
     ... | leaf = {!!} -- insertCase5
     ... | node key₁ ⟪ Black , value₁ ⟫ t₁ t₂ = {!!} -- insertCase5