# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1710893319 -32400
# Node ID 27664016173afd1033e91cc249d2341c323157ed
# Parent  39e95f17ff188229630a9c0c2215af476ea8160b
...

diff -r 39e95f17ff18 -r 27664016173a hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Tue Mar 19 10:03:04 2024 +0900
+++ b/hoareBinaryTree1.agda	Wed Mar 20 09:08:39 2024 +0900
@@ -1002,12 +1002,13 @@
         rr01 : treeInvariant (node key₃ value₁ t t₃)
         rr01 = RB-repl→ti _ _ _ _ t-leaf trb
 RB-repl→ti .(node _ ⟪ _ , _ ⟫ (node key₁ _ _ _) leaf) (node key₃ ⟪ _ , _ ⟫ (node key₂ value₁ t t₁) leaf) key value 
-    (t-left key₁ _ x₁ x₂ x₃ ti) (rbr-left x trb) = t-left key₂ _ ? ? ? (RB-repl→ti _ _ _ _ ti trb) where
-        rr00 : (key₁ < key₂) ∧ tr< key₁ t ∧ tr< key₁ t₁
-        rr00 = ?
-        rr01 : (key₂ < key₃) ∧ tr< key₃ t ∧ tr< key₃ t₁
-        rr01 = RB-repl→ti< _ _ _ _ _ trb x ?
-RB-repl→ti .(node _ ⟪ _ , _ ⟫ (node key₁ _ _ _) (node key₂ _ _ _)) .(node _ ⟪ _ , _ ⟫ _ (node key₂ _ _ _)) key value (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-left x trb) = ?
+    (t-left key₁ _ x₁ x₂ x₃ ti) (rbr-left x trb) = t-left key₂ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ ti trb) where
+        rr00 : (key₂ < key₃) ∧ tr< key₃ t ∧ tr< key₃ t₁
+        rr00 = RB-repl→ti< _ _ _ _ _ trb x ⟪ x₁ , ⟪ x₂ , x₃ ⟫ ⟫
+RB-repl→ti .(node key₃ ⟪ _ , _ ⟫ (node key₁ _ _ _) (node key₂ _ t₁ t₂)) (node key₃ ⟪ _ , _ ⟫ (node key₄ value₁ t t₃) (node key₂ _ t₁ t₂)) key value 
+    (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-left x trb) = t-node _ _ _ ? ? ? ? ? ? (RB-repl→ti _ _ _ _ ti trb) ti₁ where
+        rr00 : (key₄ < key₃) ∧ tr< key₃ t ∧ tr< key₃ t₃
+        rr00 = RB-repl→ti< _ _ _ _ _ trb x ⟪ x₁ , ⟪ x₃ , x₄ ⟫ ⟫
 RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key value ti (rbr-black-right x trb) = ?
 RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key value ti (rbr-black-left x trb) = ?
 RB-repl→ti .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key value ti (rbr-flip-ll x trb) = ?