# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1605240236 -32400
# Node ID 7399aae907fcff581107f40f02275c99f6458268
# Parent  9615a94b18cadf117168be7f50121942de295f6d
...

diff -r 9615a94b18ca -r 7399aae907fc automaton.agda
--- a/automaton.agda	Thu Nov 12 11:45:34 2020 +0900
+++ b/automaton.agda	Fri Nov 13 13:03:56 2020 +0900
@@ -11,7 +11,6 @@
   field
     δ : Q → Σ → Q
     F : Q → Set 
-    exists : (Q → Set) → Set
 
 open Automaton
 
@@ -58,10 +57,10 @@
   qe3 :  P q₃ → exists-in-Q3 P
 
 a16 : Automaton Q3 Σ2
-a16 = record { δ = δ16 ; F = λ q → a16end q ; exists = exists-in-Q3 }
+a16 = record { δ = δ16 ; F = λ q → a16end q }
 
 a16' : Automaton Q3 Σ2
-a16' = record { δ = δ16' ; F = λ q → q ≡ q₂ ; exists = exists-in-Q3 }
+a16' = record { δ = δ16' ; F = λ q → q ≡ q₂ }
 
 --
 --  ∷  →   ∷ →   ∷ →  []
@@ -202,7 +201,7 @@
 δ19 q₃ _ = q₁
 
 a19 : Automaton Q3 Σ2
-a19 = record { δ = δ19 ; F = λ q → q ≡ q₁ ; exists = exists-in-Q3 }
+a19 = record { δ = δ19 ; F = λ q → q ≡ q₁ }
 
 --  input is empty or ends in s0
 
diff -r 9615a94b18ca -r 7399aae907fc nfa.agda
--- a/nfa.agda	Thu Nov 12 11:45:34 2020 +0900
+++ b/nfa.agda	Fri Nov 13 13:03:56 2020 +0900
@@ -3,6 +3,7 @@
 
 open import Relation.Binary.PropositionalEquality 
 open import Data.List
+open import Relation.Nullary
 open import automaton
 open import logic
 
@@ -10,21 +11,22 @@
        : Set (Suc n) where
     field
           Nδ : Q → Σ → Q → Set
-          NF  :  Q → Set
-          Nexists  : (Q → Set)  → Set
+          NF : Q → Set
+          Nexists : (Q → Set)  → Set
 
 open NAutomaton
 
+
 naccept : {n : Level} {Q : Set n} {Σ : Set} → NAutomaton Q Σ → (Q → Set) → List Σ → Set
 naccept {n} {Q} {Σ} nfa qs [] = Nexists nfa (λ q → qs q ∧ NF nfa q )
 naccept {n} {Q} {Σ} nfa qs (x ∷ input) = 
     Nexists nfa (λ q → qs q ∧ (naccept nfa (Nδ nfa q x) input ))
 
-ntrace : {n  : Level} {Q : Set n} {Σ : Set } → (NFA : NAutomaton Q Σ) → (start : Q → Set ) → (input : List Σ ) → naccept NFA start input
-     → ((Q → Set) → List Q)
-     → List (List Q)
-ntrace {n} {Q} {Σ} A q [] a list = list q ∷ []
-ntrace {n} {Q} {Σ} A q (x ∷ t) a list = list q ∷ ( ntrace A {!!} t {!!} list )
+record DecStates {n : Level} ( Q : Set n ) : Set (Suc n) where
+    field
+          QList   : List Q 
+          QDec  : (P : Q → Set) → (q : Q) → Dec (P q)
+
 
 data transition136 : Q3  → Σ2  → Q3 → Set  where
     d0 : transition136 q₁ s1 q₂ 
@@ -46,6 +48,19 @@
 
 example136-2 = naccept nfa136 start136 ( s1  ∷ s0  ∷ s1 ∷ s0 ∷ s1 ∷ [] )
 
