# HG changeset patch
# User Moririn
# Date 1703053528 -32400
# Node ID a11ebb914b7c66242c3be257a695e77df3f61a92
# Parent  28323f2e6dc4a7c0122f77ded0de2d294a0fa152
...

diff -r 28323f2e6dc4 -r a11ebb914b7c hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Mon Dec 18 18:58:21 2023 +0900
+++ b/hoareBinaryTree1.agda	Wed Dec 20 15:25:28 2023 +0900
@@ -626,9 +626,14 @@
    → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1)
    → rotatedTree  (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1)))
    (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr))
+   
 RightDown : {n : Level} {A : Set n} → bt (Color ∧ A) → bt (Color ∧ A)
 RightDown leaf = leaf
 RightDown (node key ⟪ c , value ⟫ t1 t2) = t2
+LeftDown : {n : Level} {A :  Set n} → bt (Color ∧ A) → bt (Color ∧ A)
+LeftDown leaf = leaf
+LeftDown (node key ⟪ c , value ⟫ t1 t2 ) = t1
+
 RBtreeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color}
  →  (tleft tright : bt (Color ∧ A))
  → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright)
@@ -983,11 +988,13 @@
                ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | tri≈ ¬a b ¬c = {!!}
                ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | tri> ¬a ¬b c = ⊥-elim {!!}
                ... | rb-single key₂ value₂ | refl | rb-left-red x x₁ rb | t = {!!} --red -red
-               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri< a ¬b ¬c = ⟪ rb-right-red a (blackdepth≡ ? ? ? ? ? ) ? , ? ⟫
-               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri≈ ¬a b ¬c = {!!}
-               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri> ¬a ¬b c = ⊥-elim ?
+               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri< a ¬b ¬c = ⟪ rb-right-red a (blackdepth≡ (LeftDown repl) leaf (RBtreeLeftDown (LeftDown repl) leaf (RBI.replrb r)) rb-leaf (RBI.replrb r)) (RBI.replrb r) , {!!} ⟫
+               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri≈ ¬a b ¬c = ⊥-elim (¬c {!!})
+               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri> ¬a ¬b c = ⊥-elim {!!}
                ... | rb-single key₂ value₂ | refl | rb-node-red x x₁ x₂ rb x₃ rb₁ | t = {!!}　-- red-red
-               ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ | t = {!!} 
+               ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ | tri< a ¬b ¬c = {!!}
+               ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ | tri≈ ¬a b ¬c = {!!}
+               ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ | tri> ¬a ¬b c = ⊥-elim {!!}
                --... | rb-right-black x x₁ t | refl | rb | t = ? --⟪ proj1 {!!} , {!!} ⟫
                --... | rb-left-black x x₁ t | refl | rb | t = {!!} --⟪ rb-node-red ? ? ? ? ? ? , ? ⟫
                --... | rb-node-black x x₁ x₂ t x₃ t₁ | refl | rb | t = {!!}