--- a/Paper/src/agda/rbt_imple.agda.replaced	Sat Nov 06 20:06:24 2021 +0900
+++ b/Paper/src/agda/rbt_imple.agda.replaced	Sun Nov 07 00:51:16 2021 +0900
@@ -2,7 +2,7 @@
 
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Relation.Binary
-open import Data.Nat hiding (_@$\leq$@_  ; _@$\leq$@?_)
+open import Data.Nat hiding (_!$\leq$!_  ; _!$\leq$!?_)
 open import Data.List hiding ([_])
 open import Data.Product
 open import Data.Nat.Properties as NP
@@ -13,49 +13,49 @@
 mutual
   data  right-List : Set where
     [] : right-List
-    [_] : @$\mathbb{N}$@ @$\rightarrow$@ right-List
-    _@$\text{::}$@>_Cond_ : (x : @$\mathbb{N}$@) @$\rightarrow$@ (xs : right-List ) @$\rightarrow$@ (p : x Data.Nat.> top-r xs) @$\rightarrow$@ right-List
+    [_] : !$\mathbb{N}$! !$\rightarrow$! right-List
+    _!$\text{::}$!>_Cond_ : (x : !$\mathbb{N}$!) !$\rightarrow$! (xs : right-List ) !$\rightarrow$! (p : x Data.Nat.> top-r xs) !$\rightarrow$! right-List
 
-  top-r : right-List @$\rightarrow$@ @$\mathbb{N}$@
+  top-r : right-List !$\rightarrow$! !$\mathbb{N}$!
   top-r [] = {!!}
   top-r [ x ] = x
-  top-r (x @$\text{::}$@> l Cond x@$\_{1}$@) = x
+  top-r (x !$\text{::}$!> l Cond x!$\_{1}$!) = x
 
-  insert-r : @$\mathbb{N}$@ @$\rightarrow$@ right-List @$\rightarrow$@ right-List
+  insert-r : !$\mathbb{N}$! !$\rightarrow$! right-List !$\rightarrow$! right-List
   insert-r x l with l
   ... | [] = {!!}
   ... | [ y ] = ?
-  ... | y @$\text{::}$@> ys Cond p with <-cmp x y
-  ... | tri< a @$\neg$@b @$\neg$@c = l
-  ... | tri≈ @$\neg$@a b @$\neg$@c = l
-  ... | tri> @$\neg$@a @$\neg$@b c = x @$\text{::}$@> l Cond c
+  ... | y !$\text{::}$!> ys Cond p with <-cmp x y
+  ... | tri< a !$\neg$!b !$\neg$!c = l
+  ... | tri!$\approx$! !$\neg$!a b !$\neg$!c = l
+  ... | tri> !$\neg$!a !$\neg$!b c = x !$\text{::}$!> l Cond c
 
   data  left-List : Set where
     [] : left-List
-    [_] : @$\mathbb{N}$@ @$\rightarrow$@ left-List
-    _<@$\text{::}$@_Cond_ : (x : @$\mathbb{N}$@) @$\rightarrow$@ (xs : left-List ) @$\rightarrow$@ (p : x Data.Nat.< top-l xs) @$\rightarrow$@ left-List
+    [_] : !$\mathbb{N}$! !$\rightarrow$! left-List
+    _<!$\text{::}$!_Cond_ : (x : !$\mathbb{N}$!) !$\rightarrow$! (xs : left-List ) !$\rightarrow$! (p : x Data.Nat.< top-l xs) !$\rightarrow$! left-List
 
-  top-l : left-List @$\rightarrow$@ @$\mathbb{N}$@
+  top-l : left-List !$\rightarrow$! !$\mathbb{N}$!
   top-l [] = {!!}
   top-l [ x ] = x
-  top-l (x <@$\text{::}$@ l Cond x@$\_{1}$@) = x
+  top-l (x <!$\text{::}$! l Cond x!$\_{1}$!) = x
 
-  insert-l : @$\mathbb{N}$@ @$\rightarrow$@ left-List @$\rightarrow$@ left-List
+  insert-l : !$\mathbb{N}$! !$\rightarrow$! left-List !$\rightarrow$! left-List
   insert-l x [] = [ x ]
   insert-l x l@([ y ]) with <-cmp x y
-  ... | tri< a @$\neg$@b @$\neg$@c = x <@$\text{::}$@ l Cond a
-  ... | tri≈ @$\neg$@a b @$\neg$@c = l
-  ... | tri> @$\neg$@a @$\neg$@b c = l
-  insert-l x l@(y <@$\text{::}$@ ys Cond p) with <-cmp x y
-  ... | tri< a @$\neg$@b @$\neg$@c = x <@$\text{::}$@ l Cond a
-  ... | tri≈ @$\neg$@a b @$\neg$@c = l
-  ... | tri> @$\neg$@a @$\neg$@b c = l
+  ... | tri< a !$\neg$!b !$\neg$!c = x <!$\text{::}$! l Cond a
+  ... | tri!$\approx$! !$\neg$!a b !$\neg$!c = l
+  ... | tri> !$\neg$!a !$\neg$!b c = l
+  insert-l x l@(y <!$\text{::}$! ys Cond p) with <-cmp x y
+  ... | tri< a !$\neg$!b !$\neg$!c = x <!$\text{::}$! l Cond a
+  ... | tri!$\approx$! !$\neg$!a b !$\neg$!c = l
+  ... | tri> !$\neg$!a !$\neg$!b c = l
 
 
 record meta : Set where
   field
