Mercurial > hg > Members > kono > Proof > automaton

comparison agda/automaton-ex.agda @ 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 b3f05cd08d24
children
comparison
equal deleted inserted replaced
162:690a8352c1ad 163:26407ce19d66
72 ieq i0 i0 = yes refl 72 ieq i0 i0 = yes refl
73 ieq i1 i1 = yes refl 73 ieq i1 i1 = yes refl
74 ieq i0 i1 = no ( λ () ) 74 ieq i0 i1 = no ( λ () )
75 ieq i1 i0 = no ( λ () ) 75 ieq i1 i0 = no ( λ () )
76 76
77 inputnn : { n : ℕ } → { Σ : Set } → ( x y : Σ ) → List Σ → List Σ
78 inputnn {zero} {_} _ _ s = s
79 inputnn {suc n} x y s = x ∷ ( inputnn {n} x y ( y ∷ s ) )
80
81 -- lemmaNN : { Q : Set } { Σ : Set } → (M : Automaton Q Σ) → ¬ accept M ( inputnn {n} x y [] )
82 -- lemmaNN = ?
83