Mercurial > hg > Members > kono > Proof > automaton

diff automaton-in-agda/src/non-regular.agda @ 412:b85402051cdb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add mul
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 05 Apr 2024 13:38:20 +0900
parents af8f630b7e60
children
line wrap: on
line diff
--- a/automaton-in-agda/src/non-regular.agda	Wed Nov 29 17:40:55 2023 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Fri Apr 05 13:38:20 2024 +0900
@@ -40,6 +40,9 @@
 inputnn0 : ( n :  ℕ )  →  List  In2
 inputnn0 n = input-addi0 n (input-addi1 n)
 
+--
+--  using count of i0 and i1 makes the proof easier
+--
 inputnn1-i1 : (i : ℕ) → List In2 → Bool
 inputnn1-i1 zero [] = true
 inputnn1-i1 (suc _) [] = false