Mercurial > hg > Members > kono > Proof > automaton
diff agda/automaton.agda @ 39:3f099f353f1c
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 21 Dec 2018 10:56:18 +0900 |
| parents | ab265470c2d0 |
| children | e28f755a8dd0 |
line wrap: on
line diff
--- a/agda/automaton.agda Wed Dec 12 17:50:42 2018 +0900 +++ b/agda/automaton.agda Fri Dec 21 10:56:18 2018 +0900 @@ -82,8 +82,8 @@ 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 = ? +-- lemmaNN : { Q : Set } { Σ : Set } → (M : Automaton Q Σ) → ¬ accept M ( inputnn {n} x y [] ) +-- lemmaNN = ?