# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1681121734 -32400
# Node ID 0786c97b49190b7951baacd2e13f7be75c37c713
# Parent  fd63d70310c3e1d310236ac8ef10326b6a9a8219
...

diff -r fd63d70310c3 -r 0786c97b4919 hoareRedBlackTree.agda
--- a/hoareRedBlackTree.agda	Mon Apr 10 19:12:50 2023 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,644 +0,0 @@
-
-module hoareRedBlackTree 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
-
-
-
-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
-    getImpl  : treeImpl → (treeImpl → Maybe a → t) → t
-open TreeMethods
-
-record Tree  {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
-  field
-    tree : treeImpl
-    treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
-  putTree : a → (Tree treeImpl → t) → t
-  putTree d next = putImpl (treeMethods ) tree d (\t1 → next (record {tree = t1 ; treeMethods = treeMethods} ))
-  getTree : (Tree treeImpl → Maybe a → t) → t
-  getTree next = getImpl (treeMethods ) tree (\t1 d → next (record {tree = t1 ; treeMethods = treeMethods} ) d )
-
-open Tree
-
-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)
-
-data Color {n : Level } : Set n where
-  Red   : Color
-  Black : Color
-
-record Node {n : Level } (a : Set n) : Set n where
-  inductive
-  field
-    key   : ℕ
-    value : a
-    right : Maybe (Node a )
-    left  : Maybe (Node a )
-    color : Color {n}
-open Node
-
-record RedBlackTree {n : Level } (a : Set n) : Set n where
-  field
-    root : Maybe (Node a )
-    nodeStack : SingleLinkedStack  (Node a )
-
-
-open RedBlackTree
-
--- record datum {n : Level} (a : Set n) : Set n where
---   field
---     key : ℕ
---     val : 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 = {!!}
-
-
-
---- 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)をつくる
---}
-
-
-{-- 思いつき
- 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
-
-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₂) = {!!}
-
-
-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))
-
-
-{-- 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 {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)
-
-
--- 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 = {!!}
-
-
-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))) ))
-
-
-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₂
-
-
-
-
--- 何らかの集合のサイズが減っていれば良い…？
-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)
-
-
-
-
--- 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)
-
-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
-
-
-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)
-
--- {--
---   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) ∷ []
-
-
--- -- 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
-
--- -- 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))))
-
--- -- -- 末
--- -- 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
--- find-lemma tt@(node tr datum tr₁) ke st nt | tri< a ¬b ¬c = find-lemma tr ke (tt ∷ st) nt
--- find-lemma tt@(node tr datum tr₁) ke st nt | tri≈ ¬a b ¬c = nt tt st
--- find-lemma tt@(node tr datum tr₁) ke st nt | tri> ¬a ¬b c = find-lemma tr₁ ke (tt ∷ st) nt
-
-----
--- find node potition to insert or to delete, the path will be in the stack
---
-
-{-# TERMINATING #-}
-findNode : {n m  : Level } {a : Set n} {t : Set m} → RedBlackTree {n}  a  → (Node a ) → (RedBlackTree {n}  a → t) → t
-findNode {n} {m} {a}  {t} tree n0 next with root tree
-findNode {n} {m} {a}  {t} tree n0 next | nothing = next tree
-findNode {n} {m} {a}  {t} tree n0 next | just x with <-cmp (key x) (key n0)
-findNode {n} {m} {a}  {t} tree n0 next | just x | tri≈ ¬a b ¬c = next tree
-findNode {n} {m} {a}  {t} tree n0 next | just x | tri< a₁ ¬b ¬c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (left x) ; nodeStack = s}) n0 next)
-findNode {n} {m} {a}  {t} tree n0 next | just x | tri> ¬a ¬b c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (right x) ; nodeStack = s}) n0 next)
-
-
-
-findNode1 : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → t) → t
-findNode1 {n} {m} {a} {t} tree n0 next = findNode2 (root tree) (nodeStack tree)
-  module FindNode where
-    findNode2 : (Maybe (Node a )) → SingleLinkedStack (Node a ) → t
-    findNode2 nothing st = next record { root = nothing ; nodeStack = st }
-    findNode2 (just x) st with <-cmp (key n0) (key x)
-    ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st })
-    ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2 (right x) s1)
-    ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2 (left x) s1)
-
-node001 : Node  ℕ
-node001 = record { key = 2 ; value = 3 ; left = nothing ; right = nothing ; color = Black }
-node002 : Node  ℕ
-node002 = record { key = 1 ; value = 3 ; left = just node001 ; right = nothing ; color = Black }
-node003 : Node  ℕ
-node003 = record { key = 0 ; value = 3 ; left = just node002 ; right = nothing ; color = Black }
-
-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 )
-test003 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } )
-   node001 ( λ tree → tree )
-test004 = findNode {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } )
-   node001 ( λ tree → tree )
-
-replaceNode : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → t) → t
-replaceNode {n} {m} {a} {t} tree n0 next = replaceNode2 (nodeStack tree) (λ newNode → next record { root = just newNode ; nodeStack = emptySingleLinkedStack } )
-  module FindNodeR where
-      replaceNode1 : (Maybe (Node a )) → Node a
-      replaceNode1 nothing  = record n0 { left = nothing ; right = nothing  }
-      replaceNode1 (just x)  = record n0 { left = left x ; right = right x }
-      replaceNode2 : SingleLinkedStack (Node a ) → (Node a  → t)  → t
-      replaceNode2 [] next = next ( replaceNode1 (root tree) )
-      replaceNode2 (x ∷ st) next with <-cmp (key x) (key n0)
-      replaceNode2 (x ∷ st) next | tri< a ¬b ¬c = replaceNode2 st ( λ new → next ( record x { left = left new } ) )
-      replaceNode2 (x ∷ st) next | tri≈ ¬a b ¬c = replaceNode2 st ( λ new → next ( record x { left = left new ; right = right new } ) )
-      replaceNode2 (x ∷ st) next | tri> ¬a ¬b c = replaceNode2 st ( λ new → next ( record x { right = right new } ) )
-
-insertNode : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → t) → t
-insertNode tree n0 next = findNode1 tree n0 ( λ new → replaceNode tree n0 next )
-
-createEmptyRedBlackTreeℕ : {n m  : Level} {t : Set m} (a : Set n) (b : ℕ)
-     → RedBlackTree {n}  a
-createEmptyRedBlackTreeℕ a b = record {
-        root = nothing
-     ;  nodeStack = emptySingleLinkedStack
-   }
-
-findNodeLeft : {n  : Level } {a : Set n}  (r : Node a ) (t : SingleLinkedStack (Node a))  → Set n
-findNodeLeft x [] =  (left x ≡ nothing ) ∧ (right x ≡ nothing )
-findNodeLeft {n} x (h ∷ t) = Lift n ((key x) < (key h)) -- stack の top と比較するのはたぶん replace ...?
-
-findNodeRight : {n  : Level } {a : Set n}  (r : Node a ) (t : SingleLinkedStack (Node a))  → Set n
-findNodeRight x [] =  (left x ≡ nothing ) ∧ (right x ≡ nothing )
-findNodeRight {n} x (h ∷ t) = Lift n ((key x) > (key h))
-
-data FindNodeInvariant {n : Level } {a : Set n} : (t : SingleLinkedStack (Node a)) (node :  Maybe (Node a) ) → Set n where
-   fni-stackEmpty  : (now :  Maybe (Node a) ) → FindNodeInvariant [] now 
-   fni-treeEmpty  : (st : SingleLinkedStack (Node a))  → FindNodeInvariant st nothing
-   fni-Left  : (x : Node a) (st : SingleLinkedStack (Node a)) (node :  Maybe (Node a ))
-      →  FindNodeInvariant ( x ∷ st ) node → findNodeLeft x st →  FindNodeInvariant st node
-   fni-Right  : (x : Node a) (st : SingleLinkedStack (Node a)) (node :  Maybe (Node a ))
-      →  FindNodeInvariant ( x ∷ st ) node → findNodeRight x st →  FindNodeInvariant st node 
-findNodeLoop : {n  : Level } {a : Set n}  (r : Node a ) (t : SingleLinkedStack (Node a))  → Set n
-findNodeLoop x st = ((findNodeRight x st) ∨ (findNodeLeft x st))
-
-findNode1h : {n m  : Level } {a : Set n} {t : Set m}  → (tree : RedBlackTree {n} a )  → (Node a )
-     → ((new : RedBlackTree {n} a) →  FindNodeInvariant (nodeStack new) (root new ) → t ) 
-     → ( FindNodeInvariant (nodeStack tree)  (root tree) ) → t
-findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) prev
-  module FindNodeH where
-    findNode2h : (new : Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → FindNodeInvariant s new → t
-    findNode2h nothing st prev = next record { root = nothing ; nodeStack = st } prev
-    findNode2h (just x) st prev with <-cmp (key n0) (key x)
-    ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st }) prev
-    ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 (fni-Left x s1 {!!} {!!} {!!}) )
-    ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 (fni-Right x s1 {!!} {!!} {!!}) )
-
-
--- replaceNodeH : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → {!!} → t) → {!!} → t
--- replaceNodeH = {!!}
diff -r fd63d70310c3 -r 0786c97b4919 redBlackTreeTest.agda
--- a/redBlackTreeTest.agda	Mon Apr 10 19:12:50 2023 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,486 +0,0 @@
-module redBlackTreeTest where
-
-open import Level hiding (zero) renaming ( suc to succ )
-
-open import Data.Empty
-open import Data.List
-open import Data.Maybe
-open import Data.Bool
-open import Data.Nat
-open import Data.Nat.Properties  as NatProp
-
-open import Relation.Nullary
-open import Relation.Binary
-
-open import Algebra
-
-open import RedBlackTree
-open import stack
-
-open Tree
-open Node
-open RedBlackTree.RedBlackTree
-open Stack
-
--- tests
-
-putTree1 : {n m : Level } {a k : Set n} {t : Set m} → RedBlackTree {n} {m} {t} a k → k → a → ((RedBlackTree {n} {m} {t} a k) → t) → t
-putTree1 {n} {m} {a} {k} {t} tree k1 value next with (root tree)
-...                                | nothing = next (record tree {root = just (leafNode k1 value) })
-...                                | just n2  = clearSingleLinkedStack (nodeStack tree) (λ  s → findNode tree s (leafNode k1 value) n2 (λ  tree1 s n1 → replaceNode tree1 s n1 next))
-
-open import Relation.Binary.PropositionalEquality
-open import Relation.Binary.Core
-open import Function
-
-
--- check1 : {m : Level } (n : Maybe (Node  ℕ ℕ)) → ℕ → Bool
--- check1 nothing _ = false
--- check1 (just n)  x with Data.Nat.compare (value n)  x
--- ...  | equal _ = true
--- ...  | _ = false
-
-check2 : {m : Level } (n : Maybe (Node  ℕ ℕ)) → ℕ → Bool
-check2 nothing _ = false
-check2 (just n)  x with compare2 (value n)  x
-...  | EQ = true
-...  | _ = false
-
-test1 : {m : Level} {A B C : Set} → putTree1 {Level.zero} {succ Level.zero} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ {!!} {!!} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 {m} x 1 ≡ true ))
-test1 = {!!}
-
--- test2 : {m : Level} → putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
---     λ t → putTree1 t 2 2 (
---     λ t → getRedBlackTree t 1 (
---     λ t x → check2 {m} x 1 ≡ true   )))
--- test2 = refl
-
--- open ≡-Reasoning
--- test3 : {m : Level} → putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1
---     $ λ t → putTree1 t 2 2
---     $ λ t → putTree1 t 3 3
---     $ λ t → putTree1 t 4 4
---     $ λ t → getRedBlackTree t 1
---     $ λ t x → check2 {m} x 1 ≡ true
--- test3 {m} = begin
---     check2 {m} (just (record {key = 1 ; value = 1 ; color = Black ; left = nothing ; right = just (leafNode 2 2)})) 1
---   ≡⟨ refl ⟩
---     true
---   ∎
-
--- test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1
---     $ λ t → putTree1 t 2 2
---     $ λ t → putTree1 t 3 3
---     $ λ t → putTree1 t 4 4
---     $ λ t → getRedBlackTree t 4
---     $ λ t x → x
-
--- -- test5 : Maybe (Node ℕ ℕ)
--- test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4
---     $ λ t → putTree1 t 6 6
---     $ λ t0 →  clearSingleLinkedStack (nodeStack t0)
---     $ λ s → findNode1 t0 s (leafNode 3 3) ( root t0 )
---     $ λ t1 s n1 → replaceNode t1 s n1
---     $ λ t → getRedBlackTree t 3
---     -- $ λ t x → SingleLinkedStack.top (stack s)
---     -- $ λ t x → n1
---     $ λ t x → root t
---   where
---      findNode1 : {n m : Level } {a k : Set n} {t : Set m} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → (Node a k) → (Maybe (Node a k)) → (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → t) → t
---      findNode1 t s n1 nothing next = next t s n1
---      findNode1 t s n1 ( just n2 ) next = findNode t s n1 n2 next
-
--- -- test51 : putTree1 {_} {_} {ℕ} {ℕ} {_} {Maybe (Node ℕ ℕ)} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ λ t →
--- --   putTree1 t 2 2 $ λ t → putTree1 t 3 3 $ λ t → root t ≡ just (record { key = 1; value = 1; left = just (record { key = 2 ; value = 2 } ); right = nothing} )
--- -- test51 = refl
-
--- test6 : Maybe (Node ℕ ℕ)
--- test6 = root (createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)})
-
-
--- test7 : Maybe (Node ℕ ℕ)
--- test7 = clearSingleLinkedStack (nodeStack tree2) (λ  s → replaceNode tree2 s n2 (λ  t → root t))
---   where
---     tree2 = createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)}
---     k1 = 1
---     n2 = leafNode 0 0
---     value1 = 1
-
--- test8 : Maybe (Node ℕ ℕ)
--- test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1
---     $ λ t → putTree1 t 2 2 (λ  t → root t)
-
-
--- test9 : {m : Level} → putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 {m} x 1 ≡ true   ))
--- test9 = refl
-
--- test10 : {m : Level} → putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
---     λ t → putRedBlackTree t 2 2 (
---     λ t → getRedBlackTree t 1 (
---     λ t x → check2 {m} x 1 ≡ true   )))
--- test10 = refl
-
--- test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1
---     $ λ t → putRedBlackTree t 2 2
---     $ λ t → putRedBlackTree t 3 3
---     $ λ t → getRedBlackTree t 2
---     $ λ t x → root t
-
-
-compTri :  ( x y : ℕ ) ->  Tri  (x < y) ( x ≡ y )  ( x > y )
-compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder <-strictTotalOrder)
-   where open import  Relation.Binary
-
-checkT : {m : Level } (n : Maybe (Node  ℕ ℕ)) → ℕ → Bool
-checkT nothing _ = false
-checkT (just n) x with compTri (value n)  x
-...  | tri≈ _ _ _ = true
-...  | _ = false
-
-checkEQ :  {m : Level }  ( x :  ℕ ) -> ( n : Node  ℕ ℕ ) -> (value n )  ≡ x  -> checkT {m} (just n) x ≡ true
-checkEQ x n refl with compTri (value n)  x
-... |  tri≈ _ refl _ = refl
-... |  tri> _ neq gt =  ⊥-elim (neq refl)
-... |  tri< lt neq _ =  ⊥-elim (neq refl)
-
--- checkEQ' :  {m : Level }  ( x y :  ℕ ) -> ( eq : x ≡ y  ) -> ( x ≟ y ) ≡ yes eq
--- checkEQ' x y refl with  x ≟ y
--- ... | yes refl = refl
--- ... | no neq = ⊥-elim ( neq refl )
-
----  search -> checkEQ
----  findNode -> search
-
-redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} {A B C : Set Level.zero } → RedBlackTree {Level.zero} {m} {t} {A} {B} {C} a ℕ
-redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; nodeComp = λ x x₁ → {!!} } -- record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compTri }
-
-
-open stack.SingleLinkedStack
-open stack.Element
-
-
-insertP :  { a : Set } { t : Set } {P : Set }   → ( f : ( a  → t )  → t )  ( g : a  → t ) ( g' :  P  → a  → t )
-   → ( p : P )
-   → ( g ≡ g' p )
-   →  f ( λ x → g' p x ) ≡ f ( λ x → g x )  
-insertP f g g' p refl = refl
-
-
-{-# TERMINATING #-}
-inStack : {l : Level} (n : Node ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → Bool
-inStack {l} n s with ( top s )
-... | nothing = true
-... | just n1 with  compTri (key n) (key (datum n1))
-...            | tri> _ neq _ =  inStack {l} n ( record { top = next n1 } )
-...            | tri< _ neq _ =  inStack {l} n ( record { top = next n1 } )
-...            | tri≈  _ refl _  = false
-
-record StackTreeInvariant  ( n : Node ℕ ℕ )
-<<<<<<< working copy
-        ( s : SingleLinkedStack (Node  ℕ ℕ) )  : Set where
-||||||| base
-        ( s : SingleLinkedStack (Node  ℕ ℕ) ) ( t : RedBlackTree ℕ ℕ ) : Set where
-=======
-        ( s : SingleLinkedStack (Node ℕ ℕ) ) ( t : RedBlackTree ℕ ℕ ) : Set where
->>>>>>> destination
-  field
-<<<<<<< working copy
-    -- sti : replaceNode t s n $ λ  t1 → getRedBlackTree t1 (key n) (λ  t2 x1 → checkT x1 (value n)  ≡ True)
-    notInStack : inStack n s ≡ True  → ⊥
-||||||| base
-    sti : replaceNode t s n $ λ  t1 → getRedBlackTree t1 (key n) (λ  t2 x1 → checkT x1 (value n)  ≡ True)
-    notInStack : inStack n s ≡ True  → ⊥
-=======
-    sti : {m : Level} → replaceNode t s n $ λ  t1 → getRedBlackTree t1 (key n) (λ  t2 x1 → checkT {m} x1 (value n)  ≡ true)
-    notInStack : {m : Level} → inStack {m} n s ≡ true  → ⊥
->>>>>>> destination
-
-open StackTreeInvariant
-
-<<<<<<< working copy
-putTest1 : (n : Maybe (Node ℕ ℕ))
-         → (k : ℕ) (x : ℕ)
-         → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
-           (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True)) 
-putTest1 n k x with n
-...  | Just n1 = lemma0
-   where
-     tree0 : (n1 : Node  ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → RedBlackTree ℕ ℕ
-     tree0 n1 s = record { root = Just n1 ; nodeStack = s ; compare = compareT }
-     lemma2 : (n1 : Node  ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → StackTreeInvariant (leafNode k x) s 
-         → findNode (tree0 n1 s) s (leafNode k x) n1 (λ  tree1 s n1 → replaceNode tree1 s n1
-              (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True)))
-     lemma2 n1 s STI with compTri k (key n1)
-     ... |  tri> le eq gt with (right n1) 
-     ...                  | Just rightNode = {!!} -- ( lemma2 rightNode  ( record { top = Just ( cons n1 (top s)  ) }   )  (record {notInStack = {!!}  } ) )
-     ...                  | Nothing with compTri k k
-     ...                           | tri≈  _ refl _ = {!!}
-     ...                           | tri< _ neq _ =  ⊥-elim (neq refl)
-     ...                           | tri> _ neq _ =  ⊥-elim (neq refl)
-     lemma2 n1 s STI |  tri< le eq gt = {!!}
-     lemma2 n1 s STI |  tri≈ le refl gt = lemma5 s ( tree0 n1 s ) n1
-        where 
-           lemma5 :  (s : SingleLinkedStack (Node ℕ ℕ) )  → ( t :  RedBlackTree  ℕ ℕ  ) → ( n :  Node ℕ ℕ  ) → popSingleLinkedStack ( record { top = Just (cons n (SingleLinkedStack.top s)) }  )
-                   ( \ s1  _ -> (replaceNode (tree0 n1 s1) s1 (record n1 { key = k ; value = x } ) (λ t → 
-                      GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t))) )
-           lemma5 s t n with (top s)
-           ...          | Just n2  with compTri k k
-           ...            | tri< _ neq _ =  ⊥-elim (neq refl)
-           ...            | tri> _ neq _ =  ⊥-elim (neq refl)
-           ...            | tri≈  _ refl _  =  ⊥-elim ( (notInStack STI)  {!!} )
-           lemma5 s t n | Nothing with compTri k k
-           ...            | tri≈  _ refl _  = checkEQ x _ refl
-           ...            | tri< _ neq _ =  ⊥-elim (neq refl)
-           ...            | tri> _ neq _ =  ⊥-elim (neq refl)
-     lemma0 : clearSingleLinkedStack (record {top = Nothing}) (\s → findNode (tree0 n1 s) s (leafNode k x) n1 (λ  tree1 s n1 → replaceNode tree1 s n1
-              (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True))))
-     lemma0 = lemma2 n1 (record {top = Nothing}) ( record { notInStack = {!!} } )
-...  | Nothing = lemma1  
-   where 
-     lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
-               key   = k ; value = x ; right = Nothing ; left  = Nothing ; color = Red } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compareT x₁ y  } ) k
-        ( λ  t x1 → checkT x1 x  ≡ True) 
-     lemma1 with compTri k k 
-     ... | tri≈  _ refl _ = checkEQ x _ refl
-     ... | tri< _ neq _ =  ⊥-elim (neq refl)
-     ... | tri> _ neq _ =  ⊥-elim (neq refl)
-||||||| base
-putTest1 : (n : Maybe (Node ℕ ℕ))
-         → (k : ℕ) (x : ℕ)
-         → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
-           (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True)) 
-putTest1 n k x with n
-...  | Just n1 = lemma0
-   where
-     tree0 : (s : SingleLinkedStack (Node ℕ ℕ) ) → RedBlackTree ℕ ℕ
-     tree0 s = record { root = Just n1 ; nodeStack = s ; compare = compareT }
-     lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) → StackTreeInvariant (leafNode k x) s (tree0 s)
-         → findNode (tree0 s) s (leafNode k x) n1 (λ  tree1 s n1 → replaceNode tree1 s n1
-              (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True)))
-     lemma2 s STI with compTri k (key n1)
-     ... |  tri≈ le refl gt = lemma5 s ( tree0 s ) n1
-        where 
-           lemma5 :  (s : SingleLinkedStack (Node ℕ ℕ) )  → ( t :  RedBlackTree  ℕ ℕ  ) → ( n :  Node ℕ ℕ  ) → popSingleLinkedStack ( record { top = Just (cons n (SingleLinkedStack.top s)) }  )
-                   ( \ s1  _ -> (replaceNode (tree0 s1) s1 (record n1 { key = k ; value = x } ) (λ t → 
-                      GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t))) )
-           lemma5 s t n with (top s)
-           ...          | Just n2  with compTri k k
-           ...            | tri< _ neq _ =  ⊥-elim (neq refl)
-           ...            | tri> _ neq _ =  ⊥-elim (neq refl)
-           ...            | tri≈  _ refl _  =  ⊥-elim ( (notInStack STI)  {!!} )
-           lemma5 s t n | Nothing with compTri k k
-           ...            | tri≈  _ refl _  = checkEQ x _ refl
-           ...            | tri< _ neq _ =  ⊥-elim (neq refl)
-           ...            | tri> _ neq _ =  ⊥-elim (neq refl)
-     ... |  tri> le eq gt = sti ( record { sti = {!!} ; notInStack = {!!}  } )
-     ... |  tri< le eq gt = {!!}
-     lemma0 : clearSingleLinkedStack (record {top = Nothing}) (\s → findNode (tree0 s) s (leafNode k x) n1 (λ  tree1 s n1 → replaceNode tree1 s n1
-              (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True))))
-     lemma0 = lemma2 (record {top = Nothing}) ( record { sti = {!!}  ; notInStack = {!!} } )
-...  | Nothing = lemma1  
-   where 
-     lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
-               key   = k ; value = x ; right = Nothing ; left  = Nothing ; color = Red } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compareT x₁ y  } ) k
-        ( λ  t x1 → checkT x1 x  ≡ True) 
-     lemma1 with compTri k k 
-     ... | tri≈  _ refl _ = checkEQ x _ refl
-     ... | tri< _ neq _ =  ⊥-elim (neq refl)
-     ... | tri> _ neq _ =  ⊥-elim (neq refl)
-=======
-
--- testn :  {!!}
--- testn  =  putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 2 2
---   $ λ t → putTree1 t 1 1
---   $ λ t → putTree1 t 3 3 (λ ta → record {root = root ta ; nodeStack = nodeStack ta })
-
-
--- List と Node で書こうとしたがなんだかんだListに直したほうが楽そうだった
-
-nullNode = (record {key = 0 ; value = 0 ; right = nothing ; left = nothing ; color = Red})
-
--- treeTotal : { m : Level } {t : Set m} → ( s : List ℕ ) → ( tr : (Node ℕ ℕ) ) → (List ℕ → t) → t
--- treeTotal {m} {t} s tr next with (left tr) | (right tr)
--- treeTotal {m} {t} s tr next | nothing | nothing = next ((key tr) ∷ [])
--- treeTotal {m} {t} s tr next | nothing | just x = treeTotal {m} {t} s x (λ li → next ((key tr) ∷ li))
--- treeTotal {m} {t} s tr next | just x | nothing = treeTotal {m} {t} s x (λ li → next ((key tr) ∷ li))
--- treeTotal {m} {t} s tr next | just x | just x₁ = treeTotal {m} {t} s x (λ li1 → treeTotal {m} {t} s x₁ (λ li2 → next (s ++ li1 ++ li2)))
-treeTotal : { n m : Level } {a : Set n} {t : Set m} → ( s : List a ) → ( tr : (Node a a) ) → List a
-treeTotal {n} {m} {a} {t} s tr with (left tr) | (right tr)
-treeTotal {n} {m} {a} {t} s tr | nothing | nothing = (key tr) ∷ []
-treeTotal {n} {m} {a} {t} s tr | nothing | just x = (key tr) ∷ (treeTotal {n} {m} {a} {t} s x)
-treeTotal {n} {m} {a} {t} s tr | just x | nothing = (key tr) ∷ (treeTotal {n} {m} {a} {t} s x)
-treeTotal {n} {m} {a} {t} s tr | just x | just x₁ = s ++ ((key tr) ∷ (treeTotal {n} {m} {a} {t} s x) ++ (treeTotal {n} {m} {a} {t} s x₁))
-
-
--- treeTotalA : { m : Level } {t : Set m} → ( s : List ℕ ) → ( tr : (Node ℕ ℕ) ) → List ℕ
-
--- (treeTotal {_} {ℕ} ([]) (Data.Maybe.fromMaybe nullNode (root (putTree1 {_} {_} {ℕ} {ℕ} testn 5 5 {!!}))))
-
--- exput : (treeTotal {_} {ℕ} (5 ∷ []) (Data.Maybe.fromMaybe nullNode (root (createEmptyRedBlackTreeℕ ℕ))) (λ total → {!!})) ≡ {!!}
--- exput = {!!}
-
-
--- aaa = (treeTotal {_} {_} {ℕ} {_} (5 ∷ []) ((record { key = 4 ; value = 4 ; right = just (leafNode 6 6) ; left = just (leafNode 3 3) ; color = Black })))
-
-
--- fuga = putTree1 {_} {_} {ℕ} {ℕ} (record {root = just (record { key = 4 ; value = 4 ; right = just (leafNode 6 6) ; left = just (leafNode 3 3) ; color = Black }) ; nodeStack = ( record {top = nothing}) ; compare = (λ x x₁ → EQ) }) 5 5 (λ aaa → aaa )
-
--- nontree ++ 2 :: []
-
--- piyo =  putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 2 2 ( λ t1 → findNode t1 (record {top = nothing}) (leafNode 2 2) (Data.Maybe.fromMaybe nullNode (root t1)) (λ tree stack node → {!!}))
-
-
--- exn2l : {!!} ≡ (treeTotal {_} {ℕ} ([]) (putTree1 {_} {_} {ℕ} {ℕ} {!!} 5 5 (λ t → {!!}))) -- (treeTotal {_} {ℕ} (5 ∷ []) (Data.Maybe.fromMaybe nullNode (root testn)))
--- exn2l = refl
-
-
-
-
-
--- record FS {n m : Level } {a : Set n} {t : Set m} (oldTotal : List a) ( s : List a ) ( tr : (Node a a) ) : Set where
---   field
---     total : treeTotal {n} {m} {a} {t} s tr ≡ oldTotal
--- -- usage = FS.total -- relation
-
--- data P { n m : Level } { t : Set m } : Set where
---   P₀ : (old : List ℕ) ( s : List ℕ ) → (tr : (Node ℕ ℕ) ) → FS {m} {t} old s tr → P
-
-
-
--- ttt = putTree1 {_} {_} {ℕ} {ℕ}
-
--- record TreeInterface {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set n where
---   field
---     tree : treeImpl
---     list : List ℕ
---     node : Node ℕ ℕ
---     putTreeHoare : (FS {_} {ℕ} list list node) → putTree1 {!!} {!!} {!!} {!!}
-
-stack2list : {n m : Level} {t : Set m} {a : Set n} → (s : SingleLinkedStack a) → List a
-stack2list stack with top stack
-stack2list stack | just x = (datum x) ∷ (elm2list {_} {_} {ℕ} x)
-  where
-    elm2list : {n m : Level} {t : Set m} {a : Set n} → (elm : (Element a)) → List a
-    elm2list el with next el
-    elm2list el | just x = (datum el) ∷ (elm2list {_} {_} {ℕ} x)
-    elm2list el | nothing = (datum el) ∷ []
-stack2list stack | nothing = []
-
-
--- list2element : {n m : Level} {t : Set m} {a : Set n} → (l : List a) → Maybe (Element a)
--- list2element [] = nothing
--- list2element (x ∷ l) = just (cons x (list2element {_} {_} {ℕ} l))
-
--- ltest = list2element (1 ∷ 2 ∷ 3 ∷ [])
-
-list2stack : {n m : Level} {t : Set m} {a : Set n} {st : SingleLinkedStack a} → (l : List a)  → SingleLinkedStack a
-list2stack {n} {m} {t} {a} {s} (x ∷ l)  = pushSingleLinkedStack s x (λ s1 → list2stack {n} {m} {t} {a} {s1} l )
-list2stack {n} {m} {t} {a} {s} [] = s
-
-
-
--- stest = list2stack (1 ∷ 2 ∷ 3 ∷ [])
-
-open Node
-
-exfind : { m : Level } { t : Set m} → (dt : ℕ) → (node : (Node ℕ ℕ))  → (st : List ℕ) →  findNode {_} {_} {ℕ} {ℕ} (redBlackInSomeState ℕ (just node)) (emptySingleLinkedStack) (leafNode dt dt) (node) (λ t1 st1 n1 → (( treeTotal {_} {m} {ℕ} {t} (dt ∷ st) (node) ) ≡ ( treeTotal {_} {m} {ℕ} {t} (dt ∷ st) (node) ) ))
-exfind dt node st with left node | right node
-exfind dt node st | just x | just x₁ = {!!}
-exfind dt node st | just x | nothing = {!!}
-exfind dt node st | nothing | just x = {!!}
-exfind dt node st | nothing | nothing with (compTri dt (key node))
-exfind dt node st | nothing | nothing | tri< a ¬b ¬c = {!!}
-exfind dt node st | nothing | nothing | tri≈ ¬a b ¬c = {!!}
-exfind dt node st | nothing | nothing | tri> ¬a ¬b c = {!!}
-
--- exput : (ni : ℕ) → (tn : Node ℕ ℕ) → (ts : List ℕ) → (treeTotal {_} {ℕ} (ni ∷ ts) tn)
---                  ≡ (treeTotal {_} {ℕ} (ts) (Data.Maybe.fromMaybe nullNode (root (putTree1 {_} {_} {ℕ} {ℕ} (record { root = just tn } ) ni ni (λ tt → tt)))))
--- exput datum node [] with (right node) | (left node)
--- exput datum node [] | nothing | nothing = {!!}
--- exput datum node [] | just x | just x₁ = {!!}
--- exput datum node [] | just x | nothing = {!!}
--- exput datum node [] | nothing | just x = {!!}
--- exput datum node (x ∷ stack₁) = {!!}
-
-
--- proofTree : {n m : Level} {t : Set m} {a : Set n} (old stackl : List ℕ) → (node : Node ℕ ℕ) → (FS {_} {ℕ} old stackl node) → (tree : RedBlackTree ℕ ℕ) → (key : ℕ) → findNode  {{!!}} {{!!}} {{!!}} {{!!}} tree (list2stack {!!} (record {top = nothing})) (leafNode key key) node (λ tree1 stack1 datum → {!!})
--- -- -- -- putTree1 tree key key (λ t → (FS {_} {ℕ} old stackl (Data.Maybe.fromMaybe nullNode (root tree))) )
--- proofTree old stack node fs t k = {!!}
-
--- FS は 証明そのものになると思ってたけど実は違いそう
--- oldTotal と 現在の node, stack の組み合わせを比較する
--- oldTotal はどうやって作る? ><
--- treeTotal は list と node を受け取って それの total を出すのでそれで作る(list に put するデータなどを入れることで適当に作れる)
-
--- p : {n m : Level} {t : Set m} {a : Set n} → ( s : SingleLinkedStack ℕ )  ( tr : (Node ℕ ℕ) ) ( tree : RedBlackTree ℕ ℕ ) (k : ℕ) →  (FS (treeTotal (k ∷ (stack2list s)) tr) (stack2list s) tr) → putTree1 tree k k (λ atree  → FS (treeTotal (stack2list s) (Data.Maybe.fromMaybe (tr) (root atree))) {!!} {!!})
--- p stack node tree key = {!!}
-
--- tt = (FS {_} {ℕ} [] [] (Data.Maybe.fromMaybe nullNode (root (createEmptyRedBlackTreeℕ {_} ℕ {ℕ}))))
-
--- ttt : (a : P) → P
--- ttt a = P₀ {!!} {!!} (record { key = {!!} ; value = {!!} ; right = {!!} ; left = {!!} ; color = {!!} }) (record { total = {!!} })
-
-
--- FS では stack tree をあわせた整合性を示したい
--- そのためには...?
--- stack は前の node (というか一段上)が入ってる
--- tree は現在の node がある
-
-
- --   tr(Node ℕ ℕ)      s (List (Node))
- --     3                  []
- --    / \
- --   2   5
- --  /   / \
- -- 1   4   6
-
- --   search 6 (6 > 3)
- --   tr(Node ℕ ℕ)      s (List (Node))
- --     5                 just (node (1 2 nothing) 3 (4 5 6)
- --    / \                 []
- --   4   6
-
---   search 6 (6 > 5)
---   tr(Node ℕ ℕ)      s (List (Node))
---       6              just (node (4 5 6))
---                      just (node (1 2 nothing) 3 (4 5 6)
---                       []
-
--- just 6 → true みたいな感じ
-
--- stack に node ごと入れるのは間違い…？
--- 一応非破壊な感じがする(新しく作り直してる)
--- どう釣り合いをとるか
-
--- stack+tree : {n m : Level} {t : Set m} → List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → (Maybe (Node ℕ ℕ) → t) → t
--- stack+tree {n} stack mid org = st stack mid org where
--- st : List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → Maybe (Node ℕ ℕ)
--- st [] _ _ = nothing
--- st (x ∷ []) n n1 with Data.Nat.compare (key x) (key org) | Data.Nat.compare (value x) (value org)
--- st (x ∷ []) n n1 | equal .(key x) | equal .(value x) = just org
--- st (x ∷ []) n n1 | _ | _ = nothing
--- st (x ∷ a)  n n1 with st a n n1
--- st (x ∷ a) n n1 | just x₁ = {!!}
--- st (x ∷ a) n n1 | nothing = nothing
-
-
--- stack+tree : {n m : Level} {t : Set m} → List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → (Maybe (Node ℕ ℕ) → t) → t
--- stack+tree {n} stack mid org cg = st stack mid org
---   where
---            st : List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → Maybe (Node ℕ ℕ)
---            st [] _ _ = nothing
---            st (x ∷ []) n n1 with Data.Nat.compare (key x) (key org) | Data.Nat.compare (value x) (value org)
---            st (x ∷ []) n n1 | equal .(key x) | equal .(value x) = just org
---            st (x ∷ []) n n1 | _ | _ = nothing
---            st (x ∷ a)  n n1 with st a n n1
---            st (x ∷ a) n n1 | just x₁ = {!!}
---            st (x ∷ a) n n1 | nothing = nothing
-
--- findNodePush : {n : Level}  → (stack : List (Node ℕ ℕ)) → (mid : Node ℕ ℕ) → (org : Node ℕ ℕ) → stack+tree stack mid org ≡ just ?
---                → ? {return (? ∷ stack),mid'} → stack+tree (? ∷ stack) (mid') org ≡ just ?
--- findNodePush 
-
--- stack+tree が just だって言えたらよい
--- {}2 は orig の どっちかのNode
-
->>>>>>> destination