Mercurial > hg > Gears > GearsAgda

changeset 753:7127770c2176

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, 28 Apr 2023 14:13:39 +0900
parents 44837beece64
children cda422725f79
files hoareBinaryTree1.agda
diffstat 1 files changed, 12 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Wed Apr 26 13:12:31 2023 +0900
+++ b/hoareBinaryTree1.agda	Fri Apr 28 14:13:39 2023 +0900
@@ -710,8 +710,18 @@
         ... | 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 = ?
+        insertCase3 (node kp value₁ tpl tpr) (node kg value (node ku ⟪ Black , vu ⟫ tgl tgr) tr₁) tp=p tg=g with <-cmp ku kp
+        ... | tri< a ¬b ¬c = ? where
+            insertCase4 : ( right-tp left-tg : bt (Color ∧ A) ) → right-tp ≡ tpr → left-tg ≡ tgl → t
+            insertCase4 leaf lg eq1 eq2 = ?
+            insertCase4 (node krp value rp rp₁) leaf eq1 eq2 = ?
+            insertCase4 (node krp value rp rp₁) (node klg value₁ lg lg₁) eq1 eq2 with <-cmp key krp | <-cmp kp klg
+            ... | ttt4 | ttt5 = ? where
+                insertCase41 : ( left-tp right-tg : bt (Color ∧ A) ) → left-tp ≡ tpl → right-tg ≡ tgr → t
+                insertCase41 leaf rg eq3 eq4 = ?
+                insertCase41 (node klp value lp lp₁) leaf eq3 eq4 = ?
+                insertCase41 (node klp value lp lp₁) (node krg value₁ rg rg₁) eq3 eq4 with <-cmp key klp | <-cmp kp krg
+                ... | ttt4 | ttt5 = ? where
         ... | tri≈ ¬a b ¬c = ? -- can't happen
         ... | tri> ¬a ¬b c = ?
     insertCase1 : t