Module transition.
  Definition t b s := b ~> relation.binary.t s.
  Definition denote {b s : universe.sort}(tr : t b s) : regexp.abstract.automata.transition.t b s :=
    function.denote (function.map relation.denote tr).

End transition.

Record NFA b s := { trans : transition.t b s;
                    start : subset.t s;
                    final : subset.t s;
  }.

Arguments trans {b s}.
Arguments start {b s}.
Arguments final {b s}.

Definition denote {b s : universe.sort}(mac : NFA b s) : abstract.automata.NFA (universe.denote b) (universe.denote s)
  := {|
    abstract.automata.trans := transition.denote (trans mac);
    abstract.automata.start := subset.denote (start mac);
    abstract.automata.final := subset.denote (final mac)
  |}.

Definition accept {b s : universe.sort}(mac : NFA b s) : lang (universe.denote b) := abstract.automata.accept (denote mac).