# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1576658055 -32400
# Node ID 7a0634a7c25a47505f05e0d8072b97ae48fd3819
# Parent  08e2af685c69fb904abcedaf0065c4fcd884eebc
...

diff -r 08e2af685c69 -r 7a0634a7c25a a02/agda-install.ind
--- a/a02/agda-install.ind	Sun Nov 24 19:13:44 2019 +0900
+++ b/a02/agda-install.ind	Wed Dec 18 17:34:15 2019 +0900
@@ -45,7 +45,7 @@
 
 Emacs から使うので、Emacs も勉強しよう。
 
-<a href="http://www.ie.u-ryukyu.ac.jp/%7Ekono/howto/mule.html"> Emacs の使い方 </a>
+<a href="http://ie.u-ryukyu.ac.jp/%7Ekono/howto/mule.html"> Emacs の使い方 </a>
 
   C-C  control と C を同時に押す
   M-X  esc を押してから X を押す
diff -r 08e2af685c69 -r 7a0634a7c25a a02/agda/dag.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a02/agda/dag.agda	Wed Dec 18 17:34:15 2019 +0900
@@ -0,0 +1,75 @@
+module dag where
+
+--         f0
+--       -----→
+--    t0         t1
+--       -----→
+--         f1
+
+
+data  TwoObject   : Set  where
+       t0 : TwoObject
+       t1 : TwoObject
+
+
+data TwoArrow  : TwoObject → TwoObject → Set  where
+       f0 :  TwoArrow t0 t1
+       f1 :  TwoArrow t0 t1
+
+
+--         r0
+--       -----→
+--    t0         t1
+--       ←-----
+--         r1
+
+data Circle  : TwoObject → TwoObject → Set  where
+       r0 :  Circle t0 t1
+       r1 :  Circle t1 t0
+
+data ⊥ : Set where
+
+⊥-elim : {A : Set } -> ⊥ -> A
+⊥-elim ()
+
+¬_ : Set → Set
+¬ A = A → ⊥
+
+data Bool  : Set  where
+       true :  Bool
+       false :  Bool
+
+data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set  where
+    direct :   E x y -> connected E x y 
+    indirect :  { z : V  } -> E x z  ->  connected {V} E z y -> connected E x y
+
+lemma1 : connected TwoArrow t0 t1
+lemma1 =  ?
+
+lemma2 : ¬ ( connected TwoArrow t1 t0 )
+lemma2 x = ?
+
+-- lemma2 (direct ())
+-- lemma2 (indirect () (direct _))
+-- lemma2 (indirect () (indirect _ _ ))
+
+lemma3 : connected Circle t0 t0
+lemma3 = indirect r0 ( direct r1 )
+
+data Dec (P : Set) : Set where
+   yes :   P → Dec P
+   no  : ¬ P → Dec P
+
+reachable :  { V : Set } ( E : V -> V -> Set ) ( x y : V ) -> Set
+reachable {V} E x y = Dec ( connected {V} E x y )
+
+dag :  { V : Set } ( E : V -> V -> Set ) ->  Set
+dag {V} E =  ∀ (n : V)  →  ¬ ( connected E n n )
+
+lemma4 : dag TwoArrow
+lemma4 x = ?
+
+lemma5 :  ¬ ( dag Circle )
+lemma5 x = ⊥-elim ?
+
+
diff -r 08e2af685c69 -r 7a0634a7c25a a02/agda/data1.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a02/agda/data1.agda	Wed Dec 18 17:34:15 2019 +0900
@@ -0,0 +1,62 @@
+module data1 where
+
+data _∨_ (A B : Set) : Set where
+  p1 : A → A ∨ B
+  p2 : B → A ∨ B
+
+ex1 : {A B : Set} → A → ( A ∨ B ) 
+ex1 = ?
+
+ex2 : {A B : Set} → B → ( A ∨ B ) 
+ex2 = ?
+
+ex3 : {A B : Set} → ( A ∨ A ) → A 
+ex3 = ?
+
+ex4 : {A B C : Set} →  A ∨ ( B ∨ C ) → ( A ∨  B ) ∨ C 
+ex4 = ?
+
+record _∧_ A B : Set where
+  field
+     π1 : A
+     π2 : B
+
+open _∧_
+
+--- ex5 :  {A B C : Set} →  (( A → C ) ∨ ( B  → C ) ) → ( ( A ∨  B ) → C ) is wrong
+ex5 :  {A B C : Set} →  (( A → C ) ∨ ( B  → C ) ) → ( ( A ∧  B ) → C )
+ex5 = {!!}
+
+data Three : Set where
+  t1 : Three
+  t2 : Three
+  t3 : Three
+
+open Three
+
+infixl 110 _∨_ 
+
+
+data 3Ring : (dom cod : Three) → Set where
+   r1 : 3Ring t1 t2
+   r2 : 3Ring t2 t3
+   r3 : 3Ring t3 t1
+
+data Nat : Set where
+  zero : Nat
+  suc  : Nat →  Nat
+
+add : ( a b : Nat ) → Nat
+add zero x = x
+add (suc x) y = suc ( add x y )
+
+mul : ( a b : Nat ) → Nat
+mul zero x = {!!}
+mul (suc x) y = {!!}
+
+ex6 : Nat
+ex6 = mul ( suc ( suc zero)) (suc ( suc ( suc zero)) )
+
+
+
+
diff -r 08e2af685c69 -r 7a0634a7c25a a02/agda/equality.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a02/agda/equality.agda	Wed Dec 18 17:34:15 2019 +0900
@@ -0,0 +1,20 @@
+module equality where
+
+
+data _==_ {A : Set } : A → A → Set where
+   refl :  {x : A} → x == x
+
+ex1 : {A : Set} {x : A } → x == x
+ex1  = {!!}
+
+ex2 : {A : Set} {x y : A } → x == y → y == x
+ex2 = {!!}
+
+ex3 : {A : Set} {x y z : A } → x == y → y == z → x == z
+ex3 = {!!}
+
+ex4 : {A B : Set} {x y : A } { f : A → B } →   x == y → f x == f y
+ex4 = {!!}
+
+
+
diff -r 08e2af685c69 -r 7a0634a7c25a a02/agda/lambda.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a02/agda/lambda.agda	Wed Dec 18 17:34:15 2019 +0900
@@ -0,0 +1,56 @@
+module lambda ( T : Set) ( t : T ) where
+
+
+A→A : (A : Set ) → ( A → A )
+A→A = λ A → λ ( a : A ) → a
+
+lemma2 : (A : Set ) →  A → A 
+lemma2 A a = {!!}
+
+
+ex1 : {A B : Set} → Set 
+ex1 {A} {B} = ( A → B ) → A → B
+
+ex1' : {A B : Set} → Set 
+ex1' {A} {B} =  A → B  → A → B
+
+ex2 : {A : Set} → Set 
+ex2 {A}  =  A → ( A  → A )
+
+ex3 : {A B : Set} → Set 
+ex3 {A}{B}  =  A → B
+
+ex4 : {A B : Set} → Set 
+ex4 {A}{B}  =  A → B → B
+
+ex5 : {A B : Set} → Set 
+ex5 {A}{B}  =  A → B → A
+
+proof5 : {A B : Set } → ex5 {A} {B}
+proof5 = {!!}
+
+
+postulate S : Set
+postulate s : S
+
+ex6 : {A : Set} → A → S
+ex6 a = {!!}
+
+ex7 : {A : Set} → A → T
+ex7 a = {!!}
+
+ex11 : (A B : Set) → ( A → B ) → A → B
+ex11 = {!!}
+
+ex12 : (A B : Set) → ( A → B ) → A → B
+ex12 = {!!}
+
+ex13 : {A B : Set} → ( A → B ) → A → B
+ex13 {A} {B} = {!!}
+
+ex14 : {A B : Set} → ( A → B ) → A → B
+ex14 x = {!!}
+
+proof5' : {A B : Set} → ex5 {A} {B}
+proof5' = {!!}
+
diff -r 08e2af685c69 -r 7a0634a7c25a a02/agda/level1.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a02/agda/level1.agda	Wed Dec 18 17:34:15 2019 +0900
@@ -0,0 +1,22 @@
+module level1 where
+
+open import Level
+
+ex1 : { A B : Set} → Set
+ex1 {A} {B} =  A → B
+
+ex2 : { A B : Set} →  ( A → B ) → Set
+ex2 {A} {B}  A→B  =  ex1 {A} {B}
+
+
+-- record FuncBad (A B : Set) : Set where
+--   field
+--      func : A → B → Set
+
+record Func {n : Level} (A B : Set n ) : Set (suc n) where
+  field
+    func :  A → B  → Set n
+
+record Func2 {n : Level} (A B : Set n ) : Set {!!} where
+  field
+    func : A → B  → Func A B
diff -r 08e2af685c69 -r 7a0634a7c25a a02/agda/list.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a02/agda/list.agda	Wed Dec 18 17:34:15 2019 +0900
@@ -0,0 +1,76 @@
+module list where
+                                                                        
+postulate A : Set
+
+postulate a : A
+postulate b : A
+postulate c : A
+
+
+infixr 40 _::_
+data  List  (A : Set ) : Set  where
+   [] : List A
+   _::_ : A → List A → List A
+
+
+infixl 30 _++_
+_++_ :   {A : Set } → List A → List A → List A
+[]        ++ ys = ys
+(x :: xs) ++ ys = x :: (xs ++ ys)
+
+l1 = a :: []
+l2 = a :: b :: a :: c ::  []
+
+l3 = l1 ++ l2
+
+data Node  ( A : Set  ) : Set  where
+   leaf  : A → Node A
+   node  : Node A → Node A → Node A
+
+flatten :  { A : Set } → Node A → List A
+flatten ( leaf a )   = a :: []
+flatten ( node a b ) = flatten a ++ flatten b
+
+n1 = node ( leaf a ) ( node ( leaf b ) ( leaf c ))
+
+open  import  Relation.Binary.PropositionalEquality
+
+++-assoc :  (L : Set ) ( xs ys zs : List L ) → (xs ++ ys) ++ zs  ≡ xs ++ (ys ++ zs)
+++-assoc A [] ys zs = let open ≡-Reasoning in
+  begin -- to prove ([] ++ ys) ++ zs  ≡ [] ++ (ys ++ zs)
+   ( [] ++ ys ) ++ zs
+  ≡⟨ refl ⟩
+    ys ++ zs
+  ≡⟨⟩
+    [] ++ ( ys ++ zs )
+  ∎
+  
+++-assoc A (x :: xs) ys zs = let open  ≡-Reasoning in
+  begin -- to prove ((x :: xs) ++ ys) ++ zs == (x :: xs) ++ (ys ++ zs)
+    ((x :: xs) ++ ys) ++ zs
+  ≡⟨ refl ⟩
+     (x :: (xs ++ ys)) ++ zs
+  ≡⟨ refl ⟩
+    x :: ((xs ++ ys) ++ zs)
+  ≡⟨ cong (_::_ x) (++-assoc A xs ys zs) ⟩ 
+    x :: (xs ++ (ys ++ zs))
+  ≡⟨ refl ⟩
+    (x :: xs) ++ (ys ++ zs)
+  ∎
+
+open import Data.Nat
+
+length : {L : Set} → List L →  ℕ
+length [] = zero
+length (_ :: T ) = suc ( length T )
+
+lemma : {L : Set} → (x y : List L ) → ( length x + length y ) ≡ length ( x ++ y )
+lemma [] [] = refl
+lemma [] (_ :: _) = refl
+lemma (H :: T) L =  let open  ≡-Reasoning in
+  begin 
+     ?
+  ≡⟨ ? ⟩
+     ?
+  ∎
+
diff -r 08e2af685c69 -r 7a0634a7c25a a02/agda/record1.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a02/agda/record1.agda	Wed Dec 18 17:34:15 2019 +0900
@@ -0,0 +1,27 @@
+module record1 where
+
+record _∧_ (A B : Set) : Set where
+  field
+     π1 : A
+     π2 : B
+
+open _∧_
+
+ex1 : {A B : Set} → ( A ∧ B ) → A 
+ex1 a∧b = {!!}
+
+ex2 : {A B : Set} → ( A ∧ B ) → B 
+ex2 a∧b = {!!}
+
+ex3 : {A B : Set} → A → B → ( A ∧ B ) 
+ex3 a b = {!!}
+
+ex4 : {A B : Set} → A → ( A ∧ A ) 
+ex4 a  = record { π1 = {!!} ;  π2 = {!!} }
+
+ex5 : {A B C : Set} → ( A ∧ B ) ∧ C  →  A ∧ (B ∧ C) 
+ex5 a∧b∧c = record { π1 = {!!} ; π2 = {!!} }
+
+ex6 : {A B C : Set} → ( (A → B ) ∧ ( B →  C) )  → A → C
+ex6  =  {!!}
+
diff -r 08e2af685c69 -r 7a0634a7c25a agda/cfg1.agda
--- a/agda/cfg1.agda	Sun Nov 24 19:13:44 2019 +0900
+++ b/agda/cfg1.agda	Wed Dec 18 17:34:15 2019 +0900
@@ -136,3 +136,42 @@
 cfgtest8 = cfg-language IFGrammer  (IF ∷ EA ∷ THEN  ∷ IF ∷ EB ∷ THEN  ∷ SA ∷ ELSE  ∷ SB  ∷ [] ) 
 cfgtest9 = cfg-language IFGrammer  (IF ∷ EB ∷ THEN ∷ SA ∷ ELSE  ∷ SB  ∷ [] ) 
 