-    deeps : @$\mathbb{N}$@
-    black-nodes : @$\mathbb{N}$@
+    deeps : !$\mathbb{N}$!
+    black-nodes : !$\mathbb{N}$!
     l-list : left-List
     r-list : right-List
 open meta
@@ -72,36 +72,36 @@
 
 data rbt-meta : Set where
   bt-empty : rbt-meta
-  bt-node  : (node : tree-meta (node col @$\mathbb{N}$@ ) meta rbt-meta rbt-meta ) @$\rightarrow$@ rbt-meta
+  bt-node  : (node : tree-meta (node col !$\mathbb{N}$! ) meta rbt-meta rbt-meta ) !$\rightarrow$! rbt-meta
 
-test'1 = whileTestPCall' bt-empty 0
-test'2 = whileTestPCall' (rbt_t.Env.vart test'1) 1
-test'3 = whileTestPCall' (rbt_t.Env.vart test'2) 2
-test'4 = whileTestPCall' (rbt_t.Env.vart test'3) 3
-test'5 = whileTestPCall' (rbt_t.Env.vart test'4) 4
-test'6 = whileTestPCall' (rbt_t.Env.vart test'5) 5
-test'7 = whileTestPCall' (rbt_t.Env.vart test'6) 6
-test'8 = whileTestPCall' (rbt_t.Env.vart test'7) 7
-test'9 = whileTestPCall' (rbt_t.Env.vart test'8) 8
-test'10 = whileTestPCall' (rbt_t.Env.vart test'9) 9
-test'11 = whileTestPCall' (rbt_t.Env.vart test'10) 10
-test'12 = whileTestPCall' (rbt_t.Env.vart test'11) 11
-test'13 = whileTestPCall' (rbt_t.Env.vart test'12) 12
-test'14 = whileTestPCall' (rbt_t.Env.vart test'13) 13
-test'15 = whileTestPCall' (rbt_t.Env.vart test'14) 14
+test!$\prime$!1 = whileTestPCall!$\prime$! bt-empty 0
+test!$\prime$!2 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!1) 1
+test!$\prime$!3 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!2) 2
+test!$\prime$!4 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!3) 3
+test!$\prime$!5 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!4) 4
+test!$\prime$!6 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!5) 5
+test!$\prime$!7 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!6) 6
+test!$\prime$!8 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!7) 7
+test!$\prime$!9 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!8) 8
+test!$\prime$!10 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!9) 9
+test!$\prime$!11 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!10) 10
+test!$\prime$!12 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!11) 11
+test!$\prime$!13 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!12) 12
+test!$\prime$!14 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!13) 13
+test!$\prime$!15 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!14) 14
 
-testdata = rbt_t.Env.vart test'7
+testdata = rbt_t.Env.vart test!$\prime$!7
 
 -- ここからmetaの作成
 
-makemeta-comm : rbt_t.rbt @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ meta @$\rightarrow$@ rbt-meta
+makemeta-comm : rbt_t.rbt !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! meta !$\rightarrow$! rbt-meta
 
 --make meta black nodes
-makemeta-black-nodes :  rbt_t.rbt @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ meta @$\rightarrow$@ rbt-meta
+makemeta-black-nodes :  rbt_t.rbt !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! meta !$\rightarrow$! rbt-meta
 makemeta-black-nodes = {!!}
 
 -- make meta deeps
-set-black-nodes : rbt_t.rbt @$\rightarrow$@ meta @$\rightarrow$@ @$\mathbb{N}$@
+set-black-nodes : rbt_t.rbt !$\rightarrow$! meta !$\rightarrow$! !$\mathbb{N}$!
 set-black-nodes rbt fls with rbt
 ... | bt-empty = (suc (black-nodes fls) )
 ... | bt-node node with (node.coler (key node))
@@ -126,7 +126,7 @@
     ; r-list = insert-r (node.number (key node)) (r-list fls) } ) })
 
 -- init
-makemeta : rbt @$\rightarrow$@ rbt-meta
+makemeta : rbt !$\rightarrow$! rbt-meta
 makemeta rbt with rbt
 ... | bt-empty = bt-empty
 ... | bt-node node = bt-node ( record { key = key node
@@ -136,5 +136,5 @@
   ; rtree = makemeta-comm (rtree node) (node.number (key node))
     ( record { deeps = 1 ; black-nodes = 1 ; l-list = [] ; r-list = insert-r (node.number (key node)) [] } ) })
 
----test11 = makemeta (rbt_t.Env.vart test'11)
+---test11 = makemeta (rbt_t.Env.vart test!$\prime$!11)
 -}