Mercurial > hg > Members > Moririn

changeset 750:61e16b7489b8

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 Wed, 26 Apr 2023 09:10:12 +0900
parents 923f72af015c
children 4ecad6cfef4b
files hoareBinaryTree1.agda
diffstat 1 files changed, 13 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Tue Apr 25 19:13:13 2023 +0900
+++ b/hoareBinaryTree1.agda	Wed Apr 26 09:10:12 2023 +0900
@@ -667,19 +667,22 @@
 
 replaceRBP : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) → {d0 : ℕ} 
-     → (orig tree : bt (Color ∧ A)) {d0 : ℕ}
+     → (orig tree repl : bt (Color ∧ A)) {d0 : ℕ}
      →  RBtreeInvariant orig d0 
-     →  {d : ℕ} → RBtreeInvariant tree d → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
+     →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant repl dr 
+     → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
+     → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key tree) repl
      → (next : {key2 d2 : ℕ} {c2 : Color}  
-        → (to tr : bt (Color ∧ A)) 
+        → (to tr rr : bt (Color ∧ A)) 
         →  RBtreeInvariant orig d0 
-        →  {d : ℕ} → RBtreeInvariant tree d 
+        →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant rr dr 
         → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1 
+        → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key tr) rr
         → length stack1 < length stack  → t )
      → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
         →  {d : ℕ} → RBtreeInvariant repl d 
         → (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
-replaceRBP {n} {m} {A} {t} key value orig tree rbio rbit stack si next exit = insertCase1 where
+replaceRBP {n} {m} {A} {t} key value orig tree repl rbio rbit rbir stack si ri next exit = ? where
     insertCase2 : (tree parent grand : bt (Color ∧ A)) 
       → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
       → (pg : ParentGrand tree parent grand ) → t
@@ -689,14 +692,14 @@
         --
         --  in some case, stack is poped and loop to replaceRBP
         --     it means, we have to create replacedTree
-        insertCase3 : ( tr : bt (Color ∧ A) ) → tr ≡ grand → t
-        insertCase3 leaf eq = ?
-        insertCase3 (node kg value leaf tr₁) eq = ?
-        insertCase3 (node kg value (node ku ⟪ Red , vu ⟫ tr tr₂) tr₁) eq with <-cmp kg ku
+        insertCase3 : ( tp tg : bt (Color ∧ A) ) → tp ≡ parent → tg ≡ grand → t
+        insertCase3 tp leaf eq = ?
+        insertCase3 tp (node kg value leaf tr₁) eq = ?
+        insertCase3 tp (node kg value (node ku ⟪ Red , vu ⟫ tr tr₂) tr₁) eq with <-cmp kg ku
         ... | tri< a ¬b ¬c = ?
         ... | tri≈ ¬a b ¬c = ?
         ... | tri> ¬a ¬b c = ?
-        insertCase3 (node kg value (node ku ⟪ Black , vu ⟫ tr tr₂) tr₁) eq with <-cmp kg ku
+        insertCase3 tp (node kg value (node ku ⟪ Black , vu ⟫ tr tr₂) tr₁) eq with <-cmp kg ku
         ... | tri< a ¬b ¬c = ?
         ... | tri≈ ¬a b ¬c = ?
         ... | tri> ¬a ¬b c = ?