--- a/hoareRedBlackTree.agda	Thu Nov 07 21:08:14 2019 +0900
+++ b/hoareRedBlackTree.agda	Wed Dec 04 15:42:47 2019 +0900
@@ -1,15 +1,18 @@
+
 module hoareRedBlackTree where
 
 
-open import Level hiding (zero)
+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.Bool
 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
@@ -17,6 +20,7 @@
 open import logic
 
 
+
 record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
   field
     putImpl : treeImpl → a → (treeImpl → t) → t
@@ -39,7 +43,11 @@
 emptySingleLinkedStack :  {n : Level } {Data : Set n} -> SingleLinkedStack Data
 emptySingleLinkedStack = []
 
-pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> List Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
+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
@@ -64,8 +72,7 @@
   field
     root : Maybe (Node a )
     nodeStack : SingleLinkedStack  (Node a )
-    -- compare : k → k → Tri A B C
-    -- <-cmp
+
 
 open RedBlackTree
 
@@ -74,91 +81,463 @@
 --     key : ℕ
 --     val : a
 
-data BTree {n : Level} (a : Set n) : Set n where
-  leaf : BTree a
-  node : (left : BTree a) → (datum : ℕ) → (right : BTree a) → BTree a
+--  leaf nodes key is 0.
+-- 
+-- data BTree {n : Level} (a : Set n) (lk nk rk : ℕ) : Set n where
+--   leaf : (l<n : lk < nk) → BTree a lk nk rk
+--   node : (left : BTree a lk nk rk)
+--        → (datum : ℕ) → (right : BTree a lk nk rk)
+--        → BTree a lk nk rk
+
+
+{-- tree に サイズ比較をつけたい(持ち運びたい)が leaf をどう扱うか問題(0にするとright についたときにおわる)
+終わってほしくないので node のときだけにしたいがそれだと根本的に厳しい（BTree a の再帰構造なので）
+
+
+--}
+
+-- data BTree {n : Level} (a : Set n) : Set n where
+--   leaf :  BTree a
+--   node : (left : BTree a )
+--          → (datum : ℕ)
+--          → (right : BTree a )
+--          → BTree a
+
+-- {a b c : ℕ} {a≤b : a ≤ b } {b≤c : b ≤ c} →
+-- trans≤ : {n : Level} {a : Set n} → Trans {_} {_} {_} {_} {_} {_} {ℕ} {ℕ} {ℕ} (λ x y → x < y) (λ y z → y < z) (λ x z → (x < z)) -- a≤b b≤c
+-- trans≤ {n} {a} {i} {j} {k} i<j j<k = ≤-trans i<j {!!}
+-- with i <? k
+-- trans≤ {n} {a} {i} {j} {k} i<j j<k | yes p = p
+-- trans≤ {n} {a} {i} {j} {k} i<j j<k | no ¬p = {!!}
+
+
+-- data BTree {n : Level} {a : Set n} (p q : ℕ) : ℕ → Set n where
+--   leaf : (p<q : p ≤ q ) → BTree p q 0
+--   node : ∀ {hl hr h : ℕ}
+--              → (key : ℕ)
+--              → (left : BTree {n} {a} p key hl )
+--              → (right : BTree {n} {a} key q hr )
+--              → BTree p q (suc h)
+
+-- leaf-inj : {n : Level} {a : Set n} {p q : ℕ} {pp qq : p ≤ q}
+--            → (leaf {n} {a} pp) ≡ (leaf qq) → pp ≡ qq
+-- leaf-inj refl = refl
+
+
+
+-- node-inj : {n : Level} {a : Set n}
+--   {k1 k2 h : ℕ} {l1 r1 : BTree {n} {a} h} {l2 r2 : BTree {n} {a} h}
+--   → ((node {n} {a} {h} l1 k1 r1)) ≡ (node l2 k2 r2) → k1 ≡ k2
+-- node-inj refl = refl
+
+-- node-inj1 : {n : Level} {a : Set n}
+--   {k1 k2 h hl1 hl2 hr1 hr2 p q : ℕ }
+--   {l1 : BTree {n} {a} p k1 hl1 } {l2 : BTree {n} {a} p k2 hl2} {l1 : BTree {n} {a} k1 q hr1} {r2 : BTree {n} {a} k2 q hr2}
+--   → (node {n} {a} {h} {?} {?} {?}  {!!} {!!} ) ≡ (node  {!!} {!!} {!!} ) → k1 ≡ k2
+-- node-inj1 as = {!!}
 
 
 
