Quotient automaton

In computer science, in particular in formal language theory, a quotient automaton can be obtained from a given nondeterministic finite automaton by joining some of its states. The quotient recognizes a superset of the given automaton; in some cases, handled by the Myhill–Nerode theorem, both languages are equal.
Formal definition.
A (nondeterministic) finite automaton is a quintuple "A" = ⟨"Σ", "S", "s"0, "δ", "S"f⟩, where:
A string "a"1..."a""n" ∈ "Σ"* is recognized by "A" if there exist states "s"1, ..., "s""n" ∈ "S" such that ⟨"s""i"-1,"a""i","s""i"⟩ ∈ "δ" for "i"=1...,"n", and "s""n" ∈ "S"f. The set of all strings recognized by "A" is called the language recognized by "A"; it is denoted as "L"("A").
For an equivalence relation ≈ on the set "S" of "A"’s states, the quotient automaton "A"/≈ = ⟨"Σ", "S"/≈, ["s"0], "δ"/≈, "S"f/≈⟩ is defined by
The process of computing "A"/≈ is also called factoring "A" by ≈.
Example.
For example, the automaton A shown in the first row of the table is formally defined by 
It recognizes the finite set of strings { 1, 10, 100 }; this set can also be denoted by the regular expression "1+10+100".
The relation (≈) = { ⟨a,a⟩, ⟨a,b⟩, ⟨b,a⟩, ⟨b,b⟩, ⟨c,c⟩, ⟨c,d⟩, ⟨d,c⟩, ⟨d,d⟩ }, more briefly denoted as a≈b,c≈d, is an equivalence relation on the set {a,b,c,d} of automaton A’s states.
Building the quotient of A by that relation results in automaton C in the third table row; it is formally defined by 
It recognizes the finite set of all strings composed of arbitrarily many 1s, followed by arbitrarily many 0s, i.e. { ε, 1, 10, 100, 1000, ..., 11, 110, 1100, 11000, ..., 111, ... }; this set can also be denoted by the regular expression "1*0*".
Informally, C can be thought of resulting from A by glueing state onto state b, and glueing state c onto state d.
The table shows some more quotient relations, such as B = A/a≈b, and D = C/a≈c.