Mercurial > hg > Members > kono > Proof > automaton

changeset 390:b49d1f03faf9

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 Thu, 27 Jul 2023 07:17:09 +0900
parents 5264070ddd2d
children 0d8b093bc4e3
files automaton-in-agda/src/non-regular.agda
diffstat 1 files changed, 12 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/non-regular.agda	Thu Jul 27 06:49:54 2023 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Thu Jul 27 07:17:09 2023 +0900
@@ -232,17 +232,23 @@
                 a b : List In2
                 i10 : z ≡ a ++ (i1 ∷ i0 ∷ b )
           nn12 : (x : List In2 ) → inputnn1 x ≡ true → ¬ i1i0 x
-          nn12 x eq = nn18 x (nn17 x eq) eq  where
-               nn17 : (x : List In2 ) → inputnn1-i1 (proj1 (inputnn1-i0 0 x)) (proj2 (inputnn1-i0 0 x)) ≡ true   → ¬ i1i0 (proj2 (inputnn1-i0 0 x))
-               nn17 [] eq li with i1i0.a li | i1i0.i10 li
+          nn12 x eq = nn18 x (nn17 x 0 eq) eq  where
+               nn17 : (x : List In2 ) → (i : ℕ) 
+                  → inputnn1-i1 (proj1 (inputnn1-i0 i x)) (proj2 (inputnn1-i0 i x)) ≡ true   → ¬ i1i0 (proj2 (inputnn1-i0 i x))
+               nn17 [] i eq li with i1i0.a li | i1i0.i10 li
                ... | [] | ()
                ... | x ∷ s | ()
-               nn17 (i0 ∷ x₁) eq li = nn17 x₁ ? (subst (λ k → i1i0 k) (nn30 x₁ 0 ) li )
-               nn17 (i1 ∷ x₁) () li 
+               nn17 (i0 ∷ x₁) i eq li = nn17 x₁ i (nn19 eq) (subst (λ k → i1i0 k) (nn30 x₁ i ) li ) where
+                   nn19 : inputnn1-i1 (proj1 (inputnn1-i0 (suc i) x₁)) (proj2 (inputnn1-i0 (suc i) x₁)) ≡ true → 
+                          inputnn1-i1 (proj1 (inputnn1-i0 i x₁))       (proj2 (inputnn1-i0 i x₁)) ≡ true
+                   nn19 = ?
+                -- nn17 x₁ (subst (λ k →  inputnn1-i1 (proj1 (inputnn1-i0 1 x₁)) k ≡ true) (nn30 x₁ 0) eq )
+                --   (subst (λ k → i1i0 k) (nn30 x₁ 0 ) li )
+               nn17 (i1 ∷ x₁) i () li 
                nn18 : (x : List In2 ) → ¬ i1i0 (proj2 (inputnn1-i0 0 x)) 
                    → inputnn1-i1 (proj1 (inputnn1-i0 0 x)) (proj2 (inputnn1-i0 0 x)) ≡ true → ¬ i1i0 x
                nn18 [] not eq = not
-               nn18 (i0 ∷ x₁) not eq li = nn18 x₁ ? ? record { a = [] ; b = ? ; i10 = ? }
+               nn18 (i0 ∷ x₁) not eq li = nn18 (i1 ∷ i0 ∷ x₁) ? ? record { a = [] ; b = x₁ ; i10 = ? }
           nn11 : (x y z : List In2 ) → ¬ y ≡ [] → inputnn1  (x ++ y ++ z) ≡ true → ¬ ( inputnn1  (x ++ y ++ y ++ z) ≡ true )
           nn11 x y z ny xyz xyyz = ⊥-elim ( nn12 (x ++ y ++ y ++ z ) xyyz record { a = x ++ i1i0.a (bb23 bb22 ) 
                                                  ; b = i1i0.b (bb23 bb22) ++ z ; i10 = bb24 } )  where