# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1711977484 -32400
# Node ID cbae47526086ad18c0f4d052d3a0b90e31eaac9a
# Parent  6a081059aa7c93d88ce5ebbe5e8adda821a9a625
...

diff -r 6a081059aa7c -r cbae47526086 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Mon Apr 01 22:08:32 2024 +0900
+++ b/hoareBinaryTree1.agda	Mon Apr 01 22:18:04 2024 +0900
@@ -1113,14 +1113,34 @@
         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 key₁ ⟪ Black , c1 ⟫ (node key₂ ⟪ Red , c2 ⟫ t t₁) (node key₃ v3 t₂ t₃)) (node _ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) (node _ ⟪ Red , _ ⟫ .t₁ (node key₃ _ _ _))) key value 
-    (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-rotate-ll x lt trb) = t-node _ _ _ ? x₁ ? ? ? ? rr02 rr03 where
+RB-repl→ti (node key₁ ⟪ Black , c1 ⟫ (node key₂ ⟪ Red , c2 ⟫ .leaf .leaf) (node key₃ v3 t₂ t₃)) (node _ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) (node _ ⟪ Red , _ ⟫ .leaf (node key₃ _ _ _))) key value (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ (t-single .key₂ .(⟪ Red , c2 ⟫)) ti₁) (rbr-rotate-ll x lt trb) = t-node _ _ _ ? x₁ ? ? ? ? rr02 rr03 where
+        rr00 : (key₄ < key₂) ∧ tr< key₂ t₄ ∧ tr< key₂ t₅
+        rr00 = RB-repl→ti< _ _ _ _ _ trb lt ?
+        rr02 : treeInvariant (node key₄ value₁ t₄ t₅)
+        rr02 = RB-repl→ti _ _ _ _ ti₁ ?
+        rr03 : treeInvariant (node key₁ ⟪ Red , c1 ⟫ ? (node key₃ v3 t₂ t₃))
+        rr03 = RTtoTI0 _ _ _ _ ? r-node
+RB-repl→ti (node key₁ ⟪ Black , c1 ⟫ (node key₂ ⟪ Red , c2 ⟫ .leaf .(node key₅ _ _ _)) (node key₃ v3 t₂ t₃)) (node _ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) (node _ ⟪ Red , _ ⟫ .(node key₅ _ _ _) (node key₃ _ _ _))) key value (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ (t-right .key₂ key₅ x₇ x₈ x₉ ti) ti₁) (rbr-rotate-ll x lt trb) = t-node _ _ _ ? x₁ ? ? ? ? rr02 rr03 where
         rr00 : (key₄ < key₂) ∧ tr< key₂ t₄ ∧ tr< key₂ t₅
         rr00 = RB-repl→ti< _ _ _ _ _ trb lt ?
         rr02 : treeInvariant (node key₄ value₁ t₄ t₅)
         rr02 = RB-repl→ti _ _ _ _ ti₁ ?
-        rr03 : treeInvariant (node key₁ ⟪ Red , c1 ⟫ t₁ (node key₃ v3 t₂ t₃))
-        rr03 = ?
+        rr03 : treeInvariant (node key₁ ⟪ Red , c1 ⟫ ? (node key₃ v3 t₂ t₃))
+        rr03 = RTtoTI0 _ _ _ _ ? r-node
+RB-repl→ti (node key₁ ⟪ Black , c1 ⟫ (node key₂ ⟪ Red , c2 ⟫ .(node key₅ _ _ _) .leaf) (node key₃ v3 t₂ t₃)) (node _ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) (node _ ⟪ Red , _ ⟫ .leaf (node key₃ _ _ _))) key value (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ (t-left key₅ .key₂ x₇ x₈ x₉ ti) ti₁) (rbr-rotate-ll x lt trb) = t-node _ _ _ ? x₁ ? ? ? ? rr02 rr03 where
+        rr00 : (key₄ < key₂) ∧ tr< key₂ t₄ ∧ tr< key₂ t₅
+        rr00 = RB-repl→ti< _ _ _ _ _ trb lt ?
+        rr02 : treeInvariant (node key₄ value₁ t₄ t₅)
+        rr02 = RB-repl→ti _ _ _ _ ti₁ ?
+        rr03 : treeInvariant (node key₁ ⟪ Red , c1 ⟫ ? (node key₃ v3 t₂ t₃))
+        rr03 = RTtoTI0 _ _ _ _ ? r-node
+RB-repl→ti (node key₁ ⟪ Black , c1 ⟫ (node key₂ ⟪ Red , c2 ⟫ .(node key₅ _ _ _) .(node key₆ _ _ _)) (node key₃ v3 t₂ t₃)) (node _ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) (node _ ⟪ Red , _ ⟫ .(node key₆ _ _ _) (node key₃ _ _ _))) key value (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ (t-node key₅ .key₂ key₆ x₇ x₈ x₉ x₁₀ x₁₁ x₁₂ ti ti₂) ti₁) (rbr-rotate-ll x lt trb) = t-node _ _ _ ? x₁ ? ? ? ? rr02 rr03 where
+        rr00 : (key₄ < key₂) ∧ tr< key₂ t₄ ∧ tr< key₂ t₅
+        rr00 = RB-repl→ti< _ _ _ _ _ trb lt ?
+        rr02 : treeInvariant (node key₄ value₁ t₄ t₅)
+        rr02 = RB-repl→ti _ _ _ _ ti₁ ?
+        rr03 : treeInvariant (node key₁ ⟪ Red , c1 ⟫ ? (node key₃ v3 t₂ t₃))
+        rr03 = RTtoTI0 _ _ _ _ ? r-node
         rr04 : (key₂ < key₃) ∧ tr> key₂ t₂ ∧ tr> key₂ t₃
         rr04 = ?
 RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) key value ti (rbr-rotate-rr x lt trb) = ?