Mercurial > hg > Gears > GearsAgda

changeset 847:045dd0e43c56

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, 27 Mar 2024 23:30:49 +0900
parents 0355a1c14c13
children ad97032da3c8
files hoareBinaryTree1.agda
diffstat 1 files changed, 4 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Wed Mar 27 21:26:10 2024 +0900
+++ b/hoareBinaryTree1.agda	Wed Mar 27 23:30:49 2024 +0900
@@ -1042,12 +1042,14 @@
      (t-node key₁ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-black-left x x₇ trb) = t-node _ _ _ (proj1 rr00) x₂ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) x₅ x₆ (RB-repl→ti _ _ _ _ ti trb) ti₁ where
         rr00 : (key₄ < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁
         rr00 = RB-repl→ti< _ _ _ _ _ trb x₇ ⟪ x₁ , ⟪ x₃ , x₄ ⟫ ⟫
-RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ t₁) leaf) (node key₂ ⟪ Red , _ ⟫ (node key₁ ⟪ Black , _ ⟫ t t₁) .(to-black leaf)) key value 
-      (t-left _ .key₂ x₁ x₂ x₃ ti) (rbr-flip-ll x trb) = t-left _ _ x₁ rr00 x₃ (RB-repl→ti _ _ _ _ (RB-repl→ti _ _ _ _ ti (rbr-left ? trb)) rbr-to-black ) where
+RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ t₁) leaf) (node key₂ ⟪ Red , value₁ ⟫ (node key₁ ⟪ Black , _ ⟫ t t₁) .(to-black leaf)) key value 
+      (t-left _ .key₂ x₁ x₂ x₃ ti) (rbr-flip-ll x trb) = t-left _ _ x₁ rr00 x₃ ? where
         rr00 : tr< key₂ t 
         rr00 = RB-repl→ti< _ _ _ _ _ trb ? x₂
         rr01 : replacedRBTree ? ? (node key₁ ⟪ Red , ? ⟫ ? t₁) (node key₁ ⟪ Black , ? ⟫ t t₁)
         rr01 = ?
+        rr02 : treeInvariant (node key₁ ⟪ Red , ?  ⟫ t t₁)
+        rr02 = RB-repl→ti _ _ _ _ ti (rbr-left ? trb)
 RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ t₁) (node key₃ _ _ _)) (node key₂ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ t t₁) .(to-black (node key₃ _ _ _))) key value (t-node _ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-ll x trb) = ?
 RB-repl→ti .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key value ti (rbr-flip-lr x trb) = ?
 RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key value ti (rbr-flip-rl x trb) = ?