Mercurial > hg > Members > kono > Proof > automaton1

changeset 3:bf6d7843ba11

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 14 Nov 2020 09:58:56 +0900
parents b4548639121e
children 2d8d29454b0f
files nfa.agda
diffstat 1 files changed, 7 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- 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) Σ