-findT : {n m  : Level } {a : Set n} {t : Set m}  → BTree {n} a → ℕ → SingleLinkedStack (BTree a) → (BTree {n} a → SingleLinkedStack (BTree a) → t) → t
-findT leaf sd st next = next leaf st
-findT (node ltree datum rtree) sd st  next with <-cmp sd datum
-findT tree@(node ltree datum rtree) sd st  next | tri≈ ¬a b ¬c = next tree st
-findT tree@(node ltree datum rtree) sd st  next | tri< a ¬b ¬c = pushSingleLinkedStack st tree (λ st2 → findT ltree sd st2 next)
-findT tree@(node ltree datum rtree) sd st  next | tri> ¬a ¬b c = pushSingleLinkedStack st tree (λ st2 → findT rtree sd st2 next)
+--- add relation find functions
+-- fTree is start codeGear. findT2 is loop codeGear.
+-- findT2 : {n m  : Level } {a : Set n} {b lk rk kk1 kk2 : ℕ} {t : Set m}
+--       → (k1<k2 : kk1 ≤ kk2) → BTree {n} {a} b lk rk → (key : ℕ)
+--       → SingleLinkedStack (BTree {n} {a} b lk rk)
+--       → ( (lk ≤ rk) →  BTree {n} {a} b lk rk → SingleLinkedStack (BTree {n} {a} b lk rk) → t)   → t
+-- findT2 k1<k2 (leaf p<q) key stack cg = cg {!!} (leaf p<q) stack
+-- findT2 k1<k2 (node key1 tree₁ tree₂) key stack cg with <-cmp key1 key
+-- findT2 k1<k2 (node key1 tree₁ tree₂) key stack cg | tri≈ ¬a b ¬c = {!!}
+-- findT2 k1<k2 (node key1 tree₁ tree₂) key stack cg | tri< a ¬b ¬c = {!!}
+-- findT2 k1<k2 (node key1 tree₁ tree₂) key stack cg | tri> ¬a ¬b c = {!!}
+
+-- cg k1<k2 (leaf p<q) stack
+-- findT2 {n} {m} {a} {b} {kk1} {kk2} {t} k1<k2 (node rt key1 lt) key stack cg with <-cmp key1 key
+-- findT2 {n} {m} {a} {b} {kk1} {kk2} {t} k1<k2 tree@(node rt key1 lt) key stack cg | tri≈ ¬lt eq ¬gt = cg {!!} tree stack
+-- findT2 {n} {m} {a} {b} {kk1} {kk2} {t} k1<k2 (node rt key1 ltt) key stack cg | tri< lt ¬eq ¬gt = {!!}
+-- findT2 {n} {m} {a} {b} {kk1} {kk2} {t} k1<k2 (node rt key1 ltt) key stack cg | tri> ¬lt ¬eq gt = {!!}
+
+
+-- fTree : {n m  : Level } {a : Set n} {b k1 k2 : ℕ} {t : Set m}
+--      → BTree {n} {a} b → (key : ℕ)
+--      → SingleLinkedStack (BTree {n} {a} b) → ( k1 < k2  →  BTree {n} {a} b → SingleLinkedStack (BTree {n} {a} b) → t)  → t
+-- fTree {n} {m} {a} {b} tree key stack cg  = clearSingleLinkedStack stack (λ cstack → findT2 {n} {m} {a} {b} {0} {key} z≤n tree key cstack λ x x₁ x₂ → {!!})
+
+{--
+そもそも Tree は 高さを受け取るのではなく 関係だけを持つ
+leaf は関係を受け取って tran で (0 < n < m)をつくる
+--}
 
 
-testTreeType : {n : Level} {a : Set n} → BTree {n} a
-testTreeType = (node (node leaf 1 leaf) 2 (node leaf 3 leaf))
+{-- 思いつき
+ Max Hight を持ち運んで必ず規定回数で止まるようにするのはあり…ｎきがする
+ Tree を作ったあとに 左右の最大 hight を比較して Max にするのは良い
+ 操作時はMaxが減る。 途中で終わった場合や、値が見つかった場合は
+ 受け取って Max を減らすだけの関数で既定回数数を減らすだけ
+
+ 関数に持たせる?データに持たせる?
+ とりあえず関数(Data だと 再帰的な構造上定義が難しい)
+
+--}
+
+data BTree {n : Level} {a : Set n} : (hight : ℕ) → Set n where
+  leaf : {p q h : ℕ } → (p<q : p ≤ q ) → BTree (suc h)
+  node : { h : ℕ }
+             → (left : BTree {n} {a} (suc h) )
+             → (key : ℕ)
+             → (right : BTree {n} {a} (suc h) )
+             → BTree h
 
--- findT testTreeType 44 [] (λ t st → t)
--- leaf
+maxHight : {n m : Level} {a : Set n} {t : Set m} {h : ℕ} → (searchHight : ℕ) → (BTree {n} {a} h) → ℕ
+maxHight {n} {m} {a} {t} zero (leaf p<q) = 0                  -- root is leaf
+maxHight {n} {m} {a} {t} (suc hi) (leaf p<q) = (suc hi)       -- max
+maxHight {n} {m} {a} {t} hi (node tree₁ key₁ tree₂) with (maxHight {n} {m} {a} {t} hi tree₁) | (maxHight {n} {m} {a} {t} hi tree₂)
+... | lh | rh with <-cmp lh rh
+maxHight {n} {m} {a} {t} hi (node tree₁ key₁ tree₂) | lh | rh | tri< a₁ ¬b ¬c = rh
+maxHight {n} {m} {a} {t} hi (node tree₁ key₁ tree₂) | lh | rh | tri≈ ¬a b ¬c = lh
+maxHight {n} {m} {a} {t} hi (node tree₁ key₁ tree₂) | lh | rh | tri> ¬a ¬b c = lh
+-- maxHight {n} {m} {a} {t} hi (rnode tree₁ key₁ tree₂) = {!!}
+
 
