Mercurial > hg > Members > kono > Proof > automaton

changeset 13:02b4ecc9972c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
start exp version of subset construction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 24 Aug 2018 17:03:40 +0900
parents 5998479bb4ee
children 7eb71391088c
files agda/automaton.agda agda/epautomaton.agda agda/regex.agda agda/sbconst.agda agda/sbconst1.agda
diffstat 5 files changed, 149 insertions(+), 72 deletions(-) [+]
line wrap: on
line diff
--- a/agda/automaton.agda	Fri Aug 24 13:08:14 2018 +0900
+++ b/agda/automaton.agda	Fri Aug 24 17:03:40 2018 +0900
@@ -2,18 +2,18 @@
 
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Data.Nat
-open import Data.List 
-open import Data.Maybe 
+open import Data.List
+open import Data.Maybe
 open import Data.Bool using ( Bool ; true ; false )
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 
-record Automaton ( Q : Set ) ( Σ : Set  ) 
+record Automaton ( Q : Set ) ( Σ : Set  )
        : Set  where
     field
         δ : Q → Σ → Q
         astart : Q
-        aend : Q → Bool 
+        aend : Q → Bool
 
 open Automaton
 
@@ -27,14 +27,14 @@
    i1 : In2
 
 
-ieq : (i i' : In2 ) → Dec ( i ≡ i' )  
+ieq : (i i' : In2 ) → Dec ( i ≡ i' )
 ieq i0 i0 = yes refl
 ieq i1 i1 = yes refl
 ieq i0 i1 = no ( λ () )
 ieq i1 i0 = no ( λ () )
 
-moves : { Q : Set } { Σ : Set  }  
-    → Automaton Q  Σ  
+moves : { Q : Set } { Σ : Set  }
+    → Automaton Q  Σ
     → Q → List  Σ → Q
 moves {Q} { Σ} M q L = move q L
    where
@@ -42,8 +42,8 @@
       move q [] = q
       move q ( H  ∷ T ) = move (  (δ M) q H ) T
 
-accept : { Q : Set } { Σ : Set  } 
-    → Automaton Q  Σ  
+accept : { Q : Set } { Σ : Set  }
+    → Automaton Q  Σ
     → List  Σ → Bool
 accept {Q} { Σ} M L = move (astart M) L
    where
@@ -51,7 +51,7 @@
       move q [] = aend M q
       move q ( H  ∷ T ) = move (  (δ M) q H ) T
 
-transition1 : States1  → In2  → States1 
+transition1 : States1  → In2  → States1
 transition1 sr i0  = sr
 transition1 sr i1  = ss
 transition1 ss i0  = sr
@@ -59,21 +59,21 @@
 transition1 st i0  = sr
 transition1 st i1  = st
 
-fin1 :  States1  → Bool 
+fin1 :  States1  → Bool
 fin1 st = true
 fin1 _ = false
 
-am1  :  Automaton  States1 In2 
+am1  :  Automaton  States1 In2
 am1  =  record {  δ = transition1 ; astart = sr ; aend = fin1   }
 
 
 example1-1 = accept am1 ( i0  ∷ i1  ∷ i0  ∷ [] )
 example1-2 = accept am1 ( i1  ∷ i1  ∷ i1  ∷ [] )
 
-reachable : { Q : Set } { Σ : Set  } 
+reachable : { Q : Set } { Σ : Set  }
     → (M : Automaton Q  Σ  )
     → (q : Q )
-    → (L : List  Σ ) → Set 
+    → (L : List  Σ ) → Set
 reachable M q L = moves M (astart M)  L ≡ q
 
 example1-3 = reachable am1 st ( i1  ∷ i1  ∷ i1  ∷ [] )
@@ -83,28 +83,28 @@
 s1id ss = 1
 s1id st = 2
 
-record NAutomaton ( Q : Set ) ( Σ : Set  ) 
+record NAutomaton ( Q : Set ) ( Σ : Set  )
        : Set  where
     field
           nδ : Q → Σ → List Q
           sid : Q  →  ℕ
           nstart : Q
-          nend  : Q → Bool 
+          nend  : Q → Bool
 
 open NAutomaton
 
