# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1584174894 -32400
# Node ID 3be1afb87f8235d3cd8b2fd6f1d5b17a297addbb
# Parent  7a0634a7c25a47505f05e0d8072b97ae48fd3819
add utm

diff -r 7a0634a7c25a -r 3be1afb87f82 a02/agda/data1.agda
--- a/a02/agda/data1.agda	Wed Dec 18 17:34:15 2019 +0900
+++ b/a02/agda/data1.agda	Sat Mar 14 17:34:54 2020 +0900
@@ -5,16 +5,16 @@
   p2 : B → A ∨ B
 
 ex1 : {A B : Set} → A → ( A ∨ B ) 
-ex1 = ?
+ex1 = {!!}
 
 ex2 : {A B : Set} → B → ( A ∨ B ) 
-ex2 = ?
+ex2 = {!!}
 
 ex3 : {A B : Set} → ( A ∨ A ) → A 
-ex3 = ?
+ex3 = {!!}
 
 ex4 : {A B C : Set} →  A ∨ ( B ∨ C ) → ( A ∨  B ) ∨ C 
-ex4 = ?
+ex4 = {!!}
 
 record _∧_ A B : Set where
   field
@@ -58,5 +58,21 @@
 ex6 = mul ( suc ( suc zero)) (suc ( suc ( suc zero)) )
 
 
+data ⊥ : Set where
+
+⊥-elim : {A : Set } -> ⊥ -> A
+⊥-elim ()
+
+¬_ : Set → Set
+¬ A = A → ⊥
 
 
+data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set  where
+   direct :   E x y -> connected E x y
+   indirect :  { z : V  } -> E x z  ->  connected {V} E z y -> connected E x y
+
+dag :  { V : Set } ( E : V -> V -> Set ) ->  Set
+dag {V} E =  ∀ (n : V)  →  ¬ ( connected E n n )
+
+lemma : ¬ (dag 3Ring )
+lemma r = r t1 ( indirect r1 (indirect r2 (direct r3 )))
diff -r 7a0634a7c25a -r 3be1afb87f82 a02/agda/equality.agda
--- a/a02/agda/equality.agda	Wed Dec 18 17:34:15 2019 +0900
+++ b/a02/agda/equality.agda	Sat Mar 14 17:34:54 2020 +0900
@@ -16,5 +16,11 @@
 ex4 : {A B : Set} {x y : A } { f : A → B } →   x == y → f x == f y
 ex4 = {!!}
 
+subst : {A : Set } → { x y : A } → ( f : A → Set ) → x == y → f x → f y
+subst {A} {x} {y} f refl fx = fx
+
+ex5 :   {A : Set} {x y z : A } →  x == y → y == z → x == z
+ex5 {A} {x} {y} {z} x==y y==z = subst {!!} {!!} {!!}
 
 
+
diff -r 7a0634a7c25a -r 3be1afb87f82 a02/agda/lambda.agda
--- a/a02/agda/lambda.agda	Wed Dec 18 17:34:15 2019 +0900
+++ b/a02/agda/lambda.agda	Sat Mar 14 17:34:54 2020 +0900
@@ -7,6 +7,11 @@
 lemma2 : (A : Set ) →  A → A 
 lemma2 A a = {!!}
 
+→intro : {A B : Set } → A →  B → ( A → B )
+→intro _ b = λ x → b
+
+→elim : {A B : Set } → A → ( A → B ) → B
+→elim a f = f a 
 
 ex1 : {A B : Set} → Set 
 ex1 {A} {B} = ( A → B ) → A → B
diff -r 7a0634a7c25a -r 3be1afb87f82 a02/agda/practice-logic.agda
--- a/a02/agda/practice-logic.agda	Wed Dec 18 17:34:15 2019 +0900
+++ b/a02/agda/practice-logic.agda	Sat Mar 14 17:34:54 2020 +0900
@@ -7,7 +7,7 @@
 postulate b : B
 
 lemma0 : A -> B
