--- a/hoareBinaryTree1.agda	Wed Feb 26 18:27:54 2020 +0900
+++ b/hoareBinaryTree1.agda	Wed Feb 26 19:00:08 2020 +0900
@@ -14,7 +14,7 @@
 
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary
+open import Relation.Nullary hiding (proof)
 open import logic
 
 
@@ -61,7 +61,30 @@
 insert-test1 = bt-insert 5 7 bt-empty (λ x → bt-insert 15 17 x (λ y → y))
 
 
+tree+stack0 : {n : Level} {A : Set n} → (tree mtree : bt A) →  (stack : List (bt A))  → Set n
+tree+stack0 {n} {A} tree mtree [] = {!!}
+tree+stack0 {n} {A} tree mtree (x ∷ stack) = {!!}
+
 tree+stack : {n : Level} {A : Set n} → (tree mtree : bt A) →  (stack : List (bt A))  → Set n
 tree+stack {n} {A} bt-leaf mtree stack = (mtree ≡ bt-leaf) ∧ (stack ≡ [])
 tree+stack {n} {A} (bt-node key x tree tree₁) mtree stack = bt-replace key x mtree stack (λ ntree → ntree ≡ tree) 
 
+data _implies_  (A B : Set ) : Set (succ Z) where
+    proof : ( A → B ) → A implies B
+
+implies2p : {A B : Set } → A implies B  → A → B
+implies2p (proof x) = x
+
+
+bt-find-hoare1  : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree mtree : bt A ) → (stack : List (bt A))
+  → (tree+stack tree mtree stack)
+  → ( (ntree : bt A) → (nstack : List (bt A)) → (tree+stack tree ntree nstack) → t ) → t
+bt-find-hoare1 {n} {m} {A} {t}  key leaf@(bt-leaf) mtree stack t+s exit = exit leaf stack {!!}
+bt-find-hoare1 {n} {m} {A} {t}  key (bt-node key₁ AA tree tree₁) mtree stack t+s next with <-cmp key key₁
+bt-find-hoare1 {n} {m} {A} {t}  key node@(bt-node key₁ AA tree tree₁) mtree stack t+s exit | tri≈ ¬a b ¬c = exit node stack {!!}
+bt-find-hoare1 {n} {m} {A} {t}  key node@(bt-node key₁ AA ltree rtree) mtree stack t+s next | tri< a ¬b ¬c = bt-find-hoare1 {n} {m} {A} {t} key ltree {!!} (node ∷ stack) {!!} {!!}
+bt-find-hoare1 {n} {m} {A} {t}  key node@(bt-node key₁ AA ltree rtree) mtree stack t+s next | tri> ¬a ¬b c = bt-find-hoare1 key rtree {!!} (node ∷ stack) {!!} {!!}
+
+
+bt-find-hoare : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → ( (ntree : bt A) → (nstack : List (bt A)) → (tree+stack tree ntree nstack) → t ) → t
+bt-find-hoare {n} {m} {A} {t}  key node exit = bt-find-hoare1 {n} {m} {A} {t} key node bt-empty [] ({!!}) exit