# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1605149134 -32400
# Node ID 9615a94b18cadf117168be7f50121942de295f6d

new automaton in agda

diff -r 000000000000 -r 9615a94b18ca Test.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Test.agda	Thu Nov 12 11:45:34 2020 +0900
@@ -0,0 +1,32 @@
+module Test where
+open import Level
+open import Relation.Nullary
+open import Relation.Binary -- hiding (_⇔_ )
+open import Data.Empty
+open import Data.Nat hiding ( _⊔_ )
+
+id : ( A : Set ) → A → A
+id A x =  x
+
+id1 : { A : Set } → A → A
+id1 x = x
+
+
+test1 = id ℕ 1
+test2 = id1  1
+
+
+
+data Bool : Set where
+    true  : Bool
+    false : Bool
+
+record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   constructor ⟪_,_⟫
+   field
+      proj1 : A
+      proj2 : B
+
+data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   case1 : A → A ∨ B
+   case2 : B → A ∨ B
diff -r 000000000000 -r 9615a94b18ca automaton.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/automaton.agda	Thu Nov 12 11:45:34 2020 +0900
@@ -0,0 +1,217 @@
+{-# OPTIONS --allow-unsolved-metas #-} 
+module automaton where
+open import Level hiding ( suc ; zero )
+open import Data.Empty
+open import Relation.Nullary
+open import Relation.Binary.PropositionalEquality -- hiding (_⇔_)
+open import logic
+open import Data.List 
+
+record Automaton {n : Level} (Q : Set n) (Σ : Set ) : Set ((Level.suc n) ) where
+  field
+    δ : Q → Σ → Q
+    F : Q → Set 
+    exists : (Q → Set) → Set
+
+open Automaton
+
+accept : {n  : Level} {Q : Set n} {Σ : Set } → Automaton Q Σ → Q → List Σ → Set 
+accept {Q} {Σ} atm q [] = F atm q
+accept {Q} {Σ} atm q (x ∷ input) = 
+    accept atm (δ atm q x ) input
+
+trace : {n  : Level} {Q : Set n} {Σ : Set } → (A : Automaton Q Σ) → (start : Q) → (input : List Σ ) → accept A start input → List Q
+trace {n} {Q} {Σ} A q [] a = q ∷ []
+trace {n} {Q} {Σ} A q (x ∷ t) a = q ∷ ( trace A (δ A q x) t a )
+
+data Q3 : Set where
+  q₁ : Q3
+  q₂ : Q3
+  q₃ : Q3
+
+data Σ2 : Set where
+  s0 : Σ2
+  s1 : Σ2
+
+δ16 : Q3 → Σ2 → Q3
+δ16 q₁ s0 = q₁
+δ16 q₁ s1 = q₂
+δ16 q₂ s0 = q₃
+δ16 q₂ s1 = q₂
+δ16 q₃ s0 = q₂
+δ16 q₃ s1 = q₂
+
+δ16' : Q3 → Σ2 → Q3
+δ16' q₁ s0 = q₁
+δ16' q₁ s1 = q₂
+δ16' q₂ s0 = q₃
+δ16' q₂ s1 = q₂
+δ16' q₃ s0 = q₂
+δ16' q₃ s1 = q₃
+
+data a16end : Q3 → Set where
+   a16q2 : a16end q₂
+
+data exists-in-Q3 (P : Q3 → Set) :  Set where
+  qe1 :  P q₁ → exists-in-Q3 P
+  qe2 :  P q₂ → exists-in-Q3 P
+  qe3 :  P q₃ → exists-in-Q3 P
+
+a16 : Automaton Q3 Σ2
+a16 = record { δ = δ16 ; F = λ q → a16end q ; exists = exists-in-Q3 }
+
+a16' : Automaton Q3 Σ2
+a16' = record { δ = δ16' ; F = λ q → q ≡ q₂ ; exists = exists-in-Q3 }
+
+--
+--  ∷  →   ∷ →   ∷ →  []
+--  ↓     ↓      ↓
+--  s0    s0     s1
+--
+input1 : List Σ2
+input1 = s0 ∷ s0 ∷ s1 ∷ []
+
+input2 : List Σ2
+input2 = s0 ∷ s0 ∷ s0 ∷ []
+
+test1 : accept a16 q₁ input1 
+test1 =  a16q2 
+
+lemma0 : accept a16 q₁ input1 ≡ a16end q₂
+lemma0 = begin
+       accept a16 q₁  ( s0 ∷ s0 ∷ s1 ∷ [] )
+    ≡⟨ refl  ⟩  --   x ≡ x
+       accept a16 q₁  ( s0 ∷ s1 ∷ [] )
+    ≡⟨⟩
+       accept a16 q₁  ( s1 ∷ [] )
+    ≡⟨⟩
+       accept a16 q₂ []
+    ≡⟨⟩
+       a16end q₂
+    ∎ where open ≡-Reasoning
+
+lemma1 : List Q3
+lemma1 = trace a16 q₁ input1 a16q2
+
+test1' : accept a16' q₁ input1 
+test1' = refl
+
+lemma2 : List Q3
+lemma2 = trace a16' q₁ input1 refl
+
+test2 : ¬ ( accept a16 q₁ input2 )
+test2 ()
+
+open import Data.Bool
+open import Data.Unit
+
+-- contains at least 1 s1
+c1 : List Σ2 → Set
+c1 [] = ⊥
+c1 (s1 ∷ t) = ⊤
+c1 (_ ∷ t) = c1 t 
+
+-- even number of s0
+even0 : List Σ2 → Set
+odd0 : List Σ2 → Set
+odd0 [] = ⊥
+odd0 (s0 ∷ t) = even0 t
+odd0 (s1 ∷ t) = odd0 t
+even0 [] = ⊤
+even0 (s0 ∷ t) = odd0 t
+even0 (s1 ∷ t) = even0 t
+
+-- after
+
+a0 : List Σ2 → Set
+a0 [] = ⊥
+a0 (s1 ∷ t ) = even0 t
+a0 (s0 ∷ t ) = a0 t
+
+-- data ⊥ : Set 
+--
+-- data ⊤ : Set where
+--    tt : ⊤
+--    tt : ⊤
+
+lemma-a :  (x : List Σ2 ) →  accept a16' q₁ x → a0 x
+lemma-a x a = a1 x a where
+   a3 : (x : List Σ2 ) → accept a16' q₃ x →  odd0 x
+   a2 : (x : List Σ2 ) → accept a16' q₂ x →  even0 x
+   a3 [] ()
+   a3 (s0 ∷ t) a = a2 t a
+   a3 (s1 ∷ t) a = a3 t a
+   a2 [] a = tt
+   a2 (s0 ∷ t) a = a3 t a
+   a2 (s1 ∷ t) a = a2 t a
+   a1 : (x : List Σ2 ) →  accept a16' q₁ x → a0 x
+   a1 [] ()    -- a16' does not accept []
+   a1 (s0 ∷ t) a = a1 t a
+   a1 (s1 ∷ t) a = a2 t a
+
+-- ¬_ :  Set → Set
+-- ¬_ _ =  ⊥
+
+lemma-not-a : ¬ (  (x : List Σ2 ) →  accept a16 q₁ x → a0 x )
+lemma-not-a not1 with not1 (s1 ∷ s0 ∷ s1 ∷ [] ) a16q2
+... | ()
+
+-- can we prove negation similar to the lemma-a?
+-- lemma-not-a' :  ¬ ((x : List Σ2 ) →  accept a16 q₁ x → a0 x)
+-- lemma-not-a' not = {!!} where
+--    a3 : (x : List Σ2 ) → accept a16 q₃ x →  odd0 x
+--    a2 : (x : List Σ2 ) → accept a16 q₂ x →  even0 x
+--    a3 (s0 ∷ t) a = a2 t a
+--    a3 (s1 ∷ t) a = {!!}
+--    a2 [] a = tt
+--    a2 (s0 ∷ t) a = a3 t a
+--    a2 (s1 ∷ t) a = a2 t a
+--    a1 : (x : List Σ2 ) →  accept a16 q₁ x → a0 x
+--    a1 [] ()
+--    a1 (s0 ∷ t) a = a1 t a
+--    a1 (s1 ∷ t) a = a2 t a
+
+open import Data.Nat
+
+evenℕ : ℕ → Set
+oddℕ : ℕ → Set
+oddℕ zero = ⊥
+oddℕ (suc n) = evenℕ n
+evenℕ zero = ⊤
+evenℕ (suc n) = oddℕ n
+
+count-s0 : (x : List Σ2 ) → ℕ
+count-s0 [] = zero
+count-s0 (s0 ∷ t) = suc ( count-s0 t )
+count-s0 (s1 ∷ t) = count-s0 t 
+
+e1 : (x : List Σ2 ) → even0 x → evenℕ ( count-s0 x )
+o1 : (x : List Σ2 ) → odd0 x → oddℕ ( count-s0 x )
+e1 [] e = tt
+e1 (s0 ∷ t) o = o1 t o
+e1 (s1 ∷ t) e = e1 t e
+o1 [] () 
+o1 (s0 ∷ t) e = e1 t e
+o1 (s1 ∷ t) o = o1 t o
+
+δ19 : Q3 → Σ2 → Q3
+δ19 q₁ s0 = q₁
+δ19 q₁ s1 = q₂
+δ19 q₂ s0 = q₁
+δ19 q₂ s1 = q₂
+δ19 q₃ _ = q₁
+
+a19 : Automaton Q3 Σ2
+a19 = record { δ = δ19 ; F = λ q → q ≡ q₁ ; exists = exists-in-Q3 }
+
+--  input is empty or ends in s0
+
+end0 : List Σ2 → Set
+end0 [] = ⊤
+end0 (s0 ∷ [] )  =  ⊤
+end0 (s1 ∷ [] )  =  ⊥
+end0 (x ∷ t )  =  end0 t
+
+lemma-b :  (x : List Σ2 ) →  accept a19 q₁ x → end0 x
+lemma-b = {!!}
+
diff -r 000000000000 -r 9615a94b18ca finiteSet.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/finiteSet.agda	Thu Nov 12 11:45:34 2020 +0900
@@ -0,0 +1,536 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+module finiteSet  where
+
+open import Data.Nat hiding ( _≟_ )
+open import Data.Fin renaming ( _<_ to _<<_ ) hiding (_≤_)
+open import Data.Fin.Properties hiding ( eq? )
+open import Data.Empty
+open import Data.Bool renaming ( _∧_ to _/\_ ; _∨_ to _\/_ ) hiding ( _≟_ ; _<_ ; _≤_ )
+open import Relation.Nullary
+open import Relation.Binary.Definitions
+open import Relation.Binary.PropositionalEquality
+open import logic
+open import nat
+open import Data.Nat.Properties as NatP  hiding ( _≟_ ; eq? )
+
+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
+
+lt0 : (n : ℕ) →  n Data.Nat.≤ n
+lt0 zero = z≤n
+lt0 (suc n) = s≤s (lt0 n)
+lt2 : {m n : ℕ} → m  < n →  m Data.Nat.≤ n
+lt2 {zero} lt = z≤n
+lt2 {suc m} {zero} ()
+lt2 {suc m} {suc n} (s≤s lt) = s≤s (lt2 lt)
+
+record FiniteSet ( Q : Set ) { n : ℕ } : Set  where
+     field
+        Q←F : Fin n → Q
+        F←Q : Q → Fin n
+        finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
+        finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
+     finℕ : ℕ
+     finℕ = n
+     exists1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Bool
+     exists1  zero  _ _ = false
+     exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) \/ exists1 m (lt2 m<n) p
+     exists : ( Q → Bool ) → Bool
+     exists p = exists1 n (lt0 n) p 
+
+     all1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Bool
+     all1  zero  _ _ = true
+     all1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) /\ all1 m (lt2 m<n) p
+     all : ( Q → Bool ) → Bool
+     all p = all1 n (lt0 n) p
+
+     open import Data.List
+     list1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → List Q 
+     list1  zero  _ _ = []
+     list1 ( suc m ) m<n p with ? (p (Q←F (fromℕ≤ {m} {n} m<n))) true
+     ... | yes _ = Q←F (fromℕ≤ {m} {n} m<n) ∷ list1 m (lt2 m<n) p
+     ... | no  _ = list1 m (lt2 m<n)  p
+     to-list : ( Q → Bool ) → List Q 
+     to-list p = list1 n (lt0 n) p 
+
+     equal? : Q → Q → Bool
+     equal? q0 q1 with F←Q q0 ≟ F←Q q1
+     ... | yes p = true
+     ... | no ¬p = false
+
+     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
+     equal→refl {q0} {q1} () | no ne 
+     equal?-refl : {q : Q} → equal? q q ≡ true
+     equal?-refl {q} with F←Q q ≟ F←Q q
+     ... | yes p = refl
+     ... | no ne = ⊥-elim (ne refl)
+
+     eq? : (x y : Q) → Dec ( x ≡ y )
+     eq? x y with  F←Q x ≟ F←Q y
+     eq? x y | yes p = yes ( begin
+             x
+        ≡⟨ sym ( finiso→ x ) ⟩
+             Q←F (F←Q x) 
+        ≡⟨ cong (λ k → Q←F k ) p ⟩ 
+             Q←F (F←Q y) 
+        ≡⟨  finiso→ y  ⟩
+             y
+        ∎ ) where open ≡-Reasoning
+     eq? x y | no ¬p = no ( λ eq → ¬p (cong (λ k → F←Q k ) eq ))
+
+     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})
+     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) )
+     --   ¬∀⟶∃¬ : ∀ n {p} (P : Pred (Fin n) p) → Decidable P → ¬ (∀ i → P i) → (∃ λ i → ¬ P i)
+     End : (m : ℕ ) → (p : Q → Bool ) → Set
+     End m p = (i : Fin n) → m ≤ toℕ i → p (Q←F i )  ≡ false 
+     next-end : {m : ℕ } → ( p : Q → Bool ) → End (suc m) p
+              → (m<n : m < n ) → 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 = i=j (fromℕ≤ m<n) i (subst (λ k → k ≡ toℕ i) (sym (toℕ-fromℕ≤ m<n)) eq )
+     first-end :  ( p : Q → Bool ) → End n p
+     first-end p i i>n = ⊥-elim (nat-≤> i>n (fin<n {n} {i}) )
+     found : { p : Q → Bool } → (q : Q ) → p q ≡ true → exists p ≡ true
+     found {p} q pt = found1 n  (lt0 n) ( first-end p ) where
+         found1 : (m : ℕ ) (m<n : m Data.Nat.≤ n ) → ((i : Fin n) → m ≤ toℕ i → p (Q←F i )  ≡ false ) →  exists1 m m<n p ≡ true
+         found1 0 m<n end = ⊥-elim ( ? (subst (λ k → k ≡ false ) (cong (λ k → p k) (finiso→ q) ) (end (F←Q q) z≤n )) pt )
+         found1 (suc m)  m<n end with ? (p (Q←F (fromℕ≤ m<n))) true
+         found1 (suc m)  m<n end | yes eq = subst (λ k → k \/ exists1 m (lt2 m<n) p ≡ true ) (sym eq) (? {exists1 m (lt2 m<n) p} ) 
+         found1 (suc m)  m<n end | no np = begin
+                 p (Q←F (fromℕ≤ m<n)) \/ exists1 m (lt2 m<n) p
+              ≡⟨ ? ? ⟩
+                 exists1 m (lt2 m<n) p
+              ≡⟨ found1 m (lt2 m<n) (next-end p end m<n (?  np )) ⟩
+                 true
+              ∎  where open ≡-Reasoning
+     not-found : { p : Q → Bool } → ( (q : Q ) → p q ≡ false ) → exists p ≡ false
+     not-found {p} pn = not-found2 n (lt0 n) where
+         not-found2 : (m : ℕ ) → (m<n : m Data.Nat.≤ n ) → exists1 m m<n p ≡ false
+         not-found2  zero  _ = refl
+         not-found2 ( suc m ) m<n with pn (Q←F (fromℕ≤ {m} {n} m<n))
+         not-found2 (suc m) m<n | eq = begin
+                  p (Q←F (fromℕ≤ m<n)) \/ exists1 m (lt2 m<n) p 
+              ≡⟨ ? eq ⟩
+                  exists1 m (lt2 m<n) p 
+              ≡⟨ not-found2 m (lt2 m<n)  ⟩
+                  false
+              ∎  where open ≡-Reasoning
+     open import Level
+     postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n)
+     found← : { p : Q → Bool } → exists p ≡ true → Found Q p
+     found← {p} exst = found2 n (lt0 n) (first-end p ) where
+         found2 : (m : ℕ ) (m<n : m Data.Nat.≤ n ) → End m p →  Found Q p
+         found2 0 m<n end = ⊥-elim ( ? (not-found (λ q → end (F←Q q)  z≤n ) ) (subst (λ k → exists k ≡ true) (sym lemma) exst ) ) where
+             lemma : (λ z → p (Q←F (F←Q z))) ≡ p
+             lemma = f-extensionality ( λ q → subst (λ k → p k ≡ p q ) (sym (finiso→ q)) refl )
+         found2 (suc m)  m<n end with ? (p (Q←F (fromℕ≤ m<n))) true
+         found2 (suc m)  m<n end | yes eq = record { found-q = Q←F (fromℕ≤ m<n) ; found-p = eq }
+         found2 (suc m)  m<n end | no np = 
+               found2 m (lt2 m<n) (next-end p end m<n (? np )) 
+     not-found← : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false 
+     not-found← {p} np q = ? ( contra-position {_} {_} {_} {exists p ≡ true} (found q) (λ ep → ? np ep ) )
+
+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} → {n : ℕ } → FiniteSet A {n} → ISO A B → FiniteSet B {n}
+iso-fin {A} {B} {n} 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 n) → 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} → { b : ℕ } → FiniteSet B {b} → FiniteSet (One ∨ B) {suc b}
+fin-∨1 {B} {b} fb =  record {
+        Q←F = Q←F
+      ; F←Q =  F←Q
+      ; finiso→ = finiso→
+      ; finiso← = finiso←
+   }  where
+        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 : ℕ ) → { b : ℕ } → FiniteSet B {b} → FiniteSet (Fin a ∨ B) {a Data.Nat.+ b}
+fin-∨2 {B} zero {b} 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) {b} 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} → { a : ℕ } → (fin : FiniteSet A {a} ) → ISO (Fin a) 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} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A ∨ B) {a Data.Nat.+ b}
+fin-∨ {A} {B} {a} {b} fa fb = iso-fin (fin-∨2 a fb ) iso2 where
+    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} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b}
+fin-× {A} {B} {a} {b} fa fb with FiniteSet→Fin fa
+... | a=f = iso-fin (fin-×-f a ) iso-1 where
+   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) {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
+
+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    -- 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} 
+   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) {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
+
+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) {exp 2 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)) {k} ) (sym (exp2 n)) ( iso-fin (fin-∨ (fin2List {n}) (fin2List {n})) 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 m : ℕ } → n < suc m → (fin : FiniteSet Q {m} ) → ( (q : Q) → toℕ (FiniteSet.F←Q fin q ) < n  → Bool ) → Vec Bool n
+F2L  {Q} {zero} fin _ Q→B = []
+F2L  {Q} {suc n}  (s≤s n<m) fin Q→B = Q→B (FiniteSet.Q←F fin (fromℕ≤ n<m)) lemma6 ∷ F2L {Q} {n} (NatP.<-trans n<m a<sa ) fin 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 m : ℕ } → n < suc m → FiniteSet Q {m} → Vec Bool n →  Q → Bool 
+List2Func {Q} {zero} (s≤s z≤n) fin [] q = false
+List2Func {Q} {suc n} {m} (s≤s n<m) fin (h ∷ t) q with  FiniteSet.F←Q fin q ≟ fromℕ≤ n<m
+... | yes _ = h
+... | no _ = List2Func {Q} {n} {m} (NatP.<-trans n<m a<sa ) fin t q
+
+F2L-iso : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q {n}) → (x : Vec Bool n ) → F2L a<sa fin (λ q _ → List2Func a<sa fin x q ) ≡ x
+F2L-iso {Q} {m} fin x = f2l m a<sa x where
+    f2l : (n : ℕ ) → (n<m : n < suc m )→ (x : Vec Bool n ) → F2L  n<m fin (λ q q<n → List2Func n<m fin 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 (s≤s n<m) fin (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 (s≤s n<m) fin (h ∷ t) q ≡ List2Func (NatP.<-trans n<m a<sa) fin 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 (NatP.<-trans n<m a<sa) fin (λ q q<n → List2Func (s≤s n<m) fin (h ∷ t) q  ) ≡ t
+       lemma3 = begin 
+            F2L (NatP.<-trans n<m a<sa) fin (λ q q<n → List2Func (s≤s n<m) fin (h ∷ t) q )
+          ≡⟨ cong (λ k → F2L (NatP.<-trans n<m a<sa) fin ( λ q q<n → k q q<n ))
+                 (FiniteSet.f-extensionality fin ( λ q →  
+                 (FiniteSet.f-extensionality fin ( λ q<n →  lemma4 q q<n )))) ⟩
+            F2L (NatP.<-trans n<m a<sa) fin (λ q q<n → List2Func (NatP.<-trans n<m a<sa) fin t q )
+          ≡⟨ f2l n (NatP.<-trans n<m a<sa ) t ⟩
+            t
+          ∎  where
+            open ≡-Reasoning
+
+
+L2F : {Q : Set } {n m : ℕ } → n < suc m → (fin : FiniteSet Q {m} )  → Vec Bool n → (q :  Q ) → toℕ (FiniteSet.F←Q fin q ) < n  → Bool
+L2F n<m fin x q q<n = List2Func n<m fin x q 
+
+L2F-iso : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q {n}) → (f : Q → Bool ) → (q : Q ) → (L2F a<sa fin (F2L a<sa fin (λ q _ → f q) )) q (toℕ<n _) ≡ f q
+L2F-iso {Q} {m} fin f q = l2f m a<sa (toℕ<n _) where
+    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} 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 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 = 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} → { a : ℕ } → FiniteSet A {a} → FiniteSet (A → Bool ) {exp 2 a}
+fin→ {A} {a} fin = iso-fin fin2List iso where
+    iso : ISO (Vec Bool a ) (A → Bool)
+    ISO.A←B iso x = F2L a<sa fin ( λ q _ → x q )
+    ISO.B←A iso x = List2Func a<sa fin x 
+    ISO.iso← iso x  =  F2L-iso fin x 
+    ISO.iso→ iso x = lemma where
+       lemma : List2Func a<sa fin (F2L a<sa fin (λ q _ → x q)) ≡ x
+       lemma = FiniteSet.f-extensionality fin ( λ q → L2F-iso fin x q )
+    
+
+Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n) {n}
+Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl }
+
+data fin-less { n m : ℕ } { A : Set } (n<m : n < m ) (fa : FiniteSet A {m}) : Set where
+  elm1 : (elm : A ) → toℕ (FiniteSet.F←Q fa elm ) < n → fin-less n<m fa
+
+get-elm : { n m : ℕ } {n<m : n < m } { A : Set } {fa : FiniteSet A {m}} → fin-less n<m fa → A
+get-elm (elm1 a _ ) = a
+
+get-< : { n m : ℕ } {n<m : n < m } { A : Set } {fa : FiniteSet A {m}} → (f : fin-less n<m fa ) → toℕ (FiniteSet.F←Q fa (get-elm f )) < n
+get-< (elm1 _ b ) = b
+
+fin-less-cong : { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m})
+   → (x y : fin-less n<m fa ) → get-elm {n} {m} {n<m} {A} {fa} x ≡ get-elm {n} {m} {n<m} {A} {fa} y → get-< x ≅  get-< y → x ≡ y
+fin-less-cong n<m fa (elm1 elm x) (elm1 elm x) refl HE.refl = refl
+
+fin-< : {A : Set} → { n m : ℕ } → (n<m : n < m ) → (fa : FiniteSet A {m}) → FiniteSet (fin-less n<m fa) {n}
+fin-< {A} {n} {m} n<m fa  = iso-fin (Fin2Finite n) iso where
+    iso : ISO (Fin n) (fin-less n<m fa)
+    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  )
+    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  ))
+    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 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
+    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 n<m fa _ _ 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
+
+
diff -r 000000000000 -r 9615a94b18ca logic.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/logic.agda	Thu Nov 12 11:45:34 2020 +0900
@@ -0,0 +1,91 @@
+module logic where
+
+open import Level
+open import Relation.Nullary
+open import Relation.Binary.Definitions
+open import Relation.Binary.PropositionalEquality
+
+open import Data.Empty
+open import Data.Nat hiding (_⊔_)
+
+
+data Bool : Set where
+    true : Bool
+    false : Bool
+
+record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   constructor [_,_]
+   field
+      proj1 : A
+      proj2 : B
+
+data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   case1 : A → A ∨ B
+   case2 : B → A ∨ B
+
+_⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
+_⇔_ A B =  ( A → B ) ∧ ( B → A )
+
+contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
+contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a )
+
+double-neg : {n  : Level } {A : Set n} → A → ¬ ¬ A
+double-neg A notnot = notnot A
+
+double-neg2 : {n  : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
+double-neg2 notnot A = notnot ( double-neg A )
+
+de-morgan : {n  : Level } {A B : Set n} →  A ∧ B  → ¬ ( (¬ A ) ∨ (¬ B ) )
+de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
+de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
+
+dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
+dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
+dont-or {A} {B} (case2 b) ¬A = b
+
+dont-orb :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ B → A
+dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
+dont-orb {A} {B} (case1 a) ¬B = a
+
+
+infixr  130 _∧_
+infixr  140 _∨_
+infixr  150 _⇔_
+
+_/\_ : Bool → Bool → Bool 
+true /\ true = true
+_ /\ _ = false
+
+_<B?_ : ℕ → ℕ → Bool
+ℕ.zero <B? x = true
+ℕ.suc x <B? ℕ.zero = false
+ℕ.suc x <B? ℕ.suc xx = x <B? xx
+
+-- _<BT_ : ℕ → ℕ → Set
+-- ℕ.zero <BT ℕ.zero = ⊤
+-- ℕ.zero <BT ℕ.suc b = ⊤
+-- ℕ.suc a <BT ℕ.zero = ⊥
+-- ℕ.suc a <BT ℕ.suc b = a <BT b
+
+
+_≟B_ : Decidable {A = Bool} _≡_
+true  ≟B true  = yes refl
+false ≟B false = yes refl
+true  ≟B false = no λ()
+false ≟B true  = no λ()
+
+_\/_ : Bool → Bool → Bool 
+false \/ false = false
+_ \/ _ = true
+
+not_ : Bool → Bool 
+not true = false
+not false = true 
+
+_<=>_ : Bool → Bool → Bool  
+true <=> true = true
+false <=> false = true
+_ <=> _ = false
+
+infixr  130 _\/_
+infixr  140 _/\_
diff -r 000000000000 -r 9615a94b18ca nat.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/nat.agda	Thu Nov 12 11:45:34 2020 +0900
@@ -0,0 +1,290 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+module nat where
+
+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.Definitions
+-- open import  Relation.Binary.Core
+open import  logic
+
+
+nat-<> : { x y : ℕ } → x < y → y < x → ⊥
+nat-<>  (s≤s x<y) (s≤s y<x) = 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 : ℕ } → x < x → ⊥
+nat-<≡  (s≤s lt) = nat-<≡ lt
+
+nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
+nat-≡< refl lt = nat-<≡ lt
+
+¬a≤a : {la : ℕ} → suc la ≤ la → ⊥
+¬a≤a  (s≤s lt) = ¬a≤a  lt
+
+a<sa : {la : ℕ} → la < suc la 
+a<sa {zero} = s≤s z≤n
+a<sa {suc la} = s≤s a<sa 
+
+=→¬< : {x : ℕ  } → ¬ ( x < x )
+=→¬< {zero} ()
+=→¬< {suc x} (s≤s lt) = =→¬< lt
+
+>→¬< : {x y : ℕ  } → (x < y ) → ¬ ( y < x )
+>→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
+
+<-∨ : { 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 : ℕ) → ℕ
+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 )
+
+-- _*_ : ℕ → ℕ → ℕ
+-- _*_ zero _ = zero
+-- _*_ (suc n) m = m + ( 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 000000000000 -r 9615a94b18ca nfa.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/nfa.agda	Thu Nov 12 11:45:34 2020 +0900
@@ -0,0 +1,109 @@
+module nfa where
+open import Level renaming ( suc to Suc ; zero to Zero )
+
+open import Relation.Binary.PropositionalEquality 
+open import Data.List
+open import automaton
+open import logic
+
+record NAutomaton {n : Level} ( Q : Set n ) ( Σ : Set  )
+       : Set (Suc n) where
+    field
+          Nδ : Q → Σ → Q → Set
+          NF  :  Q → Set
+          Nexists  : (Q → Set)  → Set
+
+open NAutomaton
+
+naccept : {n : Level} {Q : Set n} {Σ : Set} → NAutomaton Q Σ → (Q → Set) → List Σ → Set
+naccept {n} {Q} {Σ} nfa qs [] = Nexists nfa (λ q → qs q ∧ NF nfa q )
+naccept {n} {Q} {Σ} nfa qs (x ∷ input) = 
+    Nexists nfa (λ q → qs q ∧ (naccept nfa (Nδ nfa q x) input ))
+
+ntrace : {n  : Level} {Q : Set n} {Σ : Set } → (NFA : NAutomaton Q Σ) → (start : Q → Set ) → (input : List Σ ) → naccept NFA start input
+     → ((Q → Set) → List Q)
+     → List (List Q)
+ntrace {n} {Q} {Σ} A q [] a list = list q ∷ []
+ntrace {n} {Q} {Σ} A q (x ∷ t) a list = list q ∷ ( ntrace A {!!} t {!!} list )
+
+data transition136 : Q3  → Σ2  → Q3 → Set  where
+    d0 : transition136 q₁ s1 q₂ 
+    d1 : transition136 q₁ s0 q₁ 
+    d2 : transition136 q₂ s0 q₂ 
+    d3 : transition136 q₂ s0 q₃ 
+    d4 : transition136 q₂ s1 q₃ 
+    d5 : transition136 q₃ s0 q₁ 
+
+start136 : Q3 → Set
+start136 q = q ≡ q₁
+
+nfa136 :  NAutomaton Q3 Σ2 
+nfa136 =  record { Nδ = transition136 ; NF = λ q → q ≡ q₁ ; Nexists = exists-in-Q3 }
+
+example136-1 = naccept nfa136 start136 ( s0  ∷ s1  ∷ s0 ∷ s0 ∷ [] )
+
+example136-0 = naccept nfa136 start136 ( s0 ∷ [] )
+
+example136-2 = naccept nfa136 start136 ( s1  ∷ s0  ∷ s1 ∷ s0 ∷ s1 ∷ [] )
+
+--
+-- ((Q → Set)  → Set) → ((Q → Set) → Set) → Set
+--
+
+data Nexists→exits  {n : Level} { Q : Set n }  {Σ : Set} ( NFA : NAutomaton Q  Σ ) : ((Q → Set) → Set) → Set where
+   one-of : Nexists→exits NFA  (Nexists NFA)
+
+subset-construction : {n : Level} { Q : Set n } { Σ : Set  }   → 
+    (NAutomaton Q  Σ ) → Automaton {Suc Zero ⊔ n} (Q → Set) Σ 
+subset-construction {n} {Q} { Σ}  NFA = record {
+        δ = λ qs x qs → Nexists NFA (λ q → Nδ NFA q x qs )
+     ;  F = λ qs → Nexists NFA ( λ q → NF NFA q )
+     ;  exists = Nexists→exits NFA   -- what this means?
+   } 
+
+subset-construction-lemma→ : { Q : Set } { Σ : Set  }   →   
+    (NFA : NAutomaton Q  Σ ) → (astart : Q → Set )
+    → (x : List Σ)
+    → naccept NFA ( λ q1 → astart q1) x 
+    → accept (  subset-construction NFA ) ( λ q1 → astart q1) x 
+subset-construction-lemma→ = {!!}
+
+subset-construction-lemma← : { Q : Set } { Σ : Set  }   → 
+    (NFA : NAutomaton Q  Σ ) → (astart : Q → Set )
+    → (x : List Σ)
+    → accept (  subset-construction NFA ) ( λ q1 → astart q1) x 
+    → naccept NFA ( λ q1 →  astart q1) x 
+subset-construction-lemma← = {!!}
+
+open import regular-language 
+
+open RegularLanguage
+open Automaton
+open import Data.Empty 
+
+Concat-exists : {n : Level}  {Σ : Set} → (A B : RegularLanguage {n} Σ ) →  (states A ∨ states B → Set) → Set
+Concat-exists {n} {Σ} A B P = exists (automaton A) (λ q → P (case1 q)) ∨ exists (automaton B) (λ q → P (case2 q))
+
+Concat-NFA : {n : Level}  {Σ : Set} → (A B : RegularLanguage {n} Σ ) → NAutomaton (states A ∨ states B) Σ 
+Concat-NFA {n} {Σ} A B = record { Nδ = δnfa ; NF = nend  ; Nexists = Concat-exists A B } 
+   module Concat-NFA where
+       data δnfa : states A ∨ states B → Σ → states A ∨ states B → Set where
+         a-case   : {q : states A}  {i : Σ } → δnfa ( case1 q) i (case1 (δ (automaton A) q i))
+         ab-trans : {q : states A}  {i : Σ } → F (automaton A) q  → δnfa ( case1 q) i (case2 (δ (automaton B) (astart B) i))
+         b-case   : {q : states B}  {i : Σ } → δnfa ( case2 q) i (case2 (δ (automaton B) q i))
+       nend : states A ∨ states B → Set
+       nend (case2 q) = F (automaton B) q
+       nend (case1 q) = F (automaton A) q ∧ F (automaton B) (astart B) -- empty B case
+
+data state-is {n : Level} {Σ : Set }  (A : RegularLanguage {n} Σ ) : (a : states A ) → Set where
+   this : (a : states A)  → state-is A a
+
+closed-in-concat :  {n : Level} {Σ : Set } → (A B : RegularLanguage {n}  Σ ) → ( x : List Σ ) 
+   → isRegular (Concat {n} (contain A) (contain B)) x record {states = states A ∨ states B → Set ; astart = λ q → state-is A (astart A)
+         ; automaton = subset-construction ( Concat-NFA A B )}
+closed-in-concat {Σ} A B x = {!!}
+
+
+
+
+
diff -r 000000000000 -r 9615a94b18ca regular-language.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/regular-language.agda	Thu Nov 12 11:45:34 2020 +0900
@@ -0,0 +1,97 @@
+{-# OPTIONS --allow-unsolved-metas #-} 
+module regular-language where
+
+open import Level renaming ( suc to Suc ; zero to Zero )
+open import Data.List 
+-- open import Data.Nat hiding ( _≟_ )
+-- open import Data.Bool 
+-- open import Data.Fin hiding ( _+_ )
+open import Data.Empty 
+open import Data.Unit 
+open import Data.Product
+open import Data.Maybe
+open import  Relation.Nullary
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import  Relation.Binary.Definitions
+open import logic
+open import nat
+open import automaton
+-- open import finiteSet
+
+language :  { Σ : Set } → Set (Suc Zero)
+language {Σ} = List Σ → Set
+
+open Automaton
+
+record RegularLanguage {n : Level} ( Σ : Set ) : Set (Level.suc n )  where
+   field
+      states : Set n
+      astart : states 
+      automaton : Automaton states Σ
+   contain : List Σ → Set 
+   contain x = accept automaton astart x
+
+split : {Σ : Set} → (List Σ → Set)
+      → ( List Σ → Set) → List Σ → Set
+split x y  [] = x [] ∧ y []
+split x y (h  ∷ t) = (x [] ∧ y (h  ∷ t)) ∨
+  split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t
+
+Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
+Union {Σ} A B x = (A x ) ∨ (B x)
+
+Concat : {n : Level}  {Σ : Set } → ( A B : language {Σ} ) → language {Σ}
+Concat {Σ} A B = split A B
+
+{-# TERMINATING #-}
+Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
+Star {Σ} A = split A ( Star {Σ} A )
+
+data In2 : Set where
+  i0 : In2
+  i1 : In2
+
+test-AB→split : {Σ : Set} → {A B : List In2 → Set} → 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
+
+open RegularLanguage 
+isRegular : {n : Level} {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage {n} Σ ) → Set (Suc Zero)
+isRegular A x r = A x ≡ contain r x 
+
+--
+--   (states A × states B → Set) → ( states A → Set ) → ( states B → Set )  → Set
+--
+exists-Union : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → (states A × states B → Set) → Set
+exists-Union A B Pab = exists (automaton A) (λ qa → exists (automaton B) (λ qb → Pab (qa , qb)) )
+
+M-Union : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → RegularLanguage Σ
+M-Union {n} {Σ} A B = record {
+       states =  states A × states B
+     ; astart = ( astart A , astart B )
+     ; automaton = record {
+             δ = λ q x → ( δ (automaton A) (proj₁ q) x , δ (automaton B) (proj₂ q) x )
+           ; F = λ q → ( F (automaton A) (proj₁ q) ∨ F (automaton B) (proj₂ q) )
+           ; exists = exists-Union A B
+        }
+   }  
+
+closed-in-union :  {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B )
+closed-in-union A B [] = lemma where
+   lemma : F (automaton A) (astart A) ∨ F (automaton B) (astart B) ≡
+           F (automaton A) (astart A) ∨ F (automaton B) (astart B)
+   lemma = refl
+closed-in-union {n} {Σ} A B ( h ∷ t ) = lemma4 t ((δ (automaton A) (astart A) h)) ((δ (automaton B) (astart B) h)) where
+   lemma4 : (t : List Σ) → (qa : states A ) → (qb : states B ) → 
+     accept (automaton A) qa t ∨ accept (automaton B) qb  t
+       ≡ accept (automaton (M-Union A B)) (qa , qb) t
+   lemma4 [] qa qb = refl
+   lemma4 (h ∷ t ) qa qb = lemma4 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h))
+
+-- closed-in-concat :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x {!!}
+-- closed-in-concat = {!!}
+