|
141
|
1 module non-regular where
|
|
|
2
|
|
|
3 open import Data.Nat
|
|
|
4 open import Data.List
|
|
|
5 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
6 open import logic
|
|
|
7 open import automaton
|
|
|
8 open import finiteSet
|
|
|
9 open import Relation.Nullary
|
|
|
10
|
|
|
11 inputnn : ( n : ℕ ) → { Σ : Set } → ( x y : Σ ) → List Σ → List Σ
|
|
|
12 inputnn zero {_} _ _ s = s
|
|
|
13 inputnn (suc n) x y s = x ∷ ( inputnn n x y ( y ∷ s ) )
|
|
|
14
|
|
|
15 lemmaNN : { Q : Set } { Σ : Set } → ( x y : Σ ) → ¬ (x ≡ y)
|
|
|
16 → FiniteSet Q
|
|
|
17 → (M : Automaton Q Σ) (q : Q)
|
|
|
18 → ¬ ( (n : ℕ) → accept M q ( inputnn n x y [] ) ≡ true )
|
|
|
19 lemmaNN = {!!}
|
|
|
20
|