--- findT testTreeType 44 [] (λ t st → st)
--- node leaf 3 leaf ∷ node (node leaf 1 leaf) 2 (node leaf 3 leaf) ∷ []
+LastNodeIsLeaf :  {n : Level} {a : Set n} → (h : ℕ) →  (tree : BTree {n} {a} h) → (P : BTree {n} {a} (suc h) → ℕ → BTree {n} {a} (suc h) → Bool) → Bool
+LastNodeIsLeaf h (leaf p<q) P = true
+LastNodeIsLeaf h (node rt k1 lt) P = (P rt k1 lt) /\ LastNodeIsLeaf (suc h) lt (λ _ z _ → P lt z lt) /\ LastNodeIsLeaf (suc h) rt λ _ z _ → P lt z lt
+
+-- allnodes : {n : Level} {a : Set n} → (t : BTreeEx {n} {a}) → (P : BTreeEx {n} {a} → ℕ → BTreeEx {n} {a} → Bool) → Bool
+-- allnodes leafEx p = true
+-- allnodes (nodeEx lt k rt) p = (p lt k rt) /\ allnodes lt p /\ allnodes rt p
+
+-- MaxHightStop? :  {n : Level} {a : Set n} → {h : ℕ} → (hight : ℕ) → (tree : BTree {n} {a} h) → (P : BTree {n} {a} (suc h) → ℕ → BTree {n} {a} (suc h) → Bool) → Bool
+-- MaxHightStop? {n} {a} {.(suc _)} zero (leaf p<q) P = true
+-- MaxHightStop? {n} {a} {.(suc _)} (suc allh) (leaf p<q) P = false
+-- MaxHightStop? {n} {a} {h} zero (node lt k rt) P = false
+-- MaxHightStop? {n} {a} {h} (suc allh) (node lt k rt) P = (P lt k lt) /\ (MaxHightStop? allh lt λ _ z _ → ) /\ (MaxHightStop? allh rt λ _ z _ → P rt z rt)
+
+
+SearchLeaf : {n : Level} {a : Set n} → (h : ℕ) → (t : BTree {n} {a} h) → Bool
+SearchLeaf h tree = LastNodeIsLeaf h tree (λ l k r → LastNodeIsLeaf (suc h) l (λ _ j _ → j <B? k) /\ LastNodeIsLeaf (suc h) r (λ _ n _ → k <B? n))
 
 
--- findT testTreeType 3 [] (λ t st → t)
--- node leaf 3 leaf
+{-- whats leaf relation...?
+i think keys relation...
+"leaf relation" maybe 0<"parent node key" ???
+--}
+test : {n : Level} {a : Set n} {h : ℕ} → BTree {n} {a} h
+test {n} {a} {h} = (node (leaf {n} {a} {0} {2} z≤n) 2 (node (leaf {n} {a} {0} {3} z≤n) 3 (leaf {n} {a} {0} {3} z≤n)))
+
+c : {n : Level} {a : Set n} → Bool
+c {n} {a} = SearchLeaf {n} {a} 3 test
+
+cm : {n : Level} {a : Set n} → ℕ
+cm {n} {a} = maxHight {n} {n} {a} {a} {zero} {!!} test
+
+lemma-all-leaf : {n : Level} {a : Set n} → (h : ℕ) → (tree : BTree {n} {a} h) → SearchLeaf h tree ≡ true
+lemma-all-leaf .(suc _) (leaf p<q) = refl
+lemma-all-leaf h tt@(node pltree k1 rtree) = {!!} -- lemma-all-leaf h tt
+-- lemma-all-leaf .0 tt@(rnode ltree k1 rtree) = lemma-all-leaf zero tt
+
+findT : {n m  : Level } {a : Set n} {b left current : ℕ} {t : Set m}
+      → (ta<tb : left ≤ current) → BTree {n} {a} b → (key : ℕ)
+      → SingleLinkedStack (BTree {n} {a} b)
+      →   (BTree {n} {a} b → SingleLinkedStack (BTree {n} {a} b) → t) → t
+findT = {!!}
 