-insert : { Q : Set } {  Σ : Set } → ( NAutomaton Q  Σ  ) →  List Q  → Q  → List Q  
+insert : { Q : Set } {  Σ : Set } → ( NAutomaton Q  Σ  ) →  List Q  → Q  → List Q
 insert  M  [] q =  q ∷ []
 insert  M  ( q  ∷ T ) q' with  (sid M q ) ≟ (sid M q')
 ... | yes _ = insert  M  T q'
 ... | no _ = q  ∷ (insert  M  T q' )
 
-merge : { Q : Set } {  Σ : Set } → ( NAutomaton Q  Σ  ) → List Q  → List Q  → List Q  
+merge : { Q : Set } {  Σ : Set } → ( NAutomaton Q  Σ  ) → List Q  → List Q  → List Q
 merge  M L1 [] = L1
-merge  M L1 ( H  ∷ L  ) =  insert M (merge M L1 L ) H 
+merge  M L1 ( H  ∷ L  ) =  insert M (merge M L1 L ) H
 
-Nmoves : { Q : Set } { Σ : Set  } 
-    → NAutomaton Q  Σ  
+Nmoves : { Q : Set } { Σ : Set  }
+    → NAutomaton Q  Σ
     → List Q → List  Σ → List Q
 Nmoves {Q} { Σ} M q L = Nmoves1 q L []
    where
@@ -114,8 +114,8 @@
       Nmoves1 (q  ∷ T ) (H  ∷ L) LQ = Nmoves1 T  (H  ∷ L) ( merge M  ( nδ M q H ) LQ )
 
 
-Naccept : { Q : Set } { Σ : Set  } 
-    → NAutomaton Q  Σ  
+Naccept : { Q : Set } { Σ : Set  }
+    → NAutomaton Q  Σ
     →  List  Σ → Bool
 Naccept {Q} { Σ} M L =
        checkAccept ( Nmoves M ((nstart M)  ∷ [] )  L )
@@ -127,7 +127,7 @@
       ... | false = checkAccept L
 
 
-transition2 : States1  → In2  → List States1 
+transition2 : States1  → In2  → List States1
 transition2 sr i0  = (sr ∷ [])
 transition2 sr i1  = (ss ∷ sr ∷ [] )
 transition2 ss i0  = (sr  ∷ [])
--- a/agda/epautomaton.agda	Fri Aug 24 13:08:14 2018 +0900
+++ b/agda/epautomaton.agda	Fri Aug 24 17:03:40 2018 +0900
@@ -2,8 +2,8 @@
 
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Data.Nat
-open import Data.List 
-open import Data.Maybe 
+open import Data.List
+open import Data.Maybe
 open import Data.Bool using ( Bool ; true ; false )
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Nullary using (¬_; Dec; yes; no)
@@ -33,14 +33,14 @@
 
 insertT :  {E : Set} → ℕ → E → Tree E → Tree E
 insertT {E} n e empty = leaf n e
-insertT {E} n e (leaf n1 e1 ) with  n ≟ n1  |  n ≤? n1 
+insertT {E} n e (leaf n1 e1 ) with  n ≟ n1  |  n ≤? n1
 ... | yes _ |  _ = leaf n e
 ... | no _ | yes _  = node n e ( leaf n1 e1 ) empty
 ... | no _ | no _  = node n e empty (  leaf n1 e1 )
 insertT {E} n e (node n1 e1 left right ) with n ≟ n1 | n ≤? n1
 ... | yes _ |  _ = node n e left right
 ... | no _ | yes _  = node n1 e1 ( insertT n e left ) right
-... | no _ | no _   = node n1 e1 left ( insertT n e right ) 
+... | no _ | no _   = node n1 e1 left ( insertT n e right )
 
 memberT :  {E : Set } → ℕ → Tree E → Maybe E
 memberT _ empty = nothing
@@ -54,7 +54,7 @@
 
 open import Data.Product
 
-record εAutomaton ( Q : Set ) ( Σ : Set  ) 
+record εAutomaton ( Q : Set ) ( Σ : Set  )
        : Set  where
     field
           εδ : Q → Maybe Σ → Tree Q
@@ -63,7 +63,7 @@
           Σid : Σ  →  ℕ
           allState : Tree Q
           εstart : Q
-          εend  : Q → Bool 
+          εend  : Q → Bool
 
 open εAutomaton
 
@@ -77,23 +77,23 @@
     → Tree ( Tree  Q )
 εclosure {Q} { Σ} allState εδ  = closure (  allState   )
     where
-         closure2 :  Tree Q →  Tree Q →  Tree Q 
+         closure2 :  Tree Q →  Tree Q →  Tree Q
          closure2 empty C = C
          closure2 ( leaf n1 q ) C with memberT n1 C
          ... | just _  =  C
-         ... | nothing =  insertT n1 q C 
+         ... | nothing =  insertT n1 q C
          closure2 ( node n1 q left right ) C with memberT n1 C
          ... | just _  =  closure2 left ( closure2 right C )
          ... | nothing =  insertT n1 q (closure2 left ( closure2 right C ))
-         closure1 : ℕ →  Tree  Q 
-         closure1 n with memberT n (allState  ) 
+         closure1 : ℕ →  Tree  Q
+         closure1 n with memberT n (allState  )
          ... | nothing = empty
          ... | just q = closure2 (εδ  q nothing) ( leaf n q )
          closure :  Tree Q  → Tree ( Tree  Q )
          closure empty = empty
          closure (leaf n e) = (leaf n (closure1 n)  )
          closure (node n e left right) =
-              node n (closure1 n) ( closure left ) ( closure right ) 
+              node n (closure1 n) ( closure left ) ( closure right )
 
 
 εAutomaton2U : { Q : Set } { Σ : Set  }
--- a/agda/regex.agda	Fri Aug 24 13:08:14 2018 +0900
+++ b/agda/regex.agda	Fri Aug 24 17:03:40 2018 +0900
@@ -4,8 +4,8 @@
 -- open import Data.Fin
 open import Data.Nat
 open import Data.Product
--- open import Data.List 
-open import Data.Maybe 
+-- open import Data.List
+open import Data.Maybe
 open import Data.Bool using ( Bool ; true ; false )
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Nullary using (¬_; Dec; yes; no)
@@ -32,7 +32,7 @@
    field
       state :  ℕ
       move  :  Maybe Σ → Tree (RST Σ)
-      cond  :  Maybe Σ 
+      cond  :  Maybe Σ
       RSTend : Bool
 
 open RST
@@ -44,7 +44,7 @@
       Rstart :   RST Σ
       Rend :   RST Σ
       Rnum :  ℕ
-   
+
 open RNFA
 
 [_] : { Σ : Set} → RST Σ  → Tree (RST Σ )
@@ -54,9 +54,9 @@
 [] = empty
 
 
-infixr 5 _++_ 
+infixr 5 _++_
 
-_++_ : { Q : Set} → Tree Q → Tree Q → Tree Q 
+_++_ : { Q : Set} → Tree Q → Tree Q → Tree Q
 empty ++ t = t
 leaf n e ++ t = insertT n e t
 node n e left right ++ t =
@@ -72,11 +72,11 @@
   literal (just q)  q' n with q ≟  q'
   ... | yes _ = [ record { state = n ; move = λ i → empty ; cond = nothing ; RSTend = true  } ]
   ... | no _ = []
-  generate : ( Regex  Σ ) →  RNFA Σ → RNFA Σ 
+  generate : ( Regex  Σ ) →  RNFA Σ → RNFA Σ
   generate (x *) R = record R' { Rstart =  record (Rstart R') { move = move0  }   ;
                                  Rend   =  record (Rend R')   { move = move1  }   }
     where
-       R' : RNFA Σ 
+       R' : RNFA Σ
        R' = generate x R
        move0 : Maybe Σ → Tree (RST  Σ)
        move0 (just x) =  move (Rstart R') (just x )
@@ -87,14 +87,14 @@
   generate (x & y) R = record R1 { Rend = Rend R2 ;
                                    Rstates = Rstates R1 ++ [ Rend R1 ] ++ [ Rstart R2 ] ++ Rstates R2 }
     where
-       R2 : RNFA Σ 
+       R2 : RNFA Σ
        R2 = generate y R
-       R1 : RNFA Σ 
+       R1 : RNFA Σ
        R1 = generate x ( record R2 {  Rstart = Rstart R2 ; Rend = Rstart R2 } )
   generate (x || y) R =  record R1 { Rstart =  Rstart R1 ; Rend = Rend R2 ;
                                    Rstates = [ Rstart R1 ] ++ Rstates R1 ++ [ Rend R1 ] ++ [ Rstart R2 ] ++ Rstates R2 ++ [ Rend R2 ] }
     where
-       R1 :  RNFA  Σ 
+       R1 :  RNFA  Σ
        R1 = generate x (  record R { Rnum = Rnum R + 1 } )
        S1 : RST Σ
        S1 = record { state = Rnum R ; RSTend = RSTend (Rend R) ; move  = λ q → [] ; cond = nothing }
@@ -114,7 +114,7 @@
              ; cond = just x
              ; RSTend = false
             } ;
-       Rstates =  [ Rstart R ] ++ Rstates R 
+       Rstates =  [ Rstart R ] ++ Rstates R
      }
 
 In2toℕ : In2 → ℕ
