--- a/slide/slide.html	Wed Feb 21 23:35:09 2018 +0900
+++ b/slide/slide.html	Thu Feb 22 00:23:06 2018 +0900
@@ -86,7 +86,7 @@
 <!-- === begin markdown block ===
 
       generated by markdown/1.2.0 on Ruby 2.4.1 (2017-03-22) [x86_64-darwin16]
-                on 2018-02-21 23:26:03 +0900 with Markdown engine kramdown (1.15.0)
+                on 2018-02-22 00:23:00 +0900 with Markdown engine kramdown (1.15.0)
                   using options {}
   -->
 
@@ -126,11 +126,10 @@
 <!-- _S9SLIDE_ -->
 <h2 id="agda-">Agda とは</h2>
 <ul>
-  <li>定理証明支援系</li>
-  <li>関数型言語</li>
+  <li>定理証明支援系の関数型言語</li>
   <li>型を明示する必要がある</li>
-  <li>インデントも意味を持つ</li>
-  <li>型システムを用いて証明を記述できる</li>
+  <li>また、インデントも意味を持つ</li>
+  <li>型に命題を入れ、関数部分に証明を記述する事ができる</li>
 </ul>
 
 
@@ -140,7 +139,7 @@
 <h2 id="agda--1">Agda の型、関数</h2>
 <ul>
   <li>例として singleLinkedStack の pop を使う</li>
-  <li>Agda の 型は <strong>関数名:型</strong> で定義される</li>
+  <li>Agda の 型は <strong>関数名 : 型</strong> で定義される</li>
   <li>Agda の 項、関数部分は <strong>関数名 = 値</strong></li>
   <li>なにかを受け取って計算して次の関数に継続する型(<strong>-&gt; (fa -&gt; t) -&gt; t</strong>)</li>
   <li>これはstackを受け取り、stackの先頭を取ってという処理を行い、次の関数に渡すという関数の型</li>
@@ -188,11 +187,7 @@
 <h2 id="agda">Agdaの関数</h2>
 <ul>
   <li>例として popSingleLinkedStack の関数を使う</li>
-  <li><strong>ラムダ式</strong> とは関数内で定義できる名前のない関数</li>
-  <li><strong>\ -&gt;</strong> で定義される</li>
-  <li>ラムダ式を使って CodeGear を継続することができる</li>
   <li>関数での引数は <strong>関数名 a b :</strong> のように書く</li>
-  <li><strong>{変数}</strong> のように記述すると暗黙的な意味になり省略してもよい</li>
 </ul>
 
 <pre lang="AGDA"><code>popSingleLinkedStack :  -&gt; SingleLinkedStack a -&gt; 
@@ -267,7 +262,7 @@
   <li>stackInSomeState で不定な Stack を作成し、そこに push し、直後に pop した値が push した値と等しいことを示している</li>
   <li>Agda 中では不明な部分を <strong>?</strong> と書くことができる</li>
   <li><strong>?</strong> 部分には値が入る</li>
-  <li>証明部分は ラムダ式で与える</li>
+  <li>証明部分はラムダ式で与える</li>
 </ul>
 
 <pre lang="AGDA"><code>stackInSomeState : {l m : Level } {D : Set l} {t : Set m } 
@@ -285,6 +280,21 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
+<h2 id="section-1">ラムダ式</h2>
+<ul>
+  <li>ラムダ式は関数内で無名の関数を定義することができる</li>
+  <li><strong>\s1 -&gt;</strong> はラムダ式で pushStack の次の CodeGear 部分にラムダ式を使いStackを継続している</li>
+</ul>
+
+<pre lang="AGDA"><code>push-&gt;push-&gt;pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) -&gt;
+    pushStack ( stackInSomeState s )  x ( \s1 -&gt; pushStack s1 y ( \s2 -&gt;
+    pop2Stack s2 ( \s3 y1 x1 -&gt; (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
 <h2 id="agda--interface--2">Agda での Interface を含めた部分的な証明</h2>
 <ul>
   <li>証明部分に書いた ? はコンパイル後に <strong>{ }0</strong> に変わり、中に入る型が表示される</li>
@@ -340,7 +350,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="section-1">今後の課題</h2>
+<h2 id="section-2">今後の課題</h2>
 <ul>
   <li>本研究では Agda での Interface の記述及び Interface を含めた一部の証明を行った。</li>
   <li>これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた。</li>

--- a/slide/slide.md	Wed Feb 21 23:35:09 2018 +0900
+++ b/slide/slide.md	Thu Feb 22 00:23:06 2018 +0900
@@ -26,11 +26,11 @@
 
 
 ## Agda とは
-* 定理証明支援系
-* 関数型言語
+* 定理証明支援系の関数型言語
 * 型を明示する必要がある
-* インデントも意味を持つ
-* 型システムを用いて証明を記述できる
+* また、インデントも意味を持つ
+* 型に命題を入れ、関数部分に証明を記述する事ができる
+
 
 ## Agda の型、関数
 * 例として singleLinkedStack の pop を使う
@@ -67,10 +67,7 @@
 
 ## Agdaの関数
 * 例として popSingleLinkedStack の関数を使う
-* ラムダ式を使って CodeGear を継続することができる
-* ラムダ式で**\ ->**書くことができる
 * 関数での引数は **関数名 a b :** のように書く
-* **{変数}** のように記述すると暗黙的な意味になり省略してもよい
 
 ```AGDA
 popSingleLinkedStack :  -> SingleLinkedStack a -> 
@@ -107,7 +104,6 @@
     next record {top = Just (record {datum = datum;next =(top stack)})}
 ```
 
-
 ## Agda での Interface の定義
 * stack の色々な実装を抽象的に表すために record を使い **StackMethods** をつくった
 * 実装時は関数の中で record を構築している
@@ -126,7 +122,7 @@
 * stackInSomeState で不定な Stack を作成し、そこに push し、直後に pop した値が push した値と等しいことを示している
 * Agda 中では不明な部分を **?** と書くことができる
 * **?** 部分には値が入る
-* 証明部分は ラムダ式で与える
+* 証明部分はラムダ式で与える
 
 ```AGDA
 stackInSomeState : {l m : Level } {D : Set l} {t : Set m } 
@@ -141,6 +137,17 @@
 push->push->pop2 {l} {D} x y s = ?
 ```
 
+## ラムダ式
+* ラムダ式は関数内で無名の関数を定義することができる
+* **\s1 ->** はラムダ式で pushStack の次の CodeGear 部分にラムダ式を使いStackを継続している
+
+```AGDA
+push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
+    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 ->
+    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+```
+
+
 ## Agda での Interface を含めた部分的な証明
 *  証明部分に書いた ? はコンパイル後に **{ }0** に変わり、中に入る型が表示される
 * x、y はMaybe なので Justで返ってくる