--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/automaton-in-agda/src/extended-automaton.agda	Sun Mar 12 22:49:59 2023 +0900
@@ -0,0 +1,80 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+module extended-automaton where
+
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Nat -- hiding ( erase )
+open import Data.List
+open import Data.Maybe hiding ( map )
+-- 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 Level renaming ( suc to succ ; zero to Zero )
+open import Data.Product hiding ( map )
+open import logic 
+
+record Automaton ( Q : Set ) ( Σ : Set  ) : Set  where
+    field
+        δ : Q → Σ → Q
+        aend : Q → Bool
+
+open Automaton 
+
+accept : { Q : Set } { Σ : Set  }
+    → Automaton Q  Σ
+    → Q
+    → List  Σ → Bool
+accept M q [] = aend M q
+accept M q ( H  ∷ T ) = accept M ( δ M q H ) T
+
+NAutomaton : ( Q : Set ) ( Σ : Set  ) → Set  
+NAutomaton Q Σ = Automaton ( Q → Bool ) Σ
+
+Naccept : { Q : Set } { Σ : Set  } 
+    → Automaton (Q → Bool)  Σ
+    → (exists : ( Q → Bool ) → Bool)
+    → (Nstart : Q → Bool) → List  Σ → Bool
+Naccept M exists sb []  = exists ( λ q → sb q /\ aend M sb )
+Naccept M exists sb (i ∷ t ) = Naccept M exists (λ q →  exists ( λ qn → (sb qn /\ ( δ M sb i q )  ))) t
+
+PDA : ( Q : Set ) ( Σ : Set  ) → Set  
+PDA Q Σ = Automaton ( List Q  ) Σ
+
+data Write   (  Σ : Set  ) : Set  where
+   write   : Σ → Write  Σ
+   wnone   : Write  Σ
+   --   erase write tnone
+
+data Move : Set  where
+   left   : Move  
+   right  : Move  
+   mnone  : Move  
+
+record OTuring ( Q : Set ) ( Σ : Set  ) 
+       : Set  where
+    field
+        tδ : Q →  Σ → Q × ( Write  Σ ) ×  Move 
+        tstart : Q
+        tend : Q → Bool
+        tnone :  Σ
+    taccept : List  Σ → ( Q × List  Σ × List  Σ )
+    taccept L = ?
+
+open import bijection 
+
+b0 : ( Q : Set ) ( Σ : Set  ) → Bijection (List Q) (( Q × ( Write  Σ ) ×  Move  ) ∧ ( Q × List  Σ × List  Σ ))
+b0 = ?
+
+Turing : ( Q : Set ) ( Σ : Set  ) → Set  
+Turing Q Σ = Automaton ( List Q  ) Σ
+
+NDTM : ( Q : Set ) ( Σ : Set  ) → Set  
+NDTM Q Σ = Automaton ( List Q → Bool ) Σ
+
+UTM : ( Q : Set ) ( Σ : Set  ) → Set  
+UTM Q Σ = Automaton ( List Q ) Σ
+
+SuperTM : ( Q : Set ) ( Σ : Set  ) → Set  
+SuperTM Q Σ = Automaton ( List Q ) Σ
+
+
+