--- findT testTreeType 3 [] (λ t st → st)
--- node (node leaf 1 leaf) 2 (node leaf 3 leaf) ∷ []
+-- findT {n} {m} {a} {b} {l} l<c (leaf p<q) key st cg = cg (leaf {n} {a} {b} {key} (z≤n)) st
+-- findT l<c (node tree₁ key1 tree₂) key st cg with <-cmp key key1
+-- findT l<c (node tree₁ key1 tree₂) key st cg | tri< a ¬b ¬c = {!!}
+-- findT l<c (node tree₁ key1 tree₂) key st cg | tri≈ ¬a b ¬c = {!!}
+-- findT l<c (node tree₁ key1 tree₂) key st cg | tri> ¬a ¬b c = {!!}
+-- -- findT l<c tree@(node ltree key1 rtree) key st cg                          | tri≈ ¬lt eq ¬gt = cg tree st
+-- findT {n} {m} {a} {b} {l} {cu} {?} l<c tree@(node {b} ltree key1 rtree) key st cg | tri< lt ¬eq ¬gt = ?
+-- findT {n} {m} {a} {b} {l} {cu} l<c tree@(node ltree key1 rtree) key st cg | tri> ¬lt ¬eq gt = pushSingleLinkedStack st tree (λ st2 → findT {n} {m} {a} {b} {l} {cu} {!!} ({!!}) key st2 cg)
+-- findT の {!!} の部分は trans したやつが入ってほしい(型が合わない)
+
+
+--- nomal find
+-- findT : {n m  : Level } {a : Set n} {b left current : ℕ} {t : Set m}
+--       → (ta<tb : left ≤ current) → BTree {n} {a} b → (key : ℕ)
+--       → SingleLinkedStack (BTree {n} {a} b)
+--       →   (BTree {n} {a} b → SingleLinkedStack (BTree {n} {a} b) → t)   → t
+
+-- findT {n} {m} {a} {b} {l} l<c (leaf p<q) key st cg = cg (leaf {n} {a} {b} {key} (z≤n)) st
+-- findT l<c (node tree₁ key1 tree₂) key st cg with <-cmp key key1
+-- findT l<c tree@(node ltree key1 rtree) key st cg | tri≈ ¬lt eq ¬gt = cg tree st
+
+-- findT {n} {m} {a} {b} {l} {cu} l<c tree@(node (leaf p<q) key1 rtree) key st cg | tri< lt ¬eq ¬gt = pushSingleLinkedStack st tree (λ st2 → {!!}) -- findT {n} {m} {a} {b} ⦃ !! ⦄ ⦃ !! ⦄ {!!} (leaf {n} {a} ⦃ !! ⦄ {cu} {!!}) key st2 cg)
+
+-- findT {n} {m} {a} {b} {l} {cu} l<c tree@(node ltt@(node ltree key₁ ltree₁) key1 rtree) key st cg | tri< lt ¬eq ¬gt = pushSingleLinkedStack st tree (λ st2 → findT {n} {m} {a} {b} ⦃ !! ⦄ ⦃ !! ⦄ {!!} {!!} key st2 cg)
+
+-- findT {n} {m} {a} {b} {l} {cu} l<c tree@(node ltree key1 rtree) key st cg | tri> ¬lt ¬eq gt = pushSingleLinkedStack st tree (λ st2 → findT {n} {m} {a} {b} {key} {key1} {!!} (rtree) key st2 cg)
 
 
-replaceT : {n m  : Level } {a : Set n} {t : Set m}  → BTree {n} a → ℕ → SingleLinkedStack (BTree a) → (BTree {n}  a  → t) → t
-replaceT {n} {m} {a} {t} leaf n0 [] next = next (node leaf n0 leaf)
-replaceT {n} {m} {a} {t} tree@(node x datum x₁) n0 [] next = next tree
+-- findT l<c tree@(node {lh} {rh} {h} ltree key1 rtree) key st cg | tri≈ ¬lt eq ¬gt = cg tree st
+
+-- findT {n} {m} {a} {b} {l} l<c tree@(node {lh} {rh} {h} ltree key1 rtree) key st cg | tri< lt ¬eq ¬gt = {!!} --  pushSingleLinkedStack st tree (λ st2 → findT {n} {m} {a} {lh} {rh} {h} {!!} ({!!}) key {!!} λ x x₁ → {!!})
+-- findT l<c (node tree₁ key1 tree₂) key st cg | tri> ¬lt ¬eq gt = {!!}
+-- findT (leaf p<q) key st cg = cg (leaf p<q ) st
+-- findT (node tree₁ key₁ tree₂) key st cg with <-cmp key key₁
+-- findT tree@(node tree₁ key₁ tree₂) key st cg | tri≈ ¬a b ¬c = cg tree st
+-- findT tree@(node tree₁ key₁ tree₂) key st cg | tri< a ¬b ¬c = {!!}
+-- findT tree@(node tree₁ key₁ tree₂) key st cg | tri> ¬a ¬b c = {!!}
+
 
-replaceT {n} {m} {a} {t} leaf n0 (leaf ∷ rstack) next = replaceT (node leaf n0 leaf) n0 rstack next
+data BTreeEx {n : Level} {a : Set n} : Set n where
+  leafEx : BTreeEx
+  nodeEx :(left : BTreeEx {n} {a} )
+    → (key : ℕ)
+    → (right : BTreeEx {n} {a} )
+    → BTreeEx
+
+
+cmpMax : ℕ → ℕ → ℕ
+cmpMax lh rh with <-cmp lh rh
+cmpMax lh rh | tri< a ¬b ¬c = rh
+cmpMax lh rh | tri≈ ¬a b ¬c = lh
+cmpMax lh rh | tri> ¬a ¬b c₁ = lh
+
+
+max1 : {n m : Level} {a : Set n} {t : Set m} → ℕ → (BTreeEx {n} {a}) → (ℕ → t) → t
+max1 {n} {m} {a} {t} hi leafEx cg = cg hi
+max1 {n} {m} {a} {t} hi (nodeEx tree₁ key₁ tree₂) cg = (max1 {n} {m} {a} {t} (suc hi) tree₁
+                    (λ lh → (max1 {n} {m} {a} {t} (suc hi) tree₂ (λ rh → cg (cmpMax lh rh))) ))
 
 
-replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next with <-cmp n0 datum
-replaceT {n} {m} {a} {t} leaf n0 (tree@(node x datum x₁) ∷ rstack) next | tri≈ ¬a b ¬c =  replaceT tree n0 rstack next
-replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next | tri< a₁ ¬b ¬c = replaceT (node (node leaf n0 leaf) datum x₁) n0 rstack next
-replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next | tri> ¬a ¬b c =  replaceT (node x datum (node leaf n0 leaf)) n0 rstack next
+max : {n m : Level} {a : Set n} {t : Set m} → (BTreeEx {n} {a}) → (ℕ → t) → t
+max {n} {m} {a} {t} tree = max1 zero tree
+
+
+maxI : {n m : Level} {a : Set n} {t : Set m} → (BTreeEx {n} {a}) → ℕ
+maxI {n} {m} {a} {t} tree = max tree (λ x → x)
+
+-- bad proof
+-- isStopMax? : {n m : Level} {a : Set n} {t : Set m} → ( tr : BTreeEx {n} {a}) → (max 0 tr (λ n → n ≡ n))
+-- isStopMax? leafEx = refl
+-- isStopMax? (nodeEx tree₁ key₁ tree₂) = {!!}
+
+isStopMax? : {n m : Level} {a : Set n} {t : Set m} → ( tr : BTreeEx {n} {a}) → (max tr (λ eq → eq ≡ eq))
+isStopMax? leafEx = refl
+isStopMax? (nodeEx tree₁ key₁ tree₂) = max (nodeEx tree₁ key₁ tree₂) (λ n₁ →  {!!})
+
+ltreeSearchLeaf : {n m : Level} {a : Set n} {t : Set m} → (BTreeEx {n} {a}) → ((BTreeEx {n} {a}) → t) → t
+ltreeSearchLeaf leafEx cg = cg leafEx
+ltreeSearchLeaf (nodeEx tree₁ key₁ tree₂) cg = ltreeSearchLeaf tree₁ cg
+
+ltreeStop? : {n m : Level} {a : Set n} {t : Set m} → (tree : BTreeEx {n} {a}) → ltreeSearchLeaf tree (λ tt →  tt ≡ tt)
+ltreeStop? leafEx = refl
+ltreeStop? {n} {m} {a} {t} (nodeEx tree₁ key₁ tree₂) =  ltreeStop? {n} {m} {a} {t} tree₁
+
+ltreeSearchNode : {n m : Level} {a : Set n} {t : Set m} → (key : ℕ) → (BTreeEx {n} {a}) → ( (BTreeEx {n} {a}) → t) → t
+ltreeSearchNode key leafEx cg = cg leafEx
+ltreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg with <-cmp key key₁
+ltreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg | tri< a ¬b ¬c = ltreeSearchNode key tree₁ cg
+ltreeSearchNode key tt@(nodeEx tree₁ key₁ tree₂) cg | tri≈ ¬a b ¬c = cg tt
+ltreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg | tri> ¬a ¬b c₁ = cg tree₂
+
 
 
 
