--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/.hgignore	Mon May 13 19:54:15 2019 +0900
@@ -0,0 +1,18 @@
+syntax: glob
+.DS_Store
+*.swp
+*.o
+*.agdai
+
+# CMake
+CMakeCache.txt
+CMakeFiles
+CMakeScripts
+Makefile
+cmake_install.cmake
+install_manifest.txt
+
+# binary
+src/llrb/llrb
+src/llrb/llrb_with_put_verify
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/RBTree.agda	Mon May 13 19:54:15 2019 +0900
@@ -0,0 +1,474 @@
+open import Level renaming (suc to succ ; zero to Zero )
+module RBTree where
+
+-- {
+-- RBTree,
+-- Node,
+-- Color,
+-- hight,
+-- nulln,
+-- empty,
+-- singleton
+-- }
+
+open import Data.List
+open import Data.Maybe
+open import Data.Nat
+open import Data.Bool
+open import Data.Empty
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary
+open import Relation.Binary.Core
+open import Relation.Nullary
+-- open import Level
+
+-- Builtin Function
+
+_==_ :  ℕ → ℕ → Bool
+_==_ x y with compare x y
+(x == .(ℕ.suc (x + k))) | less .x k = false
+(x == .x) | equal .x = true
+(.(ℕ.suc (y + k)) == y) | greater .y k = false
+
+_-_ : ℕ → ℕ → ℕ
+ℕ.zero - ℕ.zero = ℕ.zero
+ℕ.zero - ℕ.suc y = ℕ.zero
+ℕ.suc x - ℕ.zero = ℕ.suc x
+ℕ.suc x - ℕ.suc y = x - y
+
+contraposition : {m : Level } {A B : Set m} → (B → A) → (¬ A → ¬ B)
+contraposition f = λ x y → x (f y)
+
+
+compareTri1 : (n : ℕ) → zero <′ suc n
+compareTri1 zero =   ≤′-refl
+compareTri1 (suc n) =  ≤′-step ( compareTri1 n )
+
+compareTri2 : (n m : ℕ) → n ≤′ m → suc n ≤′ suc m
+compareTri2 _ _  ≤′-refl = ≤′-refl
+compareTri2 n (suc m) ( ≤′-step p ) =  ≤′-step { suc n }  ( compareTri2 n m p )
+
+<′dec : Set
+<′dec = ∀ m n → Dec ( m ≤′ n )
+
+compareTri6 : ∀ m {n} → ¬ m ≤′ n →  ¬ suc m ≤′ suc n
+
+is≤′ :  <′dec
+is≤′  zero zero = yes ≤′-refl
+is≤′  zero (suc n) = yes (lemma n)
+  where
+     lemma :  (n : ℕ) → zero ≤′ suc n
+     lemma zero =   ≤′-step  ≤′-refl
+     lemma (suc n) =  ≤′-step (lemma n)
+is≤′  (suc m) (zero) = no ( λ () )
+is≤′  (suc m) (suc n) with is≤′ m n
+... | yes p = yes ( compareTri2 _ _ p )
+... | no p = no ( compareTri6 _ p )
+
+compareTri20 : {n : ℕ} → ¬ suc n ≤′ zero
+compareTri20 ()
+
+
+compareTri21 : (n m : ℕ) → suc n ≤′ suc m →  n ≤′ m
+compareTri21 _ _  ≤′-refl = ≤′-refl
+compareTri21 (suc n) zero ( ≤′-step p ) = compareTri23 (suc n) ( ≤′-step p ) p
+  where
+        compareTri23 : (n : ℕ) → suc n ≤′ suc zero → suc n ≤′ zero →  n ≤′ zero
+        compareTri23 zero ( ≤′-step p ) _ =   ≤′-refl
+        compareTri23 zero ≤′-refl _ =   ≤′-refl
+        compareTri23 (suc n1) ( ≤′-step p ) ()
+compareTri21 n (suc m) ( ≤′-step p ) = ≤′-step (compareTri21 _ _ p)
+compareTri21 zero zero ( ≤′-step p ) = ≤′-refl
+
+
+compareTri3 : ∀ m {n} → ¬ m ≡ suc (m + n)
+compareTri3 zero    ()
+compareTri3 (suc m) eq = compareTri3 m (cong pred eq)
+
+compareTri4' : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
+compareTri4' m {n} with n Data.Nat.≟ m
+... | yes refl  = λ x y → x refl
+... | no  p  = λ x y → p ( cong pred y )
+
+compareTri4 : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
+compareTri4 m = contraposition ( λ x → cong pred x )
+
+-- compareTri6 : ∀ m {n} → ¬ m ≤′ n →  ¬ suc m ≤′ suc n
+compareTri6  m {n} = λ x y → x (compareTri21 _ _ y)
+
+compareTri5 : ∀ m {n} → ¬ m <′ n →  ¬ suc m <′ suc n
+compareTri5  m {n}  = compareTri6 (suc m)
+
+
+compareTri :  Trichotomous  _≡_ _<′_
+compareTri zero zero = tri≈ ( λ ()) refl ( λ ())
+compareTri zero (suc n) = tri< ( compareTri1 n )  ( λ ()) ( λ ())
+compareTri (suc n) zero = tri> ( λ ()) ( λ ()) ( compareTri1 n )
+compareTri (suc n) (suc m) with compareTri n m
+... | tri< p q r = tri<  (compareTri2 (suc n) m p ) (compareTri4 _ q) ( compareTri5 _ r )
+... | tri≈ p refl r = tri≈ (compareTri5 _ p) refl ( compareTri5 _ r )
+... | tri> p q r = tri> ( compareTri5 _ p ) (compareTri4 _ q) (compareTri2 (suc m) n r )
+
+
+data Color : Set where
+  red : Color
+  black : Color
+
+record Node {a : Set} : Set where
+  inductive
+  field
+    color : Color
+    blackHeight : ℕ
+    right : Node {a}
+    datum : ℕ
+    left : Node {a}
+open Node
+
+-- node は node であり 部分的に分けられた redblacktree そのもの
+
+data RBTree {n : Level} (a : Set n) : Set n where
+    leaf : RBTree a
+    node : Color → ℕ → RBTree a → ℕ → RBTree a → RBTree a
+
+
+record RBTreeBDel {n : Level} (a : Set n) : Set n where
+  field
+    tree : RBTree a
+    bool : Bool
+open RBTreeBDel
+
+
+module _ { n m : Level} {a : Set n} {cg : Set m} where
+
+  -- _,_ : (tree : RBTree a) → (b : Bool) → Set
+  -- leaf , false = (leaf , false)
+  -- leaf , true = {!!}
+  -- (node x x₁ t x₂ t₁) , bb = {!!}
+
+
+  hight? : RBTree a → ℕ
+  hight? leaf = 0
+  hight? (node c h l x r) = h
+
+  isLeaf : RBTree a → Bool
+  isLeaf leaf = true
+  isLeaf (node x x₁ t x₂ t₁) = false
+
+  empty : RBTree a
+  empty = leaf
+
+  singleton : ℕ → RBTree a
+  singleton x = (node black 1 leaf x leaf)
+
+  isMember : ℕ → RBTree ℕ → Bool
+  isMember _ leaf = false
+  isMember x (node _ _ l y r) with compare x y
+  isMember x (node _ _ l y r) | less x k = isMember x l
+  isMember x (node _ _ l x r) | equal x = true
+  isMember x (node _ _ l y r) | greater y k = isMember x r
+
+  blacks? : RBTree a → ℕ
+  blacks? = blacks' 0
+    where
+      blacks' : ℕ → RBTree a → ℕ
+      blacks' n leaf = (n + 1)
+      blacks' n (node red _ l _ r) = (blacks' n l) + (blacks' n r)
+      blacks' n (node black _ l _ r) = (blacks' (n + 1) l) + (blacks' (n + 1) r)
+
+  reds : Color → RBTree a → Bool
+  reds _ leaf = true
+  reds red (node x x₁ t x₂ t₁) = false
+  reds black (node c x₁ l x₂ r) = reds c l ∧ reds c r
+
+  turnR : RBTree a → (RBTree a → cg) → cg
+  turnR leaf  cg = cg leaf
+  turnR (node _ h l x r) cg = cg (node red h l x r)
+
+  turnB : RBTree a → (RBTree a → cg) → cg
+  turnB leaf cg = cg leaf
+  turnB (node _ h l x r) cg = cg (node black h l x r)
+
+  minimum : RBTree ℕ → ℕ
+  minimum (node c h leaf x r) = x
+  minimum (node c h l x r) = minimum l
+  minimum leaf = 774
+
+  maximum : RBTree ℕ → ℕ
+  maximum (node c x₁ t x leaf) = x
+  maximum (node x x₁ t x₂ r) = maximum r
+  maximum leaf = 0
+
+  isRed : RBTree a → Bool
+  isRed (node red x₁ t x₂ t₁) = true
+  isRed _ = false
+
+  isColorSame : Color → Color → Bool
+  isColorSame red red = true
+  isColorSame red black = false
+  isColorSame black red = false
+  isColorSame black black = true
+
+  root→ℕ : Maybe (RBTree a) → Maybe ℕ
+  root→ℕ (just leaf) = nothing
+  root→ℕ (just (node x x₁ x₂ x₃ x₄)) = just x₃
+  root→ℕ nothing = nothing
+
+
+-- basic operations
+-- Code Gear Style (CPS : Contination Passing Style)
+
+-- balance
+
+
+module _ { n m : Level} {a : Set n} {cg : Set m}  where
+
+  balanceL' :  ℕ → RBTree a → ℕ → RBTree a → (RBTree a → cg) → cg
+  balanceL' h (node red h1 (node red hl a x b) y c) z d cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
+  balanceL' h (node red _ a x (node red _ b y c)) z d cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
+  balanceL' h l x r cg = cg (node black h l x r)
+
+  balanceR' : ℕ -> RBTree a -> ℕ -> RBTree a -> (RBTree a → cg) → cg
+  balanceR' h a x (node red _ b y (node red _ c z d)) cg =  cg (node red (h + 1) (node black h a x b) y (node black h c z d))
+  balanceR' h a x (node red _ (node red _ b y c) z d) cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
+  balanceR' h l x r cg = cg (node black h l x r)
+
+  balanceL : Color → ℕ → RBTree a → ℕ → RBTree a → (RBTree a → cg) → cg
+  balanceL black h (node red h1 (node red hl a x b) y c) z d cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
+  balanceL black h (node red _ a x (node red _ b y c)) z d cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
+  balanceL k h l x r cg = cg (node k h l x r)
+
+  balanceR : Color → ℕ -> RBTree a -> ℕ -> RBTree a -> (RBTree a → cg) → cg
+  balanceR black h a x (node red _ b y (node red _ c z d)) cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
+  balanceR black h a x (node red _ (node red _ b y c) z d) cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
+  balanceR k h l x r cg = cg (node k h l x r)
+
+-- unbalance
+
+  -- unbalanceL' : Color → ℕ -> RBTree a -> a -> RBTree a -> (RBTreeBDel a → cg) → cg
+  -- unbalanceL' c h l@(node black _ _ _ _) x r cg = cg record { tree = ? ; bool = (isColorSame c black) }
+  -- unbalanceL' c h l x r cg = {!!}
+
+  -- unbalanceL : Color → ℕ → RBTree a → a → RBTree a → (RBTree a → cg) → cg
+  -- unbalanceL c h l@(node black _ _ _ _) x r  cg = cg (balanceL black h (turnR l) x r cg)
+  -- unbalanceL Black h l@(node red lh ll lx lr@(node black _ _ _ _)) x r  cg = cg (node black lh ll lx (balanceL black h (turnR lr) x r))
+  -- unbalanceL c h l x r  cg = cg leaf
+
+  -- unbalanceR : Color → ℕ → RBTree ℕ → ℕ → RBTree ℕ → RBTreeBDel ℕ
+  -- unbalanceR c h l x r@(node black _ _ _ _)  = record {t = (balanceR black h l x (turnR r)) ; b = (checkColor c black)}
+  -- unbalanceR Black h l x (node R rh rl@(node black _ _ _ _) rx rr) = record { t = (node black rh (balanceR black h l x (turnR rl)) rx rr); b = false}
+  -- unbalanceR c h l x r  = record {t = leaf ; b = false}
+
+
+
+{--
+  Insert Function
+
+    All Nodes → ℕ
+    search Insert Location → O(log ℕ)
+    fix Tree (balanceR,L)  → O(log ℕ)
+    Root Child Color Fix   → O(1)
+    Total → O(2 log ℕ + 1)
+--}
+
+  -- turnRtree : RBTree a → (RBTree a → cg) → cg
+  -- turnRtree leaf cg = cg leaf
+  -- -- turnRtree (node black h l@(node black _ _ _ _) x r@(node black _ _ _ _)) cg = turnRtree (node red h l x r) cg
+  -- turnRtree (node c h l x r) cg = turnRtree r cg
+
+  rootChildFix : RBTree a → (RBTree a → cg) → cg
+  rootChildFix (node black h (node black lh ll@(node black llh lll llx llr) lx lr@(node black lrh lrl lrx lrr)) x (node black rh rl@(node black rlh rll rlx rlr) rx rr@(node black rrh rrl rrx rrr))) cg = cg (node black (h - 1) (node red (lh - 1) ll lx lr) x (node red (rh - 1) rl rx rr))
+  rootChildFix n cg = cg n
+
+  insert' : ℕ → RBTree a → (RBTree a → cg) → cg
+  insert' kx leaf cg = cg (node red 1 leaf kx leaf)
+
+  insert' kx (node black h l x r) cg with compare kx x
+  insert' kx (node black h l x r) cg | less kx k = insert' kx l (λ t → balanceL' h t x r (λ tt → cg tt))
+  insert' kx s@(node black h l x r) cg | equal kx = cg s
+  insert' kx (node black h l x r) cg | greater x k = insert' kx r (λ t → balanceR' h l x t (λ tt → cg tt))
+
+  insert' kx (node red h l x r) cg with compare kx x
+  insert' kx (node red h l x r) cg | less kx k = insert' kx l (λ t → cg (node red h t x r))
+  insert' kx s@(node red h l x r) cg | equal kx = cg s
+  insert' kx (node red h l x r) cg | greater x k = insert' kx r (λ t → cg (node red h l x t))
+
+  insert : ℕ → RBTree a → (RBTree a → cg) → cg
+  insert kx t cg = insert' kx t (λ t1 → turnB t1 (λ t2 → rootChildFix t2 cg))
+
+
+  get : ℕ → RBTree a → (Maybe (RBTree a) → cg) → cg
+  get x leaf cg = cg nothing
+  get x (node c h l x1 r) cg with compareTri x x1
+  get x (node c h l x1 r) cg | tri< a ¬b ¬c = get x l cg
+  get x t@(node c h l x1 r) cg | tri≈ ¬a b ¬c = cg (just t)
+  get x (node c h l x1 r) cg | tri> ¬a ¬b c₁ = get x r cg
+
+
+
+{- Check Balance, Color rule and hight calc -}
+
+-- create RBTree from Nat List
+fromList : List ℕ → RBTree ℕ
+fromList [] = empty {_} {_} {ℕ} {Set}
+fromList (x ∷ l) = (maketree x (empty {_} {_} {ℕ} {Set}) (λ t → fromList' l t (λ tt → tt)))
+  where
+    module _  {l : Level} {cg1 : Set l} {a : Set} where
+      maketree : ℕ → RBTree a → (RBTree a → cg1) → cg1
+      maketree x t1 cg = insert x t1 cg
+      fromList' : List ℕ → RBTree a → (RBTree a → cg1) → cg1
+      fromList' [] t cg = cg t
+      fromList' (x1 ∷ nl) t cg = maketree x1 t (λ tt → fromList' nl tt (λ ttt → cg ttt))
+
+
+c1 = fromList (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ 8 ∷ 9 ∷ [])
+c2 = fromList (5 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 6 ∷ 7 ∷ 8 ∷ 9 ∷ [])
+c3 = fromList (8 ∷ 7 ∷ 6 ∷ 1 ∷ 2 ∷ 5 ∷ 4 ∷ 3 ∷ 9 ∷ [])
+
+cget = get 6 c1 (λ a → a)
+
+hoge = rootChildFix (node black 3 (node black 2 (node black 1 leaf 1 leaf) 2 (node black 1 (node red 1 leaf 3 leaf) 4 leaf)) 5 (node black 2 (node black 1 leaf 6 leaf) 7 (node black 1 leaf 8 leaf))) (λ t → t)
+
+fuga = rootChildFix c3
+
+proof-leaf : {l : Level} {D : Set l} (n : ℕ) → insert {_} {_} {ℕ} {Set} n leaf (λ t1 → get n t1 (λ n1 → (just n ≡ (root→ℕ {_} {_} {ℕ} {ℕ} n1))))
+proof-leaf n with n Data.Nat.≟ n | compareTri n n
+proof-leaf n | yes p | tri< a ¬b ¬c = ⊥-elim (¬b p)
+proof-leaf n | yes p | tri≈ ¬a b ¬c = refl
+proof-leaf n | yes p | tri> ¬a ¬b c = ⊥-elim (¬b p)
+proof-leaf n | no ¬p | tri< a ¬b ¬c = ⊥-elim (¬c a)
+proof-leaf n | no ¬p | tri≈ ¬a b ¬c = refl
+proof-leaf n | no ¬p | tri> ¬a ¬b c = ⊥-elim (¬a c)
+
+
+
+
+-- 任意の木だと insert でノードをどこに入れるか決められず計算が進まない
+-- 任意の木の root が Nothing のケースはもちろんできる
+-- proof1 : {l : Level} {D : Set l} (n : ℕ) → (t : RBTree D) → insert n t (λ t1 → get n t1 (λ n1 → (just n ≡ (root→ℕ n1))))
+-- proof1 n t with n Data.Nat.≟ n | compareTri n n
+-- proof1 n t | yes p | tri< a ¬b ¬c = ⊥-elim (¬b p)
+-- proof1 n t | yes p | tri> ¬a ¬b c = ⊥-elim (¬b p)
+-- proof1 n t | no ¬p | tri< a ¬b ¬c = ⊥-elim (¬c a)
+-- proof1 n t | no ¬p | tri> ¬a ¬b c = ⊥-elim (¬a c)
+-- proof1 n leaf | yes p | tri≈ ¬a b ¬c with compareTri n n
+-- proof1 n leaf | yes p | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b p)
+-- proof1 n leaf | yes p | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl
+-- proof1 n leaf | yes p | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b p)
+-- proof1 n (node x x₁ t x₂ t₁) | yes p | tri≈ ¬a b ¬c = {!!}
+-- proof1 n t | no ¬p | tri≈ ¬a b ¬c = {!!}
+
+
+{--
+書くなら全ての探索が木の高さ分で終わることを証明しとく必要がありそう
+あと探索で木の高さが消化されていくことも示す
+stack の push は存在してるデータ構造に関係なく上に乗るから任意のstack で証明できる
+Tree でデータの保存を確かめるには…？
+
+tree で証明するくらいだったら、親子関係、
+rb 含めると、色関係、枝の長さ、になりそう?
+--}
+
+
+-- {-# TERMINATING #-}
+-- deleteMin' : RBTree ℕ → RBTreeBDel ℕ
+-- deleteMin' leaf  = record {t = (node black 999 leaf 999 leaf) ; b = false} -- unreachable case
+-- deleteMin' (node black _ leaf x leaf) = record {t = leaf ; b = true}
+-- deleteMin' (node black _ leaf x r@(node red _ _ _ _))  = record {t = (turnB {ℕ} r) ; b = false}
+-- deleteMin' (node red _ leaf x r)  = record {t = r ; b = false}
+-- deleteMin' (node c h l x r) = (delCheck (deleteMin' l))
+--   where
+--     delCheck : RBTreeBDel ℕ → RBTreeBDel ℕ
+--     delCheck bt with (b bt)
+--     delCheck record { t = leaf ; b = b } | false = record {t = (node red 100 leaf 100 leaf) ; b = b } -- unreachable case
+--     delCheck record { t = leaf ; b = b } | true = unbalanceR {ℕ} c (h - 1) leaf x r
+--     delCheck record { t = (node x₁ x₂ t₁ x₃ t₂) ; b = b } | false = deleteMin' (node x₁ x₂ t₁ x₃ t₂)
+--     delCheck record { t = (node x₁ (x₂) t₁ x₃ t₂) ; b = b } | true = unbalanceR {ℕ} c (h - 1) (node x₁ x₂ t₁ x₃ t₂) x r
+
+-- deleteMin : RBTree ℕ → RBTree ℕ
+-- deleteMin leaf = empty
+-- deleteMin t = turnB {ℕ} (outPutTree (deleteMin' t))
+--   where
+--     outPutTree : RBTreeBDel ℕ → RBTree ℕ
+--     outPutTree record { t = s ; b = b } = s
+
+
+-- {--
+--  1~7 のとき以降 delcheck の leaf case が出るので多分どこかの red の処理ミスってるっぽい
+-- --}
+-- cd = deleteMin (fromList ( 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ []))
+
+-- cdc = fromList ( 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ [])
+
+-- dd = deleteMin (fromList (1 ∷ 2 ∷ 3 ∷ []))
+
+-- {--
+--  black 2 ( black 1 leaf 2 leaf) 3 ( red 2 ( black 1 leaf 4 leaf) 5 ( black 1 leaf 6 ( red 1 leaf 7 leaf)))
+-- --}
+
+--  -- black 3 ( black 2 ( red 999 leaf 999 leaf) 2 ( red 1 leaf 3 leaf)) 4 ( red 2 ( black 1 leaf 5 leaf) 6 ( black 1 leaf 7 leaf))
+
+
+-- --  black 2 ( black 1 leaf 2 ( red 1 leaf 3 leaf)) 4 ( red 2 ( black 1 leaf 5 leaf) 6( black 1 leaf 7 leaf))
+
+
+-- delete' : {a : Set} → ℕ → RBTree ℕ → RBTreeBDel ℕ
+-- delete' _ leaf = record { t = leaf ; b = false}
+-- delete' x (node c h l y r) with compare x y
+-- delete' x (node c h l y r) | less .x k = delCheck (delete' {ℕ} x l)
+--   where
+--     delCheck : RBTreeBDel ℕ → RBTreeBDel ℕ
+--     delCheck bt with (b bt)
+--     delCheck record { t = leaf ; b = b } | false = record {t = (node red 100 leaf 100 leaf) ; b = b } -- unreachable case
+--     delCheck record { t = leaf ; b = b } | true = unbalanceR {ℕ} c (h - 1) leaf x r
+--     delCheck record { t = (node x₁ x₂ t₁ x₃ t₂) ; b = b } | false = deleteMin' (node x₁ x₂ t₁ x₃ t₂)
+--     delCheck record { t = (node x₁ (x₂) t₁ x₃ t₂) ; b = b } | true = unbalanceR {ℕ} c (h - 1) (node x₁ x₂ t₁ x₃ t₂) x r
+-- delete' x (node c h l y r) | greater .y k = delCheck (delete' {ℕ} x r)
+--   where
+--     delCheck : RBTreeBDel ℕ → RBTreeBDel ℕ
+--     delCheck bt with (b bt)
+--     delCheck record { t = leaf ; b = b } | false = record {t = (node red 100 leaf 100 leaf) ; b = b } -- unreachable case
+--     delCheck record { t = leaf ; b = b } | true = unbalanceR {ℕ} c (h - 1) leaf x r
+--     delCheck record { t = (node x₁ x₂ t₁ x₃ t₂) ; b = b } | false = deleteMin' (node x₁ x₂ t₁ x₃ t₂)
+--     delCheck record { t = (node x₁ (x₂) t₁ x₃ t₂) ; b = b } | true = unbalanceR {ℕ} c (h - 1) (node x₁ x₂ t₁ x₃ t₂) x r
+-- delete' x (node c h l .x leaf) | equal .x with checkColor {ℕ} c black
+-- delete' x (node c h l .x leaf) | equal .x | false = record {t = l ; b = false}
+-- delete' x (node c h l .x leaf) | equal .x | true = blackify l
+--   where
+--     blackify : RBTree ℕ → RBTreeBDel ℕ
+--     blackify (node red x₂ a x₃ a₁) = record {t = turnB {ℕ} (node red x₂ a x₃ a₁) ; b = false}
+--     blackify s = record {t = s; b = true}
+-- delete' x (node c h l .x (node x₁ x₂ r x₃ r₁)) | equal .x with r
+-- delete' x (node c h l .x (node x₁ x₂ r x₃ r₁)) | equal .x | leaf with checkColor {ℕ} c black
+-- delete' x (node c h l .x (node x₁ x₂ r x₃ r₁)) | equal .x | leaf | false = blackify l
+--   where
+--     blackify : RBTree ℕ → RBTreeBDel ℕ
+--     blackify (node red x₂ a x₃ a₁) = record {t = turnB {ℕ} (node red x₂ a x₃ a₁) ; b = false}
+--     blackify s = record {t = s; b = true}
+-- delete' x (node c h l .x (node x₁ x₂ r x₃ r₁)) | equal .x | leaf | true = record {t = l ; b = false}
+-- delete' x (node c h l .x (node x₁ x₂ r x₃ r₁)) | equal .x | node x₄ x₅ rnod x₆ rnod₁ = {!!}
+
+--   -- where
+--   -- delCheck : RBTreeBDel ℕ → RBTreeBDel ℕ
+--   -- delCheck bt with (b bt)
+--   -- delCheck record { t = leaf ; b = b } | false = record {t = (node red 100 leaf 100 leaf) ; b = b } -- unreachable case
+--   -- delCheck record { t = leaf ; b = b } | true = unbalanceR {ℕ} c (h - 1) leaf x r
+--   -- delCheck record { t = (node x₁ x₂ t₁ x₃ t₂) ; b = b } | false = deleteMin' (node x₁ x₂ t₁ x₃ t₂)
+--   -- delCheck record { t = (node x₁ (x₂) t₁ x₃ t₂) ; b = b } | true = unbalanceR {ℕ} c (h - 1) (node x₁ x₂ t₁ x₃ t₂) x r
+-- -- 謎フラグがtrue なら バランスしろとのお達しなのでどっかで持ちましょうはい。
+-- -- 多分 record で適当に持つのがよいっぽい
+
+-- delete : {a : Set} → ℕ → RBTree ℕ → RBTree ℕ
+-- delete kx t = turnB {ℕ} (outPutTree (delete' {ℕ} kx t))
+--   where
+--     outPutTree : RBTreeBDel ℕ → RBTree ℕ
+--     outPutTree record { t = s ; b = b } = s
+
+-- proofs
+-- isOrdered : RBTree a → Bool
+-- isOrdered t = {!!}
+
+-- isBlackSame : RBTree a → Bool
+-- isBlackSame t = {!!}
+
+-- isBalanced : RBTree a → Bool
+-- isBalanced t = {!!}