--- a/hoareBinaryTree1.agda	Sat Jun 08 20:15:19 2024 +0900
+++ b/hoareBinaryTree1.agda	Mon Jun 10 11:13:58 2024 +0900
@@ -907,12 +907,12 @@
                                     (node kp ⟪ Black , vp ⟫ (node kg ⟪ Red , vg ⟫ uncle t) t₂ )
     -- case56 the node is inner, make it outer and rotate grand
     rbr-rotate-lr : {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A}
-         → color t₃ ≡ Red → kp < key → key < kg
+         → color t₃ ≡ Black → kp < key → key < kg
          → replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁)     uncle)
                                     (node kn ⟪ Black , vn ⟫ (node kp ⟪ Red , vp ⟫ t t₂)     (node kg ⟪ Red , vg ⟫ t₃ uncle))
     rbr-rotate-rl : {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A}
-         → color t₃ ≡ Red → kg < key → key < kp
+         → color t₃ ≡ Black → kg < key → key < kp
          → replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle                           (node kp ⟪ Red , vp ⟫ t₁ t))
                                     (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , vg ⟫ uncle t₂) (node kp ⟪ Red , vp ⟫ t₃ t))
@@ -2179,7 +2179,65 @@
                 suc (black-depth (PG.parent pg) ) ≡⟨ sym (proj1 (black-children-eq refl (cong proj1 (sym rb14)) (subst (λ k → RBtreeInvariant k) x₁ rb02))) ⟩
                 black-depth (node kg vg (PG.parent pg) (PG.uncle pg)) ≡⟨ cong black-depth (sym x₁) ⟩
                 black-depth (PG.grand pg) ∎ where open ≡-Reasoning
-        ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ?
+                -- lt          : key < kp
+                -- x           : PG.parent pg ≡ node kp vp (RBI.tree r) n1
+                -- x₁          : PG.grand pg ≡ node kg vg (PG.parent pg) (PG.uncle pg)
+                -- eq          : node rkey vr rp-left rp-right ≡ RBI.repl r
+        ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase52 where
+          insertCase52 : t
+          insertCase52 = next (PG.grand pg ∷ PG.rest pg) record {
+            tree = PG.grand pg
+            ; repl = rb01
+            ; origti = RBI.origti r
+            ; origrb = RBI.origrb r
+            ; treerb = rb02
+            ; replrb = subst (λ k → RBtreeInvariant k) rb10 (rb-black _ _ rb18 (RBI.replrb r) (rb-red _ _ rb16 uncle-black rb19 rb06 rb05))
+            ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
+            ; state = rebuild (trans (cong color x₁) (cong proj1 (sym rb14))) rb17 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) rb11
+           } rb15 where
+                -- lt          : kp < key
+                -- x           : PG.parent pg ≡ node kp vp n1 (RBI.tree r)
+                -- x₁          : PG.grand pg ≡ node kg vg (PG.parent pg) (PG.uncle pg)
+                -- eq          : node rkey vr rp-left rp-right ≡ RBI.repl r
+            rb01 : bt (Color ∧ A)
+            rb01 = to-black (node rkey vr (node kp vp n1 rp-left) (to-red (node kg vg rp-right (PG.uncle pg))))
+            rb04 : kp < key
+            rb04 = lt
+            rb21 : key < kg   -- this can be a part of ParentGand relation
+            rb21 = si-property-< (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())) (subst (λ k → treeInvariant k ) x₁ (siToTreeinvariant _ _ _ _ (RBI.origti r) 
+                 (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)))) 
+                 (subst (λ k → stackInvariant key _ orig (PG.parent pg ∷ k ∷ PG.rest pg)) x₁ (popStackInvariant _ _ _ _ _ rb00))
+            rb16 : color n1 ≡ Black
+            rb16 = proj1 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) x rb09) (trans (cong color (sym x)) pcolor))
+            rb13 : ⟪ Red , proj2 vp ⟫ ≡ vp
+            rb13 with subst (λ k → color k ≡ Red ) x pcolor
+            ... | refl = refl
+            rb14 : ⟪ Black , proj2 vg ⟫ ≡ vg
+            rb14 with RBtreeParentColorBlack _ _ (subst (λ k → RBtreeInvariant k) x₁ rb02) (case1 pcolor)
+            ... | refl = refl
+            rb23 :  vr ≡ ⟪ Red , proj2 vr ⟫ 
+            rb23 with subst (λ k → color k ≡ Red ) (sym eq) repl-red
+            ... | refl = refl
+            rb20 : color rp-right ≡ Black
+            rb20 = proj2 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r) ) (cong proj1 rb23))
+            rb03 : replacedRBTree key value (node kg _ (node kp _ n1 (RBI.tree r)) (PG.uncle pg))
+               (node rkey ⟪ Black , proj2 vr ⟫ (node kp ⟪ Red , proj2 vp ⟫  n1 rp-left) (node kg ⟪ Red , proj2 vg ⟫ rp-right (PG.uncle pg)))
+            rb03 = rbr-rotate-lr rp-left rp-right kg kp rkey rb20 rb04 rb21  
+                (subst (λ k → replacedRBTree key value (RBI.tree r) k) (trans (sym eq) (cong (λ k → node rkey k rp-left rp-right) rb23 )) rot )
+            rb10 :  node rkey ⟪ Black , proj2 vr ⟫ (RBI.repl r) (node kg ⟪ Red , proj2 vg ⟫ n1 (PG.uncle pg)) ≡ rb01
+            rb10 = ?
+            rb11 : replacedRBTree key value (PG.grand pg) rb01
+            rb11 = subst₂ (λ j k → replacedRBTree key value j k) ? ? rb03
+            rb05 : RBtreeInvariant (PG.uncle pg)
+            rb05 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb02)
+            rb06 : RBtreeInvariant n1
+            rb06 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x rb09)
+            rb19 : black-depth n1 ≡ black-depth (PG.uncle pg)
+            rb19 = ? -- trans (sym ( proj2 (red-children-eq x (sym (cong proj1 rb13))  rb09) )) (RBtreeEQ (subst (λ k → RBtreeInvariant k) x₁ rb02))
+            rb18 : black-depth (RBI.repl r) ≡ black-depth n1 ⊔ black-depth (PG.uncle pg)
+            rb18 = ?
+            rb17 : suc (black-depth (node kp vp n1 rp-left) ⊔ (black-depth rp-right ⊔ black-depth (PG.uncle pg))) ≡ black-depth (PG.grand pg)
+            rb17 = ?
         ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ?
         ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ?
     replaceRBP1 : t