-replaceT {n} {m} {a} {t} tree@(node ltree datum rtree) n0 (leaf ∷ rstack) next = replaceT tree n0 rstack next
+-- 何らかの集合のサイズが減っていれば良い…？
+ltreeStoplem : {n m : Level} {a : Set n} {t : Set m}
+  → (key : ℕ) → (lt : BTreeEx {n} {a}) → (key1 : ℕ) → (rt : BTreeEx {n} {a}) → (p<q : key < key1 )
+  → (ℕ → BTreeEx {n} {a} → t ) → t
+
+ltreeNodeStop? : {n m : Level} {a : Set n} {t : Set m} → (key : ℕ) → (tree : BTreeEx {n} {a}) → ltreeSearchNode key tree (λ tt →  tt ≡ tt)
+ltreeNodeStop? key leafEx = refl
+ltreeNodeStop? key (nodeEx tree₁ key₁ tree₂) with <-cmp key key₁
+ltreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri< a ¬b ¬c = {!!}
+
+-- ltreeNodeStop? {!!} {!!}
+{--
+Failed to solve the following constraints:
+[720] ltreeSearchNode ?4 ?5 (λ tt → tt ≡ tt)
+=< ltreeSearchNode key tree₁ (λ tt → tt ≡ tt)
+: Set n
+--}
+ltreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri≈ ¬a b ¬c = refl
+ltreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri> ¬a ¬b c₁ = refl
+
+
+
+-- rtreeSearchNode : {n m : Level} {a : Set n} {t : Set m} → (key : ℕ) → (BTreeEx {n} {a}) → ( (BTreeEx {n} {a}) → t) → t
+-- rtreeSearchNode key leafEx cg = cg leafEx
+-- rtreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg with <-cmp key key₁
+-- rtreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg | tri< a ¬b ¬c = cg tree₂
+-- rtreeSearchNode key tt@(nodeEx tree₁ key₁ tree₂) cg | tri≈ ¬a b ¬c = cg tt
+-- rtreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg | tri> ¬a ¬b c₁ = rtreeSearchNode key tree₁ cg
+
+
+-- rtreeNodeStop? : {n m : Level} {a : Set n} {t : Set m} → (key : ℕ) → (tree : BTreeEx {n} {a}) → rtreeSearchNode key tree (λ tt →  tt ≡ tt)
+-- rtreeNodeStop? key leafEx = refl
+-- rtreeNodeStop? key (nodeEx tree₁ key₁ tree₂) with <-cmp key key₁
+-- rtreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri< a ¬b ¬c = refl
+-- rtreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri≈ ¬a b ¬c = refl
+-- rtreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri> ¬a ¬b c₁ = rtreeNodeStop? key {!!}
+
+
+ltreeStoplem key lt key1 rt p<q cg = cg key (nodeEx lt key1 rt)
+
+
+
 
--- bad some code
-replaceT {n} {m} {a} {t} tree@(node ltree datum rtree) n0 ((node x rdatum x₁) ∷ rstack) next with <-cmp datum rdatum
-replaceT {n} {m} {a} {t} (node ltree datum rtree) n0 (tree@(node x rdatum x₁) ∷ rstack) next
-         | tri≈ ¬a b ¬c = replaceT tree n0 rstack next
-replaceT {n} {m} {a} {t} tree n0 (node x rdatum x₁ ∷ rstack) next
-         | tri< a₁ ¬b ¬c = replaceT (node tree rdatum x₁) n0 rstack next
-replaceT {n} {m} {a} {t} tree n0 (node x rdatum x₁ ∷ rstack) next
-         | tri> ¬a ¬b c = replaceT (node x rdatum tree) n0 rstack next
+-- with (max {n} {m} {a} {t} (suc hi) tree₁ cg) | (max {n} {m} {a} {t} (suc hi) tree₂ cg)
+-- ... | lh | rh = {!!}
+
+-- max {n} {m} {a} {t} hi (nodeEx tree₁ key₁ tree₂) cg | lh | rh | tri< a₁ ¬b ¬c = cg rh
+-- max {n} {m} {a} {t} hi (nodeEx tree₁ key₁ tree₂) cg | lh | rh | tri≈ ¬a b ¬c = cg lh
+-- max {n} {m} {a} {t} hi (nodeEx tree₁ key₁ tree₂) cg | lh | rh | tri> ¬a ¬b c = cg lh
+
+
+-- findStop : {n m  : Level } {a : Set n} {t : Set m}  → BTreeEx {n} {a} → (key : ℕ) → SingleLinkedStack (BTreeEx) → (BTreeEx {n} → SingleLinkedStack (BTreeEx) → t) → t
+-- findStop = {!!}
+
+findTEx : {n m  : Level } {a : Set n} {t : Set m}  → BTreeEx {n} {a} → (key : ℕ) → SingleLinkedStack (BTreeEx) → (BTreeEx {n} → SingleLinkedStack (BTreeEx) → t) → t
+findTEx leafEx sd st next = next leafEx st
+findTEx (nodeEx ltree datum rtree) sd st  next with <-cmp sd datum
+findTEx tree@(nodeEx ltree datum rtree) sd st  next | tri≈ ¬a b ¬c = next tree st
+findTEx tree@(nodeEx ltree datum rtree) sd st  next | tri< a ¬b ¬c = pushSingleLinkedStack st tree (λ st2 → findTEx ltree sd st2 next)
+findTEx tree@(nodeEx ltree datum rtree) sd st  next | tri> ¬a ¬b c = pushSingleLinkedStack st tree (λ st2 → findTEx rtree sd st2 next)
 
