--- a/Paper/src/while_loop_verif/verif.agda.replaced	Sat Nov 06 20:06:24 2021 +0900
+++ b/Paper/src/while_loop_verif/verif.agda.replaced	Sun Nov 07 00:51:16 2021 +0900
@@ -1,4 +1,4 @@
-proofGearsTermS : {c10 :  @$\mathbb{N}$@ } @$\rightarrow$@ @$\top$@
-proofGearsTermS {c10} = whileTest@$\prime$@ {_} {_}  {c10} (@$\lambda$@ n p @$\rightarrow$@  conversion1 n p (@$\lambda$@ n1 p1 @$\rightarrow$@
-    TerminatingLoopS Env (@$\lambda$@ env @$\rightarrow$@ varn env)
-        (@$\lambda$@ n2 p2 loop @$\rightarrow$@ whileLoopSeg {_} {_} {c10} n2 p2 loop (@$\lambda$@ ne pe @$\rightarrow$@ whileTestSpec1 c10 ne pe)) n1 p1 )) 
\ No newline at end of file
+proofGearsTermS : {c10 :  !$\mathbb{N}$! } !$\rightarrow$! !$\top$!
+proofGearsTermS {c10} = whileTest!$\prime$! {_} {_}  {c10} (!$\lambda$! n p !$\rightarrow$!  conversion1 n p (!$\lambda$! n1 p1 !$\rightarrow$!
+    TerminatingLoopS Env (!$\lambda$! env !$\rightarrow$! varn env)
+        (!$\lambda$! n2 p2 loop !$\rightarrow$! whileLoopSeg {_} {_} {c10} n2 p2 loop (!$\lambda$! ne pe !$\rightarrow$! whileTestSpec1 c10 ne pe)) n1 p1 )) 
\ No newline at end of file