@@ -122,9 +122,9 @@
 In2toℕ i2 = 1
 
 
-regex2nfa :  (regex : Regex In2 ) → εAutomaton (RST In2) In2 
+regex2nfa :  (regex : Regex In2 ) → εAutomaton (RST In2) In2
 regex2nfa regex = record {
-      εδ =  move 
+      εδ =  move
     ; all-εδ =  cond1
     ; εid = λ s → state s
     ; Σid = λ s → In2toℕ s
@@ -134,14 +134,14 @@
       where
           G : RNFA In2
           G =  generateRNFA regex ieq
-          GTree :  Tree ( Tree (RST In2) ) 
-          GTree = εclosure (Rstates G) move 
+          GTree :  Tree ( Tree (RST In2) )
+          GTree = εclosure (Rstates G) move
           cond2 : Maybe (Tree (RST In2) )  → Tree (Maybe In2 × Tree (RST In2))
           cond2 nothing =  empty
           cond2 (just empty) = empty
           cond2 (just (leaf n r)) = leaf n (  cond r , move r ( cond r ) )
           cond2 (just (node n r left  right )) = cond2 (just left ) ++ leaf n (  cond r , move r ( cond r ) ) ++  cond2 (just right )
           cond1 : RST In2 → Tree (Maybe In2 × Tree (RST In2))
-          cond1 s = cond2 ( memberT ( state s ) GTree ) 
+          cond1 s = cond2 ( memberT ( state s ) GTree )
 
 
--- a/agda/sbconst.agda	Fri Aug 24 13:08:14 2018 +0900
+++ b/agda/sbconst.agda	Fri Aug 24 17:03:40 2018 +0900
@@ -2,9 +2,9 @@
 
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Data.Nat
-open import Data.List 
-open import Data.Maybe 
-open import Data.Product 
+open import Data.List
+open import Data.Maybe
+open import Data.Product
 open import Data.Bool using ( Bool ; true ; false ; _∨_ )
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Nullary using (¬_; Dec; yes; no)
@@ -16,7 +16,7 @@
 -- all primitive state has id
 -- Tree Q is sorted by id and is contents are unique
 
-flatten : { Q : Set} → Tree Q  → List ℕ 
+flatten : { Q : Set} → Tree Q  → List ℕ
 flatten empty = []
 flatten (leaf x x₁) = [ x ]
 flatten (node x x₁ x₂ x₃) = flatten x₂ ++ [ x ] ++ flatten  x₃
@@ -52,7 +52,7 @@
 ...    | (just y) = just y
 ...    | nothing  = findT t x₃
 
-mergeT : { Q : Set} →  Tree Q  →  Tree  Q  →  Tree Q 
+mergeT : { Q : Set} →  Tree Q  →  Tree  Q  →  Tree Q
 mergeT empty t = t
 mergeT (leaf x t0) t = insertT x t0 t
 mergeT (node x t0  left right ) t =
@@ -62,9 +62,9 @@
 
 -- all inputs are exclusive each other ( only one input can happen )
 
--- merge Tree ( Maybe Σ × Tree Q ) 
-merge-itεδ : { Σ Q : Set } →  εAutomaton Q Σ → Σ → Tree Q  → Tree ( Maybe Σ × Tree Q )  → Tree ( Maybe Σ × Tree Q ) 
-merge-itεδ NFA i t empty = leaf (Σid NFA i) ( just i , t ) 
+-- merge Tree ( Maybe Σ × Tree Q )
+merge-itεδ : { Σ Q : Set } →  εAutomaton Q Σ → Σ → Tree Q  → Tree ( Maybe Σ × Tree Q )  → Tree ( Maybe Σ × Tree Q )
+merge-itεδ NFA i t empty = leaf (Σid NFA i) ( just i , t )
 merge-itεδ NFA i t (leaf x (i' , t1 )) with (Σid NFA i) ≟ x
 ... | no _ =  leaf x (i' , t1)
 ... | yes _ = leaf x (just i , mergeT t t1  )
@@ -73,18 +73,18 @@
 ... | yes _ = node x (just i , mergeT t t1  )
     ( merge-itεδ NFA i t left ) ( merge-itεδ NFA i t right )
 
-merge-iεδ : { Σ Q : Set } →  εAutomaton Q Σ → Maybe Σ → Tree Q  → Tree ( Maybe Σ × Tree Q )  → Tree ( Maybe Σ × Tree Q ) 
+merge-iεδ : { Σ Q : Set } →  εAutomaton Q Σ → Maybe Σ → Tree Q  → Tree ( Maybe Σ × Tree Q )  → Tree ( Maybe Σ × Tree Q )
 merge-iεδ NFA nothing _ t = t
 merge-iεδ NFA (just i) q t = merge-itεδ NFA i q t
 
-merge-εδ : { Σ Q : Set } →  εAutomaton Q Σ → Tree ( Maybe Σ × Tree Q ) → Tree ( Maybe Σ × Tree Q )  → Tree ( Maybe Σ × Tree Q ) 
+merge-εδ : { Σ Q : Set } →  εAutomaton Q Σ → Tree ( Maybe Σ × Tree Q ) → Tree ( Maybe Σ × Tree Q )  → Tree ( Maybe Σ × Tree Q )
 merge-εδ NFA empty t = t
 merge-εδ NFA (leaf x (i , t1) ) t = merge-iεδ NFA i t1 t
 merge-εδ NFA (node x (i , t1) left right) t =
        merge-εδ NFA left ( merge-iεδ NFA i t1 ( merge-εδ NFA right t ) )
-   
--- merge and find new state from newly created Tree ( Maybe Σ × Tree Q ) 
-sbconst13 :  { Σ Q : Set } →  εAutomaton Q Σ → Tree ( Maybe Σ × Tree Q ) →  Tree ( Tree  Q ) → Tree ( Tree  Q )  →  ℕ  → (  Tree ( Tree Q )  × Tree ( Tree Q )  × ℕ ) 
+
+-- merge and find new state from newly created Tree ( Maybe Σ × Tree Q )
+sbconst13 :  { Σ Q : Set } →  εAutomaton Q Σ → Tree ( Maybe Σ × Tree Q ) →  Tree ( Tree  Q ) → Tree ( Tree  Q )  →  ℕ  → (  Tree ( Tree Q )  × Tree ( Tree Q )  × ℕ )
 sbconst13 NFA empty nt t n = (nt , t , n)
 sbconst13 NFA (leaf x (p , q)) nt t n with memberTT q t
 ... | true = ( nt , t , n)
@@ -109,8 +109,8 @@
   where
     p1 = sbconst11 NFA left nt t n
     p2 = sbconst13 NFA (sbconst12 NFA q empty ) (  proj₁ p1 ) ( proj₁  ( proj₂ p1 ) ) ( proj₂  ( proj₂ p1 ) )
-    p3 = sbconst11 NFA right ( proj₁ p2 ) ( proj₁  ( proj₂ p2 )) ( proj₂  ( proj₂ p2 )) 
-       
+    p3 = sbconst11 NFA right ( proj₁ p2 ) ( proj₁  ( proj₂ p2 )) ( proj₂  ( proj₂ p2 ))
+
 {-# TERMINATING #-}
 sbconst0 :  { Σ Q : Set } →   εAutomaton Q Σ → Tree ( Tree  Q ) → Tree ( Tree  Q )  →  ℕ  →  ( Tree ( Tree  Q )  ×  ℕ )
 sbconst0 NFA t t1 n0 with sbconst11 NFA t t1 empty n0
@@ -121,14 +121,14 @@
 ... | t2 , node x y left right , n = p4
        where
          p1 = sbconst0 NFA left t2 n
-         p2 = sbconst11 NFA (leaf x y) (  proj₁  p1 ) empty (  proj₂ p1 ) 
+         p2 = sbconst11 NFA (leaf x y) (  proj₁  p1 ) empty (  proj₂ p1 )
          p3 = sbconst0 NFA right ( proj₁  p2 ) ( proj₂  ( proj₂ p2 ))
          p4 = sbconst0 NFA ( proj₁ ( proj₂ p2 )) ( proj₁  p3) ( proj₂  p3 )
 
 nfa2dfa : { Σ Q : Set } →  εAutomaton Q Σ →  Automaton (Tree Q) Σ
 nfa2dfa {Σ} {Q} NFA = record {
-        δ  = δ'  
-     ;  astart =  astart' 
+        δ  = δ'
+     ;  astart =  astart'
      ;  aend = aend'
   }
     where
@@ -143,7 +143,7 @@
       ... | yes p with  proj₁ q
       ...     | nothing = empty
       ...     | just _ = proj₂ q
-      δ0 x (node x₁ q left right) with  Σid NFA x ≟  x₁ 
+      δ0 x (node x₁ q left right) with  Σid NFA x ≟  x₁
       ... | no ¬p with δ0 x left
       ...    | empty = δ0 x right
       ...    | q1 = q1
@@ -160,5 +160,5 @@
       aend' empty = false
       aend' (leaf _ x)  = εend NFA x
       aend' (node _ x left right ) =
-          aend' left ∨ εend NFA x ∨ aend' right 
+          aend' left ∨ εend NFA x ∨ aend' right
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/sbconst1.agda	Fri Aug 24 17:03:40 2018 +0900
@@ -0,0 +1,77 @@
+module sbconst1 where
+
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Nat
+open import Data.List
+open import Data.Maybe
+open import Data.Bool using ( Bool ; true ; false )
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Data.Product
+-- open import Data.Nat.DivMod
+-- open import Data.Fin  using ( toℕ )
+
+
+open import automaton
+open Automaton
+open NAutomaton
+
+-- record Automaton ( Q : Set ) ( Σ : Set  )
+--        : Set  where
+--     field
+--         δ : Q → Σ → Q
+--         astart : Q
+--         aend : Q → Bool
+--
+-- record NAutomaton ( Q : Set ) ( Σ : Set  )
+--        : Set  where
+--     field
+--           nδ : Q → Σ → List Q
+--           sid : Q  →  ℕ
+--           nstart : Q
+--           nend  : Q → Bool
+
+record FiniteSet ( Q : Set ) ( max : ℕ  )
+        : Set  where
+     field
+        not-zero : max > 0
+        ←ℕ : ℕ → Q
+        ←Q : Q → ℕ 
+        finite : (q : Q) → ←Q q < max
+        finiso→ :(q : Q) → ←ℕ ( ←Q q ) ≡ q
+        finiso← :(n : ℕ) → ←Q ( ←ℕ n ) ≡ n
+
+open FiniteSet
+
+_div_ : ℕ → ℕ → Maybe ℕ
+_div_ x zero = {!!}
+_div_ x (suc y) = {!!}
+
+_mod_ : ℕ → ℕ → Maybe ℕ
+_mod_ = {!!}
+
+lemma1 : { Q R : Set} {n m : ℕ } → FiniteSet Q n → FiniteSet R m → FiniteSet (Q × R) ( n * m )
+lemma1 {Q} {R} {zero} {_} N M  = {!!}
+lemma1 {Q} {R} {n} {zero} N M  = {!!}
+lemma1 {Q} {R} {n} {m} N M = record {
+        not-zero = {!!}
+     ;  ←ℕ = λ i → ( ←ℕ N {!!} ,  ←ℕ M {!!})
+     ;  ←Q =  λ q → ( ←Q N ( proj₁ q ) * ( ←Q M (proj₂ q )))
+     ;  finite = {!!}
+     ;  finiso→ = {!!}
+     ;  finiso← = {!!}
+   }
+
+_exp_ : ℕ → ℕ → ℕ
+_exp_ = {!!}
+
+sbstFin : { Q : Set} {n  : ℕ } → FiniteSet Q n → FiniteSet (Q → Bool) {!!} 
+sbstFin = {!!}
+
+list2sbst : {Q : Set} { n :  ℕ } → FiniteSet Q n → List Q → Q → Bool
+list2sbst N [] _ = false
+list2sbst N ( h ∷ t ) q with  ←Q N q  ≟ ←Q N h 
+... | yes _ = true
+... | no _ = list2sbst N t q
+
+