+data E1Token : Set where
+   e1 : E1Token
+   e[ : E1Token
+   e] : E1Token
+   expr : E1Token
+   term : E1Token
+
+E1-token-eq? : E1Token → E1Token → Bool
+E1-token-eq? e1 e1 = true
+E1-token-eq? e[ e] = true
+E1-token-eq? e] e] = true
+E1-token-eq? expr expr = true
+E1-token-eq? term term = true
+E1-token-eq? _ _ = false
+
+typeof-E1 : E1Token → Node E1Token
+typeof-E1 expr = N expr
+typeof-E1 term = N term
+typeof-E1 x = T x
+
+E1Grammer : CFGGrammer E1Token
+E1Grammer = record {
+      cfg = cfgE
+    ; top = expr
+    ; eq? = E1-token-eq?
+    ; typeof = typeof-E1
+   } where
+     cfgE : E1Token → Body E1Token
+     cfgE expr = term ．
+       ；
+     cfgE term = e1  ．
+       ｜   e[   ， expr  ，  e]   ．
+       ；
+     cfgE x = Error  ；
+
+ecfgtest1 = cfg-language E1Grammer (  e1 ∷ [] )
+ecfgtest2 = cfg-language E1Grammer (  e[ ∷ e1 ∷ e] ∷ [] )
+ecfgtest3 = cfg-language E1Grammer (  e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ [] )
+
diff -r 08e2af685c69 -r 7a0634a7c25a agda/derive.agda
--- a/agda/derive.agda	Sun Nov 24 19:13:44 2019 +0900
+++ b/agda/derive.agda	Wed Dec 18 17:34:15 2019 +0900
@@ -1,54 +1,37 @@
 module derive where
 
 open import nfa
