Mercurial > hg > Gears > GearsAgda

changeset 769:ce0d41a84c2b

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 Sun, 07 May 2023 20:19:18 +0900
parents 1bb96bc9eb45
children a4bc901bba36
files hoareBinaryTree1.agda
diffstat 1 files changed, 12 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Sun May 07 13:57:47 2023 +0900
+++ b/hoareBinaryTree1.agda	Sun May 07 20:19:18 2023 +0900
@@ -611,6 +611,18 @@
        rest : List (bt A)
        stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest )
 
+record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A))) (C : bt (Color ∧ A) → bt (Color ∧ A) → List (bt (Color ∧ A)) → Set n) : Set n where
+   field
+     d rd : ℕ
+     tree0 rot : bt (Color ∧ A)
+     tree0rb : RBtreeInvariant tree0 d
+     replrb : RBtreeInvariant repl rd
+     d=rd : ( d ≡ rd ) ∨ ( suc d ≡ rd )
+     rotated : rotatedTree tree rot
+     si : stackInvariant key tree tree0 stack
+     ri : replacedRBTree key value (child-replaced key rot ) repl
+     ci : C tree repl stack     -- data continuation
+   
 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