--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/nfa.agda	Thu Nov 12 11:45:34 2020 +0900
@@ -0,0 +1,109 @@
+module nfa where
+open import Level renaming ( suc to Suc ; zero to Zero )
+
+open import Relation.Binary.PropositionalEquality 
+open import Data.List
+open import automaton
+open import logic
+
+record NAutomaton {n : Level} ( Q : Set n ) ( Σ : Set  )
+       : Set (Suc n) where
+    field
+          Nδ : Q → Σ → Q → Set
+          NF  :  Q → Set
+          Nexists  : (Q → Set)  → Set
+
+open NAutomaton
+
+naccept : {n : Level} {Q : Set n} {Σ : Set} → NAutomaton Q Σ → (Q → Set) → List Σ → Set
+naccept {n} {Q} {Σ} nfa qs [] = Nexists nfa (λ q → qs q ∧ NF nfa q )
+naccept {n} {Q} {Σ} nfa qs (x ∷ input) = 
+    Nexists nfa (λ q → qs q ∧ (naccept nfa (Nδ nfa q x) input ))
+
+ntrace : {n  : Level} {Q : Set n} {Σ : Set } → (NFA : NAutomaton Q Σ) → (start : Q → Set ) → (input : List Σ ) → naccept NFA start input
+     → ((Q → Set) → List Q)
+     → List (List Q)
+ntrace {n} {Q} {Σ} A q [] a list = list q ∷ []
+ntrace {n} {Q} {Σ} A q (x ∷ t) a list = list q ∷ ( ntrace A {!!} t {!!} list )
+
+data transition136 : Q3  → Σ2  → Q3 → Set  where
+    d0 : transition136 q₁ s1 q₂ 
+    d1 : transition136 q₁ s0 q₁ 
+    d2 : transition136 q₂ s0 q₂ 
+    d3 : transition136 q₂ s0 q₃ 
+    d4 : transition136 q₂ s1 q₃ 
+    d5 : transition136 q₃ s0 q₁ 
+
+start136 : Q3 → Set
+start136 q = q ≡ q₁
+
+nfa136 :  NAutomaton Q3 Σ2 
+nfa136 =  record { Nδ = transition136 ; NF = λ q → q ≡ q₁ ; Nexists = exists-in-Q3 }
+
+example136-1 = naccept nfa136 start136 ( s0  ∷ s1  ∷ s0 ∷ s0 ∷ [] )
+
+example136-0 = naccept nfa136 start136 ( s0 ∷ [] )
+
+example136-2 = naccept nfa136 start136 ( s1  ∷ s0  ∷ s1 ∷ s0 ∷ s1 ∷ [] )
+
+--
+-- ((Q → Set)  → Set) → ((Q → Set) → Set) → Set
+--
+
+data Nexists→exits  {n : Level} { Q : Set n }  {Σ : Set} ( NFA : NAutomaton Q  Σ ) : ((Q → Set) → Set) → Set where
+   one-of : Nexists→exits NFA  (Nexists NFA)
+
+subset-construction : {n : Level} { Q : Set n } { Σ : Set  }   → 
+    (NAutomaton Q  Σ ) → Automaton {Suc Zero ⊔ n} (Q → Set) Σ 
+subset-construction {n} {Q} { Σ}  NFA = record {
+        δ = λ qs x qs → Nexists NFA (λ q → Nδ NFA q x qs )
+     ;  F = λ qs → Nexists NFA ( λ q → NF NFA q )
+     ;  exists = Nexists→exits NFA   -- what this means?
+   } 
+
+subset-construction-lemma→ : { Q : Set } { Σ : Set  }   →   
+    (NFA : NAutomaton Q  Σ ) → (astart : Q → Set )
+    → (x : List Σ)
+    → naccept NFA ( λ q1 → astart q1) x 
+    → accept (  subset-construction NFA ) ( λ q1 → astart q1) x 
+subset-construction-lemma→ = {!!}
+
+subset-construction-lemma← : { Q : Set } { Σ : Set  }   → 
+    (NFA : NAutomaton Q  Σ ) → (astart : Q → Set )
+    → (x : List Σ)
+    → accept (  subset-construction NFA ) ( λ q1 → astart q1) x 
+    → naccept NFA ( λ q1 →  astart q1) x 
+subset-construction-lemma← = {!!}
+
+open import regular-language 
+
+open RegularLanguage
+open Automaton
+open import Data.Empty 
+
+Concat-exists : {n : Level}  {Σ : Set} → (A B : RegularLanguage {n} Σ ) →  (states A ∨ states B → Set) → Set
+Concat-exists {n} {Σ} A B P = exists (automaton A) (λ q → P (case1 q)) ∨ exists (automaton B) (λ q → P (case2 q))
+
+Concat-NFA : {n : Level}  {Σ : Set} → (A B : RegularLanguage {n} Σ ) → NAutomaton (states A ∨ states B) Σ 
+Concat-NFA {n} {Σ} A B = record { Nδ = δnfa ; NF = nend  ; Nexists = Concat-exists A B } 
+   module Concat-NFA where
+       data δnfa : states A ∨ states B → Σ → states A ∨ states B → Set where
+         a-case   : {q : states A}  {i : Σ } → δnfa ( case1 q) i (case1 (δ (automaton A) q i))
+         ab-trans : {q : states A}  {i : Σ } → F (automaton A) q  → δnfa ( case1 q) i (case2 (δ (automaton B) (astart B) i))
+         b-case   : {q : states B}  {i : Σ } → δnfa ( case2 q) i (case2 (δ (automaton B) q i))
+       nend : states A ∨ states B → Set
+       nend (case2 q) = F (automaton B) q
+       nend (case1 q) = F (automaton A) q ∧ F (automaton B) (astart B) -- empty B case
+
+data state-is {n : Level} {Σ : Set }  (A : RegularLanguage {n} Σ ) : (a : states A ) → Set where
+   this : (a : states A)  → state-is A a
+
+closed-in-concat :  {n : Level} {Σ : Set } → (A B : RegularLanguage {n}  Σ ) → ( x : List Σ ) 
+   → isRegular (Concat {n} (contain A) (contain B)) x record {states = states A ∨ states B → Set ; astart = λ q → state-is A (astart A)
+         ; automaton = subset-construction ( Concat-NFA A B )}
+closed-in-concat {Σ} A B x = {!!}
+
+
+
+
+