# HG changeset patch
# User soto <soto@cr.ie.u-ryukyu.ac.jp>
# Date 1675748955 -32400
# Node ID 988528add93fc9a78b4eb8641518f37025d454bd
# Parent  016e82a7140792ab16c10d7f8ffd5732ee6b805a
fix slide

diff -r 016e82a71407 -r 988528add93f DPP/sample.agda
--- a/DPP/sample.agda	Tue Feb 07 02:27:53 2023 +0900
+++ b/DPP/sample.agda	Tue Feb 07 14:49:15 2023 +0900
@@ -19,6 +19,14 @@
 ... | 0 = exit env
 ... | suc s = next (record env{varn = suc (varn env) ; vari = s })
 
+record _∧1_ (A B : Set) : Set where
+ field
+   p1 : A
+   p2 : B
+open _∧1_
+
+s1 : {A B C : Set} → (A → B) ∧1 (B → C) → (A → C)
+s1 x = 
 
 init-env-c : {l : Level} {t : Set l} → ℕ → (next : Env → t) → t
 init-env-c x next = next record { c10 = x ; varn = 0 ; vari = x }
diff -r 016e82a71407 -r 988528add93f slide/slide.md
--- a/slide/slide.md	Tue Feb 07 02:27:53 2023 +0900
+++ b/slide/slide.md	Tue Feb 07 14:49:15 2023 +0900
@@ -454,7 +454,7 @@
 test-dead-lock-loop2 : MetaEnv2 → MetaEnv2
 test-dead-lock-loop2 metaenv2 = branch-search-meta2 metaenv2 
   (λ me2 → step-meta2 me2 
-  (λ me3 → testhoge me3 metaenv2 
+  (λ me3 → exclude-same-env me3 metaenv2 
   (λ me4 → test-dead-lock-loop2 me4) ) ) 
 (λ e → check-and-judge-deadlock e (λ e1 → e1) )
 ```
@@ -468,7 +468,7 @@
 - モデル検査
     - 有向グラフからなる有限オートマトンの遷移を全自動探索する
     - live lock の検出や LTTL も用いたアサーションなどの検証
-    - State List のデータ構造を blanced tree にする
+    - State List のデータ構造を balanced tree にする
     - モデル検査に定理証明を組み込む
 - 定理証明
     - Red Black Tree の検証を行う
diff -r 016e82a71407 -r 988528add93f slide/slide.pdf
Binary file slide/slide.pdf has changed