Returns true if the language of a1 is a subset of the language of a2. Both automata must be determinized and must have no dead states.
a1
a2
Complexity: quadratic in number of states.