# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1699520695 -32400
# Node ID c7ad8d2dc1575fe2d715fbc8ed5a8cc7adc80bc3
# Parent  a60132983557f39f3d1d9eee068cf90bb4e5188e
safe halt.agda

diff -r a60132983557 -r c7ad8d2dc157 automaton-in-agda/src/finiteFunc.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/automaton-in-agda/src/finiteFunc.agda	Thu Nov 09 18:04:55 2023 +0900
@@ -0,0 +1,75 @@
+{-# OPTIONS #-}
+
+module finiteFunc  where
+
+open import Data.Nat hiding ( _≟_ )
+open import Data.Fin renaming ( _<_ to _<<_ ; _>_ to _f>_ ; _≟_ to _f≟_ ) hiding (_≤_ ; pred )
+open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ; ≤-refl ; <-irrelevant ) renaming ( <-cmp to <-fcmp )
+open import Data.Empty
+open import Relation.Nullary
+open import Relation.Binary.Definitions
+open import Relation.Binary.PropositionalEquality
+open import logic
+open import nat
+open import finiteSet
+open import finiteSetUtil
+open import fin
+open import Data.Nat.Properties as NP  hiding ( _≟_ )
+
+open import Axiom.Extensionality.Propositional
+open import Level hiding (suc ; zero)
+
+open import Level renaming ( suc to Suc ; zero to Zero) 
+postulate f-extensionality : { n : Level}  → Axiom.Extensionality.Propositional.Extensionality n n -- (Level.suc n)
+open import Data.Vec hiding ( map ; length )
+import Data.Product
+
+
+-- we cannot simply use f ≡ g for f : Q → A in Bijection of List Bool and (finite → Bool )
+-- what we can say is theres a fuction which elementwise equal
+
+F2L-iso : { Q : Set } → (fin : FiniteSet Q ) → (x : Vec Bool (FiniteSet.finite fin) ) → F2L fin a<sa (λ q _ → List2Func fin a<sa x q ) ≡ x
+F2L-iso {Q} fin x = f2l m a<sa x where
+  m = FiniteSet.finite fin
+  f2l : (n : ℕ ) → (n<m : n < suc m )→ (x : Vec Bool n ) → F2L fin n<m (λ q q<n → List2Func fin n<m x q )  ≡ x 
+  f2l zero (s≤s z≤n) [] = refl
+  f2l (suc n) (s≤s n<m) (h ∷ t ) = lemma1 lemma2 lemma3f where
+    lemma1 : {n : ℕ } → {h h1 : Bool } → {t t1 : Vec Bool n } → h ≡ h1 → t ≡ t1 →  h ∷ t ≡ h1 ∷ t1
+    lemma1 refl refl = refl
+    lemma2 : List2Func fin (s≤s n<m) (h ∷ t) (FiniteSet.Q←F fin (fromℕ< n<m)) ≡ h
+    lemma2 with FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ< n<m))  ≟ fromℕ< n<m
+    lemma2 | yes p = refl
+    lemma2 | no ¬p = ⊥-elim ( ¬p (FiniteSet.finiso← fin _) )
+    lemma4 : (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → List2Func fin (s≤s n<m) (h ∷ t) q ≡ List2Func fin (NP.<-trans n<m a<sa) t q
+    lemma4 q _ with FiniteSet.F←Q fin q ≟ fromℕ< n<m 
+    lemma4 q lt | yes p = ⊥-elim ( nat-≡< (toℕ-fromℕ< n<m) (lemma5 n lt (cong (λ k → toℕ k) p))) where 
+        lemma5 : {j k : ℕ } → ( n : ℕ) → suc j ≤ n → j ≡ k → k < n
+        lemma5 {zero} (suc n) (s≤s z≤n) refl = s≤s  z≤n
+        lemma5 {suc j} (suc n) (s≤s lt) refl = s≤s (lemma5 {j} n lt refl)
+    lemma4 q _ | no ¬p = refl
+    lemma3f :  F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q  ) ≡ t
+    lemma3f = begin 
+         F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q )
+       ≡⟨ cong (λ k → F2L fin (NP.<-trans n<m a<sa) ( λ q q<n → k q q<n ))
+              (f-extensionality ( λ q →  
+              (f-extensionality ( λ q<n →  lemma4 q q<n )))) ⟩
+         F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (NP.<-trans n<m a<sa) t q )
+       ≡⟨ f2l n (NP.<-trans n<m a<sa ) t ⟩
+         t
+       ∎  where
+         open ≡-Reasoning
+
+open Bijection
+
+fin→ : {A : Set} → FiniteSet A → FiniteSet (A → Bool ) 
+fin→ {A}  fin = iso-fin fin2List iso where
+    a = FiniteSet.finite fin
+    iso : Bijection (Vec Bool a ) (A → Bool)
+    fun← iso x = F2L fin a<sa ( λ q _ → x q )
+    fun→ iso x = List2Func fin a<sa x 
+    fiso← iso x  =  F2L-iso fin x 
+    fiso→ iso f = lemma where
+      lemma : List2Func fin a<sa (F2L fin a<sa (λ q _ → f q)) ≡ f
+      lemma = f-extensionality ( λ q → L2F-iso fin f q )
+
+    
diff -r a60132983557 -r c7ad8d2dc157 automaton-in-agda/src/halt.agda
--- a/automaton-in-agda/src/halt.agda	Wed Nov 08 21:35:54 2023 +0900
+++ b/automaton-in-agda/src/halt.agda	Thu Nov 09 18:04:55 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical-compatible  #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 module halt where
 
