--- a/hoareBinaryTree.agda	Sat May 07 20:01:07 2022 +0900
+++ b/hoareBinaryTree.agda	Tue May 10 18:44:46 2022 +0900
@@ -45,19 +45,28 @@
 bt-depth leaf = 0
 bt-depth (node key value t t₁) = suc (Data.Nat._⊔_ (bt-depth t ) (bt-depth t₁ ))
 
-find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A)
+find' : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A)
            → (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt A) → t ) → t
-find key leaf st _ exit = exit leaf st
+find' key leaf st _ exit = exit leaf st
+find' key (node key₁ v1 tree tree₁) st next exit with <-cmp key key₁
+find' key n st _ exit | tri≈ ¬a b ¬c = exit n st
+find' key n@(node key₁ v1 tree tree₁) st next _ | tri< a ¬b ¬c = next tree (n ∷ st)
+find' key n@(node key₁ v1 tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st)
+
+find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
+           → (next : (tree1 : bt A) → (stack : List (bt A)) → t)
+           → (exit : (tree1 : bt A) → (stack : List (bt A)) → t) → t
+find key leaf st _ exit = exit leaf st 
 find key (node key₁ v1 tree tree₁) st next exit with <-cmp key key₁
-find key n st _ exit | tri≈ ¬a b ¬c = exit n st
-find key n@(node key₁ v1 tree tree₁) st next _ | tri< a ¬b ¬c = next tree (n ∷ st)
-find key n@(node key₁ v1 tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st)
+find key n st _ exit | tri≈ ¬a refl ¬c = exit n st 
+find {n} {_} {A} key (node key₁ v1 tree tree₁) st  next _ | tri< a ¬b ¬c = next tree (tree ∷ st) 
+find key n@(node key₁ v1 tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st) 
 
 {-# TERMINATING #-}
 find-loop : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt A)  → (exit : bt A → List (bt A) → t) → t
 find-loop {n} {m} {A} {t} key tree st exit = find-loop1 tree st where
     find-loop1 : bt A → List (bt A) → t
-    find-loop1 tree st = find key tree st find-loop1  exit
+    find-loop1 tree st = find key tree st find-loop1 exit
 
 replaceNode : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → (bt A → t) → t
 replaceNode k v1 leaf next = next (node k v1 leaf leaf)
@@ -70,7 +79,7 @@
 ... | tri< a ¬b ¬c = exit (node key₁ value₁ repl right ) 
 ... | tri≈ ¬a b ¬c = exit (node key₁ value  left right ) 
 ... | tri> ¬a ¬b c = exit (node key₁ value₁ left repl ) 
-replace key value repl (leaf ∷ st) next exit = next key value repl st    
+replace key value repl (leaf ∷ st) next exit = next key value repl st
 replace key value repl (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁
 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st
 ... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right ) st