view hoareBinaryTree.agda @ 603:41e1c9e9718d

add fig
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 02 Nov 2021 19:32:10 +0900 (2021-11-02)
parents 803c423c2855
children 2075785a124a
line wrap: on
line source
module hoareBinaryTree where

open import Level renaming (zero to Z ; suc to succ)

open import Data.Nat hiding (compare)
open import Data.Nat.Properties as NatProp
open import Data.Maybe
-- open import Data.Maybe.Properties
open import Data.Empty
open import Data.List
open import Data.Product

open import Function as F hiding (const)

open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import logic


SingleLinkedStack = List

emptySingleLinkedStack :  {n : Level } {Data : Set n} -> SingleLinkedStack Data
emptySingleLinkedStack = []

clearSingleLinkedStack : {n m : Level } {Data : Set n} {t : Set m} -> SingleLinkedStack Data  → ( SingleLinkedStack Data → t) → t
clearSingleLinkedStack [] cg = cg []
clearSingleLinkedStack (x ∷ as) cg = cg []

pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> List Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
pushSingleLinkedStack stack datum next = next ( datum ∷ stack )


popSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
popSingleLinkedStack [] cs = cs [] nothing
popSingleLinkedStack (data1 ∷ s)  cs = cs s (just data1)



emptySigmaStack : {n : Level } { Data : Set n} → List Data
emptySigmaStack = []

pushSigmaStack : {n m : Level} {d d2 : Set n} {t : Set m} → d2 → List d  → (List (d × d2) → t) → t
pushSigmaStack {n} {m} {d} d2 st next = next (Data.List.zip (st) (d2 ∷ []) )

tt = pushSigmaStack 3 (true ∷ []) (λ st → st)

_iso_ : {n : Level} {a : Set n} → ℕ → ℕ → Set
d iso d' = (¬ (suc d ≤ d')) ∧ (¬ (suc d' ≤ d))

iso-intro : {n : Level} {a : Set n} {x y : ℕ} → ¬ (suc x ≤ y) → ¬ (suc y ≤ x) → _iso_ {n} {a} x y
iso-intro = λ z z₁ → record { proj1 = z ; proj2 = z₁ }


--
--
--  no children , having left node , having right node , having both
--
data bt {n : Level} (A : Set n) : Set n where
  L : bt A
  N :  (key : ℕ) →
    (ltree : bt A ) → (rtree : bt A ) → bt 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

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 (left (N key x x₁) ∷ st) = mtree ≡ x
findLoopInv {n} {m} {A} {t} tree mtree (right (N key x x₁) ∷ st) = mtree ≡ x₁


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)

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)


hightIsNotLeaf : {n : Level} {A : Set n} (h : ℕ) → (tree : bt A) → (0 ≡ treeHight tree (λ x → x)) →  (tree ≡ L)
hightIsNotLeaf h tree eq = {!!}

-- leaf≡0 : {n : Level} {A : Set n} (tree : bt A) → (rhight tree ≡ 0) → tree ≡ L
-- leaf≡0 L _ = refl

-- find-function sepalate "next", "loop"
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 eq ((λ tr1 st1 eq → find-hoare-loop h key otr tr1 st1 eq 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@(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


-- 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-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))


{--
[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@(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) = {!!}



-- 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つに分けて考えるといいよね
{-- find status
  1. find start → stack empty
  2. find loop  → stack Not empty ∧ node Not empty
    or "in reverse stack" ≡ "find route orig tree"
  3. find fin   → "stack Not empty ∧ current node is leaf"
    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 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) = {!!}


-- 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 )

--     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)

--     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} (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
--   bt'-right : (key : ℕ) → {right-key : ℕ} → (bt' A right-key ) → (right-key ≤ key) → bt'-path A right-key


-- test = bt'-left {Z} {ℕ} 3 {5} (bt'-leaf 5) (s≤s (s≤s (s≤s z≤n)))



-- reverse1 :  List (bt' A tn) → List (bt' A tn) → List (bt' A tn)
-- reverse1 [] s1 = s1+
-- reverse1 (x ∷ s0) s1 with reverse1 s0 (x ∷ s1)
-- ... | as = {!!}



-- bt-find' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A tn)
--     → ( {key1 : ℕ } → bt' A  key1 → List (bt'-path A key1) → t ) → t
-- bt-find' key tr@(bt'-leaf key₁) stack next = next tr stack  -- no key found
-- bt-find' key (bt'-node key₁ value tree tree₁ x x₁) stack next with <-cmp key key₁
-- bt-find' key tr@(bt'-node {l} {r} key₁ value tree tree₁ x x₁) stack next | tri< a ¬b ¬c =
--          bt-find' key tree ( (bt'-left key {!!} ({!!}) )  ∷  {!!}) next
-- bt-find' key found@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri≈ ¬a b ¬c = next found stack
-- bt-find' key tr@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri> ¬a ¬b c = 
--          bt-find' key tree ( (bt'-right key {!!} {!!} )  ∷ {!!})  next