@@ -16,36 +16,35 @@
 
 open import logic
 
-record HBijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m)  where
+record FBijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m)  where
    field
-       fun←  :  S → R
-       fun→  :  R → S
-       fiso← : (x : R)  → fun← ( fun→ x )  ≡ x 
---  normal bijection required below, but we don't need this to show the inconsistency
---     fiso→ : (x : S ) → fun→ ( fun← x )  ≡ x 
+       ffun←  :  S → R → Bool
+       ffun→  :  (R → Bool) → S
+       ffiso← : (f : R → Bool ) → (x : R)  → ffun← ( ffun→ f ) x ≡ f x 
 
-injection' :  {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m)
-injection' R S f = (x y : R) → f x ≡ f y → x ≡ y
+       -- ffun← ( ffun→ f )  ≡ f , if we have functional extensionality  but it is unsafe
 
-open HBijection 
+open FBijection 
+
+fdiag : {S : Set }  (b : FBijection  S S) → S → Bool
+fdiag b n = not (ffun← b n n)
 
-diag : {S : Set }  (b : HBijection  ( S → Bool ) S) → S → Bool
-diag b n = not (fun← b n n)
+--
+--  ffun→ b (fiag b) is some S
+--  ffun← b (ffun→ b (fdiag b) ) is a function S → Bool
+--     is pointwise equal to fdiag b , which means not (ffun← b (ffun→ b (fdiag b) ) x ≡ (fdiag b) x )
+--     but is also means not (fdiag b) x ≡ (fdiag b) x , contradiction
 
-diagonal : { S : Set } → ¬ HBijection  ( S → Bool ) S
-diagonal {S} b = diagn1 (fun→ b (diag b) ) refl where
-    diagn1 : (n : S ) → ¬ (fun→ b (diag b) ≡ n ) 
-    diagn1 n dn = ¬t=f (diag b n ) ( begin
-           not (diag b n)
-        ≡⟨⟩
-           not (not (fun← b n n))
-        ≡⟨ cong (λ k → not (k  n) ) (sym (fiso← b _)) ⟩
-           not (fun← b (fun→ b (diag b))  n)
-        ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩
-           not (fun← b n n)
-        ≡⟨⟩
-           diag b n 
-        ∎ ) where open ≡-Reasoning
+fdiagonal : { S : Set } → ¬ FBijection  S S
+fdiagonal {S} b =  ¬t=f _ (trans ff4 (sym (ff3 _) ) ) where
+    ff1 : S
+    ff1 = ffun→ b (fdiag b)
+    ff2 : S → Bool
+    ff2 = ffun← b (ffun→ b (fdiag b) ) 
+    ff3 : (x : S) → ffun← b (ffun→ b (fdiag b) ) x ≡ fdiag b x
+    ff3 x = ffiso← b (fdiag b) x
+    ff4 : not ( ffun← b (ffun→ b (fdiag b) ) (ffun→ b (fdiag b))) ≡ fdiag b (ffun→ b (fdiag b))
+    ff4  = refl   -- definition of fdiag b
 
 record TM : Set where
    field
