--- a/hoareBinaryTree.agda	Fri Nov 19 16:59:44 2021 +0900
+++ b/hoareBinaryTree.agda	Fri Nov 19 18:31:06 2021 +0900
@@ -65,7 +65,12 @@
 
 replace : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → List (bt A) → (next : ℕ → A → bt A → List (bt A) → t ) → (exit : bt A → t) → t
 replace key value tree [] next exit = exit tree
-replace key value tree (leaf ∷ st) next exit = next key value tree st 
+replace key value tree (leaf ∷ []) next exit = exit (node key value leaf leaf)
+replace key value tree (leaf ∷ leaf ∷ st) next exit = exit (node key value leaf leaf)
+replace key value tree (leaf ∷ node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁
+... | tri< a ¬b ¬c = next key value (node key₁ value₁ (node key value leaf leaf) right ) st
+... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right ) st
+... | tri> ¬a ¬b c = next key value (node key₁ value₁ left (node key value leaf leaf) ) st
 replace key value tree (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁
 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) st
 ... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right ) st
@@ -137,11 +142,6 @@
 stackInvariantTest1 : stackInvariant 2 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] )
 stackInvariantTest1 = s-right (add< 0) (s-single treeTest1 )
 
-si-property0 :  {n : Level} {A : Set n} {key : ℕ} {tree tree0 : bt A} → {st : List (bt A)} →  stackInvariant key tree tree0 (leaf ∷ st ) → tree ≡ tree0
-si-property0 {n} {A} {key} {.leaf} {.leaf} {.[]} (s-single .leaf) = refl
-si-property0 {n} {A} {key} {.leaf} {tree0} {st} (s-right x si) = {!!}
-si-property0 {n} {A} {key} {.leaf} {tree0} {st} (s-left x si) = {!!}
-
 si-property1 :  {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack  : List (bt A)) → stackInvariant key tree tree0 stack
    → stack-top stack ≡ just tree
 si-property1 key t t0 (x ∷ .[]) (s-single .x) = refl
@@ -243,19 +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 ∷ st) Pre next exit =
-    exit tree0 repl ⟪ proj1 Pre  , subst (λ k → replacedTree key value k repl ) (si-property0 (proj1 (proj2 Pre)))  (proj2 (proj2 Pre)) ⟫ 
+replaceP key value {tree0} {tree} repl (leaf ∷ []) Pre next exit = exit tree0 (node key value leaf leaf) ⟪ {!!} , {!!} ⟫
+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 right) st {!!} {!!} 
+... | tri> ¬a ¬b c = next key value (node key₁ value₁ {!!} 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
-    repleq : tree0 ≡ node key₁ value₁ left right
-    repleq with si-property1 _ _ _ _ (proj1 (proj2 Pre))
-    ... | refl = {!!}
-    repl1 : treeInvariant (node key₁ value₁ left right) -- stackInvariant (node key₁ value₁ left right) tree st
-    repl1 = stackTreeInvariant _ _ _ (node key₁ value₁ left right ∷ st) (proj1 Pre)
-        {!!} -- (subst (λ k → stackInvariant k tree (node key₁ value₁ left right ∷ st)) repleq (proj1 (proj2 Pre)))
-    repl3 : replacedTree key value (node key₁ value₁ left right) (node key₁ value left right)
-    repl3 = subst (λ k → replacedTree k value (node key₁ value₁ left right) (node key₁ value left right) ) (sym b) r-node
 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ left repl)  st ⟪ proj1 Pre , ⟪ {!!} ,  r-right a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl   where
     repl2 : stackInvariant key tree tree0 (node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ left tree) tree0 st
     repl2 (s-single .(node key₁ value₁ left right)) = {!!}