Mercurial > hg > Members > kono > Proof > automaton

changeset 163:26407ce19d66

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 13 Jan 2021 10:52:01 +0900
parents 690a8352c1ad
children bee86ee07fff
files a02/agda-install.ind a02/lecture.ind a03/lecture.ind agda/FSetUtil.agda agda/automaton-ex.agda agda/cfg1.agda agda/chap0.agda agda/fin.agda agda/finiteSetUtil.agda agda/nat.agda agda/pushdown.agda agda/regular-concat.agda
diffstat 12 files changed, 818 insertions(+), 459 deletions(-) [+]
line wrap: on
line diff
--- a/a02/agda-install.ind	Mon Jan 04 13:20:31 2021 +0900
+++ b/a02/agda-install.ind	Wed Jan 13 10:52:01 2021 +0900
@@ -2,12 +2,6 @@
 
 Homebrew を使うのが良いそうです。
 
-Emacs を先に入れます。
-
-  brew tap caskroom/cask
-  brew cask install emacs
-
-その後、
 
    brew install agda
 
@@ -47,6 +41,11 @@
 
 --Emacs
 
+Emacs を先に入れます。
+
+  brew tap caskroom/cask
+  brew cask install emacs
+
 ~/.emacs.d/init.el に以下のファイルを置きます。あるいは自分のinit.el に適当に追加します。
 中のpathは正しいものに置き換えます。
 
@@ -69,6 +68,7 @@
 
 M-X help-for-help M で、Agda のコマンドの一覧が出ます。C-X o で buffer を切り替えて読みます。
 
+Space Emacs というのもあるらしい。
 
 --vim
 
--- a/a02/lecture.ind	Mon Jan 04 13:20:31 2021 +0900
+++ b/a02/lecture.ind	Wed Jan 13 10:52:01 2021 +0900
@@ -457,7 +457,7 @@
 
 <a href="agda/level1.agda"> level </a> <!---  Exercise 2.5 --->
 
---問題2.6 List
+--List
 
 List は cons か nil かどちらかの構造で、cons は List を再帰的に含んでいる。
 
--- a/a03/lecture.ind	Mon Jan 04 13:20:31 2021 +0900
+++ b/a03/lecture.ind	Wed Jan 13 10:52:01 2021 +0900
@@ -1,7 +1,17 @@
 -title: 決定性オートマトン
 
+数学の本に書いてあることを Agda で定義してみる。なるべく、数学の本に近くする。
+
+Agda は関数型言語なので、数字の添字を使うものは合わない。そのあたりは修正する。
+
+Agda は直観主義論理なので、排他律が成立しない。存在を示すには構成的、つまり関数で構成する必要がある。
+
+数学の本でも、構成的な証明かどうかは(選択公理を使っているかどうかなどで)区別されていることが多い。
+
 -- Automaton オートマトンの定義 ( Q, Σ, σ, q0, F )
 
+教科書では以下のようになっている。
+
     1. Q is a finte set calles states
     2. Σ is a finte set calles alphabet
     3. δ : Q x Σ is the transition function
@@ -16,12 +26,12 @@
             δ : Q → Σ → Q
             aend : Q → Bool
 
+どれがどこにん対応しているかを確認しよう。
+
 <a href="../agda/automaton.agda"> automaton.agda </a>
 <br>
 <a href="../agda/logic.agda"> logic.agda </a>
 <br>
-<a href="../agda/finiteSet.agda"> finiteSet.agda </a>
-<br>
 
 record は名前のついた数学的構造で、二つの集合 Q と Σの関係定義する関数からなる。
 
@@ -127,6 +137,8 @@
 
 とする。( example1-1 の型は何か?)
 
+<a href="../agda/automaton-ex.agda"> Agda による Automaton の例題 </a>
+
 --問題 3.1
 
 教科書のAutomatonの例のいくつかを Agda で定義してみよ。
@@ -138,19 +150,119 @@
 
 --Regular Language
 
-Language とは?
+Automaton は List Σ に対して true / false を返す。つまり、文字列の部分集合を決定する。
 
-Regular Language とは?
+文字列の部分集合を (Automaton の専門用語として) Language という。でたらめの発声の部分集合が日本語なので言語といえなくもない。
+
+なんらかのAutomaton が受け付ける文字列の部分集合を Regular Language という。この範囲に収まらない Language も後で調べる。
 
 --Regular Languageの演算
 
-Concatenation
+Regular Languageは以下の演算に付いて閉じていることが知られている。閉じているとは以下の集合演算をしても、それはやはり
+Regular Language つまり、Automaton で、その集合に入っているかどうかを判定できる。
 
-Union
+    二つの文字列集合から、その結合を集める Concatenation
 
-Star
+    文字列の集合の和集合 Union
+
+    結合の繰り返し Star
 
 <a href="../agda/regular-language.agda"> Agda での Regular Language </a>
 
 
+--Agda によるRegular Languageの集合演算
 
