--- a/automaton-in-agda/src/regular-language.agda	Thu Nov 16 17:40:42 2023 +0900
+++ b/automaton-in-agda/src/regular-language.agda	Wed Nov 22 17:07:01 2023 +0900
@@ -42,7 +42,7 @@
 --
 repeat : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool 
 repeat2 : {Σ : Set} → (x : List Σ → Bool) → (pre y : List Σ ) → Bool
-repeat2 x pre [] = false
+repeat2 x pre [] = true
 repeat2 x pre (h ∷ y) = 
    (x (pre ++ (h ∷ [])) /\ repeat x y )
    \/ repeat2 x (pre ++ (h ∷ [])) y 
@@ -211,3 +211,37 @@
 split→AB1 {Σ} A B x S = subst (λ k → split A B k ≡ true ) (sp-concat S) ( AB→split A B _ _ (prop0 S) (prop1 S)  )
   
 
+-- low of exclude middle of Split A B x
+lemma-concat : {Σ : Set} → ( A B : language {Σ} ) → (x : List Σ) → Split A B x ∨ ( ¬ Split A B x )
+lemma-concat {Σ} A B x with split A B x in eq
+... | true = case1 (split→AB A B x eq )
+... | false = case2 (λ p →  ¬-bool eq (split→AB1 A B x p )) 
+
+-- Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
+-- Concat {Σ} A B = split A B
+
+Concat' : {Σ : Set} → ( A B : language {Σ} ) → (x : List Σ) → Set
+Concat' {Σ} A B = λ x → Split A B x
+
+record StarProp {Σ : Set} (A : List Σ → Bool ) (x :  List Σ ) : Set where
+    field
+        spn : List ( List Σ )
+        spn-concat : foldr (λ k → k ++_ ) [] spn ≡ x
+        propn : foldr (λ k → λ j → A k /\ j ) true spn ≡ true
+
+open StarProp
+
+Star→StarProp : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → Star A x ≡ true → StarProp A x
+Star→StarProp = ?
+
+StarProp→Star : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → StarProp A x → Star A x ≡ true
+StarProp→Star {Σ} A x sp = subst (λ k →  Star A k ≡ true ) (spsx (spn sp) refl) ( sps1 (spn sp) refl ) where
+     spsx : (y : List ( List Σ ) ) → spn sp ≡ y → foldr (λ k → k ++_ ) [] y ≡ x
+     spsx y refl = spn-concat sp 
+     sps1 : (y : List ( List Σ ) ) → spn sp ≡ y → Star A (foldr (λ k → k ++_ ) [] y) ≡ true
+     sps1 = ?
+
+
+lemma-starprop : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → StarProp A x ∨ ( ¬ StarProp A x )
+lemma-starprop = ?
+