-lemma0 = {!!}
+lemma0 a = b
 
 id : { A : Set } → ( A → A )
 id = {!!}
@@ -23,7 +23,7 @@
 Lemma1 = A -> ( A -> B ) -> B
 
 lemma1 : Lemma1
-lemma1 a b = {!!}
+lemma1 a f = f a
 
 -- lemma1 a a-b = a-b a
 
diff -r 7a0634a7c25a -r 3be1afb87f82 a02/lecture.ind
--- a/a02/lecture.ind	Wed Dec 18 17:34:15 2019 +0900
+++ b/a02/lecture.ind	Sat Mar 14 17:34:54 2020 +0900
@@ -1,7 +1,7 @@
 -title: 証明と関数型言語、Agda
 
 問題は、メールでSubjectを (a01 の 問題2.5ならば)
-    Subject: Report on Automan Lecture 2.5 
+    Subject: Report on Automaton Lecture 2.5 
 として、問題毎に提出すること。
 
 kono@ie.u-ryukyu.ac.jp まで送ること。
diff -r 7a0634a7c25a -r 3be1afb87f82 a13/smv/test10.smv
--- a/a13/smv/test10.smv	Wed Dec 18 17:34:15 2019 +0900
+++ b/a13/smv/test10.smv	Sat Mar 14 17:34:54 2020 +0900
@@ -8,4 +8,4 @@
     y=7: next(y)=0;
     TRUE : next(y) = ((y + 1) mod 16);
   esac
-LTLSPEC G ( y=4 -> X y=6 )
+LTLSPEC G ( y=4 -> X y=5 )
diff -r 7a0634a7c25a -r 3be1afb87f82 agda/omega-automaton.agda
--- a/agda/omega-automaton.agda	Wed Dec 18 17:34:15 2019 +0900
+++ b/agda/omega-automaton.agda	Sat Mar 14 17:34:54 2020 +0900
@@ -4,23 +4,24 @@
 open import Data.Nat
 open import Data.List
 open import Data.Maybe
-open import Data.Bool using ( Bool ; true ; false ; _∧_ ) renaming ( not to negate )
+-- open import Data.Bool using ( Bool ; true ; false ; _∧_ ) renaming ( not to negate )
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
-open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Relation.Nullary using (not_; Dec; yes; no)
 open import Data.Empty
 
+open import logic
 open import automaton
 
 open Automaton 
 