-- bt-find-step : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A tn)
--     → ( {key1 : ℕ } → bt' A  key1 → List (bt'-path A key1) → t ) → t
-- bt-find-step key tr@(bt'-leaf key₁) stack exit = exit tr stack  -- no key found
-- bt-find-step key (bt'-node key₁ value tree tree₁ x x₁) stack next = {!!}

-- a<sa : { a : ℕ } → a < suc a
-- a<sa {zero} = s≤s z≤n
-- a<sa {suc a} = s≤s a<sa 

-- a≤sa : { a : ℕ } → a ≤ suc a
-- a≤sa {zero} =  z≤n
-- a≤sa {suc a} = s≤s a≤sa 

-- pa<a : { a : ℕ } → pred (suc a) < suc a
-- pa<a {zero} = s≤s z≤n
-- pa<a {suc a} = s≤s pa<a

-- bt-replace' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (value : A ) → (tree : bt' A tn ) → List (bt'-path A {!!})
--     → ({key1 : ℕ } → bt' A  key1 → t ) → t
-- bt-replace' {n} {m} {A} {t} {tn} key value node stack next = bt-replace1 tn node where
--          bt-replace0 : {tn : ℕ } (node : bt' A tn ) → List (bt'-path A {!!}) → t
--          bt-replace0 node [] = next node 
--          bt-replace0 node (bt'-left key (bt'-leaf key₁) x₁ ∷ stack) = {!!}
--          bt-replace0 {tn} node (bt'-left key (bt'-node key₁ value x x₂ x₃ x₄) x₁ ∷ stack) = bt-replace0 {key₁} (bt'-node key₁ value  node  x₂ {!!} x₄ ) stack
--          bt-replace0 node (bt'-right key x x₁ ∷ stack) = {!!}
--          bt-replace1 : (tn : ℕ ) (tree : bt' A tn ) → t
--          bt-replace1 tn (bt'-leaf key0) = bt-replace0 (bt'-node tn value
--               (bt'-leaf (pred tn)) (bt'-leaf (suc tn) ) (≤⇒pred≤ ≤-refl) a≤sa) stack
--          bt-replace1 tn (bt'-node key value node node₁ x x₁) = bt-replace0 (bt'-node key value node node₁ x x₁) stack

-- tree->key : {n : Level} {tn : ℕ} → (A : Set n) → (tree : bt' A tn ) → ℕ
-- tree->key {n} {.key} (A) (bt'-leaf key) = key
-- tree->key {n} {.key} (A) (bt'-node key value tree tree₁ x x₁) = key


-- bt-find'-assert1 : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (tree : bt' A tn ) → Set n
-- bt-find'-assert1 {n} {m} {A} {t} {tn} tree = (key : ℕ) →  (val : A) → bt-find' key tree [] (λ tree1 stack → key ≡ (tree->key A tree1))


-- bt-replace-hoare : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (value : A ) → (tree : bt' A tn )
--                  → (pre : bt-find'-assert1 {n} {m} {A} {t} tree → bt-replace' {!!} {!!} {!!} {!!} {!!}) → t
-- bt-replace-hoare key value tree stack  = {!!}



-- 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}  key node@(bt'-node ⦃ 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
--                          (λ st2 → find'-support {n} {m} {a} {t} {{d}} {{lr'}} key R st2 cg)



-- lleaf : {n : Level} {a : Set n} → bt {n} {a} 
-- 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

-- test-node1 : bt' ℕ 3
-- test-node1 = bt'-node (3) 3 (bt'-leaf 2) (bt'-leaf 4) (s≤s (s≤s {!!})) (s≤s (s≤s (s≤s {!!})))


-- rleaf : {n : Level} {a : Set n} → bt {n} {a} 
-- 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} = (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) )



-- -- 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 (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 (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 を書くときは型を考えるのがやや面倒なので先に動作を書いてから型を ? から補間するとよさそう
-- bt-search-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (x : (x₁ : Maybe (Σ ℕ (λ z → ((x₂ : 4 ≤ z) → ⊥) ∧ ((x₂ : suc z ≤ 3) → ⊥)))) → t) → t
-- bt-search-test {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 3 test-node

-- bt-search-test-bad : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (x : (x₁ : Maybe (Σ ℕ (λ z → ((x₂ : 8 ≤ z) → ⊥) ∧ ((x₂ : suc z ≤ 7) → ⊥)))) → t) → t
-- bt-search-test-bad {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 7 test-node


-- -- up-some : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ {d : ℕ} → (Maybe (Σ ℕ (λ d' → _iso_  {n} {a} d d'))) → (Maybe ℕ)
-- -- up-some (just (fst , snd)) = just fst
-- -- 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 (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@(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@(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@(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
-- bt-find {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key tr st cg = clearSingleLinkedStack st
--                               (λ cst → find-support ⦃ l ⦄  ⦃ u ⦄ key tr cst cg)

-- find-test : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → List bt -- ?
-- 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 ⦄ →
--     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 (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 (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 (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 (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 -- ?
-- singleton-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄  = bt-singleton {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 10 λ x → x


-- 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@(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



-- 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 ⦄ ((N ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (L ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (L  ⦃ d ⦄  ⦃ d ⦄ ≤-refl) z≤n ≤-refl)) st cg



-- -- 証明に insert がはいっててほしい
-- bt-insert : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a})
--             → ((bt {n} {a}) → t) → t

-- 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 (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

-- insert-test-l : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → bt -- ?
-- insert-test-l {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄  = bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 1 (lleaf) λ x → x


-- insert-lem : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → (d : ℕ) → (tree : bt {n} {a})
--              → bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ d tree (λ tree1 → bt-find ⦃ l ⦄ ⦃ u ⦄ d tree1 []
--              (λ tt st ad → (pickKey {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tt)  ≡ just d ) )


-- 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 (N d₁ tree tree₁ x x₁) | tri< a ¬b ¬c = {!!}
--   where
--     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 (N d₁ tree tree₁ x x₁) | tri> ¬a ¬b c = {!!}