module nfa-lib where
open import Level renaming ( suc to Suc ; zero to Zero )

open import Relation.Binary.PropositionalEquality 
open import Data.List
open import Relation.Nullary
open import automaton
open import logic

open import nfa
open NAutomaton

Q3List : List Q3
Q3List = q₁ ∷ q₂ ∷ q₃ ∷ []

decs136 : (q : Q3) → Dec (start136 q)
decs136 q₁ = yes refl
decs136 q₂ = no (λ ())
decs136 q₃ = no (λ ())

dect136 : (x : Σ2)  → (nq q : Q3)  →  Dec (Nδ nfa136 nq x q) 
dect136 s0 q₁ q₁ = yes d1
dect136 s0 q₁ q₂ = no (λ ())
dect136 s0 q₁ q₃ =  no (λ ())
dect136 s0 q₂ q₁ =  no (λ ())
dect136 s0 q₂ q₂ =  yes d2
dect136 s0 q₂ q₃ =  yes d3
dect136 s0 q₃ q₁ =  yes d5
dect136 s0 q₃ q₂ =  no (λ ())
dect136 s0 q₃ q₃ =  no (λ ())
dect136 s1 q₁ q₁ =  no (λ ())
dect136 s1 q₁ q₂ =  yes d0
dect136 s1 q₁ q₃ =  no (λ ())
dect136 s1 q₂ q₁ =  no (λ ())
dect136 s1 q₂ q₂ =  no (λ ())
dect136 s1 q₂ q₃ =  yes d4
dect136 s1 q₃ q₁ =  no (λ ())
dect136 s1 q₃ q₂ =  no (λ ())
dect136 s1 q₃ q₃ =  no (λ ())

FindQ3 : FindQ Q3 exists-in-Q3
FindQ3 = record { create = create ;  found = found ; exists = exists } where
    create :  {P : Q3 → Set} (q : Q3) → P q → exists-in-Q3 P
    create q₁ p = qe1 p
    create q₂ p = qe2 p
    create q₃ p = qe3 p
    found : {P : Q3 → Set} → exists-in-Q3 P → Q3
    found (qe1 x) = q₁
    found (qe2 x) = q₂
    found (qe3 x) = q₃
    exists : {P : Q3 → Set} (n : exists-in-Q3 P) → P (found n)
    exists (qe1 x) = x
    exists (qe2 x) = x
    exists (qe3 x) = x

open import Data.Empty
open import Relation.Nullary
open _∧_

next136 : (qs : Q3 → Set) → ((q : Q3) → Dec (qs q)) → (x : Σ2) (q : Q3) →
    Dec (exists-in-Q3 (λ nq → qs nq ∧ Nδ nfa136 nq x q))
next136 qs dec x q = ne0 where
   ne1 : (q : Q3) → (x : Σ2) → Dec (qs q₁) → Dec (Nδ nfa136 q₁ x q) → Dec (qs q₁ ∧ Nδ nfa136 q₁ x q)
   ne1 q x (no n) _ = no (λ not → n (proj1 not))
   ne1 q x _ (no n) = no (λ not → n (proj2 not))
   ne1 q x (yes y0) (yes y1) = yes [ y0 , y1 ]
   ne2 : (q : Q3) → (x : Σ2) → Dec (qs q₂) → Dec (Nδ nfa136 q₂ x q) → Dec (qs q₂ ∧ Nδ nfa136 q₂ x q)
   ne2 q x (no n) _ = no (λ not → n (proj1 not))
   ne2 q x _ (no n) = no (λ not → n (proj2 not))
   ne2 q x (yes y0) (yes y1) = yes [ y0 , y1 ]
   ne3 : (q : Q3) → (x : Σ2) → Dec (qs q₃) → Dec (Nδ nfa136 q₃ x q) → Dec (qs q₃ ∧ Nδ nfa136 q₃ x q)
   ne3 q x (no n) _ = no (λ not → n (proj1 not))
   ne3 q x _ (no n) = no (λ not → n (proj2 not))
   ne3 q x (yes y0) (yes y1) = yes [ y0 , y1 ]
   ne0 : Dec (exists-in-Q3 (λ nq → qs nq ∧ Nδ nfa136 nq x q))
   ne0 with ne1 q x (dec q₁) (dect136 x q₁ q)
   ... | yes y = yes ( qe1 y)
   ... | no n with ne2 q x (dec q₂) (dect136 x q₂ q)
   ... | yes y2 = yes (qe2 y2)
   ... | no n2 with ne3 q x (dec q₃) (dect136 x q₃ q)
   ... | yes y3 = yes (qe3 y3)
   ... | no n3 = no ne4 where
      ne4 : ¬ exists-in-Q3 (λ nq → qs nq ∧ transition136 nq x q)
      ne4 (qe1 x) = n x
      ne4 (qe2 x) = n2 x
      ne4 (qe3 x) = n3 x

nfa136trace : (input : List Σ2 ) → naccept exists-in-Q3 nfa136 start136 input → List (List Q3)
nfa136trace x a = ntrace exists-in-Q3 nfa136 start136 x a decs136 next136 Q3List

postulate
   nfa13rs0 : example136-0 
   nfa13rs1 : example136-1 
   nfa13rs2 : example136-2 

nfa13rt0 = nfa136trace ( s0 ∷ []  ) nfa13rs0
nfa13rt1 = nfa136trace ( s0  ∷ s1  ∷ s0 ∷ s0 ∷ [] ) nfa13rs1
nfa13rt2 = nfa136trace ( s1  ∷ s0  ∷ s1 ∷ s0 ∷ s1 ∷ [] ) nfa13rs2