class Cslib.Automata.ωAcceptor (A : Type u) (Symbol : outParam (Type v)) : Type (max u v)

An ωAcceptor is a machine that recognises infinite sequences of symbols.

• Accepts (a : A) (xs : ωSequence Symbol) : Prop

  Predicate that establishes whether a string xs is accepted.

def Cslib.Automata.ωAcceptor.language {Symbol : Type v} {A : Type u_1} [ωAcceptor A Symbol] (a : A) : ωLanguage Symbol

The language of an ωAcceptor is the set of sequences it Accepts.

Equations

• Cslib.Automata.ωAcceptor.language a = { toSet := {xs : Cslib.ωSequence Symbol | Cslib.Automata.ωAcceptor.Accepts a xs} }

@[simp]

theorem Cslib.Automata.ωAcceptor.mem_language {Symbol : Type v} {A : Type u_1} [ωAcceptor A Symbol] (a : A) (xs : ωSequence Symbol) : xs ∈ language a ↔ Accepts a xs

A string is in the language of an acceptor iff the acceptor accepts it.