# HG changeset patch
# User Moririn
# Date 1702291864 -32400
# Node ID a03d00eba6b7e144a9de6f7f172c5c93ed420e67
# Parent  0eee181bd7155e125fb5904a3aecda611a1fa9bd
can use blackdepth=?

diff -r 0eee181bd715 -r a03d00eba6b7 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Sat Dec 09 14:57:21 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon Dec 11 19:51:04 2023 +0900
@@ -965,20 +965,25 @@
                 → key < key1 
                rb09 (rb-right-red x x1 x2) = x
                -- rb05 should more general
-               inkey : {n : Level} {A : Set n } → (rbt : bt (Color ∧ A)) → ℕ
-               inkey (node key value t t2) = key  
+               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 : ℕ } {value : A} → (c : Color) → (t t1 : bt (Color ∧ A)) → 0 ≡ black-depth (node key ⟪ c , value ⟫ t t1)
+               rb051 c t t1 = {!!}
                rb05 : RBtreeInvariant (node key₁ ⟪ Red , value₄ ⟫ left repl) ∧  replacedRBTree 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 (inkey orig) (inkey repl)
+               rb05 with RBI.origrb r | rb04 si eq refl | RBI.replrb r in eqrepl | <-cmp (tkey orig) (tkey repl) -- si and ri have key's relation 
                ... | rb-single key₂ value₂ | refl | rb-single key₃ value | tri< a ¬b ¬c = ⟪ rb-right-red a refl (RBI.replrb r) , {!!} ⟫
-               ... | rb-single key₂ value₂ | refl | rb-single key₃ value | tri≈ ¬a b ¬c = {!!} -- key is unique
+               ... | rb-single key₂ value₂ | refl | rb-single key₃ value | tri≈ ¬a b ¬c = {!!} -- key is unique ? 
                ... | rb-single key₂ value₂ | refl | rb-single key₃ value | tri> ¬a ¬b c = ⊥-elim (¬a {!!})
                ... | rb-single key₂ value₂ | refl | rb-right-red x x₁ rb | t = {!!} -- cant happen ? red - red
-               ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | t = {!!} --⟪ rb-right-red {!!} {!!} (RBI.replrb r) , {!!}  ⟫ -- if c₁ is Black , need rotate . 
+               ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | tri< a ¬b ¬c = ⟪ rb-right-red a (blackdepth≡ leaf {!!} {!!} {!!} {!!}) (RBI.replrb r) , {!!} ⟫ -- t₁ t₂ = leaf , c₁ = Red 
+               ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | tri≈ ¬a b ¬c = {!!}
+               ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | tri> ¬a ¬b c = ⊥-elim {!!}
                ... | rb-single key₂ value₂ | refl | rb-left-red x x₁ rb | t = {!!} --red -red
-               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | t = {!!} --⟪ rb-right-red (rb09 (proj1 rb05)) ({!!}) (RBI.replrb r) , {!!} ⟫ -- if c₁ is Black , need rotate .
-               ... | rb-single key₂ value₂ | refl | rb-node-red x x₁ x₂ rb x₃ rb₁ | t = {!!}-- red -red
-               ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ | t = {!!} --⟪ rb-right-red (rb09 (proj1 rb05)) (DepthCal {!!} {!!} {!!}) {!!} , {!!} ⟫
+               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | t = {!!} 
+               ... | rb-single key₂ value₂ | refl | rb-node-red x x₁ x₂ rb x₃ rb₁ | t = {!!}　-- red-red
+               ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ | t = {!!} 
                --... | rb-right-black x x₁ t | refl | rb | t = ? --⟪ proj1 {!!} , {!!} ⟫
                --... | rb-left-black x x₁ t | refl | rb | t = {!!} --⟪ rb-node-red ? ? ? ? ? ? , ? ⟫
                --... | rb-node-black x x₁ x₂ t x₃ t₁ | refl | rb | t = {!!}