Mercurial > hg > Members > Moririn

changeset 752:44837beece64

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, 26 Apr 2023 13:12:31 +0900
parents 4ecad6cfef4b
children 7127770c2176
files hoareBinaryTree1.agda
diffstat 1 files changed, 13 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Wed Apr 26 09:20:38 2023 +0900
+++ b/hoareBinaryTree1.agda	Wed Apr 26 13:12:31 2023 +0900
@@ -698,16 +698,21 @@
         --
         --  in some case, stack is poped and loop to replaceRBP
         --     it means, we have to create replacedTree
+        --     g     
+        --   u   p    
+        --     _   s   
         insertCase3 : ( tp tg : bt (Color ∧ A) ) → tp ≡ parent → tg ≡ grand → t
-        insertCase3 tp leaf eq = ?
-        insertCase3 tp (node kg value leaf tr₁) eq = ?
-        insertCase3 tp (node kg value (node ku ⟪ Red , vu ⟫ tr tr₂) tr₁) eq with <-cmp kg ku
+        insertCase3 tp leaf tp=p tg=g = ?
+        insertCase3 tp (node kg value leaf tr₁) tp=p tg=g = ?
+        insertCase3 leaf (node kg value (node ku ⟪ Red , vu ⟫ tr tr₂) tr₁) tp=p tg=g = ? -- can't happen
+        insertCase3 (node kp value₁ tp tp₁) (node kg value (node ku ⟪ Red , vu ⟫ tr tr₂) tr₁) tp=p tg=g with <-cmp ku kp
+        ... | tri< a ¬b ¬c = next ? ? ? ? ? ? ? ? ? ?
+        ... | tri≈ ¬a b ¬c = ? -- can't happen
+        ... | tri> ¬a ¬b c = next ? ? ? ? ? ? ? ? ? ?
+        insertCase3 leaf (node kg value (node ku ⟪ Black , vu ⟫ tr tr₂) tr₁) tp=p tg=g = ? -- can't happen
+        insertCase3 (node kp value₁ tp tp₁) (node kg value (node ku ⟪ Black , vu ⟫ tr tr₂) tr₁) tp=p tg=g with <-cmp ku kp
         ... | tri< a ¬b ¬c = ?
-        ... | tri≈ ¬a b ¬c = ?
-        ... | tri> ¬a ¬b c = ?
-        insertCase3 tp (node kg value (node ku ⟪ Black , vu ⟫ tr tr₂) tr₁) eq with <-cmp kg ku
-        ... | tri< a ¬b ¬c = ?
-        ... | tri≈ ¬a b ¬c = ?
+        ... | tri≈ ¬a b ¬c = ? -- can't happen
         ... | tri> ¬a ¬b c = ?
     insertCase1 : t
     insertCase1 with stackToPG tree orig stack si