--- a/automaton-in-agda/src/nfa136.agda	Thu Nov 16 17:40:42 2023 +0900
+++ b/automaton-in-agda/src/nfa136.agda	Wed Nov 22 17:07:01 2023 +0900
@@ -97,7 +97,9 @@
 
 aδ : Q2 → Σ2 → Q2 
 aδ a0 ca = a1 
-aδ a0 _ = af 
+aδ a0 cb = af
+aδ a0 cc = af
+aδ a0 cf = af
 aδ a1 cf = ae 
 aδ a1 _ = a1 
 aδ ae cf = ae 
@@ -109,13 +111,15 @@
 test111 : Bool
 test111 = accept fa-a a0 ( ca ∷ cf ∷ ca ∷ [] )
 
+-- b.*f
+
 b-end : Q2 → Bool
 b-end be = true
 b-end _ = false
 
 bδ : Q2 → Σ2 → Q2 
-bδ b0 cb = b1 
-bδ b0 _ = bf 
+bδ ae cb = b1 
+bδ ae _ = bf 
 bδ b1 cf = be 
 bδ b1 _ = b1 
 bδ be cf = be 
@@ -129,13 +133,20 @@
 
 open import regular-language
 
+-- (a.*f)(b.*f)    -- a.*(fb).*f
 test116 = split (accept fa-a a0) (accept fa-b b0) ( ca ∷ cf ∷ cb ∷ cf ∷ cf ∷ [] )
+--                                                  a0   ae   b0   b1   be 
+test117 = split (accept fa-a a0) (accept fa-b b0) ( ca ∷ cf ∷ ca ∷ cb ∷ ca ∷ cf ∷ cf ∷ [] )
+--                                                  a0   ae   a0   b0   b1   be
+--                                                  a0   ae   ae   b0   b1   be
 
 naδ : Q2 → Σ2 → Q2 → Bool
 naδ a0 ca a1 = true
 naδ a0 _ _ = false
 naδ a1 cf ae = true
 naδ a1 _ a1 = true
+naδ ae cf ae = true
+naδ ae _ a1 = true
 naδ _ _ _ = false
 
 a-start : Q2 → Bool
@@ -160,6 +171,8 @@
 nbδ ae _ _ = false
 nbδ b1 cf be = true
 nbδ b1 _ b1 = true
+nbδ be cf be = true
+nbδ be _ b1 = true
 nbδ _ _ _ = false
 
 b-start : Q2 → Bool
@@ -170,7 +183,7 @@
 nfa-b = record { Nδ = nbδ ; Nend = b-end }
 
 nfa-b-exists : (Q2 → Bool) → Bool
-nfa-b-exists p = p b0 \/ p b1 \/ p ae
+nfa-b-exists p = p b0 \/ p b1 \/ p be
 
 -- (a.*f)(b.*f)
 
@@ -183,11 +196,23 @@
 nfa-ab-exists : (Q2 → Bool) → Bool
 nfa-ab-exists p = nfa-a-exists p \/ nfa-b-exists p
 
+test-ab1-data : List Σ2
+test-ab1-data = ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] )
+
 test-ab1 : Bool
-test-ab1 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] )
+test-ab1 = Naccept nfa-ab nfa-ab-exists a-start test-ab1-data  -- should be false
+
+test-ab2-data : List Σ2
+test-ab2-data = ( ca ∷ cf ∷ ca ∷ cf ∷ cb ∷ cb ∷ cf ∷ [] )
 
 test-ab2 : Bool
-test-ab2 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cb ∷ [] )
+test-ab2 = Naccept nfa-ab nfa-ab-exists a-start test-ab2-data   -- should be true
+
+q2-list : List Q2
+q2-list = a0 ∷ a1 ∷ ae ∷ af ∷ b0 ∷ b1 ∷ be ∷ bf ∷ []
+
+test-tr : List (List Q2)
+test-tr = Ntrace nfa-ab q2-list nfa-ab-exists a-start ( ca ∷ cf ∷ cf ∷ cb ∷ cb ∷ cf ∷ [] )
 
 -- test-ab3 = map reverse ( NtraceDepth nfa-ab a-start (a0 ∷ a1 ∷ ae  ∷ b0 ∷ b1 ∷ be  ∷ [])  ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] ))
 
@@ -200,9 +225,36 @@
 test113 = accept test112 a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cb ∷ [] )
 
 -- 
+open import regex
+open import Relation.Nullary using (¬_; Dec; yes; no)
+
+Σ2-cmp : (x y : Σ2 ) → Dec (x ≡ y)
+Σ2-cmp ca ca = yes refl
+Σ2-cmp ca cb = no (λ ())
+Σ2-cmp ca cc = no (λ ())    
+Σ2-cmp ca cf = no (λ ())    
+Σ2-cmp cb ca =  no (λ ())
+Σ2-cmp cb cb = yes refl
+Σ2-cmp cb cc =  no (λ ())
+Σ2-cmp cb cf =  no (λ ())
+Σ2-cmp cc ca =  no (λ ())
+Σ2-cmp cc cb =  no (λ ())
+Σ2-cmp cc cc = yes refl
+Σ2-cmp cc cf =  no (λ ())
+Σ2-cmp cf ca =  no (λ ())
+Σ2-cmp cf cb =  no (λ ())
+Σ2-cmp cf cc =  no (λ ())
+Σ2-cmp cf cf = yes refl
+
+Σ2-any :  Regex Σ2
+Σ2-any = < ca > || < cb > || < cc > || < cf >
+
+test-ab1-regex : regex-language ( (< ca > & (Σ2-any *) & < cf > ) & (< cb > & (Σ2-any *) & < cf > )  )  Σ2-cmp test-ab1-data ≡ false
+test-ab1-regex = refl
+
+test-ab2-regex : regex-language ( (< ca > & (Σ2-any *) & < cf > ) & (< cb > & (Σ2-any *) & < cf > )  )  Σ2-cmp test-ab2-data ≡ true
+test-ab2-regex = refl
 
 
 
 
-
-