--- a/agda/flcagl.agda	Sun Apr 07 18:22:16 2019 +0900
+++ b/agda/flcagl.agda	Wed Oct 02 13:19:44 2019 +0900
@@ -71,16 +71,16 @@
         δ (k ∪ l) x = δ k x ∪ δ l x
 
 
-        _·'_ : ∀{i}  (k l : Lang i) → Lang i
-        ν (k ·' l) = ν k ∧ ν l
-        δ (k ·' l) x = let k′l =  δ k x  ·' l in if ν k then k′l ∪ δ l x else k′l
+        _·_ : ∀{i}  (k l : Lang i) → Lang i
+        ν (k · l) = ν k ∧ ν l
+        δ (k · l) x = let k′l =  δ k x  · l in if ν k then k′l ∪ δ l x else k′l
 
-        _·_ : ∀{i} (k l : Lang i )  → Lang i
-        ν (k · l) = ν k ∧ ν l
-        δ (_·_ {i} k  l) {j} x =
+        _*_ : ∀{i} (k l : Lang i )  → Lang i
+        ν (k * l) = ν k ∧ ν l
+        δ (_*_ {i} k  l) {j} x =
             let
                 k′l : Lang j
-                k′l  = _·_ {j} (δ k {j} x) l
+                k′l  = _*_ {j} (δ k {j} x) l
             in  if ν k then _∪_ {j}  k′l (δ l {j} x) else k′l 
 
         _* : ∀{i} (l : Lang i) → Lang i
@@ -218,43 +218,27 @@
            ∎
                where open EqR (Bis _)
         ≅δ (concat-union-distribl k {l} {m}) a | true | false = begin
-               (if true ∨ false then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m)
-           ≈⟨ ≅refl ⟩
-               ((δ k a ∪ δ l a) · m ) ∪ δ m a
-           ≈⟨ union-congl (concat-union-distribl _) ⟩
-               (δ k a · m ∪ δ l a · m) ∪ δ m a
-           ≈⟨  union-assoc _ ⟩
-                δ k a · m ∪ ( δ l a · m ∪ δ m a )
-           ≈⟨  union-congr ( union-comm   _ _) ⟩
-                δ k a · m ∪ δ m a ∪ δ l a · m
-           ≈⟨ ≅sym ( union-assoc  _  ) ⟩
-               (δ k a · m ∪ δ m a) ∪ δ l a · m
-           ≈⟨ ≅refl ⟩
+               (if true ∨ false then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m) ≈⟨ ≅refl ⟩
+               ((δ k a ∪ δ l a) · m ) ∪ δ m a ≈⟨ union-congl (concat-union-distribl _) ⟩
+               (δ k a · m ∪ δ l a · m) ∪ δ m a ≈⟨  union-assoc _ ⟩
+                δ k a · m ∪ ( δ l a · m ∪ δ m a ) ≈⟨  union-congr ( union-comm   _ _) ⟩
+                δ k a · m ∪ δ m a ∪ δ l a · m ≈⟨ ≅sym ( union-assoc  _  ) ⟩
+               (δ k a · m ∪ δ m a) ∪ δ l a · m ≈⟨ ≅refl ⟩
                ((if true then δ k a · m ∪ δ m a else δ k a · m) ∪ (if false then δ l a · m ∪ δ m a else δ l a · m))
            ∎
                where open EqR (Bis _)
         ≅δ (concat-union-distribl k {l} {m}) a | true | true = begin
-                (if true ∨ true then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m)
-           ≈⟨ ≅refl ⟩
-                (δ k a ∪ δ l a) · m ∪ δ m a
-           ≈⟨ union-congl ( concat-union-distribl _ ) ⟩
-               (δ k a · m ∪ δ l a · m) ∪ δ m a
-           ≈⟨  union-assoc _ ⟩
-               δ k a · m ∪ ( δ l a · m ∪ δ m a )
-           ≈⟨ ≅sym ( union-congr ( union-congr (  union-idem _ ) ) ) ⟩
-               δ k a · m ∪ ( δ l a · m ∪ (δ m a  ∪ δ m a) )
-           ≈⟨  ≅sym ( union-congr ( union-assoc _ )) ⟩
-               δ k a · m ∪ ( (δ l a · m ∪ δ m a  ) ∪ δ m a )
-           ≈⟨   union-congr (  union-congl  ( union-comm _  _) )   ⟩
-               δ k a · m ∪ ( (δ m a  ∪ δ l a · m ) ∪ δ m a )
-           ≈⟨  ≅sym ( union-assoc  _  ) ⟩
-               ( δ k a · m ∪  (δ m a  ∪ δ l a · m )) ∪ δ m a 
-           ≈⟨  ≅sym ( union-congl ( union-assoc _  ) ) ⟩
-               ((δ k a · m ∪ δ m a) ∪ δ l a · m) ∪ δ m a
-           ≈⟨  union-assoc _  ⟩
-                (δ k a · m ∪ δ m a) ∪ δ l a · m ∪ δ m a
-           ≈⟨ ≅refl ⟩
-                ((if true then δ k a · m ∪ δ m a else δ k a · m) ∪ (if true then δ l a · m ∪ δ m a else δ l a · m))
+               (if true ∨ true then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m) ≈⟨ ≅refl ⟩
+               (δ k a ∪ δ l a) · m ∪ δ m a ≈⟨ union-congl ( concat-union-distribl _ ) ⟩
+               (δ k a · m ∪ δ l a · m) ∪ δ m a ≈⟨  union-assoc _ ⟩
+                δ k a · m ∪ ( δ l a · m ∪ δ m a ) ≈⟨ ≅sym ( union-congr ( union-congr (  union-idem _ ) ) ) ⟩
+                δ k a · m ∪ ( δ l a · m ∪ (δ m a  ∪ δ m a) ) ≈⟨  ≅sym ( union-congr ( union-assoc _ )) ⟩
+                δ k a · m ∪ ( (δ l a · m ∪ δ m a  ) ∪ δ m a ) ≈⟨   union-congr (  union-congl  ( union-comm _  _) )   ⟩
+                δ k a · m ∪ ( (δ m a  ∪ δ l a · m ) ∪ δ m a ) ≈⟨  ≅sym ( union-assoc  _  ) ⟩
+               ( δ k a · m ∪  (δ m a  ∪ δ l a · m )) ∪ δ m a ≈⟨  ≅sym ( union-congl ( union-assoc _  ) ) ⟩
+               ((δ k a · m ∪ δ m a) ∪ δ l a · m) ∪ δ m a ≈⟨  union-assoc _  ⟩
+               (δ k a · m ∪ δ m a) ∪ δ l a · m ∪ δ m a ≈⟨ ≅refl ⟩
+               ((if true then δ k a · m ∪ δ m a else δ k a · m) ∪ (if true then δ l a · m ∪ δ m a else δ l a · m))
            ∎
                where open EqR (Bis _)
 
@@ -310,14 +294,10 @@
         star-concat-idem : ∀{i} (l : Lang ∞) → l * · l * ≅⟨ i ⟩≅ l *
         ≅ν (star-concat-idem l) = refl
         ≅δ (star-concat-idem l) a = begin
-               δ ((l *) · (l *)) a
-           ≈⟨ union-congl (concat-assoc _) ⟩
-               δ l a · (l * · l *) ∪ δ l a · l *
-           ≈⟨ union-congl (concat-congr (star-concat-idem _)) ⟩
-               δ l a · l * ∪ δ l a · l *
-           ≈⟨ union-idem _ ⟩
-               δ (l *) a
-           ∎ where open EqR (Bis _)
+               δ ((l *) · (l *)) a ≈⟨ union-congl (concat-assoc _) ⟩
+               δ l a · (l * · l *) ∪ δ l a · l * ≈⟨ union-congl (concat-congr (star-concat-idem _)) ⟩
+               δ l a · l * ∪ δ l a · l * ≈⟨ union-idem _ ⟩
+               δ (l *) a ∎ where open EqR (Bis _)
 
         star-idem : ∀{i} (l : Lang ∞) → (l *) * ≅⟨ i ⟩≅ l *
         ≅ν (star-idem l) = refl
@@ -477,3 +457,21 @@
  starA-correct : ∀{i S} (da : DA S) (s0 : S) →
    lang (starA s0 da) (nothing ∷ []) ≅⟨ i ⟩≅ (lang da s0) *
 
+record NAutomaton ( Q : Set ) ( Σ : Set  )
+           : Set  where
+        field
+              Nδ : Q → Σ → Q → Bool
+              Nstart : Q → Bool
+              Nend  :  Q → Bool
+
+postulate
+   exists : { S : Set} → ( S → Bool ) → Bool
+
+nlang : ∀{i} {S} (nfa : NAutomaton S A ) (s : S → Bool ) → Lang i
+Lang.ν (nlang nfa s) = exists ( λ x → (s x ∧ NAutomaton.Nend nfa x ))
+Lang.δ (nlang nfa s) a = nlang nfa (λ x → s x ∧ (NAutomaton.Nδ nfa x a) x) 
+
+-- nlang' : ∀{i} {S} (nfa : DA (S → Bool) ) (s : S → Bool ) → Lang i
+-- Lang.ν (nlang' nfa s) = DA.ν nfa  s
+-- Lang.δ (nlang' nfa s) a = nlang' nfa (DA.δ nfa s a)
+