# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1637320029 -32400
# Node ID 6c3d50b30bea3c331aaf04a9a1e62dc2866812b5
# Parent  7b24e17e144172e21d2c20bfa5f43397c2bb9f36
...

diff -r 7b24e17e1441 -r 6c3d50b30bea hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Fri Nov 19 18:31:06 2021 +0900
+++ b/hoareBinaryTree.agda	Fri Nov 19 20:07:09 2021 +0900
@@ -243,12 +243,15 @@
      → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
 replaceP key value {tree0} {tree} repl [] Pre next exit with proj1 (proj2 Pre)
 ... | ()
-replaceP key value {tree0} {tree} repl (leaf ∷ []) Pre next exit = exit tree0 (node key value leaf leaf) ⟪ {!!} , {!!} ⟫
+replaceP {_} {_} {A} key value {tree0} {tree} repl (leaf ∷ []) Pre next exit =
+        exit tree0 repl ⟪ proj1 Pre , subst (λ k → replacedTree key value k repl ) (repl4 (proj1 (proj2 Pre))) (proj2 (proj2 Pre)) ⟫ where
+    repl4 : stackInvariant key tree tree0 (leaf ∷ []) →  tree ≡ tree0
+    repl4 (s-single .leaf) = refl
 replaceP key value {tree0} {tree} repl (leaf ∷ leaf ∷ st) Pre next exit = {!!} -- can't happen
 replaceP key value {tree0} {tree} repl (leaf ∷ node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁
-... | tri< a ¬b ¬c = next key value (node key₁ value₁ left {!!} ) st {!!} ?
+... | tri< a ¬b ¬c = next key value (node key₁ value₁ left repl ) st {!!} {!!}
 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right) st {!!} {!!} 
-... | tri> ¬a ¬b c = next key value (node key₁ value₁ {!!} right) st {!!} {!!} 
+... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right) st {!!} {!!} 
 replaceP key value {tree0} {tree} repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁
 ... | tri> ¬a ¬b c = next key value  (node key₁ value₁ repl right ) st {!!}  ≤-refl
 ... | tri≈ ¬a b ¬c = next key value  (node key value left right ) st {!!}  ≤-refl where -- this case won't happen
@@ -259,8 +262,6 @@
     repl2 (s-left _ si) = {!!}
 
 
---- ... next key value (node key₁ value₁ left tree ) (node key₁ value₁ left repl ) st  ≤-refl  where
-
 open import Relation.Binary.Definitions
 
 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