--- a/automaton-in-agda/src/nfa136.agda	Thu Nov 09 18:04:55 2023 +0900
+++ b/automaton-in-agda/src/nfa136.agda	Wed Nov 15 16:24:07 2023 +0900
@@ -45,7 +45,7 @@
 
 t146-1 = Ntrace nfa136 states136 exists136  start136( a0  ∷ b0  ∷ a0 ∷ a0 ∷ [] )
 
-test111 = ?
+-- test111 = ?
 
 example136-0 = Naccept nfa136 exists136 start136( a0 ∷ [] )
 
@@ -83,29 +83,67 @@
    a0 : Q2
    a1 : Q2
    ae : Q2
+   af : Q2
    b0 : Q2
    b1 : Q2
    be : Q2
+   bf : Q2
 
 -- a.*f
 
-aδ : Q2 → Σ2 → Q2 → Bool
-aδ a0 ca a1 = true
-aδ a0 _ _ = false
-aδ a1 cf ae = true
-aδ a1 _ a1 = true
-aδ _ _ _ = false
-
 a-end : Q2 → Bool
 a-end ae = true
 a-end _ = false
 
+aδ : Q2 → Σ2 → Q2 
+aδ a0 ca = a1 
+aδ a0 _ = af 
+aδ a1 cf = ae 
+aδ a1 _ = a1 
+aδ ae cf = ae 
+aδ ae _ = a1 
+aδ _ _ = af 
+fa-a : Automaton Q2 Σ2
+fa-a = record { δ = aδ ; aend = a-end }
+
+test111 : Bool
+test111 = accept fa-a a0 ( ca ∷ cf ∷ ca ∷ [] )
+
+b-end : Q2 → Bool
+b-end be = true
+b-end _ = false
+
+bδ : Q2 → Σ2 → Q2 
+bδ b0 cb = b1 
+bδ b0 _ = bf 
+bδ b1 cf = be 
+bδ b1 _ = b1 
+bδ be cf = be 
+bδ be _ = b1 
+bδ _ _ = bf 
+fa-b : Automaton Q2 Σ2
+fa-b = record { δ = bδ ; aend = b-end }
+
+test115 : Bool
+test115 = accept fa-b b0 ( cb ∷ cf ∷ cf ∷ [] )
+
+open import regular-language
+
+test116 = split (accept fa-a a0) (accept fa-b b0) ( ca ∷ cf ∷ cb ∷ cf ∷ cf ∷ [] )
+
+naδ : Q2 → Σ2 → Q2 → Bool
+naδ a0 ca a1 = true
+naδ a0 _ _ = false
+naδ a1 cf ae = true
+naδ a1 _ a1 = true
+naδ _ _ _ = false
+
 a-start : Q2 → Bool
 a-start a0 = true
 a-start _ = false
 
 nfa-a : NAutomaton Q2 Σ2
-nfa-a = record { Nδ = aδ ; Nend = a-end }
+nfa-a = record { Nδ = naδ ; Nend = a-end }
 
 nfa-a-exists : (Q2 → Bool) → Bool
 nfa-a-exists p = p a0 \/ p a1 \/ p ae
@@ -113,27 +151,23 @@
 test-a1 : Bool
 test-a1 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ [] )
 
-test-a2 = map reverse ( NtraceDepth nfa-a a-start (a0 ∷ a1 ∷ ae  ∷ [])  ( ca ∷ cf ∷ cf ∷ [] ) )
+-- test-a2 = map reverse ( NtraceDepth nfa-a a-start (a0 ∷ a1 ∷ ae  ∷ [])  ( ca ∷ cf ∷ cf ∷ [] ) )
 
 -- b.*f
 
-bδ : Q2 → Σ2 → Q2 → Bool
-bδ ae cb b1 = true
-bδ ae _ _ = false
-bδ b1 cf be = true
-bδ b1 _ b1 = true
-bδ _ _ _ = false
-
-b-end : Q2 → Bool
-b-end be = true
-b-end _ = false
+nbδ : Q2 → Σ2 → Q2 → Bool
+nbδ ae cb b1 = true
+nbδ ae _ _ = false
+nbδ b1 cf be = true
+nbδ b1 _ b1 = true
+nbδ _ _ _ = false
 
 b-start : Q2 → Bool
 b-start ae = true
 b-start _ = false
 
 nfa-b : NAutomaton Q2 Σ2
-nfa-b = record { Nδ = bδ ; Nend = b-end }
+nfa-b = record { Nδ = nbδ ; Nend = b-end }
 
 nfa-b-exists : (Q2 → Bool) → Bool
 nfa-b-exists p = p b0 \/ p b1 \/ p ae
@@ -141,7 +175,7 @@
 -- (a.*f)(b.*f)
 
 abδ : Q2 → Σ2 → Q2 → Bool
-abδ x i y = aδ x i y \/ bδ x i y
+abδ x i y = naδ x i y \/ nbδ x i y
 
 nfa-ab : NAutomaton Q2 Σ2
 nfa-ab = record { Nδ = abδ ; Nend = b-end }
@@ -155,7 +189,7 @@
 test-ab2 : Bool
 test-ab2 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cb ∷ [] )
 
-test-ab3 = map reverse ( NtraceDepth nfa-ab a-start (a0 ∷ a1 ∷ ae  ∷ b0 ∷ b1 ∷ be  ∷ [])  ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] ))
+-- test-ab3 = map reverse ( NtraceDepth nfa-ab a-start (a0 ∷ a1 ∷ ae  ∷ b0 ∷ b1 ∷ be  ∷ [])  ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] ))
 
 test112 : Automaton (Q2 → Bool) Σ2
 test112 = subset-construction nfa-ab-exists nfa-ab
@@ -165,3 +199,10 @@
 test113 : Bool
 test113 = accept test112 a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cb ∷ [] )
 
+-- 
+
+
+
+
+
+