--- a/hoareBinaryTree.agda	Sun Dec 05 14:50:04 2021 +0900
+++ b/hoareBinaryTree.agda	Sun Dec 05 18:57:23 2021 +0900
@@ -241,6 +241,24 @@
 treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .leaf (t-left x ti) = t-leaf
 treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node x x₁ ti ti₁) = ti₁
 
+
+record findCond {n  : Level} {A : Set n} {C : ℕ → bt A → Set n} ( key : ℕ ) (tree : bt A) : Set (suc n) where
+   field
+      c1 : {key₁ : ℕ} } {v1 : A } { tree₀ tree₁ : bt A } → C key (node key₁ v1 tree tree₁) → key < key₁  → C key tree
+      c2 : {key₁ : ℕ} } {v1 : A } { tree₀ tree₁ : bt A } → C key (node key₁ v1 tree tree₁) → key > key₁  → C key tree
+
+
+findP0 : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
+           →  {C : ℕ → bt A → Set n} → C key tree
+           → (next : (tree1 : bt A) → (stack : List (bt A)) → C key tree1 → bt-depth tree1 < bt-depth tree   → t )
+           → (exit : (tree1 : bt A) → (stack : List (bt A)) → C key tree1 
+                 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
+findP0 key leaf st Pre _ exit = exit leaf st Pre (case1 refl)
+findP0 key (node key₁ v1 tree tree₁) st Pre next exit with <-cmp key key₁
+findP0 key n st Pre _ exit | tri≈ ¬a refl ¬c = exit n st Pre (case2 refl)
+findP0 {n} {_} {A} key (node key₁ v1 tree tree₁) st  Pre next _ | tri< a ¬b ¬c = next tree (tree ∷ st) {!!}  depth-1< 
+findP0 key n@(node key₁ v1 tree tree₁) st Pre next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st) {!!} depth-2<
+
 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
            →  treeInvariant tree ∧ stackInvariant key tree tree0 stack  
            → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree   → t )
@@ -253,6 +271,7 @@
        ⟪ treeLeftDown tree tree₁ (proj1 Pre)  , findP1 a st (proj2 Pre) ⟫ depth-1< where
    findP1 : key < key₁ → (st : List (bt A)) →  stackInvariant key (node key₁ v1 tree tree₁) tree0 st → stackInvariant key tree tree0 (tree ∷ st)
    findP1 a (x ∷ st) si = s-left a si
+
 findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ (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₁)