--- a/rbt_t.agda	Tue Dec 01 19:04:17 2020 +0900
+++ b/rbt_t.agda	Tue Jan 12 21:20:16 2021 +0900
@@ -18,12 +18,14 @@
   field
     coler : A
     number : B
+open node
 
 record tree (A B C : Set) : Set where
   field
     key : A
     ltree : B
     rtree : C
+open tree
 
 data rbt : Set where
   bt-empty : rbt
@@ -124,9 +126,12 @@
 init-node-coler record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit
   = exit record { vart = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl }
 
+--修正前
 merge-tree node@record { vart = vart ; varn = varn ; varl = [] } next exit = exit node
 merge-tree node@record { vart = vart ; varn = varn ; varl = (bt-empty ∷ varl₁) } next exit = exit node
+
 merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit with <-cmp varn number
+
 merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri≈ ¬a b ¬c
   = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = number ; varl = varl₁ }
 
@@ -136,6 +141,17 @@
 merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri< a ¬b ¬c
   = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = vart ; rtree = rtree }) ; varn = number ; varl = varl₁ }
 
+--修正後
+merge-tree1 :  {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+merge-tree1 env next exit with varl env
+... | [] = exit env
+... | bt-empty ∷ nl = exit env
+... | bt-node node₁ ∷ nl with <-cmp (varn env) (number ( key node₁ ))
+... | tri≈ ¬a b ¬c = next (record env { varn = number (key node₁) ; varl = nl })
+-- next (record{ vart = vart env ; varn = number (key node₁) ; varl = nl })
+... | tri> ¬a ¬b c = next (record env { vart = (bt-node record { key = key node₁ ; ltree = ltree node₁ ; rtree = vart env }) ; varn = number (key node₁) ; varl = nl })
+-- next (record{ vart = (bt-node record { key = key node₁ ; ltree = ltree node₁ ; rtree = vart env }) ; varn = number (key node₁) ; varl = nl })
+... | tri< a ¬b ¬c = next (record{ vart = (bt-node record { key = key node₁ ; ltree = vart env ; rtree = rtree node₁ }) ; varn = number (key node₁) ; varl = nl })
 
 -- insert
 bt-insert : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
@@ -154,6 +170,8 @@
 bt-insert record {vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit | tri< a ¬b ¬c
   = next (record {vart = rtree ; varn = varn ; varl = (bt-node record { key = key ; ltree = ltree ; rtree = bt-empty }) ∷ varl })
 
+
+
 -- normal loop without termination
 {-# TERMINATING #-}
 insert : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
@@ -216,6 +234,12 @@
 mergeP env exit = merge-tree env (λ env → skew' env (λ env → split' env (λ env → mergeP env exit)) ) exit
 
 {-
+mergeP1 : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+mergeP1 record { vart = vart ; varn = varn ; varl = [] } exit = {!!}
+mergeP1 record { vart = vart ; varn = varn ; varl = (x ∷ varl₁) } exit = {!!}
+-}
+
+{-
 merge-tree env
   (λ env → skew-bt env
     (λ env → merge-rotate-left env