Mercurial > hg > Members > kono > Proof > automaton

changeset 394:d860e357fe5f

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 Mon, 31 Jul 2023 10:02:46 +0900
parents 2ff6519fc270
children cd81e0869fac
files automaton-in-agda/src/non-regular.agda
diffstat 1 files changed, 20 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/non-regular.agda	Sun Jul 30 20:16:08 2023 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Mon Jul 31 10:02:46 2023 +0900
@@ -123,23 +123,26 @@
 top-is-i0 (i1 ∷ _) = false
 
 nn02  : (x : List In2) → inputnn1 x ≡ true → x ≡ inputnn0 (half x)
-nn02 x eq  = ? where
-     nn06 : (x : List In2) (i : ℕ) → (b : List In2) 
-         → b ≡ proj2 (inputnn1-i0 (half x) x)
-         → i ≡ proj1 (inputnn1-i0 (half x) x)
-         → inputnn1-i1 i b  ≡ true
-         → top-is-i0 x ≡ true
-         → (input-addi1 i ≡ proj2 (inputnn1-i0 (half x) x)) ∧
-           (x ≡  input-addi0 i (proj2 (inputnn1-i0 (half x) x))) 
-     nn06 [] _ _ refl refl ibeq _ = ⟪ refl , refl ⟫ 
-     nn06 (i0 ∷ t) zero b beq ieq ibeq _ = ?
-     nn06 (i0 ∷ i1 ∷ x) (suc i) b beq ieq ibeq ne = ?
-     nn06 (i0 ∷ i0 ∷ x) (suc i) b beq ieq ibeq ne = ⟪ ? , ? ⟫ where
-         nn05 : (input-addi1 i ≡ proj2 (inputnn1-i0 (half x) x)) ∧
-           (x ≡  input-addi0 i (proj2 (inputnn1-i0 (half x) x))) 
-         nn05 =  nn06 x i (proj2 (inputnn1-i0 (half x) x)) refl ? ? ? 
-     nn06 (i1 ∷ t) _ _ _ _ _ ()  
-
+nn02 x eq  = subst (λ k → x ≡ input-addi0 (half x)  k ) nn05 nn09 where
+     nn07 : (i : ℕ) → (x : List In2) → inputnn1-i1 i x ≡ true → x ≡ input-addi1 i
+     nn07 zero [] eq = refl
+     nn07 zero (i0 ∷ x₁) ()
+     nn07 zero (i1 ∷ x₁) ()
+     nn07 (suc i) (i1 ∷ x₁) eq = cong (λ k → i1 ∷ k) (nn07 i x₁ eq)
+     nn06 : (i : ℕ) → (x y : List In2)  
+         →  y ≡ proj2 (inputnn1-i0 0 x)
+         →  i ≡ half x
+         →  inputnn1-i1 i y ≡ true 
+         →  y ≡ input-addi1 i 
+         →  x ≡ input-addi0 i y
+     nn06 = ?
+     nn05 :  proj2 (inputnn1-i0 0 x) ≡ input-addi1 (half x)
+     nn05 = ?
+     nn08 : half x ≡ proj1 (inputnn1-i0 0 x)
+     nn08 = ?
+     nn04 : inputnn1-i1 (half x) (proj2 (inputnn1-i0 0 x)) ≡ true
+     nn04 = subst (λ k → inputnn1-i1 k (proj2 (inputnn1-i0 0 x)) ≡ true) (sym nn08) eq
+     nn09 = nn06 (half x) x (proj2 (inputnn1-i0 0 x)) refl refl nn04 nn05 
 --
 --  if there is an automaton with n states , which accespt inputnn1, it has a trasition function.
 --  The function is determinted by inputs,