Mercurial > hg > Members > kono > Proof > automaton

changeset 268:8006cbd87b20

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix concat dfa
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 25 Nov 2021 12:19:36 +0900
parents ae70f96cb60c
children 52ed73a116d0
files automaton-in-agda/src/fin.agda automaton-in-agda/src/finiteSetUtil.agda automaton-in-agda/src/nfa.agda automaton-in-agda/src/regular-concat.agda automaton-in-agda/src/regular-language.agda automaton-in-agda/src/sbconst2.agda
diffstat 6 files changed, 167 insertions(+), 98 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/fin.agda	Thu Nov 25 08:48:41 2021 +0900
+++ b/automaton-in-agda/src/fin.agda	Thu Nov 25 12:19:36 2021 +0900
@@ -2,7 +2,7 @@
 
 module fin where
 
-open import Data.Fin hiding (_<_ ; _≤_ )
+open import Data.Fin hiding (_<_ ; _≤_ ; _>_ )
 open import Data.Fin.Properties hiding ( <-trans )
 open import Data.Nat
 open import logic
@@ -114,4 +114,3 @@
            ∎  where
                open ≡-Reasoning
 
-
--- a/automaton-in-agda/src/finiteSetUtil.agda	Thu Nov 25 08:48:41 2021 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Thu Nov 25 12:19:36 2021 +0900
@@ -23,8 +23,16 @@
 
 open Bijection
 
+open import Axiom.Extensionality.Propositional
+open import Level hiding (suc ; zero)
+postulate f-extensionality : { n : Level}  → Axiom.Extensionality.Propositional.Extensionality n n -- (Level.suc n)
+
 module _ {Q : Set } (F : FiniteSet Q) where
      open FiniteSet F
+     equal?-refl  : { x : Q } → equal? x x ≡ true 
+     equal?-refl {x} with F←Q x ≟ F←Q x
+     ... | yes refl = refl
+     ... | no ne = ⊥-elim (ne refl)
      equal→refl  : { x y : Q } → equal? x y ≡ true → x ≡ y
      equal→refl {q0} {q1} eq with F←Q q0 ≟ F←Q q1
      equal→refl {q0} {q1} refl | yes eq = begin
@@ -62,6 +70,31 @@
               ≡⟨ found1 m (<to≤  m<n) (next-end p end m<n (¬-bool-t np )) ⟩
                  true
               ∎  where open ≡-Reasoning
+     not-found : { p : Q → Bool } → ( (q : Q ) → p q ≡ false ) → exists p ≡ false
+     not-found {p} pn = not-found2 finite NatP.≤-refl where
+         not-found2 : (m : ℕ ) → (m<n : m Data.Nat.≤ finite ) → exists1 m m<n p ≡ false
+         not-found2  zero  _ = refl
+         not-found2 ( suc m ) m<n with pn (Q←F (fromℕ< {m} {finite} m<n))
+         not-found2 (suc m) m<n | eq = begin
+                  p (Q←F (fromℕ< m<n)) \/ exists1 m (<to≤ m<n) p 
+              ≡⟨ bool-or-1 eq ⟩
+                  exists1 m (<to≤ m<n) p 
+              ≡⟨ not-found2 m (<to≤ m<n)  ⟩
+                  false
+              ∎  where open ≡-Reasoning
+     found← : { p : Q → Bool } → exists p ≡ true → Found Q p
+     found← {p} exst = found2 finite NatP.≤-refl  (first-end p ) where
+         found2 : (m : ℕ ) (m<n : m Data.Nat.≤ finite ) → End m p →  Found Q p
+         found2 0 m<n end = ⊥-elim ( ¬-bool (not-found (λ q → end (F←Q q)  z≤n ) ) (subst (λ k → exists k ≡ true) (sym lemma) exst ) ) where
+             lemma : (λ z → p (Q←F (F←Q z))) ≡ p
+             lemma = f-extensionality ( λ q → subst (λ k → p k ≡ p q ) (sym (finiso→ q)) refl )
+         found2 (suc m)  m<n end with bool-≡-? (p (Q←F (fromℕ< m<n))) true
+         found2 (suc m)  m<n end | yes eq = record { found-q = Q←F (fromℕ< m<n) ; found-p = eq }
+         found2 (suc m)  m<n end | no np = 
+               found2 m (<to≤ m<n) (next-end p end m<n (¬-bool-t np )) 
+     not-found← : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false 
+     not-found← {p} np q = ¬-bool-t ( contra-position {_} {_} {_} {exists p ≡ true} (found q) (λ ep → ¬-bool np ep ) )
+
 
 
 iso-fin : {A B : Set} → FiniteSet A  → Bijection A B → FiniteSet B 