-insertT : {n m  : Level } {a : Set n} {t : Set m}  → BTree {n} a → ℕ → SingleLinkedStack (BTree a) → (BTree {n}  a  → t) → t
-insertT tree n0 st next =  findT tree n0 st ( λ new st2 → replaceT new n0 st2 next )
+findL : {n m  : Level } {a : Set n} {t : Set m}  → BTreeEx {n} {a} → (key : ℕ) → SingleLinkedStack (BTreeEx) → (BTreeEx {n} → SingleLinkedStack (BTreeEx) → t) → t
+findL leafEx key stack cg = cg leafEx stack
+findL (nodeEx tree₁ key1 tree₂) key stack cg with (key1 ≤? key)
+findL (nodeEx tree₁ key1 tree₂) key stack cg | yes p with key1 ≟ key
+findL tree@(nodeEx tree₁ key1 tree₂) key stack cg | yes p | yes p₁ = cg tree stack
+findL tree@(nodeEx ltree key1 tree₂) key stack cg | yes p | no ¬p = pushSingleLinkedStack stack tree (λ stack1 → findL ltree key stack1 cg)
+findL (nodeEx tree₁ key1 tree₂) key stack cg | no ¬p = cg leafEx stack
+
+
+
+allnodes : {n : Level} {a : Set n} → (t : BTreeEx {n} {a}) → (P : BTreeEx {n} {a} → ℕ → BTreeEx {n} {a} → Bool) → Bool
+allnodes leafEx p = true
+allnodes (nodeEx lt k rt) p = (p lt k rt) /\ allnodes lt p /\ allnodes rt p
+
+find-leaf : {n : Level} {a : Set n} → (t : BTreeEx {n} {a}) → Bool
+find-leaf tree = allnodes tree (λ l k r → allnodes l (λ _ j _ → j <B? k) /\ allnodes r (λ _ n _ → k <B? n))
+
+testTree : {n : Level} {a : Set n} → BTreeEx {n} {a}
+testTree {n} {a} = (nodeEx (nodeEx leafEx 1 leafEx) 2 (nodeEx leafEx 3 (nodeEx (nodeEx leafEx 4 leafEx) 5 (nodeEx leafEx 6 leafEx))))
+
+badTree : {n : Level} {a : Set n} → BTreeEx {n} {a}
+badTree {n} {a} = (nodeEx (nodeEx leafEx 3 leafEx) 2 leafEx)
+
+
+
+lemm : {n : Level} {a : Set n} → find-leaf {n} {a} testTree ≡ true
+lemm = refl
 
 
-c1 : {n : Level} {a : Set n} → BTree {n} a
-c1 = insertT leaf 1 [] (λ t → insertT t 3 [] (λ t → insertT t 5 [] (λ t → insertT t 7 [] (λ t → t))))
+bool-⊥ : true ≡ false → ⊥
+bool-⊥ ()
+
+{-- badTree  --}
+-- lemm1 : {n : level} {a : set n} → find-leaf {n} {a} badtree ≡ true
+-- lemm1 {n} {a} with badtree
+-- lemm1 {n} {a} | leafex = {!!}
+-- lemm1 {n} {a} | nodeex gda key₁ gda₁ = {!!}
+
+-- lemm-all : {n : Level} {a : Set n} (any-tree : BTreeEx {n} {a}) → find-leaf {n} {a} any-tree ≡ true
+-- lemm-all leafEx = refl
+-- lemm-all t@(nodeEx ltree k rtree) with (find-leaf t) ≟B true
+-- lemm-all (nodeEx ltree k rtree) | yes p = p
+-- lemm-all (nodeEx ltree k rtree) | no ¬p = {!!}
+
+-- findT : {n m  : Level } {a : Set n} {t : Set m}  → BTree {n} {a}  → (key : ℕ) → SingleLinkedStack (BTree a) → (BTree {n} a → SingleLinkedStack (BTree a) → t) → t
+-- findT = ?
+
+-- {--
+-- 一旦の方針は hight を使って書く, 大小関係 (片方だけ) を持って証明しながら降りてく
+-- --}
+
+
+-- hoge = findTEx testTree 44 [] (λ t s → s)
 
