Mercurial > hg > Gears > GearsAgda

changeset 857:022481623aea

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, 01 Apr 2024 08:59:45 +0900
parents 9964cec86483
children 60f27ddfd0f4
files hoareBinaryTree1.agda
diffstat 1 files changed, 7 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Sun Mar 31 16:35:19 2024 +0900
+++ b/hoareBinaryTree1.agda	Mon Apr 01 08:59:45 2024 +0900
@@ -1090,11 +1090,13 @@
 RB-repl→ti {_} {A} (node k1 ⟪ Black , c1 ⟫ (node k2 ⟪ Red , c2 ⟫ .leaf .leaf) leaf) (node _ ⟪ Black , _ ⟫ (node key₁ value₁ t₂ t₃) (node _ ⟪ Red , _ ⟫ .leaf leaf)) key value (t-left _ _ x₁ x₂ x₃ (t-single .k2 .(⟪ Red , c2 ⟫))) (rbr-rotate-ll x trb) = t-node ? _ _ ? ? ? ? ? tt (RB-repl→ti _ _ _ _ ? trb) ?
 RB-repl→ti {_} {A} (node k1 ⟪ Black , c1 ⟫ (node k2 ⟪ Red , c2 ⟫ .leaf .(node key₂ _ _ _)) leaf) (node _ ⟪ Black , _ ⟫ (node key₁ value₁ t₂ t₃) (node _ ⟪ Red , _ ⟫ .(node key₂ _ _ _) leaf)) key value (t-left _ _ x₁ x₂ x₃ (t-right .k2 key₂ x₄ x₅ x₆ ti)) (rbr-rotate-ll x trb) = t-node ? _ _ ? ? ? ? ? tt ? ?
 RB-repl→ti {_} {A} (node k1 ⟪ Black , c1 ⟫ (node k2 ⟪ Red , c2 ⟫ .(node key₂ _ _ _) .leaf) leaf) (node _ ⟪ Black , _ ⟫ (node key₁ value₁ t₂ t₃) (node _ ⟪ Red , _ ⟫ .leaf leaf)) key value (t-left _ _ x₁ x₂ x₃ (t-left key₂ .k2 x₄ x₅ x₆ ti)) (rbr-rotate-ll x trb) = t-node ? _ _ ? ? ? ? ? tt (RB-repl→ti _ _ _ _ ? trb) ?
-RB-repl→ti {_} {A} (node k1 ⟪ Black , c1 ⟫ (node k2 ⟪ Red , c2 ⟫ .(node key₂ _ _ _) .(node key₃ _ _ _)) leaf) (node _ ⟪ Black , _ ⟫ (node key₁ value₁ t₂ t₃) (node _ ⟪ Red , _ ⟫ .(node key₃ _ _ _) leaf)) key value (t-left _ _ x₁ x₂ x₃ (t-node key₂ .k2 key₃ x₄ x₅ x₆ x₇ x₈ x₉ ti ti₁)) (rbr-rotate-ll x trb) = t-node ? _ _ ? ? ? ? ? tt ? ? where
-        rr03 : (tr : bt (Color ∧ A)) → tr ≡ ?   → (tir : treeInvariant (node k2 ⟪ Red , c2 ⟫ ? tr))  → treeInvariant (node k1 ⟪ Red , c1 ⟫ tr leaf) 
-        rr03 leaf eq tri = RTtoTI0 _ _ _ _ (treeRightDown _ _ tri) r-leaf
-        rr03 (node key₃ value₃ tr tr₁) refl tri = RTtoTI0 _ _ _ _ (t-left _ _ (proj1 x₃) (proj1 (proj2 x₃)) (proj2 (proj2 x₃)) (treeRightDown _ _ tri) ) 
-            (r-left (proj1 x₃) r-node) 
+RB-repl→ti {_} {A} (node k1 ⟪ Black , c1 ⟫ (node k2 ⟪ Red , c2 ⟫ (node key₂ value₃ left right) (node key₃ value₂ t₄ t₅)) leaf) (node _ ⟪ Black , _ ⟫ (node key₁ value₁ t₂ t₃) (node _ ⟪ Red , _ ⟫ .(node key₃ _ _ _) leaf)) key value (t-left _ _ x₁ x₂ x₃ (t-node key₂ .k2 key₃ x₄ x₅ x₆ x₇ x₈ x₉ ti ti₁)) (rbr-rotate-ll x trb) = t-node _ _ _ ? x₁ ? ? ⟪ x₅ , ⟪ x₈ ,  x₉ ⟫ ⟫ tt rr05 rr04 where
+        rr03 : (key₁ < k1) ∧ tr< k1 t₂ ∧ tr< k1 t₃
+        rr03 = RB-repl→ti< _ _ _ _ _ trb ? x₂
+        rr04 : treeInvariant (node k1 ⟪ Red , c1 ⟫ (node key₃ value₂ t₄ t₅) leaf)
+        rr04 = RTtoTI0 _ _ _ _ (t-left _ _ (proj1 x₃) (proj1 (proj2 x₃)) (proj2 (proj2 x₃)) ti₁ ) (r-left (proj1 x₃) r-node) 
+        rr05 : treeInvariant (node key₁ value₁ t₂ t₃)
+        rr05 = RB-repl→ti _ _ _ _ ti trb
 RB-repl→ti .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node key₂ _ _ _)) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ (node key₂ _ _ _))) key value (t-node _ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-rotate-ll x trb) = ?
 RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) key value ti (rbr-rotate-rr x trb) = ?
 RB-repl→ti .(node kg ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ _) _) .(node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₂) (node kg ⟪ Red , _ ⟫ t₃ _)) key value ti (rbr-rotate-lr t₂ t₃ kg kp kn trb) = ?