@@ -293,7 +326,7 @@
 
 open import Level renaming ( suc to Suc ; zero to Zero) 
 open import Axiom.Extensionality.Propositional
-postulate f-extensionality : { n : Level}  →  Axiom.Extensionality.Propositional.Extensionality n n 
+-- postulate f-extensionality : { n : Level}  →  Axiom.Extensionality.Propositional.Extensionality n n 
 
 F2L-iso : { Q : Set } → (fin : FiniteSet Q ) → (x : Vec Bool (FiniteSet.finite fin) ) → F2L fin a<sa (λ q _ → List2Func fin a<sa x q ) ≡ x
 F2L-iso {Q} fin x = f2l m a<sa x where
--- a/automaton-in-agda/src/nfa.agda	Thu Nov 25 08:48:41 2021 +0900
+++ b/automaton-in-agda/src/nfa.agda	Thu Nov 25 12:19:36 2021 +0900
@@ -175,40 +175,77 @@
 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
 
+-- foldr : (A → B → B) → B → List A → B
+-- foldr c n []       = n
+-- foldr c n (x ∷ xs) = c x (foldr c n xs)
+
+ssQ : {Q : Set } ( 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 
+
+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-list1 : {Q : Set } (qs : Q → Bool ) →  (all : List Q) → foldr (λ q x → qs q /\ x ) true (ssQ  qs all ) ≡ true
+to-list1 qs []  = refl
+to-list1 qs (x ∷ all)  with qs x  | inspect qs x
+... | false | record { eq = eq } = to-list1 qs all 
+... | true  | record { eq = eq } = subst (λ k → k /\ foldr (λ q → _/\_ (qs q)) true (ssQ qs all) ≡ true ) (sym eq) ( bool-t1 (to-list1 qs all) )
+
+existsS1-valid : ¬ ( (qs : States1 → Bool ) →  ( existsS1 qs ≡ true ) )
+existsS1-valid n = ¬-bool refl ( n ( λ x → false ))
+
+--
+--  using finiteSet
+--
+
+open import finiteSet
+open import finiteSetUtil
+open FiniteSet
+
+allQ : {Q : Set } (finq : FiniteSet Q) → List Q
+allQ {Q} finq = to-list finq (λ x → true)
+
+existQ : {Q : Set } (finq : FiniteSet Q) → (Q → Bool) → Bool
+existQ finq qs = exists finq qs
+
+eqQ? : {Q : Set } (finq : FiniteSet Q) → (x y : Q ) → Bool
+eqQ? finq x y = equal? finq x y
+
+finState1 : FiniteSet States1
+finState1 = record {
+     finite = finite0
+   ; Q←F = Q←F0 
+   ; F←Q = F←Q0 
+   ; finiso→ = finiso→0
+   ; finiso← = finiso←0
+ } where
+     finite0 : ℕ
+     finite0 = 3
+     Q←F0 : Fin finite0 → States1
+     Q←F0 zero = sr
+     Q←F0 (suc zero) = ss
+     Q←F0 (suc (suc zero)) = st
+     F←Q0 : States1 → Fin finite0
+     F←Q0 sr = # 0
+     F←Q0 ss = # 1
+     F←Q0 st = # 2
+     finiso→0 : (q : States1) → Q←F0 ( F←Q0 q ) ≡ q
+     finiso→0 sr = refl
+     finiso→0 ss = refl
+     finiso→0 st = refl
+     finiso←0 : (f : Fin finite0 ) → F←Q0 ( Q←F0 f ) ≡ f
+     finiso←0 zero = refl
+     finiso←0 (suc zero) = refl
+     finiso←0 (suc (suc zero)) = refl
+
--- a/automaton-in-agda/src/regular-concat.agda	Thu Nov 25 08:48:41 2021 +0900
+++ b/automaton-in-agda/src/regular-concat.agda	Thu Nov 25 12:19:36 2021 +0900
@@ -13,47 +13,47 @@
 open import logic
 open import nat
 open import automaton
-open import regular-language
+open import regular-language 
 
 open import nfa
 open import sbconst2
-
-open RegularLanguage
-open Automaton
+open import finiteSet
+open import finiteSetUtil
 
-Concat-NFA :  {Σ : Set} → (A B : RegularLanguage Σ ) → ((x y : states A )→ Dec (x ≡ y)) → ((x y : states B )→ Dec (x ≡ y))
-    → NAutomaton (states A ∨ states B) Σ 
-Concat-NFA {Σ} A B equal?A equal?B = record { Nδ = δnfa ; Nend = nend } 
+open Automaton
+open FiniteSet
+
+
+Concat-NFA :  {Σ : Set} → (A B : RegularLanguage Σ ) → NAutomaton (states A ∨ states B) Σ 
+Concat-NFA {Σ} A B = record { Nδ = δnfa ; Nend = nend } 
    module Concat-NFA where
        δnfa : states A ∨ states B → Σ → states A ∨ states B → Bool
-       δnfa (case1 q) i (case1 q₁) with equal?A (δ (automaton A) q i) q₁
-       ... | yes _ = true
-       ... | no _ =  false
-       δnfa (case1 qa) i (case2 qb) with equal?B qb (δ (automaton B) (astart B) i) 
-       ... | yes _ = aend (automaton A) qa 
-       ... | no _ =  false
-       δnfa (case2 q) i (case2 q₁) with equal?B (δ (automaton B) q i) q₁
-       ... | yes _ = true
-       ... | no _ =  false
+       δnfa (case1 q) i (case1 q₁) = equal? (afin A) (δ (automaton A) q i) q₁
+       δnfa (case1 qa) i (case2 qb) = (aend (automaton A) qa ) /\
+           (equal? (afin B) qb (δ (automaton B) (astart B) i) )
+       δnfa (case2 q) i (case2 q₁) = equal? (afin B) (δ (automaton B) q i) q₁
        δnfa _ i _ = false
        nend : states A ∨ states B → Bool
        nend (case2 q) = aend (automaton B) q
        nend (case1 q) = aend (automaton A) q /\ aend (automaton B) (astart B) -- empty B case
 
-Concat-NFA-start :  {Σ : Set} → (A B : RegularLanguage Σ ) → states A ∨ states B → ((x y : states A )→ Dec (x ≡ y))  → Bool
-Concat-NFA-start A B (case1 a) equal?A with equal?A a (astart A)
-... | yes _ = true
-... | no _ =  false
-Concat-NFA-start A B (case2 b) equal?A = false
+Concat-NFA-start :  {Σ : Set} → (A B : RegularLanguage Σ ) → states A ∨ states B → Bool
+Concat-NFA-start A B q = equal? (fin-∨ (afin A) (afin B)) (case1 (astart A)) q
+
+CNFA-exist : {Σ : Set} → (A B : RegularLanguage Σ ) → (states A ∨ states B → Bool) → Bool
+CNFA-exist A B qs = exists (fin-∨ (afin A) (afin B)) qs 
 
-M-Concat : {Σ : Set} → (A B : RegularLanguage Σ ) → ((states A → Bool) → Bool) → ((states B → Bool) → Bool)  → RegularLanguage Σ
-M-Concat {Σ} A B existsA existsB = record {
+M-Concat : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
+M-Concat {Σ} A B = record {
        states = states A ∨ states B → Bool
-     ; astart = λ ab → Concat-NFA-start A B ab {!!} 
-     ; automaton = subset-construction sbexists (Concat-NFA A B {!!} {!!} ) 
+     ; astart = Concat-NFA-start A B
+     ; afin = finf
+     ; automaton = subset-construction (CNFA-exist A B) (Concat-NFA A B) 
    } where
-       sbexists : (states A ∨ states B → Bool) → Bool
-       sbexists P = existsA ( λ a → existsB ( λ b → P (case1 a) \/ P (case2 b)))
+       fin : FiniteSet (states A ∨ states B ) 
+       fin = fin-∨ (afin A) (afin B)
+       finf : FiniteSet (states A ∨ states B → Bool ) 
+       finf = fin→ fin 
        
 record Split {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (x :  List Σ ) : Set where
     field
@@ -138,57 +138,50 @@
 open NAutomaton
 open import Data.List.Properties
 
-open import finiteSet
-open import finiteSetUtil
-
-open FiniteSet
-
 closed-in-concat :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
 closed-in-concat {Σ} A B x = ≡-Bool-func closed-in-concat→ closed-in-concat← where
-    afin : (A : RegularLanguage Σ ) → FiniteSet A
-    afin = ?
     finab = (fin-∨ (afin A) (afin B))
     NFA = (Concat-NFA A B)
     abmove : (q : states A ∨ states B) → (h : Σ ) → states A ∨ states B
     abmove (case1 q) h = case1 (δ (automaton A) q h)
     abmove (case2 q) h = case2 (δ (automaton B) q h)
     lemma-nmove-ab : (q : states A ∨ states B) → (h : Σ ) → Nδ NFA q h (abmove q h) ≡ true
-    lemma-nmove-ab (case1 q) _ = ? -- equal?-refl (afin A)
-    lemma-nmove-ab (case2 q) _ = ? -- equal?-refl (afin B)
+    lemma-nmove-ab (case1 q) h = equal?-refl (afin A) 
+    lemma-nmove-ab (case2 q) h = equal?-refl (afin B) 
     nmove : (q : states A ∨ states B) (nq : states A ∨ states B → Bool ) → (nq q ≡ true) → ( h : Σ ) →
        exists finab (λ qn → nq qn /\ Nδ NFA qn h (abmove q h)) ≡ true
     nmove (case1 q) nq nqt h = found finab (case1 q) ( bool-and-tt nqt (lemma-nmove-ab (case1 q)  h) )  
     nmove (case2 q) nq nqt h = found finab (case2 q) ( bool-and-tt nqt (lemma-nmove-ab (case2 q) h) ) 
     acceptB : (z : List Σ) → (q : states B) → (nq : states A ∨ states B → Bool ) → (nq (case2 q) ≡ true) → ( accept (automaton B) q z ≡ true ) 
-        → Naccept NFA finab nq z  ≡ true
+        → Naccept NFA (CNFA-exist A B) nq z  ≡ true
     acceptB [] q nq nqt fb = lemma8 where
         lemma8 : exists finab ( λ q → nq q /\ Nend NFA q ) ≡ true
         lemma8 = found finab (case2 q) ( bool-and-tt nqt fb )
-    acceptB (h ∷ t ) q nq nq=q fb = acceptB t (δ (automaton B) q h) (Nmoves NFA finab nq h) (nmove (case2 q) nq nq=q h) fb 
+    acceptB (h ∷ t ) q nq nq=q fb = acceptB t (δ (automaton B) q h) (Nmoves NFA (CNFA-exist A B) nq h) (nmove (case2 q) nq nq=q h) fb 
 
     acceptA : (y z : List Σ) → (q : states A) → (nq : states A ∨ states B → Bool ) → (nq (case1 q) ≡ true)
         → ( accept (automaton A) q y ≡ true ) → ( accept (automaton B) (astart B) z ≡ true ) 
-        → Naccept NFA finab nq (y ++ z)  ≡ true
+        → Naccept NFA (CNFA-exist A B) nq (y ++ z)  ≡ true
     acceptA [] [] q nq nqt fa fb = found finab (case1 q) (bool-and-tt nqt (bool-and-tt fa fb )) 
-    acceptA [] (h ∷ z)  q nq nq=q fa fb = acceptB z nextb (Nmoves NFA finab nq h) lemma70 fb where
+    acceptA [] (h ∷ z)  q nq nq=q fa fb = acceptB z nextb (Nmoves NFA (CNFA-exist A B) nq h) lemma70 fb where
          nextb : states B
          nextb = δ (automaton B) (astart B) h
          lemma70 : exists finab (λ qn → nq qn /\ Nδ NFA qn h (case2 nextb)) ≡ true
          lemma70 = found finab (case1 q) ( bool-and-tt nq=q (bool-and-tt fa (lemma-nmove-ab (case2 (astart B)) h) ))
-    acceptA (h ∷ t) z q nq nq=q fa fb = acceptA t z (δ (automaton A) q h) (Nmoves NFA finab nq h) (nmove (case1 q) nq nq=q h)  fa fb where
+    acceptA (h ∷ t) z q nq nq=q fa fb = acceptA t z (δ (automaton A) q h) (Nmoves NFA (CNFA-exist A B) nq h) (nmove (case1 q) nq nq=q h)  fa fb 
 
     acceptAB : Split (contain A) (contain B) x
-        → Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true
-    acceptAB S = subst ( λ k → Naccept NFA finab (equal? finab (case1 (astart A))) k  ≡ true  ) ( sp-concat S )
-        (acceptA (sp0 S) (sp1 S)  (astart A) (equal? finab (case1 (astart A))) ? (prop0 S) (prop1 S) )
+        → Naccept NFA (CNFA-exist A B) (equal? finab (case1 (astart A))) x  ≡ true
+    acceptAB S = subst ( λ k → Naccept NFA (CNFA-exist A B) (equal? finab (case1 (astart A))) k  ≡ true  ) ( sp-concat S )
+        (acceptA (sp0 S) (sp1 S)  (astart A) (equal? finab (case1 (astart A))) (equal?-refl finab) (prop0 S) (prop1 S) )
 
     closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true
     closed-in-concat→ concat with split→AB (contain A) (contain B) x concat
     ... | S = begin
-          accept (subset-construction finab NFA (case1 (astart A))) (Concat-NFA-start A B ) x 
-       ≡⟨ ≡-Bool-func (subset-construction-lemma← finab NFA (case1 (astart A)) x ) 
-          (subset-construction-lemma→ finab NFA (case1 (astart A)) x ) ⟩
-          Naccept NFA finab (equal? finab (case1 (astart A))) x
+          accept  (subset-construction (CNFA-exist A B) (Concat-NFA A B) ) (Concat-NFA-start A B ) x 
+       ≡⟨ ≡-Bool-func (subset-construction-lemma←  (CNFA-exist A B)  NFA (equal? finab (case1 (astart A))) x ) 
+          (subset-construction-lemma→  (CNFA-exist A B)  NFA (equal? finab (case1 (astart A))) x ) ⟩
+          Naccept NFA (CNFA-exist A B) (equal? finab (case1 (astart A))) x
        ≡⟨ acceptAB S ⟩
          true
        ∎  where open ≡-Reasoning
@@ -199,16 +192,17 @@
     ab-case (case1 qa') qa x = qa'  ≡ qa
     ab-case (case2 qb) qa x = ¬ ( accept (automaton B) qb x  ≡ true )
 
-    contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA finab nq x ≡ true )
+    contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA (CNFA-exist A B) nq x ≡ true )
           → (qa : states A )  → (  (q : states A ∨ states B) → nq q ≡ true → ab-case q qa x )
           → split (accept (automaton A) qa ) (contain B) x ≡ true
-    contain-A [] nq fn qa cond with found← finab fn 
+    contain-A [] nq fn qa cond with found← finab fn  -- at this stage, A and B must be satisfied with [] (ab-case cond forces it)
     ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S))
     ... | case1 qa' | record { eq = refl } | refl = bool-∧→tt-1 (found-p S)
     ... | case2 qb | record { eq = refl } | ab = ⊥-elim ( ab (bool-∧→tt-1 (found-p S)))
     contain-A (h ∷ t) nq fn qa cond with bool-≡-? ((aend (automaton A) qa) /\  accept (automaton B) (δ (automaton B) (astart B) h) t ) true
