Thank you so much for answering my question. Its intereseting to see that
1) (q0 <-> a | a & Xq0) & (q1 <-> a | ¬a & Xq1) & (q2 <-> q1 | q0 & Xq2) & !q2 - why is !q2 added in the end?
2) in equivalence 4 (q0 <-> a | a & Xq0) is written as in next line (q0 <-> 0). I m considering this state is a self loop and cannot understand why it is negated to 0.