diff agda.tex @ 27:e30a02baba55

Fix function name
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 11 Feb 2015 12:37:46 +0900 (2015-02-11)
parents de3397af1f8d
children c684abcc781b
line wrap: on
line diff
--- a/agda.tex	Tue Feb 10 15:30:01 2015 +0900
+++ b/agda.tex	Wed Feb 11 12:37:46 2015 +0900
@@ -469,21 +469,21 @@
 
         $ O + (S m) \equiv (S m) + O $  を証明することになる。
         この等式は + の定義により $ O + (S m) \equiv S (m + O) $ と変形できる。
-        $ S (m + O) $ は $ m + O $ に S を加えたものであるため、 cong を用いて再帰的に \verb/add_sym/ を実行することで証明できる。
+        $ S (m + O) $ は $ m + O $ に S を加えたものであるため、 cong を用いて再帰的に \verb/addSym/ を実行することで証明できる。
 
         この2つの証明はこのような意味を持つ。
         n が 0 であるとき、 m も 0 なら簡約により等式が成立する。
         n が 0 であるとき、 m が 0 でないとき、 m は後続数である。
         よって m が (S x) と書かれる時、 x は m の前の値である。
         前の値による交換法則を用いてからその結果の後続数も + の定義により等しい。
-        ここで、 \verb/add_sym/ に渡される m は1つ値が減っているため、最終的には n = 0, m = 0 である refl にまで簡約され、等式が得られる。
+        ここで、 \verb/addSym/ に渡される m は1つ値が減っているため、最終的には n = 0, m = 0 である refl にまで簡約され、等式が得られる。
 
     \item n = S n, m = O
 
         $ (S n) + O \equiv O + (S n) $ を証明する。
         この等式は + の定義により $ S (n + O) \equiv (S n) $ と変形できる。
         さらに変形すれば $ S (n + O) \equiv S (O + n) $ となる。
-        よって \verb/add_sym/ により O と n を変換した後に cong で S を加えることで証明ができる。
+        よって \verb/addSym/ により O と n を変換した後に cong で S を加えることで証明ができる。
 
         ここで、 $ O + n  \equiv n $ は + の定義により自明であるが、$ n + O \equiv n $ をそのまま導出できないことに注意して欲しい。
         + の定義は左側の項から S を右側の項への移すだけであるため、右側の項への演算はしない。