--- a/automaton-in-agda/src/non-regular.agda	Thu Jul 27 02:09:27 2023 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Thu Jul 27 03:36:06 2023 +0900
@@ -77,6 +77,16 @@
 open import  Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality
 
+nn30 : (y : List In2) → (j : ℕ) → proj2 (inputnn1-i0 (suc j) y) ≡ proj2 (inputnn1-i0 j y )
+nn30 [] _ = refl
+nn30 (i0 ∷ y) j = nn30 y (suc j)
+nn30 (i1 ∷ y) _ = refl
+
+nn31 : (y : List In2) → (j : ℕ) → proj1 (inputnn1-i0 (suc j) y) ≡ suc (proj1 (inputnn1-i0 j y ))
+nn31 [] _ = refl
+nn31 (i0 ∷ y) j = nn31 y (suc j)
+nn31 (i1 ∷ y) _ = refl
+
 nn01  : (i : ℕ) → inputnn1 ( inputnn0 i  ) ≡ true
 nn01  i = subst₂ (λ j k → inputnn1-i1 j k ≡ true) (sym (nn07 i 0 refl)) (sym (nn09 i)) (nn04 i)  where
      nn07 : (j x : ℕ) → x + j ≡ i  → proj1 ( inputnn1-i0 x (input-addi0 j (input-addi1 i))) ≡ x + j
@@ -97,11 +107,7 @@
           nn08 zero ()
           nn08 (suc i) ()
      ... | i1 ∷ t | _ = refl
-     nn09 (suc j) = trans (nn10 (input-addi0 j (input-addi1 i)) 0) (nn09 j ) where
-         nn10 : (y : List In2) → (j : ℕ) → proj2 (inputnn1-i0 (suc j) y) ≡ proj2 (inputnn1-i0 j y )
-         nn10 [] _ = refl
-         nn10 (i0 ∷ y) j = nn10 y (suc j)
-         nn10 (i1 ∷ y) _ = refl
+     nn09 (suc j) = trans (nn30 (input-addi0 j (input-addi1 i)) 0) (nn09 j ) 
      nn04 : (i : ℕ) → inputnn1-i1 i (input-addi1 i) ≡ true
      nn04 zero = refl
      nn04 (suc i) = nn04 i
@@ -184,13 +190,35 @@
              suc (count0 t + count1 t) ≡⟨ cong suc ( c0+1=n t )  ⟩ 
              suc (length t) ∎ where open  ≡-Reasoning
           nn15 : (x : List In2 ) → inputnn1 x ≡ true → count0 x ≡ count1 x
-          nn15 x eq = ? where
-               nn18 : inputnn1-i1 (proj1 (inputnn1-i0 0 x)) (proj2 (inputnn1-i0 0 x)) ≡ true
-               nn18 = eq
-               nn16 : (x : List In2 ) → proj1 (inputnn1-i0 (count0 x) x ) ≡ count0 x
-               nn16 = ?
-               nn17 : (x : List In2 ) → count1 (proj2 (inputnn1-i0 (count0 x) x ) ) ≡ count1 x
-               nn17 = ?
+          nn15 x eq = nn18 where
+               nn17 : (x : List In2 ) → (count0 x ≡ proj1 (inputnn1-i0 0 x) + count0 (proj2 (inputnn1-i0 0 x))) 
+                                      ∧ (count1 x ≡ 0                       + count1 (proj2 (inputnn1-i0 0 x)))
+               nn17 [] = ⟪ refl , refl ⟫
+               nn17 (i0 ∷ t ) with nn17 t
+               ... | ⟪ eq1 , eq2 ⟫ = ⟪ begin
+                     suc (count0 t ) ≡⟨ cong suc eq1 ⟩
+                     suc (proj1 (inputnn1-i0 0 t) + count0 (proj2 (inputnn1-i0 0 t))) ≡⟨ cong₂ _+_ (sym (nn31 t 0)) (cong count0 (sym (nn30 t 0)))  ⟩
+                          proj1 (inputnn1-i0 1 t) + count0 (proj2 (inputnn1-i0 1 t)) ∎ 
+                       , trans eq2 (cong count1 (sym (nn30 t 0)))  ⟫ where
+                  open ≡-Reasoning
+                  nn20 : proj2 (inputnn1-i0 1 t) ≡ proj2 (inputnn1-i0 0 t)
+                  nn20 = nn30 t 0
+               nn17 (i1 ∷ x₁) = ⟪ refl , refl  ⟫
+               nn19 : (n : ℕ) → (y : List In2 ) → inputnn1-i1 n y ≡ true → (count0 y ≡ 0) ∧ (count1 y ≡ n)
+               nn19 zero [] eq = ⟪ refl , refl ⟫
+               nn19 zero (i0 ∷ y) ()
+               nn19 zero (i1 ∷ y) ()
+               nn19 (suc i) (i1 ∷ y) eq with nn19 i y eq 
+               ... | t = ⟪ proj1 t , cong suc (proj2 t ) ⟫
+               nn18 :  count0 x ≡ count1 x
+               nn18 = begin
+                     count0 x ≡⟨ proj1 (nn17 x) ⟩ 
+                     proj1 (inputnn1-i0 0 x) + count0 (proj2 (inputnn1-i0 0 x))  ≡⟨ cong (λ k → proj1 (inputnn1-i0 0 x) + k) 
+                                                              (proj1 (nn19 (proj1 (inputnn1-i0 0 x)) (proj2 (inputnn1-i0 0 x)) eq)) ⟩ 
+                     proj1 (inputnn1-i0 0 x) + 0                                 ≡⟨ +-comm _ 0 ⟩ 
+                     0                       + proj1 (inputnn1-i0 0 x)           ≡⟨ cong (λ k → 0 + k) (sym (proj2 (nn19 _ _ eq))) ⟩ 
+                     0                       + count1 (proj2 (inputnn1-i0 0 x))  ≡⟨ sym (proj2 (nn17 x)) ⟩ 
+                     count1 x ∎ where open ≡-Reasoning
           cong0 : (x y : List In2 ) → count0 (x ++ y ) ≡ count0 x + count0 y
           cong0 [] y = refl
           cong0 (i0 ∷ x)  y = cong suc (cong0 x y)
@@ -203,10 +231,21 @@
              field
                 a b : List In2
                 i10 : z ≡ a ++ (i1 ∷ i0 ∷ b )
-          nn12 : (z : List In2 ) → inputnn1 z ≡ true → ¬ i1i0 z
-          nn12 = ?
+          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
+               ... | [] | ()
+               ... | 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 = ?
+               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 = ?
           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
+          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
                nn21 : count0 x + count0 y + count0 y + count0 z ≡ count1 x + count1 y + count1 y + count1 z
                nn21 = begin
                     (count0 x + count0 y + count0 y) + count0 z ≡⟨ solve +-0-monoid ⟩