# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1697881885 -32400
# Node ID 08e04ed154684161e4e139a579c7746109b22a4d
# Parent  5c6945d527a5ef1a95b4fa1adaf862b1dfa57eb9
...

diff -r 5c6945d527a5 -r 08e04ed15468 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Sat Oct 21 10:37:07 2023 +0900
+++ b/hoareBinaryTree1.agda	Sat Oct 21 18:51:25 2023 +0900
@@ -943,35 +943,39 @@
            → stackInvariant key (RBI.tree r) orig stack
            → t
         insertCase12 leaf eq1 si = ? -- can't happen
-        insertCase12  tr0@(node key₁ value₁ left right) eq1 si with <-cmp key key₁
-        ... | tri< a ¬b ¬c = ?
-        ... | tri≈ ¬a b ¬c = ? -- can't happen
-        ... | tri> ¬a ¬b c = insertCase13 value₁ refl where
+        insertCase12  tr0@(node key₁ value₁ left right) refl si with <-cmp key key₁ | child-replaced key (node key₁ value₁ left (RBI.rot r)) in eqcd
+        ... | tri< a ¬b ¬c | cr = ?
+        ... | tri≈ ¬a b ¬c | cr = ? -- can't happen
+        ... | tri> ¬a ¬b c | cr = insertCase13 value₁ refl where
            rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → right ≡ RBI.tree r
            rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl = refl
            rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x si) refl refl with si-property1 si
            ... | refl = ⊥-elim ( nat-<> x c  )
            insertCase13 : (v : Color ∧ A ) → v ≡ value₁ → t
-           insertCase13 ⟪ Black , value₄ ⟫ eq2 = exit (node key₁ value₁ left (RBI.tree r)) (orig ∷ [])  refl record {
+           insertCase13 ⟪ Black , value₄ ⟫ refl = exit (node key₁ value₁ left repl) (orig ∷ [])  refl record {
              tree = orig ; rot = node key₁ value₁ left (RBI.rot r) 
              ; origti = RBI.origti r
              ; origrb = RBI.origrb r
              ; treerb = RBI.origrb r
-             ; replrb = rb05
+             ; replrb = proj1 rb05
              ; si = s-nil
              ; rotated = subst (λ k → rotatedTree k (node key₁ value₁ left (RBI.rot r))) (
-                trans (cong (λ k → node key₁ value₁ left k) (sym (rb04 si eq eq1))) eq1) (rtt-node rtt-unit (RBI.rotated r))
-             ; ri = {!!} 
+                trans (cong (λ k → node key₁ value₁ left k) (sym (rb04 si eq refl))) refl) (rtt-node rtt-unit (RBI.rotated r))
+             ; ri = proj2 rb05
              } where
-               rb05 : RBtreeInvariant (node key₁ value₁ left (RBI.tree r))
-               rb05 with RBI.origrb r
-               ... | rb-single key value = ?
-               ... | rb-right-red x x₁ t = ?
-               ... | rb-right-black x x₁ t = ?
-               ... | rb-left-red x x₁ t = ?
-               ... | rb-left-black x x₁ t = ?
-               ... | rb-node-red x x₁ x₂ t x₃ t₁ = ?
-               ... | rb-node-black x x₁ x₂ t x₃ t₁ = ?
+               rb05 : RBtreeInvariant (node key₁ value₁ left repl) ∧  replacedRBTree key value
+                    (child-replaced key (node key₁ value₁ left (RBI.rot r))) (node key₁ value₁ left repl)
+               rb05 with RBI.origrb r | rb04 si eq refl | RBI.replrb r in eqrepl
+               ... | rb-single key₂ value₂ | refl | rb-single key value = ?
+               ... | rb-single key₂ value₂ | refl | rb-right-red x x₁ rb = ?
+               ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb = ?
+               ... | rb-single key₂ value₂ | refl | rb-left-red x x₁ rb = ?
+               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb = ?
+               ... | rb-single key₂ value₂ | refl | rb-node-red x x₁ x₂ rb x₃ rb₁ = ?
+               ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ = ?
+               ... | rb-right-black x x₁ t | refl | rb = ?
+               ... | rb-left-black x x₁ t | refl | rb = ?
+               ... | rb-node-black x x₁ x₂ t x₃ t₁ | refl | rb = ?
            insertCase13 ⟪ Red , value₄ ⟫ eq with color (RBI.tree r)
            ... | Black = exit ? ? ? ? 
            ... | Red = exit ? ? ? ?