Mercurial > hg > Members > Moririn

changeset 774:ebd8a73543dd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 09 May 2023 23:17:54 +0900
parents d6d442196c87
children fb74ba4fa38e
files hoareBinaryTree1.agda
diffstat 1 files changed, 27 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Tue May 09 19:48:59 2023 +0900
+++ b/hoareBinaryTree1.agda	Tue May 09 23:17:54 2023 +0900
@@ -644,7 +644,7 @@
              ∧  (color left  ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) (suc d))
 rbi-case1 {n} {A} {key} = ?
 
-rbi-case3 : {n : Level} {A : Set n} → {kg kp d dp : ℕ} → {vg vp : A} → {cg : Color} → (tree grand parent repl : bt (Color ∧ A) ) 
+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 dp
            → RBtreeInvariant repl d 
            → {uncle left right : bt (Color ∧ A) } 
@@ -653,7 +653,32 @@
            → color uncle ≡ Red
            →     (color left  ≡ Red → RBtreeInvariant (node kg ⟪ Red , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ repl right )) dp) 
               ∧  (color right ≡ Red → RBtreeInvariant (node kg ⟪ Red , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ left repl  )) dp)
-rbi-case3 {n} {A} {key} = ?
+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 dp
+           → RBtreeInvariant repl d 
+           → {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 )) (suc dp) )
+              ∧  (color right ≡ Red → RBtreeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ left repl  )) (suc dp) )
+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 dp
+           → RBtreeInvariant repl d 
+           → {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 )) (suc dp) )
+              ∧  (color right ≡ Red → RBtreeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ left repl  )) (suc dp) )
+rbi-case51 {n} {A} {key} = ?
 
 --... | Black = record {
 --             d = ? ; od = RBI.od rbi ; rd = ?