Mercurial > hg > Gears > GearsAgda

changeset 812:b8fb1e0755d0

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, 22 Jan 2024 11:15:38 +0900
parents f655afa1b8ea
children 8dbddf72211e
files hoareBinaryTree1.agda
diffstat 1 files changed, 3 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Jan 22 10:45:34 2024 +0900
+++ b/hoareBinaryTree1.agda	Mon Jan 22 11:15:38 2024 +0900
@@ -736,7 +736,8 @@
        replrb : RBtreeInvariant repl
        si : stackInvariant key tree orig stack
        rotated : rotatedTree tree rot
-       ri : replacedTree key ⟪ Red , value ⟫ (child-replaced key rot ) repl
+       ri : replacedTree key ⟪ Red   , value ⟫ (child-replaced key rot ) repl
+         ∨  replacedTree key ⟪ Black , value ⟫ (child-replaced key rot ) repl
        repl-red : color repl ≡ Red
        repl-eq : black-depth (child-replaced key rot ) ≡ black-depth repl
 
@@ -944,7 +945,7 @@
              ; si = s-nil
              ; rotated = subst (λ k → rotatedTree k (node key₁ value₁ left (RBI.rot r))) (
                 trans (cong (λ k → node key₁ value₁ left k) (sym (rb04 si eq refl))) refl) (rtt-node rtt-unit (RBI.rotated r))
-             ; ri = proj2 rb05
+             ; ri = ? -- proj2 rb05
              ; repl-red = refl
              ; repl-eq = rb07
              } where