--- a/Paper/tex/while_loop.tex	Thu May 05 17:38:06 2022 +0900
+++ b/Paper/tex/while_loop.tex	Thu May 05 22:32:45 2022 +0900
@@ -1,68 +1,68 @@
 \section{Gears Agda にて Hoare Logic を用いた検証の例}
-ここでは Gears Agda にて Hoare Logic を用いた検証の例として、
- While Loop プログラムを実装・検証する。
+ここでは Gears Agda にて Hoare Logic を用いた検証の例として，
+ While Loop プログラムを実装・検証する．
 
 \subsection{While Loop の実装}
-まずは前述した Gears Agda の記述形式に基づいて While Loop を実装する。
-実装はまず、 Code \ref{while-loop-dg} のように Code Gear に遷移させる Data Gear の定義から行う。
+まずは前述した Gears Agda の記述形式に基づいて While Loop を実装する．
+実装はまず， Code \ref{while-loop-dg} のように Code Gear に遷移させる Data Gear の定義から行う．
 \lstinputlisting[label=while-loop-dg, caption=Data Gearの定義] {src/while_loop_impl/while_loop_dg.agda.replaced}
 
-そのため最初の Code Gear は引数を受け取り、Envを作成する Code Gear となる Code \ref{while_init_cg}。
+そのため最初の Code Gear は引数を受け取り，Envを作成する Code Gear となる Code \ref{while_init_cg}．
 
 \lstinputlisting[label=while_init_cg, caption=Data Gear の定義を行う Code Gear] {src/while_loop_impl/init_cg.agda.replaced}
 
-次に、目的である While Loop の実装を行う。ソースコードは Code \ref{while-loop} のようになる。
+次に，目的である While Loop の実装を行う．ソースコードは Code \ref{while-loop} のようになる．
 
 \lstinputlisting[label=while-loop, caption=Loop の部分を担う Code Gears] {src/while_loop_impl/while_loop.agda.replaced}
 