@@ -63,9 +62,6 @@
 
 open _∧_
 
-open import Axiom.Extensionality.Propositional
-postulate f-extensionality : { n : Level}  → Axiom.Extensionality.Propositional.Extensionality n n 
-
 record Halt : Set where
    field
       halt :  (t : TM ) → (x : List Bool ) → Bool
@@ -74,11 +70,11 @@
 
 open Halt
 
-TNL : (halt : Halt ) → (utm : UTM) → HBijection (List Bool → Bool) (List Bool)
-TNL halt utm = record {
-       fun←  = λ tm x → Halt.halt halt (UTM.utm utm) (tm ++ x)
-     ; fun→  = λ h  → encode utm record { tm = h1 h } 
-     ; fiso← = λ h →  f-extensionality (λ y → TN1 h y )
+TNLF : (halt : Halt ) → (utm : UTM) → FBijection (List Bool) (List Bool)
+TNLF halt utm = record {
+       ffun←  = λ tm x → Halt.halt halt (UTM.utm utm) (tm ++ x)
+     ; ffun→  = λ h  → encode utm record { tm = h1 h } 
+     ; ffiso← = λ h y → TN1 h y 
   } where
      open ≡-Reasoning
      h1 : (h : List Bool → Bool) → (x : List Bool ) → Maybe Bool
@@ -111,10 +107,9 @@
               tm (UTM.utm utm) (tenc h y)  ≡⟨  is-tm utm _ y ⟩
               h1 h y ≡⟨  h-nothing h y eq1 ⟩
               nothing  ∎  
-     -- the rest of bijection means encoding is unique
+     -- the rest of bijection means encoding is unique, but we don't need it
      -- fiso→ :  (y : List Bool ) → encode utm record { tm = λ x →  h1 (λ tm → Halt.halt halt (UTM.utm utm) tm  ) x } ≡ y
           
-TNL1 : UTM → ¬ Halt 
-TNL1 utm halt = diagonal ( TNL halt utm )
+TNLF1 : UTM → ¬ Halt 
+TNLF1 utm halt = fdiagonal ( TNLF halt utm )
 
-
diff -r a60132983557 -r c7ad8d2dc157 automaton-in-agda/src/turing.agda
--- a/automaton-in-agda/src/turing.agda	Wed Nov 08 21:35:54 2023 +0900
+++ b/automaton-in-agda/src/turing.agda	Thu Nov 09 18:04:55 2023 +0900
@@ -1,4 +1,5 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
+-- {-# OPTIONS --allow-unsolved-metas #-}
 module turing where
 
 open import Level renaming ( suc to succ ; zero to Zero )
@@ -31,10 +32,7 @@
 -- left         push SR , pop      
 -- right        pop     , push SL      
 
-{-# TERMINATING #-}
 move : {Q Σ : Set } → { tnone : Σ} → {tδ : Q →  Σ → Q × ( Write  Σ ) ×  Move } → (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
-move {Q} {Σ} {tnone} {tδ} q L [] = move {Q} {Σ} {tnone} {tδ} q  L  ( tnone  ∷ [] ) 
-move {Q} {Σ} {tnone} {tδ} q [] R = move {Q} {Σ} {tnone} {tδ} q  ( tnone  ∷ [] )  R 
 move {Q} {Σ} {tnone} {tδ} 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 ) )
@@ -42,29 +40,67 @@
 ... | 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 Σ : Set } → {tend :  Q → Bool}  → { tnone : Σ} → {tδ : Q →  Σ → Q × ( Write  Σ ) ×  Move }
+move {Q} {Σ} {tnone} {tδ} q ( LH  ∷ LT ) [] with  tδ q LH  
+... | nq , write x , left  = ( nq , ( tnone ∷ x  ∷ LT ) , [] )
+... | nq , write x , right = ( nq , LT , ( x  ∷ tnone  ∷ [] ) )
+... | nq , write x , mnone = ( nq , ( x  ∷ LT ) , (  tnone ∷ [] ) )
+... | nq , wnone , left    = ( nq , ( tnone  ∷ LH  ∷ LT ) , []  )
+... | nq , wnone , right   = ( nq ,  LT , ( LH  ∷ tnone  ∷ [] ) )
+... | nq , wnone , mnone   = ( nq , ( LH  ∷ LT ) , (  tnone ∷ [] )  )
+move {Q} {Σ} {tnone} {tδ} q [] ( RH ∷ RT ) with  tδ q tnone
+... | nq , write x , left  = ( nq , ( RH ∷ x  ∷ [] ) , RT )
+... | nq , write x , right = ( nq , [] , ( x  ∷ RH  ∷ RT ) )
+... | nq , write x , mnone = ( nq , ( x  ∷ [] ) , (  RH ∷ RT ) )
+... | nq , wnone , left    = ( nq , ( RH  ∷ tnone  ∷ [] ) , RT  )
+... | nq , wnone , right   = ( nq ,  [] , ( tnone  ∷ RH  ∷ RT ) )
+... | nq , wnone , mnone   = ( nq , ( tnone  ∷ [] ) , (  RH ∷ RT )  )
+move {Q} {Σ} {tnone} {tδ} q [] [] with  tδ q tnone
+... | nq , write x , left  = ( nq , ( tnone ∷ x  ∷ [] ) , [] )
+... | nq , write x , right = ( nq , [] , ( x  ∷ tnone  ∷ [] ) )
+... | nq , write x , mnone = ( nq , ( x  ∷ [] ) , (  tnone ∷ [] ) )
+... | nq , wnone , left    = ( nq , ( tnone  ∷ tnone  ∷ [] ) , []  )
+... | nq , wnone , right   = ( nq ,  [] , ( tnone  ∷ tnone  ∷ [] ) )
+... | nq , wnone , mnone   = ( nq , ( tnone  ∷ [] ) , (  tnone ∷ [] )  )
+
+move-loop : (i : ℕ) {Q Σ : Set } → {tend :  Q → Bool}  → { tnone : Σ} → {tδ : Q →  Σ → Q × ( Write  Σ ) ×  Move }
     → (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
-move-loop {Q} {Σ} {tend} {tnone} {tδ}  q L R with tend q
+move-loop zero {Q} {Σ} {tend} {tnone} {tδ}  q L R = ( q , L , R )
+move-loop (suc i) {Q} {Σ} {tend} {tnone} {tδ}  q L R with tend q
 ... | true = ( q , L , R )
-... | flase = move-loop {Q} {Σ} {tend} {tnone} {tδ} ( proj₁ next ) ( proj₁ ( proj₂ next ) )  ( proj₂  ( proj₂ next ) )
+... | flase = move-loop i {Q} {Σ} {tend} {tnone} {tδ} ( proj₁ next ) ( proj₁ ( proj₂ next ) )  ( proj₂  ( proj₂ next ) )
         where
         next = move {Q} {Σ} {tnone} {tδ} q  L  R 
 
-{-# TERMINATING #-}
 move0 : {Q Σ : Set } ( tend : Q → Bool ) (tnone : Σ ) (tδ : Q →  Σ → Q × ( Write  Σ ) ×  Move)
    (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
-move0 tend tnone tδ  q L R with tend q
-... | true = ( q , L , R )
-move0 tend tnone tδ  q L [] | false = move0 tend tnone tδ  q  L  ( tnone  ∷ [] ) 
-move0 tend tnone tδ  q [] R | false = move0 tend tnone tδ  q  ( tnone  ∷ [] )  R 
-move0 tend tnone tδ  q ( LH  ∷ LT ) ( RH ∷ RT ) | false with  tδ q LH  
-... | nq , write x , left  = move0 tend tnone tδ  nq ( RH ∷ x  ∷ LT ) RT 
-... | nq , write x , right = move0 tend tnone tδ  nq LT ( x  ∷ RH  ∷ RT ) 
-... | nq , write x , mnone = move0 tend tnone tδ  nq ( x  ∷ LT ) (  RH ∷ RT ) 
-... | nq , wnone , left    = move0 tend tnone tδ  nq ( RH  ∷ LH  ∷ LT ) RT  
-... | nq , wnone , right   = move0 tend tnone tδ  nq  LT ( LH  ∷ RH  ∷ RT ) 
-... | nq , wnone , mnone   = move0 tend tnone tδ  nq ( LH  ∷ LT ) (  RH ∷ RT )  
+move0 tend tnone tδ  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   = ( q , ( LH  ∷ LT ) , (  RH ∷ RT )  )
+move0 tend tnone tδ  q ( LH  ∷ LT ) [] with  tδ q LH  
+... | nq , write x , left  = nq , ( tnone ∷ x  ∷ LT ) , [] 
+... | nq , write x , right = nq , LT , ( x  ∷ tnone  ∷ [] ) 
+... | nq , write x , mnone = nq , ( x  ∷ LT ) , (  tnone ∷ [] ) 
+... | nq , wnone , left    = nq , ( tnone  ∷ LH  ∷ LT ) , []  
+... | nq , wnone , right   = nq ,  LT , ( LH  ∷ tnone  ∷ [] ) 
+... | nq , wnone , mnone   = nq , ( LH  ∷ LT ) , (  tnone ∷ [] )  
+move0 tend tnone tδ  q [] ( RH ∷ RT ) with  tδ q tnone  
+... | nq , write x , left  = nq , ( RH ∷ x  ∷ [] ) , RT 
+... | nq , write x , right = nq , [] , ( x  ∷ RH  ∷ RT ) 
+... | nq , write x , mnone = nq , ( x  ∷ [] ) , (  RH ∷ RT ) 
+... | nq , wnone , left    = nq , ( RH  ∷ tnone  ∷ [] ) , RT  
+... | nq , wnone , right   = nq ,  [] , ( tnone  ∷ RH  ∷ RT ) 
+... | nq , wnone , mnone   = nq , ( tnone  ∷ [] ) , (  RH ∷ RT )  
+move0 tend tnone tδ  q [] [] with  tδ q tnone  
+... | nq , write x , left  = nq , ( tnone ∷ x  ∷ [] ) , [] 
+... | nq , write x , right = nq , [] , ( x  ∷ tnone  ∷ [] ) 
+... | nq , write x , mnone = nq , ( x  ∷ [] ) , (  tnone ∷ [] ) 
+... | nq , wnone , left    = nq , ( tnone  ∷ tnone  ∷ [] ) , []  
+... | nq , wnone , right   = nq ,  [] , ( tnone  ∷ tnone  ∷ [] ) 
+... | nq , wnone , mnone   = nq , ( tnone  ∷ [] ) , (  tnone ∷ [] )  
 
 record Turing ( Q : Set ) ( Σ : Set  ) 
        : Set  where
@@ -73,8 +109,14 @@
         tstart : Q
         tend : Q → Bool
         tnone :  Σ
-    taccept : List  Σ → ( Q × List  Σ × List  Σ )
-    taccept L = move0 tend tnone tδ tstart L []
+    taccept : (i : ℕ ) → List  Σ → ( Q × List  Σ × List  Σ )
+    taccept i L = tloop i tstart [] []  where
+        tloop : (i : ℕ)  (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
+        tloop zero q L R = ( q , L , R )
+        tloop (suc i) q L R with tend q
+        ... | true = ( q , L , R )
+        ... | false with move0 tend tnone tδ q L R 
+        ... | nq , L , R = tloop i nq L R
 
 open import automaton
 
@@ -84,20 +126,36 @@
 open import automaton
 open Automaton
 
-{-# TERMINATING #-}
-move1 : {Q Σ : Set } ( tend : Q → Bool ) (tnone : Σ ) (δ : Q →  Σ → Q ) (tδ : Q → Σ →  Write  Σ  ×  Move)
+move1 : {Q Σ : Set } (tnone : Σ ) (δ : Q →  Σ → Q ) (tδ : Q → Σ →  Write  Σ  ×  Move)
    (q : Q ) ( L : List  Σ ) ( R : List   Σ ) →  Q × List  Σ × List  Σ 
-move1 tend tnone δ tδ  q L R with tend q
-... | true = ( q , L , R )
-move1 tend tnone δ tδ  q L [] | false = move1 tend tnone δ tδ  q  L  ( tnone  ∷ [] ) 
-move1 tend tnone δ tδ  q [] R | false = move1 tend tnone δ tδ  q  ( tnone  ∷ [] )  R 
-move1 tend tnone δ tδ  q ( LH  ∷ LT ) ( RH ∷ RT ) | false with tδ (δ q LH) LH
-... |  write x , left  = move1 tend tnone δ tδ  (δ q LH) ( RH ∷ x  ∷ LT ) RT 
-... |  write x , right = move1 tend tnone δ tδ  (δ q LH) LT ( x  ∷ RH  ∷ RT ) 
-... |  write x , mnone = move1 tend tnone δ tδ  (δ q LH) ( x  ∷ LT ) (  RH ∷ RT ) 
-... |  wnone , left    = move1 tend tnone δ tδ  (δ q LH) ( RH  ∷ LH  ∷ LT ) RT  
-... |  wnone , right   = move1 tend tnone δ tδ  (δ q LH)  LT ( LH  ∷ RH  ∷ RT ) 
-... |  wnone , mnone   = move1 tend tnone δ tδ  (δ q LH) ( LH  ∷ LT ) (  RH ∷ RT )  
+move1 tnone δ tδ  q ( LH  ∷ LT ) ( RH ∷ RT ) with tδ (δ q LH) LH
+... |  write x , left  = (δ q LH) , ( RH ∷ x  ∷ LT ) , RT 
+... |  write x , right = (δ q LH) , LT , ( x  ∷ RH  ∷ RT ) 
+... |  write x , mnone = (δ q LH) , ( x  ∷ LT ) , (  RH ∷ RT ) 
+... |  wnone , left    = (δ q LH) , ( RH  ∷ LH  ∷ LT ) , RT  
+... |  wnone , right   = (δ q LH) ,  LT , ( LH  ∷ RH  ∷ RT ) 
+... |  wnone , mnone   = (δ q LH) , ( LH  ∷ LT ) , (  RH ∷ RT )  
+move1 tnone δ tδ  q ( LH  ∷ LT ) [] with tδ (δ q LH) LH
+... |  write x , left  = (δ q LH) , ( tnone ∷ x  ∷ LT ) , [] 
+... |  write x , right = (δ q LH) , LT , ( x  ∷ tnone  ∷ [] ) 
+... |  write x , mnone = (δ q LH) , ( x  ∷ LT ) , (  tnone ∷ [] ) 
+... |  wnone , left    = (δ q LH) , ( tnone  ∷ LH  ∷ LT ) , []  
+... |  wnone , right   = (δ q LH) ,  LT , ( LH  ∷ tnone  ∷ [] ) 
+... |  wnone , mnone   = (δ q LH) , ( LH  ∷ LT ) , (  tnone ∷ [] )  
+move1 tnone δ tδ  q [] ( RH ∷ RT ) with tδ (δ q tnone) tnone
+... |  write x , left  = (δ q tnone) , ( RH ∷ x  ∷ [] ) , RT 
+... |  write x , right = (δ q tnone) , [] , ( x  ∷ RH  ∷ RT ) 
+... |  write x , mnone = (δ q tnone) , ( x  ∷ [] ) , (  RH ∷ RT ) 
+... |  wnone , left    = (δ q tnone) , ( RH  ∷ tnone  ∷ [] ) , RT  
+... |  wnone , right   = (δ q tnone) ,  [] , ( tnone  ∷ RH  ∷ RT ) 
+... |  wnone , mnone   = (δ q tnone) , ( tnone  ∷ [] ) , (  RH ∷ RT )  
+move1 tnone δ tδ  q [] [] with tδ (δ q tnone) tnone
+... |  write x , left  = (δ q tnone) , ( tnone ∷ x  ∷ [] ) , [] 
+... |  write x , right = (δ q tnone) , [] , ( x  ∷ tnone  ∷ [] ) 
+... |  write x , mnone = (δ q tnone) , ( x  ∷ [] ) , (  tnone ∷ [] ) 
+... |  wnone , left    = (δ q tnone) , ( tnone  ∷ tnone  ∷ [] ) , []  
+... |  wnone , right   = (δ q tnone) ,  [] , ( tnone  ∷ tnone  ∷ [] ) 
+... |  wnone , mnone   = (δ q tnone) , ( tnone  ∷ [] ) , (  tnone ∷ [] )  
 
 record TM ( Q : Set ) ( Σ : Set  ) 
        : Set  where
@@ -105,8 +163,14 @@
         automaton : Automaton  Q Σ
         tδ : Q → Σ → Write  Σ  ×  Move 
         tnone :  Σ
-    taccept : Q → List  Σ → ( Q × List  Σ × List  Σ )
-    taccept q L = move1 (aend automaton) tnone (δ automaton) tδ q L []
+    taccept : (i : ℕ) → Q → List  Σ → ( Q × List  Σ × List  Σ )
+    taccept i q L = tloop i q L []  where
+        tloop : (i : ℕ) → (q : Q ) ( L : List  Σ ) ( R : List   Σ ) →  Q × List  Σ × List  Σ 
+        tloop i q L R with aend automaton q
+        ... | true = ( q , L , R )
+        tloop zero q L R  | false = ( q , L , R )
+        tloop (suc i) q L R  | false with move1 tnone (δ automaton) tδ q L R
+        ... | q' , L' , R' = tloop i q' L' R'
 
 data CopyStates : Set where
    s1 : CopyStates
@@ -153,7 +217,7 @@
       tend _ = false
 
 test1 : CopyStates × ( List  ℕ ) × ( List  ℕ )
-test1 = Turing.taccept copyMachine  ( 1  ∷ 1  ∷ 0  ∷ 0  ∷  0 ∷ []  )
+test1 = Turing.taccept copyMachine  10 ( 1  ∷ 1  ∷ 0  ∷ 0  ∷  0 ∷ []  )
 
 test2 : ℕ  → CopyStates × ( List  ℕ ) × ( List  ℕ )
 test2 n  = loop n (Turing.tstart copyMachine) ( 1  ∷ 1  ∷ 0  ∷ 0  ∷  0 ∷ []  ) []
diff -r a60132983557 -r c7ad8d2dc157 automaton-in-agda/src/utm.agda
--- a/automaton-in-agda/src/utm.agda	Wed Nov 08 21:35:54 2023 +0900
+++ b/automaton-in-agda/src/utm.agda	Thu Nov 09 18:04:55 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module utm where
 
 open import turing
@@ -232,9 +234,8 @@
     ^   ∷ ０  ∷  ０ ∷  １  ∷ １ ∷ []  
 
 utm-test1 : List  utmΣ → utmStates × ( List  utmΣ ) × ( List  utmΣ )
-utm-test1 inp = Turing.taccept U-TM  inp
+utm-test1 inp = Turing.taccept U-TM 10  inp
 
-{-# TERMINATING #-}
 utm-test2 : ℕ  → List  utmΣ  → utmStates × ( List  utmΣ ) × ( List  utmΣ )
 utm-test2 n inp  = loop n (Turing.tstart U-TM) inp []
   where
@@ -242,7 +243,7 @@
         loop zero q L R = ( q , L , R )
         loop (suc n) q L R with  move {utmStates} {utmΣ} {０} {utmδ} q L R | q
         ... | nq , nL , nR | reads = loop n nq nL nR
-        ... | nq , nL , nR | _ = loop (suc n) nq nL nR
+        ... | nq , nL , nR | _ = loop n nq nL nR
 
 t1 = utm-test2 3 short-input