changeset 13:e8655e0264b8

fix paper, slide
author ryokka
date Tue, 11 Feb 2020 02:31:26 +0900
parents bf3288c36d7e
children 19ab6b8055ea
files paper/abstract.tex paper/agda.tex paper/conclusion.tex paper/hoare.tex paper/master_paper.pdf paper/master_paper.tex paper/reference.bib paper/src/RedBlackTree.agda.replaced paper/src/agda-hoare-interpret.agda.replaced paper/src/agda-hoare-rule.agda.replaced paper/src/agda-hoare-soundness.agda.replaced paper/src/agda-hoare-write.agda.replaced paper/src/agda-mcg.agda.replaced paper/src/agda-mdg.agda.replaced paper/src/cbc-condition.agda.replaced paper/src/gears-while.agda.replaced paper/src/zero.agda paper/src/zero.agda.replaced slide/slide.html slide/slide.md slide/slide.pdf.html
diffstat 21 files changed, 556 insertions(+), 732 deletions(-) [+]
line wrap: on
line diff
--- a/paper/abstract.tex	Mon Feb 10 17:26:24 2020 +0900
+++ b/paper/abstract.tex	Tue Feb 11 02:31:26 2020 +0900
@@ -2,24 +2,24 @@
 
 OS やアプリケーションの信頼性は重要である。
 信頼性を上げるにはプログラムが仕様を満たしていることを検証する必要がある。
-プログラムの検証手法として、Floyd–Hoare logic (以下 Hoare Logic)が知られている。
+プログラムの検証手法として、Floyd–Hoare Logic (以下 Hoare Logic)が知られている。
 Hoare Logic は事前条件が成り立っているときにある関数を実行して、それが停止する際に事後条件を満たすことを確認することで、検証を行う。
-Hoare Logic はシンプルなアプローチであるが限定されたコマンド群やwhile programにしか適用されないことが多く、
+Hoare Logic はシンプルなアプローチであるが限定されたコマンド群や while programにしか適用されないことが多く、
 複雑な通常のプログラミング言語には向いていない。
 
 当研究室では信頼性の高い言語として Continuation based C (CbC)を開発している。
 CbC では CodeGear、DataGear という単位を用いてプログラムを記述する。
 
 CodeGearを Agda で継続渡しの記述を用いた関数として記述する。ここで
-AgdaはCurry Howard対応にもどつく定理証明系であり、それ自身が関数型プログラング言語でもある。
+Agda は Curry Howard 対応にもどつく定理証明系であり、それ自身が関数型プログラング言語でもある。
 Agda では条件を命題として記述することができるので、
 継続に事前条件や事後条件をもたせることができる。
 
-既存の言語では条件はassertなどで記述することになるが、その証明をそのプログラミング言語内で行うことはできない。
+既存の言語では条件は assert などで記述することになるが、その証明をそのプログラミング言語内で行うことはできない。
 Agdaでは証明そのもの、つまり命題に対する推論をλ項として記述することができるので、
-Hoare Logicの証明そのものを Meta Code Gearとして記述できる。これは既存の言語では不可能であった。
-ポイントは、プログラムそのものを Agda baseのCode Gearで記述できることである。
-Code Gearは入力と出力のみを持ち関数呼び出しせずにgoto的に継続実行する。この形式がそのまま
+Hoare Logicの証明そのものを Meta CodeGearとして記述できる。これは既存の言語では不可能であった。
+ポイントは、プログラムそのものを Agda baseのCodeGearで記述できることである。
+CodeGearは入力と出力のみを持ち関数呼び出しせずにgoto的に継続実行する。この形式がそのまま
 Hoare Logicのコマンドを自然に定義する。
 
 Hoare Logicの証明には3つの条件が必要である。一つは
@@ -40,8 +40,8 @@
 
 OS and application reliability are important.
 To increase reliability, verifications of program with specifications are necessary.
-Floyd-Hoare logic (hereafter Hoare Logic) is a welknown program verification method.
-Hoare Logic verifies the postonditions of a function are satisfied when the postconditions are satifiles.
+Floyd-Hoare logic (hereafter Hoare Logic) is a wellknown program verification method.
+Hoare Logic verifies the postonditions of a function are satisfied when the postconditions are satisfied.
 It also checks the halt condition of the program.
 Hoare Logic is a useful simple approach but often only applies to a limited set of commands and while programs.
 It is not generaly suitable for complex ordinary programming languages.
@@ -56,9 +56,9 @@
 
 In existing languages, conditions are described in asserts, etc., but the proof cannot be done in that programming language.
 Since Agda can describe the proof itself, that is, the inference among the propositions, as λ terms,
-The proof of Hoare Logic itself can be described as Meta Code Gear. This was not possible with existing languages.
-The point is that the program itself can be described with Code Gear of Agda base.
-Code Gear has only input and output, and executes continuously in a goto manner without calling a function. This format is
+The proof of Hoare Logic itself can be described as Meta CodeGear. This was not possible with existing languages.
+The point is that the program itself can be described with CodeGear of Agda base.
+CodeGear has only input and output, and executes continuously in a goto manner without calling a function. This format is
 naturally define Hoare Logic commands.
 
 Hoare Logic's proof requires three conditions. One,
--- a/paper/agda.tex	Mon Feb 10 17:26:24 2020 +0900
+++ b/paper/agda.tex	Tue Feb 11 02:31:26 2020 +0900
@@ -41,6 +41,8 @@
 値にコンストラクタとその型を列挙する。
 
 \coderef{agda-nat}は自然数の型である $\mathbb{N}$ (Natural Number)を例である。
+%% Agda では $\mathbb{N}$ のような utf8 の文字を扱う事ができる。なんで?
+%% 
 
 \lstinputlisting[label=agda-nat, caption=自然数を表すデータ型 Nat の定義] {src/nat.agda.replaced}
 
@@ -102,12 +104,13 @@
 
 \lstinputlisting[label=agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced}
 
