# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1710742437 -32400
# Node ID 887d84484e119fe57ff3a97913dea9e3099acd51
# Parent  61f56e51ba3d0aa8e7300e0db6539c814089e8a2
...

diff -r 61f56e51ba3d -r 887d84484e11 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Mon Mar 18 09:02:11 2024 +0900
+++ b/hoareBinaryTree1.agda	Mon Mar 18 15:13:57 2024 +0900
@@ -983,8 +983,12 @@
         rr00 : (key₂ < key₃) ∧ tr> key₂ t ∧ tr> key₂ t₁ 
         rr00 = RB-repl→ti> _ _ _ _ _ trb x ⟪ x₁ , ⟪ x₂ , x₃ ⟫ ⟫
 RB-repl→ti .(node key₂ ⟪ ca , v1 ⟫ (node key₁ value₁ t t₁) leaf) (node key₂ ⟪ ca , v1 ⟫ (node key₁ value₁ t t₁) (node key₃ value₂ t₂ t₃)) key value 
-   (t-left key₁ _ x₁ x₂ x₃ ti) (rbr-right x trb) = ?
-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-right x trb) = ?
+   (t-left key₁ _ x₁ x₂ x₃ ti) (rbr-right x trb) = t-node _ _ _ x₁ (proj1 rr00) x₂ x₃ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) ti (RB-repl→ti _ _ _ _ t-leaf trb) where
+        rr00 : (key₂ < key₃) ∧ tr> key₂ t₂ ∧ tr> key₂ t₃
+        rr00 = RB-repl→ti> _ _ _ _ _ trb x tt
+RB-repl→ti .(node key₃ ⟪ ca , v1 ⟫ (node key₁ v2 t₁ t₂) (node key₂ _ _ _)) (node key₃ ⟪ ca , v1 ⟫ (node key₁ v2 t₁ t₂) (node key₄ value₁ t₃ t₄)) key value (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-right x trb) = t-node _ _ _ ? ? ? ? ? ? ? ? where
+        rr00 : (key₃ < key₄) ∧ tr> key₃ t₃ ∧ tr> key₃ t₄
+        rr00 = RB-repl→ti> _ _ _ _ _ trb x ?
 RB-repl→ti .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key value ti (rbr-left x trb) = ?
 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) = ?