# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1706182645 -32400
# Node ID 317539bdba034528418ab297d71dd1ccaddf4cc9
# Parent  66726208b9f4d30b312ca70272b25289bda7b9e8
...

diff -r 66726208b9f4 -r 317539bdba03 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Thu Jan 25 17:03:59 2024 +0900
+++ b/hoareBinaryTree1.agda	Thu Jan 25 20:37:25 2024 +0900
@@ -932,8 +932,19 @@
     --     node-key parent < node-key repl < node-key grand  → rotateLeft  parent    then insertCase6
     --     node-key grand  < node-key repl < node-key parent → rotateRight parent    then insertCase6
     --     else insertCase6
-    insertCase51 : t
-    insertCase51 = ?
+    insertCase51 : (tree1 grand : bt (Color ∧ A)) → tree1 ≡ tree → grand ≡ PG.grand pg → t
+    insertCase51 leaf grand teq geq = ?    -- can't happen
+    insertCase51 (node key value tree1 tree2) leaf teq geq = ?    -- can't happen
+    insertCase51 (node key value tree1 tree2) (node key₁ value₁ grand grand₁) teq geq with <-cmp key key₁
+    ... | tri< a ¬b ¬c = ? where
+          insertCase511 : (parent : bt (Color ∧ A)) → parent ≡ PG.parent pg → t
+          insertCase511 leaf peq = ? -- can't happen
+          insertCase511 (node key₂ ⟪ co , value ⟫ n1 n2) peq with <-cmp key key₂
+          ... | tri< a ¬b ¬c = insertCase6 key value orig ? stack ? pg ? ?
+          ... | tri≈ ¬a b ¬c = ? -- can't happen
+          ... | tri> ¬a ¬b c = ? --- rotareRight → insertCase6 key value orig ? stack ? pg next exit
+    ... | tri≈ ¬a b ¬c = ? -- can't happen
+    ... | tri> ¬a ¬b c = ?