--- a/paper/hoare.tex	Wed Feb 12 05:02:27 2020 +0900
+++ b/paper/hoare.tex	Fri Feb 14 16:19:47 2020 +0900
@@ -10,8 +10,10 @@
 といった形で表される。
 
 Hoare Logic ではプログラムの部分的な正当性を検証することができ、
-事後条件のあとに別の コマンド をつなげてプログラムを構築することで、
-シンプルな計算に対する検証することができる。
+事後条件のあとに別のコマンドをつなげてプログラムを構築することで、
+プログラムに対する検証を行える。
+
+
 
 本章は Agda で実装された Hoare Logic について解説し、
 実際に Hoare Logic を用いた検証を行う。
@@ -31,7 +33,7 @@
 while loop が終了したとき成り立っている条件を $i = 10$
 としている。
 
-同様のプログラムを Hoare Logic 上で同様のプログラムを作成し、検証を行う。
+Hoare Logic 上で同様のプログラムを作成し、検証を行う。
 
 \begin{lstlisting}[caption=while Loop Program,label=c-while]
 n = 10;

--- a/slide/slide.md	Wed Feb 12 05:02:27 2020 +0900
+++ b/slide/slide.md	Fri Feb 14 16:19:47 2020 +0900
@@ -624,32 +624,3 @@
   - 並列実行での検証
 
 
-```AGDA
-loopPPSem : (input output : Envc ) →  output ≡ loopPP (varn input)  input refl
-  → (varn input + vari input ≡ c10 input ) → (varn input + vari input ≡ c10 input ) implies (vari output ≡ c10 output)
-loopPPSem input output refl s2p = loopPPSemInduct (varn input) input  refl refl s2p
-  where
-    lem : (n : ℕ) → (env : Envc) → n + suc (vari env) ≡ suc (n + vari env)
-    lem n env = +-suc (n) (vari env)
-    loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) 
-        →  (loopeq : output ≡ loopPP n current eq)
-      → (whileTestStateP s2 current ) 
-      → (whileTestStateP s2 current ) implies (vari output ≡ c10 output)
-    loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl)
-    loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) =
-        whileLoopPSem current refl
-            (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
-            (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
-```
-
-```AGDA
-whileLoopPSem : {l : Level} {t : Set l} → (input : Envc ) → varn input + vari input ≡ c10 input 
-    → (next : (output : Envc ) 
-        → (varn input + vari input ≡ c10 input) implies (varn output + vari output ≡ c10 output )  → t)
-    → (exit : (output : Envc ) 
-        → (varn input + vari input ≡ c10 input ) implies (vari env) ≡ (c10 env) → t) → t
-whileLoopPSem env s next exit with varn env | s
-... | zero | _ = exit env (proof (λ z → z))
-... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } )   
-    (proof λ x → +-suc varn (vari env) )
-```