--- a/hoareBinaryTree.agda	Fri Nov 05 16:37:14 2021 +0900
+++ b/hoareBinaryTree.agda	Sun Nov 07 12:35:03 2021 +0900
@@ -179,10 +179,40 @@
 insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤
 insertTreeSpec0 _ _ _ = tt
 
+findPP : {n m : Level} {A : Set n} {t : Set m}
+           → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
+           → {Cond : bt A → List (bt A) → Set n}
+           → (Pre :  Cond  tree stack )
+           → (next : (tree1 : bt A) → (stack1 : List (bt A)) → Cond tree1 stack1 →  bt-depth tree1 < bt-depth tree   → t )
+           → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → Cond tree1 stack1 → t) → t
+findPP key leaf tree0 st Pre exit = exit leaf tree0 st 
+findPP key (node key₁ v tree tree₁) st Pre next exit with <-cmp key key₁
+findPP key n st c _ exit | tri≈ ¬a b ¬c = exit n st c -- c : Cond (node key₁ v tree tree₁) st 
+findPP key n@(node key₁ v tree tree₁) st Pre next _ | tri< a ¬b ¬c = next tree (n ∷ st) {!!} {!!}  -- Cond n st → Cond tree  (n ∷ st)
+findPP key n@(node key₁ v tree tree₁) st Pre next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st) {!!} {!!} -- Cond n st → Cond tree₁ (n ∷ st)
+
+record findPR {n : Level} {A : Set n} (tree : bt A ) → (stack : List (bt A)) : Set n where
+   field
+     ti : tree-invariant tree
+     si : stack-invariant tree stack
+   
+-- findP key tree stack = findPP key tree stack {findPR} → record { ti = tree-invariant tree ; si stack-invariant tree stack } → 
+
+record findP-contains {n : Level} {A : Set n} (tree : bt A ) → (stack : List (bt A)) : Set n where
+   field
+     key : ℕ
+     value : A
+     tree1 : bt A
+     ci : replacedTree key value tree tree1
+     ti : tree-invariant tree
+     si : stack-invariant tree stack
+   
 containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → replacedTree key value tree tree1   → ⊤
 containsTree {n} {m} {A} {t} tree tree1 key value P RT =
-   TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj1 p) (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree1 , [] ⟫  ⟪ RTtoTI0 tree tree1 key value P RT , lift tt  ⟫
-       $ λ p P loop → findP key (proj1 p) tree1  (proj2 p) {!!} (λ t _ s P1 lt → loop ⟪ t ,  s  ⟫ {!!} lt )
+   TerminatingLoopS (bt A ∧ List (bt A) ∧ replacedTree key value {!!} {!!} )
+     {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj1 p) (proj1 (proj2 p)) ∧ replacedTree key value {!!} {!!} } (λ p → bt-depth (proj1 p))
+              ⟪ tree1 , ⟪ [] , RT ⟫  ⟫  ⟪ RTtoTI0 tree tree1 key value P RT , ⟪ lift tt  , {!!} ⟫ ⟫
+       $ λ p P loop → findP key (proj1 p) tree1  (proj1 (proj2 p)) {!!} (λ t _ s P1 lt → loop ⟪ t ,  ⟪ s  , {!!} ⟫ ⟫ {!!} lt )
        $ λ t _ s P → insertTreeSpec0 t value {!!}
 
 insertTreeSpec1 : {n : Level} {A : Set n}  → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → ⊤