# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1605315536 -32400
# Node ID bf6d7843ba11cb8c33a46c748b3bf3a89889c952
# Parent  b4548639121e68d74796c1d2bf47c08f8fa2c602
...

diff -r b4548639121e -r bf6d7843ba11 nfa.agda
--- a/nfa.agda	Sat Nov 14 09:27:57 2020 +0900
+++ b/nfa.agda	Sat Nov 14 09:58:56 2020 +0900
@@ -67,18 +67,18 @@
 
 decFN136 : (qs qs' : Q3 → Set)  → (x : List Σ2) → naccept exists-in-Q3 nfa136 qs x → (q : Q3) → Dec (qs' q ∧ NF nfa136 q)
 decFN136 qs qs' (_ ∷ _)  _ _ = {!!}
-decFN136 qs qs' [] (qe1 x) q₁ = {!!}
+decFN136 qs qs' [] (qe1 x) q₁ = yes [ {!!} , refl ]
 decFN136 qs qs' []  _ q₂ = no (λ ())
 decFN136 qs qs' []  _ q₃ = no (λ ())
 
-decF̨δ136 :  (qs qs' : Q3 → Set) (x : Σ2) (t : List Σ2) → naccept exists-in-Q3 nfa136 qs' t → (q : Q3) →
-    Dec (naccept exists-in-Q3 nfa136 (λ q' → qs' q ∧ Nδ nfa136 q x q') t)
-decF̨δ136 qs qs' x t a q₁ = {!!}
-decF̨δ136 qs qs' x t a q₂ = {!!}
-decF̨δ136 qs qs' x t a q₃ = {!!}
+decF̨δ136 :  (qs qs' : Q3 → Set) (s : Σ2) (t x : List Σ2) → naccept exists-in-Q3 nfa136 qs x → (q : Q3) →
+    Dec (naccept exists-in-Q3 nfa136 (λ q' → qs' q ∧ Nδ nfa136 q s q') t)
+decF̨δ136 qs qs' s t x a q₁ = {!!}
+decF̨δ136 qs qs' s t x a q₂ = {!!}
+decF̨δ136 qs qs' s t x a q₃ = {!!}
 
 nfa136trace : (qs : Q3 → Set) → (input : List Σ2 ) → naccept exists-in-Q3 nfa136 qs input → List (List Q3)
-nfa136trace qs x a = ntrace exists-in-Q3 nfa136 qs x a (λ qs' q → decFN136 qs qs' x a q ) (λ qs' x t q →  decF̨δ136 qs qs' x {!!} a q) Q3List
+nfa136trace qs x a = ntrace exists-in-Q3 nfa136 qs x a (λ qs' q → decFN136 qs qs' x a q ) (λ qs' s t q →  decF̨δ136 qs qs' s t x a q ) Q3List
 
 subset-construction : {n : Level} { Q : Set n } { Σ : Set  }   → (Nexists : (Q → Set)  → Set) → 
     (NAutomaton Q  Σ ) → Automaton {Suc Zero ⊔ n} (Q → Set) Σ