Mercurial > hg > Members > kono > Proof > automaton1
view nfa-lib.agda @ 8:894feefc3084
subset construction lemma
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 15 Nov 2020 11:30:49 +0900 |
parents | nfa.agda@8f1828ec8d1b |
children | 8a6660c5b1da |
line wrap: on
line source
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 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 (λ ()) 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 nfa13rs1 : example136-1 nfa13rt1 = nfa136trace ( s0 ∷ s1 ∷ s0 ∷ s0 ∷ [] ) nfa13rs1