--- a/Paper/src/agda-hoare-rule.agda.replaced	Sat Nov 06 20:06:24 2021 +0900
+++ b/Paper/src/agda-hoare-rule.agda.replaced	Sun Nov 07 00:51:16 2021 +0900
@@ -1,27 +1,27 @@
-data HTProof : Cond @$\rightarrow$@ Comm @$\rightarrow$@ Cond @$\rightarrow$@ Set where
-  PrimRule : {bPre : Cond} @$\rightarrow$@ {pcm : PrimComm} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@
-             (pr : Axiom bPre pcm bPost) @$\rightarrow$@
+data HTProof : Cond !$\rightarrow$! Comm !$\rightarrow$! Cond !$\rightarrow$! Set where
+  PrimRule : {bPre : Cond} !$\rightarrow$! {pcm : PrimComm} !$\rightarrow$! {bPost : Cond} !$\rightarrow$!
+             (pr : Axiom bPre pcm bPost) !$\rightarrow$!
              HTProof bPre (PComm pcm) bPost
-  SkipRule : (b : Cond) @$\rightarrow$@ HTProof b Skip b
-  AbortRule : (bPre : Cond) @$\rightarrow$@ (bPost : Cond) @$\rightarrow$@
+  SkipRule : (b : Cond) !$\rightarrow$! HTProof b Skip b
+  AbortRule : (bPre : Cond) !$\rightarrow$! (bPost : Cond) !$\rightarrow$!
               HTProof bPre Abort bPost
-  WeakeningRule : {bPre : Cond} @$\rightarrow$@ {bPre' : Cond} @$\rightarrow$@ {cm : Comm} @$\rightarrow$@
-                {bPost' : Cond} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@
-                Tautology bPre bPre' @$\rightarrow$@
-                HTProof bPre' cm bPost' @$\rightarrow$@
-                Tautology bPost' bPost @$\rightarrow$@
+  WeakeningRule : {bPre : Cond} !$\rightarrow$! {bPre!$\prime$! : Cond} !$\rightarrow$! {cm : Comm} !$\rightarrow$!
+                {bPost!$\prime$! : Cond} !$\rightarrow$! {bPost : Cond} !$\rightarrow$!
+                Tautology bPre bPre!$\prime$! !$\rightarrow$!
+                HTProof bPre!$\prime$! cm bPost!$\prime$! !$\rightarrow$!
+                Tautology bPost!$\prime$! bPost !$\rightarrow$!
                 HTProof bPre cm bPost
-  SeqRule : {bPre : Cond} @$\rightarrow$@ {cm1 : Comm} @$\rightarrow$@ {bMid : Cond} @$\rightarrow$@
-            {cm2 : Comm} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@
-            HTProof bPre cm1 bMid @$\rightarrow$@
-            HTProof bMid cm2 bPost @$\rightarrow$@
+  SeqRule : {bPre : Cond} !$\rightarrow$! {cm1 : Comm} !$\rightarrow$! {bMid : Cond} !$\rightarrow$!
+            {cm2 : Comm} !$\rightarrow$! {bPost : Cond} !$\rightarrow$!
+            HTProof bPre cm1 bMid !$\rightarrow$!
+            HTProof bMid cm2 bPost !$\rightarrow$!
             HTProof bPre (Seq cm1 cm2) bPost
-  IfRule : {cmThen : Comm} @$\rightarrow$@ {cmElse : Comm} @$\rightarrow$@
-           {bPre : Cond} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@
-           {b : Cond} @$\rightarrow$@
-           HTProof (bPre @$\wedge$@ b) cmThen bPost @$\rightarrow$@
-           HTProof (bPre @$\wedge$@ neg b) cmElse bPost @$\rightarrow$@
+  IfRule : {cmThen : Comm} !$\rightarrow$! {cmElse : Comm} !$\rightarrow$!
+           {bPre : Cond} !$\rightarrow$! {bPost : Cond} !$\rightarrow$!
+           {b : Cond} !$\rightarrow$!
+           HTProof (bPre !$\wedge$! b) cmThen bPost !$\rightarrow$!
+           HTProof (bPre !$\wedge$! neg b) cmElse bPost !$\rightarrow$!
            HTProof bPre (If b cmThen cmElse) bPost
-  WhileRule : {cm : Comm} @$\rightarrow$@ {bInv : Cond} @$\rightarrow$@ {b : Cond} @$\rightarrow$@
-              HTProof (bInv @$\wedge$@ b) cm bInv @$\rightarrow$@
-              HTProof bInv (While b cm) (bInv @$\wedge$@ neg b)
+  WhileRule : {cm : Comm} !$\rightarrow$! {bInv : Cond} !$\rightarrow$! {b : Cond} !$\rightarrow$!
+              HTProof (bInv !$\wedge$! b) cm bInv !$\rightarrow$!
+              HTProof bInv (While b cm) (bInv !$\wedge$! neg b)