--- a/hoareBinaryTree1.agda	Wed Jan 24 20:24:41 2024 +0900
+++ b/hoareBinaryTree1.agda	Thu Jan 25 17:03:59 2024 +0900
@@ -547,6 +547,14 @@
 color leaf = Black
 color (node key ⟪ C , value ⟫ rb rb₁) = C
 
+to-red : {n : Level} {A : Set n} → (tree : bt (Color ∧ A)) → bt (Color ∧ A)
+to-red leaf = leaf
+to-red (node key ⟪ _ , value ⟫ t t₁) = (node key ⟪ Red , value ⟫ t t₁)
+
+to-black : {n : Level} {A : Set n} → (tree : bt (Color ∧ A)) → bt (Color ∧ A)
+to-black leaf = leaf
+to-black (node key ⟪ _ , value ⟫ t t₁) = (node key ⟪ Black , value ⟫ t t₁)
+
 black-depth : {n : Level} {A : Set n} → (tree : bt (Color ∧ A) ) → ℕ
 black-depth leaf = 0
 black-depth (node key ⟪ Red , value ⟫  t t₁) = black-depth t  ⊔ black-depth t₁
@@ -763,6 +771,9 @@
        rotated : replacedRBTree key value tree repl
        state : RBI-state key tree repl
 
+--
+-- if we consider tree invariant, this may be much simpler and faster
+--
 stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A )
            →  (stack : List (bt A)) → stackInvariant key tree orig stack
            → ( stack ≡ orig ∷ [] ) ∨ ( stack ≡ tree ∷ orig ∷ [] ) ∨ PG A tree stack
@@ -848,6 +859,7 @@
      → (orig tree : bt (Color ∧ A))
      → (stack : List (bt (Color ∧ A)))
      → (r : RBI key value orig tree stack )
+     → (pg : PG (Color ∧ A) tree stack)
      → (next : (current : bt (Color ∧ A)) → (stack1 : List (bt (Color ∧ A)))
         → (r : RBI key value orig current stack1 )
         → length stack1 < length stack  → t )
@@ -867,6 +879,7 @@
      → (orig tree : bt (Color ∧ A))
      → (stack : List (bt (Color ∧ A)))
      → (r : RBI key value orig tree stack )
+     → (pg : PG (Color ∧ A) tree stack)
      → (next : (current : bt (Color ∧ A)) → (stack1 : List (bt (Color ∧ A)))
         → (r : RBI key value orig current stack1 )
         → length stack1 < length stack  → t )
@@ -886,6 +899,7 @@
      → (orig tree : bt (Color ∧ A))
      → (stack : List (bt (Color ∧ A)))
      → (r : RBI key value orig tree stack )
+     → (pg : PG (Color ∧ A) tree stack)
      → (next : (tree1 : (bt (Color ∧ A))) →  (stack1 : List (bt (Color ∧ A)))
         → (r : RBI key value orig tree1 stack1 )
         → length stack1 < length stack  → t )
@@ -905,6 +919,7 @@
      → (orig tree : bt (Color ∧ A))
      → (stack : List (bt (Color ∧ A)))
      → (r : RBI key value orig tree stack )
+     → (pg : PG (Color ∧ A) tree stack)
      → (next : (tree1 : (bt (Color ∧ A))) →  (stack1 : List (bt (Color ∧ A)))
         → (r : RBI key value orig tree1 stack1 )
         → length stack1 < length stack  → t )
@@ -912,7 +927,7 @@
         →  stack1 ≡ (orig ∷ [])
         →  RBI key value orig repl stack1
         → t ) → t
-insertCase5 {n} {m} {A} {t} key value = {!!} where
+insertCase5 {n} {m} {A} {t} key value orig tree stack r pg next exit = {!!} where
     -- check inner repl case
     --     node-key parent < node-key repl < node-key grand  → rotateLeft  parent    then insertCase6
     --     node-key grand  < node-key repl < node-key parent → rotateRight parent    then insertCase6
@@ -990,7 +1005,7 @@
        --  RBI key value (node key₁ ⟪ Black , value₄ ⟫ left right) repl stack
        --
        insertCase13 : (v : Color ∧ A ) → v ≡ value₁ → black-depth repl ≡ black-depth (child-replaced key (RBI.tree r)) → t
-       insertCase13 ⟪ Black , value₄ ⟫ refl beq with <-cmp key key₁ | child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left right) in creq
+       insertCase13 ⟪ cl , value₄ ⟫ refl beq with <-cmp key key₁ | child-replaced key (node key₁ ⟪ cl , value₄ ⟫ left right) in creq
        ... | tri< a ¬b ¬c | cr = ⊥-elim (¬c c)
        ... | tri≈ ¬a b ¬c | cr = ⊥-elim (¬c c)
        ... | tri> ¬a ¬b c | cr = exit (node key₁ ⟪ Black , value₄ ⟫ left repl) (orig ∷ [])  refl record {
@@ -1001,7 +1016,6 @@
          ; replrb = ?
          ; si = s-nil
          ; rotated = ?
-         ; ri = ?
          ; state = rebuild ? 
          } where
            rb09 : {n : Level} {A : Set n} →  {key key1 key2 : ℕ}  {value value1  : A} {t1 t2  : bt (Color ∧ A)}
@@ -1012,11 +1026,24 @@
            tkey : {n : Level} {A : Set n } → (rbt : bt (Color ∧ A)) → ℕ
            tkey (node key value t t2) = key
            tkey leaf = {!!} -- key is none
-       insertCase13 ⟪ Red , value₄ ⟫ eq beq = ? -- can't happen
-... | case2 (case2 pg) with PG.uncle pg
+... | case2 (case2 pg) with PG.uncle pg in uneq
 ... | leaf = ? -- insertCase5 
 ... | node key₁ ⟪ Black , value₁ ⟫ t₁ t₂ = ? -- insertCase5
-... | node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ = next ? ? ? ?   -- going to two level up
+... | node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ with PG.pg pg 
+... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = next (to-red (node kg vg (to-black (node kp vp repl n1)) (to-black (PG.uncle pg)))) (PG.rest pg) 
+    record { 
+         tree = PG.grand pg
+         ; origti = RBI.origti r
+         ; origrb = RBI.origrb r
+         ; treerb = ?
+         ; replrb = ?
+         ; si = ?
+         ; rotated = ?
+         ; state = rotate refl ?
+     }  ?
+... | 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₁ = ?