# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1638326633 -32400
# Node ID ca624203b453012c27d9ce10a1668217195f3e3b
# Parent  a971a954a345eeb90812d12c0ecc18c4de8d7fbe
...

diff -r a971a954a345 -r ca624203b453 hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Wed Dec 01 11:24:42 2021 +0900
+++ b/hoareBinaryTree.agda	Wed Dec 01 11:43:53 2021 +0900
@@ -404,7 +404,7 @@
 ... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right ) st Post ≤-refl where -- can't happen
     Post :  replacePR key value tree1 (node key₁ value left right ) (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤)
     Post with replacePR.si Pre 
-    ... | s-right  {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
+    ... | s-right  {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 b ; ci = lift tt } where
         repl09 : tree1 ≡ node key₂ v1 tree₁ tree -- (node key₁ value₁  left right)
         repl09 = si-property1 si
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
@@ -415,9 +415,10 @@
         ... |  tri< a ¬b ¬c = ⊥-elim (¬c x)
         ... |  tri≈ ¬a b ¬c = ⊥-elim (¬c x)
         ... |  tri> ¬a ¬b c = refl
-        repl12 : replacedTree key value (child-replaced key  tree1  ) (node key₁ value left right )
-        repl12 = {!!}
-    ... | s-left  {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
+        repl12 : (key ≡ key₁) → replacedTree key value (child-replaced key  tree1  ) (node key₁ value left right )
+        repl12 refl with repl09 
+        ... | refl = subst (λ k → replacedTree key value k (node key₁ value left right )) (sym repl07) r-node
+    ... | s-left  {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 b ; ci = lift tt } where
         repl09 : tree1 ≡ node key₂ v1 tree tree₁ 
         repl09 = si-property1 si
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
@@ -428,8 +429,9 @@
         ... |  tri< a ¬b ¬c = refl
         ... |  tri≈ ¬a b ¬c = ⊥-elim (¬a x)
         ... |  tri> ¬a ¬b c = ⊥-elim (¬a x)
-        repl12 : replacedTree key value (child-replaced key  tree1  ) (node key₁ value left right )
-        repl12 = {!!}
+        repl12 : (key ≡ key₁) → replacedTree key value (child-replaced key  tree1  ) (node key₁ value left right )
+        repl12 refl with repl09 
+        ... | refl = subst (λ k → replacedTree key value k (node key₁ value left right )) (sym repl07) r-node
 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st Post ≤-refl where
     Post : replacePR key value tree1 (node key₁ value₁ left repl ) st (λ _ _ _ → Lift n ⊤) 
     Post with replacePR.si Pre