-open import regex1
 open import Data.Nat hiding ( _<_ ; _>_ )
 open import Data.Fin hiding ( _<_ )
 open import Data.List hiding ( [_] )
+open import Data.Maybe 
 
 open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
 open import Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 
 open import finiteSet
+open import automaton
 
-finIn2 : FiniteSet In2
-finIn2 = record {
-        Q←F = Q←F'
-      ; F←Q  = F←Q'
-      ; finiso→ = finiso→'
-      ; finiso← = finiso←'
-   } where
-       Q←F' : Fin 2 → In2
-       Q←F' zero = i0
-       Q←F' (suc zero) = i1
-       Q←F' (suc (suc ())) 
-       F←Q' : In2 → Fin 2
-       F←Q' i0 = zero
-       F←Q' i1 = suc (zero)
-       finiso→' : (q : In2) → Q←F' (F←Q' q) ≡ q
-       finiso→' i0 = refl
-       finiso→' i1 = refl
-       finiso←' : (f : Fin 2) → F←Q' (Q←F' f) ≡ f
-       finiso←' zero = refl
-       finiso←' (suc zero) = refl
-       finiso←' (suc (suc ()))
+data Regex   ( Σ : Set  ) : Set  where
+   _*    : Regex  Σ → Regex  Σ
+   _&_   : Regex  Σ → Regex  Σ → Regex Σ
+   _||_  : Regex  Σ → Regex  Σ → Regex Σ
+   <_>   : Σ → Regex  Σ
+
+derivation : { Σ : Set } → Regex Σ → Regex Σ → Bool
+derivation = {!!}
 
-
-tr1 = < i0 > & < i1 >
-tr2 = regular-language (< i0 > & < i1 >) finIn2 ( i0  ∷ i1  ∷ [] )
-tr3 = regular-language (< i0 > & < i1 >) finIn2 ( i0  ∷ i0  ∷ [] )
-tr4 = (< i0 > * ) & < i1 >
-tr5 = ( ((< i0 > * ) & < i1 > ) || ( < i1 > & ( ( < i1 > * ) || ( < i0 > * )) ) ) *
-
-sb : { Σ : Set } → Regex Σ → List ( Regex Σ )
-sb (x *) =  map (λ r → ( r & (x *) )) ( sb x ) ++ ( sb x ) 
-sb (x & y) = map (λ r → ( r & y )) ( sb x ) ++ ( sb y ) 
-sb (x || y) = sb x ++ sb y 
-sb < x > = < x >  ∷ []
-
-
-nth : { S : Set } → (x : List S ) → Fin ( length x ) → S
-nth [] ()
-nth (s ∷ t) zero = s
-nth (_ ∷ t) (suc f) = nth t f
+derivation-step : { Σ : Set } → Regex Σ → Σ → Maybe (Regex Σ)
+derivation-step {Σ} (r *) s with derivation-step r s
+... | just ex = just ( ex & (r *) )
+... | nothing = nothing
+derivation-step {Σ} (r & r₁) s with derivation-step r s 
+... | just ex = just ( ex & r₁  )
+... | nothing = nothing
+derivation-step {Σ} (r || r₁) s with derivation-step r s  | derivation-step r₁ s
+... | just e  | just e1 = just ( e || e1 )
+... | nothing | just e1 = just e1
+... | just e  | nothing = just e
+... | nothing | nothing = nothing
+derivation-step {Σ} < x > s = {!!}
diff -r 08e2af685c69 -r 7a0634a7c25a agda/finiteSet.agda
--- a/agda/finiteSet.agda	Sun Nov 24 19:13:44 2019 +0900
+++ b/agda/finiteSet.agda	Wed Dec 18 17:34:15 2019 +0900
@@ -249,6 +249,7 @@
       lemma : (FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj₁ x)) , proj₂ x) ≡ ( proj₁ x , proj₂ x )
       lemma = cong ( λ k → ( k ,  proj₂ x ) )  (FiniteSet.finiso← fa _ )
    ISO.iso→ iso-1 x = cong ( λ k → ( k ,  proj₂ x ) )  (FiniteSet.finiso→ fa _ )
+
    iso-2 : {a : ℕ } → ISO (B ∨ (Fin a × B)) (Fin (suc a) × B)
    ISO.A←B iso-2 (zero , b ) = case1 b
    ISO.A←B iso-2 (suc fst , b ) = case2 ( fst , b )
@@ -258,6 +259,7 @@
    ISO.iso← iso-2 (case2 x) = refl
    ISO.iso→ iso-2 (zero , b ) = refl
    ISO.iso→ iso-2 (suc a , b ) = refl
+
    fin-×-f : ( a  : ℕ ) → FiniteSet ((Fin a) × B) {a * b}
    fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () }
    fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2
@@ -265,7 +267,7 @@
 open _∧_
 
 fin-∧ : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A ∧ B) {a * b}
