Mercurial > hg > Gears > GearsAgda

changeset 841:27664016173a

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, 20 Mar 2024 09:08:39 +0900
parents 39e95f17ff18
children ee2dd920e414
files hoareBinaryTree1.agda
diffstat 1 files changed, 7 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Tue Mar 19 10:03:04 2024 +0900
+++ b/hoareBinaryTree1.agda	Wed Mar 20 09:08:39 2024 +0900
@@ -1002,12 +1002,13 @@
         rr01 : treeInvariant (node key₃ value₁ t t₃)
         rr01 = RB-repl→ti _ _ _ _ t-leaf trb
 RB-repl→ti .(node _ ⟪ _ , _ ⟫ (node key₁ _ _ _) leaf) (node key₃ ⟪ _ , _ ⟫ (node key₂ value₁ t t₁) leaf) key value 
-    (t-left key₁ _ x₁ x₂ x₃ ti) (rbr-left x trb) = t-left key₂ _ ? ? ? (RB-repl→ti _ _ _ _ ti trb) where
-        rr00 : (key₁ < key₂) ∧ tr< key₁ t ∧ tr< key₁ t₁
-        rr00 = ?
-        rr01 : (key₂ < key₃) ∧ tr< key₃ t ∧ tr< key₃ t₁
-        rr01 = RB-repl→ti< _ _ _ _ _ trb x ?
-RB-repl→ti .(node _ ⟪ _ , _ ⟫ (node key₁ _ _ _) (node key₂ _ _ _)) .(node _ ⟪ _ , _ ⟫ _ (node key₂ _ _ _)) key value (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-left x trb) = ?
+    (t-left key₁ _ x₁ x₂ x₃ ti) (rbr-left x trb) = t-left key₂ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ ti trb) where
+        rr00 : (key₂ < key₃) ∧ tr< key₃ t ∧ tr< key₃ t₁
+        rr00 = RB-repl→ti< _ _ _ _ _ trb x ⟪ x₁ , ⟪ x₂ , x₃ ⟫ ⟫
+RB-repl→ti .(node key₃ ⟪ _ , _ ⟫ (node key₁ _ _ _) (node key₂ _ t₁ t₂)) (node key₃ ⟪ _ , _ ⟫ (node key₄ value₁ t t₃) (node key₂ _ t₁ t₂)) key value 
+    (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-left x trb) = t-node _ _ _ ? ? ? ? ? ? (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 _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key value ti (rbr-black-right x trb) = ?
 RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key value ti (rbr-black-left x trb) = ?
 RB-repl→ti .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key value ti (rbr-flip-ll x trb) = ?