Mercurial > hg > Members > Moririn

changeset 600:016a8deed93d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix old binary tree
author ryokka
date Wed, 04 Mar 2020 17:51:05 +0900
parents 7ae0c25d2b58
children 803c423c2855
files hoareBinaryTree.agda
diffstat 1 files changed, 364 insertions(+), 129 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Wed Feb 26 19:00:08 2020 +0900
+++ b/hoareBinaryTree.agda	Wed Mar 04 17:51:05 2020 +0900
@@ -57,73 +57,299 @@
 --  no children , having left node , having right node , having both
 --
 data bt {n : Level} (A : Set n) : Set n where
-  bt-leaf : (key : ℕ) → bt A
-  bt-node : (key : ℕ) →
-    (ltree : bt A) → (rtree : bt A) → bt A
+  L : bt A
+  N :  (key : ℕ) →
+    (ltree : bt A ) → (rtree : bt A ) → bt A
+
+
+-- data bt-path {n : Level} (A : Set n) : Set n where
+--   bt-left  : (key : ℕ) → (bt A )  → bt-path A
+--   bt-right : (key : ℕ) → (bt A ) → bt-path A
+
+data bt-path' {n : Level} (A : Set n) : Set n where
+  left  : (bt A) → bt-path' A
+  right : (bt A) → bt-path' A
+
+
+
+tree->key : {n : Level} {A : Set n} → (tree : bt A) → ℕ
+tree->key {n} L = zero
+tree->key {n} (N key tree tree₁) = key
+
+-- path2tree : {n : Level} {A : Set n} → (bt-path' {n} A) → bt A
+-- path2tree {n} {A} (left x) = x
+-- path2tree {n} {A} (right x) = x
+
+
+-- bt-find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A  ) → List (bt-path A)
+--     → ( bt A → List (bt-path A) → t ) → t
+-- bt-find {n} {m} {A} {t}  key leaf@(L) stack exit = exit leaf stack
+-- bt-find {n} {m} {A} {t}  key (N key₁ tree tree₁) stack next with <-cmp key key₁
+-- bt-find {n} {m} {A} {t}  key node@(N key₁ tree tree₁) stack exit | tri≈ ¬a b ¬c = exit node stack
+-- bt-find {n} {m} {A} {t}  key node@(N key₁ ltree rtree) stack next | tri< a ¬b ¬c = bt-find key ltree (bt-left key node ∷ stack) next
+-- bt-find {n} {m} {A} {t}  key node@(N key₁ ltree rtree) stack next | tri> ¬a ¬b c = bt-find key rtree (bt-right key node ∷ stack) next
+
+
+-- bt-find' : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A  ) → List (bt-path' A) → ( bt A → List (bt-path' A) → t ) → t
+-- bt-find' key leaf@(L) stack exit = exit leaf stack
+-- bt-find' key node@(N key1 lnode rnode) stack exit with <-cmp key key1
+-- bt-find' key node@(N key1 lnode rnode) stack exit | tri≈ ¬a b ¬c = exit node stack
+-- bt-find' key node@(N key1 lnode rnode) stack next | tri< a ¬b ¬c = bt-find' key lnode ((left node) ∷ stack) next
+-- bt-find' key node@(N key1 lnode rnode) stack next | tri> ¬a ¬b c = bt-find' key rnode ((right node) ∷ stack) next
 
 
-data bt-path {n : Level} (A : Set n) : Set n where
-  bt-left  : (key : ℕ) → (bt A )  → bt-path A
-  bt-right : (key : ℕ) → (bt A ) → bt-path A
+-- find-next : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt-path' A)
+--           → (next : bt A → List (bt-path' A) → t ) → (exit : bt A → List (bt-path' A) → t ) → t
+-- find-next key leaf@(L) st _ exit = exit leaf st
+-- find-next key (N key₁ tree tree₁) st next exit with <-cmp key key₁
+-- find-next key node@(N key₁ tree tree₁) st _ exit | tri≈ ¬a b ¬c = exit node st
+-- find-next key node@(N key₁ tree tree₁) st next _ | tri< a ¬b ¬c = next tree ((left node) ∷ st)
+-- find-next key node@(N key₁ tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ ((right node) ∷ st)
+
+-- find-loop は bt-find' とだいたい一緒(induction してるくらい)
+-- これも多分 Zコンビネータの一種?
+-- loop で induction してる hight は現在の木の最大長より大きければよい(find-next が抜けきるため)
+-- 逆に木の最大長より小さい(たどるルートより小さい)場合は途中経過の値が返る
+
+-- find-loop : {n m : Level} {A : Set n} {t : Set m} → (hight key : ℕ) → (tree : bt A ) → List (bt-path' A) → (exit : bt A → List (bt-path' A) → t) → t
+-- find-loop zero key tree st exit = exit tree st
+-- find-loop (suc h) key lf@(L) st exit = exit lf st
+-- find-loop (suc h) key tr@(N key₁ tree tree₁) st exit = find-next key tr st ((λ tr1 st1 → find-loop h key tr1 st1 exit)) exit
+
 
 
-bt-find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A  ) → List (bt-path A)
-    → ( bt A → List (bt-path A) → t ) → t
-bt-find {n} {m} {A} {t}  key leaf@(bt-leaf key₁) stack exit = exit leaf stack
-bt-find {n} {m} {A} {t}  key (bt-node key₁ tree tree₁) stack next with <-cmp key key₁
-bt-find {n} {m} {A} {t}  key node@(bt-node key₁ tree tree₁) stack exit | tri≈ ¬a b ¬c = exit node stack
-bt-find {n} {m} {A} {t}  key node@(bt-node key₁ ltree rtree) stack next | tri< a ¬b ¬c = bt-find key ltree (bt-left key node ∷ stack) next
-bt-find {n} {m} {A} {t}  key node@(bt-node key₁ ltree rtree) stack next | tri> ¬a ¬b c = bt-find key rtree (bt-right key node ∷ stack) next
+node-ex : {n : Level} {A : Set n} → bt A
+node-ex {n} {A} = (N zero (L) (L))
+
+ex : {n : Level} {A : Set n} → bt A
+ex {n} {A} = (N {n} {A} 8 (N 6 (N 2 (N 1 L L) (N 3 L L)) (N 7 L L)) (N 9 L L))
+
+exLR : {n : Level} {A : Set n} → bt A
+exLR {n} {A} = (N {n} {A} 4 (N 2 L (N 3 L L)) (N 5 L L))
+
+exRL : {n : Level} {A : Set n} → bt A
+exRL {n} {A} = (N {n} {A} 3 L (N 5 (N 4 L L) L))
+
+
+
+
+leaf-ex : {n : Level} {A : Set n} → bt A
+leaf-ex {n} {A} = L
+
+
+
+
+
+
+findLoopInv : {n m : Level} {A : Set n} {t : Set m}  →  (orig : bt A) → (modify : bt A )
+  → (stack : List (bt-path' A)) → Set n
+-- findLoopInv {n} {m} {A} {t} tree mtree [] = tree ≡ mtree
+-- findLoopInv {n} {m} {A} {t} tree mtree (left (L) ∷ st) = mtree ≡ (L)
+-- findLoopInv {n} {m} {A} {t} tree mtree (right (L) ∷ st) = mtree ≡ (L)
+findLoopInv {n} {m} {A} {t} tree mtree [] = tree ≡ mtree
+findLoopInv {n} {m} {A} {t} tree mtree (left L ∷ st) = mtree ≡ (L)
+findLoopInv {n} {m} {A} {t} tree mtree (right L ∷ st) = mtree ≡ (L)
+findLoopInv {n} {m} {A} {t} tree mtree (left (N key x x₁) ∷ st) = mtree ≡ x
+findLoopInv {n} {m} {A} {t} tree mtree (right (N key x x₁) ∷ st) = mtree ≡ x₁
+
+
+
+
+
 
 
-bt-replace : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt-path A) → (bt A → t ) → t
-bt-replace {n} {m} {A} {t} ikey otree stack next = bt-replace0 otree where
-    bt-replace1 : bt A → List (bt-path A) → t
-    bt-replace1 tree [] = next tree
-    bt-replace1 node (bt-left key (bt-leaf key₁) ∷ stack) = bt-replace1 node stack
-    bt-replace1 node (bt-right key (bt-leaf key₁) ∷ stack) = bt-replace1 node stack
-    bt-replace1 node (bt-left key (bt-node key₁ x x₁) ∷ stack) = bt-replace1 (bt-node key₁ node x₁) stack
-    bt-replace1 node (bt-right key (bt-node key₁ x x₁) ∷ stack) = bt-replace1 (bt-node key₁ x node) stack
-    bt-replace0 : (tree : bt A) → t
-    bt-replace0 tree@(bt-node key ltr rtr) = bt-replace1 tree stack  -- find case
-    bt-replace0 (bt-leaf key) with <-cmp key ikey -- not-find case
-    bt-replace0 (bt-leaf key) | tri< a ¬b ¬c = bt-replace1 (bt-node ikey (bt-leaf key) (bt-leaf (suc ikey))) stack
-    bt-replace0 (bt-leaf key) | tri≈ ¬a b ¬c = bt-replace1 (bt-node ikey (bt-leaf (pred ikey)) (bt-leaf (suc ikey))) stack
-    bt-replace0 (bt-leaf key) | tri> ¬a ¬b c = bt-replace1 (bt-node ikey (bt-leaf (suc ikey)) (bt-leaf (key))) stack
+
+
+hightMerge : {n m : Level} {A : Set n} {t : Set m} → (l r : ℕ) → (ℕ → t) → t
+hightMerge lh rh next with <-cmp lh rh
+hightMerge lh rh next | tri< a ¬b ¬c = next rh
+hightMerge lh rh next | tri≈ ¬a b ¬c = next lh
+hightMerge lh rh next | tri> ¬a ¬b c = next lh
+
+isHightL : {n m : Level} {A : Set n} {t : Set m} → bt A → (ℕ → t) → t
+isHightL L next = next zero
+isHightL {n} {_} {A} (N key tree tree₁) next = isHightL tree λ x → next (suc x)
+
+isHightR : {n m : Level} {A : Set n} {t : Set m} → bt A → (ℕ → t) → t
+isHightR L next = next zero
+isHightR {n} {_} {A} (N key tree tree₁) next = isHightR tree₁ λ x → next (suc x)
+
+isHight : {n m : Level} {A : Set n} {t : Set m} → bt A → (ℕ → t) → t
+isHight L next = next zero
+isHight {n} {_} {A} tr@(N key tree tree₁) next = isHightL tr (λ lh → isHightR tr λ rh → hightMerge {n} {_} {A} (suc lh) (suc rh) next)
+
 
--- bt-replace1 (bt-node ikey (bt-leaf {!!}) (bt-leaf {!!})) stack -- not-find case
+treeHight : {n m : Level} {A : Set n} {t : Set m} → bt A → (ℕ → t) → t
+treeHight L next = next zero
+treeHight {n} {_} {A} (N key tree tree₁) next = isHight tree (λ lh → isHight tree₁ (λ rh → hightMerge {n} {_} {A} (lh) (rh) next))
+
+rhight : {n : Level} {A : Set n}  → bt A → ℕ
+rhight L = zero
+rhight (N key tree tree₁) with <-cmp (rhight tree) (rhight tree₁)
+rhight (N key tree tree₁) | tri< a ¬b ¬c = suc (rhight tree₁)
+rhight (N key tree tree₁) | tri≈ ¬a b ¬c = suc (rhight tree₁)
+rhight (N key tree tree₁) | tri> ¬a ¬b c = suc (rhight tree)
+
+leaf≠node : {n : Level} {A : Set n} {a : ℕ} {l r : bt A} →  ((N {n} {A} a l r) ≡ L) → ⊥
+leaf≠node ()
+
+leafIsNoHight : {n : Level} {A : Set n} (tree : bt A) → tree ≡ L → (treeHight tree (λ x → x) ≡ 0)
+leafIsNoHight L refl = refl
+
+
+
+hight-tree : {n : Level} {A : Set n} {k : ℕ} {l r : bt A} → ℕ → (tree : bt A) → Set n
+hight-tree zero tree = tree ≡ L
+hight-tree {n} {A} {k} {l} {r} (suc h) tree = tree ≡ (N k l r)
 
 
-bt-insert : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → (bt A → t ) → t
-bt-insert {n} {m} {A} {t} key tree next = bt-find key tree [] (λ tr st → bt-replace key tr st (λ new → next new))
+hightIsNotLeaf : {n : Level} {A : Set n} (h : ℕ) → (tree : bt A) → (h ≡ 0 ) ∧ (h ≡ treeHight tree (λ x → x)) →  (tree ≡ L)
+hightIsNotLeaf .0 tree record { proj1 = refl ; proj2 = p2 } = {!!}
+
+-- leaf≡0 : {n : Level} {A : Set n} (tree : bt A) → (rhight tree ≡ 0) → tree ≡ L
+-- leaf≡0 L _ = refl
+
+
+
+
+
+
+
 
 
-tree->key : {n : Level} {A : Set n} → (tree : bt A ) → ℕ
-tree->key {n} (bt-leaf key) = key
-tree->key {n} (bt-node key tree tree₁) = key
+find-hoare-next : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree mt : bt A ) → (st : List (bt-path' A)) → (findLoopInv {n} {m} {A} {t} tree mt st)
+  → (next : (nt : bt A) → (ns : List (bt-path' A)) → (findLoopInv {n} {m} {A} {t} tree nt ns) → t )
+  → (exit : (nt : bt A) → (ns : List (bt-path' A)) → (nt ≡ L) ∨ (key ≡ tree->key nt) → t ) → t
+find-hoare-next key leaf@(L) mt st eq _ exit = exit leaf st (case1 refl)
+find-hoare-next key (N key₁ tree tree₁) mt st eq next exit with <-cmp key key₁
+find-hoare-next key node@(N key₁ tree tree₁) mt st eq _ exit | tri≈ ¬a b ¬c = exit node st (case2 b)
+find-hoare-next key node@(N key₁ tree tree₁) mt st eq next _ | tri< a ¬b ¬c = next tree ((left node) ∷ st) refl
+find-hoare-next key node@(N key₁ tree tree₁) mt st eq next _ | tri> ¬a ¬b c = next tree₁ ((right node) ∷ st) refl
+
+find-hoare-loop : {n m : Level} {A : Set n} {t : Set m} → (hight key : ℕ) → (tree mt : bt A ) → (st : List (bt-path' A)) → (findLoopInv {n} {m} {A} {t} tree mt st)
+  → (exit : (nt : bt A) → (ns : List (bt-path' A)) →  (nt ≡ L) ∨ (key ≡ tree->key nt) → t) → t
+find-hoare-loop zero key tree mt st eq exit with key ≟ (tree->key tree)
+find-hoare-loop zero key tree mt st eq exit | yes p = exit tree st (case2 p)
+find-hoare-loop zero key tree mt st eq exit | no ¬p = exit tree st (case1 {!!})
+
+find-hoare-loop (suc h) key otr lf@(L) st eq exit = exit lf st (case1 refl)
+find-hoare-loop (suc h) key otr tr@(N key₁ tree tree₁) st eq exit = find-hoare-next key otr tr st {!!} ((λ tr1 st1 eq → find-hoare-loop h key otr tr1 st1 {!!} exit)) exit
+
+
+-- bt-replace : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt-path A) → (bt A → t ) → t
+-- bt-replace {n} {m} {A} {t} ikey otree stack next = bt-replace0 otree where
+--     bt-replace1 : bt A → List (bt-path A) → t
+--     bt-replace1 tree [] = next tree
+--     bt-replace1 node (bt-left key (L) ∷ stack) = bt-replace1 node stack
+--     bt-replace1 node (bt-right key (L) ∷ stack) = bt-replace1 node stack
+--     bt-replace1 node (bt-left key (N key₁ x x₁) ∷ stack) = bt-replace1 (N key₁ node x₁) stack
+--     bt-replace1 node (bt-right key (N key₁ x x₁) ∷ stack) = bt-replace1 (N key₁ x node) stack
+--     bt-replace0 : (tree : bt A) → t
+--     bt-replace0 tree@(N key ltr rtr) = bt-replace1 tree stack  -- find case
+--     bt-replace0 (L) = {!!}
+
+
+
+-- bt-insert : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → (bt A → t ) → t
+-- bt-insert {n} {m} {A} {t} key tree next = bt-find key tree [] (λ tr st → bt-replace key tr st (λ new → next new))
+
 
 {--
-find でステップ毎にみている node と stack の top を一致させる
-find 中はnode と stack の top が一致する(root に来た時 stack top がなくなる)
--- どうやって経路の入ったstackを手に入れるか?(find 実行後でよい?)
+[ok] find でステップ毎にみている node と stack の top を一致させる
+[ok] find 中はnode と stack の top が一致する(pre は stack の中身がなく, post は stack の top とずれる)
+
 tree+stack≡tree は find 後の tree と stack をもって
 reverse した stack を使って find をチェックするかんじ?
 --}
 
+{--
+tree+stack は tree と stack を受け取ってひとしさ(関係)を返すやつ
 
-tree+stack : {n m : Level} {A : Set n} {t : Set m} →  (tree mtree : bt A )
-  → (stack : List (bt-path A)) → Set n
-tree+stack tree mtree [] = tree ≡ mtree -- fin case
-tree+stack {n} {m} {A} {t} tree mtree@(bt-leaf key1) (bt-left key x ∷ stack) = (mtree ≡ x) -- unknow case
-tree+stack {n} {m} {A} {t} tree mtree@(bt-leaf key₁) (bt-right key x ∷ stack) = (mtree ≡ x) -- we nofound leaf's left, right node
-tree+stack {n} {m} {A} {t} tree mtree@(bt-node key1 ltree rtree) (bt-left key x ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} tree ltree stack) -- correct case
-tree+stack {n} {m} {A} {t} tree mtree@(bt-node key₁ ltree rtree) (bt-right key x ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} tree rtree stack)
+--}
+
+-- tree+stack : {n m : Level} {A : Set n} {t : Set m} →  (tree mtree : bt A )
+--   → (stack : List (bt-path A)) → Set n
+-- tree+stack tree mtree [] = tree ≡ mtree -- fin case
+-- tree+stack {n} {m} {A} {t} tree mtree@(L) (bt-left key x ∷ stack) = (mtree ≡ x) -- unknow case
+-- tree+stack {n} {m} {A} {t} tree mtree@(L) (bt-right key x ∷ stack) = (mtree ≡ x) -- we nofound leaf's left, right node
+-- tree+stack {n} {m} {A} {t} tree mtree@(N key1 ltree rtree) (bt-left key x ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} tree ltree stack) -- correct case
+-- tree+stack {n} {m} {A} {t} tree mtree@(N key₁ ltree rtree) (bt-right key x ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} tree rtree stack)
+
+{--
+tree+stack
+  2. find loop  → "top of reverse stack" ≡ "find route orig tree"
+--}
+
+-- s+t≡t : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt-path' {n} A)) → bt-find' key tree stack (λ mt st → s+t {n} {A} tree mt st)
+-- s+t≡t {n} {m} {A} {t} key (L) [] = refl
+-- s+t≡t {n} {m} {A} {t} key (L) (left x ∷ []) = refl
+-- s+t≡t {n} {m} {A} {t} key (L) (left x ∷ x₁ ∷ stack) = refl
+-- s+t≡t {n} {m} {A} {t} key (L) (right x ∷ []) = refl
+-- s+t≡t {n} {m} {A} {t} key (L) (right x ∷ x₁ ∷ stack) = refl
+-- s+t≡t {n} {m} {A} {t} key (N key₁ tree tree₁) [] with <-cmp  key key₁
+-- s+t≡t {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri≈ ¬a b ¬c = refl
+-- s+t≡t {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri< a ¬b ¬c = {!!}
+-- s+t≡t {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri> ¬a ¬b c = {!!}
+-- s+t≡t {n} {m} {A} {t} key (N key₁ tree tree₁) (x ∷ stack) = {!!}
+
 
 
-tree+stack≡tree : {n m : Level} {A : Set n} {t : Set m} →  (tree mtree : bt A  )
-  → (stack : List (bt-path A )) → tree+stack {_} {m} {_} {t} tree mtree (reverse stack)
-tree+stack≡tree tree (bt-leaf key) stack = {!!}
-tree+stack≡tree tree (bt-node key rtree ltree) stack = {!!}
+-- s+t : {n : Level} {A : Set n} →  (tree mtree : bt A ) → (stack : List (bt-path' {n} A)) → Set n
+-- s+t tree mtree [] = tree ≡ mtree
+-- s+t tree mtree (x ∷ []) = tree ≡ mtree
+-- s+t tr@(L) mt (left x ∷ x₁ ∷ stack) = tr ≡ mt
+-- s+t {n} {A} tr@(N key tree tree₁) mt (left x ∷ x₁ ∷ stack) = (mt ≡ x) ∧ (s+t {n} {A} tree (path2tree x₁) stack)
+-- s+t tr@(L) mt (right x ∷ x₁ ∷ stack) = tr ≡ mt
+-- s+t {n} {A} tr@(N key tree tree₁) mt (right x ∷ x₁ ∷ stack) = (mt ≡ x) ∧ (s+t {n} {A} tree₁ (path2tree x₁) stack)
+
+-- data treeType {n : Level} (A : Set n) : Set n where
+--   leaf-t : treeType A
+--   node-t : treeType A
+
+-- isType : {n : Level} {A : Set n} → bt A → treeType A
+-- isType (L) = leaf-t
+-- isType (N key tree tree₁) = node-t
+
+-- data findState : Set where
+--   s1 : findState
+--   s2 : findState
+--   sf : findState
+
+-- findStateP : {n : Level} {A : Set n} → findState → ℕ → bt A → (mnode : bt A) → List (bt-path' A) → Set n
+-- findStateP s1 key node mnode stack = stack ≡ []
+-- findStateP s2 key node mnode stack = (s+t node mnode (reverse stack))
+-- findStateP sf key node mnode stack = (key ≡ (tree->key mnode)) ∨ ((isType mnode) ≡ leaf-t)
+
+-- findStartPwP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree mtree : bt A ) → (findStateP s1 key tree mtree [] → t) → t
+-- findStartPwP key tree mtree next = next refl
+
+
+
+-- findLoopPwP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree mtree : bt A ) → (st : List (bt-path' A))
+--   → (findStateP s2 key tree mtree st)
+--   → (next : (tr : bt A) → (st : List (bt-path' A)) → (findStateP s2 key tree mtree st) → t)
+--   → (exit : (tr : bt A) → (st : List (bt-path' A)) → (findStateP sf key tree mtree st) → t ) → t
+-- findLoopPwP key tree (L) [] state next exit = exit tree [] (case2 refl)
+-- findLoopPwP key tree (N key₁ mtree mtree₁) [] state next exit = next tree [] {!!}
+-- findLoopPwP key tree mtree (x ∷ []) state next exit = {!!}
+-- findLoopPwP key tree (L) (x ∷ x₁ ∷ stack) state next exit = {!!}
+-- findLoopPwP key tree (N key₁ mtree mtree₁) (left x ∷ x₁ ∷ stack) state next exit =
+--             next {!!} {!!} {!!}
+-- findLoopPwP key tree (N key₁ mtree mtree₁) (right x ∷ x₁ ∷ stack) state next exit = {!!}
+
+
+-- -- tree+stack' {n} {m} {A} {t} (N key ltree rtree) mtree@(N key₁ lmtree rmtree) (x ∷ stack)  with <-cmp key key₁
+-- tree+stack' {n} {m} {A} {t} tt@(N key ltree rtree) mt@(N key₁ lmtree rmtree) (x ∷ stack)  | tri≈ ¬a b ¬c = tt ≡ mt
+-- tree+stack' {n} {m} {A} {t} tt@(N key ltree rtree) mt@(N key₁ lmtree rmtree) st@(x ∷ stack)  | tri< a ¬b ¬c = (mt ≡ x) ∧ tree+stack' {n} {m} {A} {t} tt lmtree (mt ∷ st)
+-- tree+stack' {n} {m} {A} {t} tt@(N key ltree rtree) mt@(N key₁ lmtree rmtree) st@(x ∷ stack)  | tri> ¬a ¬b c = (mt ≡ x) ∧ tree+stack' {n} {m} {A} {t} tt rmtree (mt ∷ st)
+
+
+
+-- tree+stack≡tree : {n m : Level} {A : Set n} {t : Set m} →  (tree mtree : bt A  )
+--   → (stack : List (bt-path A )) → tree+stack {_} {m} {_} {t} tree mtree (reverse stack)
+-- tree+stack≡tree tree (L key) stack = {!!}
+-- tree+stack≡tree tree (N key rtree ltree) stack = {!!}
+
 
 
 -- loop はきっと start, running, stop の3つに分けて考えるといいよね
@@ -135,44 +361,53 @@
     or "stack Not empty ∧ current node key ≡ find-key"
 --}
 
-find-step : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A  ) → (stack : List (bt-path A))
-  → (next : bt A → List (bt-path A) → (¬ (stack ≡ [])) ∧ (tree ≡ bt-leaf key) → t)
-  → (next : bt A → List (bt-path A)
-    → ((¬ (stack ≡ [])) ∧ (tree ≡ bt-leaf key)
-      ∨ (¬ (stack ≡ [])) ∧ (key ≡ (tree->key tree)) )→ t) → t
-find-step {n} {m} {A} {t} key node stack next exit = {!!}
+-- find-step : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A) → (stack : List (bt A))
+--   → (next : (mtree : bt A) → (stack1 : List (bt A)) → (tree+stack' {n} {m} {A} {t} tree mtree stack1 ) → t)
+--   → (exit : (mtree : bt A) → List (bt A) → (tree ≡ L (tree->key mtree )) ∨ (key ≡ (tree->key mtree)) → t) → t
+-- find-step {n} {m} {A} {t} key (L) stack next exit = exit (L) stack (case1 refl)
+-- find-step {n} {m} {A} {t} key (N key₁ node node₁) stack next exit with <-cmp key key₁
+-- find-step {n} {m} {A} {t} key (N key₁ node node₁) stack next exit | tri≈ ¬a b ¬c = exit (N key₁ node node₁) stack (case2 b)
+-- find-step {n} {m} {A} {t} key (N key₁ node node₁) stack next exit | tri< a ¬b ¬c = next node stack {!!}
+-- find-step {n} {m} {A} {t} key (N key₁ node node₁) stack next exit | tri> ¬a ¬b c = next node₁ stack {!!}
+
+
+-- find-check : {n m : Level} {A : Set n} {t : Set m} → (k : ℕ) → (tree : bt A  )
+--   → (stack : List (bt-path A )) → bt-find k tree [] (λ mtree mstack → tree+stack {_} {m} {_} {t} tree mtree (reverse mstack))
+-- find-check {n} {m} {A} {t} key (L) [] = refl
+-- find-check {n} {m} {A} {t} key (N key₁ tree tree₁) [] with <-cmp key key₁
+-- find-check {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri≈ ¬a b ¬c = refl
+-- find-check {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri< a ¬b ¬c = {!!}
+-- find-check {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri> ¬a ¬b c = {!!}
+-- find-check {n} {m} {A} {t} key tree (x ∷ stack) = {!!}
 
 
-find-check : {n m : Level} {A : Set n} {t : Set m} → (k : ℕ) → (tree : bt A  )
-  → (stack : List (bt-path A )) → bt-find k tree [] (λ mtree mstack → tree+stack {_} {m} {_} {t} tree mtree (reverse mstack))
-find-check {n} {m} {A} {t} key (bt-leaf key₁) [] = refl
-find-check {n} {m} {A} {t} key (bt-node key₁ tree tree₁) [] with <-cmp key key₁
-find-check {n} {m} {A} {t} key (bt-node key₁ tree tree₁) [] | tri≈ ¬a b ¬c = refl
-find-check {n} {m} {A} {t} key (bt-node key₁ tree tree₁) [] | tri< a ¬b ¬c = {!!}
-find-check {n} {m} {A} {t} key (bt-node key₁ tree tree₁) [] | tri> ¬a ¬b c = {!!}
-find-check {n} {m} {A} {t} key tree (x ∷ stack) = {!!}
+-- module ts where
+--     tbt : {n : Level} {A : Set n} → bt A
+--     tbt {n} {A} = N {n} {A} 8 (N 6 (N 2 (L) (L)) (L)) (L)
 
+--     find : {n : Level} {A : Set n} → ℕ → List (bt-path A)
+--     find {n} {A} key = bt-find key tbt [] (λ x y → y )
+
+--     find' : {n : Level} {A : Set n} → ℕ → bt A
+--     find' {n} {A} key = bt-find' key tbt [] (λ x y → x )
 
-module ts where
-    tbt : {n : Level} {A : Set n} → bt A
-    tbt {n} {A} = bt-node {n} {A} 8 (bt-node 6 (bt-node 2 (bt-leaf 1) (bt-leaf 3)) (bt-leaf 7)) (bt-leaf 9)
-
-    find : {n : Level} {A : Set n} → ℕ → List (bt-path A)
-    find {n} {A} key = bt-find key tbt [] (λ x y → y )
+--     rep : {n m : Level} {A : Set n} {t : Set m} → ℕ → bt A
+--     rep {n} {m} {A} {t} key = bt-find {n} {_} {A} key tbt [] (λ tr st → bt-replace key tr st (λ mtr → mtr))
 
-    rep : {n m : Level} {A : Set n} {t : Set m} → ℕ → bt A
-    rep {n} {m} {A} {t} key = bt-find {n} {_} {A} key tbt [] (λ tr st → bt-replace key tr st (λ mtr → mtr))
+--     ins : {n m : Level} {A : Set n} {t : Set m} → ℕ → bt A
+--     ins {n} {m} {A} {t} key = bt-insert key tbt (λ tr → tr)
 
-    ins : {n m : Level} {A : Set n} {t : Set m} → ℕ → bt A
-    ins {n} {m} {A} {t} key = bt-insert key tbt (λ tr → tr)
---
+--     test : {n m : Level} {A : Set n} {t : Set m} (key : ℕ)
+--       → bt-find {n} {_} {A} {_} key tbt [] (λ x y → tree+stack {n} {m} {A} {t} tbt x y)
+--     test key = {!!}
+-- --
 --
 --  no children , having left node , having right node , having both
 --
--- data bt' {n : Level} { l r : ℕ } (A : Set n) : (key : ℕ) →  Set n where --  (a : Setn)
---   bt'-leaf : (key : ℕ) → bt' A key
---   bt'-node : { l r : ℕ } → (key : ℕ) → (value : A) →
---              bt' {n} {{!!}} {{!!}} A l  → bt' {n} {{!!}} {{!!}} A r → l ≤ key → key ≤ r → bt' A key
+data bt' {n : Level} (A : Set n) : (key : ℕ) →  Set n where --  (a : Setn)
+  bt'-leaf : (key : ℕ) → bt' A key
+  bt'-node : { l r : ℕ } → (key : ℕ) → (value : A) →
+             bt' A l  → bt' A r → l ≤ key → key ≤ r → bt' A key
 
 -- data bt'-path {n : Level} (A : Set n) : ℕ → Set n where --  (a : Setn)
 --   bt'-left  : (key : ℕ) → {left-key : ℕ} → (bt' A left-key ) → (key ≤ left-key)  → bt'-path A left-key
@@ -184,7 +419,7 @@
 
 
 -- reverse1 :  List (bt' A tn) → List (bt' A tn) → List (bt' A tn)
--- reverse1 [] s1 = s1
+-- reverse1 [] s1 = s1+
 -- reverse1 (x ∷ s0) s1 with reverse1 s0 (x ∷ s1)
 -- ... | as = {!!}
 
@@ -262,7 +497,7 @@
 
 
 -- lleaf : {n : Level} {a : Set n} → bt {n} {a} 
--- lleaf = (bt-leaf ⦃ 0 ⦄ ⦃ 3 ⦄ z≤n)
+-- lleaf = (L ⦃ 0 ⦄ ⦃ 3 ⦄ z≤n)
 
 -- lleaf1 : {n : Level} {A : Set n} → (0 < 3)  → (a : A) → (d : ℕ ) → bt' {n} A d
 -- lleaf1 0<3 a d = bt'-leaf d
@@ -272,10 +507,10 @@
 
 
 -- rleaf : {n : Level} {a : Set n} → bt {n} {a} 
--- rleaf = (bt-leaf ⦃ 3 ⦄ ⦃ 3 ⦄ (s≤s (s≤s (s≤s z≤n))))
+-- rleaf = (L ⦃ 3 ⦄ ⦃ 3 ⦄ (s≤s (s≤s (s≤s z≤n))))
 
 -- test-node : {n : Level} {a : Set n} → bt {n} {a} 
--- test-node {n} {a} = (bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ 4 ⦄ ⦃ 4 ⦄ 3 lleaf rleaf z≤n ≤-refl )
+-- test-node {n} {a} = (N ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ 4 ⦄ ⦃ 4 ⦄ 3 lleaf rleaf z≤n ≤-refl )
 
 -- -- stt : {n m : Level} {a : Set n} {t : Set m} → {!!}
 -- -- stt {n} {m} {a} {t} = pushSingleLinkedStack  [] (test-node ) (λ st → pushSingleLinkedStack st lleaf (λ st2 → st2) )
@@ -285,15 +520,15 @@
 -- -- search の {{ l }} {{ u }} はその時みている node の 大小。 l が小さく u が大きい
 -- -- ここでは d が現在の node のkey値なので比較後のsearch では値が変わる
 -- bt-search : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → bt {n} {a} → (Maybe (Σ ℕ (λ d' → _iso_  {n} {a} d d')) → t ) → t
--- bt-search {n} {m} {a} {t} key (bt-leaf x) cg = cg nothing
--- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg with <-cmp key d
--- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri< a₁ ¬b ¬c =  bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg
--- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c))
--- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg
+-- bt-search {n} {m} {a} {t} key (L x) cg = cg nothing
+-- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg with <-cmp key d
+-- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri< a₁ ¬b ¬c =  bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg
+-- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c))
+-- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg
 
--- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri< a₁ ¬b ¬c = ? -- bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg
--- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d L R x x₁) cg | tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c))
--- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg
+-- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri< a₁ ¬b ¬c = ? -- bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg
+-- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N d L R x x₁) cg | tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c))
+-- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg
 
 
 -- -- この辺の test を書くときは型を考えるのがやや面倒なので先に動作を書いてから型を ? から補間するとよさそう
@@ -309,25 +544,25 @@
 -- -- up-some nothing = nothing
 
 -- search-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (key : ℕ) → (tree : bt {n} {a} ) → bt-search ⦃ l ⦄ ⦃ u ⦄ key tree (λ gdata → gdata ≡ gdata)
--- search-lem {n} {m} {a} {t} key (bt-leaf x) = refl
--- search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) with <-cmp key d
--- search-lem {n} {m} {a} {t} key (bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri< lt ¬eq ¬gt = search-lem {n} {m} {a} {t} ⦃ ll' ⦄ ⦃ d ⦄  key tree₁
--- search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) | tri≈ ¬lt eq ¬gt = refl
--- search-lem {n} {m} {a} {t} key (bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri> ¬lt ¬eq gt = search-lem {n} {m} {a} {t} ⦃ d ⦄ ⦃ lr' ⦄  key tree₂
+-- search-lem {n} {m} {a} {t} key (L x) = refl
+-- search-lem {n} {m} {a} {t} key (N d tree₁ tree₂ x x₁) with <-cmp key d
+-- search-lem {n} {m} {a} {t} key (N ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri< lt ¬eq ¬gt = search-lem {n} {m} {a} {t} ⦃ ll' ⦄ ⦃ d ⦄  key tree₁
+-- search-lem {n} {m} {a} {t} key (N d tree₁ tree₂ x x₁) | tri≈ ¬lt eq ¬gt = refl
+-- search-lem {n} {m} {a} {t} key (N ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri> ¬lt ¬eq gt = search-lem {n} {m} {a} {t} ⦃ d ⦄ ⦃ lr' ⦄  key tree₂
 
 
 -- -- bt-find 
 -- 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
 
--- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key leaf@(bt-leaf x) st cg = cg leaf st nothing
--- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d tree₁ tree₂ x x₁) st cg with <-cmp key d
--- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt-node d tree₁ tree₂ x x₁) st cg | tri≈ ¬a b ¬c = cg node st (just (d , iso-intro {n} {a} ¬a ¬c))
+-- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key leaf@(L x) st cg = cg leaf st nothing
+-- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N d tree₁ tree₂ x x₁) st cg with <-cmp key d
+-- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(N d tree₁ tree₂ x x₁) st cg | tri≈ ¬a b ¬c = cg node st (just (d , iso-intro {n} {a} ¬a ¬c))
 
--- find-support {n} {m} {a} {t}  key node@(bt-node ⦃ nl ⦄ ⦃ l' ⦄ ⦃ nu ⦄ ⦃ u' ⦄ d L R x x₁) st cg | tri< a₁ ¬b ¬c =
+-- find-support {n} {m} {a} {t}  key node@(N ⦃ nl ⦄ ⦃ l' ⦄ ⦃ nu ⦄ ⦃ u' ⦄ d L R x x₁) st cg | tri< a₁ ¬b ¬c =
 --                          pushSingleLinkedStack st node
 --                          (λ st2 → find-support {n} {m} {a} {t} {{l'}} {{d}} key L st2 cg)
 
--- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d L R x x₁) st cg | tri> ¬a ¬b c = pushSingleLinkedStack st node
+-- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(N ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d L R x x₁) st cg | tri> ¬a ¬b c = pushSingleLinkedStack st node
 --                          (λ st2 → find-support {n} {m} {a} {t} {{d}} {{lr'}} key R st2 cg)
 
 -- bt-find : {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
@@ -338,24 +573,24 @@
 -- find-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-find {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 3 test-node [] (λ tt st ad → st)
 -- {-- result
 --     λ {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ →
---     bt-node 3 (bt-leaf z≤n) (bt-leaf (s≤s (s≤s (s≤s z≤n)))) z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) ∷ []
+--     N 3 (L z≤n) (L (s≤s (s≤s (s≤s z≤n)))) z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) ∷ []
 -- --}
 
 -- find-lem : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → (d : ℕ) → (tree : bt {n} {a}) → (st : List (bt {n} {a})) → find-support {{l}} {{u}} d tree st (λ ta st ad → ta ≡ ta)
--- find-lem d (bt-leaf x) st = refl
--- find-lem d (bt-node d₁ tree tree₁ x x₁) st with <-cmp d d₁
--- find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri≈ ¬a b ¬c = refl
+-- find-lem d (L x) st = refl
+-- find-lem d (N d₁ tree tree₁ x x₁) st with <-cmp d d₁
+-- find-lem d (N d₁ tree tree₁ x x₁) st | tri≈ ¬a b ¬c = refl
 
 
--- find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c with  tri< a ¬b ¬c
--- find-lem {n} {m} {a} {t} {{l}} {{u}} d (bt-node d₁ tree tree₁ x x₁) st | tri< lt ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = find-lem {n} {m} {a} {t} {{l}} {{u}} d tree {!!}
--- find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = {!!}
--- find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = {!!}
+-- find-lem d (N d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c with  tri< a ¬b ¬c
+-- find-lem {n} {m} {a} {t} {{l}} {{u}} d (N d₁ tree tree₁ x x₁) st | tri< lt ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = find-lem {n} {m} {a} {t} {{l}} {{u}} d tree {!!}
+-- find-lem d (N d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = {!!}
+-- find-lem d (N d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = {!!}
 
--- find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri> ¬a ¬b c = {!!}
+-- find-lem d (N d₁ tree tree₁ x x₁) st | tri> ¬a ¬b c = {!!}
 
 -- bt-singleton :{n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → (d : ℕ) → ( (bt {n} {a} ) → t ) → t
--- bt-singleton {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d cg = cg (bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (bt-leaf ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (bt-leaf  ⦃ d ⦄  ⦃ d ⦄ ≤-refl) z≤n ≤-refl)
+-- bt-singleton {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d cg = cg (N ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (L ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (L  ⦃ d ⦄  ⦃ d ⦄ ≤-refl) z≤n ≤-refl)
 
 
 -- singleton-test : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → bt -- ?
@@ -364,11 +599,11 @@
 
 -- replace-helper : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → t ) → t
 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree [] cg = cg tree
--- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree@(bt-node d L R x₁ x₂) (bt-leaf x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg  -- Unknown Case
--- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ (bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg with <-cmp d d₁
--- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg | tri< a₁ ¬b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ subt x₃ x₄ x₅) st cg
--- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg | tri≈ ¬a b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ subt x₃ x₄ x₅) st cg
--- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg | tri> ¬a ¬b c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ x₃ subt x₄ x₅) st cg
+-- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree@(N d L R x₁ x₂) (L x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg  -- Unknown Case
+-- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ (N d tree tree₁ x₁ x₂) (N d₁ x x₃ x₄ x₅ ∷ st) cg with <-cmp d d₁
+-- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(N d tree tree₁ x₁ x₂) (N d₁ x x₃ x₄ x₅ ∷ st) cg | tri< a₁ ¬b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (N d₁ subt x₃ x₄ x₅) st cg
+-- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(N d tree tree₁ x₁ x₂) (N d₁ x x₃ x₄ x₅ ∷ st) cg | tri≈ ¬a b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (N d₁ subt x₃ x₄ x₅) st cg
+-- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(N d tree tree₁ x₁ x₂) (N d₁ x x₃ x₄ x₅ ∷ st) cg | tri> ¬a ¬b c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (N d₁ x₃ subt x₄ x₅) st cg
 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree (x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg  -- Unknown Case
 
 
@@ -376,7 +611,7 @@
 -- bt-replace : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄
 --            → (d : ℕ) → (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} )
 --            → Maybe (Σ ℕ (λ d' → _iso_  {n} {a} d d')) → ( (bt {n} {a} ) → t ) → t
--- bt-replace {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d tree st eqP cg = replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ ((bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (bt-leaf ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (bt-leaf  ⦃ d ⦄  ⦃ d ⦄ ≤-refl) z≤n ≤-refl)) st cg
+-- bt-replace {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d tree st eqP cg = replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ ((N ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (L ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (L  ⦃ d ⦄  ⦃ d ⦄ ≤-refl) z≤n ≤-refl)) st cg
 
 
 
@@ -387,8 +622,8 @@
 -- bt-insert {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d tree cg = bt-find {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ d tree [] (λ tt st ad → bt-replace ⦃ l ⦄ ⦃ u ⦄ d tt st ad cg )
 
 -- pickKey : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (tree : bt {n} {a}) → Maybe ℕ
--- pickKey (bt-leaf x) = nothing
--- pickKey (bt-node d tree tree₁ x x₁) = just d
+-- pickKey (L x) = nothing
+-- pickKey (N d tree tree₁ x x₁) = just d
 
 -- insert-test : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → bt -- ?
 -- insert-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄  = bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 1 test-node λ x → x
@@ -402,21 +637,21 @@
 --              (λ tt st ad → (pickKey {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tt)  ≡ just d ) )
 
 
--- insert-lem d (bt-leaf x) with <-cmp d d -- bt-insert d (bt-leaf x) (λ tree1 → {!!})
--- insert-lem d (bt-leaf x) | tri< a ¬b ¬c = ⊥-elim (¬b refl)
--- insert-lem d (bt-leaf x) | tri≈ ¬a b ¬c = refl
--- insert-lem d (bt-leaf x) | tri> ¬a ¬b c = ⊥-elim (¬b refl)
--- insert-lem d (bt-node d₁ tree tree₁ x x₁) with <-cmp d d₁
---  -- bt-insert d (bt-node d₁ tree tree₁ x x₁) (λ tree1 → {!!})
--- insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c with <-cmp d d
--- insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl)
--- insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl
--- insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl)
+-- insert-lem d (L x) with <-cmp d d -- bt-insert d (L x) (λ tree1 → {!!})
+-- insert-lem d (L x) | tri< a ¬b ¬c = ⊥-elim (¬b refl)
+-- insert-lem d (L x) | tri≈ ¬a b ¬c = refl
+-- insert-lem d (L x) | tri> ¬a ¬b c = ⊥-elim (¬b refl)
+-- insert-lem d (N d₁ tree tree₁ x x₁) with <-cmp d d₁
+--  -- bt-insert d (N d₁ tree tree₁ x x₁) (λ tree1 → {!!})
+-- insert-lem d (N d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c with <-cmp d d
+-- insert-lem d (N d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl)
+-- insert-lem d (N d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl
+-- insert-lem d (N d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl)
 
--- insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri< a ¬b ¬c = {!!}
+-- insert-lem d (N d₁ tree tree₁ x x₁) | tri< a ¬b ¬c = {!!}
 --   where
---     lem-helper : find-support ⦃ {!!} ⦄ ⦃ {!!} ⦄ d tree (bt-node d₁ tree tree₁ x x₁ ∷ [])  (λ tt₁ st ad → replace-helper ⦃ {!!} ⦄ ⦃ {!!} ⦄  (bt-node ⦃ {!!} ⦄ ⦃ {!!} ⦄ ⦃ {!!} ⦄ ⦃ {!!} ⦄  d (bt-leaf ⦃ 0 ⦄ ⦃ d ⦄ z≤n) (bt-leaf ⦃ {!!} ⦄ ⦃ {!!} ⦄  (≤-reflexive refl)) z≤n   (≤-reflexive refl))   st  (λ tree1 →   find-support ⦃ {!!} ⦄ ⦃ {!!} ⦄  d tree1 [] (λ tt₂ st₁ ad₁ → pickKey {{!!}} {{!!}} {{!!}} {{!!}} ⦃ {!!} ⦄ ⦃ {!!} ⦄  tt₂ ≡ just d)))
+--     lem-helper : find-support ⦃ {!!} ⦄ ⦃ {!!} ⦄ d tree (N d₁ tree tree₁ x x₁ ∷ [])  (λ tt₁ st ad → replace-helper ⦃ {!!} ⦄ ⦃ {!!} ⦄  (N ⦃ {!!} ⦄ ⦃ {!!} ⦄ ⦃ {!!} ⦄ ⦃ {!!} ⦄  d (L ⦃ 0 ⦄ ⦃ d ⦄ z≤n) (L ⦃ {!!} ⦄ ⦃ {!!} ⦄  (≤-reflexive refl)) z≤n   (≤-reflexive refl))   st  (λ tree1 →   find-support ⦃ {!!} ⦄ ⦃ {!!} ⦄  d tree1 [] (λ tt₂ st₁ ad₁ → pickKey {{!!}} {{!!}} {{!!}} {{!!}} ⦃ {!!} ⦄ ⦃ {!!} ⦄  tt₂ ≡ just d)))
 --     lem-helper = {!!}
 
--- insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri> ¬a ¬b c = {!!}
+-- insert-lem d (N d₁ tree tree₁ x x₁) | tri> ¬a ¬b c = {!!}