--- a/hoareBinaryTree1.agda	Sat Apr 22 19:15:59 2023 +0900
+++ b/hoareBinaryTree1.agda	Sun Apr 23 14:29:09 2023 +0900
@@ -600,10 +600,14 @@
 rbt-key {n} A (t-node-black key value x x₁ rb rb₁) = just key
 
 data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent grand : bt A) → Set n where
-    s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent : bt A } → parent ≡ node kp vp self n1 → ParentGrand self parent (node kg vg parent n2) 
-    s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent : bt A } → parent ≡ node kp vp n1 self → ParentGrand self parent (node kg vg parent n2) 
-    s2-s12p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent : bt A } → parent ≡ node kp vp self n1 → ParentGrand self parent (node kg vg n2 parent) 
-    s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent : bt A } → parent ≡ node kp vp n1 self → ParentGrand self parent (node kg vg n2 parent) 
+    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 grand 
+    s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } 
+        → parent ≡ node kp vp n1 self → grand ≡ node kg vg parent n2 → ParentGrand self parent grand 
+    s2-s12p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } 
+        → parent ≡ node kp vp self n1 → grand ≡ node kg vg n2 parent → ParentGrand self parent grand 
+    s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } 
+        → parent ≡ node kp vp n1 self → grand ≡ node kg vg n2 parent → ParentGrand self parent grand 
 
 data rotatedTree  {n : Level} {A : Set n}  : (before after : bt A ) → Set n where
     rr-node : {t : bt A} → rotatedTree t t
@@ -616,6 +620,24 @@
           → rotatedTree ta ta1 → rotatedTree tb tb1 → rotatedTree tc tc1
           → rotatedTree (node kb vb ta (node ka va tb tc) ) (node ka va (node kb vb ta1 tb1)  tc1) 
 
+record PG {n : Level } (A : Set n) (stack : List (bt A)) : Set n where
+    field
+       self parent grand : bt A
+       pg : ParentGrand self parent grand
+       rest : List (bt A)
+       stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest )
+
+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 stack
+stackToPG {n} {A} {key} tree .tree .(tree ∷ []) s-nil = case1 refl
+stackToPG {n} {A} {key} tree .(node _ _ _ tree) .(tree ∷ node _ _ _ tree ∷ []) (s-right x s-nil) = case2 (case1 refl)
+stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ grand ∷ rest) (s-right {t0} {t1} {t2} {k1} {v1} x (s-right {t3} {t4} {t5} {k2} {v2} x₁ si)) = case2 (case2
+    record { self = tree ; parent = node k1 v1 t2 tree ;  grand = grand ; pg = s2-1s2p  refl ?  ; rest = rest ; stack=gp = refl } )
+stackToPG {n} {A} {key} tree orig .(tree ∷ node _ _ _ tree ∷ _) (s-right x (s-left x₁ si)) = ?
+stackToPG {n} {A} {key} tree orig .(tree ∷ _) (s-left x si) = ?
+
+
 rbsi-len :  {n : Level} {A : Set n} {orig parent grand : bt A}
      → ParentGrand orig parent grand → ℕ
 rbsi-len {n} {A} {s} {p} {g} st = ?
@@ -659,28 +681,13 @@
         → length stack1 < length stack  → t )
      → (exit : {k1 d1 : ℕ} {c1 : Color} → (repl1 : RBTree A k1 c1 d1 ) → (rot : bt A )
          → (ri : rotatedTree (RB→bt A orig) rot ) → replacedTree key value rot (RB→bt A repl1) → t ) → t
-replaceRBP {n} {m} {A} {t} key value {_} {key1} orig tree stack si next exit = insertCase1 tree stack _ _ refl refl si where
+replaceRBP {n} {m} {A} {t} key value {_} {key1} orig tree stack si next exit = insertCase1 stack _ _ refl refl si where
     insertCase2 : {k0 k1 d0 d1 d2 : ℕ} {c0 c1 c2 : Color} → (tree : RBTree A k0 c0 d0) 
       → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) 
       → (stack : List (bt A)) → (tr to : bt A) → RB→bt A grand ≡ tr →  RB→bt A orig ≡ to → (si : stackInvariant key tr to stack ) 
       → (pg : ParentGrand (RB→bt A tree) (RB→bt A parent) tr ) → t
     insertCase2 tree parent grand stack tr to treq toeq si pg = ?
-    insertCase1 : {k1 d1 : ℕ} {c1 : Color } (tree : RBTree A k1 c1 d1)
-       (stack : List (bt A)) → (tr to : bt A) → RB→bt A tree ≡ tr →  RB→bt A orig ≡ to → (si : stackInvariant key tr to stack ) → t
-    insertCase1 (rb-leaf _) .(RB→bt A (rb-leaf _) ∷ []) .(RB→bt A (rb-leaf _)) .(RB→bt A (rb-leaf _)) refl oeq s-nil = ?
-    insertCase1 (rb-leaf _) .(RB→bt A (rb-leaf _) ∷ _) .(RB→bt A (rb-leaf _)) to refl oeq (s-right x si) = ?
-    insertCase1 (rb-leaf _) .(RB→bt A (rb-leaf _) ∷ _) .(RB→bt A (rb-leaf _)) to refl oeq (s-left x si) = ?
-    insertCase1 (rb-single _ value _) .(tr ∷ []) tr .tr req oeq s-nil = ?
-    insertCase1 (rb-single _ value _) .(tr ∷ _) tr to req oeq (s-right x si) = ?
-    insertCase1 (rb-single _ value _) .(tr ∷ _) tr to req oeq (s-left x si) = ?
-    insertCase1 (t-right-red _ value x (rb-leaf _)) stack tr to req oeq si = ?
-    insertCase1 (t-right-red _ value x (rb-single _ value₁ .Black)) stack tr to req oeq si = ?
-    insertCase1 (t-right-red _ value x (t-right-black _ value₁ x₁ tree)) stack tr to req oeq si = ?
-    insertCase1 (t-right-red _ value x (t-left-black _ value₁ x₁ tree)) stack tr to req oeq si = ?
-    insertCase1 (t-right-red _ value x (t-node-black _ value₁ x₁ x₂ tree tree₁)) stack tr to req oeq si = ?
-    insertCase1 (t-right-black _ value x tree) stack tr to req oeq si = ?
-    insertCase1 (t-left-red _ value x tree) stack tr to req oeq si = ?
-    insertCase1 (t-left-black _ value x tree) stack tr to req oeq si = ?
-    insertCase1 (t-node-red _ value x x₁ tree tree₁) stack tr to req oeq si = ?
-    insertCase1 (t-node-black _ value x x₁ tree tree₁) stack tr to req oeq si = ?
+    insertCase1 : (stack : List (bt A)) → (tr to : bt A) → RB→bt A tree ≡ tr →  RB→bt A orig ≡ to → (si : stackInvariant key tr to stack ) → t
+    insertCase1 = ?
 
+