Mercurial > hg > Members > kono > Proof > automaton

changeset 331:9324852d3a17

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 07 Dec 2022 14:51:25 +0900
parents 407684f806e4
children 6f3636fbc481
files a04/fig/concat.graffle a04/fig/concat.svg a04/lecture.ind a05/lecture.ind automaton-in-agda/src/regex1.agda
diffstat 5 files changed, 237 insertions(+), 130 deletions(-) [+]
line wrap: on
line diff
Binary file a04/fig/concat.graffle has changed
--- a/a04/fig/concat.svg	Wed Nov 16 17:43:10 2022 +0900
+++ b/a04/fig/concat.svg	Wed Dec 07 14:51:25 2022 +0900
@@ -1,122 +1,90 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
-<svg version="1.1" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" viewBox="96 65 681 696" width="681" height="696">
-  <defs>
-    <font-face font-family="Helvetica Neue" font-size="16" panose-1="2 0 5 3 0 0 0 2 0 4" units-per-em="1000" underline-position="-100" underline-thickness="50" slope="0" x-height="517" cap-height="714" ascent="951.9958" descent="-212.99744" font-weight="400">
-      <font-face-src>
-        <font-face-name name="HelveticaNeue"/>
-      </font-face-src>
-    </font-face>
-    <font-face font-family="Helvetica Neue" font-size="32" panose-1="2 0 5 3 0 0 0 2 0 4" units-per-em="1000" underline-position="-100" underline-thickness="50" slope="0" x-height="517" cap-height="714" ascent="951.9958" descent="-212.99744" font-weight="400">
-      <font-face-src>
-        <font-face-name name="HelveticaNeue"/>
-      </font-face-src>
-    </font-face>
-    <font-face font-family="Helvetica Neue" font-size="26" panose-1="2 0 5 3 0 0 0 2 0 4" units-per-em="1000" underline-position="-100" underline-thickness="50" slope="0" x-height="517" cap-height="714" ascent="951.9958" descent="-212.99744" font-weight="400">
-      <font-face-src>
-        <font-face-name name="HelveticaNeue"/>
-      </font-face-src>
-    </font-face>
-  </defs>
-  <metadata> Produced by OmniGraffle 7.18\n2020-12-09 05:54:46 +0000</metadata>
-  <g id="Canvas_1" stroke="none" fill-opacity="1" fill="none" stroke-dasharray="none" stroke-opacity="1">
+<svg xmlns="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" xmlns:dc="http://purl.org/dc/elements/1.1/" version="1.1" viewBox="95 115 682 604" width="682" height="604">
+  <defs/>
+  <g id="Canvas_1" stroke-dasharray="none" stroke-opacity="1" stroke="none" fill="none" fill-opacity="1">
     <title>Canvas 1</title>
-    <rect fill="white" x="96" y="65" width="681" height="696"/>
+    <rect fill="white" x="95" y="115" width="682" height="604"/>
     <g id="Canvas_1_Layer_1">
       <title>Layer 1</title>
       <g id="Graphic_3">
-        <rect x="103" y="110" width="44" height="40" fill="white"/>
-        <rect x="103" y="110" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
-        <text transform="translate(108 120.776)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="16" font-weight="400" fill="black" x="12.704" y="15">a</tspan>
+        <rect x="97" y="200.8562" width="44" height="40" fill="white"/>
+        <rect x="97" y="200.8562" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+        <text transform="translate(102 211.6322)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="12.704" y="15">a</tspan>
         </text>
       </g>
       <g id="Graphic_4">
-        <rect x="163" y="110" width="44" height="40" fill="white"/>
-        <rect x="163" y="110" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
-        <text transform="translate(168 120.776)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="16" font-weight="400" fill="black" x="12.256" y="15">b</tspan>
+        <rect x="157" y="200.8562" width="44" height="40" fill="white"/>
+        <rect x="157" y="200.8562" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+        <text transform="translate(162 211.6322)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="12.256" y="15">b</tspan>
         </text>
       </g>
       <g id="Graphic_5">
-        <rect x="223" y="110" width="44" height="40" fill="white"/>
-        <rect x="223" y="110" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
-        <text transform="translate(228 120.776)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="16" font-weight="400" fill="black" x="12.704" y="15">c</tspan>
+        <rect x="217" y="200.8562" width="44" height="40" fill="white"/>
+        <rect x="217" y="200.8562" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+        <text transform="translate(222 211.6322)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="12.704" y="15">c</tspan>
         </text>
       </g>
       <g id="Graphic_6">
-        <rect x="283" y="110" width="44" height="40" fill="white"/>
-        <rect x="283" y="110" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
-        <text transform="translate(288 120.776)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="16" font-weight="400" fill="black" x="14.632" y="15">f</tspan>
+        <rect x="277" y="200.8562" width="44" height="40" fill="white"/>
+        <rect x="277" y="200.8562" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+        <text transform="translate(282 211.6322)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="14.632" y="15">f</tspan>
         </text>
       </g>
       <g id="Graphic_7">
-        <rect x="343" y="110" width="44" height="40" fill="white"/>
-        <rect x="343" y="110" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
-        <text transform="translate(348 120.776)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="16" font-weight="400" fill="black" x="12.256" y="15">b</tspan>
+        <rect x="337" y="200.8562" width="44" height="40" fill="white"/>
+        <rect x="337" y="200.8562" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+        <text transform="translate(342 211.6322)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="12.256" y="15">b</tspan>
         </text>
       </g>
       <g id="Graphic_8">
-        <rect x="403" y="110" width="44" height="40" fill="white"/>
-        <rect x="403" y="110" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
-        <text transform="translate(408 120.776)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="16" font-weight="400" fill="black" x="14.632" y="15">f</tspan>
+        <rect x="397" y="200.8562" width="44" height="40" fill="white"/>
+        <rect x="397" y="200.8562" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+        <text transform="translate(402 211.6322)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="14.632" y="15">f</tspan>
         </text>
       </g>
       <g id="Graphic_9">
-        <rect x="463" y="110" width="44" height="40" fill="white"/>
-        <rect x="463" y="110" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
-        <text transform="translate(468 120.776)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="16" font-weight="400" fill="black" x="14.632" y="15">f</tspan>
+        <rect x="457" y="200.8562" width="44" height="40" fill="white"/>
+        <rect x="457" y="200.8562" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+        <text transform="translate(462 211.6322)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="14.632" y="15">f</tspan>
         </text>
       </g>
       <g id="Graphic_10">
-        <rect x="523" y="110" width="44" height="40" fill="white"/>
-        <rect x="523" y="110" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
-        <text transform="translate(528 120.776)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="16" font-weight="400" fill="black" x="12.256" y="15">b</tspan>
+        <rect x="517" y="200.8562" width="44" height="40" fill="white"/>
+        <rect x="517" y="200.8562" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+        <text transform="translate(522 211.6322)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="12.256" y="15">b</tspan>
         </text>
       </g>
       <g id="Graphic_11">
-        <rect x="583" y="110" width="44" height="40" fill="white"/>
-        <rect x="583" y="110" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
-        <text transform="translate(588 120.776)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="16" font-weight="400" fill="black" x="12.704" y="15">c</tspan>
+        <rect x="577" y="200.8562" width="44" height="40" fill="white"/>
+        <rect x="577" y="200.8562" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+        <text transform="translate(582 211.6322)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="12.704" y="15">c</tspan>
         </text>
       </g>
       <g id="Graphic_12">
-        <rect x="643" y="110" width="44" height="40" fill="white"/>
-        <rect x="643" y="110" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
-        <text transform="translate(648 120.776)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="16" font-weight="400" fill="black" x="12.256" y="15">d</tspan>
+        <rect x="637" y="200.8562" width="44" height="40" fill="white"/>
+        <rect x="637" y="200.8562" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+        <text transform="translate(642 211.6322)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="12.256" y="15">d</tspan>
         </text>
       </g>
       <g id="Graphic_13">
-        <rect x="703" y="110" width="44" height="40" fill="white"/>
-        <rect x="703" y="110" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
-        <text transform="translate(708 120.776)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="16" font-weight="400" fill="black" x="14.632" y="15">f</tspan>
-        </text>
-      </g>
-      <g id="Graphic_14">
-        <text transform="translate(197 211.5122)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="4.804" y="30">(a.*f)</tspan>
+        <rect x="697" y="200.8562" width="44" height="40" fill="white"/>
+        <rect x="697" y="200.8562" width="44" height="40" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+        <text transform="translate(702 211.6322)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="14.632" y="15">f</tspan>
         </text>
       </g>
-      <g id="Graphic_15">
-        <text transform="translate(579 211.5122)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="3.908" y="30">(b.*f)</tspan>
-        </text>
-      </g>
-      <g id="Line_16">
-        <line x1="103" y1="180" x2="507" y2="180" stroke="#7f8080" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
-      </g>
-      <g id="Line_17">
-        <line x1="518" y1="180" x2="753" y2="180" stroke="#7f8080" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
-      </g>
+      <g id="Graphic_14"/>
       <g id="Line_18">
         <line x1="97" y1="495.1482" x2="321" y2="495.1482" stroke="#7f8080" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
       </g>
@@ -124,24 +92,23 @@
         <line x1="343" y1="495.1482" x2="747" y2="495.1482" stroke="#7f8080" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
       </g>
       <g id="Graphic_20">
-        <text transform="translate(104.816 297.9602)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="0" y="30">a0</tspan>
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x=".304" y="67.896">ae</tspan>
+        <text transform="translate(105.12 297.9602)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="32" fill="black" x="0" y="30">ae</tspan>
         </text>
       </g>
       <g id="Graphic_21">
         <text transform="translate(233.28 297.9602)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="14210855e-21" y="30">b1</tspan>
+          <tspan font-family="Helvetica Neue" font-size="32" fill="black" x="14210855e-21" y="30">b1</tspan>
         </text>
       </g>
       <g id="Graphic_22">
         <text transform="translate(350.384 283.5122)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="0" y="30">…</tspan>
+          <tspan font-family="Helvetica Neue" font-size="32" fill="black" x="0" y="30">…</tspan>
         </text>
       </g>
       <g id="Graphic_23">
-        <text transform="translate(721.816 297.9602)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="0" y="30">be</tspan>
+        <text transform="translate(711.34 297.9602)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="32" fill="black" x="0" y="30">be</tspan>
         </text>
       </g>
       <g id="Line_25">
@@ -151,24 +118,23 @@
         <line x1="163" y1="278.5122" x2="747" y2="278.5122" stroke="#7f8080" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
       </g>
       <g id="Graphic_31">
-        <text transform="translate(109.82 402.2102)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="0" y="30">a0   a1</tspan>
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="44.48" y="67.896">  ae</tspan>
+        <text transform="translate(114.572 402.2102)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="32" fill="black" x="0" y="30">a0  ae</tspan>
         </text>
       </g>
       <g id="Graphic_30">
         <text transform="translate(231.588 402.2102)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="14210855e-21" y="30">b0</tspan>
+          <tspan font-family="Helvetica Neue" font-size="32" fill="black" x="14210855e-21" y="30">b0</tspan>
         </text>
       </g>
       <g id="Graphic_29">
         <text transform="translate(350.384 384.4082)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="0" y="30">…</tspan>
+          <tspan font-family="Helvetica Neue" font-size="32" fill="black" x="0" y="30">…</tspan>
         </text>
       </g>
       <g id="Graphic_28">
-        <text transform="translate(729 402.2102)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="0" y="30">be</tspan>
+        <text transform="translate(711.34 403.5852)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="32" fill="black" x="0" y="30">be</tspan>
         </text>
       </g>
       <g id="Line_27">
@@ -179,22 +145,22 @@
       </g>
       <g id="Graphic_32">
         <text transform="translate(168 297.9602)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="14210855e-21" y="30">b0</tspan>
+          <tspan font-family="Helvetica Neue" font-size="32" fill="black" x="14210855e-21" y="30">b0</tspan>
         </text>
       </g>
       <g id="Graphic_37">
         <text transform="translate(666 610.4082)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="14210855e-21" y="30">b0</tspan>
+          <tspan font-family="Helvetica Neue" font-size="32" fill="black" x="14210855e-21" y="30">b0</tspan>
         </text>
       </g>
       <g id="Graphic_36">
         <text transform="translate(352.896 606.4602)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="0" y="30">…</tspan>
+          <tspan font-family="Helvetica Neue" font-size="32" fill="black" x="0" y="30">…</tspan>
         </text>
       </g>
       <g id="Graphic_35">
-        <text transform="translate(729 610.4082)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="0" y="30">be</tspan>
+        <text transform="translate(721.816 610.4082)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="32" fill="black" x="0" y="30">be</tspan>
         </text>
       </g>
       <g id="Line_34">
@@ -205,45 +171,96 @@
       </g>
       <g id="Graphic_39">
         <text transform="translate(610.2 610.4082)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="0" y="30">ae</tspan>
+          <tspan font-family="Helvetica Neue" font-size="32" fill="black" x="0" y="30">ae</tspan>
         </text>
       </g>
       <g id="Graphic_40">
         <text transform="translate(499.923 681.6162)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="26" font-weight="400" fill="black" x="0" y="25">success at one of them</tspan>
+          <tspan font-family="Helvetica Neue" font-size="26" fill="black" x="0" y="25">success at one of them</tspan>
         </text>
       </g>
-      <g id="Line_41">
-        <line x1="334.5" y1="132.51221" x2="334.5" y2="760.3286" stroke="#7f8080" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
-      </g>
       <g id="Graphic_42">
         <text transform="translate(108 610.4082)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="0" y="30">a0   a1</tspan>
+          <tspan font-family="Helvetica Neue" font-size="32" fill="black" x="0" y="30">a0   a1</tspan>
         </text>
       </g>
       <g id="Graphic_56">
-        <text transform="translate(108.584 510.4082)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="3836931e-19" y="30">a0   a1   a2   a3</tspan>
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="167.808" y="67.896">  ae</tspan>
+        <text transform="translate(108.888 510.4082)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="32" fill="black" x="29842795e-20" y="30">a0   a1   a2   ae</tspan>
         </text>
       </g>
       <g id="Graphic_55"/>
       <g id="Graphic_54">
         <text transform="translate(423 491.4082)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="0" y="30">…</tspan>
+          <tspan font-family="Helvetica Neue" font-size="32" fill="black" x="0" y="30">…</tspan>
         </text>
       </g>
       <g id="Graphic_53">
-        <text transform="translate(729 509.2102)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="0" y="30">be</tspan>
+        <text transform="translate(711.34 510.4082)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="32" fill="black" x="0" y="30">be</tspan>
         </text>
       </g>
-      <g id="Line_50">
-        <path d="M 335.692 66 L 335.92247 95.50391 L 335.692 693.8164" stroke="#7f8080" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
-      </g>
       <g id="Graphic_57">
         <text transform="translate(350.384 509.2102)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="32" font-weight="400" fill="black" x="14210855e-21" y="30">b0</tspan>
+          <tspan font-family="Helvetica Neue" font-size="32" fill="black" x="14210855e-21" y="30">b0</tspan>
+        </text>
+      </g>
+      <g id="Line_59">
+        <line x1="99.816" y1="261.5" x2="99.816" y2="288" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+      </g>
+      <g id="Line_60">
+        <line x1="147" y1="261.5" x2="147" y2="288" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+      </g>
+      <g id="Line_61">
+        <line x1="163" y1="261.5" x2="163" y2="288" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+      </g>
+      <g id="Line_62">
+        <line x1="747" y1="261.5" x2="747" y2="288" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+      </g>
+      <g id="Line_63">
+        <line x1="99.816" y1="363.33617" x2="99.816" y2="389.83617" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+      </g>
+      <g id="Line_64">
+        <line x1="96" y1="482.3982" x2="96" y2="508.8982" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+      </g>
+      <g id="Line_65">
+        <line x1="96" y1="584.5" x2="96" y2="611" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+      </g>
+      <g id="Line_66">
+        <line x1="217" y1="363.33617" x2="218" y2="389.67797" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+      </g>
+      <g id="Line_67">
+        <line x1="228.28" y1="363.33617" x2="228.28" y2="389.83617" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+      </g>
+      <g id="Line_68">
+        <line x1="747" y1="363.33617" x2="747" y2="389.83617" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+      </g>
+      <g id="Line_69">
+        <line x1="321" y1="478.9082" x2="321" y2="505.4082" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+      </g>
+      <g id="Line_70">
+        <line x1="345.384" y1="482.3982" x2="345.384" y2="508.8982" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+      </g>
+      <g id="Line_71">
+        <line x1="751.5" y1="477.7102" x2="751.5" y2="504.2102" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+      </g>
+      <g id="Line_72">
+        <line x1="762.976" y1="588.7102" x2="762.976" y2="615.2102" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+      </g>
+      <g id="Line_74">
+        <line x1="643.768" y1="584.5" x2="643.768" y2="611" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+      </g>
+      <g id="Line_75">
+        <line x1="666.916" y1="584.5" x2="666.916" y2="611" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
+      </g>
+      <g id="Graphic_76">
+        <text transform="translate(214.16 120.3042)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="32" fill="black" x="0" y="30">a0 a1 .. ae</tspan>
+        </text>
+      </g>
+      <g id="Graphic_77">
+        <text transform="translate(424.832 120.3042)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="32" fill="black" x="0" y="30">b0 b1 .. be</tspan>
         </text>
       </g>
     </g>