-    ... | yes eq = bool-or-41 eq
-    ... | no ne = bool-or-31 (contain-A t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) lemma11 ) where
+    ... | yes eq = bool-or-41 eq  -- found A ++ B all end
+    ... | no ne = bool-or-31 (contain-A t (Nmoves NFA (CNFA-exist A B) nq h) fn (δ (automaton A) qa h) lemma11 ) where -- B failed continue with ab-base condtion
+       --- prove ab-ase condition (we haven't checked but case2 b may happen)
        lemma11 :  (q : states A ∨ states B) → exists finab (λ qn → nq qn /\ Nδ NFA qn h q) ≡ true → ab-case q (δ (automaton A) qa h) t
        lemma11 (case1 qa')  ex with found← finab ex 
        ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) 
@@ -225,14 +219,14 @@
            lemma12 : accept (automaton B) qb t ≡ true → aend (automaton A) qa /\ accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true
            lemma12 fb = bool-and-tt (bool-∧→tt-0 eee) (subst ( λ k → accept (automaton B) k t ≡ true ) (equal→refl (afin B) (bool-∧→tt-1 eee) ) fb )
 
-    lemma10 : Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true → split (contain A) (contain B) x ≡ true
+    lemma10 : Naccept NFA (CNFA-exist A B) (equal? finab (case1 (astart A))) x  ≡ true → split (contain A) (contain B) x ≡ true
     lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) lemma15 where 
        lemma15 : (q : states A ∨ states B) → Concat-NFA-start A B q ≡ true → ab-case q (astart A) x
        lemma15 q nq=t with equal→refl finab nq=t 
        ... | refl = refl
 
     closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true
