--- a/hoareBinaryTree.agda	Sun Nov 21 09:22:59 2021 +0900
+++ b/hoareBinaryTree.agda	Sun Nov 21 10:09:05 2021 +0900
@@ -242,9 +242,8 @@
 findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n tree0 st Pre (case2 refl)
 findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (tree ∷ st) ⟪ treeLeftDown tree tree₁ (proj1 Pre)  , findP1 a (proj2 Pre) ⟫ depth-1< where
    findP1 : key < key₁ →  stackInvariant key (node key₁ v1 tree tree₁) tree0 st → stackInvariant key tree tree0 (tree ∷ st)
-   findP1 a si = {!!}
-findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (tree₁ ∷ st) ⟪ treeRightDown tree tree₁ (proj1 Pre) , {!!} ⟫ depth-2<
-
+   findP1 a si = s-left a si
+findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (tree₁ ∷ st) ⟪ treeRightDown tree tree₁ (proj1 Pre) , s-right c (proj2 Pre) ⟫ depth-2<
 
 replaceTree1 : {n  : Level} {A : Set n} {t t₁ : bt A } → ( k : ℕ ) → (v1 value : A ) →  treeInvariant (node k v1 t t₁) → treeInvariant (node k value t t₁)
 replaceTree1 k v1 value (t-single .k .v1) = t-single k value
@@ -277,28 +276,27 @@
      → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
 replaceP key value {tree0} {tree} {tree-st} repl [] Pre next exit with proj1 (proj2 Pre)
 ... | ()
-replaceP {_} {_} {A} key value {tree0} {tree} {tree-st} repl (leaf ∷ []) Pre next exit =
-        exit tree0 repl ⟪ proj1 Pre , subst (λ k → replacedTree key value k repl ) {!!} {!!} ⟫ where
-    repl41 : tree-st ≡ tree
-    repl41  = {!!}
-replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ leaf ∷ st) Pre next exit = ⊥-elim ( repl3 (proj1 (proj2 Pre))) where -- can't happen
-    repl3 : stackInvariant key tree-st tree0 (leaf ∷ leaf ∷ st) → ⊥
-    repl3 = {!!}
+replaceP {_} {_} {A} key value {tree0} {tree} {tree-st} repl (leaf ∷ []) Pre next exit with proj1 (proj2 Pre)
+... | s-right x ()
+... | s-left x ()
+replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ leaf ∷ st) Pre next exit with proj1 (proj2 Pre)
+... | s-right x ()
+... | s-left x ()
 replaceP {_} {_} {A} key value {tree0} {tree} {tree-st} 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₁ repl right ) (node key₁ value₁ tree right ∷ st)
                   ⟪ proj1 Pre , ⟪ repl5 (proj1 (proj2 Pre)) , r-left a (proj2 (proj2 Pre))  ⟫ ⟫ ≤-refl where
     repl5 :  stackInvariant key tree-st tree0 (leaf ∷ node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ tree right) tree0 (node key₁ value₁ tree right ∷ st )
-    repl5 = {!!}
-    -- ... | refl = ⊥-elim (nat-<> a x)
-    -- repl5 (s-left x si) with  si-property1 _ _ _ _ si -- stackInvariant key (node key₁ value₁ leaf right) tree0 (node key₁ value₁ leaf right ∷ st)
-                                                 --      stackInvariant key (node key₁ value₁ tree right) tree0 (node key₁ value₁ tree right ∷ st)
-    -- ... | refl = {!!}  -- tree ≡ leaf
+    repl5 si with si-property1 _ _ _ _ si
+    repl5 (s-right x si) | refl = s-left a {!!}
+    repl5 (s-left x si) | refl = s-left a {!!}
 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right) st {!!} depth-3<
 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right) st {!!} depth-3<
 replaceP key value {tree0} {tree} {tree-st} 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
 ... | tri< a ¬b ¬c with proj1 (proj2 Pre)
+... | s-right0 x = {!!}
+... | s-left0 x = {!!}
 ... | s-right x si1 = {!!}
 ... | s-left x si1 = next key value (node key₁ value₁ repl right )  st ⟪ proj1 Pre , ⟪ si1 ,  r-left a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl   
 -- = next key value (node key₁ value₁ repl right )  st ⟪ proj1 Pre , ⟪ repl2 (proj1 (proj2 Pre)) ,  r-left a {!!}  ⟫ ⟫ ≤-refl   where