--- 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の受理と遷移
 
--- a/a05/lecture.ind	Wed Nov 16 17:43:10 2022 +0900
+++ b/a05/lecture.ind	Wed Dec 07 14:51:25 2022 +0900
@@ -89,12 +89,7 @@
 
 Regex Σはdataなので場合分けとなる。
 
-例えば、
 
-    _‖_ : {Σ : Set} ( x y : List Σ → Bool) → List Σ → Bool
-    x ‖ y = λ s → x s ∨ y s
-
-    regular-language (x || y) f = ( regular-language x f ) ‖ ( regular-language y f )
 
 -- < a >
 
@@ -128,9 +123,31 @@
       yes : ( p :   P) → Dec P
       no  : (¬p : ¬ P) → Dec P
 
+-- x || Y
+
+
+    regular-language (x || y) f = ( regular-language x f ) ∨ ( regular-language y f )
+
 
 -- x & y
 
+--begin-comment:
+
+教科書の定義の通りに定義するべき
+
+    regular-language (x & y) f =  ( regular-language x g )  ∧ ( regular-language y h )
+           ∧ ( g ++ h ≡ f )
+
+    record Concat {Σ : Set}  (x y : List Σ → Bool ) (f : List Σ) : Set where
+       field 
+          g h : List Σ
+          f=gh : g ++ h ≡ f  
+          match  : ( regular-language x g )  ∧ ( regular-language y h ) ≡ true
+
+--end-comment:
+
+
+
 これは 
 
     split : {Σ : Set} → (List Σ → Bool)
@@ -166,6 +183,13 @@
 <a href=""> </a>  <!---  Exercise 5.6 --->
 <a href=""> </a>  <!---  Exercise 5.7 --->
 
+--begin-comment:
+
+正規表現がどんな文字列にマッチするかという問題
+
+マッチして欲しいパターンに対する正規表現を作る問題
+
+--end-comment:
 
 
 
@@ -179,4 +203,3 @@
 
 
 
-
--- a/automaton-in-agda/src/regex1.agda	Wed Nov 16 17:43:10 2022 +0900
+++ b/automaton-in-agda/src/regex1.agda	Wed Dec 07 14:51:25 2022 +0900
@@ -50,10 +50,10 @@
 tt1 : {Σ : Set} → ( P Q :  List In → Bool ) → split P Q ( a ∷ b ∷ c ∷ [] ) ≡ ?
 tt1 P Q = ?
 
--- {-# TERMINATING #-}
--- repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
--- repeat x [] = true
--- repeat {Σ} x ( h  ∷ t ) = split x (repeat {Σ} x) ( h  ∷ t )
+{-# TERMINATING #-}
+repeat-t : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
+repeat-t x [] = true
+repeat-t {Σ} x ( h  ∷ t ) = split x (repeat-t {Σ} x) ( h  ∷ t )
 
 repeat : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool 
 repeat {Σ} x [] = true