--- a/hoareBinaryTree1.agda	Sat Apr 06 18:19:23 2024 +0900
+++ b/hoareBinaryTree1.agda	Wed May 01 22:21:16 2024 +0900
@@ -833,12 +833,12 @@
                                     (node kp ⟪ Black , vp ⟫ (node kg ⟪ Red , vg ⟫ uncle t) t₂ )
     -- case56 the node is inner, make it outer and rotate grand
     rbr-rotate-lr : {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A}
-         → kp < kn → kn < kg
+         → kp < key → key < kg
          → replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁)     uncle)
                                     (node kn ⟪ Black , vn ⟫ (node kp ⟪ Red , vp ⟫ t t₂)     (node kg ⟪ Red , vg ⟫ t₃ uncle))
     rbr-rotate-rl : {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A}
-         → kg < kn → kn < kp
+         → kg < key → key < kp
          → replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle                           (node kp ⟪ Red , vp ⟫ t₁ t))
                                     (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , vg ⟫ uncle t₂) (node kp ⟪ Red , vp ⟫ t₃ t))
@@ -1198,8 +1198,9 @@
      (RB-repl→ti _ _ _ _ ti₂ trb) where
         rr00 : (key₂ < key₆) ∧ tr> key₂ t₃ ∧ tr> key₂ t₄
         rr00 = RB-repl→ti> _ _ _ _ _ trb lt ⟪ x₈ , ⟪ x₁₁ , x₁₂ ⟫ ⟫
-RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ leaf leaf) .leaf) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ leaf) (node kg ⟪ Red , _ ⟫ leaf _)) key value (t-left .kp .kg x x₁ x₂ ti) (rbr-rotate-lr .leaf .leaf kg kp kn lt1 lt2 trb) = t-node _ _ _ lt1 lt2 tt tt tt tt (t-single _ _) (t-single _ _) 
-RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ (node key₁ value₁ t t₁) leaf) .leaf) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₃) (node kg ⟪ Red , _ ⟫ t₄ _)) key value (t-left .kp .kg x x₁ x₂ ti) (rbr-rotate-lr t₃ t₄ kg kp kn lt1 lt2 trb) = ?
+RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ leaf leaf) .leaf) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ leaf) (node kg ⟪ Red , _ ⟫ leaf _)) .kn _ (t-left .kp .kg x x₁ x₂ ti) (rbr-rotate-lr .leaf .leaf kg kp kn lt1 lt2 rbr-leaf) = t-node _ _ _ lt1 lt2 tt tt tt tt (t-single _ _) (t-single _ _)
+RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ (node key₁ value₁ t t₁) leaf) .leaf) (node kn ⟪ Black , v3 ⟫ (node kp ⟪ Red , _ ⟫ _ leaf) (node kg ⟪ Red , _ ⟫ leaf _)) .kn .v3 (t-left .kp .kg x x₁ x₂ (t-left .key₁ .kp x₃ x₄ x₅ ti)) (rbr-rotate-lr .leaf .leaf kg kp kn lt1 lt2 rbr-leaf) = 
+    t-node _ _ _ lt1 lt2 ⟪ <-trans x₃ lt1  , ⟪ >-tr< x₄ lt1  , >-tr< x₅ lt1 ⟫ ⟫  tt tt tt (t-left _ _ x₃ x₄ x₅ ti) (t-single _ _) 
 RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ t (node key₁ value₁ t₁ t₂)) .leaf) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₃) (node kg ⟪ Red , _ ⟫ t₄ _)) key value (t-left .kp .kg x x₁ x₂ ti) (rbr-rotate-lr t₃ t₄ kg kp kn lt1 lt2 trb) = ?
 RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ t leaf) .(node key₂ _ _ _)) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₃) (node kg ⟪ Red , _ ⟫ t₄ _)) key value (t-node .kp .kg key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-lr t₃ t₄ kg kp kn lt1 lt2 trb) = ?
 RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ t (node key₁ value₁ t₁ t₂)) .(node key₂ _ _ _)) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₃) (node kg ⟪ Red , _ ⟫ t₄ _)) key value (t-node .kp .kg key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-lr t₃ t₄ kg kp kn lt1 lt2 trb) = ?