--- a/automaton-in-agda/src/automaton-ex.agda	Wed Nov 17 16:12:30 2021 +0900
+++ b/automaton-in-agda/src/automaton-ex.agda	Thu Nov 25 08:48:41 2021 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module automaton-ex where
 
 open import Data.Nat

--- a/automaton-in-agda/src/nfa.agda	Wed Nov 17 16:12:30 2021 +0900
+++ b/automaton-in-agda/src/nfa.agda	Thu Nov 25 08:48:41 2021 +0900
@@ -5,7 +5,7 @@
 open import Data.Nat
 open import Data.List
 open import Data.Fin hiding ( _<_ )
-open import Data.Maybe
+open import Data.Maybe hiding ( zip )
 open import Relation.Nullary
 open import Data.Empty
 -- open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
@@ -39,7 +39,7 @@
 existsS1 qs = qs sr \/ qs ss \/ qs st
 
 -- extract list of q which qs q is true
-to-listS1 : ( States1 → Bool ) → List States1            
+to-listS1 : ( States1 → Bool ) → List States1
 to-listS1 qs = ss1 LStates1 where
    ss1 : List States1 → List States1
    ss1 [] = []
@@ -150,3 +150,65 @@
 dexample4-1 = accept am2def start1 ( i0  ∷ i1  ∷ i1  ∷ i0 ∷ [] ) 
 texample4-1 = trace am2def start1 ( i0  ∷ i1  ∷ i1  ∷ i0 ∷ [] ) 
 
+-- LStates1 contains all states in States1
+
+-- a list of Q contains (q : Q)
+
+eqState1? : (x y : States1)  →  Dec ( x ≡ y )
+eqState1? sr sr = yes refl
+eqState1? ss ss = yes refl
+eqState1? st st = yes refl
+eqState1? sr ss = no (λ ())
+eqState1? sr st = no (λ ())
+eqState1? ss sr = no (λ ())
+eqState1? ss st = no (λ ())
+eqState1? st sr = no (λ ())
+eqState1? st ss = no (λ ())
+
+
+list-contains  : {Q : Set} → ( (x y : Q ) → Dec ( x ≡ y ) ) → (qs : List Q) → (q : Q ) → Bool
+list-contains {Q} eq? [] q = false
+list-contains {Q} eq? (x ∷ qs) q with eq? x q
+... | yes _  = true
+... | no _  = list-contains eq? qs q
+
+containsP : {Q : Set} → ( eq? : (x y : Q ) →  Dec ( x ≡ y ))  → (qs : List Q) → (q : Q ) → Set 
+containsP eq? qs q = list-contains eq? qs q ≡ true
+
+module All (Q : Set)  (eq? : (x y : Q ) →  Dec ( x ≡ y )) (all : List Q ) (is-all : (q : Q ) → containsP eq? all q)  where
+
+    -- foldr : (A → B → B) → B → List A → B
+    -- foldr c n []       = n
+    -- foldr c n (x ∷ xs) = c x (foldr c n xs)
+
+    ssQ : ( qs : Q → Bool ) → List Q → List Q
+    ssQ qs [] = []
+    ssQ qs (x ∷ t) with qs x
+    ... | true   = x ∷ ssQ qs t
+    ... | false  = ssQ qs t 
+
+    to-listQ : ( qs : Q → Bool ) → List Q
+    to-listQ qs = ssQ qs all 
+
+    bool-t1 : {b : Bool } → b ≡ true → (true /\ b)  ≡ true
+    bool-t1 refl = refl
+
+    bool-1t : {b : Bool } → b ≡ true → (b /\ true)  ≡ true
+    bool-1t refl = refl
+
+    to-listS2 : ( qs : Q → Bool ) → foldr (λ q x → qs q /\ x ) true (to-listQ qs) ≡ true
+    to-listS2 qs = to-list1 all where
+        to-list1 : (all : List Q) →  foldr (λ q x → qs q /\ x ) true (ssQ  qs all ) ≡ true
+        to-list1 []  = refl
+        to-list1 (x ∷ all)  with qs x  | inspect qs x
+        ... | false | record { eq = eq } = to-list1 all 
+        ... | true  | record { eq = eq } = subst (λ k → k /\ foldr (λ q → _/\_ (qs q)) true (ssQ qs all) ≡ true ) (sym eq) ( bool-t1 (to-list1 all) )
+
+    existsS1-valid : ¬ ( (qs : States1 → Bool ) →  ( existsS1 qs ≡ true ) )
+    existsS1-valid n = ¬-bool refl ( n ( λ x → false ))
+
+contains-all : (q : States1 ) → containsP eqState1? LStates1 q 
+contains-all sr = refl
+contains-all ss = refl
+contains-all st = refl
+

--- a/automaton-in-agda/src/regular-language.agda	Wed Nov 17 16:12:30 2021 +0900
+++ b/automaton-in-agda/src/regular-language.agda	Thu Nov 25 08:48:41 2021 +0900
@@ -20,16 +20,6 @@
 language-L : { Σ : Set } → Set
 language-L {Σ} = List (List Σ)
 
-open Automaton
-
-record RegularLanguage ( Σ : Set ) : Set (Suc Zero) where
-   field
-      states : Set 
-      astart : states 
-      automaton : Automaton states Σ
-   contain : List Σ → Bool
-   contain x = accept automaton astart x
-
 Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
 Union {Σ} A B x = (A x ) \/ (B x)
 
@@ -60,9 +50,27 @@
 star-nil : {Σ : Set} → ( A : language {Σ} ) → Star A [] ≡ true
 star-nil A = refl
 
+open Automaton
+
+record RegularLanguage ( Σ : Set ) : Set (Suc Zero) where
+   field
+      states : Set 
+      astart : states 
+      automaton : Automaton states Σ
+   contain : List Σ → Bool
+   contain x = accept automaton astart x
+
+RegularLanguage-is-language : { Σ : Set } → RegularLanguage Σ  → language {Σ} 
+RegularLanguage-is-language {Σ} R = RegularLanguage.contain R 
+
+RegularLanguage-is-language' : { Σ : Set } → RegularLanguage Σ  → List Σ  → Bool
+RegularLanguage-is-language' {Σ} R x = accept (automaton R) (astart R) x where
+   open RegularLanguage
+
 open RegularLanguage 
 isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set
 isRegular A x r = A x ≡ contain r x 
+--  a language is implemented by an automaton
 
 -- postulate 
 --   fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b}