-fin-∧ {A} {B} {a} {b} fa fb with FiniteSet→Fin fa
+fin-∧ {A} {B} {a} {b} fa fb with FiniteSet→Fin fa    -- same thing for our tool
 ... | a=f = iso-fin (fin-×-f a ) iso-1 where
    iso-1 : ISO (Fin a ∧ B) ( A ∧ B )
    ISO.A←B iso-1 x = record { proj1 = FiniteSet.F←Q fa (proj1 x)  ; proj2 =  proj2 x} 
@@ -274,6 +276,7 @@
       lemma : record { proj1 = FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj1 x)) ; proj2 =  proj2 x} ≡ record {proj1 =  proj1 x ; proj2 =  proj2 x }
       lemma = cong ( λ k → record {proj1 = k ;  proj2 = proj2 x } )  (FiniteSet.finiso← fa _ )
    ISO.iso→ iso-1 x = cong ( λ k → record {proj1 =  k ; proj2 =  proj2 x } )  (FiniteSet.finiso→ fa _ )
+
    iso-2 : {a : ℕ } → ISO (B ∨ (Fin a ∧ B)) (Fin (suc a) ∧ B)
    ISO.A←B iso-2 (record { proj1 = zero ; proj2 =  b }) = case1 b
    ISO.A←B iso-2 (record { proj1 = suc fst ; proj2 =  b }) = case2 ( record { proj1 = fst ; proj2 =  b } )
@@ -283,6 +286,7 @@
    ISO.iso← iso-2 (case2 x) = refl
    ISO.iso→ iso-2 (record { proj1 = zero ; proj2 =  b }) = refl
    ISO.iso→ iso-2 (record { proj1 = suc a ; proj2 =  b }) = refl
+
    fin-×-f : ( a  : ℕ ) → FiniteSet ((Fin a) ∧ B) {a * b}
    fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () }
    fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2
@@ -405,8 +409,7 @@
     l2f :  (n : ℕ ) → (n<m : n < suc m ) → (q<n : toℕ (FiniteSet.F←Q fin q ) < n )  →  (L2F n<m fin (F2L n<m  fin (λ q _ → f q))) q q<n ≡ f q
     l2f zero (s≤s z≤n) ()
     l2f (suc n) (s≤s n<m) (s≤s n<q) with FiniteSet.F←Q fin q ≟ fromℕ≤ n<m 
-    l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p with inspect f q
-    l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p | record { eq = refl } = begin 
+    l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p = begin 
              f (FiniteSet.Q←F fin (fromℕ≤ n<m)) 
           ≡⟨ cong ( λ k → f (FiniteSet.Q←F fin k )) (sym p)  ⟩
              f (FiniteSet.Q←F fin ( FiniteSet.F←Q fin q ))
