Mercurial > hg > Members > kono > Proof > automaton

changeset 396:f26444eb0275

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... look bad
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 03 Aug 2023 17:32:50 +0900
parents cd81e0869fac
children 2e22a1f3a55a
files automaton-in-agda/src/non-regular.agda
diffstat 1 files changed, 8 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/non-regular.agda	Thu Aug 03 14:55:14 2023 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Thu Aug 03 17:32:50 2023 +0900
@@ -161,9 +161,14 @@
                suc (suc (suc (length (y (i0 ∷ z))))) ≡⟨ cong suc (cong suc ( cong suc (nn17 z))) ⟩
                suc (suc (suc (length (y (x ∷ z))))) ≡⟨ refl ⟩
                suc (suc (length (i0 ∷ y (x ∷ z)))) ∎ where open ≡-Reasoning
-         nn11 : (t : List In2) → inputnn1-i1 (proj1 (inputnn1-i0 1 t)) (proj2 (inputnn1-i0 1 t)) ≡ true
-            → t ++ (i1 ∷ []) ≡  y t
-         nn11 t eq = ?
+         nn11 : (t : List In2) → inputnn1-i1 (proj1 (inputnn1-i0 0 t)) (proj2 (inputnn1-i0 0 t)) ≡ true
+            → top-is-i0 t ≡ true
+            → y t ++ (i1 ∷ []) ≡  t
+         nn11 [] eq ne = ?
+         nn11 (i0 ∷ t) eq ne = ?
+         nn11 (i1 ∷ []) eq ne = ?
+         nn11 (i1 ∷ i0 ∷ t) eq ne = ?
+         nn11 (i1 ∷ i1 ∷ t) eq ne = cong (i1 ∷_ ) (nn11 (i1 ∷ t) eq ? )
          nn10  : (y : List In2 ) 
             → inputnn1-i1 (proj1 (inputnn1-i0 0 y)) (proj2 (inputnn1-i0 0 y)) ≡ true
             →  y ≡ input-addi0 (half y) (input-addi1 (half y))