--- a/agda/regular-language.agda	Thu Oct 31 21:41:54 2019 +0900
+++ b/agda/regular-language.agda	Wed Nov 06 17:18:58 2019 +0900
@@ -44,6 +44,14 @@
 Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
 Star {Σ} A = split A ( Star {Σ} A )
 
+test-split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ (
+       ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/ 
+       ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/ 
+       ( A ( i0 ∷ i1 ∷ [] ) /\ B ( i0 ∷ [] ) ) \/
+       ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) /\ B  []  ) 
+   )
+test-split {_} {A} {B} = refl
+
 open RegularLanguage 
 isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set
 isRegular A x r = A x ≡ contain r x 
@@ -58,6 +66,11 @@
         }
    } 
 
+-- closed-in-union' :  {Σ : Set} → (A B : RegularLanguage Σ )
+--    → ( M : Automaton {!!} Σ ) → ( astart : {!!}  )
+--    → ( x : List Σ ) → (Union (contain A) (contain B) x) ≡ true → accept M astart x ≡ true
+-- closed-in-union' = {!!}
+
 closed-in-union :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B )
 closed-in-union A B [] = lemma where
    lemma : aend (automaton A) (astart A) \/ aend (automaton B) (astart B) ≡