--- a/Paper/src/cbc-hoare.agda.replaced	Sat Nov 06 20:06:24 2021 +0900
+++ b/Paper/src/cbc-hoare.agda.replaced	Sun Nov 07 00:51:16 2021 +0900
@@ -1,14 +1,14 @@
-whileTestPwP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ ((env : Envc ) @$\rightarrow$@ whileTestStateP s1 env @$\rightarrow$@ t) @$\rightarrow$@ t
+whileTestPwP : {l : Level} {t : Set l} !$\rightarrow$! (c10 : !$\mathbb{N}$!) !$\rightarrow$! ((env : Envc ) !$\rightarrow$! whileTestStateP s1 env !$\rightarrow$! t) !$\rightarrow$! t
 whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
   env : Envc
-  env = whileTestP c10 ( @$\lambda$@ env @$\rightarrow$@ env )
+  env = whileTestP c10 ( !$\lambda$! env !$\rightarrow$! env )
 
-loopPwP' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc ) @$\rightarrow$@ (n @$\equiv$@ varn env) @$\rightarrow$@ whileTestStateP s2 env @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ whileTestStateP sf env @$\rightarrow$@ t) @$\rightarrow$@ t
-loopPwP' zero env refl refl exit = exit env refl
-loopPwP' (suc n) env refl refl exit  = whileLoopPwP' (suc n) env refl refl (@$\lambda$@ env x y @$\rightarrow$@ loopPwP' n env x y exit) exit
+loopPwP!$\prime$! : {l : Level} {t : Set l} !$\rightarrow$! (n : !$\mathbb{N}$!) !$\rightarrow$! (env : Envc ) !$\rightarrow$! (n !$\equiv$! varn env) !$\rightarrow$! whileTestStateP s2 env !$\rightarrow$! (exit : (env : Envc ) !$\rightarrow$! whileTestStateP sf env !$\rightarrow$! t) !$\rightarrow$! t
+loopPwP!$\prime$! zero env refl refl exit = exit env refl
+loopPwP!$\prime$! (suc n) env refl refl exit  = whileLoopPwP!$\prime$! (suc n) env refl refl (!$\lambda$! env x y !$\rightarrow$! loopPwP!$\prime$! n env x y exit) exit
 
 
-whileTestPCallwP' : (c :  @$\mathbb{N}$@ ) @$\rightarrow$@ Set
-whileTestPCallwP' c = whileTestPwP {_} {_} c (@$\lambda$@ env s @$\rightarrow$@ loopPwP' (varn env) env refl (conv env s) ( @$\lambda$@ env s @$\rightarrow$@ vari env @$\equiv$@ c10 env )  )
+whileTestPCallwP!$\prime$! : (c :  !$\mathbb{N}$! ) !$\rightarrow$! Set
+whileTestPCallwP!$\prime$! c = whileTestPwP {_} {_} c (!$\lambda$! env s !$\rightarrow$! loopPwP!$\prime$! (varn env) env refl (conv env s) ( !$\lambda$! env s !$\rightarrow$! vari env !$\equiv$! c10 env )  )