module regop where

open import automaton

-- open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat
open import Data.List
open import Data.Maybe
open import Data.Product
open import Data.Bool using ( Bool ; true ; false ; _∧_ )
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Nullary using (¬_; Dec; yes; no)


union : {Q1 Q2  Σ : Set } → ( M1 : Automaton Q1  Σ) ( M2 : Automaton Q2  Σ) → Automaton (Q1 × Q2) Σ
union {Q1} {Q2} {Σ} M1 M2 = record {
        δ =  δ
      ; astart = astart
      ; aend =  aend
    } where
        δ : (Q1 × Q2) → Σ → (Q1 × Q2)
        δ = {!!}
        astart : (Q1 × Q2)
        astart = {!!}
        aend : (Q1 × Q2) → Bool
        aend = {!!}

data  _∨_  (A B : Set) : Set where
   p1 : A → A ∨ B
   p2 : B → A ∨ B

union← : {Q1 Q2  Σ : Set } → ( M1 : Automaton Q1  Σ) ( M2 : Automaton Q2  Σ) →
     ∀ ( s : List Σ ) → accept ( union M1 M2 ) s ≡ true → ( ( accept M1 s ≡ true ) ∨ ( accept M2 s ≡ true) )
union← {Q1} {Q2} {Σ} M1 M2 s eq = {!!}