--- a/Paper/src/cbc-agda.agda.replaced	Sat Nov 06 20:06:24 2021 +0900
+++ b/Paper/src/cbc-agda.agda.replaced	Sun Nov 07 00:51:16 2021 +0900
@@ -5,18 +5,18 @@
 
 record Env : Set where
   field
-    varx : @$\mathbb{N}$@
-    vary : @$\mathbb{N}$@
+    varx : !$\mathbb{N}$!
+    vary : !$\mathbb{N}$!
 open Env
 
-plus-com : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+plus-com : {l : Level} {t : Set l} !$\rightarrow$! Env !$\rightarrow$! (next : Env !$\rightarrow$! t) !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t
 plus-com env next exit with vary env
 ... | zero  = exit (record { varx = varx env ; vary = vary env })
 ... | suc y = next (record { varx = suc (varx env) ; vary = y })
 
-{-@$\#$@ TERMINATING @$\#$@-}
-plus-p : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
-plus-p env exit = plus-com env ( @$\lambda$@ env @$\rightarrow$@ plus-p env exit ) exit
+{-!$\#$! TERMINATING !$\#$!-}
+plus-p : {l : Level} {t : Set l} !$\rightarrow$! (env : Env) !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t
+plus-p env exit = plus-com env ( !$\lambda$! env !$\rightarrow$! plus-p env exit ) exit
 
-plus : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Env
-plus x y = plus-p (record { varx = x ; vary = y }) (@$\lambda$@ env @$\rightarrow$@ env)
+plus : !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! Env
+plus x y = plus-p (record { varx = x ; vary = y }) (!$\lambda$! env !$\rightarrow$! env)