--- a/hoareBinaryTree.agda	Sat Dec 07 08:50:54 2019 +0900
+++ b/hoareBinaryTree.agda	Wed Jan 15 20:50:50 2020 +0900
@@ -78,6 +78,28 @@
 
 test = bt'-left {Z} {ℕ} 3 {5} (bt'-leaf 5) (s≤s (s≤s (s≤s z≤n)))
 
+
+
+-- reverse1 :  List (bt' A tn) → List (bt' A tn) → List (bt' A tn)
+-- reverse1 [] s1 = s1
+-- reverse1 (x ∷ s0) s1 with reverse1 s0 (x ∷ s1)
+-- ... | as = {!!}
+
+{--
+find でステップ毎にみている node と stack の top を一致させる
+find 中はnode と stack の top が一致する(root に来た時 stack top がなくなる)
+-- どうやって経路の入ったstackを手に入れるか?(find 実行後でよい?)
+
+
+tree+stack≡tree は find 後の tree と stack をもって
+reverse した stack を使って find をチェックするかんじ?
+--}
+
+tree+stack≡tree : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} →  (tree mtree : bt' A tn )
+  → (stack : List (bt'-path A )) →  (reverse stack) ≡ {!!}
+tree+stack≡tree tree (bt'-leaf key) stack = {!!}
+tree+stack≡tree tree (bt'-node key value mtree mtree₁ x x₁) stack = {!!}
+
 bt-find' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A )
     → ( {key1 : ℕ } → bt' A  key1 → List (bt'-path A ) → t ) → t
 bt-find' key tr@(bt'-leaf key₁) stack next = next tr stack  -- no key found
@@ -88,6 +110,12 @@
 bt-find' key tr@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri> ¬a ¬b c = 
          bt-find' key tree ( (bt'-right key {key₁} tr (<⇒≤ c) )  ∷ stack)  next
 
+
+bt-find-step : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A )
+    → ( {key1 : ℕ } → bt' A  key1 → List (bt'-path A ) → t ) → t
+bt-find-step key tr@(bt'-leaf key₁) stack exit = exit tr stack  -- no key found
+bt-find-step key (bt'-node key₁ value tree tree₁ x x₁) stack next = {!!}
+
 a<sa : { a : ℕ } → a < suc a
 a<sa {zero} = s≤s z≤n
 a<sa {suc a} = s≤s a<sa 
@@ -101,7 +129,7 @@
 pa<a {suc a} = s≤s pa<a
 
 bt-replace' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (value : A ) → (tree : bt' A tn ) → List (bt'-path A )
-    → ( {key1 : ℕ } → bt' A  key1 → t ) → t
+    → ({key1 : ℕ } → bt' A  key1 → t ) → t
 bt-replace' {n} {m} {A} {t} {tn} key value node stack next = bt-replace1 tn node where
          bt-replace0 : {tn : ℕ } (node : bt' A tn ) → List (bt'-path A ) → t
          bt-replace0 node [] = next node