diff -r 08e2af685c69 -r 7a0634a7c25a agda/induction-ex.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/induction-ex.agda	Wed Dec 18 17:34:15 2019 +0900
@@ -0,0 +1,118 @@
+{-# OPTIONS --guardedness #-}
+module induction-ex where
+
+open import Relation.Binary.PropositionalEquality
+open import Size
+open import Data.Bool
+
+data List (A : Set ) : Set where
+    [] : List A
+    _∷_ : A → List A → List A
+
+data Nat : Set where
+     zero : Nat
+     suc  : Nat → Nat
+
+add : Nat → Nat → Nat
+add zero x = x
+add (suc x) y = suc ( add x y )
+
+_++_ : {A : Set} → List A → List A → List A
+[] ++ y = y
+(x ∷ t) ++ y = x ∷ ( t ++ y )
+
+test1 = (zero ∷ []) ++ (zero ∷ [])
+
+length : {A : Set } → List A → Nat
+length [] = zero
+length (_ ∷ t)  = suc ( length t )
+
+lemma1 : {A : Set} → (x y : List A ) → length ( x ++ y ) ≡ add (length x) (length y)
+lemma1 [] y = refl
+lemma1 (x ∷ t) y = cong ( λ k → suc k ) lemma2  where
+   lemma2 : length (t ++ y) ≡ add (length t) (length y)
+   lemma2 = lemma1 t y
+
+-- record List1 ( A : Set  ) : Set where
+--    inductive
+--    field
+--       nil : List1 A 
+--       cons : A → List1 A → List1 A
+-- 
+-- record List2 ( A : Set  ) : Set where
+--    coinductive
+--    field
+--       nil : List2 A 
+--       cons : A → List2 A → List2 A
+
+data SList (i : Size) (A : Set) : Set where
+  []' : SList i A
+  _∷'_ : {j : Size< i} (x : A) (xs : SList j A) → SList i A
+
+
+map : ∀{i A B} → (A → B) → SList i A → SList i B
+map f []' = []'
+map f ( x ∷' xs)= f x ∷' map f xs
+
+foldr : ∀{i} {A B : Set} → (A → B → B) → B → SList i A → B
+foldr c n []' = n
+foldr c n (x ∷' xs) = c x (foldr c n xs)
+
+any : ∀{i A} → (A → Bool) → SList i A → Bool
+any p xs = foldr _∨_ false (map p xs)
+
+-- Sappend : {A : Set } {i j : Size } → SList i A → SList j A → SList {!!} A
+-- Sappend []' y = y
+-- Sappend (x ∷' x₁) y =  _∷'_  {?}  x (Sappend x₁ y)
+
+language : { Σ : Set } → Set
+language {Σ} = List Σ → Bool
+
+record Lang (i : Size) (A : Set) : Set where
+  coinductive
+  field
+    ν : Bool
+    δ : ∀{j : Size< i} → A → Lang j A
+
+open Lang
+
+∅ : ∀ {i A}  → Lang i A
+ν ∅   = false
+δ ∅ _ = ∅
+
+∅' :  {i : Size } { A : Set }  → Lang i A
+∅' {i} {A}  = record { ν = false ; δ = lemma3 } where
+    lemma3 : {j : Size< i} → A → Lang j A
+    lemma3 {j} _ = {!!}
+
+∅l : {A : Set } → language {A}
+∅l _ = false
+
+ε : ∀ {i A} → Lang i A
+ν ε   = true
+δ ε _ = ∅
+
+εl : {A : Set } → language {A}
+εl [] = true
+εl (_ ∷ _)  = false
+
+_+_ : ∀ {i A} → Lang i A → Lang i A → Lang i A
+ν (a + b)   = ν a   ∨  ν b
+δ (a + b) x = δ a x + δ b x
+
+Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
+Union {Σ} A B x = (A x ) ∨ (B x)
+
+_·_ : ∀ {i A} → Lang i A → Lang i A → Lang i A
+ν (a · b)   = ν a ∧ ν b
+δ (a · b) x = if (ν a) then ((δ a x · b ) + (δ b x )) else ( δ a x · b )
+
+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
+
+Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
+Concat {Σ} A B = split A B
+
diff -r 08e2af685c69 -r 7a0634a7c25a agda/induction.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/induction.agda	Wed Dec 18 17:34:15 2019 +0900
@@ -0,0 +1,1 @@
+module induction where
diff -r 08e2af685c69 -r 7a0634a7c25a agda/nat.agda
--- a/agda/nat.agda	Sun Nov 24 19:13:44 2019 +0900
+++ b/agda/nat.agda	Wed Dec 18 17:34:15 2019 +0900
@@ -1,56 +1,289 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module nat where
 
-open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+open import Data.Nat 
+open import Data.Nat.Properties
 open import Data.Empty
 open import Relation.Nullary
 open import  Relation.Binary.PropositionalEquality
+open import  Relation.Binary.Core
 open import  logic
 
 
-nat-<> : { x y : Nat } → x < y → y < x → ⊥
+nat-<> : { x y : ℕ } → x < y → y < x → ⊥
 nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
 
-nat-≤> : { x y : Nat } → x ≤ y → y < x → ⊥
+nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
 nat-≤>  (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
 
-nat-<≡ : { x : Nat } → x < x → ⊥
+nat-<≡ : { x : ℕ } → x < x → ⊥
 nat-<≡  (s≤s lt) = nat-<≡ lt
 
-nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥
+nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
 nat-≡< refl lt = nat-<≡ lt
 
-¬a≤a : {la : Nat} → Suc la ≤ la → ⊥
+¬a≤a : {la : ℕ} → suc la ≤ la → ⊥
 ¬a≤a  (s≤s lt) = ¬a≤a  lt
 
-a<sa : {la : Nat} → la < Suc la 
-a<sa {Zero} = s≤s z≤n
-a<sa {Suc la} = s≤s a<sa 
+a<sa : {la : ℕ} → la < suc la 
+a<sa {zero} = s≤s z≤n
+a<sa {suc la} = s≤s a<sa 
 
-=→¬< : {x : Nat  } → ¬ ( x < x )
-=→¬< {Zero} ()
-=→¬< {Suc x} (s≤s lt) = =→¬< lt
+=→¬< : {x : ℕ  } → ¬ ( x < x )
+=→¬< {zero} ()
+=→¬< {suc x} (s≤s lt) = =→¬< lt
 
->→¬< : {x y : Nat  } → (x < y ) → ¬ ( y < x )
+>→¬< : {x y : ℕ  } → (x < y ) → ¬ ( y < x )
 >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
 
-<-∨ : { x y : Nat } → x < Suc y → ( (x ≡ y ) ∨ (x < y) )
-<-∨ {Zero} {Zero} (s≤s z≤n) = case1 refl
-<-∨ {Zero} {Suc y} (s≤s lt) = case2 (s≤s z≤n)
-<-∨ {Suc x} {Zero} (s≤s ())
-<-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt
-<-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq)
-<-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
+<-∨ : { x y : ℕ } → x < suc y → ( (x ≡ y ) ∨ (x < y) )
+<-∨ {zero} {zero} (s≤s z≤n) = case1 refl
+<-∨ {zero} {suc y} (s≤s lt) = case2 (s≤s z≤n)
+<-∨ {suc x} {zero} (s≤s ())
+<-∨ {suc x} {suc y} (s≤s lt) with <-∨ {x} {y} lt
+<-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq)
+<-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
 
-max : (x y : Nat) → Nat
-max Zero Zero = Zero
-max Zero (Suc x) = (Suc x)
-max (Suc x) Zero = (Suc x)
-max (Suc x) (Suc y) = Suc ( max x y )
+max : (x y : ℕ) → ℕ
+max zero zero = zero
+max zero (suc x) = (suc x)
+max (suc x) zero = (suc x)
+max (suc x) (suc y) = suc ( max x y )
 
--- _*_ : Nat → Nat → Nat
+-- _*_ : ℕ → ℕ → ℕ
 -- _*_ zero _ = zero
 -- _*_ (suc n) m = m + ( n * m )
 
-exp : Nat → Nat → Nat
-exp _ Zero = 1
-exp n (Suc m) = n * ( exp n m )
+exp : ℕ → ℕ → ℕ
+exp _ zero = 1
+exp n (suc m) = n * ( exp n m )
+
+minus : (a b : ℕ ) →  ℕ
+minus a zero = a
+minus zero (suc b) = zero
+minus (suc a) (suc b) = minus a b
+
+_-_ = minus
+
+m+= : {i j  m : ℕ } → m + i ≡ m + j → i ≡ j
+m+= {i} {j} {zero} refl = refl
+m+= {i} {j} {suc m} eq = m+= {i} {j} {m} ( cong (λ k → pred k ) eq )
+
++m= : {i j  m : ℕ } → i + m ≡ j + m → i ≡ j
++m= {i} {j} {m} eq = m+= ( subst₂ (λ j k → j ≡ k ) (+-comm i _ ) (+-comm j _ ) eq )
+
+less-1 :  { n m : ℕ } → suc n < m → n < m
+less-1 {zero} {suc (suc _)} (s≤s (s≤s z≤n)) = s≤s z≤n
+less-1 {suc n} {suc m} (s≤s lt) = s≤s (less-1 {n} {m} lt)
+
+sa=b→a<b :  { n m : ℕ } → suc n ≡ m → n < m
+sa=b→a<b {0} {suc zero} refl = s≤s z≤n
+sa=b→a<b {suc n} {suc (suc n)} refl = s≤s (sa=b→a<b refl)
+
+minus+n : {x y : ℕ } → suc x > y  → minus x y + y ≡ x
+minus+n {x} {zero} _ = trans (sym (+-comm zero  _ )) refl
+minus+n {zero} {suc y} (s≤s ())
+minus+n {suc x} {suc y} (s≤s lt) = begin
+           minus (suc x) (suc y) + suc y
+        ≡⟨ +-comm _ (suc y)    ⟩
+           suc y + minus x y 
+        ≡⟨ cong ( λ k → suc k ) (
+           begin
+                 y + minus x y 
+              ≡⟨ +-comm y  _ ⟩
+                 minus x y + y
+              ≡⟨ minus+n {x} {y} lt ⟩
+                 x 
+           ∎  
+           ) ⟩
+           suc x
+        ∎  where open ≡-Reasoning
+
+
+-- open import Relation.Binary.PropositionalEquality
+
+-- postulate extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n)
+
+-- <-≡-iff : {A B : (a b : ℕ ) → Set } → {a b : ℕ }  → (A a b → B a b ) → (B a b → A a b ) → A ≡ B
+-- <-≡-iff {A} {B} ab ba = {!!}
+
+
+0<s : {x : ℕ } → zero < suc x
+0<s {_} = s≤s z≤n 
+
+<-minus-0 : {x y z : ℕ } → z + x < z + y → x < y
+<-minus-0 {x} {suc _} {zero} lt = lt
+<-minus-0 {x} {y} {suc z} (s≤s lt) = <-minus-0 {x} {y} {z} lt
+
+<-minus : {x y z : ℕ } → x + z < y + z → x < y
+<-minus {x} {y} {z} lt = <-minus-0 ( subst₂ ( λ j k → j < k ) (+-comm x _) (+-comm y _ ) lt )
+
+x≤x+y : {z y : ℕ } → z ≤ z + y
+x≤x+y {zero} {y} = z≤n
+x≤x+y {suc z} {y} = s≤s  (x≤x+y {z} {y})
+
+<-plus : {x y z : ℕ } → x < y → x + z < y + z 
+<-plus {zero} {suc y} {z} (s≤s z≤n) = s≤s (subst (λ k → z ≤ k ) (+-comm z _ ) x≤x+y  )
+<-plus {suc x} {suc y} {z} (s≤s lt) = s≤s (<-plus {x} {y} {z} lt)
+
+<-plus-0 : {x y z : ℕ } → x < y → z + x < z + y 
+<-plus-0 {x} {y} {z} lt = subst₂ (λ j k → j < k ) (+-comm _ z) (+-comm _ z) ( <-plus {x} {y} {z} lt )
+
+≤-plus : {x y z : ℕ } → x ≤ y → x + z ≤ y + z
+≤-plus {0} {y} {zero} z≤n = z≤n
+≤-plus {0} {y} {suc z} z≤n = subst (λ k → z < k ) (+-comm _ y ) x≤x+y 
+≤-plus {suc x} {suc y} {z} (s≤s lt) = s≤s ( ≤-plus {x} {y} {z} lt )
+
+≤-plus-0 : {x y z : ℕ } → x ≤ y → z + x ≤ z + y 
+≤-plus-0 {x} {y} {zero} lt = lt
+≤-plus-0 {x} {y} {suc z} lt = s≤s ( ≤-plus-0 {x} {y} {z} lt )
+
+x+y<z→x<z : {x y z : ℕ } → x + y < z → x < z 
+x+y<z→x<z {zero} {y} {suc z} (s≤s lt1) = s≤s z≤n
+x+y<z→x<z {suc x} {y} {suc z} (s≤s lt1) = s≤s ( x+y<z→x<z {x} {y} {z} lt1 )
+
+*≤ : {x y z : ℕ } → x ≤ y → x * z ≤ y * z 
+*≤ lt = *-mono-≤ lt ≤-refl
+
+*< : {x y z : ℕ } → x < y → x * suc z < y * suc z 
+*< {zero} {suc y} lt = s≤s z≤n
+*< {suc x} {suc y} (s≤s lt) = <-plus-0 (*< lt)
+
+<to<s : {x y  : ℕ } → x < y → x < suc y
+<to<s {zero} {suc y} (s≤s lt) = s≤s z≤n
+<to<s {suc x} {suc y} (s≤s lt) = s≤s (<to<s {x} {y} lt)
+
+<tos<s : {x y  : ℕ } → x < y → suc x < suc y
+<tos<s {zero} {suc y} (s≤s z≤n) = s≤s (s≤s z≤n)
+<tos<s {suc x} {suc y} (s≤s lt) = s≤s (<tos<s {x} {y} lt)
+
+≤to< : {x y  : ℕ } → x < y → x ≤ y 
+≤to< {zero} {suc y} (s≤s z≤n) = z≤n
+≤to< {suc x} {suc y} (s≤s lt) = s≤s (≤to< {x} {y}  lt)
+
+refl-≤s : {x : ℕ } → x ≤ suc x
+refl-≤s {zero} = z≤n
+refl-≤s {suc x} = s≤s (refl-≤s {x})
+
+x<y→≤ : {x y : ℕ } → x < y →  x ≤ suc y
+x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n
+x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt)
+
+open import Data.Product
+
+minus<=0 : {x y : ℕ } → x ≤ y → minus x y ≡ 0
+minus<=0 {0} {zero} z≤n = refl
+minus<=0 {0} {suc y} z≤n = refl
+minus<=0 {suc x} {suc y} (s≤s le) = minus<=0 {x} {y} le
+
+minus>0 : {x y : ℕ } → x < y → 0 < minus y x 
+minus>0 {zero} {suc _} (s≤s z≤n) = s≤s z≤n
+minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt
+
+distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z) 
+distr-minus-* {x} {zero} {z} = refl
+distr-minus-* {x} {suc y} {z} with <-cmp x y
+distr-minus-* {x} {suc y} {z} | tri< a ¬b ¬c = begin
+          minus x (suc y) * z
+        ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} (x<y→≤ a)) ⟩
+           0 * z 
+        ≡⟨ sym (minus<=0 {x * z} {z + y * z} le ) ⟩
+          minus (x * z) (z + y * z) 
+        ∎  where
+            open ≡-Reasoning
+            le : x * z ≤ z + y * z
+            le  = ≤-trans lemma (subst (λ k → y * z ≤ k ) (+-comm _ z ) (x≤x+y {y * z} {z} ) ) where
+               lemma : x * z ≤ y * z
+               lemma = *≤ {x} {y} {z} (≤to< a)
+distr-minus-* {x} {suc y} {z} | tri≈ ¬a refl ¬c = begin
+          minus x (suc y) * z
+        ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} refl-≤s ) ⟩
+           0 * z 
+        ≡⟨ sym (minus<=0 {x * z} {z + y * z} (lt {x} {z} )) ⟩
+          minus (x * z) (z + y * z) 
+        ∎  where
+            open ≡-Reasoning
+            lt : {x z : ℕ } →  x * z ≤ z + x * z
+            lt {zero} {zero} = z≤n
+            lt {suc x} {zero} = lt {x} {zero}
+            lt {x} {suc z} = ≤-trans lemma refl-≤s where
+               lemma : x * suc z ≤   z + x * suc z
+               lemma = subst (λ k → x * suc z ≤ k ) (+-comm _ z) (x≤x+y {x * suc z} {z}) 
+distr-minus-* {x} {suc y} {z} | tri> ¬a ¬b c = +m= {_} {_} {suc y * z} ( begin
+           minus x (suc y) * z + suc y * z
+        ≡⟨ sym (proj₂ *-distrib-+ z  (minus x (suc y) )  _) ⟩
+           ( minus x (suc y) + suc y ) * z
+        ≡⟨ cong (λ k → k * z) (minus+n {x} {suc y} (s≤s c))  ⟩
+           x * z 
+        ≡⟨ sym (minus+n {x * z} {suc y * z} (s≤s (lt c))) ⟩
+           minus (x * z) (suc y * z) + suc y * z
+        ∎ ) where
+            open ≡-Reasoning
+            lt : {x y z : ℕ } → suc y ≤ x → z + y * z ≤ x * z
+            lt {x} {y} {z} le = *≤ le 
+
+minus- : {x y z : ℕ } → suc x > z + y → minus (minus x y) z ≡ minus x (y + z)
+minus- {x} {y} {z} gt = +m= {_} {_} {z} ( begin
+           minus (minus x y) z + z
+        ≡⟨ minus+n {_} {z} lemma ⟩
+           minus x y
+        ≡⟨ +m= {_} {_} {y} ( begin
+              minus x y + y 
+           ≡⟨ minus+n {_} {y} lemma1 ⟩
+              x
+           ≡⟨ sym ( minus+n {_} {z + y} gt ) ⟩
+              minus x (z + y) + (z + y)
+           ≡⟨ sym ( +-assoc (minus x (z + y)) _  _ ) ⟩
+              minus x (z + y) + z + y
+           ∎ ) ⟩
+           minus x (z + y) + z
+        ≡⟨ cong (λ k → minus x k + z ) (+-comm _ y )  ⟩
+           minus x (y + z) + z
+        ∎  ) where
+             open ≡-Reasoning
+             lemma1 : suc x > y
+             lemma1 = x+y<z→x<z (subst (λ k → k < suc x ) (+-comm z _ ) gt )
+             lemma : suc (minus x y) > z
+             lemma = <-minus {_} {_} {y} ( subst ( λ x → z + y < suc x ) (sym (minus+n {x} {y}  lemma1 ))  gt )
+
+minus-* : {M k n : ℕ } → n < k  → minus k (suc n) * M ≡ minus (minus k n * M ) M
+minus-* {zero} {k} {n} lt = begin
+           minus k (suc n) * zero
+        ≡⟨ *-comm (minus k (suc n)) zero ⟩
+           zero * minus k (suc n) 
+        ≡⟨⟩
+           0 * minus k n 
+        ≡⟨ *-comm 0 (minus k n) ⟩
+           minus (minus k n * 0 ) 0
+        ∎  where
+        open ≡-Reasoning
+minus-* {suc m} {k} {n} lt with <-cmp k 1
+minus-* {suc m} {.0} {zero} lt | tri< (s≤s z≤n) ¬b ¬c = refl
+minus-* {suc m} {.0} {suc n} lt | tri< (s≤s z≤n) ¬b ¬c = refl
+minus-* {suc zero} {.1} {zero} lt | tri≈ ¬a refl ¬c = refl
+minus-* {suc (suc m)} {.1} {zero} lt | tri≈ ¬a refl ¬c = minus-* {suc m} {1} {zero} lt 
+minus-* {suc m} {.1} {suc n} (s≤s ()) | tri≈ ¬a refl ¬c
+minus-* {suc m} {k} {n} lt | tri> ¬a ¬b c = begin
+           minus k (suc n) * M
+        ≡⟨ distr-minus-* {k} {suc n} {M}  ⟩
+           minus (k * M ) ((suc n) * M)
+        ≡⟨⟩
+           minus (k * M ) (M + n * M  )
+        ≡⟨ cong (λ x → minus (k * M) x) (+-comm M _ ) ⟩
+           minus (k * M ) ((n * M) + M )
+        ≡⟨ sym ( minus- {k * M} {n * M} (lemma lt) ) ⟩
+           minus (minus (k * M ) (n * M)) M
+        ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩
+           minus (minus k n * M ) M
+        ∎  where
+             M = suc m
+             lemma : {n k m : ℕ } → n < k  → suc (k * suc m) > suc m + n * suc m
+             lemma {zero} {suc k} {m} (s≤s lt) = s≤s (s≤s (subst (λ x → x ≤ m + k * suc m) (+-comm 0 _ ) x≤x+y ))
+             lemma {suc n} {suc k} {m} lt = begin
+                         suc (suc m + suc n * suc m) 
+                      ≡⟨⟩
+                         suc ( suc (suc n) * suc m)
+                      ≤⟨ ≤-plus-0 {_} {_} {1} (*≤ lt ) ⟩
+                         suc (suc k * suc m)
+                      ∎   where open ≤-Reasoning
+             open ≡-Reasoning
diff -r 08e2af685c69 -r 7a0634a7c25a agda/pushdown.agda
--- a/agda/pushdown.agda	Sun Nov 24 19:13:44 2019 +0900
+++ b/agda/pushdown.agda	Wed Dec 18 17:34:15 2019 +0900
@@ -20,7 +20,6 @@
        : Set  where
     field
         pδ : Q → Σ →  Γ → Q × ( PushDown  Γ )