-c2 : {n : Level} {a : Set n} → BTree {n} a
-c2 = insertT leaf 5 [] (λ t → insertT t 3 [] (λ t → insertT t 1 [] (λ t → insertT t 7 [] (λ t → t))))
+-- {--
+--   Tree に対して l < x < r の条件を足すときに気になるのは l or r が leaf の場合
+--   leaf のときだけ例外的な証明を書く必要ありそう
+-- --}
+
+
+-- {-- AVL Tree メモ
+-- - $AGDA-HOME/Data/AVL.agda 関連を眺めた Tips
+-- AVL は特徴として すべての枝の長さの差が1以内に収まっている木。バランスもできる。
+
+-- AVL Tree には key , value , left right の他にkeyの 上限、下限、高さを持ってるらしい
+-- (後ろに付いてるのは高さ+- 1 の関係をもってる)
+
+-- cast operation は木のサイズの log になる
+-- (cast operation は… わすれた)
+
+-- insert では 同じ key の値があったら Node を置き換え
+
+
+-- --}
+
+-- -- findT testTreeType 44 [] (λ t st → t)
+-- -- leaf
+
+-- -- findT testTree 44 [] (λ t st → st)
+-- -- node leaf 3 leaf ∷ node (node leaf 1 leaf) 2 (node leaf 3 leaf) ∷ []
 
 
-getkey : {n : Level } {a : Set n} → BTree {n} a → Maybe ℕ
-getkey leaf = nothing
-getkey (node tree₁ datum tree₂) = just datum
+-- -- findT testTreeType 3 [] (λ t st → t)
+-- -- node leaf 3 leaf
+
+-- -- findT testTreeType 3 [] (λ t st → st)
+-- -- node (node leaf 1 leaf) 2 (node leaf 3 leaf) ∷ []
+
+
+-- replaceT : {n m  : Level } {a : Set n} {t : Set m}  → BTree {n} a → ℕ → SingleLinkedStack (BTree a) → (BTree {n}  a  → t) → t
+-- replaceT {n} {m} {a} {t} leaf n0 [] next = next (node leaf n0 leaf)
+-- replaceT {n} {m} {a} {t} tree@(node x datum x₁) n0 [] next = next tree
+
+-- replaceT {n} {m} {a} {t} leaf n0 (leaf ∷ rstack) next = replaceT (node leaf n0 leaf) n0 rstack next
+
+
+-- replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next with <-cmp n0 datum
+-- replaceT {n} {m} {a} {t} leaf n0 (tree@(node x datum x₁) ∷ rstack) next | tri≈ ¬a b ¬c =  replaceT tree n0 rstack next
+-- replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next | tri< a₁ ¬b ¬c = replaceT (node (node leaf n0 leaf) datum x₁) n0 rstack next
+-- replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next | tri> ¬a ¬b c =  replaceT (node x datum (node leaf n0 leaf)) n0 rstack next
+
+
+
+-- replaceT {n} {m} {a} {t} tree@(node ltree datum rtree) n0 (leaf ∷ rstack) next = replaceT tree n0 rstack next
 
-find-insert : {n m  : Level } {a : Set n} {t : Set m} → (any : BTree {n} a) → (key : ℕ) → insertT any key [] (λ x → findT x key [] (λ return _ → (just key ≡  (getkey {n} return))))
-find-insert leaf key with <-cmp key key
-find-insert leaf key | tri< a ¬b ¬c = ⊥-elim (¬c a )
-find-insert leaf key | tri≈ ¬a b ¬c = refl
-find-insert leaf key | tri> ¬a ¬b c = ⊥-elim (¬a c )
-find-insert tr@(node any₁ datum any₂) key with <-cmp key datum
-find-insert (node any₁ datum any₂) key | tri< a ¬b ¬c = {!!}
-find-insert (node any₁ datum any₂) key | tri> ¬a ¬b c = {!!}
-find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c with <-cmp key datum
-find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = {!!}
-find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = {!!}
-find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = {!!}
+-- -- bad some code
+-- replaceT {n} {m} {a} {t} tree@(node ltree datum rtree) n0 ((node x rdatum x₁) ∷ rstack) next with <-cmp datum rdatum
+-- replaceT {n} {m} {a} {t} (node ltree datum rtree) n0 (tree@(node x rdatum x₁) ∷ rstack) next
+--          | tri≈ ¬a b ¬c = replaceT tree n0 rstack next
+-- replaceT {n} {m} {a} {t} tree n0 (node x rdatum x₁ ∷ rstack) next
+--          | tri< a₁ ¬b ¬c = replaceT (node tree rdatum x₁) n0 rstack next
+-- replaceT {n} {m} {a} {t} tree n0 (node x rdatum x₁ ∷ rstack) next
+--          | tri> ¬a ¬b c = replaceT (node x rdatum tree) n0 rstack next
+
+-- insertT : {n m  : Level } {a : Set n} {t : Set m}  → BTree {n} a → ℕ → SingleLinkedStack (BTree a) → (BTree {n}  a  → t) → t
+-- insertT tree n0 st next =  findT tree n0 st ( λ new st2 → replaceT new n0 st2 next )
+
+
+-- c1 : {n : Level} {a : Set n} → BTree {n} a
+-- c1 = insertT leaf 1 [] (λ t → insertT t 3 [] (λ t → insertT t 5 [] (λ t → insertT t 7 [] (λ t → t))))
+
+-- c2 : {n : Level} {a : Set n} → BTree {n} a
+-- c2 = insertT leaf 5 [] (λ t → insertT t 3 [] (λ t → insertT t 1 [] (λ t → insertT t 7 [] (λ t → t))))
 