-    closed-in-concat← C with subset-construction-lemma← finab NFA (case1 (astart A)) x C
+    closed-in-concat← C with subset-construction-lemma← (CNFA-exist A B) NFA (equal? finab (case1 (astart A))) x C 
     ... | CC = lemma10 CC
 
 
--- a/automaton-in-agda/src/regular-language.agda	Thu Nov 25 08:48:41 2021 +0900
+++ b/automaton-in-agda/src/regular-language.agda	Thu Nov 25 12:19:36 2021 +0900
@@ -51,15 +51,23 @@
 star-nil A = refl
 
 open Automaton
+open import finiteSet
+open import finiteSetUtil
 
 record RegularLanguage ( Σ : Set ) : Set (Suc Zero) where
    field
-      states : Set 
-      astart : states 
+      states : Set
+      astart : states
+      afin : FiniteSet states
       automaton : Automaton states Σ
    contain : List Σ → Bool
    contain x = accept automaton astart x
 
+open RegularLanguage
+
+isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set
+isRegular A x r = A x ≡ contain r x
+
 RegularLanguage-is-language : { Σ : Set } → RegularLanguage Σ  → language {Σ} 
 RegularLanguage-is-language {Σ} R = RegularLanguage.contain R 
 
@@ -67,9 +75,6 @@
 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 