-ω-run : { Q  Σ : Set } → (Ω : Automaton Q Σ ) →  ℕ → ( ℕ → Σ )  → Q
-ω-run Ω zero s = astart Ω
-ω-run Ω (suc n) s = δ Ω (ω-run Ω n s) ( s n )
+ω-run : { Q  Σ : Set } → (Ω : Automaton Q Σ ) → (astart : Q )  →  ℕ → ( ℕ → Σ )  → Q
+ω-run Ω x zero s = x
+ω-run Ω x (suc n) s = δ Ω (ω-run Ω ? n s) ( s n )
 
 record Buchi { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
     field
         from : ℕ
-        stay : (n : ℕ ) → n > from → aend Ω ( ω-run Ω n S ) ≡ true
+        stay : (n : ℕ ) → n > from → aend Ω ( ω-run Ω ? n S ) ≡ true
 
 open Buchi
        
@@ -28,9 +29,9 @@
 record Muller { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
     field
         next     : (n : ℕ ) → ℕ 
-        infinite : (n : ℕ ) →  aend Ω ( ω-run Ω (n + (next n)) S ) ≡ true 
+        infinite : (n : ℕ ) →  aend Ω ( ω-run Ω ? (n + (next n)) S ) ≡ true 
 
---                       ¬ p
+--                       not p
 --                   ------------>
 --        [] <> p *                 [] <> p 
 --                   <-----------
@@ -53,7 +54,6 @@
 ωa1 : Automaton States3 Bool
 ωa1 = record {
         δ = transition3
-     ;  astart = ts*
      ;  aend = mark1
   }  
 
@@ -65,24 +65,23 @@
 
 flip-seq :  ℕ → Bool
 flip-seq zero = false
-flip-seq (suc n) = negate ( flip-seq n )
+flip-seq (suc n) = not ( flip-seq n )
 
 lemma1 : Buchi ωa1 true-seq 
 lemma1 = record {
         from = zero
       ; stay = lem1
    } where
-      lem1 : ( n :  ℕ ) → n > zero → aend ωa1 (ω-run ωa1 n true-seq ) ≡ true
+      lem1 : ( n :  ℕ ) → n > zero → aend ωa1 (ω-run ωa1 ? n true-seq ) ≡ true
       lem1 zero ()
-      lem1 (suc n) (s≤s z≤n) with ω-run ωa1 n true-seq 
-      lem1 (suc n) (s≤s z≤n) | ts* = refl
-      lem1 (suc n) (s≤s z≤n) | ts = refl
+      lem1 (suc n) (s≤s z≤n) with ω-run ωa1 ? n true-seq 
+      lem1 (suc n) (s≤s z≤n) | ts* = ?
+      lem1 (suc n) (s≤s z≤n) | ts = ?
 
 ωa2 : Automaton States3 Bool
 ωa2 = record {
         δ = transition3
-     ;  astart = ts*
-     ;  aend = λ x → negate ( mark1 x )
+     ;  aend = λ x → not ( mark1 x )
   }  
 
 flip-dec : (n : ℕ ) →  Dec (  flip-seq n   ≡ true )
@@ -90,17 +89,15 @@
 flip-dec n | false = no  λ () 
 flip-dec n | true = yes refl
 
-flip-dec1 : (n : ℕ ) → flip-seq (suc n)  ≡ negate ( flip-seq n )
+flip-dec1 : (n : ℕ ) → flip-seq (suc n)  ≡ ( not ( flip-seq n ) )
 flip-dec1 n = let open ≡-Reasoning in
           flip-seq (suc n )
        ≡⟨⟩
-          negate ( flip-seq n )
+          ( not ( flip-seq n ) )
        ∎
 
-flip-dec2 : (n : ℕ ) → ¬ flip-seq (suc n)  ≡  flip-seq n 
-flip-dec2 n neq with  flip-seq n
-flip-dec2 n () | false 
-flip-dec2 n () | true 
+flip-dec2 : (n : ℕ ) → not flip-seq (suc n)  ≡  flip-seq n 
+flip-dec2 n = ?
 
 
 record flipProperty : Set where
diff -r 7a0634a7c25a -r 3be1afb87f82 agda/turing.agda
--- a/agda/turing.agda	Wed Dec 18 17:34:15 2019 +0900
+++ b/agda/turing.agda	Sat Mar 14 17:34:54 2020 +0900
@@ -1,7 +1,8 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module turing where
 
 open import Level renaming ( suc to succ ; zero to Zero )
-open import Data.Nat hiding ( erase )
+open import Data.Nat -- hiding ( erase )
 open import Data.List
 open import Data.Maybe
 open import Data.Bool using ( Bool ; true ; false ) renaming ( not to negate )
@@ -30,7 +31,7 @@
 -- right        pop     , push SL      
 
 {-# TERMINATING #-}
-move : {Q Σ : Set } → { tone : Σ} → {tδ : Q →  Σ → Q × ( Write  Σ ) ×  Move } → (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
+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  
@@ -41,12 +42,28 @@
 ... | nq , wnone , right   = ( nq ,  LT , ( LH  ∷ RH  ∷ RT ) )
 ... | nq , wnone , mnone   = ( nq , ( LH  ∷ LT ) , (  RH ∷ RT )  )
 {-# TERMINATING #-}
-move-loop : {Q Σ : Set } → {tend :  Q → Bool}   → (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
-move-loop {Q} {Σ} {tend}  q L R with tend q
+move-loop : {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
 ... | true = ( q , L , R )
-... | flase = move-loop {Q} {Σ} {tend} ( proj₁ next ) ( proj₁ ( proj₂ next ) )  ( proj₂  ( proj₂ next ) )
+... | flase = move-loop {Q} {Σ} {tend} {tnone} {tδ} ( proj₁ next ) ( proj₁ ( proj₂ next ) )  ( proj₂  ( proj₂ next ) )
         where
-        next = move {Q} {Σ} {{!!}} {{!!}}  q  L  R 
+        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 )  
 
 record Turing ( Q : Set ) ( Σ : Set  ) 
        : Set  where
@@ -55,21 +72,8 @@
         tstart : Q
         tend : Q → Bool
         tnone :  Σ
-    {-# TERMINATING #-}
-    move0 : (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
-    move0  q L R with tend q
-    ... | true = ( q , L , R )
-    move0 q L [] | false = move0 q  L  ( tnone  ∷ [] ) 
-    move0 q [] R | false = move0 q  ( tnone  ∷ [] )  R 
-    move0 q ( LH  ∷ LT ) ( RH ∷ RT ) | false with  tδ q LH  
-    ... | nq , write x , left  = move0 nq ( RH ∷ x  ∷ LT ) RT 
-    ... | nq , write x , right = move0 nq LT ( x  ∷ RH  ∷ RT ) 
-    ... | nq , write x , mnone = move0 nq ( x  ∷ LT ) (  RH ∷ RT ) 
-    ... | nq , wnone , left    = move0 nq ( RH  ∷ LH  ∷ LT ) RT  
-    ... | nq , wnone , right   = move0 nq  LT ( LH  ∷ RH  ∷ RT ) 
-    ... | nq , wnone , mnone   = move0 nq ( LH  ∷ LT ) (  RH ∷ RT )  
     taccept : List  Σ → ( Q × List  Σ × List  Σ )
-    taccept L = move0 tstart L []
+    taccept L = move0 tend tnone tδ tstart L []
 
 data CopyStates : Set where
    s1 : CopyStates
@@ -81,18 +85,18 @@
 
 
 Copyδ :  CopyStates →  ℕ  → CopyStates × ( Write  ℕ ) × Move 
-Copyδ s1 0  = (H    , wnone       , mnone )
-Copyδ s1 1  = (s2   , write 0 , right )
-Copyδ s2 0  = (s3   , write 0 , right )
-Copyδ s2 1  = (s2   , write 1 , right )
-Copyδ s3 0  = (s4   , write 1 , left )
-Copyδ s3 1  = (s3   , write 1 , right )
-Copyδ s4 0  = (s5   , write 0 , left )
-Copyδ s4 1  = (s4   , write 1 , left )
-Copyδ s5 0  = (s1   , write 1 , right )
-Copyδ s5 1  = (s5   , write 1 , left )
-Copyδ H  _  = (H    , wnone   , mnone )
-Copyδ _  (suc (suc _))      = (H    , wnone       , mnone )
+Copyδ s1 0  = H    , wnone       , mnone 
+Copyδ s1 1  = s2   , write 0 , right 
+Copyδ s2 0  = s3   , write 0 , right 
+Copyδ s2 1  = s2   , write 1 , right 
+Copyδ s3 0  = s4   , write 1 , left 
+Copyδ s3 1  = s3   , write 1 , right 
+Copyδ s4 0  = s5   , write 0 , left 
+Copyδ s4 1  = s4   , write 1 , left 
+Copyδ s5 0  = s1   , write 1 , right 
+Copyδ s5 1  = s5   , write 1 , left 
+Copyδ H  _  = H    , wnone   , mnone 
+Copyδ _  (suc (suc _))      = H    , wnone       , mnone 
 
 copyMachine : Turing CopyStates ℕ
 copyMachine = record {
diff -r 7a0634a7c25a -r 3be1afb87f82 agda/utm.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/utm.agda	Sat Mar 14 17:34:54 2020 +0900
@@ -0,0 +1,234 @@
+module utm where
+
+open import turing
+open import Data.Product
+open import Data.Bool
+open import Data.List
+open import Data.Nat
+
+data utmStates : Set where
+     read0 : utmStates
+     read1 : utmStates
+     read2 : utmStates
+     read3 : utmStates
+     read4 : utmStates
+     read5 : utmStates
+     read6 : utmStates
+     
+     loc0 : utmStates
+     loc1 : utmStates
+     loc2 : utmStates
+     loc3 : utmStates
+     loc4 : utmStates
+     loc5 : utmStates
+     loc6 : utmStates
+     
+     fetch0 : utmStates
+     fetch1 : utmStates
+     fetch2 : utmStates
+     fetch3 : utmStates
+     fetch4 : utmStates
+     fetch5 : utmStates
+     fetch6 : utmStates
+     fetch7 : utmStates
+     
+     print0 : utmStates
+     print1 : utmStates
+     print2 : utmStates
+     print3 : utmStates
+     print4 : utmStates
+     print5 : utmStates
+     print6 : utmStates
+     print7 : utmStates
+     
+     mov0 : utmStates
+     mov1 : utmStates
+     mov2 : utmStates
+     mov3 : utmStates
+     mov4 : utmStates
+     mov5 : utmStates
+     mov6 : utmStates
+     
+     tidy0 : utmStates
+     tidy1 : utmStates
+     halt : utmStates
+
+data utmΣ : Set where
+    ０ : utmΣ
+    １ : utmΣ
+    B : utmΣ
+    * : utmΣ
+    $ : utmΣ
+    ^ : utmΣ
+    X : utmΣ
+    Y : utmΣ
+    Z : utmΣ
+    ＠ : utmΣ
+    b : utmΣ
+
+utmδ :  utmStates →  utmΣ  → utmStates × (Write utmΣ) × Move
+utmδ read0  * = read1 , write * , left
+utmδ read0  x = read0 , write x , right
+utmδ read1  x = read2 , write ＠ , right
+utmδ read2  ^ = read3 , write ^ , right
+utmδ read2  x = read2 , write x , right
+utmδ read3  ０ = read4 , write ０ , left
+utmδ read3  １ = read5 , write １ , left
+utmδ read3  b = read6 , write b , left
+utmδ read4  ＠ = loc0 , write ０ , right
+utmδ read4  x = read4 , write x , left
+utmδ read5  ＠ = loc0 , write １ , right
+utmδ read5  x = read5 , write x , left
+utmδ read6  ＠ = loc0 , write B , right
+utmδ read6  x = read6 , write x , left
+utmδ loc0  ０ = loc0 , write X , left
+utmδ loc0  １ = loc0 , write Y , left
+utmδ loc0  B = loc0 , write Z , left
+utmδ loc0  $ = loc1 , write $ , right
+utmδ loc0  x = loc0 , write x , left
+utmδ loc1  X = loc2 , write ０ , right
+utmδ loc1  Y = loc3 , write １ , right
+utmδ loc1  Z = loc4 , write B , right
+utmδ loc1  * = fetch0 , write * , right
+utmδ loc1  x = loc1 , write x , right
+utmδ loc2  ０ = loc5 , write X , right
+utmδ loc2  １ = loc6 , write Y , right
+utmδ loc2  B = loc6 , write Z , right
+utmδ loc2  x = loc2 , write x , right
+utmδ loc3  １ = loc5 , write Y , right
+utmδ loc3  ０ = loc6 , write X , right
+utmδ loc3  B = loc6 , write Z , right
+utmδ loc3  x = loc3 , write x , right
+utmδ loc4  B = loc5 , write Z , right
+utmδ loc4  ０ = loc6 , write X , right
+utmδ loc4  １ = loc6 , write Y , right
+utmδ loc4  x = loc4 , write x , right
+utmδ loc5  $ = loc1 , write $ , right
+utmδ loc5  x = loc5 , write x , left
+utmδ loc6  $ = halt , write $ , right
+utmδ loc6  * = loc0 , write * , left
+utmδ loc6  x = loc6 , write x , right
+utmδ fetch0  ０ = fetch1 , write X , left
+utmδ fetch0  １ = fetch2 , write Y , left
+utmδ fetch0  B = fetch3 , write Z , left
+utmδ fetch0  x = fetch0 , write x , right
+utmδ fetch1  $ = fetch4 , write $ , right
+utmδ fetch1  x = fetch1 , write x , left
+utmδ fetch2  $ = fetch5 , write $ , right
+utmδ fetch2  x = fetch2 , write x , left
+utmδ fetch3  $ = fetch6 , write $ , right
+utmδ fetch3  x = fetch3 , write x , left
+utmδ fetch4  ０ = fetch7 , write X , right
+utmδ fetch4  １ = fetch7 , write X , right
+utmδ fetch4  B = fetch7 , write X , right
+utmδ fetch4  * = print0 , write * , left
+utmδ fetch4  x = fetch4 , write x , right
+utmδ fetch5  ０ = fetch7 , write Y , right
+utmδ fetch5  １ = fetch7 , write Y , right
+utmδ fetch5  B = fetch7 , write Y , right
+utmδ fetch5  * = print0 , write * , left
+utmδ fetch5  x = fetch5 , write x , right
+utmδ fetch6  ０ = fetch7 , write Z , right
+utmδ fetch6  １ = fetch7 , write Z , right
+utmδ fetch6  B = fetch7 , write Z , right
+utmδ fetch6  * = print0 , write * , left
+utmδ fetch6  x = fetch6 , write x , right
+utmδ fetch7  * = fetch0 , write * , right
+utmδ fetch7  x = fetch7 , write x , right
+utmδ print0  X = print1 , write X , right
+utmδ print0  Y = print2 , write Y , right
+utmδ print0  Z = print3 , write Z , right
+utmδ print1  ^ = print4 , write ^ , right
+utmδ print1  x = print1 , write x , right
+utmδ print2  ^ = print5 , write ^ , right
+utmδ print2  x = print2 , write x , right
+utmδ print3  ^ = print6 , write ^ , right
+utmδ print3  x = print3 , write x , right
+utmδ print4  x = print7 , write ０ , left
+utmδ print5  x = print7 , write １ , left
+utmδ print6  x = print7 , write B , left
+utmδ print7  X = mov0 , write X , right
+utmδ print7  Y = mov1 , write Y , right
+utmδ print7  x = print7 , write x , left
+utmδ mov0  ^ = mov2 , write ^ , left
+utmδ mov0  x = mov0 , write x , right
+utmδ mov1  ^ = mov3 , write ^ , right
+utmδ mov1  x = mov1 , write x , right
+utmδ mov2  ０ = mov4 , write ^ , right
+utmδ mov2  １ = mov5 , write ^ , right
+utmδ mov2  B = mov6 , write ^ , right
+utmδ mov3  ０ = mov4 , write ^ , left
+utmδ mov3  １ = mov5 , write ^ , left
+utmδ mov3  B = mov6 , write ^ , left
+utmδ mov4  ^ = tidy0 , write ０ , left
+utmδ mov5  ^ = tidy0 , write １ , left
+utmδ mov6  ^ = tidy0 , write B , left
+utmδ tidy0  $ = tidy1 , write $ , left
+utmδ tidy0  x = tidy0 , write x , left
+utmδ tidy1  X = tidy1 , write ０ , left
+utmδ tidy1  Y = tidy1 , write １ , left
+utmδ tidy1  Z = tidy1 , write B , left
+utmδ tidy1  $ = read0 , write $ , right
+utmδ tidy1  x = tidy1 , write x , left
+utmδ _  x = halt , write x , mnone
+
+U-TM : Turing utmStates utmΣ
+U-TM = record {
+        tδ = utmδ
+     ;  tstart = read0
+     ;  tend = tend
+     ;  tnone =  b
+  } where
+      tend : utmStates →  Bool
+      tend halt = true
+      tend _ = false
+
+-- Copyδ :  CopyStates →  ℕ  → CopyStates × ( Write  ℕ ) × Move
+-- Copyδ s1 0  = H    , wnone       , mnone
+-- Copyδ s1 1  = s2   , write 0 , right
+-- Copyδ s2 0  = s3   , write 0 , right
+-- Copyδ s2 1  = s2   , write 1 , right
+-- Copyδ s3 0  = s4   , write 1 , left
+-- Copyδ s3 1  = s3   , write 1 , right
+-- Copyδ s4 0  = s5   , write 0 , left
+-- Copyδ s4 1  = s4   , write 1 , left
+-- Copyδ s5 0  = s1   , write 1 , right
+-- Copyδ s5 1  = s5   , write 1 , left
+-- Copyδ H  _  = H    , wnone   , mnone
+-- Copyδ _  (suc (suc _))      = H    , wnone       , mnone
+
+Copyδ-encode : List utmΣ
+Copyδ-encode = 
+       ０  ∷ ０  ∷ １  ∷ ０  ∷  １ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ ０ ∷   -- s1 0  = H    , wnone       , mnone
+  *  ∷ ０  ∷ ０  ∷ １  ∷ １  ∷  ０ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ １ ∷   -- s1 1  = s2   , write 0 , right
+  *  ∷ ０  ∷ １  ∷ ０  ∷ ０  ∷  ０ ∷ １ ∷ １ ∷ ０ ∷ ０ ∷ １ ∷   -- s2 0  = s3   , write 0 , right
+  *  ∷ ０  ∷ １  ∷ ０  ∷ １  ∷  ０ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷   -- s2 1  = s2   , write 1 , right
+  *  ∷ ０  ∷ １  ∷ １  ∷ ０  ∷  １ ∷ ０ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷   -- s3 0  = s4   , write 1 , left
+  *  ∷ ０  ∷ １  ∷ １  ∷ １  ∷  ０ ∷ １ ∷ １ ∷ １ ∷ ０ ∷ １ ∷   -- s3 1  = s3   , write 1 , right
+  *  ∷ １  ∷ ０  ∷ ０  ∷ ０  ∷  １ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷   -- s4 0  = s5   , write 0 , left
+  *  ∷ １  ∷ ０  ∷ ０  ∷ １  ∷  １ ∷ ０ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷   -- s4 1  = s4   , write 1 , left
+  *  ∷ １  ∷ ０  ∷ １  ∷ ０  ∷  ０ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ １ ∷   -- s5 0  = s1   , write 1 , right
+  *  ∷ １  ∷ ０  ∷ １  ∷ １  ∷  １ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ ０ ∷   -- s5 1  = s5   , write 1 , left
+  []  
+      
+
+input-encode : List utmΣ
+input-encode =  １  ∷ １  ∷ ０  ∷ ０  ∷  ０ ∷ []  
+
+input+Copyδ : List utmΣ
+input+Copyδ = ( $  ∷ ０  ∷ ０  ∷  ０ ∷  ０ ∷  * ∷  [] ) -- start state
+        ++   Copyδ-encode
+        ++ ( $ ∷ ^ ∷ input-encode )
+
+utm-test1 : utmStates × ( List  utmΣ ) × ( List  utmΣ )
+utm-test1 = Turing.taccept U-TM  input+Copyδ
+
+utm-test2 : ℕ  → utmStates × ( List  utmΣ ) × ( List  utmΣ )
+utm-test2 n  = loop n (Turing.tstart U-TM) input+Copyδ []
+  where
+        loop :  ℕ → utmStates → ( List  utmΣ ) → ( List  utmΣ ) → utmStates × ( List  utmΣ ) × ( List  utmΣ )
+        loop zero q L R = ( q , L , R )
+        loop (suc n) q L R with  move {utmStates} {utmΣ} {０} {utmδ} q L R
+        ... | nq , nL , nR = loop n nq nL nR
+
+t1 = utm-test2 10