--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/lang-text.agda	Sun Dec 27 13:26:44 2020 +0900
@@ -0,0 +1,54 @@
+module lang-text where
+
+open import Data.List
+open import Data.String
+open import Data.Char
+open import Data.Char.Unsafe
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary
+open import logic
+
+split : {Σ : Set} → (List Σ → Bool)
+      → ( List Σ → Bool) → List Σ → Bool
+split x y  [] = x [] /\ y []
+split x y (h  ∷ t) = (x [] /\ y (h  ∷ t)) \/
+  split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t
+
+contains : String → String → Bool
+contains x y = contains1 (toList x ) ( toList y ) where
+   contains1 : List Char → List Char → Bool
+   contains1 []  [] = false
+   contains1 [] ( cx ∷ ly ) = false
+   contains1  (cx ∷ lx)  [] = true
+   contains1 (cx ∷ lx ) ( cy ∷ ly ) with cx ≟ cy
+   ... | yes refl = contains1 lx ly
+   ... | no n = false
+
+-- w does not contain the substring ab
+ex15a : Set
+ex15a = (w : String ) → ¬ (contains w "ab"  ≡ true )
+
+-- w does not contains substring baba
+ex15b : Set
+ex15b = (w : String ) → ¬ (contains w "baba"  ≡ true )
+
+-- w contains neither the substing ab nor ba
+ex15c : Set
+
+-- w is any string not in a*b*
+ex15c = (w : String ) → ( ¬ (contains w "ab"  ≡ true )  /\ ( ¬ (contains w "ba"  ≡ true ) 
+
+ex15d : {!!}
+ex15d = {!!}
+
+ex15e : {!!}
+ex15e = {!!}
+
+ex15f : {!!}
+ex15f = {!!}
+
+ex15g : {!!}
+ex15g = {!!}
+
+ex15h : {!!}
+ex15h = {!!}