# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1637642519 -32400
# Node ID a8e2bb44b843bbd762fa58ac8ee02ee03586f608
# Parent  3676e845d46f4236ff3b8e7d5174e2fce8158636
...

diff -r 3676e845d46f -r a8e2bb44b843 hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Tue Nov 23 11:32:35 2021 +0900
+++ b/hoareBinaryTree.agda	Tue Nov 23 13:41:59 2021 +0900
@@ -296,18 +296,15 @@
 ... | tri< a ¬b ¬c = next key value {tree1} (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 lt si1 with  si-property1 si1   -- lt : suc key₂ ≤ key  -- not allowed
-    ... | refl = record { tree0 = replacePR.tree0 Pre; ti =  replacePR.ti  Pre ; si = si1; ri = repl04 } where
-       repl03 : replacedTree key value tree1 {!!}
-       repl03 =  r-right lt ( replacePR.ri  Pre)
-       repl04 :  replacedTree key value tree1 (node key₁ value₁ repl right)
-       repl04 = subst (λ k →  replacedTree key value tree1 k ) {!!} (r-right lt ( replacePR.ri  Pre))
-    Post | s-left lt si1 with  si-property1 si1
-    ... | refl = record { tree0 = replacePR.tree0 Pre; ti =  replacePR.ti  Pre ; si = si1; ri = repl06 } where
-       repl05 : replacedTree key value tree1 {!!}
+    ... | s-right lt si1 = {!!} -- property1 si1   -- lt : suc key₂ ≤ key  -- not allowed
+        --- lt     : suc key₂ ≤ key
+        --- a      : suc key ≤ key₁ < key₂
+    Post | s-left {t1} {t2} {t3} {key₂} {v1} lt si1 with  si-property1 si1
+    ... | eq = record { tree0 = replacePR.tree0 Pre; ti =  replacePR.ti  Pre ; si = {!!} ; ri = {!!} } where
+       repl05 : replacedTree key value {!!} (node key₂ v1 repl t3)
        repl05 =  r-left lt ( replacePR.ri  Pre)
-       repl06 :  replacedTree key value tree1 (node key₁ value₁ repl right)
-       repl06 = subst (λ k →  replacedTree key value tree1 k ) {!!} (r-left lt ( replacePR.ri  Pre))
+       repl06 :  replacedTree key value {!!} (node key₁ value₁ repl right)  -- node key₂ v1 (node key₁ value₁ left right) ≡ tree1
+       repl06 = subst (λ k →  replacedTree key value tree1 k ) {!!} {!!} -- (r-left lt ( replacePR.ri  Pre))
 ... | tri≈ ¬a b ¬c = next key value {{!!}} (node key₁ value  left right ) st {!!} ≤-refl
 ... | tri> ¬a ¬b c = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl