# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1638168728 -32400
# Node ID ce79298f4c00bd20f9eda8bfb01c167aa619caec
# Parent  8dd9b11aa358e46c306e4ff8c11d479442f80c3d
...

diff -r 8dd9b11aa358 -r ce79298f4c00 hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Mon Nov 29 15:40:55 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 29 15:52:08 2021 +0900
@@ -294,16 +294,16 @@
     repl01 | refl | refl = subst (λ k → replacedTree key value k repl) repl06 (replacePR.ri Pre)
 replaceP {n} {_} {A} key value  {tree}  repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen
 replaceP {n} {_} {A} key value {tree}  repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit  with <-cmp key key₁ | si-property1 (replacePR.si Pre)
-... | tri< a ¬b ¬c | refl = next key value {{!!}} (node key₁ value₁ repl right ) st Post ≤-refl where
+... | tri< a ¬b ¬c | refl = next key value (node key₁ value₁ repl right ) st Post ≤-refl where
     Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤) 
     Post with replacePR.si Pre
-    ... | s-right x t = {!!}
+    ... | s-right x t = {!!}  -- can't happen
     ... | s-left lt si with si-property1 si | replacePR.ri Pre
-    ... | refl | ri = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = si  ; ri = {!!} ; ci = lift tt } where
-        repl03 : replacedTree key value {!!} repl
+    ... | refl | ri = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = si  ; ri = repl04 ; ci = lift tt } where
+        repl04 :  replacedTree key value (child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) si) (node key₁ value₁ repl right)
+        repl04 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right)) {!!} (r-left a ri)
+        repl03 : replacedTree key value (child-replaced key value (node key₁ value₁ left right ∷ st) (node key₁ value₁ left right) (replacePR.tree0 Pre) (replacePR.si Pre)) repl
         repl03 = ri
-        repl02 : replacedTree key value tree (node key₁ value₁ repl right)
-        repl02 = subst (λ k → replacedTree key value (node key₁ value₁ k right) _ ) {!!} ( r-left {!!} ri )
 ... | tri≈ ¬a b ¬c | refl = next key value {{!!}} (node key₁ value  left right ) st {!!} ≤-refl -- can't happen
 ... | tri> ¬a ¬b c | refl = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl