--- a/automaton-in-agda/src/regex.agda	Wed Nov 22 17:07:01 2023 +0900
+++ b/automaton-in-agda/src/regex.agda	Wed Nov 29 17:40:55 2023 +0900
@@ -14,13 +14,17 @@
 open import logic
 open import regular-language
 
+--  (abc|d.*)
+--  any = < a > || < b > || < c > || < d >
+--  ( < a > & < b > & < c > ) || ( <d > & ( any * ) )
+
 data Regex ( Σ : Set) : Set  where
   ε     : Regex Σ                -- empty
-  φ     : Regex  Σ               -- fail
-  _*    : Regex  Σ  → Regex  Σ 
-  _&_   : Regex  Σ  → Regex  Σ → Regex Σ
-  _||_  : Regex  Σ  → Regex  Σ → Regex Σ
-  <_>   : Σ → Regex  Σ
+  φ     : Regex Σ               -- fail
+  _*    : Regex Σ → Regex Σ 
+  _&_   : Regex Σ → Regex Σ → Regex Σ
+  _||_  : Regex Σ → Regex Σ → Regex Σ
+  <_>   : Σ → Regex Σ
 
 infixr 40 _&_ _||_
 
@@ -30,9 +34,9 @@
 regex-language φ cmp _ = false
 regex-language ε cmp [] = true
 regex-language ε cmp (_ ∷ _) = false
-regex-language (x *) cmp = repeat ( regex-language x cmp  )
-regex-language (x & y) cmp  = split ( λ z → regex-language x  cmp z ) (λ z →  regex-language y  cmp z )
-regex-language (x || y) cmp  = λ s → ( regex-language x  cmp s )  \/  ( regex-language y  cmp s)
+regex-language (x *) cmp = repeat ( regex-language x cmp  ) [] 
+regex-language (x & y) cmp  = split ( λ z → regex-language x  cmp z ) (regex-language y  cmp  ) 
+regex-language (x || y) cmp = λ s → ( regex-language x  cmp s )  \/  ( regex-language y  cmp s)
 regex-language < h > cmp  [] = false
 regex-language < h > cmp  (h1  ∷ [] ) with cmp h h1
 ... | yes _ = true