Mercurial > hg > Members > kono > Proof > automaton1
changeset 5:06cc23ff53d7
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 14 Nov 2020 11:05:25 +0900 |
| parents | 2d8d29454b0f |
| children | c42493f74570 |
| files | nfa.agda |
| diffstat | 1 files changed, 2 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/nfa.agda Sat Nov 14 10:41:38 2020 +0900 +++ b/nfa.agda Sat Nov 14 11:05:25 2020 +0900 @@ -58,11 +58,6 @@ example136-2 = naccept exists-in-Q3 nfa136 start136 ( s1 ∷ s0 ∷ s1 ∷ s0 ∷ s1 ∷ [] ) -nfa136-FN : (q : Q3 ) → Dec ( NF nfa136 q ) -nfa136-FN q₁ = yes refl -nfa136-FN q₂ = no (λ ()) -nfa136-FN q₃ = no (λ ()) - Q3List : List Q3 Q3List = q₁ ∷ q₂ ∷ q₃ ∷ [] @@ -74,9 +69,8 @@ decF̨δ136 : (qs' : Q3 → Set) (s : Σ2) (t : List Σ2) → (a : naccept exists-in-Q3 nfa136 (λ q' → exists-in-Q3 (λ q₄ → qs' q₄ ∧ transition136 q₄ s q')) t) → (q : Q3) → Dec (naccept exists-in-Q3 nfa136 (λ q' → qs' q ∧ Nδ nfa136 q s q') t) -decF̨δ136 qs' s t a q₁ = ? -decF̨δ136 qs' s t a q₂ = {!!} -decF̨δ136 qs' s t a q₃ = {!!} +decF̨δ136 qs' s [] a q = {!!} +decF̨δ136 qs' s (x ∷ t) 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' a' q → decFN136 qs' q a' ) (λ qs' s t a' q → decF̨δ136 qs' s t a' q ) Q3List