--- a/hoareBinaryTree.agda	Wed Mar 04 17:51:05 2020 +0900
+++ b/hoareBinaryTree.agda	Wed Mar 04 19:00:29 2020 +0900
@@ -61,11 +61,6 @@
   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
@@ -76,9 +71,98 @@
 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
+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)
@@ -116,126 +200,6 @@
 -- 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
 
-
-
-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₁
-
-
-
-
-
-
-
-
-
-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) → (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
-
-
-
-
-
-
-
-
-
-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