Formalizing

Our goal is to build a finite automaton called . We follow Hopcroft and Ullman exactly, taking the set of states to be , defining , taking [nil] as the start state and defining exactly when . In the next section we refer to this automaton as .

To show that as defined is a finite automaton accepting , we need to show that is well defined on the equivalence classes, i.e. if then . Since and , we need to know that . This is true iff . But this is an instance of the definition of since . Here is the formal statement followed by a compressed proof. In the compressed proof we use ...assertion... to indicate that an assertion was cut into the proof; that assertion is the goal of the following line. Direct Computation is key to the proof, and we display its main step by writing

1.
2.
3. is an Equivalence over
4.
5.
6.

by SidePF
7. g
8.

.....assertion .....

by SidePF
9.
10. l
accepts
accepts
.....assertion .....
accepts
by DirComp accepts


by DirComp ....
11.
12.
13.

by DirComp