Mercurial > hg > Gears > GearsAgda

changeset 914:e87dca1b4c21

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 Mon, 03 Jun 2024 15:42:43 +0900
parents f2b78b3a5fb2
children 045c98a3b8d1
files hoareBinaryTree1.agda
diffstat 1 files changed, 14 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Jun 03 15:07:48 2024 +0900
+++ b/hoareBinaryTree1.agda	Mon Jun 03 15:42:43 2024 +0900
@@ -1726,11 +1726,22 @@
  → (key : ℕ) (value : A)
  → (tree0 : bt (Color ∧ A))
  → RBtreeInvariant tree0
+ → treeInvariant tree0
  → (tree1 : bt (Color ∧ A))
  → (stack : List (bt (Color ∧ A)))
- → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
- → (exit : (r : RBI key value tree0 tree1 stack ) → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )) → t
-replaceRBTNode key value tree0 rbi tree1 stack rbi-stack exit = {!!}
+ → stackInvariant key tree1 tree0 stack
+ → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) 
+ → (exit : (r : RBI key value tree0 tree1 stack ) → t ) → t
+replaceRBTNode key value orig rbi ti tree stack si P exit = exit record {
+     tree = tree
+   ; ¬leaf = ?
+   ; origti = ti
+   ; origrb = rbi
+   ; treerb = ?
+   ; replrb = ?
+   ; si = si
+   ; state = rotate ? ? ?  
+  }
 
 --
 --   rotate and rebuild replaceTree and rb-invariant