--- a/agda/automaton.agda	Thu Oct 31 10:08:55 2019 +0900
+++ b/agda/automaton.agda	Thu Oct 31 13:03:14 2019 +0900
@@ -150,6 +150,33 @@
 
 open accept-n
 
+lemma10 : { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (q : Q ) → (x : List Σ )
+   → (eq : accept M q x ≡ true )
+   → (i : ℕ ) → i < suc (length x) → i < length (trace M q x eq)
+lemma10 M q x eq i lt = subst ( λ k → i < k ) (trace-lemma M q x eq) lt
+
+an-1 : { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (q : Q ) → (h : Σ ) → (t : List Σ ) → (an : accept-n M q (length (h ∷ t)) (get (h ∷ t) ) ) →
+    accept-n M (δ M q h) (length t) (get t )
+an-1 {Q} {Σ} M q h t an = record {
+      r = seq
+    ; accept-1 = trans (sym (accept-2 an 0 (s≤s z≤n)))( cong (λ k → δ M k h) (accept-1 an))
+    ; accept-2 = acc2
+    ; accept-3 = accept-3 an
+   } where
+       seq : (i : ℕ) → i < suc (length t) → Q
+       seq i lt = r an (suc i) ( s≤s lt)
+       acc2 : (i : ℕ) (i<n : i < length t) → δ M (seq i (lemma4 i<n)) (get t i<n) ≡ seq (suc i) (s≤s i<n)
+       acc2 i lt = accept-2 an (suc i) (s≤s lt)
+
+lemma-t :  { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (q : Q ) → (x : List Σ )
+   → (eq : accept M q x ≡ true ) → (an : accept-n M q (length x) (get x ) ) → {i : ℕ }
+   → (lt : i < suc (length x) ) → get (trace M q x eq) (lemma10 M q x eq i lt ) ≡ r an i lt
+lemma-t M q [] eq an {zero} (s≤s z≤n) = sym ( accept-1 an )
+lemma-t M q [] eq an {suc _} (s≤s ())
+lemma-t M q (h ∷ t) eq an {0} = {!!}
+lemma-t M q (h ∷ t) eq an {suc i} (s≤s lt) with lemma-t M (δ M q h) t (lemma7 M q h t eq) (an-1 M q h t an) {i} lt
+... | eq1 = {!!}
+
 lemma :  { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (q : Q ) → (x : List Σ ) → accept M q x ≡ true → accept-n M q (length x) (get x )
 lemma {Q} {Σ} M q [] eq = record { r = λ i lt → get [ q ] {i} lt ; accept-1 = refl ; accept-2 = λ _ () ; accept-3 = eq  } 
 lemma {Q} {Σ} M q (h ∷ t) eq with lemma M (δ M q h) t (lemma7 M q h t eq) 
@@ -158,6 +185,24 @@
     r1 lt rewrite trace-lemma M q (h ∷ t) eq = lt
     lemma9 : ( lt : suc (length t) < length (q ∷ trace M q (h ∷ t) eq) ) → r an (length t) lemma5 ≡ get (q ∷ trace M q (h ∷ t) eq ) {suc (length t)} lt 
     lemma9 = {!!}
+    lemma11 : get (q ∷ trace M (δ M q h) t (lemma7 M q h t eq)) lemma5 ≡ r an (length t) lemma5
+    lemma11 = {!!} -- lemma-t M (δ M q h) (h ∷ t)  ? an ?
     lemma8 : aend M (r an (length t) lemma5 ) ≡ true → aend M (get (trace M q (h ∷ t) eq) (r1 lemma5)) ≡ true
-    lemma8 eq1 with trace-lemma M q ( h ∷ t ) eq
-    ... | eq2 = subst (λ k → aend M k ≡ true ) (lemma9 {!!} ) eq1
+    lemma8 eq1 = begin
+        aend M (get (trace M q (h ∷ t) eq) (r1 lemma5))
+       ≡⟨ {!!} ⟩
+        aend M (get (q ∷ (trace M (δ M q h) t (lemma7 M q h t eq ))) lemma5 )
+       ≡⟨ {!!} ⟩
+        aend M (get (trace M (δ M q h) t eq ) {!!} ) 
+       ≡⟨ cong (λ k → aend M k ) ( lemma-t M (δ M q h) t (lemma7 M q h t eq) an lemma5 )  ⟩
+        aend M (r an (length t) lemma5 )
+       ≡⟨ eq1 ⟩
+        true
+       ∎ where open ≡-Reasoning
+    -- with trace-lemma M q ( h ∷ t ) eq | lemma-t M (δ M q h) t (lemma7 M q h t eq) an lemma5
+    -- ... | eq2 | eq3 = subst ( λ k → aend M k ≡ true ) (sym {!!}) eq1 where
+    --     lemma12 : get (q ∷ trace M (δ M q h) t (lemma7 M q h t eq )) (r1 lemma5 ) ≡ r an (foldr (λ _ → suc) 0 t) lemma5
+    --     lemma12 = {!!}
+
+
+