-        pstart : Q
         pok : Q → Bool
         pempty : Γ
     pmoves :  Q → List  Γ  → Σ → ( Q × List  Γ )
@@ -31,25 +30,23 @@
     pmoves q (H ∷ T) i | qn , pop =  ( qn , T )
     pmoves q (H ∷ T) i | qn , push x = ( qn , ( x ∷ H ∷ T) )
 
-    paccept : List  Σ → Bool
-    paccept L = move pstart L []
-           where
-              move : (q : Q ) ( In : List  Σ ) ( sp : List   Γ ) → Bool
-              move q [] [] = pok q
-              move q ( H  ∷ T) [] with pδ q H pempty
-              move q (H ∷ T) [] | qn , pop = move qn T []
-              move q (H ∷ T) [] | qn , push x = move qn T (x  ∷ [] )
-              move q [] (_ ∷ _ ) = false
-              move q ( H  ∷ T ) ( SH  ∷ ST ) with pδ q H SH
-              ... | (nq , pop )     = move nq T ST
-              ... | (nq , push ns ) = move nq T ( ns  ∷  SH ∷ ST )
+    paccept : (q : Q ) ( In : List  Σ ) ( sp : List   Γ ) → Bool
+    paccept q [] [] = pok q
+    paccept q ( H  ∷ T) [] with pδ q H pempty
+    paccept q (H ∷ T) [] | qn , pop = paccept qn T []
+    paccept q (H ∷ T) [] | qn , push x = paccept qn T (x  ∷ [] )
+    paccept q [] (_ ∷ _ ) = false
+    paccept q ( H  ∷ T ) ( SH  ∷ ST ) with pδ q H SH
+    ... | (nq , pop )     = paccept nq T ST
+    ... | (nq , push ns ) = paccept nq T ( ns  ∷  SH ∷ ST )
 
 
 --  0011
 --  00000111111
