Mercurial > hg > Members > kono > Proof > automaton

changeset 391:0d8b093bc4e3

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 08:21:21 +0900
parents b49d1f03faf9
children 23db567b4098
files automaton-in-agda/src/non-regular.agda
diffstat 1 files changed, 26 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/non-regular.agda	Thu Jul 27 07:17:09 2023 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Thu Jul 27 08:21:21 2023 +0900
@@ -232,23 +232,36 @@
                 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 0 eq) eq  where
+          nn12 x eq = nn17 x 0 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))
+                  → inputnn1-i1 (proj1 (inputnn1-i0 i x)) (proj2 (inputnn1-i0 i x)) ≡ true   → ¬ i1i0 x
                nn17 [] i eq li with i1i0.a li | i1i0.i10 li
                ... | [] | ()
                ... | x ∷ s | ()
-               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 (i1 ∷ i0 ∷ x₁) ? ? record { a = [] ; b = x₁ ; i10 = ? }
+               nn17 (i0 ∷ x₁) i eq li = nn17 x₁ (suc i) eq record { a = nn18 (i1i0.a li) (i1i0.i10 li) ; b = i1i0.b li 
+                 ; i10 = nn19 (i1i0.a li) (i1i0.i10 li) } where
+                    nn18 : (a : List In2 ) → i0 ∷ x₁ ≡ a ++ ( i1 ∷ i0 ∷ i1i0.b li) → List In2
+                    nn18 (i0 ∷ t) eq = t
+                    nn19 : (a : List In2 ) → (eq : i0 ∷ x₁ ≡ a ++ ( i1 ∷ i0 ∷ i1i0.b li)  )
+                       → x₁ ≡ nn18 a eq ++ i1 ∷ i0 ∷ i1i0.b li
+                    nn19 (i0 ∷ a) eq = cons-inject eq
+               nn17 (i1 ∷ x₁) i eq li = nn20 (i1 ∷ x₁) i eq li where
+                    nn20 : (x : List In2) → (i : ℕ) → inputnn1-i1 i x ≡ true → i1i0 x → ⊥
+                    nn20 [] zero eq li = nn21 (i1i0.a li) (i1i0.i10 li) where
+                        nn21 : (a : List In2 ) →  ¬ ( [] ≡ a ++ i1 ∷ i0 ∷ i1i0.b li )
+                        nn21 [] ()
+                        nn21 (x ∷ a) ()
+                    nn20 (i0 ∷ x₁) zero () li
+                    nn20 (i0 ∷ x₁) (suc i) () li
+                    nn20 (i1 ∷ x₁) (suc i) eqa li = nn20 x₁ i eqa record { a = nn18 (i1i0.a li) (i1i0.i10 li) ; b = i1i0.b li 
+                             ; i10 = nn19 (i1i0.a li) (i1i0.i10 li) } where
+                        nn18 : (a : List In2 ) → i1 ∷ x₁ ≡ a ++ ( i1 ∷ i0 ∷ i1i0.b li) → List In2
+                        nn18 [] eqb = ?
+                        nn18 (i1 ∷ t) eq = t
+                        nn19 : (a : List In2 ) → (eq : i1 ∷ x₁ ≡ a ++ ( i1 ∷ i0 ∷ i1i0.b li)  )
+                           → x₁ ≡ nn18 a eq ++ i1 ∷ i0 ∷ i1i0.b li
+                        nn19 (i1 ∷ a) eq = cons-inject eq
+                        nn19 [] eqb = ?
           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