+nfa136-P : (q : Q3 → Set) → (input : List Σ2 ) → Dec (naccept nfa136 q input )
+nfa136-P q [] = {!!}
+nfa136-P q (x ∷ t) = {!!}
+
+Q3List : List Q3
+Q3List = q₁ ∷ q₂ ∷ q₃ ∷ []
+
+nfa136trace : (q : Q3 → Set) → (input : List Σ2 ) → naccept nfa136 q input → List (List Q3)
+nfa136trace q [] (qe1 [ proj1 , refl ]) = {!!}
+nfa136trace q (x ∷ t) (qe1 [ proj1 , a ]) = {!!}
+nfa136trace q (x ∷ t) (qe2 [ proj1 , a ]) = {!!}
+nfa136trace q (x ∷ t) (qe3 [ proj1 , a ]) = {!!}
+
 --
 -- ((Q → Set)  → Set) → ((Q → Set) → Set) → Set
 --
@@ -58,7 +73,6 @@
 subset-construction {n} {Q} { Σ}  NFA = record {
         δ = λ qs x qs → Nexists NFA (λ q → Nδ NFA q x qs )
      ;  F = λ qs → Nexists NFA ( λ q → NF NFA q )
-     ;  exists = Nexists→exits NFA   -- what this means?
    } 
 
 subset-construction-lemma→ : { Q : Set } { Σ : Set  }   →   
@@ -81,11 +95,11 @@
 open Automaton
 open import Data.Empty 
 
-Concat-exists : {n : Level}  {Σ : Set} → (A B : RegularLanguage {n} Σ ) →  (states A ∨ states B → Set) → Set
-Concat-exists {n} {Σ} A B P = exists (automaton A) (λ q → P (case1 q)) ∨ exists (automaton B) (λ q → P (case2 q))
+-- Concat-exists : {n : Level}  {Σ : Set} → (A B : RegularLanguage {n} Σ ) →  (states A ∨ states B → Set) → Set
+-- Concat-exists {n} {Σ} A B P = exists (automaton A) (λ q → P (case1 q)) ∨ exists (automaton B) (λ q → P (case2 q))
 
 Concat-NFA : {n : Level}  {Σ : Set} → (A B : RegularLanguage {n} Σ ) → NAutomaton (states A ∨ states B) Σ 
-Concat-NFA {n} {Σ} A B = record { Nδ = δnfa ; NF = nend  ; Nexists = Concat-exists A B } 
+Concat-NFA {n} {Σ} A B = record { Nδ = δnfa ; NF = nend  ; Nexists = {!!} }
    module Concat-NFA where
        data δnfa : states A ∨ states B → Σ → states A ∨ states B → Set where
          a-case   : {q : states A}  {i : Σ } → δnfa ( case1 q) i (case1 (δ (automaton A) q i))
diff -r 9615a94b18ca -r 7399aae907fc regular-language.agda
--- a/regular-language.agda	Thu Nov 12 11:45:34 2020 +0900
+++ b/regular-language.agda	Fri Nov 13 13:03:56 2020 +0900
@@ -63,12 +63,6 @@
 isRegular : {n : Level} {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage {n} Σ ) → Set (Suc Zero)
 isRegular A x r = A x ≡ contain r x 
 
---
---   (states A × states B → Set) → ( states A → Set ) → ( states B → Set )  → Set
---
-exists-Union : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → (states A × states B → Set) → Set
-exists-Union A B Pab = exists (automaton A) (λ qa → exists (automaton B) (λ qb → Pab (qa , qb)) )
-
 M-Union : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → RegularLanguage Σ
 M-Union {n} {Σ} A B = record {
        states =  states A × states B
@@ -76,7 +70,6 @@
      ; automaton = record {
              δ = λ q x → ( δ (automaton A) (proj₁ q) x , δ (automaton B) (proj₂ q) x )
            ; F = λ q → ( F (automaton A) (proj₁ q) ∨ F (automaton B) (proj₂ q) )
-           ; exists = exists-Union A B
         }
    }