Mercurial > hg > Members > kono > Proof > automaton

changeset 389:5264070ddd2d

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 06:49:54 +0900
parents 227f1f8f9c93
children b49d1f03faf9
files automaton-in-agda/src/non-regular.agda
diffstat 1 files changed, 7 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/non-regular.agda	Thu Jul 27 03:36:06 2023 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Thu Jul 27 06:49:54 2023 +0900
@@ -232,17 +232,17 @@
                 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  where
-               nn17 : (x : List In2 ) → ¬ i1i0 (proj2 (inputnn1-i0 0 x))
-               nn17 [] li with i1i0.a li | i1i0.i10 li
+          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
                ... | [] | ()
                ... | x ∷ s | ()
-               nn17 (i0 ∷ x₁) li = nn17 x₁ (subst (λ k → i1i0 k) (nn30 x₁ 0 ) li )
-               nn17 (i1 ∷ x₁) li with i1i0.i10 li
-               ... | t = ?
+               nn17 (i0 ∷ x₁) eq li = nn17 x₁ ? (subst (λ k → i1i0 k) (nn30 x₁ 0 ) li )
+               nn17 (i1 ∷ x₁) () 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 = ?
+               nn18 [] not eq = not
+               nn18 (i0 ∷ x₁) not eq li = nn18 x₁ ? ? record { a = [] ; b = ? ; 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