--- where
+-- -- -- 末
+-- -- findDownEnd : {n m : Level} {a : Set n} {t : Set m} → (find : ℕ) → (any : BTree a) → findT any find [] (λ tt stack → {!!})
+-- -- findDownEnd d tree = {!!}
+
+-- find-insert : {n m  : Level } {a : Set n} {t : Set m} → (any : BTree {n} a) → (key : ℕ) → insertT any key [] (λ x → findT x key [] (λ return _ → (key ≡  {!!})))
+-- find-insert leaf key with <-cmp key key
+-- find-insert leaf key | tri< a ¬b ¬c = ⊥-elim (¬c a )
+-- find-insert leaf key | tri≈ ¬a b ¬c = {!!}
+-- find-insert leaf key | tri> ¬a ¬b c = ⊥-elim (¬a c )
+-- find-insert tr@(node any₁ datum any₂) key with <-cmp key datum
+-- find-insert (node any₁ datum any₂) key | tri< a ¬b ¬c = {!!}
+-- find-insert (node any₁ datum any₂) key | tri> ¬a ¬b c = {!!}
+-- find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c with <-cmp key datum
+-- find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = {!!}
+-- find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = {!!}
+-- find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = {!!}
+
+-- -- where
 -- find-lemma : {n m : Level} {a : Set n} {t : Set m} → BTree a → ℕ → SingleLinkedStack (BTree a) → (BTree a → SingleLinkedStack (BTree a) → t) → t
 -- find-lemma leaf ke st nt = nt leaf st
 -- find-lemma (node tr datum tr₁) ke st nt with <-cmp ke datum
@@ -198,7 +577,7 @@
 node003 : Node  ℕ
 node003 = record { key = 0 ; value = 3 ; left = just node002 ; right = nothing ; color = Black }
 
-test001 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = nothing ; nodeStack = emptySingleLinkedStack } )
+tes0t01 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = nothing ; nodeStack = emptySingleLinkedStack } )
    node001 ( λ tree → tree )
 test002 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node001 ; nodeStack = emptySingleLinkedStack } )
    node001 ( λ tree → tree )
@@ -253,28 +632,28 @@
    -- fni-loop  : (x : Node a) (st : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a ) → FindNodeInvariant st original
 
 
-findNode1h : {n m  : Level } {a : Set n} {t : Set m}  → (tree : RedBlackTree {n} a )  → (Node a )
-     → ((new : RedBlackTree {n} a) →  FindNodeInvariant (nodeStack new) tree → t )
-     → ( FindNodeInvariant (nodeStack tree)  tree) → t
-findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) n0 prev
-  module FindNodeH where
-    findNode2h : (Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → Node a → FindNodeInvariant s tree  → t
-    findNode2h nothing st n0 prev = next record { root = nothing ; nodeStack = st } prev
-    findNode2h (just x) st n0 prev with <-cmp (key n0) (key x)
-    ... | tri≈ ¬lt eq ¬gt = next (record {root = just x ; nodeStack = st }) {!!} -- ( fni-Last ? )
-    ... | tri< lt ¬eq ¬gt = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 n0 (fni-Left x s1 tree ({!!}) (lproof x s1 )) )
-        where
-          nextInvaliant : ({!!})
-          nextInvaliant = {!!}
-          lproof : (x : Node a) → (s1 : SingleLinkedStack (Node a)) → findNodeLeft x s1 --→ (n0 : Node a)
-          lproof ns [] with left ns | right ns
-          lproof ns [] | just x | just x₁ = {!!}
-          lproof ns [] | just x | nothing =  {!!}
-          lproof ns [] | nothing | just x = {!!}
-          lproof ns [] | nothing | nothing = {!!}
-          lproof ns (x ∷ ss) = {!!}
+-- findNode1h : {n m  : Level } {a : Set n} {t : Set m}  → (tree : RedBlackTree {n} a )  → (Node a )
+--      → ((new : RedBlackTree {n} a) →  FindNodeInvariant (nodeStack new) tree → t )
+--      → ( FindNodeInvariant (nodeStack tree)  tree) → t
+-- findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) n0 prev
+--   module FindNodeH where
+--     findNode2h : (Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → Node a → FindNodeInvariant s tree  → t
+--     findNode2h nothing st n0 prev = next record { root = nothing ; nodeStack = st } prev
+--     findNode2h (just x) st n0 prev with <-cmp (key n0) (key x)
+--     ... | tri≈ ¬lt eq ¬gt = next (record {root = just x ; nodeStack = st }) prev -- ( fni-Last ? )
+--     ... | tri< lt ¬eq ¬gt = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 n0 (fni-Left x s1 tree ({!!}) (lproof x s1 )) )
+-- b        where
+--           nextInvaliant : (t)
+--           nextInvaliant = next tree {!!}
+--           lproof : (x : Node a) → (s1 : SingleLinkedStack (Node a)) → findNodeLeft x s1 --→ (n0 : Node a)
+--           lproof ns [] with left ns | right ns
+--           lproof ns [] | just x | just x₁ = {!!}
+--           lproof ns [] | just x | nothing =  {!!}
+--           lproof ns [] | nothing | just x = {!!}
+--           lproof ns [] | nothing | nothing = record { proj1 = refl ; proj2 = refl }
+--           lproof ns (x ∷ ss) = {!!}
 
-    ... | tri> ¬lt ¬eq gt = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 n0 (fni-Right x s1 tree ({!!}) {!!}) )
+--     ... | tri> ¬lt ¬eq gt = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 n0 (fni-Right x s1 tree ({!!}) {!!}) )
 
 
 -- replaceNodeH : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → {!!} → t) → {!!} → t