-inputnn : { n :  ℕ }  →  { Σ : Set  } → ( x y : Σ )  → List  Σ → List  Σ
-inputnn {zero} {_} _ _ s = s
-inputnn {suc n} x y s = x  ∷ ( inputnn {n} x y ( y  ∷ s ) )       
+inputnn : ( n :  ℕ )  →  { Σ : Set  } → ( x y : Σ )  → List  Σ → List  Σ
+inputnn zero {_} _ _ s = s
+inputnn (suc n) x y s = x  ∷ ( inputnn n x y ( y  ∷ s ) )       
+
 
 data  States0   : Set  where
    sr : States0
@@ -57,11 +54,12 @@
 data  In2   : Set  where
    i0 : In2
    i1 : In2
+
+test0 = inputnn 5 i0 i1 []
  
 pnn : PushDownAutomaton States0 In2 States0
 pnn = record {
          pδ  = pδ
-      ;  pstart = sr
       ;  pempty = sr
       ;  pok = λ q → true
    } where
@@ -69,7 +67,29 @@
         pδ sr i0 _ = (sr , push sr) 
         pδ sr i1 _ = (sr , pop ) 
 
-test1 = PushDownAutomaton.paccept pnn ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] )
-test2 = PushDownAutomaton.paccept pnn ( i0 ∷ i0 ∷ i1 ∷ i0 ∷ [] )
+data  States1   : Set  where
+   ss : States1
+   st : States1
+
+pn1 : PushDownAutomaton States1 In2 States1
+pn1 = record {
+         pδ  = pδ
+      ;  pempty = ss
+      ;  pok = pok1
+   } where
+        pok1 :  States1 → Bool
+        pok1 ss = false
+        pok1 st = true
+        pδ  : States1 → In2 → States1 → States1 × PushDown States1
+        pδ ss i0 _ = (ss , push ss) 
+        pδ ss i1 _ = (st , pop) 
+        pδ st i0 _ = (st , push ss) 
+        pδ st i1 _ = (st , pop ) 
+
+test1 = PushDownAutomaton.paccept pnn sr ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) []
+test2 = PushDownAutomaton.paccept pnn sr ( i0 ∷ i0 ∷ i1 ∷ i0 ∷ [] ) []
 test3 = PushDownAutomaton.pmoves pnn sr [] i0 
