Mercurial > hg > Gears > GearsAgda

changeset 822:3f6e13350420

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 Fri, 26 Jan 2024 08:54:44 +0900
parents aeb14a056896
children ebee6945c697
files hoareBinaryTree1.agda
diffstat 1 files changed, 7 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Fri Jan 26 04:55:57 2024 +0900
+++ b/hoareBinaryTree1.agda	Fri Jan 26 08:54:44 2024 +0900
@@ -758,19 +758,19 @@
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle            (node kp ⟪ Red   , vp ⟫ t t₁))  
                                     (node kg ⟪ Red ,   vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t t₂))
 
-    rbr-rotate-ll : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}   - case6
+    rbr-rotate-ll : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}   -- case6
          → color t₂ ≡ Red → replacedRBTree key value t₁ t₂
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₁ t)    uncle) 
                                     (node kp ⟪ Black , vp ⟫ t₂                            (node kg ⟪ Red , vg ⟫ t uncle))
-    rbr-rotate-rr : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}   - case6
+    rbr-rotate-rr : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}   -- case6
          → color t₂ ≡ Red → replacedRBTree key value t₁ t₂
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle                          (node kp ⟪ Red   , vp ⟫ t t₁)) 
                                     (node kp ⟪ Black , vp ⟫ (node kg ⟪ Red , vg ⟫ uncle t) t₂ )
-    rbr-rotate-lr : {t t₁ t₂ t₃ uncle : bt (Color ∧ A)} {kg kp kn : ℕ} {vg vp vn : A}   - case56
+    rbr-rotate-lr : {t t₁ t₂ t₃ uncle : bt (Color ∧ A)} {kg kp kn : ℕ} {vg vp vn : A}   -- case56
          → replacedRBTree key value t (node kn ⟪ Red , vn ⟫ t₁ t₂)
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₃ t)  uncle) 
                                     (node kn ⟪ Black , vn ⟫ (node kp ⟪ Red , vp ⟫ t₃ t₁) (node kg ⟪ Red , vg ⟫ t₂ uncle))
-    rbr-rotate-rl : {t t₁ t₂ t₃ uncle : bt (Color ∧ A)} {kg kp kn : ℕ} {vg vp vn : A    - case56
+    rbr-rotate-rl : {t t₁ t₂ t₃ uncle : bt (Color ∧ A)} {kg kp kn : ℕ} {vg vp vn : A}   -- case56
          → replacedRBTree key value t (node kn ⟪ Red , vn ⟫ t₁ t₂)
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle                           (node kp ⟪ Red , vp ⟫ t  t₃)) 
                                     (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , vg ⟫ t₁ uncle) (node kp ⟪ Red , vp ⟫ t₂ t₃)) 
@@ -867,6 +867,9 @@
 ... | tri≈ ¬a b ¬c = rbi
 ... | tri> ¬a ¬b c = RBtreeRightDown _ _ rbi
 
+RBTtoRBI  : {n : Level} {A : Set n}  → (tree repl : bt (Color ∧ A)) → (key : ℕ) → (value : A) → RBtreeInvariant tree
+     → replacedRBTree key value tree repl → RBtreeInvariant repl
+RBTtoRBI  = ?
 --
 -- create RBT invariant after findRBT, continue to replaceRBT
 --