# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1705887934 -32400
# Node ID f655afa1b8ead5353d0442b874848f4a62fb8191
# Parent  194b5ae1a7a0a138242e9669d35d05e01100f1e8
...

diff -r 194b5ae1a7a0 -r f655afa1b8ea hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Mon Jan 22 10:22:56 2024 +0900
+++ b/hoareBinaryTree1.agda	Mon Jan 22 10:45:34 2024 +0900
@@ -701,17 +701,14 @@
 findRBTreeTest = findTest 14 testRBTree0 testRBI0
        $ λ tr s P O → (record {tree = tr ; stack = s ; ti = (proj1 P) ; si = (proj2 P)})
 
-
-
-
-
-data replacedRBTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt (Color ∧ A) ) → Set n where
-    rbr-leaf : {ca cb : Color} → replacedRBTree key value leaf (node key ⟪ cb , value ⟫ leaf leaf)
-    rbr-node : {value₁ : A} → {ca cb : Color } → {t t₁ : bt (Color ∧ A)} → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ cb , value ⟫ t t₁)
-    rbr-right : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)}
-          → k < key →  replacedRBTree key value t2 t →  replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t1 t)
-    rbr-left : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)}
-          → key < k →  replacedRBTree key value t1 t →  replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t t2) -- k < key → key < k 
+-- we can re use replacedTree
+-- data replacedRBTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt (Color ∧ A) ) → Set n where
+--     rbr-leaf : {ca cb : Color} → replacedTree key value leaf (node key ⟪ cb , value ⟫ leaf leaf)
+--     rbr-node : {value₁ : A} → {ca cb : Color } → {t t₁ : bt (Color ∧ A)} → replacedTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ cb , value ⟫ t t₁)
+--     rbr-right : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)}
+--           → k < key →  replacedTree key value t2 t →  replacedTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t1 t)
+--     rbr-left : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)}
+--           → key < k →  replacedTree key value t1 t →  replacedTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t t2) -- k < key → key < k 
 
 data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent uncle grand : bt A) → Set n where
     s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
@@ -739,7 +736,7 @@
        replrb : RBtreeInvariant repl
        si : stackInvariant key tree orig stack
        rotated : rotatedTree tree rot
-       ri : replacedRBTree key value (child-replaced key rot ) repl
+       ri : replacedTree key ⟪ Red , value ⟫ (child-replaced key rot ) repl
        repl-red : color repl ≡ Red
        repl-eq : black-depth (child-replaced key rot ) ≡ black-depth repl
 
@@ -953,7 +950,7 @@
              } where
                rb07 :  black-depth (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) ≡ black-depth left ⊔ black-depth repl
                rb07 with <-cmp key key₁
-               ... | tri< a ¬b ¬c = rb08 where
+               ... | tri< a ¬b ¬c = rb08 where   -- r : RBI key value (node key₁ ⟪ Black , value₄ ⟫ left right) repl stack
                    rb08 : black-depth left ≡ black-depth left ⊔ black-depth repl
                    rb08 = ?
                ... | tri≈ ¬a b ¬c = ? where
@@ -970,11 +967,11 @@
                tkey : {n : Level} {A : Set n } → (rbt : bt (Color ∧ A)) → ℕ
                tkey (node key value t t2) = key
                tkey leaf = {!!} -- key is none
-               rb051 : {n : Level} {A : Set n} {key key1 : ℕ } {value : A} {t t1 t2 : bt (Color ∧ A)} {c : Color} → replacedRBTree key value (node key1 ⟪ c , value ⟫ t1 t2) (node key1 ⟪ c , value ⟫ t1 t) → key1 < key
+               rb051 : {n : Level} {A : Set n} {key key1 : ℕ } {value : A} {t t1 t2 : bt (Color ∧ A)} {c : Color} → replacedTree key ⟪ ? , value ⟫ (node key1 ⟪ c , value ⟫ t1 t2) (node key1 ⟪ c , value ⟫ t1 t) → key1 < key
                rb051 = {!!}
                rb052 : {key key₁ : ℕ} → stackInvariant key (RBI.tree r) orig stack → key < key₁
                rb052 = {!!}
-               rb05 : RBtreeInvariant (node key₁ ⟪ Red , value₄ ⟫ left repl) ∧  replacedRBTree key value
+               rb05 : RBtreeInvariant (node key₁ ⟪ Red , value₄ ⟫ left repl) ∧  replacedTree key ⟪ ? , value ⟫
                     (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) (node key₁ ⟪ Red , value₄ ⟫ left repl)
                rb05 with RBI.origrb r | rb04 si eq refl | RBI.replrb r in eqrepl | <-cmp  key₁ (tkey repl) -- si and ri have key's relation 
                ... | rb-single key₂ value₂ | refl | rb-single key₃ value | tri< a ¬b ¬c = {!!} -- need paternmatch with c