--- a/paper/agda.tex	Tue Feb 17 17:48:30 2015 +0900
+++ b/paper/agda.tex	Wed Feb 18 11:10:19 2015 +0900
@@ -37,8 +37,7 @@
 \end{eqnarray}
 
 式\ref{exp:a_implies_b}のように A を仮定して B を導くことができたとする。
-この時 A は alive な仮定である。
-証明された B は A の仮定に依存していることを意味する。
+この時 A は alive な仮定であり、証明された B は A の仮定に依存していることを意味する。
 
 ここで、推論規則により記号 $ \Rightarrow $ を導入する。
 
@@ -52,9 +51,9 @@
     \UnaryInfC{$ A \Rightarrow B $}
 \end{prooftree}
 
-そうすると、仮定 A は dead となり、新たな命題 $ A \Rightarrow B $ を導くことができる。
+$ \Rightarrow \mathcal{I} $ を適用することで仮定 A は dead となり、新たな命題 $ A \Rightarrow B $ を導くことができる。
 A という仮定に依存して B を導く証明から、「A が存在すれば B が存在する」という証明を導いたこととなる。
-このように、仮定から始めて最終的に全ての仮定を dead とすることで、仮定に依存しない証明を導くことができる。
+このように、仮定から始めて最終的に全ての仮定を dead とすることで、仮定に依存しない証明を導ける。
 なお、dead な仮定は \verb/[A]/ のように \verb/[]/ で囲んで書く。
 
 alive な仮定を dead にすることができるのは $ \Rightarrow \mathcal{I} $ 規則のみである。
@@ -184,7 +183,7 @@
 \end{itemize}
 
 例として、natural deduction で三段論法を証明する。
-なお、三段論法とは「A は B であり、 B は C である。よって A は C である」といった文を示すこととする。
+なお、三段論法とは「A は B であり、 B は C である。よって A は C である」といった文を示す。
 
 \begin{prooftree}
     \AxiomC{ $ [A] $ $_{(1)}$}
@@ -337,7 +336,7 @@
 式の型に対する定義を正しく行なうことで証明を与える。
 
 $ \Rightarrow \mathcal{E} $ に対応する \verb/->E/ は関数の適用なので、値a と関数 f を受けとって適用することで B が得られる。
-なお、仮定を alive のまま証明を記述するのは依存した仮定を残すことになるため、必要な仮定を引数として受けとったり、implicit な parameter として指定して証明するのが良い。
+なお、仮定を alive のまま証明を記述するのは依存した仮定を残すため、必要な仮定を引数として受けとったり、implicit な parameter として指定して証明するのが良い。
 
 また、Agda は証明に用いる規則なども Agda 内部で定義することができる。
 例えば、直積型の定義はリスト\ref{src:product}のようなものがある。
@@ -435,8 +434,8 @@
     \lstinputlisting[label=src:three_plus_one, caption= Agda における 3 + 1 の結果が 4 と等しい証明] {src/three_plus_one.agda}
 \end{table}
 
-3+1 という1つの関数を定義し、その型として証明すべき式 \verb/(S (S (S O))) + (S O)≡(S (S (S (S O))))/ を記述する。
-そして証明を関数の定義として記述する。
+3+1 という関数を定義し、その型として証明すべき式 \verb/(S (S (S O))) + (S O)≡(S (S (S (S O))))/ を記述する。
+そして証明すべき式を関数の定義として記述する。
 今回は \verb/_+_/ 関数の定義により \verb/ (S (S (S (S O)))) / に簡約されるためにコンストラクタ refl が証明となる。
 
 $ \equiv $ によって証明する際、必ず同じ式に簡約されるとは限らないため、いくつかの操作が Relation.Binary.PropositionalEquality に定義されている。