-また Agda では停止性の検出機能が存在し、
-プログラム中 に停止しない記述が存在するとコンパイル時にエラーが出る。
+また Agda では停止性の検出機能が存在し，
+プログラム中 に停止しない記述が存在するとコンパイル時にエラーが出る．
 その場合は関数定義の直前に
 \{-$\#$ TERMINATING $\#$-\} のタグを付けると
 停止しないプログラムをコンパイルすることができる
 
-これまでの Code Gear を繋げることで、 While Loop　を行う Code を実装することができる。
+これまでの Code Gear を繋げることで， While Loop　を行う Code を実装することができる．
 
 \lstinputlisting[label=while-loop, caption=While Loop を行う Code Gear] {src/while_loop_impl/while_loop_c.agda.replaced}
 
 \subsection{While Loop の検証}
 
-Gears Agda にて行なった While Loop の実装コードを元に、
+Gears Agda にて行なった While Loop の実装コードを元に，
 5章にて述べた Pre / Post Condition を記述していくことで
-Hoare Logic を用いた検証を行う。
+Hoare Logic を用いた検証を行う．
 
-検証を行う Code Gear も Gears Agda による単純な実装と同じく Data Gear の定義から行う。Code \ref{while_verif_init_cg} がそれに当たる。
+検証を行う Code Gear も Gears Agda による単純な実装と同じく Data Gear の定義から行う．Code \ref{while_verif_init_cg} がそれに当たる．
 
 \lstinputlisting[label=while_verif_init_cg, caption=While Loop を行う Code Gear] {src/while_loop_verif/init_cg.agda.replaced}
 
-今回は検証を行いたいため 5.1 で述べたように、実装に加えて Pre / Post Condition を持つ必要がある。
-init時の Pre Condition のみ特殊で　Agda での関数定義の際に記述し、
-「Data Gear に正しく初期値が設定される」という条件を使用する。これが
+今回は検証を行いたいため 5.1 で述べたように，実装に加えて Pre / Post Condition を持つ必要がある．
+init時の Pre Condition のみ特殊で　Agda での関数定義の際に記述し，
+「Data Gear に正しく初期値が設定される」という条件を使用する．これが
 ((vari env) $\equiv$ 0) $\wedge$ ((varn env) $\equiv$ c10)
-に当たる。
-そしてinit時以外の、Pre Condition と Post Condition には実行開始から実行終了までの間で不変の条件を記述する。
-今回は While Loop の不変条件として、
+に当たる．
+そしてinit時以外の，Pre Condition と Post Condition には実行開始から実行終了までの間で不変の条件を記述する．
+今回は While Loop の不変条件として，
 $今回loopさせたい回数(c10) = 残りのloopする回数(vern) + 今回loopした回数(vari)$
-を設定した。これがinit時の Post Condition となる。
+を設定した．これがinit時の Post Condition となる．
 
-また、init時の Pre Condition と同じ値で
-Post Condition を設定しなければならない。
-init時の Pre Condition を Post Condition に変換する Code \ref{conversion} を記載する。
+また，init時の Pre Condition と同じ値で
+Post Condition を設定しなければならない．
+init時の Pre Condition を Post Condition に変換する Code \ref{conversion} を記載する．
 
 \lstinputlisting[label=conversion, caption=init時の Pre Condition を Post Condition に変換する Code Gear] {src/while_loop_verif/conversion.agda.replaced}
 
-ここで変換されて作成された Post Condition はプログラム実行中の不変条件となるため、
-この後の Pre / Post Condition は停止するまでこれを用いる。
+ここで変換されて作成された Post Condition はプログラム実行中の不変条件となるため，
+この後の Pre / Post Condition は停止するまでこれを用いる．
 
-以下の Code \ref{loop_verif_cg} は停止性の検証を行っていないが、 Wile Loop の Loop 部分の検証を行う Code Gear となる。
+以下の Code \ref{loop_verif_cg} は停止性の検証を行っていないが， Wile Loop の Loop 部分の検証を行う Code Gear となる．
 
 \lstinputlisting[label=loop_verif_cg, caption=停止性以外の Loop の検証も行う Code Gear] {src/while_loop_verif/while_loop.agda.replaced}
 
-Loop が停止することを示していないため、関数定義の直前に \{-\# TERMINATING \#-\} が記述されている。
-こちらも Loop の実装以外に、Pre / Post Condition を満たしているか検証を行い、次の Code Gear に渡している。
+Loop が停止することを示していないため，関数定義の直前に \{-\# TERMINATING \#-\} が記述されている．
+こちらも Loop の実装以外に，Pre / Post Condition を満たしているか検証を行い，次の Code Gear に渡している．
 
-ここまでで定義した Pre / Post Consition が付いている Code Gear を繋げることで、
-停止性以外の While Loop の検証を行う Code Gear を実装できる。
+ここまでで定義した Pre / Post Consition が付いている Code Gear を繋げることで，
+停止性以外の While Loop の検証を行う Code Gear を実装できる．
 
 \lstinputlisting[label=loop_verif_cg, caption=停止性以外の While Loop の検証を行う Code Gear] {src/while_loop_verif/verif_term.agda.replaced}
 
@@ -70,14 +70,14 @@
 
 \lstinputlisting[label=loop_verif_cg, caption=停止性の検証も行う Loop 部分の Code Gear] {src/while_loop_verif/verif_loop.agda.replaced}
 
-停止することを Agda が理解できるように記述すると良い。
-そのため引数に減少していく変数 reduce を追加し、
-loop するとデクリメントするように実装する。
+停止することを Agda が理解できるように記述すると良い．
+そのため引数に減少していく変数 reduce を追加し，
+loop するとデクリメントするように実装する．
 
 loop には先ほど実装した loop の部分を担う Code Gear が次の関数遷移先を引数に受け取れるようにした
-whileLoopSeg を使用する。
+whileLoopSeg を使用する．
 
-そしてこれらを繋げて While Loop の検証を行うことができる Code ref を実装できた。
+そしてこれらを繋げて While Loop の検証を行うことができる Code ref を実装できた．
 
 \lstinputlisting[label=loop_verif_cg, caption=停止性の検証も行う While Loop の Code Gear] {src/while_loop_verif/verif.agda.replaced}