DFA membership, emptiness, finiteness, equivalence, and containment are decidable

Membership is decidable by simulating the DFA on the finitely many letters of the input word and checking, via [L1], whether the final state is accepting.

Emptiness is decidable by a graph search from the start state through the finite transition graph: by [L1], the language is empty exactly when no accepting state is reachable.

Finiteness is decidable by restricting to states that are reachable from the start state and can themselves reach an accepting state. If that finite subgraph contains a directed cycle, then one may loop around the cycle arbitrarily many times before taking a path to acceptance, producing infinitely many accepted words. If it contains no directed cycle, then every accepting run has bounded length, so only finitely many words are accepted.

Given DFA's $D_1,D_2$, use [L3] to complement either machine and then [L2] to build DFA's for the two differences $L(D_1)\setminus L(D_2)$ and $L(D_2)\setminus L(D_1)$ and for their union. By [A1], that union is the symmetric difference, so $D_1$ and $D_2$ are equivalent exactly when the resulting DFA has empty language. Step 1.2 therefore decides equivalence.

The same constructions give a DFA for $L(D_1)\setminus L(D_2)$. By [A1], the containment $L(D_1)\subseteq L(D_2)$ holds exactly when this difference language is empty, so step 1.2 also decides containment.

Steps 1.1, 1.2, 2.1, 2.2, and 3.1 decide membership, emptiness, finiteness, equivalence, and containment respectively.