--- a/automaton-in-agda/src/derive.agda	Mon Jul 31 10:02:46 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Thu Aug 03 14:55:14 2023 +0900
@@ -204,7 +204,6 @@
      fb02 (case1 one) = refl
      fb02 (case2 (case1 record { s = s ; is-sub = is-sub })) = refl
      fb02 (case2 (case2 record { s = s ; is-sub = is-sub })) = refl
-
 finISB (x & y) = iso-fin (fin-∨ (inject-fin (fin-∧ (finISB x) (finISB y)) fi {!!}) (fin-∨1 (fin-∨ (finISB x) (finISB y)))) {!!} where
      record Z : Set where
         field 

--- a/automaton-in-agda/src/non-regular.agda	Mon Jul 31 10:02:46 2023 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Thu Aug 03 14:55:14 2023 +0900
@@ -123,26 +123,57 @@
 top-is-i0 (i1 ∷ _) = false
 
 nn02  : (x : List In2) → inputnn1 x ≡ true → x ≡ inputnn0 (half x)
-nn02 x eq  = subst (λ k → x ≡ input-addi0 (half x)  k ) nn05 nn09 where
+nn02 x eq  = nn08 x eq 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 
+     nn08 : (x : List In2 ) →  inputnn1-i1 (proj1 (inputnn1-i0 0 x)) (proj2 (inputnn1-i0 0 x)) ≡ true
+        → x ≡ input-addi0 (half x) (input-addi1 (half x))
+     nn08 [] eq = ? 
+     nn08 (i1 ∷ t) eq = ? 
+     nn08 (i0 ∷ []) eq = ?  
+     nn08 (i0 ∷ i1 ∷ t) eq = ?  
+     nn08 (i0 ∷ t @ (i0 ∷ _)) eq = ?  where
+         nn20 : top-is-i0 t ≡ true
+         nn20 = refl
+         y : List In2 → List In2
+         y [] = []
+         y (x ∷ [])  = []
+         y (x ∷ t ∷ z )  = x ∷ y (t ∷ z)
+         nn15 : ( x y : List In2) → length x ≡ suc (suc (length y)) → half x ≡ suc (half y)
+         nn15 (x ∷ x₁ ∷ []) [] eq = refl
+         nn15 (x ∷ x₁ ∷ x₃ ∷ []) (x₂ ∷ []) eq = refl
+         nn15 (x ∷ x₁ ∷ x₃ ∷ x₅ ∷ []) (x₂ ∷ x₄ ∷ []) eq = refl
+         nn15 (x ∷ x₁ ∷ x₃ ∷ x₅) (x₂ ∷ x₄ ∷ x₆ ∷ y₁) eq = cong suc (nn15 (x₃ ∷ x₅) (x₆ ∷ y₁) (cong pred (cong pred eq)) )
+         nn13 : (z : List In2) → half (i0 ∷ i0 ∷ z) ≡ suc (half (y (i0 ∷ z)))
+         nn13 z = nn15 (i0 ∷ i0 ∷ z) (y (i0 ∷ z)) ? where
+             nn17 : {x : In2} (z : List In2) →  length (y (i0 ∷ z)) ≡ length (y (x ∷ z))
+             nn17 [] = refl
+             nn17 (x ∷ []) = refl
+             nn17 (x ∷ x₁ ∷ z) = cong suc ( nn17 {x} (x₁ ∷ z)) 
+             nn16 : (z : List In2 ) → length (i0 ∷ i0 ∷ z) ≡ suc (suc (length (y (i0 ∷ z))))
+             nn16 [] = refl
+             nn16 (x ∷ z) = begin
+               length (i0 ∷ i0 ∷ x ∷ z) ≡⟨ refl ⟩
+               suc (length (i0 ∷ i0 ∷ z)) ≡⟨ cong suc (nn16 z) ⟩
+               suc (suc (suc (length (y (i0 ∷ z))))) ≡⟨ cong suc (cong suc ( cong suc (nn17 z))) ⟩
+               suc (suc (suc (length (y (x ∷ z))))) ≡⟨ refl ⟩
+               suc (suc (length (i0 ∷ y (x ∷ z)))) ∎ where open ≡-Reasoning
+         nn11 : (t : List In2) → inputnn1-i1 (proj1 (inputnn1-i0 1 t)) (proj2 (inputnn1-i0 1 t)) ≡ true
+            → t ++ (i1 ∷ []) ≡  y t
+         nn11 t eq = ?
+         nn10  : (y : List In2 ) 
+            → inputnn1-i1 (proj1 (inputnn1-i0 0 y)) (proj2 (inputnn1-i0 0 y)) ≡ true
+            →  y ≡ input-addi0 (half y) (input-addi1 (half y))
+         nn10 y eq = nn08 y eq
+         nn14 :  inputnn1-i1 (proj1 (inputnn1-i0 0 (y t))) (proj2 (inputnn1-i0 0 (y t))) ≡ true
+         nn14 = ?
+         nn12 : i0 ∷ t ≡ input-addi0 (half (i0 ∷ t)) (input-addi1 (half (i0 ∷ t)))
+         nn12 = ?
+        
+
 --
 --  if there is an automaton with n states , which accespt inputnn1, it has a trasition function.
 --  The function is determinted by inputs,