--- a/hoareBinaryTree.agda	Fri Dec 06 18:19:24 2019 +0900
+++ b/hoareBinaryTree.agda	Sat Dec 07 08:50:54 2019 +0900
@@ -76,7 +76,7 @@
   bt'-right : (key : ℕ) → {right-key : ℕ} → (bt' A right-key ) → (right-key ≤ key) → bt'-path A
 
 
-test = bt'-left {Z} {ℕ} 3 {5} (bt'-leaf 5) (s≤s (s≤s (s≤s {!!})))
+test = bt'-left {Z} {ℕ} 3 {5} (bt'-leaf 5) (s≤s (s≤s (s≤s z≤n)))
 
 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
@@ -113,8 +113,19 @@
               (bt'-leaf (pred tn)) (bt'-leaf (suc tn) ) (≤⇒pred≤ ≤-refl) a≤sa) stack
          bt-replace1 tn (bt'-node key value node node₁ x x₁) = bt-replace0 (bt'-node key value node node₁ x x₁) stack
 
-bt-find'-assert1 : {n m : Level} {A : Set n} {t : Set m} → Set n
-bt-find'-assert1 {n} {m} {A} {t} = (key : ℕ) →  (val : A) → bt-find' key {!!} {!!} (λ tree stack → {!!})
+tree->key : {n : Level} {tn : ℕ} → (A : Set n) → (tree : bt' A tn ) → ℕ
+tree->key {n} {.key} (A) (bt'-leaf key) = key
+tree->key {n} {.key} (A) (bt'-node key value tree tree₁ x x₁) = key
+
+
+bt-find'-assert1 : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (tree : bt' A tn ) → Set n
+bt-find'-assert1 {n} {m} {A} {t} {tn} tree = (key : ℕ) →  (val : A) → bt-find' key tree [] (λ tree1 stack → key ≡ (tree->key A tree1))
+
+
+bt-replace-hoare : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (value : A ) → (tree : bt' A tn )
+                 → (pre : bt-find'-assert1 {n} {m} {A} {t} tree → bt-replace' {!!} {!!} {!!} {!!} {!!}) → t
+bt-replace-hoare key value tree stack  = {!!}
+
 
 
 -- find'-support : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → (d : ℕ) → (tree : bt' {n} {a} ) → SingleLinkedStack (bt' {n} {a} ) → ( (bt' {n} {a} ) → SingleLinkedStack (bt' {n} {a} ) → Maybe (Σ ℕ (λ d' → _iso_  {n} {a} d d')) → t ) → t