@@ -79,6 +84,7 @@
 M-Union {Σ} A B = record {
        states =  states A × states B
      ; astart = ( astart A , astart B )
+     ; afin = fin-× (afin A) (afin B)
      ; automaton = record {
              δ = λ q x → ( δ (automaton A) (proj₁ q) x , δ (automaton B) (proj₂ q) x )
            ; aend = λ q → ( aend (automaton A) (proj₁ q) \/ aend (automaton B) (proj₂ q) )
--- a/automaton-in-agda/src/sbconst2.agda	Thu Nov 25 08:48:41 2021 +0900
+++ b/automaton-in-agda/src/sbconst2.agda	Thu Nov 25 12:19:36 2021 +0900
@@ -30,24 +30,24 @@
 test51 = accept test4 start1 ( i0  ∷ i1  ∷ i0  ∷ [] )
 test61 = accept test4 start1 ( i1  ∷ i1  ∷ i1  ∷ [] )
 
-subset-construction-lemma→ : { Q : Set } { Σ : Set  } { n  : ℕ }  → (exists : ( Q → Bool ) → Bool ) →
+subset-construction-lemma→ : { Q : Set } { Σ : Set  } → (exists : ( Q → Bool ) → Bool ) →
     (NFA : NAutomaton Q  Σ ) → (astart : Q → Bool ) 
     → (x : List Σ)
     → Naccept NFA exists astart  x ≡ true
     → accept (  subset-construction exists NFA ) astart  x ≡ true
-subset-construction-lemma→ {Q} {Σ} {n} exists NFA astart x naccept = lemma1 x astart naccept where
+subset-construction-lemma→ {Q} {Σ}  exists NFA astart x naccept = lemma1 x astart naccept where
     lemma1 :  (x : List Σ) → ( states : Q → Bool )
        → Naccept NFA exists states x ≡ true
        → accept (  subset-construction exists NFA ) states x ≡ true
     lemma1 [] states naccept = naccept
     lemma1 (h ∷ t ) states naccept = lemma1 t (δconv exists (Nδ NFA) states h) naccept
 
-subset-construction-lemma← : { Q : Set } { Σ : Set  } { n  : ℕ }  → (exists : ( Q → Bool ) → Bool ) →
+subset-construction-lemma← : { Q : Set } { Σ : Set  }   → (exists : ( Q → Bool ) → Bool ) →
     (NFA : NAutomaton Q  Σ ) → (astart : Q → Bool )
     → (x : List Σ)
     → accept (  subset-construction exists NFA ) astart x ≡ true
     → Naccept NFA exists astart x ≡ true
-subset-construction-lemma← {Q} {Σ} {n} exists NFA astart x saccept = lemma2 x astart saccept where
+subset-construction-lemma← {Q} {Σ}  exists NFA astart x saccept = lemma2 x astart saccept where
     lemma2 :  (x : List Σ) → ( states : Q → Bool )
        → accept (  subset-construction exists NFA ) states x ≡ true
        → Naccept NFA exists states x ≡ true