--- a/nfa.agda	Sat Nov 14 18:05:41 2020 +0900
+++ b/nfa.agda	Sat Nov 14 19:10:03 2020 +0900
@@ -69,39 +69,65 @@
 decs136 q₂ = no (λ ())
 decs136 q₃ = no (λ ())
 
+dect136 : (x : Σ2)  → (nq q : Q3)  →  Dec (Nδ nfa136 nq x q) 
+dect136 s0 q₁ q₁ = yes d1
+dect136 s0 q₁ q₂ = no (λ ())
+dect136 s0 q₁ q₃ =  no (λ ())
+dect136 s0 q₂ q₁ =  no (λ ())
+dect136 s0 q₂ q₂ =  yes d2
+dect136 s0 q₂ q₃ =  yes d3
+dect136 s0 q₃ q₁ =  yes d5
+dect136 s0 q₃ q₂ =  no (λ ())
+dect136 s0 q₃ q₃ =  no (λ ())
+dect136 s1 q₁ q₁ =  no (λ ())
+dect136 s1 q₁ q₂ =  yes d0
+dect136 s1 q₁ q₃ =  no (λ ())
+dect136 s1 q₂ q₁ =  no (λ ())
+dect136 s1 q₂ q₂ =  no (λ ())
+dect136 s1 q₂ q₃ =  yes d4
+dect136 s1 q₃ q₁ =  no (λ ())
+dect136 s1 q₃ q₂ =  no (λ ())
+dect136 s1 q₃ q₃ =  no (λ ())
+
 open import Data.Empty
 open import Relation.Nullary
 open _∧_
 
-p136→ : (qs : Q3 → Set) → exists-in-Q3 (λ nq → qs nq ) →   qs q₁  ∨  qs q₂  ∨   qs q₃  
-p136→ qs (qe1 a) = case1 a 
-p136→ qs (qe2 a) = case2 (case1 a)
-p136→ qs (qe3 a) = case2 (case2 a)
-
-p136← : (qs : Q3 → Set) → qs q₁  ∨  qs q₂  ∨   qs q₃ → exists-in-Q3 (λ nq → qs nq ) 
-p136← qs (case1 a) = qe1 a
-p136← qs (case2 (case1 a)) = qe2 a
-p136← qs (case2 (case2 a)) = qe3 a
-
 next136 : (qs : Q3 → Set) → ((q : Q3) → Dec (qs q)) → (x : Σ2) (q : Q3) →
     Dec (exists-in-Q3 (λ nq → qs nq ∧ Nδ nfa136 nq x q))
-next136 qs dec x q = {!!} where
-   ne1 : (q : Q3) → (x : Σ2) → Dec (qs q₁) → Dec (qs q₁ ∧ Nδ nfa136 q₁ x q)
-   ne1 q x ( no n)  = no ( λ not → n (proj1 not))
-   ne1 q₁ s0 (yes y) = yes [ y , d1 ]
-   ne1 q₁ s1 (yes y) = no (λ not → ne11 (proj2 not)) where
-     ne11 : ¬ Nδ nfa136 q₁ s1 q₁
-     ne11 ()
-   ne1 q₂ s0 (yes y) = no (λ not → ne12 (proj2 not)) where
-     ne12 : ¬ Nδ nfa136 q₁ s0 q₂
-     ne12 ()
-   ne1 q₂ s1 (yes y) = yes [ y , d0 ]
-   ne1 q₃ s0 (yes y) = {!!}
-   ne1 q₃ s1 (yes y) = {!!}
+next136 qs dec x q = ne0 where
+   ne1 : (q : Q3) → (x : Σ2) → Dec (qs q₁) → Dec (Nδ nfa136 q₁ x q) → Dec (qs q₁ ∧ Nδ nfa136 q₁ x q)
+   ne1 q x (no n) _ = no (λ not → n (proj1 not))
+   ne1 q x _ (no n) = no (λ not → n (proj2 not))
+   ne1 q x (yes y0) (yes y1) = yes [ y0 , y1 ]
+   ne2 : (q : Q3) → (x : Σ2) → Dec (qs q₂) → Dec (Nδ nfa136 q₂ x q) → Dec (qs q₂ ∧ Nδ nfa136 q₂ x q)
+   ne2 q x (no n) _ = no (λ not → n (proj1 not))
+   ne2 q x _ (no n) = no (λ not → n (proj2 not))
+   ne2 q x (yes y0) (yes y1) = yes [ y0 , y1 ]
+   ne3 : (q : Q3) → (x : Σ2) → Dec (qs q₃) → Dec (Nδ nfa136 q₃ x q) → Dec (qs q₃ ∧ Nδ nfa136 q₃ x q)
+   ne3 q x (no n) _ = no (λ not → n (proj1 not))
+   ne3 q x _ (no n) = no (λ not → n (proj2 not))
+   ne3 q x (yes y0) (yes y1) = yes [ y0 , y1 ]
+   ne0 : Dec (exists-in-Q3 (λ nq → qs nq ∧ Nδ nfa136 nq x q))
+   ne0 with ne1 q x (dec q₁) (dect136 x q₁ q)
+   ... | yes y = yes ( qe1 y)
+   ... | no n with ne2 q x (dec q₂) (dect136 x q₂ q)
+   ... | yes y2 = yes (qe2 y2)
+   ... | no n2 with ne3 q x (dec q₃) (dect136 x q₃ q)
+   ... | yes y3 = yes (qe3 y3)
+   ... | no n3 = no ne4 where
+      ne4 : ¬ exists-in-Q3 (λ nq → qs nq ∧ transition136 nq x q)
+      ne4 (qe1 x) = n x
+      ne4 (qe2 x) = n2 x
+      ne4 (qe3 x) = n3 x
 
 nfa136trace : (input : List Σ2 ) → naccept exists-in-Q3 nfa136 start136 input → List (List Q3)
 nfa136trace x a = ntrace exists-in-Q3 nfa136 start136 x a decs136 next136 Q3List
 
+postulate
+   nfa13rs1 : example136-1 
+nfa13rt1 = nfa136trace ( s0  ∷ s1  ∷ s0 ∷ s0 ∷ [] ) nfa13rs1
+
 subset-construction : {n : Level} { Q : Set n } { Σ : Set  }   → (Nexists : (Q → Set)  → Set) → 
     (NAutomaton Q  Σ ) → Automaton {Suc Zero ⊔ n} (Q → Set) Σ 
 subset-construction {n} {Q} { Σ} Nexists  nfa = record {