--- a/hoareBinaryTree.agda	Wed May 11 09:56:11 2022 +0900
+++ b/hoareBinaryTree.agda	Mon May 16 09:27:13 2022 +0900
@@ -56,7 +56,6 @@
 find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
            → (next : (tree1 : bt A) → (stack : List (bt A)) → t)
            → (exit : (tree1 : bt A) → (stack : List (bt A)) → t) → t
-find key _ (leaf ∷ st) _ exit = exit leaf []
 find key leaf st _ exit = exit leaf st 
 find key (node key₁ v1 tree tree₁) st next exit with <-cmp key key₁
 find key n st _ exit | tri≈ ¬a refl ¬c = exit n st 
@@ -97,8 +96,8 @@
 
 insertTest1 = insertTree leaf 1 1 (λ x → x )
 insertTest2 = insertTree insertTest1 2 1 (λ x → x )
-insertTest3 = insertTree insertTest2 3 2 (λ x → x )
-insertTest4 = insertTree insertTest3 2 2 (λ x → x ) -- this is wrong
+insertTest3 = insertTree insertTest2 3 3 (λ x → x )
+insertTest4 = insertTree insertTest3 1 4 (λ x → x ) -- this is wrong
 
 updateTree : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (empty : bt A → t ) → (next : A → bt A  → t ) → t
 updateTree {_} {_} {A} {t} tree key value empty next = find-loop key tree ( tree ∷ [] )
@@ -260,22 +259,22 @@
 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)   : Set (Level.suc n) where
-   field
-      c1 : {key key₁ : ℕ}  {v1 : A } { tree tree₁ : bt A } → C key (node key₁ v1 tree tree₁) → key < key₁  → C key tree
-      c2 : {key 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 → FindCond C
-           → (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 e _ exit | tri≈ ¬a refl ¬c = exit n st Pre (case2 refl)
-findP0 {n} {_} {A} key (node key₁ v1 tree tree₁) st  Pre e next _ | tri< a ¬b ¬c = next tree (tree ∷ st) (FindCond.c1 e Pre a) depth-1< 
-findP0 key n@(node key₁ v1 tree tree₁) st Pre e next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st) (FindCond.c2 e Pre c) depth-2<
+-- record FindCond {n  : Level} {A : Set n} (C : ℕ → bt A → Set n)   : Set (Level.suc n) where
+--    field
+--       c1 : {key key₁ : ℕ}  {v1 : A } { tree tree₁ : bt A } → C key (node key₁ v1 tree tree₁) → key < key₁  → C key tree
+--       c2 : {key 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 → FindCond C
+--            → (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 e _ exit | tri≈ ¬a refl ¬c = exit n st Pre (case2 refl)
+-- findP0 {n} {_} {A} key (node key₁ v1 tree tree₁) st  Pre e next _ | tri< a ¬b ¬c = next tree (tree ∷ st) (FindCond.c1 e Pre a) depth-1< 
+-- findP0 key n@(node key₁ v1 tree tree₁) st Pre e next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st) (FindCond.c2 e Pre c) 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