--- a/automaton-in-agda/src/pushdown.agda	Mon Jan 03 18:50:01 2022 +0900
+++ b/automaton-in-agda/src/pushdown.agda	Thu Jan 06 07:27:52 2022 +0900
@@ -10,6 +10,7 @@
 open import Level renaming ( suc to succ ; zero to Zero )
 -- open import Data.Product
 open import logic
+open import automaton
 
 
 data PushDown   (  Γ : Set  ) : Set  where
@@ -46,6 +47,23 @@
     ... | ⟪ nq , none ⟫    = paccept nq T (SH ∷ ST)
     ... | ⟪ nq , push ns ⟫ = paccept nq T ( ns  ∷  SH ∷ ST )
 
+record PDA ( Q : Set ) ( Σ : Set  ) ( Γ : Set  )
+       : Set  where
+    field
+        automaton : Automaton Q Σ
+        pδ : Q →  PushDown  Γ 
+    open Automaton
+    paccept : (q : Q ) ( In : List  Σ ) ( sp : List   Γ ) → Bool
+    paccept q [] [] = aend automaton q 
+    paccept q (H  ∷ T) [] with pδ  (δ automaton q H) 
+    paccept q (H ∷ T) [] | pop     = paccept (δ automaton q H) T []
+    paccept q (H ∷ T) [] | none    = paccept (δ automaton q H) T []
+    paccept q (H ∷ T) [] | push x  = paccept (δ automaton q H) T (x  ∷ [] )
+    paccept q [] (_ ∷ _ ) = false
+    paccept q ( H  ∷ T ) ( SH  ∷ ST ) with pδ (δ automaton q H) 
+    ... | pop      = paccept (δ automaton q H) T ST
+    ... | none     = paccept (δ automaton q H) T (SH ∷ ST)
+    ... | push ns  = paccept (δ automaton q H) T ( ns  ∷  SH ∷ ST )
 
 data  States0   : Set  where
    sr : States0
@@ -64,10 +82,32 @@
         pδ sr i0 _ = ⟪ sr , push sr ⟫
         pδ sr i1 _ = ⟪ sr , pop  ⟫ 
 
+data  States2   : Set  where
+   ph1 : States2
+   ph2 : States2
+   phf : States2
+
+pnnp : PDA States2 In2 States2
+pnnp = record {
+         automaton = record { aend = aend ; δ = δ }
+       ; pδ  = pδ
+   } where
+        δ : States2 → In2 → States2
+        δ ph1 i0 = ph1
+        δ ph1 i1 = ph2
+        δ ph2 i1 = ph2
+        δ _ _ = phf
+        aend : States2 → Bool
+        aend ph2 = true
+        aend _ = false
+        pδ  : States2 → PushDown States2
+        pδ ph1 = push ph1 
+        pδ ph2 = pop   
+        pδ phf = none   
+
 data  States1   : Set  where
    ss : States1
    st : States1
-
 pn1 : PushDownAutomaton States1 In2 States1
 pn1 = record {
          pδ  = pδ