# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1698311477 -32400
# Node ID e1737f00a7aa62dfb53ee34db4aec5a02de1e69e
# Parent  e9ba6a5bc64b6e3fa6a6788d9a00c68712c5d3d2
...

diff -r e9ba6a5bc64b -r e1737f00a7aa hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Tue Oct 24 10:33:48 2023 +0900
+++ b/hoareBinaryTree1.agda	Thu Oct 26 18:11:17 2023 +0900
@@ -700,67 +700,6 @@
        repl-red : color repl ≡ Red
        repl-eq : black-depth (child-replaced key rot ) ≡ black-depth repl
 
---   r (b , b)    inserting a node into black node does not change the black depth, but color may change
---       → b (b , r ) ∨ b (r , b)
---   b (b , b)
---       → b (b , r ) ∨ b (r , b)
---   b (r , b)    inserting to right → b (r , r )
---   b (r , b)    inserting to left may increse black depth, need rotation
---      find b in left and move the b to the right (one down or two down)
---
-rbi-case1 : {n : Level} {A : Set n} → {key d : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) )
-           → RBtreeInvariant parent
-           → RBtreeInvariant repl
-           → {left right : bt (Color ∧ A) } → parent ≡ node key ⟪ Black , value ⟫ left right
-           →    (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl  ) )
-             ∧  (color left  ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) )
-rbi-case1 {n} {A} {key} = {!!}
-
-rbi-case31 : {n : Level} {A : Set n} → {kg kp d dp : ℕ} → {vg vp : A} → {cg : Color} → (tree grand parent repl : bt (Color ∧ A) )
-           → RBtreeInvariant grand
-           → RBtreeInvariant repl
-           → {uncle left right : bt (Color ∧ A) }
-           → grand  ≡ node kg ⟪ cg , vg ⟫ uncle parent
-           → parent ≡ node kp ⟪ Red , vp ⟫ left  right
-           → color uncle ≡ Red
-           →     (color left  ≡ Red → RBtreeInvariant (node kg ⟪ Red , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ repl right )) )
-              ∧  (color right ≡ Red → RBtreeInvariant (node kg ⟪ Red , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ left repl  )) )
-rbi-case31 {n} {A} {key} = {!!}
-
---
--- case4 increase the black depth
---
-rbi-case41 : {n : Level} {A : Set n} → {kg kp d dp : ℕ} → {vg vp : A} → {cg : Color} → (tree grand parent repl : bt (Color ∧ A) )
-           → RBtreeInvariant grand
-           → RBtreeInvariant repl
-           → {uncle left right : bt (Color ∧ A) }
-           → grand  ≡ node kg ⟪ cg , vg ⟫ uncle parent
-           → parent ≡ node kp ⟪ Red , vp ⟫ left  right
-           → color uncle ≡ Black
-           →     (color left  ≡ Red → RBtreeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ repl right ))  )
-              ∧  (color right ≡ Red → RBtreeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ left repl  ))  )
-rbi-case41 {n} {A} {key} = {!!}
-
-rbi-case51 : {n : Level} {A : Set n} → {kg kp d dp : ℕ} → {vg vp : A} → {cg : Color} → (tree grand parent repl : bt (Color ∧ A) )
-           → RBtreeInvariant grand
-           → RBtreeInvariant repl
-           → {uncle left right : bt (Color ∧ A) }
-           → grand  ≡ node kg ⟪ cg , vg ⟫ uncle parent
-           → parent ≡ node kp ⟪ Red , vp ⟫ left  right
-           → color uncle ≡ Black
-           →     (color left  ≡ Red → RBtreeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ repl right ))  )
-              ∧  (color right ≡ Red → RBtreeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ left repl  ))  )
-rbi-case51 {n} {A} {key} = {!!}
-
---... | Black = record {
---             d = ? ; od = RBI.od rbi ; rd = ?
---          ;  tree = ? ; rot = ? ; repl = ?
---          ;  treerb = ? ; replrb = ?
---          ;  d=rd = ? ; si = ? ; rotated = ? ; ri = ?
---          ;  origti = RBI.origti rbi ; origrb = RBI.origrb rbi
---       }
---... | Red = ?
-
 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
@@ -959,7 +898,7 @@
            --    / \     / \           / \    rotate L   / \
            --   L   L1  L   R3        L   R  -- bad     B   B
            --              / \           / \               / \      1 : child-replace
-           ---            L   L2        L   B             L   L     2:  child-replace ( unbrance )
+           ---            L   L2        L   B             L   L     2:  child-replace ( unbalanced )
            --                              / \                      3:  child-replace ( rotated / balanced )
            --                             L   L  
            --