--- a/agda/turing.agda	Mon Aug 27 15:05:41 2018 +0900
+++ b/agda/turing.agda	Mon Aug 27 17:17:00 2018 +0900
@@ -38,21 +38,25 @@
         tend : Q → Bool
         tnone :  Σ
     {-# TERMINATING #-}
+    move : (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
+    move q L [] = move q  L  ( tnone  ∷ [] ) 
+    move q [] R = move q  ( tnone  ∷ [] )  R 
+    move q ( LH  ∷ LT ) ( RH ∷ RT ) with  tδ q LH  
+    ... | nq , write x , left  = ( nq , ( RH ∷ x  ∷ LT ) , RT )
+    ... | nq , write x , right = ( nq , LT , ( x  ∷ RH  ∷ RT ) )
+    ... | nq , write x , mnone = ( nq , ( x  ∷ LT ) , (  RH ∷ RT ) )
+    ... | nq , wnone , left    = ( nq , ( RH  ∷ LH  ∷ LT ) , RT  )
+    ... | nq , wnone , right   = ( nq ,  LT , ( LH  ∷ RH  ∷ RT ) )
+    ... | nq , wnone , mnone   = ( nq , ( LH  ∷ LT ) , (  RH ∷ RT )  )
+    {-# TERMINATING #-}
+    move-loop : (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
+    move-loop  q L R with tend q
+    ... | true = ( q , L , R )
+    ... | flase = move-loop ( proj₁ next ) ( proj₁ ( proj₂ next ) )  ( proj₂  ( proj₂ next ) )
+      where
+        next = move  q  L  R 
     taccept : List  Σ → ( Q × List  Σ × List  Σ )
-    taccept L = move tstart L []
-           where
-              move : (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
-              move q L R with tend q
-              ... | true = ( q , L , R )
-              move q L [] | false = move q L ( tnone  ∷ [] )
-              move q [] R | false = move q ( tnone  ∷ [] ) R
-              move q ( LH  ∷ LT ) ( RH ∷ RT ) | false with  tδ q LH  
-              ... | nq , write x , left  = move nq ( RH  ∷ x  ∷ LT ) RT
-              ... | nq , write x , right = move nq L ( x  ∷ RH  ∷ RT )
-              ... | nq , write x , mnone = move nq ( x  ∷ LT ) (  RH ∷ RT )
-              ... | nq , wnone , left    = move nq ( LT ) ( LH  ∷  RH ∷ RT ) 
-              ... | nq , wnone , right   = move nq ( RH ∷  LH  ∷ LT ) (  RT ) 
-              ... | nq , wnone , mnone   = move nq ( LH  ∷ LT ) (  RH ∷ RT ) 
+    taccept L = move-loop tstart L []
 
 data CopyStates : Set where
    s1 : CopyStates
@@ -60,21 +64,21 @@
    s3 : CopyStates
    s4 : CopyStates
    s5 : CopyStates
-   H : CopyStates
+   H  : CopyStates
 
 
 Copyδ :  CopyStates →  Bool → CopyStates × ( Write  Bool ) × ( Move  Bool )
 Copyδ s1 false  = (H    , wnone       , mnone )
 Copyδ s1 true   = (s2   , write false , right )
 Copyδ s2 false  = (s3   , write false , right )
-Copyδ s2 true   = (s2   , write true , right )
-Copyδ s3 false  = (s4   , write true , left )
-Copyδ s3 true   = (s3   , write true , right )
+Copyδ s2 true   = (s2   , write true  , right )
+Copyδ s3 false  = (s4   , write true  , left )
+Copyδ s3 true   = (s3   , write true  , right )
 Copyδ s4 false  = (s5   , write false , left )
-Copyδ s4 true   = (s4   , write true , left )
-Copyδ s5 false  = (s1   , write true , right )
-Copyδ s5 true   = (s5   , write true , left )
-Copyδ H  _      = (H    , wnone , mnone )
+Copyδ s4 true   = (s4   , write true  , left )
+Copyδ s5 false  = (s1   , write true  , right )
+Copyδ s5 true   = (s5   , write true  , left )
+Copyδ H  _      = (H    , wnone       , mnone )
 
 copyMachine : Turing CopyStates Bool
 copyMachine = record {
@@ -89,3 +93,12 @@
 
 test1 : CopyStates × ( List  Bool ) × ( List  Bool )
 test1 = Turing.taccept copyMachine  ( true  ∷ true  ∷ false  ∷ false  ∷  false ∷ []  )
+
+test2 : ℕ  → CopyStates × ( List  Bool ) × ( List  Bool )
+test2 n  = loop n (Turing.tstart copyMachine) ( true  ∷ true  ∷ false  ∷ false  ∷  false ∷ []  ) []
+  where
+        loop :  ℕ → CopyStates → ( List  Bool ) → ( List  Bool ) → CopyStates × ( List  Bool ) × ( List  Bool )
+        loop zero q L R = ( q , L , R )
+        loop (suc n) q L R = loop n ( proj₁ t1 ) ( proj₁ ( proj₂ t1 ) )  ( proj₂  ( proj₂ t1 ) )
+          where
+              t1 = Turing.move copyMachine q L R