--- a/hoareBinaryTree1.agda	Fri Apr 21 10:36:49 2023 +0900
+++ b/hoareBinaryTree1.agda	Fri Apr 21 10:50:10 2023 +0900
@@ -593,17 +593,16 @@
 rbt-key {n} A (t-node-red key value x x₁ rb rb₁) = just key
 rbt-key {n} A (t-node-black key value x x₁ rb rb₁) = just key
 
-data rbstackInvariant2 {n : Level} {A : Set n}  {key : ℕ} {c : Color} {d : ℕ} (orig : RBTree A key c d ) : 
-        {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (parent : RBTree A k1 c1 d1) (grand : RBTree A k2 c2 d2) → Set n where
-    s-head :  rbstackInvariant2 orig ? orig
-    s-right : rbstackInvariant2 orig ? ? → rbstackInvariant2 orig ? ?
+data rbstackInvariant2 {n : Level} {A : Set n} (orig : bt A) : (parent grand : bt A) → Set n where
+    s2-left  :  {key : ℕ} {value : A} → (n1 : bt A) → rbstackInvariant2 orig (node key value orig n1) orig
+    s2-right :  {key : ℕ} {value : A} → (n1 : bt A) → rbstackInvariant2 orig (node key value n1 orig) orig
 
 data replacedTreeRotate  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt A ) → Set n where
-    r-leaf : replacedTreeRotate key value leaf (node key value leaf leaf)
-    r-node : {value₁ : A} → {t t₁ : bt A} → replacedTreeRotate key value (node key value₁ t t₁) (node key value t t₁) 
-    r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
+    rr-leaf : replacedTreeRotate key value leaf (node key value leaf leaf)
+    rr-node : {value₁ : A} → {t t₁ : bt A} → replacedTreeRotate key value (node key value₁ t t₁) (node key value t t₁) 
+    rr-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
           → k < key →  replacedTreeRotate key value t2 t →  replacedTreeRotate key value (node k v1 t1 t2) (node k v1 t1 t) 
-    r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
+    rr-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
           → key < k →  replacedTreeRotate key value t1 t →  replacedTreeRotate key value (node k v1 t1 t2) (node k v1 t t2) 
 
 rbsi-len :  {n : Level} {A : Set n}  {key : ℕ} {c : Color} {d : ℕ} (orig : RBTree A key c d ) {key₁ : ℕ }