--- a/automaton-in-agda/src/derive.agda	Thu Jul 27 09:03:13 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Sun Jul 30 20:16:08 2023 +0900
@@ -257,7 +257,7 @@
 sbempty? < x > f = false
 
 sbderive : (r : Regex Σ) →  (ISB r → Bool) → Σ → ISB r → Bool
-sbderive ε f s record { s = .ε ; is-sub = sunit } = ?
+sbderive ε f s record { s = .ε ; is-sub = sunit } = false
 sbderive φ f s record { s = t ; is-sub = is-sub } = false
 sbderive (r *) f s record { s = t ; is-sub = is-sub } = ?
 sbderive (r & r₁) f s record { s = t ; is-sub = is-sub } = ?

--- a/automaton-in-agda/src/non-regular.agda	Thu Jul 27 09:03:13 2023 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Sun Jul 30 20:16:08 2023 +0900
@@ -112,6 +112,34 @@
      nn04 zero = refl
      nn04 (suc i) = nn04 i
 
+half : (x : List In2) → ℕ 
+half [] = 0
+half (x ∷ []) = 0
+half (x ∷ x₁ ∷ x₂) = suc (half x₂)
+
+top-is-i0 : (x : List In2) → Bool
+top-is-i0 [] = true
+top-is-i0 (i0 ∷ _) = true
+top-is-i0 (i1 ∷ _) = false
+
+nn02  : (x : List In2) → inputnn1 x ≡ true → x ≡ inputnn0 (half x)
+nn02 x eq  = ? where
+     nn06 : (x : List In2) (i : ℕ) → (b : List In2) 
+         → b ≡ proj2 (inputnn1-i0 (half x) x)
+         → i ≡ proj1 (inputnn1-i0 (half x) x)
+         → inputnn1-i1 i b  ≡ true
+         → top-is-i0 x ≡ true
+         → (input-addi1 i ≡ proj2 (inputnn1-i0 (half x) x)) ∧
+           (x ≡  input-addi0 i (proj2 (inputnn1-i0 (half x) x))) 
+     nn06 [] _ _ refl refl ibeq _ = ⟪ refl , refl ⟫ 
+     nn06 (i0 ∷ t) zero b beq ieq ibeq _ = ?
+     nn06 (i0 ∷ i1 ∷ x) (suc i) b beq ieq ibeq ne = ?
+     nn06 (i0 ∷ i0 ∷ x) (suc i) b beq ieq ibeq ne = ⟪ ? , ? ⟫ where
+         nn05 : (input-addi1 i ≡ proj2 (inputnn1-i0 (half x) x)) ∧
+           (x ≡  input-addi0 i (proj2 (inputnn1-i0 (half x) x))) 
+         nn05 =  nn06 x i (proj2 (inputnn1-i0 (half x) x)) refl ? ? ? 
+     nn06 (i1 ∷ t) _ _ _ _ _ ()  
+
 --
 --  if there is an automaton with n states , which accespt inputnn1, it has a trasition function.
 --  The function is determinted by inputs,
@@ -299,21 +327,7 @@
                     count1 x + count1 y + count1 z ∎ where open ≡-Reasoning
                -- this takes very long time to check and needs 10GB
                bb22 : count0 y ≡ count1 y
-               bb22 = begin
-                    count0 y ≡⟨ sym ( +-cancelʳ-≡  {count1 z  + count0 x + count0 y + count0 z} (count1 y) (count0 y)  (+-cancelˡ-≡ (count1 x + count1 y) (
-                       begin
-                       count1 x + count1 y + (count1 y + (count1 z + count0 x + count0 y + count0 z))  ≡⟨ solve +-0-monoid  ⟩
-                       (count1 x + count1 y + count1 y + count1 z)  + (count0 x + count0 y + count0 z) ≡⟨ sym (cong₂ _+_ nn21 (sym nn20)) ⟩
-                       (count0 x + count0 y + count0 y + count0 z)  + (count1 x + count1 y + count1 z) ≡⟨  +-comm _ (count1 x + count1 y + count1 z) ⟩
-                       (count1 x + count1 y + count1 z) + (count0 x + count0 y + count0 y + count0 z)    ≡⟨  solve +-0-monoid ⟩
-                        count1 x + count1 y + (count1 z + (count0 x + count0 y)) + count0 y + count0 z
-                            ≡⟨  cong (λ k → count1 x + count1 y + (count1 z + k) + count0 y + count0 z) (+-comm (count0 x) _) ⟩
-                        count1 x + count1 y + (count1 z + (count0 y + count0 x)) + count0 y + count0 z    ≡⟨ solve +-0-monoid ⟩
-                        count1 x + count1 y + ((count1 z + count0 y) + count0 x) + count0 y + count0 z
-                            ≡⟨  cong (λ k → count1 x + count1 y + (k + count0 x) + count0 y + count0 z    ) (+-comm (count1 z) _) ⟩
-                        count1 x + count1 y + (count0 y + count1 z + count0 x) + count0 y + count0 z    ≡⟨  solve +-0-monoid ⟩
-                        count1 x + count1 y + (count0 y + (count1 z + count0 x + count0 y + count0 z))    ∎ ))) ⟩
-                    count1 y ∎ where open ≡-Reasoning
+               bb22 = ?
                --
                --  y contains i0 and i1 , so we have i1 → i0 transition in y ++ y
                --