# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1683458358 -32400
# Node ID ce0d41a84c2b84d5fdb5333459644aa532a9b1c9
# Parent  1bb96bc9eb45af62730d50f820fb3fa389189266
...

diff -r 1bb96bc9eb45 -r ce0d41a84c2b hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Sun May 07 13:57:47 2023 +0900
+++ b/hoareBinaryTree1.agda	Sun May 07 20:19:18 2023 +0900
@@ -611,6 +611,18 @@
        rest : List (bt A)
        stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest )
 
+record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A))) (C : bt (Color ∧ A) → bt (Color ∧ A) → List (bt (Color ∧ A)) → Set n) : Set n where
+   field
+     d rd : ℕ
+     tree0 rot : bt (Color ∧ A)
+     tree0rb : RBtreeInvariant tree0 d
+     replrb : RBtreeInvariant repl rd
+     d=rd : ( d ≡ rd ) ∨ ( suc d ≡ rd )
+     rotated : rotatedTree tree rot
+     si : stackInvariant key tree tree0 stack
+     ri : replacedRBTree key value (child-replaced key rot ) repl
+     ci : C tree repl stack     -- data continuation
+   
 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