--- a/bt/bt.agda	Sat Nov 06 19:45:49 2021 +0900
+++ b/bt/bt.agda	Sat Nov 06 20:06:24 2021 +0900
@@ -4,7 +4,6 @@
 open import Level renaming (zero to Z ; suc to succ)
 open import Data.List
 
-
 open import Data.Nat.Properties as NatProp -- <-cmp
 open import Relation.Binary
 
@@ -22,19 +21,6 @@
     vart : bt A
     varl : List (bt A)
 open Env
-{-
-bt-depth : {n : Level} {A : Set n} → (env : Env A ) → ℕ
-bt-depth env  with vart env
-... | leaf = zero
-... | node key value ltree rtree = Data.Nat._⊔_ (bt-depth-c ltree ) (bt-depth-c rtree ) where
-    bt-depth-c : {n : Level} {A : Set n} → (tree : bt A ) → ℕ
-    bt-depth-c leaf = suc zero
-    bt-depth-c (node key value lt rt) = suc (Data.Nat._⊔_ (bt-depth-c lt ) ( bt-depth-c rt))
--}
-
-bt-depth : {n : Level} {A : Set n} → (tree : bt A ) → ℕ
-bt-depth leaf = 0
-bt-depth (node key value t t₁) = Data.Nat._⊔_ (bt-depth t ) (bt-depth t₁ )
 
 bt-depth1 : {n : Level} {A : Set n} → (env : Env A ) → ℕ
 bt-depth1 env  with vart env
@@ -43,24 +29,12 @@
     bt-depth-c leaf = zero
     bt-depth-c (node key value lt rt) = suc (Data.Nat._⊔_ (bt-depth-c lt ) ( bt-depth-c rt))
 
-test-depth :  ℕ
-test-depth = bt-depth (node 3 0 leaf (node 1 1 leaf (node 3 5 leaf leaf)))
-
 test-env : {n : Level} {A : Set n} →  Env ℕ
 test-env = record {varn = 0; varv = 4 ; vart = (node 3 2 leaf (node 1 1 leaf (node 3 5 leaf leaf))); varl = []}
 
 test-depth1 :  ℕ
 test-depth1 = bt-depth1 record {varn = 0; varv = 4;  vart = (node 3 0 leaf (node 1 1 leaf (node 3 5 leaf leaf))); varl = []}
 
-find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A)
-           → (next : bt A → List (bt A) → t )
-           → (exit : bt A → List (bt A) → t ) → t
-find key leaf st _ exit = exit leaf st
-find key (node key₁ v tree tree₁) st next exit with <-cmp key key₁
-find key n st _ exit | tri≈ ¬a b ¬c = exit n st
-find key n@(node key₁ v tree tree₁) st next _ | tri< a ¬b ¬c = next tree (n ∷ st)
-find key n@(node key₁ v tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st)
-
 find1 : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
            → (next : (env : Env A ) → t )
            → (exit : (env : Env A ) → t ) → t
@@ -74,20 +48,6 @@
     ... | tri≈ ¬a b ¬c = exit record env {vart = n}
     ... | tri> ¬a ¬b c = find1-c key rtree record env {vart = rtree ; varl = (n ∷ (varl env))} next exit
 
-{-
-... | leaf = exit env
-... | n@(node key-t value ltree rtree) with <-cmp (varn env) key-t
-... | tri≈ ¬a b ¬c = exit record env {vart = n}
-... | tri< a ¬b ¬c = find1 record env {vart = ltree ; varl = (n ∷ (varl env))} next exit
-... | tri> ¬a ¬b c = find1 record env {vart = rtree ; varl = (n ∷ (varl env))} next exit
--}
-
-{-# TERMINATING #-}
-find-loop : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt A)  → (exit : bt A → List (bt A) → t) → t
-find-loop {n} {m} {A} {t} key tree st exit = find-loop1 tree st where
-    find-loop1 : bt A → List (bt A) → t
-    find-loop1 tree st = find key tree st find-loop1 exit
-
 find-loop-1 : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
     → (exit : (env : Env A ) → t) → t
 find-loop-1 env exit = find1 env exit exit
@@ -97,26 +57,12 @@
 
 test-cg = find-loop-1 record {varn = 5; varv = 4; vart = (node 2 2 (node 1 1 leaf leaf) (node 4 4 leaf (node 5 5 leaf leaf))); varl = []} (λ env → env )
 
-replaceNode : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → (bt A → t) → t
-replaceNode k v leaf next = next (node k v leaf leaf)
-replaceNode k v (node key value t t₁) next = next (node k v t t₁)
-
 replaceNode1 : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
     → (next : Env A → t) → t
 replaceNode1 env next with vart env
 ... | leaf = next record env {vart = (node (varn env) (varv env) leaf leaf) }
 ... | node key-t value ltree rtree = next record env {vart = (node (varn env) (varv env) ltree rtree) }
 
-replace : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → List (bt A)
-    → (next : ℕ → A → bt A → List (bt A) → t )
-    → (exit : bt A → t) → t
-replace key value tree [] next exit = exit tree
-replace key value tree (leaf ∷ st) next exit = next key value tree st
-replace key value tree (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁
-... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) st
-... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right ) st
-... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) st
-
 replace1 : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
     → (next : Env A → t )
     → (exit : Env A → t) → t
@@ -132,25 +78,6 @@
     ... | tri≈ ¬a b ¬c = replace1-c st1 record env{vart = (node key-t (varv env) ltree rtree); varl = st1} next exit
     ... | tri> ¬a ¬b c = replace1-c st1 record env{vart = (node key-t value ltree (vart env)); varl = st1} next exit
 
-{-
-replace1 env next exit = next env
-replace1 env tree (node key₁ value₁ left right ∷ st) next exit with <-cmp (varn env) key₁
-... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) st
-... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right ) st
-... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) st
--}
-
-{-# TERMINATING #-}
-replace-loop : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → List (bt A)  → (exit : bt A → t) → t
-replace-loop {_} {_} {A} {t} key value tree st exit = replace-loop1 key value tree st where
-    replace-loop1 : (key : ℕ) → (value : A) → bt A → List (bt A) → t
-    replace-loop1 key value tree st = replace key value tree st replace-loop1  exit
-
-insertTree : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : bt A → t ) → t
-insertTree tree key value exit = find-loop key tree []
-  $ λ t st → replaceNode key value t -- find-loop next
-  $ λ t1 → replace-loop key value t1 st exit -- replaceNode exit
-
 replace-loop1 : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
     → (exit : (env : Env A ) → t) → t
 replace-loop1 env exit = replace1 env exit exit
@@ -160,12 +87,12 @@
   $ λ env → replaceNode1 env
     $ λ env → replace-loop1 env exit
 
-insertTree11 : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : Env A  → t ) → t
-insertTree11 tree key value exit = find-loop-1 record{varn = key; varv = value; vart = tree ; varl = []}
+replaceTree1 : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : Env A  → t ) → t
+replaceTree1 tree key value exit = find-loop-1 record{varn = key; varv = value; vart = tree ; varl = []}
   $ λ env → replaceNode1 env exit
 
 test-insert = insertTree1 (node 2 2 (node 1 1 leaf leaf) (node 4 4 leaf (node 5 5 leaf leaf))) 0 5 (λ env → env )
 
-test-insert1 = insertTree11 (node 2 2 (node 1 1 leaf leaf) (node 4 4 leaf (node 5 5 leaf leaf))) 0 5 (λ env → env )
+test-insert1 = replaceTree1 (node 2 2 (node 1 1 leaf leaf) (node 4 4 leaf (node 5 5 leaf leaf))) 0 5 (λ env → env )