# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1715565543 -32400
# Node ID e92daa8d617b47bdb293a8f24a69ce391c1d2b69
# Parent  0aac292a5e1c3dd4e676f4607aa9d1e43390de67
main part start again

diff -r 0aac292a5e1c -r e92daa8d617b hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Sun May 12 22:55:14 2024 +0900
+++ b/hoareBinaryTree1.agda	Mon May 13 10:59:03 2024 +0900
@@ -1507,7 +1507,7 @@
  → (stack : List (bt (Color ∧ A)))
  → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
  → (exit : (r : RBI key value tree0 tree1 stack ) → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )) → t
-replaceRBTNode = ?
+replaceRBTNode key value tree0 rbi tree1 stack rbi-stack exit = ?
 
 --
 -- RBT is blanced with the stack, simply rebuild tree without rototation
@@ -1525,7 +1525,7 @@
         →  stack1 ≡ (orig ∷ [])
         →  RBI key value orig repl stack1
         → t ) → t
-rebuildRBT = ?
+rebuildRBT key value orig repl stack r bdepth-eq next exit = ?
 
 insertCase5 : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A)