+部分集合は true / false で判断する。
+
+    language : { Σ : Set } → Set
+    language {Σ} = List Σ → Bool
+
+何かのAutomaton で判定される言語は ∃ automaton だが、これを record で書く。
+
+    record RegularLanguage ( Σ : Set ) : Set (Suc Zero) where
+       field
+          states : Set 
+          astart : states 
+          automaton : Automaton states Σ
+       contain : List Σ → Bool
+       contain x = accept automaton astart x
+
+contain が language の定義の形になっていることを確認しよう。
+
+Unio は Bool 演算を使って簡単に表される。
+
+    Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
+    Union {Σ} A B x = (A x ) \/ (B x)
+
+Concat はそんなに簡単ではない。ある文字列が、前半はAの要素で、後半がBの要素であれば良いのだが、
+
+    Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
+    Concat {Σ} A B x = ?
+
+前半と後半の分け方には非決定性がある。
+
+--Split
+
+i0 ∷ i1 ∷ i0 ∷ [] の分け方は and と or で以下のようになる。
+
+       ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/ 
+       ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/ 
+       ( A ( i0 ∷ i1 ∷ [] ) /\ B ( i0 ∷ [] ) ) \/
+       ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) /\ 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
+
+これが、実際に文字列の分解になっていることを確認する。
+
+    test-AB→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-AB→split {_} {A} {B} = refl
+
+これを使って Concat と Star を書ける。
+
+    Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
+    Concat {Σ} A B = split A B
+
+    {-# TERMINATING #-}
+    Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
+    Star {Σ} A = split A ( Star {Σ} A )
+
+{-# TERMINATING #-}は Agda が停止性を判定できないというエラーを抑止する。
+
+--Union が RegularLanguage で閉じていること
+
+RegularLanguage かどうかは以下の命題を作れるかどうかでわかる。
+
+    isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set
+    isRegular A x r = A x ≡ contain r x 
+
+たとえば Union に付いて閉じているかどうかは
+
+     closed-in-union :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B )
+
+とかける。この時に 
+
+     M-Union : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
+
+で、これは Automaton を具体的に作る必要がある。
+
+この証明は比較的やさしい。
+
+
+--Concat が RegularLanguage で閉じていること
+
+これは割と難しい。Automaton の状態が有限であることが必要になる。
+
+
+
+
--- a/agda/FSetUtil.agda	Mon Jan 04 13:20:31 2021 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,411 +0,0 @@
-module FSetUtil  where
-
-open import Data.Nat hiding ( _≟_ )
-open import Data.Fin renaming ( _<_ to _<<_ ) hiding (_≤_)
-open import Data.Fin.Properties
-open import Data.Empty
-open import Relation.Nullary
-open import Relation.Binary.Definitions
-open import Relation.Binary.PropositionalEquality
-open import logic
-open import nat
-open import finiteSet
-open import Data.Nat.Properties as NatP  hiding ( _≟_ )
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
-
-record ISO (A B : Set) : Set where
-   field
-     A←B : B → A
-     B←A : A → B
-     iso← : (q : A) → A←B ( B←A q ) ≡ q
-     iso→ : (f : B) → B←A ( A←B f ) ≡ f
-
-iso-fin : {A B : Set} → FiniteSet A  → ISO A B → FiniteSet B 
-iso-fin {A} {B}  fin iso = record {
-   Q←F = λ f → ISO.B←A iso ( FiniteSet.Q←F fin f )
- ; F←Q = λ b → FiniteSet.F←Q fin ( ISO.A←B iso b )
- ; finiso→ = finiso→ 
- ; finiso← = finiso← 
-   } where
-   finiso→ : (q : B) → ISO.B←A iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (ISO.A←B iso q))) ≡ q
-   finiso→ q = begin
-              ISO.B←A iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (ISO.A←B iso q))) 
-           ≡⟨ cong (λ k → ISO.B←A iso k ) (FiniteSet.finiso→ fin _ ) ⟩
-              ISO.B←A iso (ISO.A←B iso q)
-           ≡⟨ ISO.iso→ iso _ ⟩
-              q
-           ∎  where
-           open ≡-Reasoning
-   finiso← : (f : Fin (FiniteSet.finite fin ))→ FiniteSet.F←Q fin (ISO.A←B iso (ISO.B←A iso (FiniteSet.Q←F fin f))) ≡ f
-   finiso← f = begin
-              FiniteSet.F←Q fin (ISO.A←B iso (ISO.B←A iso (FiniteSet.Q←F fin f))) 
-           ≡⟨ cong (λ k → FiniteSet.F←Q fin k ) (ISO.iso← iso _) ⟩
-              FiniteSet.F←Q fin (FiniteSet.Q←F fin f) 
-           ≡⟨ FiniteSet.finiso← fin _  ⟩
-              f
-           ∎  where
-           open ≡-Reasoning
-
-data One : Set where
-   one : One
-
-fin-∨1 : {B : Set} → (fb : FiniteSet B ) → FiniteSet (One ∨ B) 
-fin-∨1 {B} fb =  record {
-   Q←F = Q←F
- ; F←Q =  F←Q
- ; finiso→ = finiso→
- ; finiso← = finiso←
-   }  where
-   b = FiniteSet.finite fb
-   Q←F : Fin (suc b) → One ∨ B
-   Q←F zero = case1 one
-   Q←F (suc f) = case2 (FiniteSet.Q←F fb f)
-   F←Q : One ∨ B → Fin (suc b)
-   F←Q (case1 one) = zero
-   F←Q (case2 f ) = suc (FiniteSet.F←Q fb f) 
-   finiso→ : (q : One ∨ B) → Q←F (F←Q q) ≡ q
-   finiso→ (case1 one) = refl
-   finiso→ (case2 b) = cong (λ k → case2 k ) (FiniteSet.finiso→ fb b)
-   finiso← : (q : Fin (suc b)) → F←Q (Q←F q) ≡ q
-   finiso← zero = refl
-   finiso← (suc f) = cong ( λ k → suc k ) (FiniteSet.finiso← fb f)
-
-
-fin-∨2 : {B : Set} → ( a : ℕ ) → FiniteSet B  → FiniteSet (Fin a ∨ B) 
-fin-∨2 {B} zero  fb = iso-fin fb iso where
-   iso : ISO B (Fin zero ∨ B)
-   iso =  record {
-        A←B = A←B
-      ; B←A = λ b → case2 b
-      ; iso→ = iso→
-      ; iso← = λ _ → refl
-    } where
-     A←B : Fin zero ∨ B → B
-     A←B (case2 x) = x 
-     iso→ : (f : Fin zero ∨ B ) → case2 (A←B f) ≡ f
-     iso→ (case2 x)  = refl
-fin-∨2 {B} (suc a) fb =  iso-fin (fin-∨1 (fin-∨2 a fb) ) iso
-    where
-  iso : ISO (One ∨ (Fin a ∨ B) ) (Fin (suc a) ∨ B)
-  ISO.A←B iso (case1 zero) = case1 one
-  ISO.A←B iso (case1 (suc f)) = case2 (case1 f)
-  ISO.A←B iso (case2 b) = case2 (case2 b)
-  ISO.B←A iso (case1 one) = case1 zero
-  ISO.B←A iso (case2 (case1 f)) = case1 (suc f)
-  ISO.B←A iso (case2 (case2 b)) = case2 b
-  ISO.iso← iso (case1 one) = refl
-  ISO.iso← iso (case2 (case1 x)) = refl
-  ISO.iso← iso (case2 (case2 x)) = refl
-  ISO.iso→ iso (case1 zero) = refl
-  ISO.iso→ iso (case1 (suc x)) = refl
-  ISO.iso→ iso (case2 x) = refl
-
-
-FiniteSet→Fin : {A : Set} → (fin : FiniteSet A  ) → ISO (Fin (FiniteSet.finite fin)) A
-ISO.A←B (FiniteSet→Fin fin) f = FiniteSet.F←Q fin f
-ISO.B←A (FiniteSet→Fin fin) f = FiniteSet.Q←F fin f
-ISO.iso← (FiniteSet→Fin fin) = FiniteSet.finiso← fin
-ISO.iso→ (FiniteSet→Fin fin) =  FiniteSet.finiso→ fin
-   
-
-fin-∨ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∨ B) 
-fin-∨ {A} {B}  fa fb = iso-fin (fin-∨2 a  fb ) iso2 where
-    a = FiniteSet.finite fa
-    ia = FiniteSet→Fin fa
-    iso2 : ISO (Fin a ∨ B ) (A ∨ B)
-    ISO.A←B iso2 (case1 x) = case1 ( ISO.A←B ia x )
-    ISO.A←B iso2 (case2 x) = case2 x
-    ISO.B←A iso2 (case1 x) = case1 ( ISO.B←A ia x )
-    ISO.B←A iso2 (case2 x) = case2 x
-    ISO.iso← iso2 (case1 x) = cong ( λ k → case1 k ) (ISO.iso← ia x)
-    ISO.iso← iso2 (case2 x) = refl
-    ISO.iso→ iso2 (case1 x) = cong ( λ k → case1 k ) (ISO.iso→ ia x)
-    ISO.iso→ iso2 (case2 x) = refl
-
-open import Data.Product
-
-fin-× : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A × B) 
-fin-× {A} {B}  fa fb with FiniteSet→Fin fa
-... | a=f = iso-fin (fin-×-f a ) iso-1 where
-   a = FiniteSet.finite fa
-   b = FiniteSet.finite fb
-   iso-1 : ISO (Fin a × B) ( A × B )
-   ISO.A←B iso-1 x = ( FiniteSet.F←Q fa (proj₁ x)  , proj₂ x) 
-   ISO.B←A iso-1 x = ( FiniteSet.Q←F fa (proj₁ x)  , proj₂ x) 
-   ISO.iso← iso-1 x  =  lemma  where
-     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 )
-   ISO.B←A iso-2 (case1 b) = ( zero , b )
-   ISO.B←A iso-2 (case2 (a , b )) = ( suc a , b )
-   ISO.iso← iso-2 (case1 x) = refl
-   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) 
-   fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () ; finite = 0 }
-   fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2
-
-open _∧_
-
-fin-∧ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∧ B) 
-fin-∧ {A} {B} fa fb with FiniteSet→Fin fa    -- same thing for our tool
-... | a=f = iso-fin (fin-×-f a ) iso-1 where
-   a = FiniteSet.finite fa
-   b = FiniteSet.finite fb
-   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} 
-   ISO.B←A iso-1 x = record { proj1 = FiniteSet.Q←F fa (proj1 x)  ; proj2 =  proj2 x}
-   ISO.iso← iso-1 x  =  lemma  where
-     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 } )
-   ISO.B←A iso-2 (case1 b) = record {proj1 =  zero ; proj2 =  b }
-   ISO.B←A iso-2 (case2 (record { proj1 = a ; proj2 =  b })) = record { proj1 =  suc a ; proj2 =  b }
-   ISO.iso← iso-2 (case1 x) = refl
-   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) 
-   fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () ; finite = 0 }
-   fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2
-
--- import Data.Nat.DivMod
-
-open import Data.Vec
-import Data.Product
-
-exp2 : (n : ℕ ) → exp 2 (suc n) ≡ exp 2 n Data.Nat.+ exp 2 n
-exp2 n = begin
-      exp 2 (suc n)
-   ≡⟨⟩
-      2 * ( exp 2 n )
-   ≡⟨ *-comm 2 (exp 2 n)  ⟩
-      ( exp 2 n ) * 2
-   ≡⟨ *-suc ( exp 2 n ) 1 ⟩
-      (exp 2 n ) Data.Nat.+ ( exp 2 n ) * 1
-   ≡⟨ cong ( λ k →  (exp 2 n ) Data.Nat.+  k ) (proj₂ *-identity (exp 2 n) ) ⟩
-      exp 2 n Data.Nat.+ exp 2 n
-   ∎  where
-       open ≡-Reasoning
-       open Data.Product
-
-cast-iso : {n m : ℕ } → (eq : n ≡ m ) → (f : Fin m ) → cast eq ( cast (sym eq ) f)  ≡ f
-cast-iso refl zero =  refl
-cast-iso refl (suc f) = cong ( λ k → suc k ) ( cast-iso refl f )
-
-
-fin2List : {n : ℕ } → FiniteSet (Vec Bool n) 
-fin2List {zero} = record {
-   Q←F = λ _ → Vec.[]
- ; F←Q =  λ _ → # 0
- ; finiso→ = finiso→ 
- ; finiso← = finiso← 
-   } where
-   Q = Vec Bool zero
-   finiso→ : (q : Q) → [] ≡ q
-   finiso→ [] = refl
-   finiso← : (f : Fin (exp 2 zero)) → # 0 ≡ f
-   finiso← zero = refl
-fin2List {suc n} = subst (λ k → FiniteSet (Vec Bool (suc n)) ) (sym (exp2 n)) ( iso-fin (fin-∨ (fin2List ) (fin2List )) iso )
-    where
-   QtoR : Vec Bool (suc  n) →  Vec Bool n ∨ Vec Bool n
-   QtoR ( true ∷ x ) = case1 x
-   QtoR ( false ∷ x ) = case2 x
-   RtoQ : Vec Bool n ∨ Vec Bool n → Vec Bool (suc  n) 
-   RtoQ ( case1 x ) = true ∷ x
-   RtoQ ( case2 x ) = false ∷ x
-   isoRQ : (x : Vec Bool (suc  n) ) → RtoQ ( QtoR x ) ≡ x
-   isoRQ (true ∷ _ ) = refl
-   isoRQ (false ∷ _ ) = refl
-   isoQR : (x : Vec Bool n ∨ Vec Bool n ) → QtoR ( RtoQ x ) ≡ x
-   isoQR (case1 x) = refl
-   isoQR (case2 x) = refl
-   iso : ISO (Vec Bool n ∨ Vec Bool n) (Vec Bool (suc n))
-   iso = record { A←B = QtoR ; B←A = RtoQ ; iso← = isoQR ; iso→ = isoRQ  }
-
-F2L : {Q : Set } {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin) → ( (q : Q) → toℕ (FiniteSet.F←Q fin q ) < n  → Bool ) → Vec Bool n
-F2L  {Q} {zero} fin _ Q→B = []
-F2L  {Q} {suc n} fin (s≤s n<m) Q→B = Q→B (FiniteSet.Q←F fin (fromℕ< n<m)) lemma6 ∷ F2L {Q} fin (NatP.<-trans n<m a<sa ) qb1 where
-   lemma6 : toℕ (FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ< n<m))) < suc n
-   lemma6 = subst (λ k → toℕ k < suc n ) (sym (FiniteSet.finiso← fin _ )) (subst (λ k → k < suc n) (sym (toℕ-fromℕ< n<m ))  a<sa )
-   qb1 : (q : Q) → toℕ (FiniteSet.F←Q fin q) < n → Bool
-   qb1 q q<n = Q→B q (NatP.<-trans q<n a<sa)
-
-List2Func : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin)  → Vec Bool n →  Q → Bool 
-List2Func {Q} {zero} fin (s≤s z≤n) [] q = false
-List2Func {Q} {suc n} fin (s≤s n<m) (h ∷ t) q with  FiniteSet.F←Q fin q ≟ fromℕ< n<m
-... | yes _ = h
-... | no _ = List2Func {Q} fin (NatP.<-trans n<m a<sa ) t q
-
-open import Level renaming ( suc to Suc ; zero to Zero) 
-open import Axiom.Extensionality.Propositional
-postulate f-extensionality : { n : Level}  →  Axiom.Extensionality.Propositional.Extensionality n n 
-
-F2L-iso : { Q : Set } → (fin : FiniteSet Q ) → (x : Vec Bool (FiniteSet.finite fin) ) → F2L fin a<sa (λ q _ → List2Func fin a<sa x q ) ≡ x
-F2L-iso {Q} fin x = f2l m a<sa x where
-  m = FiniteSet.finite fin
-  f2l : (n : ℕ ) → (n<m : n < suc m )→ (x : Vec Bool n ) → F2L fin n<m (λ q q<n → List2Func fin n<m x q )  ≡ x 
-  f2l zero (s≤s z≤n) [] = refl
-  f2l (suc n) (s≤s n<m) (h ∷ t ) = lemma1 lemma2 lemma3 where
-    lemma1 : {n : ℕ } → {h h1 : Bool } → {t t1 : Vec Bool n } → h ≡ h1 → t ≡ t1 →  h ∷ t ≡ h1 ∷ t1
-    lemma1 refl refl = refl
-    lemma2 : List2Func fin (s≤s n<m) (h ∷ t) (FiniteSet.Q←F fin (fromℕ< n<m)) ≡ h
-    lemma2 with FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ< n<m))  ≟ fromℕ< n<m
-    lemma2 | yes p = refl
-    lemma2 | no ¬p = ⊥-elim ( ¬p (FiniteSet.finiso← fin _) )
-    lemma4 : (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → List2Func fin (s≤s n<m) (h ∷ t) q ≡ List2Func fin (NatP.<-trans n<m a<sa) t q
-    lemma4 q _ with FiniteSet.F←Q fin q ≟ fromℕ< n<m 
-    lemma4 q lt | yes p = ⊥-elim ( nat-≡< (toℕ-fromℕ< n<m) (lemma5 n lt (cong (λ k → toℕ k) p))) where 
-        lemma5 : {j k : ℕ } → ( n : ℕ) → suc j ≤ n → j ≡ k → k < n
-        lemma5 {zero} (suc n) (s≤s z≤n) refl = s≤s  z≤n
-        lemma5 {suc j} (suc n) (s≤s lt) refl = s≤s (lemma5 {j} n lt refl)
-    lemma4 q _ | no ¬p = refl
-    lemma3 :  F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q  ) ≡ t
-    lemma3 = begin 
-         F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q )
-       ≡⟨ cong (λ k → F2L fin (NatP.<-trans n<m a<sa) ( λ q q<n → k q q<n ))
-              (f-extensionality ( λ q →  
-              (f-extensionality ( λ q<n →  lemma4 q q<n )))) ⟩
-         F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (NatP.<-trans n<m a<sa) t q )
-       ≡⟨ f2l n (NatP.<-trans n<m a<sa ) t ⟩
-         t
-       ∎  where
-         open ≡-Reasoning
-
-
-L2F : {Q : Set } {n : ℕ } → (fin : FiniteSet Q )  → n < suc (FiniteSet.finite fin) → Vec Bool n → (q :  Q ) → toℕ (FiniteSet.F←Q fin q ) < n  → Bool
-L2F fin n<m x q q<n = List2Func fin n<m x q 
-
-L2F-iso : { Q : Set } → (fin : FiniteSet Q ) → (f : Q → Bool ) → (q : Q ) → (L2F fin a<sa (F2L fin a<sa (λ q _ → f q) )) q (toℕ<n _) ≡ f q
-L2F-iso {Q} fin f q = l2f m a<sa (toℕ<n _) where
-  m = FiniteSet.finite fin
-  lemma11 : {n : ℕ } → (n<m : n < m )  → ¬ ( FiniteSet.F←Q fin q ≡ fromℕ< n<m ) → toℕ (FiniteSet.F←Q fin q) ≤ n → toℕ (FiniteSet.F←Q fin q) < n
-  lemma11  n<m ¬q=n q≤n = lemma13 n<m (contra-position (lemma12 n<m _) ¬q=n ) q≤n where
-     lemma13 : {n nq : ℕ } → (n<m : n < m )  → ¬ ( nq ≡ n ) → nq  ≤ n → nq < n
-     lemma13 {0} {0} (s≤s z≤n) nt z≤n = ⊥-elim ( nt refl )
-     lemma13 {suc _} {0} (s≤s (s≤s n<m)) nt z≤n = s≤s z≤n
-     lemma13 {suc n} {suc nq} n<m nt (s≤s nq≤n) = s≤s (lemma13 {n} {nq} (NatP.<-trans a<sa n<m ) (λ eq → nt ( cong ( λ k → suc k ) eq )) nq≤n)
-     lemma3 : {a b : ℕ } → (lt : a < b ) → fromℕ< (s≤s lt) ≡ suc (fromℕ< lt)
-     lemma3 (s≤s lt) = refl
-     lemma12 : {n m : ℕ } → (n<m : n < m ) → (f : Fin m )  → toℕ f ≡ n → f ≡ fromℕ< n<m 
-     lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl
-     lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl = subst ( λ k → suc f ≡ k ) (sym (lemma3 n<m) ) ( cong ( λ k → suc k ) ( lemma12 {n} {m} n<m f refl  ) )
-  l2f :  (n : ℕ ) → (n<m : n < suc m ) → (q<n : toℕ (FiniteSet.F←Q fin q ) < n )  →  (L2F fin n<m (F2L fin n<m  (λ 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 = 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 ))
-     ≡⟨ cong ( λ k → f k ) (FiniteSet.finiso→ fin _ ) ⟩
-        f q 
-     ∎  where
-       open ≡-Reasoning
-  l2f (suc n) (s≤s n<m) (s≤s n<q) | no ¬p = l2f n (NatP.<-trans n<m a<sa) (lemma11 n<m ¬p n<q)
-
-fin→ : {A : Set} → FiniteSet A → FiniteSet (A → Bool ) 
-fin→ {A}  fin = iso-fin fin2List iso where
-    a = FiniteSet.finite fin
-    iso : ISO (Vec Bool a ) (A → Bool)
-    ISO.A←B iso x = F2L fin a<sa ( λ q _ → x q )
-    ISO.B←A iso x = List2Func fin a<sa x 
-    ISO.iso← iso x  =  F2L-iso fin x 
-    ISO.iso→ iso x = lemma where
-      lemma : List2Func fin a<sa (F2L fin a<sa (λ q _ → x q)) ≡ x
-      lemma = f-extensionality ( λ q → L2F-iso fin x q )
-    
-
-Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n) 
-Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl }
-
-data fin-less { n : ℕ } { A : Set }  (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa ) : Set where
-  elm1 : (elm : A ) → toℕ (FiniteSet.F←Q fa elm ) < n → fin-less fa n<m 
-
-get-elm : { n : ℕ }  { A : Set } {fa : FiniteSet A } {n<m : n < FiniteSet.finite fa } → fin-less fa n<m → A
-get-elm (elm1 a _ ) = a
-
-get-< : { n : ℕ }  { A : Set } {fa : FiniteSet A } {n<m : n < FiniteSet.finite fa }→ (f : fin-less fa n<m ) → toℕ (FiniteSet.F←Q fa (get-elm f )) < n
-get-< (elm1 _ b ) = b
-
-fin-less-cong : { n : ℕ }  { A : Set } (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa )
-   → (x y : fin-less fa n<m ) → get-elm {n} {A} {fa} x ≡ get-elm {n} {A} {fa} y → get-< x ≅  get-< y → x ≡ y
-fin-less-cong fa n<m (elm1 elm x) (elm1 elm x) refl HE.refl = refl
-
-fin-< : {A : Set} → { n : ℕ } → (fa : FiniteSet A ) → (n<m : n < FiniteSet.finite fa ) → FiniteSet (fin-less fa n<m ) 
-fin-< {A}  {n} fa n<m = iso-fin (Fin2Finite n) iso where
-    m = FiniteSet.finite fa
-    iso : ISO (Fin n) (fin-less fa n<m )
-    lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
-    lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
-    lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i}  refl  )
-    lemma10 : {n i j  : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n }  → fromℕ< i<n ≡ fromℕ< j<n
-    lemma10  refl  = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8 refl  ))
-    lemma3 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
-    lemma3 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl) 
-    lemma11 : {n : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
-    lemma11 {n} {x} n<m  = begin
-         toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m))
-      ≡⟨ toℕ-fromℕ< _ ⟩
-         toℕ x
-      ∎  where
-          open ≡-Reasoning
-    ISO.A←B iso (elm1 elm x) = fromℕ< x
-    ISO.B←A iso x = elm1 (FiniteSet.Q←F fa (fromℕ< (NatP.<-trans x<n n<m ))) to<n where
-      x<n : toℕ x < n
-      x<n = toℕ<n x
-      to<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ< (NatP.<-trans x<n n<m)))) < n
-      to<n = subst (λ k → toℕ k < n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k < n ) (sym ( toℕ-fromℕ< (NatP.<-trans x<n n<m) )) x<n )
-    ISO.iso← iso x  = lemma2 where
-      lemma2 : fromℕ< (subst (λ k → toℕ k < n) (sym
-       (FiniteSet.finiso← fa (fromℕ< (NatP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
-       (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) ≡ x
-      lemma2 = begin
-        fromℕ< (subst (λ k → toℕ k < n) (sym
-          (FiniteSet.finiso← fa (fromℕ< (NatP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
-               (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) 
-        ≡⟨⟩
-           fromℕ< ( subst (λ k → toℕ ( k ) < n ) (sym (FiniteSet.finiso← fa _ )) lemma6 )
-        ≡⟨ lemma10 (cong (λ k → toℕ k) (FiniteSet.finiso← fa _ ) ) ⟩
-           fromℕ< lemma6
-        ≡⟨ lemma10 (lemma11 n<m ) ⟩
-           fromℕ< ( toℕ<n x )
-        ≡⟨ fromℕ<-toℕ _ _ ⟩
-           x 
-        ∎  where
-          open ≡-Reasoning
-          lemma6 : toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) < n
-          lemma6 = subst ( λ k → k < n ) (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x )
-    ISO.iso→ iso (elm1 elm x) = fin-less-cong fa n<m _ _ lemma (lemma8 (cong (λ k → toℕ (FiniteSet.F←Q fa k) ) lemma ) ) where
-      lemma13 : toℕ (fromℕ< x) ≡ toℕ (FiniteSet.F←Q fa elm)
-      lemma13 = begin
-            toℕ (fromℕ< x)
-         ≡⟨ toℕ-fromℕ< _ ⟩
-            toℕ (FiniteSet.F←Q fa elm)
-         ∎  where open ≡-Reasoning
-      lemma : FiniteSet.Q←F fa (fromℕ< (NatP.<-trans (toℕ<n (ISO.A←B iso (elm1 elm x))) n<m)) ≡ elm 
-      lemma = begin
-           FiniteSet.Q←F fa (fromℕ< (NatP.<-trans (toℕ<n (ISO.A←B iso (elm1 elm x))) n<m))
-         ≡⟨⟩
-           FiniteSet.Q←F fa (fromℕ< ( NatP.<-trans (toℕ<n ( fromℕ< x ) ) n<m))
-         ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma10 lemma13 ) ⟩
-            FiniteSet.Q←F fa (fromℕ< ( NatP.<-trans x n<m))
-         ≡⟨ cong (λ k → FiniteSet.Q←F fa (fromℕ< k ))  lemma3 ⟩
-           FiniteSet.Q←F fa (fromℕ< ( toℕ<n (FiniteSet.F←Q fa elm)))
-         ≡⟨ cong (λ k → FiniteSet.Q←F fa k ) ( fromℕ<-toℕ _ _ ) ⟩
-           FiniteSet.Q←F fa (FiniteSet.F←Q fa elm )
-         ≡⟨ FiniteSet.finiso→ fa _ ⟩
-            elm 
-         ∎  where open ≡-Reasoning
-
-
--- a/agda/automaton-ex.agda	Mon Jan 04 13:20:31 2021 +0900
+++ b/agda/automaton-ex.agda	Wed Jan 13 10:52:01 2021 +0900
@@ -74,10 +74,3 @@
 ieq i0 i1 = no ( λ () )
 ieq i1 i0 = no ( λ () )
 
-inputnn : { n :  ℕ }  →  { Σ : Set  } → ( x y : Σ )  → List  Σ → List  Σ 
-inputnn {zero} {_} _ _ s = s
-inputnn {suc n} x y s = x  ∷ ( inputnn {n} x y ( y  ∷ s ) )
-
--- lemmaNN :  { Q : Set } { Σ : Set  } → (M : Automaton Q  Σ) →  ¬ accept M ( inputnn {n} x y [] )
--- lemmaNN = ?
-
--- a/agda/cfg1.agda	Mon Jan 04 13:20:31 2021 +0900
+++ b/agda/cfg1.agda	Wed Jan 13 10:52:01 2021 +0900
@@ -10,6 +10,13 @@
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 
+--
+--   Java → Java Byte Code
+--
+--   CFG    Stack Machine (PDA)
+--
+
+
 data Node (Symbol  : Set) : Set where
     T : Symbol → Node Symbol 
     N : Symbol → Node Symbol 
--- a/agda/chap0.agda	Mon Jan 04 13:20:31 2021 +0900
+++ b/agda/chap0.agda	Wed Jan 13 10:52:01 2021 +0900
@@ -86,6 +86,18 @@
 --
 --  _≟_ :  (s t : ℕ ) → Dec ( s ≡ t )
 
+-- ¬ A = A → ⊥
+
+_n≟_ :  (s t : ℕ ) → Dec ( s ≡ t )
+zero n≟ zero = yes refl
+zero n≟ suc t = no (λ ())
+suc s n≟ zero = no (λ ())
+suc s n≟ suc t with s n≟ t 
+... | yes refl = yes refl
+... | no n = no (λ k → n (tt1 k) )  where
+   tt1 : suc s ≡ suc t → s ≡ t
+   tt1 refl = refl
+
 open import Data.Bool  hiding ( _≟_ )
 
 conn : List ( ℕ × ℕ ) → ℕ → ℕ → Bool
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/fin.agda	Wed Jan 13 10:52:01 2021 +0900
@@ -0,0 +1,117 @@
+{-# OPTIONS --allow-unsolved-metas #-} 
+
+module fin where
+
+open import Data.Fin hiding (_<_ ; _≤_ )
+open import Data.Fin.Properties hiding ( <-trans )
+open import Data.Nat
+open import logic
+open import nat
+open import Relation.Binary.PropositionalEquality
+
+
+-- toℕ<n
+fin<n : {n : ℕ} {f : Fin n} → toℕ f < n
+fin<n {_} {zero} = s≤s z≤n
+fin<n {suc n} {suc f} = s≤s (fin<n {n} {f})
+
+-- toℕ≤n
+fin≤n : {n : ℕ} (f : Fin (suc n)) → toℕ f ≤ n
+fin≤n {_} zero = z≤n
+fin≤n {suc n} (suc f) = s≤s (fin≤n {n} f)
+
+pred<n : {n : ℕ} {f : Fin (suc n)} → n > 0  → Data.Nat.pred (toℕ f) < n
+pred<n {suc n} {zero} (s≤s z≤n) = s≤s z≤n
+pred<n {suc n} {suc f} (s≤s z≤n) = fin<n
+
+fin<asa : {n : ℕ} → toℕ (fromℕ< {n} a<sa) ≡ n
+fin<asa = toℕ-fromℕ< nat.a<sa
+
+-- fromℕ<-toℕ
+toℕ→from : {n : ℕ} {x : Fin (suc n)} → toℕ x ≡ n → fromℕ n ≡ x
+toℕ→from {0} {zero} refl = refl
+toℕ→from {suc n} {suc x} eq = cong (λ k → suc k ) ( toℕ→from {n} {x} (cong (λ k → Data.Nat.pred k ) eq ))
+
+0≤fmax : {n : ℕ } → (# 0) Data.Fin.≤ fromℕ< {n} a<sa
+0≤fmax  = subst (λ k → 0 ≤ k ) (sym (toℕ-fromℕ< a<sa)) z≤n
+
+0<fmax : {n : ℕ } → (# 0) Data.Fin.< fromℕ< {suc n} a<sa
+0<fmax = subst (λ k → 0 < k ) (sym (toℕ-fromℕ< a<sa)) (s≤s z≤n)
+
+-- toℕ-injective
+i=j : {n : ℕ} (i j : Fin n) → toℕ i ≡ toℕ j → i ≡ j
+i=j {suc n} zero zero refl = refl
+i=j {suc n} (suc i) (suc j) eq = cong ( λ k → suc k ) ( i=j i j (cong ( λ k → Data.Nat.pred k ) eq) )
+
+-- raise 1
+fin+1 :  { n : ℕ } → Fin n → Fin (suc n)
+fin+1  zero = zero 
+fin+1  (suc x) = suc (fin+1 x)
+
+open import Data.Nat.Properties as NatP  hiding ( _≟_ )
+
+fin+1≤ : { i n : ℕ } → (a : i < n)  → fin+1 (fromℕ< a) ≡ fromℕ< (<-trans a a<sa)
+fin+1≤ {0} {suc i} (s≤s z≤n) = refl
+fin+1≤ {suc n} {suc (suc i)} (s≤s (s≤s a)) = cong (λ k → suc k ) ( fin+1≤ {n} {suc i} (s≤s a) )
+
+fin+1-toℕ : { n : ℕ } → { x : Fin n} → toℕ (fin+1 x) ≡ toℕ x
+fin+1-toℕ {suc n} {zero} = refl
+fin+1-toℕ {suc n} {suc x} = cong (λ k → suc k ) (fin+1-toℕ {n} {x})
+
+open import Relation.Nullary 
+open import Data.Empty
+
+fin-1 :  { n : ℕ } → (x : Fin (suc n)) → ¬ (x ≡ zero )  → Fin n
+fin-1 zero ne = ⊥-elim (ne refl )
+fin-1 {n} (suc x) ne = x 
+
+fin-1-sx : { n : ℕ } → (x : Fin n) →  fin-1 (suc x) (λ ()) ≡ x 
+fin-1-sx zero = refl
+fin-1-sx (suc x) = refl
+
+fin-1-xs : { n : ℕ } → (x : Fin (suc n)) → (ne : ¬ (x ≡ zero ))  → suc (fin-1 x ne ) ≡ x
+fin-1-xs zero ne = ⊥-elim ( ne refl )
+fin-1-xs (suc x) ne = refl
+
+-- suc-injective
+-- suc-eq : {n : ℕ } {x y : Fin n} → Fin.suc x ≡ Fin.suc y  → x ≡ y
+-- suc-eq {n} {x} {y} eq = subst₂ (λ j k → j ≡ k ) {!!} {!!} (cong (λ k → Data.Fin.pred k ) eq )
+
+-- this is refl
+lemma3 : {a b : ℕ } → (lt : a < b ) → fromℕ< (s≤s lt) ≡ suc (fromℕ< lt)
+lemma3 (s≤s lt) = refl
+
+-- fromℕ<-toℕ 
+lemma12 : {n m : ℕ } → (n<m : n < m ) → (f : Fin m )  → toℕ f ≡ n → f ≡ fromℕ< n<m 
+lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl
+lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl =  cong suc ( lemma12 {n} {m} n<m f refl  ) 
+
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+open import Data.Fin.Properties
+
+-- <-irrelevant
+<-nat=irr : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
+<-nat=irr {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
+<-nat=irr {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( <-nat=irr {i} {i} {n} refl  )
+
+lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
+lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
+lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i} {n} refl  )
+
+-- fromℕ<-irrelevant 
+lemma10 : {n i j  : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n }  → fromℕ< i<n ≡ fromℕ< j<n
+lemma10 {n} refl  = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8 refl  ))
+
+lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
+lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl) 
+
+-- toℕ-fromℕ<
+lemma11 : {n m : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
+lemma11 {n} {m} {x} n<m  = begin
+              toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m))
+           ≡⟨ toℕ-fromℕ< _ ⟩
+              toℕ x
+           ∎  where
+               open ≡-Reasoning
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/finiteSetUtil.agda	Wed Jan 13 10:52:01 2021 +0900
@@ -0,0 +1,461 @@
+{-# OPTIONS --allow-unsolved-metas #-} 
+
+module finiteSetUtil  where
+
+open import Data.Nat hiding ( _≟_ )
+open import Data.Fin renaming ( _<_ to _<<_ ) hiding (_≤_)
+open import Data.Fin.Properties
+open import Data.Empty
+open import Relation.Nullary
+open import Relation.Binary.Definitions
+open import Relation.Binary.PropositionalEquality
+open import logic
+open import nat
+open import finiteSet
+open import fin
+open import Data.Nat.Properties as NatP  hiding ( _≟_ )
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+
+record Found ( Q : Set ) (p : Q → Bool ) : Set where
+     field
+       found-q : Q
+       found-p : p found-q ≡ true
+
+module _ {Q : Set } (F : FiniteSet Q) where
+     open FiniteSet F
+     equal→refl  : { x y : Q } → equal? x y ≡ true → x ≡ y
+     equal→refl {q0} {q1} eq with F←Q q0 ≟ F←Q q1
+     equal→refl {q0} {q1} refl | yes eq = begin
+            q0
+        ≡⟨ sym ( finiso→ q0) ⟩
+            Q←F (F←Q q0)
+        ≡⟨ cong (λ k → Q←F k ) eq ⟩
+            Q←F (F←Q q1)
+        ≡⟨ finiso→ q1 ⟩
+            q1
+        ∎  where open ≡-Reasoning
+     End : (m : ℕ ) → (p : Q → Bool ) → Set
+     End m p = (i : Fin finite) → m ≤ toℕ i → p (Q←F i )  ≡ false 
+     first-end :  ( p : Q → Bool ) → End finite p
+     first-end p i i>n = ⊥-elim (nat-≤> i>n (fin<n {finite} {i}) )
+     next-end : {m : ℕ } → ( p : Q → Bool ) → End (suc m) p
+              → (m<n : m < finite ) → p (Q←F (fromℕ< m<n )) ≡ false
+              → End m p
+     next-end {m} p prev m<n np i m<i with NatP.<-cmp m (toℕ i) 
+     next-end p prev m<n np i m<i | tri< a ¬b ¬c = prev i a
+     next-end p prev m<n np i m<i | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<i c )
+     next-end {m} p prev m<n np i m<i | tri≈ ¬a b ¬c = subst ( λ k → p (Q←F k) ≡ false) (m<n=i i b m<n ) np where
+              m<n=i : {n : ℕ } (i : Fin n) {m : ℕ } → m ≡ (toℕ i) → (m<n : m < n )  → fromℕ< m<n ≡ i
+              m<n=i i eq m<n = {!!} -- toℕ-inject (fromℕ≤ ?) i (subst (λ k → k ≡ toℕ i) (sym (toℕ-fromℕ≤ m<n)) eq )
+     found : { p : Q → Bool } → (q : Q ) → p q ≡ true → exists p ≡ true
+     found {p} q pt = found1 finite  (NatP.≤-refl ) ( first-end p ) where
+         found1 : (m : ℕ ) (m<n : m Data.Nat.≤ finite ) → ((i : Fin finite) → m ≤ toℕ i → p (Q←F i )  ≡ false ) →  exists1 m m<n p ≡ true
+         found1 0 m<n end = ⊥-elim ( ¬-bool (subst (λ k → k ≡ false ) (cong (λ k → p k) (finiso→ q) ) (end (F←Q q) z≤n )) pt )
+         found1 (suc m)  m<n end with bool-≡-? (p (Q←F (fromℕ< m<n))) true
+         found1 (suc m)  m<n end | yes eq = subst (λ k → k \/ exists1 m (≤to<  m<n) p ≡ true ) (sym eq) (bool-or-4 {exists1 m (≤to<  m<n) p} ) 
+         found1 (suc m)  m<n end | no np = begin
+                 p (Q←F (fromℕ< m<n)) \/ exists1 m (≤to<  m<n) p
+              ≡⟨ bool-or-1 (¬-bool-t np ) ⟩
+                 exists1 m (≤to<  m<n) p
+              ≡⟨ found1 m (≤to<  m<n) (next-end p end m<n (¬-bool-t np )) ⟩
+                 true
+              ∎  where open ≡-Reasoning
+
+
+
+record ISO (A B : Set) : Set where
+   field
+     A←B : B → A
+     B←A : A → B
+     iso← : (q : A) → A←B ( B←A q ) ≡ q
+     iso→ : (f : B) → B←A ( A←B f ) ≡ f
+
+iso-fin : {A B : Set} → FiniteSet A  → ISO A B → FiniteSet B 
+iso-fin {A} {B}  fin iso = record {
+   Q←F = λ f → ISO.B←A iso ( FiniteSet.Q←F fin f )
+ ; F←Q = λ b → FiniteSet.F←Q fin ( ISO.A←B iso b )
+ ; finiso→ = finiso→ 
+ ; finiso← = finiso← 
+   } where
+   finiso→ : (q : B) → ISO.B←A iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (ISO.A←B iso q))) ≡ q
+   finiso→ q = begin
+              ISO.B←A iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (ISO.A←B iso q))) 
+           ≡⟨ cong (λ k → ISO.B←A iso k ) (FiniteSet.finiso→ fin _ ) ⟩
+              ISO.B←A iso (ISO.A←B iso q)
+           ≡⟨ ISO.iso→ iso _ ⟩
+              q
+           ∎  where
+           open ≡-Reasoning
+   finiso← : (f : Fin (FiniteSet.finite fin ))→ FiniteSet.F←Q fin (ISO.A←B iso (ISO.B←A iso (FiniteSet.Q←F fin f))) ≡ f
+   finiso← f = begin
+              FiniteSet.F←Q fin (ISO.A←B iso (ISO.B←A iso (FiniteSet.Q←F fin f))) 
+           ≡⟨ cong (λ k → FiniteSet.F←Q fin k ) (ISO.iso← iso _) ⟩
+              FiniteSet.F←Q fin (FiniteSet.Q←F fin f) 
+           ≡⟨ FiniteSet.finiso← fin _  ⟩
+              f
+           ∎  where
+           open ≡-Reasoning
+
+data One : Set where
+   one : One
+
+fin-∨1 : {B : Set} → (fb : FiniteSet B ) → FiniteSet (One ∨ B) 
+fin-∨1 {B} fb =  record {
+   Q←F = Q←F
+ ; F←Q =  F←Q
+ ; finiso→ = finiso→
+ ; finiso← = finiso←
+   }  where
+   b = FiniteSet.finite fb
+   Q←F : Fin (suc b) → One ∨ B
+   Q←F zero = case1 one
+   Q←F (suc f) = case2 (FiniteSet.Q←F fb f)
+   F←Q : One ∨ B → Fin (suc b)
+   F←Q (case1 one) = zero
+   F←Q (case2 f ) = suc (FiniteSet.F←Q fb f) 
+   finiso→ : (q : One ∨ B) → Q←F (F←Q q) ≡ q
+   finiso→ (case1 one) = refl
+   finiso→ (case2 b) = cong (λ k → case2 k ) (FiniteSet.finiso→ fb b)
+   finiso← : (q : Fin (suc b)) → F←Q (Q←F q) ≡ q
+   finiso← zero = refl
+   finiso← (suc f) = cong ( λ k → suc k ) (FiniteSet.finiso← fb f)
+
+
+fin-∨2 : {B : Set} → ( a : ℕ ) → FiniteSet B  → FiniteSet (Fin a ∨ B) 
+fin-∨2 {B} zero  fb = iso-fin fb iso where
+   iso : ISO B (Fin zero ∨ B)
+   iso =  record {
+        A←B = A←B
+      ; B←A = λ b → case2 b
+      ; iso→ = iso→
+      ; iso← = λ _ → refl
+    } where
+     A←B : Fin zero ∨ B → B
+     A←B (case2 x) = x 
+     iso→ : (f : Fin zero ∨ B ) → case2 (A←B f) ≡ f
+     iso→ (case2 x)  = refl
+fin-∨2 {B} (suc a) fb =  iso-fin (fin-∨1 (fin-∨2 a fb) ) iso
+    where
+  iso : ISO (One ∨ (Fin a ∨ B) ) (Fin (suc a) ∨ B)
+  ISO.A←B iso (case1 zero) = case1 one
+  ISO.A←B iso (case1 (suc f)) = case2 (case1 f)
+  ISO.A←B iso (case2 b) = case2 (case2 b)
+  ISO.B←A iso (case1 one) = case1 zero
+  ISO.B←A iso (case2 (case1 f)) = case1 (suc f)
+  ISO.B←A iso (case2 (case2 b)) = case2 b
+  ISO.iso← iso (case1 one) = refl
+  ISO.iso← iso (case2 (case1 x)) = refl
+  ISO.iso← iso (case2 (case2 x)) = refl
+  ISO.iso→ iso (case1 zero) = refl
+  ISO.iso→ iso (case1 (suc x)) = refl
+  ISO.iso→ iso (case2 x) = refl
+
+
+FiniteSet→Fin : {A : Set} → (fin : FiniteSet A  ) → ISO (Fin (FiniteSet.finite fin)) A
+ISO.A←B (FiniteSet→Fin fin) f = FiniteSet.F←Q fin f
+ISO.B←A (FiniteSet→Fin fin) f = FiniteSet.Q←F fin f
+ISO.iso← (FiniteSet→Fin fin) = FiniteSet.finiso← fin
+ISO.iso→ (FiniteSet→Fin fin) =  FiniteSet.finiso→ fin
+   
+
+fin-∨ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∨ B) 
+fin-∨ {A} {B}  fa fb = iso-fin (fin-∨2 a  fb ) iso2 where
+    a = FiniteSet.finite fa
+    ia = FiniteSet→Fin fa
+    iso2 : ISO (Fin a ∨ B ) (A ∨ B)
+    ISO.A←B iso2 (case1 x) = case1 ( ISO.A←B ia x )
+    ISO.A←B iso2 (case2 x) = case2 x
+    ISO.B←A iso2 (case1 x) = case1 ( ISO.B←A ia x )
+    ISO.B←A iso2 (case2 x) = case2 x
+    ISO.iso← iso2 (case1 x) = cong ( λ k → case1 k ) (ISO.iso← ia x)
+    ISO.iso← iso2 (case2 x) = refl
+    ISO.iso→ iso2 (case1 x) = cong ( λ k → case1 k ) (ISO.iso→ ia x)
+    ISO.iso→ iso2 (case2 x) = refl
+
+open import Data.Product
+
+fin-× : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A × B) 
+fin-× {A} {B}  fa fb with FiniteSet→Fin fa
+... | a=f = iso-fin (fin-×-f a ) iso-1 where
+   a = FiniteSet.finite fa
+   b = FiniteSet.finite fb
+   iso-1 : ISO (Fin a × B) ( A × B )
+   ISO.A←B iso-1 x = ( FiniteSet.F←Q fa (proj₁ x)  , proj₂ x) 
+   ISO.B←A iso-1 x = ( FiniteSet.Q←F fa (proj₁ x)  , proj₂ x) 
+   ISO.iso← iso-1 x  =  lemma  where
+     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 )
+   ISO.B←A iso-2 (case1 b) = ( zero , b )
+   ISO.B←A iso-2 (case2 (a , b )) = ( suc a , b )
+   ISO.iso← iso-2 (case1 x) = refl
+   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) 
+   fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () ; finite = 0 }
+   fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2
+
+open _∧_
+
+fin-∧ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∧ B) 
+fin-∧ {A} {B} fa fb with FiniteSet→Fin fa    -- same thing for our tool
+... | a=f = iso-fin (fin-×-f a ) iso-1 where
+   a = FiniteSet.finite fa
+   b = FiniteSet.finite fb
+   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} 
+   ISO.B←A iso-1 x = record { proj1 = FiniteSet.Q←F fa (proj1 x)  ; proj2 =  proj2 x}
+   ISO.iso← iso-1 x  =  lemma  where
+     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 } )
+   ISO.B←A iso-2 (case1 b) = record {proj1 =  zero ; proj2 =  b }
+   ISO.B←A iso-2 (case2 (record { proj1 = a ; proj2 =  b })) = record { proj1 =  suc a ; proj2 =  b }
+   ISO.iso← iso-2 (case1 x) = refl
+   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) 
+   fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () ; finite = 0 }
+   fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2
+
+-- import Data.Nat.DivMod
+
+open import Data.Vec
+import Data.Product
+
+exp2 : (n : ℕ ) → exp 2 (suc n) ≡ exp 2 n Data.Nat.+ exp 2 n
+exp2 n = begin
+      exp 2 (suc n)
+   ≡⟨⟩
+      2 * ( exp 2 n )
+   ≡⟨ *-comm 2 (exp 2 n)  ⟩
+      ( exp 2 n ) * 2
+   ≡⟨ *-suc ( exp 2 n ) 1 ⟩
+      (exp 2 n ) Data.Nat.+ ( exp 2 n ) * 1
+   ≡⟨ cong ( λ k →  (exp 2 n ) Data.Nat.+  k ) (proj₂ *-identity (exp 2 n) ) ⟩
+      exp 2 n Data.Nat.+ exp 2 n
+   ∎  where
+       open ≡-Reasoning
+       open Data.Product
+
+cast-iso : {n m : ℕ } → (eq : n ≡ m ) → (f : Fin m ) → cast eq ( cast (sym eq ) f)  ≡ f
+cast-iso refl zero =  refl
+cast-iso refl (suc f) = cong ( λ k → suc k ) ( cast-iso refl f )
+
+
+fin2List : {n : ℕ } → FiniteSet (Vec Bool n) 
+fin2List {zero} = record {
+   Q←F = λ _ → Vec.[]
+ ; F←Q =  λ _ → # 0
+ ; finiso→ = finiso→ 
+ ; finiso← = finiso← 
+   } where
+   Q = Vec Bool zero
+   finiso→ : (q : Q) → [] ≡ q
+   finiso→ [] = refl
+   finiso← : (f : Fin (exp 2 zero)) → # 0 ≡ f
+   finiso← zero = refl
+fin2List {suc n} = subst (λ k → FiniteSet (Vec Bool (suc n)) ) (sym (exp2 n)) ( iso-fin (fin-∨ (fin2List ) (fin2List )) iso )
+    where
+   QtoR : Vec Bool (suc  n) →  Vec Bool n ∨ Vec Bool n
+   QtoR ( true ∷ x ) = case1 x
+   QtoR ( false ∷ x ) = case2 x
+   RtoQ : Vec Bool n ∨ Vec Bool n → Vec Bool (suc  n) 
+   RtoQ ( case1 x ) = true ∷ x
+   RtoQ ( case2 x ) = false ∷ x
+   isoRQ : (x : Vec Bool (suc  n) ) → RtoQ ( QtoR x ) ≡ x
+   isoRQ (true ∷ _ ) = refl
+   isoRQ (false ∷ _ ) = refl
+   isoQR : (x : Vec Bool n ∨ Vec Bool n ) → QtoR ( RtoQ x ) ≡ x
+   isoQR (case1 x) = refl
+   isoQR (case2 x) = refl
+   iso : ISO (Vec Bool n ∨ Vec Bool n) (Vec Bool (suc n))
+   iso = record { A←B = QtoR ; B←A = RtoQ ; iso← = isoQR ; iso→ = isoRQ  }
+
+F2L : {Q : Set } {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin) → ( (q : Q) → toℕ (FiniteSet.F←Q fin q ) < n  → Bool ) → Vec Bool n
+F2L  {Q} {zero} fin _ Q→B = []
+F2L  {Q} {suc n} fin (s≤s n<m) Q→B = Q→B (FiniteSet.Q←F fin (fromℕ< n<m)) lemma6 ∷ F2L {Q} fin (NatP.<-trans n<m a<sa ) qb1 where
+   lemma6 : toℕ (FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ< n<m))) < suc n
+   lemma6 = subst (λ k → toℕ k < suc n ) (sym (FiniteSet.finiso← fin _ )) (subst (λ k → k < suc n) (sym (toℕ-fromℕ< n<m ))  a<sa )
+   qb1 : (q : Q) → toℕ (FiniteSet.F←Q fin q) < n → Bool
+   qb1 q q<n = Q→B q (NatP.<-trans q<n a<sa)
+
+List2Func : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin)  → Vec Bool n →  Q → Bool 
+List2Func {Q} {zero} fin (s≤s z≤n) [] q = false
+List2Func {Q} {suc n} fin (s≤s n<m) (h ∷ t) q with  FiniteSet.F←Q fin q ≟ fromℕ< n<m
+... | yes _ = h
+... | no _ = List2Func {Q} fin (NatP.<-trans n<m a<sa ) t q
+
+open import Level renaming ( suc to Suc ; zero to Zero) 
+open import Axiom.Extensionality.Propositional
+postulate f-extensionality : { n : Level}  →  Axiom.Extensionality.Propositional.Extensionality n n 
+
+F2L-iso : { Q : Set } → (fin : FiniteSet Q ) → (x : Vec Bool (FiniteSet.finite fin) ) → F2L fin a<sa (λ q _ → List2Func fin a<sa x q ) ≡ x
+F2L-iso {Q} fin x = f2l m a<sa x where
+  m = FiniteSet.finite fin
+  f2l : (n : ℕ ) → (n<m : n < suc m )→ (x : Vec Bool n ) → F2L fin n<m (λ q q<n → List2Func fin n<m x q )  ≡ x 
+  f2l zero (s≤s z≤n) [] = refl
+  f2l (suc n) (s≤s n<m) (h ∷ t ) = lemma1 lemma2 lemma3f where
+    lemma1 : {n : ℕ } → {h h1 : Bool } → {t t1 : Vec Bool n } → h ≡ h1 → t ≡ t1 →  h ∷ t ≡ h1 ∷ t1
+    lemma1 refl refl = refl
+    lemma2 : List2Func fin (s≤s n<m) (h ∷ t) (FiniteSet.Q←F fin (fromℕ< n<m)) ≡ h
+    lemma2 with FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ< n<m))  ≟ fromℕ< n<m
+    lemma2 | yes p = refl
+    lemma2 | no ¬p = ⊥-elim ( ¬p (FiniteSet.finiso← fin _) )
+    lemma4 : (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → List2Func fin (s≤s n<m) (h ∷ t) q ≡ List2Func fin (NatP.<-trans n<m a<sa) t q
+    lemma4 q _ with FiniteSet.F←Q fin q ≟ fromℕ< n<m 
+    lemma4 q lt | yes p = ⊥-elim ( nat-≡< (toℕ-fromℕ< n<m) (lemma5 n lt (cong (λ k → toℕ k) p))) where 
+        lemma5 : {j k : ℕ } → ( n : ℕ) → suc j ≤ n → j ≡ k → k < n
+        lemma5 {zero} (suc n) (s≤s z≤n) refl = s≤s  z≤n
+        lemma5 {suc j} (suc n) (s≤s lt) refl = s≤s (lemma5 {j} n lt refl)
+    lemma4 q _ | no ¬p = refl
+    lemma3f :  F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q  ) ≡ t
+    lemma3f = begin 
+         F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q )
+       ≡⟨ cong (λ k → F2L fin (NatP.<-trans n<m a<sa) ( λ q q<n → k q q<n ))
+              (f-extensionality ( λ q →  
+              (f-extensionality ( λ q<n →  lemma4 q q<n )))) ⟩
+         F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (NatP.<-trans n<m a<sa) t q )
+       ≡⟨ f2l n (NatP.<-trans n<m a<sa ) t ⟩
+         t
+       ∎  where
+         open ≡-Reasoning
+
+
+L2F : {Q : Set } {n : ℕ } → (fin : FiniteSet Q )  → n < suc (FiniteSet.finite fin) → Vec Bool n → (q :  Q ) → toℕ (FiniteSet.F←Q fin q ) < n  → Bool
+L2F fin n<m x q q<n = List2Func fin n<m x q 
+
+L2F-iso : { Q : Set } → (fin : FiniteSet Q ) → (f : Q → Bool ) → (q : Q ) → (L2F fin a<sa (F2L fin a<sa (λ q _ → f q) )) q (toℕ<n _) ≡ f q
+L2F-iso {Q} fin f q = l2f m a<sa (toℕ<n _) where
+  m = FiniteSet.finite fin
+  lemma11f : {n : ℕ } → (n<m : n < m )  → ¬ ( FiniteSet.F←Q fin q ≡ fromℕ< n<m ) → toℕ (FiniteSet.F←Q fin q) ≤ n → toℕ (FiniteSet.F←Q fin q) < n
+  lemma11f  n<m ¬q=n q≤n = lemma13 n<m (contra-position (lemma12 n<m _) ¬q=n ) q≤n where
+     lemma13 : {n nq : ℕ } → (n<m : n < m )  → ¬ ( nq ≡ n ) → nq  ≤ n → nq < n
+     lemma13 {0} {0} (s≤s z≤n) nt z≤n = ⊥-elim ( nt refl )
+     lemma13 {suc _} {0} (s≤s (s≤s n<m)) nt z≤n = s≤s z≤n
+     lemma13 {suc n} {suc nq} n<m nt (s≤s nq≤n) = s≤s (lemma13 {n} {nq} (NatP.<-trans a<sa n<m ) (λ eq → nt ( cong ( λ k → suc k ) eq )) nq≤n)
+     lemma3f : {a b : ℕ } → (lt : a < b ) → fromℕ< (s≤s lt) ≡ suc (fromℕ< lt)
+     lemma3f (s≤s lt) = refl
+     lemma12f : {n m : ℕ } → (n<m : n < m ) → (f : Fin m )  → toℕ f ≡ n → f ≡ fromℕ< n<m 
+     lemma12f {zero} {suc m} (s≤s z≤n) zero refl = refl
+     lemma12f {suc n} {suc m} (s≤s n<m) (suc f) refl = subst ( λ k → suc f ≡ k ) (sym (lemma3f n<m) ) ( cong ( λ k → suc k ) ( lemma12f {n} {m} n<m f refl  ) )
+  l2f :  (n : ℕ ) → (n<m : n < suc m ) → (q<n : toℕ (FiniteSet.F←Q fin q ) < n )  →  (L2F fin n<m (F2L fin n<m  (λ 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 = 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 ))
+     ≡⟨ cong ( λ k → f k ) (FiniteSet.finiso→ fin _ ) ⟩
+        f q 
+     ∎  where
+       open ≡-Reasoning
+  l2f (suc n) (s≤s n<m) (s≤s n<q) | no ¬p = l2f n (NatP.<-trans n<m a<sa) (lemma11f n<m ¬p n<q)
+
+fin→ : {A : Set} → FiniteSet A → FiniteSet (A → Bool ) 
+fin→ {A}  fin = iso-fin fin2List iso where
+    a = FiniteSet.finite fin
+    iso : ISO (Vec Bool a ) (A → Bool)
+    ISO.A←B iso x = F2L fin a<sa ( λ q _ → x q )
+    ISO.B←A iso x = List2Func fin a<sa x 
+    ISO.iso← iso x  =  F2L-iso fin x 
+    ISO.iso→ iso x = lemma where
+      lemma : List2Func fin a<sa (F2L fin a<sa (λ q _ → x q)) ≡ x
+      lemma = f-extensionality ( λ q → L2F-iso fin x q )
+    
+
+Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n) 
+Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl }
+
+data fin-less { n : ℕ } { A : Set }  (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa ) : Set where
+  elm1 : (elm : A ) → toℕ (FiniteSet.F←Q fa elm ) < n → fin-less fa n<m 
+
+get-elm : { n : ℕ }  { A : Set } {fa : FiniteSet A } {n<m : n < FiniteSet.finite fa } → fin-less fa n<m → A
+get-elm (elm1 a _ ) = a
+
+get-< : { n : ℕ }  { A : Set } {fa : FiniteSet A } {n<m : n < FiniteSet.finite fa }→ (f : fin-less fa n<m ) → toℕ (FiniteSet.F←Q fa (get-elm f )) < n
+get-< (elm1 _ b ) = b
+
+fin-less-cong : { n : ℕ }  { A : Set } (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa )
+   → (x y : fin-less fa n<m ) → get-elm {n} {A} {fa} x ≡ get-elm {n} {A} {fa} y → get-< x ≅  get-< y → x ≡ y
+fin-less-cong fa n<m (elm1 elm x) (elm1 elm x) refl HE.refl = refl
+
+fin-< : {A : Set} → { n : ℕ } → (fa : FiniteSet A ) → (n<m : n < FiniteSet.finite fa ) → FiniteSet (fin-less fa n<m ) 
+fin-< {A}  {n} fa n<m = iso-fin (Fin2Finite n) iso where
+    m = FiniteSet.finite fa
+    iso : ISO (Fin n) (fin-less fa n<m )
+    lemma8f : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
+    lemma8f {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
+    lemma8f {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8f {i} {i}  refl  )
+    lemma10f : {n i j  : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n }  → fromℕ< i<n ≡ fromℕ< j<n
+    lemma10f  refl  = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8f refl  ))
+    lemma3f : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
+    lemma3f {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8f refl) 
+    lemma11f : {n : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
+    lemma11f {n} {x} n<m  = begin
+         toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m))
+      ≡⟨ toℕ-fromℕ< _ ⟩
+         toℕ x
+      ∎  where
+          open ≡-Reasoning
+    ISO.A←B iso (elm1 elm x) = fromℕ< x
+    ISO.B←A iso x = elm1 (FiniteSet.Q←F fa (fromℕ< (NatP.<-trans x<n n<m ))) to<n where
+      x<n : toℕ x < n
+      x<n = toℕ<n x
+      to<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ< (NatP.<-trans x<n n<m)))) < n
+      to<n = subst (λ k → toℕ k < n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k < n ) (sym ( toℕ-fromℕ< (NatP.<-trans x<n n<m) )) x<n )
+    ISO.iso← iso x  = lemma2 where
+      lemma2 : fromℕ< (subst (λ k → toℕ k < n) (sym
+       (FiniteSet.finiso← fa (fromℕ< (NatP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
+       (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) ≡ x
+      lemma2 = begin
+        fromℕ< (subst (λ k → toℕ k < n) (sym
+          (FiniteSet.finiso← fa (fromℕ< (NatP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
+               (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) 
+        ≡⟨⟩
+           fromℕ< ( subst (λ k → toℕ ( k ) < n ) (sym (FiniteSet.finiso← fa _ )) lemma6 )
+        ≡⟨ lemma10 (cong (λ k → toℕ k) (FiniteSet.finiso← fa _ ) ) ⟩
+           fromℕ< lemma6
+        ≡⟨ lemma10 (lemma11 n<m ) ⟩
+           fromℕ< ( toℕ<n x )
+        ≡⟨ fromℕ<-toℕ _ _ ⟩
+           x 
+        ∎  where
+          open ≡-Reasoning
+          lemma6 : toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) < n
+          lemma6 = subst ( λ k → k < n ) (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x )
+    ISO.iso→ iso (elm1 elm x) = fin-less-cong fa n<m _ _ lemma (lemma8 (cong (λ k → toℕ (FiniteSet.F←Q fa k) ) lemma ) ) where
+      lemma13 : toℕ (fromℕ< x) ≡ toℕ (FiniteSet.F←Q fa elm)
+      lemma13 = begin
+            toℕ (fromℕ< x)
+         ≡⟨ toℕ-fromℕ< _ ⟩
+            toℕ (FiniteSet.F←Q fa elm)
+         ∎  where open ≡-Reasoning
+      lemma : FiniteSet.Q←F fa (fromℕ< (NatP.<-trans (toℕ<n (ISO.A←B iso (elm1 elm x))) n<m)) ≡ elm 
+      lemma = begin
+           FiniteSet.Q←F fa (fromℕ< (NatP.<-trans (toℕ<n (ISO.A←B iso (elm1 elm x))) n<m))
+         ≡⟨⟩
+           FiniteSet.Q←F fa (fromℕ< ( NatP.<-trans (toℕ<n ( fromℕ< x ) ) n<m))
+         ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma10 lemma13 ) ⟩
+            FiniteSet.Q←F fa (fromℕ< ( NatP.<-trans x n<m))
+         ≡⟨ cong (λ k → FiniteSet.Q←F fa (fromℕ< k ))  {!!} ⟩
+           FiniteSet.Q←F fa (fromℕ< ( toℕ<n (FiniteSet.F←Q fa elm)))
+         ≡⟨ cong (λ k → FiniteSet.Q←F fa k ) ( fromℕ<-toℕ _ _ ) ⟩
+           FiniteSet.Q←F fa (FiniteSet.F←Q fa elm )
+         ≡⟨ FiniteSet.finiso→ fa _ ⟩
+            elm 
+         ∎  where open ≡-Reasoning
+
+
--- a/agda/nat.agda	Mon Jan 04 13:20:31 2021 +0900
+++ b/agda/nat.agda	Wed Jan 13 10:52:01 2021 +0900
@@ -7,6 +7,7 @@
 open import Relation.Nullary
 open import  Relation.Binary.PropositionalEquality
 open import  Relation.Binary.Core
+open import  Relation.Binary.Definitions
 open import  logic
 
 
@@ -99,7 +100,6 @@
            suc x
         ∎  where open ≡-Reasoning
 
-
 -- open import Relation.Binary.PropositionalEquality
 
 -- postulate extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n)
@@ -180,6 +180,21 @@
 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
 
+-- open import Level hiding (suc ; zero)
+-- record Mind {l : Level} ( P : ℕ → Set l ) : Set (Level.suc l) where
+--   field 
+--      diff : ℕ
+--      mind : ( n : ℕ ) → P n → P (n + diff)
+
+-- minus-induction : { P : ℕ → Set } → Mind P → P zero → (n : ℕ) → P n
+-- minus-induction {P} mi p0 n = mi1 n n ≤-refl  where
+--     mi1 : (n n1 : ℕ) → n ≤ n1  → P n
+--     mi1 zero _ _ = p0
+--     mi1 (suc n) n1 n≤n1 with <-cmp (n1 + Mind.diff mi) n
+--     ... | tri< a ¬b ¬c = {!!}
+--     ... | tri≈ ¬a refl ¬c = {!!}
+--     ... | tri> ¬a ¬b c = {!!}
+
 open import Relation.Binary.Definitions
 
 distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z) 
--- a/agda/pushdown.agda	Mon Jan 04 13:20:31 2021 +0900
+++ b/agda/pushdown.agda	Wed Jan 13 10:52:01 2021 +0900
@@ -94,6 +94,20 @@
 test5 = PushDownAutomaton.paccept pn1 ss ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) []
 test6 = PushDownAutomaton.paccept pn1 ss ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ i0 ∷ i1 ∷ [] ) []
 
+open import Data.Empty
+
+test70 : (n : ℕ ) → (x : List In2) →  PushDownAutomaton.paccept pnn sr x [] ≡ true → inputnn n i0 i1 [] ≡ x
+test70 zero [] refl = refl
+test70 zero (x ∷ y) pa = ⊥-elim (test701 pa) where
+   test701 : PushDownAutomaton.paccept pnn sr (x ∷ y) [] ≡ true → ⊥
+   test701 pa with  PushDownAutomaton.pδ pnn sr x sr
+   ... | sr , pop = {!!}
+   ... | sr , push x = {!!}
+test70 (suc n) x pa = {!!}
+
+test71 : (n : ℕ ) → (x : List In2)  → inputnn n i0 i1 [] ≡ x →  PushDownAutomaton.paccept pnn sr x [] ≡ true
+test71 = {!!}
+
 test7 : (n : ℕ ) →  PushDownAutomaton.paccept pnn sr (inputnn n i0 i1 []) [] ≡ true
 test7 zero = refl
 test7 (suc n) with test7 n
--- a/agda/regular-concat.agda	Mon Jan 04 13:20:31 2021 +0900
+++ b/agda/regular-concat.agda	Wed Jan 13 10:52:01 2021 +0900
@@ -138,45 +138,62 @@
 open NAutomaton
 open import Data.List.Properties
 
-closed-in-concat :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B {!!} {!!} )
+open import finiteSet
+open import finiteSetUtil
+
+open FiniteSet
+
+closed-in-concat :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
 closed-in-concat {Σ} A B x = ≡-Bool-func closed-in-concat→ closed-in-concat← where
-    finab = {!!} -- (fin-∨ (afin A) (afin B))
-    NFA = (Concat-NFA A B {!!} {!!} )
+    afin : (A : RegularLanguage Σ ) → FiniteSet A
+    afin = ?
+    finab = (fin-∨ (afin A) (afin B))
+    NFA = (Concat-NFA A B)
     abmove : (q : states A ∨ states B) → (h : Σ ) → states A ∨ states B
     abmove (case1 q) h = case1 (δ (automaton A) q h)
     abmove (case2 q) h = case2 (δ (automaton B) q h)
     lemma-nmove-ab : (q : states A ∨ states B) → (h : Σ ) → Nδ NFA q h (abmove q h) ≡ true
-    lemma-nmove-ab (case1 q) _ = {!!} -- equal?-refl (afin A)
-    lemma-nmove-ab (case2 q) _ = {!!} -- equal?-refl (afin B)
+    lemma-nmove-ab (case1 q) _ = equal?-refl (afin A)
+    lemma-nmove-ab (case2 q) _ = equal?-refl (afin B)
     nmove : (q : states A ∨ states B) (nq : states A ∨ states B → Bool ) → (nq q ≡ true) → ( h : Σ ) →
-       {!!} -- exists finab (λ qn → nq qn /\ Nδ NFA qn h (abmove q h)) ≡ true
-    nmove (case1 q) nq nqt h = {!!} -- found finab (case1 q) ( bool-and-tt nqt (lemma-nmove-ab (case1 q)  h) )  
-    nmove (case2 q) nq nqt h = {!!} -- found finab (case2 q) ( bool-and-tt nqt (lemma-nmove-ab (case2 q) h) ) 
+       exists finab (λ qn → nq qn /\ Nδ NFA qn h (abmove q h)) ≡ true
+    nmove (case1 q) nq nqt h = found finab (case1 q) ( bool-and-tt nqt (lemma-nmove-ab (case1 q)  h) )  
+    nmove (case2 q) nq nqt h = found finab (case2 q) ( bool-and-tt nqt (lemma-nmove-ab (case2 q) h) ) 
     acceptB : (z : List Σ) → (q : states B) → (nq : states A ∨ states B → Bool ) → (nq (case2 q) ≡ true) → ( accept (automaton B) q z ≡ true ) 
         → Naccept NFA finab nq z  ≡ true
     acceptB [] q nq nqt fb = lemma8 where
-        lemma8 : {!!} -- exists finab ( λ q → nq q /\ Nend NFA q ) ≡ true
-        lemma8 = {!!} -- found finab (case2 q) ( bool-and-tt nqt fb )
+        lemma8 : exists finab ( λ q → nq q /\ Nend NFA q ) ≡ true
+        lemma8 = found finab (case2 q) ( bool-and-tt nqt fb )
     acceptB (h ∷ t ) q nq nq=q fb = acceptB t (δ (automaton B) q h) (Nmoves NFA finab nq h) (nmove (case2 q) nq nq=q h) fb 
 
     acceptA : (y z : List Σ) → (q : states A) → (nq : states A ∨ states B → Bool ) → (nq (case1 q) ≡ true)
         → ( accept (automaton A) q y ≡ true ) → ( accept (automaton B) (astart B) z ≡ true ) 
         → Naccept NFA finab nq (y ++ z)  ≡ true
-    acceptA [] [] q nq nqt fa fb = {!!} -- found finab (case1 q) (bool-and-tt nqt (bool-and-tt fa fb )) 
+    acceptA [] [] q nq nqt fa fb = found finab (case1 q) (bool-and-tt nqt (bool-and-tt fa fb )) 
     acceptA [] (h ∷ z)  q nq nq=q fa fb = acceptB z nextb (Nmoves NFA finab nq h) lemma70 fb where
          nextb : states B
          nextb = δ (automaton B) (astart B) h
-         lemma70 : {!!} -- exists finab (λ qn → nq qn /\ Nδ NFA qn h (case2 nextb)) ≡ true
-         lemma70 = {!!} -- found finab (case1 q) ( bool-and-tt nq=q (bool-and-tt fa (lemma-nmove-ab (case2 (astart B)) h) ))
+         lemma70 : exists finab (λ qn → nq qn /\ Nδ NFA qn h (case2 nextb)) ≡ true
+         lemma70 = found finab (case1 q) ( bool-and-tt nq=q (bool-and-tt fa (lemma-nmove-ab (case2 (astart B)) h) ))
     acceptA (h ∷ t) z q nq nq=q fa fb = acceptA t z (δ (automaton A) q h) (Nmoves NFA finab nq h) (nmove (case1 q) nq nq=q h)  fa fb where
 
     acceptAB : Split (contain A) (contain B) x
-        → {!!} -- Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true
-    acceptAB S = {!!} -- subst ( λ k → Naccept NFA finab (equal? finab (case1 (astart A))) k  ≡ true  ) ( sp-concat S )
-        -- (acceptA (sp0 S) (sp1 S)  (astart A) (equal? finab (case1 (astart A))) (equal?-refl finab) (prop0 S) (prop1 S) )
+        → Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true
+    acceptAB S = subst ( λ k → Naccept NFA finab (equal? finab (case1 (astart A))) k  ≡ true  ) ( sp-concat S )
+        (acceptA (sp0 S) (sp1 S)  (astart A) (equal? finab (case1 (astart A))) (equal?-refl finab) (prop0 S) (prop1 S) )
 
-    closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B {!!} {!!} ) x ≡ true
-    closed-in-concat→ concat = {!!}
+    closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true
+    closed-in-concat→ concat with split→AB (contain A) (contain B) x concat
+    ... | S = begin
+          accept (subset-construction finab NFA (case1 (astart A))) (Concat-NFA-start A B ) x 
+       ≡⟨ ≡-Bool-func (subset-construction-lemma← finab NFA (case1 (astart A)) x ) 
+          (subset-construction-lemma→ finab NFA (case1 (astart A)) x ) ⟩
+          Naccept NFA finab (equal? finab (case1 (astart A))) x
+       ≡⟨ acceptAB S ⟩
+         true
+       ∎  where open ≡-Reasoning
+
+    open Found
 
     ab-case : (q : states A ∨ states B ) → (qa : states A ) → (x : List Σ ) → Set
     ab-case (case1 qa') qa x = qa'  ≡ qa
@@ -185,16 +202,38 @@
     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 = {!!}
+    contain-A [] nq fn qa cond with found← finab fn 
+    ... | 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
+       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)) 
+       ... | case1 qa | record { eq = refl } | refl = sym ( equal→refl (afin A)  ( bool-∧→tt-1 (found-p S) ))  -- continued A case
+       ... | case2 qb | record { eq = refl } | nb with  bool-∧→tt-1 (found-p S) -- δnfa (case2 q) i (case1 q₁) is false
+       ... | ()   
+       lemma11 (case2 qb)  ex with found← finab ex 
+       ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) 
+       lemma11 (case2 qb)  ex | S | case2 qb' | record { eq = refl } | nb = contra-position lemma13 nb where -- continued B case should fail
+           lemma13 :  accept (automaton B) qb t ≡ true → accept (automaton B) qb' (h ∷ t) ≡ true
+           lemma13 fb = subst (λ k → accept (automaton B) k t ≡ true ) (sym (equal→refl (afin B) (bool-∧→tt-1 (found-p S)))) fb  
+       lemma11 (case2 qb)  ex | S | case1 qa | record { eq = refl } | refl with bool-∧→tt-1 (found-p S)
+       ... | eee = contra-position lemma12 ne where -- starting B case should fail
+           lemma12 : accept (automaton B) qb t ≡ true → aend (automaton A) qa /\ accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true
+           lemma12 fb = bool-and-tt (bool-∧→tt-0 eee) (subst ( λ k → accept (automaton B) k t ≡ true ) (equal→refl (afin B) (bool-∧→tt-1 eee) ) fb )
 
-    lemma10 : Naccept NFA finab {!!} x  ≡ true → split (contain A) (contain B) x ≡ true
-    lemma10 CC = contain-A x {!!} CC (astart A) lemma15 where 
-       lemma15 : (q : states A ∨ states B) → Concat-NFA-start A B q {!!} ≡ true → ab-case q (astart A) x
-       lemma15 q nq=t = {!!}
+    lemma10 : Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true → split (contain A) (contain B) x ≡ true
+    lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) lemma15 where 
+       lemma15 : (q : states A ∨ states B) → Concat-NFA-start A B q ≡ true → ab-case q (astart A) x
+       lemma15 q nq=t with equal→refl finab nq=t 
+       ... | refl = refl
 
-    closed-in-concat← : contain (M-Concat A B {!!} {!!}) x ≡ true → Concat (contain A) (contain B) x ≡ true
-    closed-in-concat← C with subset-construction-lemma← finab NFA  
-    ... | CC = {!!}
+    closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true
+    closed-in-concat← C with subset-construction-lemma← finab NFA (case1 (astart A)) x C
+    ... | CC = lemma10 CC