--- a/a04/lecture.ind	Wed Nov 16 17:43:10 2022 +0900
+++ b/a04/lecture.ind	Wed Dec 07 14:51:25 2022 +0900
@@ -10,6 +10,8 @@
 にわけて x を A が受理し、y を B で受理するものを、単一ののオートマトンで実現できると言う意味である。
 しかい、 これを決定性オートマトンで示すのは難しい。A ++ B の 境目がどこかを前もって予測することができないからである。
 
+二つのオートマトンが、a0..ae b0..be につながる様子を図にしてみる。
+
 <center><img src="fig/concat.svg"></center>
 
 このためには後半のB automatonを、前半のA automatonが終わる可能性がある時だけ、
@@ -19,12 +21,64 @@
 
 状態はAの状態とBの状態の部分集合の組になる。
 
+--(a.*f)(b.*f) を考えよう
+
+abcfbffbcdf は、この正規表現にマッチする。a.*fb.*f と書いても良い。
+
+a.*f は以下の状態遷移で書ける。
+
+State は a0,a1,ae,af で、ae ならば受理。
+
+     δa a0 a = a1
+     δa a1 f = ae
+     δa a1 _ = a1
+     δa a0 _ = af
+
+b.*f もどうように書ける。
+
+     δb b0 b = b1
+     δb b1 f = be
+     δb b1 _ = b1
+     δb b0 _ = bf
+
+これを使って、a.*fb.*f を受理してみる。
+
+<center><img src="fig/af-concat.svg"></center>
+
+受理パターンは二通りある。これを非決定性があるという。
+
+この状況は、f がきた時に a.*f を終了しても良く、終了しなくてよいことから来てる。
+
+なので、それを許すオートマトンを考える。
+
 --非決定性オートマトン
 
-そこで、状態の部分集合からなるオートマトンを考える。
+オートマトンの状態遷移は関数だった。
+
+   δ : Q → Σ → Q 
+
+その代わりに、複数の状態を許したい。Aの場合なら、f でaeにもa1にもいって良い。
+それには、a1の状態で f がきた時に ae と a1 で true を返すようにすると良い。
+行き先の状態を  Q → Bool で、部分集合として指定する。
 
-これは状態遷移が非決定的な場合に相当する。この場合では 1 が来た時に q1 に
-行っても、q2,q3 に行っても良い。q1から始める。
+    record NAutomaton ( Q : Set ) ( Σ : Set  )
+           : Set  where
+        field
+              Nδ : Q → Σ → Q → Bool
+              Nend  :  Q → Bool
+
+これを非決定性オートマトンという。
+
+入力にそって、可能な状態の集合を作ってやれば良い。そうすると
+決定性オートマトンにできる。
+
+<center><img src="fig/afbf.svg"></center>
+
+
+--もう一つの例
+
+
+この場合では 1 が来た時に q1 に行っても、q2,q3 に行っても良い。q1から始める。
 
     q1  0 → q1
     q1  1 → q1
@@ -57,7 +111,20 @@
 
 これを非決定性オートマトンという。Agda では同じ名前を使いまわしすることはできない(monomorpphism)ので、Nを付けた。
 
-<a href="../agda/nfa.agda"> nfa.agda </a>
+たとえば、以下のように非決定的な状態遷移を定義する
+
+    transition3 : States1  → In2  → States1 → Bool
+    transition3 sr i0 sr = true
+    transition3 sr i1 ss = true
+    transition3 sr i1 sr = true
+    transition3 ss i0 sr = true
+    transition3 ss i1 st = true
+    transition3 st i0 sr = true
+    transition3 st i1 st = true
+    transition3 _ _ _ = false
+
+
+<a href="../agda/src/nfa.agda"> nfa.agda </a>
 
 --NAutomatonの受理と遷移