+test4 = PushDownAutomaton.paccept pnn sr ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ i0 ∷ i1 ∷ [] ) []
 
+test5 = PushDownAutomaton.paccept pn1 ss ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) []
+test6 = PushDownAutomaton.paccept pn1 ss ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ i0 ∷ i1 ∷ [] ) []
diff -r 08e2af685c69 -r 7a0634a7c25a agda/regex1.agda
--- a/agda/regex1.agda	Sun Nov 24 19:13:44 2019 +0900
+++ b/agda/regex1.agda	Wed Dec 18 17:34:15 2019 +0900
@@ -49,6 +49,36 @@
 repeat {Σ} x ( h  ∷ t ) = split x (repeat {Σ} x) ( h  ∷ t )
 
 open import finiteSet
+
+fin : FiniteSet hoge
+fin = record {
+        Q←F = Q←F
+      ; F←Q  = F←Q
+      ; finiso→ = finiso→
+      ; finiso← = finiso←
+   } where
+       Q←F : Fin 4 → hoge
+       Q←F zero = a
+       Q←F (suc zero) = b
+       Q←F (suc (suc zero)) = c
+       Q←F (suc (suc (suc zero))) = d
+       F←Q : hoge → Fin 4
+       F←Q a = zero
+       F←Q b = suc zero
+       F←Q c = suc (suc zero)
+       F←Q d = suc (suc (suc zero))
+       finiso→ : (q : hoge) → Q←F (F←Q q) ≡ q
+       finiso→ a = refl
+       finiso→ b = refl
+       finiso→ c = refl
+       finiso→ d = refl
+       finiso← : (f : Fin 4) → F←Q (Q←F f) ≡ f
+       finiso← zero = refl
+       finiso← (suc zero) = refl
+       finiso← (suc (suc zero)) = refl
+       finiso← (suc (suc (suc zero))) = refl
+       finiso← (suc (suc (suc (suc ()))))
+
 open FiniteSet
 
 cmpi :  {Σ : Set} → {n : ℕ } (fin : FiniteSet Σ {n}) → (x y : Σ ) → Dec (F←Q fin x ≡  F←Q fin y) 
@@ -64,3 +94,22 @@
 ... | no _  = false
 regular-language < h > f _ = false
 
+1r1' =    (< a > & < b >) & < c >
+1r1 =    < a > & < b > & < c >
+1any = < a > || < b >  || < c > || < d >
+1r2 =    ( any * ) & ( < a > & < b > & < c > )
+1r3 =    ( any * ) & ( < a > & < b > & < c > & < a > & < b > & < c > )
+1r4 =    ( < a > & < b > & < c > ) || ( < b > & < c > & < d > )
+1r5 =    ( any * ) & ( < a > & < b > & < c > || < b > & < c > & < d > )
+
+test-regex : regular-language 1r1' fin ( a ∷ [] ) ≡ false
+test-regex = refl
+
+test-regex1 : regular-language 1r1' fin ( a ∷ b ∷ c ∷ [] ) ≡ true
+test-regex1 = refl
+
+
+open import Data.Nat.DivMod
+
+test-regex-even : Set
+test-regex-even = (s : List hoge ) → regular-language ( ( 1any || 1any ) * )  fin s  ≡ true → (length s) mod 2 ≡ zero
diff -r 08e2af685c69 -r 7a0634a7c25a agda/regular-language.agda
--- a/agda/regular-language.agda	Sun Nov 24 19:13:44 2019 +0900
+++ b/agda/regular-language.agda	Wed Dec 18 17:34:15 2019 +0900
@@ -280,13 +280,14 @@
     contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA finab nq x ≡ true )
           → (qa : states A )  → (  (q : states A ∨ states B) → nq q ≡ true → ab-case q qa x )
           → split (accept (automaton A) qa ) (contain B) x ≡ true
-    contain-A [] nq fn qa cond with found← finab fn 
+    contain-A [] nq fn qa cond with found← finab fn  -- at this stage, A and B must be satisfied with [] (ab-case cond forces it)
     ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S))
     ... | case1 qa' | record { eq = refl } | refl = bool-∧→tt-1 (found-p S)
     ... | case2 qb | record { eq = refl } | ab = ⊥-elim ( ab (bool-∧→tt-1 (found-p S)))
     contain-A (h ∷ t) nq fn qa cond with bool-≡-? ((aend (automaton A) qa) /\  accept (automaton B) (δ (automaton B) (astart B) h) t ) true
-    ... | yes eq = bool-or-41 eq
-    ... | no ne = bool-or-31 (contain-A t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) lemma11 ) where
+    ... | yes eq = bool-or-41 eq  -- found A ++ B all end
+    ... | no ne = bool-or-31 (contain-A t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) lemma11 ) where -- B failed continue with ab-base condtion
+       --- prove ab-ase condition (we haven't checked but case2 b may happen)
        lemma11 :  (q : states A ∨ states B) → exists finab (λ qn → nq qn /\ Nδ NFA qn h q) ≡ true → ab-case q (δ (automaton A) qa h) t
        lemma11 (case1 qa')  ex with found← finab ex 
        ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S))