-\section{Agda の関数での停止性}
-Agda では停止性の検出機能が存在し、プログラム中に停止しない記述が存在するとコンパイル時にエラーが出る。
+また Agda では停止性の検出機能が存在し、プログラム中に停止しない記述が存在するとコンパイル時にエラーが出る。
 \verb/{-# TERMINATING #-}/のタグを付けると停止しないプログラムをコンパイルすることができるがあまり望ましくない。
+\coderef{term} で書かれた、\verb/loop/ と \verb/stop/ は任意の自然数を受け取り、0になるまでループして0を返す関数である。
+\verb/loop/ では $\mathbb{N}$ の数を受け取り、 \verb/loop/ 自身を呼び出しながら 数を減らす関数 pred を呼んでいる。しかし、\verb/loop/の記述では関数が停止すると言えないため、定義するには\verb/{-# TERMINATING #-}/のタグが必要である。
+\verb/stop/ では自然数がパターンマッチで分けられ、\verb/zero/のときは \verb/zero/を返し、 \verb/suc n/ のときは \verb/suc/ を外した \verb/n/ で stop を実行するため停止する。
 
-ここでは停止する関数と停止しない関数の例\coderef{termination}を扱う。
-%% \lstinputlisting[label=termination, caption=停止する関数、停止しない関数] {src/terminating.agda.replaced}
+\lstinputlisting[label=term, caption=停止しない関数 loop、停止する関数 stop] {src/termination.agda.replaced}
 
 このように再帰的な定義の関数が停止するときは、何らかの値が減少する必要がある。
 
@@ -118,8 +121,9 @@
 ここでの \verb/+zero/ は右から \verb/zero/ を足しても $\equiv$ の両辺は等しいことを証明している。
 これは、引数として受けている \verb/y/ が \verb/Nat/ なので、 \verb/zero/ の時と \verb/suc y/ の二つの場合を証明する必要がある。
 
-\verb/y = zero/ の時は両辺が \verb/zero/ とできて、左右の項が等しいということを表す \verb/refl/ で証明することができる。
-\verb/y = suc y/ の時は $x \equiv y$ の時 $fx \equiv fy$ が成り立つという \verb/cong/ を使って、y の値を 1 減らしたのちに再帰的に \verb/+zero y/
+\verb/y = zero/ の時は $zero \equiv zero$ とできて、左右の項が等しいということを表す \verb/refl/ で証明することができる。
+\verb/y = suc y/ の時は $x \equiv y$ の時 $fx \equiv fy$ が成り立つという
+\verb/cong/ を使って、y の値を 1 減らしたのち、再帰的に \verb/+zero y/
 を用いて証明している。
 
 \lstinputlisting[caption=等式変形の例,label=proof]{src/zero.agda.replaced}
@@ -127,6 +131,9 @@
 %% +zero : { y : ℕ } → y + zero  ≡ y
 %% +zero {zero} = refl
 %% +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
+%%
+%% -- cong : ∀ (f : A → B) {x y} → x ≡ y → f x ≡ f y
+%% -- cong f refl = refl
 %% \end{lstlisting}
 
 また、他にも $\lambda$ 項部分で等式を変形する構文がいくつか存在している。
--- a/paper/conclusion.tex	Mon Feb 10 17:26:24 2020 +0900
+++ b/paper/conclusion.tex	Tue Feb 11 02:31:26 2020 +0900
@@ -32,13 +32,12 @@
 
 また、Meta DataGear で DataGear の関係等の制約条件を扱うことで、
 常に制約を満たすデータを作成することができる。
-予めそのようなデータをプログラムを使用することで、検証を行う際の記述が減ると思われる。
+予めそのようなデータをプログラムを使用することで、検証を行う際の記述減らすことができると考えている。
 これも同様に Binary Tree や RedBlack Tree などのデータ構造に適用し、
 検証の一助になると考えている。
 
 その他の課題としては、
 CbC で開発されている GearsOS に存在する並列構文の検証や、
+検証を行った Agda 上の CbC 記述から
+ノーマルレベルの CbC プログラムの生成などが挙げられる。
 
-Agda の CbC 記述から
-検証された CbC プログラムの生成などが挙げられる。
-
--- a/paper/hoare.tex	Mon Feb 10 17:26:24 2020 +0900
+++ b/paper/hoare.tex	Tue Feb 11 02:31:26 2020 +0900
@@ -89,7 +89,7 @@
 
 比較しやすいように \coderef{c-while} を \coderef{c-while2} に再掲した。
 
-\begin{lstlisting}[caption= while Loop (再掲),label=c-while-2]
+\begin{lstlisting}[caption= while Loop (再掲),label=c-while2]
 n = 10;
 i = 0;
 
@@ -125,8 +125,13 @@
 -- record { varn = 0 ; vari = 10 }
 \end{lstlisting}
 
-\section{While Program の部分正当性}
-ここでは先程記述した \coderef{agda-hoare-prog} の部分正当性の検証を行う。
+\section{while program の部分正当性}
+ここでは先程記述した \coderef{agda-hoare-prog} の検証を行う。
+Hoare Logic ではコマンドに対応した仕様が存在しており、それらを組み合わせた形で
+仕様を記述する必要がある。
+この仕様を記述する際、部分正当性が成り立っている必要がある。
+部分正当性とは Hoare Logic のコマンドが実行される前には事前条件が成り立っていて、
+コマンドが停止したとき事後条件が成り立っていることである。
 
 \coderef{hoare-rule} の \verb/HTProof/ は Agda 上での Hoare Logic でのコマンドに対応した性質を型としてまとめたものである。
 \verb/HTProof/ では Pre-Condition とコマンド、Post-Condition を受け取って定義される Agda のデータである。
@@ -152,8 +157,7 @@
 
 \lstinputlisting[caption=Axiom と Tautology,label=axiom-taut]{src/axiom-taut.agda.replaced}
 
-
-\coderef{hoare-rule}を使って \coderef{c-while}の WhileProgram の仕様を構成する。
+\coderef{hoare-rule}を使って \coderef{c-while}の while program の仕様を構成する。
 
 \lstinputlisting[caption=Agda での Hoare Locig の構成,label=hoare-rule]{src/agda-hoare-rule.agda.replaced}
 
@@ -164,8 +168,9 @@
 それぞれの Condition は Rule の後に記述されている \verb/{}/ に囲まれた部分で、
 \verb/initCond/のみ無条件で \verb/true/ を返す Condition になっている。
 
-それぞれの Rule の中にそこで証明する必要のある補題が \verb/lemma/ で埋められている。
-\verb/lemma1/ から \verb/lemma5/ の証明は概要のみを示し、全体は付録に載せる。
+それぞれの Rule の中にそれぞれの部分正当性を検証するための証明存在しており、
+それぞれ \verb/lemma/ で埋められている。
+\verb/lemma1/ から \verb/lemma5/ の証明は概要のみを示し、全体は付録に載せることにする。
 
 これらの lemma は HTProof の Rule に沿って必要なものを記述されており、
 \verb/lemma1/ では PreCondition と PostCondition が存在するときの代入の保証、
@@ -174,7 +179,7 @@
 \verb/lemma4/ では While Loop を抜けたときの Condition の整合性、
 \verb/lemma5/ では While Loop を抜けた後のループ不変条件からCondition への変換と termCond への移行の整合性を保証している。
 
-\lstinputlisting[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while]{src/agda-hoare-while.agda.replaced}
+\lstinputlisting[caption=while loop の検証用記述,label=agda-hoare-while]{src/agda-hoare-while.agda.replaced}
 %% \begin{lstlisting}[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while]  
 %% proof1 : HTProof initCond program termCond
 %% proof1 =
@@ -186,18 +191,17 @@
 %%                      $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5
 %% \end{lstlisting}
 
-proof1 は\coderef{agda-hoare-prog}の program と似た形をとっている。
-Hoare Logic では Comannd に対応する証明規則があるため、仕様はプログラムに対応している。
+Hoare Logic ではコマンドに対応した仕様が存在するため、 \verb/proof1/ は\coderef{agda-hoare-prog}の program に近い記述になる。
 
 
 \section{Hoare Logic での健全性}
 \coderef{agda-hoare-while} では Agda での Hoare Logic を用いた仕様の構成を行った。
-この仕様で実際に正しく動作するかどうか(健全性)を検証する必要がある。
+ここでは、\coderef{agda-hoare-while} で構成した仕様が
+実際に正しく動作するかどうか(健全性)の検証を行う。
 
-\coderef{agda-hoare-satisfies} は Hoare Logic 上での部分正当性を確かめるための関数である。
- \verb/SemComm/ では Comm を受け取って成り立つ関係を返す。
- \verb/Satisfies/ では Pre Condition と コマンド、 Post Condition を受け取って、
- Pre Condition から Post Condition を正しく導けるという仕様を返す。
+\coderef{agda-hoare-satisfies} の \verb/SemComm/ では各 Comm で成り立つ関係を返す。
+\verb/Satisfies/ では 事前条件 と コマンド、 事後条件 を受け取って、
+これらが、正しく Comm で成り立つ関係を構築する。
 
 \lstinputlisting[caption= State Sequence の部分正当性,label=agda-hoare-satisfies]{src/agda-hoare-satisfies.agda.replaced}
 
@@ -229,7 +233,7 @@
 %%       SemCond bPre s1 -> SemComm cm s1 s2 -> SemCond bPost s2
 %% \end{lstlisting}
 
-これらの仕様を検証することでそれぞれの コマンド に対する部分正当性を示す。
+実行する際、これらの関係を満たしていることで健全性が証明できる。
 
 \coderef{agda-hoare-soundness} の \verb/Soundness/ では \verb/HTProof/ を受け取り、 \verb/Satisfies/ に合った証明を返す。
 \verb/Soundness/ では \verb/HTProof/ に記述されている Rule でパターンマッチを行い、対応する証明を適応している。
Binary file paper/master_paper.pdf has changed
--- a/paper/master_paper.tex	Mon Feb 10 17:26:24 2020 +0900
+++ b/paper/master_paper.tex	Tue Feb 11 02:31:26 2020 +0900
@@ -19,6 +19,7 @@
 \usepackage{type1cm}
 \usepackage[usenames]{color}
 \usepackage{ulem}
+\usepackage{lstlinebgrd} 
 
 \jtitle{Continuation based C での Hoare Logic を用いた仕様記述と検証}
 %% \etitle{Hoare Logic based Specification and Verification in Continuation based C}
@@ -115,7 +116,6 @@
 \input{agda.tex}
 \input{hoare.tex}
 \input{cbc_agda.tex}
-%% \input{tree.tex}
 \input{cbc_hoare.tex}
 \input{conclusion.tex}
 
--- a/paper/reference.bib	Mon Feb 10 17:26:24 2020 +0900
+++ b/paper/reference.bib	Tue Feb 11 02:31:26 2020 +0900
@@ -116,7 +116,7 @@
 @misc{agda-alpa-old,
     title = {Example - Hoare Logic},
     howpublished = {\url{http://ocvs.cfv.jp/Agda/readmehoare.html}},
-    note = {Accessed: 2020/2/9(Sun)},
+    note = {Accessed: 2019/1/16(Wed)},
 }
 
 @misc{agda-alpa,
--- a/paper/src/RedBlackTree.agda.replaced	Mon Feb 10 17:26:24 2020 +0900
+++ b/paper/src/RedBlackTree.agda.replaced	Tue Feb 11 02:31:26 2020 +0900
@@ -51,7 +51,7 @@
 --
 -- put new node at parent node, and rebuild tree to the top
 --
-{-# TERMINATING #-}   -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html
+{-@$\#$@ TERMINATING @$\#$@-}   -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html
 replaceNode : {n m : Level } {t : Set m } {a k : Set n} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@  Node a k @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t
 replaceNode {n} {m} {t} {a} {k} tree s n0 next = popSingleLinkedStack s (
       \s parent @$\rightarrow$@ replaceNode1 s parent)
@@ -97,7 +97,7 @@
         ...                                    | EQ = rotateNext tree s (Just n1) parent 
         ...                                    | _ = rotateNext tree s (Just n1) parent 
 
-{-# TERMINATING #-}
+{-@$\#$@ TERMINATING @$\#$@-}
 insertCase5 : {n m : Level } {t : Set m } {a k : Set n} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ Node a k @$\rightarrow$@ Node a k @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t
 insertCase5 {n} {m} {t} {a} {k}  tree s n0 parent grandParent next = pop2SingleLinkedStack s (\ s parent grandParent @$\rightarrow$@ insertCase51 tree s n0 parent grandParent next)
   where
@@ -140,7 +140,7 @@
 colorNode : {n : Level } {a k : Set n}  @$\rightarrow$@ Node a k @$\rightarrow$@ Color  @$\rightarrow$@ Node a k
 colorNode old c = record old { color = c }
 
-{-# TERMINATING #-}
+{-@$\#$@ TERMINATING @$\#$@-}
 insertNode : {n m : Level } {t : Set m } {a k : Set n} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Node a k @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t
 insertNode {n} {m} {t} {a} {k}  tree s n0 next = get2SingleLinkedStack s (insertCase1 n0)
    where
--- a/paper/src/agda-hoare-interpret.agda.replaced	Mon Feb 10 17:26:24 2020 +0900
+++ b/paper/src/agda-hoare-interpret.agda.replaced	Tue Feb 11 02:31:26 2020 +0900
@@ -1,4 +1,4 @@
-{-# TERMINATING #-}
+{-@$\#$@ TERMINATING @$\#$@-}
 interpret : Env @$\rightarrow$@ Comm @$\rightarrow$@ Env
 interpret env Skip = env
 interpret env Abort = env
--- a/paper/src/agda-hoare-rule.agda.replaced	Mon Feb 10 17:26:24 2020 +0900
+++ b/paper/src/agda-hoare-rule.agda.replaced	Tue Feb 11 02:31:26 2020 +0900
@@ -19,9 +19,9 @@
   IfRule : {cmThen : Comm} @$\rightarrow$@ {cmElse : Comm} @$\rightarrow$@
            {bPre : Cond} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@
            {b : Cond} @$\rightarrow$@
-           HTProof (bPre /\ b) cmThen bPost @$\rightarrow$@
-           HTProof (bPre /\ neg b) cmElse bPost @$\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 /\ b) cm bInv @$\rightarrow$@
-              HTProof bInv (While b cm) (bInv /\ neg b)
+              HTProof (bInv @$\wedge$@ b) cm bInv @$\rightarrow$@
+              HTProof bInv (While b cm) (bInv @$\wedge$@ neg b)
--- a/paper/src/agda-hoare-soundness.agda.replaced	Mon Feb 10 17:26:24 2020 +0900
+++ b/paper/src/agda-hoare-soundness.agda.replaced	Tue Feb 11 02:31:26 2020 +0900
@@ -16,99 +16,51 @@
         hyp1 = Soundness pr1
         hyp2 : Satisfies bMid cm2 bPost
         hyp2 = Soundness pr2
-        sMid : State
-        sMid = proj@$\_{1}$@ q2
-        r1 : SemComm cm1 s1 sMid @$\times$@ SemComm cm2 sMid s2
-        r1 = proj@$\_{2}$@ q2
-        r2 : SemComm cm1 s1 sMid
-        r2 = proj@$\_{1}$@ r1
-        r3 : SemComm cm2 sMid s2
-        r3 = proj@$\_{2}$@ r1
-        r4 : SemCond bMid sMid
-        r4 = hyp1 s1 sMid q1 r2
-    in hyp2 sMid s2 r4 r3
+    in hyp2 (proj@$\_{1}$@ q2) s2 (hyp1 s1 (proj@$\_{1}$@ q2) q1 (proj@$\_{1}$@ (proj@$\_{2}$@ q2))) (proj@$\_{2}$@ (proj@$\_{2}$@ q2))
 Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse)
           s1 s2 q1 q2
-  = let hypThen : Satisfies (bPre /\ b) cmThen bPost
+  = let hypThen : Satisfies (bPre @$\wedge$@ b) cmThen bPost
         hypThen = Soundness pThen
-        hypElse : Satisfies (bPre /\ neg b) cmElse bPost
+        hypElse : Satisfies (bPre @$\wedge$@ neg b) cmElse bPost
         hypElse = Soundness pElse
-        rThen : RelOpState.comp
-                  (RelOpState.delta (SemCond b))
-                  (SemComm cmThen) s1 s2 @$\rightarrow$@
-                SemCond bPost s2
-        rThen = @$\lambda$@ h @$\rightarrow$@
-                  let t1 : SemCond b s1 @$\times$@ SemComm cmThen s1 s2
-                      t1 = (proj@$\_{2}$@ (RelOpState.deltaRestPre
-                                     (SemCond b)
-                                     (SemComm cmThen) s1 s2)) h
-                      t2 : SemCond (bPre /\ b) s1
-                      t2 = (proj@$\_{2}$@ (respAnd bPre b s1))
-                           (q1 , proj@$\_{1}$@ t1)
-                  in hypThen s1 s2 t2 (proj@$\_{2}$@ t1)
-        rElse : RelOpState.comp
-                  (RelOpState.delta (NotP (SemCond b)))
-                  (SemComm cmElse) s1 s2 @$\rightarrow$@
-                SemCond bPost s2
+        rThen : RelOpState.comp (RelOpState.delta (SemCond b))
+                  (SemComm cmThen) s1 s2 @$\rightarrow$@ SemCond bPost s2
+        rThen = @$\lambda$@ h @$\rightarrow$@ hypThen s1 s2 ((proj@$\_{2}$@ (respAnd bPre b s1)) (q1 , proj@$\_{1}$@ t1))
+          (proj@$\_{2}$@ ((proj@$\_{2}$@ (RelOpState.deltaRestPre (SemCond b) (SemComm cmThen) s1 s2)) h))
+        rElse : RelOpState.comp (RelOpState.delta (NotP (SemCond b)))
+                  (SemComm cmElse) s1 s2 @$\rightarrow$@ SemCond bPost s2
         rElse = @$\lambda$@ h @$\rightarrow$@
-                  let t10 : (NotP (SemCond b) s1) @$\times$@
-                            (SemComm cmElse s1 s2)
+                  let t10 : (NotP (SemCond b) s1) @$\times$@ (SemComm cmElse s1 s2)
                       t10 = proj@$\_{2}$@ (RelOpState.deltaRestPre
-                                    (NotP (SemCond b)) (SemComm cmElse) s1 s2)
-                            h
-                      t6 : SemCond (neg b) s1
-                      t6 = proj@$\_{2}$@ (respNeg b s1) (proj@$\_{1}$@ t10)
-                      t7 : SemComm cmElse s1 s2
-                      t7 = proj@$\_{2}$@ t10
-                      t8 : SemCond (bPre /\ neg b) s1
-                      t8 = proj@$\_{2}$@ (respAnd bPre (neg b) s1)
-                           (q1 , t6)
-                  in hypElse s1 s2 t8 t7
+                                  (NotP (SemCond b)) (SemComm cmElse) s1 s2) h
+                  in hypElse s1 s2 (proj@$\_{2}$@ (respAnd bPre (neg b) s1)
+                             (q1 , (proj@$\_{2}$@ (respNeg b s1) (proj@$\_{1}$@ t10)))) (proj@$\_{2}$@ t10)
     in when rThen rElse q2
 Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2
-  = proj@$\_{2}$@ (respAnd bInv (neg b) s2) t20
+  = proj@$\_{2}$@ (respAnd bInv (neg b) s2)
+          (lem1 (proj@$\_{1}$@ q2) s2 (proj@$\_{1}$@ t15) , proj@$\_{2}$@ (respNeg b s2) (proj@$\_{2}$@ t15))
     where
-      hyp : Satisfies (bInv /\ b) cm' bInv
+      hyp : Satisfies (bInv @$\wedge$@ b) cm' bInv
       hyp = Soundness pr
-      n : $mathbb{N}$
-      n = proj@$\_{1}$@ q2
-      Rel1 : $mathbb{N}$ @$\rightarrow$@ Rel State (Level.zero)
+      Rel1 : @$\mathbb{N}$@ @$\rightarrow$@ Rel State (Level.zero)
       Rel1 = @$\lambda$@ m @$\rightarrow$@
                RelOpState.repeat
                  m
                  (RelOpState.comp (RelOpState.delta (SemCond b))
                                   (SemComm cm'))
-      t1 : RelOpState.comp
-             (Rel1 n)
-             (RelOpState.delta (NotP (SemCond b))) s1 s2
-      t1 = proj@$\_{2}$@ q2
-      t15 : (Rel1 n s1 s2) @$\times$@ (NotP (SemCond b) s2)
+      t15 : (Rel1 (proj@$\_{1}$@ q2) s1 s2) @$\times$@ (NotP (SemCond b) s2)
       t15 = proj@$\_{2}$@ (RelOpState.deltaRestPost
-                    (NotP (SemCond b)) (Rel1 n) s1 s2)
-              t1
-      t16 : Rel1 n s1 s2
-      t16 = proj@$\_{1}$@ t15
-      t17 : NotP (SemCond b) s2
-      t17 = proj@$\_{2}$@ t15
-      lem1 : (m : $mathbb{N}$) @$\rightarrow$@ (ss2 : State) @$\rightarrow$@ Rel1 m s1 ss2 @$\rightarrow$@
-             SemCond bInv ss2
-      lem1 $mathbb{N}$.zero ss2 h
-        = substId1 State (proj@$\_{2}$@ h) (SemCond bInv) q1
-      lem1 ($mathbb{N}$.suc n) ss2 h
-        = let hyp2 : (z : State) @$\rightarrow$@ Rel1 n s1 z @$\rightarrow$@
+        (NotP (SemCond b)) (Rel1 (proj@$\_{1}$@ q2)) s1 s2) (proj@$\_{2}$@ q2)
+      lem1 : (m : @$\mathbb{N}$@) @$\rightarrow$@ (ss2 : State) @$\rightarrow$@ Rel1 m s1 ss2 @$\rightarrow$@ SemCond bInv ss2
+      lem1 zero ss2 h = substId1 State (proj@$\_{2}$@ h) (SemCond bInv) q1
+      lem1 (suc n) ss2 h
+    = let hyp2 : (z : State) @$\rightarrow$@ Rel1 (proj@$\_{1}$@ q2) s1 z @$\rightarrow$@
                      SemCond bInv z
               hyp2 = lem1 n
-              s20 : State
-              s20 = proj@$\_{1}$@ h
-              t21 : Rel1 n s1 s20
-              t21 = proj@$\_{1}$@ (proj@$\_{2}$@ h)
-              t22 : (SemCond b s20) @$\times$@ (SemComm cm' s20 ss2)
-              t22 = proj@$\_{2}$@ (RelOpState.deltaRestPre
-                            (SemCond b) (SemComm cm') s20 ss2)
+              t22 : (SemCond b (proj@$\_{1}$@ h)) @$\times$@ (SemComm cm' (proj@$\_{1}$@ h) ss2)
+              t22 = proj@$\_{2}$@ (RelOpState.deltaRestPre (SemCond b) (SemComm cm') (proj@$\_{1}$@ h) ss2)
                     (proj@$\_{2}$@ (proj@$\_{2}$@ h))
-              t23 : SemCond (bInv /\ b) s20
-              t23 = proj@$\_{2}$@ (respAnd bInv b s20)
-                    (hyp2 s20 t21 , proj@$\_{1}$@ t22)
-          in hyp s20 ss2 t23 (proj@$\_{2}$@ t22)
-      t20 : SemCond bInv s2 @$\times$@ SemCond (neg b) s2
-      t20 = lem1 n s2 t16 , proj@$\_{2}$@ (respNeg b s2) t17
+              t23 : SemCond (bInv @$\wedge$@ b) (proj@$\_{1}$@ h)
+              t23 = proj@$\_{2}$@ (respAnd bInv b (proj@$\_{1}$@ h))
+                (hyp2 (proj@$\_{1}$@ h) (proj@$\_{1}$@ (proj@$\_{2}$@ h)) , proj@$\_{1}$@ t22)
+      in hyp (proj@$\_{1}$@ h) ss2 t23 (proj@$\_{2}$@ t22)
--- a/paper/src/agda-hoare-write.agda.replaced	Mon Feb 10 17:26:24 2020 +0900
+++ b/paper/src/agda-hoare-write.agda.replaced	Tue Feb 11 02:31:26 2020 +0900
@@ -1,10 +1,14 @@
--- 通常の CodeGear
-whileLoop' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc) @$\rightarrow$@ (n @$\equiv$@ varn env) @$\rightarrow$@ (next : Envc @$\rightarrow$@ t) @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ t
+-- Nomal CodeGear
+whileLoop' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc)
+  @$\rightarrow$@ (n @$\equiv$@ varn env)
+  @$\rightarrow$@ (next : Envc @$\rightarrow$@ t)
+  @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ t
 whileLoop' zero env refl _ exit = exit env
 whileLoop' (suc n) env refl next _ = next (record env {varn = pred (varn env) ; vari = suc (vari env) })
 
--- Hoare Logic ベースの CodeGear
-whileLoopPwP' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc ) @$\rightarrow$@ (n @$\equiv$@ varn env) @$\rightarrow$@ (pre : varn env + vari env @$\equiv$@ c10 env)
+-- Hoare Logic base CodeGear
+whileLoopPwP' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc )
+  @$\rightarrow$@ (n @$\equiv$@ varn env) @$\rightarrow$@ (pre : varn env + vari env @$\equiv$@ c10 env)
   @$\rightarrow$@ (next : (env : Envc ) @$\rightarrow$@ (pred n @$\equiv$@ varn env) @$\rightarrow$@ (post : varn env + vari env @$\equiv$@ c10 env) @$\rightarrow$@ t)
   @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ (fin : vari env @$\equiv$@ c10 env)  @$\rightarrow$@ t) @$\rightarrow$@ t
 whileLoopPwP' zero env refl refl next exit = exit env refl
--- a/paper/src/agda-mcg.agda.replaced	Mon Feb 10 17:26:24 2020 +0900
+++ b/paper/src/agda-mcg.agda.replaced	Tue Feb 11 02:31:26 2020 +0900
@@ -1,5 +1,5 @@
 whileTestPwP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@
-             ((env : Envc ) @$\rightarrow$@ (mdg : (vari env @$\equiv$@ 0) /\ (varn env @$\equiv$@ c10 env)) @$\rightarrow$@ t) @$\rightarrow$@ t
+             ((env : Envc ) @$\rightarrow$@ (mdg : (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env)) @$\rightarrow$@ t) @$\rightarrow$@ t
 whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
   env : Envc
   env = whileTestP c10 ( @$\lambda$@ env @$\rightarrow$@ env )
--- a/paper/src/agda-mdg.agda.replaced	Mon Feb 10 17:26:24 2020 +0900
+++ b/paper/src/agda-mdg.agda.replaced	Tue Feb 11 02:31:26 2020 +0900
@@ -5,6 +5,6 @@
 
 
 whileTestStateP : whileTestState @$\rightarrow$@ Envc @$\rightarrow$@  Set
-whileTestStateP s1 env = (vari env @$\equiv$@ 0) /\ (varn env @$\equiv$@ c10 env)
+whileTestStateP s1 env = (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env)
 whileTestStateP s2 env = (varn env + vari env @$\equiv$@ c10 env)
 whileTestStateP sf env = (vari env @$\equiv$@ c10 env)
--- a/paper/src/cbc-condition.agda.replaced	Mon Feb 10 17:26:24 2020 +0900
+++ b/paper/src/cbc-condition.agda.replaced	Tue Feb 11 02:31:26 2020 +0900
@@ -4,6 +4,6 @@
   sf : whileTestState
 
 whileTestStateP : whileTestState @$\rightarrow$@ Envc @$\rightarrow$@  Set
-whileTestStateP s1 env = (vari env @$\equiv$@ 0) /\ (varn env @$\equiv$@ c10 env)
+whileTestStateP s1 env = (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env)
 whileTestStateP s2 env = (varn env + vari env @$\equiv$@ c10 env)
 whileTestStateP sf env = (vari env @$\equiv$@ c10 env)
--- a/paper/src/gears-while.agda.replaced	Mon Feb 10 17:26:24 2020 +0900
+++ b/paper/src/gears-while.agda.replaced	Tue Feb 11 02:31:26 2020 +0900
@@ -1,13 +1,13 @@
 whileTest : {l : Level} {t : Set l}  @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ (Code : (env : Env)  @$\rightarrow$@
-            ((vari env) @$\equiv$@ 0) /\ ((varn env) @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t
+            ((vari env) @$\equiv$@ 0) @$\wedge$@ ((varn env) @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t
 whileTest {_} {_} {c10} next = next env proof2
   where
     env : Env
     env = record {vari = 0 ; varn = c10}
-    proof2 : ((vari env) @$\equiv$@ 0) /\ ((varn env) @$\equiv$@ c10)
+    proof2 : ((vari env) @$\equiv$@ 0) @$\wedge$@ ((varn env) @$\equiv$@ c10)
     proof2 = record {pi1 = refl ; pi2 = refl}    
 
-conversion1 : {l : Level} {t : Set l } @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ ((vari env) @$\equiv$@ 0) /\ ((varn env) @$\equiv$@ c10)
+conversion1 : {l : Level} {t : Set l } @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ ((vari env) @$\equiv$@ 0) @$\wedge$@ ((varn env) @$\equiv$@ c10)
                @$\rightarrow$@ (Code : (env1 : Env) @$\rightarrow$@ (varn env1 + vari env1 @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t
 conversion1 env {c10} p1 next = next env proof4
    where
@@ -23,7 +23,7 @@
             c10
           @$\blacksquare$@
 
-{-# TERMINATING #-}
+{-@$\#$@ TERMINATING @$\#$@-}
 whileLoop : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ ((varn env) + (vari env) @$\equiv$@ c10) @$\rightarrow$@ (Code : Env @$\rightarrow$@ t) @$\rightarrow$@ t
 whileLoop env proof next with  ( suc zero  @$\leq$@? (varn  env) )
 whileLoop env proof next | no p = next env
--- a/paper/src/zero.agda	Mon Feb 10 17:26:24 2020 +0900
+++ b/paper/src/zero.agda	Tue Feb 11 02:31:26 2020 +0900
@@ -1,3 +1,6 @@
 +zero : { y : ℕ } → y + zero  ≡ y
 +zero {zero} = refl
-+zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
++zero {suc y} = cong suc ( +zero {y} )
+
+-- cong : ∀ (f : A → B) {x y} → x ≡ y → f x ≡ f y
+-- cong f refl = refl
--- a/paper/src/zero.agda.replaced	Mon Feb 10 17:26:24 2020 +0900
+++ b/paper/src/zero.agda.replaced	Tue Feb 11 02:31:26 2020 +0900
@@ -1,3 +1,6 @@
 +zero : { y : @$\mathbb{N}$@ } @$\rightarrow$@ y + zero  @$\equiv$@ y
 +zero {zero} = refl
-+zero {suc y} = cong ( @$\lambda$@ x @$\rightarrow$@ suc x ) ( +zero {y} )
++zero {suc y} = cong suc ( +zero {y} )
+
+-- cong : @$\forall$@ (f : A @$\rightarrow$@ B) {x y} @$\rightarrow$@ x @$\equiv$@ y @$\rightarrow$@ f x @$\equiv$@ f y
+-- cong f refl = refl
--- a/slide/slide.html	Mon Feb 10 17:26:24 2020 +0900
+++ b/slide/slide.html	Tue Feb 11 02:31:26 2020 +0900
@@ -135,25 +135,6 @@
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="gears-について">Gears について</h2>
-<ul>
-  <li><strong>Gears</strong> は当研究室で提案しているプログラム記述手法</li>
-  <li>処理の単位を <strong>CodeGear</strong> 、データの単位を <strong>DataGear</strong></li>
-  <li>CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す</li>
-  <li>Output の DataGear は次の CodeGear の Input として接続される
-<!-- [fig1](file://./fig/cgdg.pdf) --></li>
-  <li>CodeGear の接続処理などのメタ計算は Meta CodeGear として定義</li>
-  <li>Meta CodeGear で信頼性の検証を行う</li>
-</ul>
-<p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt="" width="60%" height="75%" /></p>
-<!-- <p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt=""  width="75%" height="75%"/></p> -->
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
 <h2 id="agda-のデータ型">Agda のデータ型</h2>
 <ul>
   <li><strong>データ型</strong>はプリミティブなデータ</li>
@@ -185,58 +166,22 @@
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="agda-のデータ型と-datagear">Agda のデータ型と DataGear</h2>
+<h2 id="agda-の関数">Agda の関数</h2>
 <ul>
-  <li><strong>DataGear</strong> は CodeGear でつかわれる引数をまとめたもの</li>
-  <li>Agda で使われる</li>
-</ul>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="agda-での-gears-の記述whiletest">Agda での Gears の記述(whileTest)</h2>
-<ul>
-  <li>Agda での CodeGear は継続渡し (CPS : Continuation Passing Style) で記述された関数</li>
-  <li><strong>{}</strong> は暗黙的(推論される)</li>
-  <li>継続渡しの関数は引数として継続を受け取って継続に計算結果を渡す</li>
-  <li>CodeGear の型は<strong>引数 → (Code : fa → t) → t</strong></li>
-  <li><strong>t</strong> は継続(最終的に返すもの)</li>
-  <li><strong>(Code : fa → t)</strong> は次の継続先
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  whileTest : {t : Set} → (c10 : Nat) 
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>                → (Code : Env → t) → t
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>  whileTest c10 next = next (record {varn = c10 
-<span class="line-numbers"><a href="#n4" name="n4">4</a></span>                                     ; vari = 0} )
+  <li>関数にも同様に型が必要
+    <div class="language-HASKELL highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  +1 : ℕ → ℕ
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>  +1 m = suc m
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span>  -- eval +1 zero
+<span class="line-numbers"><a href="#n5" name="n5">5</a></span>  -- return suc zero
 </pre></div>
 </div>
     </div>
   </li>
-</ul>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="agda-での-gears-の記述whileloop">Agda での Gears の記述(whileLoop)</h2>
-<ul>
-  <li>関数の動作を条件で変えたいときはパターンマッチを行う</li>
-  <li>whileLoop は varn が 0 より大きい間ループする
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  whileLoopPwP' : {t : Set} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>    → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env  → t)
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>    → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
-<span class="line-numbers"><a href="#n4" name="n4">4</a></span>  whileLoopPwP' zero env refl refl next exit = exit env refl
-<span class="line-numbers"><a href="#n5" name="n5">5</a></span>  whileLoopPwP' (suc n) env refl refl next exit =
-<span class="line-numbers"><a href="#n6" name="n6">6</a></span>    next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env))
-</pre></div>
-</div>
-    </div>
-  </li>
+  <li>関数の型は <strong>input → output</strong></li>
+  <li>複数入力がある場合は <strong>input1 → input2 → output</strong></li>
+  <li><strong>=</strong> の左側は関数名と引数、右側に実装</li>
 </ul>
 
 
@@ -248,112 +193,133 @@
 <h2 id="agda-での証明">Agda での証明</h2>
 <ul>
   <li>関数との違いは<strong>型が証明すべき論理式</strong>で<strong>関数自体がそれを満たす導出</strong>
-    <ul>
-      <li><strong>refl</strong> は <strong>x ≡ x</strong></li>
-      <li><strong>cong</strong> は 関数と x ≡ y 受け取って、x ≡ y の両辺に関数を適応しても等しいことが変わらないこと</li>
-    </ul>
+    <div class="language-HASKELL highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  +zero : { y : Nat } → y + zero ≡ y
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>  +zero {zero} = refl
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>  +zero {suc y} = cong suc ( +zero {y} )
+</pre></div>
+</div>
+    </div>
   </li>
+  <li><strong>refl</strong> は <strong>x ≡ x</strong></li>
+  <li><strong>cong</strong> は <strong>関数</strong> と等式を受け取って、等式の両辺に関数を適応しても等しくなること</li>
   <li><strong>+zero</strong> は任意の自然数の右から zero を足しても元の数と等しいことの証明
     <ul>
       <li><strong>y = zero</strong> のときは <strong>zero ≡ zero</strong> のため refl</li>
-      <li><strong>y = suc y</strong> のときは cong を使い y の数を減らして再帰的に<strong>+zero</strong>を行っている</li>
-      <li>y の数を減らしても大丈夫なことを cong の関数として受け取った数を suc する関数で保証している
-        <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>+zero : { y : Nat } → y + zero ≡ y
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>+zero {zero} = refl
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>+zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
-</pre></div>
-</div>
-        </div>
-      </li>
+      <li><strong>y = suc y</strong> のときは cong を使い y の数を減らして帰納的に証明している</li>
     </ul>
   </li>
 </ul>
 
-<!-- ## Agda での証明(項変換) -->
-<!-- <\!-- -- もしかしたら rewrite で代用しちゃうかも -\-> -->
-<!-- - **x + y ≡ y + x** の証明 **+-sym** -->
-<!-- - 項変換の例として引数が zero, suc y のパターンをみる -->
-<!-- - **zero + suc y**を変換して**suc y + zero**にする -->
-<!-- - begin の下の行に変形したい式を記述 -->
-<!-- - **≡⟨  ⟩** に変形規則、その次の行に変換した結果、 **∎** が項変換終了 -->
-<!-- ```AGDA -->
-<!-- +-sym : { x y : Nat } → x + y ≡ y + x -->
-<!-- +-sym {zero} {suc y} = let open ≡-Reasoning  in -->
-<!--           begin -->
-<!--             zero + suc y  -->
-<!--           ≡⟨⟩ -->
-<!--             suc y -->
-<!--           ≡⟨ sym +zero  ⟩ -->
-<!--             suc y + zero -->
-<!--           ∎ -->
-<!-- -- sym : Symmetric {A = A} _≡_ -->
-<!-- -- sym refl = refl -->
-<!-- -- +zero : { y : Nat } → y + zero ≡ y -->
-<!-- ``` -->
-
-<!-- ## Agda での証明(項変換) -->
-<!-- - **x + y ≡ y + x** の証明 **+-sym** -->
-<!-- - 項の変換には **rewrite** と  **** -->
-<!-- - begin の下の行に変形したい式を記述 -->
-<!-- - **≡⟨  ⟩** に変形規則、その次の行に変換した結果、 **∎** が項変換終了 -->
-<!-- ```AGDA -->
-<!-- +-comm : (x y : ℕ) → x + y ≡ y + x -->
-<!-- +-comm zero y rewrite (+zero {y}) = refl -->
-<!-- +-comm (suc x) y = let open ≡-Reasoning in -->
-<!--   begin -->
-<!--   suc (x + y) ≡⟨⟩ -->
-<!--   suc (x + y) ≡⟨ cong suc (+-comm x y) ⟩ -->
-<!--   suc (y + x) ≡⟨ sym (+-suc {y} {x}) ⟩ -->
-<!--   y + suc x ∎ -->
-
-<!-- -- +-suc : {x y : ℕ} → x + suc y ≡ suc (x + y) -->
-<!-- -- +-suc {zero} {y} = refl -->
-<!-- -- +-suc {suc x} {y} = cong suc (+-suc {x} {y}) -->
-<!-- ``` -->
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="hoare-logic-をベースとした-gears-での検証手法">Hoare Logic をベースとした Gears での検証手法</h2>
-<ul>
-  <li>今回 Hoare Logic で証明する次のようなコードを検証した</li>
-  <li>このプログラムは変数iとnをもち、 n&gt;0 の間nの値を減らし、i の値を増やす</li>
-  <li>n==0 のとき停止するため、終了時の変数の結果は i==10、n==0 になる
-    <div class="language-C highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> n = <span style="color:#00D">10</span>;
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span> i = <span style="color:#00D">0</span>;
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>
-<span class="line-numbers"><a href="#n4" name="n4">4</a></span> <span style="color:#080;font-weight:bold">while</span> (n&gt;<span style="color:#00D">0</span>)
-<span class="line-numbers"><a href="#n5" name="n5">5</a></span> {
-<span class="line-numbers"><a href="#n6" name="n6">6</a></span>   i++;
-<span class="line-numbers"><a href="#n7" name="n7">7</a></span>   n--;
-<span class="line-numbers"><a href="#n8" name="n8">8</a></span> }
-</pre></div>
-</div>
-    </div>
-  </li>
-</ul>
-
 
 
 </div>
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="gears-をベースにしたプログラム">Gears をベースにしたプログラム</h2>
+<h2 id="gears-について">Gears について</h2>
+<ul>
+  <li><strong>Gears</strong> は当研究室で提案しているプログラム記述手法</li>
+  <li>処理の単位を <strong>CodeGear</strong> 、データの単位を <strong>DataGear</strong></li>
+  <li>CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す</li>
+  <li>Output の DataGear は次の CodeGear の Input として接続される
+<!-- [fig1](file://./fig/cgdg.pdf) --></li>
+  <li>CodeGear の接続処理などのメタ計算は Meta CodeGear として定義</li>
+  <li>Meta CodeGear で信頼性の検証を行う</li>
+</ul>
+<p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt="" width="60%" height="75%" /></p>
+<!-- <p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt=""  width="75%" height="75%"/></p> -->
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="agda-での-datagear">Agda での DataGear</h2>
 <ul>
-  <li>test は whileTest と whileLoop を使った Gears のプログラム</li>
-  <li>whileTest の継続先にDataGear を受け取って whileLoop に渡す
-    <ul>
-      <li><strong>(λ 引数 → )</strong>は無名の関数で引数を受け取って継続する</li>
-    </ul>
+  <li><strong>DataGear</strong> は CodeGear でつかわれる引数をまとめたもの</li>
+  <li>Agda は CodeGear、 DataGear は検証メタ計算そのものと考えられる</li>
+  <li>DataGear は Agda の CodeGear で使われる<strong>全てのデータ</strong>に当たる</li>
+</ul>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="agda-での-codegear">Agda での CodeGear</h2>
+<ul>
+  <li>Agda での CodeGear は継続渡しで記述された関数
+    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  whileTest : {t : Set} → (c10 : Nat) 
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>                → (Code : Env → t) → t
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>  whileTest c10 next = next (record {varn = c10 
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span>                                     ; vari = 0} )
+</pre></div>
+</div>
+    </div>
   </li>
+  <li>CodeGear の型は<strong>引数 → (Code : fa → t) → t</strong></li>
+  <li><strong>(Code : fa → t)</strong> は継続先</li>
+  <li>引数として継続先を受け取って計算結果を渡す</li>
 </ul>
 
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="agda-での-gears-の記述whileloop">Agda での Gears の記述(whileLoop)</h2>
+<ul>
+  <li>関数の動作を条件で変えたいときはパターンマッチを行う
+    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  whileLoop : {l : Level} {t : Set l} → Envc 
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>     → (next : Envc → t) → (exit : Envc → t) → t
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>  whileLoop env@(record { c10 = _ ; varn = zero ; vari = _ }) _ exit = exit env
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span>  whileLoop record { c10 = _ ; varn = suc varn1 ; vari = vari } next _ = 
+<span class="line-numbers"><a href="#n5" name="n5">5</a></span>       next (record {c10 = _ ; varn = varn1 ; vari = suc vari })
+</pre></div>
+</div>
+    </div>
+  </li>
+  <li>whileLoop は varn が 0 より大きい間ループする</li>
+</ul>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="hoare-logic-をベースとした-gears-での検証手法">Hoare Logic をベースとした Gears での検証手法</h2>
+<div class="language-C highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>   n = <span style="color:#00D">10</span>;
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>   i = <span style="color:#00D">0</span>;
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span>   <span style="color:#080;font-weight:bold">while</span> (n&gt;<span style="color:#00D">0</span>)
+<span class="line-numbers"><a href="#n5" name="n5">5</a></span>   {
+<span class="line-numbers"><a href="#n6" name="n6">6</a></span>     i++;
+<span class="line-numbers"><a href="#n7" name="n7">7</a></span>     n--;
+<span class="line-numbers"><a href="#n8" name="n8">8</a></span>   }
+</pre></div>
+</div>
+</div>
+<ul>
+  <li>今回 Hoare Logic で証明する次のようなコードを検証した</li>
+  <li>このプログラムは変数iとnをもち、 n&gt;0 の間nの値を減らし、i の値を増やす</li>
+  <li>n ≡ 0 のとき停止するため、終了時の変数の結果は i ≡ 10、n ≡ 0 になる</li>
+</ul>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="gears-をベースにしたプログラム">Gears をベースにしたプログラム</h2>
 <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
   <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>    test : Env
 <span class="line-numbers"><a href="#n2" name="n2">2</a></span>    test = whileTest 10 (λ env → whileLoop env (λ env1 → env1))
@@ -363,6 +329,14 @@
 </pre></div>
 </div>
 </div>
+<ul>
+  <li>test は whileTest と whileLoop を実行した結果を返す関数</li>
+  <li>whileTest の継続先にDataGear を受け取って whileLoop に渡す
+    <ul>
+      <li><strong>(λ 引数 → )</strong>は無名の関数で引数を受け取って継続する</li>
+    </ul>
+  </li>
+</ul>
 
 
 
@@ -371,23 +345,22 @@
 <div class='slide'>
   <!-- _S9SLIDE_ -->
 <h2 id="gears-をベースにした-hoare-logic-と証明全体">Gears をベースにした Hoare Logic と証明(全体)</h2>
+<div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>    -- test = whileTest 10 (λ env → whileLoop env (λ env1 → env1))
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>    proofGears : {c10 :  Nat } → Set
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>    proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span>             conversion1 n p1  (λ n1 p2 → whileLoop' n1 p2 
+<span class="line-numbers"><a href="#n5" name="n5">5</a></span>             (λ n2 →  ( vari n2 ≡ c10 )))) 
+</pre></div>
+</div>
+</div>
 <ul>
   <li>proofGears は Hoare Logic をベースとした証明
     <ul>
       <li>先程のプログラムと違い、引数として証明も持っている</li>
     </ul>
   </li>
-  <li>whileTest’ の継続に conversion1、その継続に whileLoop’ が来て最後の継続に vari が c10 と等しい
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  -- test = whileTest 10 (λ env → whileLoop env (λ env1 → env1))
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>  proofGears : {c10 :  Nat } → Set
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>  proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →
-<span class="line-numbers"><a href="#n4" name="n4">4</a></span>           conversion1 n p1  (λ n1 p2 → whileLoop' n1 p2 
-<span class="line-numbers"><a href="#n5" name="n5">5</a></span>           (λ n2 →  ( vari n2 ≡ c10 )))) 
-</pre></div>
-</div>
-    </div>
-  </li>
+  <li>whileTest’ の継続に conversion1、その継続に whileLoop’ が来て最後の継続に vari が c10 と等しい</li>
 </ul>
 
 
@@ -397,29 +370,23 @@
 <div class='slide'>
   <!-- _S9SLIDE_ -->
 <h2 id="gears-と-hoare-logic-をベースにした証明whiletest">Gears と Hoare Logic をベースにした証明(whileTest)</h2>
+<div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>    whileTest' : {l : Level} {t : Set l} {c10 :  ℕ } 
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>      → (Code : (env : Env )  → ((vari env) ≡ 0) ∧ ((varn env) ≡ c10) → t) → t
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>    whileTest' {_} {_}  {c10} next = next 
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span>      (record env {vari = 0 ; varn = c10 }) (record {pi1 = refl ; pi2 = refl})
+</pre></div>
+</div>
+</div>
 <ul>
-  <li>最初の Command なので PreCondition がない</li>
-  <li>proof2は Post Condition が成り立つことの証明
+  <li>最初の Command なので PreCondition はない</li>
+  <li>(record {pi1 = refl ; pi2 = refl}) は <strong>(vari env) ≡ 0</strong> と <strong>(varn env) ≡ c10</strong>の証明
     <ul>
-      <li><strong><em>/\</em></strong> は pi1 と pi2 のフィールドをもつレコード型</li>
-      <li>これは2つのものを引数に取り、両方が同時に成り立つことを表している</li>
-      <li><strong>refl</strong> は <strong>x == x</strong> で左右の項が等しいことの証明</li>
+      <li><strong><em>∧</em></strong> は pi1 と pi2 のフィールドをもつレコード型</li>
+      <li>両方とも成り立つので <strong>refl</strong></li>
     </ul>
   </li>
-  <li>Gears での PostCondition は <strong>引数 → (Code : fa → PostCondition → t) → t</strong>
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  whileTest' : {l : Level} {t : Set l} {c10 :  ℕ } 
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>    → (Code : (env : Env )  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>  whileTest' {_} {_}  {c10} next = next env proof2
-<span class="line-numbers"><a href="#n4" name="n4">4</a></span>    where
-<span class="line-numbers"><a href="#n5" name="n5">5</a></span>      env : Env
-<span class="line-numbers"><a href="#n6" name="n6">6</a></span>      env = record {vari = 0 ; varn = c10 }
-<span class="line-numbers"><a href="#n7" name="n7">7</a></span>      proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition
-<span class="line-numbers"><a href="#n8" name="n8">8</a></span>      proof2 = record {pi1 = refl ; pi2 = refl}
-</pre></div>
-</div>
-    </div>
-  </li>
+  <li>Gears での PostCondition は <strong>引数 → (Code : fa → PostCondition → t) → t</strong></li>
 </ul>
 
 
@@ -429,45 +396,32 @@
 <div class='slide'>
   <!-- _S9SLIDE_ -->
 <h2 id="gears-と-hoare-logic-をベースにした証明conversion">Gears と Hoare Logic をベースにした証明(conversion)</h2>
-<ul>
-  <li>conversion は Condition から LoopInvaliant への変換を行う CodeGear
-    <ul>
-      <li>Condition の条件は Loop 内では厳しいのでゆるくする</li>
-    </ul>
-  </li>
-  <li>proof4 は LoopInvaliant の証明</li>
-</ul>
-
 <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>    conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>    conv : (env : Envc ) → (vari env ≡ 0) ∧ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
 <span class="line-numbers"><a href="#n2" name="n2">2</a></span>    conv e record { pi1 = refl ; pi2 = refl } = +zero
 </pre></div>
 </div>
 </div>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="hoare-logic-の証明">Hoare Logic の証明</h2>
 <ul>
-  <li>Hoare Logic の証明では基本的に項の書き換えを行って証明している</li>
-  <li>proof4 の証明部分では論理式の<strong>varn env + vari env</strong> を 書き換えて <strong>c10</strong> に変換している</li>
-  <li>変換で使っている <strong>cong</strong> は 関数と x ≡ y 受け取って両辺に関数を適応しても等しいことが変わらないことの証明</li>
-  <li>変換後の式を次の行に書いて変換を続ける
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  conv1 : {l : Level} {t : Set l } → (env : Envc )
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>    → ((vari env) ≡ 0) /\ ((varn env) ≡ (c10 env))
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>    → (Code : (env1 : Envc ) → (varn env1 + vari env1 ≡ (c10 env1)) → t) → t
-<span class="line-numbers"><a href="#n4" name="n4">4</a></span>  conv1 env record { pi1 = refl ; pi2 = refl } next = next env +zero
-</pre></div>
-</div>
-    </div>
+  <li>conv は制約を緩める CodeGear
+    <ul>
+      <li><strong>(vari env ≡ 0) ∧ (varn env ≡ c10 env)</strong> が成り立つとき <strong>varn env + vari env ≡ c10 env</strong> が成り立つ</li>
+    </ul>
   </li>
 </ul>
 
+<!-- ##  Hoare Logic の証明 -->
+<!-- - Hoare Logic の証明では基本的に項の書き換えを行って証明している -->
+<!-- - proof4 の証明部分では論理式の**varn env + vari env** を 書き換えて **c10** に変換している -->
+<!-- - 変換で使っている **cong** は 関数と x ≡ y 受け取って両辺に関数を適応しても等しいことが変わらないことの証明 -->
+<!-- - 変換後の式を次の行に書いて変換を続ける -->
+<!-- ```AGDA -->
+<!--     conv1 : {l : Level} {t : Set l } → (env : Envc ) -->
+<!--       → ((vari env) ≡ 0) /\ ((varn env) ≡ (c10 env)) -->
+<!--       → (Code : (env1 : Envc ) → (varn env1 + vari env1 ≡ (c10 env1)) → t) → t -->
+<!--     conv1 env record { pi1 = refl ; pi2 = refl } next = next env +zero -->
+<!-- ``` -->
+
 
 
 </div>
@@ -475,11 +429,6 @@
 <div class='slide'>
   <!-- _S9SLIDE_ -->
 <h2 id="gears-と-hoare-logic-をベースにした証明whileloop">Gears と Hoare Logic をベースにした証明(whileLoop)</h2>
-<ul>
-  <li>whileLoop も whileTest と同様に PreCondition が CodeGear に入りそれに対する証明が記述されている</li>
-  <li>ループステップごとに <strong>whileLoopPwP’</strong> で停止か継続かを判断し、 <strong>loopPwP’</strong> でループが回る</li>
-</ul>
-
 <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
   <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span>    whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env
 <span class="line-numbers"> <a href="#n2" name="n2">2</a></span>      → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env  → t)
@@ -494,6 +443,10 @@
 </pre></div>
 </div>
 </div>
+<ul>
+  <li>whileLoop も whileTest と同様に PreCondition が CodeGear に入りそれに対する証明が記述されている</li>
+  <li>ループが回るごとに、<strong>whileLoopPwP’</strong> で停止か継続かを判断し、 <strong>loopPwP’</strong> でループが回る</li>
+</ul>
 
 
 
@@ -502,10 +455,6 @@
 <div class='slide'>
   <!-- _S9SLIDE_ -->
 <h2 id="gears-と-hoare-logic-をベースにした仕様記述">Gears と Hoare Logic をベースにした仕様記述</h2>
-<ul>
-  <li><strong>proofGears</strong> では最終状態が i と c10 が等しくなるため仕様になっている</li>
-</ul>
-
 <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
   <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>    whileProofs : (c :  ℕ ) → Set
 <span class="line-numbers"><a href="#n2" name="n2">2</a></span>    whileProofs c = whileTestPwP {_} {_} c 
@@ -515,6 +464,9 @@
 </pre></div>
 </div>
 </div>
+<ul>
+  <li><strong>whileProofs</strong> では最終状態が vari と c10 が等しくなるため仕様になっている</li>
+</ul>
 
 
 
@@ -523,11 +475,6 @@
 <div class='slide'>
   <!-- _S9SLIDE_ -->
 <h2 id="gears-と-hoare-logic-を用いた仕様の証明">Gears と Hoare Logic を用いた仕様の証明</h2>
-<ul>
-  <li>先程の <strong>whileProofs</strong> で行った仕様記述を型に記述し、実際に証明していく</li>
-  <li>このままだと loopPwP’ のループが進まず証明できない</li>
-</ul>
-
 <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
   <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span>--    whileProofs c = whileTestPwP {_} {_} c 
 <span class="line-numbers"> <a href="#n2" name="n2">2</a></span>--       ( λ env s → conv1 env s 
@@ -550,6 +497,10 @@
 </pre></div>
 </div>
 </div>
+<ul>
+  <li>先程の <strong>whileProofs</strong> で行った仕様記述を型に記述し、実際に証明していく</li>
+  <li>しかし loopPwP’ のループが進まず証明できない</li>
+</ul>
 
 
 
@@ -558,11 +509,6 @@
 <div class='slide'>
   <!-- _S9SLIDE_ -->
 <h2 id="検証時の-loop-の解決">検証時の Loop の解決</h2>
-<ul>
-  <li><strong>loopHelper</strong> は今回のループを解決する証明</li>
-  <li>ループ解決のためにループの簡約ができた</li>
-</ul>
-
 <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
   <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>    loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) → (seq : whileTestStateP s2 env) 
 <span class="line-numbers"><a href="#n2" name="n2">2</a></span>      → loopPwP' n env (sym eq) seq (λ env₁ x → (vari env₁ ≡ c10 env₁))
@@ -572,6 +518,10 @@
 </pre></div>
 </div>
 </div>
+<ul>
+  <li><strong>loopHelper</strong> は今回のループを解決する証明</li>
+  <li>ループ解決のためにループの簡約ができた</li>
+</ul>
 
 
 
@@ -580,10 +530,6 @@
 <div class='slide'>
   <!-- _S9SLIDE_ -->
 <h2 id="gears-と-hoare-logic-を用いた仕様の証明完成">Gears と Hoare Logic を用いた仕様の証明(完成)</h2>
-<ul>
-  <li><strong>loopHelper</strong> を使って簡約することで <strong>whileProofs</strong> の証明を行うことができた</li>
-</ul>
-
 <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
   <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>    --    whileProofs c = whileTestPwP {_} {_} c 
 <span class="line-numbers"><a href="#n2" name="n2">2</a></span>    --       ( λ env s → conv1 env s 
@@ -595,9 +541,9 @@
 </pre></div>
 </div>
 </div>
-
-<!-- ## Binary Tree について -->
-<!-- -  -->
+<ul>
+  <li><strong>loopHelper</strong> を使って簡約することで <strong>whileProofs</strong> の証明を行うことができた</li>
+</ul>
 
 
 
--- a/slide/slide.md	Mon Feb 10 17:26:24 2020 +0900
+++ b/slide/slide.md	Tue Feb 11 02:31:26 2020 +0900
@@ -30,17 +30,6 @@
 - 定理証明支援機の Agda 上で Gears 単位を用いた検証を行う
 - 本研究では Gears 単位を用いた Hoare Logic ベースの検証手法を提案する
 
-## Gears について
-- **Gears** は当研究室で提案しているプログラム記述手法
-- 処理の単位を **CodeGear** 、データの単位を **DataGear**
-- CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す
-- Output の DataGear は次の CodeGear の Input として接続される
-<!-- [fig1](file://./fig/cgdg.pdf) -->
-- CodeGear の接続処理などのメタ計算は Meta CodeGear として定義
-- Meta CodeGear で信頼性の検証を行う
-<p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt=""  width="60%" height="75%"/></p>
-<!-- <p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt=""  width="75%" height="75%"/></p> -->
-
 ## Agda のデータ型
 - **データ型**はプリミティブなデータ
 - この型のとき値は一意に定まる
@@ -58,94 +47,72 @@
           vari : Nat
 ```
 
-## Agda のデータ型と DataGear
-- **DataGear** は CodeGear でつかわれる引数をまとめたもの
-- Agda は CodeGear、 DataGear は検証メタ計算そのものと考えられる
-- DataGear は Agda の CodeGear で使われる**全てのデータ**に当たる
+## Agda の関数
+- 関数にも同様に型が必要
+```HASKELL
+    +1 : ℕ → ℕ
+    +1 m = suc m
+
+    -- eval +1 zero
+    -- return suc zero
+```
+- 関数の型は **input → output**
+- 複数入力がある場合は **input1 → input2 → output**
+- **=** の左側は関数名と引数、右側に実装
 
-## Agda の関数
-- Agda の関数はほにゃらら
+## Agda での証明
+- 関数との違いは**型が証明すべき論理式**で**関数自体がそれを満たす導出**
+```HASKELL
+    +zero : { y : Nat } → y + zero ≡ y
+    +zero {zero} = refl
+    +zero {suc y} = cong suc ( +zero {y} )
+```
+- **refl** は **x ≡ x**
+- **cong** は **関数** と等式を受け取って、等式の両辺に関数を適応しても等しくなること
+- **+zero** は任意の自然数の右から zero を足しても元の数と等しいことの証明
+  - **y = zero** のときは **zero ≡ zero** のため refl
+  - **y = suc y** のときは cong を使い y の数を減らして帰納的に証明している
 
-## Agda での Gears の記述(whileTest)
+## Gears について
+- **Gears** は当研究室で提案しているプログラム記述手法
+- 処理の単位を **CodeGear** 、データの単位を **DataGear**
+- CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す
+- Output の DataGear は次の CodeGear の Input として接続される
+<!-- [fig1](file://./fig/cgdg.pdf) -->
+- CodeGear の接続処理などのメタ計算は Meta CodeGear として定義
+- Meta CodeGear で信頼性の検証を行う
+<p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt=""  width="60%" height="75%"/></p>
+<!-- <p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt=""  width="75%" height="75%"/></p> -->
+
+## Agda での DataGear
+- **DataGear** は CodeGear でつかわれる引数をまとめたもの
+- Agda は CbC の上位言語
+  - メタ計算を含めて記述できる
+- DataGear は Agda の CodeGear で使うことのできる**全てのデータ**
+
+
+## Agda での CodeGear
 - Agda での CodeGear は継続渡しで記述された関数
-- 継続渡しの関数は引数として継続を受け取って継続に計算結果を渡す
-- CodeGear の型は**引数 → (Code : fa → t) → t**
-- **t** は継続(最終的に返すもの)
-- **(Code : fa → t)** は次の継続先
 ```AGDA
     whileTest : {t : Set} → (c10 : Nat) 
                   → (Code : Env → t) → t
     whileTest c10 next = next (record {varn = c10 
                                        ; vari = 0} )
 ```
+- CodeGear の型は継続先を返す関数
+- **(Code : fa → t)** は継続先
+- 引数として継続先の CodeGear を受け取る
 
 ## Agda での Gears の記述(whileLoop)
 - 関数の動作を条件で変えたいときはパターンマッチを行う
-- whileLoop は varn が 0 より大きい間ループする
 ```AGDA
-    whileLoopPwP' : {t : Set} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env
-      → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env  → t)
-      → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
-    whileLoopPwP' zero env refl refl next exit = exit env refl
-    whileLoopPwP' (suc n) env refl refl next exit =
-      next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env))
-```
-
-## Agda での証明
-```AGDA
-    +zero : { y : Nat } → y + zero ≡ y
-    +zero {zero} = refl
-    +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
+    whileLoop : {l : Level} {t : Set l} → Envc 
+       → (next : Envc → t) → (exit : Envc → t) → t
+    whileLoop env@(record { c10 = _ ; varn = zero ; vari = _ }) _ exit = exit env
+    whileLoop record { c10 = _ ; varn = suc varn1 ; vari = vari } next _ = 
+         next (record {c10 = _ ; varn = varn1 ; vari = suc vari })
 ```
-- 関数との違いは**型が証明すべき論理式**で**関数自体がそれを満たす導出**
-  - **refl** は **x ≡ x**
-  - **cong** は 関数と x ≡ y 受け取って、x ≡ y の両辺に関数を適応しても等しいことが変わらないこと
-- **+zero** は任意の自然数の右から zero を足しても元の数と等しいことの証明
-  - **y = zero** のときは **zero ≡ zero** のため refl
-  - **y = suc y** のときは cong を使い y の数を減らして再帰的に**+zero**を行っている
-  - y の数を減らしても大丈夫なことを cong の関数として受け取った数を suc する関数で保証している
-
-<!-- ## Agda での証明(項変換) -->
-<!-- <\!-- -- もしかしたら rewrite で代用しちゃうかも -\-> -->
-<!-- - **x + y ≡ y + x** の証明 **+-sym** -->
-<!-- - 項変換の例として引数が zero, suc y のパターンをみる -->
-<!-- - **zero + suc y**を変換して**suc y + zero**にする -->
-<!-- - begin の下の行に変形したい式を記述 -->
-<!-- - **≡⟨  ⟩** に変形規則、その次の行に変換した結果、 **∎** が項変換終了 -->
-<!-- ```AGDA -->
-<!-- +-sym : { x y : Nat } → x + y ≡ y + x -->
-<!-- +-sym {zero} {suc y} = let open ≡-Reasoning  in -->
-<!--           begin -->
-<!--             zero + suc y  -->
-<!--           ≡⟨⟩ -->
-<!--             suc y -->
-<!--           ≡⟨ sym +zero  ⟩ -->
-<!--             suc y + zero -->
-<!--           ∎ -->
-<!-- -- sym : Symmetric {A = A} _≡_ -->
-<!-- -- sym refl = refl -->
-<!-- -- +zero : { y : Nat } → y + zero ≡ y -->
-<!-- ``` -->
-
-<!-- ## Agda での証明(項変換) -->
-<!-- - **x + y ≡ y + x** の証明 **+-sym** -->
-<!-- - 項の変換には **rewrite** と  **** -->
-<!-- - begin の下の行に変形したい式を記述 -->
-<!-- - **≡⟨  ⟩** に変形規則、その次の行に変換した結果、 **∎** が項変換終了 -->
-<!-- ```AGDA -->
-<!-- +-comm : (x y : ℕ) → x + y ≡ y + x -->
-<!-- +-comm zero y rewrite (+zero {y}) = refl -->
-<!-- +-comm (suc x) y = let open ≡-Reasoning in -->
-<!--   begin -->
-<!--   suc (x + y) ≡⟨⟩ -->
-<!--   suc (x + y) ≡⟨ cong suc (+-comm x y) ⟩ -->
-<!--   suc (y + x) ≡⟨ sym (+-suc {y} {x}) ⟩ -->
-<!--   y + suc x ∎ -->
-
-<!-- -- +-suc : {x y : ℕ} → x + suc y ≡ suc (x + y) -->
-<!-- -- +-suc {zero} {y} = refl -->
-<!-- -- +-suc {suc x} {y} = cong suc (+-suc {x} {y}) -->
-<!-- ``` -->
+- whileLoop は varn が 0 より大きい間ループする
 
 
 ## Hoare Logic をベースとした Gears での検証手法
@@ -161,7 +128,7 @@
 ```
 - 今回 Hoare Logic で証明する次のようなコードを検証した
 - このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす
-- n==0 のとき停止するため、終了時の変数の結果は i==10、n==0 になる
+- n ≡ 0 のとき停止するため、終了時の変数の結果は i ≡ 10、n ≡ 0 になる
 
 ## Gears をベースにしたプログラム
 ```AGDA
@@ -171,7 +138,7 @@
     -- whileTest : {t : Set} → (c10 : Nat) → (Code : Env → t) → t
     -- whileLoop : {t : Set} → Env → (Code : Env → t) → t
 ```
-- test は whileTest と whileLoop を使った Gears のプログラム
+- test は whileTest と whileLoop を実行した結果を返す関数
 - whileTest の継続先にDataGear を受け取って whileLoop に渡す
   - **(λ 引数 → )**は無名の関数で引数を受け取って継続する
 
@@ -189,27 +156,25 @@
 - whileTest' の継続に conversion1、その継続に whileLoop' が来て最後の継続に vari が c10 と等しい
 
 ## Gears と Hoare Logic をベースにした証明(whileTest)
-- 最初の Command なので PreCondition がない
-- proof2は Post Condition が成り立つことの証明
-  - **_/\\_** は pi1 と pi2 のフィールドをもつレコード型
-  - これは2つのものを引数に取り、両方が同時に成り立つことを表している
-  - **refl** は **x == x** で左右の項が等しいことの証明
-- Gears での PostCondition は **引数 → (Code : fa → PostCondition → t) → t**
 ```AGDA
     whileTest' : {l : Level} {t : Set l} {c10 :  ℕ } 
-      → (Code : (env : Env )  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
+      → (Code : (env : Env )  → ((vari env) ≡ 0) ∧ ((varn env) ≡ c10) → t) → t
     whileTest' {_} {_}  {c10} next = next 
       (record env {vari = 0 ; varn = c10 }) (record {pi1 = refl ; pi2 = refl})
 ```
+- 最初の Command なので PreCondition はない
+- (record {pi1 = refl ; pi2 = refl}) は **(vari env) ≡ 0** と **(varn env) ≡ c10**の証明
+  - **_∧_** は pi1 と pi2 のフィールドをもつレコード型
+  - 両方とも成り立つので **refl**
+- Gears での PostCondition は **引数 → (Code : fa → PostCondition → t) → t**
 
 ## Gears と Hoare Logic をベースにした証明(conversion)
 ```AGDA
-    conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
+    conv : (env : Envc ) → (vari env ≡ 0) ∧ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
     conv e record { pi1 = refl ; pi2 = refl } = +zero
 ```
-- conversion は Condition から LoopInvaliant への変換を行う CodeGear
-  - Condition の条件では Loop 内では厳しいのでゆるめる
-
+- conv は制約を緩める CodeGear
+  - **(vari env ≡ 0) ∧ (varn env ≡ c10 env)** が成り立つとき **varn env + vari env ≡ c10 env** が成り立つ
 
 <!-- ##  Hoare Logic の証明 -->
 <!-- - Hoare Logic の証明では基本的に項の書き換えを行って証明している -->
@@ -224,9 +189,6 @@
 <!-- ``` -->
 
 ## Gears と Hoare Logic をベースにした証明(whileLoop)
-- whileLoop も whileTest と同様に PreCondition が CodeGear に入りそれに対する証明が記述されている
-- ループステップごとに **whileLoopPwP'** で停止か継続かを判断し、 **loopPwP'** でループが回る
-
 ```AGDA
     whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env
       → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env  → t)
@@ -239,10 +201,11 @@
     loopPwP' (suc n) env refl refl exit  = whileLoopPwP' (suc n) env refl refl 
         (λ env x y → loopPwP' n env x y exit) exit
 ```
+- whileLoop も whileTest と同様に PreCondition が CodeGear に入りそれに対する証明が記述されている
+- ループが回るごとに、**whileLoopPwP'** で停止か継続かを判断し、 **loopPwP'** でループが回る
+
 
 ## Gears と Hoare Logic をベースにした仕様記述
-- **whileProofs** では最終状態が vari と c10 が等しくなるため仕様になっている
-
 ```AGDA
     whileProofs : (c :  ℕ ) → Set
     whileProofs c = whileTestPwP {_} {_} c 
@@ -250,12 +213,11 @@
        ( λ env s → loopPwP' (varn env) env refl s 
        ( λ env s → vari env ≡ c10 env )))
 ```
+- **whileProofs** では最終状態が vari と c10 が等しくなるため仕様になっている
+
 
 
 ## Gears と Hoare Logic を用いた仕様の証明
-- 先程の **whileProofs** で行った仕様記述を型に記述し、実際に証明していく
-- しかし loopPwP' のループが進まず証明できない
-
 ```AGDA
 --    whileProofs c = whileTestPwP {_} {_} c 
 --       ( λ env s → conv1 env s 
@@ -276,11 +238,11 @@
     env  : Envc
     c    : ℕ
 ```
+- 先程の **whileProofs** で行った仕様記述を型に記述し、実際に証明していく
+- しかし loopPwP' のループが進まず証明できない
+
 
 ## 検証時の Loop の解決
-- **loopHelper** は今回のループを解決する証明
-- ループ解決のためにループの簡約ができた
-
 ```AGDA
     loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) → (seq : whileTestStateP s2 env) 
       → loopPwP' n env (sym eq) seq (λ env₁ x → (vari env₁ ≡ c10 env₁))
@@ -288,10 +250,10 @@
     loopHelper (suc n) env eq refl rewrite eq = loopHelper n 
       (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) refl (+-suc n (vari env))
 ```
+- **loopHelper** は今回のループを解決する証明
+- ループ解決のためにループの簡約ができた
 
 ## Gears と Hoare Logic を用いた仕様の証明(完成)
-- **loopHelper** を使って簡約することで **whileProofs** の証明を行うことができた
-
 ```AGDA
     --    whileProofs c = whileTestPwP {_} {_} c 
     --       ( λ env s → conv1 env s 
@@ -301,9 +263,7 @@
     ProofGears c = whileTestPwP {_} {_} c 
        (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero)
 ```
-
-<!-- ## Binary Tree について -->
-<!-- -  -->
+- **loopHelper** を使って簡約することで **whileProofs** の証明を行うことができた
 
 ## まとめと今後の課題
 - CodeGear、 DataGear を用いた Hoare Logic ベースの仕様記述を導入した
--- a/slide/slide.pdf.html	Mon Feb 10 17:26:24 2020 +0900
+++ b/slide/slide.pdf.html	Tue Feb 11 02:31:26 2020 +0900
@@ -119,25 +119,6 @@
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="gears-について">Gears について</h2>
-<ul>
-  <li><strong>Gears</strong> は当研究室で提案しているプログラム記述手法</li>
-  <li>処理の単位を <strong>CodeGear</strong> 、データの単位を <strong>DataGear</strong></li>
-  <li>CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す</li>
-  <li>Output の DataGear は次の CodeGear の Input として接続される
-<!-- [fig1](file://./fig/cgdg.pdf) --></li>
-  <li>CodeGear の接続処理などのメタ計算は Meta CodeGear として定義</li>
-  <li>Meta CodeGear で信頼性の検証を行う</li>
-</ul>
-<p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt="" width="60%" height="75%" /></p>
-<!-- <p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt=""  width="75%" height="75%"/></p> -->
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
 <h2 id="agda-のデータ型">Agda のデータ型</h2>
 <ul>
   <li><strong>データ型</strong>はプリミティブなデータ</li>
@@ -169,58 +150,22 @@
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="agda-のデータ型と-datagear">Agda のデータ型と DataGear</h2>
+<h2 id="agda-の関数">Agda の関数</h2>
 <ul>
-  <li><strong>DataGear</strong> は CodeGear でつかわれる引数をまとめたもの</li>
-  <li>Agda で使われる</li>
-</ul>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="agda-での-gears-の記述whiletest">Agda での Gears の記述(whileTest)</h2>
-<ul>
-  <li>Agda での CodeGear は継続渡し (CPS : Continuation Passing Style) で記述された関数</li>
-  <li><strong>{}</strong> は暗黙的(推論される)</li>
-  <li>継続渡しの関数は引数として継続を受け取って継続に計算結果を渡す</li>
-  <li>CodeGear の型は<strong>引数 → (Code : fa → t) → t</strong></li>
-  <li><strong>t</strong> は継続(最終的に返すもの)</li>
-  <li><strong>(Code : fa → t)</strong> は次の継続先
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  whileTest : {t : Set} → (c10 : Nat) 
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>                → (Code : Env → t) → t
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>  whileTest c10 next = next (record {varn = c10 
-<span class="line-numbers"><a href="#n4" name="n4">4</a></span>                                     ; vari = 0} )
+  <li>関数にも同様に型が必要
+    <div class="language-HASKELL highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  +1 : ℕ → ℕ
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>  +1 m = suc m
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span>  -- eval +1 zero
+<span class="line-numbers"><a href="#n5" name="n5">5</a></span>  -- return suc zero
 </pre></div>
 </div>
     </div>
   </li>
-</ul>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="agda-での-gears-の記述whileloop">Agda での Gears の記述(whileLoop)</h2>
-<ul>
-  <li>関数の動作を条件で変えたいときはパターンマッチを行う</li>
-  <li>whileLoop は varn が 0 より大きい間ループする
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  whileLoopPwP' : {t : Set} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>    → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env  → t)
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>    → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
-<span class="line-numbers"><a href="#n4" name="n4">4</a></span>  whileLoopPwP' zero env refl refl next exit = exit env refl
-<span class="line-numbers"><a href="#n5" name="n5">5</a></span>  whileLoopPwP' (suc n) env refl refl next exit =
-<span class="line-numbers"><a href="#n6" name="n6">6</a></span>    next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env))
-</pre></div>
-</div>
-    </div>
-  </li>
+  <li>関数の型は <strong>input → output</strong></li>
+  <li>複数入力がある場合は <strong>input1 → input2 → output</strong></li>
+  <li><strong>=</strong> の左側は関数名と引数、右側に実装</li>
 </ul>
 
 
@@ -232,112 +177,133 @@
 <h2 id="agda-での証明">Agda での証明</h2>
 <ul>
   <li>関数との違いは<strong>型が証明すべき論理式</strong>で<strong>関数自体がそれを満たす導出</strong>
-    <ul>
-      <li><strong>refl</strong> は <strong>x ≡ x</strong></li>
-      <li><strong>cong</strong> は 関数と x ≡ y 受け取って、x ≡ y の両辺に関数を適応しても等しいことが変わらないこと</li>
-    </ul>
+    <div class="language-HASKELL highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  +zero : { y : Nat } → y + zero ≡ y
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>  +zero {zero} = refl
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>  +zero {suc y} = cong suc ( +zero {y} )
+</pre></div>
+</div>
+    </div>
   </li>
+  <li><strong>refl</strong> は <strong>x ≡ x</strong></li>
+  <li><strong>cong</strong> は <strong>関数</strong> と等式を受け取って、等式の両辺に関数を適応しても等しくなること</li>
   <li><strong>+zero</strong> は任意の自然数の右から zero を足しても元の数と等しいことの証明
     <ul>
       <li><strong>y = zero</strong> のときは <strong>zero ≡ zero</strong> のため refl</li>
-      <li><strong>y = suc y</strong> のときは cong を使い y の数を減らして再帰的に<strong>+zero</strong>を行っている</li>
-      <li>y の数を減らしても大丈夫なことを cong の関数として受け取った数を suc する関数で保証している
-        <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>+zero : { y : Nat } → y + zero ≡ y
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>+zero {zero} = refl
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>+zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
-</pre></div>
-</div>
-        </div>
-      </li>
+      <li><strong>y = suc y</strong> のときは cong を使い y の数を減らして帰納的に証明している</li>
     </ul>
   </li>
 </ul>
 
-<!-- ## Agda での証明(項変換) -->
-<!-- <\!-- -- もしかしたら rewrite で代用しちゃうかも -\-> -->
-<!-- - **x + y ≡ y + x** の証明 **+-sym** -->
-<!-- - 項変換の例として引数が zero, suc y のパターンをみる -->
-<!-- - **zero + suc y**を変換して**suc y + zero**にする -->
-<!-- - begin の下の行に変形したい式を記述 -->
-<!-- - **≡⟨  ⟩** に変形規則、その次の行に変換した結果、 **∎** が項変換終了 -->
-<!-- ```AGDA -->
-<!-- +-sym : { x y : Nat } → x + y ≡ y + x -->
-<!-- +-sym {zero} {suc y} = let open ≡-Reasoning  in -->
-<!--           begin -->
-<!--             zero + suc y  -->
-<!--           ≡⟨⟩ -->
-<!--             suc y -->
-<!--           ≡⟨ sym +zero  ⟩ -->
-<!--             suc y + zero -->
-<!--           ∎ -->
-<!-- -- sym : Symmetric {A = A} _≡_ -->
-<!-- -- sym refl = refl -->
-<!-- -- +zero : { y : Nat } → y + zero ≡ y -->
-<!-- ``` -->
-
-<!-- ## Agda での証明(項変換) -->
-<!-- - **x + y ≡ y + x** の証明 **+-sym** -->
-<!-- - 項の変換には **rewrite** と  **** -->
-<!-- - begin の下の行に変形したい式を記述 -->
-<!-- - **≡⟨  ⟩** に変形規則、その次の行に変換した結果、 **∎** が項変換終了 -->
-<!-- ```AGDA -->
-<!-- +-comm : (x y : ℕ) → x + y ≡ y + x -->
-<!-- +-comm zero y rewrite (+zero {y}) = refl -->
-<!-- +-comm (suc x) y = let open ≡-Reasoning in -->
-<!--   begin -->
-<!--   suc (x + y) ≡⟨⟩ -->
-<!--   suc (x + y) ≡⟨ cong suc (+-comm x y) ⟩ -->
-<!--   suc (y + x) ≡⟨ sym (+-suc {y} {x}) ⟩ -->
-<!--   y + suc x ∎ -->
-
-<!-- -- +-suc : {x y : ℕ} → x + suc y ≡ suc (x + y) -->
-<!-- -- +-suc {zero} {y} = refl -->
-<!-- -- +-suc {suc x} {y} = cong suc (+-suc {x} {y}) -->
-<!-- ``` -->
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="hoare-logic-をベースとした-gears-での検証手法">Hoare Logic をベースとした Gears での検証手法</h2>
-<ul>
-  <li>今回 Hoare Logic で証明する次のようなコードを検証した</li>
-  <li>このプログラムは変数iとnをもち、 n&gt;0 の間nの値を減らし、i の値を増やす</li>
-  <li>n==0 のとき停止するため、終了時の変数の結果は i==10、n==0 になる
-    <div class="language-C highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> n = <span style="color:#00D">10</span>;
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span> i = <span style="color:#00D">0</span>;
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>
-<span class="line-numbers"><a href="#n4" name="n4">4</a></span> <span style="color:#080;font-weight:bold">while</span> (n&gt;<span style="color:#00D">0</span>)
-<span class="line-numbers"><a href="#n5" name="n5">5</a></span> {
-<span class="line-numbers"><a href="#n6" name="n6">6</a></span>   i++;
-<span class="line-numbers"><a href="#n7" name="n7">7</a></span>   n--;
-<span class="line-numbers"><a href="#n8" name="n8">8</a></span> }
-</pre></div>
-</div>
-    </div>
-  </li>
-</ul>
-
 
 
 </div>
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="gears-をベースにしたプログラム">Gears をベースにしたプログラム</h2>
+<h2 id="gears-について">Gears について</h2>
+<ul>
+  <li><strong>Gears</strong> は当研究室で提案しているプログラム記述手法</li>
+  <li>処理の単位を <strong>CodeGear</strong> 、データの単位を <strong>DataGear</strong></li>
+  <li>CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す</li>
+  <li>Output の DataGear は次の CodeGear の Input として接続される
+<!-- [fig1](file://./fig/cgdg.pdf) --></li>
+  <li>CodeGear の接続処理などのメタ計算は Meta CodeGear として定義</li>
+  <li>Meta CodeGear で信頼性の検証を行う</li>
+</ul>
+<p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt="" width="60%" height="75%" /></p>
+<!-- <p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt=""  width="75%" height="75%"/></p> -->
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="agda-での-datagear">Agda での DataGear</h2>
 <ul>
-  <li>test は whileTest と whileLoop を使った Gears のプログラム</li>
-  <li>whileTest の継続先にDataGear を受け取って whileLoop に渡す
-    <ul>
-      <li><strong>(λ 引数 → )</strong>は無名の関数で引数を受け取って継続する</li>
-    </ul>
+  <li><strong>DataGear</strong> は CodeGear でつかわれる引数をまとめたもの</li>
+  <li>Agda は CodeGear、 DataGear は検証メタ計算そのものと考えられる</li>
+  <li>DataGear は Agda の CodeGear で使われる<strong>全てのデータ</strong>に当たる</li>
+</ul>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="agda-での-codegear">Agda での CodeGear</h2>
+<ul>
+  <li>Agda での CodeGear は継続渡しで記述された関数
+    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  whileTest : {t : Set} → (c10 : Nat) 
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>                → (Code : Env → t) → t
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>  whileTest c10 next = next (record {varn = c10 
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span>                                     ; vari = 0} )
+</pre></div>
+</div>
+    </div>
   </li>
+  <li>CodeGear の型は<strong>引数 → (Code : fa → t) → t</strong></li>
+  <li><strong>(Code : fa → t)</strong> は継続先</li>
+  <li>引数として継続先を受け取って計算結果を渡す</li>
 </ul>
 
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="agda-での-gears-の記述whileloop">Agda での Gears の記述(whileLoop)</h2>
+<ul>
+  <li>関数の動作を条件で変えたいときはパターンマッチを行う
+    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  whileLoop : {l : Level} {t : Set l} → Envc 
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>     → (next : Envc → t) → (exit : Envc → t) → t
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>  whileLoop env@(record { c10 = _ ; varn = zero ; vari = _ }) _ exit = exit env
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span>  whileLoop record { c10 = _ ; varn = suc varn1 ; vari = vari } next _ = 
+<span class="line-numbers"><a href="#n5" name="n5">5</a></span>       next (record {c10 = _ ; varn = varn1 ; vari = suc vari })
+</pre></div>
+</div>
+    </div>
+  </li>
+  <li>whileLoop は varn が 0 より大きい間ループする</li>
+</ul>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="hoare-logic-をベースとした-gears-での検証手法">Hoare Logic をベースとした Gears での検証手法</h2>
+<div class="language-C highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>   n = <span style="color:#00D">10</span>;
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>   i = <span style="color:#00D">0</span>;
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span>   <span style="color:#080;font-weight:bold">while</span> (n&gt;<span style="color:#00D">0</span>)
+<span class="line-numbers"><a href="#n5" name="n5">5</a></span>   {
+<span class="line-numbers"><a href="#n6" name="n6">6</a></span>     i++;
+<span class="line-numbers"><a href="#n7" name="n7">7</a></span>     n--;
+<span class="line-numbers"><a href="#n8" name="n8">8</a></span>   }
+</pre></div>
+</div>
+</div>
+<ul>
+  <li>今回 Hoare Logic で証明する次のようなコードを検証した</li>
+  <li>このプログラムは変数iとnをもち、 n&gt;0 の間nの値を減らし、i の値を増やす</li>
+  <li>n ≡ 0 のとき停止するため、終了時の変数の結果は i ≡ 10、n ≡ 0 になる</li>
+</ul>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="gears-をベースにしたプログラム">Gears をベースにしたプログラム</h2>
 <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
   <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>    test : Env
 <span class="line-numbers"><a href="#n2" name="n2">2</a></span>    test = whileTest 10 (λ env → whileLoop env (λ env1 → env1))
@@ -347,6 +313,14 @@
 </pre></div>
 </div>
 </div>
+<ul>
+  <li>test は whileTest と whileLoop を実行した結果を返す関数</li>
+  <li>whileTest の継続先にDataGear を受け取って whileLoop に渡す
+    <ul>
+      <li><strong>(λ 引数 → )</strong>は無名の関数で引数を受け取って継続する</li>
+    </ul>
+  </li>
+</ul>
 
 
 
@@ -355,23 +329,22 @@
 <div class='slide'>
   <!-- _S9SLIDE_ -->
 <h2 id="gears-をベースにした-hoare-logic-と証明全体">Gears をベースにした Hoare Logic と証明(全体)</h2>
+<div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>    -- test = whileTest 10 (λ env → whileLoop env (λ env1 → env1))
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>    proofGears : {c10 :  Nat } → Set
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>    proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span>             conversion1 n p1  (λ n1 p2 → whileLoop' n1 p2 
+<span class="line-numbers"><a href="#n5" name="n5">5</a></span>             (λ n2 →  ( vari n2 ≡ c10 )))) 
+</pre></div>
+</div>
+</div>
 <ul>
   <li>proofGears は Hoare Logic をベースとした証明
     <ul>
       <li>先程のプログラムと違い、引数として証明も持っている</li>
     </ul>
   </li>
-  <li>whileTest’ の継続に conversion1、その継続に whileLoop’ が来て最後の継続に vari が c10 と等しい
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  -- test = whileTest 10 (λ env → whileLoop env (λ env1 → env1))
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>  proofGears : {c10 :  Nat } → Set
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>  proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →
-<span class="line-numbers"><a href="#n4" name="n4">4</a></span>           conversion1 n p1  (λ n1 p2 → whileLoop' n1 p2 
-<span class="line-numbers"><a href="#n5" name="n5">5</a></span>           (λ n2 →  ( vari n2 ≡ c10 )))) 
-</pre></div>
-</div>
-    </div>
-  </li>
+  <li>whileTest’ の継続に conversion1、その継続に whileLoop’ が来て最後の継続に vari が c10 と等しい</li>
 </ul>
 
 
@@ -381,29 +354,23 @@
 <div class='slide'>
   <!-- _S9SLIDE_ -->
 <h2 id="gears-と-hoare-logic-をベースにした証明whiletest">Gears と Hoare Logic をベースにした証明(whileTest)</h2>
+<div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>    whileTest' : {l : Level} {t : Set l} {c10 :  ℕ } 
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>      → (Code : (env : Env )  → ((vari env) ≡ 0) ∧ ((varn env) ≡ c10) → t) → t
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>    whileTest' {_} {_}  {c10} next = next 
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span>      (record env {vari = 0 ; varn = c10 }) (record {pi1 = refl ; pi2 = refl})
+</pre></div>
+</div>
+</div>
 <ul>
-  <li>最初の Command なので PreCondition がない</li>
-  <li>proof2は Post Condition が成り立つことの証明
+  <li>最初の Command なので PreCondition はない</li>
+  <li>(record {pi1 = refl ; pi2 = refl}) は <strong>(vari env) ≡ 0</strong> と <strong>(varn env) ≡ c10</strong>の証明
     <ul>
-      <li><strong><em>/\</em></strong> は pi1 と pi2 のフィールドをもつレコード型</li>
-      <li>これは2つのものを引数に取り、両方が同時に成り立つことを表している</li>
-      <li><strong>refl</strong> は <strong>x == x</strong> で左右の項が等しいことの証明</li>
+      <li><strong><em>∧</em></strong> は pi1 と pi2 のフィールドをもつレコード型</li>
+      <li>両方とも成り立つので <strong>refl</strong></li>
     </ul>
   </li>
-  <li>Gears での PostCondition は <strong>引数 → (Code : fa → PostCondition → t) → t</strong>
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  whileTest' : {l : Level} {t : Set l} {c10 :  ℕ } 
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>    → (Code : (env : Env )  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>  whileTest' {_} {_}  {c10} next = next env proof2
-<span class="line-numbers"><a href="#n4" name="n4">4</a></span>    where
-<span class="line-numbers"><a href="#n5" name="n5">5</a></span>      env : Env
-<span class="line-numbers"><a href="#n6" name="n6">6</a></span>      env = record {vari = 0 ; varn = c10 }
-<span class="line-numbers"><a href="#n7" name="n7">7</a></span>      proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition
-<span class="line-numbers"><a href="#n8" name="n8">8</a></span>      proof2 = record {pi1 = refl ; pi2 = refl}
-</pre></div>
-</div>
-    </div>
-  </li>
+  <li>Gears での PostCondition は <strong>引数 → (Code : fa → PostCondition → t) → t</strong></li>
 </ul>
 
 
@@ -413,45 +380,32 @@
 <div class='slide'>
   <!-- _S9SLIDE_ -->
 <h2 id="gears-と-hoare-logic-をベースにした証明conversion">Gears と Hoare Logic をベースにした証明(conversion)</h2>
-<ul>
-  <li>conversion は Condition から LoopInvaliant への変換を行う CodeGear
-    <ul>
-      <li>Condition の条件は Loop 内では厳しいのでゆるくする</li>
-    </ul>
-  </li>
-  <li>proof4 は LoopInvaliant の証明</li>
-</ul>
-
 <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>    conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>    conv : (env : Envc ) → (vari env ≡ 0) ∧ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
 <span class="line-numbers"><a href="#n2" name="n2">2</a></span>    conv e record { pi1 = refl ; pi2 = refl } = +zero
 </pre></div>
 </div>
 </div>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="hoare-logic-の証明">Hoare Logic の証明</h2>
 <ul>
-  <li>Hoare Logic の証明では基本的に項の書き換えを行って証明している</li>
-  <li>proof4 の証明部分では論理式の<strong>varn env + vari env</strong> を 書き換えて <strong>c10</strong> に変換している</li>
-  <li>変換で使っている <strong>cong</strong> は 関数と x ≡ y 受け取って両辺に関数を適応しても等しいことが変わらないことの証明</li>
-  <li>変換後の式を次の行に書いて変換を続ける
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  conv1 : {l : Level} {t : Set l } → (env : Envc )
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>    → ((vari env) ≡ 0) /\ ((varn env) ≡ (c10 env))
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>    → (Code : (env1 : Envc ) → (varn env1 + vari env1 ≡ (c10 env1)) → t) → t
-<span class="line-numbers"><a href="#n4" name="n4">4</a></span>  conv1 env record { pi1 = refl ; pi2 = refl } next = next env +zero
-</pre></div>
-</div>
-    </div>
+  <li>conv は制約を緩める CodeGear
+    <ul>
+      <li><strong>(vari env ≡ 0) ∧ (varn env ≡ c10 env)</strong> が成り立つとき <strong>varn env + vari env ≡ c10 env</strong> が成り立つ</li>
+    </ul>
   </li>
 </ul>
 
+<!-- ##  Hoare Logic の証明 -->
+<!-- - Hoare Logic の証明では基本的に項の書き換えを行って証明している -->
+<!-- - proof4 の証明部分では論理式の**varn env + vari env** を 書き換えて **c10** に変換している -->
+<!-- - 変換で使っている **cong** は 関数と x ≡ y 受け取って両辺に関数を適応しても等しいことが変わらないことの証明 -->
+<!-- - 変換後の式を次の行に書いて変換を続ける -->
+<!-- ```AGDA -->
+<!--     conv1 : {l : Level} {t : Set l } → (env : Envc ) -->
+<!--       → ((vari env) ≡ 0) /\ ((varn env) ≡ (c10 env)) -->
+<!--       → (Code : (env1 : Envc ) → (varn env1 + vari env1 ≡ (c10 env1)) → t) → t -->
+<!--     conv1 env record { pi1 = refl ; pi2 = refl } next = next env +zero -->
+<!-- ``` -->
+
 
 
 </div>
@@ -459,11 +413,6 @@
 <div class='slide'>
   <!-- _S9SLIDE_ -->
 <h2 id="gears-と-hoare-logic-をベースにした証明whileloop">Gears と Hoare Logic をベースにした証明(whileLoop)</h2>
-<ul>
-  <li>whileLoop も whileTest と同様に PreCondition が CodeGear に入りそれに対する証明が記述されている</li>
-  <li>ループステップごとに <strong>whileLoopPwP’</strong> で停止か継続かを判断し、 <strong>loopPwP’</strong> でループが回る</li>
-</ul>
-
 <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
   <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span>    whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env
 <span class="line-numbers"> <a href="#n2" name="n2">2</a></span>      → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env  → t)
@@ -478,6 +427,10 @@
 </pre></div>
 </div>
 </div>
+<ul>
+  <li>whileLoop も whileTest と同様に PreCondition が CodeGear に入りそれに対する証明が記述されている</li>
+  <li>ループが回るごとに、<strong>whileLoopPwP’</strong> で停止か継続かを判断し、 <strong>loopPwP’</strong> でループが回る</li>
+</ul>
 
 
 
@@ -486,10 +439,6 @@
 <div class='slide'>
   <!-- _S9SLIDE_ -->
 <h2 id="gears-と-hoare-logic-をベースにした仕様記述">Gears と Hoare Logic をベースにした仕様記述</h2>
-<ul>
-  <li><strong>proofGears</strong> では最終状態が i と c10 が等しくなるため仕様になっている</li>
-</ul>
-
 <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
   <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>    whileProofs : (c :  ℕ ) → Set
 <span class="line-numbers"><a href="#n2" name="n2">2</a></span>    whileProofs c = whileTestPwP {_} {_} c 
@@ -499,6 +448,9 @@
 </pre></div>
 </div>
 </div>
+<ul>
+  <li><strong>whileProofs</strong> では最終状態が vari と c10 が等しくなるため仕様になっている</li>
+</ul>
 
 
 
@@ -507,11 +459,6 @@
 <div class='slide'>
   <!-- _S9SLIDE_ -->
 <h2 id="gears-と-hoare-logic-を用いた仕様の証明">Gears と Hoare Logic を用いた仕様の証明</h2>
-<ul>
-  <li>先程の <strong>whileProofs</strong> で行った仕様記述を型に記述し、実際に証明していく</li>
-  <li>このままだと loopPwP’ のループが進まず証明できない</li>
-</ul>
-
 <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
   <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span>--    whileProofs c = whileTestPwP {_} {_} c 
 <span class="line-numbers"> <a href="#n2" name="n2">2</a></span>--       ( λ env s → conv1 env s 
@@ -534,6 +481,10 @@
 </pre></div>
 </div>
 </div>
+<ul>
+  <li>先程の <strong>whileProofs</strong> で行った仕様記述を型に記述し、実際に証明していく</li>
+  <li>しかし loopPwP’ のループが進まず証明できない</li>
+</ul>
 
 
 
@@ -542,11 +493,6 @@
 <div class='slide'>
   <!-- _S9SLIDE_ -->
 <h2 id="検証時の-loop-の解決">検証時の Loop の解決</h2>
-<ul>
-  <li><strong>loopHelper</strong> は今回のループを解決する証明</li>
-  <li>ループ解決のためにループの簡約ができた</li>
-</ul>
-
 <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
   <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>    loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) → (seq : whileTestStateP s2 env) 
 <span class="line-numbers"><a href="#n2" name="n2">2</a></span>      → loopPwP' n env (sym eq) seq (λ env₁ x → (vari env₁ ≡ c10 env₁))
@@ -556,6 +502,10 @@
 </pre></div>
 </div>
 </div>
+<ul>
+  <li><strong>loopHelper</strong> は今回のループを解決する証明</li>
+  <li>ループ解決のためにループの簡約ができた</li>
+</ul>
 
 
 
@@ -564,10 +514,6 @@
 <div class='slide'>
   <!-- _S9SLIDE_ -->
 <h2 id="gears-と-hoare-logic-を用いた仕様の証明完成">Gears と Hoare Logic を用いた仕様の証明(完成)</h2>
-<ul>
-  <li><strong>loopHelper</strong> を使って簡約することで <strong>whileProofs</strong> の証明を行うことができた</li>
-</ul>
-
 <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
   <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>    --    whileProofs c = whileTestPwP {_} {_} c 
 <span class="line-numbers"><a href="#n2" name="n2">2</a></span>    --       ( λ env s → conv1 env s 
@@ -579,9 +525,9 @@
 </pre></div>
 </div>
 </div>
-
-<!-- ## Binary Tree について -->
-<!-- -  -->
+<ul>
+  <li><strong>loopHelper</strong> を使って簡約することで <strong>whileProofs</strong> の証明を行うことができた</li>
+</ul>